Home

Church’s Thesis and Functional Programming

David Turner gives a condensed summary of the lambda calculus and functional programming in this paper on Church’s Thesis and Functional Programming.

The lambda-calculus, which Church developed during the period of convergence from which the Thesis emerged, has influenced almost every aspect of the development of programming and programming languages. It is the basis of functional programming, which after a long infancy is entering adulthood as a practical alternative to traditional ad-hoc imperative programming languages. Many important ideas in mainstream programming languages—recursion, procedures as parameters, linked lists and trees, garbage collectors — came by cross fertilization from functional programming. Moreover the main schools of both operational and denotational semantics are lambda-calculus based and amount to using functional programming to explain other programming systems.

The original project from whose wreckage by paradox lambda-calculus survived, to unify logic with an account of computable functions, appears to have been reborn in unexpected form, via the propositions-as-types paradigm.

Many of the PLT topics mentioned on LtU are covered - PLT in 20 pages or less. I'm still hoping for someone to publish a pop-PLT book that takes something like these 20 pages and turns them into a 800 page novel. In the meantime, this is a nice roadmap for PLT that helps provide the connections between such things as Curry-Howard, Coq, System F. (About as close to a cheatsheet for LtU that I've come across).

By Chris Rathman at 2007-04-20 05:08 | Theory | other blogs | 28176 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Holy Cow!

This thing is awesome! It most definitely belongs at the top of the "Getting Started" page, IMHO, as it is indeed an excellent summary of what many (most?) of us discuss here. I'll no doubt refer to it often as I muddle through my self-study efforts.

By Paul Snively at Fri, 2007-04-20 15:02 | login or register to post comments

Thanks!

Nice post.

By James Roome at Fri, 2007-04-20 18:07 | login or register to post comments

I am an amateur beginner and

I am an amateur beginner and I was just wondering if by

What we get from untyped [lambda]-calculus, or a typed calculus with N and general recursion, are the sequential functions. To get all computable partial functions at every type we must add primitives expressing interleaving or concurrency. In fact just the two above are sufficient. [p. 13]

the author means concurrency is beyond lambda calculus. also, does he mean interleaving and concurrency are synonymous or does he mean either of the two will suffice?

thanks in advance.

By uchchwhash at Sun, 2007-04-22 09:27 | login or register to post comments

Interleaving and Concurency

I'm thinking that interleaving refers to things like coroutines, which is not the same thing as concurrency.

Pi-Calculus would be a place to look for concurrency.

By Chris Rathman at Sun, 2007-04-22 13:49 | login or register to post comments

Concurrency

What the author means, in this case, is that there is no way in lambda-calculus to write the function "or" which takes two booleans and returns a boolean, in such a way that it terminates successfully if either of the two inputs terminates with a "True" result.

For example, borrowing some syntax from Haskell:
undefined = undefined

undefined is an expression which creates an infinite loop when evaluated (a non-terminating expression).

or1 x y = if x then True else y
or2 x y = if y then True else x

or1 and or2 return the same result if both x and y terminate, but in the case that one of them goes into an infinite loop and the other returns true, they have different behavior:

> or1 True undefined => True
> or2 True undefined => infinite loop
> or1 undefined True => infinite loop
> or2 undefined True => True

"Parallel or" solves this problem; conceptually, parallel-or begins executing both x and y in parallel, and as soon as either of them terminates with a True result, the other result is no longer needed and we can stop trying to calculate it. This isn't possible in lambda calculus without this additional primitive.

By Ryan Ingram at Wed, 2007-06-27 23:02 | login or register to post comments

Quibble

David Turner claims that Martin-Löf's type theory has the strong-normalisation property: in the presence of predicative universes there are terms with weak-head normal forms but not full normal forms.

By Charles Stewart at Tue, 2007-04-24 12:22 | login or register to post comments

Nice!

I finally got around to this. I agree it's a really excellent survey and is a great place to start. It says it's from Church's Thesis after 70 Years, and makes some tantalizing references to other articles in the same volume. Sadly, the book has a pretty hefty price tag, and I'm curious if anyone has actually seen it, and whether the rest of the book is equally good...

By Matt Hellige at Mon, 2007-05-07 21:43 | login or register to post comments

eBook

Church's Thesis after 70 Years is also available as an eBook for Windows, at about 1/6 the price.

By Scott Turner at Tue, 2007-05-08 15:36 | login or register to post comments

Curry-Howard Isomorphism

Highly recommended if only for the wonderfully clear explanation of the Curry-Howard isomorphism (in the section "Propositions-as-Types", pp. 14-15).

By namin at Tue, 2008-07-22 00:14 | login or register to post comments