Canonical forms lemma

From The Twelf Project
Jump to: navigation, search
This article is about proving an object language lemma. For the notion of canonical form within LF itself, see canonical form.

In a standard proofs of type safety, the progress theorem requires canonical forms lemmas about the values in a language. These lemmas are usually in the form "If e is a value and e : T, then e is of some form appropriate for T". A specific example would be "If e is a value and e : T1 → T2, then e is of the form λx:T1.e'".

Depending on the complexity of the type system, there are two general ways to state and prove these lemmas. In some cases, Twelf's input coverage can give you the canonical forms lemma for free. In other cases, you must state and prove canonical forms explicitly using equality.

Canonical forms lemmas for free

If there is only one rule through which the canonical form at a particular type can be derived, then Twelf's input coverage is actually strong enough to give you canonical forms for free via inversion.

Consider the following language:

tp : type.
tp/unit  : tp.
tp/arrow : tp -> tp -> tp.

exp : type.

exp/unit : exp.
exp/lam  : tp -> (exp -> exp) -> exp.
exp/app  : exp -> exp -> exp.

of : exp -> tp -> type.

of/unit : of exp/unit tp/unit.

of/lam  : of (exp/lam T1 E) (tp/arrow T1 T2)
           <- ({x} of x T1
                -> of (E x) T2).

of/app  : of (exp/app E1 E2) T2
           <- of E2 T1
           <- of E1 (tp/arrow T1 T2).


val : exp -> type.

val/unit : val exp/unit.

val/lam  : val (exp/lam _ _).


step : exp -> exp -> type.

