A proof of Löb's theorem in Haskell(lesswrong.com)
lesswrong.com
A proof of Löb's theorem in Haskell
http://lesswrong.com/lw/l0d/a_proof_of_l%C3%B6bs_theorem_in_haskell/
2 comments
Interesting to see you can jam something like this into Haskell despite its inappropriateness. The (genuine) Agda proofs are much, much nicer.
Agreed :-)
One of the big questions to me now is whether we can prove the Diagonal Lemma, not just assume it. Do you know if it's possible in Agda? I heard somewhere that it might be hard to find an intuitionistic proof.
One of the big questions to me now is whether we can prove the Diagonal Lemma, not just assume it. Do you know if it's possible in Agda? I heard somewhere that it might be hard to find an intuitionistic proof.