Slide 1

Type-Based Termination and Productivity Checking

Andreas Abel Dept. of Comp. Sci., Chalmers

TCS Oberseminar, LMU Munich July 19, 2005

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

Slide 2

Short CV

1999 Diploma from this university Major in computer science, minor in mathematics Diplomathesis: termination checker foetus for structural recursion

1999-2003 Ph.D. student at this chair in the PhD program Logic in Computer Science:

2000/01 Visit to Frank Pfenning at Carnegie-Mellon, Pittsburgh, USA: Development of a tutorial proof checker (Tutch) for constructive logics Slide 3

Short CV (cont.)

2004-today Postdoc at Chalmers, Göteborg, Sweden Verifying Haskell programs using First-Order Logic and Type Theory

Oct 2005(?!) Ph.D. from this university A Polymorphic Lambda-Calculus with Sized Higher-Order Types

Slide 4

Talk outline

1. Introduction to termination

2. Inductive types and a recursion principle

3. F_{ω}—a type system for termination

4. Examples: the type system at work

5. Productivity via coinduction

6. Achieved results and future work 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, LEGO, 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 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

Inductive types

• Semantical perspective: types are value sets.

• Example: integer lists – [ ] is an int. list

– if x is an int. and xs an int. list, then x :: xs is an int. list • Least solution of type equation

List Int = {[ ]} ∪ {x :: xs | x ∈ Int and xs ∈ List Int} • Abstracting away the names

List Int = 1 + Int ×List Int

• Definable as least fixed-point μ^{∞}F of some type operator F List Int := μ^{∞}(λX. 1 + Int ×X)

Slide 9

Iterating to the least fixed point

μ^{0}F μ^{1}F μ^{2}F  μ^{ω}F μ^{ω+1}F  μ^{∞}F

Slide 10

Iterating to the least fixed point

• The least fixed point is reachable from below by ordinal iteration:

\begin{aligned}μ^{0}F & = & ∅ \\ μ^{α+1}F & = & F (μ^{α} F) \\ μ^{λ}F & = & ⋃_{α<λ} μ^{α}F \end{aligned}

• E.g., List^{α} Int := μ^{α}(λX. 1 + Int ×X) contains integer lists of length < α.

• List^{ω} Int is already the least fixed point.

• List constructors definable:

[ ] ∈ List^{α+1} Int
(::) ∈ Int → List^{α} Int → List^{α+1} Int

Slide 11

Recursive functions over inductive types

• E.g., we want to define list summation sum ∈ List^{ω} Int → Int.

• Recursive program:

sum [ ]  = 0
sum (x :: xs) = x + sum xs

• Via fixed-point combinator fix f = f (fix f).

sum = fix \underbrace{(λsum.λl. match l with nil ↦ 0 (x :: xs) ↦ x + sum xs)}_{f}

• How to prove that sum is well defined, i.e., terminating?

Slide 12

A recursion principle from transfinite induction

• Rule for transfinite induction:

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

• 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^{β}}

• For sum ∈ List^{ω} Int → Int, instantiate A^{α} = List^{α} Int → Int and β = ω.

Slide 13

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^{α} = μ^{α}F → C,

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

• Specialized rule

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

Slide 14

From semantics to syntax

• Recapitulation of semantic types we used:

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

sum ∈ List^{ω} Int → Int
nil ∈ List^{α+1} Int
(::) ∈ Int → List^{α} Int → List^{α+1} Int

• We only talk about ordinal variables (α, β), successor, and closure ordinal (in this case, ω)!

• We can turn these semantic rules into syntax without an ordinal notation system (e.g., Cantor normal form).

Slide 15

F_{ω}: a type system for termination

• A language with three levels:

– Terms (programs) which have types.

– Type constructors: a language to construct types.

– Kinds, the “types” of type constructor.

• Kinds:

κ ::= ∗  types A, B
| ord  ordinals a, b
| κ_{1} →^{p} κ_{2}  p-variant type constructors F, G

• Constructors can be covariant (p = +), contravariant (p = −), and non-varaint (p = ∘, “don’t know”).

Slide 16

F_{ω}: constructors

• Types and type constructors:

\begin{aligned}F, G & ::= & X | λX.F | F G | → | ∀_{κ} | μ^{a} \\ a, b & ::= & i | a + 1 | ∞ \end{aligned}

• Defined types:

\begin{aligned}∀X:κ.A & = & ∀_{κ}(λX.A) \\ 1 & = & ∀X:∗. X → X \\ A + B & = & ∀X:∗. (A → X) → (B → X) → X \\ A × B & = & ∀X:∗. (A → B → X) → X \end{aligned}

Slide 17

F_{ω}: sized inductive types

• Sized polymorphic lists and tree ordinals:

