Talk:Ask Twelf Elf
Contents
- 1 Archives
- 2 LF representation of complete development
- 3 Question Regarding Explicit LF Specification Generation
- 4 Queries with non-empty contexts?
- 5 normalization theorems?
- 6 More exercises.
- 7 %Undefine
- 8 hypothetical judgments vs judgments with premises
- 9 proving things about an intensional property
- 10 Negative premises
- 11 Coverage checking
- 12 Twelf User Manual
- 13 freezing violation: X would depend on Y
- 14 Termination and %mode
- 15 POPL tutorial slides location?
- 16 Twelf 1.7.1 ?
- 17 Problem to find an induction metric
- 18 trouble with twelf server
- 19 How to prove totality in this case?
- 20 %reduces not as smart as what is done in %total, it seems
- 21 dictionary in which keys are variable names
- 22 Twelf bug reports?
- 23 Syntax highlighting for IntelliJ IDEA
- 24 Problems with pages
- 25 Can’t solve obvious goal or is it me?
- 26 Twelf pre-built Mac OS distro needs update
Archives
LF representation of complete development
Consider pure lambda terms:
trm : type. lam : (trm -> trm) -> trm. app : trm -> trm -> trm.
Tait/Martin-Loef parallel reduction is represented in Frank Pfenning's paper on Church-Rosser as:
=> : trm -> trm -> type. %infix none 10 =>.
pr1_beta : (app (lam M) N) => M' N'
<- ({x:trm} x => x -> M x => M' x)
<- N => N'.
pr1_app : (app M N) => (app M' N')
<- N => N'
<- M => M'.
pr1_lam : lam M => lam M'
<- ({x:trm} x => x -> M x => M' x).
I'm not completely satisfied by the explanation in Frank's paper for why the pr1_beta rule has higher-order premise "{x:trm} x => x", but pr1 is reflexive, and that premise seems necessary to prove it.
The complete development relation is informally given by the following rules:
----------- x ==> x
M ==> M' N ==> N' ----------------- (M is not a lambda) (M N) ==> (M' N')
M ==> N -------------- \x.M ==> \x.N
M ==> M' N ==> N' ------------------------ (\x.M) N ==> M'[x::=N']
Informally, ==> is the same as => except for the side condition "M is not a lambda" on the application rule. This removes the non-determinism of => and forces ==> to contract every redex in the input term; ==> goes as far as any => can. ==> is a subrelation of =>.
My question is how to represent ==> in LF. There seem to be two issues: how to represent the side condition (the informal system accepts both applications and variables), and what to do about the higher-order premise "{x:trm} x => x" (because ==> is not reflexive).
Thanks, Rpollack 10:16, 28 February 2008 (EST) Randy
- Hi Randy. This is a great question. I've started a tutorial answering it: Working with higher-order judgements. Feel free to discuss the tutorial on its talk page if it's at all unclear. Drl 15:07, 28 February 2008 (EST)
Question Regarding Explicit LF Specification Generation
Question: can Twelf produce a fully explicit LF specification from one that is not fully explicit? By "fully explicit", I mean one that needs no further term reconstruction (all type parameters are explicitly bound). Twelf-sml's Print.sgn is close, but doesn't provide explicit (or even original) %solve or %query directives (nor would I expect it to, as that is not the function's purpose). As a note, Print.sgn places terms declared as infix in head position, which is fine for my use.
The reason I am interested in such functionality is that I want to perform some syntactic analyses of LF specifications. I would like to use existing Twelf specifications as input, but I don't want to manually make type parameters explicit, nor do I want to reimplement term reconstruction. However the analyses require fully explicit input.
Thanks!
Queries with non-empty contexts?
Is it possible to use pi-types in the in the goals for %query? The example below shows what I'm trying to do. Since the workaround using a dummy type family works it does not seem to be an inherent limitation in the logic programming engine... This is Twelf 1.5R1, Mar 8, 2005 (tabling).
exp : type.
app : exp -> exp -> exp.
lam : (exp -> exp) -> exp.
tp : type.
unit : tp.
arrow : tp -> tp -> tp.
of : exp -> tp -> type.
of-app : (of E1 (arrow T1 T2)) -> (of E2 T1) -> of (app E1 E2) T2.
of-lam : of (lam ([x] Body x)) (arrow T1 T2)
<- {x : exp} {Hx : of x T1} of (Body x) T2.
%% finds a solution as expected:
%query 1 1
of (lam ([x] (lam ([y] (app x y))))) T.
%% "found 0" solutions.
%query 1 1
{x : exp} {Hx : of x (arrow unit unit)}
{y : exp} {Hy : of y unit}
of (app x y) T.
%% This works, however.
dummy : tp -> type.
dummy1 : dummy T
<- {x : exp} {Hx : of x (arrow unit unit)}
{y : exp} {Hy : of y unit}
of (app x y) T.
%query 1 1 dummy T.
normalization theorems?
Hello,
I was wandering if the meta logic of Twelf can somehow express (weak or strong) normalization properties. Or if it currently cannot, what would be a natural extension of this meta logic suitable for this?
Thanks,
Andrei Popescu
- See Hereditary substitution for the STLC for an example of normalization of the simply-typed lambda calculus. The common way of stating theorems in Twelf does not extend to logical relations arguments defined by induction on a type; however, see [Structural Logical Relations] for a slightly different way to encode these in Twelf (as it currently exists).
— Rob (and his talk) 02:26, 12 October 2008 (EDT)
More exercises.
Dear Elves,
the Twelf web-page is great to learn about it, but I wish you guys could
post more exercises with answers. It makes it easier to teach teach in the classroom, and it helps self-learners like me. I have coded a simple exercise using even/odd numbers, and I am sending it to you guys, so that maybe you could post it at: http://twelf.plparty.org/wiki/Proving_metatheorems:Natural_numbers:_Answers_to_exercises
All the best,
71.106.190.54 18:25, 23 October 2008 (EDT)Fernando
We have already seen how to proof a theorem showing that the addition of two even numbers produces an even number. This theorem can be stated as follows:
sum-evens : even N1 -> even N2 -> plus N1 N2 N3 -> even N3 -> type. %mode sum-evens +D1 +D2 +D3 -D4.
The proof of our theorem is a simple case analysis on the possible derivations of even numbers:
sez : sum-evens even-z DevenN2 plus-z DevenN2.
ses : sum-evens
(even-s EvenN1)
EvenN2
(plus-s (plus-s PlusN1N2N3))
(even-s EvenN3)
<- sum-evens EvenN1 EvenN2 PlusN1N2N3 EvenN3.
%worlds () (sum-evens _ _ _ _). %total D (sum-evens D _ _ _).
In what follows, you will be asked to write proofs for three similar theorems. Exercise 2 defines lemmas that will be useful in the proofs in Exercise 3.
Exercise 1: define the odd numbers. Start with one, e.g, s z as your base case, and define the other odd numbers inductively.
Answer: ================================================================== % Odd natural numbers: odd : nat -> type. odd-1 : odd (s z). odd-s : odd N -> odd (s (s N)). Answer: ==================================================================
Exercise 2: now that we have defined the odd numbers, you are asked to prove a simple relation between odd and even numbers. First, state and prove a Theorem succ-even that shows that the successor of an even number is an odd number. After that, state and prove a Theorem succ-odd that shows that the successor of an odd number is an even number.
Answer: ================================================================== succ-even : even N -> odd (s N) -> type. %mode succ-even +D1 -D2.
sez : succ-even even-z odd-1.
ses : succ-even (even-s EvenA) (odd-s OddA)
<- succ-even EvenA OddA.
%worlds () (succ-even _ _). %total D (succ-even D _).
succ-odd : odd N -> even (s N) -> type. %mode succ-odd +D1 -D2.
so1 : succ-odd odd-1 (even-s even-z).
sos : succ-odd (odd-s OddA) (even-s EvenA)
<- succ-odd OddA EvenA.
%worlds () (succ-odd _ _). %total D (succ-odd D _). Answer: ==================================================================
Exercise 3: now we would like to prove theorems that state the relation between sums of odd and even numbers, and between odd numbers.
(3a) First, state and prove the theorem sum-even-odd that shows that the sum of an even and an odd number results in an odd number:
Answer: ================================================================== sum-even-odd : even N1 -> odd N2 -> plus N1 N2 N3 -> odd N3 -> type. %mode sum-even-odd +D1 +D2 +D3 -D4.
seoz : sum-even-odd even-z OddN2 plus-z OddN2.
seos : sum-even-odd
(even-s EvenN1)
OddN2
(plus-s (plus-s PlusN1N2N3))
(odd-s OddN3)
<- sum-even-odd EvenN1 OddN2 PlusN1N2N3 OddN3.
%worlds () (sum-even-odd _ _ _ _). %total D (sum-even-odd D _ _ _). Answer: ==================================================================
(3b) State and prove a theorem sum-odd-even that shows that the sum of an odd plus an even number produces an odd number:
Answer: ================================================================== sum-odd-even : odd N1 -> even N2 -> plus N1 N2 N3 -> odd N3 -> type. %mode sum-odd-even +D1 +D2 +D3 -D4.
soe1 : sum-odd-even odd-1 EvenN2 _ OddN3 <- succ-even EvenN2 OddN3.
soes : sum-odd-even (odd-s OddN1) EvenN2 (plus-s (plus-s PlusN1N2N3)) (odd-s OddN3) <- sum-odd-even OddN1 EvenN2 PlusN1N2N3 OddN3.
%worlds () (sum-odd-even _ _ _ _). %total D (sum-odd-even D _ _ _). Answer: ==================================================================
(3c) Finally, state and prove a theorem sum-odds that shows that the sum of two odd numbers produces an even number:
Answer: ================================================================== sum-odds : odd N1 -> odd N2 -> plus N1 N2 N3 -> even N3 -> type. %mode sum-odds +D1 +D2 +D3 -D4.
soz : sum-odds odd-1 OddN2 _ EvenN3
<- succ-odd OddN2 EvenN3.
sos : sum-odds (odd-s OddN1) OddN2 (plus-s (plus-s PlusN1N2N3)) (even-s EvenN3)
<- sum-odds OddN1 OddN2 PlusN1N2N3 EvenN3.
%worlds () (sum-odds _ _ _ _). %total D (sum-odds D _ _ _). Answer: ==================================================================
%Undefine
Is there a way to do the 'opposite' of %abbrev in Twelf? Consider the following definition of 'and':
and : o -> o -> o = [A][B] forall [C] (A imp B imp C) imp C. and_i : pf A -> pf B -> pf (A and B) = ... and_e1 : pf (A and B) -> pf A = ... and_e2 : pf (A and B) -> pf B = ...
How could I prevent Twelf from expanding 'and' after this point? I'm working on an automated prover based on Felty's and Appel's ideas and unnecessary expansion causes the prover to terminate with unintelligible output, whenever it fails to prove something. (The prover outputs all unfinished goals.)
- Hey! Feel free to contact us by email, I can give you a bit of advice depending on what your precise goals are. I think in Twelf the way of doing this is probably %clause, but it turns out to be a bit messy to do things that way. I discuss two styles of Appel & Felty style proving in the article on tactical theorem proving. — Rob (and his talk) 09:56, 2 February 2009 (EST)
hypothetical judgments vs judgments with premises
I am having trouble understanding when hypothetical judgments can be used in place of judgments with premises. In the code segment below, the two queries at the bottom look logically equivalent, but Twelf only finds a solution for one of the queries. Any help is appreciated. Thanks, --128.119.240.174 11:04, 9 February 2009 (EST) John
% Define elements
elem : type.
i : elem.
j : elem.
% Define lists
list : type.
nil : list.
, : elem -> list -> list. %infix right 10 ,.
% neq = not equal relation judging when two elements are not equal
neq : elem -> elem -> type.
% notin A L = A is an element that is not in L
notin : elem -> list -> type.
notin/nil : notin A nil.
notin/skip : notin A (B, L)
<- neq A B
<- notin A L.
sample-list : list = j , j , nil.
% Solution found for this query:
%query 1 1 Y : notin i sample-list <- neq i j.
% Solution NOT found this query:
%query 1 1 Z : {x:neq i j} notin i sample-list.
proving things about an intensional property
I find it easy to prove a Twelf metatheorem that an extensional definiton satsifies certain intensional properties. For example, suppose I define some relation P |- Q using extensional rules (like a sequent calculus). Suppose now I have a semantics s |= P that means that P is true in situation s. Now I want to talk about an intensional property P |= Q, which says forall s such that s |= P, we have s |= Q. In Twelf, it is natural to write a meta theorem that says forall s such that s |= P and P |- Q, then s |= Q. In other words, we can express the idea that the extensional relation satisfies the intensional relation.
But now I want to prove some theorems such as P |= Q and Q |= R implies Q |= R. But I don't know how to express this idea in Twelf. This question must come up a lot. Can you point me to a tutorial on it?
Boyland 16:29, 27 February 2009 (EST)
- I'm not sure I know a way to express this without using a heavy structural-logical-relations-style formulation - it's outside of the forall-exists fragment if you expand the definitions. However, it seems that whenever such a property would be needed in a proof you could acquire it by calling the theorem you described twice - is that not the case? — Rob (and his talk) 22:36, 1 March 2009 (EST)
- Yes, if I needed transitivity, it can easily be proved at that point. But I'm going to try to prove a host of theorems like A * B |= B * A (which can be rephrased with |=) and P |= Q, A |= B implies P * A |= Q * B which cannot be easily rephrased. Can you point me to the cleanest tutorial on logical relations? Boyland 13:57, 2 March 2009 (EST)
- An interesting side-note. I tried phrasing |= in Twelf anyway using
implies : term -> term -> type.
implies/def : ({s} models s P -> models s Q) -> implies P Q.
This works great for proving transitivity, but is terrible at proving anything else, like A * B |= B * A. Boyland 13:57, 2 March 2009 (EST)
- It seems like you want a computational function, not an LF function; I'm working on a framework that would provide you with that: A Universe of Binding and Computation. Would "mixed datatypes" in the sense of the introduction of that paper be useful in your definition of "|="? Drl 19:33, 3 March 2009 (EST)
- Yes, that is what I need, but it seems not to be part of Twelf! Boyland 22:25, 7 July 2009 (EDT)
- A further update: I started working through the structural logical relations paper and got the impression I needed to design a simple sequent calculus with atomic rules specific to my application and then prove a cut elimination theorem (or cut admissibility theorem). I did this (and learned a bit more about cut elimination). But then when I went further, I think I bumped into a show stopper: the relation P |= Q includes universal quantification over heaps and thus with the normal Twelf way, hypothetical heaps. The problem is that I have a lot of theorems about heaps (e.g., associativity of heap addition) and as far as I can understand, none of them will work if there might be a hypothetical heap in the context.
- To be a little more concrete: suppose one has a nat type and a plus operation with an effectiveness lemma. Suppose one further has a simple assertion language expressed in a sequent calculus with an atomic rule (form/plus N1 N2 N3) defined as true precisely when (plus N1 N2 N3) is true. Now if I try to form the assertion:forall N exists N2:(form/plus N N N2) , then I cannot use my effectiveness lemma, right? The "solution" is to put every single theorem one needs about nats into the context whenever one has a hypothetical nat. Is this right? If so, this approach seems useless.
- I guess the problem is that Twelf doesn't "know" that this hypothetical value must be of one of the declared forms (z or s) if it is ever substituted. I wonder why Twelf doesn't have this ability. Would it make the logic unsound? Boyland 22:25, 7 July 2009 (EDT)
- I tried this out in Twelf and got the expected worlds violation:(this code requires my nat.elf "library" signature)
form : type.
form/plus : nat -> nat -> nat -> form.
form/forall : (nat -> form) -> form.
form/exists : (nat -> form) -> form.
hyp : form -> type.
conc : form -> type.
conc/plus : plus N1 N2 N3 -> conc (form/plus N1 N2 N3).
ax : hyp F -> conc F.
allr : ({n:nat} conc (F n)) -> conc (form/forall F).
alll : {n:nat} (hyp (F n) -> conc H) -> hyp (form/forall F) -> conc H.
somer : {n:nat} (conc (F n)) -> conc (form/exists F).
somel : ({n:nat} (hyp (F n) -> conc H)) -> hyp (form/exists F) -> conc H.
%theorem assert-exists-double :
forall {N}
exists {AE: (conc (form/exists ([n] (form/plus N N n))))}
true.
- : assert-exists-double N (somer N2 (conc/plus P))
<- plus-total P.
%worlds () (assert-exists-double _ _).
%total { } (assert-exists-double _ _). % Just fine.
%theorem assert-exists-double2 :
exists {AE: (conc (form/forall ([n] (form/exists ([n2] (form/plus n n n2))))))}
true.
- : assert-exists-double2
(allr ([n:nat] (somer (N2 n) (conc/plus (P n)))))
<- ({n:nat} plus-total* n n (N2 n) (P n)).
%worlds () (assert-exists-double2 _). % NB: world violation!
%total { } (assert-exists-double2 _).
- It makes sense that this is rejected in Twelf, because the "function" (N2 n) has no ability to be expressed in LF. But this does mean that the limitation of Twelf's metatheorems is a live issue: not put to rest by the "Structural Logical Relations" paper.
- After some discussion with Karl Crary, it seems that the best solution is to define an empty relation, define some trustme "metatheorems" that express the desired properties and then prove all theorems in a context (worlds) with a variable of the empty relation. This ensures that Twelf will not split on the empty relation. Boyland 15:26, 20 February 2010 (EST)
Negative premises
I'm attempting to express the operational semantics of concurrent calculi like CCS in Twelf, but the inference rules for these calculi often require negative premises. I was wondering if such a thing is possible in Twelf.
Below is my specification for (part of) a CCS-like language without the rule for hiding actions. Here, 'trans P1 A P2' represents a transition from P1 to P2 labelled with A.
label : type.
proc : type.
a : label.
b : label.
c : label.
d : label.
0 : proc.
, : label -> proc -> proc.
+ : proc -> proc -> proc.
| : proc -> proc -> proc.
%infix right 12 ,.
%infix left 10 +.
%infix left 9 |.
trans : proc -> label -> proc -> type.
pref-rule : {A:label} {P:proc} trans (A , P) A P.
suml-rule : {A:label} {P1:proc} {Q:proc} {P2:proc} trans P1 A P2 -> trans (P1 + Q) A P2.
sumr-rule : {A:label} {P1:proc} {Q:proc} {P2:proc} trans P1 A P2 -> trans (Q + P1) A P2.
parl-rule : {A:label} {P1:proc} {Q:proc} {P2:proc} trans P1 A P2 -> trans (P1 | Q) A (P2 | Q).
parr-rule : {A:label} {P1:proc} {Q:proc} {P2:proc} trans P1 A P2 -> trans (Q | P1) A (Q | P2).
In order to encode the rule for hiding, I would need something like this:
\ : proc -> label -> proc. %infix left 11.
hide-rule: {A:label} {P1:proc} {P2:proc} trans P1 A P2 -> A != B -> trans (P1 \ B) A (P2 \ B)
where A != B is meant to be inequality of labels. Is there a simple way of encoding such negative premise?
- Unfortunately, no: you'll have to define the != judgement inductively yourself, by giving a case for each pair of non-equal labels (and then you may need to prove that A != A is a contradiction). But we're working on a framework where you could express this directly, so thanks for the example! Drl 14:28, 4 May 2009 (EDT)
Coverage checking
I am having trouble understanding the behavior of the coverage checker on this example, a snippet of a dependently-typed functional language encoding:
tp : type.
vl : tp -> type. % values tm : tp -> type. % terms obs : tp -> tp -> type. % "observations"
! : vl A -> tm A.
%prefix 90 !.
cut: obs A B -> vl A -> tm B.
%% body is a functional relation, defining each value %% as a "map from observations to terms". body : vl A -> obs A X -> tm X -> type. %mode body +V +C -E.
%% We introduce one kind of type, pi (and non-depenendent =>)... pi : {a:tp} (vl a -> tp) -> tp. => : tp -> tp -> tp = [A] [B] pi A [_]B.
%infix right 120 =>.
%% With one kind of observation on pi... @ : {x:vl A}obs (B* x) C -> obs (pi A B*) C.
%infix right 120 @.
%% Now we define function abstraction... fn : ({x:vl A}vl (B* x)) -> vl (pi A B*). fn/_ : body (fn E*) (V @ K) E' <- body (E* V) K E'.
%% At this point, we could verify that body covers and is unique, %% by uncommenting the following lines... % %worlds () (body V C _). % %covers body +V +C -E. % %unique body +V +C -E.
%% Now we define *non-dependent* function application... app-nd : vl (A => B) -> vl A -> vl B. app-nd/_ : body (app-nd F V) C E' <- body F (V @ C) E'.
%% Again, we could verify that body covers and is unique... % %worlds () (body V C _). % %covers body +V +C -E. % %unique body +V +C -E.
%% However, now consider *dependent* function application, %% with essentially the same body clause... app : vl (pi A ([x]B* x)) -> {x:vl A} vl (B* x). app/_ : body (app F V) C E' <- body F (V @ C) E'.
%% Suddenly, the coverage check fails... % %worlds () (body V C _). % %covers body +V +C -E. % %unique body +V +C -E. Any ideas? Thanks, Noam 07:43, 19 September 2009 (EDT)
- Okay now I see that the problem is Inactive Splits. I don't quite understand what the suggested workaround is (is there an example somewhere?), but I figured out something, which may or may not amount to the same thing...
- Begin by defining a tp to internalize the LF application:
tapp : (vl A -> tp) -> vl A -> tp.
t@ : obs (B* V) X -> obs (tapp B* V) X.
- Then assign app a type in terms of tapp, and give a slightly tweaked body clause:
app : vl (pi A ([x]B* x)) -> {x:vl A} vl (tapp B* x).
app/_ : body (app F V) (t@ C) E'
<- body F (V @ C) E'.
- Now this coverage checks! Noam 00:58, 20 September 2009 (EDT)
Twelf User Manual
Is the user manual for Twelf version 1.5 available? I only noticed that for version 1.4 on Twelf Web site.
freezing violation: X would depend on Y
Occasionally the Twelf type checker will generate variables of type such as term -> nat and then complain that nat would depend on term in that case. I find this error message frustrating since (1) I didn't create this variable -- it was generated from an implicit underscore, (2) Since nat does NOT depend on term (e.g.), then why does Twelf generate the dependency, and (3) Just because we have a value of type term -> nat, it doesn't mean that nat depends on term, but rather that the function must ignore its argument.
Another frustrating thing is that it interferes with incremental proof development: I often supply cases to theorem after earlier (unsuccessfully) checking totality. In this case I get the error message "Freezing violation: constant - extends type family X" which I ignore and then check totality again. When totality succeeds, I conclude that the theorem is done, but if I read the theorem in over again, it gets this "nat would depend on term" error message.
BTW: I'm using latest CVS Twelf (1.5R3) which apparently has been frozen for a few years. Is this a bug that has since been fixed?
If it would be helpful, I can try to generate a small example which causes this behavior.Boyland 15:37, 20 February 2010 (EST)
- Here is a relatively small example that indicates the problem:
%%%% Definitions
%% Define natural numbers
nat : type.
z : nat.
s : nat -> nat.
%% Define terms
term : nat -> type.
%abbrev t = term z.
lit : nat -> t.
%% equality on terms
eq : term N1 -> term N2 -> type.
eq/ : eq T T.
%%% Variable levels and nolevel
var : term N -> type.
%block blockvar : some {n} block {t:term n} {v:var t}.
% without this, we get a freezing violation: var would depend on var
fake : type.
- : (var X -> var X') -> fake.
%%% Variable lists
varlist : type.
varlist/0 : varlist.
varlist/+ : {N} {V:term N} var V -> varlist -> varlist.
%%% Operations on variable lists:
count : varlist -> nat -> nat -> type.
lookup : varlist -> term N -> varlist -> type.
count/0 : count varlist/0 N z.
count/= : count VL N M ->
count (varlist/+ N V _ VL) N (s M).
lookup/= : lookup (varlist/+ _ V _ VL) V VL.
lookup/!= :
lookup VL V VL' ->
lookup (varlist/+ _ _ _ VL) V VL'.
%%% Theorems about operations on varlists.
%theorem count-independent:
forall* {N} {N'} {M} {VL}
forall {FC: {v:term N} (var v) -> count VL N' M}
exists {C: count VL N' M}
true.
- : count-independent ([v] [i] count/0) count/0.
- : count-independent ([v] [i] count/= (FC v i)) (count/= C)
<- count-independent FC C.
%worlds (blockvar) (count-independent _ _).
%total (C) (count-independent C _).
%theorem lookup-count-independent:
forall* {N} {N'} {FVL} {FFVL'} {M}
forall {FFL: {v': term N'} {i': var v'} {v: term N} {i: var v}
lookup (FVL v i) v (FFVL' v' i' v i)}
{FFC: {v': term N'} {i': var v'} {v: term N} {i: var v}
count (FFVL' v' i' v i) N M}
exists {FVL': {v: term N} {i:var v} varlist}
{FL: {v: term N} {i:var v} lookup (FVL v i) v (FVL' v i)}
{FC: {v: term N} {i:var v} count (FVL' v i) N M}
true.
- : lookup-count-independent ([v'] [i'] [v] [i] lookup/=) FFC _ ([v] [i] lookup/=) FC
<- ({v} {i} count-independent ([v'] [i'] FFC v' i' v i) (FC v i)).
- : lookup-count-independent ([v':term N'] [i':var v'] [v:term N] [i:var v] lookup/!= (FFL v' i' v i)) FFC ([v] [i] FVL v i)
([v:term N] [i:var v] lookup/!= (FL v i)) FC
<- lookup-count-independent FFL FFC _ FL FC.
%worlds (blockvar) (lookup-count-independent _ _ _ _ _).
%total (L) (lookup-count-independent L _ _ _ _).
- This code checks fine with the online version of Twelf. It must be a problem with Twelf-CVS.
- Update: The code still fails with the latest truck from SVN. So it seems the online twelf checker has a different version than twelf-CVS/SVN. older? Boyland 18:17, 22 February 2010 (EST)
Termination and %mode
Hi Twelf Elf: I've just started getting into twelf and have been working my way through Frank Pfenning's Computation and Deduction notes (http://www.cs.cmu.edu/~fp/courses/comp-ded/handouts/cd.pdf). I got so far as trying to get twelf to confirm that doubling 2 yields 4, but it gets stuck. (I'm also using the latest release of twelf, not the nightly build version.)
Below is my complete program; when I run it in twelf, it does not seem to terminate.
Any advice?
Thanks, Robby
exp : type.
z : exp.
s : exp -> exp.
case : exp -> exp -> (exp -> exp) -> exp.
lam : (exp -> exp) -> exp.
app : exp -> exp -> exp.
fix : (exp -> exp) -> exp.
eval : exp -> exp -> type.
ev_z : eval z z.
ev_s : eval E V -> eval (s E) (s V).
ev_case_z : eval E1 z -> eval E2 V -> eval (case E1 E2 ([y:exp] E3 y)) V.
ev_case_s : eval E1 (s V1)
-> eval (E3 V1) V
-> eval (case E1 E2 E3) V.
ev_lam : eval (lam F) (lam F).
ev_app : eval E1 (lam F) -> eval E2 V2 -> eval (F V2) V -> eval (app E1 E2) V.
ev_fix : eval (E1 (fix E1)) V -> eval (fix E1) V.
double : exp = fix ([double : exp]
(lam [i : exp]
(case i
z
([iminusone : exp] (s (s (app double iminusone))))))).
%query 1 1 D : eval (app double (s z)) (s (s z)).
Hi Robby! Glad you're using Twelf. I'd definitely encourage you to use the "nightly build" - it's currently very stable and has lots of improvements (and fewer bugs) than the last release. Also, it's a good idea to sign your comment with four tildes ~~~~
Anyway - I had a hunch, that turned out to be right, that the right thing to do was to write a %mode declaration %mode eval +E -V., which basically means "it makes sense to run eval as a function with input E and output V. Sure enough, it complains about both the rule ev_case_s and ev_app. If I reorder the premises so it no longer complains, the two rules look like this:
ev_case_s : eval (E3 V1) V
-> eval E1 (s V1)
-> eval (case E1 E2 E3) V.
ev_app : eval (F V2) V
-> eval E2 V2
-> eval E1 (lam F)
-> eval (app E1 E2) V.
In general, it's better to use backwards arrows when you intend to be running something as a logic program; the above program "looks better" written as this equivalent program:
ev_case_s : eval (case E1 E2 E3) V
<- eval E1 (s V1)
<- eval (E3 V1) V.
ev_lam : eval (lam F) (lam F).
ev_app : eval (app E1 E2) V
<- eval E1 (lam F)
<- eval E2 V2
<- eval (F V2) V.Good luck learning Twelf, let us know if we can help you in the future! — Rob (and his talk) 16:04, 1 November 2010 (EDT)
Also, you can use this to run programs even if you don't know the answer:
%query 1 1 eval (app double (app double (app double (s (s (s z)))))) V.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)See the corrected Twelf code along with this query — Rob (and his talk) 16:14, 1 November 2010 (EDT)%query 1 1 eval (app double (app double (app double (s (s (s z)))))) V. ---------- Solution 1 ---------- V = s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s (s z))))))))))))))))))))))). ____________________________________________
%% OK %%
Thanks! I had read about %mode, and had even tried it with the definition of eval I posted above (getting the errors you allude to), but what I read about modes didn't suggest that ordering of the premises had any influence on the mode declaration. (Of course, I've now tried out your revision and sure enough I see that it does.). Is there more I should read about that? (So far I've just read 4.5 in _Computation and Deduction_.)
And yes, I do know how to run things without knowing the answer; of course it also didn't work for the example given. I put in the precise answer in a futile hope that that would help twelf terminate. Thanks also for the wiki advice. I'm amazed that it's taken me this long to post on one.... one question about wiki's tho: I had to come back here to see you'd posted. Is there a way to get email notification? (I had already clicked the "watch this page" checkbox.)
Robby 11:28, 2 November 2010 (EDT)
I think this wiki has email turned off, actually. To understand the effect of %mode you might find it helpful to read some general stuff about logic programming, which is where a lot of the intuition behind proving metatheorems comes from. — Rob (and his talk) 12:11, 4 November 2010 (EDT)
POPL tutorial slides location?
The slides linked to from POPL Tutorial are 404. I tried to use Google to find the slides, but it was no help. Jbapple 15:09, 15 January 2011 (EST)
Twelf 1.7.1 ?
It seems Twelf 1.7.1 is released, but the documentation still seems to be at 1.4 (with some wiki pages for 1.5 additions.)
(1) Is there any summary of changes since 1.4/1.5 ?
(2) Any plans to update the 1.4 documentation?
- I don't know of any plans to do so (I think the wiki is now, for better or worse, the primary documentation). We should probably go through the wiki and turn some of the tags indicating "this is a SVN-only feature" to tags indicating "this is a Twelf 1.7 feature," though. There is a revision history on the wiki. — Rob (and his talk) 21:33, 24 August 2011 (EDT)
Problem to find an induction metric
I would like to prove that if two numbers are the same, e.g., N0 = N1, then, if I set the K-th position of a list to N0, or to N1, I get the same resulting list. The proof is not obvious to me because I cannot, in this case, do induction on the derivation rules of lists. I have these signatures for numbers:
nat : type.
z : nat.
s : nat -> nat.
% eq N1 N2 is true if N1 and N2 represent the same number.
eq : nat -> nat -> type.
%mode eq +N1 +N2.
eq_z : eq z z.
eq_s : eq (s N1) (s N2)
<- eq N1 N2.
%worlds () (eq N1 N2).
%terminates {N1 N2} (eq N1 N2).
And these signatures for the list:
list : type.
element : type.
nil : list.
con : element -> list -> list.
value : nat -> element.
% set L E N L' == L' is the same list as L, except that its N-th cell has
% been set to E.
set : list -> element -> nat -> list -> type.
%mode set +L +E +N -L'.
set_z : set (con E' EL) E z (con E EL).
set_s : set (con E' L) E (s N) (con E' L')
<- set L E N L'.
And below is the theorem that I would like to prove:
eq_set : eq N N' -> set L (value N') V L' -> set L (value N) V L' -> type. %mode eq_set +Eq +Set' -Set. eq_set_z : eq_set eq_z Set Set. % eq_set_s ??? %worlds () (eq_set _ _ _). %total Eq (eq_set Eq _ _).
- I think you need to determine an equality judgment on L', and prove
eq_set : eq N N' -> set L (value N') V L' -> set L (value N) V L' -> eq-list L L' -> type.
%mode eq_set +Eq +Set' +Set -Eq'.
trouble with twelf server
Hi,
Im doing my final year project on LF and imperative languages and Ive decided to use Twelf to mechanize the theory, however, I'm finding it difficult to start the server on Linux, while on OsX had no problem. Please help. I've dwnloaded the pre-installed Linux version on Ubuntu and straight away I call bin/twelf-server, however this error comes up:
@ubuntu:~/twelf$ bin/twelf-server bin/twelf-server: error while loading shared libraries: libgmp.so.3: cannot open shared object file: No such file or directory
What am I missing? For what ive understood I do not need to use Make as is pre-installed, right? So I should be a ble to run it from scratch....
Looking forward to hear from you, J. Dominguez
How to prove totality in this case?
I am formalizing a programming language. One of the things I need is a conditional statement and prove its totality (this is needed for dynamic semantics, that has to search through an associative list, and the keys have decidable equality). I can do a simple one, like this:
bool : type.
true : bool.
false : bool.
% my language has expressions and computations
expr : type.
comp : type.
% lambda abstraction and injection of expressions into computations create a headache later on
fun : (expr -> comp) -> expr.
val : comp -> expr.
cond-expr : bool -> expr -> expr -> expr -> type.
%mode cond-expr +B +E +E' -E''.
- : cond-expr true E _ E.
- : cond-expr false _ E' E'.
%worlds () (cond-expr _ _ _ _).
%total {B E E'} (cond-expr B E E' _).
So far so good. But I actually need a slightly more complicated conditional:
%abbrev cow = (expr -> (expr -> comp) -> comp). cond-cow : bool -> cow -> cow -> cow -> type. %mode cond-cow +B +Moo +Moo' -Moo''. - : cond-cow true Moo _ Moo. - : cond-cow false _ Moo' Moo'.
Now suppose we want to check totality of cond-cow:
%worlds () (cond-cow _ _ _ _).
%total {B Moo Moo'} (cond-cow B Moo Moo' _).
Then we get this error message:
While checking constant %-%: Family expr has no worlds declaration %% ABORT %%
So one would like to add %worlds for expr and comp. But if I try something like
%worlds () (expr). %worlds () (comp).
I get "comp would depend on expr". And I think that val and fun can be a further source of trouble.
I am stumped. Why is it even analyzing cow? What is Twelf thinking and how to I fix it?
Thanks! Andrej Bauer (please notify me by email about the answer at Andrej.Bauer@andrej.com)
- I think you need to declare the worlds of both expr and comp together as in
%worlds () (expr) (comp).
- Boyland 15:28, 5 June 2013 (EDT)
%reduces not as smart as what is done in %total, it seems
I don't see a way to prove %reduces through a lambda abstraction, although, it appears that %total checking is able to reason about these. For example:
%% HOAS for LC
t : type.
lam : (t -> t) -> t.
app : t -> t -> t.
m : t -> t -> type.
m/0 : m T T.
m/app1 : m T1 T2 -> m (app T1 _) T2.
m/app2 : m T1 T2 -> m (app _ T1) T2.
m/lam : ({x} m (F x) T) -> m (lam ([x] F x)) T.
%reduces T2 <= T1 (m T1 T2).
This gives error
Reduction violation: Pi (T) <= (F x) ---> (T) <= (lam ([x:t] F x))
Is there a workaround to this problem? Boyland 05:07, 3 October 2013 (EDT)
- What's an example where this works for %total?
Here's one that checks just fine: Boyland 08:51, 11 October 2013 (EDT)
nat : type.
z : nat.
s : nat -> nat.
max : nat -> nat -> nat -> type.
%mode max +N1 +N2 -N3.
max/zz : max z z z.
max/sz : max (s N) z (s N).
max/zs : max z (s N) (s N).
max/ss : max N1 N2 N3 -> max (s N1) (s N2) (s N3).
%worlds () (max _ _ _).
%total (N) (max N _ _).
height : t -> nat -> type.
%mode height +T -N.
%block hb : block {x} {h:height x z}.
height/lam : ({x} (height x z) -> height (F x) N) -> height (lam F) (s N).
height/app : height (app T1 T2) (s N3)
<- height T1 N1
<- height T2 N2
<- max N1 N2 N3.
%worlds (hb) (height _ _).
%total (T) (height T _).
dictionary in which keys are variable names
Dear Elfs,
We are using Twelf for implementing a language semantics. We have typing judgement of the form:
Γ |- e : τ : Ω
- Γ is the context - e is the expression - τ is the type - Ω is a set of relations between variables in e and a label
For this typing judgement, we would like to have the following mode:
%mode of +E -T -L.
For instance:
x : int, y: int |- x + y + 1 : int : {x:low, y: high}
In our typing semantics, we have some rules that modifies Ω and others that retrieve a label given a specific variable name.
To implement this, we have 2 options: - implement a complex way to deal with variables which means redefining substitution and so on (very tedious) - use twelf variables in our expression to write expressions such as "λx:int.x" as "lambda int ([x] x)" but we need an elfy magic trick to implement Ω
Do you have examples or ideas about how to implement some sort of dictionary in which keys are actual variable names?
I hope all of this was clear.
Thank you.
Thierry
- Either way should be possible.
- If you implement explicit (non-LF) variables, then as you say, you need to define substitution etc yourself, which is a pain. But you can use the set/map types in my Twelf library.
- Otherwise, trying to implement a true ("adequate") map from variables to sets of labels is very tricky. It can be done but will pollute your context with tons of extra things. See HOAS nat bijection.
- The big problem is "inequality". It's very difficult to determine if two variables are equal or not in Twelf.
- Boyland 11:02, 13 January 2014 (EST)
Twelf bug reports?
Is Twelf still being maintained? I have a (BIG) example where type reconstruction doesn't terminate in Twelf 1.7.1+ (r1887M). Is anyone interested in bug reports?
Syntax highlighting for IntelliJ IDEA
Good evening Twelf Elf,
I have created an IntelliJ plugin for Twelf which can be downloaded from the IntelliJ plugin repository: http://plugins.jetbrains.com/plugin/7533
The source code is also available on Github: https://github.com/alahijani/Jelf
You can download IntelliJ IDEA community edition from: http://www.jetbrains.com/idea/download/
Sorry, I could not find a publicly editable notice board. Is there a place where I can post instructions?
Ali 02:23, 19 August 2014 (EDT)
Problems with pages
See for example Lax logic where errors reported with: "Failed to parse (PNG conversion failed; check for correct installation of latex, dvips, gs, and convert)" occur very frequently.
Fairflow 04:11, 9 December 2014 (EST)
I don't see the problem. Perhaps (1) it has been rsolved, or (2) it may be browser related? Boyland (talk) 21:00, 21 October 2016 (UTC)
Can’t solve obvious goal or is it me?
I’m new to Twelf (have to see it matches what I’m planning to do).
Testing the very simple sample below:
nat : type. z : nat. s : nat -> nat. sum : nat -> nat -> nat -> type. sum/z : sum z N N. sum/s : sum M (s N) (s S) <- sum M N S.
Then querying this:
%query 1 * sum (s z) (s z) X.
It fails. While if `sum/s` is changed from `sum/s : sum M (s N) (s S) <- sum M N S.` to `sum/s : sum (s M) N (s S) <- sum M N S.` it works.
Unless I’m wrong, the goal should be as much solvable is both case. Is this me missing something?
Twelf pre-built Mac OS distro needs update
Dear Twelf Elves,
Mac OS X Catalina deprecated running 32-bit apps, and the pre-built Mac OSX distro of Twelf does not work anymore. (Building from source with SMLNJ still works.)
Could this be updated?
Thanks.
