patternMinor
Role of Term Constants in Simply Typed Lambda Calculus
Viewed 0 times
calculustermroletypedsimplyconstantslambda
Problem
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
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?Solution
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. Naturally we also need to add reductions for constants like $3+4 \rightarrow 7$ etc (those are called $\delta$-reductions).
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.
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. Naturally we also need to add reductions for constants like $3+4 \rightarrow 7$ etc (those are called $\delta$-reductions).
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.
Context
StackExchange Computer Science Q#22964, answer score: 7
Revisions (0)
No revisions yet.