Content deleted Content added
m →Compilation of functional languages: clean up |
m Brought all references to the alphabetical list and referenced them inline by {{sfn}} and {{harvtxt}}; removed redundant spaces and line feeds; |
||
Line 2:
{{distinguish|text=[[combinational logic]], a topic in digital electronics}}
'''Combinatory logic''' is a notation to eliminate the need for [[Quantifier (logic)|quantified]] variables in [[mathematical logic]]. It was introduced by [[Moses Schönfinkel]]
==In mathematics==
Combinatory logic was originally intended as a 'pre-logic' that would clarify the role of [[quantifier (logic)|quantified variables]] in logic, essentially by eliminating them. Another way of eliminating quantified variables is [[Willard Van Orman Quine|Quine's]] [[predicate functor logic]]. While the [[expressive power (computer science)|expressive power]] of combinatory logic typically exceeds that of [[first-order logic]], the expressive power of [[predicate functor logic]] is identical to that of first order logic ([[#Quine 1960 1966|Quine 1960, 1966, 1976]]).
The original inventor of combinatory logic, [[Moses Schönfinkel]], published nothing on combinatory logic after his original 1924 paper. [[Haskell Curry]] rediscovered the combinators while working as an instructor at [[Princeton University]] in late 1927.
==In computing==
Line 15 ⟶ 14:
Combinatory logic can be viewed as a variant of the [[lambda calculus]], in which lambda expressions (representing functional abstraction) are replaced by a limited set of ''combinators'', primitive functions without [[free variables and bound variables|free variable]]s. It is easy to transform lambda expressions into combinator expressions, and combinator reduction is much simpler than lambda reduction. Hence combinatory logic has been used to model some [[non-strict programming language|non-strict]] [[functional programming]] languages and [[graph reduction machine|hardware]]. The purest form of this view is the programming language [[Unlambda]], whose sole primitives are the S and K combinators augmented with character input/output. Although not a practical programming language, Unlambda is of some theoretical interest.
Combinatory logic can be given a variety of interpretations. Many early papers by Curry showed how to translate axiom sets for conventional logic into combinatory logic equations
== Summary of lambda calculus ==
{{main|Lambda calculus}}
Lambda calculus is concerned with objects called ''lambda-terms'', which can be represented by the following three forms of strings:
* {{tmath|v}}
Line 27 ⟶ 25:
* {{tmath|(E_1 E_2)}}
where {{tmath|v}} is a variable name drawn from a predefined infinite set of variable names, and {{tmath|E_1}} and {{tmath|E_2}} are lambda-terms.
Terms of the form {{tmath|\lambda v.E_1}} are called ''abstractions''. The variable ''v'' is called the [[formal parameter]] of the abstraction, and {{tmath|E_1}} is the ''body'' of the abstraction. The term {{tmath|\lambda v.E_1}} represents the function which, applied to an argument, binds the formal parameter ''v'' to the argument and then computes the resulting value of {{tmath|E_1}}— that is, it returns {{tmath|E_1}}, with every occurrence of ''v'' replaced by the argument.
Terms of the form {{tmath|(E_1 E_2)}} are called ''applications''. Applications model function invocation or execution: the function represented by {{tmath|E_1}} is to be invoked, with {{tmath|E_2}} as its argument, and the result is computed. If {{tmath|E_1}} (sometimes called the ''applicand'') is an abstraction, the term may be ''reduced'': {{tmath|E_2}}, the argument, may be substituted into the body of {{tmath|E_1}} in place of the formal parameter of {{tmath|E_1}}, and the result is a new lambda term which is ''equivalent'' to the old one. If a lambda term contains no subterms of the form {{tmath|((\lambda v.E_1) E_2)}} then it cannot be reduced, and is said to be in [[Beta normal form|normal form]].
The expression {{tmath|E[v :{{=}} a]}}
:{{tmath|((\lambda v.E) a) \Rightarrow E[v :{{=}} a]}}
Line 53 ⟶ 37:
By convention, we take {{tmath|(a b c)}} as shorthand for {{tmath|((a b) c)}} (i.e., application is [[Associative#Non-associativity|left associative]]).
The motivation for this definition of reduction is that it captures the essential behavior of all mathematical functions. For example, consider the function that computes the square of a number. We might write
:The square of ''x'' is {{tmath|x*x}}
(Using "{{tmath|*}}" to indicate multiplication.) ''x'' here is the [[formal parameter]] of the function. To evaluate the square for a particular argument, say 3, we insert it into the definition in place of the formal parameter:
:The square of 3 is {{tmath|3*3}}
To evaluate the resulting expression {{tmath|3*3}}, we would have to resort to our knowledge of multiplication and the number 3. Since any computation is simply a composition of the evaluation of suitable functions on suitable primitive arguments, this simple substitution principle suffices to capture the essential mechanism of computation.
Moreover, in lambda calculus, notions such as '3' and '{{tmath|*}}' can be represented without any need for externally defined primitive operators or constants. It is possible to identify terms in lambda calculus, which, when suitably interpreted, behave like the number 3 and like the multiplication operator, q.v. [[Church encoding]].
Lambda calculus is known to be computationally equivalent in power to many other plausible models for computation (including [[Turing machine]]s); that is, any calculation that can be accomplished in any of these other models can be expressed in lambda calculus, and vice versa. According to the [[Church-Turing thesis]], both models can express any possible computation.
It is perhaps surprising that lambda-calculus can represent any conceivable computation using only the simple notions of function abstraction and application based on simple textual substitution of terms for variables. But even more remarkable is that abstraction is not even required. ''Combinatory logic'' is a model of computation equivalent to lambda calculus, but without abstraction. The advantage of this is that evaluating expressions in lambda calculus is quite complicated because the semantics of substitution must be specified with great care to avoid variable capture problems. In contrast, evaluating expressions in combinatory logic is much simpler, because there is no notion of substitution.
== Combinatory calculi ==
Since abstraction is the only way to manufacture functions in the lambda calculus, something must replace it in the combinatory calculus. Instead of abstraction, combinatory calculus provides a limited set of primitive functions out of which other functions may be built.
=== Combinatory terms ===
Line 116 ⟶ 71:
|}
The primitive functions are ''combinators'', or functions that, when seen as lambda terms, contain no [[free variable|free variables]]
To shorten the notations, a general convention is that {{tmath|(E_1 E_2 E_3 ... E_n)}}, or even {{tmath|E_1 E_2 E_3... E_n}}, denotes the term {{tmath|(...((E_1 E_2) E_3)... E_n)}}. This is the same general convention (left-associativity) as for multiple application in lambda calculus.
Line 130 ⟶ 85:
=== Examples of combinators ===
The simplest example of a combinator is '''I''', the identity combinator, defined by
:('''I''' ''x'') = ''x''
for all terms ''x''. Another simple combinator is '''K''', which manufactures constant functions: ('''K''' ''x'') is the function which, for any argument, returns ''x'', so we say
:(('''K''' ''x'') ''y'') = ''x''
for all terms ''x'' and ''y''. Or, following the convention for multiple application,
:('''K''' ''x'' ''y'') = ''x''
A third combinator is '''S''', which is a generalized version of application:
:('''S''' ''x y z'') = (''x z'' (''y z''))
'''S''' applies ''x'' to ''y'' after first substituting ''z'' into
each of them. Or put another way, ''x'' is applied to ''y'' inside the environment ''z''.
Given '''S''' and '''K''', '''I''' itself is unnecessary, since it can be built from the other two:
:(('''S K K''') ''x'')
Line 165 ⟶ 113:
for any term ''x''. Note that although (('''S K K''')
''x'') = ('''I''' ''x'') for any ''x'', ('''S K K''')
itself is not equal to '''I'''. We say the terms are [[extensional equality|extensionally equal]]. Extensional equality captures the mathematical notion of the equality of functions: that two functions are ''equal'' if they always produce the same results for the same arguments. In contrast, the terms themselves, together with the reduction of primitive combinators, capture the notion of ''intensional equality'' of functions: that two functions are ''equal'' only if they have identical implementations [[up to]] the expansion of primitive combinators. There are many ways to implement an identity function; ('''S K K''') and '''I''' are among these ways. ('''S K S''') is yet another. We will use the word ''equivalent'' to indicate extensional equality, reserving ''equal'' for identical combinatorial terms.
A more interesting combinator is the [[fixed point combinator]] or '''Y''' combinator, which can be used to implement [[recursion]].
Line 182 ⟶ 119:
=== Completeness of the S-K basis ===
'''S''' and '''K''' can be composed to produce combinators that are extensionally equal to ''any'' lambda term, and therefore, by Church's thesis, to any computable function whatsoever.
''T''[ ] may be defined as follows:
Line 197 ⟶ 134:
This process is also known as ''abstraction elimination''. This definition is exhaustive: any lambda expression will be subject to exactly one of these rules (see [[Combinatory logic#Summary of lambda calculus|Summary of lambda calculus]] above).
It is related to the process of ''bracket abstraction'', which takes an expression ''E'' built from variables and application and produces a combinator expression [x]E in which the variable x is not free, such that [''x'']''E x'' = ''E'' holds. A very simple algorithm for bracket abstraction is defined by induction on the structure of expressions as follows:{{sfn|Turner|1979}}
# [''x'']''y'' := '''K''' ''y''
# [''x'']''x'' := '''I'''
Line 206 ⟶ 142:
==== Conversion of a lambda term to an equivalent combinatorial term ====
For example, we will convert the lambda term ''λx''.''λy''.(''y'' ''x'') to a combinatorial term:
:''T''[''λx''.''λy''.(''y'' ''x'')]
Line 221 ⟶ 156:
:: = ('''S''' ('''K''' ('''S I''')) ('''S''' ('''K K''') '''I''')) (by 4)
If we apply this combinatorial term to any two terms ''x'' and ''y'' (by feeding them in a queue-like fashion into the combinator 'from the right'), it reduces as follows:
: ('''S''' ('''K''' ('''S''' '''I''')) ('''S''' ('''K''' '''K''') '''I''') x y)
Line 234 ⟶ 168:
:: = (y x)
The combinatory representation, ('''S''' ('''K''' ('''S I''')) ('''S''' ('''K K''') '''I''')) is much longer than the representation as a lambda term, ''λx''.''λy''.(y x). This is typical. In general, the ''T''[ ] construction may expand a lambda term of length ''n'' to a combinatorial term of length [[Big O notation|Θ]](''n''<sup>3</sup>).{{sfn|Lachowski |2018}}
==== Explanation of the ''T''[ ] transformation ====
The ''T''[ ] transformation is motivated by a desire to eliminate abstraction. Two special cases, rules 3 and 4, are trivial: ''λx''.''x'' is clearly equivalent to '''I''', and ''λx''.''E'' is clearly equivalent to ('''K''' ''T''[''E'']) if ''x'' does not appear free in ''E''.
The first two rules are also simple: Variables convert to themselves,and applications, which are allowed in combinatory terms, are converted to combinators simply by converting the applicand and the argument to combinators.
It is rules 5 and 6 that are of interest. Rule 5 simply says that to convert a complex abstraction to a combinator, we must first convert its body to a combinator, and then eliminate the abstraction. Rule 6 actually eliminates the abstraction.
''λx''.(''E''₁ ''E''₂) is a function which takes an argument, say ''a'', and substitutes it into the lambda term (''E''₁ ''E''₂) in place of ''x'', yielding (''E''₁ ''E''₂)[''x'' : = ''a'']. But substituting ''a'' into (''E''₁ ''E''₂) in place of ''x'' is just the same as substituting it into both ''E''₁ and ''E''₂, so
:
:
:::::
:::::
By extensional equality,
:
Therefore, to find a combinator equivalent to ''λx''.(''E''₁ ''E''₂), it is sufficient to find a combinator equivalent to ('''S''' ''λx''.''E''₁ ''λx''.''E''₂), and
:
evidently fits the bill. ''E''₁ and ''E''₂ each contain strictly fewer applications than (''E''₁ ''E''₂), so the recursion must terminate in a lambda term with no applications at all—either a variable, or a term of the
form ''λx''.''E''.
Line 281 ⟶ 201:
==== η-reduction ====
The combinators generated by the ''T''[ ] transformation can be made smaller if we take into account the ''η-reduction'' rule:
:
''λx''.(''E'' x) is the function which takes an argument, ''x'', and applies the function ''E'' to it; this is extensionally equal to the function ''E'' itself. It is therefore sufficient to convert ''E'' to combinatorial form.
Taking this simplification into account, the example above becomes:
:
:
:
:
This combinator is equivalent to the earlier, longer one:
:
:
:
:
:
:
Similarly, the original version of the ''T''[ ] transformation transformed the identity function ''λf''.''λx''.(''f'' ''x'') into ('''S''' ('''S''' ('''K S''') ('''S''' ('''K K''') '''I''')) ('''K I''')). With the η-reduction rule, ''λf''.''λx''.(''f'' ''x'') is
transformed into '''I'''.
Line 315 ⟶ 230:
There are one-point bases from which every combinator can be composed extensionally equal to ''any'' lambda term. The simplest example of such a basis is {'''X'''} where:
:
It is not difficult to verify that:
:
:
Since {'''K''', '''S'''} is a basis, it follows that {'''X'''} is a basis too. The [[Iota and Jot|Iota]] programming language uses '''X''' as its sole combinator.
Line 325 ⟶ 240:
Another simple example of a one-point basis is:
:
:
:
In fact, there exist infinitely many such bases.
==== Combinators B, C ====
In addition to '''S''' and '''K''',
:
:
He also explains how they in turn can be expressed using only '''S''' and '''K''':
:
:
These combinators are extremely useful when translating predicate logic or lambda calculus into combinator expressions. They were also used by [[Haskell Curry|Curry]], and much later by [[David Turner (computer scientist)|David Turner]], whose name has been associated with their computational use. Using them, we can extend the rules for the transformation as follows:
#
#
#
#
#
#
#
#
Using '''B''' and '''C''' combinators, the transformation of ''λx''.''λy''.(''y'' ''x'') looks like this:
:
:
:
:
:
:
:
And indeed, ('''C''' '''I''' ''x'' ''y'') does reduce to (''y'' ''x''):
:
:
:
The motivation here is that '''B''' and '''C''' are limited versions of '''S'''. Whereas '''S''' takes a value and substitutes it into both the applicand and its argument before performing the application, '''C''' performs the
substitution only in the applicand, and '''B''' only in the argument.
The modern names for the combinators come from [[Haskell Curry]]'s doctoral thesis of 1930 (see [[B, C, K, W System]]). In [[Moses Schönfinkel|Schönfinkel]]'s original paper, what we now call '''S''', '''K''', '''I''', '''B''' and '''C''' were called '''S''', '''C''', '''I''', '''Z''', and '''T''' respectively.
The reduction in combinator size that results from the new transformation rules can also be achieved without introducing '''B''' and '''C''', as demonstrated in Section 3.2 of {{harvtxt|Tromp|2008}}.
===== CL<sub>K</sub> versus CL<sub>I</sub> calculus =====
Line 389 ⟶ 299:
=== Reverse conversion ===
The conversion ''L''[ ] from combinatorial terms to lambda terms is trivial:
:
:
:
:
:
:
Note, however, that this transformation is not the inverse
Line 408 ⟶ 317:
First, the term
:
has no normal form, because it reduces to itself after three steps, as follows:
:
:
:
:
and clearly no other reduction order can make the expression shorter.
Now, suppose '''N''' were a combinator for detecting normal forms, such that
:<math>(\mathbf{N} \ x) = \begin{cases} \mathbf{T}, \text{ if } x \text{ has a normal form} \\
Line 428 ⟶ 335:
Now let
:
now consider the term ('''S''' '''I''' '''I''' ''Z''). Does ('''S''' '''I''' '''I''' ''Z'') have a normal
form?
:{{spaces|2}}
:
:
:
:
:
:
:
Now we need to apply '''N''' to ('''S''' '''I''' '''I''' ''Z'').
Either ('''S''' '''I''' '''I''' ''Z'') has a normal form, or it does not. If it ''does'' have a normal form, then the foregoing reduces as follows:
:{{spaces|2}}
:
:
but '''Ω''' does ''not'' have a normal form, so we have a contradiction. But
if ('''S''' '''I''' '''I''' ''Z'') does ''not'' have a normal form, the foregoing reduces as follows:
:{{spaces|2}}
:
:
:
which means that the normal form of ('''S''' '''I''' '''I''' ''Z'') is simply '''I''', another
contradiction. Therefore, the hypothetical normal-form combinator '''N''' cannot exist.
The combinatory logic analogue of [[Rice's theorem]] says that there is no complete nontrivial predicate. A ''predicate'' is a combinator that, when applied, returns either '''T''' or '''F'''.
{{math proof
| proof = By reductio ad absurdum. Suppose there is a complete non trivial predicate, say '''N'''. Because '''N''' is supposed to be non trivial there are combinators ''A'' and ''B'' such that
Line 492 ⟶ 396:
David Turner used his combinators to implement the [[SASL programming language]].
[[Kenneth E. Iverson]] used primitives based on Curry's combinators in his [[J programming language]], a successor to [[APL (programming language)|APL]]. This enabled what Iverson called [[tacit programming]], that is, programming in functional expressions containing no variables, along with powerful tools for working with such programs. It turns out that tacit programming is possible in any APL-like language with user-defined operators.
=== Logic ===
Line 534 ⟶ 426:
== References ==
{{reflist|2}}
==
*
*{{cite book|first=Edward |last=Cherlin |title=Proceedings of the international conference on APL '91 - APL '91 |chapter=Pure functions in APL and J |pages=88–93 |year=1991 |doi=10.1145/114054.114065|isbn=0897914414 |s2cid=25802202 }}
*{{cite journal|last=Curry|first=Haskell Brooks|title=Grundlagen der Kombinatorischen Logik|journal=American Journal of Mathematics|year=1930|volume=52|issue=3|pages=509–536|author-link=Haskell Curry|trans-title=Foundations of combinatorial logic|publisher=The Johns Hopkins University Press|language=de|doi=10.2307/2370619|jstor=2370619}}
*
*
*
*{{cite journal | first=Mayer | last=Goldberg | doi=10.1016/j.ipl.2003.12.005 | volume=89 | issue=6 | year=2004 | title=A construction of one-point bases in extended lambda calculi | journal=Information Processing Letters | pages=281–286}}
*{{cite journal| last1=Hindley|first1=J. Roger|author-link1=J. Roger Hindley|last2=Meredith|first2=David|title=Principal type-schemes and condensed detachment|url=http://projecteuclid.org/euclid.jsl/1183743187|mr=1043546|journal=[[Journal of Symbolic Logic]]|volume = 55|issue=1|pages=90–105|year=1990|doi=10.2307/2274956|jstor=2274956|s2cid=6930576}}
*{{cite book |last1=Hindley |first1=J. R. |author-link1=J. Roger Hindley |last2=Seldin |first2=J. P. |year=2008 |url=http://www.cambridge.org/catalogue/catalogue.asp?isbn=9780521898850 |title=λ-calculus and Combinators: An Introduction |publisher=[[Cambridge University Press]]}}
*{{cite journal |last=Lachowski |first=Łukasz |title=On the Complexity of the Standard Translation of Lambda Calculus into Combinatory Logic |journal=Reports on Mathematical Logic |date=2018 |volume=2018 |issue=53 |pages=19–42 |doi=10.4467/20842589RM.18.002.8835 |url=http://www.ejournals.eu/rml/2018/Number-53/art/12285 |access-date=9 September 2018|doi-access=free}}
* {{cite book |last=Paulson |first=Lawrence C. |author-link=Lawrence Paulson |year=1995 |url=http://www.cl.cam.ac.uk/Teaching/Lectures/founds-fp/Founds-FP.ps.gz |title=Foundations of Functional Programming |publisher=University of Cambridge}}
*
*{{cite book |author-link=Willard Van Orman Quine |last=Quine |first=W. V.|year=1996|orig-date=1960|chapter=Variables explained away|title=Selected Logic Papers|publisher=[[Harvard University Press]]|location=Cambridge, Mass.|pages=227–235|isbn=9780674798373|edition=Enl. ed., 2. print}}
*{{cite journal |first=Moses |last=Schönfinkel |author-link=Moses Schönfinkel |year=1924 |url=http://www.cip.ifi.lmu.de/~langeh/test/1924%20-%20Schoenfinkel%20-%20Ueber%20die%20Bausteine%20der%20mathematischen%20Logik.pdf |title=Über die Bausteine der mathematischen Logik |journal=Mathematische Annalen |volume=92 |issue=3–4 |pages=305–316 |doi=10.1007/bf01448013|s2cid=118507515|language=de|quote=The article that founded combinatory logic. English translation: {{harvtxt|Schönfinkel|1967}}}}
*{{cite book |first=Moses|last=Schönfinkel|author-link=Moses Schönfinkel|orig-year=1924|translator-first=Stefan|translator-last=Bauer-Mengelberg|title=Über die Bausteine der mathematischen Logik|trans-title=On the building blocks of mathematical logic|editor-first= Jean|editor-last=Van Heijenoort|editor-link=Jean van Heijenoort|year=1967|series=From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931|publisher=[[Harvard University Press]]| location=Cambridge, MA, USA|language=en|pages=355-366|isbn=978-0674324497|oclc=503886453}}
*{{cite web|last=Seldin|first=Jonathan P.|title=The Logic of Curry and Church|date=3 March 2008|url=http://people.uleth.ca/%7Ejonathan.seldin/CCL.pdf|access-date=17 September 2023}}
* [[Raymond Smullyan|Smullyan, Raymond]], 1985. ''[[To Mock a Mockingbird]]''. Knopf. {{ISBN|0-394-53491-3}}. A gentle introduction to combinatory logic, presented as a series of recreational puzzles using bird watching metaphors.
* ______, 1994. ''Diagonalization and Self-Reference''. [[Oxford University Press]]. Chapters 17–20 are a more formal introduction to combinatory logic, with a special emphasis on fixed point results.
* Sørensen, Morten Heine B. and Paweł Urzyczyn, 1999. ''[https://web.archive.org/web/20051016213140/http://folli.loria.fr/cds/1999/library/pdf/curry-howard.pdf Lectures on the Curry–Howard Isomorphism]''. [[University of Copenhagen]] and [[University of Warsaw]], 1999.
*{{cite book |first=John |last=Tromp |chapter=Binary Lambda Calculus and Combinatory Logic |title=Randomness And Complexity, from Leibniz To Chaitin |editor-first=Cristian S. |editor-last=Calude |publisher=World Scientific Publishing Company |year=2008 |chapter-url=http://tromp.github.io/cl/LC.pdf|archive-url=https://web.archive.org/web/20160304083208/http://tromp.github.io/cl/LC.pdf |archive-date=2016-03-04}}
*{{cite journal|last=Turner|first=David A.|author-link=David Turner (computer scientist)|title=Another Algorithm for Bracket Abstraction|journal=The Journal of Symbolic Logic|volume=44|issue=2|pages=267–270|year=1979|doi=10.2307/2273733|jstor=2273733|s2cid=35835482}}
* {{cite book |last=Wolfengagen |first=V. E. |url=https://archive.org/details/CLP-2003_780 |title=Combinatory logic in programming: Computations with objects through examples and exercises |edition=2nd |location=Moscow |publisher="Center JurInfoR" Ltd. |year=2003 |isbn=5-89158-101-9}}
* {{cite book| last=Wolfram | first=Stephen | authorlink=Stephen Wolfram | url=https://www.wolfram-media.com/products/combinators-a-centennial-view.html |title= Combinators: A Centennial View | publisher=[[Wolfram Media]] | year=2021 | isbn=978-1-57955-043-1 }} e{{ISBN|978-1-57955-044-8}}. A celebration of the development of combinators, a hundred years after they were introduced by [[Moses Schönfinkel]] in 1920.
| |||