Term Rewriting - Revision history

Ffrohn: /* Integer Transition Systems */

2025-02-12T08:19:56Z

Integer Transition Systems

2025-02-12T08:18:14Z

Integer Transition Systems

2025-02-12T08:17:02Z

Integer Transition Systems

2025-02-12T08:16:19Z

Complexity

2025-02-12T08:13:34Z

Complexity

2025-02-12T08:12:21Z

Integer Transition Systems

2025-02-12T08:12:00Z

Integer Transition Systems

2025-02-12T08:11:33Z

Integer Transition Systems

2025-02-12T08:11:07Z

Integer Transition Systems

2025-02-12T07:59:56Z

Non-Relative Termination

@@ Line 87: / Line 87: @@
 * currently, we only support the condition-type ''oriented''
-=== Integer Transition Systems ===
+==== Integer Transition Systems ====
 Integer Transition Systems (ITSs) are [https://project-coco.uibk.ac.at/ARI/lctrs.php LCTRSs] with the following restrictions:

@@ Line 103: / Line 103: @@
 where the given identifier refers to a previously declared function symbol.
-The goal is to prove termination w.r.t. all startterms of the form
+The goal is to prove termination w.r.t. all well-sorted startterms of the form
 <pre>
-(f t_1 ... t_k)
+(f c_1 ... c_k)
 </pre>
-where f is the entrypoint and t_1,...,t_k are terms built from variables and predefined function symbols from the theory Ints.
+where f is the entrypoint and c_1,...,c_k are constants from the theory Ints (i.e., integers or Booleans).
 == Complexity ==

@@ Line 97: / Line 97: @@
 rhs  ::= (identifier term+)
 </pre>
-Moreover, ITSs must declare an entrypoint
+Moreover, ITSs must declare one and only one entrypoint
 <pre>
 entrypoint ::= (entrypoint identifier)

← Older revision		Revision as of 08:16, 12 February 2025
Line 136:		Line 136:

	* full rewriting		* full rewriting
		+
		+	=== Complexity w.r.t. an entrypoint ===
		+
		+	Here, we only consider basic start terms where the root symbol is the provided entrypoint.
		+
		+	==== Integer Transition Systems ====
		+
		+	* see the definition of ITSs for termination above

@@ Line 111: / Line 111: @@
 == Complexity ==
-See [https://project-coco.uibk.ac.at/ARI/trs.php here] for all complexity categories.
+See [https://project-coco.uibk.ac.at/ARI/trs.php here] for all complexity categories except for "Integer Transition Systems".
 === Runtime Complexity ===

@@ Line 93: / Line 93: @@
 * Rules must comply with the following grammar:
 <pre>
-rule ::= (rule lhs rhs (:guard term)? (:var (vars))? )
+rule ::= (rule lhs rhs (:guard term)? (:var (vars))?)
 lhs  ::= (identifier identifier+)
 rhs  ::= (identifier term+)

@@ Line 89: / Line 89: @@
 === Integer Transition Systems ===
-Integer Transition Systems are [LCTRSs]() with the following restrictions:
+Integer Transition Systems (ITSs) are [LCTRSs](https://project-coco.uibk.ac.at/ARI/lctrs.php) with the following restrictions:
 * The theory is always Ints.
 * Rules must comply with the following grammar:
 <pre>
-rule ::= ( rule lhs rhs guard? )
+rule ::= (rule lhs rhs (:guard term)? (:var (vars))? )
-lhs  ::= ( identifier identifier+ )
+lhs  ::= (identifier identifier+)
-rhs  ::= ( identifier expression+ )
+rhs  ::= (identifier term+)
 </pre>
 == Complexity ==