Talk:SKI combinator calculus

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?

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