forked from petervanroy/lingi1101
-
Notifications
You must be signed in to change notification settings - Fork 0
/
partie13.tex
154 lines (132 loc) · 8.69 KB
/
partie13.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
%document réalisé par Scott Ivinza, Florent Lejoly, Cédric Vanden Buckle et Guillaume Demaude
\section{Théorie de l'égalité (EG)}
Le concept d'égalité est omniprésent dans les mathématiques.
Nous allons définir une théorie pour le formaliser.
D'abord, il faut faire attention à la notation.
Il existe différents symboles pour représenter l'égalité :
\begin{itemize}
\item E(x,y)
\item $x = y$
\item $x == y $
\end{itemize}
Nous allons utiliser ``$==$'' dans la suite de ce cours pour représenter l'égalité.
La théorie de l'égalité est souvent {\em ajoutée} à d'autres axiomes pour être utile en pratique.
Dans cette section on donne que les axiomes d'égalité. Dans la suite nous allons voir comment
ajouter l'égalité à d'autres théories.
\subsection{Axiomes}
Pour définir ce qu'est une égalité, nous avons d'abord besoin de définir 3 axiomes et 2 schémas d'axiomes:
\begin{enumerate}
\item Réflexivité \\$\forall x, x==x$
\item Symétrie \\$\forall x, \forall y, x==y \Rightarrow y==x$
\item Transitivité \\$\forall x, \forall y, \forall z, (x==y \land y==z) \Rightarrow x==z$
\item Substituabilité dans les fonctions\\$\forall x, x_{1}, ..., x_i, ..., x_{n}\ .\ x==x_i \Rightarrow f(..., x, ...) == f(..., x_i, ...)$
\item Substituabilité dans les prédicats\\$\forall x, x_{1}, ..., x_i, ..., x_{n}\ .\ x==x_i \Rightarrow P(..., x, ...) == P(..., x_i, ...)$
\end{enumerate}
Les deux derniers axiomes sont des {\em schémas}: chaque schéma définit plusieurs axiomes, où on remplace $f$ par tout symbole de fonction et $P$ par tout symbole de prédicat.
\subsection{Règles d'inférences}
En plus de ces 5 axiomes, il nous faut aussi définir deux règles d'inférences.\\ \\
Substituabilité fonctionnelle
$$ \frac{s_{1}==t_{1} \land s_{2}==t_{2} \land ... \land s_{n}==t_{n}}{f(s_{1},s_{2},...,s_{n}) == f(t_{1},t_{2},...,t_{n})}$$
Substituabilité prédicative
$$ \frac{s_{1}==t_{1} \land s_{2}==t_{2} \land ... \land s_{n}==t_{n}}{P(s_{1},s_{2},...,s_{n}) == P(t_{1},t_{2},...,t_{n})}$$
\subsection{Théorème sur la sémantique de l'égalité}
$$\mathrm{Si}\ \ \mathrm{VAL}_{I}(t_{1}) == \mathrm{VAL}_{I}(t_{2}) \ \ \mathrm{alors}\ \ \mathrm{VAL}_{I}(t_{1} == t_{2}) = \mathrm{true}$$
L'égalité comme elle est définie ici est une propriété syntaxique qui nous permet de faire des preuves.
Avec ce théorème, nous pouvons aussi raisonner sur un modèle (c'est-à-dire la sémantique) pour déterminer l'égalité.
C'est-à-dire, si deux termes donnent la même entité dans le domaine de discours, alors on peut dire que les
deux termes sont égaux.
\subsubsection{Preuve}
Voici la preuve étape par étape:
\begin{itemize}
\item Soit $I$ un modèle de EG et deux termes quelconques $t_{1}$ et $t_{2}$.
\item Par définition $\mathrm{VAL}_{I}(t_{1} == t_{2}) = \mathrm{VAL}_{I}(==)(\mathrm{VAL}_{I}(t_{1}), \mathrm{VAL}_{I}(t_{2}))$.
\item On pose $VAL_{I}(==) = E_{I}$ et $VAL_{I}(t_{1}) = e_1$ et $VAL_{I}(t_{2}) = e_2$.
\item La prémisse du théorème nous dit que $e_1 = e_2 = e$.
\item Donc $\mathrm{VAL}_{I}(t_{1} == t_{2}) =E_{I}(e,e)$.
\item L'axiome de réflexivité nous dit $\mathrm{VAL}_{I}(\forall x.\ x==x)= \mathrm{true}$.
\item La sémantique de $\forall$ nous dit que pour tout $d \in D_I$, il est vrai que $\mathrm{VAL}_{I}(d==d)=\mathrm{true}$.
\item On prend $d=e$ et on peut conclure que $E_{I}(e,e)=\mathrm{true}$.
\end{itemize}
\vspace{\baselineskip}
Remarquez que ceci n'est pas une preuve en logique des prédicats, mais une preuve en méta-langage, c'est-à-dire
une preuve qui parle de la logique des prédicats.
On ne peut pas formaliser cette preuve comme un objet formel qui est une preuve en logique des prédicats.
Toute l'argumentation sur la sémantique de la logique des prédicats et la justification des règles de preuve
sont des raisonnements en méta-langage.
\section{Théorie de l'ordre partiel (OP)}
Pour définit la théorie de l'ordre partiel, nous prenons EG et nous ajoutons un symbole en
plus du symbole d'égalité:
On ajoute un deuxième symbole dans le langage en plus du symbole d'égalité.
\begin{itemize}
\item $\leq$
\end{itemize}
Les axiomes d'égalité sont déjà présents.
Il nous reste de faire les axiomes pour ce nouveau symbole.
\subsection{Axiomes}
Aux axiomes et schémas d'axiomes de la théorie de l'égalité, on rajoute de nouveaux axiomes:
\begin{enumerate}
\item Réflexivité \\$\forall x$, $x\leq x$
\item Anti-symétrie \\$\forall x$, $\forall y$, $ x\leq y \land y\leq x\Rightarrow y==x$
\item Transitivité \\$\forall x$, $\forall y$, $\forall z$, $(x\leq y \land y\leq z) \Rightarrow x\leq z$
\item Substituabilité à gauche \\$\forall x_{1}$, $\forall x_{2}$, $\forall x$, $x_{1}==x \Rightarrow x_{1}\leq x_{2} \Leftrightarrow x \leq x_{2}$
\item Substituabilité à droite \\$\forall x_{1}$, $\forall x_{2}$, $\forall x$, $x_{2}==x \Rightarrow x_{1}\leq x_{2} \Leftrightarrow x_{1} \leq x$
\end{enumerate}
\subsubsection{Exemple de théorème}
Nous allons prouver le théorème suivant:
$$\models \forall x.\ \forall y.\ [x==y \Leftrightarrow (x\leq y)\land (y \leq x)] $$
\subsubsection{Preuve}
Le théorème n'est pas une formule en logique des prédicats, mais en méta-langage.
La preuve va donc être démontrée en partie en méta-langage.
\begin{align*}
\Leftrightarrow \text{equivaut à :} \Leftarrow \land \Rightarrow \\
\Leftarrow \text{: est démontré par l'axiome antisymétrique} \\
\Rightarrow \models_{op} \forall x, \forall y, [x\leq y \land y \leq x]
\end{align*}
\underline{Preuve formelle :}
\begin{enumerate}
\item $ \forall x, \forall y, x==y \Rightarrow x \leq x \Leftrightarrow y \leq x$ \hfill substituabilité à gauche
\item $ \forall x, \forall y, x==y \Rightarrow x \leq x \Leftrightarrow x \leq y$ \hfill substituabilité à droite
\item $ x==y \Rightarrow x \leq x \Leftrightarrow y \leq x $ \hfill $\forall$ élimination
\item $ x==y \Rightarrow x \leq x \Leftrightarrow x \leq y $ \hfill $\forall$ élimination
\end{enumerate}
\underline{Preuve conditionnelle :}
\begin{enumerate}
\setcounter{enumi}{4}
\item $ x==y$ \hfill supposition
\item $ y\leq x$ \hfill modus ponens (1,4)
\item $ x\leq y$ \hfill modus ponens (2,4)
\item $ y\leq x \land x\leq y$ \hfill conjonction (6,7)
\item $ x==y \Rightarrow x \leq x \Leftrightarrow y\leq x \land x\leq y$
\item $ \forall x, \forall y, x==y \Rightarrow x \leq x \Leftrightarrow y\leq x \land x\leq y$ \hfill $\forall$ Introduction
\end{enumerate}
\subsection{Exemples de modèles d'OP}
\begin{itemize}
\item \underline{$I_{1}$} : $D_{I_{1}} = \mathbb{Z}$ \\
$ val_{I_{1}}(==) = '=' :$ égalité d'entiers \\
$ val_{I_{1}}(\leq) = '\leq' :$ plus petit ou égal pour les entiers\\
Cette interprétation va satisfaire tous les entiers.
\item \underline{$I_{2}$} : $D_{I_{2}} = P(E)$ ensemble des sous-ensembles de E\\
$ val_{I_{2}}(==) = '=' :$ égalité d'ensemble \\
$ val_{I_{2}}(\leq) = '\subseteq' :$ inclusion d'ensemble
\item \underline{$I_{3}$} : $D_{I_{3}} = ALPH^{2} = {(l_{1},l_{2}),..}$ doublons de lettres de l'alphabet\\
$ val_{I_{3}}(==) = $ égalité des paires \\
$ val_{I_{3}}(\leq) =$ suivant ordre lexicographique\\
Exemple : $(l_{i},l_{j}) \leq (l_{p},l_{q})$ si $ l_{i} < l_{p}$ ou $ l_{i} = l_{p}$ et $ l_{j} < l_{q}$ ou $ l_{j} = l_{q}$
\item \underline{$I_{3}$} : $D_{I_{4}} =$ ensemble de listes\\
$ val_{I_{4}}(==) = $ = égalité de liste (si elles possèdent les mêmes composants à la même position)\\
$ val_{I_{3}}(\leq) =$ "suffixe de" \\
Exemple : $l_{1} $ est suffixe de $l_{2}$ \\
$l_{1} $ = [d, e, f, g, h] et $l_{2} =$ [a, b, c, d, e, f, g, h, i]
\item \underline{$I_{5}$} : Soit D$_{I_{5}}$ l'ensemble des formules en logique des propositions. On commence à utiliser la logique pour parler d'elle-même:\\
VAL$_{I_{5}}$(==) = "$\Lleftarrow \Rrightarrow$" : L'égalité est synonyme d'équivalence en logique des propositions \\
VAL$_{I_{5}}$($\leq$) = "$\models$" : Le signe d'inclusion entre les ensembles de modèles.
Maintenant qu'on a défini la sémantique de l'ordre partiel en utilisant la notion de modèles, on peut prendre quelques exemples en raisonnant sur la logique :\\
p $\leq_{I_{5}}$ q \hspace{1.5cm} p $\models_{I_{5}}$ q \hspace{1.5cm} $\models$ p $\Rightarrow$ q
\item \underline{$I_{6}$} : D$_{I_{6}}$ = l'ensemble des unificateurs d'un ensemble S de termes ou de formules
VAL$_{I_{6}}$(==) = égalité entre substitutions \{ (x$_{i}$,t$_{i}$)... \} : un ensemble de paires avec une variable et un terme VAL$_{I_{6}}$($\leq$) = "moins général que"\\
\newline
Exemple: P(x,f(y)) \hspace{1cm} $\underbrace{P(x,z)}_{\sigma}$\\
$\sigma$' = $\sigma$ $\cup$ \{(z, f(y)\} donc
$\sigma$' $\leq$ $\sigma$\\
\end{itemize}
Ces exemples montrent qu'on peut raisonner sur tout, y compris sur la logique et les algorithmes eux-mêmes, à partir du moment où on respecte les axiomes.