Slide 1

A Semantic Analysis of Structural Recursion

Andreas Abel

May 10, 1999

Slide 2

Example 1: Addition of ordinal numbers in SML

datatype Nat = …

datatype Ord = O | S of Ord | Lim of Nat –> Ord;

fun addord x O = x | addord x (S y′) = S (addord x y′) | addord x (Lim f) = Lim (fn z => addord x (f z))

Slide 3

Example 2: A pattern matching proof in LEGO

$[leRefl: {T|ClTy}{t|ClTm T}{v:Val T Ts0 t}vLe v v];
[[S,T:ClTy][t:ClTm T][v:Val T Ts0 t][s:ClTm S]
[w:Val S Ts0 s][R:Ty one][r:ClTm (UnfoldRec R)][x:ClV r]
   leRefl vUnit ==> leUnit
|| leRefl (vInl S v) ==> leInl S S (leRefl v)
|| leRefl (vInr S v) ==> leInr S S (leRefl v)
|| leRefl (vPair v w) ==> lePair (leRefl v) (leRefl w)
|| leRefl (vFold R x) ==> leFoldl R (leFoldr R (leRefl x))
];

Slide 4 Goal: From structural recursiveness …

∀v. (∀w < v. f(w) ⇓) → f(v) ⇓

... infer termination

∀v. f(v) ⇓

Outline:

1. Def. of the foetus system: types σ ∈ Ty(X⃗), terms t ∈ Tm^{σ}[Γ]

2. Def. of the evaluation strategy: syntactic values v ∈ Val^{σ}, closures ⟨t; e⟩ ∈ Cl^{σ}, op. sem. ⇓⊆ Cl^{σ} × Val^{σ}

3. Def. of the semantics: “good” values v ∈ [[σ]]

4. Def. of the structural ordering <_{σ,τ} ⊆ [[σ]] × [[τ]]

5. Proof of the wellfoundedness [[σ]] w.r.t. <

6. Def. of the good terms TM^{σ}[Γ]

7. Proof of the normalization: ∀t ∈ TM.⟨t; e⟩ ⇓ Slide 5

The foetus system

Type  Terms / Values Explanation
(Unit) 1  ()  unit set
(Var) X, Y, Z, … –  type variables
(Sum) σ + τ  inl, inr, case  disjoint sum
(Prod) σ × τ  (–,–), fst, snd  product
(Arr) σ → τ(X⃗)  λ, rec, – – (app) function space
(Rec) Rec X.σ(X) fold, unfold  recursive (fixed-point) type

σ(Rec X.σ(X)) \underrightarrow{fold} \overleftarrow{unfold} Rec X.σ(X)

Slide 6

Example 3: Recursor for Nat in foetus

Nat ≡ Rec X. 1 + X

O ≡ fold(inl())
S(v) ≡ fold(inr(v))

R^{σ} ≡ rec R^{σ→(Nat→σ→σ)→Nat→σ}. λf_{O}^{σ}. λf_{S}^{Nat→σ→σ}. λn^{Nat}.

case(unfold(n), 1. f_{O},

n^{′Nat}. f_{S} n′ (R f_{O} f_{S} n′))

Slide 7

Example 4: addord in foetus

Ord ≡ Rec X.(1 + X) + (Nat → X)
O ≡ fold(inl(inl()))
S(v) ≡ fold(inl(inr(v)))
Lim(f) ≡ fold(inr(f))
addOrd ≡ rec addOrd^{Ord→Ord→Ord}. λx^{Ord}. λy^{Ord}. case(unfold(y),
n^{1+Ord}. case(n,
1. x,
y^{′Ord}. S(addOrd x y′))
f^{Nat→Ord}. Lim(λz^{Nat}. addOrd x (f z)))

Slide 8

Operational semantics

Closures Cl^{σ}:

⟨t^{σ}; e⟩ t term, e environment f^{ρ→σ}@u^{ρ} f function value, u argument value

Evaluation relation ⇓^{σ}⊆ Cl^{σ} × Val^{σ}:

• big step

• call-by-value

• fixed evaluation strategy Slide 9

Semantics

Let V⃗ ⊆ Valτ⃗. Define [[σ(X⃗)]]V⃗ inductively:

(Unit) [[1]] := {()} (Var) [[X_{n}]]V⃗ := V_{n} (Sum) [[(σ + τ)(X⃗)]]V⃗ := {inl(v) : v ∈ [[σ(X⃗)]]V⃗ } ∪ {inr(v) : v ∈ [[τ(X⃗)]]V⃗ } (Arr) [[σ → τ(X⃗)]]V⃗ := {f ∈ Val^{σ→τ(τ⃗)} : ∀u ∈ [[σ]]. ∃v ∈ [[τ(X⃗)]]V⃗ .

f@u ⇓ v}

(Rec) [[Rec Y.σ(X⃗, Y)]]V⃗ := lfp F, where we define F as

F : P (Val^{Rec Y.σ(τ⃗,Y)}) → P (Val^{Rec Y.σ(τ⃗,Y)})
W ↦ fold ([[σ(X⃗, Y)]]_{V⃗ ,W} )

Slide 10

Fixed-point

Let (U, ⊆) be a complete lattice, F : U → U an operator. The least fixed-point F = lfp F is characterized by:

(ispfp)  F(F) ⊆ F
(ismpfp)  ∀A ∈ U. F(A) ⊆ A → F ⊆ A

Monotonicity

∀σ(X). A ⊆ B → [[σ(X)]]_{A} ⊆ [[σ(X)]]_{B}

Proof: Induction on σ:

(Arr) Show: For all f ∈ [[σ → τ(X)]]_{A} and u ∈ [[σ]] there is a

