Integer Term Rewriting: Difference between revisions
J.waldmann (talk | contribs) Created page with '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…' |
No edit summary |
||
| (3 intermediate revisions by 2 users not shown) | |||
| Line 5: | Line 5: | ||
+, -, *,/ ,%, >, >=, <, &&, ||, !, ... | +, -, *,/ ,%, >, >=, <, &&, ||, !, ... | ||
to conventional TRSs. To this | to conventional TRSs using the ''innermost'' rewrite strategy. To this | ||
aim it is necessary to extend the XTC format by the ability to represent | aim it is necessary to extend the XTC format by the ability to represent | ||
pre-defined semantics for function symbols. | pre-defined semantics for function symbols. | ||
Not only ITRSs, but also other extensions with pre-defined functions can be | Not only ITRSs, but also other extensions with pre-defined functions can be | ||
represented using this extension of the XTC format. | represented using this extension of the XTC format. A formal definition of ITRSs and their evaluation can be found | ||
in [http://verify.rwth-aachen.de/giesl/papers/idp-distribute.pdf this paper]. | |||
[http://lists.lri.fr/pipermail/termtools/2009-October/000775.html full text of the proposal] | [http://lists.lri.fr/pipermail/termtools/2009-October/000775.html full text of the proposal] | ||
[[Category:Categories]] | |||
Latest revision as of 16:00, 17 June 2014
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 using the innermost rewrite strategy. To this aim it is necessary to extend the XTC format by the ability to represent pre-defined semantics for function symbols. Not only ITRSs, but also other extensions with pre-defined functions can be represented using this extension of the XTC format. A formal definition of ITRSs and their evaluation can be found in this paper.