Fondements de la théorie du traitement de l'information

Pour formaliser la notion de traitement de l'information, il convient de formaliser

la notion d'information
la notion de traitement.

L'objectif est de trouver une formalisation la plus simple possible, basée sur un nombre le plus petit possible de concepts de base.

Nous allons d'abord montrer que l'information peut être représentée par un traitement d'information, ce qui permet de faire reposer toute la théorie sur le concept de traitement ou d'opération.

L'information la plus élémentaire concevable est binaire : vrai ou faux, 0 ou 1... On peut représenter cette information par une opération de choix entre deux possibilités, une fonction qui à deux arguments associe par exemple le premier pour la valeur vraie, et le second pour la valeur faux.

Des informations plus complexes peuvent être représentées par des structures, la plus élémentaires étant le couple de deux valeurs, qui peut être représenté par une fonction qui à la valeur vraie associe la première valeur du couple, et à la valeur faux la seconde.

Voyons maintenant comment on peut représenter le concept d'opération ou de fonction. Il s'agit de produire un certain nombre de résultats à partir d'un certain nombre de données. On peut en fait se limiter au cas où on produit un résultat à partir d'une donnée car plusieurs données ou résultats peuvent être représentés par une seule donnée ou un seule résultat, une structure regroupant ces éléments. D'autre part, la production d'un résultat par application d'une fonction à plusieurs arguments donnés peut être décomposée : l'application de la fonction au premier argument donne une nouvelle fonction qu'on applique au deuxième argument, et ainsi de suite.

On est donc ramené au problème de la représentation d'une fonction (ou combinateur) f qui produit un résultat y à partir d'un argument x. Les différents cas sont les suivants :

Ce résultat ne résulte pas de l'application d'une fonction à un argument, il est élémentaire.
- C'est l'argument lui-même : la fonction n'effectue aucune transformation sur son argument, on l'appelle l'identité et on la note I. On note I x = x pour exprimer le fait que cette fonction rend son argument en résultat.
- Ce n'est pas l'argument mais une autre valeur y qui ne dépend pas de l'argument. La fonction est une fonction constante qui rend toujours y quel que soit la valeur de son argument. On la note K y, qu'on peut voir comme le résultat de l'application d'une fonction K constructrice de fonctions constantes à la valeur y du résultat. On a donc K y x = y.
Ce résultat est le résultat de l'application d'une fonction a à un argument b (y = a b), pouvant tous deux dépendre de l'argument x de f. On peut formaliser cette dépendance par des fonctions g qui à x associe a et h qui à x associe b. La fonction f dépend donc des fonctions f et g. On formalise cette dépendance par une fonction notée S. On écrit "f = S g h" ce qui signifie que la fonction S appliquée à g donne une fonction qui est elle-même appliquée à h pour donner f. (On peut écrire f = (S g) h mais les parenthèses en début d'expression sont facultatives par convention de notation). On a donc :
- f x = y
- donc S g h x = y
- mais :
  - y = a b
  - a = g x
  - b = h x
  - donc y = (g x) (a x)
- donc S g h x = (g x) (h x)

Cette décomposition s'arrête-t-elle ou continue-t-elle à l'infini ? Si elle s'arrête, on peut alors représenter f par une combinaison finie de I, K et S (ou même de K et S seulement car on peut remarquer que I = S K K). Si elle est infinie, peut-on néanmoins la décrire de façon finie ? Si on ne peut pas, elle n'est pas représentable par un expression finie. Si on peut, quelle forme peut prendre cette représentation ? On peut la représenter de façon récursive. Par exemple :
factorielle n = si n = 0 alors 1 sinon n * factorielle (n-1)
Une fonction récursive peut être définie comme le point fixe d'une fonctionnelle, par exemple dans le cas de la factorielle, celle qui à f associe la fonction qui à n associe (si n = 0 alors 1 sinon n * f (n-1)). Un point fixe f d'une fonction F est un élément inchangé par F, c'est-à-dire un f tel que F f = f.
On peut représenter le point fixe avec I, K et S de la façon suivante : Le point fixe d'une fonction F est l'auto-application de la composée de F et de l'auto-application.
On définit l'auto-application A par A x = x x, c'est-à-dire A = S I I, et la composée : B f g x = f (g x). Un point fixe de F noté Y F est donc A (B F A). On a en effet :

