Talk:XTC Format Specification

Proposed <predefined> extension

Proposal: Add a new element <predefined> to <problem> to extend the problem with a (possibly infinite set) of predefined function symbols and rules.

Rationale: TRS problems with predefined rules for integers. As there are infinitely many predefined rules ( like 1 + 1 -> 2, 1 + 2 -> 3, ...), those cannot be expressed with the proposed format. Apart from the infinite number of rules, those are normal TRS (with the additional restriction, that occurence of predefined defined symbols on the lhs is forbidden).

Syntax

Optional element, may occur arbitrary often.

<xs:element name="predefined" type="xs:string" minOccurs="0" maxOccurs="unbounded">
  <xs:attribute name="prefix" use="optional" type="xs:string" />
</xs:element>

The value of this element describes the predefined module to include. The optional "prefix" attribute will prefix every function symbol included in the module with the supplied string. This allows disambiguating when using multiple modules.

Name clashes (not resolved by a prefix) either between different modules or between a module and a TRS are an error.

(SB: Edited the declaration of <xs:element/> so the element can occur 0..* times) (LN: Added predefined attribute)

Modules

Other possible modules would be e.g. restricted_integers (like 32-bit integers).

unrestricted_integers

• integer constants: 0, -1, 1, -2, 2, ...
• integer operations: 0 + 0 -> 0, 0 + 1 -> 1, 2 * 3 -> 6, ...
• comparisons: 0 < 1 -> TRUE, -2 == 3 -> FALSE, ...
• boolean constants: TRUE, FALSE
• boolean operations: not(TRUE) -> FALSE, and(TRUE, FALSE) -> FALSE, ...
• Additional restriction: Predefined defined symbols may not occur on the lhs of rules.

"proprietary" modules

If a tool wants to define its own modules, it SHOULD use a name like X-$TOOLNAME-$MODULE, e.g. X-APROVE-INTEGERS.

Open problems

Name clashes

How to cope with name clashes, if more than one module is used? E.g. both restricted and unrestricted integers would want to declare TRUE, FALSE and boolean operations.

This could be solved by adding an optional prefix to each function symbol, like

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

This would give aus int.0, int.-1, int.TRUE, ... Disadvantage of this approach is, that we get incompatible booleans.

(JW: The root of this problem being that booleans seem to be hard-wired into the integer module. The boolean module should be separate, and the integer module(s) can import it. Well, there's a huge design space for module systems, disambiguating names etc.)

(LN: This problem cannot be solved without adding a real module system. So I think having built-in booleans in the integer and adding "cast" rules, if it is necessary to interoperate between multiple modules seems like a workable solution)

Proposed Change

As far as I remember, the name XTC was originally planned for the XML format used by certifiers (something like XML Termination Certificate). There is now a different name for that, namely CPF (see [1]). Still, XTC should either be backronymed as Carsten proposed here, or there should be a new name (e.g., XTP for XML Termination Problem).