Cheap and Secure Web Hosting Provider : See Now

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

, ,
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:

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?

#### 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.