Formal Description  

Call Matrix

Be R = {` < ',` = ',`?'} set of the relations ``less than'', ``equal to'' and ``relation unknown''. In the context of `` f (x,y) calls g(a,b) '' a ` < ' y means ``we know that (call) argument a is less than (input) parameter y '', a ` = ' y means `` a is (at least) equal to y (if not less than)'' and a `?' y means ``we do not know the relation between a and y ''.

With the two operations + and $\cdot$ 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 $\cdot$ however is ``serial combination'', e.g. a ` < ' y and y ` = ' z can be combined into a (` < ' $\cdot$ ` = ') z , simplified: a ` < ' z . `?' is neutral regarding + because it gives you no new information, whereas ` < ' is dominant because it is the strongest information. Regarding $\cdot$ the relation ` = ' is neutral and `?' is dominant because it ``destroys'' all information. Check the table to see which relation overrides which.

 

+ ` < ' ` = ' `?'

` < ' ` < ' ` < ' ` < '

` = ' ` < ' ` = ' ` = '

`?' ` < ' ` = ' `?'

$$\cdot$$ ` < ' ` = ' `?'

` < ' ` < ' ` < ' `?'

` = ' ` < ' ` = ' `?'

`?' `?' `?' `?'

 

Now we can define multiplication on matrices over R as usual:

$$\cdot$$ : R ^{n x m} x R ^{m x l} $$\rightarrow$$ R ^{n x l}

$$\left((a_{ij}), (b_{ij})\right)\mapsto$$(c_ij) = $$\left( \sum_{k=1}^m a_{ik} b_{kj} \right)$$

Why is this a reasonable definition? Assume you have three sets of variables {x₁,...,x_n} , {y₁,...,y_m} and {z₁,...,z_l} , a matrix A = (a_ij) $\epsilon$ R ^{n x m} reflecting the relations between the x_i s and the y_i s (i.d. a_ij = $\rho$$\iff$x_i $\rho$ y_j ) and a matrix B $\epsilon$ R ^{m x l} reflecting the relations between the y_i s and the z_i s. Then the matrix product C = AB reflects the relations between the x_i s and the z_i s. Because

c_ij = a_i1 $$\cdot$$ b_1j + a_i2 $$\cdot$$ b_2j + ... + a_im $$\cdot$$ b_mj,

we have e.g. x_i ` < ' z<sub>j</sub> if we know it by intermediate variable y<sub>1</sub> ( a<sub>i1</sub> $\cdot$ b<sub>1j</sub> = ` < ' ) or by intermediate variable y₂ or ... (to be continued).

Definition.

A call matrix is a matrix over R with no more than one element different from `?' per row.

CM(n,m) : = {(a_ij) $$\epsilon$$ R ^{n x m} : $$\forall$$i$$\forall$$j$$\forall$$k $$\not=$$j(a_ij = `?'$$\lor$$a<sub>ik</sub> = `?')}

Remark.

The reason we define call matrices this way is these are the only ones foetus produces by function call extraction (see section 4.1). Because foetus recognizes only the three described cases of dependecies, a call argument can only depend of one function parameter. But multiple dependecies are imaginable, like in

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.

Proposition.

Matrix multiplication on matrices induces a multiplication on call matrices

$$\cdot$$ : CM(n,m) x CM(m,l ) $$\rightarrow$$ CM (n,l )

This operation is well defined.

Proof.

Be A = (a_ij) $\epsilon$ CM (n,m) , B = (b_ij) $\epsilon$ CM (m,l ) , AB = C = (c_ij) $\epsilon$ R ^{n x l} and k(i) the index of the element of the i th row of A that is different to `?' (or 1, if no such element exists). The we have with the rules in rig R

c_ij = $$\sum_{k=1}^{m}$$a_ikb_kj = a_i,k(i)b_k(i),j

Now consider the i th row of C :

c_i = (c_ij)_{1 $\leq$ j $\leq$ l} = (a_i,k(i)b_k(i),j)_{1 $\leq$ j $\leq$ l}

Because at most one b_k(i),j is unequal to `?' , at most one element of c<sub>i</sub> is unequal to `?' . Therefore C $\epsilon$ CM (n,l ) .

