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

[Peter Schneider-Kamp]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Johannes Waldmann wrote:
> I'd prefer to have them in the program, as annotations.

That's what we prefer, too. Otherwise some meta information
needs to be added to the TPDB which does not sound like much fun.

> But then let's have some special symbol, e. g. "-- terminates:"
> *but* this would make multi-line  queries inconvenient,
> so I suggest a block pragma {-# TERMINATES: foo x y #-}

"-- start term: " or "-- terminates: " would both be okay
with me. I do not see the need for multi-line queries, though.
What kind of queries do you have in mind?

> I am a bit worried about variables in such expressions:
> I would feel much better to declare them.
> {-# TERMINATES: forall  x :: [Integer] , y :: Bool . foo x y #-}
> 
> I am totally against the convention "every undeclared identifier
> is considered an all-quantified variable" because it breaks all too easy
> (imagine you add some declaration for a constant "x" to the program).

Declaring all abstract variables (whatever the syntax) sound like
a good idea to me. But declaring the type could be done
in the term: foo (x::Integer) (y::Bool)
This would provide greater flexibility in typing as whole
expressions could also be typed.

> It should be OK to have several such TERMINATES annotations
> in one program.

Of course.

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

iD8DBQFEGVrB3VbrCXkKHhwRAlUXAJ9Q/cnGtcflXXhWalne639eg/NilwCfWSyc
mA1tomHa7SvIacpUPf6Jk/I=
=GrYm
-----END PGP SIGNATURE-----

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