List : ord →^{+} ∗ →^{+} ∗
List := λa.λA. μ^{a} (λX. 1 + A × X)
Ord : ord →^{+} ∗
Ord := λa. μ^{a} (λX. 1 + X + (Nat^{∞} → X))

• Sized de Bruijn terms:

Lam : ord →^{+} ∗ →^{+} ∗
Lam := λa. μ^{a} (λX.λA. A + (X A × X A) + X (1 + A))

• Lam is an example of a non-regular type / heterogeneous type / nested type / inductive constructor.

Slide 18

F_{ω}: judgements on constructors

• Judgements

F : κ  constructor F has kind κ
F = G : κ constructors F, G are βη-equal
F ≤ G : κ F is a higher-order subtype of G

• Kinding of type constructor constants

→ : ∗ →^{−} ∗ →^{+} ∗  function space
∀_{κ} : (κ →^{∘} ∗) →^{+} ∗  quantification
μ_{κ} : ord →^{+} (κ →^{+} κ) →^{+} κ  inductive constructors

Slide 19

F_{ω}: higher-order subtyping

• Subtyping for ordinal expressions:

\frac{a ≤ b : ord}{a + 1 ≤ b + 1 : ord} \frac{a ≤ b : ord}{a ≤ b + 1 : ord} \frac{a : ord}{a ≤ ∞ : ord}

• Point-wise ordering of type constructors

\frac{F ≤ F′ : κ →^{p} κ′ G : κ}{F G ≤ F′ G : κ′}

• Co/contra-variant subtyping

\frac{F : κ →^{+} κ′ G ≤ G′ : κ}{F G ≤ F G′ : κ′} \frac{F : κ →^{−} κ′ G ≤ G′ : κ}{F G′ ≤ F G : κ′}

• Subtyping for inductive constructors:

\frac{a ≤ b : ord F : κ →^{+} κ}{μ^{a}F ≤ μ^{b}F : κ}

Slide 20

F_{ω}: terms

• Terms:

r, s, t ::= x | λx.t | r s | fix

• Typing judgment t : A.

• Inductive type folding and unfolding:

\frac{t : F (μ^{a}F)}{t : μ^{a+1}F}  \frac{t : μ^{a+1}F}{t : F (μ^{a}F)}

• Recursion rule:

\frac{a : ord}{fix : (∀i. A^{i} → A^{i+1}) → A^{a}} A^{i} admissible

Slide 21

Examples

• Typing of sum:

sum : List^{∞} Int → Int
sum = fix (λsum :List^{i} Int → Int. λl:List^{i+1}. match l with nil  ↦ 0 (x :: (xs : List^{i})) ↦ x + sum xs)

• Syntax with implicit fix and size annotations:

sum ([ ])^{i+1}  = 0
sum (x :: xs^{i})^{i+1} = x + sum xs^{i}

Slide 22

Merge sort: splitting phase

\xymatrix{[71] &  & [53] &  & [62] &  & [84] \\  & [71, 53] \ar[ul] \ar[ur] &  &  &  & [62, 84] \ar[ul] \ar[ur] \\  &  &  & [71, 62, 53, 84] \ar[ull] \ar[urr]}

Slide 23

Merge sort: merging phase

\xymatrix{[71] \ar[dr] &  & [53] \ar[dl] &  & [62] \ar[dr] &  & [84] \ar[dl] \\  & [53, 71] \ar[drr] &  &  &  & [62, 84] \ar[dll] \\  &  &  & [53, 62, 71, 84]}

Slide 24

Splitting: definition

split : ∀i:ord. ∀A:∗. List^{i}A → List^{i}A × List^{i}A split [ ]^{i+1} = ([ ]^{i+1}, [ ]^{i+1}) split (y :: l^{i})^{i+1} = let (xs^{i}, ys^{i})=split l^{i} in

((y :: ys)^{i+1}, xs^{i≤i+1})

Slide 25

Splitting: termination

split : ∀i:ord. ∀A:∗. List^{i}A → List^{i}A × List^{i}A split [ ]^{i+1} = ([ ]^{i+1}, [ ]^{i+1}) split (y :: l^{i})^{i+1} = let (xs^{i}, ys^{i})=split l^{i} in

((y :: ys)^{i+1}, xs^{i≤i+1})

• To compute split at stage i + 1, split is only used at stage i.

• Hence, split is terminating.

Slide 26

Splitting: bounded output

split : ∀i:ord. ∀A:∗. List^{i}A → List^{i}A × List^{i}A split [ ]^{i+1} = ([ ]^{i+1}, [ ]^{i+1}) split (y :: l^{i})^{i+1} = let (xs^{i}, ys^{i})=split l^{i} in

((y :: ys)^{i+1}, xs^{i≤i+1})

