Logique combinatoire - Définition

Le système de type

On peut associer un type à chacun des combinateurs. Le type d'un combinateur dit comment il prend en compte le type de ses paramètres pour produire un objet d'un certain type. Ainsi le combinateur I change son paramètre en lui-même ; si on attribue le type α à ce paramètre x, alors on peut dire que Ix a le type α et que I a le type α → α. Ici la flèche → désigne le constructeur de type fonctionnel, en gros α → α est le type de la classe des fonctions de α vers α, → a construit une nouveau type α → α à partir du type α.

K prend un paramètre, disons de type α et rend une fonction d'un paramètre de type β qui rend le premier paramètre, le type de cette dernière fonction est donc β → α et le type de K est ainsi α → (β → α), que l'on écrit α → β → α. S prend trois paramètres x, y et z ; donnons le type α au troisième paramètre z et le type γ au résultat final, le deuxième paramètre y prend un paramètre de type α et rend un paramètre de type disons β (son type est donc α → β), le premier paramètre x prend un paramètre de type α et rend une fonction de type β → γ, son type est donc α → (β → γ), que l'on écrit α → β → γ. Résumons-nous, on a z:α , y: β → α et x: α → β → γ et S x y z: γ, on en conclut que S a le type (α → β → γ) → (α → β) → α → γ.

Le résultat M N qui consiste à appliquer M à N est typable si M à un type fonctionnel, disons α → β et si N a pour type α. M N a alors pour type β.

Le type de B est (α → β) → (γ → α) → γ → β. On le voit soit en remarquant que B x y z →* x (y z), soit en appliquant la règle de composition à S (K S) K.

Le type de C est (α → β → γ) → β → α → γ, pour les mêmes raisons que celles invoquées pour B.

Le combinateur W n'est pas typable.

En résumé:

K : α → β → α

S : (α → β → γ) → (α → β) → α → γ

I  : α → α

B : (α → β) → (γ → α) → γ → β

C : (α → β → γ) → β → α → γ

Forte normalisation

Si M est un combinateur typé, alors toute chaine de réduction qui commence en M est finie. On appelle cette propriété la forte normalisation.

Quelques combinateurs dérivés

• B ≡ S (K S) K. Le combinateur B correspond à l'opérateur de composition des fonctions habituellement noté «   ». Son nom est dérivé du syllogisme Barbara. On a donc

B x y z ≡ S (K S) K x y z

→ K S x (K x) y z

→ S (K x) y z

→ K x z (y z)

→ x (y z).

• C ≡ S (B B S) (K K) est un combinateur qui intervertit ses paramètres.

C x y z ≡ S (B B S) (K K) x y z

→ B B S x (K K x) y z

→ B (S x) (K K x) y z

→ S x (K K x y) z

→ x z (K K x y z)

→ x z (K y z)

→ x z y

• W ≡ S I I. Le combinateur W permet de construire un autre combinateur à savoir W W, qui a la propriété de se réduire à lui-même. On a ainsi

W W ≡ S I I (S I I)

→ I (S I I) (I (S I I))

→ S I I (I (S I I))

→ S I I (S I I) ≡ W W