7 ms·
I'm reminded of the Philosophy of Computer Science entry in the Stanford Encyclopedia of Philosophy [0], which briefly considers what it means for two programs
by jkaptur 2y ago
I'm reminded of the Philosophy of Computer Science entry in the Stanford Encyclopedia of Philosophy [0], which briefly considers what it means for two programs to be identical.
"... it has been argued that there are cases in which it is not possible to determine whether two programs are the same without making reference to an external semantics. Sprevak (2010) proposes to consider two programs for addition which differ from the fact that one operates on Arabic, the other one on Roman numerals. The two programs compute the same function, namely addition, but this cannot always be established by inspecting the code with its subroutines; it must be determined by assigning content to the input/output strings"
"The problem can be tackled by fixing an identity criterion, namely a formal relation, that any two programs should entertain in order to be defined as identical. Angius and Primiero (2018) show how to use the process algebra relation of bisimulation between the two automata implemented by two programs under examination as such an identity criterion. Bisimulation allows to establish matching structural properties of programs implementing the same function, as well as providing weaker criteria for copies in terms of simulation."
(Of course, it isn't surprising that this would be relevant, because proofs and programs themselves are isomorphic).
This technique seems rather stricter than what Gowers has in mind, but it seems helpful as a baseline.
0. https://plato.stanford.edu/entries/computer-science/ https://plato.stanford.edu/entries/computer-science/
- chongli 2y agoI think it's also important to make a distinction between a pair of programs which compute the same function using an identical amount of space and time and a pair of programs which compute the same function with different amounts of either space or time (or both). Two programs might compute the same function and be considered formally identical in that sense but may be in radically different complexity classes [O(1) vs O(n) vs O(n^2) vs O(2^n)]. Formally we may not be interested in this distinction but practically we definitely are. One program may be extremely practical and useful whereas the other might not finish computing anything before the heat death of the universe on anything but trivial-sized inputs.
- setopt 2y agoOn the other hand, compiler tricks like tail call optimization can e.g. reduce an O(n) algorithm to an O(1) algorithm. Is it a “different program” if the same source code is compiled with a new compiler?
- Jtsummers 2y agoTail call optimization does not turn O(n) algorithms into O(1) algorithms unless you're talking about the space used and not the runtime.
- naniwaduni 2y agoAt a certain level of abstraction, that's easily an example of converting an O(n log n) algorithm into an O(n) one. In practice, of course, the effect is far more dramatic with a MMU.
- Jtsummers 2y agoCan you show a O(n log n) algorithm with tail calls but not TCO that's O(n) after being optimized with TCO?
- naniwaduni 2y agoComputing f(0)=0; f(n)=f(n-1) is O(n log n) without tail calls because you need O(log n) addresses to hold your stack frames.
- Jtsummers 2y ago> Computing f(0)=0; f(n)=f(n-1) is O(n log n) without tail calls because you need O(log n) addresses to hold your stack frames. There are two principal ways of applying asymptotic analysis to algorithms: time or memory used. In both, your procedure is O(n) without TCO. With TCO it is O(n) for runtime (though further optimization would reduce it to O(1) since it's just the constant function 0, but TCO alone doesn't get us there) and O(1) for space since it would reuse the same stack frame. What O(log n) addresses do you need to hold the stack frames when there are O(n) stack frames needing O(n) addresses (without TCO, which, again, reduces it to O(1) for memory)? Also, regarding "without tail calls", your example already has tail calls. What do you mean by that?
- tightbookkeeper 2y agoKnuth answers this question in chapter 0.
- cloogshicer 2y agoIn which book? Sounds interesting.
- tightbookkeeper 2y agoArt of computer programming volume 1. It’s an exercise with a solution at the end.
- cloogshicer 2y agoThank you, will look into it!
- drpossum 2y agoYou've misunderstood the difference of "sameness" those two works are trying to address. Knuth is not using an equivalent idea of "sameness" as discussed above. Two people each going by Philosophy of Computer Science and the Art of Computer Programming exercise notion would not always agree if two programs are "the same". It's also a bridge too far to make a blanket statement of Knuth "already answered this" (it's also not accurate to attribute that idea to Knuth; e.g. Church did work exactly on this decades before). Meaningful discourse and mathematical analysis requires nuance and degrees of equivalence and mixing them up makes it needlessly confusing and difficult. Sameness as "same input same output" is NOT the same as the "isomorphic equivalence" which is more difficult, strict, and abstract. In this sense they are the same if they follow the same "steps" (also isomorphic between programs), i.e. they are different representations of the same algorithm.
- tightbookkeeper 2y ago> same input same output He doesn’t say this. > NOT the same as the "isomorphic equivalence" which is more difficult, strict, and abstract. This is what the exercise is about. So I would recommend reading before making assumptions. Of course there are more than one definition of equivalence and isomorphism, but the one explored there is just as interesting as the comment I’m replying to. drpossum you stop with these gotcha posts? This is our 3rd encounter.
- mentalically 2y agoIn the most general case there is no technique that can determine if two programs are equivalent other than running both programs on some set of inputs and verifying that the outputs (after termination) are the same. Every other technique must cut out all possible sources of non-termination to get around the halting problem in order to make the resulting equivalence relation on the set of programs effectively computable and constructively provable.