Rubrication

Recently on Lambda the Ultimate there was a post called "Total Functional Programming".  The title didn't catch my eye particularly, but I tend to read the abstract of any paper that is posted there that doesn't sound terribly boring.  I've found that this is a fairly good strategy since I tend to get very few false positives this way and I'm too busy for false negatives. The paper touches directly and indirectly on subjects I've posted about here before.  The idea is basically to eschew the current dogma that programming languages should be Turing-complete, and run with the alternative to the end of supplying "Total Functional Programming" .  At first glance this might seem to be a paper aimed at "hair-shirt" wearing functional programming weenies.  My reading was somewhat different. Most hobbiest mathematicians have some passing familiarity with "Turing's Halting Problem" and the related "Goedel's Inco...

I just spent a couple of very cold weeks in Anchorage Alaska.  I went out with a bunch of friends to a bar on the night prior to leaving, where I met up with an old friend (and listened to two other friends play music).  I started describing the lambda calculus to him since it is related to my work and he was curious what I was up to.  In any case I found myself unable to produce addition of the church numerals off the top of my head, which I found pretty disturbing since it shows that I probably didn't quite understand it in the first place.  Therefor I sat down this morning to see if I couldn't reconstruct it from first principles.  It turns out that it is relatively easy. First, let us start with a bit of notation, and a description of the lambda calculus .  Since wikipedia describes the lambda calculus in detail, I'll just show how one procedes with calculations.  As examples let us start with the church numerals .  1 = (λf x.f x) 2 = (λf...