Combinatorial Logic

The title of this article is ambiguous. For the network of logic switching elements, which is sometimes also referred to as combinational logic , see switching network .

Combinatorial Logic (abbreviated CL for English. Combinatory Logic) is a notation that of Moses Schönfinkel and Haskell Curry was introduced to the use of variables in mathematical logic to avoid. It is used particularly in computer science as a theoretical model for computation and as a basis for the design of functional programming languages.

Combinatorial Logic in Mathematics

Combinatorial logic was intended to be simpler logic that should clarify the meaning of quantified variables in the notation of logic and actually make them unnecessary.

See Curry, 1958-1972.

Combinatorial Logic in Computer Science

In computer science, the combinatorial logic serves as a simple model of a calculation. This is needed in computability theory and proof theory . Indeed, combinatorial logic encompasses many aspects of natural computation.

The combinatorial logic can be understood as a variation of the lambda calculus , whereby the expressions of the lambda calculus are replaced by a few combiners . Combinators are primitive functions that do not contain free variables. Since it is very easy to convert lambda expressions into terms of the CL, and the reduction of combiners is much easier than the lambda reduction, the CL is often used as an implementation basis for non-strict languages.

There are many other ways of looking at CL, as many earlier papers show the equivalence of different combiners to axioms of logic. [Hindley and Meredith, 1990].

A brief summary of the lambda calculus

A detailed description of the lambda calculus can be found under its article. Lambda terms consist of

• Variables , ${\displaystyle v}$
• abstractions , ${\displaystyle \lambda v.T}$
• Applications , ${\displaystyle (T1~T2)}$

where here for any variable name and , and again for lambda terms. Lambda terms are simplified by beta reduction, where the application is replaced by the replacement . ${\displaystyle v}$ ${\displaystyle T}$ ${\displaystyle {\mathit {T}}1}$ ${\displaystyle T2}$ ${\displaystyle (\lambda v.E)~a}$ ${\displaystyle E[v:=a]}$

The combinatorial logic is a calculation model that is equivalent to the lambda calculus, but does without abstraction.

The combinatorial calculus

Since abstraction is used in the lambda calculus to model functions, there must be something comparable in the combinatorial calculus. Instead of abstraction, there are a few primitive functions ( combiners ) from which further functions can now be put together.

Combinatorial terms

Combinatorial terms consist of

• Combiners ${\displaystyle P}$
• Applications ${\displaystyle (T1~T2)}$

${\displaystyle T1}$and are again combinatorial terms. As in the lambda calculus, the application is left-associative, i.e. it is synonymous with . ${\displaystyle T2}$ ${\displaystyle T1~T2~T3~T4}$ ${\displaystyle (((T1~T2)~T3)~T4)}$

Examples of combiners

${\displaystyle x}$, etc. denote arbitrary terms in the following. ${\displaystyle y}$

The simplest combiner is the identity combiner . For him applies: ${\displaystyle \mathbf {I} }$

${\displaystyle ({\mathbf {I} }~x)=x}$

Another simple combiner is the constant combiner . models a function that always returns for a further argument , so: ${\displaystyle \mathbf {K} }$ ${\displaystyle ({\mathbf {K} }~x)}$ ${\displaystyle x}$

${\displaystyle ({\mathbf {K} }~x~y)=x}$

A third combiner is , it represents a generalized version of the application: ${\displaystyle \mathbf {S} }$

${\displaystyle ({\mathbf {S} }~x~y~z)=(x~z~(y~z))}$

${\displaystyle \mathbf {S} }$turns on to, except that before one in both. ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle z}$

It is actually unnecessary if you have and , because ${\displaystyle \mathbf {I} }$ ${\displaystyle \mathbf {S} }$ ${\displaystyle \mathbf {K} }$

${\displaystyle (({\mathbf {S} }~{\mathbf {K} }~{\mathbf {K} })~x)}$

${\displaystyle =({\mathbf {S} }~{\mathbf {K} }~{\mathbf {K} }~x)}$

${\displaystyle =({\mathbf {K} }~x~({\mathbf {K} }~x))}$

${\displaystyle =x}$.

Fixed point combiner

Even more interesting is the checkpoint combiner used to implement recursion. ${\displaystyle \mathbf {Y} }$

${\displaystyle ({\mathbf {Y} }~{\mathbf {x} })={\mathbf {x} }~({\mathbf {Y} }~{\mathbf {x} })}$

