UP | HOME

Systèmes d'inférence
Définitions inductives et co-inductives

Table of Contents

1 Systèmes d'inférence : un outil puissant pour la formalisation

Comment formaliser un langage logique ou un langage de programmation ? Nous présentons ici une solution qui a progressivement émergé au carrefour de la logique et de l'informatique : les systèmes d'inférence.

Les systèmes d'inférence permettent de valider des jugements en construisant des preuves suivant des règles d'inférence. Les jugements peuvent être de différentes natures suivant les systèmes considérés. Cependant en pratique, ils ressortissent à quelques classes :

  • des jugements de bonne formation, les preuves définissant alors des éléments d'un ensemble de données,
  • des jugements de typage,
  • de jugements relationnels, d'évaluation ou de déduction, par exemple avec des séquents.

Notre but est de définir formellement cette notion, de présenter des exemples et de montrer comment les exprimer en Coq.

Notation

  • Nous utilisons par la suite la notation utilisée par Coq et inspirée de Lisp. Une fonction f appliquée à n arguments se note
    • (f a1 … an).
  • On utilisera le jugement de typage t : A pour signifier que t a le type A.

2 Définition formelle des systèmes d'inférence

Il est recommandé d'aborder cette définition formelle des systèmes d'inférence après l'étude d'exemples, notamment ceux qui suivent. Elle est en effet très générale, alors qu'en pratique elle se présente sous des formes simplifiées. Elle vise à réaliser une synthèse entre le point de vue logique et celui retenu par Coq pour faciliter la définition des données.

Un système d'inférence I définit un type de données, une proposition ou un ensemble. Il permet de construire soit des preuves de la proposition, soit des éléments de l'ensemble. Il peut être paramétré, ce qui permet une définition générique, et indexé, ce qui permet une définition spécialisée. Les paramètres et les indices appartiennent à des types déjà existants. Par exemple, on peut définir l'ensemble (Liste T), paramétré par un type T et représentant les listes d'éléments appartenant à T, et la proposition (Pair n), indexé par l'entier naturel n, et représentant la parité d'entiers naturels. Comme on le verra dans une section suivante, cette distinction n'est pas essentielle mais pragmatique.

Un système d'inférence (I p u), où p représente la paramétrisation et u l'indexation, est formé d'un ensemble fini de règles d'inférence. Chaque règle d'inférence introduit un constructeur c, identifiant la règle, et se décompose en des prémisses en nombre fini et en une conclusion. Les prémisses et les conclusions sont des jugements de typage (x : T) exprimant que x a le type T, pour signifier que x est une preuve de la proposition T ou que x est un élément de l'ensemble T.

Voici la notation la plus générale utilisée pour une règle.

(x_1 : P_1)  ... (x_n : P_n)               prémisses non-récursives
	   (z_1 : Q_1)  ... (z_m : Q_m)      prémisses récursives 
---------------------------------------    ------------------------
 (c p x_1 ... x_n z_1 ... z_m) : I p u           conclusion

Du fait que les variables z_k ne sont pas utilisées dans les types, comme nous allons le voir, une forme simplifiée peut être utilisée. Elle est d'usage fréquent en logique : elle met en évidence la proposition I définie et l'identification de la règle, la forme de la preuve important moins.

(x_1 : P_1)  ... (x_n : P_n)         prémisses non-récursives
	 Q_1 ... Q_m                   prémisses récursives
---------------------------- [c]    ------------------------ [constructeur]
	   I p u                           conclusion

De plus, des variables des prémisses non récursives peuvent être omises lorsqu'elles ne sont pas utilisées ailleurs. C'est souvent le cas en logique. Enfin, les constructeurs peuvent être omis s'ils ne servent pas par ailleurs. La règle est alors identifiée par la propriété qu'elle exprime : par exemple on dira la règle de transitivité.

Paramétrisation de la règle

  • Paramétrisation p du système d'inférence
  • Variables x_i des prémisses non-récursives
  • Variables z_k des prémisses récursives

Prémisses non-récursives

  • Chaque prémisse x_i est une variable à instancier par un élément ou une preuve de P_i.
  • Chaque type P_i peut dépendre des paramètres, p et des variables déjà introduites, x_1, …, xi-1. Il est égal à un type existant dans le contexte, soit un ensemble ou une proposition.

