NationMaster - Encyclopedia: Combinatory logic

Combinatory logic is a notation introduced by Moses Schönfinkel and Haskell Curry to eliminate the need for variables in mathematical logic. It 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. A combinator is a higher-order function which, for defining a result from its arguments, solely use function application and earlier defined combinators. This article is not about combinatory logic, a topic in mathematical logic. ... Moses SchÃ¶nfinkel, also known as Moisei Isaievich Sheinfinkel Ð¨ÐµÐ¹Ð½Ñ„Ð¸Ð½ÐºÐµÐ»ÑŒ (September 4, 1889 Ekaterinoslav â€“ 1942, Moscow) was a Russian logician and mathematician. ... Haskell Brooks Curry (September 12, 1900, Millis, Massachusetts - September 1, 1982, State College, Pennsylvania) was an American mathematician and logician. ... In computer science and mathematics, a variable (IPA pronunciation: ) (sometimes called a pronumeral) is a symbolic representation denoting a quantity or expression. ... Mathematical logic is a major area of mathematics, which grew out of symbolic logic. ... Functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions. ... In mathematics and computer science, higher-order functions are functions which can take other functions as arguments, and may also return functions as results. ...

Combinatory logic 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 Willard Van Orman Quine's predicate functors. While most systems of combinatory logic exceed the expressive power of first-order logic, Quine's predicate functors are equivalent in expressive power to first-order logic (Quine [1960] 1966). For people named Quine, see Quine (surname). ... First-order logic (FOL) is a universal language in symbolic science, and is in use everyday by mathematicians, philosophers, linguists, computer scientists and practitioners of artificial intelligence. ...

