A proof of Löb's theorem in Haskell
lesswrong.com
A proof of Löb's theorem in Haskell
1–3 of 3 posts
Re: A proof of Löb's theorem in Haskell
#2Interesting to see you can jam something like this into Haskell despite its inappropriateness. The (genuine) Agda proofs are much, much nicer.
Re: A proof of Löb's theorem in Haskell
#3Interesting 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.