Prémisses récursives

  • Chaque prémisse z_k est une variable à instancier par un élément ou une preuve de Q_k.
  • Chaque type Q_k peut dépendre des paramètres p et des variables déjà introduites, x_1, …, x_n. Il est égal

    • soit à une instance (I q v) du type défini par le système d'inférence
    • soit à une famille (I q_j v_j)_j d'instances de ce type (j parcourant un ensemble existant).

    Comme les familles peuvent être indexées par des ensembles infinis, la récursion peut donc impliquer réellement une infinité de prémisses récursives.

Conclusion

  • Le constructeur a pour arguments les paramètres de la règle.
  • La conclusion est nécessairement de la forme (… : I p …) : autrement dit, la définition est bien générique en p.
  • Les indices u peuvent varier : ils peuvent dépendre des prémisses non-récursives x_i et des paramètres p.

Remarquons que si

  • la paramétrisation p du système d'inférence est instanciée,
  • les variables x_i des prémisses non récursives sont instanciées,

alors

  • les types P_i des prémisses non récursives sont déterminés,
  • les types Q_k des prémisses récursives sont déterminés,
  • le type (I p u) de la conclusion est déterminé.

On qualifiera une telle instanciation de la paramétrisation p et des variables x_i des prémisses non récursives d'instanciation partielle déterminante. Cette détermination est importante car elle garantit que les seules occurrences récursives du type I sont celles des prémisses récursives : elles sont dites "strictement positives".

Un système d'inférence peut être interprété de deux manières, inductivement ou co-inductivement. Dans tous les cas, il définit

  • des arbres dont les nœuds sont les constructeurs et
  • la relation d'appartenance au type associé au système d'inférence.

Précisément, à chaque nœud c de sous-arbres d, a_1, …, a_n, b_1, …, b_m, alors il existe une règle

(x_1 : P_1)  ... (x_n : P_n)
	 (z_1 : Q_1)  ... (z_m : Q_m)
-------------------------------------
(c p x_1 ... x_n z_1 ... z_m) : I p u

et une valuation σ définie sur les variables x_i, z_k, et les paramètres p tels que

  • d = p[σ],
  • a_i = x_i[σ],
  • b_k = z_k[σ],
  • a_i : P_i[σ] est valide,
  • b_k : Q_k[σ] est valide,

On en déduit alors que (c d a_1 … a_n b_1 … b_m) : (I d u[σ]) est valide, autrement dit que (c d a_1 … a_n b_1 … b_m) est une preuve de la proposition (I d u[σ]) ou un élément de l'ensemble (I d u[σ]). De tels arbres sont aussi appelés des termes.

Parfois, une règle d'inférence peut être obtenue par composition d'autres règles d'inférence : son constructeur est obtenu par composition d'autres constructeurs. Une telle règle est dite dérivable. Etant donné un système d'inférence, il est assez fréquent de lui ajouter des règles dérivables : elles ont pour effet de simplifier la construction des preuves ou des éléments, mais ne modifient pas l'interprétation du système.

3 Induction

Dans l'interprétation inductive, on ne considère que les arbres bien fondés, pour lesquels tout chemin partant de la racine se termine par un constructeur associé à une règle sans prémisses, appelée axiome en logique. L'ensemble des arbres bien fondés forme l'algèbre initiale associée au système d'inférence, notée (Δ I).

Avec une algèbre initiale, il est possible de raisonner par induction, grâce à une récurrence structurelle sur les arbres bien fondés.

Commençons par le cas propositionnel. Considérons un prédicat A donnant des propositions (A p u), comme le prédicat I associé au système d'inférence. Considérons la règle d'inférence suivante.

(x_1 : P_1)  ... (x_n : P_n)
	 (z_1 : Q_1)  ... (z_m : Q_m)
-------------------------------------
(c p x_1 ... x_n z_1 ... z_m) : I p u

On dit que les prémisses vérifient A si

  • toutes les prémisses non-récursives (x_i : P_i) sont vérifiées,
  • à chaque fois que Q_k est une instance I q v, alors (A q v) est vérifié, et
  • à chaque fois que Q_k est une famille d'instances (I q_j v_j)_j, alors pour tout j, (A q_j v_j) est vérifié.

