短路逻辑
计算机科学中的逻辑
2013-03-13 v4 逻辑
摘要
短路求值表示命题连接词的语义，其中仅当第一个参数不足以确定表达式的值时，才求值第二个参数。在编程中，短路求值被广泛使用，顺序合取和析取是原始连接词。短路逻辑是命题逻辑的一种变体，可以借助Hoare条件（一种类似于if-then-else的三元连接词）来定义，并且蕴含所有可从条件的四个基本公理推导出且可在命题逻辑中表达的等式（例如，合取结合律和双重否定移位的公理）。在没有副作用的情况下，短路求值刻画了命题逻辑。然而，短路求值允许对副作用进行建模，并产生了各种不同的短路逻辑。第一个极端情况是FSCL（自由短路逻辑），它刻画了每个原子（命题变量）的求值都可能产生副作用的环境。另一个极端情况是MSCL（记忆短路逻辑），这是我们在命题逻辑之下区分的、具有最多识别能力的变体。在MSCL中，只能对非常有限类型的副作用进行建模，而顺序合取是非交换的。我们为FSCL和MSCL提供了公理化。将MSCL扩展一个简单公理得到SSCL（静态短路逻辑，或顺序命题逻辑），我们也为其提供了完备性结果。我们简要讨论了介于FSCL和MSCL之间的两个变体，其中包括一个允许原子及其否定收缩的逻辑。
引用
@article{arxiv.1010.3674,
title = {Short-circuit logic},
author = {Jan A. Bergstra and A. Ponse and D. J. C. Staudt},
journal= {arXiv preprint arXiv:1010.3674},
year = {2013}
}
备注
59 pages, 7 tables, 3 figures; Daan Staudt is added as an extra author; normal forms for FSCL are defined and completeness of its axiomatization is proved