|
|
"Charlie-Boo" <shymathguy@xxxxxxxxx> writes:
>> >> > (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"?
Reel away;
I have no idea what you're snagged on.
>> >> > 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?
Let's stick with Nuprl as an example;
there are several others -- oh, and I mean implemented system, not
just theory.
>> >> 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.
Once again, *you* have to provide a situation where there is a constructive
proof of (all x)(exists y)R(x,y) where there is no corresponding recursive
function.
This is your claim.
Do you believe in backing up the claims that you make?
If so, let's see it.
>> > 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?
Three people have given you different examples in the newsgroup.
>> > 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,
another unsubstantiated claim;
do you bedlieve in backing up the claims that you make?
It is *your* claim that constructive proofs don't prove anything,
so let's see the justification.
> 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?
Good, you're catching on.
> But isn't a term a wff?
Well, no.
Standard logical terminology differentiates between terms and wffs,
and for good reason.
> Then a proof of a wff is a wff!
The rest of your deductions therefore fail.
> 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?
Take the advice of CB earlier in the thread:
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
From: Charlie-Boo
Date: Wed, Jul 26 2006 7:55 pm
...
I've been researching this problem for decades. But I am not the topic
of discussion. The question is whether there is a system (outside of
CBL) that synthesizes computer programs.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
> 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.
Shown to you for the case of simply typed lambda calculus.
> 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?
If you want to debate the topic with CB feel free.
>> >> > "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?
No, much simpler than using CBL;
throw away all that deductive machinery, since finding proofs is
hard work. Just use the axioms, and you have a synthesis system
for all possible programs.
>> > 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.
What is?
Who has claimed completeness?
>> > 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.
And since provided.
> 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 . . ."?
wake up and smell the coffee;
or remain in your dogmatic slumbers --
the choice is yours.
> C-B
>
>> --
>> Alan Smaill
>
--
Alan Smaill
|
|