Go backward to A.4 Implicit Function Definitions
Go up to A Defining New Notions
Go forward to A.6 Evaluating Definitions
|
Go backward to A.4 Implicit Function Definitions Go up to A Defining New Notions Go 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 : <=> ~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.
f(x0, ..., xn-1) := Tis 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.
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.
computes the sum of the elements of a finite set of numbers S; a corresponding termination function is
sum: FiniteSet -> N sum(S) := if S = 0 then 0 else any(S)+sum(rest(S))
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).
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 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).
r(x, y) := y.
computes the sum of the elements of two finite sets A and B. A corresponding termination function is
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))
r(A, B) := #A + #B.
Logic Evaluator We may define a function recursively by a statement
where R is a term that denotes the value of a termination function.fun f(x_0, ..., x_n-1) recursive R = 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.
p(x0, ..., xn-1) : <=> Fis 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.
(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.
introduces a unary predicate on natural numbers; a corresponding termination function is
iseven subset N iseven(x) : <=> if x = 0 then T else ~iseven(x-1)
r(x) := x.
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
where R is a term that denotes the value of a termination function. For writing recursive predicates, we also need the conditional formulapred p(x_0, ..., x_n-1) recursive R <=> F;
whose value is (if F then F0 else F1).if(F, F_0, F_1)
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.
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
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 (comparereduce(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: