💻 computer science

Fully Evaluated Left-Sequential Logics

Cet article présente une hiérarchie de logiques séquentielles à gauche entièrement évaluées, allant de FEL libre à FEL statique, et fournit des axiomatisations complètes pour leurs versions à deux et trois valeurs en utilisant des arbres d'évaluation comme fondement sémantique.

Auteurs originaux : Alban Ponse, Daan J. C. Staudt

Publié 2026-05-14

📖 7 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Alban Ponse, Daan J. C. Staudt

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Imaginez que vous êtes un chef préparant un plat complexe. Dans le monde de la logique informatique, les « ingrédients » sont des faits (vrais ou faux), et les « recettes » sont des instructions sur la manière de les combiner. Cet article présente une famille de styles culinaires appelés Logiques Left-Sequential Évaluées Complètement (FEL).

L'idée centrale est simple : Vous devez goûter chaque ingrédient individuellement, dans l'ordre, de gauche à droite, avant de décider si le plat est prêt. Vous ne pouvez pas sauter une étape, et vous ne pouvez pas vous arrêter à mi-chemin simplement parce que le premier ingrédient avait mauvais goût.

Voici une analyse des différents « styles culinaires » (logiques) explorés par les auteurs, en utilisant des analogies du quotidien.

1. La Règle de Base : « Left-Sequential »

Dans ces logiques, l'ordre compte. Si vous avez une recette « A puis B », vous devez goûter A en premier.

Le Point : Les auteurs utilisent un point spécial (comme ∧•) pour indiquer cela. Cela signifie « Goûtez d'abord le côté gauche. Une fois cela fait, goûtez le côté droit. »
La Différence : Dans la logique normale (comme une table de vérité standard), si la première partie est « Faux », vous pourriez vous arrêter là car l'ensemble est déjà faux. Dans ces logiques, vous continuez. Vous goûtez la deuxième partie de toute façon. Cela s'appelle l'« Évaluation Complète ».

2. Les Quatre Niveaux de « Styles Culinaires »

L'article présente une hiérarchie de quatre logiques, allant de la plus chaotique à la plus rigide. Imaginez-les comme différents niveaux de discipline en cuisine.

Niveau 1 : FEL Libre (FFEL) – Le « Dégustateur Chaotique »

