Semi-continuous Sized Types and Termination

Termination Checking via Type Systems

Andreas Abel

Department of Computer Science Ludwig-Maximilians-University Munich

Computer Science Logic 2006 Szeged, Hungary September 26, 2006

Introduction

Theorem Provers for Constructive Logic

Theorem Provers built on Dependent Type Theory: Coq (INRIA, France) Epigram (Nottingham, UK) Agda (Chalmers, Sweden)

Their soundness is based on termination.

Introduction

Constructive Logics

The Curry-Howard Isomorphism:

Proposition Type
A implies B A → B
Proof  Purely Functional Program
Valid Proof Terminating Program

Non-terminating programs lead to inconsistency:

\begin{matrix}f : (0 = 0) → (0 = 1) \\ f (p) = f (p) \end{matrix}

Type-Based Termination Explained

Type-Based Termination, Informally

Recipe Step 1 In the type system, attach sizes to data structures. Step 2 Using type-checking, ensure that recursive calls use only

arguments with decreased size.

Type-Based Termination Explained

Step 1: Sized Binary Trees

Let BTree^{ı} denote trees of height < ı. The empty tree has height 0, hence leaf : BTree^{1}, but also leaf : BTree^{2}, leaf : BTree^{3}, … In general leaf : BTree^{ı+1} for all ı.

leaf : ∀ı. BTree^{ı+1}
node : ∀ı. Int ×(BTree^{ı} × BTree^{ı}) → BTree^{ı+1}

BTree^{∞} contains all binary trees. Subtyping: BTree^{ı} ⊆ BTree^{ı+1} ⊆ ⋯ ⊆ BTree^{∞}.

Type-Based Termination Explained

Step 2: Equality Test for Sized Binary Trees

Code annotated with sizes:

eq : ∀ı. BTree^{ı} → BTree^{ı} → Bool

eq leaf leaf = true

eq node(i_{1}, (l_{1}, r_{1}))^{ı+1} node(i_{2}, (l_{2}, r_{2}))^{ı+1} = (i_{1} == i_{2}) &&

eq l_{1}^{ı} l_{2}^{ı} && eq r_{1}^{ı} r_{2}^{ı}

eq = false

Input arguments assumed to be of size ı + 1. Recursive arguments inferred to be of size ı. Descend in size, hence, termination.

Andreas Abel (LMU Munich)  Semi-continuous Sized Types  CSL’06  6 / 21

Abstraction and Polymorphism

Abstracting the Branching Type

Generalize to F -Branching Int-labelled trees Tree^{ı} F Constructors:

leaf : ∀F ∀ı. Tree^{ı+1}F
node : ∀F ∀ı. Int ×F (Tree^{ı}F ) → Tree^{ı+1}F

Valid instances

binary trees  F T = T × T
lists  F T = T
finitely branching trees F T = List^{∞} T
infinitely branching trees F T = Nat^{∞} → T

Invalid instance (F not monotone), e.g., F T = T → Bool

Andreas Abel (LMU Munich)  Semi-continuous Sized Types  CSL’06  7 / 21

Abstraction and Polymorphism

Equality of F -Branching Trees

Generalize equality test to F -branching trees: Termination not inferable with untyped methods.

Abstraction and Polymorphism

Termination and Polymorphism

Eq T = T → T → Bool eq : (∀T .Eq T → Eq (F T )) → ∀ı. Eq (Tree^{ı}F ) eq eqF leaf leaf = true

eq eqF node(i_{1}, ft_{1}) \overbrace{node(i_{2}, \underbrace{ft_{2}}_{F (Tree^{ı} F )})}^{Tree^{ı+1} F} = (i_{1} == i_{2}) &&

eqF

Eq T =Eq (Tree^{ı}F )

\overbrace{(eq eqF)} ft

1

ft

2

eq = false Observe the role reversal: The recursive function (eq eqF) becomes an argument to its own argument eqF!

Andreas Abel (LMU Munich)  Semi-continuous Sized Types  CSL’06  9 / 21

Abstraction and Polymorphism

Termination and Polymorphism

Eq T = T → T → Bool eq : (∀T .Eq T → Eq (F T )) → ∀ı. Eq (Tree^{ı}F ) eq eqF leaf leaf = true

eq eqF node(i_{1}, ft_{1}) \overbrace{node(i_{2}, \underbrace{ft_{2}}_{F (Tree^{ı} F )})}^{Tree^{ı+1} F} = (i_{1} == i_{2}) &&

eqF

Eq T =Eq (Tree^{ı}F )

\overbrace{(eq eqF)} ft

1

ft

2

eq = false Observe the role reversal: The recursive function (eq eqF) becomes an argument to its own argument eqF!

Andreas Abel (LMU Munich)  Semi-continuous Sized Types  CSL’06  9 / 21

Abstraction and Polymorphism

Evaluation

No untyped formalism can handle this example:

In the untyped setting, eq diverges, e.g., define

eqF eqT ft_{1} ft_{2} = eqT node(0, ft_{1}) node(0, ft_{2})

and execute the function clause

eq eqF node(i_{1}, ft_{1}) node(i_{2}, ft_{2}) = …

