标题： 命题逻辑的短路求值：非交换变体和交换变体 显示英文标题

标题： Propositional logic with short-circuit evaluation: a non-commutative and a commutative variant

摘要： 短路求值表示命题联结词的语义，在这种语义中，只有当第一个参数不足以确定表达式的值时，才会对第二个参数进行求值。 短路求值在编程中被广泛使用，其中顺序合取和析取作为原始联结词。 我们研究的问题是，在以下假设下，哪些逻辑定律可以公理化短路求值：复合语句从左到右进行求值，每个原子（命题变量）求值为真或假，并且原子求值可能导致副作用。 这个问题的答案取决于可能发生的基本副作用类型，并导致不同的“短路逻辑”。 基本情况是FSCL（自由短路逻辑），它描述了每个原子求值可能导致副作用的情况。 我们回顾了一些主要结果，然后将FSCL与MSCL（记忆短路逻辑）相关联，在复合语句的求值过程中，每个原子的第一次求值结果会被记忆。 MSCL可以看作是命题逻辑的顺序变体：原子求值不能引起副作用，且顺序联结词不是可交换的。 然后我们将MSCL与SSCL（静态短路逻辑）相关联，SSCL是命题逻辑的一种变体，它规定使用可交换的顺序联结词进行短路求值。 我们提出了求值树作为短路求值的直观语义，并为上述提到的短路逻辑提供了简单的等式公理化方法，这些方法仅使用否定和顺序联结词。 显示英文摘要

摘要： Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first argument does not suffice to determine the value of the expression. Short-circuit evaluation is widely used in programming, with sequential conjunction and disjunction as primitive connectives. We study the question which logical laws axiomatize short-circuit evaluation under the following assumptions: compound statements are evaluated from left to right, each atom (propositional variable) evaluates to either true or false, and atomic evaluations can cause a side effect. The answer to this question depends on the kind of atomic side effects that can occur and leads to different "short-circuit logics". The basic case is FSCL (free short-circuit logic), which characterizes the setting in which each atomic evaluation can cause a side effect. We recall some main results and then relate FSCL to MSCL (memorizing short-circuit logic), where in the evaluation of a compound statement, the first evaluation result of each atom is memorized. MSCL can be seen as a sequential variant of propositional logic: atomic evaluations cannot cause a side effect and the sequential connectives are not commutative. Then we relate MSCL to SSCL (static short-circuit logic), the variant of propositional logic that prescribes short-circuit evaluation with commutative sequential connectives. We present evaluation trees as an intuitive semantics for short-circuit evaluation, and simple equational axiomatizations for the short-circuit logics mentioned that use negation and the sequential connectives only.