It is well known that initial algebra semantics is sufficient to express all partial recursive functions over the usual data types. Since we want to map our specifications to functional programs, we have to require that all sorts are free datatypes. Over these data types, we can specify partial recursive functions by strong equations which specify the value of a function for each of the different constructors in an unambiguous way.

Consider the following restriction of the CASL grammar:

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 ::= partial-op-type SORTS SORT SORTS ::= sorts SORT* OP-HEAD ::= 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 OP-NAME+ 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+ | free-spec SPEC

We further introduce the following restrictions:

- 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
^{2}and must (apart from the head operation symbol) consist entirely of variables and constructor symbols. - All equations must be left-linear, that is, no variable may occur twice in a left hand-side.
- The free datatype declarations must not occur within the scope of a freeness, while all other basic items must occur within the scope of a freeness.

The grammar together with the restrictions determine a sublanguage of CASL,
call it *P-REC*.
For the specifications of this sublanguage, there is an obvious
translation to any of the popular functional programming languages,
with the property that the unique^{3}
model of the specification
is isomorphic to (a suitable abstraction of^{4})
the denotation of the program. A proof of this would exploit
the fact that both free extension semantics of specifications
in *P-REC* and least fixed-point semantics of functional
programs follow the principle of minimal definedness.

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

Comments to till@informatik.uni-bremen.de