"The same" must mean "the same bits." Even programs that have the same semantics in a high-level language aren't "the same" unless they're the same bits, since a compiler or an interpreter might run them differently on an actual machine. That's how I'd use it.
I never liked "observationally equivalent" because I don't think it's very precise. Everyone seems to have different opinions about what "counts" as an observable effect. I recently read this article discussing an optimization in the C++ compiler which surprised the author, because he thought that the program made a change to the "observational" semantics of his program, and the compiler didn't:
Saying that two programs are equivalent *assumes* a given semantics according to which they have the same meaning. If you know the context, which semantics should be clear. If you don't - then indeed clarify the context.
In the end, for any bitwise-different programs, you can find a semantics that distinguishes them. Worse: even if the two programs are bitwise identical, by the very assumption that they are two programs, and in the context of linear logic at the meta-level, they are different! Indeed, by the virtue of their being two they appear in different contexts, and thus are different. For instance one is on your harddrive, and will have a future determined by your harddrive's continuation, whereas mine is on my harddrive, and will have a different continuation.
On the other hand, if you only care about observable I/O through evaluation by some given semantics, ignoring time and space constraints, then I'm sure we can prove that seen in some useful light, (+ 2 2) and 4 are the same program.
As Fare hinted, formally, equivalence depends on the semantic model of the language.
Generally, if one is dealing with an imperative language of some sort, we say that two programs are equivalent if the language's step relation will transform the store in the same way for both programs. Some distinctions happen if you're using big step vs. small step semantics, if the programming language is imperative vs. functional, etc., but generally, the idea seems to be that "equivalent programs transform things equivalently".
Benjamin Pierce's book "Types and Programming Languages" or his lecture notes for "Software Foundations" (online) can tell you more. The latter includes a section in which formal proofs of equivalence are performed using the Coq proof assistant system.
Note that one can personally have very different definitions of "equivalence", but this is what a computer scientist involved in programming language theory generally means these days.
And so the distinctions proposed by jrm are usually made in the context of layering the meaning of programs in terms of SYNTAX and SEMANTICS.
The SYNTAX layer is made to be simple. It abstracts away details such as whitespace or character streams, and provides a basic recursive data structure on top of which to explain the semantics. Whether two programs are 'the same' according to the SYNTAX layer is the matter of a trivial linear-time comparison of the programs' respective syntax trees.
The SEMANTICS layer handles all the difficult computations, the time and space complexity, ambiguity, divergence, context-dependence, etc. Whether two programs are (observationally) equivalent according to the considered SEMANTICS is a hard problem usually without a guaranteed computable answer.
Some people layer a STATIC SEMANTICS between the SYNTAX and the (let's call it DYNAMIC) SEMANTICS of programs, associating types to programs through some mechanism that is hopefully simpler and cheaper than evaluating programs. Sometimes the dynamic semantics can be explained simply without mentioning the intermediate static semantics at all: it is a "type erasure semantics", as in ML. Sometimes as in Haskell, the very definition of the DYNAMIC SEMANTICS is crucially expressed in terms of the STATIC SEMANTICS; it is a type-passing semantics.
If your static analysis allows to express the fact that two programs are equivalent, then they may be called intensionally equivalent. Otherwise, the usual "extensional" observational equivalence applies.
The definitions of equivalence used in programming language theory don't generally have anything to do with static vs. dynamic. Indeed, it is often necessary to prove things about the dynamic behavior of programs to do a proof of equivalence.
One of the major activities of a compiler is (in effect) to prove that certain programs are equivalent. The translation of a high level language into a lower level one is an exercise in generating an equivalent program, optimizations and other program transformations hopefully produce equivalent programs, etc. Proofs of correctness in compilers are strongly related to proofs of equivalence of the transformed versions of programs and their originals.
5 comments:
"The same" must mean "the same bits." Even programs that have the same semantics in a high-level language aren't "the same" unless they're the same bits, since a compiler or an interpreter might run them differently on an actual machine. That's how I'd use it.
I never liked "observationally equivalent" because I don't think it's very precise. Everyone seems to have different opinions about what "counts" as an observable effect. I recently read this article discussing an optimization in the C++ compiler which surprised the author, because he thought that the program made a change to the "observational" semantics of his program, and the compiler didn't:
http://blog.regehr.org/archives/140
Speak about putting the cart before the horse!
Saying that two programs are equivalent *assumes* a given semantics according to which they have the same meaning. If you know the context, which semantics should be clear. If you don't - then indeed clarify the context.
In the end, for any bitwise-different programs, you can find a semantics that distinguishes them. Worse: even if the two programs are bitwise identical, by the very assumption that they are two programs, and in the context of linear logic at the meta-level, they are different! Indeed, by the virtue of their being two they appear in different contexts, and thus are different. For instance one is on your harddrive, and will have a future determined by your harddrive's continuation, whereas mine is on my harddrive, and will have a different continuation.
On the other hand, if you only care about observable I/O through evaluation by some given semantics, ignoring time and space constraints, then I'm sure we can prove that seen in some useful light, (+ 2 2) and 4 are the same program.
As Fare hinted, formally, equivalence depends on the semantic model of the language.
Generally, if one is dealing with an imperative language of some sort, we say that two programs are equivalent if the language's step relation will transform the store in the same way for both programs. Some distinctions happen if you're using big step vs. small step semantics, if the programming language is imperative vs. functional, etc., but generally, the idea seems to be that "equivalent programs transform things equivalently".
Benjamin Pierce's book "Types and Programming Languages" or his lecture notes for "Software Foundations" (online) can tell you more. The latter includes a section in which formal proofs of equivalence are performed using the Coq proof assistant system.
Note that one can personally have very different definitions of "equivalence", but this is what a computer scientist involved in programming language theory generally means these days.
And so the distinctions proposed by jrm are usually made in the context of layering the meaning of programs in terms of SYNTAX and SEMANTICS.
The SYNTAX layer is made to be simple. It abstracts away details such as whitespace or character streams, and provides a basic recursive data structure on top of which to explain the semantics. Whether two programs are 'the same' according to the SYNTAX layer is the matter of a trivial linear-time comparison of the programs' respective syntax trees.
The SEMANTICS layer handles all the difficult computations, the time and space complexity, ambiguity, divergence, context-dependence, etc. Whether two programs are (observationally) equivalent according to the considered SEMANTICS is a hard problem usually without a guaranteed computable answer.
Some people layer a STATIC SEMANTICS between the SYNTAX and the (let's call it DYNAMIC) SEMANTICS of programs, associating types to programs through some mechanism that is hopefully simpler and cheaper than evaluating programs. Sometimes the dynamic semantics can be explained simply without mentioning the intermediate static semantics at all: it is a "type erasure semantics", as in ML. Sometimes as in Haskell, the very definition of the DYNAMIC SEMANTICS is crucially expressed in terms of the STATIC SEMANTICS; it is a type-passing semantics.
If your static analysis allows to express the fact that two programs are equivalent, then they may be called intensionally equivalent. Otherwise, the usual "extensional" observational equivalence applies.
Is that what you meant?
The definitions of equivalence used in programming language theory don't generally have anything to do with static vs. dynamic. Indeed, it is often necessary to prove things about the dynamic behavior of programs to do a proof of equivalence.
One of the major activities of a compiler is (in effect) to prove that certain programs are equivalent. The translation of a high level language into a lower level one is an exercise in generating an equivalent program, optimizations and other program transformations hopefully produce equivalent programs, etc. Proofs of correctness in compilers are strongly related to proofs of equivalence of the transformed versions of programs and their originals.
Post a Comment