Also is unnecessary. If typing is not required, it can be used as a ${\displaystyle \mathbf {Y} }$

${\displaystyle {\mathbf {Y} }={\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }~({\mathbf {S} }~({\mathbf {K} }~({\mathbf {S} }~{\mathbf {I} }))({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }))}$

being represented.

Completeness of the basis SK

It is astonishing that combiners can be put together from and alone, which are extensionally equal to any arbitrary lambda term, and therefore, according to Church's thesis , extensionally equal to any arbitrary computable function. The proof is a transformation that converts lambda terms into an equivalent CL term. The only requirement is that the lambda term to be transformed does not contain any free variables. ${\displaystyle \mathbf {S} }$ ${\displaystyle \mathbf {K} }$ ${\displaystyle T[~]}$

${\displaystyle T[~]}$ can be defined as follows

1. ${\displaystyle T[V]\Rightarrow V}$
2. ${\displaystyle T[(E1~E2)]\Rightarrow (T[E1]~T[E2])}$
3. ${\displaystyle T[\lambda x.E]\Rightarrow ({\mathbf {K} }~T[E])}$(only if not free in ) ${\displaystyle x}$ ${\displaystyle E}$
4. ${\displaystyle T[\lambda x.x]\Rightarrow {\mathbf {I} }}$
5. ${\displaystyle T[\lambda x.\lambda y.E]\Rightarrow T[\lambda x.T[\lambda y.E]]}$(if free variable of ) ${\displaystyle x}$ ${\displaystyle E}$
6. ${\displaystyle T[\lambda x.(E1~E2)]\Rightarrow ({\mathbf {S} }~T[\lambda x.E1]T[\lambda x.E2])}$

The transformation of a lambda term into a CL term

For example, we're trying to translate the term into a CL term: ${\displaystyle \lambda x.\lambda y.(y~x)}$

${\displaystyle T[\lambda x.\lambda y.(y~x)]}$

${\displaystyle =T[\lambda x.T[\lambda y.(y~x)]]}$ (Rule 5)

${\displaystyle =T[\lambda x.({\mathbf {S} }~T[\lambda y.y]~T[\lambda y.x])]}$ (Rule 6)

${\displaystyle =T[\lambda x.({\mathbf {S} }~{\mathbf {I} }~T[\lambda y.x])]}$ (Rule 4)

${\displaystyle =T[\lambda x.({\mathbf {S} }~{\mathbf {I} }~({\mathbf {K} }~x))]}$ (Rule 3 and rule 1)

${\displaystyle =({\mathbf {S} }~T[\lambda x.({\mathbf {S} }~{\mathbf {I} })]~T[\lambda x.({\mathbf {K} }~x)])}$ (Rule 6)

${\displaystyle =({\mathbf {S} }~({\mathbf {K} }~({\mathbf {S} }~{\mathbf {I} }))~T[\lambda x.({\mathbf {K} }~x)])}$ (Rule 3)

${\displaystyle =({\mathbf {S} }~({\mathbf {K} }~({\mathbf {S} }~{\mathbf {I} }))~({\mathbf {S} }~T[\lambda x.{\mathbf {K} }]~T[\lambda x.x]))}$ (Rule 6)

${\displaystyle =({\mathbf {S} }~({\mathbf {K} }~({\mathbf {S} }~{\mathbf {I} }))~({\mathbf {S} }~({\mathbf {K} }~{\mathbf {K} })~T[\lambda x.x]))}$ (Rule 3)

${\displaystyle =({\mathbf {S} }~({\mathbf {K} }~({\mathbf {S} }~{\mathbf {I} }))~({\mathbf {S} }~({\mathbf {K} }~{\mathbf {K} })~{\mathbf {I} }))}$ (Rule 4)

If we now apply this combiner to two terms and , the reduction looks like this: ${\displaystyle x}$ ${\displaystyle y}$

${\displaystyle ({\mathbf {S} }~({\mathbf {K} }~({\mathbf {S} }~{\mathbf {I} }))~({\mathbf {S} }~({\mathbf {K} }~{\mathbf {K} })~{\mathbf {I} })~x~y)}$

${\displaystyle =({\mathbf {K} }~({\mathbf {S} }~{\mathbf {I} })~x~({\mathbf {S} }~({\mathbf {K} }~{\mathbf {K} })~{\mathbf {I} }~x)~y)}$

