On the Axiomatization of “If-Then-Else”
Irène Guessarian, José Meseguer · SIAM Journal on Computing · 1987
The equationally complete proof system for “if-then-else” of Bloom and Tindell (this Journal, 12(1983), pp. 677–707) is extended to a complete proof system for many-sorted algebras with extra operations, predicates and equations among those. We give similar completeness results for continuous algebras and program schemes (infinite trees) by the methods of algebraic semantics. These extensions provide a purely equational proof system to prove properties of functional programs over user-definable data types.