[Haskell-cafe] currying combinators

[wren ng thornton]

Dan Doel wrote:
> On Thursday 27 May 2010 1:49:36 pm wren ng thornton wrote:
>> 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.
> 
> How, exactly, is it non-constructive to encode the propositional calculus and 
> its proofs as, say, types in intuitionistic type theory, write the algorithm 
> djinn uses in the same (it was specially crafted to be provably terminating, 
> after all), and prove the algorithm complete (again, hopefully in the type 
> theory)? I realize this has not all been done, strictly speaking, but I see 
> nowhere that it is necessarily non-constructive.


All I'm saying is that a proof of (\forall x. ~ P x) does not constitute 
  a proof of (~ \exist x. P x) for some intuitionists. The issue is one 
of the range of quantification and whether \forall truly exhausts every 
possibility. The BHK interpretation says the two propositions are the 
same, but others say the latter is a stronger claim.

If you believe that Djinn truly does exhaust the search space, then it's 
fine to convert Djinn's proof of (\forall x. ~ P x) into a proof of (~ 
\exist x. P x). However, that just pushes the question back to why you 
feel justified in believing that Djinn truly exhausts the search space. 
I'm not saying you shouldn't believe in Djinn, I'm saying that belief in 
Djinn is not justification for a theorem unless you have justification 
for believing in Djinn.

-- 
Live well,
~wren