The original inventor of combinatory logic, Schönfinkel, published nothing on combinatory logic after his original 1924 paper, and largely ceased to publish after Stalin consolidated his power in 1929. Curry rediscovered the combinators while a PhD student at the University of Göttingen in the late 1920s, but that epochal department fell apart when Hitler came to power in 1933. In the latter 1930s, Alonzo Church and his students at Princeton University 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 70s, 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 parallel treatment of combinatory logic and the lambda calculus, see Barendregt (1984), who also reviews the models Dana Scott devised for combinatory logic in the 1960s and 70s. Year 1924 (MCMXXIV) was a leap year starting on Tuesday (link will display the full calendar) of the Gregorian calendar. ... Iosif (usually anglicized as Joseph) Vissarionovich Stalin (Russian: Иосиф Виссарионович Сталин), original name Ioseb Jughashvili (Georgian: იოსებ ჯუღაშვი&#4314... The Georg-August University of GÃ¶ttingen (Georg-August-UniversitÃ¤t GÃ¶ttingen, often called the Georgia Augusta) was founded in 1734 by George II, King of Great Britain and Elector of Hanover, and opened in 1737. ... The 1920s is a decade that is sometimes referred to as the Jazz Age or the Roaring Twenties, usually applied to America. ... Adolf Hitler Adolf Hitler (April 20, 1889 – April 30, 1945, standard German pronunciation in the IPA) was the Führer (leader) of the National Socialist German Workers Party (Nazi Party) and of Nazi Germany from 1933 to 1945. ... Face The 1930s (years from 1930â€“1939) were described as an abrupt shift to more radical and conservative lifestyles, as countries were struggling to find a solution to the Great Depression, also known in Europe as the World Depression. ... â€¹ The template below (Expand) is being considered for deletion. ... Princeton University is a private coeducational research university located in Princeton, New Jersey. ... The lambda calculus is a formal system designed to investigate function definition, function application, and recursion. ... The 1960s decade refers to the years from January 1, 1960 to December 31, 1969, inclusive. ... Centuries: 1st century BC - 1st century - 2nd century Decades: 20s - 30s - 40s - 50s - 60s - 70s - 80s - 90s - 100s - 110s - 120s 70 71 72 73 74 75 76 77 78 79 Note: Sometimes the 70s is used as shorthand for the 1970s, the 1870s, or other such decades in other centuries... Haskell Brooks Curry (September 12, 1900, Millis, Massachusetts - September 1, 1982, State College, Pennsylvania) was an American mathematician and logician. ... Robert Feys (1889 â€” 1961) was a logician and philosopher. ... In mathematics, model theory is the study of the representation of mathematical concepts in terms of set theory, or the study of the structures that underlie mathematical systems. ... Dana Stewart Scott (born 1932) is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, California. ... The 1960s decade refers to the years from January 1, 1960 to December 31, 1969, inclusive. ... Centuries: 1st century BC - 1st century - 2nd century Decades: 20s - 30s - 40s - 50s - 60s - 70s - 80s - 90s - 100s - 110s - 120s 70 71 72 73 74 75 76 77 78 79 Note: Sometimes the 70s is used as shorthand for the 1970s, the 1870s, or other such decades in other centuries...

Combinatory logic 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. Look up computation in Wiktionary, the free dictionary. ... Computability theory is the branch of theoretical computer science that studies which problems are computationally solvable using different models of computation. ... Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. ...

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 free 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. The lambda calculus is a formal system designed to investigate function definition, function application, and recursion. ... In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a free variable is a notation for a place or places in an expression, into which some definite substitution may take place, or with respect to which some operation (summation or quantification, to give two... A strict programming language is one in which only strict functions may be defined by the user. ... Functional programming is a programming paradigm that conceives computation as the evaluation of mathematical functions and avoids state and mutable data. ... A graph reduction machine is a special-purpose computer built to perform combinator calculations by graph reduction. ... Unlambda is a minimal functional programming language based on combinatory logic, a version of the lambda calculus that omits the lambda operator. ...

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 70s showed how to marry model theory and combinatory logic. In mathematics, model theory is the study of the representation of mathematical concepts in terms of set theory, or the study of the structures that underlie mathematical systems. ...

Summary of the lambda calculus

Main article: lambda calculus

The lambda calculus is concerned with objects called lambda-terms, which are strings of symbols of one of the following forms: The lambda calculus is a formal system designed to investigate function definition, function application, and recursion. ...

v
λv.E1
(E1 E2)

where v is a variable name drawn from a predefined infinite set of variable names, and E1 and E2 are lambda-terms. Terms of the form λv.E1 are called abstractions. The variable v is called the formal parameter of the abstraction, and E1 is the body of the abstraction. A parameter is a measurement or value on which something else depends. ...

The term λv.E1 represents the function which, applied to an argument, binds the formal parameter v to the argument and then computes the resulting value of E1---that is, it returns E1, with every occurrence of v replaced by the argument.

Terms of the form (E1 E2) are called applications. Applications model function invocation or execution: the function represented by E1 is to be invoked, with E2 as its argument, and the result is computed. If E1 (sometimes called the applicand) is an abstraction, the term may be reduced: E2, the argument, may be substituted into the body of E1 in place of the formal parameter of E1, 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 (λv.E1 E2) then it cannot be reduced, and is said to be in normal form. In the lambda calculus, a term is in beta normal form if no beta reduction is possible. ...

The expression E[v := a] represents the result of taking the term E and replacing all free occurrences of v with a. Thus we write

(λv.E a) => E[v := a]

By convention, we take (a b c d ... z) as short for (...(((a b) c) d) ... z). (i.e., application is left associative.) In mathematics, associativity is a property that a binary operation can have. ...

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 x*x

(Using "*" 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: A parameter is a measurement or value on which something else depends. ...

The square of 3 is 3*3

To evaluate the resulting expression 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 the lambda calculus, notions such as '3' and '*' can be represented without any need for externally defined primitive operators or constants. It is possible to identify terms in the lambda calculus, which, when suitably interpreted, behave like the number 3 and like the multiplication operator.

The lambda calculus is known to be computationally equivalent in power to many other plausible models for computation (including Turing machines); that is, any calculation that can be accomplished in any of these other models can be expressed in the lambda calculus, and vice versa. According to the Church-Turing thesis, both models can express any possible computation. An artistic representation of a Turing Machine . ... In computability theory the Church-Turing thesis, Churchs thesis, Churchs conjecture or Turings thesis, named after Alonzo Church and Alan Turing, is a hypothesis about the nature of mechanical calculation devices, such as electronic computers. ...

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 the 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

A combinatory term has one of the following forms:

v
P
(E1 E2)

where v is a variable, P is one of the primitive functions, and E1 and E2 are combinatory terms. The primitive functions themselves are combinators, or functions that contain no free variables. In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a free variable is a notation for a place or places in an expression, into which some definite substitution may take place, or with respect to which some operation (summation or quantification, to give two...

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 same convention for multiple application as in the lambda-calculus,

(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)

= (S K K x)

= (K x (K x))

= 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 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 capture the notion of intensional equality of functions: that two functions are 'equal' only if they have identical implementations. 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. In mathematics, this usually refers to some form of the principle, going back to Leibniz, that two mathematical objects are equal if there is no test to distinguish them. ...

A more interesting combinator is the fixed point combinator or Y combinator, which can be used to implement recursion. A fixed point combinator (or fixed-point operator) is a higher-order function which computes a fixed point of other functions. ... A visual form of recursion known as the Droste effect. ...

Completeness of the S-K basis

It is a perhaps astonishing fact that 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[V] => V
T[(E1 E2)] => (T[E1] T[E2])
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.(E1 E2)] => (S T[λx.E1] T[λx.E2])

This process is also known as abstraction elimination.

Conversion of a lambda term to an equivalent combinatorial term

For example, we will convert the lambda term λx.λy.(y x) to a combinator:

T[λx.λy.(y x)]

= 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 x))] (by 3 and 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)