On dit que la conclusion vérifie A si

  • (A p u) est vérifié.

On dit que A est stable pour le système d'inférence I lorsque pour toute règle, pour toute paramétrisation de cette règle, si les prémisses vérifient A, alors la conclusion vérifie A. On peut alors énoncer le principe d'induction ainsi :

si A est stable, alors pour tous p et u, (I p u) implique (A p u).

La démonstration se fait par récurrence structurelle sur les arbres bien fondés appartenant à (I p u), en utilisant la stabilité.

Considérons maintenant le cas ensembliste. Considérons un prédicat A défini sur (I p u), pour toute paramétrisation p et toute indexation u. Considérons la règle d'inférence suivante.

(x_1 : P_1)  ... (x_n : P_n)
	 (z_1 : Q_1)  ... (z_m : Q_m)
-------------------------------------
(c p x_1 ... x_n z_1 ... z_m) : I p u

On dit que les prémisses vérifient A si

  • toutes les prémisses non-récursives (x_i : P_i) sont vérifiées,
  • à chaque fois que Q_k est une instance I q v, alors (A z_k) est vérifié, et
  • à chaque fois que Q_k est une famille d'instances (I q_j v_j)_j, alors pour tout j, (A (z_k j)) est vérifié.

On dit que la conclusion vérifie A si

  • (A (c p x_1 … x_n z_1 … z_m)) est vérifié.

On dit que A est stable lorsque pour toute règle, pour toute paramétrisation de la règle, si les prémisses vérifient A, alors la conclusion vérifie A. On peut énoncer le principe d'induction ainsi :

si A est stable, alors pour tous p et u, tout élément de (I p u) vérifie A.

La démonstration se fait par récurrence structurelle sur les arbres bien fondés appartenant à (I p u), en utilisant la stabilité.

Avec une algèbre initiale, il est aussi possible de calculer par récursion. Considérons la règle d'inférence suivante.

(x_1 : P_1)  ... (x_n : P_n)
	 (z_1 : Q_1)  ... (z_m : Q_m)
-------------------------------------
(c p x_1 ... x_n z_1 ... z_m) : I p u

Associons à cette règle un type fonctionnel, étant donné une famille de types (R p u y)p, u, y, où y appartient à I p u.

  • Arguments :
    • p : paramètres du système d'inférence,
    • x_1 : P_1, …, x_n : P_n,
    • z_1 : Q_1, …, z_m : Q_m,
    • si z_k est une prémisse récursive de type I q v, alors un argument r_k : (R q v z_k),
    • si z_k est une prémisse récursive de type (I q_j v_j)_j, alors une famille d'arguments r_k : (R q_j v_j (z_k j))_j,
  • Résultat de type R p u (c p x_1 … x_n z_1 … z_m).

On peut alors énoncer le principe de récursion ainsi :

si on associe à toute règle une fonction du type associé à la règle, alors il existe une unique fonction F

  • associant à tout élément y de (I p u) un élément de (R p u y), pour toute paramétrisation p et toute indexation u,
  • et vérifiant les équations récursives suivantes.

Equation récursive vérifiée par F, pour un élément obtenu par la règle précédente, de fonction associée G

F (c p x_1 ... x_n z_1 ... z_m) 
= (G p x_1 ... x_n  z_1 ... z_m (r_k)_k)
    [r_k := (Q_k = (I _ _)) ? (F z_k) : (F (z_k j))_j]

La démonstration de l'unicité et de l'existence se fait par récurrence structurelle sur les arbres bien fondés appartenant à (I p u).

Bien que nous ayons distingué le principe d'induction et celui de récursion, ils constituent en réalité un seul principe : comme la vérification d'une proposition correspond au calcul d'une preuve, le principe d'induction devient une instance du principe de récursion.

En résumé, le principe d'induction ou de récursion peut être vu comme une annotation des règles, notée => … ci dessous. Il affirme que si toutes les règles peuvent être annotées, alors tout arbre bien fondé formé à partir des règles peut l'être. En effet, on commence par les feuilles, correspondant aux axiomes, puis on remonte vers la racine, en appliquant les règles annotées. Les schémas ci-dessous rendent compte de ce point de vue, et peuvent servir de moyen mnémotechnique.

