Logique combinatoire

Logique combinatoire
Page d'aide sur l'homonymie Pour les articles homonymes, voir combinatoire (homonymie).
Page d'aide sur l'homonymie Cet article traite de la logique combinatoire, au sens qu'a ce mot en logique mathématique et en informatique théorique. Il ne doit pas être confondu avec ce que l'on appelle logique combinatoire en électronique.

La logique combinatoire est une notation introduite par Moses Schönfinkel et Haskell Curry pour supprimer le besoin de variables en mathématiques, pour formaliser rigoureusement la notion de fonction et pour minimiser le nombre d'opérateurs nécessaires pour définir le calcul des prédicats à la suite de Henry M. Sheffer. Plus récemment elle a été utilisée en informatique comme modèle théorique de calcul et comme base pour la conception de langages de programmation fonctionnels.

Le concept de base de la logique combinatoire est celui de combinateur qui est une fonction d'ordre supérieur ; elle utilise uniquement l'application de fonctions et éventuellement d'autres combinateurs pour définir de nouvelles fonctions d'ordre supérieur. Elle a des liens très forts avec le lambda calcul et avec la logique intuitionniste grâce à la correspondance de Curry-Howard.

Sommaire

Introduction

La logique combinatoire est fondée sur deux « opérations » de base (on dit aussi deux « combinateurs ») S et K que nous définirons plus loin ; plus précisément nous en définirons le comportement ou l'« intention », car la logique combinatoire est une approche de la logique qui montre plutôt comment marchent les choses que comment les objets peuvent être décrits, on dit alors que c'est une approche intentionnelle de la logique. Si l'on veut définir la fonction[1] que nous appellerons C et qui prend trois paramètres et rend comme résultat le premier appliqué au troisième, le tout étant appliqué au second, on pourra l'écrire :

C ≡ S ((S (K S) K) (S (K S) K) S) (K K)

qui, comme on le voit, ne comporte pas de variable. On pourra regretter que l'avantage de ne pas utiliser de variables se paie par la longueur des expressions et une certaine illisibilité. Aujourd'hui la logique combinatoire est surtout utilisée par les logiciens pour répondre positivement à la question « Est-il possible de se passer de variables ? » et par les informaticiens pour compiler les langages fonctionnels[2].

Les combinateurs de base

Le plus simple des combinateurs est I (identité) défini par[3]

I x = x.

Un autre combinateur simple est K, il fabrique des fonctions constantes, ainsi (K x) est la fonction qui, pour tout paramètre, retourne x, autrement dit

(K x) y = x

pour tous termes x et y. Comme en lambda-calcul, on associe les applications de gauche à droite, ce qui permet de supprimer des parenthèses, ainsi on écrit

K x y = x.

Un autre combinateur de base est S qui distribue le paramètre (ici z) aux applications composantes :

S x y z = x z (y z)

S applique le résultat de l'application de x à z au résultat de l'application de y à z.

I peut être construit à partir de S et K, en effet :

(S K K) x = S K K x
= K x (K x)
= x.

On décrète donc que I est un combinateur dérivé et que I = S K K et on décide de décrire tous les combinateurs à l'aide de S et K, ce qui est raisonnable car on peut montrer que cela suffit pour décrire « toutes » les fonctions d'une certaine forme[4].

La réduction

En fait, les transformations fonctionnent comme des réductions et pour cela on les note →. On obtient donc les deux règles de réduction de base de la logique combinatoire.

K x y → x,
S x y z → x z (y z).

