Past exam of the computer science course of the University of Oxford / 2015 / Lambda calculus and types (A12077W1)

Solutions to all twelve numbered subparts of the University of Oxford computer science Finals paper held on 4 June 2015. Question 2(d) has a wording issue: its literal impossibility claim is false, and the solution gives the exact condition for a valid typing judgment.^[ref]

Choose all auxiliary bound variables fresh for the free variables of $p,q,r$; alpha equivalence permits this. The operation $\bullet$ is composition of lambda terms, so expand its definition and use beta reduction:The two lambda terms have the same reduct, up to alpha equivalence, hence they are related by beta equivalence:No eta conversion is needed for this associativity calculation.

Write $I\equiv \lambda u.u$ for the I combinator, and choose $x$ outside the free variables of $p$. Both orders of composition of lambda terms first give the same lambda abstraction by beta reduction:The freshness condition is exactly the side condition for eta conversion, which contracts $\lambda x.px$ to $p$. ThereforeHere eta conversion matters: a free variable $p$ is already in beta-normal form, as is $\lambda x.px$, and beta equivalence alone does not equate them.

The argument order in $p$ is a cyclic permutation. Undo it by rotating in the other direction. For $n\ge 1$, choose the lambda termUse fresh bound variables throughout. Substituting $qz$ for the first argument of $p$ and then performing beta reduction givesIndeed, the arguments received by $qz$ are $y_1=x_2,\dots ,y_{n-1}=x_n,y_n=x_1$, so its last argument moves back to the front. Apply eta conversion successively, starting with the innermost lambda abstraction. At each step the bound variable being removed is absent from the preceding expression. Thus the last expression is related to $z$ by beta-eta equivalence, and consequentlyFor the induction needed in the next part, also compute the reverse composition of lambda terms:So this $q$ is a two-sided inverse. The empty argument list at $n=0$ means $p=\lambda z.z$; choose $q=I$. For $n=1$, both displayed rotations give $\lambda z{y}_1.z{y}_1$, which is also related to $I$ by eta conversion. These boundary cases require no exceptional inverse construction.

Use structural induction on the construction of $p\in \mathcal{R}$, with the stronger induction claim that $p$ is an invertible lambda term: there is a lambda term $q$ satisfying bothThe base constructor has exactly the two-sided inverse proved in part (c). Strengthening the claim is useful because the inductive construction needs inverses of its constituent lambda terms in both orders.

For the inductive constructor, let $t_i$ be the two-sided inverse supplied for $s_i$. Thus, for a fresh variable $u$, beta-eta equivalence givesFor $n\ge 1$, defineThis lambda term reverses the cyclic permutation and applies the appropriate inverse to each argument. First use beta reduction to expand one order of composition of lambda terms:For the other order, beta reduction givesThese computations close the stronger induction. For $n=1$, each formula has the single argument involving $s_1$ and $t_1$; for $n=0$, the constructor is $I$ and its inverse is $I$. Every construction is finite, so the inverse is a finite lambda term. There is no requirement that this inverse itself belong to $\mathcal{R}$.

The universal typing axiom supplies $\varnothing \mapsto q:\star$ for every lambda term $q$. Use this as the argument premise of the lambda application rule. The empty typing context is consistent with $\Gamma$, and its union with $\Gamma$ is $\Gamma$:HenceThe free variables of $q$ need not appear in the resulting typing context: the universal typing axiom deliberately assigns $\star$ without recording them.

Choose $\star$ as the domain of the new function type. Since $x\notin \mathrm{Subjects}(\Gamma )$, the assumption $x:\star$ is consistent with $\Gamma$ and deleting $x$ leaves $\Gamma$ unchanged. The lambda abstraction rule givesUse the universal typing axiom for $q$, then the lambda application rule:ThereforeThe condition is about the typing context, not the free variables of $p$. Some occurrences of $x$ in $p$ might have been hidden by a use of the universal typing axiom; the derivation above still follows the printed rules.

Begin with the variable typing judgment $\{x:A\}\mapsto x:A$. Because $z$ is absent from this typing context, the lambda abstraction rule permits $z$ to have type $\star$:Assign the entire lambda application $yx$ type $\star$ using the universal typing axiom, without attempting to assign a function type to $y$. ThenAlthough $y$ is a free variable of the body, it is absent from its recorded typing context. Consequently the lambda abstraction rule allows any simple type $B$ for $y$. Abstract over $y$ and then $x$:The side condition for $y$ holds because $y$ is absent; the side condition for $x$ holds because its recorded simple type is $A$. Thus

The exact restriction in the ordinary simply typed lambda calculus isThus the unrestricted choice of $A,B$ available in part (c) fails. A reading of the printed sentence as asserting impossibility for every choice of $A,B$ is false. This issue occurs in the original PDF as well as its transcription.^[ref]

To prove necessity, first observe why the ordinary rules cannot hide assumptions. Structural induction on a derivation provesFor a variable, both sides are the singleton containing that variable. For lambda application, both sides are the union of the two premise supports. For lambda abstraction, both sides delete the bound variable. There is no universal typing axiom to interrupt this equality.

Now invert the proposed derivation. Each outer lambda abstraction must have been introduced by the abstraction rule, since the other ordinary rules conclude a variable or a lambda application. The body must therefore have the typing judgmentThe support equality just proved ensures that both displayed assumptions occur; consistency fixes their simple types to those specified by the outer function type. Inverting the lambda application gives a simple type $C$ for its argument and the following premises:There is no flexibility in the supports: $\lambda z.x$ has the single free variable $x$, whereas $yx$ has both free variables $y,x$. Invert the second lambda application. Its two premises must befor some simple type $D$. The variable rule is the only possible final rule for each premise. It forces $D=A$ and $B=D\Rightarrow C$, yielding $B=A\Rightarrow C$.

