|
|
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."
I think that a lot of people conclude that something that they don't
understand must be "advanced". It's also hard to understand
gibberish. Good example: The Boyer/Moore paper on formalizing Turing
1937 was discussed and I asked its supporters for the logical argument
that is being formalized in the paper. Nobody could give it. (There
is none.) So they believe that it contains something without ever
finding it.
> > > 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
I thought you meant the Resolution theorem-proving competition.
> > 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).
TPTP is a collection of theorems that serve as a benchmark for
theorem-provers. Good idea, but the "axioms" are given with each
theorem and are hard-wired for the theorem. For example, the Halting
Problem axioms have as a primitive proposition "The Halting Problem
is solvable." This is not at all general, would not generate
anything but itself, and totally misses how the Halting Problem fits in
with the rest of the Theory of Computation.
In CBL, the Halting Problem is just a Predicate Calculus wff, there is
only one (small) set of axioms, and all sorts of problems
(always-halting, ever-halting, membership, etc.) are also Predicate
Calculus wffs, and easily generated. (My ARXIV paper gives a number of
complete examples.)
I could hardly imagine a more stark contrast: a single hard-wired
"proof" vs. a general purpose scheme, which uses classic
mathematics with only a minor extension to express and prove Theory of
Computation results. Knowing how Theory of Computation results really
works (Predicate Calculus wffs formed from the proof predicate plus
Peano's Natural numbers being recursively enumerable) shows me they
totally missed it.
It is truly a shame that academia feeds the public such unadulterated
shit as this. In real life debate, people make points and
counter-points. The truth is reached by combining forces and weeding
out the good ideas from the bad. When has one journal article ever
questioned the validity of another? It's like being in the military
where questioning the commander is treason.
> 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.
But if each theorem has its own axioms, is that an axiomatic system for
proving these results?
> as to hardwiring...that's a value judgement that, again, I think you
> share with hardly anybody.
You don't see any problem with a different set of axioms for each
theorem (assuming it is so)?
> >- which are also (wrongly) propositional calculus.
>
> no, the TPTP axioms are first order.
Look at the Theory of Computation examples.
> > 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.
You really need to talk in technical, not personal, terms.
> 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).
Without examples, you have nothing (aside from warm and squishy.)
> > > > 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.
You refer to opinion rather than technical points. No, I think of real
problems of Program Synthesis: Mathematical functions and sets. My
ARXIV paper lists dozens of Number Theoretic problems, and solves some
of them. What does one quirky type translation problem - a program
that outputs a random program of a given type - give you? Who ever
asked for that as a Program Synthesis problem? What does that have to
do with creating useful programs that calculate real life Mathematical
functions?
> > 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).
You call the quirky type translation problem a good example? What
variations are there? What other problems does it apply to? What good
is creating a program that outputs a random program of a given type?
What Mathematician or Programmer even wrote, needed, or discussed this
problem? Apparently none. How many Mathematicians and Programmers
have wanted, discussed, and programmed Number Theoretic functions?
Countless many since antiquity.
How can you take such a stark contrast and compare the two? You are
equating zero and infinity. Calling that a Program Synthesis problem
is absolute nonsense with no basis in reality. Calling it an
"opinion" doesn't make sense in a scientific setting - not as a
result or achievement.
> 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.
All anyone can do is to admit that they have never seen one. Sort of
like martians from outer space.
> > > 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).
The right to face your accuser and get answers to questions. The
inadmissibility of unsubstantiated statements as evidence, or the use
of prejudicial statements. It's great!
> 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...;
At length?? Why is one type translation problem (asking for a program
that produces a random program of a given type) acceptable? Do you see
the difference between that and a vast collection of Number Theoretic
problems (see ARXIV paper)?
> 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?
Absolutely. What are the reasons?
> > > 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.
I beg your pardon - time is everything. There's also truth and
justice in there somewhere.
> > > 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.
What "them"? We agree on the definition of Program Synthesis.
Now, what realistic useful program has been shown to be generated
solely from the specification? How would you compare a single type
translation problem with a dozen Number Theoretic problems? Really.
> > 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.
There are also conferences on people who have been abducted by aliens
from space.
Mitch, you really have to point to an authentic example. Merely
quoting the names of systems and conferences just doesn't hack it.
That's just the superficial game of name-dropping.
> > > > 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'.
We can express FLT easily, but a system where, in effect, a particular
sentence is provable iff FLT is true, took 350 years.
> > 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?
New? Are you aware of the correspondence between logic and computing
(Turing Machines) discovered in the 1930's? wff = program, provable
= halt yes, refutable = halt no, proof = execution history?
> > 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)
How many ways can a wff characterize a given set?
C-B
> Mitch
|
|