Difference between revisions of "Integer Term Rewriting"

From Termination-Portal.org
Jump to navigationJump to search
(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…')
 
 
(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.

full text of the proposal