Documentation out of dateLearn more

Concrete representation

The use of higher-order abstract syntax, using STELF’s binding structure to represent binding structure in an encoded language, is one of the more unique and convenient aspects of using STELF. However, the fundamental nature of the binding structure has been troubling to some, because it is not obvious that everything you might ever want to do to a lambda term is doable within the framework of HOAS.

One way to deal with this question is to show that there is a bijection between HOAS terms in STELF and some concrete representation of terms with bound variables. In that case, any arbitrary operation on the concrete representation can be related to an operation in the HOAS representation by translating the HOAS term into concrete form, performing the operation on the concrete term, and translating it back into HOAS. That said, we do not know of any practical proof that has required this technique.

The technique of de Bruijn indices, described fully on Wikipedia, is a popular technique for concretely representing binding structures. This page describes a bijection between closed de Bruijn indices and closed HOAS terms, and proves that bijection correct. We will use a modified version of de Bruijn indices - it was easier to start counting from 0, whereas true de Bruijn indices count from 1. The bijection is defined using two relations, exp-->db and db-->exp. We prove the bijection is correct in four steps:

exp-->db is a total and unique relation between HOAS to de Bruijn terms, and can therefore be thought of as the function e2d.
db-->exp is a total and unique relation between de Bruijn terms to HOAS, and can therefore be thought of as the function d2e.
For all closed de Bruijn terms E, d2e(e2d E) = E
For all closed HOAS terms E, e2d (d2e E) = E

We do not prove that the bijection is an isomorphism - both HOAS and de Bruijn indices have a built-in notion of “substitution,” and a proof of isomorphism would require us to define substitution on our de Bruijn terms and show that substitution behaves the same way in the de Bruijn representation as it does in the HOAS representation.

This encoding makes heavy use of intrinsic encoding in representing de Bruijn terms, both to ensure well-formedness of all terms and to encode a structural metric directly into the type of a de Bruijn term. The proof could also be done with extrinsic encoding by having a separate well-formedness judgment for de Bruijn terms and a separate judgment relating a de Bruijn term to the structural metric it corresponds to, but in this example the intrinsic approach made the proofs simpler.

Preliminaries

We will need the ability to use reasoning from false at one place to avoid a spurious case that coverage checking does not deal with correctly, and as is the case with many examples, we will utilize natural numbers extensively..

%sort uninhabited %.
%freeze uninhabited %.
%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%sort id-nat {_ nat} {_ nat} %.
%term id-nat/refl id-nat N N %.

We will also need a less-than relation on numbers. For reasons that will become clear, we will also need to define an identity on less-than derivations. Finally, we define lt12, which allows us to take two numbers N < M and case analyze on whether (s N) = M or (s N) < M.

%sort lt {_ nat} {_ nat} %.
%term lt/z lt z (s N) %.
%term lt/s %pi (lt (s N1) (s N2)) %<- (lt N1 N2) %.
%sort id-lt {_ lt N M} {_ lt N' M'} %.
%term id-lt/refl id-lt L L %.
%sort lt12 {_ nat} {_ nat} %.
%term lt12/1 lt12 N (s N) %.
%term lt12/2 %pi (lt12 N (s M)) %<- (lt N M) %.

Finally, we define two helper functions lt+, which produces a derivation M < (N + 1) from a derivation of M < N, and lts, which produces a derivation of N < (s N) from any natural number N. Most of the tedious reasoning required for this example is about trivial properties of these two helper functions; it is hidden here but can be revealed by clicking on the source code link at the top of the page.

%sort lt+ {_ lt M N} {_ lt M (s N)} %.
%mode lt+ %in %out %.
%term lt+/z lt+ lt/z lt/z %.
%term lt+/s %pi (lt+ (lt/s LT1) (lt/s LT2)) %<- (lt+ LT1 LT2) %.
%worlds () (lt+ _ _) %.
%total T (lt+ T _) %.
%sort lts {N} {_ lt N (s N)} %.
%mode lts %in %out %.
%term lts/z lts z lt/z %.
%term lts/s %pi (lts (s N) (lt/s D)) %<- (lts N D) %.
%worlds () (lts _ _) %.
%total T (lts T _) %.
%sort lt+-irrev {L1 lt N1 N2} {_ lt+ L1 L2} {L1' lt N1 N2} {_ lt+ L1' L2} %.
%mode lt+-irrev %in %in %in %out %.
%term _ lt+-irrev lt/z lt+/z lt/z lt+/z %.
%term _
  %pi (lt+-irrev (lt/s L1) (lt+/s L1+) (lt/s L2) (lt+/s L2+))
  %<- (lt+-irrev L1 L1+ L2 L2+) %.
