{ "cells": [ { "cell_type": "markdown", "metadata": {}, "source": [ "# Formules Logiques" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Marc Lorenzi - 20 avril 2018" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "import matplotlib.pyplot as plt\n", "%matplotlib inline\n", "import random, sys" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## 1. Syntaxe des formules" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 1.1 Notion de formule" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "On se donne un ensemble $\\mathcal V$ dont les éléments sont appelés les __variables propositionnelles__. La nature exacte de $\\mathcal V$ n'a pas d'importance. De façon informelle, lorsque nous aurons besoin de variables nous les noterons $x, y, z, a, b, a_0$, etc. \n", "\n", "On pose également $\\mathcal S = \\{-, +, ., \\rightarrow, \\leftrightarrow\\, (, )\\}$. Nous appellerons formule toute suite de symboles (les informaticiens disent \"chaîne de caactères\", les théoriciens disent \"mot\") de $\\mathcal V \\cup \\mathcal S$ vérifiant les propriétés suivantes :\n", "\n", "- Les éléments de $\\mathcal V$ sont des formules.\n", "- Si $f$ est une formule, $-f$ est une formule.\n", "- Si $f_1$ et $f_2$ sont des formules, $(f_1 . f_2)$ est une formule.\n", "- Si $f_1$ et $f_2$ sont des formules, $(f_1 + f_2)$ est une formule.\n", "- Si $f_1$ et $f_2$ sont des formules, $(f_1 \\rightarrow f_2)$ est une formule.\n", "- Si $f_1$ et $f_2$ sont des formules, $(f_1 \\leftrightarrow f_2)$ est une formule." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "\"$-$\" est le __connecteur unaire__ (il symbolise la négation). \"$+$\", \"$.$\", \"$\\rightarrow$\" et \"$\\leftrightarrow$\" sont les __connecteurs binaires__. Le point symbolise le \"et\", le $+$ représente le \"ou\", et les flèches $\\rightarrow$ et $\\leftrightarrow$ représentent l'implication et l'équivalence. Le choix des symboles de connecteurs est guidé par le fait qu'ils sont faciles à entrer au clavier. \n", "\n", "On adopte également des conventions de priorité qui permettent de ne pas écrire certaines parenthèses : les connecteurs, du plus prioritaire au moins prioritaire, sont $-, ., +, \\rightarrow, \\leftrightarrow$. Ainsi, par exemple, $(x\\rightarrow y)+(y\\rightarrow z)\\leftrightarrow (x\\rightarrow z)$ est une façon abrégée d'écrire la formule $(((x\\rightarrow y)+(y\\rightarrow z))\\leftrightarrow (x\\rightarrow z))$." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 1.2 Représenter les formules en Python" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Nous allons dans ce notebook écrire des fonctions qui prennent des formules en paramètre, qui calculent des formules, qui les combient entre-elles ... Il s'agit d'avoir une représentation des formules dans notre langage préféré qui nous permette de les manipuler efficacement. Cette formule est elle un \"et\" ? Une implication ? Quelles sont ses variables ? etc." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "On peut distinguer trois sortes de formules.\n", "\n", "- Les variables. Nous les représenterons par un couple `('var', x)` où $x$ est une chaîne de caractères, qui est le nom proprement dit de la variable.\n", "- La négation d'une formule. Nous représenterons une négation par le couple `('not', f1)` où $f_1$ est elle même la représentation d'une formule.\n", "- Les formules \"binaires\". Nous représenterons une telle formule par un triplet `(symb, f1, f2)` où `symb` peut prendre les valeurs `and`, `or`, `imp` et `eqv` (et, ou, implication et équivalence)." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Voici un exemple, la représentation de la formule $(x\\rightarrow y)+(y\\rightarrow z)\\leftrightarrow (x\\rightarrow z)$." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "exemple = ('eqv', \n", " ('and', ('imp', ('var', 'x'), ('var', 'y')), \n", " ('imp', ('var', 'y'), ('var', 'z'))\n", " ), \n", " ('imp', ('var', 'x'), ('var', 'z')))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "On voit tout de suite apparaître deux problèmes pratiques :\n", "\n", "1. C'est impossible à lire.\n", "2. C'est impossible à écrire.\n", "\n", "Nous allons petit à petit régler ces deux problèmes." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 1.3 Affichage des formules" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Résolvons déjà le premier problème : l'affichage d'une formule. Nous allons écrire une fonction qui, étant donnée une formule $f$, renvoie une représentation de $f$ sous forme d'une chaîne de caractères lisible par un être humain (enfin par un logicien)." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Voici deux fonctions évidentes. Pour une formule $f$ de type `('not', g)`, `left(f)` renvoie $g$. Pour une formule binaire, `left` et `right` renvoient les constituants de la formule. " ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def left(f): return f[1]\n", "def right(f): return f[2]" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "left(exemple)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "right(exemple)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Le dictionnaire `symbol` contient la représentation symbolique de chacun des connecteurs." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "symbol = {'not': '-', 'and': '.', 'or': '+', 'imp': '->', 'eqv': '<->'}" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "symbol['eqv']" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Le dictionnaire `prio` contient les priorités de tous les connecteurs. On a également assigné une priorité maximale aux variables." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "prio = {'var': 15, 'not': 10, 'and': 8, 'or': 6, 'imp': 4, 'eqv': 2}" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "La fonction `paren` prend en paramètres une chaîne de caractères $s$ et deux formules. Selon la priorité relative de ces formules, elle renvoie la chaîne $s$ entre parenthèses ou pas." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def paren(s, f1, f):\n", " if prio[f1[0]] <= prio[f[0]]: return '(' + s + ')'\n", " else: return s" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Et voici enfin la fonction `to_string`. Elle prend une formule $f$ en paramètre et renvoie une chaîne qui est une forme \"humainement lisible\" de la formule. Le code est simple, étudiez-le. En particulier, comprenez à quoi sert l'appel à `paren`." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def to_string(f):\n", " if f[0] == 'var': return f[1]\n", " elif f[0] == 'not': \n", " f1 = left(f)\n", " s1 = to_string(f1)\n", " return '-' + paren(s1, f1, f)\n", " else:\n", " smb = symbol[f[0]]\n", " f1 = left(f)\n", " f2 = right(f)\n", " s1 = to_string(f1)\n", " s2 = to_string(f2)\n", " return paren(s1, f1, f) + smb + paren(s2, f2, f)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "to_string(exemple)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "exemple" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 1.4 Hauteur d'une formule" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "La hauteur $h(f)$ d'une formule $f$ est définie comme suit :\n", "\n", "- La hauteur d'une variable est 0.\n", "- Si $f =-f_1$, alors $h(f)=1+h(f_1)$.\n", "- Si $f =f_1 \\alpha f_2$, où $\\alpha$ est un connecteur binaire alors $h(f)=1+\\max(h(f_1), h(f_2))$.\n", "\n", "Pourquoi appeler cela \"hauteur\" ? Lorsque nous verrons qu'à chaque formule on peut associer un arbre, on comprendra mieux. Ou alors, si on a déjà lu le notebook sur les arbres, on a déjà compris." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def hauteur(f):\n", " if f[0] == 'var': return 0\n", " elif f[0] == 'not' : return 1 + hauteur(left(f))\n", " else:\n", " h1 = hauteur(left(f))\n", " h2 = hauteur(right(f))\n", " return 1 + max([h1, h2])" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "hauteur(exemple)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 1.5 Formules \"aléatoires\"" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Pour tester les fonctions que nous allons écrire, il peut être intéressant de pouvoir fabriquer des formules un peu n'importe comment et très très compliquées. La fonction ci-dessous renvoie une formule \"aléatoire\" de hauteur $h$ dont les variables sont $a_0,a_1,\\ldots,a_{n-1}$." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def formule_aleatoire(h, n):\n", " if h == 0:\n", " p = random.randint(0, n - 1)\n", " return ('var', 'a' + str(p))\n", " else:\n", " f1 = formule_aleatoire(h - 1, n)\n", " p = random.randint(0, 4)\n", " if p == 0: return ('not', f1)\n", " else:\n", " h1 = random.randint(0, h - 1)\n", " f2 = formule_aleatoire(h1, n)\n", " b = random.randint(0, 1)\n", " if b == 1: f1, f2 = f2, f1\n", " if p == 1: return ('and', f1, f2)\n", " elif p == 2: return ('or', f1, f2)\n", " elif p == 3: return ('imp', f1, f2)\n", " else: return ('eqv', f1, f2)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "f = formule_aleatoire(10, 5)\n", "to_string(f)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "f" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "hauteur(f)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Ben oui c'est normal." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 1.6 Arbre associé à une formule" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Je vais ici supposer que vous avez jeté un coup d'oeil au notebook sur les arbres. Je ne reprendrai pas la définition de racine, de fils, de noeud, de feuille, etc. Si ce qui suit est d'une obscurité totale pour vous, sautez les explications et foncez à l'exemple !\n", "\n", "Eh oui, une formule, par exemple $f_1 + f_2$ peut être vue comme un arbre dont la racine est $+$ et les deux fils sont les arbres associés aux formules $f_1$ et $f_2$. Selon le type de la formule $f$, l'arbre qui la représente a différentes formes :\n", "\n", "- si $f$ est une variable $x$, l'arbre a juste un noeud, d'étiquette $x$.\n", "- Si $f =-g$, l'arbre a une racine étiquetée par $\\tilde{}$ et un seul fils qui est l'arbre qui représente $g$.\n", "- Si $f=f_1 . f_2$, l'arbre a une racine étiquetée par $.$ et deux fils qui sont les arbre qui représentent $f_1$ et $f_2$. Et de même pour les autres connecteurs binaires." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "La fonction `draw(f)` ci-dessous dessine l'arbre qui représente la formule `f`. Elle utilise une fonction auxiliaire `draw_aux`. Dans le notebook sur les arbres apparaissent des fonctions quasiment identiques." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def draw_aux(f, rect, dy):\n", " x1, x2, y1, y2 = rect\n", " xm = (x1 + x2) // 2\n", " if f[0] == 'var': noeud = f[1]\n", " else: noeud = symbol[f[0]]\n", " plt.text(xm + 3, y2, noeud, fontsize=12, horizontalalignment='left',verticalalignment='bottom')\n", " if f[0] == 'var': return\n", " if f[0] == 'not':\n", " draw_aux(left(f), (x1, x2, y1, y2 - dy), dy)\n", " a, b = ((xm, xm), (y2, y2 - dy))\n", " plt.plot(a, b, 'k', marker='o')\n", " else:\n", " draw_aux(left(f), (x1, xm, y1, y2 - dy), dy)\n", " draw_aux(right(f), (xm, x2, y1, y2 - dy), dy)\n", " a, b = ((xm, (x1 + xm) // 2), (y2, y2 - dy))\n", " plt.plot(a, b, 'k', marker='o')\n", " c, d = ((xm, (x2 + xm) // 2), (y2, y2 - dy))\n", " plt.plot(c, d, 'k', marker='o')" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def draw(f):\n", " d = 512\n", " pad = 20\n", " dy = (d - 2 * pad) / (hauteur(f))\n", " draw_aux(f, (pad, d - pad, pad, d - pad), dy)\n", " plt.axis([0, d, 0, d])\n", " plt.axis('off')\n", " plt.show()" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "La ligne suivante, c'est pour que nos arbres soient affichés assez gros à l'écran." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "plt.rcParams['figure.figsize'] = (12, 8)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Testons `draw` ..." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "draw(exemple)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "f = formule_aleatoire(6, 5)\n", "draw(f)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 1.7 Les variables d'une formule" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Quelles sont les variables qui interviennent dans une formule ? La fonction ci-dessous résout le problème." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def variables(f):\n", " if f[0] == 'var': return set([f[1]])\n", " elif f[0] == 'not': return variables(f[1])\n", " else: return variables(f[1]).union(variables(f[2]))" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "variables(exemple)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "variables(formule_aleatoire(8, 6))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## 2. Un analyseur syntaxique" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "#### Ce paragraphe n'est pas facile. Il peut être sauté sans honte en première lecture." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "L'ensemble des formules logiques est un langage, c'est à dire un ensemble de mots, dont les lettres appartiennent à l'alphabet $\\mathcal A = \\mathcal V\\cup\\mathcal S$ que nous avons défini au début de ce notebook. Étant donné un mot sur l'alphabet $\\mathcal A$ qui représente une formule valide, nous voudrions décrire un algorithme qui permet de l'analyser pour en déduire la représentation en Python de la formule. Histoire de compliquer un peu les choses, on autorise un parenthésage \"minimal\". \n", "\n", "La tâche paraît ardue." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 2.1 Premier jet" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Appelons irréductible toute formule qui ne contient que des parenthèses, des \"not\", et une variable. Une telle formule peut être de trois sortes :\n", "\n", "- $x$, où $x$ est une variable\n", "- $(f)$ où $f$ est une formule irréductible\n", "- $-f$ où $f$ est irréductible. \n", "\n", "On peut résumer cela par la ligne\n", "\n", "`I ::= -I | V | (I)`\n", "\n", "La barre verticale signifie \"ou bien\", $V$ et $I$ signifient respectivement \"variable\" et \"formule irréductible\"" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "La fonction `parseI` ci-dessous prend une chaîne de caractères $s$ en paramètre. Elle renvoie un couple $(f, r)$ où $f$ est le formule irréductible représentée par le plus petit __préfixe__ possible de $s$, et $r$ est la partie de $s$ qui n'a servi à rien (c'est un __suffixe__ de $s$).\n", "\n", "__Remarque__ : un préfixe d'une chaîne de caractères $s$ est une chaîne constituée des premières lettres de $s$. Par exemple, les préfixes de 'bonjour' sont '', 'b', 'bo', 'bon', ..., 'bonjour'. Un préfixe de $s$ différent $s$ est dit __strict__. On définit bien sûr de même la notion de __suffixe__. " ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def parseI(s):\n", " if s[0] == '(':\n", " f, reste = parseI(s[1:])\n", " assert reste[0] == ')'\n", " return (f, reste[1:])\n", " elif s[0] == '-':\n", " f, reste = parseI(s[1:])\n", " return (('not', f), reste)\n", " else:\n", " return (('var', s[0]), s[1:])" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Par exemple, prenons $s=--(-((x)))(y\\to z)$. La partie intéressante du début de $s$ est $--(-((x)))$. Le reste est $(y\\to z)$." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "parseI('--(-((x)))(y->z)')" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 2.2 On complique un peu" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Tâchons maintenant d'analyser des formules contenant des \"et\", des \"not\", des variables et des parenthèses. Une formule de cette sorte est essentiellement\n", "\n", "- une formule irréductible, ou bien\n", "- une formule irréductible \"et\" une autre formule de cette sorte\n", "\n", "Notons `E4` une telle formule : `E4 ::= I . E4 | I`\n", "\n", "Oui, d'accord, à condition de redéfinir `I`en : `I ::= -I | V | (E4)`. Eh oui, une expression de type `E4` avec une paire de parenthèses englobantes doit être considérée comme irréductible ! Le code Python devient donc :" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def parse4(s):\n", " f, reste = parseI(s)\n", " if len(reste) >= 1 and reste[0] == '.':\n", " f1, reste1 = parse4(reste[1:])\n", " return (('and', f, f1), reste1)\n", " else:\n", " return (f, reste)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def parseI(s):\n", " if s[0] == '(':\n", " f, reste = parse4(s[1:])\n", " assert reste[0] == ')'\n", " return (f, reste[1:])\n", " elif s[0] == '-':\n", " f, reste = parseI(s[1:])\n", " return (('not', f), reste)\n", " else:\n", " return (('var', s[0]), s[1:])" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Testons ..." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "parse4('a.(a.-b)c->d')" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Le premier préfixe de notre exemple qui est de type `E4` est correctement analysé, et tout ce qui suit est renvoyé sans y toucher. " ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 2.3 On rajoute les $+$" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Attaquons nous à l'analyse des formules contenant des \"ou\", des \"et\", des \"not\", des variables et des parenthèses. Une formule de cette sorte est essentiellement\n", "\n", "- une formule du type `E4`, ou bien\n", "- une formule du type `E4` \"ou\" une autre formule de cette sorte\n", "\n", "Notons `E3` une telle formule : `E3 ::= E4 . E3 | E4`\n", "\n", "Pourquoi cela fonctionne-t-il ? parce que le \"et\" est prioritaire par rapport au \"ou\" !\n", "\n", "Le code Python devient donc :" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def parse3(s):\n", " f, reste = parse4(s)\n", " if len(reste) >= 1 and reste[0] == '+':\n", " f1, reste1 = parse3(reste[1:])\n", " return (('or', f, f1), reste1)\n", " else:\n", " return (f, reste)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def parse4(s):\n", " f, reste = parseI(s)\n", " if len(reste) >= 1 and reste[0] == '.':\n", " f1, reste1 = parse4(reste[1:])\n", " return (('and', f, f1), reste1)\n", " else:\n", " return (f, reste)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def parseI(s):\n", " if s[0] == '(':\n", " f, reste = parse4(s[1:])\n", " assert reste[0] == ')'\n", " return (f, reste[1:])\n", " elif s[0] == '-':\n", " f, reste = parseI(s[1:])\n", " return (('not', f), reste)\n", " else:\n", " return (('var', s[0]), s[1:])" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Testons ..." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "parse3('a.b+-(c.d)+e->f')" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Le premier préfixe de notre exemple qui est de type `E3` est correctement analysé, et tout ce qui suit, c'est à dire $\\to f$, est renvoyé sans y toucher. " ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 2.4 On rajoute implications et équivalences" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Rajouter les derniers connecteurs ne pose pas de problème supplémentaires. Il faut juste prendre garde à leur priorité : les moins prioritaires d'abord. Appelons `E1` le type des formules qui sont des équivalences et `E2` le type des formules qui sont des implications. Voici enfin la __grammaire__ complète des formules : " ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "`E1 ::= E2 <-> E1 | E2`\n", "\n", "`E2 ::= E3 -> E2 | E3`\n", "\n", "`E3 ::= E4 + E3 | E4`\n", "\n", "`E4 ::= I . E4 | I`\n", "\n", "`I ::= -I | V | (E1)`" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Je vous suggère d'écrire quelques formules et de réfléchir à la question avant de poursuivre ..." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Notre analyseur de formules est donc composé de 5 fonctions, une pour chaque ligne de la grammaire. Chacune des fonctions appelle la fonction de numéro \"un de plus\", sauf la dernière qui peut se permettre d'appeler la première. Oui, nous avons là 5 fonctions mutuellement récursives.\n", "\n", "Chacune de ces fonctions prend en paramètre une chaine de caractères $s$. Elle analyse le début de $s$ jusqu'à trouver une formule bien formée pour la fonction en question. Puis la fonction renvoie un couple formé de la formule trouvée et du reste non analysé de $s$." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def parse1(s):\n", " f, reste = parse2(s)\n", " if len(reste) >= 3 and reste[0:3] == '<->':\n", " f1, reste1 = parse1(reste[3:])\n", " return (('eqv', f, f1), reste1)\n", " else:\n", " return (f, reste)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def parse2(s):\n", " f, reste = parse3(s)\n", " if len(reste) >= 2 and reste[0:2] == '->':\n", " f1, reste1 = parse2(reste[2:])\n", " return (('imp', f, f1), reste1)\n", " else:\n", " return (f, reste)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def parse3(s):\n", " f, reste = parse4(s)\n", " if len(reste) >= 1 and reste[0] == '+':\n", " f1, reste1 = parse3(reste[1:])\n", " return (('or', f, f1), reste1)\n", " else:\n", " return (f, reste)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def parse4(s):\n", " f, reste = parseI(s)\n", " if len(reste) >= 1 and reste[0] == '.':\n", " f1, reste1 = parse4(reste[1:])\n", " return (('and', f, f1), reste1)\n", " else:\n", " return (f, reste)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def parseI(s):\n", " if s[0] == '(':\n", " f, reste = parse1(s[1:])\n", " assert reste[0] == ')'\n", " return (f, reste[1:])\n", " elif s[0] == '-':\n", " f, reste = parseI(s[1:])\n", " return (('not', f), reste)\n", " else:\n", " return (('var', s[0]), s[1:])" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Pour analyser la chaîne $s$, on appelle `parse1`, qui renvoie un couple $(f, r)$ et on laisse tomber $r$ ... qui devrait être la chaîne vide. Disons-le clairement, cet analyseur n'est pas bien solide :\n", "\n", "- il n'accepte que des variables propositionnelles de 1 caractère\n", "- il ne supporte pas les espaces\n", "- il ne fait aucun effort pour détecter les erreurs de syntaxe\n", "\n", "Mais il suffira pour ce que nous voulons en faire : taper rapidement des exemples." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def parse(s):\n", " f, reste = parse1(s)\n", " return f" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Testons !" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "f = parse('(x->y)+(y->z)<->x->z')\n", "f" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "draw(f)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "f = parse('x->--x+-(y.z)')\n", "f" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "draw(f)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Vous pouvez maintenant très facilement utiliser avec Python vos formules logiques préférées." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## 3. Disséquer les formules" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Juste pour voir ... Voici quelques illustrations de ce que nous pouvons faire avec notre représentation des formules." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 3.1 Éliminer les implications et les équivalences" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Voici une fonction qui prend en paramètre une formule $f$ et renvoie une formule $f'$ équivalente à $f$ qui ne contient ni le connecteur $\\rightarrow$ ni le connecteur $\\leftrightarrow$. Comment faire cela ? Facile, en utilisant les équivalences classiques. On sait que $f_1 \\rightarrow f_2\\equiv (- f_1 + f_2)$ et $f_1 \\leftrightarrow f_2\\equiv (- f_1 + f_2).(- f_2 + f_1)$. Une fonction récursive s'impose." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def et_ou(f):\n", " if f[0] == 'var': return f\n", " elif f[0] == 'not': return ('not', et_ou(left(f)))\n", " else:\n", " f1 = et_ou(left(f))\n", " f2 = et_ou(right(f))\n", " if f[0] == 'and': return ('and', f1, f2)\n", " elif f[0] == 'or': return ('or', f1, f2)\n", " elif f[0] == 'imp': return ('or', ('not', f1), f2)\n", " elif f[0] == 'eqv': return ('and',('or', ('not', f1), f2),('or', ('not', f2), f1))" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "to_string(et_ou(exemple))" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "draw(et_ou(exemple))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 3.2 La forme prénexe" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Une formule est dite sous forme __prénexe__ lorsque les seuls symboles de n'égation intervenant dans la formule le sont devant des variables. La fonction ci-dessous prend une formule $f$ ne contenant ni \"implique\" ni \"équivaut\" et renvoie une formule équivalente à $f$ sous forme prénexe. Comment faire ? Eh bien les lois de Morgan $- (f_1 . f2)\\equiv - f_1 + - f_2$ et $- (f_1 + f2)\\equiv - f_1 . - f_2$ ainsi que la loi $--f\\equiv f$ sont nos amies ..." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "__Remarque__ : à la fin de ce notebook nous serons en mesure de ___démontrer___ en Python que les lois de Morgan (et toutes les formules que nous voulons) sont des tautologies." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def prenexe(f):\n", " if f[0] == 'var': return f\n", " elif f[0] == 'not':\n", " f1 = left(f)\n", " if f1[0] == 'var': return ('not', f1)\n", " elif f1[0] == 'not': return prenexe(left(f1))\n", " else:\n", " g1 = prenexe(('not', left(f1)))\n", " g2 = prenexe(('not', right(f1)))\n", " if f1[0] == 'and': return ('or', g1, g2)\n", " else: return ('and', g1, g2)\n", " else:\n", " f1 = prenexe(left(f))\n", " f2 = prenexe(right(f))\n", " if f[0] == 'and': return ('and', f1, f2)\n", " else: return ('or', f1, f2)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "to_string(prenexe(et_ou(exemple)))" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "draw(prenexe(et_ou(exemple)))" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "f = prenexe(et_ou(formule_aleatoire(8, 4)))\n", "to_string(f)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "draw(f)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 3.3 Substitution" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Soit $f$ une formule. Soit $x$ une variable. Soit $g$ une autre formule. Comment substituer $g$ à $x$ dans la formule $f$ ? Du code Python sera aussi clair qu'une longue explication." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def substituer(f, x, g):\n", " if f[0] == 'var':\n", " if f[1] == 'x': return g\n", " else: return f\n", " elif f[0] == 'not':\n", " return ('not', substituer(left(f), x, g))\n", " else:\n", " return (f[0], substituer(left(f), x, g), substituer(right(f), x, g))" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "f = parse('x->(y->x)')\n", "g = parse('a.b')\n", "to_string(substituer(f, 'x', g))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "On pourrait continuer longtemps. Ce n'est évidemment pas la fin de l'histoire mais j'espère vous avoir montré que plus rien ne nous résiste concernant la __syntaxe__ des formules. Nous allons passer maintenant à autre chose, la __sémantique__. Une formule est-elle vraie ou fausse ? " ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## 4. Sémantique: évaluation des formules" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Disons-le tout de suite : une formule n'est NI vraie NI fausse. Faisons un parallèle avec les formules de l'algèbre. Considérons $A=x+y.z$, où $x,y,z\\in\\mathbb R$. Que vaut $A$ ? C'est évidemment une question idiote. La réponse est : \"ça dépend !\". Oui, et de quoi ? Eh bien de $x, y$ et $z$.\n", "\n", "Maintenant si je vous dit que $x=2$, $y=3$ et $z=4$, alors vous me direz que $A$ vaut $15$. Et vous aurez tort, ça vaut 14 :-). Bref, une formule ne vaut quelque chose que lorsque ses variables valent quelque chose. Pour évaluer une formule nous devons être dans un certain __environnement__. Revenons aux formules logiques et soyons précis :\n", "\n", "__Définition__ : un environnement est une fonction $\\gamma : \\mathcal V\\to\\{0, 1\\}$.\n", "\n", "Le choix de $\\{0, 1\\}$ est arbitraire. Moralement, 0 signifie \"faux\" et 1 signifie \"vrai\", mais toute autre __interprétation__ est possible. Le mot est lâché. Sens ? Signification ? Interprétation ? Nous ne pouvons plus nous contenter d'écrire des formules, nous voulons en plus leur donner un sens. C'est le but de la __sémantique__." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Je n'irai pas plus avant dans la théorie. Pour faire court, on peut montrer que pour tout environnement $\\gamma$, pour toute formule $f$, il existe une valeur dans $\\{0, 1\\}$ dépendant de $f$ et $\\gamma$, pour laquelle les connecteurs apparaissant dans $f$ ont le comportement que l'on souhaite. On note cette valeur ${\\text eval}(f, \\gamma)$. Par exemple, il est souhaitable que ${\\text eval}(f_1.f_2, \\gamma)$ soit égal à ${\\text eval}(f_1,\\gamma)\\times{\\text eval}(f_2,\\gamma)$ pour repecter ce que l'on pense du \"et\" (faux et faux = faux, faux et vrai = faux, etc.). \n", "\n", "\n", "On montre également que cette valeur ne dépend que de la valeur de $\\gamma$ en les variables qui apparaissent dans $f$." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 4.1 Codes de longueur n" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Étape 1 : fabriquer tous les $n$-uplets de 0 et de 1, pour un $n$ donné." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def codes(n):\n", " if n == 0: return [[]]\n", " else:\n", " cs = codes(n - 1)\n", " return [[0] + c for c in cs] + [[1] + c for c in cs]" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "codes(4)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 4.2 Environnements" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Étape 2 : fabriquer tous les environnements possibles pour une liste donnée de variables." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def environnement(vs, c):\n", " gamma = {}\n", " for i in range(len(vs)):\n", " gamma[vs[i]] = c[i]\n", " return gamma" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "environnement(['x', 'y', 'z'], [0, 1, 0])" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def environnements(vs):\n", " n = len(vs)\n", " cs = codes(n)\n", " return [environnement(vs, c) for c in cs]" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "environnements(list(variables(exemple)))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 3.3 Évaluer une formule dans un environnement" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Nous y voilà. Voici la fonction d'évaluation. La comprendre, c'est la lire. Les formules pour l'implication et l'équivalence peuvent paraître absconses, vérifiez-les." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def eval(f, gamma):\n", " if f[0] == 'var': return gamma[f[1]]\n", " elif f[0] == 'not':\n", " b = eval(f[1], gamma)\n", " return 1 - b\n", " else:\n", " b1 = eval(f[1], gamma)\n", " b2 = eval(f[2], gamma)\n", " if f[0] == 'and': return b1 * b2\n", " elif f[0] == 'or': return b1 + b2 - b1 * b2\n", " elif f[0] == 'imp': return 1 - b1 + b1 * b2\n", " elif f[0] == 'eqv': return 1 - b1 - b2 + 2 * b1 * b2 " ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Voici l'évaluation de notre exemple fétiche sur tous les environnements possibles." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "env = environnements(list(variables(exemple)))\n", "[(gamma, eval(exemple, gamma)) for gamma in env]" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 3.4 Table de vérité" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "La fonction ci-dessous ne fait qu'afficher sous forme plus \"lisible\" le résultat que nous avons obtenu ci-dessus. On range tout cela dans ce que l'on appelle \"la\" table de vérité de la formule." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def afficher_table(f):\n", " vars = list(variables(f))\n", " vars.sort()\n", " env = environnements(vars)\n", " for x in env[0]: sys.stdout.write('%3s' % x) # étiquettes de la table de vérité\n", " sys.stdout.write('%3s\\n'% 'f') # la dernière étiquette\n", " for gamma in env:\n", " b = eval(f, gamma)\n", " for x in gamma: sys.stdout.write('%3d' % gamma[x])\n", " sys.stdout.write('%3d\\n' % b)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "afficher_table(exemple)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "afficher_table(formule_aleatoire(10, 4))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 3.5 Satisfiabilité, tautologies, contradictions" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Ce notebook est déjà bien long. Je me contenterai de finir en disant deux mots sur la satisfiabilité." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "__Définition__ : soient $f$ une formule et $\\gamma$ un environnement. On dit que $\\gamma$ satisfait $f$ (ou que $f$ est satisfaite par $\\gamma$) lorsque ${\\text eval}(f,\\gamma)=1$." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "__Définition__ : Une formule est satisfiable lorsqu'il existe un environnement qui la satisfait." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "__Définition__ : Une formule est une contradiction lorsqu'aucun environnement ne la satisfait." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "__Définition__ : Une formule est une tautologie lorsque tous les environnements la satisfont.\n", "\n", "Une tautologie est donc une formule très satisfaite :-)." ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def satisfiable(f):\n", " vars = list(variables(f))\n", " env = environnements(vars)\n", " for gamma in env:\n", " if eval(f, gamma) == 1: return (True, gamma)\n", " return (False, None)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "f = parse(('x->(y->x)'))\n", "satisfiable(f)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def contradiction(f):\n", " return not satisfiable(f)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "def tautologie(f):\n", " vars = list(variables(f))\n", " env = environnements(vars)\n", " for gamma in env:\n", " if eval(f, gamma) == 0: return False\n", " return True" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "tautologie(f)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "f = formule_aleatoire(10, 5)\n", "tautologie(f)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Et notre exemple adoré ? Est-ce une tautologie ? Est-il au moins satisfiable ?" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "satisfiable(exemple)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "tautologie(exemple)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### 3.5 Tautologies incontournables" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Une des tâches première du logicien en particulier et du mathématicien en général est d'écrire des tautologies. Parmi les tautologies fondamentales de la logique nous trouvons :" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "#### 3.5.1 La double négation" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "double_negation = parse('--x<->x')\n", "tautologie(double_negation)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "#### 3.5.2 La non-contradiction" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "non_contradiction = parse('-(x.-x)')\n", "tautologie(non_contradiction)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "#### 3.5.3 Le tiers exclu" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "tiers_exclu = parse('x+-x')\n", "tautologie(tiers_exclu)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "#### 3.5.4 Les lois de Morgan" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "morgan1 = parse('-(a.b)<->-a+-b')\n", "tautologie(morgan1)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "morgan2 = parse('-(a+b)<->-a.-b')\n", "tautologie(morgan2)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "#### 3.5.5 Le modus Ponens" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "modus_ponens = parse('x.(x->y)->y')\n", "tautologie(modus_ponens)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "#### 3.5.6 La transitivité de l'implication" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "trans_impl = parse('(x->y).(y->z)->(x->z)')\n", "tautologie(trans_impl)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "#### 3.5.7 Le principe de contraposition" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [ "contra = parse('(a->b)<->(-b->-a)')\n", "tautologie(contra)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Et bien d'autres ... démontrez autant que vous voudrez. Quoique \"démontrer\" veuille maintenant dire \"appuyer sur la touche Entrée\" :-)" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [] } ], "metadata": { "kernelspec": { "display_name": "Python 3", "language": "python", "name": "python3" }, "language_info": { "codemirror_mode": { "name": "ipython", "version": 3 }, "file_extension": ".py", "mimetype": "text/x-python", "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", "version": "3.6.4" } }, "nbformat": 4, "nbformat_minor": 2 }