Cours 4 : Introduction à la réécriture et la décision modulo, par Frédéric Blanqui

Rappels

Arithmétique comme théorie axiomatique.

  • Objets : $0, S, +, ×$
  • Propositions : $\bot, ⟹, ∀, ⋯$, Prédicats : $=, ⋯$
  • Axiomes / Schémas d’axiomes (quand il y en un ensemble infini) ⟶ hypothèses

  • Règles de déduction/inférence :

    • $\vdash$ : relation de prouvabilité = la plus petite relation $⊆ ℙ(𝒫) × 𝒫$
  • langage pour représenter les preuves basé sur le $𝜆$-calcul

Exemple de système d’inférence :

Déduction naturelle (Gentzen, 1934) :

\[\cfrac{𝛤 \vdash A \quad 𝛤 \vdash B}{𝛤 \vdash A∧B} (∧ intro)\] \[\cfrac{𝛤 \vdash A∧B}{𝛤 \vdash A} (∧ elim left)\] \[\cfrac{𝛤 \vdash A∧B}{𝛤 \vdash B} (∧ elim right)\] \[\cfrac{𝛤, A \vdash B}{𝛤 \vdash A ⟹ B} (⟹ intro)\] \[\cfrac{𝛤 \vdash A ⟹ B \quad 𝛤 \vdash A}{𝛤 \vdash B} (⟹ elim)\] \[\cfrac{𝛤 \vdash \bot}{𝛤 \vdash A} (\bot elim)\] \[\cfrac{\qquad}{𝛤 \vdash A}(Axiom) A∈𝛤\]

En $𝜆$-calcul :

\[\cfrac{𝛤, x:A \vdash u:B}{𝛤 \vdash 𝜆x. u : A ⟹ B} (⟹ intro)\] \[\cfrac{𝛤 \vdash u: A ⟹ B \quad 𝛤 \vdash v : A}{𝛤 \vdash uv : B} (⟹ elim)\] \[\cfrac{𝛤 \vdash u :A \quad 𝛤 \vdash v:B}{𝛤 \vdash (u, v) : A∧B} (∧ intro)\] \[\cfrac{𝛤 \vdash u:A∧B}{𝛤 \vdash 𝜋_1(u): A} (∧ elim left)\]

Arithmétique de Peano :

  • Théorie de l’égalité (avec ses schémas d’axiomes) :

    • réflexivité, symétrie, transitivité

    • schéma d’axiomes de passage au contexte :

      \[∀i, j. i=j ⟹ F ⟹ F[i:=j]\]

  • Arithmétique élémentaire $Q$

    • définition de l’addition par réc à droite
    • définition de la multiplication par réc à droite
    • injectivité du successeur
    • zéro n’est pas un successeur
    • tout élément non nul est un successeur

  • Schéma de récurrence/induction :

    \[F[i:=0] ⟹ (∀i, F[i:=j] ⟹ F[i:=S j]) ⟹ ∀i, F\]

Correspondance de Curry-de Bruijn-Howard

NB : de Bruijn : système AUTOMATH dans les années 60/70

Preuves ⟺ Programmes

Propositions/Formules ⟺ Types

On peut déduire des choses sur la complexité d’une fonction en fonction de son type, dans un système de types donné.

Coupure (Cut) :

règle d’introduction suivie d’une règle d’élimination

Simplification des preuves = élimination des coupures ⟺ $𝛽$-réduction

Un même terme peut avoir plusieurs coupures ⟶ élimination des coupures = une relation.

Problèmes :

  • est-ce que l’ordre d’élimination a une importance ?

    • si non : propriété de confluence

  • terminaison ?

  • choix du sous-terme à réduire ? (dans les langages de programmation : stratégie d’évaluation)

\[𝜋_1(u, v) ⟶ u\] \[\lbrace (a,b) \mid ∃c; a=𝜋_1(b, c) \rbrace\]

Plus petit couple : $(𝜋_1(𝛼, 𝛽), 𝛼)$

Règle de réécriture :

ex : $(\underbrace{𝜋_1(𝛼, 𝛽)}_{\text{ motif (pattern) }}, 𝛼) ⟶ 𝛼$ : filtrage

On veut définir une relation avec un nombre fini de règles.

Relation engendrée par un ensemble de règles de réécriture $⟶_R$ :

plus petite relation contenant $R$ et stable par substitution et contexte

\[\cfrac{\qquad}{l ⟶_R r} \; l⟶r∈R\] \[\cfrac{t ⟶_R u}{t 𝜃 ⟶_R u 𝜃}\] \[\cfrac{t ⟶_R u}{f \, t_1 \, ⋯ \, t_{i-1} \, t \, t_{i+1} \, t_n 𝜃 ⟶_R f \, t_1 \, ⋯ \, t_{i-1} \, u \, t_{i+1} \, t_n 𝜃}\]

Question qui se pose : $t$ est-il une instance de $l$ ? i.e est-ce qu’il existe une substitution $𝜃$ tq

\[t = l 𝜃 \quad \text{ ( noté } l \preceq t \text{ )}\]

(cas particulier d’unification : on veut $t = l 𝜃$ au lieu de $t 𝜃 = l 𝜃$)

Ou bien : on utilise la notion de position $p$ dans un arbre syntaxique (représentant un terme) : on remplace le sous-terme $l 𝜃$ à la position $p$ par un sous-terme $r 𝜃$ (filtrage par la règle $l ⟶_R r$)

NB : il peut y avoir ambiguïté : à une même position, plusieurs règles peuvent s’appliquer.