• We additionally can infer that split is non-size increasing.

• Using split, we can define merge sort… Slide 27

Merging: definition

merge produces a sorted list from two sorted input lists

merge : ∀i:ord. List^{i} Int → List^{∞} Int → List^{∞} Int
merge [ ]  l = l
merge (x :: xs^{i})^{i+1} l = merge′ l

where

merge′ : ∀j:ord. List^{j} A → List^{∞} A
merge′ [ ]  = x :: xs
merge′ (y :: ys^{j})^{j+1} = if x ≤ y then
x :: merge xs^{i} (y :: ys)^{j+1}
else y :: merge′ ys^{j}

Slide 28

Merging: termination

merge terminates by lexicographic ordering

merge : ∀i:ord. List^{i} Int → List^{∞} Int → List^{∞} Int
merge [ ]  l = l
merge (x :: xs^{i})^{i+1} l = merge′ l

where

merge′ : ∀j:ord. List^{j} A → List^{∞} A
merge′ [ ]  = x :: xs
merge′ (y :: ys^{j})^{j+1} = if x ≤ y then
x :: merge xs^{i} (y :: ys)^{j+1≤∞}
else y :: merge′ ys^{j}

Slide 29

Merging: termination

merge terminates by lexicographic ordering

merge : ∀i:ord. List^{i} Int → List^{∞} Int → List^{∞} Int
merge [ ]  l = l
merge (x :: xs^{i})^{i+1} l = merge′ l

where

merge′ : ∀j:ord. List^{j} A → List^{∞} A
merge′ [ ]  = x :: xs
merge′ (y :: ys^{j})^{j+1} = if x ≤ y then
x :: merge xs^{i} (y :: ys)^{j+1≤∞}
else y :: merge′ ys^{j}

Slide 30

Merge sort: definition

msort : List^{∞} Int → List^{∞} Int msort [ ] = [ ] msort (x :: l) = msort′ x l

msort′ : ∀i:ord. Int → List^{i} Int → List^{∞} Int msort′ x [ ]^{i+1} = [x] msort′ x (y :: l^{i}) = let (xs^{i}, ys^{i})=split l^{i} in

merge (msort′ x xs^{i}) (msort′ y ys^{i})

Slide 31

Merge sort: termination

msort : List^{∞} Int → List^{∞} Int msort [ ] = [ ] msort (x :: l) = msort′ x l

msort′ : ∀i:ord. Int → List^{i} Int → List^{∞} Int msort′ x [ ]^{i+1} = [x] msort′ x (y :: l^{i}) = let (xs^{i}, ys^{i})=split l^{i} in

merge (msort′ x xs^{i}) (msort′ y ys^{i})

Slide 32

Leaving Hindley-Milner typing

• So far, termination could have been checked without types • The size relation of split could have been recorded separately • But now let us parametrize merge sort over a split function...

Slide 33

Merge sort: abstract split

msort′ split x [ ]^{i+1} = [x] msort′ split x (y :: l^{i}) = let (xs^{i}, ys^{i})=split l^{i} in

merge (msort′ x xs^{i}) (msort′ y ys^{i})

• The variable split can only be instantiated with non size increasing functions

• This is naturally expressed with a rank-2 size polymorphic type

Slide 34

Merge sort: abstract split (II)

msort′ : (∀i:ord. ∀A:∗. List^{i}A → List^{i}A × List^{i}A) →

∀i:ord. Int → List^{i} Int → List^{∞} Int msort′ split x [ ]^{i+1} = [x] msort′ split x (y :: l^{i}) = let (xs^{i}, ys^{i})=split l^{i} in

merge (msort′ x xs^{i}) (msort′ y ys^{i})

• We drop the restriction of Hughes, Pareto, and Sabry and Barthe et. al. that sizes should be inferable Slide 35

Tree ordinals

• Tree ordinals Ord^{a} = μ^{a} (λX. 1 + X + (Nat^{∞} → X))

• Definable constructors

ozero : ∀i:ord. Ord^{i}
osucc : ∀i:ord. Ord^{i} → Ord^{i+1}
olim : ∀i:ord. (Nat → Ord^{i}) → Ord^{i+1}

Slide 36

An element of infinite height

[figure: Ord^{1}; Ord^{2}; Ord^{3}; …; ⊆ Ord^{ω}; ozero; ozero; osucc; ozero; osucc; osucc; …; olim; _{Ord_{ω+1}}]

Slide 37

Example: addition for tree ordinals

• Constructors:

ozero : ∀i:ord. Ord^{i}
osucc : ∀i:ord. Ord^{i} → Ord^{i+1}
olim : ∀i:ord. (Nat → Ord^{i}) → Ord^{i+1}

• Addition:

add : Ord^{∞} → ∀i:ord. Ord^{i} → Ord^{∞}

