Talk:SKI combinator calculus

86.82.44.193 (talk) 14:24, 22 July 2017 (UTC) Can someone rewrite or remove the lines in informal introduction? It really reads like if someone who shouldn't be understanding this is grappling with the basic concepts of a combinator system and is poorly written..

How is this page related to the Combinatory Logic page [1] ? I am surprised not to see Curry in the references here (in particular the book Combinatory Logic by Curry and Feys 1958).

JulienCo (talk) 11:36, 5 July 2016 (UTC)

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:

$ix=x\mathbf {SK}$

I find this unconvincing - $i$ is defined in terms of S and K, which means the system needs three combinators. If you could define i in terms of itself only, then I'd be convinced. I doubt this is possible, but I would be pleased if someone could prove me wrong! The iota language in the link uses S and K internally, it's just in the syntax that it is forbidden.

So I think this might mislead readers into thinking that single combinator systems are possible. Can anyone provide a more compelling example or clarify somehow?

86.82.44.193 (talk) 14:24, 22 July 2017 (UTC) It is well-known that a minimal system consisting out of one combinator and even defined by only one equality exists. I've read a paper on it but fail to remember the author. Some Dutch guy.

Edwin 20:17, 14 May 2006 (UTC)

JA: The statement above is just the usual reduction of I to S and K, which gets it down to two. The reduction to one is rather artificial, but does it in terms of a combinator J. You can find that discussed in van Heijenoort's anthology. Jon Awbrey 20:40, 14 May 2006 (UTC)

Of course you can define $i$ in terms of $i$.

$i=\lambda x.x\mathbf {SK}$

By abstraction elimination,

$i=\mathbf {S(SI(KS))(KK)}$

On the iota page, translations for S, K and I to i are given. Performing these, we get

$i=***i*i*i*ii***i*i*i*ii*ii**i*i*ii*i*i*i*ii**i*i*ii*i*i*ii$

I haven't checked this to be correct. There are other one combinator bases that give shorter translations for S and K. Two of these are $\lambda f.f\mathbf {S} (\lambda xyz.x)$ and $\lambda f.f\mathbf {I(K(K(KS)))(KK)}$

--Bsmntbombdood 05:40, 17 February 2007 (UTC)

Not

I'm probably missing something, but i'm confused by the postfix NOT in the article. it says "(T) NOT = T(F)(T) = F", but NOT is a unary function that applies its (binary function) argument to T and F, and T is a binary function that returns its first argument, so what we really want to do is apply NOT to T. Am I getting confused by the notation? Example in ML:

fun T x y = x;
fun F x y = y;
fun NOT x = x F T;

