POPL Tutorial/Session 2 Answer

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

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.

ERROR: option 'name' deprecated or invalid

ERROR: option 'name' deprecated or invalid

For example, the constant

ERROR: option 'name' deprecated or invalidERROR: option 'ignore' deprecated or invalid
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

ERROR: option 'include' deprecated or invalidERROR: option 'name' deprecated or invalid
mult-bad-mode : mult M N P.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

mult-bad-mode : {M:nat} {N:nat} {P:nat} mult M N P. Error: Occurrence of variable P in output (-) argument not necessarily ground

%% ABORT %%

is not well-moded---the output P is not determined by the inputs. Similarly,

ERROR: option 'include' deprecated or invalidERROR: option 'name' deprecated or invalid
mult-badmode2 : mult N1 N2 N3 
		 <- mult N4 N2 N3.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: Occurrence of variable P in output (-) argument not necessarily ground %% ABORT %% %% OK %% mult-badmode2 : {N4:nat} {N2:nat} {N3:nat} {N1:nat} mult N4 N2 N3 -> mult N1 N2 N3. Error: Occurrence of variable N4 in input (+) argument not necessarily ground

%% ABORT %%

is not well-moded---first input to the premise is not determined by the inputs of the conclusion.

Subgoal order matters:

ERROR: option 'include' deprecated or invalidERROR: option 'name' deprecated or invalid
mult/s : mult (s M) N Q
	  <- add P N Q
	  <- mult M N P.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: Occurrence of variable P in output (-) argument not necessarily ground %% ABORT %% %% OK %% mult/s : {M:nat} {N:nat} {P:nat} {Q:nat} mult M N P -> add P N Q -> mult (s M) N Q. Error: Occurrence of variable P in input (+) argument not necessarily ground

%% ABORT %%

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

ERROR: option 'name' deprecated or invalidERROR: option 'ignore' deprecated or invalid
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:

ERROR: option 'include' deprecated or invalidERROR: option 'name' deprecated or invalid
%total N (mult _ N _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: Occurrence of variable P in output (-) argument not necessarily ground %% ABORT %% %% OK %% Error: Termination violation: ---> (N) < (N)

%% ABORT %%

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

ERROR: option 'include' deprecated or invalidERROR: option 'name' deprecated or invalid
mult-bad-output : mult (s N1) N2 (s (s N3))
                   <- mult N1 N2 (s N3).
%worlds () (mult _ _ _).
%total N1 (mult N1 N2 N3).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: Occurrence of variable P in output (-) argument not necessarily ground %% ABORT %% %% OK %% mult-bad-output : {N1:nat} {N2:nat} {N3:nat} mult N1 N2 (s N3) -> mult (s N1) N2 (s (s N3)). %worlds () (mult _ _ _). Error: Totality: Output of subgoal not covered Output coverage error --- missing cases: {X1:nat} {X2:nat} |- mult X1 X2 z.

%% ABORT %%

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:

ERROR: option 'include' deprecated or invalidERROR: option 'name' deprecated or invalid
mult-bad-output-freeness : mult (s N1) N2 (s N2)
                            <- mult N1 N2 N2.
%worlds () (mult _ _ _).
%total N1 (mult N1 N2 N3).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: Occurrence of variable P in output (-) argument not necessarily ground %% ABORT %% %% OK %% mult-bad-output-freeness : {N1:nat} {N2:nat} mult N1 N2 N2 -> mult (s N1) N2 (s N2). %worlds () (mult _ _ _). Error: Constant mult-bad-output-freeness Occurrence of variable N2 in output (-) argument not free

%% ABORT %%

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:

ERROR: option 'include' deprecated or invalidERROR: option 'name' deprecated or invalid
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 _ _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: Occurrence of variable P in output (-) argument not necessarily ground %% ABORT %% %% OK %% mult' : nat -> nat -> nat -> type. %mode +{N1:nat} +{N2:nat} -{X3:nat} (mult' N1 N2 X3). mult'/s : {P:nat} {N:nat} {Q:nat} {M:nat} add P N Q -> mult' M N P -> mult' (s M) N Q. %worlds () (mult' _ _ _). Error: Coverage error --- missing cases: {X1:nat} {X2:nat} |- mult' z X1 X2.

%% ABORT %%

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:

  1. 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.
  2. 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.
  3. 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 _ _).
ERROR: option 'name' deprecated or invalid
%total E (eval E _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: Occurrence of variable P in output (-) argument not necessarily ground %% ABORT %% %% OK %% Error: Undeclared identifier eval in call pattern

%% ABORT %%

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).
ERROR: option 'name' deprecated or invalid
%worlds () (of _ _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: Occurrence of variable P in output (-) argument not necessarily ground %% ABORT %% %% OK %% Error: Undeclared identifier of in call pattern

%% ABORT %%

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}.
ERROR: option 'name' deprecated or invalid
%worlds (valb) (of _ _).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: Occurrence of variable P in output (-) argument not necessarily ground %% ABORT %% %% OK %% Error: Undeclared identifier of in call pattern

%% ABORT %%

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

ERROR: option 'name' deprecated or invalid
example : of (let (ret (num z)) ([y] (ret y))) natural 
 	   = of/let ([x] (of/ret (XXX x))) (of/ret of-val/num).
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

Error: Occurrence of variable P in output (-) argument not necessarily ground %% ABORT %% %% OK %% Error: Undeclared identifier of Error: Undeclared identifier let Error: Undeclared identifier ret Error: Undeclared identifier num Error: Undeclared identifier ret Error: Undeclared identifier natural Error: Undeclared identifier of/let Error: Undeclared identifier of/ret Error: Undeclared identifier of/ret Error: Undeclared identifier of-val/num Error: Ambiguous level The level of this term could not be inferred Defaulting to object level Error: Ambiguous reconstruction Inferred: {x:`%A1%} {x1:`%A2%} type Omitted term has ambiguous kind Error: Ambiguous reconstruction Inferred: [x:`%A1%] [x1:`%A2%] `%A3% Omitted type is ambiguous Error: Ambiguous reconstruction Inferred: {x:`%A4%} {x1:{x1:`%A5%} `%A6%} `%A1% Omitted term has ambiguous type Error: Ambiguous reconstruction Inferred: {x:`%A7%} `%A4% Omitted term has ambiguous type Error: Ambiguous reconstruction Inferred: {x:{x:`%A8%} `%A9%} {x1:`%A10%} `%A3% Omitted term has ambiguous type Error: Ambiguous reconstruction Inferred: {x1:`%A11%} `%A9% Omitted term has ambiguous type Error: Ambiguous reconstruction Inferred: {x:`%A12%} `%A10% Omitted term has ambiguous type Error: 18 errors found

%% ABORT %%

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).