[Termtools] Extension of the XTC format / predefined functions

[Martin Plücker]

Dear all,
	
for the Termination Competition 2009 we wish to introduce a new category for
integer term rewriting systems (ITRSs) as we proposed them in [1]. To this
aim it is necessary to extend the XTC format by the ability to represent
pre-defined semantics for function symbols. The main idea of ITRSs is to add
pre-defined constructors for integers (the integers themselves) and Booleans
(true / false) and arithmetic, relational and Boolean functions like +, -,
*,/ ,%, >, >=, <, &&, ||, !, ... to conventional TRSs. The pre-defined
functions are represented by implicitly adding an infinite set of rules to
the user-defined rules. For example, the implicit rules for + are {+(x, y)
-> z | x, y and z are integers and x + y = z}.

Not only ITRSs, but also other extensions with pre-defined functions can be
represented using this extension of the XTC format, which we present in more
detail below.


A function symbol can have pre-defined semantics which is indicated by
adding a <semantics> tag to the declaration of the function symbol in the
signature. 

There are two categories of pre-defined function symbols.

1. Pre-Defined Constructors

Example:
<funcsym>
  <name>17</name>
  <arity>0</arity>
  <semantics>
    <integers/>
  </semantics>
</funcsym>
	
The function symbol "17" is assigned to the pre-defined integer 17 by giving
it the integer domain as semantics. Here we agree that numbers always have
their own value and it is not possible to give non numeric function symbols
like "foo" the pre-defined semantics of a number. Analogous rules apply for
Booleans (true / false) and other pre-defined constructors.

2. Pre-Defined Operations

Example:
<funcsym>
  <name>myPlus</name>
  <arity>2</arity>
  <semantics>
    <plus>
      <integers/>
    </plus>
  </semantics>
</funcsym>

Semantics are defined by a (maybe infinite) set of rules PR which is
implicitly added to the set of user-defined rules. For the example PR would
consist of all rules of the form PR = {myPlus(x, y) -> z | x, y and z are
integers and x + y = z}.

More examples for Booleans:
<funcsym>
  <name>true</name>
  <arity>0</arity>
  <semantics>
    <booleans/>
  </semantics>
</funcsym>

<funcsym>
  <name>myOr</name>
  <arity>2</arity>
  <semantics>
    <logical_or>
      <booleans/>
    </logical_or>
  </semantics>
</funcsym>

The complete list of pre-defined semantics needed to represent ITRSs is: 
- Constructors: integers, Booleans (true / false),
- Arithmetic functions: plus, minus, times, div, modulo, 
- Relational functions: greater_than, greater_equals, less_than,
less_equals, equals, not_equals,
- Logical functions: logical_and, logical_or, logical_not.

The semantics of these operations corresponds to the usual behavior of these
functions. One has to take care how div and modulo behave, we propose to use
the version which is used in most programming languages, e.g., Java. Here
div is rounding to zero, i.e., div(2, 3) = 1, div(-3, 2) = -1. Modulo is
defined as x % y = x - y * div(x, y).

As we mentioned above, a formal definition of TRSs with pre-defined integers
can be found in [1]. A patch for the XSD format is included in the
attachment.

Best regards,
Fabian Emmes, Martin Plücker

[1]
C. Fuhs, J. Giesl, M. Plücker, P. Schneider-Kamp, and S. Falke Proving
Termination of Integer Term Rewriting In Proceedings of the 20th
International Conference on Rewriting Techniques and Applications (RTA '09),
Brasilia, Brazil, Lecture Notes in Computer Science 5595, pages 32-47, 2009.
©Springer-Verlag
-------------- next part --------------
A non-text attachment was scrubbed...
Name: xtc.xsd
Type: application/octet-stream
Size: 13040 bytes
Desc: not available
Url : http://lists.lri.fr/pipermail/termtools/attachments/20091028/6537bf8a/attachment.obj 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: xtc_semantics.patch
Type: application/octet-stream
Size: 6332 bytes
Desc: not available
Url : http://lists.lri.fr/pipermail/termtools/attachments/20091028/6537bf8a/attachment-0001.obj