Charlie-Boo <shymathguy@gmail.com> writes:

> On Monday, December 27, 2021 at 11:02:07 AM UTC-5, Ben Bacarisse wrote:
>> Charlie-Boo <shyma...@gmail.com> writes:
>>
>> > What is a "vague reference"?
>> One that does not have enough detail for someone else to confirm what
>> you claim. No one asserts what you claim they do. Arguing against a
>> made-up claim is just a waste of time.
>
> "Program synthesis is the mechanized construction of software."
>
> Program synthesis: challenges and opportunities
> Cristina David - University of Cambridge
> October 2017Philosophical Transactions of The Royal Society A
> Mathematical Physical and Engineering Sciences

Nowhere does this paper say that mathematics and computer science have
been automated. It's a rather cautious paper. Even so, it's a probably
a bit optimistic, given the history of the subject. But it does not say
what you set up as the big lie. In fact, I can't see any lies in it.

> "A proof by a computer program of the unsolvability of the halting
> problem is described."
>
> A Mechanical Proof of the Unsolvability of the Halting Problem
> Robert S. Boyer, J. Strother Moore
> Journal of the ACM, Volume 31, Issue 3, July 1984, pp 441–458,
> https://doi.org/10.1145/828.1882)

I gave you the full citation for this one when I explain that it too
fails to support your polemic.

--
Ben.

On Monday, December 27, 2021 at 3:59:40 PM UTC-5, Ben Bacarisse wrote:
> Charlie-Boo <shyma...@gmail.com> writes:
>
> > On Monday, December 27, 2021 at 11:02:07 AM UTC-5, Ben Bacarisse wrote:
> >> Charlie-Boo <shyma...@gmail.com> writes:
> >>
> >> > What is a "vague reference"?
> >> One that does not have enough detail for someone else to confirm what
> >> you claim. No one asserts what you claim they do. Arguing against a
> >> made-up claim is just a waste of time.
> >
> > "Program synthesis is the mechanized construction of software."
> >
> > Program synthesis: challenges and opportunities
> > Cristina David - University of Cambridge
> > October 2017Philosophical Transactions of The Royal Society A
> > Mathematical Physical and Engineering Sciences
> Nowhere does this paper say that mathematics and computer science have
> been automated. It's a rather cautious paper. Even so, it's a probably
> a bit optimistic, given the history of the subject. But it does not say
> what you set up as the big lie. In fact, I can't see any lies in it.
> > "A proof by a computer program of the unsolvability of the halting
> > problem is described."
> >
> > A Mechanical Proof of the Unsolvability of the Halting Problem
> > Robert S. Boyer, J. Strother Moore
> > Journal of the ACM, Volume 31, Issue 3, July 1984, pp 441–458,
> > https://doi.org/10.1145/828.1882)
> I gave you the full citation for this one when I explain that it too
> fails to support your polemic.
>
> --
> Ben.

Then what are they claiming that they did?

Did they show any examples of doing whatever you call it?

Whatever you call it, it is a lie because they did nothing, They have nothing to show. No programs, no proofs.

You're just arguing over terminology. They are liars. They say that software generated the programs, generated the theorems. Call it anything you want. It's a lie. They have not created a system to generate programs or theorems.

You say: "In fact, I can't see any lies in it."
They say: "A proof by a computer program of the unsolvability of the halting problem is described."

What is that proof - spell it out - write it here. If they are telling the truth, then where is it?

You claim it does what they say, but when I say show it - it's my responsibility? To do the impossible.

You say they are telling the truth. Then prove it. What is that proof they generated?

"Program synthesis is the mechanized construction of software.
"A proof by a computer program of the unsolvability of the halting problem is described."

What does this mean?
It mean computer programming - the construction of software - has been automated by having software do it.
It means part of mathematics - theorem proving - has been automated by having software do it.

They don't generate anything.
They don't automate anything.
They don't create programs, proofs, theorems, anything.

They have no examples of programs created. They have no examples of proofs generated.

I offer $100.00 through fiverr.com for anyone who can show me a system that generates programs.
Input a nonprocedural specification, output a non-trivial program.
Generate 3 programs and you get $100.00 through an agreement on the fiverr.com website for hiring people.

