Prev Up Next
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*

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

 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:

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.
Comments to

Prev Up Next