Voir la source de Logique combinatoire

{{homonyme|combinatoire (homonymie)}}
{{confusion|texte=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 (électronique)|logique combinatoire]] en [[électronique numérique]].}}

En [[logique mathématique]], la '''logique combinatoire''' est une théorie [[Logique mathématique|logique]]<ref>{{Ouvrage|prénom1=Katalin|nom1=Bimbó|titre=The Stanford Encyclopedia of Philosophy|éditeur=Metaphysics Research Lab, Stanford University|date=2016|lire en ligne=https://plato.stanford.edu/archives/win2016/entries/logic-combinatory/|consulté le=2017-10-10}}</ref> introduite par [[Moses Schönfinkel]]<ref>[[Moses Schönfinkel]] "Über die Bausteine der mathematischen Logik", ''Mathematische Annalen'' '''92''', {{p.}}305-316. Traduit en français par Geneviève Vandevelde : {{Article
| prénom = Moses
| nom = Schönfinkel 
| titre = Sur les éléments de construction de la logique mathématique
| année = 1990 
| journal =  Mathématiques et sciences humaines
| volume = 112
| pages = 5-26
| lire en ligne = http://www.numdam.org/article/MSH_1990__112__5_0.pdf
}}
 et traduit en anglais dans {{chapitre | auteur = [[Moses Schönfinkel]] | traducteur = Stefan Bauer-Mengelberg | titre = On the building blocks of mathematical logic| auteur ouvrage = [[Jean van Heijenoort]] |date =  1967 | titre ouvrage = A Source Book in Mathematical Logic, 1879-1931 | éditeur = Harvard Univ. Press | page = 355-66| lire en ligne = http://sshieh.web.wesleyan.edu/wescourses/2013f/388/e-texts/Schonfinkel%20On%20the%20Building%20Blocks%20of%20Mathematical%20Logic.pdf}}.</ref> en 1920 lors d'une conférence{{Laquelle|date=5 juin 2023}} et développée dès 1929 par [[Haskell Curry|Haskell Brooks Curry]]<ref>{{Article|prénom1=H. B.|nom1=Curry|titre=Grundlagen der Kombinatorischen Logik|périodique=American Journal of Mathematics|volume=52|numéro=3|date=1930|doi=10.2307/2370619|lire en ligne=https://www.jstor.org/stable/2370619|consulté le=2017-10-11|pages=509–536}}</ref> pour supprimer le besoin de variables en [[mathématiques]], pour formaliser rigoureusement la notion de [[Routine (informatique)|fonction]] et pour minimiser le nombre d'[[Connecteur logique|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 [[programmation fonctionnelle|langages de programmation fonctionnels]].

Le concept de base de la logique combinatoire est celui de combinateur qui est une fonction d'[[Fonction d'ordre supérieur|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. Chaque combinateur simplement typable est une [[système à la Hilbert|démonstration à la Hilbert]] en [[logique intuitionniste]] et vice-versa <ref> H. Curry, J. R. Hindley et J. P. Seldin, ''Combinatory Logic II''. North-Holland, 1972.</ref>. On appelle ceci la [[correspondance de Curry-Howard]]

== 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<ref>Plus précisément le combinateur.</ref> 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 [[Compilateur|compiler]] les langages fonctionnels<ref>Quoique les informaticiens utilisent une logique fondée sur des super-combinateurs moins bavarde que la logique combinatoire fondée sur '''S''' et '''K'''.</ref>.

La logique combinatoire est un [[Système de réécriture|système de réécriture du premier ordre]]. C'est-à-dire qu'à la différence du [[lambda-calcul]], il ne comporte pas de variables liées, ce qui permet une théorie beaucoup plus simple. Il n'a que trois opérateurs : un opérateur binaire et deux constantes.

;Le parenthésage : Pour alléger l'écriture, la logique combinatoire supprime certaines parenthèses et adopte par convention l'associativité à gauche. En d'autres termes, (a b c d ... z) est un raccourci d'écriture pour (...(((a b) c) d) ... z)<ref>Cette convention est plutôt malheureuse car on adopte l'associativité à droite pour l'écriture du [[#Le système de type|type du combinateur]].</ref>.

== Les combinateurs de base ==

Le combinateur identité, noté '''I''', est défini par<ref>''x'' qui apparaît 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.</ref>
:'''I''' ''x'' = ''x''.

Un autre combinateur, noté '''K''', fabrique des fonctions constantes : ('''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, noté '''S''', 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<ref>Théorème de complétude de [[Harvey Friedman]].</ref>{{,}}<ref>{{Référence Harvard sans parenthèses|Henk Barendregt|1984|p=90}}</ref>.

== 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 ==
* '''B''' ≡ '''S''' ('''K S''') '''K'''. Le combinateur '''B''' correspond à l'opérateur de composition des fonctions habituellement noté « <math>\circ</math> ». Son nom est dérivé du [[Barbara (syllogisme)|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'''

== Le système de type ==

On peut associer un [[théorie des types|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 '''I'''x 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 un 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''' a 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'''.

'''W''' en revanche n'est pas typable. On peut voir cela en se rappelant que '''S''' : (α → β → γ) → (α → β) → α → γ et '''I''' : (α → α).
Si on applique '''S''' à '''I''' on doit avoir α = β → γ, puis si on applique '''S I''' à I on doit avoir α = β, donc β = β → γ. Cette équation n'a pas de solution. Donc '''S I I''' = '''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
: <math>\frac{P \to Q \qquad P}{Q}</math>
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 [[Calcul des propositions#La déduction à la Hilbert|présentation à la Hilbert de la logique propositionnelle]] à savoir:
:'''K''' : ''P'' → ''Q'' → ''P''
:'''S''' : (''P'' → ''Q'' → ''R'') → (''P'' → ''Q'') → ''P'' → ''R''.
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.

=== Un exemple ===
La formule
:: '''B''' : (α → β) → (γ → α) → γ → β
signifie (dans le langage de [[Rocq (logiciel)|Rocq]], par exemple) que '''B''' est une preuve de la [[formule propositionnelle]] (α → β) → (γ → α) → γ → β.
::'''B ≡ S (K S) K'''
fournit alors une preuve effective de la formule dans la [[système à la Hilbert|théorie de Hilbert]] qui n'emploie que le [[modus ponens]] et les axiomes K et S.

Cela demande un petit travail de réécriture:
Tout d'abord, on rétablit les parenthèses
::'''B ≡ (S (K S)) K'''
ensuite, on introduit l'opérateur '''⇒'''
::'''B ≡ (S ⇒ (K ⇒ S)) ⇒ K'''
enfin, on emploie la [[Notations infixée, préfixée, polonaise et postfixée|notation postfixée]] :
::'''B ≡ K S K ⇒ S ⇒ ⇒'''
Alors cette formule donne les étapes de la démonstration dans le sens de la déduction<ref>C'est-à-dire, que l'on va des hypothèses (ici des axiomes) au but à atteindre.</ref>. ⇒ dénote le recours au modus ponens ; K et S, l'utilisation des axiomes K et S. Plus, précisément '''Q ≡ I P ⇒''' signifie que si '''I''' est la démonstration de ''P'' → ''Q'', et '''P''' la démonstration de ''P'', alors '''I P ⇒''' est bien celle de ''Q''. Malheureusement cette formule ne fournit pas les opérations de substitutions qui doivent être utilisées dans l'introduction des axiomes.

La notation préfixée,
::'''B ≡ ⇒ ⇒ S ⇒ K S K'''
représente le sens de la démonstration dans le langage de Rocq<ref>C'est-à-dire, l'ordre des tactiques (« tactic » en anglais) employées. Rocq procède par modification du but jusqu'à l'identifier aux hypothèses, aux théorèmes, ou aux axiomes.</ref>. Ici, les informations manquantes sont les formules des ''P'' employés dans les modus ponens.
{{démonstration/début}}
Pour alléger l'écriture, on note
* ''P⁰=(P→Q)''
* ''Q⁰=(R→P→Q)''
* ''R⁰=(R→P)→(R→Q)''
* '''MP'''(''P'') dénote l'utilisation du modus ponens avec la [[prémisse]] ''P''
Le but est donc
* ''B = P⁰ → R⁰''.<!--

-->
# '''MP'''(''P⁰→Q⁰'') remplace le but ''B'' par les 2 buts
#:* ''P¹→B''
#:* ''P¹=P⁰→Q⁰''<!--

-->
# '''MP'''(''P⁰→Q⁰→R⁰'') remplace le but ''P¹→B'' par les 2 buts
#:* ''P²→(P¹→B)
#:* ''P²=P⁰→Q⁰→R⁰<!--

-->
# '''S''' démontre ''P²→(P¹→B)'' car
#:* ''P²→(P¹→B) = (P⁰→Q⁰→R⁰)→(P⁰→Q⁰)→(P⁰→R⁰)''<!--

-->
# '''MP'''(''Q⁰→R⁰'') remplace le but ''P²'' par les 2 buts
#:* ''P³→P²''
#:* ''P³=Q⁰→R⁰''<!--

-->
# '''K''' démontre ''P³→P²'' car
#:* ''P³→P² = (Q⁰→R⁰)→P⁰→(Q⁰→R⁰)''<!--

-->
# '''S''' démontre ''P³'' car
#:* ''P³ =(R→P→Q)→(R→P)→(R→Q)''<!--

-->
# '''K''' démontre ''P¹'' car
#:* ''P¹=P⁰→Q⁰=(P→Q)→R→(P→Q)''.

<syntaxhighlight lang="ocaml">
(*
demonstration à l'aide de Rocq du syllogisme Barbara
par la logique propositionnelle a la Hilbert
*)
Section Logique_propositionnelle_a_la_Hilbert.
Variable P Q R : Prop.
(* le modus ponens *)
Ltac MP := fun P => match goal with
                      |- ?G => assert(TMP: P->G); [  | apply TMP;clear TMP]
                      end.
Ltac K := match goal with
           | |- (?P -> ?Q -> ?P) => tauto
           | |- _ => fail
          end.
Ltac S := match goal with
           | |- (?P -> ?Q -> ?R)->(?P->?Q)->?P->?R => tauto
           | |- _ => fail
          end.

(* syllogisme Barbara. *)
Theorem B : (P->Q)->(R->P)->(R->Q).
MP((P->Q)->(R->P->Q)).
MP((P->Q)->(R->P->Q)->((R->P)->(R->Q))).
S.
MP((R->P->Q)->((R->P)->(R->Q))).
K.
S.
K.
Qed.
End Logique_propositionnelle_a_la_Hilbert.
</syntaxhighlight>
{{démonstration/fin}}

== Correspondance avec le λ-calcul ==
{{Source de la section|de {{Référence Harvard sans parenthèses|Henk Barendregt|1984|p=156-162}}}}
Toute expression de la logique combinatoire admet une expression du λ-calcul équivalente, et toute expression du λ-calcul admet une expression de la logique combinatoire équivalente.
=== De la logique combinatoire vers le λ-calcul ===
Notons <math>[\![-]\!]_{\lambda}</math> la traduction des combinateurs vers le λ-calcul, elle est définie par :
* si <math>x</math> désigne une variable, <math>[\![x]\!]_{\lambda}=x</math> ;
* <math> [\![\mathsf{K}]\!]_{\lambda}=\lambda x.\lambda y.x</math> ;
* <math> [\![\mathsf{S}]\!]_{\lambda}=\lambda x.\lambda y.\lambda z.x z (y z)</math> ;
* <math> [\![M\,N]\!]_{\lambda}=[\![M]\!]_{\lambda}\,[\![N]\!]_{\lambda}</math>, pour tous combinateurs <math>M</math> et <math>N</math>.
Cette traduction est compatible avec la [[Lambda-calcul#Réductions|<math>\beta</math>-équivalence]], c'est-à-dire que si <math>M = N</math>, alors <math>[\![M]\!]_{\lambda} =_{\beta} [\![N]\!]_{\lambda}</math>.

=== Abstraction en logique combinatoire ===
Avant de définir la représentation du λ-calcul en logique combinatoire nous avons besoin de définir une abstraction dans la logique combinatoire <ref>{{ouvrage
| titre = Lambda-Calculu and Combinators an Introduction
| auteur1 = J. Roger Hindley
| auteur2 = Jonathan P. Seldin
| éditeur = Cambrdige University Press
| année = 2008
| lire en ligne = http://pds14.egloos.com/pds/200901/16/93/Lambda-Calculus_and_Combinators.pdf
}} Section 2C p. 26.</ref>. Si <math>M</math> est un terme, on définit <math>[x].M</math> qui va jouer le rôle de <math>\lambda x. M</math>.
::<math>
\begin{array}{llcl}
(a)&{[}x].M &=& \mathsf{K} M \qquad \textrm{si} ~ x\notin FV(M)\\
(b)&{[}x].x&=& \mathsf{I}\\
(c)&{[}x].U x &=& U  \qquad \textrm{si} ~x\notin FV(U)\\
(d)&{[}x]. U V &=& \mathsf{S} ([x]. U) ([x]. V)  \qquad \textrm{si}~\textrm{ni}~ (a) ~\textrm{ni}~ (c) ~\textrm{ne}~ \textrm{s'appliquent}.
\end{array}
</math>

=== Du λ-calcul à la logique combinatoire ===
On définit l'interprétation des termes <math>M</math> du λ-calcul en termes <math>[\![M]\!]_{CL}</math> de la logique combinatoire:
::<math>
\begin{array}{rcl}
{[}\![x]\!]_{CL}&=& x\\
{[}\![M N]\!]_{CL}&=& [\![M]\!]_{CL} [\![N]\!]_{CL}\\
{[}\![\lambda x.M]\!]_{CL}&=& [x].[\![M]\!]_{CL}
\end{array}
</math>

Cette interprétation n'est pas compatible avec la <math>\beta</math>-équivalence : il existe des lambda-termes <math>M</math> et <math>N</math> tels que <math>M =_\beta N</math> et <math>[\![M]\!]_{CL} \neq [\![N]\!]_{CL}</math>, par exemple <math>[\![\mathsf{SK}]\!]_{\lambda}</math> et <math>[\![\mathsf{KI}]\!]_{\lambda}</math> :

<math display="block">[\![\mathsf{SK}]\!]_{\lambda}
= (\lambda x.\lambda y.\lambda z.x z (y z)) (\lambda t. \lambda u. t)
=_{\beta} \lambda y.\lambda z. z
=_{\beta} (\lambda x.\lambda y. x)(\lambda z. z)
= [\![\mathsf{KI}]\!]_{\lambda}</math>

Mais <math>[\![ [\![\mathsf{SK}]\!]_{\lambda} ]\!]_{CL} = \mathsf{SK}</math>, <math>[\![ [\![\mathsf{KI}]\!]_{\lambda} ]\!]_{CL} = \mathsf{KI}</math> et <math>\mathsf{SK} \neq \mathsf{KI}</math>.

=== Exemple ===

Le [[Lambda-calcul#Combinateur de point fixe|combinateur de point fixe]] de [[Alan Turing|Turing]], noté <math>\Theta</math> a pour expression en λ-calcul <math>(\lambda x.\lambda y.y\,(x\,x\,y))\,(\lambda x.\lambda y.y\,(x\,x\,y))</math>. On peut alors calculer :
::<math>
\begin{array}{rcl}
[\![\lambda y.y\,(x\,x\,y))]\!]_{CL} & = & [y].[\![y\,(x\,x\,y))]\!]_{CL}\\
&=& S([y].[\![y]\!]_{CL}) ([y].[\![x x y]\!]_{CL}) \\
&=& S I ([\![x x]\!]_{CL}) \\
&=& S I (x x)
\end{array}
</math>
puis
::<math>
\begin{array}{rcl}
[\![\lambda x . \lambda y.y\,(x\,x\,y))]\!]_{CL} & = & [x].[\![\lambda y . y\,(x\,x\,y))]\!]_{CL}\\
&=& [x] . S I (x x) \\
&=& S([x]. S I) ([x]. x x)\\
&=& S (K (S I)) (S ([x]. x) ([x]. x)\\
&=& S (K (S I)) (S I I)
\end{array}
</math>
On définit alors deux combinateurs '''A''' et '''Θ'''

'''A''':='''S (K (S I)) (S I I)'''

'''Θ''': ='''A A'''

'''Θ''' est un combinateur de point fixe.

On observe que, qu'il s'agisse du λ-terme ou de sa traduction en tant que combinateur, on a <math> \Theta x ~ \stackrel{*}{\longrightarrow} ~ x (\Theta x)</math>.

== Problèmes indécidables en logique combinatoire ==
Une [[Lambda-calcul#La normalisation : notions de calcul et de terme en forme normale|forme normale]] est un combinateur dans lequel aucune règle de réduction n'est applicable. Déterminer si un combinateur peut se réduire en combinateur en forme normale est indécidable. De même, déterminer si deux combinateurs distincts sont égaux est indécidable<ref>{{Référence Harvard sans parenthèses|Henk Barendregt|1984|p=164}}</ref>. Ces deux résultats sont à rapprocher de l'indécidabilité de l'équivalence de deux termes dans le lamda-calcul, ou de l'indécidabilité de l'existence d'une forme normale pour un terme donné<ref>{{Référence Harvard sans parenthèses|Henk Barendregt|1984|p=144-146}}</ref>.

== Références ==
{{Références|colonnes=}}

== Bibliographie ==
* {{Ouvrage|langue=en|auteur1=[[Haskell Curry]]|auteur2=[[Robert Feys]]|titre=Combinatory Logic|volume=1|éditeur=[[North-Holland]]|collection=Studies in Logic and the Foundations of Mathematics|année=1958|isbn=9780720422085}}. La plupart du contenu de cet ouvrage fut rendu obsolète par l'ouvrage de 1972 et les suivants.
* {{Ouvrage|langue=en|auteur1=[[Haskell Curry]]|auteur2=J. Roger Hindley|auteur3=J. P. Seldin|titre=Combinatory Logic|volume=2|éditeur=[[North-Holland]]|collection=Studies in Logic and the Foundations of Mathematics|année=1972|isbn=9780720422085}}. Une rétrospective complète de la logique combinatoire, incluant une approche chronologique.
* {{ouvrage
| titre = Lambda-Calculus and Combinators
|sous-titre=An Introduction|langue=en| auteur1 = J. Roger Hindley
| auteur2 = J. P. Seldin
| éditeur = [[Cambridge University Press]]
| année = 2008
|numéro édition=2|isbn=9780521898850| lire en ligne = 
}}.
* {{Ouvrage|auteur1=Jean-Pierre Desclés|auteur2=Gaëll Guibert|auteur3=Benoît Sauzay|titre=Logique combinatoire et lambda-calcul : des logiques d'opérateurs|éditeur=[[Éditions Cépaduès]]|année=2016|isbn=9782364935303}}.
* {{Ouvrage|auteur1=Desclés Jean-Pierre|auteur2=Guibert Gaëll|auteur3=Sauzay Benoît|titre=Calculs de signification par une logique d'opérateurs|éditeur=[[Éditions Cépaduès]]|année=2016|isbn=9782364935754}}.
* {{Ouvrage|auteur1=[[Jean-Pierre Ginisti]]|titre=La logique combinatoire|lieu=Paris|éditeur=[[PUF]]|collection=Que sais-je ?|numéro dans collection=3205|année=1997|pages totales=127|passage=|isbn=9782130480105|présentation en ligne=https://doi.org/10.7202/004928ar}}.
* {{Chapitre|langue=en|auteur1=[[Moses Schönfinkel]]|titre chapitre=On the building blocks of mathematical logic.|auteurs ouvrage=[[Jean van Heijenoort]]|titre ouvrage=From Frege to Gödel|sous-titre ouvrage=A Source Book in Mathematical Logic, 1879–1931|éditeur=[[Harvard University Press]]|année=1967|passage=355-366|isbn=9780674324497|lire en ligne=https://archive.org/details/fromfregetogodel0000vanh/page/n679/mode/2up}}.
* {{Ouvrage|langue=fr|prénom1=Jean-Louis|nom1=Krivine|titre=Lambda-calcul: types et modèles|éditeur=Masson|date=1990|isbn=978-2-225-82091-5|lire en ligne=https://www.irif.fr/~krivine/articles/Lambda.pdf}}.
* {{Article|auteur1=[[Robert Feys]]|prénom1=|nom1=|titre=La technique de la logique combinatoire|périodique=[[Revue philosophique de Louvain]]|série=Troisième série|volume=44|numéro=1|pages=74–103|date=1946|doi=10.3406/phlou.1946.4039|lire en ligne=https://www.persee.fr/doc/phlou_0035-3841_1946_num_44_1_4039}}.
* {{Ouvrage|langue=en|auteur1=[[Henk Barendregt]]|titre=The Lambda Calculus|sous-titre=Its Syntax and Semantics|lieu=Amsterdam|éditeur=[[North-Holland]]|collection=Studies in Logic and the Foundations of Mathematics|numéro dans collection=103|année=1984|pages totales=621|isbn=978-0-444-87508-2|lire en ligne=https://www.sciencedirect.com/bookseries/studies-in-logic-and-the-foundations-of-mathematics/vol/103/|plume=oui}}
== Liens externes ==

* {{Autorité}}

{{Portail|mathématiques|logique}}

[[Catégorie:Logique mathématique]]
[[Catégorie:Théorie des types]]
[[Catégorie:Théorie de la démonstration]]
[[Catégorie:Informatique théorique]]
[[Catégorie:Calculabilité]]