[go: nahoru, domu]
Wikipedia

Combinatory logic: Difference between revisions

Browse history interactively
← Previous edit
Content deleted Content added
VisualWikitext
Undid revision 1198945212 by EmilJ (talk)
Tags: Undo Reverted
m Reverted edits by 91.242.213.233 (talk): not providing a reliable source (WP:CITE, WP:RS) (HG) (3.4.12)
 
(16 intermediate revisions by 10 users not shown)
Line 48:
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-TuringChurch–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.
Line 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. The proof is to present a transformation, {{math|''T''[ ]}}, which converts an arbitrary lambda term into an equivalent combinator.
 
{{math|''T''[ ]}} may be defined as follows:
 
# {{math| ''T''[''x''] =>⇒ ''x''}}
# {{math| ''T''[(''E''₁ ''E''₂)] =>⇒ (''T''[''E''₁] ''T''[''E''₂])}}
# {{math| ''T''[''λx''.''E''] =>⇒ ('''K''' ''T''[''E''])}} (if ''x'' does not occur free in ''E'')
# {{math| ''T''[''λx''.''x''] =>⇒ '''I'''}}
# {{math| ''T''[''λx''.''λy''.''E''] =>⇒ ''T''{{!(}}''λx''.''T''{{!(}}''λy''.''E''{{))!}}}} (if ''x'' occurs free in ''E'')
# {{math| ''T''[''λx''.(''E''₁ ''E''₂)] =>⇒ ('''S''' ''T''[''λx''.''E''₁] ''T''[''λx''.''E₂''])}} (if ''x'' occurs free in ''E''₁ or ''E''₂)
 
Note that ''T''[ ] as given is not a well-typed mathematical function, but rather a term rewriter: Although it eventually yields a combinator, the transformation may generate intermediary expressions that are neither lambda terms nor combinators, via rule (5).
Line 260:
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:
 
#{{math|''T''[''x''] ⇒ ''x''}}
#{{math|''T''[(''E₁'' ''E₂'')] ⇒ (''T''[''E₁''] ''T''[''E₂''])}}
#{{math|''T''[''λx''.''E''] ⇒ ('''K''' ''T''[''E''])}} (if ''x'' is not free in ''E'')
#{{math|''T''[''λx''.''x''] ⇒ '''I'''}}
#{{math|''T''[''λx''.''λy''.''E''] ⇒ ''T''{{!(}}''λx''.''T''{{!(}}''λy''.''E''{{))!}}}} (if ''x'' is free in ''E'')
#{{math|''T''[''λx''.(''E₁'' ''E₂'')] ⇒ ('''S''' ''T''[''λx''.''E₁''] ''T''[''λx''.''E₂''])}} (if ''x'' is free in both ''E₁'' and ''E₂'')
#{{math|''T''[''λx''.(''E₁'' ''E₂'')] ⇒ ('''C''' ''T''[''λx''.''E₁''] ''T''[''E₂''])}} (if ''x'' is free in ''E₁'' but not ''E₂'')
#{{math|''T''[''λx''.(''E₁'' ''E₂'')] ⇒ ('''B''' ''T''[''E₁''] ''T''[''λx''.''E₂''])}} (if ''x'' is free in ''E₂'' but not ''E₁'')
 
Using '''B''' and '''C''' combinators, the transformation of ''λx''.''λy''.(''y'' ''x'') looks like this:
 
:{{spaces|2}}{{math|1=''T''[''λx''.''λy''.(''y'' ''x'')]}}
:{{math|1== ''T''{{!(}}''λx''.''T''{{!(}}''λy''.(''y'' ''x''){{))!}}}}
:{{math|1== ''T''[''λx''.('''C''' ''T''[''λy''.''y''] ''x'')]}} (by rule 7)
:{{math|1== ''T''[''λx''.('''C''' '''I''' ''x'')]}}
:{{math|1== ('''C''' '''I''')}} (η-reduction)
:= <math>= \mathbf{C}_{*}</math> (traditional canonical notation: <math>\mathbf{X}_{*} = \mathbf{X I}</math>)
:= <math>= \mathbf{I}'</math> (traditional canonical notation: <math>\mathbf{X}' = \mathbf{C X}</math>)
 
