SKI combinator calculus

SKI combinator calculus

SKI combinator calculus is a computational system that is a reduced, untyped version of Lambda calculus.

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

Although the most formal representation of the objects in this system requires binary trees, they are usually represented, for typesettability, 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).

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::I"x" → "x"

K, when applied to any argument x, yields a one-argument constant function Kx , which, when applied to any argument, returns x::K"xy" → "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::S"xyz" → "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, and 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 (S K 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 [http://barker.linguistics.fas.nyu.edu/Stuff/Iota/ iota] combinator, defined as follows:: ι"x" = "x"SK

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. [http://people.cs.uchicago.edu/~odonnell/Teacher/Lectures/Formal_Organization_of_Knowledge/Examples/combinator_calculus/]

KI expressions

elf-application and recursion

SII is an expression that takes an argument and applies that argument to itself:: SIIα → Iα(Iα) → αα

One interesting property of this is that it makes the expression SII(SII) irreducible:: 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β → ββ → α(ββ) → α(α(ββ)) → …

The reversal expression

S(K(SI))K reverses the following two terms:: S(K(SI))Kαβ →: K(SI)α(Kα)β →: SI(Kα)β →: Iβ(Kαβ) →: Iβα → βα

Boolean logic

SKI combinator calculus can also implement Boolean logic in the form of an if-then-else structure. An if-then-else structure consists of a Boolean expression that is either T (True) or F (False) and two arguments, such that:: T"xy" → "x"and: F"xy" → "y"

The key is in defining the two Boolean expressions. The first works just like one of our basic combinators:: T = K: K"xy" → "x"

The second is also fairly simple:: F = KI: KIxy" → I"y" → "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 False and True 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 True if either of the two Boolean values surrounding it is True) works the same as an if-then-else structure with True as the second value, so it can be implemented as an infix operation:: OR = T = KIf 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 True if both of the two Boolean values surrounding it are True) works the same as an if-then-else structure with False as the third value, so it can be implemented as a postfix operation:: AND = F = KIIf 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 True, False, 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.

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".

ee also

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

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.

External links

* " [http://c2.com/cgi/wiki?EssAndKayCombinators Ess and Kay Combinators.] "
* O'Donnell, Mike " [http://people.cs.uchicago.edu/~odonnell/Teacher/Lectures/Formal_Organization_of_Knowledge/Examples/combinator_calculus/ The SKI Combinator Calculus as a Universal System.] "
* Keenan, David C. (2001) " [http://users.bigpond.net.au/d.keenan/Lambda/index.htm To Dissect a Mockingbird.] "
* Rathman, Chris, " [http://www.angelfire.com/tx4/cus/combinator/birds.html Combinator Birds.] "
* " [http://cstein.kings.cam.ac.uk/~chris/combinators.html "Drag 'n' Drop Combinators (Java Applet).] "


Wikimedia Foundation. 2010.

Игры ⚽ Нужно решить контрольную?

Look at other dictionaries:

  • Ski (disambiguation) — Ski may refer to: *Ski, a device worn on the feet to slide over snow. * ski, a common ending of surnames of Polish origin. *Ski (driving stunt), a driving stunt where the car is driven while balanced only on two wheels *Ski (producer) An African… …   Wikipedia

  • Lambda calculus — In mathematical logic and computer science, lambda calculus, also written as λ calculus, is a formal system designed to investigate function definition, function application and recursion. It was introduced by Alonzo Church and Stephen Cole… …   Wikipedia

  • Fixed-point combinator — Y combinator redirects here. For the technology venture capital firm, see Y Combinator (company). In computer science, a fixed point combinator (or fixpoint combinator[1] ) is a higher order function that computes a fixed point of other functions …   Wikipedia

  • Fixed point combinator — A fixed point combinator (or fixed point operator) is a higher order function that computes a fixed point of other functions. This operation is relevant in programming language theory because it allows the implementation of recursion in the form… …   Wikipedia

  • Combinatory logic — Not to be confused with combinational logic, a topic in digital electronics. 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… …   Wikipedia

  • B,C,K,W system — The B, C, K, W system is a variant of combinatory logic that takes as primitive the combinators B, C, K, and W. This systems was discovered by Haskell Curry in his doctoral thesis Grundlagen der kombinatorischen Logik , whose results are set out… …   Wikipedia

  • To Mock a Mockingbird — infobox Book | name = To Mock a Mockingbird and Other Logic Puzzles: Including an Amazing Adventure in Combinatory Logic image caption = Cover art for To Mock a Mockingbird author = Raymond Smullyan illustrator = country = United States language …   Wikipedia

  • List of functional programming topics — This is a list of functional programming topics. Contents 1 Foundational concepts 2 Lambda calculus 3 Combinatory logic 4 Intuitionistic logic …   Wikipedia

  • Cálculo lambda — Artículo parcialmente traducido: Contiene texto en inglés. Ayuda a terminarlo. El cálculo lambda es un sistema formal diseñado para investigar la definición de función, la noción de aplicación de funciones y la recursión. Fue introducido por… …   Wikipedia Español

  • Unlambda — is a minimal functional programming language invented by David Madore. It is based on combinatory logic, a version of the lambda calculus that omits the lambda operator. It relies mainly on two built in functions ( s and k ) and an apply operator …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”