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
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
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
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,
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
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
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
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
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
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
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
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
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
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
14 matches
Mail list logo
