BASIC-SPEC ::= basic-spec BASIC-ITEMS* BASIC-ITEMS ::= SIG-ITEMS | var-items VAR-DECL+ | local-var-axioms VAR-DECL+ FORMULA+ | axiom-items FORMULA+ | free-datatype DATATYPE-DECL+ SIG-ITEMS ::= op-items OP-ITEM+ OP-ITEM ::= op-decl OP-NAME+ OP-TYPE | op-defn OP-NAME OP-HEAD TERM OP-TYPE ::= total-op-type SORTS SORT | partial-op-type SORTS SORT SORTS ::= sorts SORT* OP-HEAD ::= total-op-head ARG-DECL* SORT | partial-op-head ARG-DECL* SORT ARG-DECL ::= arg-decl VAR+ SORT DATATYPE-DECL ::= datatype-decl SORT ALTERNATIVE+ ALTERNATIVE ::= total-construct OP-NAME COMPONENTS* COMPONENTS ::= partial-select SORT VAR-DECL ::= var-decl VAR+ SORT FORMULA ::= quantification QUANTIFIER VAR-DECL+ strong-equation TERM TERM QUANTIFIER ::= forall TERMS ::= terms TERM* TERM ::= VAR-OR-CONST | qual-var VAR SORT | application OP-SYMB TERMS | sorted-term TERM SORT OP-SYMB ::= OP-NAME | QUAL-OP-NAME QUAL-OP-NAME ::= qual-op-name OP-NAME OP-TYPE SORT ::= ID OP-NAME ::= ID VAR ::= SIMPLE-ID VAR-OR-CONST ::= SIMPLE-ID ID ::= SIMPLE-ID SIMPLE-ID ::= ... SPEC-DEFN ::= spec-defn SPEC-NAME SPEC SPEC ::= BASIC-SPEC | extension SPEC+

We additionally introduce the following restrictions, very similar as above:

- The head operation symbol (i.e. the outermost operation symbol of the left hand side) of each equation must not be a constructor or selector symbol, nor a operation symbol from an operation definition.
- For each operation symbol at most one operation definition is allowed.
- For each operation symbol, consider the set of equations which have
it as their head operation symbol. The left hand sides
of all the equations must not overlap
and must (apart
from the head operation symbol) consist entirely of
variables and constructor symbols. Moreover, the set of
left hand-sides must be complete
^{5} - All equations must be left-linear, that is, no variable may occur twice in a left hand-side.
- The term rewriting system induced by the equations must be terminating.

The main difference to *P-REC* is that we have dropped freeness.
Instead, we require all operations to be completely specified
and to be total^{6}.
Totality is guaranteed by termination of the induced term
rewriting system. Completeness and totality imply
that the specification has a unique model up to isomorphism,
and moreover, that this model is isomorphic to the
(abstracted) denotation of the corresponding functional
program.

Now termination of a term rewriting is not decidable. So we have not defined a useful sublanguage of CASL, since membership in the sublanguage is not decidable. There are several possibilities to overcome this

- Require the specification to consist only of primitive recursive definitions (or some extension of the primitive recursive formalism that guarantees totality).
- Allow the user to specify a well-founded ordering on terms such that the equations are decreasing w.r.t. this ordering.
- Allow the user to specify an ordering on the operation symbols that leads to a well-founded recursive path ordering.
- Automatically compute an ordering on the operation symbols that leads to a well-founded recursive path ordering, and accept only those specifications for which this computation succeeds.

Note that confluence is not a problem here, because the specifications in the "total recursive" sublanguage lead to orthogonal (i.e. left-linear, non-overlapping) term rewriting systems, which are always confluent.

CoFI Note: L-9 --Version 1.0-- 21 March 1998.

Comments to till@informatik.uni-bremen.de