I hope the ideas in this paper will lead to clearer languages and documentation. All language reference manuals use some kind of Backus-Naur form (BNF) grammar to define syntax. Hardly any provide formal semantics. People have proposed operational, axiomatic, and denotational methods. None has become popular. This paper extends Dijkstra’s work on predicate transformers. These are a form of axiomatic semantics. They help programmers construct correct programs. This paper extends predicate transformers to work on general expressions or terms. For example, an assignment such as x:=x+1; has a term transformer that maps the expression x × y into (x+1) × y.

This paper presents a logic of phrases that includes term transformers. It attempts to explain the theory. The confusing initial examples do not help. Delayed definitions make it even worse. For example, defining T as including the maps T→T allows paradoxes. But this possibility is excluded in an appendix where the maps must be monotonic. The middle of the paper proves results. The appendices state the axioms. Readers need to understand Dijkstra’s work, the lambda calculus, and formal logic. Perhaps they should start with the appendices. Farmer and von Mohrenschildt [1] define a different kind of term transformer using von Neumann-Bernays-Gödel set theory. They aim to improve theorem provers. They do not develop them in the direction of semantics. Somebody should introduce these two teams of researchers. Term transformers are worthy of study and application. These papers are a good start. Morris et al. promise a sequel, applying them to define a real language.