add x ozero  = x
add x (osucc y^{i})^{i+1} = osucc (add x y^{i})
add x (olim f^{·→i})^{i+1} = olim (λn. add x (f n)^{i})

Slide 38

Productivity

• Productivity is dual to termination

• A productive process should continuously turn input into output

• Examples: editor, operating system, stream

• Important in embedded and functional reactive programming Slide 39

Infinite structures

• On infinite objects like streams, we are interested in the definedness rather than the size.

• s : Stream^{a}A means s is defined upto depth a.

• Objects which are defined upto depth ∞ are called productive.

• Basic stream operations:

(::) : A → ∀i:ord. Stream^{i}A → Stream^{i+1}A
hd : ∀i:ord. Stream^{i+1}A → A
tl : ∀i:ord. Stream^{i+1}A → Stream^{i}A

• Subtyping: Stream^{∞}A ≤ … Stream^{i+1}A ≤ Stream^{i}A

Slide 40

F_{ω}: extension by coinduction

• Add type constructor ν_{κ} : ord →^{−} (κ →^{+} κ) →^{+} κ.

• Example Stream^{a} = λA. ν^{a} (λX. A × X).

• Recursion rule also usable for corecursion!

\frac{a : ord}{fix : (∀i. A^{i} → A^{i+1}) → A^{a}} A^{i} admissible

• Example: defining infinite sequence upfrom 0 = [0, 1, 2, ...]

upfrom : Int → Stream^{∞} Int
upfrom := fix (λupfrom.λn. \underbrace{(n, \overbrace{upfrom(n + 1)}^{Stream^{i} Int})}_{Stream^{i+1} Int})

Slide 41

Related works on type-based termination

• Hughes, Pareto, Sabry (1996)

Proving the correctness of reactive system using sized types • Amadio and Coupet-Grimal (1998)

Analysis of a guard condition in type theory

• Barthe, Frade, Giménez, Pinto, Uustalu (2004)

Type-based termination of recursive definitions

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

Slide 42

Own works on termination

• Specification and verification of a formal system for structural recursion (TYPES’99)

• A predicative analysis of structural recursion (with Altenkirch, JFP, 2002)

• Termination and guardedness checking with continuous types (TLCA’03)

• Termination checking with types (ITA, 2004)

• A polymorphic λ-calculus with sized higher-order types (Ph.D. thesis, almost ready for submission)

Slide 43

Works on iteration and recursion

• A predicative strong normalization proof for a λ-calculus with interleaving inductive types (Abel, Altenkirch, TYPES’99)

• Co(iteration) for higher-order nested datatypes (Abel, Matthes, TYPES’02)

• Generalized iteration and coiteration for higher-order nested datatypes (Abel, Matthes, Uustalu, FoSSaCS’03)

• Fixed points of type constructors and primitive recursion (Abel, Matthes, CSL’04)

• Generalized iteration and coiteration for higher-order and nested datatypes (Abel, Matthes, Uustalu, TCS, 2005)

Slide 44

Works on dependent type theory

• Meta-theoretical:

Untyped algorithmic equality for Martin-Löf’s Logical Framework with Surjective Pairs (Abel, Coquand, TLCA’05)

• Case studies:

– A third-order representation of the λμ-calculus (MERLIN’01)

– Weak normalization for the simply-typed λ-calculus in Twelf (LFM’04)

– Verifying Haskell programs in constructive type theory (Abel, Benke, Bove, Hughes, Norell, Haskell’05)

Slide 45

Short-term research goals

• Adopt type-based termination to dependent types

• Investigate type-based termination for higher-order abstract syntax

– Challenge: negative inductive types

Tm = (Tm × Tm) + (Tm → Tm)
app : Tm^{i} → Tm^{i} → Tm^{i+1}
abs : (Tm^{?} → Tm^{i}) → Tm^{i+1}

– Type-based termination not directly applicable.

– Can it be adopted to negative types?

Slide 46

Longer-term research goals

• Can type-based termination be adopted to languages with references?

• Integrate with heap type system

• Combinable with Hofmann/Jost system?

Slide 47

Works on theorem proving

• Human-readable machine-verifiable proofs for teaching constructive logic (Abel, Chang, Pfenning, PTP’01)

• Connecting a logical framework to a first-order prover (Abel, Coquand, Norell, FroCoS’05)

Slide 48

Long term research: proof documents

• Future of theorem proving:

– User writes legible, formal proof document

– Trivial steps are filled in by machine

• How should the proof language look like?

• What can be considered a trivial step?

• How to integrate automation?

This is a community effort (TYPES).

Slide 49

Acknowledgements

• Technical discussions on my thesis:

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

• Stipends GKLI CoVer

• Colleagues at Munich and Chalmers for support