%worlds () (lt+-irrev _ _ _ _) %.
%total T (lt+-irrev T _ _ _) %.
%sort can-lts {N} {LT lt N (s N)} {_ lts N LT} %.
%mode can-lts %in %in %out %.
%term _ can-lts z _ lts/z %.
%term _ %pi (can-lts (s N) (lt/s LT) (lts/s LTS)) %<- (can-lts N LT LTS) %.
%worlds () (can-lts _ _ _) %.
%total T (can-lts T _ _) %.
%sort can-lt+ {LT lt M N} {LT' lt M (s N)} {_ lt+ LT LT'} %.
%mode can-lt+ %in %in %out %.
%term _ can-lt+ lt/z lt/z lt+/z %.
%term _ %pi (can-lt+ (lt/s LT) (lt/s LT') (lt+/s LT+)) %<- (can-lt+ LT LT' LT+) %.
%worlds () (can-lt+ _ _ _) %.
%total T (can-lt+ T _ _) %.
%sort lt-s-cong {_ id-lt L1 L1'} {_ id-lt (lt/s L1) (lt/s L1')} %.
%mode lt-s-cong %in %out %.
%term _ lt-s-cong id-lt/refl id-lt/refl %.
%worlds () (lt-s-cong _ _) %.
%total {} (lt-s-cong _ _) %.
%sort lt+-uniq {_ id-lt L1 L2} {_ lt+ L1 L1'} {_ lt+ L2 L2'} {_ id-lt L1' L2'} %.
%mode lt+-uniq %in %in %in %out %.
%term _ lt+-uniq id-lt/refl lt+/z lt+/z id-lt/refl %.
%term _
  %pi (lt+-uniq id-lt/refl (lt+/s LT+1) (lt+/s LT+2) ID)
  %<- (lt+-uniq id-lt/refl LT+1 LT+2 ID2)
  %<- (lt-s-cong ID2 ID) %.
%worlds () (lt+-uniq _ _ _ _) %.
%total T (lt+-uniq _ T _ _) %.
%sort lts-uniq {_ id-nat N1 N2} {_ lts N1 L1} {_ lts N2 L2} {_ id-lt L1 L2} %.
%mode lts-uniq %in %in %in %out %.
%term _ lts-uniq id-nat/refl lts/z lts/z id-lt/refl %.
%term _
  %pi (lts-uniq id-nat/refl (lts/s LT1) (lts/s LT2) ID)
  %<- (lts-uniq id-nat/refl LT1 LT2 ID1)
  %<- (lt-s-cong ID1 ID) %.
%worlds () (lts-uniq _ _ _ _) %.
%total T (lts-uniq _ T _ _) %.
%sort lt-opt-s {_ lt12 N M} {_ lt12 (s N) (s M)} %.
%mode lt-opt-s %in %out %.
%term lt-opt-s/1 lt-opt-s lt12/1 lt12/1 %.
%term lt-opt-s/2 lt-opt-s (lt12/2 LT) (lt12/2 (lt/s LT)) %.
%worlds () (lt-opt-s _ _) %.
%total {} (lt-opt-s _ _) %.
%sort lt-opt {_ lt N M} {_ lt12 N M} %.
%mode lt-opt %in %out %.
%term lt-opt/z1 lt-opt lt/z lt12/1 %.
%term lt-opt/z2 lt-opt lt/z (lt12/2 lt/z) %.
%term lt-opt/s %pi (lt-opt (lt/s LT) LT12') %<- (lt-opt LT LT12) %<- (lt-opt-s LT12 LT12') %.
%worlds () (lt-opt _ _) %.
%total T (lt-opt T _) %.
%sort lt-opt-succ1 {LT lt N (s N)} {_ lt-opt LT lt12/1} %.
%mode lt-opt-succ1 %in %out %.
%term _ lt-opt-succ1 lt/z lt-opt/z1 %.
%term _ %pi (lt-opt-succ1 (lt/s LT) (lt-opt/s lt-opt-s/1 LTS)) %<- (lt-opt-succ1 LT LTS) %.
%worlds () (lt-opt-succ1 _ _) %.
%total T (lt-opt-succ1 T _) %.
%sort lt-opt-succ2 {_ lt+ LT LT'} {_ lt-opt LT' (lt12/2 LT)} %.
%mode lt-opt-succ2 %in %out %.
%term _ lt-opt-succ2 lt+/z lt-opt/z2 %.
%term _
  %pi (lt-opt-succ2 (lt+/s LT+) (lt-opt/s lt-opt-s/2 LTO))
  %<- (lt-opt-succ2 LT+ LTO) %.