And indeed, ('''C''' '''I''' ''x'' ''y'') does reduce to (''y'' ''x''):
Line 313:
== Undecidability of combinatorial calculus ==
 
A [[normal form (abstract rewriting)|normal form]] is any combinatory term in which the primitive combinators that occur, if any, are not applied to enough arguments to be simplified. It is undecidable whether a general combinatory term has a normal form; whether two combinatory terms are equivalent, etc. This iscan equivalentbe toshown thein undecidabilitya ofsimilar way as for the corresponding problems for lambda terms. However, a direct proof is as follows:
 
=== Undefinability by predicates ===
First, the term
The undecidable problems above (equivalence, existence of normal form, etc.) take as input syntactic representations of terms under a suitable encoding (e.g., Church encoding). One may also consider a toy trivial computation model where we "compute" properties of terms by means of combinators applied directly to the terms themselves as arguments, rather than to their syntactic representations. More precisely, let a ''predicate'' be a combinator that, when applied, returns either '''T''' or '''F''' (where {{math|'''T'''}} and {{math|'''F'''}} represent the conventional [[Church encoding]]s of true and false, ''λx''.''λy''.''x'' and ''λx''.''λy''.''y'', transformed into combinatory logic; the combinatory versions have {{math|1='''T''' = '''K'''}} and {{math|1='''F''' = ('''K''' '''I''')}}). A predicate '''N''' is ''nontrivial'' if there are two arguments ''A'' and ''B'' such that '''N''' ''A'' = '''T''' and '''N''' ''B'' = '''F'''. A combinator '''N''' is ''complete'' if '''N'''''M'' has a normal form for every argument ''M''. An analogue of Rice's theorem for this toy model then says that every complete predicate is trivial. The proof of this theorem is rather simple.{{sfn|Engeler|1995}}
 
:'''Ω''' = ('''S''' '''I''' '''I''' ('''S''' '''I''' '''I'''))
 
has no normal form, because it reduces to itself after three steps, as follows:
 
:('''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'''))
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} \\
\mathbf{F}, \text{ otherwise.} \end{cases}</math>
:(Where {{math|'''T'''}} and {{math|'''F'''}} represent the conventional [[Church encoding]]s of true and false, ''λx''.''λy''.''x'' and ''λx''.''λy''.''y'', transformed into combinatory logic. The combinatory versions have {{math|1='''T''' = '''K'''}} and {{math|1='''F''' = ('''K''' '''I''')}}.)
 
Now let
 
:''Z'' = ('''C''' ('''C''' ('''B''' '''N''' ('''S''' '''I''' '''I''')) '''Ω''') '''I''')
 
now consider the term ('''S''' '''I''' '''I''' ''Z''). Does ('''S''' '''I''' '''I''' ''Z'') have a normal
form? It does if and only if the following do also:
 