Nobody collects it. I could make it $200 or more.

C-B

I don't really understand all the details of the thread (long and difficult for me).
But the terms Automatic Theorem Proving, Program Synthesis are really implying
Big Lie if they could be translated to Halting Problem or related corollaries
e.g. language translation, depending how big they were.

There are full of lies in media everyday, every moment (If you can pick up, good).

We hear radio, watching TV,..., receiving information. Commercial advertisement
is the first example. 'Lies' in academia is no better, because they are mostly driven
by reward. No reward no research. But no saying is absolute like this saying is not.

On Monday, December 27, 2021 at 8:05:57 PM UTC-5, wij wrote:
> I don't really understand all the details of the thread (long and difficult for me).
> But the terms Automatic Theorem Proving, Program Synthesis are really implying
> Big Lie if they could be translated to Halting Problem or related corollaries
> e.g. language translation, depending how big they were.
>
> There are full of lies in media everyday, every moment (If you can pick up, good).
>
> We hear radio, watching TV,..., receiving information. Commercial advertisement
> is the first example. 'Lies' in academia is no better, because they are mostly driven
> by reward. No reward no research. But no saying is absolute like this saying is not.

Program Synthesis means mapping a specification to one or more computer programs in a given programming language that perform the indicated calculation. The specification can be a FOL wff with an indication of input (decide) or output (enumerate). The Halting Problem is the specification that is the halting set (program plus input that halt) as input i.e. decide if a given program plus input is a member i.e. does it halt.

Published research on Program Synthesis doesn't address it because they have made no progress - no programs have ever been generated (such claims are false) - but no program could be created and if it is smart then it declares that is the case and possibly with a proof e.g. the Turing '37 proof.

Now, the BS extends into Computability (aka Theory of Computation) with a bogus claim of a program that proves the halting set is undecidable. But it is a simple proof and with the advent of Kleene's Arithmetic Hierarchy it is trivial. Any relation that is not recursive cannot be decided (input) and any relation that is not recursively enumerable cannot be enumerated (output.)

So yes, there are many aspects of the Big Lie of Academia, indeed.

C-B

On Tuesday, 28 December 2021 at 10:51:34 UTC+8, Charlie-Boo wrote:
> On Monday, December 27, 2021 at 8:05:57 PM UTC-5, wij wrote:
> > I don't really understand all the details of the thread (long and difficult for me).
> > But the terms Automatic Theorem Proving, Program Synthesis are really implying
> > Big Lie if they could be translated to Halting Problem or related corollaries
> > e.g. language translation, depending how big they were.
> >
> > There are full of lies in media everyday, every moment (If you can pick up, good).
> >
> > We hear radio, watching TV,..., receiving information. Commercial advertisement
> > is the first example. 'Lies' in academia is no better, because they are mostly driven
> > by reward. No reward no research. But no saying is absolute like this saying is not.
> Program Synthesis means mapping a specification to one or more computer programs in a given programming language that perform the indicated calculation. The specification can be a FOL wff with an indication of input (decide) or output (enumerate). The Halting Problem is the specification that is the halting set (program plus input that halt) as input i.e. decide if a given program plus input is a member i.e. does it halt.
>
> Published research on Program Synthesis doesn't address it because they have made no progress - no programs have ever been generated (such claims are false) - but no program could be created and if it is smart then it declares that is the case and possibly with a proof e.g. the Turing '37 proof.
>
> Now, the BS extends into Computability (aka Theory of Computation) with a bogus claim of a program that proves the halting set is undecidable. But it is a simple proof and with the advent of Kleene's Arithmetic Hierarchy it is trivial. Any relation that is not recursive cannot be decided (input) and any relation that is not recursively enumerable cannot be enumerated (output.)
>
> So yes, there are many aspects of the Big Lie of Academia, indeed.
>
> C-B

'Program Synthesis' is read to me like language translation, which we know is
an undecidable problem (natural language translators are practical anyway).

Many academia produced papers are actually for reward.
Many papers produced I know deliberately invent some abstract, obscure
notion/symbols in order to pass examination, no real thing is new there but
rephrase the same old thing in different perspective (even in books). This is
not a real lie but full of garbage in academia is true, and increasing every year.