Quelques combinateurs dérivés

  • BS (K S) K. Le combinateur B correspond à l'opérateur de composition des fonctions habituellement noté « \circ ». 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).
  • CS (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
  • WS 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 WS 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


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.

La logique combinatoire et la correspondance de Curry-Howard

On constate que le modus ponens

\frac{P \to Q \qquad P}{Q}

ressemble à la règle de conservation des types quand on applique un combinateur de type α → β à un combinateur de type α. Examinons aussi les deux premiers axiomes de la présentation à la Hilbert de la logique propositionnelle à savoir:

PQP
(PQR) → (PQ) → PR.

Rappelons qu'ils permettent de formaliser le calcul propositionnel intuitionniste. On remarque que le premier axiome est identique au type de K et que le deuxième axiome est identique au type de S si l'on remplace la proposition P par α, la proposition Q par β et la proposition R par γ. Cette correspondance entre proposition et type et entre combinateur et démonstration s'appelle la correspondance de Curry-Howard. Elle met en parallèle le système de déduction à la Hilbert pour la logique propositionnelle intuitionniste et la logique combinatoire qui ont été, notons-le, découverts indépendamment.

Références

  1. Plus précisément le combinateur.
  2. Quoique les informaticiens utilisent une logique fondée sur des super-combinateurs moins bavarde que la logique combinatoire fondée sur S et K.
  3. x qui apparait ici n'est pas une variable du langage de la logique combinatoire, car comme on l'a dit la logique variable se passe de variables ; en fait, x est une « méta-variable » qui permet de présenter les identités de la logique combinatoire.
  4. Théorème de complétude de Harvey Friedman.

Bibliographie

  • Haskell Curry et Robert Feys, Combinatory Logic I. North Holland 1958. La plupart du contenu de cet ouvrage fut rendu obsolète par l'ouvrage de 1972 et les suivants.
  • H. Curry, J. R. Hindley etJ. P. Seldin, Combinatory Logic II. North-Holland, 1972. Une rétrospective complète de la logique combinatoire, incluant une approche chronologique.
  • J.-P. Desclés, Langages applicatifs, langues naturelles et cognition, 1990. Paris, Hermès.
  • Jean-Pierre Ginisti, La logique combinatoire, Paris, PUF (coll. « Que sais-je? » n°3205), 1997, 127 p.
  • M. Shönfinkel, In: J. van Heijenoort, Editor, From Frege to Gödel, Harvard University Press, Cambridge, MA (1967), pp. 355–366 1924.
  • J.-L. Krivine, Lambda-calcul, types et modèles, Masson, 1990, chap. Logique combinatoire, traduction anglaise accessible sur le site de l'auteur [1].

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Logique combinatoire de Wikipédia en français (auteurs)

Игры ⚽ Поможем сделать НИР

Regardez d'autres dictionnaires:

  • Logique Combinatoire — Pour les articles homonymes, voir combinatoire (homonymie). Avertissement: Cet article traite de la logique combinatoire, au sens qu a ce mot en logique mathématique et en informatique théorique. Il ne doit pas être confondu avec ce que l on… …   Wikipédia en Français

  • Logique combinatoire — ● Logique combinatoire théorie logique fondée sur l élimination complète des variables et des connecteurs, à l exception d une notation pour désigner l application d une fonction unaire à son argument …   Encyclopédie Universelle

  • logique combinatoire — kombinatorinė logika statusas T sritis automatika atitikmenys: angl. combinational logic; combinatory logic; combinatorial logic vok. kombinatorische Logik, f; Schaltlogik, f rus. комбинаторная логика, f pranc. logique combinatoire, f …   Automatikos terminų žodynas

  • Logique combinatoire (Electronique) — Logique combinatoire Pour les articles homonymes, voir combinatoire (homonymie). Avertissement: Cet article traite de la logique combinatoire, au sens qu a ce mot en logique mathématique et en informatique théorique. Il ne doit pas être confondu… …   Wikipédia en Français

  • fonction logique combinatoire — kombinacinė loginė funkcija statusas T sritis automatika atitikmenys: angl. combinational logic function vok. kombinatorische Logikfunktion, f rus. комбинационная логическая функция, f pranc. fonction logique combinatoire, f …   Automatikos terminų žodynas

  • combinatoire — [ kɔ̃binatwar ] adj. et n. f. • 1732 philos.; de combiner 1 ♦ (1819) Relatif aux combinaisons, à leur dénombrement et leur mise en ordre; qui procède par combinaison d éléments. Math. Analyse combinatoire : théorie des ensembles finis traitant du …   Encyclopédie Universelle

  • LOGIQUE (HISTOIRE DE LA) — Ce n’est qu’à une époque relativement récente qu’on a vraiment commencé à s’intéresser à l’histoire de la logique. Jusqu’au milieu du XIXe siècle régnait en effet l’idée que la logique n’avait pas d’histoire, étant, pour l’essentiel, sortie… …   Encyclopédie Universelle

  • Logique Séquentielle — En théorie des circuits électroniques, la logique séquentielle est un type de logique dont les résultats ne dépendent pas seulement des données actuellement traitées mais aussi des données traitées précédemment. Elle s oppose à la logique… …   Wikipédia en Français

  • Logique sequentielle — Logique séquentielle En théorie des circuits électroniques, la logique séquentielle est un type de logique dont les résultats ne dépendent pas seulement des données actuellement traitées mais aussi des données traitées précédemment. Elle s oppose …   Wikipédia en Français

  • Logique séquentielle — En théorie des circuits électroniques, la logique séquentielle est un type de logique dont les résultats ne dépendent pas seulement des données actuellement traitées mais aussi des données traitées précédemment. Elle s oppose à la logique… …   Wikipédia en Français

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”