5 ms·

Compiling to lambda-calculus: Turtles all the way down

86 points by budu 16y ago

shasta 16y ago
"The other direction requires more thought: how do you coax such a simple language into providing the features we expect of a modern programming language, such as numbers, Booleans, conditionals, lists and recursion? " No, the other direction requires simulating a Turing machine with lambda calculus.
- mattmight 16y ago
  Good point. But, those are exactly the language features that make it easy to implement a Turing machine.
  - davidmathers 16y ago
    That really is a strange paragraph. Turing machines only consist of a line of memory cells, a pointer to the current cell, and a CRUD mechanism for the cells.
    - joelhaasnoot 16y ago
      See http://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis http://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis Labda Calculus can be shown equivalent to Turing machines.
      - davidmathers 16y ago
        Sure, but the otherwise excellent OP isn't about that. It's about building higher level concepts out of the lambda calculus. Nothing to do with Turing machines. Turing machines and lambda calculus are both foundational languages on top of which those higher level concepts can be constructed. How to translate back and forth from Turing machine to lambda calculus is something I really want to understand actually. I've been meaning to sit down and figure it out but haven't done it yet.
        mattmight 16y ago
        Thanks for your feedback. I tweaked the abstract a bit to reflect your point. I'll do a follow-on post on how to explicitly reduce the lambda calculus to Turing machines and vice versa. Most of the hard work is done with this post.
        TheSOB88 16y ago
        Some things just don't have an algorithm. You have to figure out each case by itself.
  - jacquesm 16y ago
    Hey Matt, Just a quick little note to thank you for your series of posts, not just this one. I've been trying to get my head wrapped around the lambda calculus and your posts have been by far the most enlightening ones on the subject. Thank you very much!
    - mattmight 16y ago
      Thanks for reading! I'll keep the posts coming.
joelhaasnoot 16y ago
"Barendregt is a helluva drug." Not sure I agree: his lectures are quite sleep inducing these days. Though reducing programming to something so simple and mathematical does open lots of possibilities...
- mattmight 16y ago
  That thick yellow book rocked my world once upon a time. Never saw him lecture though.
  - joelhaasnoot 16y ago
    He teaches classes at the Radboud University in Nijmegen, the Netherlands, specifically my "Languages and automata/machines" class. He has a "zen" something going on with lots of interesting comments.
  - mahmud 16y ago
    How did you keep it together? The binding is so bad, you can't open it up more than 45 degrees.
binarymax 16y ago
I don't fully understand lambda calculus, but i inferred a stack overflow from his tattoo? Went to buy the book and its beyond my budget at the moment ($215 on Amazon).
- mattmight 16y ago
  It's a tattoo of the call-by-name Y combinator. You'll get a stack overflow in a strict language, but not a lazy one.
- mindcrime 16y ago
  $215? When I clicked through to the book, I see "Available from these sellers. 9 used from $597.95" WTF?!?? http://www.amazon.com/gp/product/0444875085 http://www.amazon.com/gp/product/0444875085
  - nitrogen 16y ago
    Click on the hardcover edition link.
    - mindcrime 16y ago
      Aaah, I see. Still, I give a big "WTF?!??" to the idea of paying $597 for any version of this book. I mean, I'm sure it's a good book, but $597 worth???? Heck, even $215 seems a bit crazy.
- 1331 16y ago
  Though incomparable to the book, you may be interested in a free introduction by the author: ftp://ftp.cs.ru.nl/pub/CompMath.Found/lambda.pdf
joshrule 16y ago
I'm always a bit awed when recognizable functions like 'if' and 'let' start emerging from a mess of lambdas and Xs. It amazing how simple items and simple rules can combine to create fantastically intricate systems (i.e. the entire space of computable functions). Thanks for sharing, Matt.
fexl 16y ago
I've been working on a combinatoric approach with Fexl, "compiling" all the way down to my two turtles S and C, e.g.: http://fexl.com/blog/9 http://fexl.com/blog/9 I'm also relying on two higher-level combinators L and R to reduce the size of the combinatorial forms, e.g.: http://fexl.com/blog/10 http://fexl.com/blog/10 The bottom line is that the entire Fexl parser is defined in terms of the two primitive combinators S and C.
- iam 16y ago
  I was confused a while till I saw you talking about Moses Schönfinkel. From everything I've seen people usually refer to those as SK combinators not SC combinators.
  - fexl 16y ago
    Right, that's "K" as in "Konstanzfunktion" in the original German. The book "From Frege to Gödel" uses "C" as in "Constancy Function" in English, and I got in the habit of using that.
sb 16y ago
While this is a nice article on compiling to lambda calculus, the uninitiated might find Barendregt's "Introduction to Lambda Calculus" (ftp://ftp.cs.ru.nl/pub/CompMath.Found/lambda.pdf) an invaluable resource. (IMHO, it's the best work for groking lambda calculus, at least it was for me and my learning prefernece/style)
iam 16y ago
Nothing like posting a picture of the y-combinator on a ycombinator.com site :)

