Slide 1

Weak Normalization for the Simply-Typed Lambda-Calculus in Twelf

A Case Study on Higher-Order Abstract Syntax

Andreas Abel

LFM’04, IJCAR Cork, Ireland July 5, 2004

Work supported by: GKLI (DFG), TYPES & APPSEM-II (EU), CoVer (SSF)

Slide 2

Twelf

• Logical framework based on the Edinburgh LF (dependently-typed λ-calculus)

• Propositions-as-types, derivations-as-objects

• Higher-order abstract syntax (HOAS)

• No internal recursion or induction

• Higher-order logic programming

• Applications:

– Prototyping of logics and programming languages

– Verification of syntactic properties (e.g., Church-Rosser, subject reduction, cut elimination)

– Type-checking dependent types (Appel, Foundational PCC; Stump, SVC)

Slide 3

Twelf Syntax

• Kinds, types and terms.

𝕂 ::= type  kind of types
| {𝕏:𝔸}𝕂  dependent function kind
𝔸 ::= 𝔽 𝕄_{1} … 𝕄_{n} base type (user-def.)
| {𝕏:𝔸}𝔸  dependent function type
| 𝔸 → 𝔸  non-dependent function type
𝕄 ::= ℂ  term constant (user-def.)
| 𝕏  term variable
| [𝕏:𝔸]𝕄  term abstraction
| 𝕄 𝕄  term application

• Terms considered upto βη-equality

• No user-def. reduction rules: all functions parametrics

Slide 4

Representation of Syntactic Objects in Twelf

• Representation of simple types A, B, C ::= ∗ | A → B.

ty     : type.
*      : ty.
=>     : ty -> ty -> ty.

• Representation of λ-terms r, s, t, u ::= x | λx.t | r s.

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

• HOAS = represent object variables by framework variables.

twice = lam [f:tm] lam [x:tm] app f (app f x).

Slide 5

Representation of Judgements without Hypotheses

• Weak head reduction t ⟶_{w} t′.

\overline{(λx.t) s ⟶_{w} [s/x]t} beta    \frac{r ⟶_{w} r′}{r s ⟶_{w} r′ s} appl

• Representation in Twelf.

-->w  : tm -> tm -> type.
beta  : app (lam T) S -->w T S.
appl  : R -->w R' -> app R S -->w app R' S.

• Substitution in object theory is application of the framework.

Slide 6

Representation of Judgements with Hypotheses

• Type assignment, natural-deduction style.

x : A ; \begin{matrix}· \\ · \\ · \end{matrix} ; t : B ; \overline{of lam} ; λx.t : A → B  r : A → B  s : A ; \overline{of app} ; r s : B

• Typing assumption is represented as hypothetical judgement.

of     : tm -> ty -> type.
of_lam : ({x:tm} of x A -> of (T x) B)
           -> of (lam [x:tm] T x) (A => B).
of_app : of R (A => B) -> of S A -> of (app R S) B.

Slide 7

Weak Head Reduction is Closed under Substitution

