Slide 1

Eine semantische Analyse struktureller Rekursion

Andreas Abel

26. Februar 1999

Slide 2

Beispiel 1: Addition von Ordinalzahlen in SML

datatype Nat = …

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

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

Slide 3

Beispiel 2: Beweis mit Pattern Matching 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 Ziel: Zeige aus struktureller Rekursivität …

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

... Termination

∀v. f(v) ⇓

Vorgehen:

1. Def. des Systems foetus: Typen σ ∈ Ty(X⃗), Terme t ∈ Tm^{σ}[Γ]

2. Def. der Auswertungsstrategie: syntakt. Werte v ∈ Val^{σ}, Hüllen ⟨t; e⟩ ∈ Cl^{σ}, op. Sem. ⇓⊆ Cl^{σ} × Val^{σ}

3. Def. der Semantik: “gute” Werte v ∈ [[σ]]

4. Def. der strukturellen Ordnung <_{σ,τ} ⊆ [[σ]] × [[τ]]

5. Beweis der Wohlfundiertheit von [[σ]] bzgl. <

6. Def. der guten Terme TM^{σ}[Γ]

7. Bew. der Normalisierung: ∀t ∈ TM.⟨t; e⟩ ⇓ Slide 5

Typen

Strikt positive rekursive Typen.

(Unit) 1 ∈ Ty(∅)

(Var)

X⃗, X ⊂ TyVars X ∈ Ty(X⃗, X)

(Weak) {σ ∈ Ty(X⃗) X ∉ X⃗ \atop σ ∈ Ty(X⃗, X)}

(Sum) {σ, τ ∈ Ty(X⃗) \atop σ + τ ∈ Ty(X⃗)}
(Arr) {σ ∈ Ty(∅) τ ∈ Ty(X⃗) \atop σ → τ ∈ Ty(X⃗)} (Rec) {σ ∈ Ty(X⃗, X) \atop Rec X.σ ∈ Ty(X⃗)}

Notation: σ(X⃗)

Slide 6

(unit) () ∈ Tm^{1}[]

(var)

Γ ∈ Cxt x ∉ Γ x ∈ Tm^{σ}[Γ, x^{σ}] (weak)

{t ∈ Tm^{σ}[Γ] x ∉ Γ \atop t ∈ Tm^{σ}[Γ, x^{τ}]}

(inl) t ∈ Tm^{σ}[Γ] τ ∈ Ty inl(t) ∈ Tm^{σ+τ} [Γ] (inr)

t ∈ Tm^{τ} [Γ] σ ∈ Ty
inr(t) ∈ Tm^{σ+τ} [Γ]

(case) t ∈ Tm^{σ+τ} [Γ] l ∈ Tm^{ρ}[Γ, x^{σ}] r ∈ Tm^{ρ}[Γ, y^{τ}]

case(t, x^{σ}.l, y^{τ} .r) ∈ Tm^{ρ}[Γ]

(lam)

{t ∈ Tm^{τ} [Γ, x^{σ}] \atop λx^{σ}.t ∈ Tm^{σ→τ} [Γ]}

(rec)

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

(app) t ∈ Tm^{σ→τ} [Γ] s ∈ Tm^{σ}[Γ]

t s ∈ Tm^{τ} [Γ]

(fold) t ∈ Tm^{σ(Rec X.σ(X))}[Γ] fold(t) ∈ Tm^{Rec X.σ(X)}[Γ] (unfold)

t ∈ Tm^{Rec X.σ(X)}[Γ]

unfold(t) ∈ Tm^{σ(Rec X.σ(X))}[Γ] Slide 7

Beispiel 3: Rekursor für 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 8

Beispiel 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(x),

n^{1+Ord}. case(n,
1. y,

x^{′Ord}. S(addOrd x′ y))

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

Slide 9

Syntaktische Werte und Hüllen

(vlam) t ∈ Tm^{τ} [Γ, x^{σ}] e ∈ Val(Γ)

⟨λx^{σ}.t; e⟩ ∈ Val^{σ→τ} (vunit)

() ∈ Val^{1}

(vrec) t ∈ Tm^{σ→τ} [Γ, g^{σ→τ}] e ∈ Val(Γ)

⟨rec g^{σ→τ} .t; e⟩ ∈ Val^{σ→τ}

(vinl) v ∈ Val^{σ} τ ∈ Ty inl(v) ∈ Val^{σ+τ} (vinr)

v ∈ Val^{τ} σ ∈ Ty
inr(v) ∈ Val^{σ+τ}

(vfold) v ∈ Val^{σ(Rec X.σ(X))} fold(v) ∈ Val^{Rec X.σ(X)}

