Re: [Haskell-cafe] currying combinators
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
Re: [Haskell-cafe] currying combinators
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 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
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 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
Re: [Haskell-cafe] currying combinators
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. True, though I think I didn't make my point clearly. The question is, when can we consider a proof of (\forall x. ~ P x) as a valid *constructive* proof of (~ \exists x. P x)? If you tell me you've checked every x and found none supporting P, and I believe you have the capability to have done so, and I believe things you say are true, then I may take your statement that (\forall x. ~ P x) and prove to myself that (~ \exists x. P x). However, my proof ---no matter how much I believe it--- is not the sort of thing I can pick up and hand to someone else. If they do not trust your diligence, then they have no reason to trust my proof. I haven't constructed a witness to the proposition, I've only convinced myself of it. If, however, you construct a proof of (\forall x. ~ P x) which shows that all options have been exhausted, but does so in a finite way that's open to inspection and analysis, well then that's a different story. In this case, because we've actually constructed some mathematical object that we can poke and prod to understand what it is and how it works, we do have something that we can hand to a skeptic to convince them. We needn't argue from authority or put our faith in an elder or prophet, the proof stands on its own. When someone says prove it, it's not always clear whether they mean they want to be convinced it's true, or whether they mean they want concrete evidence that witnesses its truth. Exhaustive search may be convincing, but it's not constructive. When the OP was asking how we'd go about proving that no total function exists with a particular type, I was assuming they were seeking a witness rather than a convincing. For a witness, I'd think you'd have to reason from parametricity, understand the process that Djinn is automating, or similar; just running Djinn is merely convincing. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] currying combinators
David Sankel wrote: keep :: ((t - b) - u - b) - ((t1 - t) - b) - (t1 - u) - b On Wed, May 26, 2010 at 12:49 PM, Lennart Augustsson lenn...@augustsson.net wrote: There are no interesting (i.e. total) functions of that type. I wonder how one would prove that to be the case. I tried and didn't come up with anything. By parametricty, presumably. We must ultimately construct some value of type b, where b is universally quantified. Therefore, the only 'constructors' available for b are the ((t - b) - u - b) and ((t1 - t) - b) arguments. However, since b is universally quantified, these arguments have no way of actually constructing some b, other than by returning bottom. Remember, if a language lacks typecase, (forall a. X - a) is just another way of saying (X - Void). -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] currying combinators
On Thursday 27 May 2010 3:27:58 am wren ng thornton wrote: By parametricty, presumably. Actually, I imagine the way he proved it was to use djinn, which uses a complete decision procedure for intuitionistic propositional logic. The proofs of theorems for that logic correspond to total functions for the analogous type. Since djinn is complete, it will either find a total function with the right type, or not, in which case there is no such function. At that point, all you have left to do is show that djinn is in fact complete. For that, you can probably look to the paper it's based on: Contraction-Free Sequent Calculi for Intuitionistic Logic* (if I'm not mistaken) by Roy Dyckhoff. -- Dan [*] http://www.cs.st-andrews.ac.uk/~rd/publications/jsl57.pdf ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] currying combinators
wren ng thornton wrote: David Sankel wrote: keep :: ((t - b) - u - b) - ((t1 - t) - b) - (t1 - u) - b Lennart Augustsson wrote: There are no interesting (i.e. total) functions of that type. I wonder how one would prove that to be the case. I tried and didn't come up with anything. By parametricty, presumably. We must ultimately construct some value of type b, where b is universally quantified. Therefore, the only 'constructors' available for b are the ((t - b) - u - b) and ((t1 - t) - b) arguments. However, since b is universally quantified, these arguments have no way of actually constructing some b, other than by returning bottom. Er, that's not quite right. That's only true if those arguments are rank-2 quantified. I'd had a longer (correct) explanation and tried shortening it. So here's the better proof: In order to produce a value of type b, keep must either use one of those two arguments or return bottom. If it uses the ((t - b) - u - b) argument, then keep can only return non-bottom if that function [1] ignores its arguments and returns an arbitrary b, or [2] uses the (t - b) argument to construct the b. If we assume #1 then keep is not total, because we have no way of proving that the assumption is valid. So we must expect #2; so in order for keep to be total it must be able to construct a total function (t - b). In order to construct such a function it must use one of the original two arguments, so this is only possible if we can construct a b via ((t1 - t) - b). If it uses the ((t1 - t) - b) argument, then keep can only return non-bottom if that function [1] ignores its arguments, or [2] uses the (t1 - t) argument. We can't assume #1 and be total, so we must expect #2. In order to construct (t1 - t) we must construct a t. But, since t is universally quantified, keep knows of no total functions which return t. Thus, keep can only construct a function which returns bottom. Thus, keep can only return non-bottom under the assumption that the ((t - b) - u - b) and ((t1 - t) - b) arguments ignore their arguments to return a constant b. -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] currying combinators
Dan Doel wrote: On Thursday 27 May 2010 3:27:58 am wren ng thornton wrote: By parametricty, presumably. Actually, I imagine the way he proved it was to use djinn, which uses a complete decision procedure for intuitionistic propositional logic. The proofs of theorems for that logic correspond to total functions for the analogous type. Since djinn is complete, it will either find a total function with the right type, or not, in which case there is no such function. At that point, all you have left to do is show that djinn is in fact complete. For that, you can probably look to the paper it's based on: Contraction-Free Sequent Calculi for Intuitionistic Logic* (if I'm not mistaken) by Roy Dyckhoff. 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. (Sorry, just finished writing a philosophy paper on intuitionism :) -- Live well, ~wren ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] currying combinators
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. If you point is that the result you get is: ¬ ⊢ (...) instead of ⊢ ¬ (...) then this is true, but the former is what was originally claimed (there are no total functions of that type == that proposition is not a theorem). In fact, if one can prove the second, then we're in trouble, because the proposition is a classical theorem, and djinn provides a result for ⊢ ¬ ¬ (...) which contradicts the second statement above. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] currying combinators
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? As I understand, in general this can only be proven using meta theory rather than the logic itself (it could happen that the given formula implies absurdity, and then we'd know it can't be proven, given that the logic is consistent). 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. -- Lennart On Thu, May 27, 2010 at 7:49 PM, wren ng thornton w...@freegeek.org wrote: Dan Doel wrote: On Thursday 27 May 2010 3:27:58 am wren ng thornton wrote: By parametricty, presumably. Actually, I imagine the way he proved it was to use djinn, which uses a complete decision procedure for intuitionistic propositional logic. The proofs of theorems for that logic correspond to total functions for the analogous type. Since djinn is complete, it will either find a total function with the right type, or not, in which case there is no such function. At that point, all you have left to do is show that djinn is in fact complete. For that, you can probably look to the paper it's based on: Contraction-Free Sequent Calculi for Intuitionistic Logic* (if I'm not mistaken) by Roy Dyckhoff. 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. (Sorry, just finished writing a philosophy paper on intuitionism :) -- 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
Re: [Haskell-cafe] currying combinators
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] currying combinators
There are no interesting (i.e. total) functions of that type. 2010/5/25 Yitzchak Gale g...@sefer.org: Günther Schmidt wrote: http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=25694 in which I attempt to develop a currying combinator library. I'm stuck at some point and would appreciate any help. How about this: keep :: ((t - b) - u - b) - ((t1 - t) - b) - (t1 - u) - b so then nameZip = keep (drop' . drop') names Regards, Yitz ___ 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
Re: [Haskell-cafe] currying combinators
keep :: ((t - b) - u - b) - ((t1 - t) - b) - (t1 - u) - b On Wed, May 26, 2010 at 12:49 PM, Lennart Augustsson lenn...@augustsson.net wrote: There are no interesting (i.e. total) functions of that type. I wonder how one would prove that to be the case. I tried and didn't come up with anything. David -- David Sankel Sankel Software www.sankelsoftware.com 585 617 4748 (Office) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] currying combinators
Günther Schmidt wrote: http://www.hpaste.org/fastcgi/hpaste.fcgi/view?id=25694 in which I attempt to develop a currying combinator library. I'm stuck at some point and would appreciate any help. How about this: keep :: ((t - b) - u - b) - ((t1 - t) - b) - (t1 - u) - b so then nameZip = keep (drop' . drop') names Regards, Yitz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
