{ "cells": [ { "cell_type": "markdown", "metadata": { "toc": "true" }, "source": [ "# Table of Contents\n", "

1  Texte d'oral de modélisation - Agrégation Option Informatique
1.1  Préparation à l'agrégation - ENS de Rennes, 2016-17
1.2  À propos de ce document
1.3  Question de programmation
1.3.1  Théorème 3
1.3.2  Choix d'implémentation
1.4  Réponse à l'exercice requis
1.4.1  Symboles et arités
1.4.2  Vérification de l'écriture préfixe
1.4.3  Vérification et localisation de la première erreur
1.4.4  Exemples
1.5  Bonus : évaluation d'un terme
1.5.1  Manipulation basique sur une pile
1.5.2  Interprétation des symboles
1.5.3  Évaluation d'un terme
1.5.4  Un exemple d'évaluation d'un terme du calcul propositionnel
1.5.5  Avec une autre interprétation
1.6  Bonus : un autre exemple
1.6.1  Symboles et arités
1.6.2  Formules de l'arithmétique de Presburger
1.6.3  Quelques exemples de formules de Presburger
1.6.4  Vérification de l'écriture préfixe pour des formules de Presburger
1.7  Conclusion
" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "# Texte d'oral de modélisation - Agrégation Option Informatique\n", "## Préparation à l'agrégation - ENS de Rennes, 2016-17\n", "- *Date* : 09 mai 2017\n", "- *Auteur* : [Lilian Besson](https://GitHub.com/Naereen/notebooks/)\n", "- *Texte*: Annale 2012, [\"Mots bien formés\"](http://agreg.org/Textes/public2012-D6.pdf)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## À propos de ce document\n", "- Ceci est une *proposition* de correction, partielle et probablement non-optimale, pour la partie implémentation d'un [texte d'annale de l'agrégation de mathématiques, option informatique](http://Agreg.org/Textes/).\n", "- Ce document est un [notebook Jupyter](https://www.Jupyter.org/), et [est open-source sous Licence MIT sur GitHub](https://github.com/Naereen/notebooks/tree/master/agreg/), comme les autres solutions de textes de modélisation que [j](https://GitHub.com/Naereen)'ai écrite cette année.\n", "- L'implémentation sera faite en OCaml, version 4+ :" ] }, { "cell_type": "code", "execution_count": 1, "metadata": { "scrolled": true }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "The OCaml toplevel, version 4.04.2\n" ] }, { "data": { "text/plain": [ "- : int = 0\n" ] }, "execution_count": 1, "metadata": {}, "output_type": "execute_result" } ], "source": [ "Sys.command \"ocaml -version\";;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "----\n", "## Question de programmation\n", "La question de programmation pour ce texte était donnée à la fin, en page 7 :\n", "\n", "> « Programmer la reconnaissance des mots bien formés en écriture préfixe sur la signature de\n", "l’exemple du texte à l’aide du critère fourni par le théorème 3 page 5. Il est conseillé de représenter le mot à valider sous forme d’un tableau ou d’une liste de caractères. »\n", "\n", "Mathématiquement, l'énoncé à implémenter sous forme d'un critère est le suivant :\n", "\n", "### Théorème 3\n", "> Pour que la suite de symboles $s_1,\\dots,s_n \\in \\Omega$ soit l'écriture *préfixe* d'un terme, il faut et il suffit que les $h_p := \\sum_{i=1}^{p} (1 - \\alpha(s_i))$ vérifient :\n", "> $$ h_1,\\dots,h_{n-1} \\leq 0 \\; \\text{et} \\; h_n = 1. $$\n", "\n", "\n", "### Choix d'implémentation\n", "- Ce critère numérique va être très simple à implémenter.\n", "\n", "- Le choix des structures de données à utiliser n'est cependant pas évident.\n", " + Le sujet suggérait d'utiliser un tableau ou une liste de caractères pour représenter la \"suite de symboles\" $s_1,\\dots,s_n \\in \\Omega$\n", " + On va définir un type formel pour l'alphabet $\\Omega$, avec l'exemple du texte, $\\Omega = \\{V, F, \\mathrm{Non}, \\mathrm{Ou}, \\mathrm{Et}, \\mathrm{ITE}\\}$.\n", " + On doit ensuite représenter l'arité, sous forme de tableau, table d'association ou de hashage, ou une fonction, qui permette d'associer un entier $\\alpha(s)$ à chaque symbole $s$. Par simplicité, on choisit d'utiliser une fonction : $\\alpha : \\Omega \\to \\mathbb{N}, s \\mapsto \\alpha(s)$.\n", " + Enfin, la fonction demandée sera récursive, et très rapide à écrire." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "----\n", "## Réponse à l'exercice requis" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Symboles et arités\n", "On définit :\n", "- les symboles du calcul propositionnel par un type énumération (abstrait) :\n", " $$ \\Omega = \\{V, F, \\mathrm{Non}, \\mathrm{Ou}, \\mathrm{Et}, \\mathrm{ITE}\\} $$\n", " $\\mathrm{ITE}$ correspond au \"If then else\" ternaire (`a ? b : c` en C, `if a then b else c` en OCaml, ou `b if a else c` en Python).\n", "- Et les formules du calcul propositionnel comme une *liste* de symboles." ] }, { "cell_type": "code", "execution_count": 2, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "type symbole_calcul_prop = F | V | Ou | Et | Non | ITE\n" ] }, "execution_count": 2, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "type formule_calcul_prop = symbole_calcul_prop list\n" ] }, "execution_count": 2, "metadata": {}, "output_type": "execute_result" } ], "source": [ "type symbole_calcul_prop = F | V | Ou | Et | Non | ITE ;;\n", "\n", "type formule_calcul_prop = symbole_calcul_prop list ;;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Quelques exemples de formules du calcul propositionnel, écrites sous forme préfixes, bien formées ou non :\n", "\n", "- \"$\\mathrm{Ou} \\; \\mathrm{Non} \\; \\mathrm{Ou} \\; F \\; V \\; \\mathrm{Ou} \\; \\mathrm{Non} \\; V \\; F\"$ $\\equiv (\\neg(F \\vee V)) \\vee ((\\neg V) \\vee F)$ est bien formé,\n", "- \"$\\mathrm{Ou} \\; \\mathrm{Non} \\; F \\; \\mathrm{Non}$\" est mal formé,\n", "- \"$\\mathrm{ITE} \\; V \\; F \\; V$\" un exemple de \"If then else\" bien formé,\n", "- \"$\\;$\" la formule vide." ] }, { "cell_type": "code", "execution_count": 3, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val ex_correct : symbole_calcul_prop list =\n", " [Ou; Non; Ou; F; V; Ou; Non; V; F]\n" ] }, "execution_count": 3, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val ex_incorrect : symbole_calcul_prop list = [Ou; Non; F; Non]\n" ] }, "execution_count": 3, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val ex_ite : symbole_calcul_prop list = [ITE; V; F; V]\n" ] }, "execution_count": 3, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val ex_vide : 'a list = []\n" ] }, "execution_count": 3, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let ex_correct = [Ou; Non; Ou; F; V; Ou; Non; V; F];;\n", "let ex_incorrect = [Ou; Non; F; Non];;\n", "let ex_ite = [ITE; V; F; V];;\n", "let ex_vide = [];;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Cette fonction donne l'arité du symbole du calcul propositionnel pris en argument.\n", "\n", "- $V$ et $F$ ont arités $\\alpha = 0$,\n", "- $\\mathrm{Non}$ a arité $\\alpha = 1$,\n", "- $\\mathrm{Et}$ et $\\mathrm{Ou}$ ont arités $\\alpha = 2$,\n", "- $\\mathrm{ITE}$ a arité $\\alpha = 3$.\n", "\n", "Autrement dit, avec les notations du texte :\n", "$$ S = \\Omega = S_0 \\sqcup S_1 \\sqcup S_2 \\sqcup S_3 \\\\\n", "\\begin{cases}\n", " S_0 &= \\{ V, F \\}, \\\\\n", " S_1 &= \\{ \\mathrm{Non} \\}, \\\\\n", " S_2 &= \\{ \\mathrm{Et}, \\mathrm{Ou} \\}, \\\\\n", " S_3 &= \\{ \\mathrm{ITE} \\}.\n", "\\end{cases}\n", "$$\n", "\n", "> Notez qu'on peut supposer que l'appel à cette fonction d'arité se fait en $\\mathcal{O}(1)$ dans les calculs de complexité, puisqu'après compilation, cette fonction sera une simple lecture d'un tableau." ] }, { "cell_type": "code", "execution_count": 4, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val arite_calcul_prop : symbole_calcul_prop -> int = \n" ] }, "execution_count": 4, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let arite_calcul_prop (s : symbole_calcul_prop) : int =\n", " match s with\n", " | F -> 0\n", " | V -> 0\n", " | Non -> 1\n", " | Ou -> 2\n", " | Et -> 2\n", " | ITE -> 3\n", ";;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Vérification de l'écriture préfixe\n", "\n", "Cette fonction prend en argument une liste de symboles `l` et une fonction d'arité sur ces symboles et renvoie \"vrai\" (`true`) si `l` est l'écriture préfixe d'un terme et \"faux\" sinon (`false`).\n", "\n", "Notez que le \"et\" en Caml est paresseux, i.e., `x && y` n'évalue pas `y` si `x` est `false`.\n", "Donc cette fonction peut s'arrêter avant d'avoir parcouru tous les symboles, dès qu'elle trouve un symbole qui contredit le critère sur les hauteurs $h_p$.\n", "\n", "Et cela permet aussi d'obtenir une indication sur le premier symbole à contredire le critère, comme implémenté ensuite." ] }, { "cell_type": "code", "execution_count": 5, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val ecriture_prefixe_valide : 'a list -> ('a -> int) -> bool = \n" ] }, "execution_count": 5, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let ecriture_prefixe_valide (l : 'a list) (arite : 'a -> int) : bool =\n", " let rec aux (l : 'a list) (h : int) : bool =\n", " match l with\n", " | [] -> false\n", " | [t] -> ((h + 1 - (arite t)) = 1)\n", " | t :: q ->\n", " let h_suivant = (h + 1 - (arite t)) in\n", " (h_suivant <= 0) && (aux q h_suivant)\n", " in aux l 0\n", ";;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "On vérifie tout de suite sur les 4 exemples définis ci-dessus :" ] }, { "cell_type": "code", "execution_count": 6, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "- : bool = true\n" ] }, "execution_count": 6, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : bool = false\n" ] }, "execution_count": 6, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : bool = true\n" ] }, "execution_count": 6, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : bool = false\n" ] }, "execution_count": 6, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let _ = ecriture_prefixe_valide ex_correct arite_calcul_prop;; (* true *)\n", "let _ = ecriture_prefixe_valide ex_incorrect arite_calcul_prop;; (* false *)\n", "let _ = ecriture_prefixe_valide ex_ite arite_calcul_prop;; (* true *)\n", "let _ = ecriture_prefixe_valide ex_vide arite_calcul_prop;; (* false *)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Vérification et localisation de la première erreur\n", "Avec la remarque précédente, on peut écrire une fonction très similaire, mais qui donnera une indication sur la position (i.e., l'indice) du premier symbole qui fait que le mot n'est pas bien équilibré, si le mot n'est pas bien formé. Si le mot est bien formé, `None` est renvoyé." ] }, { "cell_type": "code", "execution_count": 7, "metadata": { "scrolled": true }, "outputs": [ { "data": { "text/plain": [ "val ecriture_prefixe_valide_info : 'a list -> ('a -> int) -> int option =\n", " \n" ] }, "execution_count": 7, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let ecriture_prefixe_valide_info (l : 'a list) (arite : 'a -> int) : int option =\n", " let rec aux (l : 'a list) (compteur : int) (h : int) : int option =\n", " match l with\n", " | [] -> Some compteur\n", " | [t] ->\n", " if (h + 1 - (arite t)) = 1 (* h = arite(t) *)\n", " then None\n", " else Some compteur\n", " | t :: q ->\n", " (* h est l'accumulateur qui contient la somme des 1 - arite(t) *)\n", " let h_suivant = (h + 1 - (arite t)) in\n", " if h_suivant > 0 then\n", " Some compteur\n", " else\n", " aux q (compteur + 1) h_suivant\n", " in\n", " aux l 0 0\n", ";;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "On vérifie tout de suite sur les 4 exemples définis ci-dessus :" ] }, { "cell_type": "code", "execution_count": 8, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "- : int option = None\n" ] }, "execution_count": 8, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : int option = Some 3\n" ] }, "execution_count": 8, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : int option = None\n" ] }, "execution_count": 8, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : int option = Some 0\n" ] }, "execution_count": 8, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let _ = ecriture_prefixe_valide_info ex_correct arite_calcul_prop;; (* None *)\n", "let _ = ecriture_prefixe_valide_info ex_incorrect arite_calcul_prop;; (* Some 3 *)\n", "let _ = ecriture_prefixe_valide_info ex_ite arite_calcul_prop;; (* None *)\n", "let _ = ecriture_prefixe_valide_info ex_vide arite_calcul_prop;; (* Some 0 *)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Cela permet de voir que sur la formule \"$\\mathrm{Ou} \\; \\mathrm{Non} \\; F \\; \\mathrm{Non}$\", le premier symbole à poser problème est le dernier symbole.\n", "Et effectivement, le critère est vérifié jusqu'au dernier symbole $\\mathrm{Non}$." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Exemples\n", "Avec les mêmes exemples :" ] }, { "cell_type": "code", "execution_count": 9, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "- : bool = true\n" ] }, "execution_count": 9, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : bool = false\n" ] }, "execution_count": 9, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : bool = true\n" ] }, "execution_count": 9, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : bool = false\n" ] }, "execution_count": 9, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let _ = ecriture_prefixe_valide ex_correct arite_calcul_prop;; (* true *)\n", "let _ = ecriture_prefixe_valide ex_incorrect arite_calcul_prop;; (* false *)\n", "let _ = ecriture_prefixe_valide ex_ite arite_calcul_prop;; (* true *)\n", "let _ = ecriture_prefixe_valide ex_vide arite_calcul_prop;; (* false *)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "On peut aussi transformer un peu la deuxième formule pour la rendre valide." ] }, { "cell_type": "code", "execution_count": 10, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val ex_correct_2 : symbole_calcul_prop list = [Ou; Non; F; V]\n" ] }, "execution_count": 10, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : bool = true\n" ] }, "execution_count": 10, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let ex_correct_2 = [Ou; Non; F; V];;\n", "let _ = ecriture_prefixe_valide ex_correct_2 arite_calcul_prop;; (* true *)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Bonus : évaluation d'un terme\n", "\n", "L'objectif est de construire la fonction d'évaluation d'un terme en écriture postfixe présentée dans le texte (Algorithme 2, page 4) :\n", "\n", "![images/algorithme_evaluation_terme.png](images/algorithme_evaluation_terme.png)\n", "\n", "- La pile utilisée dans l'algorithme sera implémentée par une simple liste.\n", "\n", "- Ce que le texte appelle \"valeur\" et \"omegabarre\" sont regroupés dans une liste de couples tels que le premier élément du couple est un symbole `s` et le deuxième la fonction `f_s` permettant d'interpréter ce symbole ; on considère que les constante sont des fonctions d'arité 0. Cette fonction `f_s` prend en arguments une liste d'éléments du domaine et renvoie un élément du domaine.\n" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Manipulation basique sur une pile\n", "\n", "On a besoin de savoir dépiler plus d'une valeur, pour récupérer les $k$ valeurs successives à donner à l'interprétation d'un symbole d'arité $k \\geq 1$.\n", "\n", "Cette fonction renvoie un couple de listes :\n", "- la liste des `k` éléments en sommet de la pile `p` de sorte que le sommet de la pile `p` se trouve en dernière position dans cette liste,\n", "- et la pile `p` une fois qu'on a dépilé ses `k` éléments du sommet." ] }, { "cell_type": "code", "execution_count": 11, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val depile : int -> 'a list -> 'a list * 'a list = \n" ] }, "execution_count": 11, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let depile (k : int) (p : 'a list) : ('a list * 'a list) =\n", " let rec aux (k : int) (p : 'a list) (sommet_pile : 'a list) : ('a list * 'a list) =\n", " match k with\n", " | 0 -> (sommet_pile, p)\n", " | _ when p = [] ->\n", " failwith \"Liste vide\"\n", " | i ->\n", " let sommet_modif = (List.hd p) :: sommet_pile in\n", " let p_modif = List.tl p in\n", " aux (i - 1) p_modif sommet_modif\n", " in\n", " aux k p []\n", ";;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Il est absolument crucial de faire *au moins un test* à ce moment là :" ] }, { "cell_type": "code", "execution_count": 12, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "- : int list * int list = ([], [0; 1; 2; 3; 4; 5; 6; 7])\n" ] }, "execution_count": 12, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : int list * int list = ([0], [1; 2; 3; 4; 5; 6; 7])\n" ] }, "execution_count": 12, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : int list * int list = ([2; 1; 0], [3; 4; 5; 6; 7])\n" ] }, "execution_count": 12, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : int list * int list = ([7; 6; 5; 4; 3; 2; 1; 0], [])\n" ] }, "execution_count": 12, "metadata": {}, "output_type": "execute_result" } ], "source": [ "depile 0 [0; 1; 2; 3; 4; 5; 6; 7];;\n", "depile 1 [0; 1; 2; 3; 4; 5; 6; 7];;\n", "depile 3 [0; 1; 2; 3; 4; 5; 6; 7];;\n", "depile 8 [0; 1; 2; 3; 4; 5; 6; 7];;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Ça semble bien fonctionner.\n", "Notez que la première liste a été retournée (\"renversée\"), puisque les valeurs ont été empilées dans le sens inverse lors de leurs lectures.\n", "\n", "On peut aussi proposer une implémentation alternative, moins élégante mais plus rapide à écrire, avec des tableaux, et deux appels à `Array.sub` pour découper le tableau, et `Array.of_list` et `Array.to_list` pour passer d'une liste à un tableau puis de deux tableaux à deux listes." ] }, { "cell_type": "code", "execution_count": 13, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val depile_2 : int -> 'a list -> 'a list * 'a list = \n" ] }, "execution_count": 13, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let depile_2 (k : int) (p : 'a list) : ('a list * 'a list) =\n", " let pa = Array.of_list p in\n", " let debut = Array.sub pa 0 k in\n", " let fin = Array.sub pa k ((Array.length pa) - k) in\n", " (List.rev (Array.to_list debut)), (Array.to_list fin)\n", ";;" ] }, { "cell_type": "code", "execution_count": 14, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "- : int list * int list = ([], [0; 1; 2; 3; 4; 5; 6; 7])\n" ] }, "execution_count": 14, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : int list * int list = ([0], [1; 2; 3; 4; 5; 6; 7])\n" ] }, "execution_count": 14, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : int list * int list = ([2; 1; 0], [3; 4; 5; 6; 7])\n" ] }, "execution_count": 14, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : int list * int list = ([7; 6; 5; 4; 3; 2; 1; 0], [])\n" ] }, "execution_count": 14, "metadata": {}, "output_type": "execute_result" } ], "source": [ "depile_2 0 [0; 1; 2; 3; 4; 5; 6; 7];;\n", "depile_2 1 [0; 1; 2; 3; 4; 5; 6; 7];;\n", "depile_2 3 [0; 1; 2; 3; 4; 5; 6; 7];;\n", "depile_2 8 [0; 1; 2; 3; 4; 5; 6; 7];;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Interprétation des symboles\n", "\n", "Cette fonction prend en entrée une liste `interpretation` de couples (symbole, fonction interprétant ce symbole), un symbole `t` et une liste d'arguments `arg` et renvoie `f_t(arg)`, où `f_t` est la fonction associée au sympole `t` via `interpretation`.\n", "\n", "Avec les notations mathématiques du texte, le symbole `t` est $\\omega$ et `f_t` est $\\overline{\\omega}$ (\"omegabarre\" dans l'algorithme)." ] }, { "cell_type": "code", "execution_count": 15, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val interprete : ('a * ('d list -> 'd)) list -> 'a -> 'd list -> 'd = \n" ] }, "execution_count": 15, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let interprete (interpretation : ('a * ('d list -> 'd)) list) (t : 'a) (arg : 'd list) : 'd =\n", " (List.assoc t interpretation) arg;;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "L'interprétation choisie consiste à évaluer la valeur de vérité d'une formule du calcul propositionnel, avec l'interprétation classique.\n", "\n", "Notez que pour faciliter le typage, ces fonctions recoivent la pile, i.e., une *liste* d'arguments (de taille arbitraire) et s'occupent elles-mêmes de récupérer le sommet de pile et les valeurs suivantes.\n", "\n", "> Les fonctions échouent si la pile donnée n'est pas assez profonde, bien évidemment." ] }, { "cell_type": "code", "execution_count": 16, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val interp_V : 'a -> bool = \n" ] }, "execution_count": 16, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val interp_F : 'a -> bool = \n" ] }, "execution_count": 16, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val interp_Non : bool list -> bool = \n" ] }, "execution_count": 16, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val interp_Ou : bool list -> bool = \n" ] }, "execution_count": 16, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val interp_Et : bool list -> bool = \n" ] }, "execution_count": 16, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val interp_ITE : bool list -> bool = \n" ] }, "execution_count": 16, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let interp_V _ = true;;\n", "let interp_F _ = false;;\n", "let interp_Non l = not (List.hd l);;\n", "let interp_Ou l = (List.hd l) || (List.hd (List.tl l));;\n", "let interp_Et l = (List.hd l) && (List.hd (List.tl l));;\n", "let interp_ITE l = if (List.hd l) then (List.hd (List.tl l)) else (List.hd (List.tl (List.tl l)));;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Ensuite, on crée cette liste d'association, qui permet d'associer à un symbole $\\omega$ sa fonction $\\overline{\\omega}$ :" ] }, { "cell_type": "code", "execution_count": 17, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val interp_calcul_prop : (symbole_calcul_prop * (bool list -> bool)) list =\n", " [(V, ); (F, ); (Non, ); (Ou, ); (Et, );\n", " (ITE, )]\n" ] }, "execution_count": 17, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let interp_calcul_prop = [\n", " (V, interp_V); (F, interp_F); (* Arité 0 *)\n", " (Non, interp_Non); (* Arité 1 *)\n", " (Ou, interp_Ou); (Et, interp_Et); (* Arité 2 *)\n", " (ITE, interp_ITE) (* Arité 3 *)\n", "];;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Évaluation d'un terme\n", "\n", "Cette fonction prend une liste `l`, de symboles que l'on suppose correspondre à l'écriture postfixe *correcte* d'un terme, une fonction `arite : symbole -> entier` et une liste `interpretation` d'interprétation des symboles.\n", "\n", "Elle renvoie le résultat de l'évaluation du terme `l` pour l'interpretation `interpretation`.\n", "\n", "L'algorithme est annoncé correct par le théorème 2, non prouvé dans le texte (ça peut être une idée de développement à faire au tableau)." ] }, { "cell_type": "code", "execution_count": 18, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val evalue : 'a list -> ('a -> int) -> ('a * ('d list -> 'd)) list -> 'd =\n", " \n" ] }, "execution_count": 18, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let evalue (l : 'a list) (arite : 'a -> int) (interpretation : ('a * ('d list -> 'd)) list) : 'd =\n", " let rec aux (l : 'a list) (p : 'd list) : 'd =\n", " match l with\n", " | [] -> List.hd p\n", " | t :: q ->\n", " let k = arite t in\n", " let (arguments, p_temp) = depile k p in\n", " let valeur = interprete interpretation t arguments in\n", " let p_fin = valeur :: p_temp\n", " in (aux q p_fin)\n", " in\n", " aux l [];;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Si la lecture de l'arité d'un symbole `t`, `k = arite t`, est en $\\mathcal{O}(1)$, alors l'algorithme `evalue` a une complexité en $\\mathcal{O}(n)$ où $n$ est le nombre de symbole du terme donné en entrée.\n", "\n", "En d'autres termes, l'évaluation d'un terme postfixe par la méthode naïve, utilisée pour la [notation polonaise inversée](https://en.wikipedia.org/wiki/Polish_notation), est *linéaire* dans la taille du terme. Chouette !" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Un exemple d'évaluation d'un terme du calcul propositionnel" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "On considère le terme \"$\\mathrm{Ou} \\; \\mathrm{Non} \\; V \\; \\mathrm{Ou} \\; V \\; F$\" $= \\vee \\neg V \\vee V F \\equiv (\\neg V) \\vee (V \\vee F)$ suivant :\n", "\n", "![images/exemple_terme.png](images/exemple_terme.png)" ] }, { "cell_type": "code", "execution_count": 19, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val ex1 : symbole_calcul_prop list = [F; V; Ou; V; Non; Ou]\n" ] }, "execution_count": 19, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : bool = true\n" ] }, "execution_count": 19, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let ex1 = List.rev [ Ou; Non; V; Ou; V; F ];; (* écriture préfixe *)\n", "let _ = evalue ex1 arite_calcul_prop interp_calcul_prop;;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "On vient de passer de l'écriture préfixe à postfixe, simplement en inversant l'ordre des termes (`List.rev`).\n", "\n", "> Attention, cela ne fonctionne que si tous les symboles sont symmétriques !" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Avec un autre exemple, directement écrit en postfixe, correspondant au terme suivant, qui s'interprête à \"faux\" (`F = false`) :\n", "\n", "$$ (F \\vee \\neg V) \\vee (\\neg (V \\vee F)) \\;\\; \\;\\; \\underset{\\text{Interpretation}}{\\longrightarrow} \\;\\; \\;\\; F $$" ] }, { "cell_type": "code", "execution_count": 20, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val ex2 : symbole_calcul_prop list = [F; V; Ou; Non; V; Non; F; Ou; Ou]\n" ] }, "execution_count": 20, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : bool = false\n" ] }, "execution_count": 20, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let ex2 = [F; V; Ou; Non; V; Non; F; Ou; Ou];;\n", "let _ = evalue ex2 arite_calcul_prop interp_calcul_prop;;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Avec une autre interprétation\n", "\n", "On considère un second exemple : l'interprétation choisie consiste à construire **l'arbre syntaxique** d'une formule du calcul propositionnel." ] }, { "cell_type": "code", "execution_count": 21, "metadata": { "scrolled": false }, "outputs": [ { "data": { "text/plain": [ "type arbre =\n", " FeuilleV\n", " | FeuilleF\n", " | NNon of arbre\n", " | NEt of arbre * arbre\n", " | NOu of arbre * arbre\n", " | NITE of arbre * arbre * arbre\n" ] }, "execution_count": 21, "metadata": {}, "output_type": "execute_result" } ], "source": [ "type arbre =\n", " | FeuilleV | FeuilleF (* Arité 0 *)\n", " | NNon of arbre (* Arité 1 *)\n", " | NEt of arbre * arbre | NOu of arbre * arbre (* Arité 2 *)\n", " | NITE of arbre * arbre * arbre (* Arité 3 *)\n", ";;" ] }, { "cell_type": "code", "execution_count": 22, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val interp_V_a : 'a -> arbre = \n" ] }, "execution_count": 22, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val interp_F_a : 'a -> arbre = \n" ] }, "execution_count": 22, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val interp_Non_a : arbre list -> arbre = \n" ] }, "execution_count": 22, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val interp_Ou_a : arbre list -> arbre = \n" ] }, "execution_count": 22, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val interp_Et_a : arbre list -> arbre = \n" ] }, "execution_count": 22, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val interp_ITE_a : arbre list -> arbre = \n" ] }, "execution_count": 22, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let interp_V_a _ = FeuilleV;;\n", "let interp_F_a _ = FeuilleF;;\n", "let interp_Non_a l = NNon (List.hd l);;\n", "let interp_Ou_a l = NOu ( (List.hd l), (List.hd (List.tl l) ) );;\n", "let interp_Et_a l = NEt ( (List.hd l), (List.hd (List.tl l) ) );;\n", "let interp_ITE_a l = NITE ( (List.hd l), (List.hd (List.tl l) ), (List.hd (List.tl (List.tl l) ) ) );;" ] }, { "cell_type": "code", "execution_count": 23, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val interp_calcul_prop_a : (symbole_calcul_prop * (arbre list -> arbre)) list =\n", " [(V, ); (F, ); (Non, ); (Ou, ); (Et, );\n", " (ITE, )]\n" ] }, "execution_count": 23, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let interp_calcul_prop_a = [\n", " (V, interp_V_a); (F, interp_F_a); (* Arité 0 *)\n", " (Non, interp_Non_a); (* Arité 1 *)\n", " (Ou, interp_Ou_a); (Et, interp_Et_a); (* Arité 2 *)\n", " (ITE, interp_ITE_a); (* Arité 3 *)\n", "];;" ] }, { "cell_type": "code", "execution_count": 24, "metadata": { "scrolled": true }, "outputs": [ { "data": { "text/plain": [ "- : symbole_calcul_prop list = [F; V; Ou; Non; V; Non; F; Ou; Ou]\n" ] }, "execution_count": 24, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : arbre =\n", "NOu (NNon (NOu (FeuilleF, FeuilleV)), NOu (NNon FeuilleV, FeuilleF))\n" ] }, "execution_count": 24, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let _ = ex2;;\n", "let _ = evalue ex2 arite_calcul_prop interp_calcul_prop_a;;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "> Un bonus rapide va être de jouer avec l'API du notebook Jupyter, [accessible depuis OCaml via le kernel OCaml-Jupyter](https://github.com/akabe/ocaml-jupyter/), pour afficher joliment le terme en $\\LaTeX{}$." ] }, { "cell_type": "code", "execution_count": 25, "metadata": { "scrolled": true }, "outputs": [ { "name": "stderr", "output_type": "stream", "text": [ "/home/lilian/.opam/4.04.2/lib/ocaml/threads: added to search path\n", "/home/lilian/.opam/4.04.2/lib/ocaml/unix.cma: loaded\n", "/home/lilian/.opam/4.04.2/lib/ocaml/threads/threads.cma: loaded\n" ] } ], "source": [ "#thread;;" ] }, { "cell_type": "code", "execution_count": 26, "metadata": {}, "outputs": [ { "name": "stderr", "output_type": "stream", "text": [ "/home/lilian/.opam/4.04.2/lib/easy-format: added to search path\n", "/home/lilian/.opam/4.04.2/lib/easy-format/easy_format.cma: loaded\n", "/home/lilian/.opam/4.04.2/lib/biniou: added to search path\n", "/home/lilian/.opam/4.04.2/lib/biniou/biniou.cma: loaded\n", "/home/lilian/.opam/4.04.2/lib/bytes: added to search path\n", "/home/lilian/.opam/4.04.2/lib/result: added to search path\n", "/home/lilian/.opam/4.04.2/lib/result/result.cma: loaded\n", "/home/lilian/.opam/4.04.2/lib/ppx_deriving: added to search path\n", "/home/lilian/.opam/4.04.2/lib/ppx_deriving/ppx_deriving_runtime.cma: loaded\n", "/home/lilian/.opam/4.04.2/lib/yojson: added to search path\n", "/home/lilian/.opam/4.04.2/lib/yojson/yojson.cma: loaded\n", "/home/lilian/.opam/4.04.2/lib/ppx_deriving_yojson: added to search path\n", "/home/lilian/.opam/4.04.2/lib/ppx_deriving_yojson/ppx_deriving_yojson_runtime.cma: loaded\n", "/home/lilian/.opam/4.04.2/lib/uuidm: added to search path\n", "/home/lilian/.opam/4.04.2/lib/uuidm/uuidm.cma: loaded\n", "/home/lilian/.opam/4.04.2/lib/jupyter: added to search path\n", "/home/lilian/.opam/4.04.2/lib/jupyter/jupyter.cma: loaded\n", "/home/lilian/.opam/4.04.2/lib/base64: added to search path\n", "/home/lilian/.opam/4.04.2/lib/base64/base64.cma: loaded\n", "/home/lilian/.opam/4.04.2/lib/ocaml/compiler-libs: added to search path\n", "/home/lilian/.opam/4.04.2/lib/ocaml/compiler-libs/ocamlcommon.cma: loaded\n", "/home/lilian/.opam/4.04.2/lib/jupyter/notebook: added to search path\n", "/home/lilian/.opam/4.04.2/lib/jupyter/notebook/jupyter_notebook.cma: loaded\n" ] } ], "source": [ "#require \"jupyter\";;\n", "#require \"jupyter.notebook\";;" ] }, { "cell_type": "code", "execution_count": 27, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val print_latex : string -> Jupyter_notebook.display_id = \n" ] }, "execution_count": 27, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let print_latex (s : string) = Jupyter_notebook.display \"text/html\" (\"$$\" ^ s ^ \"$$\");;" ] }, { "cell_type": "code", "execution_count": 28, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$$\\cos(x)$$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "- : Jupyter_notebook.display_id = \n" ] }, "execution_count": 28, "metadata": {}, "output_type": "execute_result" } ], "source": [ "print_latex \"\\\\cos(x)\";;" ] }, { "cell_type": "code", "execution_count": 29, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val symbole_to_latex : symbole_calcul_prop -> string = \n" ] }, "execution_count": 29, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let symbole_to_latex (sym : symbole_calcul_prop) =\n", " match sym with\n", " | ITE -> \"\\\\implies\"\n", " | Ou -> \"\\\\vee\"\n", " | Et -> \"\\\\wedge\"\n", " | Non -> \"\\\\neg\"\n", " | V -> \"V\" | F -> \"F\"\n", ";;" ] }, { "cell_type": "code", "execution_count": 30, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val formule_to_latex : symbole_calcul_prop list -> string = \n" ] }, "execution_count": 30, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let formule_to_latex (form : symbole_calcul_prop list) =\n", " String.concat \" \" (List.map symbole_to_latex form)\n", ";;" ] }, { "cell_type": "code", "execution_count": 31, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$$F V \\vee \\neg V \\neg F \\vee \\vee$$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "- : Jupyter_notebook.display_id = \n" ] }, "execution_count": 31, "metadata": {}, "output_type": "execute_result" } ], "source": [ "print_latex (formule_to_latex ex2);;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Sans prendre en compte la structure d'arbre, c'est très moche !" ] }, { "cell_type": "code", "execution_count": 32, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val arbre_to_latex : arbre -> string = \n" ] }, "execution_count": 32, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val formule_to_latex2 : symbole_calcul_prop list -> string = \n" ] }, "execution_count": 32, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let rec arbre_to_latex (arb : arbre) =\n", " match arb with\n", " | FeuilleV -> \"V\"\n", " | FeuilleF -> \"F\"\n", " | NNon(a) -> \"(\\\\neg \" ^ (arbre_to_latex a) ^ \")\"\n", " | NEt(a, b) -> \"(\" ^ (arbre_to_latex a) ^ \" \\\\wedge \" ^ (arbre_to_latex b) ^ \")\"\n", " | NOu(a, b) -> \"(\" ^ (arbre_to_latex a) ^ \" \\\\vee \" ^ (arbre_to_latex b) ^ \")\"\n", " | NITE(a, b, c) -> \"(\" ^ (arbre_to_latex a) ^ \" ? \" ^ (arbre_to_latex b) ^ \" : \" ^ (arbre_to_latex c) ^ \")\"\n", ";;\n", "\n", "let formule_to_latex2 (form : symbole_calcul_prop list) =\n", " let arb = evalue form arite_calcul_prop interp_calcul_prop_a in\n", " arbre_to_latex arb\n", ";;" ] }, { "cell_type": "code", "execution_count": 33, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "- : arbre =\n", "NOu (NNon (NOu (FeuilleF, FeuilleV)), NOu (NNon FeuilleV, FeuilleF))\n" ] }, "execution_count": 33, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let _ = evalue ex2 arite_calcul_prop interp_calcul_prop_a" ] }, { "cell_type": "code", "execution_count": 34, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$$((\\neg (F \\vee V)) \\vee ((\\neg V) \\vee F))$$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "- : Jupyter_notebook.display_id = \n" ] }, "execution_count": 34, "metadata": {}, "output_type": "execute_result" } ], "source": [ "print_latex (formule_to_latex2 ex2);;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "----\n", "## Bonus : un autre exemple\n", "\n", "On va considérer ici un second exemple, celui de l'[arithmétique de Presburger](http://minerve.bretagne.ens-cachan.fr/images/Presburger.pdf).\n", "\n", "En gros, c'est l'arithmétique avec :\n", "\n", "- des constantes (`Cst`), dans les entiers positifs $\\mathbb{N}$,\n", "- des variables (`Let`), sous formes de lettres ici (un seul `char`),\n", "- le test d'*égalité binaire* entre variables et constantes (`Eq`), de la forme $x = y$, où $x$ et $y$ sont des constantes ou des variables,\n", "- le test d'*égalité sur des sommes*, de la forme $x + y = z$, où $x$, $y$ et $z$ sont des constantes ou des variables,\n", "- le *ou binaire* sur des formules, de la forme $\\phi \\vee \\phi'$,\n", "- le *et binaire* sur des formules, de la forme $\\phi \\wedge \\phi'$,\n", "- le *non unaire* sur une formule, de la forme $\\neg \\phi$,\n", "- et le *test existenciel*, de la forme $\\exists x, \\phi$." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Symboles et arités" ] }, { "cell_type": "code", "execution_count": 35, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "type symbole_presburger = Cst | Let | Eq | PEq | O | A | N | Ex\n" ] }, "execution_count": 35, "metadata": {}, "output_type": "execute_result" } ], "source": [ "type symbole_presburger =\n", " Cst | Let | Eq | PEq | O | A | N | Ex\n", ";;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Avec ces symboles, on définit facilement leur arités." ] }, { "cell_type": "code", "execution_count": 36, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val arite_presburger : symbole_presburger -> int = \n" ] }, "execution_count": 36, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let arite_presburger (s : symbole_presburger) : int =\n", " match s with\n", " | Cst | Let -> 0\n", " | N -> 1\n", " | Eq | O | A | Ex -> 2\n", " | PEq -> 3\n", ";;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Formules de l'arithmétique de Presburger\n", "Les formules suivent cette grammaire :\n", "$$\\phi,\\phi' := (x=y)|(x+y=z)|\\phi\\vee\\phi'|\\phi\\wedge\\phi'|\\neg\\phi|\\exists x, \\phi$$\n", "\n", "Les symboles sont donc :\n", "\n", "- tous les entiers, et toutes les lettres d'arités 0,\n", "- $\\neg$, noté `Not`, d'arité 1,\n", "- $\\vee$, noté `Or`, $\\wedge$, noté `And`, $=$, noté `Equal`, et $\\exists$, noté `Exists`, d'arités 2,\n", "- \"$+=$\", noté `PlusEqual`.\n", "\n", "\n", "A noter que cet exemple nécessite des signatures non homogènes :\n", "\n", "- $=$ et $+ =$ exigent deux arguments qui soient des entiers ou des lettres,\n", "- $\\exists$ exige un premier argument qui soit une lettre, un second qui soit une formule,\n", "- $\\vee$ et $\\neg$ n'acceptent que des arguments qui soient des formules." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Plutôt que de travailler avec des listes de symboles, on définit une structure arborescente pour les formules de l'arithmétique de Presburger." ] }, { "cell_type": "code", "execution_count": 37, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "type entier = int\n" ] }, "execution_count": 37, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "type lettre = char\n" ] }, "execution_count": 37, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "type cst = I of entier | L of lettre\n" ] }, "execution_count": 37, "metadata": {}, "output_type": "execute_result" } ], "source": [ "type entier = int ;;\n", "type lettre = char ;;\n", "type cst = I of entier | L of lettre ;;" ] }, { "cell_type": "code", "execution_count": 38, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "type formule_presburger =\n", " Equal of cst * cst\n", " | PlusEqual of cst * cst * cst\n", " | Or of formule_presburger * formule_presburger\n", " | And of formule_presburger * formule_presburger\n", " | Not of formule_presburger\n", " | Exists of cst * formule_presburger\n" ] }, "execution_count": 38, "metadata": {}, "output_type": "execute_result" } ], "source": [ "type formule_presburger =\n", " | Equal of cst * cst\n", " | PlusEqual of cst * cst * cst\n", " | Or of formule_presburger * formule_presburger\n", " | And of formule_presburger * formule_presburger\n", " | Not of formule_presburger\n", " | Exists of cst * formule_presburger" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Ces formules peuvent facilement s'écrire comme un terme en notation préfixes :" ] }, { "cell_type": "code", "execution_count": 39, "metadata": {}, "outputs": [ { "name": "stderr", "output_type": "stream", "text": [ "File \"[39]\", line 2, characters 4-916:\n", "Warning 8: this pattern-matching is not exhaustive.\n", "Here is an example of a case that is not matched:\n", "Exists (I _, _)\n" ] }, { "data": { "text/plain": [ "val formule_vers_symboles : formule_presburger -> symbole_presburger list =\n", " \n" ] }, "execution_count": 39, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let rec formule_vers_symboles form =\n", " match form with\n", " | Equal(L(_), L(_)) -> [Eq; Let; Let]\n", " | Equal(I(_), L(_)) -> [Eq; Cst; Let]\n", " | Equal(L(_), I(_)) -> [Eq; Let; Cst]\n", " | Equal(I(_), I(_)) -> [Eq; Cst; Cst]\n", " | PlusEqual(L(_), L(_), L(_)) -> [PEq; Let; Let; Let]\n", " | PlusEqual(I(_), L(_), L(_)) -> [PEq; Cst; Let; Let]\n", " | PlusEqual(L(_), I(_), L(_)) -> [PEq; Let; Cst; Let]\n", " | PlusEqual(I(_), I(_), L(_)) -> [PEq; Cst; Cst; Let]\n", " | PlusEqual(L(_), L(_), I(_)) -> [PEq; Let; Let; Cst]\n", " | PlusEqual(I(_), L(_), I(_)) -> [PEq; Cst; Let; Cst]\n", " | PlusEqual(L(_), I(_), I(_)) -> [PEq; Let; Cst; Cst]\n", " | PlusEqual(I(_), I(_), I(_)) -> [PEq; Cst; Cst; Cst]\n", " | Or(a, b) -> O :: (formule_vers_symboles a) @ (formule_vers_symboles b)\n", " | And(a, b) -> A :: (formule_vers_symboles a) @ (formule_vers_symboles b)\n", " | Not(a) -> N :: (formule_vers_symboles a)\n", " | Exists(L(_), a) -> [Ex; Let] @ (formule_vers_symboles a)\n", ";;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "> *Cet avertissement est normal*, ici on impose que dans `Exists(u, a)`, `u` soit nécessairement de la forme `L(x)`, i.e., une variable et non une constante." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "On peut aussi afficher une formule, en la convertissant vers une chaîne de caractère :" ] }, { "cell_type": "code", "execution_count": 40, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val i : int -> string = \n" ] }, "execution_count": 40, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val c : char -> string = \n" ] }, "execution_count": 40, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let i = string_of_int ;;\n", "let c car = String.make 1 car ;;" ] }, { "cell_type": "code", "execution_count": 41, "metadata": {}, "outputs": [ { "name": "stderr", "output_type": "stream", "text": [ "File \"[41]\", line 2, characters 4-1040:\n", "Warning 8: this pattern-matching is not exhaustive.\n", "Here is an example of a case that is not matched:\n", "Exists (I _, _)\n" ] }, { "data": { "text/plain": [ "val formule_vers_chaine : formule_presburger -> string = \n" ] }, "execution_count": 41, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let rec formule_vers_chaine form =\n", " match form with\n", " | Equal(L(x), L(y)) -> (c x) ^ \"=\" ^ (c y)\n", " | Equal(I(x), L(y)) -> (i x) ^ \"=\" ^ (c y)\n", " | Equal(L(x), I(y)) -> (c x) ^ \"=\" ^ (i y)\n", " | Equal(I(x), I(y)) -> (i x) ^ \"=\" ^ (i y)\n", " | PlusEqual(L(x), L(y), L(z)) -> (c x) ^ \"+\" ^ (c y) ^ \"=\" ^ (c z)\n", " | PlusEqual(I(x), L(y), L(z)) -> (i x) ^ \"+\" ^ (c y) ^ \"=\" ^ (c z)\n", " | PlusEqual(L(x), I(y), L(z)) -> (c x) ^ \"+\" ^ (i y) ^ \"=\" ^ (c z)\n", " | PlusEqual(I(x), I(y), L(z)) -> (i x) ^ \"+\" ^ (i y) ^ \"=\" ^ (c z)\n", " | PlusEqual(L(x), L(y), I(z)) -> (c x) ^ \"+\" ^ (c y) ^ \"=\" ^ (i z)\n", " | PlusEqual(I(x), L(y), I(z)) -> (i x) ^ \"+\" ^ (c y) ^ \"=\" ^ (i z)\n", " | PlusEqual(L(x), I(y), I(z)) -> (c x) ^ \"+\" ^ (i y) ^ \"=\" ^ (i z)\n", " | PlusEqual(I(x), I(y), I(z)) -> (i x) ^ \"+\" ^ (i y) ^ \"=\" ^ (i z)\n", " | Or(a, b) -> (formule_vers_chaine a) ^ \"v\" ^ (formule_vers_chaine b)\n", " | And(a, b) -> (formule_vers_chaine a) ^ \"^\" ^ (formule_vers_chaine b)\n", " | Not(a) -> \"~\" ^ (formule_vers_chaine a)\n", " | Exists(L(x), a) -> \"E\" ^ (c x) ^ \", \" ^ (formule_vers_chaine a)\n", ";;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Et en bonus, on affiche aussi avec une chaîne en $\\LaTeX$ :" ] }, { "cell_type": "code", "execution_count": 42, "metadata": {}, "outputs": [ { "name": "stderr", "output_type": "stream", "text": [ "File \"[42]\", line 2, characters 4-1056:\n", "Warning 8: this pattern-matching is not exhaustive.\n", "Here is an example of a case that is not matched:\n", "Exists (I _, _)\n" ] }, { "data": { "text/plain": [ "val formule_vers_latex : formule_presburger -> string = \n" ] }, "execution_count": 42, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let rec formule_vers_latex form =\n", " match form with\n", " | Equal(L(x), L(y)) -> (c x) ^ \"=\" ^ (c y)\n", " | Equal(I(x), L(y)) -> (i x) ^ \"=\" ^ (c y)\n", " | Equal(L(x), I(y)) -> (c x) ^ \"=\" ^ (i y)\n", " | Equal(I(x), I(y)) -> (i x) ^ \"=\" ^ (i y)\n", " | PlusEqual(L(x), L(y), L(z)) -> (c x) ^ \"+\" ^ (c y) ^ \"=\" ^ (c z)\n", " | PlusEqual(I(x), L(y), L(z)) -> (i x) ^ \"+\" ^ (c y) ^ \"=\" ^ (c z)\n", " | PlusEqual(L(x), I(y), L(z)) -> (c x) ^ \"+\" ^ (i y) ^ \"=\" ^ (c z)\n", " | PlusEqual(I(x), I(y), L(z)) -> (i x) ^ \"+\" ^ (i y) ^ \"=\" ^ (c z)\n", " | PlusEqual(L(x), L(y), I(z)) -> (c x) ^ \"+\" ^ (c y) ^ \"=\" ^ (i z)\n", " | PlusEqual(I(x), L(y), I(z)) -> (i x) ^ \"+\" ^ (c y) ^ \"=\" ^ (i z)\n", " | PlusEqual(L(x), I(y), I(z)) -> (c x) ^ \"+\" ^ (i y) ^ \"=\" ^ (i z)\n", " | PlusEqual(I(x), I(y), I(z)) -> (i x) ^ \"+\" ^ (i y) ^ \"=\" ^ (i z)\n", " | Or(a, b) -> (formule_vers_latex a) ^ \"\\\\vee\" ^ (formule_vers_latex b)\n", " | And(a, b) -> (formule_vers_latex a) ^ \"\\\\wedge\" ^ (formule_vers_latex b)\n", " | Not(a) -> \"\\\\neg\" ^ (formule_vers_latex a)\n", " | Exists(L(x), a) -> \"\\\\exists \" ^ (c x) ^ \", \" ^ (formule_vers_latex a)\n", ";;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Quelques exemples de formules de Presburger\n", "On peut prendre quelques exemples de formules, et les convertir en liste de symboles.\n", "Notez qu'on perd l'information des constantes et des lettres !\n", "\n", "Des formules bien formées :\n", "\n", "- $\\phi_1 = \\exists x, x = 3$, (vraie).\n", "- $\\phi_2 = \\exists x, \\exists y, x + y = 10$, (vraie).\n", "- $\\phi_3 = \\exists x, x + 1 = 0$ (fausse)." ] }, { "cell_type": "code", "execution_count": 43, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val formule_1 : formule_presburger = Exists (L 'x', Equal (L 'x', I 3))\n" ] }, "execution_count": 43, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val formule_2 : formule_presburger =\n", " Exists (L 'x', Exists (L 'y', PlusEqual (L 'x', L 'y', I 10)))\n" ] }, "execution_count": 43, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val formule_3 : formule_presburger =\n", " Exists (L 'x', PlusEqual (L 'x', I 1, I 0))\n" ] }, "execution_count": 43, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let formule_1 = Exists(L('x'), Equal(L('x'), I(3)));;\n", "let formule_2 = Exists(L('x'), Exists(L('y'), PlusEqual(L('x'), L('y'), I(10))));;\n", "let formule_3 = Exists(L('x'), PlusEqual(L('x'), I(1), I(0)));;" ] }, { "cell_type": "code", "execution_count": 44, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "Ex, x=3\n" ] }, { "data": { "text/plain": [ "- : unit = ()\n" ] }, "execution_count": 44, "metadata": {}, "output_type": "execute_result" }, { "name": "stdout", "output_type": "stream", "text": [ "Ex, Ey, x+y=10\n" ] }, { "data": { "text/plain": [ "- : unit = ()\n" ] }, "execution_count": 44, "metadata": {}, "output_type": "execute_result" }, { "name": "stdout", "output_type": "stream", "text": [ "Ex, x+1=0\n" ] }, { "data": { "text/plain": [ "- : unit = ()\n" ] }, "execution_count": 44, "metadata": {}, "output_type": "execute_result" } ], "source": [ "print_endline (formule_vers_chaine formule_1);;\n", "print_endline (formule_vers_chaine formule_2);;\n", "print_endline (formule_vers_chaine formule_3);;" ] }, { "cell_type": "code", "execution_count": 45, "metadata": {}, "outputs": [ { "data": { "text/html": [ "$$\\exists x, x=3$$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "- : Jupyter_notebook.display_id = \n" ] }, "execution_count": 45, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/html": [ "$$\\exists x, \\exists y, x+y=10$$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "- : Jupyter_notebook.display_id = \n" ] }, "execution_count": 45, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/html": [ "$$\\exists x, x+1=0$$" ] }, "metadata": {}, "output_type": "display_data" }, { "data": { "text/plain": [ "- : Jupyter_notebook.display_id = \n" ] }, "execution_count": 45, "metadata": {}, "output_type": "execute_result" } ], "source": [ "print_latex (formule_vers_latex formule_1);;\n", "print_latex (formule_vers_latex formule_2);;\n", "print_latex (formule_vers_latex formule_3);;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "### Vérification de l'écriture préfixe pour des formules de Presburger" ] }, { "cell_type": "code", "execution_count": 46, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val sy1 : symbole_presburger list = [Ex; Let; Eq; Let; Cst]\n" ] }, "execution_count": 46, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val sy2 : symbole_presburger list = [Ex; Let; Ex; Let; PEq; Let; Let; Cst]\n" ] }, "execution_count": 46, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val sy3 : symbole_presburger list = [Ex; Let; PEq; Let; Cst; Cst]\n" ] }, "execution_count": 46, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let sy1 = formule_vers_symboles formule_1;;\n", "let sy2 = formule_vers_symboles formule_2;;\n", "let sy3 = formule_vers_symboles formule_3;;" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Elles sont évidemment bien formées." ] }, { "cell_type": "code", "execution_count": 47, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "- : bool = true\n" ] }, "execution_count": 47, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : bool = true\n" ] }, "execution_count": 47, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : bool = true\n" ] }, "execution_count": 47, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let _ = ecriture_prefixe_valide sy1 arite_presburger;; (* true *)\n", "let _ = ecriture_prefixe_valide sy2 arite_presburger;; (* true *)\n", "let _ = ecriture_prefixe_valide sy3 arite_presburger;; (* true *)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "On peut regarder d'autres suites de symboles qui ne sont pas valides." ] }, { "cell_type": "code", "execution_count": 48, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "val sy4 : symbole_presburger list = [Ex; Let; Eq; Let; Eq]\n" ] }, "execution_count": 48, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val sy5 : symbole_presburger list = [Ex; Let; Ex; Let; Eq; Let; Let; Cst]\n" ] }, "execution_count": 48, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "val sy6 : symbole_presburger list = [Ex; Let; PEq; Let; Eq; Cst]\n" ] }, "execution_count": 48, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let sy4 = [Ex; Let; Eq; Let; Eq];;\n", "let sy5 = [Ex; Let; Ex; Let; Eq; Let; Let; Cst];;\n", "let sy6 = [Ex; Let; PEq; Let; Eq; Cst];;" ] }, { "cell_type": "code", "execution_count": 49, "metadata": {}, "outputs": [ { "data": { "text/plain": [ "- : int option = Some 4\n" ] }, "execution_count": 49, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : int option = Some 6\n" ] }, "execution_count": 49, "metadata": {}, "output_type": "execute_result" }, { "data": { "text/plain": [ "- : int option = Some 5\n" ] }, "execution_count": 49, "metadata": {}, "output_type": "execute_result" } ], "source": [ "let _ = ecriture_prefixe_valide_info sy4 arite_presburger;; (* Some 4 *)\n", "let _ = ecriture_prefixe_valide_info sy5 arite_presburger;; (* Some 6 *)\n", "let _ = ecriture_prefixe_valide_info sy6 arite_presburger;; (* Some 5 *)" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Ça suffit pour cet exemple, on voulait juste montrer une autre utilisation de cette fonction `ecriture_prefixe_valide`.\n", "\n", "> Il serait difficile d'interpréter ces termes, par contre, à cause du prédicat $\\exists$...\n", "\n", "> Je n'ai pas essayé d'en faire plus ici, inutile." ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "----\n", "## Conclusion\n", "\n", "Voilà pour la question obligatoire de programmation :\n", "\n", "- on a préféré être prudent, en testant avec l'exemple du texte (calcul propositionnel) mais on a essayé un autre exemple,\n", "- on a fait des exemples et *on les garde* dans ce qu'on présente au jury.\n", "\n", "Et on a essayé de faire *un peu plus*, en implémentant l'algorithme d'évaluation des termes.\n", "\n", "> Bien-sûr, ce petit notebook ne se prétend pas être une solution optimale, ni exhaustive.\n", "\n", "> Merci à Aude et Vlad pour leur implémentation, sur laquelle ce document est principalement basé." ] } ], "metadata": { "kernelspec": { "display_name": "OCaml 4.04.2", "language": "OCaml", "name": "ocaml-jupyter" }, "language_info": { "codemirror_mode": "text/x-ocaml", "file_extension": ".ml", "mimetype": "text/x-ocaml", "name": "OCaml", "nbconverter_exporter": null, "pygments_lexer": "OCaml", "version": "4.04.2" }, "toc": { "colors": { "hover_highlight": "#DAA520", "running_highlight": "#FF0000", "selected_highlight": "#FFD700" }, "moveMenuLeft": true, "nav_menu": { "height": "289px", "width": "252px" }, "navigate_menu": true, "number_sections": true, "sideBar": true, "threshold": 4, "toc_cell": true, "toc_position": { "height": "657px", "left": "0px", "right": "1127px", "top": "117px", "width": "249px" }, "toc_section_display": "block", "toc_window_display": false } }, "nbformat": 4, "nbformat_minor": 2 }