Go backward to 1 Introduction
Go up to Top
Go forward to 3 Total recursive functions through termination proofs

# 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-TYPE          ::=  partial-op-type SORTS SORT
SORTS            ::=  sorts 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 overlap2 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 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.

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