Induction - Cas propositionnel

...   (z_k : I q v) => (A q v)   ...
------------------------------------
    (c ...) : I p u => (A p u)

Induction - Cas ensembliste

 ...   (z_k : I q v) => (A z_k)   ...
-------------------------------------
  (c ...) : I p u => (A (c ...))

Récursion - Cas ensembliste

...     (z_k : I q v) => (F z_k)     ...
---------------------------------------- [G : fonction associée à la règle]
  (c ...) : I p u => (G ... (F z_k) ...)

Application : les règles admissibles

  • Il est assez fréquent d'ajouter à un système d'inférence des règles pour faciliter la construction des preuves ou des éléments, sans pour autant modifier l'interprétation du système. Nous avons déjà vu l'exemple des règles dérivables.
  • Considérons une règle susceptible d'être ajoutée au système d'inférence.

    (x_1 : P_1)  ... (x_n : P_n)               prémisses non-récursives
    	   (z_1 : Q_1)  ... (z_m : Q_m)      prémisses récursives 
    ---------------------------------------    ------------------------
    	       I p u                              conclusion
    

    Elle n'a pas de constructeur puisqu'il s'agit de construire un élément de I p u en utilisant les constructeurs existants. La règle est dite admissible si pour tous (x_i : P_i), tous (z_j : Q_j), il existe (t : I p u).

  • La démonstration de l'admissibilité se fait très souvent par induction sur une des prémisses, ou plusieurs.
  • Exemple : toute règle dérivable est admissible. La démonstration est directe, sans induction.
  • Exemple : la règle de coupure dans le calcul des séquents est admissible.
    • C'est le théorème d'élimination des coupures. La démonstration, compliquée en logique du premier ordre, se fait par induction sur la proposition utilisée pour la coupure.

4 Co-induction

Dans l'interprétation co-inductive, on considère non seulement les arbres bien fondés, comme dans l'interprétation inductive, mais aussi les arbres non fondés, pour lesquels il existe un chemin infini en profondeur. L'ensemble de ces arbres forme la co-algèbre finale associée au système d'inférence, notée (∇ I). Un principe de co-induction ou de co-récursion permet d'associer une preuve ou un élément de la co-algèbre finale à un élément d'un ensemble donné de départ. C'est une situation inverse, duale, du principe d'induction ou de récursion, où on associe à une preuve ou un élément de l'algèbre initiale un élément d'un ensemble donné d'arrivée.

(Δ I) --  récursion   -> A

    D -- co-récursion -> (∇ I)

Avec une co-algèbre finale, il est possible de raisonner par co-induction ou de calculer par co-récursion, en construisant un arbre infini à partir de la racine.

Commençons par le cas propositionnel. Considérons comme précédemment pour le cas inductif un prédicat A donnant des propositions (A p u), comme le prédicat I associé au système d'inférence. On dit que A est dense si pour tous p et u tels que (A p u) est vérifié, alors il existe

  • une règle

    (x_1 : P_1)  ... (x_n : P_n)
    	 (z_1 : Q_1)  ... (z_m : Q_m)
    -------------------------------------
    (c p x_1 ... x_n z_1 ... z_m) : I p u
    
  • une instanciation partielle déterminante de la paramétrisation p du système d'inférence et des variables x_i des prémisses non récursives,

telles que les prémisses (récursives) vérifient A. On peut alors énoncer le principe de co-induction ainsi :

si A est dense, alors pour tous p et u, (A p u) implique (I p u).

La démonstration se fait en définissant un système d'équations récursives. Une inconnue Xp, u est associée à chaque couple p, u vérifiant A. Comme il existe une règle partiellement instanciée

(x_1 : P_1)  ... (x_n : P_n)
	 (z_1 : Q_1)  ... (z_m : Q_m)
-------------------------------------
(c p x_1 ... x_n z_1 ... z_m) : I p u

on peut former l'équation Xp, u = (c p x_1 … x_n z_1 … z_m), où

  • si z_k est une prémisse récursive de type (I q v), alors z_k := Xq, v,
  • si z_k est une prémisse récursive de type (I q_j v_j)_j, alors z_k := (Xq_j, v_j)_j.

