Postponement theorem in Untyped Lambda Calculus

This module contains a formalised proof of the (η-)Postponement Theorem for the untyped lambda calculus. The formalisation is based on an ``informal'' proof due to Masako Takahashi in ``Parallel Reductions in Lambda-calculus'' (Information and Computation, Volume 118, 1995). Except for the gymnastics related to working with de Bruijn indices, the translation of the Takashi's proof is rather straightforward.

Preliminaries

We at first prove various properties about the relation between beta_par and the eta-expansion lam_k. (This is Lemma 3.3 in Takahashi). We however do it in in a slightly different order than in the paper, because the cases of the lemma actually depend on each other in a slightly differently order than the one stated in the paper. Firstly, an application of a k-fold eta-expansion of a lambda abstraction can be reduced simply to a substitution via parallel beta.

Similarly, a k-fold eta-expansion of a lambda abstraction can be reduced to a single lambda abstraction via parallel beta reduction.

In case of an application, we can also contract the whole eta-expansion of the applied term via parallel beta reduction

Finally, k+1 eta-expansions can always be contracted to only one eta-expansion via parallel beta reduction.

It now remains to prove the crucial Lemma 3.4 from Takahashi, stating that postponement holds for the case of parallel beta and eta reductions. Before we can do that, we need one auxiliary fact: Parallel beta is closed under eta-expansion.

We can now prove the postponement theorem for the specific case of parallel reductions. This is Lemma 3.4 in Takahashi.

We now define the beta-eta relation and its reflexive-transitive closure

We need a couple of auxiliary statements about the relationships between the parallel and reflexive-transitive versions of beta and eta reductions which appear in the conclusions of the postponement theorem. They make it more convenient to do the rewriting while proving the main result. Firstly, since the reflexive-transitive closures are equivalent to the transitive closures of the parallel relations, the following holds:

Also, it is obviously sufficient to show this to hold for parallel beta, in order for it to also hold for the transitive closure:

Finally, a couple of "one-sided" rewrites for convenience within the proof.

We now build up to the full postponement lemma by proving a series of simpler lemmas Here we consider the case where we postpone eta_star in the presence of only a parallel beta.

Similarly, here we consider only the postponement of eta_par in the presence bstar:

We now combine all the previous lemmas to prove a simplified version of the eta-postponement where we consider separate eta_star and bstar reductions, rather than a single reduction of their union.

The eta postponement theorem

Finally, we prove the full eta-postponement theorem using the separate reduction version in eta_postponement_basic.