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

[Johannes Waldmann]

> I propose to use the syntax and the evaluation strategy of Haskell98
> (as defined by http://haskell.org/onlinereport/).

Sure, I'm all for it ... Note this implies that each prover
that wants to participate in this category
needs a Haskell parser and a Haskell type checker...

and probably a translator to "kernel haskell" (see 1.2 of the report)
to get the semantics right. E. g. visible Haskell
has pattern matching ( map f (x : xs) = ... )
but the kernel version has this translated into
case expressions ( map f l = case l of x : xs -> ... )

Or do we want pattern matching in left-hand sides
(as in term rewriting) directly? Then we need a translation
for case expressions in the right-hand sides.
Or we forbid case expressions (and "if" expressions)

While we're at it, we probably don't want
"let", "lambda" and "where" either (at least for the start)
so that it looks more like term rewriting.

Even then, pattern matching has nasty details:
patterns have priorities (earlier position in source code wins)
and there are pattern guards (|) and lazy patterns (~).

Best regards,
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------

_______________________________________________
Termtools mailing list
Termtools at serveur-listes.lri.fr
http://serveur-listes.lri.fr/mailman/listinfo/termtools