Ce système d'équations récursives gardées (par les constructeurs c) admet une unique solution : chaque solution en Xp, u est une preuve de I p u, ce qui montre l'implication recherchée : (A p u) implique (I p u).

Remarque : la garde dans l'équation garantit que la solution progresse à chaque dépliage d'une variable, lors de la résolution.

Considérons maintenant le cas ensembliste. Le principe de co-récursion permet d'associer un élément de la co-algèbre finale à tout élément d'un ensemble dense. Partant cette fois d'une famille (A p u) d'ensembles, on procède comme pour le principe de co-induction. On dit que A est dense lorsque pour tous p et u tels que (A p u) n'est pas vide, si a appartient à (A p u), alors il existe

  • une règle

    (x_1 : P_1)  ... (x_n : P_n)
    	 (z_1 : Q_1)  ... (z_m : Q_m)
    -------------------------------------
    (c p x_1 ... x_n z_1 ... z_m) : I p u
    
  • une instanciation partielle déterminante de la paramétrisation p du système d'inférence et des variables x_i des prémisses non récursives,

telles que

  • si z_k est une prémisse récursive de type (I q v), alors il existe a_k dans (A q v),
  • si z_k est une prémisse récursive de type (I q_j v_j)_j, alors il existe une famille a_k telle que (a_k j) appartient à (A q_j v_j).

On peut énoncer le principe de co-récursion ainsi :

si A est dense, alors pour tous p et u, il existe une unique fonction F de (A p u) vers (I p u) vérifiant le système suivant d'équations récursives gardées.

F a = (c p x_1 ... x_n z_1 ... z_m)
	[z_k := (Q_k = (I _ _)) ? (F a_k) : (F (a_k j))_j]

La démonstration se fait comme précédemment en définissant un système d'équations récursives gardées. Les inconnues sont les (X_a)_a, avec a appartenant à un ensemble (A p u).

5 Exemples : formules, listes, séquents, flots

En logique, on utilise des systèmes d'inférence pour décrire les déductions valides. Préalablement, on définit les formules et les séquents, formés de deux listes de formules.

Formules

		   p : Formule  q : Formule
----------------   -------------------------  
  V : Formule          p ∨ q : Formule

C'est une définition récursive sans paramètres ni indices. V (pour "Vrai") et (pour "ou") sont deux constructeurs, le second noté de manière infixe.

On peut définir des listes inductivement ainsi.

Listes

			  (t : T)    (r : Liste T) 
------------------       --------------------------
 vide T : Liste T          cons T t r : Liste T

Cette définition récursive possède un paramètre, T, un type. C'est la définition habituelle des listes : une liste est soit vide, soit construite à partir d'un élément et d'une liste. Par la suite, on simplifie vide T en [] et cons T t r en (t::r) ou t, r.

Pour ce genre de définitions inductives purement paramétrées, on utilise souvent une notation alternative, dite de Backus-Naur et fondée sur des grammaires sans contexte. Voici ce qu'on pourrait obtenir pour les définitions précédentes, en simplifiant. A chaque système d'inférence, on associe un non-terminal, et à chaque règle, une alternative dans la définition du non-terminal. Les variables correspondant à des prémisses récursives sont remplacées par le non-terminal.

Formule p ::= V | p ∨ p
Liste   l ::= [] | p :: l

Un séquent se forme à partir d'un couple de listes de formules, (G, D). Nous cherchons à exprimer la validité des séquents, en utilisant une relation notée exprimant la déduction. Dans un séquent, la liste gauche G s'interprète comme une conjonction, la liste droite D comme une disjonction. Le séquent G ⊢ D exprime que de la conjonction G, on peut déduire la disjonction D. Cette interprétation justifie les règles qui suivent.

Calcul des séquents exprimant leur validité (extrait)

   Γ ⊢ Δ           
------------ [V-G]           ----- [V-D]   
  V, Γ ⊢ Δ                    ⊢ V


				Γ ⊢ p, Δ
			    ---------------- [∨-Dg]   
