Proving metatheorems:Representing the judgements of the STLC
Previous: Representing syntax |
Proving metatheorems with Twelf | Next: Proving metatheorems |
Static semantics
Informal definition
The typing rules for the simply typed lambda calculus use a typing context containing assumptions of the form . Such a context is well-formed when all variables in it are distinct.
This is a hypothetical judgement, which means that the following structural properties are true:
- Hypothesis: .
- Weakening: if and is fresh then .
- Exchange: if then .
- Substitution: if and then .
Hypothesis is derivable by the rule . Weakening, exchange, and substitution are admissible.
LF representation
In the previous section, we used LF binding to represent object-language variables. In this section, we use LF binding to represent object-language hypothetical judgements. The following LF signature represents the above judgement with the LF type family of.
of : tm -> tp -> type. of-empty : of empty unit. of-lam : of (lam T2 ([x] E x)) (arrow T2 T) <- ({x: tm} of x T2 -> of (E x) T). of-app : of (app E1 E2) T <- of E1 (arrow T2 T) <- of E2 T2.
The first thing to note is that the type family is indexed by a tm and a tp but not a representation of the context . The reason for this is that we identify the object-language context with the LF context. Specifically, an object-language assumption does two things:
- It binds the variable .
- It declares a typing assumption .
Thus, an object-language assumption is represented by the following two LF assumptions:
x : tm, dx : of x T (where T is the encoding of ).
The first LF variable represents an object-language term x, as per the encoding of syntax in the previous section. The second variable represents a derivation that of x T. Consequently, there is no LF constant corresponding to the rule ; uses of this rule are represented by uses of the corresponding LF variable dx.
This representation of hypotheses gives rise to the higher-order premise of the constant of-lam, which has type
{x: tm} of x T2 -> of (E x) T
An LF term of this type has the form ([x] [dx: of x T2] M), where M : of (E x) T in an LF context extended with x : tm, dx : of x T2. Thus, M is the representation of an object-language derivation under the additional assumption .
The constants of-empty and of-app correspond to the informal inference rules of the same name; they are no more complicated than the rules for the judgements on natural numbers from the previous sections.
Some examples may help clarify the intended representation:
This article or section needs examples. |
Eta-expansion. As we mentioned before, Twelf permits programmers to write non-eta-expanded terms, which it treats as syntactic sugar for their eta-expansions. For example, we could equivalently have written:
of-lam : of (lam T2 E) (arrow T2 T) <- ...
This version differs from of-lam above in that the term E is not eta-expanded. Some consider it good Twelf style to write terms in a fully eta-expanded (eta-long) form, because (1) the eta-expanded terms are the canonical forms of LF, and (2) the eta-expansion makes the binding structure apparent in the syntax, without knowing the types of the involved constants. On the other hand, readers who know the types of the constants may find the eta-short version easier to read.
Theorems for free
There are several advantages to using this higher-order representation of a hypothetical judgement, as opposed to a first-order representation where the context is treated explicitly.
First, the representation is quite succinct: there is no need define and work with auxiliary data structures like lists of distinct assumptions.
More importantly, this representation gives the structural properties of the hypothetical judgement for free: the structural properties for the object language are inherited from the corresponding properties of LF. For instance, there is no need to prove a substitution lemma about the object language. As an example, we can derive
T:tp, T2:tp. E:tm->tm, E2:tm, D1:({x : tm} of x T2 -> of (E x) T), D2:(of E2 T2) ⊦ D1 E2 D2 : of (E E2) T
The term D1 E2 D2 represents a derivation that the substitution (E E2) is well-typed. (We call the LF application (E E2) a substitution because when E is substituted by an actual term [x] M, the application will reduce to [E2/x]M.)
Adequacy
The adequate theorem for typing derivations is as follows:
- Adequacy for typing: There is a compositional bijection between informal derivations of and LF terms D such that x1 : tm, dx1 : of x1 T1, ... ⊦ D : of E T, where , , and , ... .
To prove this adequacy theorem, it is necessary to show that STLC terms and types remain adequately represented when considered in LF contexts of this form. Intuitively, adding canonical forms of type of does not change the canonical forms of types tp and tm because STLC typing derivations cannot appear in STLC types or terms. This kind of argument can be made precise using subordination.
Dynamic semantics
Informal definition
We define the dynamic semantics of the STLC by a call-by-value, left-to-right structural operational semantics on closed terms.
The judgement identifies the values:
Next, we define the operational semantics with a judgement :
LF representation
These judgements are represented in LF in the usual fashion. The closed LF terms of these types adequately represent the above judgements.
value : tm -> type. value-empty : value empty. value-lam : value (lam T ([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') <- value E1 <- step E2 E2'. step-app-beta : step (app (lam T2 ([x] E x)) E2) (E E2) <- value E2.
In step-app-beta, the right-hand term is the application E E2, which represents the substitution on the right-hand side of the informal rule.
And that completes our representation of the STLC in LF. Now, we can start proving metatheorems about the language using Twelf.
Previous: Representing syntax |
Proving metatheorems with Twelf | Next: Proving metatheorems |