Talk:SKI combinator calculus

From Wikipedia, the free encyclopedia

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:
i x = 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)

[edit] 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)

[edit] 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)