If we apply this combinator to any two terms x and y, it reduces as follows:

(S (K (S I)) (S (K K) I) x y)

= (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)

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 Θ(3ⁿ). For other uses, see Big O. In computational complexity theory, big O notation is often used to describe how the size of the input data affects an algorithms usage of computational resources (usually running time or memory). ...

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 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's 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.(E1 E2) is a function which takes an argument, say a, and substitutes it into the lambda term (E1 E2) in place of x, yielding (E1 E2)[x : = a]. But substituting a into (E1 E2) in place of x is just the same as substituting it into both E1 and E2, so

 (E1 E2)[x := a] = (E1[x := a] E2[x := a])

(λx.(E1 E2) a) = ((λx.E1 a) (λx.E2 a))

 = (S λx.E1 λx.E2 a) = ((S λx.E1 λx.E2) a)

By extensional equality,

 λx.(E1 E2) = (S λx.E1 λx.E2)

Therefore, to find a combinator equivalent to λx.(E1 E2), it is sufficient to find a combinator equivalent to (S λx.E1 λx.E2), and

 (S T[λx.E1] T[λx.E2])

evidently fits the bill. E1 and E2 each contain strictly fewer applications than (E1 E2), 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.

Simplifications of the transformation

η-reduction

The combinators generated by the T[ ] transformation can be made smaller 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, 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:

 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[] 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.

One point basis

There are one point bases from which every combinator can be composed extentionally 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.

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: Moses SchÃ¶nfinkel, also known as Moisei Isaievich Sheinfinkel Ð¨ÐµÐ¹Ð½Ñ„Ð¸Ð½ÐºÐµÐ»ÑŒ (September 4, 1889 Ekaterinoslav â€“ 1942, Moscow) was a Russian logician and mathematician. ...

 (C a b c) = (a c b) (B a b c) = (a (b c))

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 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: Haskell Brooks Curry (September 12, 1900, Millis, Massachusetts - September 1, 1982, State College, Pennsylvania) was an American mathematician and logician. ... David A. Turner is a prominent British computer scientist. ...