Elimination des coupures :

  1. consistance/cohérence

    • on peut montrer qu’on ne peut pas avoir de preuves sans coupures de $\bot$ ⟹ si on exhibe une preuve sans coupure, ça ne peut pas être une preuve de $\bot$

  2. En logique intuitionniste, l’élimination des coupures dans une preuve de $A∨B$ permet de déterminer si $A$ ou si $B$ est vrai (avec la règle d’introduction du $∨$)

  3. Pareil pour les règles d’introduction du quantificateur existentiel $∃$ : l’élimination des coupures donne un témoin existentiel effectif.

Intérêt en génie logiciel : si on a une preuve constructive de :

\[∀ \underbrace{x}_{\text{ input }}, ∃ \underbrace{y}_{\text{ input }}, P(x, y)\]

on peut en extraire un programme effectif, qui à chaque input $x$ donne un output $y$.

Règles de conversion

Relation sur les termes :

  • $i+0 ⟶_ℕ i$
  • $i+s j ⟶_ℕ s(i+j)$
  • $i×0 ⟶_ℕ 0$
  • $i × s j ⟶_ℕ i × j + i$
  • $\vdots$

Relation sur les propositions :

  • $0 = s i ⟶ \bot$
  • $s i = s j ⟶ i = j$

on peut prouver :

\[\cfrac{𝛤 \vdash F \quad F \longleftrightarrow^\ast_ℕ G}{𝛤 \vdash G}\]
Déduction modulo :

une théorie =

  • un ensemble d’axiomes
  • une congruence (rel. d’éq. monotone (= qui passe au contexte)) sur les propositions $≡$

on a des règles :

\[\cfrac{𝛤 \vdash A \quad A ≡ B}{𝛤 \vdash B}\] \[\cfrac{𝛤 \vdash C \quad C ≡ A ∧ B}{𝛤 \vdash A}\]

Avantages :

  • preuves + petites
  • séparation entre les déductions “créatives” (qui demandent de l’intuition, où les hommes sont meilleurs que les machines) et le calcul mécanique (ou les machines sont meilleures que les hommes)
  • élimination des coupures / propriété du témoin (= constructivisme des preuves)

Propriété de témoin/disjonction

  • $∃x, A(x)$ ⟶ on a un témoin explicite

  • $A∨B$ ⟶ on a $A$ ou $B$

  • $\bot$ ⟶ pas possible de le dériver

Idée : convertir les schémas d’axiomes (théories purement axiomatique) en congruence (déduction modulo ⟶ théories purement calculatoire), pour éliminer les axiomes, et ainsi avoir ces trois propriétés.

Théories purement calculatoire (cf. cours de déduction modulo par Gilles Dowek en M2 au MPRI) :

  • Arithmétique
  • Théorie des ensembles
  • Théorie des types simples (HOL)

NB : on essaye d’avoir des congruences décidables :

Exs :

  • la congruences des formules équivalentes à $\top$ n’est pas décidable : on ne peut pas dire si une formule est vraie.

  • si on a $A∨B ≡ C ∧ D$ : on ne peut pas éliminer la coupure $A \vdash C∧D \vdash C$ (intro puis élim)

Donc on peut que la congruence soit non-confusing = préserve la structure des connecteurs :

  • si $A ≡ A’$ alors

    • soit $A$ ou $A’$ est atomique
    • soit si $A= B ∧ C$, alors $A’ = B’ ∧ C’$ avec $B ≡ B’$ et $C≡C’$

On a une congruence définie par un ensemble d’équations $E$ : on en prend la clôture réflexive symétrique transitive $\longleftrightarrow_E^\ast$ :

Comment décider $\longleftrightarrow_E^\ast$ ?

Procédure de complétion de Knuth-Bendix, i.e. essayer de trouver $R$ un ensemble de règles de réécriture tq

  1. $\longleftrightarrow_E^\ast = \longleftrightarrow_R^\ast$
  2. $R$ termine (⟹ existence d’une forme normale)
  3. $R$ conflue (⟹ unicité de la forme normale)

⟹ en partant des équations, on essaye de les “orienter” (pour transformer les équations via des règles de réécriture)

Dans le cas de l’arithmétique : représentation purement calculatoire :

  • termes avec 2 sortes :

    • $𝜄$ pour les objets

      • constructeurs : $0, s, +, ×, pred$

    • $𝜅$ pour les classes (ou ensembles d’objets)

  • propositions avec connecteurs logiques habituels $∧, ∨, ⋯ \mid t = u \mid t∈c \mid \underbrace{Null(t)}_{“t=0”} \mid Nat(t)$

  • schéma de compréhension $∀x_1, ⋯, ∀x_n, ∃c, ∀y \; (y ∈ c ⟺ A)$

    • $”∈” ∉ A$
    • $fv(A) ⊆ \lbrace x_1, ⋯, x_n \rbrace$

  • Schéma de récurrence $∀y, \, Nat(y) ⟺ ∀c, \, (0∈c ⟹ (∀x, \; Nat(x) ⟹ x∈c ⟹ s x ∈ c) ⟹ y ∈ c)$

  • $pred \, 0 ⟶ 0$
  • $pred \, s x ⟶ x$
  • addition, multiplication, …
  • $Null(0) ⟶ \top$
  • $Null( s \, x) ⟶ \bot$
  • sorte de Skolémisation : $y∈ f_{x_1, \ldots, x_n, y, A} ⟶ A$

de cette manière, on a une présentation purement calculatoire : pas d’axiomes, que des règles de réécriture.

Leave a comment