Alban Ponse

Proposition algebra is based on Hoare’s conditional, a ternary connective comparable to if–then–else and used in the context of propositional logic. Conditional statements are composed from atomic propositions (propositional variables), constants for the Boolean truth values, and the conditional. In previous work, various equational axiomatisations have been defined, each of which leads to a so-called valuation congruence. The weakest of these is “free valuation congruence” and the strongest is “static valuation congruence”, which is equivalent to propositional logic. Free valuation congruence is axiomatised by four simple equational axioms, and we use evaluation trees to give a simple semantics: two conditional statements are free valuation congruent if, and only if, they have equal evaluation trees. Increasingly stronger valuation congruences arise by adding axioms to the four that define free valuation congruence: repetition-proof, contractive, memorising, and static valuation congruence. We prove that each such valuation congruence C can be characterised using a transformation on evaluation trees: two conditional statements are C-valuation congruent if, and only if, their C-transformed evaluation trees are equal. In order to prove that these transformations preserve the congruence property, we use normalisation functions: two conditional statements are C-valuation congruent if, and only if, the C-normalisation function returns equal images. Our framework provides the first comprehensive tree-based semantics that unifies all major valuation congruences in proposition algebra, offering both conceptual clarity and practical decision procedures.

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. In programming, short-circuit evaluation is widely used, with left-sequential conjunction and disjunction as primitive connectives. We consider left-sequential, non-commutative propositional logic, also known as MSCL (memorising short-circuit logic), and start from a previously published, equational axiomatisation. First, we extend this logic with a left-sequential version of the biconditional connective, which allows for an elegant axiomatisation of MSCL. Next, we consider a left-sequential version of the NAND operator (the Sheffer stroke) and again give a complete, equational axiomatisation of the corresponding variant of MSCL. Finally, we consider these logical systems in a three-valued setting with a constant for `undefined', and again provide completeness results.

Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first is insufficient to determine the value of the expression. Compound statements are evaluated from left to right. Short-circuit evaluation is widely used in programming, with negation and sequential conjunction and disjunction as primitives. We study the question of which laws axiomatise short-circuit evaluation. In MSCL (memorising short-circuit logic), atoms (propositional variables) evaluate to true or false, and in the evaluation of a compound statement, the first evaluation result of each atom is memorised. Hence, MSCL is 'Non-commutative propositional logic with short-circuit evaluation' and atomic evaluations cannot cause a side effect. Next, we consider the case that atoms can also evaluate to the truth value 'undefined'. For two- and three-valued MSCL, we present evaluation trees as an intuitive semantics and provide complete independent equational axiomatisations.

Common meadows are fields expanded with a total inverse function. Division by zero produces an additional value denoted with "a" that propagates through all operations of the meadow signature (this additional value can be interpreted as an error element). We provide a basis theorem for so-called common cancellation meadows of characteristic zero, that is, common meadows of characteristic zero that admit a certain cancellation law.

A datatype defining rewrite system (DDRS) is an algebraic (equational) specification intended to specify a datatype. When interpreting the equations from left-to-right, a DDRS defines a term rewriting system that must be ground-complete. First we define two DDRSs for the ring of integers, each comprising twelve rewrite rules, and prove their ground-completeness. Then we introduce natural number and integer arithmetic specified according to unary view, that is, arithmetic based on a postfix unary append constructor (a form of tallying). Next we specify arithmetic based on two other views: binary and decimal notation. The binary and decimal view have as their characteristic that each normal form resembles common number notation, that is, either a digit, or a string of digits without leading zero, or the negated versions of the latter. Integer arithmetic in binary and decimal notation is based on (postfix) digit append functions. For each view we define a DDRS, and in each case the resulting datatype is a canonical term algebra that extends a corresponding canonical term algebra for natural numbers. Then, for each view, we consider an alternative DDRS based on tree constructors that yields comparable normal forms, which for that view admits expressions that are algorithmically more involved. For all DDRSs considered, ground-completeness is proven.Comment: arXiv admin note: text overlap with arXiv:1406.3280

We consider several novel congruences on the signature of meadows with the aim to survey different notions of fractions. In particular we suggest a notion of “true fraction”.

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.