Y F = A (B F A)
= B F A (B F A)
= F (A (B F A))
= F (Y F).

En résumé, on peut représenter n'importe quelle opération et n'importe quelle structure de données par une combinaison par application des combinateurs de base I, K et S. Ces combinateurs sont définis par les règles :

I a = a
K a b = a
S a b c = a c (b c)

Si on note \x.y la fonction qui à x associe y, on a :

\x.x = I
\x.y = K y si y ne dépend pas de x
\x.(a b) = S (\x.a) (\x.b)

Pour compléter la théorie, on doit ajouter aux règles définissant les combinateurs de base celles définissant l'égalité. On a d'abord la règle d'égalité des applications : si f = g et a = b, alors f a = g b. L'égalité est une relation d'équivalence, réfléxive, symétrique et transitive. La réflexivité (x = x) peut être construite pour tout x à partir des axiomes I = I, K = K et S = S et de la règle d'égalité des applications. La symétrie (si x = y alors y = x) et la transitivité (si x = y et y = z alors x = z) peuvent être remplacées par une règle unique, la transymétrie droite (si x = z et y = z alors x = y) ou la transymétrie gauche (si x = y et x = z alors y = z).

Les règles définissant les combinateurs de base pourraient être formalisées par des règles telles que : "Si a est un terme, alors I a = a" mais cela aboutirait à deux types de propositions élémentaires :

x est un terme
x = y

