Mathématiques pour l’Informatique 2 2016–17 http://www.lri.fr/~blsk/MI2
Mathématiques pour l’Informatique 2 |
4 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.
4.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 :
-
une preuve de P(0) (le cas de base, appelé aussi initialisation)
- 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.
4.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 :
-
la relation contient 3 et 5
- si la relation contient x et y, elle contient aussi x+y
Cela peut se traduire par les trois formules suivantes :
S(3) S(5) ∀ x y, S(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(x−y).
Exercice 2
-
Trouver deux autres relations sur les entiers qui vérifient les mêmes propriétés que S (juste pour l’addition).
- Montrer S(11).
- En utilisant la définition avec soustraction, montrer S(1), S(−1). Que peut-on en déduire ?
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 case à droite et 2 cases vers le haut
- 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 n ≤ m 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 x≤ y+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:
-
∀ x, P(x) ⇒ ¬ P(x)
- ∀ x, ¬ P(x) ⇒ P(x)
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.
4.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:
-
-
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
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.
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:
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 R ⊆ S 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 :
-
Elle satisfait les propriétés associées aux règles d’inférence:
∀ x1,…,xp,T1 ⇒ ⋯ ⇒ Tn ⇒
R(t1,…,tk) |
- C’est la plus petite qui satisfait ces propriétes : soit une
relation P(y1,…,yk). Si pour chaque règle d’inférence
la propriété P
satisfait la règle, c’est-à-dire:
∀ x1,…,xp,T1(P) ⇒ ⋯ ⇒ Tn(P) ⇒
P(t1,…,tk) |
alors R est incluse dans P donc:
∀ y1,…,yk, R(y1,…,yk) ⇒ P(y1,…,yk) |
Lorsqu’on utilise ce schéma de preuve, on parle de raisonnement
inductif ou encore de preuve par induction.
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 :
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 :
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
| | step(x,y) path(y,z) |
|
path(x,z) |
|
Exercice 4
Donner deux autres définitions par cloture de la même relation:Preuve:
-
path(x,y) step(y,z) |
|
path(x,z) |
-
path(x,y) path(y,z) |
|
path(x,z) |
□
4.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
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 ∈ℕ, x ≤1 y ⇒ P(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.
La donnée de ce système d’inférence, définit deux relations
x≤1 y et x≤2 y qui vérifient les propriétés
suivantes.Pour la relation x≤1 y :
-
∀ x ∈ ℕ,x ≤1 x
- ∀ x y ∈ ℕ,x ≤1 y ⇒ x ≤1 y+1
- pour tout prédicat P(x,y),
(∀ x ∈ ℕ,P(x,x)) ⇒ (∀ x y ∈ ℕ,
P(x,y) ⇒ P(x,y+1)) ⇒ ∀ x y ∈ ℕ,x ≤1 y ⇒
P(x,y)
- Schéma généralisé:
(∀ x ∈ ℕ,P(x,x)) ⇒ (∀ x y ∈ ℕ,x ≤1 y
⇒ P(x,y) ⇒ P(x,y+1)) ⇒ ∀ x y ∈ ℕ,x ≤1 y ⇒ P(x,y)
Pour la relation x≤2 y :
-
∀ x ∈ ℕ,0 ≤2 x
- ∀ x y ∈ ℕ,x ≤2 y ⇒ x+1 ≤2 y+1
- pour tout prédicat P(x,y),
(∀ x ∈ ℕ,P(0,x)) ⇒ (∀ x y ∈ ℕ,
P(x,y) ⇒ P(x+1,y+1)) ⇒ ∀ x y ∈ ℕ,x ≤2 y ⇒ P(x,y) - Schéma généralisé:
(∀ x ∈ ℕ,P(0,x)) ⇒ (∀ x y ∈ ℕ,x ≤2 y
⇒ P(x,y) ⇒ P(x+1,y+1)) ⇒ ∀ x y ∈ ℕ,x ≤2 y ⇒ P(x,y)
Pour montrer x ≤1 y ⇒ x ≤2 y,
on utilise une raisonnement inductif sur la relation x ≤1
y. Il suffit de montrer que la relation x ≤2 y
satisfait les propriétés de la définition de x ≤1 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.
-
La première propriété se prouve par récurrence sur x, il
suffit de montrer :
0 ≤2 0 ∀ x, x ≤2 x
⇒ x+1 ≤2 x+1 |
qui sont des conséquences triviales des
propriétés de définition de x ≤2 y.
- La seconde propriété peut se montrer en utilisant un raisonnement
inductif sur la définition de x ≤2 y en prenant pour
relation P(x,y) =def x ≤2 y+1. Il suffit de démontrer
que P satisfait les propriétés de définition de
x ≤2 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 x ≤2 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.-
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.
- Donner une preuve (sous forme d’arbre de dérivation) que la position 4 peut être atteinte.
- Ecrire le principe d’induction associé à la définition pos.
- Montrer que toutes les positions qui peuvent être atteintes sont des entiers pairs.
- Montrer que si x peut être atteint alors x+2 et x−2 peuvent aussi être atteintes.
4.4 Définition récursive de fonction
Une manière naturelle de définir une application f dans
ℕ → A consiste à définir la valeur a∈ A 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
ℕ × A → A 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 a∈ A et G dans
ℕ × A → A il existe une unique application
f dans
ℕ → A telle que
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 :
Il faut
ensuite montrer que cette relation est fonctionnelle, c’est-à-dire :
∀ n x y, F(n,x) ⇒ F(n,y) ⇒ x=y |
On commence par
montrer une propriété d’inversion:
∀ n x, F(n,x) ⇒
(n=0∧ x=a) ∨ ∃ m y, n=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 ℕ× B → A, on se
donne une fonction H ∈ B → A pour le cas 0 et
G dans ℕ × A × B → A pour le passage au
successeur. On montre alors qu’il existe une unique fonction f
∈ ℕ× B → A 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.
-
L’addition plus est définie par plus(0,y)=y plus(x+1,y)=plus(x,y)+1.
Les fonctions intermédiaires utilisées sont
H(y)=y G(n,z,y)=z+1.
- La multiplication est définie par mult(0,y)=0
mult(x+1,y)=plus(mult(x,y),y).
Les fonctions intermédiaires
utilisées sont H(y)=0 G(n,z,y)=plus(z,y).
Définition avec accumulateur.
Lorsque l’on définit une fonction de ℕ× B → C 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 ∈ ℕ × B → B 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.