= Solution
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\vdash t:A$, where the context assigns types to its free variables. The basic typing rules are
$$
\frac{x:A\in\Gamma}{\Gamma\vdash x:A},\qquad
\frac{\Gamma,x:A\vdash t:B}{\Gamma\vdash\lambda x.t:A\to B},\qquad
\frac{\Gamma\vdash f:A\to B\quad\Gamma\vdash u:A}{\Gamma\vdash fu:B}.
$$
The <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 \b[<Church numeral>] is
$$
\boxed{\overline n=\lambda f.\lambda x.f^n x},\qquad
\overline0=\lambda f.\lambda x.x,
$$
where $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:
$$
\begin{aligned}
\mathsf{Succ}&=\lambda n f x.f(nfx),\\
\mathsf{Add}&=\lambda m n f x.mf(nfx),\\
\mathsf{Mul}&=\lambda m n f x.m(nf)x,\\
\mathsf{Pow}&=\lambda m n f x.(nm)fx.
\end{aligned}
$$
Their concise conclusions are
$$
\boxed{\mathsf{Succ}\,\overline n\equiv_\beta\overline{n+1},\quad
\mathsf{Add}\,\overline m\,\overline n\equiv_\beta\overline{m+n},\quad
\mathsf{Mul}\,\overline m\,\overline n\equiv_\beta\overline{mn},\quad
\mathsf{Pow}\,\overline m\,\overline n\equiv_\beta\overline{m^n}.}
$$
For 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 \b[<Y combinator>] is the <fixed-point combinator>
$$
\boxed{Y=\lambda g.(\lambda x.g(xx))(\lambda x.g(xx)).}
$$
For $X_g=(\lambda x.g(xx))(\lambda x.g(xx))$, <beta reduction> gives $Yg\to_\beta X_g\to_\beta gX_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}$, define
$$
\mathsf{Run}=Y(\lambda r c.\mathsf{Halt}\,c\,(\mathsf{Out}\,c)\,(r(\mathsf{Next}\,c))),\qquad
\mathsf{Compute}=\lambda n.\mathsf{Run}(\mathsf{Init}\,n).
$$
Use <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 \b[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.
Back to article page
