Cheap and Secure Web Hosting Provider : See Now

[Solved]: Role of Term Constants in Simply Typed Lambda Calculus

, , No Comments
Problem Detail: 

In the Wikipedia article on Simply Typed Lambda Calculus (among other places), there is a notion of a "term constant". This is particularly notable in the production grammar given:

enter image description here

In this production grammar, the c is the term constant. I am new to the simply typed variant of lambda calculus -- I do not understand what role this constant plays in the overall computations of STLC. Can anyone give some examples of how the term constant is used and explain its general purpose?

Asked By : BlackVegetable

Answered By : Martin Berger

As per Sam's request, I rephrase my comment as an answer.

Constants play an important role in λ-calculi (not just the simply typed variant).

  • They are often convenient: even though we can usually represent our target data using $\lambda$-terms without constants this tends to be unwieldy. For example integers directly by some variant of an unary encoding, e.g. the Church encoding has $$\lambda g x. \underbrace{g ( g ( ... g ( g\ x ) .. ) ) }_{n}$$ as representation of $n$. That leads to cumbersome, unreadable terms. With constants we can do arithmetic with 0,1,2,..., and +,−,∗,...

  • In a typed calculus, we need constructors for types, and constants play this rule. E.g. 0,1,2,..., or +,−,∗,... for the type of integers, true,false... or ∨,∧ for booleans etc.

Note that the STLC was born with constants : Church's original formulation contains constants $N_{oo}$, $A_{ooo}$, $\Pi_{o(o\alpha)}$ as well as $\iota_{\alpha(o\alpha)}$, representing negation, disjunction, universal quantification and the selection operator, respectively.

Best Answer from StackOverflow

Question Source :

3.2K people like this

 Download Related Notes/Documents


Post a Comment

Let us know your responses and feedback