From Löb's theorem to spreadsheet evaluation | Hacker News Reader

From Löb's theorem to spreadsheet evaluation

blog.sigfpe.com

30 pointsaufreak35 comments

Wow, this actually helped me understand the proof of Loeb's theorem, which I've always had trouble with. But I think the most confusing part is the fixed-point theorem it uses, which I've never seen a nice proof of; the Haskell code seems to be just implicitly accepting that a fixed point exists when he defines loeb x in terms of itself.

Is this something Haskell does in general? What happens when you try and write a function that doesn't have a fixed point?

> What happens when you try and write a function that doesn't have a fixed point?

It's like non-well founded recursion, it loops. But as a bonus, some cases are caught at runtime :

    x :: String
    x = x
    
    main = print x
    
    ./x
    x: <<loop>>

So is it just looping and hoping it converges? It won't do logic to figure it out, something like:

    x :: Real
    x = 2 / x

Guess that's to be expected, though a bit disappointing; I think it means the "loeb" given will be a lot less broadly applicable than the general mathematical version.

    "It won't do logic to figure it out,..."

If it could do that, wouldn't that amount to having an oracle that can tell whether a program will terminate?

What would you like that code to do? Fork the process and set x = sqrt(2) in one branch and x = -sqrt(2) in the other? In fact, should its behaviour depend on whether or not your floating-point implementation has a value such that x == 2/x holds exactly?

No, wait, Real is actually a type class, not a type, right? Perhaps when you write that code the system should extend itself to support an infinite-precision real-number type that implements Real, and make x be exactly sqrt(2)? (And exactly -sqrt(2), of course.)

All of which is just another way of saying: I really don't think it's quite fair to be disappointed that Haskell doesn't try to solve the extremely difficult (not to say provably unsolvable) problems of "doing logic to figure it out".

Reply on news.ycombinator.com