Concrete representation

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% OK %%
Output: here.

The use of higher-order abstract syntax, using Twelf's binding structure to represent binding structure in an encoded language, is one of the more unique and convenient aspects of using Twelf. 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 Twelf 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:

  1. exp-->db is a total and unique relation between HOAS to de Bruijn terms, and can therefore be thought of as the function e2d.
  2. db-->exp is a total and unique relation between de Bruijn terms to HOAS, and can therefore be thought of as the function d2e.
  3. For all closed de Bruijn terms E, d2e(e2d E) = E
  4. 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..

uninhabited : type.
%freeze uninhabited.

nat : type.
z : nat.
s : nat -> nat.

id-nat : nat -> nat -> type.
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.

lt : nat -> nat -> type.
lt/z : lt z (s N).
lt/s : lt (s N1) (s N2) <- lt N1 N2.

id-lt : lt N M -> lt N' M' -> type.
id-lt/refl : id-lt L L.

lt12 : nat -> nat -> type.
lt12/1 : lt12 N (s N).
lt12/2 : 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.

lt+ : lt M N -> lt M (s N) -> type.
%mode lt+ +D -D2.
lt+/z : lt+ lt/z lt/z.
lt+/s : lt+ (lt/s LT1) (lt/s LT2) <- lt+ LT1 LT2.
%worlds() (lt+ _ _).
%total T (lt+ T _).

