|
|
"Charlie-Boo" <shymathguy@xxxxxxxxx> writes:
> Alan Smaill wrote:
>> "Charlie-Boo" <shymathguy@xxxxxxxxx> writes:
>>
>> > Alan Smaill "Charlie-Boo" Alan Smaill:
>> >
>> >> >> why do you think a constructive proof is not a proof?
>> >> >
>> >> > Because it doesn't demonstrate the truth of anything.
>> >>
>> >> So you claim;
>> >> do you believe in justifying your claims?
>> >> Then do so.
>> >
>> > The claim is that what Curry-Howard describes is a proof. I say that
>> > in order to be a proof, then you have to demonstrate the truth of
>> > something. That has not been shown.
>>
>> CH makes a claim about a relationship between constructive proofs
>> and computable functions. You object to the idea that the
>> constructive proofs in question prove anything.
>> Your claim, your justification.
>>
>> > [You are trying to use the trick of requiring that someone prove a
>> > negative result, i.e., of the form "there does not exist . . ."
>> > That requires traversing the universal set, which may be impossible.
>> > We can only ask if one can give an example of what is supposed to
>> > exist, either a specific value or a set of values that must contain an
>> > example.]
>>
>> what statement "there does not exist ..." do you have in mind?
>
> There does not exist an assertion that is being proven.
You said that constructive proof "doesn't demonstrate the truth of
anything." For any sentence p, there is a constructive proof of
p -> p. That is the proof of a true assertion, isn't it?
So what is your claim about constructive logic?
>> Do you claim constructive logic is unsound?
>
> My claim is that there is no relationship between R(x,y) being a
> recursive function R:x => y, and the assertion (all x)(exists y)R(x,y).
This claim doesn't even mention constructive logic.
It doesn't help to see what you meant by "not proving anything".
As we have been though before, the claim is that there *is*
a relationship between constructive proof of (all x)(exists y)R(x,y)
and the existence of a recursive function f with the property that
(all x)R(x,f(x)). If you want to debunk CH, then *this* is the claim
that you need to object to. Your point is simply irrelevant
to the claim that CH depends on.
> The problem with calling it a "proof" is that it implies that it can be
> generated algorithmically
no, it doesn't --
of course it is undecidable in general whether a statement has a proof.
> and that all the research into
> theorem-proving applies and facilitates the implementation of the
> system. This is not so. The lack of examples illustrates that.
>
>> If so you just need some false conclusion derived from
>> true premisses with constructive logic.
>>
>> Your claim, your justification.
..
>> >> All right, here's an example:
>> >> find *two* proofs of
>> >>
>> >> [] ==> a:u(1)=>(a=>a=>a)
>> >>
>> >> in the system given earlier.
>> >>
>> >> You get back two *different* programs of this type,
>> >>
>> >> lambda(~,lambda(v0,lambda(~,v0)))
>> >> lambda(~,lambda(~, lambda(v0,v0))).
>> >>
>> >> According to CB, this proves that the system is not a compiler.
>> >
>> > If you can show (1) the formal request (input) that produces the above
>> > "programs",
>>
>> user input:
>> [] ==> a:u(1)=>(a=>a=>a)
>>
>> > (2) how these programs satisfy that formal request,
>>
>> In each case, evaluate (p of t1) where p is the program
>> and t1 is a concrete type. The result is two different lambda terms
>> that have the type (t1 => t1 => t1). The two functions have
>> different input/output behaviour.
>>
>> > (3)
>> > how the programs were formally generated from the formal request,
>>
>> automated proof search constructs one proof (with corresponding program);
>> the user requests another proof, which has the corresponding different
>> program. There are proof trees that can be inspected as in the
>> earlier example for each of the proofs.
>
> You are asserting that you can do something without giving an example
> showing exactly what you do and how that produces the right answer.
If you want the line by line proofs, say so;
it's excessive to keep posting these on a newsgroup, I think.
>> > and
>> > (4) that the two programs use different algorithms (i.e. are not
>> > translatable into each other by a series of local changes), then you
>> > have shown that your system creates the algorithm, which is in fact
>> > more than what a compiler does.
>>
>> They have different I/O behaviour.
>>
>> >> > Have you ever read a description of how it works? What was the input
>> >> > and output? The input is a series of program segments that are
>> >> > combined into one program. *
>> >>
>> >> By CB so it must be true?
>> >> By CB, so no justification needed?
>> >
>> > If you don't need to, then why should I have to?
>>
>> Oh, but I do.
>>
>> > The last time someone showed Curry-Howard here, the user had to enter
>> > in pieces of the program, calling these pieces "proofs". If you
>> > want me to dig it up . . .
>>
>> How does CBL synthesise the function that takes no input
>> and return a value y such that 0 <= y*y < 1*1 ?
>
> The user inputs:
>
> (eA)MUL(x,x,A)^(eB)MUL("1","1",B)^~LT(A,"0")^LT(A,B)
>
> The inverses of the rules described in the ARXIV paper are applied to
> reduce the problem down to axiomatized wffs e.g. MUL(I,J,x) ["We can
> multiply"] which are then used to construct the program. I can give
> more details if you wish. (The ARXIV paper goes into complete detail
> for numerous examples, in Number Theeory, Database Retrieval, and
> Theory of Computation.)
Yes, I'd like to see the detail for this example.
> Note that CBL doesn't produce any value that satisfies a given
> predicate, but rather all values that satisfy that predicate.
>
> "a value y that meets a given predicate" is not in general a function.
> Your specific predicate is, but the general scheme of "produce any
> value that meets this predicate" does not represent Program Synthesis
> problems in general.
>
> Program Synthesis deals with creating programs that produce a value
> that is uniquesly defined: the value of a function, or all values in a
> given set (the above.)
This is an unnecessarily restricted view of program synthesis;
the specification may ask for a function where the output is constrained
in some way, but not uniquely defined. If CBL does not deal
with this, then it is not as general as CH.
> CBL does that, as described in the ARXIV paper.
> Does Curry-Howard?
If the specification is chosen suitably, yes.
> C-B
>
>> --
>> Alan Smaill
>
--
Alan Smaill
|
|