Slide 1

Termination of Mutually Recursive Functions

Andreas Abel POP Seminar, CMU Computer Science May 26, 2000

1. Introduction

2. The foetus Project

3. Mutually Recursive Functions with One Argument

4. Mutually Recursive Functions with Several Arguments

Slide 2

Recursion over Inductive Types

• Functional programming languages and logical frameworks base upon λ-calculus enriched with inductive types. Examples: ML, LEGO

• Definition of functions/constants by recursion over inductive type possible.

• Standard means: recursor/elimination. Ensures totality.

Example: half’ = R^{N} (λx^{B}. 0) (λx^{N}λf^{B→N}. R^{B} (f true) (1 + (f false))) half = λn^{N}. half’ n false Drawback: Misses intuition, readability, usability.

Slide 3

Pattern Matching

• Alternative: “free recursive definitions”.

Example: half 0 = 0 half 1 = 0 half n+2 = (half n)+1 But: syntax permits non-total functions ⟹ totality check required!

• LEGO allows to implement proofs by pattern matching, but fails to perform totality check ⟹ invalid proofs possible!

Slide 4

The foetus Project

1996 Munich Type Theory Implementation (T. Altenkirch) 1998 Implementation of termination checker foetus for a sublanguage of MuTTI

(A. Abel) 1999 Reimplementation of termination checker into Agda (C. Coquand,

Chalmers, Sweden) 1999 Verification I: Wellfoundedness of domains [AA99] 2000 Verification II: Single Recursive Functions [Abe00]

Verification III: Mutually Recursive Functions (in progress)

Slide 5

Wellfoundedness and Accessibility

Let S be a set and < a relation on S. The accessible part Acc_{>} ⊆ S is defined as the smallest set closed under

w ∈ Acc_{>} :⟺ ∀v < w. v ∈ Acc_{>}

Accessible part induction (wellfounded induction):

{∀w ∈ S. (∀v < w. P (v)) ⇒ P (w) \atop ∀w ∈ Acc_{>}. P (w)}

Wellfounded part WF ⊆ S:

w ∈ WF_{>} :⟺ ∄f : ℕ → S. f(0) = w ∧ ∀n ∈ ℕ. f(n) > f(n + 1)

Brouwer’s bar theorem (axiom of bar induction):

WF_{>} ⊆ Acc_{>}

(Classically provable.)

Slide 6

Single Recursive Function

• Assume a wellfounded domain (D, <), i.e., D = Acc_{>}.

• Provided that:

1. all statements (except the recursive calls) in f terminate

2. in each recursive call the argument v is smaller than the function input w we can define termination of function f at argument w ∈ D as:

{∀v < w. f@v ⇓ \atop f@w ⇓}

• Goal: ∀w ∈ D. f@w ⇓

• Proof by wellfounded induction.

Slide 7

Mutually Recursive Functions with a Single Argument

• Let F be a finite set of function symbols.

g ⪯ f :⟺ f ⟶ g  “f calls g”

• Straightforward extension of predicate “terminates at”:

f@w ⇓ :⟺ ∀g ⪯ f, v < w. g@v ⇓
F@w ⇓ :⟺ ∀f ∈ F. f@w ⇓

• Goal: ∀w ∈ D. F@w ⇓

• Proof by wellfounded induction.

• But: criterion to strict!

Slide 8

Call Graphs

• Sufficient: In each call cycle

f ⟶ g ⟶ … ⟶ f

the argument is decreased once.

• Functions and calls can be organized in a labelled directed graph:

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

• Indirect (combined) calls:

{f ⟶^{R} g \atop f ⟶^{R}^{+} g}  {f ⟶^{R}^{+} g  g ⟶^{S}^{+} h \atop f ⟶^{S⋆R}^{+} h}  \begin{aligned}⋆ & < & ≤ & ? \\ < & < & < & ? \\ ≤ & < & ≤ & ? \\ ? & ? & ? & ? \end{aligned}

Slide 9

Good Call Graphs

• Let C be a call graph.

C good :⟺ ∀f ∈ F. ∀f ⟶^{R_{1}} f_{1} ⟶^{R_{2}} … ⟶^{R_{n}} f_{n} ⟶^{R_{n+1}} f. ∏_{i=1}^{n+1} R_{i} = “<”

• Good call graphs have two properties:

Each cycle

f ⟶^{R⃗} f

1. contains only calls that are at least preserving:

∀i. R_{i} ∈ {<, ≤}

2. contains at least one decreasing call:

∃i. R_{i} = “<”

Slide 10

No Infinite Call Sequences

