Go backward to A.4 Implicit Function DefinitionsGo up to A Defining New NotionsGo forward to A.6 Evaluating 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.

<is well-founded : <=> ~existsS,s:N->S:foralliinN:s_i+1<s_i.

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

is af(x_{0}, ...,x_{n-1}) :=T

<This definition introduces anT_{0}, ...,T_{n-1}><<x_{0}, ...,x_{n-1}>.

forallx_{0}, ...,x_{n-1}:f(x_{0}, ...,x_{n-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

In this case, only the value ofifFthenT_{0}elseT_{1}.

can therefore not make sense because every subterm of the definiens is needed to compute the function result.f(x) := 1+f(x)

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 `x`_{0}, ..., `x`_{n-1},

Then the well-founded ordering is defined asr(x_{0}, ...,x_{n-1}) inN.

where < is the usual ordering of the natural numbers.x<y: <=>r(x) <r(y)

any( S) :=suchx:xinSrest( S) := {xinS:xnot = any(S)}# S:= the number of elements in a finite setS.

- The recursive definition

computes the sum of the elements of a finite set of numberssum: FiniteSet -> **N**sum( `S`) :=**if**`S`=**0****then**0**else**any(`S`)+sum(rest(`S`))`S`; a corresponding termination function is`r`(`S`) := #`S`.`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

introduces multiplication over the natural numbers; a corresponding termination function is*: **N**x**N**->**N**`x`*`y`:=**if**`y`= 0**then**0**else**`x`+`x`* (`y`-1)

For`r`(`x`,`y`) :=`y`.`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

computes the sum of the elements of two finite setsdsum: 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`))`A`and`B`. A corresponding termination function is`r`(`A`,`B`) := #`A`+ #`B`.

**Logic Evaluator** We may define a function recursively
by a statement

wherefunf(x_0, ...,x_n-1) recursiveR=T;

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.

is ap(x_{0}, ...,x_{n-1}) : <=>F

<This definition introduces anT_{0}, ...,T_{n-1}><<x_{0}, ...,x_{n-1}>.

forallx_{0}, ...,x_{n-1}:p(x_{0}, ...,x_{n-1}) <=>F.

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

(is a formula whose truth value is the value ofifFthenF_{0}elseF_{1})

By above definition, we have the relationship

(ifFthenF_{0}elseF_{1}) <=> ((F=>F_{0}) /\ (~F=>F_{1})).

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

In this case, only the value ofifFthenF_{0}elseF_{1}.

- The definition

introduces a unary predicate on natural numbers; a corresponding termination function isiseven subset **N**iseven( `x`) : <=>**if**`x`= 0**then**T**else**~iseven(`x`-1)`r`(`x`) :=`x`. - The definition

introduces the usual ordering on natural numbers; a corresponding termination function is<= subset **N**x**N**`x`<=`y`: <=>**if**`x`=`0`**then**T**else****if**`y`=`0`**then**F**else**`x`-1 <=`y`-1`r`(`x`,`y`) :=`x`.

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

wherepredp(x_0, ...,x_n-1) recursiveR<=>F;

whose value is (if(F,F_0,F_1)

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

g(S) :=ifS=0thenbelselete=suchx:xinS: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.

6 = (1+(2+3))+0 = (2+(1+3))+0 = (2+1)+(3+0).The reduction of

6 = (1*(2*3))*1 = (2*(1*3))*1 = ((1*1)*2)*3.

The Logic Evaluator provides the function

which returns the reduction ofreduce(f,S,b)

`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