|
|
"Charlie-Boo" <shymathguy@xxxxxxxxx> writes:
> Alan Smaill, Charlie-Boo, Alan Smaill, Charlie-Boo:
>
>> >> > on what specific basis (e.g. excerpts from some
>> >> > publications) do you say that Manna & Waldinger did not change the
>> >> > background logic?
>> >>
>> >> See the footnote on p28 of
>> >>
>> >> 129.215.101.90:1001/publications/PICTworkingpapers/WP38.pdf
>> >
>> > "The page cannot be dispayed" : (
>>
>> works for me ...
>
> Email me a copy through Google, please.
have you retried the link?
If it's still not working, I will post the relevant footnote.
>> >> 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?
>> > (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.
>> > 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
>> 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?
> 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.
> 2. Programs correspond to wffs, not proofs. Proofs correspond to
> execution history, not programs.
Not in CH.
> 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.
> 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.
>> >> 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.
>> 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.
>> > "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.
> 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?
> 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 kid of science is that?
Example follows in another post.
> C-B
>
>> --
>> Alan Smaill
>
--
Alan Smaill
|
|