Hmm. If we’re trying to argmax some function f over the real numbers, then the simplest algorithm would be something like “iterate over all mathematical expressions e; for each one, check whether the program ‘iterate over all provable theorems, halting when you find one that says e=argmaxf’ halts; if it does, return e.”
...but I guess that’s not guaranteed to ever halt, since there could conceivably be an infinite procession of ever-more-complex expressions, eking out ever-smaller gains on f. It seems possible that no matter what (reasonably powerful) mathematical language you choose, there are function-expressions with finite maxima at values not expressible in your language. Which is maybe what you meant by “as far as I know there can’t be [an algorithm for it].”
(I’m assuming our mathematical language doesn’t have the word argmax, since in that case we’d pretty quickly stumble on the expression argmaxf, verify that argmaxf=argmaxf, and return it, which is obviously a cop-out.)
Hmm. If we’re trying to argmax some function f over the real numbers, then the simplest algorithm would be something like “iterate over all mathematical expressions e; for each one, check whether the program ‘iterate over all provable theorems, halting when you find one that says e=argmaxf’ halts; if it does, return e.”
...but I guess that’s not guaranteed to ever halt, since there could conceivably be an infinite procession of ever-more-complex expressions, eking out ever-smaller gains on f. It seems possible that no matter what (reasonably powerful) mathematical language you choose, there are function-expressions with finite maxima at values not expressible in your language. Which is maybe what you meant by “as far as I know there can’t be [an algorithm for it].”
(I’m assuming our mathematical language doesn’t have the word argmax, since in that case we’d pretty quickly stumble on the expression argmaxf, verify that argmaxf=argmaxf, and return it, which is obviously a cop-out.)