💻 computer science

Fully Evaluated Left-Sequential Logics

This paper introduces a hierarchy of fully evaluated left-sequential logics ranging from Free to Static FEL, providing complete axiomatisations for their two-valued and three-valued versions using evaluation trees as a semantic foundation.

Original authors: Alban Ponse, Daan J. C. Staudt

Published 2026-05-14

📖 6 min read🧠 Deep dive

CC BY 4.0

Original authors: Alban Ponse, Daan J. C. Staudt

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you are a chef preparing a complex dish. In the world of computer logic, the "ingredients" are facts (true or false), and the "recipes" are instructions on how to combine them. This paper introduces a family of cooking styles called Fully Evaluated Left-Sequential Logics (FELs).

The core idea is simple: You must taste every single ingredient in order, from left to right, before you decide if the dish is ready. You cannot skip a step, and you cannot stop halfway just because the first ingredient tasted bad.

Here is a breakdown of the different "cooking styles" (logics) the authors explore, using everyday analogies.

1. The Basic Rule: "Left-Sequential"

In these logics, the order matters. If you have a recipe A then B, you must taste A first.

The Dot: The authors use a special dot (like ∧•) to show this. It means "Taste the left side first. Once that's done, taste the right side."
The Difference: In normal logic (like a standard truth table), if the first part is "False," you might stop there because the whole thing is already false. In these logics, you keep going. You taste the second part anyway. This is called "Full Evaluation."

2. The Four Levels of "Cooking Styles"

The paper presents a hierarchy of four logics, ranging from the most chaotic to the most rigid. Think of them as different levels of kitchen discipline.

Level 1: Free FEL (FFEL) – The "Chaotic Taster"

The Vibe: This is the most basic, "free" style.
The Rule: You taste everything in order. However, if you taste the same ingredient twice (e.g., A and then A again), the second time might taste different because the first time changed the kitchen!
The Analogy: Imagine tasting a lemon. The first time, it's sour. But if you taste it again immediately after squeezing it, maybe it's now just a wet rind. In FFEL, A and A are not necessarily the same because the first A might have had a "side effect" (like changing the environment).
Key Feature: It is immune to side effects only if you promise the ingredients don't change. It's the "weakest" logic because it allows for the most unpredictability.

Level 2: Memorising FEL (MFEL) – The "Note-Taking Chef"

The Vibe: This chef is organized.
The Rule: If you taste an ingredient (say, A), you write it down in a notebook. If you encounter A again later in the recipe, you just look at your notebook. You don't taste it again.
The Analogy: Imagine a security guard checking IDs. If he checks your ID at the door, he doesn't need to check it again at the back entrance; he remembers you.
Key Feature: This removes the "side effects." Once an atom (ingredient) is evaluated, its value is fixed for the rest of the process. This makes the logic stronger and more predictable.

Level 3: Conditional FEL (CℓFEL) – The "Flexible Team"

The Vibe: This team can swap places.
The Rule: It's like MFEL (you remember what you tasted), but now you can swap the order of ingredients if they are different. A then B is treated the same as B then A.
The Analogy: Imagine a group of friends deciding where to eat. If Alice and Bob are deciding between Pizza and Sushi, it doesn't matter who speaks first; the final decision is the same.
Key Feature: This logic is equivalent to a famous 3-valued logic called Bochvar's Logic. It handles "undefined" ingredients (like a broken egg) by treating the whole dish as "broken" (undefined) immediately.

Level 4: Static FEL (SFEL) – The "Strict Accountant"

The Vibe: The most rigid, traditional style.
The Rule: This is just standard propositional logic (like high school math), but with the rule that you still taste everything in order.
The Analogy: This is the "Gold Standard." If you have a recipe that says "If the egg is bad, the cake is bad," this logic agrees. It absorbs all the chaos.
Key Feature: It is so strict that it cannot handle "undefined" ingredients. If you try to mix "undefined" with "false," the math breaks (because Undefined becomes False, which is a contradiction).

3. The "Undefined" Ingredient (U)

The authors also explore what happens if an ingredient is Undefined (U).

In the "Free" and "Memorising" styles: If you taste an undefined ingredient, the whole process stops or becomes undefined. It's like trying to bake a cake with "mystery powder." The result is "mystery cake."
The "Absorbing" Rule: In the strongest 3-valued version (Conditional FEL), the undefined ingredient is "absorptive." If you mix Undefined with anything, the result is Undefined. It's like a black hole in your recipe.

4. The "Trees" of Logic

To prove their rules work, the authors use Evaluation Trees.

Imagine a Family Tree:
- The top is the main question.
- The branches are the "Left" (True) and "Right" (False) paths.
- The leaves at the bottom are the final answers (True or False).
The Innovation: In these logics, the tree shows the exact path you took. If you tasted A, then B, the tree shows that specific journey. In "Memorising" logic, the tree is cleaner because it doesn't show you tasting the same ingredient twice.

Summary of the Paper's Achievement

The authors didn't just describe these cooking styles; they wrote the Rulebooks (Axioms) for each one.

