Uniqueness lemma

From The Twelf Project
Jump to: navigation, search

Many judgements of an object language have the property that, given some subjects of the judgement, the other subjects are determined uniquely. For example: The addition judgement on natural numbers has the property that the two addends determine the sum uniquely. A typing judgement for a programming language may have the property that a term has at most one type. The operational semantics of a programming language may have the property that a term steps to at most one other term. We refer to a metatheorem that establishes such a property a uniqueness lemma.

The goal of this article is to teach you how to prove uniqueness lemmas in Twelf. The only subtlety is that the statement of a uniqueness lemma requires an auxiliary definition of a judgement defining equality at the relevant types.

In this article, we refer to the "given" subjects of the judgement as inputs and those subjects that are determined uniquely by the givens as outputs. However, these inputs and outputs do not need to correspond with the %mode of the judgement: it is meaningful to prove a uniqueness lemma for a judgement that has no mode specified in Twelf. Note that a judgement may satisfy a uniqueness lemma but not define a function: uniqueness says that the outputs are uniquely determined if they exist at all. To know that a judgement defines a function, it is necessary to prove a corresponding effectiveness lemma establishing that some instance of the judgement holds for each input.

Sometimes a uniqueness lemma can be proven trivially by leveraging a %unique declaration.

Example: Flipping bits

The following is a simple example of a uniqueness lemma. First we define bits and a simple relation bit-flip that negates a bit.

bit : type.

bit/0 : bit.
bit/1 : bit.

bit-flip : bit -> bit -> type.

bit-flip/01 : bit-flip bit/0 bit/1.
bit-flip/10 : bit-flip bit/1 bit/0.

We would like to prove that the second argument of bit-flip is determined uniquely by the first. How do we state this theorem? We assume two derivations of bit-flip for the same input that seem to have distinct outputs and we prove that the outputs are the same:

If D : bit-flip B1 B2 and D' : bit-flip B1 B2' then B2 = B2'.

The only subtlety in proving this theorem in Twelf is that we need a judgement representing the equality used in the conclusion. If the output of the judgement is in fact unique (rather than unique modulo some equivalence relation), then the best judgement to use is the identity relation at the appropriate type:

id-bit : bit -> bit -> type.
id-bit/refl : id-bit B B.

Identity internalizes syntactic equality of canonical forms as a judgement: id B B' is inhabited only when B an B' are the same LF term.

Thus, we can prove the theorem by exhibiting the following total relation:

bit-flip-unique : bit-flip B1 B2
               -> bit-flip B1 B2'
               -> id-bit B2 B2'
               -> type.
%mode bit-flip-unique +D1 +D2 -D3.

- : bit-flip-unique bit-flip/01 bit-flip/01 id-bit/refl.

- : bit-flip-unique bit-flip/10 bit-flip/10 id-bit/refl.

%worlds () (bit-flip-unique _ _ _).
%total {} (bit-flip-unique _ _ _).
See Twelf's output

Alternate formulation

Uniqueness can also be expressed in a less-direct but sometimes more-convenient way that is nonetheless logically equivalent to the previous theorem. In this theorem statement, we assume derivations whose inputs are related by an identity relation, and show that the outputs are identical as well. This theorem statement applies when we have evidence that the inputs are identical but the two derivations of the judgement in question have different types. The proof is no more complicated than the previous formulation, because when we derive the precondition id-bit B1 B1' using id-bit/refl (the only rule we could use to derive that fact), B1 and B1' are forced to be identical objects, just as they were in the previous proof.

bit-flip-unique-alt : id-bit B1 B1'
                       -> bit-flip B1 B2
                       -> bit-flip B1' B2'
                       -> id-bit B2 B2'
                       -> type.
%mode bit-flip-unique-alt +D0 +D1 +D2 -D3.

- : bit-flip-unique-alt id-bit/refl bit-flip/01 bit-flip/01 id-bit/refl.

- : bit-flip-unique-alt id-bit/refl bit-flip/10 bit-flip/10 id-bit/refl.

%worlds () (bit-flip-unique-alt _ _ _ _).
%total {} (bit-flip-unique-alt _ _ _ _).
See Twelf's output

