Problème — Une grammaire pour la logique propositionnelle

1. La grammaire. On note $\neg$ par {}, $\wedge$ par &, $\vee$ par | et $\Rightarrow$ par >. Un niveau par priorité, du moins prioritaire au plus prioritaire. On écrit les règles une par ligne et l'on sépare les variantes par le mot « ou » : la barre verticale appartient ici à l'alphabet, elle ne peut donc plus servir de notation pour l'alternance.

I  -->  D > I    ou   D            (implication, recursive a DROITE)
D  -->  D | C    ou   C            (disjonction, recursive a gauche)
C  -->  C & N    ou   N            (conjonction, recursive a gauche)
N  -->    N      ou   A            (negation, prefixe)
A  -->  ( I )    ou   p  ou  q  ou  r  ou  0  ou  1

L'implication est le seul niveau récursif à droite, et ce n'est pas un détail de présentation : c'est ainsi que $p\Rightarrow q\Rightarrow r$ se lit $p\Rightarrow (q\Rightarrow r)$. Les deux autres binaires sont récursifs à gauche, donc traduits par des boucles.

2. L'analyseur. Le type est celui du chapitre chap:logique ; la grammaire en est la syntaxe concrète.

type formule =
  | Vrai | Faux
  | Var of char
  | Non of formule
  | Et of formule * formule
  | Ou of formule * formule
  | Implique of formule * formule

let analyser texte =
  let n = String.length texte in
  let pos = ref 0 in
  let regarde () = if !pos < n then Some texte.[!pos] else None in
  let lire c =
    if !pos < n && texte.[!pos] = c then incr pos
    else raise (Echec (Printf.sprintf "attendu %c en position %d" c !pos))
  in
  let rec i () =                       (* implication : recursive a DROITE *)
    let g = d () in
    match regarde () with
    | Some '>' -> lire '>'; Implique (g, i ())
    | _ -> g
  and d () =                           (* disjonction : a gauche, donc BOUCLE *)
    let acc = ref (c ()) in
    while regarde () = Some '|' do lire '|'; acc := Ou (!acc, c ()) done;
    !acc
  and c () =                           (* conjonction : a gauche, donc BOUCLE *)
    let acc = ref (nn ()) in
    while regarde () = Some '&' do lire '&'; acc := Et (!acc, nn ()) done;
    !acc
  and nn () =
    match regarde () with
    | Some ' ' -> lire ' '; Non (nn ())
    | _ -> atome ()
  and atome () =
    match regarde () with
    | Some '(' -> lire '('; let x = i () in lire ')'; x
    | Some '0' -> lire '0'; Faux
    | Some '1' -> lire '1'; Vrai
    | Some ch when ch >= 'p' && ch <= 'r' -> incr pos; Var ch
    | Some ch -> raise (Echec (Printf.sprintf "symbole inattendu %c en %d" ch !pos))
    | None -> raise (Echec "formule attendue, fin du texte")
  in
  let x = i () in
  if !pos <> n then raise (Echec (Printf.sprintf "reste a lire en %d" !pos));
  x

Noter que nn s'appelle elle-même pour la négation préfixe : c'est une récursivité à droite, elle consomme le {} avant de s'appeler, donc elle termine.

3. Décider une tautologie. On évalue sous les $2^3=8$ valuations et l'on regarde si la réponse est toujours vraie. Les tables de vérité mesurées, les huit valuations étant rangées dans l'ordre binaire de $(p,q,r)$, de $000$ à $111$ :

Trois lectures de ce tableau :

• les priorités sont bien celles annoncées : p|q&r et (p|q)&r n'ont pas la même table ; sans les niveaux de la grammaire, on ne pourrait pas les distinguer ;
• l'associativité de l'implication compte : p>q>r et (p>q)>r diffèrent ;
• les lois de De Morgan se lisent : {(p&q)} et {p| {}q} ont la même table. Le programme le confirme aussi pour {(p|q)} et {p& {}q}, et pour p>q et {p|q}.

Le dernier essai, $(p\Rightarrow q)\wedge (q\Rightarrow r)\Rightarrow (p\Rightarrow r)$, a une table constante à $1$ : c'est le syllogisme, et c'est bien une tautologie — mesuré, pas supposé.

Ce que le problème apporte. Le chapitre chap:logique manipule des formules ; le chapitre chap:deduction les démontre. Ni l'un ni l'autre ne dit d'où vient l'objet. Il vient d'ici : un texte, une grammaire, un analyseur, un arbre. Le passage de la syntaxe concrète — une chaîne de caractères — à la syntaxe abstraite — une valeur du type inductif — est le seul endroit du livre où l'on voit une formule naître.