[Termtools] predefined integers, was: termination competition changes

[Lars Noschinski]

[Sorry for the doublepost, forgot to use the correct mail address for
the list]

* Johannes Waldmann <waldmann at imn.htwk-leipzig.de> [09-02-23 12:47]:
> 
> >   <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.

I will use

    http://termination-portal.org/mediawiki/index.php?title=Talk:XTC_Format_Specification

for this.

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

Probably. For example, n-bit integers would be of particular interest
for the analysis of e.g. Java code.

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

Currently we treat them (and the common operators) as predefined
symbols. From a theoretical point of view, treating and, or, xor, not as
predefined symbols may not be strictly necessary, but our current
design depends on it.

> 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. (*)

Overlapping would be especially likely with booleans, e.g. both
unrestricted and restricted integers would want to define comparisons.
The simplest workaround would be to allow setting an optional, arbitrary
prefix, e.g.

    <predefined prefix="int.">integers</predefined>

which would give us int.42 instead of int.

Disadvantage would be, that every predefined module would define its
own, incompatible booleans. Or we could make "integers" and
"restricted_ingeres" import "booleans" - but this seems kind of heavy.

> How to you want to write literals for negative integers?

Like "-42".

Our current self-defined format uses infix-notation and therefore parses
-42 as -(42) to avoid ambiguities. In the XML format, this problem does
not exist and therefore I would suggest to treat -42 as a literal. This
avoids special casing negative literals on serialization.

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

We are not aware of any problems. Strategies should work, theories and
replacement maps as well, as long as they do not modify predefined
symbols.  For relative rules, the same restriction applies as  normal
rules (no predefined defined symbols on the LHS).

 - Lars.