Categories: Lambda calculus | Mathematical logic | Functional programming

SKI combinator calculus

SKI combinator calculus is a computational system that is a reduced, untyped version of Lambda calculus. The system states that all operations in Lambda calculus can be expressed in terms of the three combinators $\mathbf{S}$ , $\mathbf{K}$ , and $\mathbf{I}$ .

All functions in this system can be expressed using the alphabet of only $\mathbf{S}$ , $\mathbf{K}$ , $\mathbf{I}$ , and parentheses (used as grouping symbols). Although the most formal representation of this system requires fully balanced parentheses, it is usually simplified for readability by leaving out parentheses on the left (those that do not effect order of operations), as expressions are evaluated left to right.

Contents

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 See also

5 External links

Informal description

Informally, the combinators in this system are defined as follows ( $x$ , $y$ , and $z$ represent expressions made frome the functions $\mathbf{S}$ , $\mathbf{K}$ , and $\mathbf{I}$ , and set values):

$\mathbf{I}$ takes one argument and returns it:

$\mathbf{I}x\to x$

$\mathbf{K}$ takes two arguments, throws away the second, and returns the first:

$\mathbf{K}xy\to x$

$\mathbf{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:

$\mathbf{S}xyz\to xz(yz)$

[1]

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 $\mathbf{I}$ can be expressed in terms of $\mathbf{S}$ and $\mathbf{K}$ . This can be proven by comparing the following expression to the definition of $\mathbf{I}$ above:

$\mathbf{SKK}x \to \mathbf{K}x(\mathbf{K}x) \to x$

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.

$\mathbf{S}$ , $\mathbf{K}$ , and $\mathbf{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 of the form $\alpha(\mathbf{I}\beta)\iota$ , then $Δ$ can also be expressed as the derivation $αβι$ .
If $Δ$ is a derivation of the form $\alpha((\mathbf{K}\beta)\gamma)\iota$ , then $Δ$ can also be expressed as the derivation $αβι$ .
If $Δ$ is a derivation of the form $\alpha(((\mathbf{S}\beta)\gamma)\delta)\iota$ , then $Δ$ can also be expressed as the derivation $α((βδ)(γδ))ι$ .

Assuming a sequence is a valid derivation to begin with, it can be evaluated using these rules. [2]

SKI expressions

Self-application and recursion

$\mathbf{SII}$ is an expression that takes an argument and applies that argument to itself:

$\mathbf{SII}\alpha \to \mathbf{I}\alpha(\mathbf{I}\alpha) \to \alpha\alpha$

One interesting property of this is that it makes the expression $\mathbf{SII}(\mathbf{SII})$ irreducible:

$\mathbf{SII}(\mathbf{SII}) \to \mathbf{I}(\mathbf{SII})(\mathbf{I}(\mathbf{SII})) \to \mathbf{I}(\mathbf{SII})(\mathbf{SII}) \to \mathbf{SII}(\mathbf{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:

$(\mathbf{S}(\mathbf{K}\alpha)(\mathbf{SII}))\beta \to \mathbf{K}\alpha\beta(\mathbf{SII}\beta) \to \alpha(\mathbf{SII}\beta) \to \alpha(\beta\beta)$

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:

$\beta = \mathbf{S}(\mathbf{K}\alpha)(\mathbf{SII})$

then:

$\mathbf{SII}\beta \to \beta\beta \to \alpha(\beta\beta) \to \alpha(\alpha(\beta\beta)) \to \ldots$

The reversal expression

$\mathbf{S}(\mathbf{K}(\mathbf{SI}))(\mathbf{S}(\mathbf{KK})\mathbf{I})$ reverses the following two terms:

$\mathbf{S}(\mathbf{K}(\mathbf{SI}))(\mathbf{S}(\mathbf{KK})\mathbf{I})\alpha\beta \to$

$\mathbf{K}(\mathbf{SI})\alpha(\mathbf{S}(\mathbf{KK})\mathbf{I}\alpha)\beta \to$

$\mathbf{SI}(\mathbf{S}(\mathbf{KK})\mathbf{I}\alpha)\beta \to$

$\mathbf{SI}(\mathbf{KK}\alpha(\mathbf{I}\alpha))\beta \to$

$\mathbf{SI}(\mathbf{K}(\mathbf{I}\alpha))\beta \to$

$\mathbf{SI}(\mathbf{K}\alpha)\beta \to$

$\mathbf{I}\beta(\mathbf{K}\alpha\beta) \to$

$\mathbf{I}\beta\alpha \to \beta\alpha$

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 $\mathbf{T}$ (True) or $\mathbf{F}$ (False) and two arguments, such that:

$\mathbf{T}xy \to x$

and

$\mathbf{F}xy \to y$

The key is in defining the two Boolean expressions. The first works just like one of our basic combinators:

$\mathbf{T} = \mathbf{K}$

$\mathbf{K}xy \to x$

The second is also fairly simple:

$\mathbf{F} = \mathbf{KI}$

$\mathbf{KI}xy\to \mathbf{I}y \to y$

Once True and False are defined, all Boolean logic can be implemented in terms of if-then-else structures.

Boolean $N O T$ (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 = (\mathbf{F})(\mathbf{T}) = (\mathbf{KI})(\mathbf{K})$

If this is put in an if-then-else structure, it can be shown that this has the expected result

$(\mathbf{T})NOT=\mathbf{T}(\mathbf{F})(\mathbf{T})=\mathbf{F}$

$(\mathbf{F})NOT=\mathbf{F}(\mathbf{F})(\mathbf{T})=\mathbf{T}$

Boolean $O R$ (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 = \mathbf{T} = \mathbf{K}$

If this is put in an if-then-else structure, it can be shown that this has the expected result:

$(\mathbf{T})OR(\mathbf{T})=\mathbf{T}(\mathbf{T})(\mathbf{T})=\mathbf{T}$

$(\mathbf{T})OR(\mathbf{F})=\mathbf{T}(\mathbf{T})(\mathbf{F})=\mathbf{T}$

$(\mathbf{F})OR(\mathbf{T})=\mathbf{F}(\mathbf{T})(\mathbf{T})=\mathbf{T}$

$(\mathbf{F})OR(\mathbf{F})=\mathbf{F}(\mathbf{T})(\mathbf{F})=\mathbf{F}$

Boolean $A N D$ (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 = \mathbf{F} = \mathbf{KI}$

If this is put in an if-then-else structure, it can be shown that this has the expected result:

$(\mathbf{T})(\mathbf{T})AND=\mathbf{T}(\mathbf{T})(\mathbf{F})=\mathbf{T}$

$(\mathbf{T})(\mathbf{F})AND=\mathbf{T}(\mathbf{F})(\mathbf{F})=\mathbf{F}$

$(\mathbf{F})(\mathbf{T})AND=\mathbf{F}(\mathbf{T})(\mathbf{F})=\mathbf{F}$

$(\mathbf{F})(\mathbf{F})AND=\mathbf{F}(\mathbf{F})(\mathbf{F})=\mathbf{F}$

Because this defines True, False, $N O T$ (as a postfix operator), $O R$ (as an infix operator), and $A N D$ (as a postfix operator) in terms of SKI notation, this proves that the SKI system can fully express Boolean logic.

External links

Categories: Lambda calculus | Mathematical logic | Functional programming

The contents of this article are licensed from Wikipedia.org under the GNU Free Documentation License. How to see transparent copy

Encyclopedia

Dictionary

Quotes

SKI combinator calculus

Informal description

Formal definition