Slide 1

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

Andreas Abel

ProgLog, Chalmers Göteborg, Sweden June 9, 2004

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

Slide 2

Twelf

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

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

• Higher-order abstract syntax

• Terms: abstraction, application, user-def. constants

• Terms considered upto βη-equality

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

• Types: dependent function, user-def. type family constants • Logic programming through proof search Slide 3

Simply Typed λ-Calculus (STL)

• Syntax.

r, s, t, u ::= x | λx.t | r s untyped terms
A, B, C ::= ∗ | A → B  simple types
Γ  ::= ⋄ | Γ, x:A  contexts

• Type assignment Γ ⊢ t : A.

\frac{(x:A) ∈ Γ}{Γ ⊢ x : A} of var
\frac{Γ, x:A ⊢ t : B}{Γ ⊢ λx.t : A → B} of lam    \frac{Γ ⊢ r : A → B  Γ ⊢ s : A}{Γ ⊢ r s : B} of app

• 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

Slide 4

Representation of Syntactic Objects in Twelf

• Representation of simple types.

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

• Representation of λ-terms.

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

• Representation of weak head reduction.

-->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

• Representation of typing relation: Think in natural deduction trees.

\begin{aligned}& x \\ A \end{aligned} ; \begin{matrix}· \\ · \\ · \end{matrix} ; B ; \overline{of lam} ; A → B  A → B  A ; \overline{of app} ; B

• Typing assumption is represented as hypothetical judgement.

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

Slide 7

Weak Head Reduction is Closed under Substitution

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

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

– Case (λx.t) s ⟶_{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 \\ & ⟶_{w} & [[u/y]s/x][u/y]t & = & [u/y][s/x]t. \end{aligned}

– Case r s ⟶_{w} r′ s with r ⟶_{w} r′. By ind. hyp., [u/y]r ⟶_{w} [u/y]r′. Hence,

\begin{aligned}[u/y](r s) & = & ([u/y]r) ([u/y]s) \\ & ⟶_{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 +P -P'.

• 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 (P y)) (appl P')
                <- subst_red U P P'.
%terminates P (subst_red _P _).

• 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.

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