Equality in the Untyped Lambda Calculus

This page contains a solution to a problem set out in the paper "The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations" by Felty et al.[1]

This benchmark provides a specification for the untyped $\lambda$-calculus with two forms of equality: algorithmic and declarative.

The full solutions are provided in equal-untyped.lf and equal-untyped.ath.

Specification

tm: type.
lam: {M: tm -> tm} tm.
app: {M1:tm}{M2:tm} tm.

aeq: tm -> tm -> type.
deq: tm -> tm -> type.

ae_a : {M1: tm}{M2: tm}{N1:tm}{N2:tm}
       {D1:aeq M1 N1}{D2:aeq M2 N2}
       aeq (app M1 M2) (app N1 N2).
ae_l : {M: tm -> tm}{N: tm -> tm}
       {D: {z:tm} aeq z z -> aeq (M z) (N z)}
       aeq (lam ([x] M x)) (lam ([x] N x)).

de_a : {M1:tm}{M2:tm}{N1:tm}{N2:tm}
       {D1: deq M1 N1}{D2: deq M2 N2}
       deq (app M1 M2) (app N1 N2).
de_l : {M: tm -> tm}{N: tm -> tm}
       {D: {z:tm} deq z z -> deq (M z) (N z)}
       deq (lam ([x] M x)) (lam ([x] N x)).
de_s : {M:tm}{N:tm}
       {D: deq M N}
       deq N M.
de_t : {M1:tm}{M2:tm}{M3:tm}
       {D1: deq M1 M2}
       {D2: deq M2 M3}
       deq M1 M3.
de_r : {M:tm} deq M M.

The benchmark also defines two different context schemas to be used:

Schema xaG := (x: tm,a: aeq x x).
Schema daG := (x:tm, a:aeq x x, u:deq x x).

Properties of Algorithmic Equality

One wishes to prove three properties about algorithmic equality in isolation:

1. Reflexivity

   

   Theorem reflG: ctx G:xaG, forall T, {G |- T : tm} => exists D, {G |- D : aeq T T}.
   induction on 1. intros. case H1 (keep).
   %app
   apply IH to H2.
   apply IH to H3.
   exists ae_a M1 M2 M1 M2 D D1.
   search.
   %lam
   weaken H2 with aeq n n.
   apply IH to H3 with (G = G, n1: tm, n:aeq n1 n1).
   prune H2.
   exists ae_l M M D.
   search.
   %var
   exists n1. search.
2. Symmetry

   

   Theorem symG: ctx G:xaG, forall T1 T2 Q,
     {G |- Q : aeq T1 T2} => exists D, {G |- D : aeq T2 T1}.
   induction on 1.intros. case H1(keep).
   %lam
   apply IH to H4 with (G = G, n1: tm, n: aeq n1 n1).
   prune H5.
   exists (ae_l N M D1).
   search.
   %app
   apply IH to H6.
   apply IH to H7.
   exists (ae_a N1 N2 M1 M2 D D3).
   search.
   %var
   exists n1. search.
3. Transitivity

   

   Theorem tranG: ctx G:xaG, forall M1 M2 M3 D1 D2,
     {G |- D1: aeq M1 M2} => {G |- D2: aeq M2 M3} => exists D3, {G |- D3: aeq M1 M3}.
   induction on 1. intros.
   case H1 (keep).
   %lam
   case H2.
   apply IH to H5 H8 with (G = G, n1:tm, n: aeq n1 n1).
   prune H9.
   exists ae_l M M4 D1. search.
   %app
   case H2.
   apply IH to H7 H13.
   apply IH to H8 H14.
   exists ae_a M4 M5 N3 N4 D1 D2. search.
   %var
   case H2.
   exists n1. search.

Completeness via Schema Subsumption

Now, one wishes to show that algorithmic equality is complete with respect to declarative equality. In other words "If two terms are declaratively equal, then they are algorithmically equal." This would entail analyzing the cases in which the terms under consideration are equal by reflexivity, symmetry, and transitivity. Then, one must prove that these properties hold for algorithmic equality. However, we have already shown these properties to hold in our above theorems.

The wrinkle is that these properties were proven with a context variable circumscribed by xaG which has the shape (x:tm, a:aeq x x), and in order to reason about declarative equality we must have the context variable circumscribed by daG which has the shape (x:tm, a:aeq x x, u:deq x x). Schema subsumption will allow Adelfa to realize that this extended shape's entry u: deq x x cannot impact the theorems reflG, tranG, or symG, and we can use them directly in daG.

Theorem ceqG: ctx G:daG, forall M N D1,
  {G |- D1: deq M N} => exists D2, {G |- D2 : aeq M N}.
induction on 1.
intros. case H1 (keep). apply reflG to H2. exists D. search.
apply IH to H5.
apply IH to H6.
apply tranG to H7 H8. exists D5. search.
apply IH to H4.
apply symG to H5. exists D1. search.
weaken H4 with aeq n2 n2.
ctxpermute H5 to G, n2: tm, n4: aeq n2 n2, n3:deq n2 n2.
apply IH to H6 with (G = G, n1:tm, n2:aeq n1 n1, n:deq n1 n1).
prune H7.
strengthen H7.
exists ae_l M1 N1 ([x][y] D2 y x). search.
apply IH to H6. apply IH to H7.
exists ae_a M1 M2 N1 N2 D1 D4. search.
exists n1. search.

References

1. [1] Felty, A.P., Momigliano, A., Pientka, B.: The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations. Journal of Automated Reasoning. 55, 307–372 (2015). https://doi.org/10.1007/s10817-015-9327-3⁠.