Prev Up Next
Go backward to 2 Partial recursive functions through free extensions
Go up to Top
Go forward to 4 Conclusion

3 Total recursive functions through termination proofs

Usually, one does not exploit the full power of programming languages by writing partial recursive functions, but rather all functions are total (in most cases even primitive recursive). Moreover, the equations defining a total function in a functional programming language often directly lead to a loose specification having the (abstracted) meaning of the program as its unique model (up to isomorphism).

 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          ::=  total-op-type   SORTS SORT
                    |  partial-op-type SORTS SORT
 SORTS            ::=  sorts SORT*
 OP-HEAD          ::=  total-op-head   ARG-DECL* SORT
                    |  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 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+

We additionally introduce the following restrictions, very similar as above:

The main difference to P-REC is that we have dropped freeness. Instead, we require all operations to be completely specified and to be total6. Totality is guaranteed by termination of the induced term rewriting system. Completeness and totality imply that the specification has a unique model up to isomorphism, and moreover, that this model is isomorphic to the (abstracted) denotation of the corresponding functional program.

Now termination of a term rewriting is not decidable. So we have not defined a useful sublanguage of CASL, since membership in the sublanguage is not decidable. There are several possibilities to overcome this

Note that confluence is not a problem here, because the specifications in the "total recursive" sublanguage lead to orthogonal (i.e. left-linear, non-overlapping) term rewriting systems, which are always confluent.

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

Prev Up Next