Proving metatheorems:Representing the syntax of the natural numbers

From The Twelf Project
Jump to: navigation, search
Proving metatheorems with Twelf Next:
Simply typed LF

To use Twelf, you need to know how to represent deductive systems using the LF logical framework. LF is a very convenient language for representing deductive systems that involve variable binding and hypothetical judgements, such as programming languages and logics. However, we won't see any examples of such uses of LF until later. The goal of the first part of this guide is to take a broad sweep through LF and Twelf; you will see how to represent and prove properties of a very simple language, which will prepare you for more sophisticated (and more impressive) content later on.

Our first task is to introduce LF and see how to represent the syntax of a deductive system in it. We refer to a language that we are formalizing in LF as an object language (i.e., it is the object of our study). In contrast, we sometimes refer to LF as the meta-language. To keep things simple, we use the natural numbers as first example object language.

Natural numbers

Informal definition

In informal mathematical notation ("informal" is used here in the sense of "not formalized"), the syntax of the natural numbers is defined by the following grammar:

That is, is a natural number, and if is a natural number, then is as well.

LF representation

LF is a typed lambda-calculus. We represent an object language in LF by writing an LF signature. A signature declares type and term constants. For example, this LF signature defines a type representing the natural numbers:

nat : type.
z   : nat.
s   : nat -> nat.

Intuitively, the LF type nat classifies the LF representations of natural numbers. The LF constant z corresponds to and the LF constant s corresponds to .

The signature declares that z has type nat, which makes sense because is a natural number.

The signature declares that s has function type nat -> nat. An LF term of function type can be applied to another LF term of the appropriate type to form a new term. For example, the constant s can be applied to the constant z to form the term s z representing the number . Then s can be applied to this term to form s (s z), and so on. An informal natural number is represented by the LF term s N where is represented by N.

We can state the relationship between the informal presentation of the object language and its LF representation by giving an encoding judgement relating an informal object with its representation:



Is this a correct encoding of the natural numbers? In the LF methodology, the correctness criterion for an encoding is called adequacy:

An encoding is adequate iff it is an isomorphism between the informal object-language entities and the LF terms of the appropriate type.

Adequacy permits any reasoning in or about an object language to be "ported" between the informal and LF descriptions. For example, if we prove a property about the LF representation, by adequacy, that property holds for the informal description as well. Adequacy ensures that the work we do using the formalization has bearing on the actual language that we had in mind to begin with.

In this example, the informal object-language entity is the syntax of the natural numbers, and the appropriate LF type is nat. Thus, to satisfy adequacy, the above encoding judgement must be an isomorphism between informal natural numbers and LF terms of type nat. In this case, because both the informal and LF representations are first order (there is no binding structure), adequacy requires only a simple bijection. (More complicated examples require the adequacy argument to exhibit a compositional bijection instead of the simple bijection discussed here - an example like this is discussed later.)

To establish a bijection, we must show three things:

  1. If then is a well-formed number and is an LF term of type nat.
  2. For all , there exists a unique LF term such that .
  3. For all LF terms N : nat, there exists a unique such that .

The first part establishes that the judgement relates informal numbers to LF terms of the appropriate type. The second and third show that this relation defines a function in both directions. Because we show that the same relation is functional in both directions, these functions are mutually inverse, establishing a bijection.

The first part can be proved by a simple induction on the derivation of the encoding. The second can be proved by structural induction on . The third part states that all LF terms of type nat represent a unique informal number. It can be proved by induction on the structure of LF terms. To do so, we will need to give a more precise account of LF.

Proving metatheorems with Twelf Next:
Simply typed LF