With the two operations
+ and defined as in table 1 R forms a
commutative
rig
with 0-element `?' and 1 -element ` = ' . The operation + can be
understood as ``combining parallel information about a relation'',
e.g. if we have a `?' y and
a ` < ' y we have
a (`?' + ` < ') y and that simplifies to
a ` < ' y .
The operation
however is ``serial combination'', e.g.
a ` < ' y
and
y ` = ' z can be combined into
a (` < '
` = ') z ,
simplified:
a ` < ' z . `?' is neutral regarding + because
it gives you no new information, whereas ` < ' is dominant because
it is the strongest information. Regarding
the relation
` = ' is neutral
and `?' is dominant because it ``destroys'' all
information. Check the table to see which relation overrides which.
+ | ` < ' | ` = ' | `?' |
` < ' | ` < ' | ` < ' | ` < ' |
` = ' | ` < ' | ` = ' | ` = ' |
`?' | ` < ' | ` = ' | `?' |
![]() |
` < ' | ` = ' | `?' |
` < ' | ` < ' | ` < ' | `?' |
` = ' | ` < ' | ` = ' | `?' |
`?' | `?' | `?' | `?' |
Now we can define multiplication on matrices over R as usual:
: R n x m x R m x l
R n x l
(cij) =
cij = ai1 b1j + ai2
b2j + ... + aim
bmj,
CM(n,m) : = {(aij) R n x m :
i
j
k
j(aij = `?'
aik = `?')}
f(x,y) = if (x=0) then 0 else let a=min(x,y)-1 in f(a,x)Here the second call argument a is less than both x and y. The next proposition assures that all matrices foetus will have do deal with are call matrices.
: CM(n,m) x CM(m,l )
CM (n,l )
cij = aikbkj = ai,k(i)bk(i),j
ci = (cij)1 j
l = (ai,k(i)bk(i),j)1
j
l
= {(f (n),g (m),A) : f (n)
F (n),g (m)
F (m),A
CM(m,n)}
o : x
(f (n),h (l),BA)
o : (
) x
(
)
(
)
(C,C') {c o
c' : c
C,c'
C',(c,c')
Dom( o
)}
E o E E
c E'
n > 0,c1,...,cn
E : c1 o ... o cn = c
d = d1 o ... o dn |
![]() |
d1,...,dn ![]() | |
e = e1 o ... o em |
![]() |
e1,...,em ![]() |
= : E n
E'' for all n.
E0 | = | E | |
En + 1 | = |
En ![]() |
E' = En = En + 1 = En + 2 = ...
(Obviously the En grow monotonously.)
Second: Because we have a finit set of starting edges E and
therefore a finit set of reachable vertices and also a finit set of
possible edges between two vertices (limited by the number of
different call matrices of fixed dimensions) the Ei s cannot grow
endlessly. Thus an
n N exists with
En = En + 1 .
Third: We show that
E' En for that particular n . Be
c
E' . Then there exists an m such that
c = d1 o ... o dm , therefore
c
Em . Now if m
n then
Em
En , otherwise m > n and hence Em = En , in both cases
c
En .
q
e
d
Ef(i) : = {(C) : (f (i),f (i),C)
E}
R i
Each row of this set represents one possible recursive call of f (i) and how the orders of all parameters are altered in this call. The diagonals of the call matrices are taken because we want to know only how a parameter relates to its old value in the last call to f (i). Ef(i) of course is a finite subset of R i.
In the following we identify lexical orders on parameters with
permutations
Sn of the arguments. Often not all of the
parameters are relevant for termination; these are not listed in the
lexical order and can appear in the permutation in any sequence.
In example 3.11 (fib') only the argument 0 has to be considered to prove termination, the order of argument 1 and 2 are irrelevant and therefore both permutations
=
=
r
B
1
k
n : r
(k) = ` < '
(
1
i
k : r
(i) = ` = ')
This definition is a very wide one. In most cases you will look for more special termination orders:
![]() ![]() ![]() | |||
![]() ![]() ![]() ![]() | |||
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
The algorithm implemented in foetus searches termination orders like in definition (2); it is a one-to-one transfer of this definition. Every termination order matching definition (2) also matches definition (1) and it can easily be shown that if there is a termination order of type (1) there also exists on of type (2).
Example 2986
Be
E = {(` = ',` < ',`?'),(` = ',` = ',` < '),(` = ',` < ',` = ')} the given recursion behaviour. Then
= [012] is a type (1) termination order on E and
= [120] is of
both types.