(NOT T) 1 2 -> 2 (it returned the second argument, so it's F)

Moe Aboulkheir 07:21, 18 August 2006 (UTC)

NOT is not really a unary function the way it's defined in the article, it's just a pair of arguments supplied to the function that appears to its left. For example, "T NOT" = "T F T" = "F" because "T x y = x". I don't really understand what you're asking. Jon Purdy 07:22, 27 September 2006 (EDT)

If you're still interested in this, NOT can be defined as a prefix function like this:

NOT = (S (S I) (S S (K (K K))))

where I = (S K K). Then NOT (K I) = K, and NOT K = (K (S K (K K))) which is extensionally equal to (K I). I discovered the expression through a computer search. TomCubed (talk) 07:22, 30 May 2008 (UTC)

Authorship

An external link says:

Drakos, Nikos, and Moore, Ross (1993-99) "The SKI Combinator Calculus as a Universal System."

when, in fact, Drakos and Moore are authors of the LaTeX2HTML-software used to generate the linked page. Changing to Mike O'Donnell who appers to be the author. 89.27.19.182 (talk) 19:23, 15 February 2008 (UTC)

K and S arising from the exponential monad on a cartesian closed category

Lambda calculus gives rise to a notion of cartesian closed category. S and K can be defined generally for such a category as follows: Given a monad (T,η,µ) on C, define the forgetful functor U : Kl(T) → C (where Kl(T) is the Kleisli category of the monad T) by UA = A, Uf = μ_Tf. Then K and S arise as, respectively, η and the morphism part of U for the monad —^A for all objects A (the covariant exponential functor for A : C). (The "morphism part of U" is the operation called "bind" or ">>=" in functional programming languages with monads.)

I would add this as an extra section, but it would probably be considered original research because I came up with this description from memory (with some help from Abstract and Concrete Categories by Adámek et al) and I can't find any citations for its content. Also I'm not sure it explains how S can be a morphism (or maybe natural transformation) in such a category. Can anyone help here? Hairy Dude (talk) 21:10, 23 October 2009 (UTC)

Historical timeline of SKI Calculus and Lambda Calculus

In the article, it says that

SKI combinator calculus is a computational system that may be perceived as a reduced version of untyped Lambda calculus.

This is indeed a good way to think about it, and it is also the way it is usually taught, but historically, Combinator Calculus actually predates Lambda Calculus.

Because of the way Combinator Calculus is usually taught, there is a common misconception that it is based on Lambda Calculus. It would be nice to explicitly spell out somewhere that this is in fact not true. In this article, the only indication of this is the "may be percieved" portion of the sentence I quoted above.

It is implicit, of course, in the publication dates of the papers in the references section of the Lambda calculus and Combinatory logic pages, but it would be nice to make it more explicit.

Could someone who actually speaks English natively take a stab at this? --jwmittag (talk) 13:37, 16 September 2010 (UTC)

I'll have a stab at this tomorrow, but in the meantime I note that this article has no primary references (e.g. the names Curry and Schönfinkel are entirely absent). So this "implicit" information isn't really present in this article right now. Hairy Dude (talk) 00:20, 19 September 2010 (UTC)

I was wondering the same sort of thing: who created the calculus and when. (Jkauzlar (talk) 00:25, 1 February 2011 (UTC))

Unlambda and Lazy K references

These esoteric languages, Unlambda and Lazy K, are based in S K I calculus, maybe they deserve to be included in this article.

Patillotes (talk) 19:35, 17 June 2011 (UTC)

Ooops, I'm sorry, now I see the link to Unlambda. Patillotes (talk) 19:39, 17 June 2011 (UTC)

Implementations

Would it be worth linking to current implementations of SKI combinator calculus? I know nothing of SKI, very little of Lambda calculus, and my functional programming experience is currently Clojure, but I am very interested in a minimal and complete implementation of something like SKI or minimal lambda calculus syntax. I would happily link to the implementations I've found, but it's my feeling that this is best handled by an expert in lambda calculus, functional programming or SKI. Would people be against having implementations being linked to? This is an exciting development in functional languages, and I'd love for people to easily be able to go to a given (hopefully open source) implementation of the language spec. Stilroc (talk) 17:03, 10 July 2012 (UTC)

Describe abstraction elimination algorithm?

I wonder if it would be worth adding the algorithm for converting lambda expressions to SKI expressions. What I use to eliminate a single lambda is:

1. Convert $\lambda x\,.\,x$ to $I$.

2. Convert $\lambda x\,.\,y$ to $K~y$ if $y$ is either a free variable other than $x$, or one of the combinators $S$, $K$, $I$. (As an optional optimization, also apply this rule if $y$ is a complex expression in which $x$ is not a free variable.)

3. As an optional optimization, convert $\lambda x\,.\,fx$ to $f$ if $x$ does not appear as a free variable in $f$. ($\eta$ equivalence)

4. Given $\lambda x\,.\,a~b$, recursively convert $\lambda x\,.\,a$ and $\lambda x\,.\,b$ to $A$ and $B$ respectively, and convert $\lambda x\,.\,a~b$ to $S~A~B$.

Then apply this from inside to outside, and the result should be an SKI expression with the same free variables as the original lambda expression.

As examples:

The composition operator is

${\begin{aligned}\circ &=\lambda f~g\,.\,\lambda x\,.\,f(g~x)\\&=\lambda f~g\,.\,S~(K~f)~g\\&=\lambda f\,.\,S~(K~f)\\&=S~(K~S)~K.\end{aligned}}$

For the boolean operator examples:

${\begin{aligned}T&=\lambda x~y\,.\,x\\&=\lambda x\,.\,K~x\\&=K;\end{aligned}}$

${\begin{aligned}F&=\lambda x~y\,.\,y\\&=\lambda x\,.\,I\\&=K~I;\end{aligned}}$

${\begin{aligned}\vee &=\lambda x~y\,.\,x~T~y\\&=\lambda x\,.\,x~T\\&=S~I~(K~T)\\&=S~I~(K~K);\end{aligned}}$

${\begin{aligned}\wedge &=\lambda x~y\,.\,x~y~F\\&=\lambda x\,.\,S~x~(K~F)\\&=S~S~(K~(K~F))\\&=S~S~(K~(K~(K~I)));\end{aligned}}$

${\begin{aligned}\lnot &=\lambda x\,.\,x~F~T\\&=S~(S~I~(K~F))~(K~T)\\&=S~(S~I~(K~(K~I)))~(K~K).\end{aligned}}$

I don't have a reference for this as I came up with this independently; but I seriously doubt this could be new, and in fact I see a previous reference to it on this Talk page.

(Also these are possibly some good examples why SKI combinator calculus isn't really a practical programming language, as simple lambda expressions tend to balloon to insanely large and indecipherable SKI expressions.)

Daniel Schepler (talk) 20:46, 11 December 2014 (UTC)