| An Algebraic Construction of Predicate Transformers (1994) | |||||||||||||||||
Abstract | |||||||||||||||||
| . In this paper we present an algebraic construction of monotonic predicate transformers, using a categorical construction which is similar to the algebraic construction of the integers from the natural numbers. When applied to the category of sets and total functions once, it yields a category isomorphic to the category of sets and relations; a second application yields a category isomorphic to the category of monotonic predicate transformers. This hierarchy cannot be extended further: the category of total functions is not itself an instance of the categorical construction, and can only be extended by it twice. 1 Introduction Predicate transformers were introduced originally by Dijkstra [8] in order to provide an elegant semantics for his programming language. Their strength lies in the fact that they can be used to model non-deterministic and non-terminating behaviour in terms of total functions, rather than relations. Not all monotonic predicate transformers represent programs in ... | |||||||||||||||||
Publication details | |||||||||||||||||
| |||||||||||||||||