Call Graph

For each i $\epsilon$ N we assume a set F ⁽ⁱ⁾ = {f ⁽ⁱ⁾,g ⁽ⁱ⁾,h ⁽ⁱ⁾,...} of identifiers for functions of arity i , $\mathcal {F}$ = $\biguplus_{i \,\epsilon\,\mathbf{N}}^{}$F ⁽ⁱ⁾.

Definition.

We form the set of calls as follows

$$\mathcal {C}$$ = {(f ⁽ⁿ⁾,g ^(m),A) : f ⁽ⁿ⁾ $$\epsilon$$ F ⁽ⁿ⁾,g ^(m) $$\epsilon$$ F ^(m),A $$\epsilon$$ CM(m,n)}

On calls we define the partial operation combination of calls

o : $$\mathcal {C}$$ x $$\mathcal {C}$$ $$\rightarrow$$ $$\mathcal {C}$$

$$\left( (g^{(m)}, h^{(l)}, B), (f^{(n)}, g^{(m)}, A) \right)\mapsto$$(f ⁽ⁿ⁾,h ^(l),BA)

Meaning: If g calls h with call matrix B and f calls g with call matrix A , then f indirectly calls h with call matrix BA . o cannot be applied to calls that have no ``common function'' like g , therefore it is partial. o can be expanded to sets of calls

o : $$\mathcal {P}$$($$\mathcal {C}$$) x $$\mathcal {P}$$($$\mathcal {C}$$) $$\rightarrow$$ $$\mathcal {P}$$($$\mathcal {C}$$)

