Slide 1

A Predicative Analysis of Structural Recursion

Andreas Abel

November 19, 1999

• The termination checker foetus

• Soundness of structural recursion by an impredicative semantic analysis

• A predicative semantic analysis

Slide 2

Motivation (1): Division by 2

half 0 = 0 half 1 = 0 half n+2 = (half n)+1

half’ = R^{N} (λx^{B}. 0) (λx^{N} λf^{B)N} . R^{B} (f true) (1 + (f false))) half = λn^{N} . half’ n false Slide 3

Motivation (2): Pattern matching in LEGO

[leRefl: {...}{v:...}vLe v v];
[...
    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

Structural Recursion

∀ w < v. f(w)⟩ } f(v)⟩

Example: Addition of Ordinal Numbers

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:Nat => addord x (f z))

Slide 5

Lexicographic Ordering

Example: Ackermann Function

fun ack O y = S y | ack (S x) O = ack x (S O) | ack (S x) (S y) = ack x (ack (S x) y)

Slide 6

Mutual Recursive Functions

Example: List Flattening

fun flat [] = []

| flat (l::ls) = aux l ls and aux [] ls = flat ls

| aux (x::xs) ls = x :: aux xs ls;

[figure: flat; ( ^{<} ); ^{( \begin{matrix}< \\ < \end{matrix} )}; aux; ( \begin{matrix}< & ? \\ ? & ≤ \end{matrix} ); _{( _{?  ≤} )}]

Slide 7

Soundness of structural recursion

f(u_{0}) ⇝ f(u_{1}) ⇝ f(u_{2}) ⇝ …
u_{0} > u_{1} > u_{2} > …

• Define types σ, terms, values Val^{σ}

• Define semantics [[σ]] ⊆ Val^{σ}

• Define ordering < on [[σ]]

• Show wellfoundedness of [[σ]] w.r.t. <

Slide 8

The foetus system

Type  Terms / Values Explanation
(Var) X, Y, Z, … – type variables
(Sum) Σ(σ_{1}, …, σ_{n} ) in_{j}, case  finite disjoint sum
(Prod) Π(σ_{1}, …, σ_{n} ) (–,…,–), pi_{j}  finite product
(Arr) σ ) τ(X⃗)  λ, rec, – – (app) function space
(Mu) μ X.σ(X)  fold, unfold  inductive type

σ(μ X.σ) fold ; −) (− ; unfold μ X.σ(X)

Slide 9

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 10

Semantics

Let V⃗ ⊆ Valτ⃗. Define [[σ(X⃗)]](V⃗) inductively: (Var) [[X_{i}]](V⃗) := V_{i}

(Sum) [[Σσ⃗]](V⃗) := ⋃_{j=1}^{n} {in_{j}(v) : v ∈ [[σ_{j}]](V⃗)}
(Prod) [[Πσ⃗]](V⃗) := {(v⃗) : v_{i} ∈ [[σ_{i}]](V⃗)}
(Arr) [[σ ) τ(X⃗)]](V⃗) := {f ∈ Val^{σ)τ(τ⃗)} : ∀u ∈ [[σ]].

∃v ∈ [[τ(X⃗)]](V⃗). f@u ⟩ v}

(Mu) [[μY. σ(X⃗, Y)]](V⃗) smallest set closed under

{v ∈ [[σ]](V⃗, [[μY. σ]](V⃗)) \atop fold(v) ∈ [[μY. σ]](V⃗)} (using Knaster-Tarski)

Slide 11

Example: Lists

[[\underbrace{μY. 1 + X × Y}_{List (X)}]](\{a, b, c\}) ⊆ [[List(X)]](Val^{τ})

[[List(X)]]([[\underbrace{μX. 1 + X}_{Nat}]]) = [[List(Nat)]]

Slide 12

Structural Ordering

Define <,≤ ⊆ [[σ]] × [[τ]]:

• v ≤ in_{j}(v)

• v_{i} ≤ (v⃗)

• f(v) ≤ f

• v < fold(v)

