2.9.4 Miscellaneous Differences from OBJ3

1. True rewriting modulo identity is implemented rather than the restricted version done by OBJ3; this leads to nontermination more often.
2. The attribute idr: is not recognized.
3. Maude allows arbitrary forward references to sorts, variables and operators within a module. The order of statements in a module is irrelevant, except, possibly, on error messages, importations, and nonconfluent systems.
4. Identities are not restricted to being constants; an identity may be any ground term that does not have the parent operator on top. Cyclic dependencies between two or more identity elements is explicitly allowed and is correctly resolved by the matching algorithms.
5. The attribute idem means rewriting modulo idempotence, rather than adding the equation for idempotence.
6. The lefthand side of an equation can be a single variable; this often (but not always) leads to nontermination.
7. Error supersorts are used instead of retracts; this is due to the use of membership equational logic, so that the error supersorts exactly correspond to kinds.
8. Operator strategies available with the strat attribute do not support negative integers (evaluate on demand) and are restricted to a subset of "sensible" strategies that depend on the operator's other attributes. Various OBJ3 strategy bugs are not emulated [21].
9. Operators which have the assoc attribute may be used in "flattened" form, e.g., f(a, b, c) instead of f(a, f(b, c)) or f(f(a, b), c).
10. Operators may always be used in prefix form, e.g., if_then_else_fi(b, t, e) instead of if b then t else e fi.
11. Labeled equations are not supported (use labeled rules).
12. Sort declarations of operators with assoc, comm, id: and idem attributes must respect those attributes: rearrangement or permutation by associativity or commutativity must not change the sort of a term, while collapse due to identity or idempotence must either lower the sort of a term or leave it unchanged.
13. There is no support for Lisp--the Maude interpreter is written in C++.