p, Γ ⊢ Δ   q, Γ ⊢ Δ          Γ ⊢ (p ∨ q), Δ
------------------- [∨-G]
  (p ∨ q), Γ ⊢ Δ                Γ ⊢ q, Δ
			    ---------------- [∨-Dd]   
			     Γ ⊢ (p ∨ q), Δ

Alors que les systèmes d'inférence précédents définissent des ensembles, ce dernier système décrit une proposition. Il est indexé par un séquent, c'est-à-dire deux listes. Pour simplifier, les déclarations des listes de formules Γ et Δ, ou des formules p et q, sont omises, puisqu'elles peuvent être inférées facilement : c'est une pratique habituelle. Les constructeurs de preuve identifient les règles, si bien qu'une preuve dans ce système est un arbre dont les nœuds sont ces constructeurs : on retrouve ainsi la définition habituelle utilisée en logique pour interpréter un système d'inférence et définir les preuves dans un système d'inférence.

Terminons ces exemples en étudiant les principes inductifs et récursifs pour les listes, puis l'interprétation co-inductive.

Induction sur les listes

  • (A T) prédicat défini sur (Liste T)
    • A stable :=
      • (A T []) vérifié
      • pour tous t dans T et r dans (Liste T), si (A T r) est vérifié, alors (A T (t::r)) est vérifié.
  • Induction : si A est stable, alors pour toute liste l de (Liste T), (A T l) est vérifié.

On reconnaît une induction classique sur les listes avec deux cas :

  • le cas vide, où on vérifie la propriété pour une liste vide,
  • le cas construit, où on vérifie la propriété pour une liste construite à partir d'une tête et d'un corps, en supposant la propriété vérifié par le corps de la liste.

Récursion sur les listes

  • Type des résultats : famille (R T l), où l dans (Liste T).
  • Données
    • Règle vide : fonction CV associant un élément de (R T []) à T
    • Règle cons : fonction CC associant un élément de (R T (t::r)) à T, t dans T, l dans (Liste T) et r dans (R T l)
  • Résultat : fonction F définie récursivement et vérifiant les équations suivantes
    • F T [] = CV T
    • F T (t::l) = CC T t l (F T l)

On reconnaît une récursion classique sur des listes, où on procède par filtrage.

Il est aussi possible d'interpréter le même système co-inductivement. Dans ce cas, la règle pour les listes construites peut être utilisée indéfiniment, menant à une liste infinie, ou flot ("stream"). Par exemple le flot (0 :: 1 :: 2 :: …) est engendré ainsi.

		  ...
	    -------------------------
(0 : Nat)   1 :: 2 :: ... : Liste Nat 
-------------------------------------
    0 :: 1 :: ... : Liste Nat

