Format
To specify the replacement map, needed for context-sensitive rewriting,
the fun parsing rule is extended with an optional
argument:
CSTRS ::= ( format CSTRS ) fun* rule* fun ::= ( fun identifier number (:replacement-map ( number* ))? ) rule ::= ( rule term term )The variable conditions on rules is the same as in the TRS format. The numbers in a
:replacement-map ( number* )
declaration must form a sequence of strictly increasing positive integers
between 1 and the arity of the function symbol declared in the
identifier number part.
Declarations (fun f n) are equivalent to
(fun f n :replacement-map (1 …
n)), so the full replacement map is default.
Examples
(format CSTRS) (fun cons 2 :replacement-map (1)) (fun incr 1) (fun idx 1) (fun head 1) (fun tail 1) (fun s 1) (fun 0 0) (fun nil 0) (fun zeros 0) (fun nats 0) (rule (incr nil) nil) (rule (incr (cons X L)) (cons (s X) (incr L))) (rule (idx nil) nil) (rule (idx (cons X L)) (incr (cons X (idx L)))) (rule nats (idx zeros)) (rule zeros (cons 0 zeros)) (rule (head (cons X L)) X) (rule (tail (cons X L)) L)In the first example, rewriting in the second argument of
cons is forbidden since argument
position 2 is missing from the replacement map
(1).
; @cops 1205
; TPDB TRS_Contextsensitive/Maude_06/MYNAT_nokinds-noand-peanoSimple
(format CSTRS)
(fun 0 0 :replacement-map ())
(fun U11 2 :replacement-map (1))
(fun U12 1 :replacement-map (1))
(fun U21 1 :replacement-map (1))
(fun U31 2 :replacement-map (1))
(fun U41 3 :replacement-map (1))
(fun U42 3 :replacement-map (1))
(fun isNat 1 :replacement-map ())
(fun plus 2 :replacement-map (1 2))
(fun s 1 :replacement-map (1))
(fun tt 0 :replacement-map ())
(rule (U11 tt V2) (U12 (isNat V2)))
(rule (U12 tt) tt)
(rule (U21 tt) tt)
(rule (U31 tt N) N)
(rule (U41 tt M N) (U42 (isNat N) M N))
(rule (U42 tt M N) (s (plus N M)))
(rule (isNat (plus V1 V2)) (U11 (isNat V1) V2))
(rule (isNat 0) tt)
(rule (isNat (s V1)) (U21 (isNat V1)))
(rule (plus N 0) (U31 (isNat N) N))
(rule (plus N (s M)) (U41 (isNat M) M N))
In the second example, the replacement map declarations in
(fun 0 0 :replacement-map ())
(fun U12 1 :replacement-map (1))
(fun U21 1 :replacement-map (1))
(fun plus 2 :replacement-map (1 2))
(fun s 1 :replacement-map (1))
(fun tt 0 :replacement-map ())
can be omitted.