Dan Doel wrote:
On Thursday 27 May 2010 3:27:58 am wren ng thornton wrote:
By parametricty, presumably.
Actually, I imagine the way he proved it was to use djinn, which uses a
complete decision procedure for intuitionistic propositional logic. The proofs
of theorems for that logic correspond to total functions for the analogous
type. Since djinn is complete, it will either find a total function with the
right type, or not, in which case there is no such function.
At that point, all you have left to do is show that djinn is in fact complete.
For that, you can probably look to the paper it's based on: Contraction-Free
Sequent Calculi for Intuitionistic Logic* (if I'm not mistaken) by Roy
Dyckhoff.
Sure, that's another option. But the failure of exhaustive search isn't
a constructive/intuitionistic technique, so not everyone would accept
the proof. Djinn is essentially an implementation of reasoning by
parametricity, IIRC, so it comes down to the same first principles.
(Sorry, just finished writing a philosophy paper on intuitionism :)
--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
