Algorithmic Equality for the Untyped Lambda-calculus (Generalized context version)

We discuss completeness of algorithmic equality for untyped lambda-terms with respect to declarative equality of lambda-terms. This case-study is part of ORBI, Open challenge problem Repository for systems reasoning with BInders. For a detailed description of the proof and a discussion regarding other systems see (Felty et al, 2014).
The mechanization highlights several aspects:


We first define lambda-terms in the logical framework LF using Beluga-style syntax.

LF tm : type = 
| app : tmtmtm
| lam : (tmtm) → tm;

The type for lam reflects that binders are represented in the object language using binders in the HOAS meta-language.

Judgements and Rules

We describe algorithmic and declarative equality for the untyped lambda-calculus using axioms and inference rules. The Beluga code is a straightforward HOAS encoding of the associated rules.

Algorithmic Equality

For algorithmic equality, we have the predicate aeq of type tm → tm → type, and inference rules for term applications ae_a and lambda-abstractions ae_l

LF aeq : tmtmtype = 
| ae_a : aeq M1 N1 → aeq M2 N2 → aeq (app M1 M2) (app N1 N2)
| ae_l : ({x : tm} (aeq x x → aeq (M x) (N x))) → aeq (lam (λx. M x)) (lam (λx. N x));

Declarative Equality

Next we define declarative equality in order to establish its equivalence with algorithmic equality and prove completeness. Note that the only difference between the two judgements is that declarative equality explicitly includes inference rules for reflexivity de_r, transitivity de_t, and symmetry de_s: properties which we will prove to be intrinsic to algorithmic equality in the untyped lambda-calculus.

