Previous Up Next
Mathématiques pour l’Informatique 2 2015–16                  http://www.lri.fr/~paulin/MathInfo2


3  Systèmes d’inférence, induction, récursion

On a vu que l’on pouvait définir un ensemble (et donc en particulier une relation) par extension (dans le cas de relation finie, par exemple {(0,2),(1,3),(2,4)}) ou encore en compréhension en spécifiant une propriété vérifiée par les éléments (par exemple {(x,y)∈ℕ×ℕ|y=x+2 ∧ x ≤ 2}.

Cette section introduit une manière systématique de définir une relation étant données certaines propriétés que doit vérifier la relation. Elle nous donne également les outils pour raisonner sur de tels objets. Les principes mis en œuvre sont une généralisation du principe de récurrence sur les entiers.

3.1  Récurrence sur les entiers

La règle logique générale que nous avons donnée pour prouver x,P(x) consiste à introduire une variable x arbitraire et à montrer P(x). Il est rare que l’on puisse démontrer la propriété P(x) sans s’appuyer sur la forme possible des objets que représente la variable x.

Dans le cas des entiers, au lieu de montrer directement P(x) on va fournir deux objets :

  1. une preuve de P(0) (le cas de base, appelé aussi initialisation)
  2. une preuve de n,P(n) ⇒ P(n+1) c’est-à-dire un moyen de transformer une preuve de P(n) en preuve de P(n+1) et ce pour un n arbitraire (le cas d’hérédité)

Le principe de récurrence dit que ces deux éléments sont suffisants pour justifier que x∈ℕ, P(x) est vrai.

En effet si on prend un entier quelconque, par exemple x=45 alors on part de la preuve P(0) qui nous est donnée par le cas 1, puis on utilise une fois la propriété 2, ce qui permet d’avoir une preuve de P(1) puis encore une fois pour avoir une preuve de P(2) et enfin à la 45ème application, on a bien une preuve de P(45).

Exercice 1   Montrer par récurrence sur n que Σi=1n (2i−1) = n2

Le principe de récurrence exprime que l’ensemble des entiers est le plus petit ensemble qui contient 0 et qui s’il contient x contient aussi x+1.

3.2  Définition de relation par cloture

En informatique, on utilise souvent un procédé de définition de relation dit par cloture. On rappelle qu’une relation R sur A1×⋯ × Ak est un ensemble de n-uplets (x1,…,xk) et que l’on écrit R(x1,…,xk) au lieu de (x1,…,xk)∈ R

Pour définir une relation R sur des objets, on se donne des propriétés que doit vérifier la relation R, puis on définit R comme la plus petite relation qui vérifie ces propriétés. D’un point de vue mathématique, la relation R est définie, lorsque c’est possible (c’est-à-dire quand il en existe au moins une), comme l’intersection de toutes les relations qui vérifient les propriétés données.

Exemple 1 (Définition par cloture)   Supposons que l’on cherche à définir l’ensemble des entiers relatifs qui peuvent se calculer en utilisant juste l’addition à partir des entiers 3 et 5 on peut le faire en caractérisant une relation S(x) qui représente que x est obtenu ainsi. On identifie 3 propriétés de la relation : Cela peut se traduire par les trois formules suivantes :
S(3)    S(5)      ∀ x yS(x) ∧ S(y) ⇒ S(x+y)
Si on veut autoriser en plus la soustraction, on ajoutera la propriété : x y, S(x) ∧ S(y) ⇒ S(xy).
Exercice 2  

Les définitions par cloture sont aussi très utiles pour décrire des systèmes qui évoluent suivant certaines étapes élémentaires.

Exercice 3   Donner des propriétés qui caractérisent une relation P(x,y) représentant les positions sur un plan d’un pion qui part de l’origine (0,0) et qui peut seulement se déplacer de deux manières :
  1. 1 case à droite et 2 cases vers le haut
  2. 2 cases à droite et 1 case vers le haut
Exemple 2 (Définitions de l’ordre sur les entiers par cloture)   Dans les chapitres précédents, on a utilisé la relation d’ordre sur les entiers soit comme une relation primitive soit comme définie par compréhension {(x,y)∈ ℕ× ℕ|∃ z,y=x+z} mais on n’a pas dit comment était définie l’addition. On va montrer comment définir la relation d’ordre en utilisant sur les entiers uniquement la constante 0 et l’opération x+1.

L’ordre sur les entiers vérifie les propriétés suivantes:

∀ x ∈ ℕ, x ≤ x    et    ∀ x  y∈ ℕ, x ≤ y ⇒ x ≤ (y+1)

Par ailleurs ces deux propriétés sont suffisantes pour dériver la relation nm pour deux entiers arbitraires. Ces deux propriétés forment une définition par cloture de l’ordre sur les entiers naturels.
Une autre définition possible est :

∀ x∈ ℕ, 0 ≤ x    et    ∀ x  y∈ ℕ, x ≤ y ⇒ (x+1) ≤ (y+1)

On remarque que l’ordre sur les entiers n’est pas la seule relation qui vérifie ces propriétés, par exemple la relation x≤′y =def  xy+1.

Exemple 3 (Relation mal formée)   Supposons que l’on souhaite définir un prédicat P comme le plus petit prédicat tel que les deux conditions suivantes sont vérifiées: L’existence d’un prédicat P vérifiant ces deux conditions implique que P(x) ⇔ ¬ P(x) et donc que l’on peut prouver d’où une contradiction: un tel prédicat P n’existe pas.

3.2.1  Système d’inférence

Le processus de définition par cloture est surtout utilisé pour des propriétés de la relation à définir ayant une forme particulière : on parlera de définition constructive ou encore de système d’inférence.

Exemple 4 (Règles d’inférences pour la définition de l’ordre sur les entiers)   Pour définir l’ordre sur les entiers, on peut se donner l’un des deux systèmes de règles d’inférence suivantes:
  1.  
    x ≤1 x 
         
    x ≤1 y 
    x ≤1 (y+1) 
  2.  
    0 ≤2 x 
         
    x ≤2 y 
    (x+1) ≤2 (y+1) 
Définition 1 (Règle d’inférence)   Une règle d’inférence pour définir une relation R(x1,…,xk) se présente sous la forme
T1  …  Tn
R(t1,…,tk)
où chaque Ti est une formule logique qui peut contenir la formule R. Les règles d’inférence peuvent contenir des variables libres x1,…,xp qui sont implicitement quantifiées universellement. La règle d’inférence est interprétée comme la formule:
∀ x1,…,xp,T1 ⇒ ⋯ ⇒ Tn ⇒ R(t1,…,tk)
On appelle T1,…,Tn les prémisses de la règle d’inférence et R(t1,…,tk) la conclusion.
Exemple 5   On peut construire une preuve d’une relation définie par cloture R(t1,…,tn) en exhibant un arbre dont la conclusion est R(t1,…,tn) et dont chaque nœud correspond à une instance d’une règle d’inférence. Par exemple, on peut construire des preuves de 1 ≤ 3 en suivant l’une ou l’autre des définitions.
(2) 
(2) 
(1)  
 1 ≤1 1
 1 ≤1 2
 1 ≤1 3
            
(2) 
(1)  
 0 ≤2 2
 1 ≤2 3
Exemple 6 (Entiers)   Les entiers ont été introduits à l’aide de la constante 0 et l’opération successeur x+1. Ces opérations existent aussi dans d’autres ensembles (ℤ, ℚ, ℝ, …). Les entiers naturels sont le plus petit ensemble qui contient 0 et qui est stable pour l’opération successeur. On peut définir cette notion par cloture en introduisant une prédicat N(x) par les règles d’inférence:
 
 N(0) 
     
 N(x
 N(x+1) 
Il suffit alors d’ajouter à la théorie l’axiome x ∈ ℕ, N(x).
Définition 2 (Relation définie par des règles d’inférence)   Soit un ensemble fini de règles d’inférence qui construisent une relation R. La relation définie par ces règles d’inférence est la plus petite relation qui satisfait les formules associées aux règles d’inférence.

On remarque que du fait de la forme spécifique des règles d’inférence, il existe au moins une relation qui vérifie les règles d’inférence, à savoir la relation triviale qui vaut vrai partout R(x1,…,xk)  =def  ⊤. Ceci est nécessaire pour pouvoir considérer l’intersection de toutes les relations qui vérifient la propriété.

Proposition 1   Si chaque formule Ti qui mentionne R est monotone en R, c’est-à-dire que si RS alors Ti(R) ⇒ Ti(S) alors la relation R est bien définie et vérifie les règles d’inférence, c’est-à-dire :

La preuve de cette proposition sera faite plus tard lorsque l’on verra les notions d’ordre. La condition de monotonie est essentielle, comme le montre la définition suivante:

Exemple 7   Soit la propriété A(n) sur les entiers définie par la règle d’inférence suivante :
¬ A(n
A(n+1) 
Il y a plusieurs propriétés qui vérifient cette propriété: A0(n)  =def  ⊤ mais aussi la propriété d’être pair A1(n)  =def  ∃ k, n=2× k et la propriété d’être impair A2(n)  =def  ∃ k, n=2× k+1.
Si on prend l’intersection
A de toutes les relations qui vérifient la condition alors si A(n) est vérifié on a aussi A1(n) et A2(n) donc n devrait être à la fois pair et impair ce qui conduit à une contradiction et donc n, ¬ A(n). Donc A ne vérifie pas la condition de la règle d’inférence n, ¬ A(n) ⇒ A(n+1).

En pratique dans une règle d’inférence :

T1 … Tn
R(t1,…,tk)

une prémisse sera soit une propriété qui ne mentionne pas R (condition de bord) soit une instance de R, c’est-à-dire de la forme R(u1,…,uk). La condition de monotonicité est alors trivialement satisfaite.

Exemple 8 (Fermeture transitive)   Les définitions par cloture sont très utiles pour définir des propriétés de fermeture transitive de relations binaires. On suppose donée une relation step binaire sur un ensemble A. On veut définir la relation path sur le même ensemble A, tel que path(x,y) est vrai si on peut passer de x à y en un nombre fini d’étapes. Une définition possible est
 
path(x,x
          
step(x,y)     path(y,z
path(x,z
Exercice 4   Donner deux autres définitions par cloture de la même relation:

Preuve:

  1.  
    path(x,x
              
    path(x,y)     step(y,z
    path(x,z
  2.  
    path(x,x
              
    step(x,y
    path(x,y
              
    path(x,y)     path(y,z
    path(x,z

3.3  Preuve par induction

Induction généralisée.

Le schéma d’induction peut être généralisé. Soit la propriété P à établir par induction sur une relation R définie par des règles d’inférence. Pour une règle d’inférence

T1 … Tn
R(t1,…,tk)

on suppose que T1,…,Tm mentionnent R, il suffit de vérifier que P satisfait la propriété :

x1,…,xp,T1 ⇒ ⋯ ⇒ Tn ⇒ T1(P) ⇒ Tm(P) ⇒ P(t1,…,tk)

C’est-à-dire que l’on peut ajouter en hypothèse les prémisses de la règle d’inférence.

Preuve: Le schéma généralisé se dérive à partir du schéma simple en prenant comme propriété à montrer Q(y1,…,yk) =def  R(y1,…,yk) ∧ P(y1,…,yk).

Exemple 9   Dans le cas de la première définition de l’ordre sur les entiers, supposons que l’on souhaite montrer x  y ∈ℕ, x1 yP(x,y).
Par induction simple sur la relation il faut montrer :
∀ x ∈ ℕ, P(x,x)           ∀ x  y ∈ ℕ, P(x,y) ⇒ P(x,y+1)
avec le schéma généralisé, on est ramené à montrer :
x∈ ℕ, P(x,x)           ∀ x  y∈ ℕ, x ≤1 y ⇒ P(x,y) ⇒ P(x,y+1)
Ce dernier schéma est utile pour montrer simplement une propriété dite d’inversion de la relation à savoir :
∀ x y∈ ℕ, x ≤1 y ⇒ (y = x ∨ ∃ y′, (y=y′+1 ∧ x ≤1 y′)
Exemple 10   On peut montrer par induction l’équivalence des deux définitions de l’ordre. Pour cela on utilisera la récurrence sur les entiers en plus de l’induction sur les relations.
 
x ≤1 x 
     
x ≤1 y 
x ≤1 (y+1) 
               
 
0 ≤2 x 
     
x ≤2 y 
(x+1) ≤2 (y+1) 
La donnée de ce système d’inférence, définit deux relations x1 y et x2 y qui vérifient les propriétés suivantes.

Pour la relation x1 y :

  1. x ∈ ℕ,x1 x
  2. x y ∈ ℕ,x1 yx1 y+1
  3. pour tout prédicat P(x,y),
    (∀ x ∈ ℕ,P(x,x)) ⇒ (∀ x y ∈ ℕ, P(x,y) ⇒ P(x,y+1)) ⇒ ∀ x y ∈ ℕ,x1 yP(x,y)
  4. Schéma généralisé:
    (∀ x ∈ ℕ,P(x,x)) ⇒ (∀ x y ∈ ℕ,x1 yP(x,y) ⇒ P(x,y+1)) ⇒ ∀ x y ∈ ℕ,x1 yP(x,y)

Pour la relation x2 y :

  1. x ∈ ℕ,0 ≤2 x
  2. x y ∈ ℕ,x2 yx+1 ≤2 y+1
  3. pour tout prédicat P(x,y),
    (∀ x ∈ ℕ,P(0,x)) ⇒ (∀ x y ∈ ℕ, P(x,y) ⇒ P(x+1,y+1)) ⇒ ∀ x y ∈ ℕ,x2 yP(x,y)
  4. Schéma généralisé:
    (∀ x ∈ ℕ,P(0,x)) ⇒ (∀ x y ∈ ℕ,x2 yP(x,y) ⇒ P(x+1,y+1)) ⇒ ∀ x y ∈ ℕ,x2 yP(x,y)

Pour montrer x1 yx2 y, on utilise une raisonnement inductif sur la relation x1 y. Il suffit de montrer que la relation x2 y satisfait les propriétés de la définition de x1 y c’est-à-dire:

∀ x ∈ ℕ, x ≤2 x       ∀ x  y∈ ℕ, x ≤2 y ⇒ x ≤2 y+1

L’autre direction se fait de manière analogue et est laissée en exercice.

  1. La première propriété se prouve par récurrence sur x, il suffit de montrer :
    0 ≤2 0         ∀ xx ≤2 x ⇒ x+1 ≤2 x+1
    qui sont des conséquences triviales des propriétés de définition de x2 y.
  2. La seconde propriété peut se montrer en utilisant un raisonnement inductif sur la définition de x2 y en prenant pour relation P(x,y)  =def  x2 y+1. Il suffit de démontrer que P satisfait les propriétés de définition de x2 y, c’est-à-dire :
    ∀ x∈ ℕ,0 ≤2 x+1       ∀ x  y∈ ℕ, x ≤1 y+1 ⇒ x+1 ≤2 (y+1)+1
    ces deux propriétés sont des conséquences directes des propriétés de définition de x2 y.
Exercice 5   Un robot se déplace sur une ligne, il peut se déplacer soit de 6 pas en avant, soit de 4 pas en arrière.
On représente la position du robot par un entier relatif
x ∈ ℤ. Initialement le robot se trouve à la position 0.
  1. Définir par un système d’inférence un prédicat pos tel que pos(x) est vrai si le robot peut atteindre la position x.
  2. Donner une preuve (sous forme d’arbre de dérivation) que la position 4 peut être atteinte.
  3. Ecrire le principe d’induction associé à la définition pos.
  4. Montrer que toutes les positions qui peuvent être atteintes sont des entiers pairs.
  5. Montrer que si x peut être atteint alors x+2 et x−2 peuvent aussi être atteintes.

3.4  Définition récursive de fonction

Une manière naturelle de définir une application f dans ℕ → A consiste à définir la valeur aA de l’application pour 0 et pour un entier m ∈ ℕ arbitraire de définir f(m+1) en fonction de m et de f(m), c’est-à-dire se donner une application G dans ℕ × AA telle que f(m+1)=G(m,f(m)). On dit que la fonction f est définie de manière primitive récursive.

Proposition 2 (Définition primitive récursive)   Nous allons montrer qu’étant donnés aA et G dans ℕ × AA il existe une unique application f dans ℕ → A telle que
f(0)=a           f(m+1)=G(m,f(m))

Preuve: Définir une application dans ℕ → A revient à définir une relation binaire fonctionnelle F(n,x) de ℕ× A, ce que l’on peut faire par cloture de la manière suivante :

 
F(0,a
       
F(m,x
F(m+1,G(m,x)) 

Il faut ensuite montrer que cette relation est fonctionnelle, c’est-à-dire :

∀ n  x  yF(n,x) ⇒ F(n,y) ⇒ x=y

On commence par montrer une propriété d’inversion:

∀ n  xF(n,x) ⇒ (n=0∧ x=a) ∨ ∃ m  yn=m+1 ∧ F(m,y) ∧ x=G(n,y)

ce qui se fait simplement par une induction généralisée. On utilise ensuite une induction simple sur F en utilisant la propriété : P(n,x)  =def  ∀ y, F (n,y) ⇒ x=y. On montre ensuite que f est unique. Pour cela on suppose qu’il existe une fonction g qui vérifie les équations. On montre la propriété n∈ ℕ,f(n)=g(n) sans difficulté par récurrence sur n.

Fonctions avec paramètres.

Ce schéma se généralise pour des fonctions à plusieurs arguments.

Si on veut définir une fonction dans ℕ× BA, on se donne une fonction HBA pour le cas 0 et G dans ℕ × A × BA pour le passage au successeur. On montre alors qu’il existe une unique fonction f ∈ ℕ× BA telle que

f(0,b)=H(b)        f(n+1,b)=G(n,f(n,b),b)
Exemple 11   Beaucoup de fonctions usuelles sur les entiers peuvent être définies ainsi.

Définition avec accumulateur.

Lorsque l’on définit une fonction de ℕ× BC de manière récursive sur le premier argument entier, il peut être utile dans la définition de l’équation récursive pour f(n+1,b) au lieu de simplement mentionner f(n,b) de pouvoir utiliser f(n,t) pour un terme t quelconque qui dépend de n et b.

Par exemple pour une définition récursive de l’ordre sur les entiers on peut utiliser :

le(0,m)=true    le(n+1,m)=false si m=0    le(n+1,m)=le(n,m−1) si m≠0

De manière générale, on peut se donner en plus des fonctions H et G, une fonction T ∈ ℕ × BB et résoudre les équations :

f(0,b)=H(b)   f(n+1,b)=G(n,f(n,T(n,b)),b)

Pour justifier ce schéma, on fait une définition par clotûre comme dans le cas simple et les preuves de fonctionnalité et de totalité suivent les mêmes schémas.

Remarque.

La notion de définition par cloture est au centre des langages de programmation tels que Prolog. Des relations sont introduites par des formules logiques particulières (des clauses de Horn) qui peuvent se voir comme des règles d’inférence. Le compilateur prend en entrée une formule R(u1,…,uk) et cherche à construire un arbre de dérivation dont la conclusion est la formule à prouver (ou une instance de cette formule si celle-ci contient des variables).

Les définitions par cloture sont également un outil important en informatique pour décrire les propriétés des langages de programmation (règles de typage, résultat de l’évaluation …).

Les définitions récursives de fonctions sont un moyen opérationnel de construire des programmes informatiques. C’est la base de la programmation fonctionnelle.


Previous Up Next