Below are my personal notes, written while preparing for the talk.
This talk is about some of the interesting things I remember from the Workshop in Termination and Type Theory, Göteborg, 14-15 November 2002.
This talk/paper presents a little imperative langauge IMP with while loops and gives semantics for it in two ways in type theory: an natural semantics (operational) and a denotational (functional) semantics. They prove that these agree. There is of course a problem with giving a naive denotation function for IMP: you need general recursion, in particular nested recursion, and type theory (Coq) allows only total functions defined by structural recursion. The paper shows how to overcome these problem in simple and elegant way. Another interesting aspect is that from the functional semantics, a functional program (in OCaml) can be extracted. You thus get an interpreter that is formally proved to be equivalent to the natural semantics!
David has worked on a termination checker based on Size-Change termination (Niel Jones), to replace the current termination checker in Alfa/Agda. Size-Change termination works by constructing the call graph of the program, and annotating the edges of the graph with size-change relations. Termination is then proved by proving that every infinite path in the call graph requires an infinite decrease in size, which is impossible. (Upper limits on sizes can also be used to detect termination.) This subsumes termination by structural recursion and lexicographical orderings. For example, it handles argument swappings. (But what about higher order functions and laziness?)
Traditional Martin-Löf type theory comes with a predefined set of types with associated sturctural induction principles. Compared to that, this talk thus proposes a type theory with a more general form of recursive definitions. Per Martin-Löf then asked the natural question if the right approach to extensions of this kind isn't to give a translation into the primitive, well understood concepts. (Torsten Altenkirch mentioned the general idea of certifying checkers.) Per's question prompted a long disussion that continued in a discussion session in the afternoon, introduced by Peter Dybjer, who contrasted the approaches taken in the constructive communities (open, extensible system) with the approach used in logical frameworks based on classical logic (where everything is reduced to a small set of primitive notions), e.g. HOL.
Ana recently defended her PhD thesis (abstract) on her approach to reasoning about general recursive (and partial) functions in type theory. The method deals with non-structural recursion, mutual recursion and nested recursion and gives you a way to express and reason about such functions in type theory, without requiring a termination proof. It works by mechanically translating a function in a functional language that allows general recursion, into (1) an inductively defined domain predicate and (2) a structurally recursive function over the proofs that arguments satisfy the domain predicate. Advantages over previous methods based on the general accessibility predicate include that the resulting functions closely resemble the original functions, and that termination proofs can be kept separate.
Conor's thesis seems to be that general recursion is overrated. Instead of using general recursive functions over simple data structures (do this, then do that), we should be using more sofisticated data structures that captures the pattern of the computation (seeing, making the computation pattern visible). More powerful type system allows more complex computation patterns to be captured, so dependent types are interesting. Conor also gives examples of how to transform general recursion to structural recursion in a conventional functional language (Haskell). (I'll show two ways to transform the quicksort function.)
Another relevant paper by Conor: First-Order Unification by Structural Recursion.
See also: John Matthews: Recursive Function Definition over Coinductive Types