functional programs, was: Re: [Termtools] Next competition
psk at informatik.rwth-aachen.de
Wed Mar 15 15:43:09 CET 2006
-----BEGIN PGP SIGNED MESSAGE-----
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 http://haskell.org/onlinereport/). That way we can
add a second real language category (ISO Prolog being the first) to
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
For the above example program the following abstract start
terms (among others) are "terminating":
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
Peter Schneider-Kamp mailto:psk at informatik.rwth-aachen.de
LuFG Informatik II http://www-i2.informatik.rwth-aachen.de/~nowonder
RWTH Aachen phone: ++49 241 80-21211
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v126.96.36.199 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org
-----END PGP SIGNATURE-----
Termtools mailing list
Termtools at serveur-listes.lri.fr
More information about the Termtools