The tale of the “Devil of the Excluded Middle” appears in [Wadl03] as a humorous sketch depicting the execution of a program typed by the law of the excluded middle. With apologies to Wadler, I reproduce it here: Once upon a time, the devil approached a man and made an offer: “Either (a) I will give you one billion dollars, or (b) I will grant you any wish if you pay me one billion dollars.

This post is based on a lovely article on “Deriving the \(Y\) Combinator”. In a course on programming language fundamentals, our lecturer proved the Turing completeness of untyped \(\lambda\) calculus by encoding Gödel’s recursive functions into the calculus. This proof included a translation of the primitive recursion operation into a parametrized extension of the much simpler function composition operation. Sadly, the rigid nature of this translation meant that he needed new ideas to encode the \(\mu\)-operator.