86 points by budu 16y ago

"The other direction requires more thought: how do you coax such a simple language into providing the features we expect of a modern programming language, such as numbers, Booleans, conditionals, lists and recursion? " No, the other direction requires simulating a Turing machine with lambda calculus.

mattmight 16y ago
Good point. But, those are exactly the language features that make it easy to implement a Turing machine.
- davidmathers 16y ago
  That really is a strange paragraph. Turing machines only consist of a line of memory cells, a pointer to the current cell, and a CRUD mechanism for the cells.
  - joelhaasnoot 16y ago
    See http://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis http://en.wikipedia.org/wiki/Church%E2%80%93Turing_thesis Labda Calculus can be shown equivalent to Turing machines.
    - davidmathers 16y ago
      Sure, but the otherwise excellent OP isn't about that. It's about building higher level concepts out of the lambda calculus. Nothing to do with Turing machines. Turing machines and lambda calculus are both foundational languages on top of which those higher level concepts can be constructed. How to translate back and forth from Turing machine to lambda calculus is something I really want to understand actually. I've been meaning to sit down and figure it out but haven't done it yet.
      - mattmight 16y ago
        Thanks for your feedback. I tweaked the abstract a bit to reflect your point. I'll do a follow-on post on how to explicitly reduce the lambda calculus to Turing machines and vice versa. Most of the hard work is done with this post.
      - TheSOB88 16y ago
        Some things just don't have an algorithm. You have to figure out each case by itself.
- jacquesm 16y ago
  Hey Matt, Just a quick little note to thank you for your series of posts, not just this one. I've been trying to get my head wrapped around the lambda calculus and your posts have been by far the most enlightening ones on the subject. Thank you very much!
  - mattmight 16y ago
    Thanks for reading! I'll keep the posts coming.

joelhaasnoot 16y ago

"Barendregt is a helluva drug." Not sure I agree: his lectures are quite sleep inducing these days. Though reducing programming to something so simple and mathematical does open lots of possibilities...

mattmight 16y ago
That thick yellow book rocked my world once upon a time. Never saw him lecture though.
- joelhaasnoot 16y ago
  He teaches classes at the Radboud University in Nijmegen, the Netherlands, specifically my "Languages and automata/machines" class. He has a "zen" something going on with lots of interesting comments.
- mahmud 16y ago
  How did you keep it together? The binding is so bad, you can't open it up more than 45 degrees.

binarymax 16y ago

I don't fully understand lambda calculus, but i inferred a stack overflow from his tattoo? Went to buy the book and its beyond my budget at the moment ($215 on Amazon).

mattmight 16y ago
It's a tattoo of the call-by-name Y combinator. You'll get a stack overflow in a strict language, but not a lazy one.
mindcrime 16y ago
$215? When I clicked through to the book, I see "Available from these sellers. 9 used from $597.95" WTF?!?? http://www.amazon.com/gp/product/0444875085 http://www.amazon.com/gp/product/0444875085
- nitrogen 16y ago
  Click on the hardcover edition link.
  - mindcrime 16y ago
    Aaah, I see. Still, I give a big "WTF?!??" to the idea of paying $597 for any version of this book. I mean, I'm sure it's a good book, but $597 worth???? Heck, even $215 seems a bit crazy.
1331 16y ago
Though incomparable to the book, you may be interested in a free introduction by the author: ftp://ftp.cs.ru.nl/pub/CompMath.Found/lambda.pdf

joshrule 16y ago

I'm always a bit awed when recognizable functions like 'if' and 'let' start emerging from a mess of lambdas and Xs. It amazing how simple items and simple rules can combine to create fantastically intricate systems (i.e. the entire space of computable functions). Thanks for sharing, Matt.

fexl 16y ago

I've been working on a combinatoric approach with Fexl, "compiling" all the way down to my two turtles S and C, e.g.: http://fexl.com/blog/9 http://fexl.com/blog/9 I'm also relying on two higher-level combinators L and R to reduce the size of the combinatorial forms, e.g.: http://fexl.com/blog/10 http://fexl.com/blog/10 The bottom line is that the entire Fexl parser is defined in terms of the two primitive combinators S and C.

iam 16y ago
I was confused a while till I saw you talking about Moses Schönfinkel. From everything I've seen people usually refer to those as SK combinators not SC combinators.
- fexl 16y ago
  Right, that's "K" as in "Konstanzfunktion" in the original German. The book "From Frege to Gödel" uses "C" as in "Constancy Function" in English, and I got in the habit of using that.

sb 16y ago

While this is a nice article on compiling to lambda calculus, the uninitiated might find Barendregt's "Introduction to Lambda Calculus" (ftp://ftp.cs.ru.nl/pub/CompMath.Found/lambda.pdf) an invaluable resource. (IMHO, it's the best work for groking lambda calculus, at least it was for me and my learning prefernece/style)

iam 16y ago

Nothing like posting a picture of the y-combinator on a ycombinator.com site :)