Introduction
How to use CafeOBJ processor: Start and Quit; Describing specifications; Reading specifications
Fundamentals of CafeOBJ: Comments; Modules; Sorts; Imports; Operators; Equations; Variables; Show; Parse; Reduce
Verification with proof scores: Proof scores; Equality predicate =; Associativity of +; Commutativity of +
Appendix: Troubleshooting; Built-in modules; Exercises

Operators

An operator is declared with the keyword op:

op <op-name> : <arity> -> <sort-of-op> { <operator-attribute> }

The name of the operator is written in <op-name>. The arity and the the coarity of the operator are written in <arity> and <sort-of-op> respectively. An arity is a sequence of sorts and a coarity is a single sort. An operator takes a list of elements according to its arity and returns an element of its coarity. A pair of the arity and the coarity is called the rank. Operator attributes will be explained later.

Operators which have exactly the same rank can be declared with ops simultaneously.

ops <op-name> ... <op-name> : <arity> -> <sort-of-op> { <operator-attribute> }

In CafeOBJ, places of arguments of operators can be designated by underbars. Operators including underbars are called mix-fix operators. For example, _+_ is an infix operator. Mix-fix operators give us a way to declare more flexible argument positions like while_do_od.

Examples:

** Constants (The arity is empty)
ops true false : -> Bool

** Infix operator
op _+_ : Nat Nat -> Nat

** Mix-fix operator
op if_then_else_if : Bool Exp Exp -> Exp

** Juxtaposition ('e1 e2 e3 ... en nil' can be a term of Sequence)
op __ : Elt Sequence -> Sequence

Operator attributes

Operators can be declared with attributes. There are several useful attributes.

assoc : Associativity
comm : Commutativity
idem : Idempotency
idr: <op-name> : identity
r-assoc : Right-assosiativity (for parsing terms)
l-assoc : Left-assosiativity (for parsing terms)
prec: <precedence> : Precedence (for parsing terms. Larger integer, stronger connectivity)
strat: (<e-strategy>) : Strategy (for reducing terms)

See CafeOBJ manual for more details.

For example, the associative and commutative operator + in NAT+ can be declared as follows:

mod! NAT+AC {
  pr(NAT+)
  op _+_ : Nat Nat -> Nat { assoc comm }
}

Module NAT+AC denotes the same model with the module obtained by adding the equations eq (X + Y) + Z = X + (Y + Z) . and eq X + Y = Y + X . to NAT+.

[Next] Equations