So what would you consider a proof that there are no total Haskell
functions of that type?
Or, using Curry-Howard, a proof that the corresponding logical formula
is unprovable in intuitionistic logic?
As I understand, in general this can only be proven using meta theory
rather than the logic itself (it could happen that the given formula
implies absurdity, and then we'd know it can't be proven, given that
the logic is consistent).
If Djinn correctly implements the decision procedure that have been
proven to be total (using meta theory), then I would regard Djinn
saying no as a proof that there is no function of that type.
-- Lennart
On Thu, May 27, 2010 at 7:49 PM, wren ng thornton
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