Programs as term transformers

Abstract

Predicates describing the states of computation may be regarded as functions into the Boolean algebra {false, true} and programs as transformers of those functions. If we do not restrict ourselves to this algebra, we get instead terms describing the states of computation and programs transforming the terms. In many cases this approach turns out to be more natural. This paper is a mathematical study of partial correctness and termination of programs in the language of term transformations.