${\displaystyle =({\mathbf {S} }~{\mathbf {I} }~({\mathbf {S} }~({\mathbf {K} }~{\mathbf {K} })~{\mathbf {I} }~x)~y)}$

${\displaystyle =({\mathbf {I} }~y~({\mathbf {S} }~({\mathbf {K} }~{\mathbf {K} })~{\mathbf {I} }~x~y))}$

${\displaystyle =(y~({\mathbf {S} }~({\mathbf {K} }~{\mathbf {K} })~{\mathbf {I} }~x~y))}$

${\displaystyle =(y~({\mathbf {K} }~{\mathbf {K} }~x~({\mathbf {I} }~x)~y))}$

${\displaystyle =(y~({\mathbf {K} }~({\mathbf {I} }~x)~y))}$

${\displaystyle =(y~({\mathbf {I} }~x))}$

${\displaystyle =(y~x)}$

The combinatorial representation is much longer than the lambda term . That is typical of the transformation. In general it can happen that a -Construction converts a lambda term of the length into a combiner of the length . ${\displaystyle ({\mathbf {S} }~({\mathbf {K} }~({\mathbf {S} }~{\mathbf {I} }))~({\mathbf {S} }~({\mathbf {K} }~{\mathbf {K} })~{\mathbf {I} }))}$ ${\displaystyle \lambda x.\lambda y.(y~x)}$ ${\displaystyle T[~]}$ ${\displaystyle n}$ ${\displaystyle \Theta (3^{n})}$

Explanation of the T [] transformation

The motivation of the transformation is the elimination of abstractions. Three of the rules are trivial: Rule 4 transforms into its unique equivalence , Rule 3 transforms into , which only works if the bound variable in is not used (ie: in is not free). Rule 2 transforms the application of two terms, which is also allowed in the terms of the CL. ${\displaystyle T[~]}$ ${\displaystyle \lambda x.x}$ ${\displaystyle \mathbf {I} }$ ${\displaystyle \lambda x.E}$ ${\displaystyle ({\mathbf {K} }~T[E])}$ ${\displaystyle x}$ ${\displaystyle E}$ ${\displaystyle E}$

Rule 1 is a bit tricky because it converts variables: variables can only be resolved by rule 4, so they are preserved for now. Since there are no free variables in the overall term and every transformation of abstractions takes the bound variables into account (rules 3, 4, 5, 6), all variables will eventually be resolved.

Rules 5 and 6 move the abstractions inside the function body until they can be resolved by rule 4. Rule 5 first converts the body of the external abstraction, then the abstraction itself. Rule 6 distributes the abstraction over an application to its sub-terms:

${\displaystyle \lambda x.(E1~E2)}$is a function that takes an argument and replaces it in the lambda term for . This is exactly what the combiner does , only for functions or : ${\displaystyle (E1~E2)}$ ${\displaystyle x}$ ${\displaystyle \mathbf {S} }$ ${\displaystyle E1[x]}$ ${\displaystyle E2[x]}$

${\displaystyle (\lambda x.(E1~E2)~a)=((\lambda x.E1~a)~(\lambda x.E2~a))}$

${\displaystyle =({\mathbf {S} }~\lambda x.E1~\lambda x.E2~a)}$

${\displaystyle =(({\mathbf {S} }~\lambda x.E1~\lambda x.E2)~a)}$

Therefore, according to extensional equality:

${\displaystyle \lambda x.(E1~E2)=({\mathbf {S} }~\lambda x.E1~\lambda x.E2)}$

In order to find a combiner for , it is sufficient to find a combiner for , so: ${\displaystyle \lambda x.(E1~E2)}$ ${\displaystyle ({\mathbf {S} }~\lambda x.E1~\lambda x.E2)}$

${\displaystyle ({\mathbf {S} }~T[\lambda x.E1]~T[\lambda x.E2])}$

Simplify the transformation

η reduction

The combinators that yields become shorter if we use the η-reduction from the lambda calculus: ${\displaystyle T[~]}$

${\displaystyle T[\lambda x.(E~x)]=T[E]}$ (only if not free in ) ${\displaystyle x}$ ${\displaystyle E}$

${\displaystyle [[\lambda x.(E~x)]]}$is the function that takes an argument and puts it in the function ; this is extensionally equal to the function itself. It is therefore sufficient to simply transform into its combinatorial form. ${\displaystyle x}$ ${\displaystyle E}$ ${\displaystyle E}$ ${\displaystyle E}$

