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

[Peter Schneider-Kamp]

-----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