Talk:XTC Format Specification - Revision history

Griff: /* Proposed Change */ new section

2010-01-12T08:49:35Z

Proposed Change: new section

Noschinski: added prefix attribute to syntax

2009-04-17T10:08:40Z

added prefix attribute to syntax

Noschinski at 09:29, 24 March 2009

2009-03-24T09:29:17Z

Binabik: /* Syntax */

2009-02-26T08:00:29Z

Syntax

J.waldmann: /* Name clashes */

2009-02-24T17:09:39Z

Name clashes

Noschinski at 14:17, 24 February 2009

2009-02-24T14:17:59Z

Noschinski: add predefined proposal

2009-02-24T14:11:31Z

add predefined proposal

New page

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

← Older revision		Revision as of 08:49, 12 January 2010
Line 53:		Line 53:

	(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)		(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 [http://cl-informatik.uibk.ac.at/software/cpf/]). Still, XTC should either be backronymed as Carsten proposed [http://lists.lri.fr/pipermail/termtools/2009-December/000787.html here], or there should be a new name (e.g., XTP for XML Termination Problem).

@@ Line 10: / Line 10: @@
 Optional element, may occur arbitrary often.
-  <xs:element name="predefined" type="xs:string" minOccurs="0" maxOccurs="unbounded"/>
+  <xs:element name="predefined" type="xs:string" minOccurs="0" maxOccurs="unbounded">
-The value of this element describes the predefined module to include.
+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
 (SB: Edited the declaration of <xs:element/> so the element can occur 0..* times)
 === Modules ===

← Older revision		Revision as of 09:29, 24 March 2009
Line 45:		Line 45:
	The boolean module should be separate, and the integer module(s) can import it.		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.)		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)

← Older revision		Revision as of 17:09, 24 February 2009
Line 39:		Line 39:

	This would give aus int.0, int.-1, int.TRUE, ... Disadvantage of this approach is, that we get incompatible booleans.		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.)

← Older revision		Revision as of 14:17, 24 February 2009
Line 25:		Line 25:
	* boolean operations: not(TRUE) -> FALSE, and(TRUE, FALSE) -> FALSE, ...		* boolean operations: not(TRUE) -> FALSE, and(TRUE, FALSE) -> FALSE, ...
	* Additional restriction: Predefined defined symbols may not occur on the lhs of rules.		* 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.