|
|
"Charlie-Boo" <shymathguy@xxxxxxxxx> writes:
> Alan Smaill wrote:
>> "Charlie-Boo" <shymathguy@xxxxxxxxx> writes:
>
>> > I don't know what the they're talking about.
>
>> This is more illuminating than your repeated claims that
>> axioms, formal system etc are "not there", or that
>> there is no explanation.
>
> Yes, it is an interesting problem - cutting through the Gordian Knot.
> I have touched on it here on occasions. The basic problem is being
> presented with an unwieldy maze of non-standard formalisms with no
> indication as to where to look for explanations of each term. The
> explanation should be right there - simply tell us all what that little
> expression means and how it was built. Not just a reference to 200
> pages of expressions surrounded by more nonstandard terms couched in
> English.
Some may have the view that telling folk that something is "not there"
when you have no idea if it is there or not is just a tad misleading.
> 2. A system that formally creates computer programs would necessarily
> allow the author to show examples of programs produced. These would be
> in some existing programming language known to be implementable. Thus
> any paper consisting of only formal expressions in its own syntax
> hasn't produced the program claimed.
When the system is implemented, downloadable, and the synthesise
programs run as advertised, as is the case, the situation is different.
>> > Thanks for the
>> > effort, but you have not shown the prerequisite program, formal
>> > derivation, and explanation as to how it calculates the specified
>> > function.
>>
>> What prerequisite program?
>
> Formally generated, satisfies a formal requirement in a system capable
> of expressing useful functionality e.g. concerning prime numbers,
> factors and employees in a database.
If you mean program corresponding to the given specification,
this is in a post later than the one to which you reply here.
>> This is the start of using the formal system (which you claim does
>> not exist) in order to produce the program at the end of the day.
>
> But it's not even "the program" - it's any program that outputs any
> single value that meets the condition, not the entire set. How can you
> list the factors of a given number?
Fine, if you want an enumeration, use a different specification
that says that the output list contains what you want it to contain.
>> Perhaps you regard it as
>> reasonable to say that something is "not there" when
>> in fact you don't know what is being talked about.
>
> Yes, as I show above.
Well, no more to be said then.....
>> 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.
>
> But you said that proofs are programs. Now you are switching back to
> the authentic correspondence.
If it helps you to think so, by all means.
>> 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.
>
> So to turn the type A -> (B -> A) into the program \x.(\y.x) we change
> -> to . to get A.(B.A) then add \ in front of each expression that
> contains . to get \A.(\B.A) and change A B C to x y z to get \x.(\y.x),
> right? You are just using different syntaxes for the same things.
so, what do you think we get for (A -> B) -> (B -> C) -> (A -> C)?
>> 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.
>
> Just change the syntax as I describe above. It's trivial.
well, your superficial pattern-matching didn't get you very far
in this case.
>> First, let's ignore the problem of getting back the program, and just
>> prove a correponding theorem.
>
> You don't have to prove anything. It's just a simple syntactic
> change. By Occam's Razor, Curry-Howard is horribly overly complex.
oh, but we want to show that this set-up has the axioms, inference
rules, goals and programs that you claim no-one has done.
Whether it can be done more simply is a different question altogether.
>> We work with sequents of the form
>>
>> x1:F1, x2:F2, ..., xn:Fn >> G (abbreviate as H >> G).
>>
>> where F1,..,Fn,G are formulas,
>> x1,..xn variables. Read the sequent as saying that
>>
>> F1 & F2 & ... & Fn => G.
>
> Why include X1 . . . as they are not used in the definition?
Because they are used subsequently in building up a program
>> Now the rules say that we can deduce the sequent above the line
>> from the sequents below the line. u(1) is the type of base types.
>
> The above refers to H >> G and says that G is a formula and H is a
> series of variable:formula, that u(1) is the set of base types A, B, C,
> . . ., and that => means implication. Then the rules below seem
> ill-formed. For example, in rule # 1 below:
>
> 1. What is A? The above says that A is a base type.
That was for the example;
here the A is used differently (see below)
> The 2nd. line in
> rule 1 below also uses A as a base type [ A in u(1) ]. But the top
> line below [ H >> A => B in u(1) ] uses A as either the formula G in H
>>> G where G is A here, or the formula A in implication A => B.
Here is the rule:
1. H >> A => B in u(1)
------------------------------ intro
H >> A in u(1) H >> B in u(1)
As is normal in giving inference rules, this corresponds to
a whole set of instances where the rule is used, with particular
values substituted;
eg
a:u(1),b:u(1),c:u(1) >> (c => b) => (a => b) in u(1)
-----------------------------------------------------
a:u(1),b:u(1),c:u(1) >> (c => b) in u(1)
and a:u(1),b:u(1),c:u(1) >> (a => b) in u(1)
> 2. The second line says that H implies B in u(1), and the top line
> conclusion refers to B in u(1) also given H. So we can simplify the
> top line by substituting TRUE for B in u(1) and apply properties of
> TRUE to that as well. If the top line means (A => B) in u(1) then u(1)
> is not the set of base types A, B, C . . . after all, and you are using
> => for two different meanings.
I think this is a parsing problem; the top line should be read as
H >> (A => B) in u(1)
Precedence for the operators is given in the book.
> 3. The second line has two expressions next to each other without
> defining the meaning - which I took to mean that each expression is a
> premise.
Right
> 4. What is rule # 1 trying to say, that if A and B are types then A=>B
> is a type? But don't you mean A->B?
I'm following notation from an implementation that happens to use
the former. Think of the latter everywhere if you want.
> In rule # 2 below:
>
> 5. The bottom line places f: A=>B where the above defines a
> variable:formula. But f is a function not a variable,
we do want f to be a variable here -- it's a label for the hypothesis.
> and A => B also
> seems to be a function, not a formula.
see, you're catching on to Curry-Howard --
spot the isomorphism?
> 6. In lines 3 and 4, T is used but never defined.
The rule:
H, f: A=>B >> T
----------------------------------------- elim f
H, f: A=>B >> A H, f: A=> B, y:B >> T
The normal use is to look at a goal that matches the
sequent above the line (so T is defined by assumption),
getting two subgoals.
> 7. This places two rules of inference (elim f, intro) on a vertical
> line without defining the meaning of this arrangement.
These are the two inference rules that reason about the
same connective.
> 8. What is rule # 2 trying to say?
If you want to show that something from an assumption A=>B ,
then it's enough to show both that A holds, and that your
original goal can be achieved with the extra assumption B.
> In rule # 3 below:
>
> 9. A is a set above, and in the top line [ x: A => B ] below, but is a
> formula in the bottom line below left side [ H, y:A >> B ].
Curry-Howard again ...
there are two readings. Either read things in terms of sets (types)
and functions, or read everything as formulas.
> 10. B is a set above and in the top line below [ x: A => B ], but a
> formula in the bottom line [ H, y:A >> B ] below.
Same.
> 11. What is rule # 3 trying to say?
If you want to show that all x:A. B holds (given H),
it's enough to show that B holds given the extra assumption that
some y is in A (and also show that A is a well formed type).
> In rule # 4 (axiom) below:
>
> 12.Doesn't the x:T already imply the T on the right side?
yes, that's why this is a (logical) axiom.
> 13. What is rule # 4 trying to say?
On assumption T, T holds.
>> * rule and axiom for showing type expressions are well formed
>>
>> 1. H >> A => B in u(1)
>> ------------------------------ intro
>> H >> A in u(1) H >> B in u(1)
>>
>> H >> u(1) in u(2)
>>
>> * rules for implication
>>
>> 2. H >> A => B
>> ----------- intro (y fresh)
>> H, y:A >> B
>>
>>
>> H, f: A=>B >> T
>> ----------------------------------------- elim f
>> H, f: A=>B >> A H, f: A=> B, y:B >> T
>>
>> * rule for universal quantifier
>> (read x:A=>B as forall x of type A, B(x)
>>
>> 3.
>> H >> x: A => B
>> ------------------------------ intro at 2
>> H, y:A >> B H >> A in u(2)
>>
>> * axiom
>>
>> 4. H, x:T >> T hyp(x)
>>
>>
>> Now we have an inference system, and we can generate proofs
>> of statements of the form "all A all B ... all F X"
>> where X just involves A,B,...F and the connective => .
>>
>> Here is a proof that gives every step required to prove
>> (a=>b=>c)=>(a=>b)=>(a=>c). The tree structure
>> is given by the indentation; the extra hypotheses introduced
>> by a rule application are given incrementally, so to see
>> what the formulas on the lhs of a sequent are, just go back up
>> the tree and pick them up as you go.
>>
>> [] complete
>> ==> a:u(1)=>b:u(1)=>c:u(1)=>(a=>b=>c)=>(a=>b)=>a=>c
>> by intro(at(2))
>
> How do you create [ a:u(1)=>b:u(1)=>c:u(1)=>(a=>b=>c)=>(a=>b)=>a=>c ] ?
That's the user's input goal.
> Intro at 2 (rule 3) doesn't give this.
intro(at(2)) is the inference rule applied to this goal;
this goal is at the root of the proof tree (marked []);
the two subgoals are at the first indentation level, labelled [1]
and [2] respectively.
>> [1] complete
>> 1. a:u(1)
>> ==> b:u(1)=>c:u(1)=>(a=>b=>c)=>(a=>b)=>a=>c
>> by intro(at(2))
>
> What does [1] mean, as opposed to [] above?
as above
>> [1] complete
>> 2. b:u(1)
>> ==> c:u(1)=>(a=>b=>c)=>(a=>b)=>a=>c
>> by intro(at(2))
>>
>> [1] complete
>> 3. c:u(1)
>> ==> (a=>b=>c)=>(a=>b)=>a=>c
>> by intro
>>
>> [1] complete
>> 4. v0:a=>b=>c
>> ==> (a=>b)=>a=>c
>> by intro
>
> What is v0 - where did it come from?
the intro rule requires a fresh variable in the first subgoal --
v0 in this case.
>> [1] complete
>> 5. v1:a=>b
>> ==> a=>c
>> by intro
>>
>> [1] complete
>> 6. v2:a
>> ==> c
>> by elim(v1)
>>
>> [1] complete
>> ==> a
>> by hyp(v2)
>
> How do you create a here?
the sequent above this point, got by looking up in the tree, is
[ a:u(1), b:u(1), c:u(1), v0: a=>b=>c, v1:a=>b, v2:a] ==> c
use the elim rule on the hypothesis v1:a=>b,
the first subgoal is:
[ a:u(1), b:u(1), c:u(1), v0: a=>b=>c, v1:a=>b, v2:a] ==> a
> C-B
>
>
--
Alan Smaill
|
|