|
|
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.
> >> They have an (apparently unpublished) article
> >
> > You mean it has not passed peer review?
>
> astonishing, eh?
No, it's called "hypocrisy".
> > (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?
> > 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?
> is flawed?
It is an example of such (among many.) Flaws in Curry-Howard?
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.)
2. Programs correspond to wffs, not proofs. Proofs correspond to
execution history, not programs.
You said "Terms of the lambda calculus are programs, I hope you
agree." I thought the idea is that "Proofs are programs"?
BTW I once wrote a program to generate lambda calculus expression and
evaluate them for the first few natural numbers. I found identity,
successor, addition, exponentiation, etc. But then I noticed that all
of the functions were monotonic! At some point I read that they
(Church?) hadn't been able to create subtraction, I believe it was.
And years later someone claimed to have but using some kind of a trick.
So, is lambda calculus really Turing complete?
3. It's not a proof, because it doesn't meet the definition of
proving something.
4. It's not a proof, because in every example of a program being
constructed the user has to enter in the pieces of the program, rather
than it being generated as proofs are.
Note: Papers which brag about something but never give an example to
show that it works are BS.
5. It has never produced anything - a program, a theorem, a new result.
BTW Computationally Based Logics correct all of the above. Have you
ever read about or used them?
> >> 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.
> 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?
> >> > [give this R the name Q2] R(x,y) is x=(y*y). R:x => y is
> >> > recursive but not all x have a corresponding y such that R(x,y).
> >
> >> this is not even a mathematical function from naturals to
> >> naturals, then.
> >
> > Yes it is. For each x there is no more than one natural number y such
> > that x=(y*y).
>
> Not a function according to wikipedia:
>
> "In mathematics, a function relates each of its inputs to exactly one
> output."
How do they define "total function" and "partial function",
then?
You don't have to be total to be recursive. So you (they) lied when
you (they) said it creates all programs (computes all recursive
functions)? Have you no shame?
> >> >> For the unsoundness claim, how about you give us an example?
> >> >> Take a simple case where you can stick with classical first order logic,
> >> >> as it happens. Take Peano arithmetic, with normal structural induction,
> >> >> plus, times, zero. Now take any formula
> >> >
> >> >> all x1, ..., xn some y1,...,ym R(x1,...,xn,y1,...,ym)
> >> >
> >> >> where R is a formula of PA with shown free variables, but with no
> >> >> quantifiers (you can have bounded quantifiers if you want also). Now
> >> >> show us where there is a proof of the statement without there being a
> >> >> corresponding recursive function.
> >> >
> >> > R is Q1 as defined above. But this is not the requirement of Program
> >> > Synthesis. This may be the requirement that you impose on R in your
> >> > system, but that does not guarantee we can synthesize a program to
> >> > compute any given recursive function R:x => y.
> >>
> >> Please supply the proof that CBL can synthesise any recursive function.
> >
> > "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. 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?
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?
C-B
> --
> Alan Smaill
|
|