|
|
"Charlie-Boo" <shymathguy@xxxxxxxxx> writes:
> Alan Smaill wrote:
>
>> OK, let's take this one step at a time.
>> I'll use some of the nuprl rules (simplified a bit, but
>> we could use them as given). Let's look at the following
>> problem.
>>
>> Terms of the lambda calculus are programs, I hope you
>> agree.
>>
>> en.wikipedia.org/wiki/Lambda_calculus
>>
>> gives more detail. Some of these programs can be typed,
>> e.g. (using \ for lambda) \x.(\y.x) has type A -> (B -> A)
>> for types A,B. Now let's use Curry-Howard to solve
>> the following problem. Given a type (formed from
>> base types A,B,C,... with the only connective ->), find a program
>> of that type.
>
> . . . [see original post for snipped details]
>
>> [2] complete
>> ==> u(1)in u(2)
>> by intro
>
>> Let me know what you would like clarified and we can continue
>> to see the automatic derivation of a program from this proof.
>
> 1. What does the resulting program do?
As I said, so far we only have the proof.
So it is not yet time to clarify this, as I have not presented it yet.
> 2. What is its input?
>
> 3. What is its output?
>
> 4. What is the relationship between its input and output?
>
> 5. What is the formal representation of the request that the user
> enters to create this program?
>
> 6. What are the resulting programs?
>
> 7. How does each execute - what is the algorithm that is executed?
Same answer applies.
So, can I take it that you are clear so far that we have entered a statement
to be proved:
a:u(1)=>b:u(1)=>c:u(1)=>(a=>b=>c)=>(a=>b)=>a=>c
and found a proof in the formal system given in my previous post?
If so, I will show how we can extract a program automatically from this proof
and then answer the questions above.
> What would be the input to request the following fundamental functions:
One thing at a time;
I will gladly address the other questions also, when and if
you are happy with this simple example.
> Thank you for explaining how your Program Synthesis system works.
>
> I would be glad to answer these questions (8-13) using a
> Computationally Based Logic. (Many of them are explicitly answered in
> my ARXIV paper.)
This is not about CB and his system;
it is about CB's claim that there is no (other) account of
program synthesis.
>
> C-B
>
--
Alan Smaill
|
|