Lambda the Ultimate

... that makes Intercal look easy.

Unlambda

should be

  K : a -> b -> a
  S : (a -> b -> c) -> (a -> b) -> a -> c

as in

Standard ML of New Jersey v110.59 [built: Mon Aug 14 21:39:53 2006]
- fun K x y = x ;
val K = fn : 'a -> 'b -> 'a
- fun S x y z = x z (y z) ;
val S = fn : ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c

My understanding is it's very popular for graph reduction.

Sorta like all those parens in lisp, all those S's and K's start confusing me after a point -- maybe you just have to be smarter than I am to use it. :-)

So the questions I am pondering are: why is the lambda calculus so much more popular?

Because it supports names as a core feature, as well as nested abstractions.

Is it because Scheme and other similar languages more closely resemble the lambda calculus?

It's the other way around. Lambda calculus makes a good model for a programming language, so many languages are based on it.

If there was a language based on the SK calculus, would it become more popular?

See the comment about Unlambda. Of course, you could implement an extended SK calculus with names - but if they're lexically scoped, then you'd either have lambda calculus or a subset of it, and the SK part would be redundant.

I also wonder what applications there are for the SK calculus, and what place it should occupy in my programming language theory arsenal?

Combinator reduction is easier than lambda reduction, so there are applications in the implementation and analysis of functional languages.

Lambda calculus is more popular because the SK calculus is pointless. Er, point-free. I like names, names are good...

Cool to see you posting this though, highlighting corners of theory to poke around with's always fun.

I'm not showing your post on the LtU home page. Probably needs to be promoted by one of the "senior" editors". The "create content" selection is what I think you intended?

As for the topic, the lambda and SK calculus are expressable in each other (though that can be about as useful as saying they are Turing complete, but they are closely related). As I mentioned in another thread, I put together a list of the common combinator birds with a calculator and a stripped down unlambda in javascript (one of those projects that'll probably never finish).

From a PL perspective, it was David Turner's work with the B C K W combinators that made a big breakthrough for lazy evaluation PLs.

This SASL compiler compiles to SK-style combinators. But the problems immediately become apparent. It takes many combinators to do anything. The compiler introduces a bunch of new primitive combinators to deal with the issue. Although they simplify things a little, simple pieces of SASL code can explode into very large combinataions of combinators which in turn are very slow to evaluate.

It's not just practical considerations. When you need to write so many S's and K's, theoretical work becomes hard to read. I know that when implementing SASL for myself it was hard work to read and understand combinator expressions. I won't mention debugging...

There is a fun book on combinatorial calculus.
To Mock a Mockingbird (Paperback)
by Raymond M. Smullyan
http://www.amazon.com/Mock-Mockingbird-Raymond-M-Smullyan/dp/0192801422/sr=8-1/qid=1164990574/ref=pd_bbs_sr_1/102-2040050-9082551?ie=UTF8&s=books

As far as I know, the size of SK expressions can explode during abstraction elemination (i.e., the process of converting lambda expressions to SK expressions). Hence it is just not a very practical way to do programming with, I think.

But SK calculus has always fascinated as being the ultimate "library" (i.e. only reuse/composition of existing parts).

I've found programming in SK-combinators directly to be nearly impossible. I compiled \x.\y.if (< x y) y x into SK-combinators by hand, and the result took me 45 minutes to debug.

But the translation is relatively straightforward. In my DHTML lambda-calculus interpreter, the translation from lambdas into S, K, I, B, and C is about 40 lines of JavaScript, which isn't too horrible. (Except, you know, that it's JavaScript, which isn't very popular, and it's considerably longer than it would be in a language with pattern-matching.) So far I haven't written any significant programs in the lambda-calculus in it, so I don't know to what extent I've avoided the exponential blowup. (In the graph structure. I don't care about exponential blowup in the linearized expression representation of the graph structure, without sharing.)

One of the more complicated examples implements cons, car, cdr, and nil in the pure lambda-calculus, then does this:

map (+ 2) (cons 1 (cons 2 (cons 3 nil)))

or in context:

(\cons.\nil.(\car.\cdr.\map.
                            map (+ 2) (cons 1 (cons 2 (cons 3 nil))))
 (\cons.cons (\car.\cdr.car) x)
 (\cons.cons (\car.\cdr.cdr) x)
 (Y (\map.\f.\list.list (\car.\cdr.cons (f car) 
                                        (map f cdr)) (\ifcons.\ifnil.ifnil)))) 
(\car.\cdr.\ifcons.\ifnil.ifcons car cdr)
(\ifcons.\ifnil.ifnil)

which translates to this:

(S (B C (C (B C (C (B C (B (B K) 
                           (B (B K)
                              (B (B (C (C I (+ 2))))
                                 (S (B B (C I 1))
                                    (S (B B (C I 2))
                                       (C (B B (C I 3)) I)))))))
                   (C (C I (B K I)) x)))
           (C (C I (K I)) x)))
   (B Y (C (B C (B (B C)
                   (B (B (B C)) 
                      (B (B (B (C I)))
                         (C (B B (B S (B (B C) (B (B (B B)) 
                                                  (C (B B (B B I))
                                                     (C (B B I) I))))))
                            (C (B C (B (B B) (C (B B I) I))) I))))))
           (K I))) 
   (B (B (B K)) (C (B B (B C (B (C I) I))) I))
   (K I))

I know I'm not using B*, C', and S', which Peyton-Jones's 1987 book explains are necessary to avoid quadratic blowups on deeply nested variables --- thus the many more levels of nesting in the output than in the input. But I don't know if there's more hidden danger awaiting. What other kinds of expressions cause big blowups?

I'm thinking that Abadi and Cardelli's sigma-calculus might be a nicer basic abstract system to program in directly; it has most of Wouter van Oortmerssen's abstractionless programming already present, and it's even less point-free than the labmda-calculus. It's more complicated than the lambda-calculus by about the same amount that the lambda-calculus is more complicated than SK; there are four expression types.