%worlds () (lt-opt-succ2 _ _) %.
%total T (lt-opt-succ2 T _) %.
%sort lt-opt2-s-uniq {_ id-lt LT1 LT1'} {_ lt-opt-s (lt12/2 LT1) (lt12/2 LT2)} {_ lt-opt-s (lt12/2 LT1') (lt12/2 LT2')} {_ id-lt LT2 LT2'} %.
%mode lt-opt2-s-uniq %in %in %in %out %.
%term _ lt-opt2-s-uniq id-lt/refl lt-opt-s/2 lt-opt-s/2 id-lt/refl %.
%worlds () (lt-opt2-s-uniq _ _ _ _) %.
%total {} (lt-opt2-s-uniq _ _ _ _) %.
%sort lt-opt2-uniq {_ id-lt LT1 LT1'} {_ lt-opt LT1 (lt12/2 LT2)} {_ lt-opt LT1' (lt12/2 LT2')} {_ id-lt LT2 LT2'} %.
%mode lt-opt2-uniq %in %in %in %out %.
%term _ lt-opt2-uniq id-lt/refl lt-opt/z2 lt-opt/z2 id-lt/refl %.
%term _
  %pi (lt-opt2-uniq id-lt/refl (lt-opt/s LS L) (lt-opt/s LS' L') ID)
  %<- (lt-opt2-uniq id-lt/refl L L' ID1)
  %<- (lt-opt2-s-uniq ID1 LS LS' ID) %.
%worlds () (lt-opt2-uniq _ _ _ _) %.
%total T (lt-opt2-uniq _ T _ _) %.
%sort lt-opt-excl {_ lt-opt LT lt12/1} {_ lt-opt LT (lt12/2 L)} {_ uninhabited} %.
%mode lt-opt-excl %in %in %out %.
%term _ %pi (lt-opt-excl (lt-opt/s LS L) (lt-opt/s LS' L') X) %<- (lt-opt-excl L L' X) %.
%worlds () (lt-opt-excl _ _ _) %.
%total T (lt-opt-excl T _ _) %.

HOAS lambda terms

The representation of the untyped lambda calculus is extremely simple in higher-order abstract syntax; we also define congruence lemmas for lam and app.

What is interesting is the %block declaration of blocksimple. This is a standard way of looking at the LF context when we are using HOAS lambda terms, but it is not the one we will use in most cases.

%sort exp %.
%term lam %pi (%pi exp %-> exp) %-> exp %.
%term app %pi exp %-> exp %-> exp %.
%block blocksimple {v exp}%.
%sort id-exp {_ exp} {_ exp} %.
%term id-exp/refl id-exp E E %.
%sort id-lam-cong {_ {v} id-exp (E v) (E' v)} {_ id-exp (lam E) (lam E')} %.
%term _ id-lam-cong ([v] id-exp/refl) id-exp/refl %.
%mode id-lam-cong %in %out %.
%worlds (blocksimple) (id-lam-cong _ _) %.
%total {} (id-lam-cong _ _) %.
%sort id-app-cong {_ id-exp E1 E1'} {_ id-exp E2 E2'} {_ id-exp (app E1 E2) (app E1' E2')} %.
%term _ id-app-cong id-exp/refl id-exp/refl id-exp/refl %.
%mode id-app-cong %in %in %out %.
%worlds (blocksimple) (id-app-cong _ _ _) %.
%total {} (id-app-cong _ _ _) %.

The problem with blocksimple is that we will need, crucially, to be able to know when something is a variable (as opposed to an application or a lambda term). The world blockvar achieves this by requiring that all variables be accompanied by a judgment isvar v; because these judgments cannot be defined, they can only be introduced as hypothetical judgments, so having (isvar E) ensures that E is a variable.

%sort isvar {_ exp} %.
%block blockvar {v} {iv isvar v}%.

However, we will need one more block declaration to be able to do everything we need. In particular, the block blockvar is not enough to ensure that we always will be able to determine whether an open lambda term is a lambda, an application, or a variable. In order to do this, we need a specialized block declaration blockcases that specifies that whenever I add a variable to the context, I add it along with a isvar hypothesis and a can-case hypothesis.

The definition of fake is a bit of a hack - we need to allow can-case to depend on can-case or we will run afoul of STELF’s autofreeze feature. If you are running this proof on your own computer, try deleting the line to see STELF’s error message.

%sort case {_ exp} %.
%term case/lam case (lam ([x] E x)) %.
%term case/app case (app E1 E2) %.
%term case/var %pi (isvar V) %-> (case V) %.
%sort can-case {E} {_ case E} %.
%sort fake {_ can-case E C} {_ can-case E C} %.
%term _ %pi (fake E F) %<- ({d can-case X Y} can-case X' Y') %.
%block blockcases {v} {iv isvar v} {d can-case v (case/var iv)}%.
%term can-case/lam can-case (lam ([x] E x)) case/lam %.
%term can-case/app can-case (app E1 E2) case/app %.
%mode can-case %in %out %.
%worlds (blockcases) (can-case _ _) %.
%total T (can-case T _) %.

de Bruijn lambda terms

Structural metric: Trees

In order for the totality proof for the de Bruijn to HOAS translation to go through, we will need to show that there is a metric by which unbind does not change the size of a term.

Because STELF does not relate the sizes of bound variables and the free variables unbind replaces them with in any way, in order to achieve this we relate de Bruijn terms to an abstract tree representation; then, we can use that tree representation as the structural metric to prove termination for the de Bruijn to HOAS translation.

%sort etree %.
%term etree/lam %pi etree %-> etree %.
%term etree/app %pi etree %-> etree %-> etree %.
%term etree/var etree %.
%sort id-etree {_ etree} {_ etree} %.
%term id-etree/refl id-etree E E %.
%sort id-etree/app-cong {_ id-etree E1 E1'} {_ id-etree E2 E2'} {_ id-etree (etree/app E1 E2) (etree/app E1' E2')} %.
%mode id-etree/app-cong %in %in %out %.
%term _ id-etree/app-cong id-etree/refl id-etree/refl id-etree/refl %.
%worlds () (id-etree/app-cong _ _ _) %.
%total {} (id-etree/app-cong _ _ _) %.
%sort id-etree/lam-cong {_ id-etree E E'} {_ id-etree (etree/lam E) (etree/lam E')} %.
%mode id-etree/lam-cong %in %out %.
%term _ id-etree/lam-cong id-etree/refl id-etree/refl %.
%worlds () (id-etree/lam-cong _ _) %.
%total {} (id-etree/lam-cong _ _) %.

Encoding terms

We choose an intrinsic encoding of de Bruijn terms so that every term that passes the LF type checker is well-formed - in particular, a term with exp^ N is a well-formed de Bruijn term inside of N lambdas. An earlier version of this encoding had a separate well-formedness judgment; the upshot of this encoding was that a lot of complexity got rephrased in terms of simple reasoning about relations like lt+.

The structural metric is made a part of the intrinsic in order to simplify later proofs.

%sort exp^ {_ nat} {_ etree} %.
%term lam^ %pi (exp^ (s N) Et) %-> (exp^ N (etree/lam Et)) %.
%term app^ %pi (exp^ N Et1) %-> (exp^ N Et2) %-> (exp^ N (etree/app Et1 Et2)) %.
%term fvar^ {x exp} %pi (isvar x) %-> (exp^ N etree/var) %.
%term bvar^ {n nat} %pi (lt n M) %-> (exp^ M etree/var) %.

We will think of de Bruijn terms in two different ways depending on whether we are thinking in terms of a closed world or a world described by blockvar. Recall that in a closed world (i.e. an empty LF context) we cannot form anything with type isvar V, so in an empty context we cannot form a term with fvar^. The fvar^ constructor is what allows us to link HOAS terms and de Bruijn terms, by incorporating variables from the HOAS representation directly inside of a de Bruijn term.

We also define identity and congruence on de Bruijn terms.

%sort id-exp^ {_ exp^ N E1} {_ exp^ M E2} %.
%term id-exp^/refl id-exp^ E E %.
%sort id-bvar^-cong {_ id-nat N N'} {_ id-lt LT LT'} {_ id-exp^ (bvar^ N LT) (bvar^ N' LT')} %.
%term _ id-bvar^-cong id-nat/refl id-lt/refl id-exp^/refl %.
%mode id-bvar^-cong %in %in %out %.
%worlds (blockvar) (id-bvar^-cong _ _ _) %.
%total {} (id-bvar^-cong _ _ _) %.
%sort id-app^-cong {_ id-exp^ E1 E1'} {_ id-exp^ E2 E2'} {_ id-exp^ (app^ E1 E2) (app^ E1' E2')} %.
%term _ id-app^-cong id-exp^/refl id-exp^/refl id-exp^/refl %.
%mode id-app^-cong %in %in %out %.
%worlds (blockvar) (id-app^-cong _ _ _) %.
%total {} (id-app^-cong _ _ _) %.
%sort id-lam^-cong {_ id-exp^ E E'} {_ id-exp^ (lam^ E) (lam^ E')} %.
%term _ id-lam^-cong id-exp^/refl id-exp^/refl %.
%mode id-lam^-cong %in %out %.
%worlds (blockvar) (id-lam^-cong _ _) %.
%total {} (id-lam^-cong _ _) %.

Binding and unbinding

The key operations on de Bruijn terms are a binding and unbinding operation - essentially, bind takes a free (HOAS) variable and makes it a different free (de Bruijn) variable. By way of an example, if we have $x,y \vdash (\lambda 1 x) y$ , then binding $x$ will result in $y \vdash (\lambda 1 2) y$ , and binding $y$ will result in $x \vdash (\lambda 1 x) 1$ .

Unfortunately, the structural metric ends up being included in both bind and unbind, which complicates the otherwise relatively simple judgments significantly.

%sort bind {_ {v} %pi (isvar v) %-> (exp^ N Et)} {_ exp^ (s N) Et} %.
%mode bind %in %out %.
%term bind/match %pi (bind ([v] [iv] fvar^ v iv) (bvar^ N LT)) %<- (lts N LT) %.
%term bind/fvar bind ([v] [iv] fvar^ X V) (fvar^ X V) %.
%term bind/bvar %pi (bind ([v] [iv] bvar^ M LT) (bvar^ M LT')) %<- (lt+ LT LT') %.
%term bind/app
  %pi (bind ([v] [iv] app^ (E1 v iv) (E2 v iv)) (app^ E1' E2'))
  %<- (bind ([v] [iv] E1 v iv) E1')
  %<- (bind ([v] [iv] E2 v iv) E2') %.
%term bind/lam %pi (bind ([v] [iv] lam^ (E v iv)) (lam^ E')) %<- (bind ([v] [iv] E v iv) E') %.
%worlds (blockvar) (bind _ _) %.
%total T (bind T _) %.
%sort unbind-bvar {_ lt12 M (s N)} {_ {v} %pi (isvar v) %-> (exp^ N etree/var)} %.
%mode unbind-bvar %in %out %.
%term unbind-bvar/match unbind-bvar lt12/1 ([v] [iv] fvar^ v iv) %.
%term unbind-bvar/nomatch unbind-bvar (lt12/2 LT) ([v] [iv] bvar^ M LT) %.
%worlds (blockvar) (unbind-bvar _ _) %.
%total {} (unbind-bvar _ _) %.
%sort unbind {_ exp^ (s N) Et} {_ {v} %pi (isvar v) %-> (exp^ N Et)} %.
%mode unbind %in %out %.
%term unbind/fvar unbind (fvar^ V' IV') ([v] [iv] fvar^ V' IV') %.
%term unbind/bvar
  %pi (unbind (bvar^ M LT) ([v] [iv] E v iv))
  %<- (lt-opt LT LT12)
  %<- (unbind-bvar LT12 ([v] [iv] E v iv)) %.
%term unbind/app
  %pi (unbind (app^ E1 E2) ([v] [iv] app^ (E1' v iv) (E2' v iv)))
  %<- (unbind E1 ([v] [iv] E1' v iv))
  %<- (unbind E2 ([v] [iv] E2' v iv)) %.
%term unbind/lam
  %pi (unbind (lam^ E1) ([v] [iv] lam^ (E1' v iv)))
  %<- (unbind E1 ([v] [iv] E1' v iv)) %.
%worlds (blockvar) (unbind _ _) %.
%total T (unbind T _) %.

Properties of bind and unbind

Now we will show that bind and unbind are inverses of each other, which mirrors the proof we will eventually prove about the exp->db and db->exp being inverses of each other. In particular, in unbind-uniq we need to use reasoning from false along with a special lemma.

The theorem statements were difficult to get correct, but the proofs are relatively straightforward and are omitted (they are present in the full source code for this page).

%sort bind-uniq {_ {v} {iv isvar v} id-exp^ (Ea v iv) (Ea' v iv)} {_ bind Ea Eb} {_ bind Ea' Eb'} {_ id-exp^ Eb Eb'} %.
%mode bind-uniq %in %in %in %out %.
%{}%
%sort unbind-uniq {_ id-exp^ Ea Ea'} {_ unbind Ea Eb} {_ unbind Ea' Eb'} {_ {v} {iv isvar v} id-exp^ (Eb v iv) (Eb' v iv)} %.
%mode unbind-uniq %in %in %in %out %.
%{}%
%sort bind-unbind {_ bind ([v] E^ v) E^'} {_ unbind E^' ([v] E^ v)} %.
%mode bind-unbind %in %out %.
%{}%
%sort unbind-bind {_ unbind E^ ([v] E^' v)} {_ bind ([v] E^' v) E^} %.
%mode unbind-bind %in %out %.
%{|hidden=true}%
% Cases for bind-uniq
%term _ bind-uniq ([v] [iv] id-exp^/refl) bind/fvar bind/fvar id-exp^/refl %.
%term _
  %pi (bind-uniq ([v] [iv] id-exp^/refl) (bind/bvar LT+) (bind/bvar LT+') ID)
  %<- (lt+-uniq id-lt/refl LT+ LT+' ID+)
  %<- (id-bvar^-cong id-nat/refl ID+ ID) %.
%term _
  %pi (bind-uniq ([v] [iv] id-exp^/refl) (bind/match LTS) (bind/match LTS') ID)
  %<- (lts-uniq id-nat/refl LTS LTS' IDS)
  %<- (id-bvar^-cong id-nat/refl IDS ID) %.
%term _
  %pi (bind-uniq ([v] [iv] id-exp^/refl) (bind/app F2 F1) (bind/app F2' F1') ID)
  %<- (bind-uniq ([v] [iv] id-exp^/refl) F1 F1' ID1)
  %<- (bind-uniq ([v] [iv] id-exp^/refl) F2 F2' ID2)
  %<- (id-app^-cong ID1 ID2 ID) %.
%term _
  %pi (bind-uniq ([v] [iv] id-exp^/refl) (bind/lam F1) (bind/lam F1') ID)
  %<- (bind-uniq ([v] [iv] id-exp^/refl) F1 F1' ID1)
  %<- (id-lam^-cong ID1 ID) %.
%worlds (blockvar) (bind-uniq _ _ _ _) %.
%total T (bind-uniq _ T _ _) %.
% Cases for unbind-uniq
%sort lem {Eb {v} %pi (isvar v) %-> (exp^ N Et)} {Eb' {v} %pi (isvar v) %-> (exp^ N Et)} {_ uninhabited} {_ {v} {iv isvar v} id-exp^ (%the (exp^ N Et) (Eb v iv)) (%the (exp^ N Et) (Eb' v iv))} %.
%mode lem %in %in %in %out %.
%worlds (blockvar) (lem _ _ _ _) %.
%total {} (lem _ _ _ _) %.
%term _ unbind-uniq id-exp^/refl unbind/fvar unbind/fvar ([v] [iv] id-exp^/refl) %.
%term _
  %pi (unbind-uniq id-exp^/refl (unbind/bvar unbind-bvar/match A) (unbind/bvar unbind-bvar/nomatch B) ID)
  %<- (lt-opt-excl A B X)
  %<- (lem _ _ X ID) %.
%term _
  %pi (unbind-uniq id-exp^/refl (unbind/bvar unbind-bvar/nomatch A) (unbind/bvar unbind-bvar/match B) ID)
  %<- (lt-opt-excl B A X)
  %<- (lem _ _ X ID) %.
%term _ unbind-uniq id-exp^/refl (unbind/bvar unbind-bvar/match A) (unbind/bvar unbind-bvar/match B) ([v] [iv] id-exp^/refl) %.
%term _
  %pi (unbind-uniq id-exp^/refl (unbind/bvar unbind-bvar/nomatch (%the (lt-opt LT (lt12/2 LT2)) Opt1)) (unbind/bvar unbind-bvar/nomatch (%the (lt-opt LT (lt12/2 LT2')) Opt2)) ID)
  %<- (lt-opt2-uniq id-lt/refl Opt1 Opt2 ID1)
  %<- ({v} {iv isvar v} id-bvar^-cong id-nat/refl ID1 (ID v iv)) %.
%term _
  %pi (unbind-uniq id-exp^/refl (unbind/app E2 E1) (unbind/app E2' E1') ID)
  %<- (unbind-uniq id-exp^/refl E1 E1' ID1)
  %<- (unbind-uniq id-exp^/refl E2 E2' ID2)
  %<- ({v} {iv isvar v} id-app^-cong (ID1 v iv) (ID2 v iv) (ID v iv)) %.
%term _
  %pi (unbind-uniq id-exp^/refl (unbind/lam E) (unbind/lam E') ID)
  %<- (unbind-uniq id-exp^/refl E E' ID1)
  %<- ({v} {iv isvar v} id-lam^-cong (ID1 v iv) (ID v iv)) %.
%worlds (blockvar) (unbind-uniq _ _ _ _) %.
%total T (unbind-uniq _ T _ _) %.
% Cases for bind-unbind
%term _ bind-unbind bind/fvar unbind/fvar %.
%term _
  %pi (bind-unbind (bind/match (%the (lts N LT) LTS)) (unbind/bvar unbind-bvar/match Opt))
  %<- (lt-opt-succ1 LT Opt) %.
%term _
  %pi (bind-unbind (bind/bvar (%the (lt+ LT LT') LT+)) (unbind/bvar unbind-bvar/nomatch Opt))
  %<- (lt-opt-succ2 LT+ Opt) %.
%term _
  %pi (bind-unbind (bind/app B2 B1) (unbind/app U2 U1))
  %<- (bind-unbind B1 U1)
  %<- (bind-unbind B2 U2) %.
%term _ %pi (bind-unbind (bind/lam B) (unbind/lam U)) %<- (bind-unbind B U) %.
%worlds (blockvar) (bind-unbind _ _) %.
%total T (bind-unbind T _) %.
% Cases for unbind-bind
%term _ unbind-bind unbind/fvar bind/fvar %.
%term _
  %pi (unbind-bind (unbind/bvar unbind-bvar/match Opt) (bind/match LTS))
  %<- (can-lts _ _ LTS) %.
%term _
  %pi (unbind-bind (unbind/bvar unbind-bvar/nomatch (%the (lt-opt LT' (lt12/2 LT)) Opt)) (bind/bvar LT+))
  %<- (can-lt+ LT LT' LT+) %.
%term _
  %pi (unbind-bind (unbind/app U2 U1) (bind/app B2 B1))
  %<- (unbind-bind U1 B1)
  %<- (unbind-bind U2 B2) %.
%term _ %pi (unbind-bind (unbind/lam U) (bind/lam B)) %<- (unbind-bind U B) %.
%worlds (blockvar) (unbind-bind _ _) %.
%total T (unbind-bind T _) %.
%{}%

Relating HOAS and de Bruijn representations

This is the penultimate section. What we want to prove, ultimately, is a bijection between closed HOAS terms and closed de Bruijn terms; however, in order to get there we will prove a bijection between open HOAS terms and open de Bruijn terms, which is the subject of this section. Doing so requires reasoning with the structural metric, using the complex blockcases block description, and generally making a mess. The theorem about closed terms in the next session will be simpler, but will use the more complex lemmas from this section.

HOAS to de Bruijn

It is here that we will need to use the blockcases block description discussed above; even though it makes the translation more complicated, we directly prove the translation total in order to avoid writing a ton of effectiveness lemmas; the uniqueness of this translation is simple, but dependent on the effectiveness of bind.

%sort exp->db {E} {_ case E} {Et} {_ exp^ z Et} %.
%mode exp->db %in %in %out %out %.
%term exp->db/var exp->db _ (case/var IV) etree/var (fvar^ V IV) %.
%term exp->db/lam
  %pi (exp->db (lam ([v] E2 v)) case/lam (etree/lam Et) (lam^ E^'))
  %<- ({v} {iv isvar v} %pi (can-case v (case/var iv)) %-> (can-case (E2 v) (CASE v iv)))
  %<- ({v} {iv isvar v} %pi (can-case v (case/var iv)) %-> (exp->db (E2 v) (CASE v iv) Et (E^'' v iv)))
  %<- (bind E^'' E^') %.
%term exp->db/app
  %pi (exp->db (app E1 E2) case/app (etree/app Et1 Et2) (app^ E1' E2'))
  %<- (can-case E1 CASE1)
  %<- (can-case E2 CASE2)
  %<- (exp->db E1 CASE1 Et1 E1')
  %<- (exp->db E2 CASE2 Et2 E2') %.
%worlds (blockcases) (exp->db _ _ _ _) %.
%total T (exp->db T _ _ _) %.
%{}%
%sort uniq->db {_ exp->db E2 C Et E^} {_ exp->db E2 C Et' E^'} {_ id-etree Et Et'} {_ id-exp^ E^ E^'} %.
%mode uniq->db %in %in %out %out %.
%term _ uniq->db exp->db/var exp->db/var id-etree/refl id-exp^/refl %.
%term _
  %pi (uniq->db (exp->db/lam F T C) (exp->db/lam F' T' C') IDe ID^)
  %<- ({v} {iv isvar v} {c can-case v (case/var iv)} uniq->db (T v iv c) (T' v iv c) IDe1 (ID^1 v iv))
  %<- (bind-uniq ID^1 F F' ID^2)
  %<- (id-etree/lam-cong IDe1 IDe)
  %<- (id-lam^-cong ID^2 ID^) %.
%term _
  %pi (uniq->db (exp->db/app T2 T1 C2 C1) (exp->db/app T2' T1' C2' C1') IDe ID^)
  %<- (uniq->db T1 T1' IDe1 ID^1)
  %<- (uniq->db T2 T2' IDe2 ID^2)
  %<- (id-etree/app-cong IDe1 IDe2 IDe)
  %<- (id-app^-cong ID^1 ID^2 ID^) %.
%worlds (blockcases) (uniq->db _ _ _ _) %.
%total T (uniq->db T _ _ _) %.

de Bruijn to HOAS

It is here that we will need to use the etree structural metric to provide a usable termination argument for db->exp.

%sort db->exp {Et} {_ exp^ z Et} {E} {_ case E} %.
%mode db->exp %in %in %out %out %.
%term db->exp/fvar db->exp etree/var (fvar^ V IV) V (case/var IV) %.
%term db->exp/lam
  %pi (db->exp (etree/lam ET) (lam^ E^) (lam E) case/lam)
  %<- (unbind E^ E^')
  %<- ({v} {iv isvar v} %pi (can-case v (case/var iv)) %-> (db->exp ET (E^' v iv) (E v) _)) %.
%term db->exp/app
  %pi (db->exp (etree/app ET1 ET2) (app^ E1^ E2^) (app E1 E2) case/app)
  %<- (db->exp ET1 E1^ E1 _)
  %<- (db->exp ET2 E2^ E2 _) %.
%worlds (blockcases) (db->exp _ _ _ _) %.
%total T (db->exp T _ _ _) %.
%{}%
%sort uniq->exp {_ id-exp^ E^ E^'} {_ db->exp ET E^ E C} {_ db->exp ET' E^' E' C'} {_ id-exp E E'} %.
%mode uniq->exp %in %in %in %out %.
%term _ uniq->exp id-exp^/refl db->exp/fvar db->exp/fvar id-exp/refl %.
%term _
  %pi (uniq->exp id-exp^/refl (db->exp/lam ([v] [iv] [c can-case v (case/var iv)] T v iv c) UB) (db->exp/lam ([v] [iv] [c can-case v (case/var iv)] T' v iv c) UB') ID)
  %<- (unbind-uniq id-exp^/refl UB UB' (%the ({v exp} {iv isvar v} id-exp^ (E v iv) (E' v iv)) ID1))
  %<- ({v} {iv isvar v} {c can-case v (case/var iv)} uniq->exp (ID1 v iv) (T v iv c) (T' v iv c) (ID2 v))
  %<- (id-lam-cong ID2 ID) %.
%term _
  %pi (uniq->exp id-exp^/refl (db->exp/app T2 T1) (db->exp/app T2' T1') ID)
  %<- (uniq->exp id-exp^/refl T1 T1' ID1)
  %<- (uniq->exp id-exp^/refl T2 T2' ID2)
  %<- (id-app-cong ID1 ID2 ID) %.
%worlds (blockcases) (uniq->exp _ _ _ _) %.
%total T (uniq->exp _ T _ _) %.

Composition: HOAS -> de Bruijn -> HOAS

%sort inverseEDE {_ exp->db E C Et E^} {_ db->exp Et E^ E C} %.
%mode inverseEDE %in %out %.
%term _ inverseEDE exp->db/var db->exp/fvar %.
%term _
  %pi (inverseEDE (exp->db/lam B T C) (db->exp/lam T' U))
  %<- (bind-unbind B U)
  %<- ({v} {iv isvar v} {c can-case v (case/var iv)} inverseEDE (T v iv c) (T' v iv c)) %.
%term _
  %pi (inverseEDE (exp->db/app T2 T1 C2 C1) (db->exp/app T2' T1'))
  %<- (inverseEDE T1 T1')
  %<- (inverseEDE T2 T2') %.
%worlds (blockcases) (inverseEDE _ _) %.
%total T (inverseEDE T _) %.
%{}%

Composition: de Bruijn -> HOAS -> de Bruijn

We need one last trick in order to make this proof go through in the opposite direction; we will need an effectiveness lemma on top of an effectiveness lemma! (Effectiveness lemmas can get out of control sometimes.)

%sort can-can-case {C case E} {_ can-case E C} %.
%sort fake %.
%term _ %pi fake %<- (%pi (can-can-case E V) %-> (can-can-case E' V')) %.
%block blockcancases {v} {iv isvar v} {c can-case v (case/var iv)} {cc can-can-case (case/var iv) c}%.
%term _ can-can-case case/app can-case/app %.
%term _ can-can-case case/lam can-case/lam %.
%mode can-can-case %in %out %.
%worlds (blockcancases) (can-can-case _ _) %.
%total {} (can-can-case _ _) %.

With our slightly absurd effectiveness effectiveness lemma in tow, we can complete the proof that composition in the other direction is the identity.

%sort inverseDED {_ db->exp Et E^ E C} {_ exp->db E C Et E^} %.
%mode inverseDED %in %out %.
%term _ inverseDED db->exp/fvar exp->db/var %.
%term _
  %pi (inverseDED (db->exp/lam (%the ({v} {iv isvar v} {c} db->exp Et (E^ v iv) (E v) (Case v iv)) T) U) (exp->db/lam B T' C))
  %<- (unbind-bind U B)
  %<- ({v} {iv isvar v} {c can-case v (case/var iv)} %pi (can-can-case (case/var iv) c) %-> (inverseDED (T v iv c) (T' v iv c)))
  %<- ({v} {iv isvar v} {c can-case v (case/var iv)} %pi (can-can-case (case/var iv) c) %-> (can-can-case _ (C v iv c))) %.
%term _
  %pi (inverseDED (db->exp/app T2 T1) (exp->db/app T2' T1' C2 C1))
  %<- (inverseDED T1 T1')
  %<- (inverseDED T2 T2')
  %<- (can-can-case _ C1)
  %<- (can-can-case _ C2) %.
%worlds (blockcancases) (inverseDED _ _) %.
%total T (inverseDED T _) %.
%{}%

Wrapping up

The one step that remains is to perform the above four steps for a simpler theorem statement in a closed world, since ultimately what we want is a theorem about closed terms anyway. These theorems would likely be less useful in practice than the ones already proven because the closed world assumption makes them less general, but they more concisely state what was done.

exp-->db is a total and unique relation between HOAS to de Bruijn terms, and can therefore be thought of as the function e2d.

%sort exp-->db {_ exp} {_ exp^ z Et} %.
%term exp-->db/
  %pi (exp-->db E E^)
  %<- (can-case E (%the (case E) C))
  %<- (exp->db E C Et (%the (exp^ z Et) E^)) %.
%mode exp-->db %in %out %.
%worlds () (exp-->db _ _) %.
%total {} (exp-->db _ _) %.
%sort uniq-->db {_ exp-->db E E1} {_ exp-->db E E2} {_ id-exp^ E1 E2} %.
%term _ %pi (uniq-->db (exp-->db/ ED C) (exp-->db/ ED' C') ID) %<- (uniq->db ED ED' _ ID) %.
%mode uniq-->db %in %in %out %.
%worlds () (uniq-->db _ _ _) %.
%total {} (uniq-->db _ _ _) %.

db-->exp is a total and unique relation between de Bruijn terms to HOAS, and can therefore be thought of as the function d2e.

%sort db-->exp {_ exp^ z Et} {_ exp} %.
%term db-->exp/ %pi (db-->exp E^ E) %<- (db->exp Et E^ E _) %.
%mode db-->exp %in %out %.
%worlds () (db-->exp _ _) %.
%total {} (db-->exp _ _) %.
%sort uniq-->exp {_ db-->exp E E1} {_ db-->exp E E2} {_ id-exp E1 E2} %.
%term _
  %pi (uniq-->exp (db-->exp/ DE) (db-->exp/ DE') ID)
  %<- (uniq->exp id-exp^/refl DE DE' ID) %.
%mode uniq-->exp %in %in %out %.
%worlds () (uniq-->exp _ _ _) %.
%total {} (uniq-->exp _ _ _) %.

For all closed de Bruijn terms E, d2e(e2d E) = E.

%sort db-->exp-->db {_ db-->exp E^ E} {_ exp-->db E E^} %.
%term _
  %pi (db-->exp-->db (db-->exp/ DE) (exp-->db/ ED C))
  %<- (inverseDED DE (%the (exp->db E Case Et E^) ED))
  %<- (can-can-case Case C) %.
%mode db-->exp-->db %in %out %.
%worlds () (db-->exp-->db _ _) %.
%total {} (db-->exp-->db _ _) %.

For all closed HOAS terms E, e2d (d2e E) = E.

%sort exp-->db-->exp {_ exp-->db E E^} {_ db-->exp E^ E} %.
%term _ %pi (exp-->db-->exp (exp-->db/ ED C) (db-->exp/ DE)) %<- (inverseEDE ED DE) %.
%mode exp-->db-->exp %in %out %.
%worlds () (exp-->db-->exp _ _) %.
%total {} (exp-->db-->exp _ _) %.
%{}%

Examples

It’s also a good idea to run a %query on some examples as a sanity check. First, we translate the Church numeral “4,” $\lambda f.\lambda x.f(f(f(f x)))$ from a HOAS to a de Bruijn index representation.

%query 1 _ _ exp-->db (lam ([f] lam ([x] app f (app f (app f (app f x)))))) DB %.

Next, we translate the Church boolean operator “Not,” $\lambda p . p (\lambda x . \lambda y . y) (\lambda x . \lambda y . x)$ from a Bruijn index to a HOAS representation.

%query 1 _ _ db-->exp (lam^ (app^ (app^ (bvar^ z lt/z) (lam^ (lam^ (bvar^ z lt/z)))) (lam^ (lam^ (bvar^ (s z) (lt/s lt/z)))))) HOAS %.