Behavioural constructor implementation for regular algebras

Abstract

We investigate regular algebras, admitting infinitary regular terms interpreted as least upper bounds of suitable approximation chains. The main result of this paper is an adaptation of the concept of behavioural constructor implementation, studied widely e.g. for standard algebras, to the setting of regular algebras. We formulate moreover a condition that makes proof of correctness of an implementation step tractable. In particular, we indicate when it is sufficient to consider only finitary observational contexts in the proofs of behavioural properties of regular algebras.