No, I mean the obvious implementation would have the program basically asking “what does this program return? Well, it tries to find out what this program returns. What does this program return? Well, it tries to find out...” until it hits the length limit and comes back with no solution found (or, if the length limit is lifted, keeps going forever). This is true even if the proof checker always returns quickly.
This is absolutely not the obvious implementation of the algorithm in the post. My program does not “try to find out” something. It mechanically checks all proofs up to some maximum length. You can’t just replace a piece of code with another piece that has a vaguely similar intent, but fails to halt!
The ‘fails to halt’ part in either case would be only if the length limit were removed. But you are right that mechanically checking all proofs up to a maximum length is a mathematically valid implementation and can only be replaced with another piece of code that is guaranteed to give an identical result.
However, that implementation can still be reasonably described as trying to find out something. The intent can be seen not in the simple loop that iterates through all proofs up to a certain length, but in the choice of logic and axioms to encode the problem. The proofs generated from suitably chosen axioms are isomorphic to execution paths of an appropriately written program (as whpearson observed, a way to see this is to consider the Curry-Howard correspondence).
No, I mean the obvious implementation would have the program basically asking “what does this program return? Well, it tries to find out what this program returns. What does this program return? Well, it tries to find out...” until it hits the length limit and comes back with no solution found (or, if the length limit is lifted, keeps going forever). This is true even if the proof checker always returns quickly.
This is absolutely not the obvious implementation of the algorithm in the post. My program does not “try to find out” something. It mechanically checks all proofs up to some maximum length. You can’t just replace a piece of code with another piece that has a vaguely similar intent, but fails to halt!
The ‘fails to halt’ part in either case would be only if the length limit were removed. But you are right that mechanically checking all proofs up to a maximum length is a mathematically valid implementation and can only be replaced with another piece of code that is guaranteed to give an identical result.
However, that implementation can still be reasonably described as trying to find out something. The intent can be seen not in the simple loop that iterates through all proofs up to a certain length, but in the choice of logic and axioms to encode the problem. The proofs generated from suitably chosen axioms are isomorphic to execution paths of an appropriately written program (as whpearson observed, a way to see this is to consider the Curry-Howard correspondence).
This isn’t the same as the calculator that asks itself what value it will return, because there’s a subtle separation of levels here.