UNIQUENESS OF SOLUTION OF FIXED POINT EQUATIONS IN REGULAR EXTENSIONS OF ITERATIVE ALGEBRAS

Two approaches to the semantics of programming languages using fixed points have been investigated for a number of years.

The first approach deals with least fixed points of continuous mappings defined on complete posets and it has been extensively studied by D. Scott, M. Nivat and J. W. Thatcher, among others.

The second approach, based on the existence and uniqueness of fixed points of certain maps, was introduced by C. C. Elgot.

The two approaches were compared by J. Tiuryn, who proved the existence of extensions of algebras with the unique fixed point property (iterative algebras) to ordered algebras with the least fixed point property (regular algebras), extensions preserving the fixed point solutions.

Given an iterative algebra A, the construction of the extension is carried out by considering the algebra R(,(SIGMA))(A) of all (SIGMA)(A)-trees of finite index and defining on it two successive equivalence relations, =(,A) and =(omega)(,1) . A* = R(,(SIGMA))(A)/=(,A) and A(,R) = A*/=(omega)(,1) are obtained using the two relations: A(,R) is the sought extension of A, which coincides with A* whenever the extension is "faithful", that is obtained without collapsing elements of the carrier A.

It had been conjectured that both A* and A(,R) are again iterative algebras.

My dissertation shows that A* is again iterative, while J. Tiuryn has constructed an iterative algebra A whose regular extension A(,R) is not iterative.

The positive answer provides us with a method for extending iterative algebras to iterative regular algebras, where every nontrivial algebraic system of fixed point equations has a unique solution which can furthermore be generated by taking the least upper bound of an increasing sequence of successive approximations.

The dissertation also extends this result to a more general situation.

Given an iterative algebra A, let K(,1) be a congruence relation on(, )

R(,(SIGMA))(A), the (SIGMA)-algebra of all totally defined regular trees on (SIGMA)(A). Let

r = (r(,1),...,r(,n)) and s = (s(,1),...,s(,n)) and define

K(,2) = {(q{r},q{s}) : q(ELEM)R(,(SIGMA))(X(,n)),(r(,i),s(,i))(ELEM)K(,1) for i = 1,...,n}.

Theorem. If R(,(SIGMA))(A)/K(,1) is iterative, then R(,(SIGMA))(A)/K(,2) is iterative.