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-TYPE          ::=  total-op-type   SORTS SORT
|  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 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 complete5
• 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 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

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