step/app-1    : step (exp/app E1 E2) (exp/app E1' E2)
                 <- step E1 E1'.

step/app-2    : step (exp/app E1 E2) (exp/app E1 E2')
                 <- step E2 E2'
                 <- val E1.

step/app-beta : step (exp/app (exp/lam _ E) E2) (E E2)
                 <- val E2.


notstuck : exp -> type.

notstuck/val  : notstuck E
                 <- val E.

notstuck/step : notstuck E
                 <- step E E'.

To prove progress for this language, we use an output factoring lemma that collects the post-inductive-call reasoning in the application case:

progress-exp/app : notstuck E1
                    -> notstuck E2
                    -> of E1 (tp/arrow _ _)
                    -> notstuck (exp/app E1 E2)
                    -> type.
%mode progress-exp/app +D1 +D2 +D3 -D4.

- : progress-exp/app (notstuck/step S)  _ _ 
     (notstuck/step (step/app-1 S)).

- : progress-exp/app (notstuck/val V) (notstuck/step S) _
     (notstuck/step (step/app-2 V S)).

- : progress-exp/app (notstuck/val val/lam) (notstuck/val V2) (of/lam _)
     (notstuck/step (step/app-beta V2)).

%worlds () (progress-exp/app _ _ _ _).
%total {} (progress-exp/app _ _ _ _).

In the final case, we use inversion to assert that E1 is a value in the form of a lambda. Because we also pass in a typing derivation that says E1 is of an arrow type, Twelf's input coverage verifies that the only time E1 is a value and has an arrow type is when it is a lambda. Because the type system is simple enough that Twelf can figure out that the only values of arrow type are lambdas, we get canonical forms "for free".

It is then simple to complete the proof of progress:

progress : of E T
            -> notstuck E
            -> type.
%mode progress +D1 -D2.

- : progress of/unit (notstuck/val val/unit).

- : progress (of/lam _) (notstuck/val val/lam).

- : progress (of/app D1 D2) NS
     <- progress D1 NS1
     <- progress D2 NS2
     <- progress-exp/app NS1 NS2 D1 NS.

%worlds () (progress _ _).
%total (D1) (progress D1 _).
See Twelf's output

Canonical forms lemmas stated using equality

Some languages do not have the luxury of having exactly one rule through which a canonical form could be derived. This is common for languages with re-typing rules that make use of subtyping/type equality. In such languages, canonical forms lemmas must be explicitly stated and proven. The conclusion of the lemma "e is of the form ..." can be stated in a straightforward way using shallow equality. This example makes use of output factoring and reasoning from equality.

For example, we extend the above language with a trivial notion of subtyping. It is equivalent to syntactic equality on types. The purpose of this tutorial is to illustrate how to state/prove canonical forms lemmas when subtyping/equality are part of the type system, and this trivial notion is enough to motivate the discussion.

tp-sub  : tp -> tp -> type.

tp-sub/unit  : tp-sub tp/unit tp/unit.

tp-sub/arrow : tp-sub (tp/arrow T1 T2) (tp/arrow T3 T4)
                <- tp-sub T2 T4
                <- tp-sub T3 T1.

of/sub  : of E1 T2
           <- tp-sub T1 T2
           <- of E1 T1.

Now, we state and prove the canonical forms lemma explicitly. In the theorem statement, we use the syntactic equality judgement as an output in order to state "E1 is of the form (exp/lam T E)".

seq-exp : exp -> exp -> type.
seq-exp/i : seq-exp E E. 

cfl-tp/arrow    : val E1
                  -> of E1 (tp/arrow _ _)
                  -> seq-exp E1 (exp/lam T E)
                  -> type.
%mode cfl-tp/arrow +D1 +D2 -D3.

- : cfl-tp/arrow val/lam (of/lam _) seq-exp/i.

- : cfl-tp/arrow V (of/sub D1 (tp-sub/arrow _ _)) DQ
     <- cfl-tp/arrow V D1 DQ.

%worlds () (cfl-tp/arrow _ _ _).
%total (D1) (cfl-tp/arrow _ D1 _).

Next, we define a helper lemma for showing that (exp/app E1 E2) is notstuck when E1 is of the form (exp/lam T E) and E2 is a value. We use this lemma because we get the derivation of (seq-exp E1 (exp/lam T E)) as the output of the canonical forms lemma. If we were to try to invert the derivation as an output, we would cause Twelf's coverage checker to fail. So instead, we call a helper lemma with the equality derivation as an input. Because the derivation is an input, we can safely apply inversion on it.

progress-exp/app-beta : seq-exp E1 (exp/lam T E)
                         -> val E2
                         -> notstuck (exp/app E1 E2)
                         -> type.
%mode progress-exp/app-beta +D1 +D2 -D3.

- : progress-exp/app-beta seq-exp/i V (notstuck/step (step/app-beta V)).

%worlds () (progress-exp/app-beta _ _ _).
%total {} (progress-exp/app-beta _ _ _).

Next, we prove the output factoring lemma:

progress-exp/app : notstuck E1
                    -> notstuck E2
                    -> of E1 (tp/arrow _ _)
                    -> notstuck (exp/app E1 E2)
                    -> type.
%mode progress-exp/app +D1 +D2 +D3 -D4.

- : progress-exp/app (notstuck/step S)  _ _
     (notstuck/step (step/app-1 S)).

- : progress-exp/app (notstuck/val V) (notstuck/step S) _
     (notstuck/step (step/app-2 V S)).

Because there is more than one way to derive that a value that has an arrow type, we must use the canonical forms lemma we have just proven. To make use of the equality we get out of the canonical forms lemma, we call the special helper lemma progress-exp/app-beta.

- : progress-exp/app (notstuck/val V) (notstuck/val V2) D1
     NS
     <- cfl-tp/arrow V D1 DQ
     <- progress-exp/app-beta DQ V2 NS.

%worlds () (progress-exp/app _ _ _ _).
%total {} (progress-exp/app _ _ _ _).
See Twelf's output

Finally, we prove the overall progress theorem as before.

progress : of E T
            -> notstuck E
            -> type.
%mode progress +D1 -D2.

- : progress of/unit (notstuck/val val/unit).

- : progress (of/lam _) (notstuck/val val/lam).

- : progress (of/app D1 D2) NS
     <- progress D1 NS1
     <- progress D2 NS2
     <- progress-exp/app NS1 NS2 D1 NS.

- : progress (of/sub D1 _) NS
     <- progress D1 NS.

%worlds () (progress _ _).
%total (D1) (progress D1 _).
See Twelf's output

The only change from before is the case for of-sub, where the inductive hypothesis gives the result.

Note: There is actually a very subtle way to prove progress-exp/app using canonical forms lemmas "for free". However, explicitly stating and proving the canonical forms lemma is the more robust strategy in general.


Read more Twelf tutorials and other Twelf documentation.