With this simplification, the above example becomes:

${\displaystyle T[\lambda x.\lambda y.(y~x)]}$

${\displaystyle =\ldots }$

${\displaystyle =({\mathbf {S} }~({\mathbf {K} }~({\mathbf {S} }~{\mathbf {I} }))~T[\lambda x.({\mathbf {K} }~x)])}$

${\displaystyle =({\mathbf {S} }~({\mathbf {K} }~({\mathbf {S} }~{\mathbf {I} }))~{\mathbf {K} })}$ (by η-reduction)

This combiner is (extensionally) equal to the longer one from the previous example:

${\displaystyle ({\mathbf {S} }~({\mathbf {K} }~({\mathbf {S} }~{\mathbf {I} }))~{\mathbf {K} }~x~y)}$

${\displaystyle =({\mathbf {K} }~({\mathbf {S} }~{\mathbf {I} })~x~({\mathbf {K} }~x)~y)}$

${\displaystyle =({\mathbf {S} }~{\mathbf {I} }~({\mathbf {K} }~x)~y)}$

${\displaystyle =({\mathbf {I} }~y~({\mathbf {K} }~x~y))}$

${\displaystyle =(y~({\mathbf {K} }~x~y))}$

${\displaystyle =(y~x)}$

Similarly, the normal -T transformation would turn the identity function into . With the new η-reduction rule it just becomes . ${\displaystyle T[~]}$ ${\displaystyle \lambda f.\lambda x.(f~x)}$ ${\displaystyle ({\mathbf {S} }~({\mathbf {S} }~({\mathbf {K} }~{\mathbf {S} })~({\mathbf {S} }~({\mathbf {K} }~{\mathbf {K} })~{\mathbf {I} }))~({\mathbf {K} }~{\mathbf {I} }))}$ ${\displaystyle \lambda f.\lambda x.(f~x)}$ ${\displaystyle \mathbf {I} }$

The combiners B, C of Curry

The combiners and already immersed in the work of Schönfinkel on (but was there ), Curry led his dissertation basics of combinational logic continues , , (and ) one. and can simplify many reductions, they look like this: ${\displaystyle \mathbf {S} }$ ${\displaystyle \mathbf {K} }$ ${\displaystyle \mathbf {K} }$ ${\displaystyle \mathbf {C} }$ ${\displaystyle \mathbf {B} }$ ${\displaystyle \mathbf {C} }$ ${\displaystyle \mathbf {W} }$ ${\displaystyle \mathbf {K} }$ ${\displaystyle \mathbf {B} }$ ${\displaystyle \mathbf {C} }$

${\displaystyle ({\mathbf {C} }~a~b~c)=(a~c~b)}$

${\displaystyle ({\mathbf {B} }~a~b~c)=(a~(b~c))}$

For these two combiners, the rules are extended as follows:

1. ${\displaystyle T[V]\Rightarrow V}$
2. ${\displaystyle T[(E1~E2)]\Rightarrow (T[E1]~T[E2])}$
3. ${\displaystyle T[\lambda x.E]\Rightarrow ({\mathbf {K} }~T[E])}$(only if not free in ) ${\displaystyle x}$ ${\displaystyle E}$
4. ${\displaystyle T[\lambda x.x]\Rightarrow {\mathbf {I} }}$
5. ${\displaystyle T[\lambda x.\lambda y.E]\Rightarrow T[\lambda x.T[\lambda y.E]]}$(if free variable of ) ${\displaystyle x}$ ${\displaystyle E}$
6. ${\displaystyle T[\lambda x.(E1~E2)]\Rightarrow ({\mathbf {S} }~T[\lambda x.E1]~T[\lambda x.E2])}$(if free variable of and ) ${\displaystyle x}$ ${\displaystyle E1}$ ${\displaystyle E2}$
7. ${\displaystyle T[\lambda x.(E1~E2)]\Rightarrow ({\mathbf {C} }~T[\lambda x.E1]~T[E2])}$(if free variable from but not from ) ${\displaystyle x}$ ${\displaystyle E1}$ ${\displaystyle E2}$
8. ${\displaystyle T[\lambda x.(E1~E2)]\Rightarrow ({\mathbf {B} }~T[E1]~T[\lambda x.E2])}$(if free variable from but not from ) ${\displaystyle x}$ ${\displaystyle E2}$ ${\displaystyle E1}$