eqF (eq eqF) ft_{1} ft_{2}

A typed formalism such as TBT uses the information that

eqF : ∀T .Eq T → Eq (F T )

is polymorphic (hence, the above instance of eqF is ill-typed).

Andreas Abel (LMU Munich)  Semi-continuous Sized Types  CSL’06  10 / 21

Theory of Type-Based Termination Transfinite Induction

Type-Based Termination, Formally

Theorem f = s(f ) : ∀ı. A(ı) is well-defined if

1 (bottom check) A(0) contains all programs, e.g.,

A(ı) = BTree^{ı} → C. 2 (descent) f : A(ı) implies s(f ) : A(ı + 1). 3 (admissibility) ⋂_{α<λ} A(α) ⊆ A(λ) for all limit ordinals λ ≠ 0.

Proof. By transfinite induction on ı.

1 (base) f : A(0) trivial. 2 (step) ind.hyp. f : A(α) implies s(f ) = f : A(α + 1). 3 (limit) f : ⋂_{α<λ} A(α) by ind.hyp., hence f : A(λ).

Theory of Type-Based Termination Admissible Types for Recursion

Upper Semi-Continuous Types

Definition (upper semi-continuous) A semantical type A : On → P(SN) is upper semi-continuous (usc) if for all limits λ ≠ 0

lim sup_{α→λ} A(α) := ( ⋂_{α_{0}<λ} ⋃_{α_{0}≤α<λ} A(α)) ⊆ A(λ)

An usc type fulfills ⋂_{α<λ} A(α) ⊆ A(λ), hence, is admissible.

Theory of Type-Based Termination Admissible Types for Recursion

Lower Semi-Continuous Types

Definition (upper semi-continuous) A semantical type A : On → P(SN) is lower semi-continuous (usc) if for all limits λ ≠ 0

A(λ) ⊆ lim inf_{α→λ} A(α) := ⋃_{α_{0}<λ} ⋂_{α_{0}≤α<λ} A(α)

Continuous Types

usc  lsc

lim sup_{α→λ} A(α) ⊆ A(λ)  A(λ) ⊆ lim inf_{α→λ} A(α)

continuous

lim_{α→λ} A(α) = A(λ)

Closure Properties of Semi-Continuity

usc  condition  lsc  condition
A usc  A monotone A lsc  A antitone
A + B usc A, B usc  A + B lsc A, B lsc
A × B usc A, B usc  A × B lsc A, B lsc
A → B usc A lsc, B usc —
νF usc  F usc  μF lsc  F lsc

Theory of Type-Based Termination Admissible Types for Recursion

Why Upper Semi-Continuity is Vital

Let pred : ∀ı. Nat^{ı+1} → Nat^{ı} such that pred 0 raises an exception. Define

f : ∀ı. \overbrace{(Nat^{∞} → Nat^{ı}) → X}^{A(ı)}

f (g : Nat^{∞} → Nat^{ı+1}) = f ((pred ∘ g ∘ succ) : Nat^{∞} → Nat^{ı}) Now f (id) loops. The definition passes the bottom check and the descent criterion, but A(ı) is neither usc nor admissible.

Further Work

Related Work

Expressivity  Xi Par Ama Gim Fra A Bar Bla Buch
term. measures +  –  –  –  –  –  –  +  o
dep. types  o  –  –  +  –  –  +  +  –
polymorphism  +  o  –  +  – + +  +  –
infinite branch. –  –  –  +  + + +  –  +
semi-cont.  –  ω  –  –  – + –  –  –
productivity  –  +  +  +  + + +  –  +

Features

symbolic exec.  –  –  +  +  + + +  +  +
soundness  V  D  SN  – SN SN o SN  D
ordinals  < ω ≤ ω On  –  Ω Ω_{ω} – < ω ≤ ω
equi-rec.  –  +  –  –  – +  –  –  –
size inference  –  +  –  –  –  –  +  –  –

Further Work

Conclusions

Termination checking can be integrated into type checking Especially powerful in combination with polymorphism Type-Based Termination is a modern technology, still under active development

Further Work

Future Work

Extend to dependent types Investigate semi-continuity for dependent types Find intuitive explanations for non-admissibility of types Integrate into a theorem prover

Further Work

Acknowledgements

Technical discussions on my thesis Klaus Aehlig Thorsten Altenkirch Ikegami Daisuke Martin Hofmann

John Hughes  Ralph Matthes  Tarmo Uustalu

Financial support

Graduiertenkolleg Logik in der Informatik Project CoVer (Swedish Foundation for Strategic Research) TYPES APPSEM II

Further Work Construction of Sized Types

Formalizing Sized Types

Capture the structure of data types, forget about constructor names.

Types are build from the primitives + (disjoint sum), × (cartesian product), → (function space).

Sized types μ^{ı}F are recursive types obtained by iterating a type transformer F :

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

E.g., type constructor for binary trees: BTreeF X = 1 + Int ×(X × X )

Sized binary trees: BTree^{ı} = μ^{ı} BTreeF.

Andreas Abel (LMU Munich)  Semi-continuous Sized Types  CSL’06  21 / 21