L'Ambiance : C'est le style le plus basique, « libre ».
La Règle : Vous goûtez tout dans l'ordre. Cependant, si vous goûtez le même ingrédient deux fois (par exemple A puis A à nouveau), la deuxième fois pourrait avoir un goût différent car la première fois a changé la cuisine !
L'Analogie : Imaginez goûter un citron. La première fois, il est acide. Mais si vous le goûtez à nouveau immédiatement après l'avoir pressé, peut-être n'est-ce plus qu'une écorce humide. Dans le FFEL, A et A ne sont pas nécessairement identiques car le premier A pourrait avoir eu un « effet secondaire » (comme changer l'environnement).
Caractéristique Clé : Il est immunisé contre les effets secondaires uniquement si vous promettez que les ingrédients ne changent pas. C'est la logique la « plus faible » car elle autorise le plus d'imprévisibilité.

Niveau 2 : FEL Mémoire (MFEL) – Le « Chef Preneur de Notes »

L'Ambiance : Ce chef est organisé.
La Règle : Si vous goûtez un ingrédient (disons A), vous l'écrivez dans un carnet. Si vous rencontrez A plus tard dans la recette, vous regardez simplement votre carnet. Vous ne le goûtez pas à nouveau.
L'Analogie : Imaginez un gardien de sécurité vérifiant les cartes d'identité. S'il vérifie votre carte à la porte, il n'a pas besoin de la vérifier à nouveau à l'entrée arrière ; il se souvient de vous.
Caractéristique Clé : Cela élimine les « effets secondaires ». Une fois qu'un atome (ingrédient) est évalué, sa valeur est fixée pour le reste du processus. Cela rend la logique plus forte et plus prévisible.

Niveau 3 : FEL Conditionnel (CℓFEL) – L'« Équipe Flexible »

L'Ambiance : Cette équipe peut échanger des places.
La Règle : C'est comme le MFEL (vous vous souvenez de ce que vous avez goûté), mais maintenant vous pouvez échanger l'ordre des ingrédients s'ils sont différents. « A puis B » est traité de la même manière que « B puis A ».
L'Analogie : Imaginez un groupe d'amis décidant où manger. Si Alice et Bob choisissent entre Pizza et Sushi, peu importe qui parle en premier ; la décision finale est la même.
Caractéristique Clé : Cette logique est équivalente à une logique à 3 valeurs célèbre appelée Logique de Bochvar. Elle gère les ingrédients « indéfinis » (comme un œuf cassé) en traitant l'ensemble du plat comme « cassé » (indéfini) immédiatement.

Niveau 4 : FEL Statique (SFEL) – Le « Comptable Rigide »

L'Ambiance : Le style le plus rigide et traditionnel.
La Règle : Il s'agit simplement de la logique propositionnelle standard (comme les mathématiques du lycée), mais avec la règle que vous goûtez tout de même tout dans l'ordre.
L'Analogie : C'est la « Référence Or ». Si vous avez une recette qui dit « Si l'œuf est mauvais, le gâteau est mauvais », cette logique est d'accord. Elle absorbe tout le chaos.
Caractéristique Clé : Elle est si stricte qu'elle ne peut pas gérer les ingrédients « indéfinis ». Si vous essayez de mélanger « Indéfini » avec « Faux », les mathématiques s'effondrent (car Indéfini devient Faux, ce qui est une contradiction).

3. L'Ingrédient « Indéfini » (U)

Les auteurs explorent également ce qui se passe si un ingrédient est Indéfini (U).

Dans les styles « Libre » et « Mémoire » : Si vous goûtez un ingrédient indéfini, tout le processus s'arrête ou devient indéfini. C'est comme essayer de faire un gâteau avec de la « poudre mystère ». Le résultat est un « gâteau mystère ».
La Règle « Absorbante » : Dans la version à 3 valeurs la plus forte (FEL Conditionnel), l'ingrédient indéfini est « absorbant ». Si vous mélangez Indéfini avec n'importe quoi, le résultat est Indéfini. C'est comme un trou noir dans votre recette.

4. Les « Arbres » de la Logique

Pour prouver que leurs règles fonctionnent, les auteurs utilisent des Arbres d'Évaluation.

Imaginez un Arbre Généalogique :
- Le sommet est la question principale.
- Les branches sont les chemins « Gauche » (Vrai) et « Droite » (Faux).
- Les feuilles en bas sont les réponses finales (Vrai ou Faux).
L'Innovation : Dans ces logiques, l'arbre montre le chemin exact que vous avez emprunté. Si vous avez goûté A, puis B, l'arbre montre ce voyage spécifique. Dans la logique « Mémoire », l'arbre est plus propre car il ne montre pas que vous avez goûté le même ingrédient deux fois.

Résumé de la Réalisation de l'Article

Les auteurs n'ont pas seulement décrit ces styles culinaires ; ils ont écrit les Règlements (Axiomes) pour chacun d'eux.

Ils ont défini exactement comment combiner les ingrédients (équations).
Ils ont prouvé que ces règlements sont Complets (ils couvrent chaque scénario possible) et Indépendants (aucune règle n'est redondante ; vous ne pouvez en supprimer aucune sans briser le système).
Ils ont utilisé des outils informatiques (Prover9 et Mace4) pour vérifier leurs mathématiques, s'assurant qu'aucune erreur humaine ne s'était glissée.

En résumé : Cet article cartographie un spectre de systèmes logiques où vous êtes contraint de goûter chaque ingrédient individuellement dans l'ordre. Il commence par un système chaotique où les ingrédients peuvent changer, passe à un système où vous vous souvenez de ce que vous avez goûté, puis à un système où l'ordre n'a pas d'importance, et enfin à un système rigide qui se comporte comme les mathématiques standard. Ils fournissent les lois mathématiques exactes pour chaque style.

Résumé technique : Logiques left-séquentielles entièrement évaluées

Énoncé du problème
Ce papier traite de la formalisation et de l'axiomatisation des « Logiques left-séquentielles entièrement évaluées » (FELs). Contrairement aux logiques à court-circuit (SCLs), où l'évaluation s'arrête dès que le résultat d'une expression composée est déterminé, les FELs prescrivent une stratégie d'évaluation « complète » ou « stricte » : chaque proposition atomique au sein d'un terme est évaluée, indépendamment du fait que sa valeur soit strictement nécessaire pour le résultat final. Cette stratégie est motivée par des contextes de programmation où des effets de bord (par exemple, des changements d'état) doivent être garantis pour tous les atomes d'une expression. Les auteurs visent à définir une hiérarchie de telles logiques, allant de la plus faible (FEL Libre), qui est immunisée contre les effets de bord atomiques, à la plus forte (FEL Statique), qui se comporte comme une version séquentielle de la logique propositionnelle classique. De plus, l'article étend ces logiques à un cadre à trois valeurs pour gérer l'« indéfinition » ( $U$ ), une caractéristique courante en programmation et en logique (par exemple, la division par zéro).

Méthodologie
Les auteurs emploient un cadre sémantique basé sur les arbres d'évaluation, un concept introduit dans leur travail antérieur [19].

Sémantique : Les arbres d'évaluation sont des arbres binaires où les nœuds internes représentent des atomes et les feuilles représentent des valeurs de vérité ( $T$ $T$ , $F$ $F$ ou $U$ $U$ ). Un chemin de la racine à une feuille modélise une séquence d'évaluation.
- Dans la FEL Libre (FFEL), la structure de l'arbre préserve strictement l'ordre d'évaluation et permet des occurrences répétées du même atome, modélisant ainsi des effets de bord potentiels.
- Dans la FEL à mémorisation (MFEL), la sémantique est affinée de telle sorte qu'aucun chemin dans l'arbre ne contient plusieurs occurrences du même atome ; l'évaluation d'un atome est « mémorisée » s'il est rencontré à nouveau.
- Dans la FEL conditionnelle (CℓFEL), la logique incorpore la commutativité des atomes, traitant efficacement l'ordre des atomes indépendants comme sans importance.
- Dans la FEL Statique (SFEL), la logique se réduit à une version séquentielle de la logique propositionnelle où les lois d'absorption sont valables.
Extension à trois valeurs : Pour toutes les logiques sauf la SFEL, les auteurs introduisent une constante $U$ (indéfini). La sémantique est étendue à des arbres dont les feuilles appartiennent à $\{T, F, U\}$ , où $U$ agit comme un élément absorbant (par exemple, $U \land_r x = U$ ).
Axiomatisation : La contribution méthodologique principale est la dérivation d'axiomatisations équationnelles complètes pour chaque logique. Les auteurs définissent des formes normales (par exemple, forme normale FEL, formes normales $\sigma$ ) pour prouver la complétude. Ils utilisent le prouveur de théorèmes Prover9 pour vérifier les dérivabilités et Mace4 pour générer des contre-modèles finis afin de prouver l'indépendance des axiomes.

Principales contributions et résultats

Hiérarchie des FELs à deux valeurs :
- FEL Libre (FFEL) : La logique la plus faible, axiomatisée par l'ensemble $EqFFEL$. Elle réfute l'idempotence ( $x \land_r x \neq x$ ) mais satisfait l'associativité. C'est la logique de l'évaluation complète sans contraintes d'effets de bord.
- FEL à mémorisation (MFEL) : Axiomatisée en ajoutant un axiome à la FFEL (spécifiquement, $(x \lor_r y) \land_r z = (\neg x \land_r (y \land_r z)) \lor_r (x \land_r z)$ ). Elle impose que les atomes répétés soient traités comme identiques, éliminant ainsi les effets de bord.
- FEL conditionnelle (CℓFEL $_2$ ) : Axiomatisée en ajoutant la commutativité ( $x \land_r y = y \land_r x$ ) à la MFEL. Cette logique est équivalente à la sous-logique à deux valeurs de la Logique Conditionnelle (Guzmán et Squier [12]).
- FEL Statique (SFEL) : La logique la plus forte, obtenue en ajoutant $x \land_r F = F$ à la CℓFEL $_2$ . Elle est équivalente à la Logique à court-circuit Statique (SSCL) et à la logique propositionnelle standard sous évaluation séquentielle.
Extensions à trois valeurs (FELU) :
- Les auteurs définissent des versions à trois valeurs (FFELU, MFELU, CℓFEL) en ajoutant les axiomes $\neg U = U$ et $U \land_r x = U$ .
- La CℓFEL (la FEL conditionnelle à trois valeurs) est prouvée équivalente à la logique stricte de Bochvar [8].
- La SFEL ne peut pas être étendue avec $U$ car la loi d'absorption $F = U \land_r F = U$ entraîne un effondrement des valeurs de vérité.
Complétude et indépendance :
- Des axiomatisations équationnelles complètes sont fournies pour toutes les logiques définies.
- Les auteurs présentent des ensembles alternatifs, plus concis, d'axiomes indépendants pour chaque logique (par exemple, l'ensemble $MF$ pour la MFEL), vérifiés à l'aide d'outils automatisés.
- Des formes normales sont construites pour prouver que l'égalité syntaxique des formes normales correspond à l'égalité sémantique des arbres d'évaluation.

Importance et affirmations
L'article affirme fournir un cadre unifié pour comprendre l'évaluation left-séquentielle complète, comblant le fossé entre les logiques à court-circuit et la logique propositionnelle classique.

Prévisibilité : Les auteurs soutiennent que les FELs offrent une plus grande prévisibilité concernant l'état de l'environnement (effets de bord) après l'évaluation par rapport aux SCLs, car tous les atomes sont garantis d'être évalués.
Expressivité : L'article démontre que, tandis que la FFEL ne peut pas exprimer certains arbres d'évaluation uniformes (par exemple, des arbres où un atome apparaît dans différentes branches avec des résultats différents), la MFEL et les logiques plus fortes peuvent les exprimer, augmentant ainsi le pouvoir expressif de la logique.
Relation avec les travaux existants : Le travail situe la CℓFEL dans la hiérarchie des logiques, montrant qu'elle est équivalente à la logique de Bochvar et une sous-logique de la Logique Conditionnelle. Il clarifie également la relation entre les FELs et les Logiques à court-circuit (SCLs), notant que les connecteurs FEL peuvent être définis dans des cadres SCL (et vice versa sous certaines conditions), bien que les FELs imposent une discipline d'évaluation plus stricte.

L'article conclut que ces logiques fournissent une base théorique robuste pour raisonner sur des expressions où une évaluation complète est requise, offrant des axiomatisations complètes et indépendantes qui facilitent le raisonnement et la vérification automatisés.