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 main difference to P-REC is that we have dropped freeness. Instead, we require all operations to be completely specified and to be total6. 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
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.