They defined exactly how to combine ingredients (equations).
They proved that these rulebooks are Complete (they cover every possible scenario) and Independent (no rule is redundant; you can't remove any without breaking the system).
They used computer tools (Prover9 and Mace4) to double-check their math, ensuring no human error slipped in.

In a nutshell: This paper maps out a spectrum of logic systems where you are forced to taste every single ingredient in order. It starts with a chaotic system where ingredients might change, moves to a system where you remember what you tasted, then to a system where order doesn't matter, and finally to a rigid system that behaves like standard math. They provide the exact mathematical laws for each style.

Technical Summary: Fully Evaluated Left-Sequential Logics

Problem Statement
This paper addresses the formalization and axiomatization of "Fully Evaluated Left-Sequential Logics" (FELs). Unlike short-circuit logics (SCLs), where evaluation halts once the result of a compound expression is determined, FELs prescribe a strategy of "full" or "strict" evaluation: every atomic proposition within a term is evaluated regardless of whether its value is strictly necessary for the final result. This strategy is motivated by programming contexts where side effects (e.g., state changes) must be guaranteed to occur for all atoms in an expression. The authors aim to define a hierarchy of such logics, ranging from the weakest (Free FEL), which is immune to atomic side effects, to the strongest (Static FEL), which behaves as a sequential version of classical propositional logic. Furthermore, the paper extends these logics to a three-valued setting to handle "undefinedness" ( $U$ ), a common feature in programming and logic (e.g., division by zero).

Methodology
The authors employ a semantic framework based on evaluation trees, a concept introduced in their prior work [19].

Semantics: Evaluation trees are binary trees where internal nodes represent atoms and leaves represent truth values ( $T$ $T$ , $F$ $F$ , or $U$ $U$ ). A path from root to leaf models an evaluation sequence.
- In Free FEL (FFEL), the tree structure strictly preserves the order of evaluation and allows for repeated occurrences of the same atom, modeling potential side effects.
- In Memorising FEL (MFEL), the semantics are refined such that no path in the tree contains multiple occurrences of the same atom; the evaluation of an atom is "memorized" if encountered again.
- In Conditional FEL (CℓFEL), the logic incorporates commutativity of atoms, effectively treating the order of independent atoms as irrelevant.
- In Static FEL (SFEL), the logic collapses to a sequential version of propositional logic where absorption laws hold.
Three-Valued Extension: For all logics except SFEL, the authors introduce a constant $U$ (undefined). The semantics are extended to trees with leaves in $\{T, F, U\}$ , where $U$ acts as an absorptive element (e.g., $U \land_r x = U$ ).
Axiomatization: The primary methodological contribution is the derivation of complete equational axiomatizations for each logic. The authors define normal forms (e.g., FEL Normal Form, $\sigma$ -normal forms) to prove completeness. They utilize the theorem prover Prover9 to verify derivabilities and Mace4 to generate finite counter-models to prove the independence of axioms.

Key Contributions and Results

Hierarchy of Two-Valued FELs:
- Free FEL (FFEL): The weakest logic, axiomatized by the set $EqFFEL$. It refutes idempotence ( $x \land_r x \neq x$ ) but satisfies associativity. It is the logic of full evaluation without side-effect constraints.
- Memorising FEL (MFEL): Axiomatized by adding one axiom to FFEL (specifically, $(x \lor_r y) \land_r z = (\neg x \land_r (y \land_r z)) \lor_r (x \land_r z)$ ). It enforces that repeated atoms are treated as identical, eliminating side effects.
- Conditional FEL (CℓFEL $_2$ ): Axiomatized by adding commutativity ( $x \land_r y = y \land_r x$ ) to MFEL. This logic is equivalent to the two-valued sublogic of Conditional Logic (Guzmán and Squier [12]).
- Static FEL (SFEL): The strongest logic, obtained by adding $x \land_r F = F$ to CℓFEL $_2$ . It is equivalent to Static Short-Circuit Logic (SSCL) and standard propositional logic under sequential evaluation.
Three-Valued Extensions (FELU):
- The authors define three-valued versions (FFELU, MFELU, CℓFEL) by adding axioms $\neg U = U$ and $U \land_r x = U$ .
- CℓFEL (the three-valued Conditional FEL) is proven to be equivalent to Bochvar's strict logic [8].
- SFEL cannot be extended with $U$ because the absorption law $F = U \land_r F = U$ leads to a collapse of truth values.
Completeness and Independence:
- Complete equational axiomatizations are provided for all defined logics.
- The authors present alternative, more concise sets of independent axioms for each logic (e.g., the set $MF$ for MFEL), verified using automated tools.
- Normal forms are constructed to prove that syntactic equality of normal forms corresponds to semantic equality of evaluation trees.

Significance and Claims
The paper claims to provide a unified framework for understanding full left-sequential evaluation, bridging the gap between short-circuit logics and classical propositional logic.

Predictability: The authors argue that FELs offer greater predictability regarding the state of the environment (side effects) after evaluation compared to SCLs, as all atoms are guaranteed to be evaluated.
Expressiveness: The paper demonstrates that while FFEL cannot express certain uniform evaluation trees (e.g., trees where an atom appears in different branches with different outcomes), MFEL and stronger logics can express these, thereby increasing the expressive power of the logic.
Relation to Existing Work: The work situates CℓFEL within the hierarchy of logics, showing it is equivalent to Bochvar's logic and a sublogic of Conditional Logic. It also clarifies the relationship between FELs and Short-Circuit Logics (SCLs), noting that FEL connectives can be defined within SCL frameworks (and vice versa under specific conditions), though FELs enforce a stricter evaluation discipline.

The paper concludes that these logics provide a robust theoretical basis for reasoning about expressions where full evaluation is required, offering complete and independent axiomatizations that facilitate automated reasoning and verification.