Exemple 1. Représentation du calcul propositionnel

1.3 Exemple 1. Représentation du calcul propositionnel

Nous sommes habitués à représenter les valeurs de vérité vrai et faux par 1 et 0 (si nous représentons les connecteurs comme des opérations arithmétiques dans l'algèbre booléenne), comme nil et t en lisp, comme 0 et n'importe quelle autre valeur retournée par une fonction en C.
En l-calcul pur nous pouvons les représenter par des l-termes. Une représentation possible est la suivante :

T = l xy.x
F = l xy.y

On comprendra la grande habileté de ce choix en construisant un terme qui représente l'opérateur conditionnel. Nous pouvons le concevoir comme une fonction qui prend comme arguments une condition c et deux expressions e₁ et e₂. Cette fonction doit retourner e₁ , si c évalue à T, e₂ si c évalue à F, ce qui conduit à la définition suivante:

cond = l c e₁ e₂.( (c e₁ ) e₂)

Essayons. Soient E1 et E2 deux l -termes quelconques.

(((l c e₁ e₂ . ((c e₁) e₂ ) T ) E1 ) E2)
	®	((T E1) E2)
	=	((l xy.x E1) E2)
	®	( l y.E1 )E2
	®	E1

Naturellement on peut, pour se faciliter la vie, se définir des abbréviations comme la suivante:

if c then e1 else e2 = cond c e1 e2

Exercice : définir les autres connecteurs au moyen de l-termes et démontrer les lois de De Morgan.