Talk:Ask Twelf Elf/Archive 2

From The Twelf Project

Contents 1 two questions from a complete novice. 2 Forcing coverage checker to split on particular variables 3 Mapping HOAS isomorphically to the natural numbers 4 commutativity of plus in the introduction 5 definition violation 5.1 Response

[edit] two questions from a complete novice.

1 I can't find any papers comparing Coq and Twelf. Can someone summarize the differences?

2 Can you explain the vast difference in style between the examples shown on this site and what is done by Andrew Appel at Princeton? The two styles seem as if they are two completely different languages!

Thanks. -Michael Fortson

Hi Michael; thanks for your questions! I've started answering them on the Answers page. Drl 16:43, 8 April 2007 (EDT)

[edit] Forcing coverage checker to split on particular variables

I'm writing a proof of something that involves a relation (synchronizes-with) between two evaluation relations. Evaluation is defined (basically) as a pair of two execution states, each including a program term. Something like:

 eAdd : plus I1 I2 I3 -> eval (add (lit I1) (lit I2)) (lit I3)

(Here's I'm highly simplifying my example).

Now in my proof, I do case analysis based on the evaluation relation

 eAdd: ..
 eSub: ...
 ...

But the Twelf coverage checker insists on splitting on the term syntax instead, and so finds hundreds of cases I haven't handled, such as

 eval (add (lit I1) (lit I2)) (sub (lit I3) (lit I4))

but of course, I don't handle this case because it doesn't occur.

Turning chatter on to 6, I can see that the coverage checker considers splitting on the evaluation relation but then finds that the syntax has fewer choices and so decides to split on it instead; and because syntax is recursive, it can do such splits indefinitely until it gives up.

How can I convince the input coverage checker (called with %total) to split on the "correct" variable?

For completeness, here is the lemma itself. It uses many thousands of lines of previous Twelf code that I could zip up if it would help, but I expect that other people have encountered the same problem before:

