Evaluation trees for proposition algebra

TL;DR

This paper introduces evaluation trees for proposition algebra, characterizing various valuation congruences through transformations and axiomatizations, enhancing understanding of conditional statement equivalences.

Contribution

It provides a novel tree-based semantics and transformations for different valuation congruences in proposition algebra, with axiomatizations and normalization functions.

Findings

Evaluation trees characterize free valuation congruence.

Transformations on trees characterize other valuation congruences.

Axiomatizations and normalization functions are developed for each congruence.

Abstract

Proposition algebra is based on Hoare's conditional connective, which is a ternary connective comparable to if-then-else and used in the setting of propositional logic. Conditional statements are provided with a simple semantics that is based on evaluation trees and that characterizes so-called free valuation congruence: two conditional statements are free valuation congruent if, and only if, they have equal evaluation trees. Free valuation congruence is axiomatized by the four basic equational axioms of proposition algebra that define the conditional connective. Valuation congruences that identify more conditional statements than free valuation congruence are repetition-proof, contractive, memorizing, and static valuation congruence. Each of these valuation congruences is characterized using a transformation on evaluation trees: two conditional statements are C-valuation congruent if, and only if, their C-transformed evaluation trees are equal. These transformations are simple and natural, and only for static valuation congruence a slightly more complex transformation is used. Also, each of these valuation congruences is axiomatized in proposition algebra. A spin-off of our approach can be called "normalization functions for proposition algebra": for each valuation congruence C considered, two conditional statements are C-valuation congruent if, and only if, the C-normalization function returns equal images.