Conversely, suppose $B=A\Rightarrow C$. The ordinary rules giveThe typing contexts are consistent, so another lambda application gives the body type $A$. Two lambda abstractions discharge $y$ and $x$, establishingThis proves sufficiency and supplies a family of counterexamples to the literal impossibility claim. For a concrete failure of the unrestricted claim, choose $A=\alpha$ and $B=\beta$ as atomic type variables. The type variable $\beta$ is not a function type $\alpha \Rightarrow C$, so no derivation exists for that fixed pair. Here the atomic type variables are fixed type expressions, rather than unknowns that one may change during type inference.

The reason for the restriction is the otherwise discarded lambda application $yx$: the ordinary rules still type-check it. Its subsequent disappearance under beta reduction does not license reversing that beta reduction while preserving every simple type of the result. The beta-normal form $\lambda xy.x$ admits arbitrary $A\Rightarrow (B\Rightarrow A)$, whereas the unreduced lambda term has the additional constraint just derived.

Take an infinite supply of variables and the two distinguished constants of combinatory logic, the K combinator and the S combinator. The combinatory logic terms are exactly the finite expressions generated byThus every variable and each distinguished constant is a combinatory logic term, and the application of two combinatory logic terms is a combinatory logic term. Nothing else is a combinatory logic term. Application associates to the left, so $ABC$ means $(AB)C$; it is not assumed to be associative. The I combinator can be used as the abbreviation $\mathbf{I}\equiv \mathbf{SKK}$, without adding a new primitive constant.

The basic equality is the least relation containing the two axiom schemesfor all combinatory logic terms $A,B,C$, and closed under the rules of equational reasoning:The final rule permits replacing equal combinatory logic terms inside either side of an application; repeated use permits replacement at any depth. Uniform substitution of combinatory logic terms for variables preserves equality, either included as a rule or proved by induction on these derivations, since the displayed axioms are schemes. No rule equating two combinatory logic terms merely because they agree after an extra argument belongs to this basic theory. Its equality is the symmetric, reflexive and transitive closure of weak combinatory reduction.

Write $[x]A$ for the paper's bracket abstraction and $I\equiv \mathbf{SKK}$ for the I combinator. Prove the result by structural induction following the three clauses of bracket abstraction.

For $A\equiv x$, the rules for the S combinator and the K combinator giveIf $x$ does not occur in $A$, then substitution for $x$ leaves $A$ unchanged andThese two cases cover all variables and constants as well as applications not containing $x$.

In the remaining case, $A\equiv CD$ and $x$ occurs in at least one of $C,D$. The bracket abstraction clause, the rule for the S combinator, the induction hypotheses and compatibility of equality with application giveThe last line is the defining application clause of substitution. ThereforeThe conclusion is equality in combinatory logic; it need not be literal identity of strings. There are no binders in a combinatory logic term, so this substitution introduces no variable capture.

Again write $[x]A$ for bracket abstraction. In combinatory logic, all variable occurrences are free variables. Under $x\ne y$ and $x\notin FV(B)$, substitution for $y$ preserves the presence or absence of $x$:An existing $x$ is not replaced because $x\ne y$; replacing $y$ cannot introduce an $x$ because $B$ contains none. This ensures that the same clause of bracket abstraction applies before and after substitution.

Use structural induction on $A$, respecting those clauses. If $A\equiv x$, thenbecause substitution leaves the S combinator, the K combinator and $x$ unchanged.

If $x$ is absent from $A$, it is also absent from $A[B/y]$. ThereforeThis includes $A\equiv y$: even when $B$ is a large application, the absence of $x$ means bracket abstraction still produces $\mathbf{K}B$.

Finally, let $A\equiv CD$ with $x$ occurring in $C$ or $D$. By the occurrence observation, $x$ also occurs in $C[B/y]$ or $D[B/y]$, so the application clause applies on both sides. Apply the induction hypotheses:Every step uses the definitions of substitution and bracket abstraction, without applying the equality axioms for the S combinator or the K combinator. Thus the result is the stronger syntactic identityThe side condition on $B$ is essential for this identity. For example, substituting $x$ for $y$ in $[x]y\equiv \mathbf{K}y$ gives $\mathbf{K}x$, whereas $[x](y[x/y])\equiv [x]x\equiv \mathbf{SKK}$, a different string.

Successive bracket abstractions are processed from the inside out: $[x][y]((\mathbf{K}x)y)$. Retain $I\equiv (\mathbf{SK})\mathbf{K}$ only as a temporary abbreviation for the I combinator. Since $y$ is absent from $\mathbf{K}x$, the first bracket abstraction isFor the outer bracket abstraction, $x$ is absent from $I$ and the S combinator, while it occurs in $\mathbf{K}(\mathbf{K}x)$. HenceSubstituting upward and then expanding $I$ gives the following fully bracketed string, consisting solely of the S combinator, the K combinator and parentheses:For readability, the same result with the usual left association convention and the temporary abbreviation isThe syntactic result comes from the specified bracket abstraction algorithm. Replacing it by the shorter K combinator, despite agreement after two arguments, would not answer the requested computation. As a check using the result of part (b), applying the computed combinatory logic term to $u,v$ gives $\mathbf{K}uv=u$.