Church’s Thesis and Functional Programming

(I realise it’s gone very “theory of programming languages” round here lately. Don’t worry, I’m sure I’ll have something else to talk about soon.)

Church’s Thesis and Functional Programming, a lovely little paper by David Turner (he of SASL & Miranda fame). Like the Google Tech Talk I mentioned a couple of days ago, it’s big on unifying historical perspective, which is a welcome change from most of the papers I see on these topics, which seem to assume you’ve either read all the papers they reference (recursively), or you’re about to. ;-)

It’s a veritable concucopial tour of TPL: Church’s thesis; the equivalence of lambda-calculus, Turing machines, and recursive functions; how the halting problem fits into that; the lambda calculus; Church-Rosser; strict vs. non-strict; combinatory logic; typed lambda-calculi; implementation of lazy FP (exemplars Miranda & Haskell); domain theory; FP without general recursion; Curry-Howard; Martin-Lof; and a hint of abstract Stone duality (which always makes me think of Father Stone). Seriously, if you’re at all interested in theoretical computer science, you should definitely take a look at this. I started losing the thread in the final section, but loved the rest and, I think, learnt quite a bit – mainly how various bits fit together; like joining the dots on a map.

(Ooh. Strachey coined the term “syntactic sugar”.)

2 Responses to “Church’s Thesis and Functional Programming”

  1. April 22nd, 2007 | 12:55 am

    I think you’ll find that the word you were looking for was ‘cornucopial’. Concucopial, as any fule kno, is an adjective descriptive of or relating to a collection of concubines.


  2. April 22nd, 2007 | 11:12 am

    Maybe that was what I meant. The Church-Rosser theorem, the Curry-Howard isomorphism, the Y combinator – they are my concubines. ;-)