• Goal: All call sequences f(w) ⇝ g(v) ⇝ … terminate.

• Evaluation ordering ≪ on F × D must fulfill

(g, v) ≪ (f, w) ⇐ f \underrightarrow{?} g
∨ (f \underrightarrow{≤} g ∧ v ≤ w)
∨ (f \underrightarrow{<} g ∧ v < w)

• Theorem: For good call graphs the most general ordering ≪ is wellfounded:

W F_{≫} = F × D

• Proof: Consider an infinite call sequence. Since F is finite, one particular function symbol f must appear infinitly often. Goodness of the call graph implies an infinite descend on the argument of f. Contradiction!

Slide 11

Classical Termination Proof

• New (weaker) termination predicate:

f@w ⇓ :⟺ ∀(g, v) ≪ (f, w). g@v ⇓

• Goal: ∀f ∈ F, w ∈ D. f@w ⇓ .

• Proof by wellfounded induction, making use of the bar theorem.

• Question 1: Can we proof termination constructively without bar induction?

Slide 12

Alternative Goodness Characterization

• A call graph C is good if there is a bijective naming

f^{11}, …, f^{1m_{1}}, …, f^{n1} … f^{nm_{n}}

of the function symbols in F s.th.

f^{i_{1}j_{1}} \underrightarrow{?} f^{i_{2}j_{2}} ⇒ i_{1} > i_{2}
f^{i_{1}j_{1}} \underrightarrow{≤} f^{i_{2}j_{2}} ⇒ i_{1} > i_{2} ∨ (i_{1} = i_{2} ∧ j_{1} > j_{2})
f^{i_{1}j_{1}} \underrightarrow{<} f^{i_{2}j_{2}} ⇒ i_{1} ≥ i_{2}

• This characterization has been used, e.g., by Frank Pfenning and Carsten Schürmann for termination checking in the Twelf system [PS98].

• Question 2: Are the two criteria equivalent?

Slide 13

Ordering on Function Symbols

• Define two relations ≺, ⊲ on F by

g ≺ f :⟺ f ⟶ g ∧ g −̸→^{+} f
g ⊲ f :⟺ f \underrightarrow{≤} g

• Theorem: Both relations are wellfounded.

• Proof: In both cases the transitive closure is irreflexive. Since F is finite, this entails wellfoundedness.

f ≺^{+} f ⇒ f ⟶^{+} f ∧ f −̸→^{+} f
f ⊲^{+} f ⇒ f \underrightarrow{≤}^{+} f  (contradicts goodness)

• The modified lexicographic product ≺ ⊗′ ⊲ is wellfounded, too, and can be completed to a total ordering. Answer 2: yes!

g ≺⊗′ ⊲ f :⟺ g ≺ f ∨ (g ⪯ f ∧ g ⊲ f)

Slide 14

Wellfounded Evaluation Ordering

• Define relation ≪ on F × D:

(g, v) ≪ (f, w) :⟺ g ≺ f
∨ (g ⪯ f ∧ v < w
∨ (v ≤ w ∧ g ⊲ f))

• Theorem: ≪ is a wellfounded evaluation ordering.

• Proof: Wellfounded: ≪ is a modified lexicographic product of wellfounded relations. Evaluation ordering:

f \underrightarrow{?} g  ⇒ g ≺ f  (Goodness property 1)
f \underrightarrow{<} g ∧ v < w ⇒ g ⪯ f ∧ v < w
f \underrightarrow{≤} g ∧ v ≤ w ⇒ g ⪯ f ∧ v ≤ w ∧ g ⊲ f

• Now we can proof ∀w ∈ D, f ∈ F. f@w ⇓ by wellfounded induction. Answer 1: yes!

Slide 15

Towards Functions with Several Arguments

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 16

Call Graphs for Functions with Several Arguments

• Let F be a finite set of function symbols with arity mapping ar : F → ℕ • A call graph is a labelled directed multi-graph with edges

f ⟶^{σ,a} g

s.th.

σ : ar(g) → ar(f)  permutation of arguments
a : ar(g) → {<, ≤,?}  size change information

• A call graph is good iff

∀f ⟶^{σ,a}^{+} f. ∃k. σ = id ↾ k ∧ lex_{<}^{k}(a)

where we refer to k as number of relevant arguments and

lex_{<}^{k}(a) :⟺ ∃k′ < k. a(k′) = “<” ∧ ∀i < k′.a(i) = “≤”
lex_{=}^{k}(a) :⟺ ∀i < k. a(i) = “≤”
lex_{≤}^{k}(a) :⟺ lex_{<}^{k}(a) ∨ lex_{=}^{k}(a)

