# Role of Term Constants in Simply Typed Lambda Calculus

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?

• I agree that this is not a research-level question. And I think that the Wikipedia article is a bit misleading, the "real deal" is the STLC without constants. – Damiano Mazza Mar 22 '14 at 20:04
• Whether this stays here or not, am I to draw the conclusion that STLC does not introduce constants to LC but they are a form of "syntactic sugar" that could be used in either? – BlackVegetable Mar 22 '14 at 22:35
• @BlackVegetable: absolutely. The essential difference between the STLC and the pure LC is in the typing discipline, certainly not in adding or removing constants. – Damiano Mazza Mar 22 '14 at 22:40
• Alright, that makes perfect sense. Someone needs to fix that Wikipedia article which shows it as intrinsically adding the constant term! – BlackVegetable Mar 22 '14 at 22:42

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.

I also don't like the explanation of constants in the article, but there are reasons for them.

You can certainly consider constants also in untyped lambda-calculus, and the behavior of constants is not generally interesting — as long as you allow them to be there.

However, most constants are typically redundant in untyped lambda-calculus, because any datatype can be Church-encoded. A typed variant of Church-encoding (called Böhm-Berarducci encoding, often also called Church encoding) is also available in polymorphic lambda-calculus (System F) and calculi containing it (TAPL*, Sec. 24.3).

However, Church encoding does not really work in STLC: if you try to write 2 as λ zero succ . succ (succ zero), you'll find you need to fix in advance what type τ to use for the type annotations λ zero : τ. succ : τ → τ . succ (succ zero). Once you fix τ (say to Bool, assuming you have that type), you can only compute booleans with it, not anything else (in particular, not even numbers).

There's also another problem: unlike in System F, pure STLC the set of types is empty, as one can see by examining the definition of types (TAPL, Figure 9-1):

T ::= T → T

Since there is no base case, one can construct no finite type.

This is a different problem, and to solve it it is enough to add a set of uninterpreted base types. However, to make the calculus useful, you need to allow at least for arbitrary uninterpreted constants. Theoretically speaking, this is not a small problem in theory — every interesting bit of proofs about STLC can be done without base types, but all the statements are also vacuously true since no typed terms exist (because there is no type to fill in the type annotations).

*TAPL is the book Types and Programming Languages by Benjamin Pierce, a standard reference nowadays in its field.