For example, the transformation looks like this: ${\displaystyle \lambda x.\lambda y.(y~x)}$

${\displaystyle T[\lambda x.\lambda y.(y~x)]}$

${\displaystyle =T[\lambda x.T[\lambda y.(y~x)]]}$

${\displaystyle =T[\lambda x.({\mathbf {C} }~T[\lambda y.y]~x)]}$ (Rule 7)

${\displaystyle =T[\lambda x.({\mathbf {C} }~{\mathbf {I} }~x)]}$

${\displaystyle =({\mathbf {C} }~{\mathbf {I} })}$ (η reduction)

${\displaystyle ={\mathbf {C} }_{\ast }}$(Notation: ) ${\displaystyle {\mathbf {X} }_{\ast }={\mathbf {X} }~{\mathbf {I} }}$

${\displaystyle ={\mathbf {I} }'}$(Notation: ) ${\displaystyle {\mathbf {X} }'={\mathbf {C} }~{\mathbf {X} }}$

In fact reduced to : ${\displaystyle ({\mathbf {C} }~{\mathbf {I} }~x~y)}$ ${\displaystyle (y~x)}$

${\displaystyle ({\mathbf {C} }~{\mathbf {I} }~x~y)}$

${\displaystyle =({\mathbf {I} }~y~x)}$

${\displaystyle =(y~x)}$

${\displaystyle \mathbf {B} }$and represent limited versions of . While inserting a value into both the applicant and the argument, inserting it only into the applicant and only into the argument. ${\displaystyle \mathbf {C} }$ ${\displaystyle \mathbf {S} }$ ${\displaystyle \mathbf {S} }$ ${\displaystyle \mathbf {C} }$ ${\displaystyle \mathbf {B} }$

Reverse transformation

The transformation of CL terms into lambda terms is very easy, since we have all the options in the lambda calculus that are also available in the CL: ${\displaystyle L[~]}$

${\displaystyle L[{\mathbf {I} }]=\lambda x.x}$

${\displaystyle L[{\mathbf {K} }]=\lambda x.\lambda y.x}$

${\displaystyle L[{\mathbf {C} }]=\lambda x.\lambda y.\lambda z.(x~z~y)}$

${\displaystyle L[{\mathbf {B} }]=\lambda x.\lambda y.\lambda z.(x~(y~z))}$

${\displaystyle L[{\mathbf {S} }]=\lambda x.\lambda y.\lambda z.(x~z~(y~z))}$

${\displaystyle L[(E1~E2)]=(L[E1]~L[E2])}$

It is important to know, however, that this transformation is not the inverse of the -transformation, since it is extensionally the same , but the term is not necessarily retained. ${\displaystyle T[~]}$ ${\displaystyle T[L[x]]}$ ${\displaystyle x}$

Undecidability of the combinatorial calculus

It is undecidable whether a general combiner has a normal form, whether two combiners are equal, etc. This already results from the similarity to the lambda calculus, but here again a direct proof:

The term

${\displaystyle {\mathbf {\Omega } }=({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }~({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }))}$

has no normal form, as it reduces to itself again in three steps:

${\displaystyle ({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }~({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }))}$

${\displaystyle =({\mathbf {I} }~({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} })~({\mathbf {I} }~({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} })))}$

${\displaystyle =({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }~({\mathbf {I} }~({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} })))}$

${\displaystyle =({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }~({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }))}$

and there can't be any other way that makes the combiner shorter.

Now be a combiner that tests for normal form such that ${\displaystyle \mathbf {N} }$

${\displaystyle ({\mathbf {N} }~x)\Rightarrow {\mathbf {T} }}$if has a normal form, ${\displaystyle x}$

${\displaystyle {\mathbf {F} }}$, otherwise.

( and here are the corresponding combiners to and from the lambda calculus: ${\displaystyle \mathbf {T} }$ ${\displaystyle \mathbf {F} }$ ${\displaystyle true}$ ${\displaystyle false}$

${\displaystyle true=\lambda x.\lambda y.x={\mathbf {K} }={\mathbf {T} }}$

${\displaystyle false=\lambda x.\lambda y.y=({\mathbf {K} }~{\mathbf {I} })={\mathbf {F} }}$)

Be now

${\displaystyle Z=({\mathbf {C} }~({\mathbf {C} }~({\mathbf {B} }~{\mathbf {N} }~({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }))~{\mathbf {\Omega } })~{\mathbf {I} })}$