Val(Γ) := {x_{1} =v_{1}, …, x_{n} =v_{n} : v_{i} ∈ Val^{σ_{i}}}
Cl^{τ} := {⟨t; e⟩ : Γ ∈ Cxt, t ∈ Tm^{τ} [Γ], e ∈ Val(Γ)}
∪ {f@u : f ∈ Val^{σ→τ} , u ∈ Val^{σ}}

Slide 10

Operationale Semantik

Auswertungsrelation ⇓^{σ}⊆ Cl^{σ} × Val^{σ}.

• big step

• call-by-value

• feste Auswertungsstrategie

(oplam) ⟨λx.t; e⟩ ⇓ ⟨λx.t; e⟩  (oprec) ⟨rec g.t; e⟩ ⇓ ⟨rec g.t; e⟩
(opapp) {⟨t; e⟩ ⇓ f ⟨s; e⟩ ⇓ u f@u ⇓ v \atop ⟨t s; e⟩ ⇓ v}
(opappvl) {⟨t; e, x = u⟩ ⇓ v \atop ⟨λx.t; e⟩@u ⇓ v}  (opappvr) {⟨t; e, g = rec g.t⟩ ⇓ f f@u ⇓ v \atop ⟨rec g.t; e⟩@u ⇓ v}

Slide 11

Semantik

(Unit) [[1]] := {()} (Var) [[X_{n}]]V⃗ := V_{n}

(Weak) [[σ(X⃗, Y)]]_{V⃗ ,W} := [[σ(X⃗)]]V⃗ (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 12

Fixpunkt

Sei (U, ⊆) vollständiger Verband, F : U → U Operator. Der kleinste Fixpunkt F = lfp F ist charakterisiert durch:

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

Monotonie

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

Beweis: Induktion über σ:

(Arr) Zeige: Für alle f ∈ [[σ → τ(X)]]_{A} und u ∈ [[σ]] gibt es ein

v ∈ [[τ(X)]]_{B} mit f@u ⇓ v.

(Rec) Zeige: [[Rec Z.σ(X, Z)]] ⊆ [[Rec Z.σ(X, Z)]]_{B}.

Slide 13

Substitution

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

Für V ⊆ [[τ]] gilt somit

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

Slide 14

Beispiel 5: Alle Numerale sind gut

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

Zeige: Val^{Nat} is kleinster Fixpunkt von

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

Nur zu zeigen: (ismpfp). Dazu

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

Slide 15

Strukturelle Ordung

Idee: Werte sind Bäume, “<” ist Teilbaum-Relation.

Definition von <_{σ,τ} , ≤_{σ,τ}:⊆ [[σ]] × [[τ]]

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

Wohlfundiertheit

Def. der erreichbaren Teilmenge Acc^{σ} ⊆ [[σ]]:

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

Alle semantischen Werte sind erreichbar.

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

Beweis durch Induktion über den Aufbau des Typs σ.

(Arr) Sei f ∈ [[σ → τ(X⃗)]]_{Accρ⃗}. Monotonie liefert f ∈ [[σ → τ(ρ⃗)]], nach Induktionsvoraussetzung CoDom(f) ⊆ [[τ(X⃗)]]_{Accρ⃗} ⊆ Acc^{τ(ρ⃗)} folgt mit einem Hilfslemma f ∈ Acc^{σ→τ(ρ⃗)}.

(Rec) Zu zeigen [[Rec σ(X⃗, Y)]]_{Accρ⃗} ⊆ Acc^{Rec Y.σ(ρ⃗,Y)}. Wir nutzen die Ind.vor. [[σ(X⃗, Y)]]_{Accρ⃗,Acc^{Rec Y.σ(ρ⃗,Y )}} ⊆ Acc^{σ(ρ⃗,Rec Y.σ(ρ⃗,Y))} und die Fixpunkteigenschaften.

Slide 17

Strukturell rekursive Terme

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

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

Induktionsschema für wohlfundierte Mengen:

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

Damit sind strukturell rekursive Terme gut:

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

Slide 18

Beispiel 6: addord ist strukturell rekursiv

Rekursive Aufrufe:

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

Normalisierung

Definiere gute Terme TM^{σ}[Γ] ⊂ Tm^{σ}[Γ] induktiv wie Tm mit der Ausnahme

(REC)

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

Zeige Normalisierung

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

durch Induktion über t mit Hilfe der operationalen Semantik.

Slide 20

Erweiterungsmöglichkeiten und offene Fragen

• positive Typen (?)

• polymorphe Typen

• abhängige Typen

• Coinduktive Typen