functional programs, was: Re: [Termtools] Next competition

Peter Schneider-Kamp psk at
Wed Mar 15 15:43:09 CET 2006

Hash: SHA1

Johannes Waldmann wrote:
> Termination for Functional programming opens up quite some problems
> (of which syntax should be the easiest one):
> what is "termination"? what evaluation strategy?
> Full termination or top termination (because of lazy eval.)?
> Are the programs typed? If so, what type system?
> (Does it have an influence on termination?)
> Do we do higher-order rewriting?
> (I certainly use lambdas in my Haskell programs.)
> Anyway to avoid syntax discussions, can we try for a subset
> of some existing functional programming language (e. g. ML or Haskell).

I propose to use the syntax and the evaluation strategy of Haskell98
(as defined by That way we can
add a second real language category (ISO Prolog being the first) to
the TPDB.

This answers all your questions but one. What is "termination"?

Obviously, "termination of all functions for all possible arguments"
is not a good definition. Consider the following simple Haskell program:

  first (x:_) = x
  ones = 1 : ones
  main = first ones

The program terminates, but the function ones does not.

Thus, I would propose to use abstract start terms, i.e.,
Haskell terms possibly containing abstract variables. This
roughly corresponds to the idea of abstract queries in Prolog:

A term t containing no abstract variables is "terminating"
if and only if
(a) its evaluation (according to Haskell strategy) is finite
(b) all (type-correct) applications of t to a "terminating"
    term are "terminating"

An abstract term t is "terminating" if and only if
all (type-correct) instantiations of t which instantiate
all abstract variables with "terminating" terms
are "terminating".

For the above example program the following abstract start
terms (among others) are "terminating":

  first x
  first ones
  1 : [first ones]

Here "x" is an abstract variable.
Examples for abstract start terms that are not terminating:

  1 : ones

Thus, like for Prolog, there could be multiple abstract
start terms (terminating and non-terminating) for one
Haskell program.

Best regards,
- --
Peter Schneider-Kamp   mailto:psk at
LuFG Informatik II
RWTH Aachen            phone: ++49 241 80-21211

Version: GnuPG v1.4.2.1 (GNU/Linux)
Comment: Using GnuPG with Mozilla -


Termtools mailing list
Termtools at

More information about the Termtools mailing list