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

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

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.