%{
== Arithmetic primitives ==
}%
nat : type.
z : nat.
s : nat -> nat.
add : nat -> nat -> nat -> type.
%mode add +M +N -P.
add/z : add z N N.
add/s : add (s M) N (s P) <- add M N P.
%worlds () (add _ _ _).
%total M (add M _ _).
%{
== Multiplication ==
(Interactively) First, let's write multiplication:
Answer:
}%
mult : nat -> nat -> nat -> type.
mult/z : mult z N z.
mult/s : mult (s M) N Q
<- mult M N P
<- add P N Q.
%{
Now let's check that multiplication is total.
First, we specify the mode: which arguments are inputs, and which
arguments are outputs?
Answer:
}%
%mode mult +M +N -P.
%{
+ means input (univeral); - means output (existential).
Next the world:
}%
%worlds () (mult _ _ _).
%{
This means we consider terms of type mult in the empty LF context only.
Finally, we ask Twelf to check that it is total by induction over the
first argument:
}%
%total M (mult M _ _).
%{
What does this really mean? "For any two LF terms M and N in the empty
context, there exists a term P and a deriation of mult M N P in
the empty context."
==How Twelf checks assertions==
Twelf proves a totality assertion for a type family such as
mult by checking several properties. These properties, taken
together, constitute a proof by induction on canonical forms that the
type family defines a total relation.
===Mode===
Twelf checks that each constant inhabiting the type family is
''well-moded''. Roughly, this means that the inputs to the conclusion
of a constant determine the inputs of the first premise, and that these
together with the outputs of the first premise determine the inputs of
the second premise, and so on, until the outputs of all the premises
determine the outputs of the conclusion.
%% so we don't get freezing errors
nat : type.
z : nat.
s : nat -> nat.
add : nat -> nat -> nat -> type.
%mode add +M +N -P.
add/z : add z N N.
add/s : add (s M) N (s P) <- add M N P.
%worlds () (add _ _ _).
%total M (add M _ _).
mult : nat -> nat -> nat -> type.
%mode mult +M +N -P.
mult/z : mult z N z.
mult/s : mult (s M) N Q
<- mult M N P
<- add P N Q.
For example, the constant
mult/s : mult (s M) N Q
<- mult M N P
<- add P N Q.
has mode +M +N -P because the input M and N
in the conclusion determine the inputs of the premise, and the
P output by the premise determines the first input to the second
premise (add), and the output of that determines the conclusion.
On the other hand, a constant
mult-bad-mode : mult M N P.
is not well-moded---the output P is not determined by the
inputs. Similarly,
mult-badmode2 : mult N1 N2 N3
<- mult N4 N2 N3.
is not well-moded---first input to the premise is not determined
by the inputs of the conclusion.
Subgoal order matters:
mult/s : mult (s M) N Q
<- add P N Q
<- mult M N P.
===Worlds===
Twelf checks that each constant inhabiting the type family obeys the
worlds declaration. Because we are only proving theorems about closed
terms right now, we will not run across any problems with world
checks.
===Termination===
Twelf checks that each constant inhabiting the type family obeys the
induction order specified in the %total declaration. In each
inductive premise of a constant, the specified induction position must
be a strict subterm of the corresponding argument in the conclusion.
For example, the constant
mult/s : mult (s M) N Q
<- mult M N P
<- add P N Q.
obeys the induction order M specified in the above totality
assertion because the term M is a strict subterm of the term
(s M).
On the other hand, Twelf would not accept the totality of mult
if N were used as the induction order—the same term
N in the conclusion of this constant appears in the premise:
%total N (mult _ N _).
In addition to the subterm ordering on a single argument, Twelf supports
[[mutual induction]] and [[lexicographic induction]].
===Output coverage===
In the definition of a type family, you may pattern-match the outputs of
a premise. For example, we might write
mult-bad-output : mult (s N1) N2 (s (s N3))
<- mult N1 N2 (s N3).
%worlds () (mult _ _ _).
%total N1 (mult N1 N2 N3).
Here we have insisted that the output of the premise has the form s
N3 for some N3. Twelf correctly reports an output
coverage error because this condition can fail..
Pattern-matching the output of a premise is like an [[inversion]] step
in a proof: you're insisting that the premise derivation must conclude a
particular fact that is more specific than the judgement form itself.
For Twelf to accept a relation as total, Twelf must notice that all of
these inversions are permissible. Twelf permits such inversions when it
is readily apparent that they are justified, and those inversions that
Twelf does not accept can be proved explicitly.
In this example, we got an output coverage error because we constrained
the output of the premise by insisting it be formed by a particular
constant. The other way to get output coverage errors is to insist that
the output of a premise be a variable that occurs elsewhere in the type.
For example:
mult-bad-output-freeness : mult (s N1) N2 (s N2)
<- mult N1 N2 N2.
%worlds () (mult _ _ _).
%total N1 (mult N1 N2 N3).
Here, we insisted that the output of the premise be the number
N2 that we put in. Twelf is very conservative in checking
[[output freeness]]: a type family will not be judged total if you
constrain the outputs of any premise at all in this manner.
===Input coverage===
Mode, worlds, termination, and output coverage ensure that each constant
really does cover the part of the relation indicated by its conclusion.
For example, if mult passes these four checks, we know that
mult/z and mult/s cover (z, N, _) and (s N1,
N2, _), respectively. What else is necessary to know that
mult defines a total relation? We need to know that all the
constants inhabiting mult, taken together, cover all of the
inputs. Input coverage checks exactly this.
For example, if we forgot mult/z, input coverage for
mult would fail. For example:
mult' : nat -> nat -> nat -> type.
%mode mult' +N1 +N2 -X3.
mult'/s : mult' (s M) N Q
<- mult' M N P
<- add P N Q.
%worlds () (mult' _ _ _).
%total M (mult' M _ _).
Here's an analogy that might be helpful: You can think of each constant
of a type as being a clause in an ML pattern matching declaration. Then
input coverage is like the exhaustiveness checker for pattern matching.
Twelf checks input coverage by [[splitting]] the input types to
case-analyze the various constants that could have been used to inhabit
them. For plus, Twelf splits the first nat argument
N1, and then checks that the cases plus z N2 N2 and
plus (s N1) N2 N3 are covered. Fortunately, these are exactly
the cases we wrote down. If we had case-analyzed further in the
definition of the judgement (e.g., if the definition of plus
case-analyzed the second argument as well), Twelf would continue
splitting the input space. Because Twelf separates termination checking
and coverage checking, the constants defining a type family do not need
to follow any particular primitive recursion schema-the constants may
pattern-match the inputs in a general manner.
==When Twelf checks what==
To a first approximation, you can think of the %mode and %worlds declarations as specifying a totality assertion and the %total declaration as checking it. This isn't exactly how Twelf works, though:
# When a %mode declaration is entered, Twelf checks that all previous constants inhabiting the specified type family are well-moded; further, it then mode-checks any subsequent constants inhabiting that family.
# When a %worlds declaration is entered, Twelf world-checks the type family; further, it then reports an error if any new constants contributing to the family at all are added.
# When a %total declaration is entered, Twelf checks termination, then input coverage, then output coverage. When checking output coverage, Twelf checks for unjustified constant pattern-matching in a first pass and then output freeness problems in a second pass.
This separation allows you to, for example, check that each constant in a family is well-moded (i.e., takes specified inputs to specified outputs) without checking that the entire type family is total. You can also use the declarations [[%terminates]] and [[%covers]] to check termination and input coverage independently.
If any constant in a type family fails mode, worlds, or output coverage, then mode, worlds, or totality checking fails for the whole type family. One could imagine that Twelf instead would just disregard the offending constant: it is possible that the type family as a whole satisfies a totality assertion without that constant, and, in a mathematical sense, adding additional constants never invalidates the fact a totality assertion is true of a family. The reason Twelf does not work this way is that %total actually has a more specific meaning, as we discuss in the next section.
}%
%{
== Expressions from before ==
}%
val : type.
num : nat -> val.
exp : type.
ret : val -> exp.
plus : exp -> exp -> exp.
let : exp -> (val -> exp) -> exp.
eval : exp -> val -> type.
%mode eval +E1 -E2.
eval/val : eval (ret V) V.
eval/plus : eval (plus E1 E2) (num N)
<- eval E1 (num N1)
<- eval E2 (num N2)
<- add N1 N2 N.
eval/let : eval (let E1 ([x] E2 x)) A
<- eval E1 V
<- eval (E2 V) A.
%worlds () (eval _ _).
%total E (eval E _).
%{
== Expressions with times ==
We'll add syntax for 'times' and an evaluation rule
}%
val : type.
num : nat -> val.
exp : type.
ret : val -> exp.
plus : exp -> exp -> exp.
let : exp -> (val -> exp) -> exp.
%% NEW
times : exp -> exp -> exp.
eval : exp -> val -> type.
%mode eval +E1 -E2.
eval/val : eval (ret V) V.
eval/plus : eval (plus E1 E2) (num N)
<- eval E1 (num N1)
<- eval E2 (num N2)
<- add N1 N2 N.
eval/let : eval (let E1 ([x] E2 x)) A
<- eval E1 V
<- eval (E2 V) A.
%% NEW
eval/times : eval (times E1 E2) (num N)
<- eval E1 (num N1)
<- eval E2 (num N2)
<- mult N1 N2 N.
%worlds () (eval _ _).
%total E (eval E _).
%{
== Expressions with pairs ==
}%
val : type.
num : nat -> val.
%% NEW
pair : val -> val -> val.
exp : type.
ret : val -> exp.
plus : exp -> exp -> exp.
let : exp -> (val -> exp) -> exp.
times : exp -> exp -> exp.
%% NEW
fst : exp -> exp.
snd : exp -> exp.
eval : exp -> val -> type.
%mode eval +E1 -E2.
eval/val : eval (ret V) V.
eval/plus : eval (plus E1 E2) (num N)
<- eval E1 (num N1)
<- eval E2 (num N2)
<- add N1 N2 N.
eval/let : eval (let E1 ([x] E2 x)) A
<- eval E1 V
<- eval (E2 V) A.
eval/times : eval (times E1 E2) (num N)
<- eval E1 (num N1)
<- eval E2 (num N2)
<- mult N1 N2 N.
%% NEW
eval/fst : eval (fst E) V1
<- eval E (pair V1 V2).
%% NEW
eval/snd : eval (snd E) V2
<- eval E (pair V1 V2).
%worlds () (eval _ _).
%{
%total E (eval E _).
We get an output coverage error for eval-plus.
Why? Not every expression evaluates to a num, e.g. (plus (ret (pair 6 7)) 8).
== Typing 1 ==
We'll introduce a typing judgement.
}%
tp : type.
natural : tp.
prod : tp -> tp -> tp.
%% relates a value to a type.
of-val : val -> tp -> type.
of-val/num : of-val (num N) natural.
of-val/pair : of-val (pair V1 V2) (prod T1 T2)
<- of-val V1 T1
<- of-val V2 T2.
%% synthesis
%mode of-val +E -T.
%worlds () (of-val _ _).
of : exp -> tp -> type.
%mode of +E -T.
of/ret : of (ret V) T
<- of-val V T.
of/plus : of (plus E1 E2) natural
<- of E1 natural
<- of E2 natural.
of/times : of (times E1 E2) natural
<- of E1 natural
<- of E2 natural.
of/fst : of (fst E) T1
<- of E (prod T1 T2).
of/snd : of (snd E) T2
<- of E (prod T1 T2).
of/let : of (let E1 ([x] E2 x)) T
<- of E1 T1
<- ({x : val} of (E2 x) T).
%{
%worlds () (of _ _).
We promised we'd stay in the empty LF context, but we don't.
== Typing 2a ==
}%
%% relates a value to a type.
of-val : val -> tp -> type.
of-val/num : of-val (num N) natural.
of-val/pair : of-val (pair V1 V2) (prod T1 T2)
<- of-val V1 T1
<- of-val V2 T2.
%% synthesis
%mode of-val +E -T.
%worlds () (of-val _ _).
of : exp -> tp -> type.
of/ret : of (ret V) T
<- of-val V T.
of/plus : of (plus E1 E2) natural
<- of E1 natural
<- of E2 natural.
of/times : of (times E1 E2) natural
<- of E1 natural
<- of E2 natural.
of/fst : of (fst E) T1
<- of E (prod T1 T2).
of/snd : of (snd E) T2
<- of E (prod T1 T2).
of/let : of (let E1 ([x] E2 x)) T
<- of E1 T1
<- ({x : val} of (E2 x) T).
%mode of +E -T.
%block valb : block {x : val}.
%{
%worlds (valb) (of _ _).
== Typing 2 ==
}%
%% relates a value to a type.
of-val : val -> tp -> type.
of-val/num : of-val (num N) natural.
of-val/pair : of-val (pair V1 V2) (prod T1 T2)
<- of-val V1 T1
<- of-val V2 T2.
%% synthesis
%mode of-val +E -T.
%block valb : block {x : val}.
%worlds (valb) (of-val _ _).
of : exp -> tp -> type.
of/ret : of (ret V) T
<- of-val V T.
of/plus : of (plus E1 E2) natural
<- of E1 natural
<- of E2 natural.
of/times : of (times E1 E2) natural
<- of E1 natural
<- of E2 natural.
of/fst : of (fst E) T1
<- of E (prod T1 T2).
of/snd : of (snd E) T2
<- of E (prod T1 T2).
of/let : of (let E1 ([x] E2 x)) T
<- of E1 T1
<- ({x : val} of (E2 x) T).
%mode of +E -T.
%worlds (valb) (of _ _).
%{
== Typing 3 ==
example : of (let (ret (num z)) ([y] (ret y))) natural
= of/let ([x] (of/ret (XXX x))) (of/ret of-val/num).
We need a derivation of of-val x natural!
}%
of-val : val -> tp -> type.
of-val/num : of-val (num N) natural.
of-val/pair : of-val (pair V1 V2) (prod T1 T2)
<- of-val V1 T1
<- of-val V2 T2.
%mode of-val +E -T.
%block valb : some {T : tp} block {x : val} {dx : of-val x T}.
%worlds (valb) (of-val _ _).
of : exp -> tp -> type.
of/ret : of (ret V) T
<- of-val V T.
of/plus : of (plus E1 E2) natural
<- of E1 natural
<- of E2 natural.
of/times : of (times E1 E2) natural
<- of E1 natural
<- of E2 natural.
of/fst : of (fst E) T1
<- of E (prod T1 T2).
of/snd : of (snd E) T2
<- of E (prod T1 T2).
of/let : of (let E1 ([x] E2 x)) T
<- of E1 T1
<- ({x : val} of-val x T1 -> of (E2 x) T).
%mode of +E -T.
%worlds (valb) (of _ _).
%% now we can finish it:
example : of (let (ret (num z)) ([y] (ret y))) natural
= of/let ([x] [dx : of-val x natural] (of/ret dx)) (of/ret of-val/num).