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*

 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          ::=  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 
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+

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

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. Moreover, the set of left hand-sides must be complete⁵
All equations must be left-linear, that is, no variable may occur twice in a left hand-side.
The term rewriting system induced by the equations must be terminating.

The main difference to P-REC is that we have dropped freeness. Instead, we require all operations to be completely specified and to be total⁶. 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

Require the specification to consist only of primitive recursive definitions (or some extension of the primitive recursive formalism that guarantees totality).
Allow the user to specify a well-founded ordering on terms such that the equations are decreasing w.r.t. this ordering.
Allow the user to specify an ordering on the operation symbols that leads to a well-founded recursive path ordering.
Automatically compute an ordering on the operation symbols that leads to a well-founded recursive path ordering, and accept only those specifications for which this computation succeeds.

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 till@informatik.uni-bremen.de