Prev: New Primitive Programming Language - Is it Turing Complete?
Next: The size of proper classes?
From: Marshall on 11 Dec 2009 12:51
On Dec 2, 7:00 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
> Marshall <marshall.spi...(a)gmail.com> writes:
> > Is there a formal way for extracting axioms/theorems from this model?
>
> Sure. Have a look at any exposition of constructive type theory. For a
> hands-on approach perfect for someone of a Haskell turn of mind, try
> your hand at Agda!

Wow.

When I first read your response, I just had a minute to glance at
Agda, and it reminded me of Coq, which seemed impressive
enough but didn't grab me. But taking a deeper look today,
it looks, as you say, perfect for someone of my turn of mind.
Sweet. Thanks for the reference.


> > How might we go about proving, say, commutativity of + from this?
>
> By structural induction, of course.

Yeah, eventually it came to me that one could prove
x + 0 = 0 + x easily enough with induction, and then
use that as the basis step for an inductive proof of
x + y = y + x.

Is that the way to generalize induction from arity 1
to arity n? Somehow it vaguely feels too simple, and
that there must be something more clever I'm missing.

(Amusingly, structural induction on the algebraic datatype
definition of the naturals makes the usual formulation of
induction over the naturals into a special case of structural
induction. I suppose that's old hat to y'all but I just
discovered it.)


Marshall
From: Marshall on 11 Dec 2009 13:03
On Dec 11, 9:50 am, Arturo Magidin <magi...(a)member.ams.org> wrote:
> On Dec 11, 11:10 am, Marshall <marshall.spi...(a)gmail.com> wrote:
>
> > On Dec 2, 6:48 am, David C. Ullrich <dullr...(a)sprynet.com> wrote:
> > > Which I guess amounts to saying I don't quite see the point
> > > to the question - seems to me those bits of Haskell are
> > > just reformulations of the Peano axioms...
>
> > Um, that doesn't seem right to me. It satisfies the
> > Peano axioms, but it isn't equivalent to them, is it?
> > (If that's what you meant by "refomulations".)
>
> No; "reformulation" here means "a different but equivalent form".

All right. I had thought he was saying that the Haskell code
was equivalent to the Peano axioms; is there some nuance
in "equivalent form" I'm missing?

In either case, I don't see the equivalence; it seems to me
that any formula that is true of the naturals will be true of
the type "nat" defined above, and that the same is not the
case with the Peano axioms, per the first incompleteness
theorem. However I would be happy to have my
understanding corrected if I am wrong.


Marshall
From: Tegiri Nenashi on 11 Dec 2009 14:15
On Dec 11, 9:51 am, Marshall <marshall.spi...(a)gmail.com> wrote:
> On Dec 2, 7:00 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
> > ...your hand at Agda!
>
> Wow.

Unfortunately, it is based upon flawed assumption:
"Predicates are dependent types"
From: Marshall on 11 Dec 2009 19:44
On Dec 11, 11:15 am, Tegiri Nenashi <tegirinena...(a)gmail.com> wrote:
> On Dec 11, 9:51 am, Marshall <marshall.spi...(a)gmail.com> wrote:
>
> > On Dec 2, 7:00 am, Aatu Koskensilta <aatu.koskensi...(a)uta.fi> wrote:
> > > ...your hand at Agda!
>
> > Wow.
>
> Unfortunately, it is based upon flawed assumption:
> "Predicates are dependent types"

Can you elaborate? The theory isn't sufficiently powerful
for your tastes, because of self-imposed limitations?
Or do you instead see some flaw?


Marshall
From: David C. Ullrich on 13 Dec 2009 12:21
On Fri, 11 Dec 2009 10:03:53 -0800 (PST), Marshall
<marshall.spight(a)gmail.com> wrote:

>On Dec 11, 9:50�am, Arturo Magidin <magi...(a)member.ams.org> wrote:
>> On Dec 11, 11:10�am, Marshall <marshall.spi...(a)gmail.com> wrote:
>>
>> > On Dec 2, 6:48�am, David C. Ullrich <dullr...(a)sprynet.com> wrote:
>> > > Which I guess amounts to saying I don't quite see the point
>> > > to the question - seems to me those bits of Haskell are
>> > > just reformulations of the Peano axioms...
>>
>> > Um, that doesn't seem right to me. It satisfies the
>> > Peano axioms, but it isn't equivalent to them, is it?
>> > (If that's what you meant by "refomulations".)
>>
>> No; "reformulation" here means "a different but equivalent form".
>
>All right. I had thought he was saying that the Haskell code
>was equivalent to the Peano axioms; is there some nuance
>in "equivalent form" I'm missing?
>
>In either case, I don't see the equivalence; it seems to me
>that any formula that is true of the naturals will be true of
>the type "nat" defined above, and that the same is not the
>case with the Peano axioms, per the first incompleteness
>theorem. However I would be happy to have my
>understanding corrected if I am wrong.

Well, I'm not certain exactly what we're talking about
(and of course not certain that the things I'm saying
about what I think we're talking about are correct):

In another post you say something about how the Haskell
gives a "concrete model". I don't see how it's any more
"concrete" than the abstract "minimal model"
or "standard model" for the Peano axioms, and
those two models are isomorhic, "concrete" or not.

But you _asked_ about axioms and theorems that
could be _formally_ extracted from the Haskell
code. Seems to me that those are exactly the
logical conseqences of the Peano axioms, which
is the same as the class of formulas true in
_every_ model. There are indeed formulas
true in the standard model that are not logic
consequences of the axioms, but I don't see
how they're going to be "formally extracted"
from the Haskell any more than from the
Peano axioms.

Iow, it seems to me that the Haskell and the
Peano axioms _are_ equivalent, and the only
reason they seem different to you is that in
one case you're fixing attention on the minimal
model while in the other case you're considering
all possible models. If we did have a computer
with infinitely much memory, so it could construct
an _actually_ "concrete" model of the Haskell
"axioms" as a single array in memory, that
machine could also construct nonstandard models.
I don't see how you're going to distinguish the
two "formally" in the Haskell any more than
in the Peano case.



>
>Marshall

David C. Ullrich

"Understanding Godel isn't about following his formal proof.
That would make a mockery of everything Godel was up to."
(John Jones, "My talk about Godel to the post-grads."
in sci.logic.)
First  |  Prev  |  Next  |  Last
Pages: 1 2 3
Prev: New Primitive Programming Language - Is it Turing Complete?
Next: The size of proper classes?