Re: [Haskell-cafe] currying combinators

On 28 May 2010, at 08:47, Lennart Augustsson wrote:

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.)

Just to flesh out the thought, let me sketch completeness (the result is due to Roy Dyckhoff). Fortunately, an exhaustive search is not necessary for completeness in this logic. Let's say that a "cycle" in a proof is where some atomic proposition P is derived by a proof tree which includes internal derivations of P ... ----- P ...... --------------------- P Of course, you can simplify such a proof by replacing the larger P-proof with the smaller. If a proposition has a proof, then it has a cycle-free proof. An exhaustive search of the cycle-free proofs is thus complete. But can we implement such a search? Given that an assumption can prove at most one atomic formula (an assumption which does not hold in *predicate* logic), you can be sure that any path in a proof tree which uses the same assumption twice creates a cycle. Correspondingly, you can be sure that in each branch of a proof, you can discard the assumptions you've already used. That's enough of a "resource bound" to ensure that an exhaustive search of the cycle-free proofs will terminate. (You can acquire new assumptions when you backchain on a higher-order assumptions, but the new assumptions are two orders lower than the assumption disposed of, so you can readily construct an order-based lexicographic termination scheme (shameless plug for my PAR2010 talk).) So, there's some reason to believe that there is a complete algorithm, which might even be the one Lennart implemented in Djinn. All the best Conor

On Fri, May 28, 2010 at 8:14 AM, wren ng thornton 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe