Slide 1

Termination of Functions that Are Passed to Their Arguments

Andreas Abel Dept. of Comp. Sci., Chalmers

September 13, 2005 APPSEM II Workshop Frauenchiemsee, Bavaria

Work supported by: GKLI (DFG), TYPES, APPSEM-II and CoVer (SSF)

Slide 2

Quiz: Is eqList terminating on all total inputs?

data  MList m a  where
    Nil  :: MList m a
    Cons :: a -> m (MList m a) -> MList m a
eqList eqM eq Nil Nil = True
eqList eqM eq (Cons a mas) (Cons b mbs)
                      = eq a b
                        && eqM (eqList eqM eq) mas mbs
eqList eqM eq __= False

Slide 3

Answer: No!

• Counterexample:

data  Maybe a  where
    Nothing :: Maybe a
    Just    :: a -> Maybe a
l         = Cons "BLA" Nothing
eqM f __= f l l
loop      = eqList eqM (==) l l

• We see that loop reduces to itself.

eqList eqM eq (Cons a mas) (Cons b mbs)
                      = eq a b
                        && eqM (eqList eqM eq) mas mbs

Slide 4

Quiz Reloaded: Is eqList now terminating on all total inputs?

data  MList m a  where
 Nil  :: MList m a
 Cons :: a -> m (MList m a) -> MList m a
type Eq a = a -> a -> Bool
eqList :: (forall a. Eq a -> Eq (m a)) -> Eq a -> Eq (MList m a)
eqList eqM eq (Cons a mas) (Cons b mbs)
                   = eq a b
                     && eqM (eqList eqM eq) mas mbs
eqList ...

Slide 5

Termination

• Question: Will the run of a program eventually halt?

• Undecidable for Turing-complete programming languages (Halteproblem).

• No termination checker can give a definitive answer for all programs.

• Problem still interesting for:

– optimization and program specialization

– total correctness of programs

– theorem proving

Slide 6

Termination for theorem proving

• Inductive theorem provers: e.g., Agda, Coq, Epigram, Twelf.

• Some proofs are tree-shaped deriviations, e.g., proof that [a, 0] = [b, 0].

{a = b  {0 = 0  [ ] = [ ] \atop (0 :: [ ]) = (0 :: [ ])} \atop a :: (0 :: [ ]) = b :: (0 :: [ ])}

• Some proofs are recursive programs, manipulating derivations.

• E.g., proof of (l_{1} = l_{2}) → (l_{2} = l_{3}) → (l_{1} = l_{3}).

• Only terminating programs denote valid proofs.

• E.g., program let trans d_{1} d_{2} = trans d_{1} d_{2} has to be rejected.

Slide 7

Termination of Functions Over Inductive Types

• For termination, only structure of trees is interesting.

• Structure of these trees can be represented by inductive types.

• More inductive types:

– lists

– binary trees

– natural numbers

– tree ordinals

Slide 8

Sized Inductive Types

• If T is an inductive type, let T^{α} denote the set of its elements with at most α constructors.

• E.g., List^{α} Int contains integer lists of length < α.

• List^{ω} Int is the type of all integer lists.

• In general, T^{∞} denotes the full type T.

• Sized list constructors:

nil ∈ List^{α+1} Int
cons ∈ Int → List^{α} Int → List^{α+1} Int

Slide 9

A recursion principle from transfinite induction

• Rule for transfinite induction:

\frac{P (0) P (α) → P (α + 1) (∀α < λ. P (α)) → P (λ)}{P (β)}

• Recursive programs via fixed-point combinator fix f = f (fix f).

• Instance P (α) = (fix f ∈ A^{α}):

• Use transfinite induction to define a recursive program:

\frac{fix f ∈ A^{0}  f ∈ A^{α} → A^{α+1}  (∀α < λ. fix f ∈ A^{α}) → fix f ∈ A^{λ}}{fix f ∈ A^{β}}

Slide 10

Handling base and limit case

• Recursion principle:

\frac{fix f ∈ A^{0} f ∈ A^{α} → A^{α+1} (fix f ∈ ⋂_{α<λ} A^{α}) → fix f ∈ A^{λ}}{fix f ∈ A^{β}}

• Restrict admissible types A^{α} such that – fix f ∈ A^{0} is trivial, e.g., A^{α} = T^{α} → C,

– (⋂_{α<λ} A^{α}) ⊆ A^{λ}.

• Specialized rule

\frac{∀α. f ∈ A^{α} → A^{α+1}}{fix f ∈ A^{β}} A^{α} admissible

Slide 11

Type-Based Termination

• When termination checking a function clause

\begin{matrix}f : A^{∞} \\ f p_{1} … p_{n} = t(f), \end{matrix}

• assume f to be of type A^{α} on the right hand side,

• assume f of type A^{α+1} on the left hand side,

• check well-typedness.

• For details and soundness, see draft of my thesis.

          http://www.tcs.ifi.lmu.de/~abel/diss/

Slide 12

Sized Monadic Lists

In context α : ord, M : ∗ →^{+} ∗, A : ∗ we have

MList^{α} M A : ∗
nil  : MList^{α+1} M A
cons  : A → M (MList^{α} M A) → MList^{α+1} M A

Slide 13

Solving the Quiz

• With Eq A = A → A → Bool we can type monadic list equality as follows:

eqMList : ∀M. (∀A. Eq A → Eq (M A)) → ∀A. Eq A → Eq (MList^{∞}M A)

\overbrace{eqMList eqM eq}^{Eq (MList^{α+1} M A)} \overbrace{(cons a mas)}^{MList^{α+1} M A} (cons b mbs) = eq a b and

eqM \overbrace{(eqMList eqM eq)}^{Eq (MList^{α} M A)}
Eq M (MList^{α} M A)

M (MList^{α} M A) \overbrace{mas}

mbs

• A bit suprisingly, the quiz can be answered affirmatively.

Slide 14

Related works on type-based termination

• Hughes, Pareto, Sabry (POPL 1996)

Proving the correctness of reactive systems using sized types

• Amadio and Coupet-Grimal (FoSSaCS 1998)

Analysis of a guard condition in type theory

• Xi (LICS 2001), Prg. termination verification with dep. types

• Chin, Khoo (HOSC 2001), Calculating sized types

• Barthe, Frade, Giménez, Pinto, Uustalu (MSCS 2004) Type-based termination of recursive definitions

• Blanqui (RTA 2004), A type-based termination criterion for dependently-typed higher-order rewrite systems

• Barthe et. al. (TLCA 2005): Inferring sized types

• Buchholz (2003), Recursion on non-wellfounded trees Slide 15

Acknowledgements

• Technical discussions on my thesis:

Klaus Aehlig Thorsten Altenkirch Martin Hofmann John Hughes Ralph Matthes Thomas Streicher Tarmo Uustalu

• Stipends GKLI CoVer

• Colleagues at Munich and Chalmers for support