Slide 1

Termination of Mutually Recursive Functions with Several Arguments by Lexicographic Orderings

Andreas Abel

April 6, 2000

Slide 2

Example

            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 3

Size Change Precategory L

• objects: function identifiers F

• morphisms: ⊔-semilattices of size change information

⋆ : L(g, h) × L(f, g) → L(f, h)

Interpretation [[−]]

L(f, g) ∋ A ↦ [[A]] ⊆ D_{g} × D_{f}

1. A ⊑ B ⇒ [[A]] ⊆ [[B]]

2. [[C ⋆ B]] ⊇ [[C]] ∘ [[B]]

Slide 4

Call Graph C ⊆ L

C : ((f, g) ∈ F × F) → P(L(f, g))

f ⟶^{A} g  iff  A ∈ C(f, g)

Completion C^{+}

C complete :⟺ closed under composition

{A ∈ C(f, g) B ∈ C(g, h) \atop B ⋆ A ∈ C(f, h)}

C^{+} :⟺ completion of C
f ⟶^{A}^{+} g  iff  A ∈ C^{+}(f, g)

Slide 5

Termination ⇓

{∀g, f ⟶^{A} g, v ∈ D_{g}, w ∈ D_{f}. v [[A]] w ⇒ g@v ⇓ \atop f@w ⇓}

f ⇓ :⟺ ∀v ∈ D_{f}. f@v ⇓

Evaluation Ordering ≪

f ⟶^{A} g ∧ v [[A]] w ⇒ (g, v) ≪ (f, w)

Prop. If a wellfounded evaluation ordering exists for C, then all functions f ∈ F terminate.

Slide 6

Functions with a Single Argument

                                 [figure: f; ?; g; ≤; h; <]

Slide 7

Single Argument Lattice 𝕃

Consists of the three elements < ⊑ ≤ ⊑ ?.

\begin{aligned}⋆ & < & ≤ & ? \\ < & < & < & ? \\ ≤ & < & ≤ & ? \\ ? & ? & ? & ? \end{aligned}

Interpretation in Wellordered Domain (D, <)

v [[<]] w :⟺ v < w
v [[≤]] w :⟺ v = w or v < w
v [[?]] w :⟺ True

Slide 8

Good Call Graph

f ⟶^{R}^{+} f implies R = <

Lemma.

f ⟶^{R_{0}} f_{1} ⟶^{R_{1}} … ⟶^{R_{n−1}} f_{n} ⟶^{R_{n}} f implies R_{i} ⊑ ≤ for all i

Lemma.

f ⟶^{R_{0}} f_{1} ⟶^{R_{1}} … ⟶^{R_{n−1}} f_{n} ⟶^{R_{n}} f implies R_{i} = < for some i

Slide 9

Function Orderings

g ⊲ h :⟺ h \underrightarrow{≤} g
g ⪯ h :⟺ h ⟶ g
g ≈ h :⟺ g ⪯^{+} h ∧ h ⪯^{+} g
g ≺ h :⟺ g ⪯\≈ h

Theorem. ⊲^{+} and ≺^{+} are irreflexive. Corollary. For a finite F ⊲ and ≺ are wellfounded.

Slide 10

Evaluation Ordering ≪

(g, v) ≪ (f, w) :⟺ g ≺ f
∨ (g ≈ f ∧ v < w
∨ (v = w ∧ g ⊲ f))

Prop. ≪ is a wellfounded evaluation ordering.

Slide 11

Functions with Several Arguments

ar : F → ℕ

Call Matrices Precategory L

Size change information (σ, a) ∈ L(f, g)

σ : ar(g) → ar(f)
a : ar(g) → 𝕃
((σ′, a′) ⋆ (σ, a))(i) := (σ(σ′(i)), a′_{i} ⋆_{𝕃} a_{σ′(i)})

Interpretation in D_{f} := D^{ar(f)}

Let (σ, a) ∈ L(f, g).

v [[σ, a]] w :⟺ v [[a]] w ∘ σ :⟺ ∀i ∈ ar(g). v_{i} [[a_{i}]] w_{σ(i)}

Slide 12

Good Call Graph

For each f ∈ F a permutation

π_{f} : ar(f) → ar(f)

s.th. for each cycle Z := f ⟶^{(σ,a)}^{+} f there is a 1 ≤ k(Z) ≤ ar(f) fulfilling

σ ∘ π_{f} ↾ k(Z) = π_{f} ↾ k(Z)  (1)
a ∘ π_{f} ↾ k(Z) = <^{k(Z)}  (2)

where

<^{k} := (≤, …, ≤, <) ∈ 𝕃^{k}
≤^{k} := (≤, …, ≤, ≤) ∈ 𝕃^{k}

Slide 13

Function Ordering ⊲

g ⊲ f :⟺ ∃f ⟶^{(σ,a)} g. ∀Z. Z = h ⟶^{∗} f ⟶^{(σ,a)} g ⟶^{τ}^{∗} h

⇒ a ∘ τ ∘ π_{h} ↾ k(Z) = ≤^{k(Z)}

Lemma. The relation ⊲^{+}⊆ F × F is irreflexive.

Let f ⟶^{σ} g.

v <_{h} w :⟺ ∀Z = h ⟶^{∗} f ⟶^{σ} g ⟶^{τ}^{∗} f.
v ∘ τ ∘ π_{h} ↾ k(Z) [[<^{k(Z)}]] w ∘ σ ∘ τ ∘ π_{h} ↾ k(Z)
v ≤_{h} w :⟺ ∀Z = h ⟶^{∗} f ⟶^{σ} g ⟶^{τ}^{∗} f.
v ∘ τ ∘ π_{h} ↾ k(Z) [[≤^{k(Z)}]] w ∘ σ ∘ τ ∘ π_{h} ↾ k(Z)

Evaluation Ordering ≪

Slide 14 \begin{matrix}(g, v) ≪ (f, w) :⟺ g ≺ f ∨ (g ≈ f ∧ ∃f ⟶^{(σ,a)} g. \\ ∀h ≈ f. v ≤_{h} w ∧ (∃h ≈ f. v <_{h} w ∨ g ⊲ f)) \end{matrix}

Theorem. ≪ is a wellfounded evaluation ordering.