|
|
Charlie-Boo wrote:
> Mitch Charlie-Boo Mitch wrote:
>
> > > > Charlie-Boo wrote:
> > > > > Mitch wrote:
> > > > > > Charlie-Boo wrote:
> > > > > > > Because nobody has shown a Program Synthesis system before.
> > > > > > > Nobody can
> > > > > > > show that theirs works.
> >
> > OK how's this: you're right for an interpretation of 'Program
> > Synthesis' that pretty much nobody shares with you.
>
> Which is what? And the correct definition is what?
>
> My definition is that you input a statement that asserts what the
> program must do (e.g. in English, Set Theory, or Predicate Calculus -
> they're all the same) and it outputs one or more computer programs
> that do what you said. If you don't think that's Program
> Synthesis, then call it something else.
>
> (Long ago I developed this type of response to those who attempt to
> debate terminology. The point isn't that "It does Program
> Synthesis, whatever is the correct definition of Program Synthesis.",
> but rather, "It creates computer programs, which people usually call
> Program Synthesis.")
Great. That sounds like a good definition of "Program Synthesis". And
I'm with you on the point about terminology. Maybe the difference is in
our usage. You said:
"nobody has shown a Program Synthesis system before"
and since I believe that they have, I infer that our ideas of what PS
means must be different And because I believe that many other people
agree with me, that's why I say that you have:
"...an interpretation of 'Program Synthesis' that pretty much nobody
shares with you."
> > Neither of us is convincing the other of anything. Maybe another forum
> > would be more receptive to your ideas. Submit to CADE.
>
> That's for propositional calculus (Resolution) theorem-proving, I
> believe.
No, it's a conference for all sorts of theorem proving: first order,
2nd, higher order, substructural logics, etc. Research in propositional
systems has moved over (for political/administrative resource reasons)
mostly to CAV or SAT
> TPTP is for general theorem-proving,
TPTP is a collection of theorems supported by a single research group,
not a proving system (on the one hand), and not a vetting system
(peer/expert review). I was implying that you should submit to CADE or
some other related conference as the latter (usenet does not tend to
give particularly robust reviews). TPTP is a place to get
already-formed theorem statements to test on a newcomer's proving
system (like for benchmarking).
> but they give you the (BS - hardwired for each theorem) axioms to make it
> easier for their
> professor friends
so logical content is sometimes in axioms, sometimes in rules of
inference; there's an efficiency tradeoff.
as to hardwiring...that's a value judgement that, again, I think you
share with hardly anybody.
>- which are also (wrongly) propositional calculus.
no, the TPTP axioms are first order.
> My ARXIV paper gives 8 examples, describing each in detail, and I offer
> to answer any questions. If anyone did likewise for any other system,
> I would gladly be convinced.
I think you're blinded by your interest in your own system. As
advertisment, Otter/Mace is another excellent 1st order theorem prover.
(I can't remember of there is a program synthesis part (like there is
for nuPRL) but one can think of Mace (the finite model checker) as a
way of calculating (finite) models for first order sentences).
> > > Calling it a "proof" implies that it can be generated. That is part of
> > > the Big Lie.
> > >
> > > The only way to cut through this gibberish is to supply a complete
> > > formal example. And by example, this means that it is a general scheme
> > > that includes many program requirements, not just one quirky type
> > > translation problem.
> >
> > Well, I think Alan Smaill went through a lot of trouble to show you one.
>
> No, it was the quirky type translation problem.
Another terminology/interpretation problem...one can always think of a
correspondence (however complicated) as translation; you think it's
trivial, others do not.
> After I asked about 5
> times, he claimed that it could solve the real Program Synthesis
> problems of deciding and enumerating factors. And guess what happened
> when I asked for examples of programs that are generated to solve these
> problems?
I'd be curious to see such an example program, too, but it might take a
lot of work on his part; he might be doing you a big favor by doing the
work, or he may realize that his troubles aren't worth it (because
every time he's come up with perfectly convincing examples, you don't
sem to be convinced). Or there is certainly the possibility that
absolutely no Program Synthesis system has ever been invented (other
than yours of course) to take care of that problem. I personally don't
know enough about all of them right now to support that latter
statement.
> > Normally a prof giving a class would do an example (as part of his
> > duties as a prof) and expect the student to follow up with
> > reading/homework. Here (usenet) nobody owes anybody anything.
>
> Anyone who makes a contrary claim to anyone owes them a substantiation
> of that claim. (Read the U. S. Constitution.)
(I don't see how the Constitution is relevant). Right, burden of proof.
You originally said: PS doesn't exist; others responded, yes, they do,
look at X,Y,Z....; you said, that's not PS; others said, yes it is,
here's an example; you said, no that's not an acceptable answer; others
said, "Hunh?", tried to explain why they are acceptable at length...;
you said, no that's not acceptable... can we now ask you to support
(take the burden of proof) why those reasons are not acceptable?
> > He's just
> > doing you (and anybody who is skeptical like you) a favor
>
> His unsubstantiated bullshit is a favor? How much do I owe for that
> favor?
Exactly. Nothing. You didn't like it? Well, you didn't pay anything for
it anyway.
> > You'll get many complete formal examples
> > (Curry-Howard, Program synthesis, theorem proving, etc, etc) supplying
> > them yourself by downloading and running the many apps out there.
>
> There are plenty of articles that explain them. Why would anyone be
> stupid enough to spend 5 days trying to download, install, learn, and
> use unsupported software to see what it does when he can read about it
> in 5 minutes? The articles show that it's warm and squishy.
OK, so none of them are good enough for you. Fine.
> If Program Synthesis systems exist, then why do people waste time with
> Hurry-Coward which even its supporters say is only "a first step"
> and not an actual Program Synthesis system?
>
> Either you are saying that without any evidence or you are purposely
> holding back your examples. Which is it?
Did anybody mention nuPRL yet? google for it.
Oh man, I'm really out of my mind. I forgot to mention LOPSTR (another
conference), loko at papers there.
> > > BTW Deciding what constitutes a "program" is extremely interesting. It
> > > seems on the surface to be the same problem that Logicians have been
> > > grappling with forever:
> >
> > Oh man, that is almost exactly what we've been trying to get at, that
> > there is not just an intuitive analogy between programs and proofs, but
> > a formal correspondence.
>
> No, I mean express vs. represent. It is easy to express a set but
> harder to write a program to generate it. It is the difference between
> the set of true sentences and the set of provable ones. It is trivial
> to express Fermat's Last Theorem, but took 350 years to represent it.
hmm... I didn't understand how you meant 'represent'. It sounds like
'proof'.
> And the correspondence is between wffs and programs, not proofs and
> programs.
Which correspondence? CH talks about a correspondence between proofs
and programs, plain and simple. Maybe you're saying that the CH
correspondence is not the important one people should be looking at?
And that your (new?) wff-program is more important?
> A wff represents a set (the set of values that when
> substituted for its free variable produces a provable sentence) and a
> program enumerates it.
Are you defining wff anew here (i.e. let's define a wff to be a set
with these properties)...? or are you just saying one can represent a
set using a wff? (I tend to think of a 'wff' as simply a grammar)
Mitch
|
|