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"/>

The value of this element describes the predefined module to include.

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

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