February 19th, 2008

beartato phd

(no subject)

Here is a history of the λ-calculus from LtU:

I have not finished reading it, but it seems good.

I usually think of combinators (and across the curry-howard bridge, hilbert-style presentations of logics) as cute but not a serious or important view of logic, but here is a couple of questions anyway:

Recall that in ordinary abstraction elimination with S, K, and I, we get an exponential blowup in the size of the term. Is there any finite set of combinators that does better? Is there a nice generalized notion of combinator that captures deBruijn encoding of terms? I tentatively conjecture no, and yes, respectively. Conjecturing "yes" for hazy "does there exist kinda some way to do this" questions isn't very bold though.


ETA: a moment's thought makes the second trivially true; in fact, the first only really makes sense if I demand the combinators be typed only using simple types and arrow. As soon as you have pairs, deBruijn becomes trivial to code up.
fun one (x, y) = y (* 'a * 'b -> 'b *)
fun up f = (fn (x,y) => f x) (* ('a -> 'b) -> 'a * 'c -> 'b *)
fun s x y z = (x z) (y z) (* ('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c *)
fun lam f = (fn x => fn y => f (x, y)) (* ('a * 'b -> 'c) -> 'a -> 'b -> 'c *)

wjl, I consider this a challenge to you in particular, because I feel tempted again to claim that the direction of associativity matters. The difference between ('a * 'b -> 'c) and ('a -> 'b -> 'c) is that 'b is made available in the first, uncurried form. If you could come up with combinators typeable without product types, that only have some polynomial blowup, then I'll be refuted yet again.