Let's examine the term . Has a normal form? If so, the following derivatives must also have a normal form: ${\displaystyle ({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }~Z)}$ ${\displaystyle ({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }~Z)}$

${\displaystyle ({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }~Z)}$

${\displaystyle =({\mathbf {I} }~Z~({\mathbf {I} }~Z))}$

${\displaystyle =(Z~({\mathbf {I} }~Z))}$

${\displaystyle =(Z~Z)}$

${\displaystyle =({\mathbf {C} }~({\mathbf {C} }~({\mathbf {B} }~{\mathbf {N} }~({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }))~{\mathbf {\Omega } })~{\mathbf {I} }~Z)}$(Definition of ) ${\displaystyle Z}$

${\displaystyle =({\mathbf {C} }~({\mathbf {B} }~{\mathbf {N} }~({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }))~{\mathbf {\Omega } }~Z~{\mathbf {I} })}$

${\displaystyle =({\mathbf {B} }~{\mathbf {N} }~({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} })~Z~{\mathbf {\Omega } }~{\mathbf {I} })}$

${\displaystyle =({\mathbf {N} }~({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }~Z)~{\mathbf {\Omega } }~{\mathbf {I} })}$

Now we turn on to. Either has a normal form or it doesn't. ${\displaystyle \mathbf {N} }$ ${\displaystyle ({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }~Z)}$ ${\displaystyle ({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }~Z)}$

If so, then:

${\displaystyle ({\mathbf {N} }~({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }~Z)~{\mathbf {\Omega } }~{\mathbf {I} })}$

${\displaystyle =({\mathbf {K} }~{\mathbf {\Omega } }~{\mathbf {I} })}$(Definition of ) ${\displaystyle N}$

${\displaystyle ={\mathbf {\Omega } }}$

but has no normal form. we got from derivatives , so it has no normal form. This is a contradiction. ${\displaystyle \mathbf {\Omega } }$ ${\displaystyle \mathbf {\Omega } }$ ${\displaystyle ({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }~Z)}$ ${\displaystyle ({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }~Z)}$

If has no normal form, the term is reduced as follows: ${\displaystyle ({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }~Z)}$

${\displaystyle ({\mathbf {N} }~({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }~Z)~{\mathbf {\Omega } }~{\mathbf {I} })}$

${\displaystyle =({\mathbf {K} }~{\mathbf {I} }~{\mathbf {\Omega } }~{\mathbf {I} })}$(Definition of ) ${\displaystyle \mathbf {N} }$

${\displaystyle =({\mathbf {I} }~{\mathbf {I} })}$

${\displaystyle ={\mathbf {I} }}$

which means that the normal form has simple , so again a contradiction. Hence there cannot be such a combiner . ${\displaystyle ({\mathbf {S} }~{\mathbf {I} }~{\mathbf {I} }~Z)}$ ${\displaystyle \mathbf {I} }$ ${\displaystyle \mathbf {N} }$

application areas

Translation of functional programming languages

Functional programming languages are often based on the simple but universal semantics of the lambda calculus.

David Turner used CL for the SASL language.

credentials

• “On the building blocks of mathematical logic”, Moses Schönfinkel, 1924, translated as “On the Building Blocks of Mathematical Logic” in From Frege to Gödel: a source book in mathematical logic, 1879–1931 , ed. Jean van Heijenoort, Harvard University Press, 1977. ISBN 0-674-32449-8 - The original publication on combinatorial logic.
• Combinatory Logic . Curry, Haskell B. et al. , North-Holland, 1972. ISBN 0-7204-2208-6 - A comprehensive overview of the CL, including the historical outlines.
• Functional programming . Field, Anthony J. and Peter G. Harrison. Addison-Wesley, 1998. ISBN 0-201-19249-7
• "Foundations of Functional Programming" ( GZIP ; 105 kB). Lawrence C. Paulson. University of Cambridge, 1995.
• "Lectures on the Curry-Howard Isomorphism" . Sørensen, Morten Heine B. and Pawel Urzyczyn. University of Copenhagen and University of Warsaw, 1998.
• "Principal Type-Schemes and Condensed Detachment", Hindley and Meredith, Journal of Symbolic Logic (JSL), Volume 55 (1990), Number 1, pages 90-105

Web links

• Katalin Bimbó:  Combinatory Logic. In: Edward N. Zalta (Ed.): Stanford Encyclopedia of Philosophy .