## Programming in Lambda Calculus

Many texts on untyped lambda calculus are heavily loaded with math.

I have tried a different approach to look at lambda calculus from a programming point of view. The results are posted in a little paper on this website.

As a special add-on, I show how to systematically construct algebraic datatypes in lambda calculus.

## Comment viewing options

### History

This sounds like a fun topic, and I look forward to reading it properly (just haven't had time yet). So I'm nit-picking, I s'pose; I wouldn't exactly have said Church created the lambda calculus for the purpose of exploring the limits of computability and decidability. I fear I've got too many details rattling around in my head, putting me at a disadvantage; I don't know what to say briefly.

### Thanks for the hint. Maybe I

Thanks for the hint. Maybe I was a little bit sloppy to say that Church's purpose for inventing the lambda calculus had been to explore the limits of computability.

As you mentioned, Church did a lot of work in formal logic and not only in computability.

But I assume that we agree that the major achievement of Church's lambda calculus had been to demonstrate the existence of noncomputable and undecidable problems. Church's lambda calculus and Turing's automatic machine addressed the "Entscheidungsproblem" nearly at the same time (Church a little bit before) by very different means. And they both proved that Turing machines and lambda calculus are equal in expressive power.

The literature on computability and decidability focuses much more on Turing machines than on lambda calculus. That's a pity, because in my opinion lambda calculus is much more beautiful than Turing machines.

### Elegance

As I understand, he started in logic (I love this reminiscence by a former student) and, yes, did certainly turn very much toward computation. My take these days on lambda-calculus and Turing machines: Of the three main models of computation of the 1930s, proving general recursive functions equi-powerful with lambda-calculus left Church convinced of the full computational generality of both, but didn't really convince Gödel; whereas proving them equi-powerful with Turing machines convinced Gödel. I find this deeply insightful about Turing machines. They're nuts-and-bolts; you can see what they're doing, and believe in it. Since about 1960 (if not earlier) people had been wanting to use lambda-calculus to define the semantics of programming languages, and when Plotkin finally cracked that problem in the mid-seventies, he did it by setting up correspondence theorems between a lambda-style calculus — because that's got the mathematical elegance you want for reasoning about the semantics — and a deterministic operational semantics — ugly mathematically but, like the Turing machine, manifestly describing the very thing whose semantics you want to study.