lts : {N} lt N (s N) -> type.
%mode lts +N -LT.
lts/z : lts z lt/z.
lts/s : lts (s N) (lt/s D) <- lts N D.
%worlds () (lts _ _).
%total T (lts 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.

exp : type.
lam : (exp -> exp) -> exp.
app : exp -> exp -> exp.

%block blocksimple : block {v: exp}.

id-exp : exp -> exp -> type.
id-exp/refl : id-exp E E.

id-lam-cong : ({v} id-exp (E v) (E' v)) 
		-> id-exp (lam E) (lam E') -> type.
- : id-lam-cong ([v] id-exp/refl) id-exp/refl.
%mode id-lam-cong +I1 -I.
%worlds (blocksimple) (id-lam-cong _ _).
%total {} (id-lam-cong _ _).

id-app-cong : id-exp E1 E1' 
		-> id-exp E2 E2'
		-> id-exp (app E1 E2) (app E1' E2') -> type.
- : id-app-cong id-exp/refl id-exp/refl id-exp/refl.
%mode id-app-cong +I1 +I2 -I.
%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.

isvar : exp -> type.
%block blockvar : block {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 Twelf's autofreeze feature. If you are running this proof on your own computer, try deleting the line to see Twelf's error message.

case : exp -> type.
case/lam : case (lam [x] E x).
case/app : case (app E1 E2).
case/var : isvar V -> case V.

can-case : {E} case E -> type.
fake : can-case E C -> can-case E C -> type.
- : fake E F <- ({d:can-case X Y} can-case X' Y').

%block blockcases : block {v}{iv: isvar v}{d: can-case v (case/var iv)}.

can-case/lam : can-case (lam [x] E x) (case/lam).
can-case/app : can-case (app E1 E2) (case/app) .
%mode can-case +E -C.
%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 Twelf 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.

etree : type.
etree/lam : etree -> etree.
etree/app : etree -> etree -> etree.
etree/var : etree.

id-etree : etree -> etree -> type.
id-etree/refl : id-etree E E.

id-etree/app-cong : id-etree E1 E1'
		     -> id-etree E2 E2' 
		     -> id-etree (etree/app E1 E2) (etree/app E1' E2') -> type.
%mode id-etree/app-cong +ID +ID2 -ID'.
- : id-etree/app-cong id-etree/refl id-etree/refl id-etree/refl.
%worlds () (id-etree/app-cong _ _ _).
%total {} (id-etree/app-cong _ _ _).

id-etree/lam-cong : id-etree E E' 
		     -> id-etree (etree/lam E) (etree/lam E') -> type.
%mode id-etree/lam-cong +ID -ID'.
- : 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.

exp^  : nat -> etree -> type.
lam^  : exp^ (s N) Et -> exp^ N (etree/lam Et).
app^  : exp^ N Et1 -> exp^ N Et2 -> exp^ N (etree/app Et1 Et2).
fvar^ : {x: exp} isvar x -> exp^ N etree/var.
bvar^ : {n: nat} 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.

id-exp^ : exp^ N E1 -> exp^ M E2 -> type.
id-exp^/refl : id-exp^ E E.

id-bvar^-cong : id-nat N N'
		 -> id-lt LT LT'
		 -> id-exp^ (bvar^ N LT) (bvar^ N' LT') -> type.
- : id-bvar^-cong id-nat/refl id-lt/refl id-exp^/refl.
%mode id-bvar^-cong +D1 +D2 -D^.
%worlds (blockvar) (id-bvar^-cong _ _ _).
%total {} (id-bvar^-cong _ _ _).

id-app^-cong : id-exp^ E1 E1' 
		-> id-exp^ E2 E2' 
		-> id-exp^ (app^ E1 E2) (app^ E1' E2') -> type.
- : id-app^-cong id-exp^/refl id-exp^/refl id-exp^/refl.
%mode id-app^-cong +D1 +D -D2.
%worlds (blockvar) (id-app^-cong _ _ _).
%total {} (id-app^-cong _ _ _).

id-lam^-cong : id-exp^ E E' -> id-exp^ (lam^ E) (lam^ E') -> type.
- : id-lam^-cong id-exp^/refl id-exp^/refl.
%mode id-lam^-cong +D1 -D2.
%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 , then binding will result in , and binding will result in .

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

bind : ({v} isvar v -> exp^ N Et) -> exp^ (s N) Et -> type.
%mode bind +E1 -E.

bind/match : bind ([v][iv] fvar^ v iv) (bvar^ N LT)
		   <- lts N LT.

bind/fvar : bind ([v][iv] fvar^ X V) (fvar^ X V).

bind/bvar : bind ([v][iv] bvar^ M LT) (bvar^ M LT') 
		  <- lt+ LT LT'.

bind/app : 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'.

bind/lam : bind ([v][iv] lam^ (E v iv)) (lam^ E') 
		 <- bind ([v][iv] E v iv) E'.

%worlds (blockvar) (bind _ _).
%total T (bind T _).
unbind-bvar : lt12 M (s N) -> ({v} isvar v -> exp^ N etree/var) -> type.
%mode unbind-bvar +LT -E .

unbind-bvar/match : unbind-bvar lt12/1 ([v][iv] fvar^ v iv).

unbind-bvar/nomatch : unbind-bvar (lt12/2 LT) ([v][iv] bvar^ M LT).

%worlds (blockvar) (unbind-bvar _ _).
%total {} (unbind-bvar _ _).

unbind : exp^ (s N) Et -> ({v} isvar v -> exp^ N Et) -> type.
%mode unbind +E1 -E2.

unbind/fvar : unbind (fvar^ V' IV') ([v][iv] fvar^ V' IV').

unbind/bvar : unbind (bvar^ M LT) ([v][iv] E v iv) 
		   <- lt-opt LT LT12 
		   <- unbind-bvar LT12 ([v][iv] E v iv).

unbind/app : 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).

unbind/lam : 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).

bind-uniq : ({v}{iv:isvar v} id-exp^ (Ea v iv) (Ea' v iv))
		  -> bind Ea Eb
		  -> bind Ea' Eb'
		  -> id-exp^ Eb Eb' -> type.
%mode bind-uniq +I1 +B1 +B2 -I2.
unbind-uniq : id-exp^ Ea Ea'
		   -> unbind Ea Eb
		   -> unbind Ea' Eb'
		   -> ({v}{iv: isvar v} id-exp^ (Eb v iv) (Eb' v iv)) -> type.
%mode unbind-uniq +I1 +U1 +U2 -I2.
bind-unbind : bind ([v] E^ v) E^'
	      -> unbind E^' ([v] E^ v) -> type.
%mode bind-unbind +B -U.
unbind-bind : unbind E^ ([v] E^' v)
	      -> bind ([v] E^' v) E^ -> type.
%mode unbind-bind +U -B.



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.

exp->db : {E} case E -> {Et} exp^ z Et -> type.
%mode exp->db +E +C -Et -E^.

exp->db/var : exp->db _ (case/var IV) etree/var (fvar^ V IV).
exp->db/lam : exp->db (lam ([v] E2 v)) case/lam (etree/lam Et) (lam^ E^')
	       <- ({v}{iv: isvar v} can-case v (case/var iv) ->
		     can-case (E2 v) (CASE v iv))
	       <- ({v}{iv: isvar v} can-case v (case/var iv) ->
		     exp->db (E2 v) (CASE v iv) Et (E^'' v iv))
	       <- bind E^'' E^'.
exp->db/app : 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 _ _ _).
uniq->db : exp->db E2 C Et E^ 
	    -> exp->db E2 C Et' E^' 
	    -> id-etree Et Et'
	    -> id-exp^ E^ E^' -> type.
%mode uniq->db +E1 +E2 -ID1 -ID2.

- : uniq->db exp->db/var exp->db/var id-etree/refl id-exp^/refl.
- : 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^.
- : 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.

db->exp : {Et} exp^ z Et -> {E} case E -> type.
%mode db->exp +ET +E^ -E -C.

db->exp/fvar : db->exp etree/var (fvar^ V IV) V (case/var IV).
db->exp/lam : db->exp (etree/lam ET) (lam^ E^) (lam E) case/lam
	       <- unbind E^ E^'
	       <- {v}{iv: isvar v} can-case v (case/var iv)
		  -> db->exp ET (E^' v iv) (E v) _.
db->exp/app : 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 _ _ _).
uniq->exp : id-exp^ E^ E^'
	     -> db->exp ET E^ E C
	     -> db->exp ET' E^' E' C'
	     -> id-exp E E' -> type.
%mode uniq->exp +ID1 +E1 +E2 -ID.

- : uniq->exp id-exp^/refl db->exp/fvar db->exp/fvar id-exp/refl.
- : 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' 
	(ID1: {v:exp} {iv:isvar v} id-exp^ (E v iv) (E' v iv))
     <- ({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.
- : 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

inverseEDE : exp->db E C Et E^ -> db->exp Et E^ E C -> type.
%mode inverseEDE +ED -DE.

- : inverseEDE exp->db/var db->exp/fvar.
- : 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).
- : 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.)

can-can-case : {C: case E} can-case E C -> type.
fake : type.
- : fake <- (can-can-case E V -> can-can-case E' V').
%block blockcancases
   : block {v}{iv:isvar v}{c:can-case v (case/var iv)}
      {cc:can-can-case (case/var iv) c}.
- : can-can-case case/app can-case/app.
- : can-can-case case/lam can-case/lam.
%mode can-can-case +C -CC.
%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.

inverseDED : db->exp Et E^ E C -> exp->db E C Et E^ -> type.
%mode inverseDED +DE -ED.

- : inverseDED db->exp/fvar exp->db/var.
- : inverseDED (db->exp/lam (T:{v}{iv:isvar v}{c} 
				 db->exp Et (E^ v iv) (E v) (Case v iv)) U) 
     (exp->db/lam B T' C)
     <- unbind-bind U B
     <- ({v}{iv:isvar v}{c:can-case v (case/var iv)}
	   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)}
	   can-can-case (case/var iv) c
	   -> can-can-case _ (C v iv c)).
- : 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.
exp-->db : exp -> exp^ z Et -> type.
exp-->db/ : exp-->db E E^ 
	     <- can-case E (C: case E)
	     <- exp->db E C Et (E^: exp^ z Et).
%mode exp-->db +E -E^.
%worlds () (exp-->db _ _).
%total {} (exp-->db _ _).

uniq-->db : exp-->db E E1 -> exp-->db E E2 -> id-exp^ E1 E2 -> type.
- : uniq-->db (exp-->db/ ED C) (exp-->db/ ED' C') ID
     <- uniq->db ED ED' _ ID.
%mode uniq-->db +E +E' -ID.
%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.
db-->exp : exp^ z Et -> exp -> type.
db-->exp/ : db-->exp E^ E
	     <- db->exp Et E^ E _.
%mode db-->exp +E^ -E.
%worlds () (db-->exp _ _).
%total {} (db-->exp _ _).

uniq-->exp : db-->exp E E1 -> db-->exp E E2 -> id-exp E1 E2 -> type.
- : uniq-->exp (db-->exp/ DE) (db-->exp/ DE') ID
     <- uniq->exp id-exp^/refl DE DE' ID.
%mode uniq-->exp +E +E' -ID.
%worlds () (uniq-->exp _ _ _).
%total {} (uniq-->exp _ _ _).
  • For all closed de Bruijn terms E, d2e(e2d E) = E.
db-->exp-->db : db-->exp E^ E -> exp-->db E E^ -> type.
- : db-->exp-->db (db-->exp/ DE) (exp-->db/ ED C)
     <- inverseDED DE (ED: exp->db E Case Et E^) 
     <- can-can-case Case C.
%mode db-->exp-->db +DE -ED.
%worlds () (db-->exp-->db _ _).
%total {} (db-->exp-->db _ _).
  • For all closed HOAS terms E, e2d (d2e E) = E.
exp-->db-->exp : exp-->db E E^ -> db-->exp E^ E -> type.
- : exp-->db-->exp (exp-->db/ ED C) (db-->exp/ DE)
     <- inverseEDE ED DE.
%mode exp-->db-->exp +ED -DE.
%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," 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.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%query 1 * exp-->db (lam ([f:exp] lam ([x:exp] app f (app f (app f (app f x)))))) DB. ---------- Solution 1 ---------- DB = lam^ (lam^ (app^ (bvar^ (s z) (lt/s lt/z)) (app^ (bvar^ (s z) (lt/s lt/z)) (app^ (bvar^ (s z) (lt/s lt/z)) (app^ (bvar^ (s z) (lt/s lt/z)) (bvar^ z lt/z)))))). ____________________________________________

%% OK %%

Next, we translate the Church boolean operator "Not," 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.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%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. ---------- Solution 1 ---------- HOAS = lam ([x:exp] app (app x (lam ([x1:exp] lam ([x2:exp] x2)))) (lam ([x1:exp] lam ([x2:exp] x1)))). ____________________________________________

%% OK %%