Format

The format for many-sorted term rewrite systems modifies the TRS format, according to the following grammar:

MSTRS ::= ( format MSTRS ) sort* fun* rule*
 sort ::= ( sort identifier )
  fun ::= ( fun identifier type )
 type ::= identifier | ( -> identifier+ identifier )
 rule ::= ( rule term term )

We adopt arrow notation -> for function types, anticipating that a consistent notation will be used in a new format for higher-order rewrite systems. Function declarations such as (fun cons 2) are invalid in the MSTRS format. Every term must be a well-typed term according the types in the ( fun identifier type ) declarations. The variable conditions on rules is the same as in the TRS format. The sorts of variables used in many-sorted rewrite rules must be inferred from the rules separately.

Examples

; @cops 646
; @author Takahito Aoto
; @doi 10.4230/LIPIcs.FSCD.2017.7
; Example 13
(format MSTRS)
(sort Nat)
(sort Tree)
(fun + (-> Nat Nat Nat))
(fun s (-> Nat Nat))
(fun 0 Nat)
(fun node (-> Nat Tree Tree Tree))
(fun leaf (-> Nat Tree))
(fun sum (-> Tree Nat))
(rule (sum (leaf x)) x)
(rule (sum (node x yt zt)) (+ x (+ (sum yt) (sum zt))))
(rule (+ x 0) x)
(rule (+ x (s y)) (s (+ x y)))
(rule (node x yt zt) (node x zt yt))

Due to the type declarations, (+ 0 (leaf 0)) and (node (s x) (leaf 0) x) are ill-formed terms.

(format MSTRS)
(sort N)
(sort L)
(fun f (-> N N))
(fun g (-> L L))
(rule (f x) x)
(rule (g x) x)

In the second example, the variable x has sort N in the first rule and sort L in the second rule.