(Nat est l'ensemble des entiers naturels.)

Pour définir ce flot infini, on peut procéder par co-induction en montrant que Nat est dense. A n dans Nat, on associe la règle partiellement instanciée

 (n : Nat)    (r : Liste Nat) 
--------------------------
   (n :: r) : Liste Nat

et n+1 à la prémisse r. Par co-récursion, il existe une unique fonction F vérifiant le système suivant d'équations récursives gardées.

F n = n :: (F (n+1))

Le flot (F O) est le flot recherché.

6 Paramétrisation ou indexation ?

Un système d'inférence possède à la fois une paramétrisation et une indexation. La paramétrisation permet des définitions génériques alors que l'indexation permet des définitions spécialisées.

Par exemple, le prédicat de validité pour un séquent est indexé par le séquent. Ainsi la règle suivante

   Γ ⊢ Δ           
------------ [V-G]
  V, Γ ⊢ Δ

spécialise la conclusion, en ne retenant que les conclusions supposant V. Le système peut cependant devenir paramétré et non indexé, en modifiant les règles comme la règle [V-G] de la manière suivante.

(Γ' : Liste Formule)  (Γ = V, Γ')  Γ' ⊢ Δ           
----------------------------------------- [V-G']
		Γ ⊢ Δ

Cette fois, la règle est générique. Dans ce nouveau système, toute règle a pour conclusion Γ ⊢ Δ, et des équations sont introduites dans les prémisses pour décrire les formes de Γ et de Δ. C'est à vrai dire une méthode tout à fait générale, permettant de remplacer une indexation par une paramétrisation, au prix d'équations concernant les indices comme prémisses supplémentaires. Il faut remarquer que le fait que toute instanciation des paramètres et des variables des prémisses non récursives soit déterminante implique que le système d'inférence paramétré associé est bien formé : les équations supplémentaires ne dépendent pas des prémisses récursives.

Il reste qu'en Coq, l'égalité est définie inductivement par un système d'inférence indexé. Précisément, le système possède deux paramètres, le type E sur lequel on définit l'égalité, et le premier terme (x : E) de l'égalité. Le second terme de l'égalité, (u : E), est un indice. Ce système possède une seule règle, que voici.

------------ [eq_refl]
  eq E x x

Elle exprime le fait que l'égalité s'obtient par réflexivité. Si on applique notre méthode générale de paramétrisation à ce système d'inférence, on obtient la règle suivante.

  eq E x y
------------ [eq_refl']
  eq E x y

Evidemment, ce système d'inférence définit inductivement un ensemble vide, faute d'axiomes. Autrement dit, la méthode générale s'applique à tous les systèmpes d'inférence, sauf à celui définissant l'égalite.

On peut cependant exprimer l'égalité par un système d'inférence paramétré en utilisant le principe de Leibniz, soit le principe d'identité des indiscernables.

 (∀ P. P x <-> P y)
-------------------- [indiscernable]
     egL E x y

Il est facile de montrer l'équivalence (eq E x y) <-> (egL E x y), pour tous x et y dans E.

  • Supposons (eq E x y). Soit P un prédicat. Montrons par induction sur l'égalité (eq E x y) que P x <-> P y. Considérons le prédicat A E x y := (P x <-> P y). Comme A est stable puisque (P x <-> P x), on déduit que (P x <-> P y), d'où (egL E x y).
  • Réciproquement, supposons (egL E x y). Montrons par induction sur l'égalité (egL E x y) que (eq E x y). Il suffit de montrer la stabilité de eq, soit que l'hypothèse (∀ P. P x <-> P y) implique (eq E x y). Il suffit de prendre P _ := (eq E x _). Comme par réflexivité, on a (eq E x x), on déduit (eq E x y).

Conclusion : tout système d'inférence indexé est équivalent à un système d'inférence paramétré. Cette propriété est importante car elle permet de définir simplement l'inversion : étant donné un système d'inférence définissant I et un but (I p u), l'inversion détermine les règles et les prémisses associées qui permettent d'aboutir en conclusion au but. L'inversion est triviale dans un système paramétré. En effet, toute règle est susceptible de s'appliquer ; comme le but détermine la paramétrisation du système, il reste à déterminer les variables associées aux prémisses, autrement dit il reste à résoudre des sous-buts. L'inversion est ainsi l'étape élémentaire permettant de construire un terme appartenant au but (I p u). Dans un système indexé, cette inversion n'est pas triviale, du fait de l'indexation. Elle peut cependant être définie par un transfert dans le système d'inférence paramétré associé.

système indexé  <= équivalence =>  système paramétré

  sous-buts <------------------------ sous-buts   (équations supplémentaires)         
					 ∧
					 | inversion
    but ------------------------------> but

Remarquons que lorsque les équations supplémentaires ne sont pas vérifiables, la règle peut être éliminée.

En pratique, il est préférable de définir des systèmes d'inférence le plus paramétré possible : ainsi si un indice est utilisé dans toutes les règles de manière générique, alors il doit être intégré aux paramètres. Cette pratique a pour effet de faciliter l'inversion.

7 Extensions utiles : récursivité mutuelle, imbrication

A ce stade, nous avons défini des systèmes d'inférence en isolation. Cependant, comme la définition est indexée, il est possible de coder des définitions mutuellement récursives : il suffit d'attribuer à chaque système de la définition mutuelle un indice et de rassembler dans un seul système toutes les règles.

Voici un exemple d'une définition mutuellement récursive de deux systèmes : elle permet de déterminer la parité d'un entier naturel.

Parité - Prédicat Pair indexé par un naturel

		 (n : nat)  (Impair n)
--------- [P0]  ----------------------- [PS]
 Pair 0               Pair (S n)

Parité - Prédicat Impair indexé pr un naturel

 (n : nat)  (Pair n)
--------------------- [IS]
    Impair (S n)

Cette définition mutuellement récursive (Pair faisant appel à Impair et inversement) peut être remplacée par la définition équivalente d'un seul système, doublement indexé.

Parité - Prédicat Parité indexé pau un naturel et un booléen

		       (n : nat)  (Parite n faux) 
--------------- [P0]  ---------------------------- [PS]
 Parite 0 vrai             Parite (S n) vrai

		       (n : nat)  (Parite n vrai) 
		      ---------------------------- [IS]
			   Parite (S n) faux

Il serait aussi utile de pouvoir élargir les possibilités de récursivité dans les prémisses. Prenons l'exemple d'arbres définis comme une racine ayant pour sous-arbres une liste d'arbres.

Arbres

 (r : E)  (s : Liste (Arbre E)) 
-------------------------------
     cons r s : Arbre E

Actuellement, cette définition est impossible du fait que l'occurrence récursive du type (Arbre E) n'est pas directement une prémisse. Cependant, il est possible de remplacer ce système par une définition mutuellement récursive en définissant

  • Arbre E en faisant appel à Liste (Arbre E) et
  • Liste (Arbre E) en faisant appel à Arbre E.

Cette solution n'est pas pratique puisqu'elle ne permet pas la composition, en contraignant à la répétition des règles définissant les listes. On préfèrera donc affaiblir la condition des occurrences récursives de manière à autoriser de telles définitions.

Définitions imbriquées

  • Le type défini par un système d'inférence peut apparaître non seulement dans les prémisses récursives, mais aussi dans les autres prémisses. La définition est bien formée si la définition mutuellement récursive équivalente est bien formée.

Etant donné un système d'inférence définissant I, la construction de la définition mutuellement récursive équivalente implique l'inversion des prémisses non récursives (x : J p u) dans lesquelles le type I apparaît. Cette inversion peut aboutir à des occurrences non strictement positives si I apparaît dans les indices u : il suffit de penser à la définition de l'inversion par transfert dans le système paramétré équivalent, puisque les indices engendrent des équations supplémentaires ; or, le prédicat d'égalité sous sa forme paramétrée aboutit à des occurrences qui ne sont pas strictement positives, C'est pourquoi il est requis que si I apparaît dans (J p u), alors il apparaît dans la paramétrisation p mais n'apparaît pas dans l'indexation u.

Voici un exemple élémentaire illustrant l'importance de cette condition.

Système d'inférence indexé par un type définissant A

-------
 A nat

Système paramétré équivalent

egL T nat  (T = nat, avec l'égalité de Leibniz)
---------
   A T

Système d'inférence avec une imbrication définissant I

A I
---
 I

C'est un exemple proche de celui précédent, avec I pour Arbre et A pour Liste. A est cependant indexé.

Système d'inférence équivalent éliminant l'imbrication

A I   egL I nat    (∀ P. P I <-> P nat)
---   ---------    --------------------
 I       A I           egL I nat

Ce système d'inférence constitue un abus de notation. Voici le système qu'il dénote : un système d'inférence définissant M et indexé par 0, 1 ou 2, correpondant respectivement à I, A I et egL I nat.

M 1   M 2   (∀ P. P (M 0) <-> P nat)
---   ---   ------------------------
M 0   M 1           M 2

Clairement, l'occurence M 0 dans la famille de prémisses de la règle se concluant par M 2 n'est pas strictement positive. Cette définition doit donc être rejetée.

8 Conclusion : un outil puissant pour définir, raisonner et calculer

Les systèmes d'inférence permettent non seulement de définir des jugements de toutes sortes, mais aussi de raisonner ou de calculer sur ces jugements, le tout d'une manière à la fois simple et rigoureuse. Comme on l'a vu, ces définitions et ces raisonnements sont facilement implémentables en Coq. D'un point de vue pratique, il est très souvent utile de formaliser avec des systèmes d'inférence les problèmes qu'on traite : on y gagne en clarté et en assurance (concernant la correction du résultat).

Author: Hervé Grall
Version history: v1: 2020-01-07; v2: 2020-01-21[+inversion, +mutual definition, +admissibility].
Comments or questions: Send a mail.
The webpage content is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.