GetWiki
combinatory logic
ARTICLE SUBJECTS
being →
database →
ethics →
fiction →
history →
internet →
language →
linux →
logic →
method →
news →
policy →
purpose →
religion →
science →
software →
truth →
unix →
wiki →
ARTICLE TYPES
essay →
feed →
help →
system →
wiki →
ARTICLE ORIGINS
critical →
forked →
imported →
original →
combinatory logic
please note:
- the content below is remote from Wikipedia
- it has been imported raw for GetWiki
{{distinguish|text=combinational logic, a topic in digital electronics}}Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses SchÃ¶nfinkelJOURNAL, Moses, SchÃ¶nfinkel, Moses SchÃ¶nfinkel, 1924,weblink Ãœber die Bausteine der mathematischen Logik, Mathematische Annalen, 92, 305â€“316, 10.1007/bf01448013, Translated by Stefan Bauer-Mengelberg as "On the building blocks of mathematical logic" in Jean van Heijenoort, 1967. A Source Book in Mathematical Logic, 1879–1931. Harvard Univ. Press: 355–66. and Haskell Curry,JOURNAL, Curry, Haskell Brooks, Grundlagen der Kombinatorischen Logik, American Journal of Mathematics, 1930, 52, 3, 509â€“536, Haskell Curry, Foundations of combinatorial logic, The Johns Hopkins University Press, German, 10.2307/2370619, 2370619, and has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming languages. It is based on combinators which were introduced by SchÃ¶nfinkel in 1920 with the idea of providing an analogous way to build up functions - and to remove any mention of variables - particularly in predicate logic.BOOK, Wolfram, Stephen, A New Kind of Science, Wolfram Media, Inc., 2002, 1121, 1-57955-008-8, A combinator is a higher-order function that uses only function application and earlier defined combinators to define a result from its arguments.- the content below is remote from Wikipedia
- it has been imported raw for GetWiki
In mathematics
Combinatory logic was originally intended as a 'pre-logic' that would clarify the role of quantified variables in logic, essentially by eliminating them. Another way of eliminating quantified variables is Quine's predicate functor logic. While the 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, 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.JOURNAL, Seldin, Jonathan, The Logic of Curry and Church, 2008,weblink In the latter 1930s, Alonzo Church and his students at Princeton invented a rival formalism for functional abstraction, the lambda calculus, which proved more popular than combinatory logic. The upshot of these historical contingencies was that until theoretical computer science began taking an interest in combinatory logic in the 1960s and 1970s, nearly all work on the subject was by Haskell Curry and his students, or by Robert Feys in Belgium. Curry and Feys (1958), and Curry et al. (1972) survey the early history of combinatory logic. For a more modern treatment of combinatory logic and the lambda calculus together, see the book by Barendregt,{{sfn|Barendregt|1984}} which reviews the models Dana Scott devised for combinatory logic in the 1960s and 1970s.In computing
In computer science, combinatory logic is used as a simplified model of computation, used in computability theory and proof theory. Despite its simplicity, combinatory logic captures many essential features of computation.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 from which bound variables are absent. 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 functional programming languages and 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 (Hindley and Meredith 1990). Dana Scott in the 1960s and 1970s showed how to marry model theory and combinatory logic.Summary of lambda calculus
Lambda calculus is concerned with objects called lambda-terms, which can be represented bythe following three forms of strings:- {{mvar|v}}
- {{tmath|lambda v.E_1}}
- {{tmath|(E_1 E_2)}}
{{tmath|((lambda v.E) a) Rightarrow E[v :{{=}} a]}}
By convention, we take {{tmath|(a b c)}} as shorthand for {{tmath|((a b) c)}} (i.e., application is left associative).The motivation for this definition of reduction is that it capturesthe essential behavior of all mathematical functions. For example,consider the function that computes the square of a number. We mightwrite
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 particularargument, say 3, we insert it into the definition in place of theformal parameter:
The square of 3 is {{tmath|3*3}}
To evaluate the resulting expression {{tmath|3*3}}, we would have to resort toour knowledge of multiplication and the number 3. Since anycomputation is simply a composition of the evaluation of suitablefunctions on suitable primitive arguments, this simple substitutionprinciple suffices to capture the essential mechanism of computation.Moreover, in lambda calculus, notions such as '3' and '{{tmath|*}}' can berepresented without any need for externally defined primitiveoperators or constants. It is possible to identify terms in lambda calculus, which, when suitably interpreted, behave like thenumber 3 and like the multiplication operator, q.v. Church encoding.Lambda calculus is known to be computationally equivalent in power tomany other plausible models for computation (including Turing machines); that is, any calculation that can be accomplished in anyof these other models can be expressed in lambda calculus, andvice versa. According to the Church-Turing thesis, both modelscan express any possible computation.It is perhaps surprising that lambda-calculus can represent anyconceivable computation using only the simple notions of functionabstraction and application based on simple textual substitution ofterms for variables. But even more remarkable is that abstraction isnot even required. Combinatory logic is a model of computationequivalent to lambda calculus, but without abstraction. The advantageof this is that evaluating expressions in lambda calculus is quite complicatedbecause the semantics of substitution must be specified with great care toavoid variable capture problems. In contrast, evaluating expressions incombinatory logic is much simpler, because there is no notion of substitution.Combinatory calculi
Since abstraction is the only way to manufacture functions in thelambda calculus, something must replace it in the combinatorycalculus. Instead of abstraction, combinatory calculus provides alimited set of primitive functions out of which other functions may bebuilt.Combinatory terms
A combinatory term has one of the following forms:- {{mvar|x}}
- {{mvar|P}}
- {{tmath|(E_1 E_2)}}
Reduction in combinatory logic
In combinatory logic, each primitive combinator comes with a reduction rule of the form
{{math|1=(P x1 ... xn) = E}}
where E is a term mentioning only variables from the set {{math|{{mset|x1 ... xn}}}}. It is in this way that primitive combinators behave as functions.Examples of combinators
The simplest example of a combinator is I, the identitycombinator, defined by
(I x) = x
for all terms x. Another simple combinator is K, whichmanufactures 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 formultiple application,
(K x y) = x
A third combinator is S, which is a generalized version ofapplication:
(S x y z) = (x z (y z))
S applies x to y after first substituting z intoeach of them. Or put another way, x is applied to y inside theenvironment z.Given S and K, I itself is unnecessary, since it canbe built from the other two:
((S K K) x)
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 extensionally equal. Extensional equality captures themathematical notion of the equality of functions: that two functionsare equal if they always produce the same results for the samearguments. In contrast, the terms themselves, together with thereduction of primitive combinators, capture the notion ofintensional equality of functions: that two functions are equalonly if they have identical implementations up to the expansion of primitivecombinators when these ones are applied to enough arguments. There are many ways toimplement an identity function; (S K K) and Iare among these ways. (S K S) is yet another. Wewill 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.
= (S K K x)
= (K x (K x))
= x
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, T[ ], which converts an arbitrary lambda term into an equivalent combinator.T[ ] may be defined as follows:- T[x] => x
- T[(Eâ‚ Eâ‚‚)] => (T[Eâ‚] T[Eâ‚‚])
- T[Î»x.E] => (K T[E]) (if x does not occur free in E)
- T[Î»x.x] => I
- T[Î»x.Î»y.E] => T{{!(}}Î»x.T{{!(}}Î»y.E{{))!}} (if x occurs free in E)
- T[Î»x.(Eâ‚ Eâ‚‚)] => (S T[Î»x.Eâ‚] T[Î»x.Eâ‚‚]) (if x occurs free in Eâ‚ or Eâ‚‚)
- [x]y := K y
- [x]x := I
- [x](Eâ‚ Eâ‚‚) := S([x]Eâ‚)([x]Eâ‚‚)
Conversion of a lambda term to an equivalent combinatorial term
For example, we will convert the lambda term Î»x.Î»y.(y x) to acombinatorial term:
T[Î»x.Î»y.(y x)]
If we apply this combinatorial term to any two terms x and y, itreduces as follows:
= T{{!(}}Î»x.T{{!(}}Î»y.(y x){{))!}} (by 5)
= T[Î»x.(S T[Î»y.y] T[Î»y.x])] (by 6)
= T[Î»x.(S I T[Î»y.x])] (by 4)
= T[Î»x.(S I (K T[x]))] (by 3)
= T[Î»x.(S I (K x))] (by 1)
= (S T[Î»x.(S I)] T[Î»x.(K x)]) (by 6)
= (S (K (S I)) T[Î»x.(K x)]) (by 3)
= (S (K (S I)) (S T[Î»x.K] T[Î»x.x])) (by 6)
= (S (K (S I)) (S (K K) T[Î»x.x])) (by 3)
= (S (K (S I)) (S (K K) I)) (by 4)
(S (K (S I)) (S (K K) I) x y)
The combinatory representation, (S (K (S I)) (S (K K) I)) is muchlonger than the representation as a lambda term, Î»x.Î»y.(y x). This is typical. In general, the T[ ] construction may expand a lambdaterm of length n to a combinatorial term of lengthÎ˜(n3) JOURNAL, Lachowski, Åukasz, On the Complexity of the Standard Translation of Lambda Calculus into Combinatory Logic, Reports on Mathematical Logic, 2018, 53, 19-42, 10.4467/20842589RM.18.002.8835,weblink 9 September 2018, .
= (K (S I) x (S (K K) I x) y)
= (S I (S (K K) I x) y)
= (I y (S (K K) I x y))
= (y (S (K K) I x y))
= (y (K K x (I x) y))
= (y (K (I x) y))
= (y (I x))
= (y x)
Explanation of the T[ ] transformation
The T[ ] transformation is motivated by a desire to eliminateabstraction. Two special cases, rules 3 and 4, are trivial: Î»x.x isclearly 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, areconverted to combinators simply by converting the applicand and theargument 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, andsubstitutes 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
(Eâ‚ Eâ‚‚)[x := a] = (Eâ‚[x := a] Eâ‚‚[x := a])
(Î»x.(Eâ‚ Eâ‚‚) a) = ((Î»x.Eâ‚ a) (Î»x.Eâ‚‚ a))
By extensional equality,
= (S Î»x.Eâ‚ Î»x.Eâ‚‚ a)
= ((S Î»x.Eâ‚ Î»x.Eâ‚‚) a)
Î»x.(Eâ‚ Eâ‚‚) = (S Î»x.Eâ‚ Î»x.Eâ‚‚)
Therefore, to find a combinator equivalent to Î»x.(Eâ‚ Eâ‚‚), it issufficient to find a combinator equivalent to (S Î»x.Eâ‚ Î»x.Eâ‚‚), and
(S T[Î»x.Eâ‚] T[Î»x.Eâ‚‚])
evidently fits the bill. Eâ‚ and Eâ‚‚ each contain strictly fewerapplications than (Eâ‚ Eâ‚‚), so the recursion must terminate in a lambdaterm with no applications at allâ€”either a variable, or a term of theform Î»x.E.Simplifications of the transformation
Î·-reduction
The combinators generated by the T[ ] transformation can be madesmaller if we take into account the Î·-reduction rule:
T[Î»x.(E x)] = T[E] (if x is not free in E)
Î»x.(E x) is the function which takes an argument, x, andapplies the function E to it; this is extensionally equal to thefunction E itself. It is therefore sufficient to convert E tocombinatorial form.Taking this simplification into account, the example above becomes:
T[Î»x.Î»y.(y x)]
= ...
= (S (K (S I)) T[Î»x.(K x)])
= (S (K (S I)) K) (by Î·-reduction)
This combinator is equivalent to the earlier, longer one:
(S (K (S I)) K x y)
= (K (S I) x (K x) y)
= (S I (K x) y)
= (I y (K x y))
= (y (K x y))
= (y x)
Similarly, the original version of the T[ ] transformationtransformed 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) istransformed into I.One-point basis
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:
X â‰¡ Î»x.((xS)K)
It is not difficult to verify that:
X (X (X X)) =Î·Î² K and
X (X (X (X X))) =Î·Î² S.
Since {K, S} is a basis, it follows that {X} is a basis too. The Iota programming language uses X as its sole combinator.Another simple example of a one-point basis is:
X' â‰¡ Î»x.(x K S K) with
(X' X') X' =Î² K and
X' (X' X') =Î² S
X' does not need Î· contraction in order to produce K and S. In fact, there exist infinitely many such bases.JOURNAL, Mayer, Goldberg,weblink 10.1016/j.ipl.2003.12.005, 89, 2004, A construction of one-point bases in extended lambda calculi, Information Processing Letters, 281â€“286, Combinators B, C
In addition to S and K, SchÃ¶nfinkel's paper included two combinators which are now called B and C, with the following reductions:
(C f g x) = ((f x) g)
(B f g x) = (f (g x))
He also explains how they in turn can be expressed using only S and K:
B = (S (K S) K)
C = (S (S (K (S (K S) K)) S) (K K))
These combinators are extremely useful when translating predicate logic or lambda calculus into combinator expressions. They were also used by Curry, and much later by David Turner, whose name has been associated with their computational use. Using them, we can extend the rules for the transformation as follows: - T[x] ⇒ x
- T[(Eâ‚ Eâ‚‚)] ⇒ (T[Eâ‚] T[Eâ‚‚])
- T[Î»x.E] ⇒ (K T[E]) (if x is not free in E)
- T[Î»x.x] ⇒ I
- T[Î»x.Î»y.E] ⇒ T{{!(}}Î»x.T{{!(}}Î»y.E{{))!}} (if x is free in E)
- T[Î»x.(Eâ‚ Eâ‚‚)] ⇒ (S T[Î»x.Eâ‚] T[Î»x.Eâ‚‚]) (if x is free in both Eâ‚ and Eâ‚‚)
- T[Î»x.(Eâ‚ Eâ‚‚)] ⇒ (C T[Î»x.Eâ‚] T[Eâ‚‚]) (if x is free in Eâ‚ but not Eâ‚‚)
- T[Î»x.(Eâ‚ Eâ‚‚)] ⇒ (B T[Eâ‚] T[Î»x.Eâ‚‚]) (if x is free in Eâ‚‚ but not Eâ‚)
T[Î»x.Î»y.(y x)]
= T{{!(}}Î»x.T{{!(}}Î»y.(y x){{))!}}
= T[Î»x.(C T[Î»y.y] x)] (by rule 7)
= T[Î»x.(C I x)]
= (C I) (Î·-reduction)
= mathbf{C}_{*} (traditional canonical notation : mathbf{X}_{*} = mathbf{X I})
= mathbf{I}' (traditional canonical notation: mathbf{X}' = mathbf{C X})
And indeed, (C I x y) does reduce to (y x):
(C I x y)
= (I y x)
= (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 andits argument before performing the application, C performs thesubstitution 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 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 rulescan also be achieved without introducing B and C, as demonstrated in Section 3.2 of.BOOK, John, Tromp, Binary Lambda Calculus and Combinatory Logic, Randomness And Complexity, from Leibniz To Chaitin, Cristian S., Calude, World Scientific Publishing Company, 2008,weblink" title="web.archive.org/web/20160304083208weblink">weblink CLK versus CLI calculus
A distinction must be made between the CLK as described in this article and the CLI calculus. The distinction corresponds to that between the Î»K and the Î»I calculus. Unlike the Î»K calculus, the Î»I calculus restricts abstractions to:
Î»x.E where x has at least one free occurrence in E.
Reverse conversion
The conversion L[ ] from combinatorial terms to lambda terms istrivial:
L[I] = Î»x.x
L[K] = Î»x.Î»y.x
L[C] = Î»x.Î»y.Î»z.(x z y)
L[B] = Î»x.Î»y.Î»z.(x (y z))
L[S] = Î»x.Î»y.Î»z.(x z (y z))
L[(Eâ‚ Eâ‚‚)] = (L[Eâ‚] L[Eâ‚‚])
Note, however, that this transformation is not the inversetransformation of any of the versions of T[ ] that we have seen.Undecidability of combinatorial calculus
A 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 is equivalent to the undecidability of the corresponding problems for lambda terms. However, a direct proof is as follows:First, observe that the term
Î© = (S I I (S I I))
has no normal form, because it reduces to itself after three steps, asfollows:
{{spaces|2}} (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
(mathbf{N} x) = begin{cases} mathbf{T}, text{ if } x text{ has a normal form}
mathbf{F}, text{ otherwise.} end{cases}
(Where {{math|T}} and {{math|F}} represent the conventional Church encodings 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 normalform? 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 doeshave 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. Butif (S I I Z) does not have a normal form, the foregoing reduces asfollows:
{{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, anothercontradiction. Therefore, the hypothetical normal-form combinator Ncannot 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 and only if NM 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.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
(N A) = T and
(N B) = F.
Define NEGATION â‰¡ Î»x.(if (N x) then B else A) â‰¡ Î»x.((N x) B A)
Define ABSURDUM â‰¡ (Y NEGATION)
Fixed point theorem gives: ABSURDUM = (NEGATION ABSURDUM), for
ABSURDUM â‰¡ (Y NEGATION) = (NEGATION (Y NEGATION)) â‰¡ (NEGATION ABSURDUM).
Because N is supposed to be complete either: - (N ABSURDUM) = F or
- (N ABSURDUM) = T
- Case 1: F = (N ABSURDUM) = N (NEGATION ABSURDUM) = (N A) = T, a contradiction.
- Case 2: T = (N ABSURDUM) = N (NEGATION ABSURDUM) = (N B) = F, again a contradiction.
(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.Applications
Compilation of functional languages
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. 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.JOURNAL, Pure Functions in APL and J, Proceedings of the international conference on APL '91, Edward, Cherlin, 88â€“93, 1991, 10.1145/114054.114065,Logic
The Curryâ€“Howard isomorphism implies a connection between logic and programming: every proof of a theorem of intuitionistic logic corresponds to a reduction of a typed lambda term, and conversely. Moreover, theorems can be identified with function type signatures. Specifically, a typed combinatory logic corresponds to a Hilbert system in proof theory.The K and S combinators correspond to the axioms
AK: A â†’ (B â†’ A),
AS: (A â†’ (B â†’ C)) â†’ ((A â†’ B) â†’ (A â†’ C)),
and function application corresponds to the detachment (modus ponens) rule
MP: from A and A â†’ B infer B.
The calculus consisting of AK, AS, and MP is complete for the implicational fragment of the intuitionistic logic, which can be seen as follows. Consider the set W of all deductively closed sets of formulas, ordered by inclusion. Then langle W,subseteqrangle is an intuitionistic Kripke frame, and we define a model Vdash in this frame by
XVdash Aiff Ain X.
This definition obeys the conditions on satisfaction of â†’: on one hand, if XVdash Ato B, and Yin W is such that Ysupseteq X and YVdash A, then YVdash B by modus ponens. On the other hand, if XnotVdash Ato B, then X,Anotvdash B by the deduction theorem, thus the deductive closure of Xcup{A} is an element Yin W such that Ysupseteq X, YVdash A, and YnotVdash B.Let A be any formula which is not provable in the calculus. Then A does not belong to the deductive closure X of the empty set, thus XnotVdash A, and A is not intuitionistically valid.See also
- Applicative computing systems
- B, C, K, W system
- Categorical abstract machine
- Combinatory categorial grammar
- Explicit substitution
- Fixed point combinator
- Graph reduction machine
- Lambda calculus and Cylindric algebra, other approaches to modelling quantification and eliminating variables
- SKI combinator calculus
- Supercombinator
- To Mock a Mockingbird
References
{{reflist}}Further reading
- BOOK, Barendregt, Hendrik Pieter, Henk Barendregt, 1984, The Lambda Calculus, Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, Volume 103, North Holland, 0-444-87508-5, harv,
- BOOK, Curry, Haskell B., Haskell Curry, Feys, Robert, Robert Feys, Combinatory Logic, Vol. I, 1958, North Holland, Amsterdam, 0-7204-2208-6,
- BOOK, Curry, Haskell B., Haskell Curry, J. Roger, Hindley, J. Roger Hindley, Jonathan P., Seldin, Combinatory Logic, Vol. II, 1972, North Holland, Amsterdam, 0-7204-2208-6,
- BOOK, Field, Anthony J., Peter G., Harrison, Peter G. Harrison, 1998, Functional Programming, Addison-Wesley, 0-201-19249-7,
- {{citation|last1=Hindley|first1=J. Roger|authorlink1=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|pp=90â€“105|year=1990|doi=10.2307/2274956|jstor=2274956}}
- BOOK, Hindley, J. R., J. Roger Hindley, Seldin, J. P., 2008,weblink Î»-calculus and Combinators: An Introduction, Cambridge University Press,
- BOOK, Paulson, Lawrence C., Lawrence Paulson, 1995,weblink Foundations of Functional Programming, University of Cambridge,
- JOURNAL, Willard Van Orman Quine, Quine, W. V., 1960, Variables explained away, Proceedings of the American Philosophical Society, 104, 3, 343â€“347, 985250, Reprinted as Chapter 23 of Quine's Selected Logic Papers (1966), pp. 227â€“235
- SchÃ¶nfinkel, Moses, 1924, "Ãœber die Bausteine der mathematischen Logik," translated as "On the Building Blocks of Mathematical Logic" in From Frege to GÃ¶del: a source book in mathematical logic, 1879â€“1931, Jean van Heijenoort, ed. Harvard University Press, 1967. {{ISBN|0-674-32449-8}}. The article that founded combinatory logic.
- 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 Univ. 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. weblink" title="web.archive.org/web/20051016213140weblink">Lectures on the Curryâ€“Howard Isomorphism. University of Copenhagen and University of Warsaw, 1999.
- BOOK, Wolfengagen, V. E.,weblink Combinatory logic in programming: Computations with objects through examples and exercises, 2nd, Moscow, "Center JurInfoR" Ltd., 2003, 5-89158-101-9, .
External links
- Stanford Encyclopedia of Philosophy: "Combinatory Logic" by Katalin BimbÃ³.
- weblink" title="web.archive.org/web/20070209093802weblink">1920â€“1931 Curry's block notes.
- Keenan, David C. (2001) "To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction."
- Rathman, Chris, "Combinator Birds." A table distilling much of the essence of Smullyan (1985).
- weblink" title="web.archive.org/web/20081029051502weblink">Drag 'n' Drop Combinators. (Java Applet)
- weblink" title="web.archive.org/web/20160304083208weblink">Binary Lambda Calculus and Combinatory Logic.
- Combinatory logic reduction web server
- content above as imported from Wikipedia
- "combinatory logic" does not exist on GetWiki (yet)
- time: 7:59pm EST - Sat, Feb 23 2019
- "combinatory logic" does not exist on GetWiki (yet)
- time: 7:59pm EST - Sat, Feb 23 2019
[ this remote article is provided by Wikipedia ]
LATEST EDITS [ see all ]
GETWIKI 09 MAY 2016
GetMeta:About
GetWiki
GetWiki
GETWIKI 18 OCT 2015
M.R.M. Parrott
Biographies
Biographies
GETWIKI 20 AUG 2014
GetMeta:News
GetWiki
GetWiki
GETWIKI 19 AUG 2014
GETWIKI 18 AUG 2014
Wikinfo
Culture
Culture
© 2019 M.R.M. PARROTT | ALL RIGHTS RESERVED