T[V] => V
T[(E1 E2)] => (T[E1] T[E2])
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.(E1 E2)] => (S T[λx.E1] T[λx.E2]) (if x is free in both E1 and E2)
T[λx.(E1 E2)] => (C T[λx.E1] T[E2]) (if x is free in E1 but not E2)
T[λx.(E1 E2)] => (B T[E1] T[λx.E2]) (if x is free in E2 but not E1)

Using B and C combinators, the transformation of λx.λy.(y x) looks like this:

 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) = C_*(traditional canonical notation : X_* = X I) = I'(traditional canonical notation: X' = 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 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 Schönfinkel's original paper, what we now call S, K, I, B and C were called S, C, I, Z, and T respectively. Haskell Brooks Curry (September 12, 1900, Millis, Massachusetts - September 1, 1982, State College, Pennsylvania) was an American mathematician and logician. ... Haskell Curry, in his doctoral thesis Grundlagen der kombinatorischen Logik [GKL], already proposed a system with separated functional characteristics: association, conversion, cancellation and duplication. ... Moses SchÃ¶nfinkel, also known as Moisei Isaievich Sheinfinkel Ð¨ÐµÐ¹Ð½Ñ„Ð¸Ð½ÐºÐµÐ»ÑŒ (September 4, 1889 Ekaterinoslav â€“ 1942, Moscow) was a Russian logician and mathematician. ...

CL_K versus CL_I calculus

A distinction must be made between the CL_K as described in this article and the CL_I calculus. The distinction corresponds to that between the λ_K and the λ_I calculus. Unlike the λ_K calculus, the λ_I calculus restricts abstractions to:

λv.E1 where v has at least one free occurrence in E1.

As a consequence, combinator K is not present in the λ_I calculus nor in the CL_I calculus. The constants of CL_I are: I, B, C and S, which form a basis from which all CL_I terms can be composed (modulo equality) Together, B and C simulate K. Every λ_I term can be converted into an equal CL_I combinator according to rules similar to those presented above for the conversion of λ_K terms into CL_K combinators. See chapter 9 in Barendregt (1984).

Reverse conversion

The conversion L[ ] from combinatorial terms to lambda terms is trivial:

 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[(E1 E2)] = (L[E1] L[E2])

Note, however, that this transformation is not the inverse transformation of any of the versions of T[ ] that we have seen.

Undecidability of combinatorial calculus

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, 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

 (N x) => T, if x has a normal form F, otherwise.