• (reflexive) transitive closure Slide 13

Wellfoundedness

Define Acc^{σ} ⊆ [[σ]] inductively:

{∀w < v. w ∈ Acc^{τ} \atop v ∈ Acc^{σ}}

Theorem. [[σ(X_{1}, …, X_{n} )]](Acc^{τ_{1}} , …Acc^{τ_{n}} ) ⊆ Acc^{σ(τ_{1} ,... ,τ_{n} )} Proof by induction on σ.

Slide 14 Lemma (acc^{−1}).

{v ∈ Acc^{σ} w < v \atop w ∈ Acc^{τ}}

Lemma (Destructors for Acc).

in_{j}(v) ∈ Acc^{Σσ⃗}

v ∈ Acc^{σ_{j}}

{(v⃗) ∈ Acc^{Πσ⃗} \atop v_{i} ∈ Acc^{σ_{i}}}

f ∈ Acc^{σ)τ} f@u ⟩ v ; v ∈ Acc^{τ} fold(v) ∈ Acc^{μX.σ}

v ∈ Acc^{σ(μX.σ)}

Proof by (acc^{−1}).

Slide 15 Lemma.

{v ∈ Acc^{τ} w ≤ v \atop w ∈ Acc^{σ}}

Proof by induction on w ≤ v using destructor property. Lemma.

v ∈ Acc^{σ_{j}}
in_{j}(v) ∈ Acc^{Σσ⃗}

v_{i} ∈ Acc^{σ_{i}} for all i
(v⃗) ∈ Acc^{Πσ⃗}

f ∈ [[σ) τ]] ∀u ∈ [[σ]]. f@u ⟩ v ∈ Acc^{τ} ; f ∈ Acc^{σ)τ} v ∈ Acc^{σ(μX.σ)}

fold(v) ∈ Acc^{μX.σ}

Proof: Show ∀w < [−]. w ∈ Acc by case analysis on w < [−].

Slide 16

Predicative semantics construction

Avoid Knaster-Tarski, use only strictly positive inductive definitions on the meta-level. For σ(X⃗), τ⃗ define “has urelement”-relations U_{i}^{σ} ⊆ Val^{σ(τ⃗)} × Val^{τ_{i}}

with properties \begin{matrix}(I) & {v ∈ [[σ]](V⃗) v U_{i}^{σ} u \atop u ∈ V_{i}} \\ (II) & {v ∈ [[σ]](Valτ⃗) \atop v ∈ [[σ]](U⃗^{σ} (v))} \end{matrix}

Proposition.

v ∈ [[σ]](V⃗) {} v ∈ [[σ]](Valτ⃗) & U⃗^{σ} (v) ⊆ V⃗

Slide 17 Strictly positive definition of [[μX. σ]]:

{v ∈ [[σ]](V⃗, Val^{μX.σ(τ⃗)} ) U_{n+1}^{σ} (v) ⊆ [[μX. σ]](V⃗) \atop fold(v) ∈ [[μX. σ]](V⃗)}

Task. By induction on σ • Define [[σ]] and U_{i}^{σ}.

• Verify monotonicity of [[σ]].

• Verify properties (I) and (II) of U_{i}^{σ}.

Slide 18

The U-relation for Lists

List(X) = μY. 1 + X × Y U ⊆ Val^{List (τ)} × Val^{τ}

fold(in_{2}(v, vs)) U v {vs U u \atop fold(in_{2}(v, vs)) U u}

Slide 19

Extensions and open questions

• positive types (?)

• polymorphic types √

• coinductive types

• dependent types

Soundness of foetus

• define structural recursion syntactically

• show syntactically s.r. } semantically s.r.

Slide 20

Resources

• A. Abel, foetus – Termination Checker for Simple Functional Programs

• A. Abel, A Semantic Analysis of Structural Recursion

• A. Abel, T. Altenkirch, A Predicative Strong Normalisation Proof for a λ-calculus with Interleaving Inductive Types

• in preparation: A. Abel, T. Altenkirch, A Predicative Analysis of Structural Recursion