However, this alternate formulation is equivalent to the above uniqueness lemma. It is easy to see that this lemma implies the above, as we can always call this lemma with id-bit/refl. To prove the other direction, we can compose the above uniqueness lemma with a respects lemma showing that bit-flip respects equality. Here is an example of proving bit-flip-unique-alt using a uniqueness lemma and a respects lemma (here is Twelf's output). Because the respects lemma will often be necessary for other reasons, it is usually preferable to prove it and the above uniqueness lemma, rather than the composed version presented here.

Bigger example: determinism of evaluation

As a slightly more-involved example of a uniqueness lemma, we can prove that the operational semantics of the simply typed λ-calculus are deterministic:

If and then .

Here, equality of terms means syntactic identity modulo α-equivalence

This proof reuses the formulation of the STLC from Proving metatheorems with Twelf; see that article for a description of the language and its operational semantics. We recap the signature for the STLC here:

%% Syntax
tp    : type.

unit  : tp.
arrow : tp -> tp -> tp.

tm    : type.
empty : tm.
lam   : tp -> (tm -> tm) -> tm.
app   : tm -> tm -> tm.

%% Dynamic Semantics

value       : tm -> type.
value_empty : value empty.
value_lam   : value (lam T2 ([x] E x)).
step          : tm -> tm -> type.
step_app_1    : step (app E1 E2) (app E1' E2)
                 <- step E1 E1'.
step_app_2    : step (app E1 E2) (app E1 E2')
                 <- step E2 E2'
                 <- value E1.

step_app_beta : step (app (lam T2 ([x] E x)) E2) (E E2)
                 <- value E2.

To state the uniqueness lemma, we define an identity type for tm:

id : tm -> tm -> type.
refl : id E E.

The judgement id represent object-language α-equivalence: α-equivalent STLC terms are represented by α-equivalent LF terms, and id E E' is inhabited exactly when E and E' are α-equivalent in LF.

The proof of determinism requires a congruence lemma, which states that applications are equal if their subterms are:

id_app_cong : id E1 E1' 
               -> id E2 E2' 
               -> id (app E1 E2) (app E1' E2') 
               -> type.
%mode id_app_cong +X1 +X2 -X3.

- : id_app_cong refl refl refl.

%worlds () (id_app_cong _ _ _).
%total {} (id_app_cong _ _ _).

Next, we present a complete proof of determinism:

det : step E E' -> step E E'' -> id E' E'' -> type.
%mode det +X1 +X2 -X3.

det-1 : det (step_app_1 DstepE1') (step_app_1 DstepE1'') DidApp
         <- det DstepE1' DstepE1'' DidE1
         <- id_app_cong DidE1 refl DidApp.

det-2 : det (step_app_2 _ DstepE2') (step_app_2 _ DstepE2'') DidApp
         <- det DstepE2' DstepE2'' DidE2
         <- id_app_cong refl DidE2 DidApp.

det-b : det (step_app_beta _) (step_app_beta _) refl.

%worlds () (det _ _ _).
%total D (det D _ _).
See Twelf's output

Observe that the totality assertion for this type family implies the informal statement above.

The proof consists of three cases, and in each case the two step derivations conclude with the same final rule. The cases det-1 and det-2 appeal to the inductive hypothesis on the subderivations and then use the congruence lemma for identity. The case det-b concludes equality by reflexivity because the left-hand term of step-app-beta uniquely determines the form of the right-hand term.

Twelf successfully proves the totality of det, even though the relation elides the "off-diagonal" cases where the two step derivations do not concludes with the same final rule. This is because the off-diagonal cases are all vacuously true---and moreover, Twelf's coverage checker rules out these contradictory cases automatically. For example, if one derivation concluded with step-app-1 and the other with step-app-2, then there would be subderivations concluding both value E1 and step E1 E1'. These two types can never be simultaneously inhabited: step is only inhabited when E1 is an application, and there is no rule inhabiting value for an application. Similarly, if one derivation concluded with step-app-1 and the other with step-app-beta, subderivations would give a step derivation whose left-hand side is a lam, which cannot exist. The other off-diagonal cases can be contradicted in a similar manner. Twelf's coverage checker rules out cases like these where the inputs to a metatheorem result in an uninhabited instance of some type family. See also: Reasoning from false

Read more Twelf tutorials and other Twelf documentation.