:{{spaces|2}}('''S''' '''I''' '''I''' ''Z'')
:= ('''I''' ''Z'' ('''I''' ''Z''))
:= (''Z'' ('''I''' ''Z''))
:= (''Z'' ''Z'')
:= ('''C''' ('''C''' ('''B''' '''N''' ('''S''' '''I''' '''I''')) '''Ω''') '''I''' ''Z'') (definition of ''Z'')
:= ('''C''' ('''B''' '''N''' ('''S''' '''I''' '''I''')) '''Ω''' ''Z'' '''I''')
:= ('''B''' '''N''' ('''S''' '''I''' '''I''') ''Z'' '''Ω''' '''I''')
:= ('''N''' ('''S''' '''I''' '''I''' ''Z'') '''Ω''' '''I''')
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}}('''N''' ('''S''' '''I''' '''I''' ''Z'') '''Ω''' '''I''')
:= ('''K''' '''Ω''' '''I''') (definition of '''N''')
:= '''Ω'''
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}}('''N''' ('''S''' '''I''' '''I''' ''Z'') '''Ω''' '''I''')
:= ('''K''' '''I''' '''Ω''' '''I''') (definition of '''N''')
:= ('''I''' '''I''')
:= '''I'''
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'''. A predicate '''N''' is ''nontrivial'' if there are two arguments ''A'' and ''B'' such that '''N''' ''A'' = '''T''' and '''N''' ''B'' = '''F'''. A combinator '''N''' is ''complete'' if '''N'''''M'' has a normal form for every argument ''M''. The analogue of Rice's theorem then says that every complete predicate is trivial. The proof of this theorem is rather simple.
{{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 385 ⟶ 337:
Hence ('''N''' ABSURDUM) is neither '''T''' nor '''F''', which contradicts the presupposition that '''N''' would be a complete non trivial predicate. '''[[Q.E.D.]]'''
}}
From this undecidabilityundefinability theorem it immediately follows that there is no complete predicate that can discriminate between terms that have a normal form and terms that do not have a normal form. It also follows that there is '''no''' complete predicate, say EQUAL, such that:
:(EQUAL ''A B'') = '''T''' if ''A'' = ''B'' and
:(EQUAL ''A B'') = '''F''' if ''A'' ≠ ''B''.
If EQUAL would exist, then for all ''A'', ''λx.''(EQUAL ''x A'') would have to be a complete non trivial predicate.
 
However, note that it also immediately follows from this undefinability theorem that many properties of terms that are obviously decidable are not definable by complete predicates either: e.g., there is no predicate that could tell whether the first primitive function letter occurring in a term is a '''K'''. This shows that definability by predicates is a not a reasonable model of decidability.
 
== Applications ==
Line 434 ⟶ 388:
*{{cite book| last1=Curry|first1=Haskell Brooks|author-link1=Haskell Curry|last2=Feys|first2=Robert|author-link2=Robert Feys|title=Combinatory Logic|volume=I|year=1958|publisher=North Holland|location=Amsterdam|isbn=0-7204-2208-6}}
*{{cite book| last1=Curry|first1=Haskell Brooks|author-link1=Haskell Curry|first2=J. Roger|last2=Hindley|author-link2=J. Roger Hindley|first3=Jonathan P.|last3=Seldin|title=Combinatory Logic|volume=II|year=1972| publisher=North Holland |location=Amsterdam | isbn=0-7204-2208-6}}
*{{cite book
| last = Engeler | first = E.
| pages = 5–6
| publisher = Birkhäuser
| title = The Combinatory Programme
| url = https://people.math.ethz.ch/~engeler/CombinatoryProgram-foreword.pdf
| year = 1995}}
*{{cite book| last1=Field |first1=Anthony J. |first2=Peter G.|last2=Harrison |author-link2=Peter G. Harrison |year=1998 |title=Functional Programming |url=https://archive.org/details/functionalprogra0000fiel |url-access=registration |publisher=Addison-Wesley |isbn=0-201-19249-7}}
*{{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}}
Line 457 ⟶ 418:
*[https://web.archive.org/web/20070209093802/http://www.sadl.uleth.ca/gsdl/cgi-bin/library?a=p&p=about&c=curry 1920–1931 Curry's block notes.]
*Keenan, David C. (2001) "[http://dkeenan.com/Lambda/index.htm To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction.]"
*Rathman, Chris, "[httphttps://www.angelfire.com/tx4/cus/combinator/birds.html Combinator Birds.]" A table distilling much of the essence of Smullyan (1985).
*[https://web.archive.org/web/20081029051502/http://cstein.kings.cam.ac.uk/~chris/combinators.html Drag 'n' Drop Combinators.] (Java Applet)
*[https://web.archive.org/web/20160304083208/http://tromp.github.io/cl/LC.pdf Binary Lambda Calculus and Combinatory Logic.]
Line 465 ⟶ 426:
|first=Stephen
|author-link=Stephen Wolfram
|date={{date|2020-04-29}} April 2020
|url=https://www.youtube.com/watch?v=PG2G5xSz0NQ
|title=Combinators: 100-Year Celebration
|publisher=[[Stephen Wolfram|Wolfram Physics Project]] on [[YouTube]]
|access-date={{date|2023-09-26}} September 2023
}}
 
{{authority control}}
 
[[Category:Combinatory logic|Combinatory logic]]
[[Category:Lambda calculus]]
Retrieved from "https://en.wikipedia.org/wiki/Combinatory_logic"