LF deq : tmtmtype = 
| de_l : ({x : tm} (deq x x → deq (M x) (M' x))) → deq (lam (λx. M x)) (lam (λx. M' x))
| de_a : deq M1 N1 → deq M2 N2 → deq (app M1 M2) (app N1 N2)
| de_r : deq M M
| de_t : deq M L → deq L N → deq M N
| de_s : deq T S → deq S T;

## Context schemas Just as types classify expressions, contexts are classified by context schemas.

schema xaG = block (x:tm, ae_v:aeq x x);

schema daG = block (x:tm, ae_v:aeq x x, de_v:deq x x);

Proof of Reflexivity

We first prove admissibility of reflexivity. The proof is implemented as a recursive function called reflG of type {g:xaG}{M:[γ ⊢ tm ]}[γ ⊢ aeq M M]: for all contexts g that have schema xaG, for all terms M, we have a proof that [γ ⊢ aeq M M]. Quantification over contexts and contextual objects in computation-level types is denoted by curly braces; the corresponding abstraction on the level of expressions is written as mlam g ⇒ mlam M ⇒ e.

rec reflG : {γ : xaG} {M : [γ ⊢ tm]} [γ ⊢ aeq M M]  =
mlam γ ⇒ mlam M ⇒ case [γ ⊢ M] of 
  | [γ ⊢ #p.1] ⇒ [γ ⊢ #p.2]
  | [γ ⊢ lam (λx. M)] ⇒
    let  [γ, b : block (y:tm, ae_v:aeq y y) ⊢ D[…, b.1, b.2]] =
    reflG [γ, b : block (y:tm, ae_v:aeq y y)] [γ, b ⊢ M[…, b.1]] in [γ ⊢ ae_l (λx. λw. D)]
  | [γ ⊢ app M1 M2] ⇒
    let  [γ ⊢ D1] = reflG [γ] [γ ⊢ M1] in 
    let  [γ ⊢ D2] = reflG [γ] [γ ⊢ M2] in [γ ⊢ ae_a D1 D2];

In the proof for reflG we begin by introducing and M followed by a case analysis on [γ ⊢ M] using pattern matching. There are three possible cases for M:

Proof of Transitivity

Next, we prove admissibility of transitivity. We encode the proof of transitivity by pattern-matching on the first derivation [γ ⊢ aeq M L] to arrive at the second [γ ⊢ aeq L N]. The recursive function transG handles the three cases for variables, lambda-terms, and applications in a similar fashion to reflG}. The context g:xaG is surrounded by parentheses ( ) to indicate that it is implicit in the actual proof and need to be reconstructed.

rec transG : (γ:xaG) [γ ⊢ aeq M L] → [γ ⊢ aeq L N] → [γ ⊢ aeq M N]  =
fn d1 ⇒ fn d2 ⇒ case d1 of 
  | [γ ⊢ #p.2] ⇒ d2
  | [γ ⊢ ae_l (λx. λu. D1)] ⇒
    let  [γ ⊢ ae_l (λx. λu. D2)] = d2 in 
    let  [γ, b : block (x:tm, ae_v:aeq x x) ⊢ E[…, b.1, b.2]] =
    transG [γ, b : block (x':tm, ae_v:aeq x' x') ⊢ D1[…, b.1, b.2]] [γ, b ⊢ D2[…, b.1, b.2]] in
    [γ ⊢ ae_l (λx. λu. E)]
  | [γ ⊢ ae_a D1 D2] ⇒
    let  [γ ⊢ ae_a F1 F2] = d2 in 
    let  [γ ⊢ E1] = transG [γ ⊢ D1] [γ ⊢ F1] in 
    let  [γ ⊢ E2] = transG [γ ⊢ D2] [γ ⊢ F2] in [γ ⊢ ae_a E1 E2];

Here, the variable case exploits that if aeq M N is an element of the context g, then M = N. Note that the recursive calls do not take the context g as an explicit argument.

Proof of Symmetry

Again, we encode the proof of symmetry as a recursive function symG. As in transG, the context g is implicit. Furthermore, we handle the variable case using the same property in both functions.

rec symG : (γ:xaG) [γ ⊢ aeq M L] → [γ ⊢ aeq L M]  =
fn d ⇒ case d of 
  | [γ ⊢ #p.2] ⇒ d
  | [γ ⊢ ae_l (λx. λu. D1)] ⇒
    let  [γ, b : block (x:tm, ae_v:aeq x x) ⊢ E[…, b.1, b.2]] =
    symG [γ, b : block (x':tm, ae_v:aeq x' x') ⊢ D1[…, b.1, b.2]] in [γ ⊢ ae_l (λx. λu. E)]
  | [γ ⊢ ae_a D1 D2] ⇒
    let  [γ ⊢ E1] = symG [γ ⊢ D1] in 
    let  [γ ⊢ E2] = symG [γ ⊢ D2] in [γ ⊢ ae_a E1 E2];

Proof of Completeness

Finally, we implement the completeness proof as as a recursive function ceqG.

rec ceq : (γ:daG) [γ ⊢ deq M N] → [γ ⊢ aeq M N]  =
fn e ⇒ case e of 
  | [γ ⊢ #p.3] ⇒ [γ ⊢ #p.2]
  | [γ ⊢ de_r] ⇒ reflG [γ] [γ ⊢ _]
  | [γ ⊢ de_a D1 D2] ⇒
    let  [γ ⊢ F1] = ceq [γ ⊢ D1] in 
    let  [γ ⊢ F2] = ceq [γ ⊢ D2] in [γ ⊢ ae_a F1 F2]
  | [γ ⊢ de_l (λx. λu. D)] ⇒
    let  [γ, b : block (x:tm, _t:aeq x x, u:deq x x) ⊢ F[…, b.1, b.2]] =
    ceq [γ, b : block (x:tm, _t:aeq x x, u:deq x x) ⊢ D[…, b.1, b.3]] in
    [γ ⊢ ae_l (λx. λv. F)]
  | [γ ⊢ de_t D1 D2] ⇒
    let  [γ ⊢ F2] = ceq [γ ⊢ D2] in 
    let  [γ ⊢ F1] = ceq [γ ⊢ D1] in transG [γ ⊢ F1] [γ ⊢ F2]
  | [γ ⊢ de_s D] ⇒
    let  [γ ⊢ F] = ceq [γ ⊢ D] in symG [γ ⊢ F];

We explain here the three cases shown in the informal proof in the companion paper (Felty et al, 2014). First, let us consider the case where we used an assumption from the context. Since the context g consists of blocks with the following structure: block x:tm , ae_v:aeq x x,de_v: deq x x, we in fact want to match on the third element of such a block. This is written as #p.3. The type of #p.3 is deq #p.1 #p.1. Since our context always contains a block and the parameter variable #p describes such a block, we know that there exists a proof for aeq #p.1 #p.1, which can be described by #p.2.

Second, we consider the case where we applied the reflexivity rule de_r as a last step. In this case, we need to refer to the reflexivity lemma we proved about algorithmic equality. To use the function reflG, which implements the reflexivity lemma for algorithmic equality, we need a context of schema xaG; however, the context used in the proof for ceqG is of schema daG and we rely on context subsumption to justify passing a context daG in place of a context xaG. The cases for transitivity and symmetry are similar.

Third, we consider the case for de_l, the case for lambda-abstractions. In this case, we extend the context with the new declarations about variables and pass to the recursive call ceqG the derivation [γ, b:block (x:tm ,ae_v:aeq x x, de_v: deq x x) ⊢ D[…,b.1, b.3]]. Declaration weakening (in the informal proof d-wk (Felty et al, 2014)) is built-in. In the pattern, the derivation D has type [γ, x:tm , ae_v:aeq x x ⊢ deq M[…,x] N]. We hence construct a weakening substitution … b.1 b.3 that allows us to move D to the context γ, b:block (x:tm,ae_v:aeq x x, de_v:deq x x). The result of recursive call is a derivation F, where F only depends on x:tm and u:aeq x x. In the on-paper proof we refer to declaration strengthening (d-str) to justify that F cannot depend on de_v assumptions. In Beluga, the programmer uses strengthening by stating which assumptions F can depend on. The coverage checker will then subsequently rely on subordination to verify that the restricted case is sufficient and no other cases have been forgotten. Subordination allows us to verify that indeed assumptions of type de_v: deq x x cannot be used in proofs for aeq M[…, b.1] N[…, b.1]. Finally, we use F to assemble the final result ae_l (λx.λv. F).

We conclude this example with a few observations: The statement of the theorem is directly and succinctly represented in Beluga using contextual types and contextual objects. Every case in the on-paper proof corresponds directly to a case in the implementation of the recursive function. Type reconstruction is used to reconstruct implicit type arguments and infer the type of free contextual variables that occur in patterns. This is crucial to achieve a palatable source language. Weakening and strengthening are supported in Beluga through the typing rules and on the level of context variables and context schemas using context subsumption. If schema W is a prefix of a schema W', then we can always use a context of schema W' in place of a context of schema W.

To download the code: Untyped_Algorithmic_Equality_-_Context_Subsumption.bel