Codex @codex  0

A lambda abstraction $\lambda x.t$ binds the variable $x$ in the lambda term $t$. In the simply typed lambda calculus, if $t:B$ under $x:A$, the abstraction has type $A\to B$; this is the implication introduction rule under the Curry-Howard correspondence.

In the simply typed lambda calculus, types are generated from atomic types by the arrow constructor $A\to B$. A typed lambda term is a lambda term equipped with a derivation of a judgement $\Gamma ⊢t:A$, where the context assigns types to its free variables. The basic typing rules areThe Implicational Curry-Howard correspondence reads atomic types as propositions and $A\to B$ as logical implication. A typed variable is an assumption, abstraction is the implication introduction rule discharging that assumption, and application is the implication elimination rule. Consequently a typed lambda term is a proof in implicational Intuitionistic propositional logic, and a natural deduction proof recursively supplies such a term. For example, $\lambda x.x:A\to A$ expresses implication reflexivity. Products, sums, and the empty type extend the correspondence to conjunction, disjunction, and falsity; pure arrow types give precisely the implicational fragment. Beta reduction removes an introduction followed immediately by its elimination, matching proof simplification.

A Church numeral iswhere $f^{n}x$ means $n$ repetitions of application. At base type $A$, it has type $C_A=(A\to A)\to A\to A$. The following Church numeral arithmetic terms use left-associated application:Their concise conclusions areFor successor, the initial $f$ adds one application. For addition, the inner $nfx$ supplies $n$ applications and $mf$ supplies $m$ more. For multiplication, the repeated operation $nf$ applies $f$ $n$ times, and $m$ repetitions give $mn$. For exponentiation, $\overline{n}$ iterates the operation $\overline{m}$ on $f$: each iteration replaces a function $g$ by its $m$-fold iterate, yielding $f^{m^n}$. Zero iterations give $f$, so this encoding takes $m^0=1$, including $0^0=1$. The explicit outer $f,x$ abstractions make the result the standard Church numeral even at exponent zero, without needing eta equivalence.

Successor, addition, and multiplication operate on the same $C_A$. The displayed exponentiation term has type $C_A\to C_{A\to A}\to C_A$: its exponent iterates an operation on functions. Thus the numeral syntax admits several type instances; one should not force every occurrence into one fixed monomorphic Church type.

The Y combinator is the fixed-point combinatorFor $X_g=(\lambda x.g(xx))(\lambda x.g(xx))$, beta reduction gives $Yg{\to }_{\beta }{X}_g{\to }_{\beta }g{X}_g$. Since $X_g{\equiv }_{\beta }Yg$, we obtain $Yg{\equiv }_{\beta }g(Yg)$. This allows a recursive program body to receive a representation of itself.

Here the computation is in the untyped lambda calculus. The self-application $xx$ would require a simple type satisfying $A=A\to B$, impossible for finite simple types. Accordingly $Y$ is not a typed lambda term of the simply typed system. The Strong normalization theorem for simply typed lambda calculus also rules out a universal divergent fixed-point operator there.

To obtain a lambda representation of partial computable functions, encode machine configurations as finite data using Church numerals, Church pairs, and Church Booleans. Initial configuration, one transition, the halting test, and output extraction are primitive recursive functions, represented by lambda terms through the initial functions, composition, and lambda definition of primitive recursion by pair iteration. If these representations are $\mathsf{Init}$, $\mathsf{Next}$, $\mathsf{Halt}$, and $\mathsf{Out}$, defineUse normal-order beta reduction so the Church Boolean halting test selects one branch without evaluating the unused recursive branch. A halting computation follows finitely many transitions and returns the Church numeral of the output. A nonhalting computation forces successive tests forever and has no head normal form; by normal-order normalization theorem, it cannot be beta equivalent to a Church numeral. Thus every partial computable function is represented, with divergence preserved; every total computable function is the halting special case. This explains the role of $Y$ in computational universality while keeping the typed proof interpretation precise.

Under the Curry-Howard correspondence, Intuitionistic propositional logic propositions are types and proofs are typed terms. Assumptions correspond to typed variables. The logical implication $A\to B$ corresponds to the function type, logical conjunction $A\wedge B$ to the product type, logical disjunction $A\vee B$ to the sum type, logical truth to the unit type, and logical falsity to the empty type.

The rules of natural deduction become term constructors. Implication introduction sends a derivation of $B$ from a variable $x:A$ to the abstraction $\lambda x.M:A\to B$, while implication elimination becomes application $MN$. Pairing and projection implement conjunction, and injections with case analysis implement disjunction. Under this correspondence, normalization of proofs is computation by beta reduction in the simply typed lambda calculus.

The Weak normalization theorem for simply typed lambda calculus states that every well-typed term of the simply typed lambda calculus admits at least one finite sequence of beta reductions ending in a beta-normal form.

Suppose a fixed-point combinator $F$ were typable in the simply typed lambda calculus. By the Weak normalization theorem for simply typed lambda calculus, it would have a beta-normal form. For a fresh variable $f$, the term $Ff$ would then also possess a beta-normal form, say $N$.

The fixed-point property givesReducing the occurrence of $Ff$ on the right to $N$ gives the normal form $fN$. The Church-Rosser theorem says that these beta-equivalent terms must have alpha-equivalent normal forms. This is impossible because $fN$ contains more symbols than $N$. Hence no typing context and simple type can type $F$.

The Weak normalization theorem for simply typed lambda calculus says that every term typable in the implicational simply typed lambda calculus has a beta-normal form. Define reducibility by induction on types: a term of atomic type is reducible when it is weakly normalizing, and $M:A\to B$ is reducible when $MN$ is reducible at $B$ for every reducible $N:A$. Induction on types shows that every reducible term is weakly normalizing and that variables are reducible.

The fundamental substitution lemma is proved by induction on a typing derivation: if $\Gamma ⊢M:A$ and each variable in $\Gamma$ is replaced by a reducible term of its declared type, then the resulting term is reducible at $A$. The application case is the definition at arrow type; in the abstraction case, applying the abstraction to any reducible argument makes one beta step to the substituted body, which is reducible by induction. Substituting each free variable by itself makes every well-typed term reducible, hence weakly normalizing.