%theorem synchs-with?-total*/hold+synch :
	forall* {G} {P1} {M1} {KN1} {A1} {O1} {O1'} {S1'}
                    {P2} {M2} {KN2} {A2} {O2} {T2}  {S2'} {CO}
        forall 
        {E1:eval G P1 (state/ M1 KN1 (hold A1 O1 (lit O1'))) S1'}
        {E2:eval G P2 (state/ M2 KN2 (synch A2 (lit O2) T2)) S2'}
        {CMPO:compare O1 O2 CO}
        {TNA1: thread-not-ancestor P1 P2}
        {TNA2: thread-not-ancestor P2 P1}
        exists {B} {SW?:synchs-with? E1 E2 B}
	true.

...

- : synchs-with?-total*/hold+synch _ (eAcqS2 _ _ _) _ N1 N2 _
	(synchs-with?/no (not-synchs-with/eRelS+eAcqS N1 N2)).

%worlds () (synchs-with?-total*/hold+synch _ _ _ _ _ _ _).
%total (E) (synchs-with?-total*/hold+synch _ E _ _ _ _ _).

I'm using Twelf 1.5R1, but would switch to 1.5R3 if this is a known problem fixed in 1.5R3.

I don't really understand the problem yet, it may be that I need either more code or a better understanding of what you're doing. In general, reasoning from false that is a solution that works when you are trying to get Twelf to recognize that a problem can't occur, you show that in cases where Twelf's coverage checker can't find a problem, there is nevertheless a contradiction. It's also a possibility that the coverage checker doesn't behave correctly in this case because of the %theorem syntax, while this is doubtful it's worth confirming that this *doesn't* work.

It's not the theorem syntax. Here reasoning from false would be incredibly painful here: I would have to enumerate each possible syntax pattern and program state that a hold or synch cannot evaluate to. But I may be forced to do this.Boyland 03:37, 18 May 2007 (EDT)

synchs-with?-total*/hold+synch : 
        eval G P1 (state/ M1 KN1 (hold A1 O1 (lit O1'))) S1' ->
        eval G P2 (state/ M2 KN2 (synch A2 (lit O2) T2)) S2' ->
        compare O1 O2 CO ->
        thread-not-ancestor P1 P2 ->
        thread-not-ancestor P2 P1 ->
        % => 
        {B} synchs-with? E1 E2 B -> type.
%mode synchs-with?-total*/hold+synch +E1 +E2 +C +T1 +T2 -B -S.

Assuming that's not the problem, since (I believe) coverage checking goes from the later arguments to the earlier arguments, it might also be worth trying to change the order of the arguments. I may have this incorrect or backwards, however, so take with a grain of salt:

I moved E1 and E2 to the end, and the coverage checker dutifully considers them first:

   Split E2 in synchs-with?-total*/hold+synch CMPO TNA1 TNA2 E1 E2 B SW?
   Inactive split:
   synch X1 (lit N1) X2 = X3 X4.
   Split E1 in synchs-with?-total*/hold+synch CMPO TNA1 TNA2 E1 E2 B SW?
   Inactive split:
   hold X1 N1 (lit N2) = X2 X3.
   Split CMPO in synchs-with?-total*/hold+synch CMPO TNA1 TNA2 E1 E2 B SW?

The "Inactive split" messages (chatter 7) are interesting and may be the key to why coverage is failing. For some reason, Twelf doesn't want to split on the variable it needs to if it wishes to prove the theorem. Boyland 04:20, 18 May 2007 (EDT)

synchs-with?-total*/hold+synch : 
        thread-not-ancestor P1 P2 ->
        thread-not-ancestor P2 P1 ->
        compare O1 O2 CO ->
        eval G P1 (state/ M1 KN1 (hold A1 O1 (lit O1'))) S1' ->
        eval G P2 (state/ M2 KN2 (synch A2 (lit O2) T2)) S2' ->
        % => 
        {B} synchs-with? E1 E2 B -> type.
%mode synchs-with?-total*/hold+synch +E1 +E2 +C +T1 +T2 -B -S.

As another idea, it could be the case that, if you already have something like a progress theorem for the language, that the problem is that the last argument to eval is being treated like an input instead of like an output, and that the %mode on your theorem needs to be modified to recognize that.

Hope one of these suggestions is somewhat enlightening... — Rob (and his talk) 09:46, 14 May 2007 (EDT)

I don't understand the details your example, but in my experience this sort of error message (the coverage checker finding a bunch of uncovered cases, albeit not by splitting the term you want it to) often results from a bug in a proof. Though I've heard that there are some pathological cases where the coverage checker splits the wrong term and is consequently unable to split the term it needs to split, I've personally never run into such a case. When I've gotten an error message like this, it's been because my proof is wrong (but the coverage checker's error message is somewhat surprising because it's not splitting the same term that I would split). So the problem may have nothing to do with the details of the coverage checker; it's possible that you simply haven't defined a total relation. The technique described in Debugging coverage errors might help you debug. And, as Rob said, it may be a situation where you need to explicitly contradict some cases (using reasoning from false) because the coverage checker isn't automatically ruling them out. Drl 12:27, 16 May 2007 (EDT)

It is indeed possible that I have omitted a case, however, it sure would be easier to find it if the coverage checker split on the variable I want it to: by splitting on the wrong variables, it ends up with 4000 lines of cases not considered! I'll let you know if/when I resolve the issue. It seems the "Inactive Split" message is key. I'm not sure why it is using a higher ordered type here. Here eval* (and friends) have type

state : kind -> type.
state/ : {K:kind} map -> %map -> term K -> state K.
eval* : {K:kind} unit -> nat -> state K -> state K -> type.

eval is abbreviated as eval* with the first parameter (kind) implicit. (Don't be alarmed by the %map% vs. map. It's due to my C-preprocessor-based functor system for Twelf. I've proved many, many things already with these things. Also, the variable K for state/ is implicit. This is from the server output. In the theorem in question K is always exprk)

Maybe someone out there knows why the coverage checker gets the higher-order constraints (and then fails).Boyland 04:20, 18 May 2007 (EDT)

The "Inactive Split" is indeed key: it means that because higher-order unification failed, that Twelf won't split on the variable. I was able to fix this by introducing an equality indirection so that Twelf wouldn't try to unify "(F X)" with "(lit O)" (for example). Maybe somebody (me?) should write up a trouble-shooting tip about this, or is it to esoteric? Boyland 23:45, 20 May 2007 (EDT)

Glad you resolved the problem. It would be great if you'd contribute a trouble-shooting tip about this! Drl 11:40, 22 May 2007 (EDT)

[edit] Mapping HOAS isomorphically to the natural numbers

I need an arbitrary isomorphic mapping between terms and the natural numbers. Without higher-order abstract syntax, this is uninteresting grunt work. With higher-order abstract syntax, I am able to define the mapping:

%%% Definition



%% Untyped lambda calculus using HOAS


exp : type.


app : exp -> exp -> exp.

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



%% Mapping exp isomorphically to the natural numbers


varlevel : exp -> nat -> type.

% only inhabited dynamically



exp2nat : nat -> exp -> nat -> type.

% exp2nat D E N   convert E into a number N assuming we are inside D lambda expressions.



exp2nat/app : exp2nat D (app E1 E2) (s N)
    <- exp2nat D E1 N1
    <- exp2nat D E2 N2
    <- pair2nat (natpair/ N1 N2) N3
    <- plus N3 N3 N4
    <- plus D N4 N.

exp2nat/lam : exp2nat D (lam ([x] B x)) N
    <- ({x} varlevel x D -> exp2nat (s D) (B x) N1)
    <- plus N1 N1 N2
    <- plus D N2 N.


exp2nat/var : exp2nat D V N
    <- varlevel V L
    <- plus (s L) N D.




%%% Blocks



%block bind : some {l:nat} block {x:exp} {D:varlevel x l}.

The first parameter to exp2nat is the depth of lambdas we are in. It is used to "leave space" for the variables in the encoding of the body. When asking for the number for a top-level term, one uses zero.

?- exp2nat z (lam ([x] (lam [y] y))) N.
Solving...
N = s (s z).
More? no
?- exp2nat z (lam ([x] x)) N.
Solving...
N = z.
More? no
?- exp2nat z (lam ([x] (lam [y] x))) N.
Solving...
N = s (s (s (s (s (s z))))).
More? no
?- exp2nat z (app (lam ([x] x)) (lam ([y] y))) N.
Solving...
N = s z.
More? no
?- exp2nat z (app (lam ([x] x)) (app (lam ([x] x)) (lam ([y] y)))) N.
Solving...
N = s (s (s z)).
More? no

I don't see how to prove things about it. Assuming natpair has a provably isomorphic mapping to the natural numbers (I can post that too if you want) and that we have all the theorems about plus we could care about, plus division and multiplication thrown in "for free", it still seems tricky.

The big problem is proving 1-1 and onto. I have zero experience with non-trivial "worlds", but it seems to me that a lemma will have to use that the "varlevel" bindings are all distinct, and indeed fill up the values 0,1,...,D-1 where D is the depth parameter to exp2nat. I don't see how to do this.

Perhaps there's a better way to define the mapping? (In fact, my encoding may be incorrect---I haven't proved it is correct!) Boyland 21:28, 26 June 2007 (EDT)

---

I can rephrase the problem ignoring the messiness of arithmetic, by asking about an isomorphism between HOAS and nameless terms, since nameless terms are normal syntax for which I know how to make provable isomorphisms to the natural numbers. As an added bonus, the following Twelf code is self-contained:

%%% Definitions



%% Natural numbers


nat : type.

z : nat.

s : nat -> nat.



%% Untyped lambda calculus using HOAS


exp : type.


app : exp -> exp -> exp.

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



%% deBruijn variables


dbvar : nat -> type.


0 : dbvar (s N).

^ : dbvar N -> dbvar (s N).



%% deBruijn terms


dbterm : nat -> type.


dbuse : dbvar N -> dbterm N.

dblam : dbterm (s N) -> dbterm N.

dbapp : dbterm N -> dbterm N -> dbterm N.



%% Mapping exp isomorphically to debruijn terms


varlevel : exp -> nat -> type.    only inhabited dynamically



exp2db : {N} exp -> dbterm N -> type.

nat2db : {N} nat -> dbvar N -> type.


exp2db/app : exp2db D (app E1 E2) (dbapp DB1 DB2)
    <- exp2db D E1 DB1
    <- exp2db D E2 DB2.

exp2db/lam : exp2db D (lam ([x] B x)) (dblam DB)
    <- ({x} varlevel x D -> exp2db (s D) (B x) DB).

exp2db/var : exp2db D V (dbuse DBV)
    <- varlevel V L
    <- nat2db D L DBV.


nat2db/0 : nat2db (s z) z 0.

nat2db/^ : nat2db D N V -> nat2db (s D) N (^ V).

nat2db/- : nat2db (s D) N 0 -> nat2db (s (s D)) (s N) 0.

The definition of deBruijn terms is carefully written to ensure that there is only one way to write each lambda expression. (The representation in the the Twelf source examples directory does not enjoy this property.) So my challenge to Twelfers everywhere is prove

1. that exp2db is total: for every E there exists D such that exp2db z E D.

2. that exp2db is deterministic: there exists exactly one such D

3. that exp2db is onto: for every deBruijn term D, there exists E such that exp2nat z E D

4. that exp2db is one2one: there exists exactly one such E.

(Or provide a counter example if I have an error in my "isomorphism.") Boyland 22:09, 16 August 2007 (EDT)

This took a little while - I think the end result is pleasant enough, but some of the arguments for how to get there weren't obvious. My approach is rather different than yours, but the end result is the same - a correspondence between closed HOAS terms and closed de Bruijn terms (my de Bruijn terms are slightly different than yours because they have an extra index encoding a structural metric, but it is obvious to me, and it shouldn't be hard to prove, that these are in correspondance with your encoding of de Bruijn terms.

It might be worth trying something similar with this "varlevel" machinery, but I'm not sure all the induction hypotheses that are needed end up working. — Rob (and his talk) 10:02, 4 October 2007 (EDT)

[edit] commutativity of plus in the introduction

I've added a solution to the first problem posed in Dan's tutorial. However, since I'm just learning Twelf now, I suspect that it could be improved, but couldn't get anything else to go through. Could someone experienced have a look and determine if it is the best proof?

Any style tips would also be appreciated. I've got a couple other exercises, which I'll add once I'm sufficiently confident that I'm doing things in a reasonable way.

--Ccasin 15:37, 2 October 2007 (EDT)

Those solutions seem pretty good to me! The only style note I have is lemma naming. This is really a complete matter of personal preference, but similar to how I write plus/s: plus N M P -> plus (s N) M (s P)., I find it is more memorable to call what you called "plus-flip" "plus-s," because it's doing roughly the same thing as plus/s but in another direction (and as a metatheorem, not a constructor). Happy Twelfing! — Rob (and his talk) 09:54, 4 October 2007 (EDT)

%{

[edit] definition violation

I defined a simple dependently-typed language but when I went to prove Preservation I get this error message which is mystifying me.

 Definition violation: family preserv |> expr, which occurs as
 right-hand side of a type-level definition.

I checked the manual on Subordination but I don't understand how preserv can be a subterm of expr.

I also noticed that the Wiki page on Subordination seems to use flipped syntax from the manual, which isn't helping.

Print.subord uses #> syntax for which I cannot find a definition.

 Expressions (also types)
expr : type. %name expr E.
tp   = expr.

$    : expr -> expr -> expr. %infix left 50 $.
lam  : expr -> (expr -> expr) -> expr.
pi   : expr -> (expr -> expr) -> expr.
star : expr.
box  : expr.
=>   = [a:expr] [b:expr] pi a ([_] b). %infix right 50 =>.
%freeze expr.

allowed-kinds : expr -> expr -> type.
%mode allowed-kinds +E1 +E2.
akss : allowed-kinds star star.
akbb : allowed-kinds box box.
akbs : allowed-kinds box star.
aksb : allowed-kinds star box.
%worlds () (allowed-kinds _ _).
%terminates {} (allowed-kinds _ _).

 Values
value : expr -> type.
%mode value +E1.
value-lam : value (lam _ _).
value-pi  : value (pi _ _).
value-star : value star.
value-box  : value box.
%worlds () (value _).
%terminates {} (value _).

 Call-by-name small step operational semantics.
|-> : expr -> expr -> type. %infix left 10 |->.
%mode |-> +E1 -E2.
|->$    : E1 $ E2 |-> E1' $ E2
           <- E1 |-> E1'.
|->beta : lam _ E1 $ E2 |-> E1 E2.
%worlds () (|-> _ _).
%terminates E (|-> E _).

 Multi-step
|->* : expr -> expr -> type. %infix left 10 |->*.
%mode |->* +E1 -E2.
|->*refl  : E |->* E.
|->*trans : E |->* E'' <- E |-> E' <- E' |->* E''.
%worlds () (|->* _ _).

 Normal form
nf : expr -> expr -> type.
%mode nf +E1 -E2.
nf-value : nf E E <- value E.
nf-multi : nf E E' <- E |->* E' <- value E'.
%worlds () (nf _ _).

 Type-checking
of : expr -> tp -> type.
%mode of +E1 -E2.
of-star : of star box.
of-$    : of (E1 $ E2) (RT E2)
           <- of E1 T
           <- nf T (pi AT RT)
           <- of E2 AT.
of-lam  : of (lam AT E1) (pi AT RT)
           <- ({x:expr} of x AT -> of (E1 x) (RT x)).
of-pi   : of (pi A B) T
           <- of A S'
           <- nf S' S
           <- ({x:expr} of x A -> of (B x) T')
           <- nf T' T
           <- allowed-kinds S T.
%freeze of.



preserv : of E T -> E |-> E' -> of E' T -> type.
%mode preserv +D1 +D2 -D3.
 - : preserv (of-$ DofE2AT DnfT DofE1T) (|->$ DstepE1E1')
      (of-$ DofE2AT DnfT DofE1'T)
      <- preserv DofE1T DstepE1E1' DofE1'T.
 ...
%worlds () (preserv _ _ _).
%total D (preserv _ D _).

 Definition violation: family preserv |> expr, which occurs as
 right-hand side of a type-level definition.

 excerpts from manual

 We say that type family b subordinates type family a, (written b |>
 a) if a term of type b ... might occur as a subterm of a term of
 type a.

 preserv |> expr  =  preserv subordinates expr

 "a term of type preserv might occur as a subterm of a term of type expr."


 Print.subord
 expr #> expr 
 tp |> 
 allowed-kinds #> expr 
 value #> expr 
 |-> #> |-> expr 
 |->* #> |->* |-> expr 
 nf #> |->* value expr 
 of #> of nf allowed-kinds expr 
 preserv #> of expr

[edit] Response

This is poorly explained on the wiki right now, but when you're doing metatheorems then writing things like:

 Expressions (also types)
expr : type. %name expr E.
tp   = expr.

... is a problem - the last line is a type-level definition and is a part of Twelf that was added for very different reasons (see tactical theorem proving). In general, defining a type to be equal to another type is something you should never do if you're writing metatheroems at all. You may be able to partially address your problem by using an abbrev declaration.

 Expressions (also types)
expr : type. %name expr E.
%abbrev tp   = expr.

However, without looking closely at your example there may be a problem with tp = expr - is your intention to make your types and expressions indistinguisable? — Rob (and his talk) 13:27, 26 October 2007 (EDT)

Adding %abbrev did help, in that I am now facing the usual Coverage error. I did intend to make types and expressions the same, in fact, the tp = expr was an afterthought because the original language does not contain a separate family for types (and typechecking is of : expr -> expr -> type). - mrd