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 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 unique3 model of the specification is isomorphic to (a suitable abstraction of4) 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.