(C,C') $$\mapsto$$ {c o _{$\mathcal {C}$}c' : c $$\epsilon$$ C,c' $$\epsilon$$ C',(c,c') $$\epsilon$$ Dom( o _{$\mathcal {C}$})}

Here we combine each call in C with each call in $\hat{C}$ to which o _{$\mathcal {C}$} is applicable and form a set of the combined calls. o _{$\mathcal {P}$($\mathcal {C}$)} is a total function.

Definition.

A call graph is a graph (V,E) with vertices V = $\mathcal$F and edges E $\subset_{\mathrm{finit}}^{}$ $\mathcal {C}$ . A call graph is complete if

E o E $$\subseteq$$ E

Definition.

The completion of a call graph (V,E) is a call graph (V,E') such that

1.

(V,E') is complete, 

2.

E $\subseteq$ E' and 

3.

for all E'' satisfying (1) and (2) we have E' $\subseteq$ E'' .

Proposition.

The completion of a call graph (V,E) is the call graph (V,E') such that

c $$\epsilon$$ E'$$\iff$$$$\exists$$n > 0,c₁,...,c_n $$\epsilon$$ E : c₁ o ... o c_n = c

Proof.

1.

Be c $\epsilon$ E' o E' . Then there are d,e $\epsilon$ E' with c = d o e . Because (V,E') is complete, we have

$$\qquad \epsilon$$ d = d₁ o ... o d_n

$$\qquad \epsilon$$ e = e₁ o ... o e_m

Thus c = d₁ o ... o d_n o e₁ o ... o e_m $\epsilon$ E' .

2.

E $\subseteq$ E' is trivial with n = 1 .

3.

Be (V,E'') complete and E $\subseteq$ E'' . This gives us E o E $\subseteq$ E'' from which we gain by induction

$$\underbrace{E \circ \dots \circ E}_{n\mathrm{-times}}^{}$$ = : E ⁿ $$\subseteq$$ E''    for   all   n.

Now be c $\epsilon$ E' . That implies c = c₁ o ... o c_n ( c_i $\epsilon$ E ) for a suitable n . Hence c $\epsilon$ E ⁿ $\subseteq$ E'' . q $\cdot$ e $\cdot$ d

Proposition. (Completion algorithm)

Be (V,E) a call graph, (V,E') its completion and (E_n)_{n $\epsilon$ N} a sequence of sets of calls defined as follows:

E₀ = E

$$\cup$$ E_{n + 1} =

Then there is a n $\epsilon$ N so that

E' = E_n = E_{n + 1} = E_{n + 2} = ...

(Obviously the E_n grow monotonously.)

Proof.

First we show by induction that E_n $\subseteq$ E' for all n $\epsilon$ N : It is obvious that E₀ $\subseteq$ E' . Now be E_n $\subseteq$ E' and c $\epsilon$ E_{n + 1} $\setminus$ E_n . Then c $\epsilon$ E_n o E , therefore c = d₁ o ... o d_n o e , d₁,...,d_n,e $\epsilon$ E . It follows c $\epsilon$ E' , E_{n + 1} $\subseteq$ E' .

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 E_i s cannot grow endlessly. Thus an n $\epsilon$ N exists with E_n = E_{n + 1} .

Third: We show that E' $\subseteq$ E_n for that particular n . Be c $\epsilon$ E' . Then there exists an m such that c = d₁ o ... o d_m , therefore c $\epsilon$ E_m . Now if m $\leq$ n then E_m $\subseteq$ E_n , otherwise m > n and hence E_m = E_n , in both cases c $\epsilon$ E_n . q $\cdot$ e $\cdot$ d

Lexical Order

Definition.

Be (V,E) a complete call graph and f ⁽ⁱ⁾ a function of arity i . We call

E_f⁽ⁱ⁾ : = {$$\Delta$$(C) : (f ⁽ⁱ⁾,f ⁽ⁱ⁾,C) $$\epsilon$$ E} $$\subset$$ R ⁱ

the recursion behaviour of function f ⁽ⁱ⁾. ( $\Delta$ takes the diagonal of square matrices).

Each row of this set represents one possible recursive call of f ⁽ⁱ⁾ 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 ⁽ⁱ⁾. E_f⁽ⁱ⁾ of course is a finite subset of R ⁱ.

In the following we identify lexical orders on parameters with permutations $\pi$ $\epsilon$ S_n 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

$$\pi_{1}^{}$$ = $$\left(\begin{array} {ccc}0&1&2\ 0&1&2\end{array}\right)$$

and

$$\pi_{2}^{}$$ = $$\left(\begin{array} {ccc}0&1&2\ 0&2&1\end{array}\right)$$

are valid continuations of the lexical order ``0''.

Note:

In the following we abbreviate the notation of permutations to $\pi_{1}^{}$ = [012] and $\pi_{2}^{}$ = [021] .

Definition. (1)

Be B the recursion behaviour of function f ⁽ⁿ⁾. We call the permutation $\pi$ $\epsilon$ S_n a termination order for f ⁽ⁿ⁾ if

$$\forall$$r $$\epsilon$$ B$$\exists$$1 $$\leq$$ k $$\leq$$ n : r_$\pi$(k) = ` < '$$\land$$($$\forall$$1 $$\leq$$ i $$\leq$$ k : r<sub>$\pi$(i)</sub> = ` = ')

This definition is a very wide one. In most cases you will look for more special termination orders:

Definition. (2, inductive)

Be B the recursion behaviour of a given function. We call the permutation $\pi$ $\epsilon$ S_n a termination order on B if |B| = 0 or

$$\exists \epsilon \pi$$

$$\land \not\exists \epsilon \pi$$

$$\land \pi \epsilon \pi \pi \not= \subset$$

whereas $\pi$'_i = [k₀...k_{i - 1}k_{i + 1}...k_{n - 1}] $\epsilon$ S_{n - 1} given $\pi$ = [k₀...k_{n - 1}] $\epsilon$ S_n and r'_i = (k₀,...,k_{i - 1},k_{i + 1},...,k_{n - 1}) $\epsilon$ R ^{n - 1} given r = (k₀,...,k_{n - 1}) $\epsilon$ R ⁿ.

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 $\pi_{1}^{}$ = [012] is a type (1) termination order on E and $\pi_{2}^{}$ = [120] is of both types.