Download Le Langage Caml

Représentation et vérification des propositions
215
Fichier prop.ml
let rec vérifie_lignes proposition liaisons variables =
match variables with
| [] ->
if not évalue_dans liaisons proposition
then raise (Réfutation liaisons)
| var :: autres ->
vérifie_lignes proposition ((var, true) :: liaisons) autres;
vérifie_lignes proposition ((var, false):: liaisons) autres;;
let vérifie_tautologie proposition variables =
vérifie_lignes proposition [] variables;;
La fonction vérifie_lignes vérifie toutes les lignes de la table de vérité, sans la construire effectivement. Elle prend en argument une proposition, un ensemble de liaisons
et la liste des variables libres de la proposition. Elle lie alors les variables libres à des
valeurs true ou false, puis évalue la proposition. En effet, la règle [] -> procède à
l’évaluation de la proposition, lorsqu’il n’y a plus de variables à lier. La seconde règle
correspond au cas où il y a des variables à lier ; elle exécute une séquence de deux
appels récursifs à vérifie_lignes, en liant la première variable rencontrée d’abord à
true, puis à false. Ce programme assure donc que toutes les combinaisons possibles
seront envisagées et si la vérification ne déclenche jamais l’exception Réfutation on
aura effectivement prouvé que la proposition s’évalue toujours en true dans toutes
les liaisons possibles de ses variables. La fonction vérifie_tautologie se contente
d’appeler vérifie_lignes avec un ensemble de liaisons initialement vide.
Dans un style apparemment plus « fonctionnel », on écrirait :
let rec vérifie_lignes proposition liaisons = function
| [] ->
évalue_dans liaisons proposition || raise (Réfutation liaisons)
| var :: autres ->
vérifie_lignes proposition ((var, true) :: liaisons) autres &&
vérifie_lignes proposition ((var, false):: liaisons) autres;;
Cette version n’est pas plus claire que la précédente : elle est trompeuse car bien qu’elle
semble calculer un booléen, son résultat n’est pas intéressant. En effet, elle retourne
toujours le booléen true si la proposition est une tautologie, ou lève une exception si la
proposition est réfutable. C’est donc bien une procédure, puisqu’elle fonctionne par effets : l’effet attendu est soit « évaluation réussie », soit un déclenchement d’exception. Il
ne sert à rien de la déguiser en fonction . . . Si l’on renonce à renvoyer une réfutation de
la proposition analysée, il est possible d’écrire une vraie fonction qui calcule vraiment
un booléen. Malheureusement on perd la liaison des variables qui a prouvé que la proposition n’est pas une tautologie et il faut alors écrire une autre fonction, complètement
analogue, pour renvoyer une réfutation. Cet exemple nous montre un autre intérêt
des exceptions : dans certains cas une fonction peut calculer en fait deux résultats de
type différent, l’un véhiculé par le mécanisme normal des appels de fonctions, l’autre
transporté par une exception (vérifie_lignes calcule un booléen dans le cas d’une
tautologie et une liste d’association (nom de variable, valeur booléenne) dans le cas
contraire).