on termination

[C T McBride]

Hi

> On Tuesday 13 May 2003 16:08, Cagdas Ozgenc wrote:
> > Indeed, I am still looking for a theorem of some sort that either equates
> > stongly normalizing systems to primitive recursive functions (if this is
> > the case), or a theorem that demonstrates some sort of limitation to
> > strongly normalizing systems when compared to a turing machine, or a system
> > that can decide recursive class but unable to recognize recursively
> > enumerable class.

There ain't no such thing. Recursiveness is undecidable. More concretely,
a strongly normalizing system captures a class of terminating functions
which is necessarily incomplete: a simple diagonalization argument shows
that the system's own normalization function (terminating, by definition)
cannot be coded within the system itself.

> Hmm, I think this depends on what a strongly normalizing system is :)
> Slightly going out of my sphere of knowledge (^_^)

A *strongly* normalizing system is one where *all* reduction strategies
yield a normal form. Type theories are usually designed to be strongly
normalizing, hence they are Turing incomplete; they do contain all
programs which are *provably* terminating in the particular logic to which
they correspond, but that logic, being consistent, is necessarily also
incomplete.

(Incidentally, Cayenne's type theory is the exception rather than the
rule: it's much-criticized undecidable typechecking comes down to the
availability of non-terminating programs at the type level. ghc with
`undecidable instances' allows you to write non-terminating Prolog
programs at the type level, thus breaking for exactly the same reason.
What exactly is Haskell's type level programming language, anyway?)

Of course, restricting to an incomplete fragment does not necessarily
mean `primitive recursion' in the narrow sense which excludes Ackermann's
function, viz

  data Nat = O | S Nat

  primrec :: Nat -> (Nat -> Nat -> Nat) -> Nat -> Nat
  primrec base step  O    = base
  primrec base step (S n) = step n (primrec base step n)

Just a bit of polymorphism is enough to overcome that problem:

  polyprimrec :: t -> (Nat -> t -> t) -> Nat -> t
  polyprimrec base step  O    = base
  polyprimrec base step (S n) = step n (polyprimrec base step n)

Old fashioned dependent type theories present computation over inductive
datatypes by equipping their structural induction principles with a
computational behaviour---an inductive proof of all n : Nat . P n, when
applied to 3, reduces to step 2 (step 1 (step 0 base)), just like
polyprimrec, but with

    base :: P 0,
and step :: all n : Nat. P n -> P (S n).

Suitably equipped with `pattern matching' sugar, these induction
principles provide quite a rich language of terminating functions,
necessarily incomplete, but including such notoriously troublesome
customers as first-order unification.

Moreover, a structural induction principle is just the recursion operator
which comes `free of charge' with an inductive datatype: many other total
recursive idioms can be proven admissible once (by a process which
resembles coding up a memoization scheme), then re-used freely in
programs.

So there's no magic complete answer to guaranteed termination, but it is,
I claim, useful to work within an incomplete but terminating language
if it enables you te express the structural reasons why your program
works, not just what it should do next.

Hope this helps

Conor