命题代数的评估树
Evaluation trees for proposition algebra
AI总结：
本文研究命题代数中基于评估树的条件语句等价关系，定义了四种不同的估值同余关系，并通过转换规则进行形式化。
摘要：
命题代数基于霍尔的条件连接词，是一种与if-then-else类似的三元连接词。条件语句具有基于评估树的简单语义，其特征是所谓的自由估值同余：两个条件语句自由估值同余当且仅当它们有相等的评估树。自由估值同余由命题代数的四个基本等式公理定义。能够识别比自由估值同余更多条件语句的估值同余包括重复证明、收缩、记忆和静态估值同余。每种估值同余都通过评估树上的转换进行特征化：两个条件语句C-估值同余当且仅当它们的C转换后的评估树相等。这些转换简单自然，仅在静态估值同余中使用稍微复杂的转换。此外，每种估值同余都在命题代数中形式化。我们的方法的一个衍生品可以称为“命题代数的规范化函数”：对于考虑的每种估值同余C，两个条件语句C-估值同余当且仅当C-规范化函数返回相等的图像。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