To add to the Big Lie, I published a medical level nicotine extraction method
in Chinese to refute many lies from a Big Lie made by my government (to help
nicotine intakers), a lie too big for me to ignore.
https://sourceforge.net/projects/cscall/files/MisFiles/Nicotine-extraction.txt/download
Interesting readers (with chemical knowledge) can use google translator to
understand the contents.

On Wednesday, December 29, 2021 at 1:57:36 AM UTC-5, wij wrote:
> On Tuesday, 28 December 2021 at 10:51:34 UTC+8, Charlie-Boo wrote:
> > On Monday, December 27, 2021 at 8:05:57 PM UTC-5, wij wrote:
> > > I don't really understand all the details of the thread (long and difficult for me).
> > > But the terms Automatic Theorem Proving, Program Synthesis are really implying
> > > Big Lie if they could be translated to Halting Problem or related corollaries
> > > e.g. language translation, depending how big they were.
> > >
> > > There are full of lies in media everyday, every moment (If you can pick up, good).
> > >
> > > We hear radio, watching TV,..., receiving information. Commercial advertisement
> > > is the first example. 'Lies' in academia is no better, because they are mostly driven
> > > by reward. No reward no research. But no saying is absolute like this saying is not.
> > Program Synthesis means mapping a specification to one or more computer programs in a given programming language that perform the indicated calculation. The specification can be a FOL wff with an indication of input (decide) or output (enumerate). The Halting Problem is the specification that is the halting set (program plus input that halt) as input i.e. decide if a given program plus input is a member i.e. does it halt.
> >
> > Published research on Program Synthesis doesn't address it because they have made no progress - no programs have ever been generated (such claims are false) - but no program could be created and if it is smart then it declares that is the case and possibly with a proof e.g. the Turing '37 proof.
> >
> > Now, the BS extends into Computability (aka Theory of Computation) with a bogus claim of a program that proves the halting set is undecidable. But it is a simple proof and with the advent of Kleene's Arithmetic Hierarchy it is trivial. Any relation that is not recursive cannot be decided (input) and any relation that is not recursively enumerable cannot be enumerated (output.)
> >
> > So yes, there are many aspects of the Big Lie of Academia, indeed.
> >
> > C-B
> 'Program Synthesis' is read to me like language translation, which we know is
> an undecidable problem (natural language translators are practical anyway).
>
> Many academia produced papers are actually for reward.
> Many papers produced I know deliberately invent some abstract, obscure
> notion/symbols in order to pass examination, no real thing is new there but
> rephrase the same old thing in different perspective (even in books). This is
> not a real lie but full of garbage in academia is true, and increasing every year.
>
> To add to the Big Lie, I published a medical level nicotine extraction method
> in Chinese to refute many lies from a Big Lie made by my government (to help
> nicotine intakers), a lie too big for me to ignore.
> https://sourceforge.net/projects/cscall/files/MisFiles/Nicotine-extraction.txt/download
> Interesting readers (with chemical knowledge) can use google translator to
> understand the contents.

Yes, every Program Synthesis request is in some logical language and each resulting program is in a particular programming language. However, it is not translation from one language to another in the sense of natural language translation of the syntactic elements of one language to its semantics to the syntax for each of these semantics in another language.

That would be 1-to-1 (aside from synonyms.) There are many ways to code a particular function and in fact no way to if it is not computable (regardless of the target language.) We cannot "translate" a request for a program to solve the halting problem or enumerate all non-halting programs.

Rather, Program Synthesis is expressing the net result of a calculation in terms of arbitrary semantics in the target language [missing from almost all published discussions of how to perform Program Synthesis] aided by mathematical identities. An expression for the modulo operation can be calculated by integer division and remainder. A loop to sum the integers from 1 to N could be expressed as N times the sum of N and 1 all divided by 2, due to a proof by Induction of their equivalence (handy for competitive programming.)

So Induction is not used to create every loop, as Per Martin-Löf and his followers have proclaimed, but rather to eliminate a loop on the occasion that its mathematical nature can be reduced to a constant time expression. Loops may be needed to enumerate a set or search for a factor of a number, which has nothing to do with proof by induction that every natural number has some particular property.