functional programs, was: Re: [Termtools] Next competition
Peter Schneider-Kamp
psk at informatik.rwth-aachen.de
Wed Mar 15 15:43:09 CET 2006
-----BEGIN PGP SIGNED MESSAGE-----
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 http://haskell.org/onlinereport/). 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
and
(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
first x
main
first ones
1 : [first ones]
Here "x" is an abstract variable.
Examples for abstract start terms that are not terminating:
ones
1 : ones
Thus, like for Prolog, there could be multiple abstract
start terms (terminating and non-terminating) for one
Haskell program.
Best regards,
Peter
- --
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 v1.4.2.1 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org
iD8DBQFEGCf83VbrCXkKHhwRAic4AJ9b7k2cHRXKUHf2uJyqaaVcT5X7bQCghyIj
26rIBD9nyRacELoBRxQVnIo=
=5waf
-----END PGP SIGNATURE-----
_______________________________________________
Termtools mailing list
Termtools at serveur-listes.lri.fr
http://serveur-listes.lri.fr/mailman/listinfo/termtools
More information about the Termtools
mailing list