(Draft) Tuesday Seminar

10 December 2002

by Thomas Hallgren

Highlights from the Workshop on Termination and Type Theory

[Hjortviken lobby]

Tuesday Seminar at OGI on 12 December, 2002.

by Thomas Hallgren

Workshop on Termination and Type Theory

A session is about to start

[Conference room]

Some interesting talks

I pick three talks that I liked and talk about them.

Conor McBride: Seeing and Doing

or Termination for Free

A common programming style:
  • Pick a simple data structure.
  • Describe your algorithm by saying first do this, then do that.
A better style:
  • Understand the structure of your computation and design your data structures to match.
  • This allows you to see the structure of the computation, since it follows the data structure.

Conor McBride: Seeing and Doing

Next: examples in Haskell.
Seeing and Doing :

Example: sorting by structural recursion

Sorting is easy to define with structural recursion:

insert :: Ord a => a -> [a] -> [a] sort :: Ord a => [a] -> [a] insert x [] = [x] insert x (y:ys) = if x<=y then x:y:ys else y:insert x ys sort [] = [] sort (x:xs) = insert x (sort xs)

However, there are more efficient sorting algorithms...

Seeing and Doing : Example :

Sorting efficiently

Resorting to general recursion, we can define a better sorting function:

quicksort :: Ord a => [a] -> [a] quicksort [] = [] quicksort (x:xs) = quicksort (filter (<x) xs)++ x: quicksort (filter (>=x) xs)

But this is almost structurally recursive. We only need to get rid of the call to filter in the recursive call to quicksort.

Seeing and Doing : Example :

Sorting efficiently with structural recursion

We combine quicksort and filter into one function:

qsf p xs = quicksort (filter p xs)
By simple transformations, we obtain:
qsf p [] = [] qsf p (x:xs) = if p x then qsf (\x'->p x' && x'<x) xs++ x: qsf (\x'->p x' && x'>=x) xs else qsf p xs

We used the law: filter p1 . filter p2 === filter (\x->p2 x && p1 x)

Seeing and Doing : Example :

Sorting efficiently with structural recursion

Seeing and Doing :

From doing to seeing

Seeing and Doing :

From doing to seeing

The structure that emerges is a binary search tree. This reveals the following alternative formulation of quicksort:

treesort xs = flatten (foldr insert Empty xs) data Tree a = Empty | Node a (Tree a) (Tree a) insert a Empty = Node a Empty Empty insert a (Node b l r) = if a<=b then Node b (insert a l) r else Node b l (insert a r) flatten t = flatten' t [] where flatten' Empty = id flatten' (Node a l r) = flatten' l . (a:) . flatten' r

Ana Bove: Modelling General Recursion in Type Theory

Modelling General Recursion in Type Theory :

General recursion in type theory

The old way

Modelling General Recursion in Type Theory :

General recursion in type theory

The new way

Modelling General Recursion in Type Theory :

An example

Modelling General Recursion in Type Theory :

An example

Modelling General Recursion in Type Theory :

An example

Assuming you have a termination proof,
qsAll :: (xs::[a]) -> Dqs xs
you can define
qs :: Ord a => [a] -> [a] qs xs = quicksort xs (qsAll xs)
with the same type as the original function.
Modelling General Recursion in Type Theory :

What about mutual recursion?

Modelling General Recursion in Type Theory :

What about nested recursion

Modelling General Recursion in Type Theory :

What about nested recursion

General Recursion in Type Theory :

A non-trivial example: Unification

Part 1: data types

type Var = Int type Fun = Int data Term = Var Var | Fun Fun [Term] type Assignment = (Var,Term) type Substitution = [Assignment] type Equation = (Term,Term) type Equations = [Equation]
General Recursion in Type Theory :

Unification

Part 2: the unification function

unify :: Equations -> Maybe Substitution unify eqs = unify' eqs [] unify' :: Equations -> Substitution -> Maybe Substitution unify' [] s = Just s unify' ((Var x,Var y):eqs) s | x==y = unify' eqs s unify' ((Var x,t):eqs) s | x `elem` vars t = Nothing | not (x `elem` vars t) = unify' (substEqs x t eqs) ((x,t):substS x t s) unify' ((Fun f ts,Var x):eqs) s = unify' ((Var x,Fun f ts):eqs) s unify' ((Fun f ts1,Fun g ts2):eqs) s | f/=g || length ts1/=length ts2 = Nothing | f==g && length ts1==length ts2 = unify' (zip ts1 ts2++eqs) s
Is unify' structurally recursive?
General Recursion in Type Theory : Unification :

Termination?

General Recursion in Type Theory : Unification :

Domain predicate

[Definition of UniAcc]
General Recursion in Type Theory : Unification :

Proofs

Ana's thesis contains formal proofs of the following:

Yves Bertot: Type-theoretic functional semantics

Type-theoretic functional semantics :

The language IMP

Arithmetic expressions:

a ::= n | X | a₀ + a₁ | a₀ - a₁ | a₀ * a₁

Boolean expressions:

b ::= true | false | a₀ = a₁ | a₀a₁ | ¬b | b₀b₁ | b₀b₁

Commands:

c ::= skip | X := a | c₀ ; c₁ | if b then c₀ else c₁ | while b do c

Type-theoretic functional semantics :

Operational Semantics

No surprises here.
Type-theoretic functional semantics :

Denotational Semantics

But there is a problem with a naive definition of the denotation function for commands...
Type-theoretic functional semantics : Denotational Semantics :

Denotation of Commands

Naive attempt

[Naive recursive denotation function]
Type-theoretic functional semantics : Denotational Semantics :

Denotation of Commands

Solution

Untie the recursive knot!
[Untied recusive knot]
Type-theoretic functional semantics :

Relating the two semantics

[Theorem 1]
Type-theoretic functional semantics :

Relating the two semantics

[Theorem 2]
Type-theoretic functional semantics :

Program extraction

Extraction of function F is simple, since it doesn't contain any proof components. The interpreter is then obtained by
interp :: Command -> State -> State interp = fix F

Other talks

Conclusions


[ Valid HTML?| Check Links]