- Wait, didn’t Yedida and you just disqualified the entry of “BB(10000)” in that game by proving that it’s not computable?

Please see my comment #101 to Ward Cleaver, which answers exactly that.

]]>But come on: it’s not like I said, “unless the mathematics you love helps me with my problem, I’m going to condemn it and ban you from studying it.” I just said I probably won’t get around to studying it *myself*!

But in any case, this time it looks highly plausible that λ-calculus *will* help us—in which case, I will indeed have no choice but to learn it!

That was wonderful essay indeed. IIRC one of the requirement for the game in that essay was that one should name a number that would be unambiguous for a reasonable mathematician… Wait, didn’t Yedida and you just disqualified the entry of “BB(10000)” in that game by proving that it’s not computable? 🙂

]]>The pattern of this remark is familiar to category theorists: “if you can promise that the mathematics you love turns out be the key to solving whatever highly specialized, technical problem I’m interested in at the moment, then I’ll learn it”. And there’s an unspoken addendum: “But otherwise, forget it.” 🙂

Turing machines are idealized, ultra-simple hardware; the λ-calculus is an idealized, ultra-simple programming language. So, their charms are complementary.

]]>An obfuscated C implementation of the Krivine machine is shown at the top of my homepage. ]]>

But John Tromp and Haskell: OK, it sounds like I should just set aside a week sometime to learn how to code in Lisp or Haskell!

]]>You might say, well, that’s not a problem with first order logic, because we know what ∀ and ∃ mean, and don’t need so much to rely on the formal rules; but we know what λ means too, so, like, I don’t think that’s a real difference.

And I mean, the three rules are just:

α-renaming: What variables are called does not matter. I.e., you can rename them.

β-reduction: Functions do what they say they do.

η-conversion: “The function that takes x and returns f(x)” is just the same thing as f.

The one really weird thing I think, is the possibility of doubly-binding a variable — you need some convention to define what the hell is meant by λx.λx.x; there’s nothing intuitive about that. As it is, it’s defined that inner bindings override outer ones, so the above is equivalent to λx.λy.y. But once again, formal logic has the same problem; you need to define what’s meant by ∀x∃x P(x), and the convention is the same, that it means ∀x∃y P(y). (Kind of a dumb statement since it has no real dependence on x, but…) And of course you might object that nobody would ever write a statement like that, but the same applies to the lambda-calculus — why would anyone ever write a function like λx.λx.x? Just write λx.λy.y so people can tell what you mean.

Note by the way that β-reduction doesn’t care about whether variables are bound or free; and while α does, well, α is just a rule saying you can rename variables, so how that interacts with boundness should already be intuitive even if writing it out formally is annoying — as I said, it’s no different than how you can rename variables in formal logic, or, well, anywhere in math. The only nontrivial rule where it’s an issue is η. But again, keep in mind what it means and it’s simple; η is supposed to mean “The function that takes x and returns f(x)” is just the same thing as f”, not “The function that takes x and returns f_x(x) is just the same thing as f”, because the latter statement is obviously false.

And if you really want to avoid renaming and bound/free issues, you can always use De Bruijn index notation… though personally I find that to be just about unreadable, and it makes the two remaining rules (α is unnecessary when variables don’t have names!) considerably less clear.

]]>I’d be comfortable writing Riemann and Con(ZFC) in a lambda calculus with some syntactic sugar on top, which is basically what Haskell is. ]]>