POPL Tutorial/Session 2 Answer

Arithmetic primitives

%sort nat %.
%term z nat %.
%term s %pi nat %-> nat %.
%sort add {_ nat} {_ nat} {_ nat} %.
%mode add %in %in %out %.
%term add/z add z N N %.
%term add/s %pi (add (s M) N (s P)) %<- (add M N P) %.
%worlds () (add _ _ _) %.
%total M (add M _ _) %.

Multiplication

(Interactively) First, let’s write multiplication:

Answer:

%sort mult {_ nat} {_ nat} {_ nat} %.
%term mult/z mult z N z %.
%term mult/s %pi (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 %in %in %out %.

• 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 STELF 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 STELF checks assertions

STELF 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

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

For example, the constant

%term mult/s %pi (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

%term mult-bad-mode mult M N P %.

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

%term mult-badmode2 %pi (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:

%term mult/s %pi (mult (s M) N Q) %<- (add P N Q) %<- (mult M N P) %.

Worlds

STELF 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

STELF 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

%term mult/s %pi (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, STELF 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, STELF 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

%term mult-bad-output %pi (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. STELF 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 STELF to accept a relation as total, STELF must notice that all of these inversions are permissible. STELF permits such inversions when it is readily apparent that they are justified, and those inversions that STELF 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:

%term mult-bad-output-freeness %pi (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. STELF 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:

%sort mult' {_ nat} {_ nat} {_ nat} %.
%mode mult' %in %in %out %.
%term mult'/s %pi (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.

STELF checks input coverage by splitting the input types to case-analyze the various constants that could have been used to inhabit them. For plus, STELF 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), STELF would continue splitting the input space. Because STELF 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 STELF 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 STELF works, though:

• When a %mode declaration is entered, STELF 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, STELF 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, STELF checks termination, then input coverage, then output coverage. When checking output coverage, STELF 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 STELF 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 STELF does not work this way is that %total actually has a more specific meaning, as we discuss in the next section.

Expressions from before

%sort val %.
%term num %pi nat %-> val %.
%sort exp %.
%term ret %pi val %-> exp %.
%term plus %pi exp %-> exp %-> exp %.
%term let %pi exp %-> (%pi val %-> exp) %-> exp %.
%sort eval {_ exp} {_ val} %.
%mode eval %in %out %.
%term eval/val eval (ret V) V %.
%term eval/plus
  %pi (eval (plus E1 E2) (num N))
  %<- (eval E1 (num N1))
  %<- (eval E2 (num N2))
  %<- (add N1 N2 N) %.
%term eval/let %pi (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

%sort val %.
%term num %pi nat %-> val %.
%sort exp %.
%term ret %pi val %-> exp %.
%term plus %pi exp %-> exp %-> exp %.
%term let %pi exp %-> (%pi val %-> exp) %-> exp %.
%% NEW
%term times %pi exp %-> exp %-> exp %.
%sort eval {_ exp} {_ val} %.
%mode eval %in %out %.
%term eval/val eval (ret V) V %.
%term eval/plus
  %pi (eval (plus E1 E2) (num N))
  %<- (eval E1 (num N1))
  %<- (eval E2 (num N2))
  %<- (add N1 N2 N) %.
%term eval/let %pi (eval (let E1 ([x] E2 x)) A) %<- (eval E1 V) %<- (eval (E2 V) A) %.
%% NEW
%term eval/times
  %pi (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

%sort val %.
%term num %pi nat %-> val %.
%% NEW
%term pair %pi val %-> val %-> val %.
%sort exp %.
%term ret %pi val %-> exp %.
%term plus %pi exp %-> exp %-> exp %.
%term let %pi exp %-> (%pi val %-> exp) %-> exp %.
%term times %pi exp %-> exp %-> exp %.
%% NEW
%term fst %pi exp %-> exp %.
%term snd %pi exp %-> exp %.
%sort eval {_ exp} {_ val} %.
%mode eval %in %out %.
%term eval/val eval (ret V) V %.
%term eval/plus
  %pi (eval (plus E1 E2) (num N))
  %<- (eval E1 (num N1))
  %<- (eval E2 (num N2))
  %<- (add N1 N2 N) %.
%term eval/let %pi (eval (let E1 ([x] E2 x)) A) %<- (eval E1 V) %<- (eval (E2 V) A) %.
%term eval/times
  %pi (eval (times E1 E2) (num N))
  %<- (eval E1 (num N1))
  %<- (eval E2 (num N2))
  %<- (mult N1 N2 N) %.
%% NEW
%term eval/fst %pi (eval (fst E) V1) %<- (eval E (pair V1 V2)) %.
%% NEW
%term eval/snd %pi (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.

%sort tp %.
%term natural tp %.
%term prod %pi tp %-> tp %-> tp %.
%% relates a value to a type.
%sort of-val {_ val} {_ tp} %.
%term of-val/num of-val (num N) natural %.
%term of-val/pair %pi (of-val (pair V1 V2) (prod T1 T2)) %<- (of-val V1 T1) %<- (of-val V2 T2) %.
%% synthesis
%mode of-val %in %out %.
%worlds () (of-val _ _) %.
%sort of {_ exp} {_ tp} %.
%mode of %in %out %.
%term of/ret %pi (of (ret V) T) %<- (of-val V T) %.
%term of/plus %pi (of (plus E1 E2) natural) %<- (of E1 natural) %<- (of E2 natural) %.
%term of/times %pi (of (times E1 E2) natural) %<- (of E1 natural) %<- (of E2 natural) %.
%term of/fst %pi (of (fst E) T1) %<- (of E (prod T1 T2)) %.
%term of/snd %pi (of (snd E) T2) %<- (of E (prod T1 T2)) %.
%term of/let %pi (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.
%sort of-val {_ val} {_ tp} %.
%term of-val/num of-val (num N) natural %.
%term of-val/pair %pi (of-val (pair V1 V2) (prod T1 T2)) %<- (of-val V1 T1) %<- (of-val V2 T2) %.
%% synthesis
%mode of-val %in %out %.
%worlds () (of-val _ _) %.
%sort of {_ exp} {_ tp} %.
%term of/ret %pi (of (ret V) T) %<- (of-val V T) %.
%term of/plus %pi (of (plus E1 E2) natural) %<- (of E1 natural) %<- (of E2 natural) %.
%term of/times %pi (of (times E1 E2) natural) %<- (of E1 natural) %<- (of E2 natural) %.
%term of/fst %pi (of (fst E) T1) %<- (of E (prod T1 T2)) %.
%term of/snd %pi (of (snd E) T2) %<- (of E (prod T1 T2)) %.
%term of/let %pi (of (let E1 ([x] E2 x)) T) %<- (of E1 T1) %<- ({x val} of (E2 x) T) %.
%mode of %in %out %.
%block valb {x val}%.

%worlds (valb) (of _ _) %.

Typing 2

%% relates a value to a type.
%sort of-val {_ val} {_ tp} %.
%term of-val/num of-val (num N) natural %.
%term of-val/pair %pi (of-val (pair V1 V2) (prod T1 T2)) %<- (of-val V1 T1) %<- (of-val V2 T2) %.
%% synthesis
%mode of-val %in %out %.
%block valb {x val}%.
%worlds (valb) (of-val _ _) %.
%sort of {_ exp} {_ tp} %.
%term of/ret %pi (of (ret V) T) %<- (of-val V T) %.
%term of/plus %pi (of (plus E1 E2) natural) %<- (of E1 natural) %<- (of E2 natural) %.
%term of/times %pi (of (times E1 E2) natural) %<- (of E1 natural) %<- (of E2 natural) %.
%term of/fst %pi (of (fst E) T1) %<- (of E (prod T1 T2)) %.
%term of/snd %pi (of (snd E) T2) %<- (of E (prod T1 T2)) %.
%term of/let %pi (of (let E1 ([x] E2 x)) T) %<- (of E1 T1) %<- ({x val} of (E2 x) T) %.
%mode of %in %out %.
%worlds (valb) (of _ _) %.

Typing 3

%define 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!

%sort of-val {_ val} {_ tp} %.
%term of-val/num of-val (num N) natural %.
%term of-val/pair %pi (of-val (pair V1 V2) (prod T1 T2)) %<- (of-val V1 T1) %<- (of-val V2 T2) %.
%mode of-val %in %out %.
%block valb [T tp] {x val} {dx of-val x T}%.
%worlds (valb) (of-val _ _) %.
%sort of {_ exp} {_ tp} %.
%term of/ret %pi (of (ret V) T) %<- (of-val V T) %.
%term of/plus %pi (of (plus E1 E2) natural) %<- (of E1 natural) %<- (of E2 natural) %.
%term of/times %pi (of (times E1 E2) natural) %<- (of E1 natural) %<- (of E2 natural) %.
%term of/fst %pi (of (fst E) T1) %<- (of E (prod T1 T2)) %.
%term of/snd %pi (of (snd E) T2) %<- (of E (prod T1 T2)) %.
%term of/let
  %pi (of (let E1 ([x] E2 x)) T)
  %<- (of E1 T1)
  %<- ({x val} %pi (of-val x T1) %-> (of (E2 x) T)) %.
%mode of %in %out %.
%worlds (valb) (of _ _) %.
%% now we can finish it:
%define 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) %.