User:Boyland
From The Twelf Project
John Boyland, Associate Professor, University of Wisconsin--Milwaukee.
I'm interested in using Twelf and have written a biased and under-informed tutorial of Twelf. I also have defined some library signatures for Twelf.
I have signed up for the Coq tutorial at POPL 2008. I hope to be able to get a better feel of how the systems compare. Update: It's great to have polymorphism and real libraries, and it's also wonderful to be able to use excluded middle. (Negation is a big pain in Twelf). But proofs are just flat sequences of tactics. And HOAS isn't possible. Disappointing.
Contents |
[edit] Desired Features
Here are some features that I would like to see in Twelf. I start with the simplest to implement (in my opinion).
[edit] What free variables?
In Twelf, if you neglect to declare all the free variables in a theorem, you get the error message "Free variables In theorem." It would be nice if the error message included the names of these free variables. Update: of course Control-C Control-L will tell you all the free variables that have names.
[edit] An exists* keyword
In Twelf currently, a theorem has the form
my-theorem : forall* {K1} {K2} {V1:term K1} {V2: term K2} forall {D:rule V1 V2} exists {K3} {V3:term K3} {DP:rule2 V1 V2 V3} true.
Sometimes the existentially bound variables are as extraneous as the forall* bound variables. One would like to write
my-theorem : forall* {K1} {K2} {V1:term K1} {V2: term K2} forall {D:rule V1 V2} exists* {K3} exists {V3:term K3} {DP:rule2 V1 V2 V3} true.
Currently my workaround is to avoid the theorem syntax and use an explicit mode declaration:
my-theorem : (rule V1 V2) -> ({V3} (rule2 V1 V2 V3)) -> type. %mode +{K1} +{K2} +{V1:term K1} +{V2: term K2} +{D:rule V1 V2} -{K3} -{V3:term K3} -{DP:rule2 V1 V2 V3} (my-theorem D DP).
An exists* keyword should be a trivial addition.
[edit] Output coverage checking
It would be desirable to have output coverage checking done at the same time as mode checking, or at least to have the ability to check output coverage before a total declaration. I have often found it frustrating to get an output coverage error late in the process of writing a proof. And the "covers" check doesn't include output coverage
[edit] Totality checker and theorem prover integration
Currently the theorem prover and totality checker live in different worlds, and neither trusts the other. This seems peculiar to a user of Twelf who may wish to use the theorem prover for certain obvious lemmas but the totality checker for more complex theorems. Currently this is impossible except in unsafe mode with the addition of assertions and "trustme" declarations.
I propose
1. The theorem prover should accept proved theorems: If a totality flag is set on a metatheorem, it should accept it as proved.
2. The totality checker should accept metatheorems proved automatically. If necessary, the theorem prover should deliver the proof to the totality checker internally (invisibly) for re-checking.
3. The %assert and %trustme declarations should have the same effect: in unsafe mode make the metatheorem trusted by both the totality checker and the theorem prover.
[edit] Local Type Inference
After using Twelf for about a year and writing 100K lines of Twelf, the most frustrating and time consuming process is "debugging" coverage errors. Because unification is bidirectional, any mistake in the middle of a theorem will cause the pattern taht one is trying to match to not be exhaustive, even though it appears to be. It would be nice to use a system with a slightly less powerful type inference system that would prevent this long-distance effect of unification. Pierce and Turner have defined "Local Type Inference". It is interesting to wonder what this would mean for Twelf.
[edit] Known Bugs
[edit] Coverage Checker Nontermination
The coverage checker sometimes fails to terminate.
%%%% coverage checking doesn't always terminate %%%% Definitions void : type. expr : type. unit : expr. add : expr -> expr -> expr. %%% Nested for evaluation expr-in-expr : (expr -> expr) -> type. expr-in-expr/add1 : expr-in-expr ([E] (add E _)). expr-in-expr/add2 : expr-in-expr ([E] (add unit E)). %%% ready for atomic evaluation atomic-expr : expr -> type. atomic-expr/add : atomic-expr (add unit unit). %% this "theorem" is actually false %theorem expr-in-atomic-expr-contradiction : forall* {E} {T} forall {AE:atomic-expr (T E)} {Tok:expr-in-expr T} exists {F:void} true. %worlds () (expr-in-atomic-expr-contradiction _ _ _). %total { } (expr-in-atomic-expr-contradiction _ _ _).
[edit] Theorem Prover Nontermination
The prover sometimes fails to terminate. See example in my tutorial (Section 2.3) I have copied it here for completeness:
%%% Example of Twelf from "using-twelf" paper term : type. true : term. false : term. if : term -> term -> term -> term. zero : term. ty : type. bool : ty. int : ty. %% relations is_value : term -> type. is_value/true : is_value true. is_value/false : is_value false. is_value/zero : is_value zero. eval : term -> term -> type. eval/if_true : eval (if true X _) X. eval/if_false : eval (if false _ X) X. eval/if : eval (if E E1 E2) (if E' E1 E2) <- eval E E'. not_stuck : term -> type. not_stuck/value : not_stuck X <- is_value X. not_stuck/eval : not_stuck X <- eval X X'. of : term -> ty -> type. of/true : of true bool. of/false : of false bool. of/zero : of zero int. of/if : of X bool -> of Y T -> of Z T -> of (if X Y Z) T. %% theorems progress : (of X T) -> (not_stuck X) -> type. %mode progress +D1 -D2. %prove 2 T (progress T _).
[edit] Challenges
[edit] Is HOAS countable?
A challenge: define a mapping from HOAS to the natural numbers (or equivalently to a nameless term representation) and then prove that the mapping is isomorphic using Twelf. For details and sample mappings, see question on the Twelf Elf page: Talk:Ask_Twelf_Elf#Mapping_HOAS_isomorphically_to_the_natural_numbers.
Update: Rob has posted a solution (Concrete_representation) that defines a mapping between HOAS and nameless terms and proves that it is bijective. (I asked for an "isomorphic" mapping between HOAS and natural numbers, but should have said "bijective mapping.") Thanks Rob!
My personal challenge is to write a general technique for generating bijective mappings (with proof) between many kinds of terms and natural numbers. In general, of course, this would be undecidable. I hope only to handle cases that are used as AST types.
Update: I did it for a simple HOAS before POPL 2008 (see HOAS nat bijection), and in May 2008, finished a more complex example Indexed HOAS nat bijection that handle an indexed term language.
