[Haskell-cafe] currying combinators

[Lennart Augustsson]

Yes, of course you have to trust Djinn to believe its proof.
That's no different from having to trust me if I had done the proof by hand.
Our you would have to trust yourself if you did the proof.

BTW, Djinn does not do an exhaustive search, since there are
infinitely many proofs.
(Even if you just consider cut free proofs there's usually infinitely many.)

On Fri, May 28, 2010 at 8:14 AM, wren ng thornton <wren at freegeek.org> wrote:
> Lennart Augustsson wrote:
>>
>> 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?
>
>
> It depends on what kind of proof I'm looking for. If I'm looking for an
> informal proof to convince myself, then I'd probably trust Djinn. If I'm
> trying to convince others, am deeply skeptical, or want to understand the
> reasoning behind the result, then I'd be looking for a more rigorous proof.
> In general, that rigorous proof would require metatheory (as you say)---
> either my own, or understanding the metatheory behind some tool I'm using to
> develop the proof. For example, I'd only trust Djinn for a rigorous proof
> after fully understanding the algorithms it's using and the metatheory used
> to prove its correctness (and a code inspection, if I didn't trust the
> developers).
>
>
>> 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.
>
> So would I. However, that's adding prerequisites for trusting Djinn--- which
> was my original point: that Djinn says there isn't one is not sufficient
> justification for some folks, they'd also want justification for why we
> should believe Djinn actually does exhaust every possibility.
>
> --
> Live well,
> ~wren
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>