v ∈ [[τ(X)]]_{B} satisfying f@u ⇓ v.
(Rec) Show: [[Rec Z.σ(X, Z)]]_{A} ⊆ [[Rec Z.σ(X, Z)]]_{B}.

Slide 11

Substitution

[[σ(X)]]_{[[τ]]} = [[σ(τ)]]

For V ⊆ [[τ]] we get

[[σ(X)]]_{V} ⊆ [[σ(τ)]]

Slide 12

Example 5: All numerals are good

Val^{Nat} = {(fold ∘ inr)^{n}(inl()) : n ∈ ℕ} =^{!} [[Nat]]

Show: Val^{Nat} is smallest fixed-point of

F : P (Val^{Nat}) → P (Val^{Nat})
F(W) := {fold(v) : v ∈ [[1 + X]]_{W} }
= {fold(inl()), fold(inr(v)) : v ∈ W }

We must only show (ismpfp):

(i)  ⋃_{n∈ℕ} F^{n}(∅) ⊆ W
(ii)  Val^{Nat} ⊆ ⋃_{n∈ℕ} F^{n}(∅)

Slide 13

Structural ordering

Idea: Values are trees, “<” is subtree relation. Definition of <_{σ,τ} , ≤_{σ,τ} ⊆ [[σ]] × [[τ]]:

(lerefl) v ≤_{σ,σ} v  (lelt) {w <_{σ,τ} v \atop w ≤_{σ,τ} v}
(ltinl) {w ≤_{ρ,σ} v \atop w <_{ρ,σ+τ} inl(v)}  (ltinr) {w ≤_{ρ,τ} v \atop w <_{ρ,σ+τ} inr(v)}
(ltarr) {∃v ∈ CoDom(f).w <_{ρ,τ} v \atop w <_{ρ,σ→τ} f} (learr) {∃v ∈ CoDom(f).w ≤_{ρ,τ} v \atop w ≤_{ρ,σ→τ} f}

(ltfold)

w <_{σ,τ(Rec X.τ(X))} v
w <_{σ,Rec X.τ(X)} fold(v)

(lefold)

w ≤_{σ,τ(Rec X.τ(X))} v
w ≤_{σ,Rec X.τ(X)} fold(v)

Slide 14

Wellfoundedness

Def. of the accessible set Acc^{σ} ⊆ [[σ]]:

(acc)  {∀τ, [[τ]] ∋ w < v. w ∈ Acc^{τ} \atop v ∈ Acc^{τ}}

All semantic values are accessible.

∀σ(X⃗), ρ⃗. [[σ(X⃗)]]_{Accρ⃗} ⊆ Acc^{σ(ρ⃗)}

Proof by induction on generation of σ.

(Arr) Let f ∈ [[σ → τ(X⃗)]]_{Accρ⃗}. By monotonicity f ∈ [[σ → τ(ρ⃗)]], and from the induction hypothesis CoDom(f) ⊆ [[τ(X⃗)]]_{Accρ⃗} ⊆ Acc^{τ(ρ⃗)} we infer f ∈ Acc^{σ→τ(ρ⃗)} (we need a small lemma). (Rec) Show [[Rec σ(X⃗, Y)]]_{Accρ⃗} ⊆ Acc^{Rec Y.σ(ρ⃗,Y)}. We use the induction

hypothesis [[σ(X⃗, Y)]]_{Accρ⃗,Acc^{Rec Y.σ(ρ⃗,Y )}} ⊆ Acc^{σ(ρ⃗,Rec Y.σ(ρ⃗,Y))} and the fixed-point properties.

Slide 15

Structural recursive terms

SR^{σ→τ} [Γ] := {rec g.t ∈ Tm^{σ→τ} [Γ] : ∀e ∈ [[Γ]], v ∈ [[σ]].

(∀[[σ]] ∋ w < v.⟨rec g.t; e⟩@w ⇓) → ⟨rec g.t; e⟩@v ⇓}

Induction principle for wellfounded sets:

(accind)  {∀v ∈ [[σ]]. (∀[[σ]] ∋ w < v. P (w)) → P (v) \atop ∀v ∈ Acc^{σ}. P (v)}

All structural recursive terms are good:

t ∈ SR^{σ→τ} [Γ], e ∈ [[Γ]] → ⟨t; e⟩ ∈ [[σ → τ]]

Slide 16

Example 6: addord is structural recursive

Recursive calls:

… S(addOrd x′ y) …

\overline{lerefl} ; v′ ≤ v′ ; \overline{ltinr} ; v′ < inr(v′)

\overline{lelt}

v′ ≤ inr(v′)

\overline{ltinl}

v′ < inl(inr(v′))

\overline{ltfold}

v′ < S(v′) ≡ fold(inl(inr(v′)))

… Lim(λz^{Nat}. addOrd (f z) y) …

\overline{lerefl} ; w ≤ w

∃I

∃v′ ∈ CoDom(f). w ≤ v′

\overline{learr}

w ≤ f

\overline{ltinr}

w < inr(f)

\overline{ltfold}

w < Lim(f) ≡ fold(inr(f))

Slide 17

Normalization

Define the good terms TM^{σ}[Γ] ⊂ Tm^{σ}[Γ] inductively in the same way as Tm with the exception

(REC)

t ∈ TM^{σ→τ} [Γ, g^{σ→τ}] rec g.t ∈ SR^{σ→τ} [Γ]
rec g.t ∈ TM^{σ→τ} [Γ]

Show normalization

∀σ, Γ, t ∈ TM^{σ}[Γ], e ∈ [[Γ]]. ⟨t; e⟩ ⇓

by induction on t using the operational sematics.

Slide 18

Extensions and open questions

• positive types (?)

• polymorphic types √

• dependent types

• coinductive types