Format

The format for CTRSs reuses the parsing rules for fun and term of the TRS format, while the remaining rules look as follows:

     CTRS ::= ( format CTRS cond-type ) fun* rule*
cond-type ::= oriented | join | semi-equational
     rule ::= ( rule term term cond* )
     cond ::= ( = term term )

Left-hand sides of rewrite rules cannot be variables, but variables appearing in right-hand sides need not appear in the corresponding left-hand sides. The condition type cond-type determines how the equality sign in the conditions cond is interpreted.

Examples

(format CTRS oriented)
(fun f 1)
(fun g 1)
(fun h 1)
(rule (f x) (f y) (= (g x) z) (= (g z) (h y)))

The oriented declaration demands that the equations are interpreted as reachability constraints. So f(s) rewrites to f(t) if there exists a term u such that both g(s) →* u and g(u) →* h(t).

; @cops 331
; @author Thomas Sternagel
; @author Aart Middeldorp
; @doi 10.1007/3-540-19242-5_14
; p. 185
(format CTRS join)
(fun f 1) (fun g 1) (fun h 1) (fun j 1)
(fun a 0) (fun b 0) (fun c 0) (fun d 0)
(rule (h (f a)) c)
(rule (h x) (j x))
(rule c (j (f a)))
(rule a b)
(rule c d)
(rule (j (g b)) d)
(rule (f x) (g x) (= d (h (f x))))

The second example is a join CTRS, in which the equality sign is interpreted as joinability. So f(a) rewrites to g(a), because the terms d and h(f(a)) are joinable.

; @cops 282
; @author Thomas Sternagel
; @author Aart Middeldorp
; @doi 10.1007/3-540-56393-8_9
; Example 5
(format CTRS semi-equational)
(fun G 2)
(fun a 0)
(fun b 0)
(fun c 0)
(rule a a (= b c))
(rule (G x y) x)
(rule (G x y) y)

The third example is a semi-equational CTRS, in which the equality sign is interpreted as convertibility. So a rewrites to a, because the terms b and c are convertible (via the term G(b,c)).