   Go backward to A.4 Implicit Function DefinitionsGo up to A Defining New NotionsGo forward to A.6 Evaluating Definitions ## A.5 Recursive Definitions

The definitions discussed in the previous sections are constrained by the fact that the new notion has to be defined in terms of other notions only. However, there are also situations in which it is necessary to reduce the value of a predicate or functions to other values of the same predicate or function. Such a recursive definition makes sense if this reduction does not continue forever, i.e., if eventually a situation is reached where the value can be defined directly in terms of other (previously introduced) notions.

In order to bound the number of recursive unfoldings, we introduce the following concept.

Definition 143 (Well-Founded Ordering) A binary relation < is well-founded if there is no infinitely decreasing chain with respect to < :
< is well-founded : <=> ~exists S, s: N -> S: forall i in N: s_i+1 < s_i.

We now drop the constraint that the definiens must not refer to the definiendum.

Definition 144 (Recursive Function Definition) Let f be a function constant of arity n that is not yet in use, x0, ..., xn-1 be n distinct variables, and T be a term with no other free variables than x0, ..., xn-1. Then
f(x0, ..., xn-1) := T
is a  recursive function definition (rekursive Funktionsdefinition), if there exists a well-founded ordering < with the following property: for all x0, ..., xn-1 and every occurrence of f(T0, ..., Tn-1) in T that is needed to determine the value of f(x0, ..., xn-1), we have
<T0, ..., Tn-1> < <x0, ..., xn-1>.
This definition introduces an n-ary function constant f with the axiom
forall x0, ..., xn-1: f(x0, ..., xn-1) = T.

The predicate "is needed" in above definition is a bit vague; for our purposes it suffices to state that every subterm of a term T is needed to determine the value of T, unless T is of the form

if F then T0 else T1.
In this case, only the value of T0 is needed if F is true, and only the value of T1 is needed, otherwise. A "definition" like
f(x) := 1+f(x)
can therefore not make sense because every subterm of the definiens is needed to compute the function result.

The existence of a well-founded ordering ensures that for every argument only a finite number of recursive "unfoldings" of a function definition is required to determine the function value. Frequently, such an ordering is constructed by defining a corresponding  termination function (Terminationsfunktion) r such that, for every x0, ..., xn-1,

r(x0, ..., xn-1) in N.
Then the well-founded ordering is defined as
x < y : <=> r(x) < r(y)
where < is the usual ordering of the natural numbers.

Example  We define
 any(S) := such x: x in S rest(S) := {x in S: x not = any(S)} #S := the number of elements in a finite set S.
• The recursive definition
 sum: FiniteSet -> N sum(S) := if S = 0 then 0 else any(S)+sum(rest(S))
computes the sum of the elements of a finite set of numbers S; a corresponding termination function is
r(S) := #S.
For finite S, sum(S) in N. If S = 0, no other application of `sum' is needed to determine sum(S). Otherwise, we need sum(rest(S)) with r(rest(S)) = r(S)-1 < r(S).
• The recursive definition
 *: N x N -> N x * y := if y = 0 then 0 else x + x * (y-1)
introduces multiplication over the natural numbers; a corresponding termination function is
 r(x, y) := y.
For x in N and y in N, r(x, y) in N. If y = 0, no other application of * is needed to determine x * y. If y not = 0, we need x * (y-1) with r(x, y-1) = y-1 < y = r(x, y).
• The function defined as
 dsum: FiniteSet x FiniteSet -> N dsum(A, B) := if A = 0 then any(B)+dsum(A, rest(B)) else if B = 0 then any(A)+dsum(rest(A), B) else any(A)+any(B)+dsum(rest(A), rest(B))
computes the sum of the elements of two finite sets A and B. A corresponding termination function is
 r(A, B) := #A + #B.

Logic Evaluator  We may define a function recursively by a statement

```fun f(x_0, ..., x_n-1) recursive R = T;
```
where R is a term that denotes the value of a termination function.

The evaluator checks that in every recursive invocation function this term is appropriately decreased (unless the potentially dangerous statement `option check = false` is executed).

Also a predicate can be defined in a recursive way.

Definition 145 (Recursive Predicate Definition) Let p be a predicate constant of arity n that is not yet in use, x0, ..., xn-1 be n distinct variables, and F be a formula and with no other free variables than x0, ..., xn-1. Then
p(x0, ..., xn-1) : <=> F
is a  recursive predicate definition (rekursive Prädikatsdefinition) provided that there exists a well-founded ordering < with the following property: for all x0, ..., xn-1, and every occurrence of p(T0, ..., Tn-1) in F that is needed to determine the truth value of p(x0, ..., xn-1) we have
<T0, ..., Tn-1> < <x0, ..., xn-1>.
This definition introduces an n-ary predicate constant p with the axiom
forall x0, ..., xn-1: p(x0, ..., xn-1) <=> F.

As for functions, the predicate "is needed" needs some refinement. We introduce a new kind of formula.

Definition 146 (Conditional Formula) For every formula F and terms F0 and F1, the phrase
(if F then F0 else F1)
is a formula whose truth value is the value of F0, if F holds, and the value of F1, otherwise. We omit the parentheses, if F1 is clear.

By above definition, we have the relationship

(if F then F0 else F1) <=> ((F => F0) /\  (~F => F1)).

We now state that every subformula of a formula F is needed to determine the value of F, unless F is of the form

if F then F0 else F1.
In this case, only the value of F0 is needed if F is true, and only the value of F1 is needed, otherwise.

Example
• The definition
 iseven subset N iseven(x) : <=> if x = 0 then T else ~iseven(x-1)
introduces a unary predicate on natural numbers; a corresponding termination function is
 r(x) := x.
• The definition
 <= subset N x N x <= y : <=> if x = 0 then T else if y = 0 then F else x-1 <= y-1
introduces the usual ordering on natural numbers; a corresponding termination function is
 r(x, y) := x.

Logic Evaluator  Similar to recursive function definitions, predicates may be recursively defined by a statement

```pred p(x_0, ..., x_n-1) recursive R <=> F;
```
where R is a term that denotes the value of a termination function. For writing recursive predicates, we also need the conditional formula
```if(F, F_0, F_1)
```
whose value is (if F then F0 else F1).

Reduction of Sets  Frequently functions over sets are recursively defined as follows:

 g(S) := if S = 0 then b else let e = such x: x in S: f(e, g(S-{e})).

We call this a  reduction (Reduktion) of S by f with base b. If f is commutative and associative, the result of a reduction is uniquely defined.

Example  Let S := {1, 2, 3}. Then the reduction of S by + with base 0 is
6 = (1+(2+3))+0 = (2+(1+3))+0 = (2+1)+(3+0).
The reduction of S by * with base 1 is
6 = (1*(2*3))*1 = (2*(1*3))*1 = ((1*1)*2)*3.

The Logic Evaluator provides the function

```reduce(f, S, b)
```
which returns the reduction of S by f with base b which is more efficiently evaluated than a corresponding recursive function defined by the user (compare `sum` and `sum'` in the example below).

With the help of this operator also set union and powerset can be implemented as follows:

Author: Wolfgang Schreiner
Last Modification: October 4, 1999   