|
|
Alan Smaill wrote:
> >> >> 129.215.101.90:1001/publications/PICTworkingpapers/WP38.pdf
> have you retried the link?
> If it's still not working, I will post the relevant footnote.
Yes, but apparently people already have, but feel free to post or email
the entire article if you have it in machine readable form.
> >> >> They have an (apparently unpublished) article
> >> >
> >> > You mean it has not passed peer review?
> >>
> >> astonishing, eh?
> >
> > No, it's called "hypocrisy".
>
> On whose part and why?
It just dawned on me that some lowlife here try to use the fact that
some improvement to conventional wisdom is not published (well
"Duh!" - how could it be otherwise?) as a basis for personally
attacking it (and the author), but at the same time plenty of published
articles cite unpublished papers. Not I see you do too!
> >> > (I think it's better to not redefine existing words such as
> >> > "equivalent". If you are referring to something else, I think it would
> >> > be better to use a completely different term.)
> >>
> >> I am not referring to something other than your "equivalent" here;
> >> I'm simply pointing out that the equivalence is classical.
> >
> > Classical as opposed to what?
>
> Constructive.
> Constructively equivalent formulas (A,B where you can show A <-> B in
> constructive logic) are classically equivalent, but not vice versa.
[Crank fishing reel] Then how can you say "I am not referring to
something other than your "equivalent" here"?
> >> > Then you will have to prove (all x)(exists y)R(x,y) when it is not so,
> >> > or you will produce a program that supposedly computes a non-recursive
> >> > function.
> >> >
> >> >> But this is irrelevant to Curry-Howard.
> >> >
> >> > However, I believe that it would be relevant to a lot of other people.
> >>
> >> How is it relevant to the question of whether the Curry-Howard approach
> >
> > Approach to what - getting grants?
>
> to program synthesis
Who has ever shown a Program Synthesis system based on C-H?
> >> is flawed?
> >
> > It is an example of such (among many.) Flaws in Curry-Howard?
>
> Since C-H does not make the claim that every all exists statement
> true in classical logic corresponds to a recursive function,
> why are you harping on about it?
Once again: Then you will have to prove (all x)(exists y)R(x,y) when it
is not so, or you will produce a program that supposedly computes a
non-recursive function.
> > 1. Nobody has ever shown that it works, with an example of a program
> > generated from the specifications only. "Google it" is not an
> > example (although it is correct English now.)
>
> Wrong.
Who has and where? After
http://groups.google.com/group/sci.logic/msg/5793a5308b655a28?hl=en&;
you went running like a scared bunny rabbit. And after
groups.google.com/group/sci.logic/msg/aba76db40d396e3e?hl=en&">http://groups.google.com/group/sci.logic/msg/aba76db40d396e3e?hl=en&;
Steven Zenith joined you in your little cubbyhole. (I haven't heard
a peep out of either of you about the matter since. You and he
weren't used to probing questions such as mine. Why? Besides my
superior intellect, my experience as being the only person who has
formalized any branch of Computer Science - yea, every branch of
Computer Science - has shown me how to quickly spot the difference
between an authentic formalization (mine) and bullshit (what has been
published.) And all that people can do is roll their eyes - you
never give any examples to prove your point!)
Why don't you just admit it? You believe in (and consequently claim)
certain things that you can't substantiate. You don't believe it
due to its having been demonstrated (like a scientist is supposed to
do) but rather because you have emotionally bonded with the authors.
There's nothing to be ashamed of. Most of my heroes (e.g. Martin
Gardner, and, before I realized the truth, Zohar Manna) are authors,
too. It's just that I don't idolize them. I realize that from
time to time they will spew out some BS like claiming that various
branches of Computer Science have been formalized. So I am never in
the awkward position of being unable to substantiate my claims.
Now some people have said that I don't want to look at the literature
(no matter how much I quote from it.) But think about it: Why
wouldn't I enjoy reading the literature? Every time I do (especially
regarding formalizing any branch of Computer Science) I am reminded
that (a) they claim to have formalized some branch of Computer Science,
(b) they haven't, and (c) I have. Who wouldn't enjoy being
reminded that they are smarter (and more honest) than all of those
people whom saps like you and Steven Zenith admire so much?
> > 2. Programs correspond to wffs, not proofs. Proofs correspond to
> > execution history, not programs.
>
> Not in CH.
I see. Pv~P can't be proven, proofs don't prove anything, and now
programs don't correspond to wffs! Question: How much is 1+1 in CH?
And how much did you pay for this little gem? BTW I have a nice
bridge that I have for sale - perhaps you and Steven Zenith would care
to become co-owners?
> > You said "Terms of the lambda calculus are programs, I hope you
> > agree." I thought the idea is that "Proofs are programs"?
>
> Yes it is;
> a proof, in the appropriate logic, can be turned automatically
> into a program.
I see. So a proof is a program and a term is a program. So a proof is
a term? But isn't a term a wff? Then a proof of a wff is a wff! So
a proof of a proof is a wff? And a wff of a wff is a wff (which is
also a proof)? Wow - it looks like everything is equal to everything
else!
> > BTW I once wrote a program to generate lambda calculus expression and
> > evaluate them for the first few natural numbers.
>
> This is not about CB.
What's wrong with citing the literature?
> >> >> now please supply the constructive proof of the statement
> >> >> "For every x there is a corresponding y such that R(x,y)".
> >> >> and I will agree that Curry-Howard is unsound.
> >> >
> >> > Ok. Define H(a,b) to be the wff that expresses "Program a halts at
> >> > iteration b-1."
> >> >
> >> > Then, suppressing the leading universal quantifier of a, (eA)R(a,A) is
> >> > (eB)R(a,B) is:
> >> >
> >> > Thm. (eB) [ (eA)H(a,A) ^ H(a,B) ] v [ ~(eA)H(a,A) ^ (B=0) ]
> >> > 1. (eB) B=0
> >> > 2. (eA)H(a,A) v ~(eA)H(a,A)
> >> > 3. [ (eA)H(a,A) ^ (eB)H(a,B) ] v [ ~(eA)H(a,A) ^ (eB)B=0 ]
> >> > 4. (eB) [ (eA)H(a,A) ^ H(a,B) ] v [ ~(eA)H(a,A) ^ (B=0) ]
> >> > qed
> >> >
> >> > Rules: 1 is (eB) introduction on (or is) Peano. 2 is substitution on
> >> > Pv~P.
> >>
> >> Pv~P is not constructively valid.
> >> This is not a constructive proof.
> >
> > No Pv~P and you call that a proof? You can't create diddley, then.
>
> Yes you can;
> try it some time.
I've asked people to show me how about 200 times, and all they can tell
me is that a wff of a wff is a wff of a wff of a wff! I'm still
waiting for the part where a program comes out of it somewhere.
Meanwhile, the Computationally Based Logics have generated almost
everything under the sun!
> >> Please supply a constructive proof as requested.
> >>
> >> > quantifiers. Note that this proof is valid (useful, needed) for other
> >> > H.
> >> >
> >> > BTW Do you agree that:
> >>
> >> This is not about CB and his system.
> >
> > You can brag (falsely) about H-C but I can't even mention (honestly)
> > CBL?
>
> This is not about CB.
I though it was about Program Synthesis? Did you know that CBL is the
only Program Synthesis system ever developed? I'm serious. I'll
personally pay $1,000.00 to the PayPal account of anyone who can prove
me wrong.
> >> > "the" proof? Who said there was such a proof? But yes, there is.
> >> > Any program can be an axiom.
> >>
> >> Classic CB!
> >
> > I though logicians call that "interesting" vs. "uninteresting"
> > axioms? So classic CB uses classic Logic methods? Now THAT is an
> > insult. They don't know squat. Look how badly they incorporated
> > Peano's Axioms. CBL does that using a tiny fraction of the size as
> > classic Logic. (Occam prefers CBL.)
> >
> >> CBL can synthesise any recursive function because it can be given as
> >> an axiom !!!
> >
> > You snipped the part about what axioms I actually use and all the
> > programs and theorems that it creates.
>
> Of course;
> they are all redundant.
> Simply allow as axioms any recursive program;
> then you need no rules of inference at all.
>
> Much simpler that way.
You mean instead of Peano Arithmetic? You do have a point there. But
what happened to the set of axioms being recursive? And finite?
> > There's no limit to what it
> > can produce in theory, as far as your question goes. Just give it the
> > right axioms. But in practice, you want to have a fixed set of axioms
> > for any domain. I give axioms for Number Theory, DataBase retrieval,
> > and Theory of Computation in the ARXIV paper.
> >
> > You also snipped "Speaking of which, can you prove that Curry-Howard
> > can synthesise any recursive function?" Where is YOUR proof?
>
> Who said there is a proof?
Oh, this is another article of faith? I see.
> > And since you can't show a system to synthesize anything at all, how
> > can you talk? You have NOTHING (except the gullibility to believe
> > professors without examples.) What kind of science is that?
>
> Example follows in another post.
Where, at the end of the Yellow Brick Road? You're starting to sound
more and more like that genius Steven Zenith. "Follow, follow,
follow, follow, follow the Yellow Brick Road . . ." Or is it the
scarecrow - "If I only had a brain . . ."?
C-B
> --
> Alan Smaill
|
|