Slide 17

Complications

• Attributes “decreasing” (<) and “preserving” (≤) of a call are no longer global. The call f ⟶ g is decreasing for f and preserving for g.

[figure: f; ( \begin{matrix}< & · \\ · & ≤ \end{matrix} ); ^{( \begin{matrix}· & ≤ \\ < & · \end{matrix} )}; g; ( \begin{matrix}< & · \\ · & ≤ \end{matrix} ); _{( \begin{matrix}· & ≤ \\ < & · \end{matrix} )}]

• Two call cycles may have a different number of relevant arguments. Here k(g → f → g) = 1 and k(g → h → g) = 2.

\xymatrix{f \ar[r]_{( \begin{matrix}≤ & · \\ · & ? \end{matrix} )} & g \ar[l]_{( \begin{matrix}< & · \\ · & ? \end{matrix} )} \ar[r]^{( \begin{matrix}< & · \\ · & ≤ \end{matrix} )} & h \ar[l]^{( \begin{matrix}≤ & · \\ · & ≤ \end{matrix} )}}

Slide 18

Argument Trace

• Arguments are being permuted ⇒ we need an argument trace

τ_{f→g} : ar(g) → ar(f) for all f, g ∈ F

• Requirements: For each cycle h ⟶^{∗} f ⟶^{σ,a} g ⟶^{∗} h with k relevant arguments

τ_{h→h} = id ↾ k  (1)
τ_{f→h} = σ ∘ τ_{g→h} ↾ k  (2)

Slide 19 • Example: τ_{g→f} = id, not τ_{g→f} = (1 2).

\xymatrix{f \ar[r]^{^{( \begin{matrix}< & · & · \\ · & · & < \\ · & < & · \end{matrix} )} ^{( \begin{matrix}≤ & · & · \\ · & ≤ & · \\ · & · & ≤ \end{matrix} )}} & g \ar[l]^{_{( \begin{matrix}≤ & · & · \\ · & < & · \\ · & · & ? \end{matrix} )}}}

Slide 20

Call Classification

• We classify the calls as decreasing resp. (strictly) preserving by

(R ∈ {<, =, ≤}):

class_{R}^{h}(f ⟶^{σ,a} g) :⟺ ∀Z = h ⟶^{∗} f ⟶^{σ,a} g ⟶^{∗} h. lex_{R}^{k(Z)}(a ∘ τ_{g→h})

• Property 1. In each cycle each call is preserving

∀Z = h ⟶^{∗} f ⟶^{σ,a} g ⟶^{∗} h. class_{≤}^{h}(f ⟶^{σ,a} g)

• Classification of transitions:

f \underrightarrow{<} g :⟺ ∃h ≈ f. ∀f ⟶^{σ,a} g. class_{<}^{h}(f ⟶^{σ,a} g)
f \underrightarrow{≤} g :⟺ ∀h ≈ f. ∃f ⟶^{σ,a} g. class_{=}^{h}(f ⟶^{σ,a} g)
f \underrightarrow{?} g :⟺ g −̸→ f

h ≈ f is defined as h ⟶^{∗} f ⟶^{∗} h.

Slide 21

Evaluation Ordering

• We define g ≺ f as before and

g ⊲ f :⟺ f \underrightarrow{≤} g

• Theorem: Both relations are wellfounded.

• Define v <_{f→g}^{h} w as “v is smaller than w wrt. to h in a call from f to g”. This relation is wellfounded.

• Theorem: The relation ≪ defined by

(g, v) ≪ (f, w) :⟺ g ≺ f ∨ g ≈ f ∧ (∀h. v ≤_{f→g}^{h} w)
∧ ((∃h. v <_{f→g}^{h} w) ∨ g ⊲ f)

is a wellfounded evaluation ordering.

• Proof: ≪ is a lexicographic product of three wellfounded relations. The second of these is a multiset ordering of wellfounded relations indexed by h.

Slide 22

Further Extensions

Weaken the definition of good to allow:

• Multiset orderings.

• Cycles of higher order. Example:

  zip []      l = l
   |  (x::xs) l = x :: zip l xs;

References

[AA99] Andreas Abel and Thorsten Altenkirch. A predicative analysis of structural recursion. Submitted to the Journal of Functional Programming, December 1999.

[Abe00] Andreas Abel. Specification and verification of a formal system for structurally recursive functions. Submitted to TYPES’99, January 2000.

[PS98] Frank Pfenning and Carsten Schürmann. Twelf user’s guide. Technical report, Carnegie Mellon University, 1998.