[Termtools] predefined integers, was: termination competition changes

[Johannes Waldmann]

>   <predefined>integers</predefined>

This certainly is important for applications,
so I'm generally in favour of such an extension.

I suggest the author(s) of the <predefined> proposal
create a page in the termination wiki,
containing the proposal itself (semantics + examples)
and a record of the ongoing discussion.


Some immediate technical questions:

The proposed <predefined> element
actually extends the signature (number symbols and operators)
and the rule set (evaluation rules for operators).

Are there other candidates for such pre-defined modules?
(e.g. "floating point" numbers)

What if one <problem> wants to use several such modules,
and their signatures overlap? If we have one global namespace,
then we should be careful. (*)

With predefined integers, how do you plan to handle booleans
(e.g. the results of comparison operators)?

How to you want to write literals for negative integers?

Is the proposal orthogonal w.r.t. other parts of the
TRS problem specification
(e.g. relative termination, theories, strategies),
or are there any "side effects"
(combinations with non-obvious semantics)


Best regards, Johannes.


(*) We could ultimately think of having qualified names,
or even operator overloading base on argument sorts,
(do we have sorted rewriting?) but that seems a bit heavy now.

On the other hand, there are many known designs
(e.g. for "scrpting" programming languages)
that are irreparably broken because they tried
to keep things superficially simple when they really aren't.


-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 257 bytes
Desc: OpenPGP digital signature
Url : http://lists.lri.fr/pipermail/termtools/attachments/20090223/c2708e38/attachment.pgp