SKI combinator calculus( http://en.wikipedia.org/wiki/SKI_combinator_calculus )

SKI

SKI combinator calculus is a computational system that may be perceived as a reduced version of untyped lambda calculus.
SKIコンビネータ算法とは、型無しラムダ算法の単純化されたものと言われている計算理論である。
 It can be thought of as a computer programming language, though it is not useful for writing software.
SKIコンビネータは、大きなプログラムを書くのには向いていないが、プログラミング言語と見ることもできる。
 Instead, it is important in the mathematical theory of algorithms because it is an extremely simple Turing complete language.
しかし、これはアルゴリズムの理論としては重要なものである。なぜなら、とても単純ではあるが、チューリング完全であるからである。
All operations in lambda calculus are expressed in SKI as binary trees whose leaves are one of the three symbols S, K, and I (called combinators).
全てのラムダ式は、SKIの二分木として表すことができる。それらの葉はコンビネータと呼ばれるSKIの三つである。
 In fact, the symbol I is added only for convenience, and just the other two suffice for all of the purposes of the SKI system.
実は、Iコンビネータは、利便性の為に存在しているに過ぎない。残りの二つだけで全てのラムダ式をSKIコンビネータに書き換えられる。
Although the most formal representation of the objects in this system requires binary trees, they are usually represented, for typesetability, as parenthesized expressions, either with all the subtrees parenthesized, or only the right-side children subtrees parenthesized. So, the tree whose left subtree is the tree KS and whose right subtree is the tree SK is usually typed as ((KS)(SK)), or more simply as KS(SK), instead of being fully drawn as a tree (as formality and readability would require).
Contents  [hide] 
1 Informal description
2 Formal definition
3 SKI expressions
3.1 Self-application and recursion
3.2 The reversal expression
3.3 Boolean logic
4 Connection to intuitionistic logic
5 See also
6 References
7 External links
[edit]Informal description

Informally, and using programming language jargon, a tree (xy) can be thought of as a "function" x applied to an "argument" y. When "evaluated" (i.e., when the function is "applied" to the argument), the tree "returns a value", i.e., transforms into another tree. Of course, all three of the "function", the "argument" and the "value" are either combinators, or binary trees, and if they are binary trees they too may be thought of as functions whenever the need arises.
The evaluation operation is defined as follows:
(x, y, and z represent expressions made from the functions S, K, and I, and set values):
I returns its argument:
Ix = x
K, when applied to any argument x, yields a one-argument constant function Kx , which, when applied to any argument, returns x:
Kxy = x
S is a substitution operator. It takes three arguments and then returns the first argument applied to the third, which is then applied to the result of the second argument applied to the third. More clearly:
Sxyz = xz(yz)
Example computation: SKSK evaluates to KK(SK) by the S-rule. Then if we evaluate KK(SK), we get K by the K-rule. As no further rule can be applied, the computation halts here.
Note that, for all trees x and all trees y, SKxy will always evaluate to y in two steps, Ky(xy) = y, so the ultimate result of evaluating SKxy will always equal the result of evaluating y. We say that SKx and I are "functionally equivalent" because they always yield the same result when applied to any y.
Note that from these definitions it can be shown that SKI calculus is not the minimum system that can fully perform the computations of lambda calculus, as all occurrences of I in any expression can be replaced by (SKK) or (SKS) or (SK whatever) and the resulting expression will yield the same result. So the "I" is merely syntactic sugar.
In fact, it is possible to define a complete system using only one combinator. An example is Chris Barker's iota combinator, defined as follows:
ιx = xSK
[edit]Formal definition

The terms and derivations in this system can also be more formally defined:
Terms: The set T of terms is defined recursively by the following rules.
S, K, and I are terms.
If τ1 and τ2 are terms, then (τ1τ2) is a term.
Nothing is a term if not required to be so by the first two rules.
Derivations: A derivation is a finite sequence of terms defined recursively by the following rules (where all Greek letters represent valid terms or expressions with fully balanced parentheses):
If Δ is a derivation ending in an expression of the form α(Iβ)ι, then Δ followed by the term αβι is a derivation.
If Δ is a derivation ending in an expression of the form α((Kβ)γ)ι, then Δ followed by the term αβι is a derivation.
If Δ is a derivation ending in an expression of the form α(((Sβ)γ)δ)ι, then Δ followed by the term α((βδ)(γδ))ι is a derivation.
Assuming a sequence is a valid derivation to begin with, it can be extended using these rules. [1]
[edit]SKI expressions

[edit]Self-application and recursion
自己適用(？？)と再帰
SII is an expression that takes an argument and applies that argument to itself:
SIIは一つの引数を取って、それを自身に適用する式である。
SIIα = Iα(Iα) = αα
One interesting property of this is that it makes the expression SII(SII) irreducible:
一つの面白いSIIの性質として、SII(SII)という式はこれ以上簡約できない。
SII(SII) = I(SII)(I(SII)) = I(SII)(SII) = SII(SII)
Another thing that results from this is that it allows you to write a function that applies something to the self application of something else:
(S(Kα)(SII))β = Kαβ(SIIβ) = α(SIIβ) = α(ββ)
This function can be used to achieve recursion.
この式は再帰を実現する為に使うことができる。
 If β is the function that applies α to the self application of something else, then self-applying β performs α recursively on ββ. More clearly, if:
もしβが
β = S(Kα)(SII)
then:
SIIβ = ββ = α(ββ) = α(α(ββ)) = 
[edit]The reversal expression
S(K(SI))K reverses the following two terms:
S(K(SI))Kは後ろに続く二つの項の順序を入れ替える。
S(K(SI))Kαβ →
K(SI)α(Kα)β →
SI(Kα)β →
Iβ(Kαβ) →
Iβα
βα
[edit]Boolean logic
論理演算
SKI combinator calculus can also implement Boolean logic in the form of an if-then-else structure.
SKIコンビネータはif-then-else形式の論理演算をも実装することができる。
 An if-then-else structure consists of a Boolean expression that is either true (T) or false (F) and two arguments, such that:
if-then-else形式は真(T)または偽(F)の項から成り立つ。それぞれは、二つの引数を取り、以下のように定義される。
Txy = x
and
Fxy = y
The key is in defining the two Boolean expressions.
重要なのは二つのブール項の定義である。
The first works just like one of our basic combinators:
(T)は単に基本のコンビネータで表すことができる。
T = K
Kxy = x
The second is also fairly simple:
(F)もまた非常に単純である。
F = KI
KIxy = Iy = y
Once true and false are defined, all Boolean logic can be implemented in terms of if-then-else structures.
真と偽のブール項が定義されると、全ての論理演算を定義できる。
Boolean NOT (which returns the opposite of a given Boolean) works the same as the if-then-else structure, with F and T as the second and third values, so it can be implemented as a postfix operation:
論理否定演算(与えられたブール項と逆の項を返す)は後置演算子として定義できる。
NOT = (F)(T) = (KI)(K)
If this is put in an if-then-else structure, it can be shown that this has the expected result
これがブール項の後ろに置かれると、以下のように期待する結果を得られる。
(T)NOT = T(F)(T) = F
(F)NOT = F(F)(T) = T
Boolean OR (which returns T if either of the two Boolean values surrounding it is T) works the same as an if-then-else structure with T as the second value, so it can be implemented as an infix operation:
論理和(二つの引数のうちどちらかが(T)の時、かつその時に限り(T)を返す)は中置演算子として定義できる。
OR = T = K
If this is put in an if-then-else structure, it can be shown that this has the expected result:
以下のような結果を得る。
(T)OR(T) = T(T)(T) = T
(T)OR(F) = T(T)(F) = T
(F)OR(T) = F(T)(T) = T
(F)OR(F) = F(T)(F) = F
Boolean AND (which returns T if both of the two Boolean values surrounding it are T) works the same as an if-then-else structure with F as the third value, so it can be implemented as a postfix operation:
論理積(二つの引数の両方が(T)であった時、かつその時に限り(T)を返す)は後置演算子として定義できる。
AND = F = KI
If this is put in an if-then-else structure, it can be shown that this has the expected result:
以下の結果を得る。
(T)(T)AND = T(T)(F) = T
(T)(F)AND = T(F)(F) = F
(F)(T)AND = F(T)(F) = F
(F)(F)AND = F(F)(F) = F
Because this defines T, F, NOT (as a postfix operator), OR (as an infix operator), and AND (as a postfix operator) in terms of SKI notation, this proves that the SKI system can fully express Boolean logic.
SKIコンビネータによって(T)、(F)、NOT(後置演算子)、OR(中置演算子)、AND(後置演算子)が定義できたので、SKIシステムはブール代数の全てを表現できることが示された。
[edit]Connection to intuitionistic logic

The combinators K and S correspond to two well-known axioms of sentential logic:
AK: A  (B  A),
AS: (A  (B  C))  ((A  B)  (A  C)).
Function application corresponds to the rule modus ponens:
MP: from A and A  B, infer B.
The axioms AK and AS, and the rule MP are complete for the implicational fragment of intuitionistic logic. In order for combinatory logic to have as a model:
The implicational fragment of classical logic, would require the combinatory analog to the law of excluded middle, e.g., Peirce's law;
Complete classical logic, would require the combinatory analog to the sentential axiom F  A.
[edit]See also

Combinatory logic
B,C,K,W system
Fixed point combinator
Lambda calculus
Functional programming
Unlambda programming language
To Mock a Mockingbird
[edit]References

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. Chpts. 17-20 are a more formal introduction to combinatory logic, with a special emphasis on fixed point results.
[edit]External links

O'Donnell, Mike "The SKI Combinator Calculus as a Universal System."
Keenan, David C. (2001) "To Dissect a Mockingbird."
Rathman, Chris, "Combinator Birds."
""Drag 'n' Drop Combinators (Java Applet)."