[Haskell-cafe] currying combinators

[Conor McBride]

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