Programmers generate every possible melody in MIDI to prevent lawsuits

Re:Programmers generate every possible melody in MIDI to pre... by dmurray on Friday February 28, 2020 @05:59AM (#22441946)

Kind of. A constructive proof by definition means something like you can explain exactly what the number is in a finite number of bytes.

The standard diagonalization argument is a constructive proof, identifying a specific number. Normally a constructive proof is preferable. But with a bit of hand waving you can make it into a non-constructive proof that there are "unknowable" numbers that cannot be described in any finite amount of bytes.

[ Parent | on HN ]

Re:Programmers generate every possible melody in MIDI to pre... by afiori on Friday February 28, 2020 @07:55AM (#22442428)

In practice constructible for reals mean that you can approximate them with arbitrarily small know precision e.g. a sequence of retional number numbers q_n each no more that 1/n apart from the actual real number.

The point is that such a sequence needs to be constructive in the usual sense, so there are still only a countable number of them.

[ Parent | on HN ]