2 Partial recursive functions through free extensions

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² 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.

Predicates are omitted, since they are not there in usual functional programming languages (and initial semantics also covers semi-decidable predicates that cannot be implemented as functions to bool). Structured specifications (apart from free extensions which is the minimum that is needed to simulate fixed-point semantics) are omitted because functional programming languages have structuring mechanisms different from those of CASL. Architectural specifications of course should correspond in some way to structuring mechanisms in programming languages, but this is orthogonal to the subject of this note.

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