(Where T and F the transformations of the conventional lambda-calculus definitions of true and false, λx.λy.x and λx.λy.y. The combinatory versions have T = K and 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:

 (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:

 (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:

 (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 NA=T and NB=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. Rices theorem (also known as The Rice-Myhill-Shapiro theorem) is an important result in the theory of recursive functions. ...

Applications

Compilation of functional languages

Functional programming languages are often based on the simple but universal semantics of the lambda calculus. Functional programming is a programming paradigm that treats computation as the evaluation of mathematical functions. ... The lambda calculus is a formal system designed to investigate function definition, function application, and recursion. ...

David Turner used his combinators to implement the SASL programming language. SASL (from St. ...

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 a clumsier manner in any APL-like language with user-defined operators (Pure Functions in APL and J). Kenneth Eugene Iverson (17 December 1920, Camrose, Alberta, Canada â€“ 19 October 2004, Toronto, Ontario, Canada) was a computer scientist most notable for developing the APL programming language in 1957. ... The J programming language, developed in the early 1990s by Ken Iverson and Roger Hui, is a synthesis of APL (also by Iverson) and the FP and FL functional programming languages created by John Backus (of FORTRAN, ALGOL, and BNF fame). ... APL (for A Programming Language) is an array programming language based on a notation invented in 1957 by Kenneth E. Iverson while at Harvard University. ...

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 (consisting of axioms and rules) in proof theory. The Curry-Howard correspondence is the close relationship between computer programs and mathematical proofs; the correspondence is also known as the Curry-Howard isomorphism, or the formulae-as-types correspondence. ... Intuitionistic logic, or constructivist logic, is the logic used in mathematical intuitionism and other forms of mathematical constructivism. ... Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. ...

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 A is a subset of B, and B is a superset of A. In mathematics, especially in set theory, the terms, subset, superset and proper (or strict) subset or superset are used to describe the relation, called inclusion, of one set being contained inside another set. ... Kripke semantics (also known as possible world semantics, relational semantics, or frame semantics) is a formal semantics for modal logic systems, created in late 1950s and early 1960s by Saul Kripke. ...

$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$ . In mathematical logic, the deduction theorem states that if a formula F is deducible from E then the implication E â†’ F is demonstrable (i. ...

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.

References

Moses Schönfinkel, 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.
Curry, Haskell B.; Robert Feys (1958). Combinatory Logic Vol. I. Amsterdam: North Holland.
Curry, Haskell B.; J. Roger Hindley and Jonathan P. Seldin (1972). Combinatory Logic Vol. II. Amsterdam: North Holland. ISBN 0-7204-2208-6.
Field, Anthony J. and Peter G. Harrison, 1998. Functional Programming. . Addison-Wesley. ISBN 0-201-19249-7
Paulson, Lawrence C., 1995. Foundations of Functional Programming. University of Cambridge.
Sørensen, Morten Heine B. and Paweł Urzyczyn, 1999. Lectures on the Curry-Howard Isomorphism. University of Copenhagen and University of Warsaw, 1999.
1920-1931 Curry's block notes
Hindley, Roger, and Meredith, 1990, "Principal Type-Schemes and Condensed Detachment," Journal of Symbolic Logic 55: 90-105
Hendrik Pieter Barendregt, 1984. The Lambda Calculus, Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, Volume 103, North-Holland. ISBN 0-444-87508-5
Quine, W. V., 1960 "Variables explained away", Proceedings of the American Philosophical Society 104:3:343-347 (Jun. 15, 1960) at JSTOR. Reprinted as Chapter 23 of Quine's Selected Logic Papers (1966), pp. 227–235

Moses SchÃ¶nfinkel, also known as Moisei Isaievich Sheinfinkel Ð¨ÐµÐ¹Ð½Ñ„Ð¸Ð½ÐºÐµÐ»ÑŒ (September 4, 1889 Ekaterinoslav â€“ 1942, Moscow) was a Russian logician and mathematician. ... Jean van Heijenoort (prounounced highenort) (July 23, 1912, Creil France - March 29, 1986, Mexico City) was a pioneer historian of mathematical logic. ... Hendrik Pieter (Henk) Barendregt (b. ... For people named Quine, see Quine (surname). ...

External links

"Drag 'n' Drop Combinators (Java Applet)"

Contents

Combinatory logic in mathematics

Combinatory logic in computing

Summary of the lambda calculus

Combinatory calculi

Combinatory terms

Examples of combinators

Completeness of the S-K basis

Conversion of a lambda term to an equivalent combinatorial term

Explanation of the T[ ] transformation

Simplifications of the transformation

η-reduction

One point basis

Combinators B, C

CL_K versus CL_I calculus

Reverse conversion

Undecidability of combinatorial calculus

Applications

Compilation of functional languages

Logic

See also

References

External links

Further reading

Contents

Combinatory logic in mathematics GA_googleFillSlot("encyclopedia_square");

Combinatory logic in computing

Summary of the lambda calculus

Combinatory calculi

Combinatory terms

Examples of combinators

Completeness of the S-K basis

Conversion of a lambda term to an equivalent combinatorial term

Explanation of the T[ ] transformation

Simplifications of the transformation

η-reduction

One point basis

Combinators B, C

CLK versus CLI calculus

Reverse conversion

Undecidability of combinatorial calculus

Applications

Compilation of functional languages

Logic

See also

References

External links

Further reading

Combinatory logic in mathematics

CL_K versus CL_I calculus