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
<w...@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@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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