• Lemma: If t ⟶^{D}_{w} t′ then [u/y]t ⟶^{D'}_{w} [u/y]t′.

• Proof: By induction on the derivation D of t ⟶_{w} t′.

– Case (λx.t) s ⟶^{beta}_{w} [s/x]t. W.l.o.g. x ≠ y and x not free in u. Then,

\begin{aligned}[u/y]((λx.t) s) & = & (λx.[u/y]t) [u/y]s \\ & ⟶^{beta}_{w} & [[u/y]s/x][u/y]t & = & [u/y][s/x]t. \end{aligned}

– Case r s ⟶^{appl D}_{w} r′ s with r ⟶^{D}_{w} r′. By ind. hyp.,

[u/y]r ⟶^{D'}_{w} [u/y]r′. Hence,

\begin{aligned}[u/y](r s) & = & ([u/y]r) ([u/y]s) \\ & ⟶^{appl D'}_{w} & ([u/y]r′) ([u/y]s) & = & [u/y](r′ s) \end{aligned}

Slide 8

Representation of Theorems and Proofs

• A theorem is represented as a functional relation.

     subst_red : {U:tm} ({y:tm} T y -->w T' y)
                             -> T U -->w T' U -> type.
     %mode subst_red +U +D -D'.

• Its proof is represented as a logic program which implements the relation.

     subst_red_beta: subst_red U ([y] beta) beta.
     subst_red_appl: subst_red U ([y] appl (D y)) (appl D')
                     <- subst_red U D D'.
     %terminates D (subst_red _D _).

• Function must be total to represent a valid proof.

• This requires termination and coverage of all possible inputs.

Slide 9

A Formalized Proof of Weak Normalization for the STL

• Structure of a normalization proof:

1. Define a relation t ⇓ A which is closed under application.

2. Show: If t : A then t ⇓ A.

3. Show: If t ⇓ A then t is normalizing.

• Tait and crowd: t ⇓ A is a logical relation (semantical).

• Joachimski and Matthes (2004): t ⇓ A is a finitary inductive definition.

• Forerunners: Goguen (1995), van Raamsdonk and Severi (1995).

Slide 10

Inductive Characterization of Weakly Normalizing Terms

• “De-vectorized” version of Joachimski and Matthes (2004)

• Γ ⊢ t ⇓ A: t is weakly normalizing of type A.

• Γ ⊢ t ↓^{x} A: t is wn and neutral of type A.

• Rules:

\frac{(x:A) ∈ Γ}{Γ ⊢ x ↓^{x} A}  \frac{Γ ⊢ r ↓^{x} A → B  Γ ⊢ s ⇓ A}{Γ ⊢ r s ↓^{x} B} wne app
\frac{Γ ⊢ r ↓^{x} A}{Γ ⊢ r ⇓ A} wn ne
\frac{Γ, x:A ⊢ t ⇓ B}{Γ ⊢ λx.t ⇓ A → B} wn lam    \frac{r ⟶_{w} r′  Γ ⊢ r′ ⇓ A}{Γ ⊢ r ⇓ A} wn exp

Slide 11

Difficult: Closure under Application

• Lemma: Let D :: Γ ⊢ s ⇓ A.

1. If E :: Γ ⊢ r ⇓ A → C then Γ ⊢ r s ⇓ C.

2. If E :: Γ, x:A ⊢ t ⇓ C, then Γ ⊢ [s/x]t ⇓ C.

3. If E :: Γ, x:A ⊢ t ↓^{x} C, then Γ ⊢ [s/x]t ⇓ C and C is a subexpression of A.

4. If E :: Γ, x:A ⊢ t ↓^{y} C with x ≠ y, then Γ ⊢ [s/x]t ↓^{y} C.

• Proof: Simultaneously by main induction on type A (for part 3) and side induction on the derivation E.

• Similar to Girard, Lafont and Taylor (1989): Lexicographic induction on highest degree (=type) of a redex and the number of redexes of highest degree.

Slide 12

Closure under Application and Substitution in Twelf

• Representation of lemma as 4 type families.

• “C is a subexpression of A” expressed by %reduces C <= A.

• Mutual lexicographic termination order.

Slide 13

Soundness of Inductive Characterization

• Simple induction: t ⇓ A for every typed term t : A.

• Lemma (Soundness): If t ⇓ A then t ⟶^{∗} v for some v.

• Requires characterization of valued and properties of reduction.

• Technical, but well understood. □

Slide 14

Tait-Style Proofs in Twelf?

• Heart of Tait’s proof is the rule:

\frac{∀s. s ⇓ A ⇒ r s ⇓ B}{r ⇓ A → B}

• Literal encoding in Twelf…

       ({S:tm} wn S A -> wn (app R S) B) -> wn R (A => B).

• … means something else:

if for a fresh term S for which we assume wn S A it holds

     that wn (app R S) B, then wn R (A => B).

• Problem: Tait’s infinitary premise is not expressible.

Slide 15

Strong Normalization in Twelf?

• Classical definition of strongly normalizing: no infinite reduction sequences.

• No good in a constructive setting.

• Inductive definition of strongly normalizing: wellfounded part of reduction relation.

\frac{∀t′. t ⟶ t′ ⇒ sn t′}{sn t} ,

• Suffers likewise from an infinitary premise.

Slide 16

Conclusion

• Normalization for a proof-theoretically weak object theory directly implementable in Twelf.

• Limits for normalization proofs: expressiveness of Twelf, termination checker.

• Conjecture 1: Infinitary premises not expressible in Twelf.

• Conjecture 2: Strong normalization not expressible in Twelf.

• Conjecture 3: Proof-theoretical strength of Twelf bounded by arithmetic.

Slide 17

Related Work

• Altenkirch (1993): SN for System F in LEGO.

• Filinski in 1990s: Feasibility of logical relations in Twelf. Not published.

• Berghofer and Nipkow: Joachimski and Matthes’ proof in Isabelle. Submitted.

• Watkins and Crary: Normalization for Concurrent LF in Twelf.