On peut éviter cette dualité en représentant la proposition "x est un terme" par la proposition "x = x". Ainsi l'axiome "I est un terme" est identifié à l'axiome "I = I" et la règle "Si f est un terme et a est un terme alors f a est un terme" à la règle d'égalité des applications. La règle "Si a est un terme alors I a = a" devient donc "Si a = a alors I a = a". Mais on peut encore simplifier en réalisant qu'en fait la condition "Si a = a" n'est qu'une abréviation pour "Si a = b et si a est syntaxiquement égal à b" (on s'en aperçoit en programmant) et que la condition "a est syntaxiquement égal à b" est inutile. On obtient finalement "Si a = b alors I a = b". De même pour les règles définissant K et S.

En résumé, la logique combinatoire peut être formalisée axiomatiquement de la façon suivante :

Si x = z et y = z alors x = y
Si f = g et a = b alors f a = g b
I = I
K = K
S = S
Si a = a' alors I a = a'
Si a = a' et b = b' alors K a b = a'
Si a = a' et b = b' et c = c' alors S a b c = a' c' (b' c')

Une autre approche de la logique combinatoire est décrite dans la Grande Encyclopédie Larousse. Elle consiste à voir une expression f k a1 a2 a3... comme une opération f agissant sur une pile a1 a2 a3... avec une continuation k. Les opérations de base sont :

I k = k : l'opération vide
K k a = k : dépiler
W k a = k a a : répéter
C k a b = k b a : permuter
B f g k = f (g k) : séquencer

La logique combinatoire peut être étendue par l'ajout de nouveaux éléments de base appelés symboles, dont la sémantique est définie par des axiomes d'égalités entre des termes contenant ces symboles. On obtient ainsi la logique combinatoire symbolique. Par exemple, pour représenter une opération commutative on introduit un symbole F avec bien sûr l'axiome d'existence et de réflexivité de F, F = F, mais aussi l'axiome de commutativité qui doit exprimer F x y = F y x, c'est-à-dire \x. \y. F x y = \x. \y. F y x, ou F = C F = S (K (S F)).
On peut représenter une théorie avec un nombre quelconque de symboles Z1, ... Zn et d'axiomes définissant ces symboles f1 Z1 ... Zn = g1 Z1 ... Zn, ... , fp Z1 ... Zn = gp Z1 ... Zn, par une théorie avec un seul symbole Z et un seul axiome f Z = g Z, à savoir :
< f1 (Z s1) ... (Z sn), ... , fp (Z s1) ... (Z sn) > = < g1 (Z s1) ... (Z sn), ... , gp (Z s1) ... (Z sn) >,
avec f = f a1 ... an
et si a1 ... an = ai.

La logique propositionnelle classique est habituellement formalisée par les règles suivantes :

la règle de modus ponens : si (p => q) et p, alors q
(AI : p => p)
l'axiome AK : p => (q => p)
l'axiome AS : (p => (q => r)) => ((p => q) => (p => r))
l'axiome de raisonnement par l'absurde : ((p => faux) => faux) => p.

On peut remarquer une correspondence avec les combinateurs : si on associe des types aux arguments et résultats des fonctions, I est du type a -> a (fonction qui à un argument de type a associe un résultat du type a), K est du type a -> (b -> a), et S du type (a -> (b -> c)) -> ((a -> c) -> (b -> c)). La règle de modus ponens correspond à l'application, et la notion d'hypothèse à l'abstraction \x.y. De même que le combinateur I peut être défini par I = S K K, AI n'est pas nécessaire comme axiome car il peut être déduit de AK et AS.

La difficulté pour formaliser la logique à partir de la logique combinatoire vient de l'existence du point fixe, qui entraine la possibilité de construire une proposition p telle que p = ~p, ou p = p => faux, ce qui, en logique classique ou même en logique intuitionniste, entraine une inconsistance :

Supposons p :
- alors (par définition de p) p => faux
- alors (par modus ponens) faux
donc p => faux
donc p, par définition de p
donc faux, par modus ponens.

On ne peut éviter cette inconsistance qu'au prix d'un affaiblissement très important qui consiste à distinguer deux types d'implication :

l'implication affirmative p =!> q : si j'ai pu démontrer p, alors je peux affirmer q. Cette implication est formalisée par le modus ponens : si (p =!> q) et p, alors q.
l'implication interrogative p =?> q : si je suppose p, je peux en déduire q. Cette implication est formalisée par les règles suivantes :
- p =?> p : sous l'hypothèse p, p est vrai.
- p =!> (q =?> p) : une proposition vraie hors hypothèse reste vraie sous hypothèse.
- (p =?> (q =!> r)) =!> ((p =?> q) =!> (p =?> r) : on peut appliquer le modus ponens sous l'hypothèse p.

Avec la logique combinatoire, la notion de proposition p est remplacée par celle d'égalité a = b. L'implication p =!> q devient (a = b) =!> (c = d) que l'on peut représenter par E! a b c = E! a b d, où E! est un symbole. De même pour =!> et E?.

Le modus ponens devient :

si (E! a b c = E! a b d) et (a = b), alors (c = d)
c'est-à-dire : si E! a a c = E! a a d, alors c = d,
qui est vérifié si E! a a = I
ou S E! I = K I

La règle p =?> p devient E? a b a = E? a b b

La règle p =!> (q =?> p) devient : si a = b alors E? c d a = E? c d b, que l'on peut obtenir par la règle d'égalité d'applications. Cette règle est donc inutile.

L'axiome d'application du modus ponens sous hypothèse
(p =?> (q =!> r)) =!> (p =?> q) =!> (p =?> r)
peut être obtenue par l'axiome
E? a b (f x) = E? a b f (E? a b x)
En effet, si on a E? a b (E! c d e) = E? a b (E! c d f)
et E? a b c = E? a b d,
on peut inférer E? a b e = E? a b f.
En effet, on a :

E? a b (E! c d e) = (E? a b E!) (E? a b c) (E? a b d) (E? a b e)
= (E? a b E!) (E? a b c) (E? a b c) (E? a b e)
= E? a b (E! c c e)
= E? a b e

De même, E? a b (E! c d f) = E? a b f
Donc E? a b e = E? a b f.

En résumé, cette logique affaiblie permettant de manipuler des propositions égales à leur propre négation sans être inconsistante, peut être formalisée en logique combinatoire symbolique en ajoutant les symboles E! et E? définis par les axiomes :

E! = E!
E? = E?
S E! I = K I
\a. \b. E? a b a = \a. \b. E? a b b
\a. \b. \f. \x. E? a b (f x) = \a. \b. \f. \x. E? a b f (E? a b x)