4 ms·

> All really express the same computation -- the operational semantics are isomorphic The operational semantics are certainly not isomorphic. fac1 consumes st

by tome 9y ago

> All really express the same computation -- the operational semantics are isomorphic The operational semantics are certainly not isomorphic. fac1 consumes stack, for example, and fac2 doesn't.

pron 9y ago
So what? That's still isomorphic (I said isomorphic, not identical), as you can map a value to a stack state and vice-versa. See my Java programs in the comment below, where I explicitly perform a mapping on the state of the stack to map it to a variable in a different expression of the computation. My talk (https://www.youtube.com/watch?v=15uy9Ga-14I https://www.youtube.com/watch?v=15uy9Ga-14I) addresses this precise point.
- tome 9y ago
  I'm confused. It would be a very strange operational semantics that considered an O(n)-space program isomorphic to an O(1)-space program. What is your notion of "isomorphism" here?
  - pron 9y ago
    > It would be a very strange operational semantics that considered an O(n)-space program isomorphic to an O(1)-space program. Why? Intuitively, wouldn't you consider Euclid's algorithm operating on unary and binary representations of numbers isomorphic despite the exponential difference in complexity? We can have complexity preserving isomorphisms and non-preserving isomorphisms, and it's quite easy to see from the mappings which is which. That's exactly why, if you're writing a reduction to prove complexity bounds, you must show that the reduction itself is polynomial. Otherwise, you get a mapping, but not one that preserves complexity. > What is your notion of "isomorphism" here? The usual one: bisimulation [1] (the operational semantics of the lambda calculus is just a state machine, where the current expression is the state, and the reductions are transitions), or refinement mappings in both directions, if you like, as in my talk. Also, you can clearly see in my Java examples how the imperative denotation is preserved in all versions of the program. [1]: https://en.wikipedia.org/wiki/Bisimulation https://en.wikipedia.org/wiki/Bisimulation
    - tome 9y ago
      > > It would be a very strange operational semantics that considered an O(n)-space program isomorphic to an O(1)-space program. > Why? Because the operational semantics is very specifically intended to capture how the program executes as a sequence of state changes happening over time, typically with reference to some stack and heap. It is the denotational semantics whose notion of meaning is what the program calculates, i.e. the "end result of the computation". > We can have complexity preserving isomorphisms and non-preserving isomorphisms, and it's quite easy to see from the mappings which is which. Those can't be isomorphisms of operational semantics because part of operational semantics is the complexity. How else would you define complexity other than by reference to operational semantics? Any "isomorphism" of operational semantics by definition preserves the complexity. > Wouldn't you intuitively consider Euclid's algorithm operating on unary and binary representations of numbers isomorphic No, not at all. In fact let's make it simpler: I wouldn't even consider addition of unary integers to be operationally isomorphic to addition of binary integers. Denotationally they're the same, of course. (There's a more subtle point which I think you're not making but I'll mention it all the same: yes, I consider the "Euclid's algorithm" part of "Euclid's algorithm operating on unary integers" to be the same as the "Euclid's algorithm" part of "Euclid's algorithm operating on binary integers".) > > What is your notion of "isomorphism" here? > The usual one: bisimulation (or a refinement mapping in both directions, if you like). I'm not especially familiar with the notion of bisimulation but if you can demonstrate that the addition of unary integers is bisimilar to the addition of binary integers then I would be very interested!
      - pron 9y ago
        > Because the operational semantics is very specifically intended to capture how the program executes as a sequence of state changes happening over time, typically with reference to some stack and heap. First, operational semantics is usually a state machine (e.g., in the case of lambda calculus, the current expression is the state and the reductions are transitions). Second, there is no a-priori requirement that mapping the states of two state machines preserve complexity. You can add this restriction if you want to show they have the same complexity (as in polynomial reduction when showing membership of complexity classes), but that's an additional constraint. > It is the denotational semantics whose notion of meaning is the "end result of the computation". No. That's just the functional denotational semantics (i.e., the matehmatical meaning of a program is a so-called "partial function", which resembles a function). Imperative programs can have a Hoare-logic denotation (which I used in my Java example). TLA has a behavior denotation (the mathematical meaning of a program is a set of its possible behaviors, where a behavior is an infinite sequence of states, where a "terminating" computation is defined to be one where some state is reached in a finite number of steps, and then "stutters" forever). A language such as Eve can use a denotation where every block is a relation on the current and next state, and the entire program is such a relation, made by intersecting all blocks. > No, not at all. In fact let's make it simpler: I wouldn't even consider addition of unary integers to be operationally isomorphic to addition of binary integers. Well, in program analysis, the ordinary (homo/iso)morphism between programs is the (bi)simulation relation, and in this case the two are isomorphic. > Denotationally they're the same, of course. No, again, this depends on what your denotation is. In Haskell, for example, even two instances of Euclid's algorithm using a binary representation may not be denotationally equivalent, as in my example, but in TLA, for example, they would be. > yes, I consider the "Euclid's algorithm" part of "Euclid's algorithm operating on unary integers" to be the same as the "Euclid's algorithm" part of "Euclid's algorithm operating on binary integers" Ah, and the simulation relation (or the much nicer refinement relation in TLA) precisely and mathematically captures the notion of what it means for two programs to implement the same algorithm. In TLA, A => S and B => S iff A and B implement the same algorithm S. I.e., in TLA, you have a very simple and precise operator that defines the notion of abstraction. > I'm not especially familiar with the notion of bisimulation but if you can demonstrate that the addition of unary integers is bisimilar to the addition of binary integers then I would be very interested! Picture a graph where each node is the state of the computation, and the edges signify transitions. If you want to think in terms of LC, the state can be some lambda expression, and the transitions are reductions. In the case of deterministic programs with a fixed input (let's say that we're only considering the computation of factorial(5)), it's a linear graph. There is a subtlety here, as the lambda calculus does not specify a reduction order and so creates a non-linear graph, with different paths representing different reduction orders. But normally, programming languages come with an evaluation strategy, a state machine, that accompanies the LC (by-name for Haskell, by-value for ML). BTW, if we label each node with the set of all atomic propositions that are true in that state, we get what is known as the Kripke structure of the program, which is the canonical program representation in all of program analysis. A simulation relation is a relation from program A to program B that maps states to states and transitions to transitions, such that for every transition that A makes, B can match it with a mapped transition that leads to a mapped state. If the relation is invertible, we say that it's a bisimulation, and it forms an isomorphism on programs. You can see that whether you label the states with a number in unary or in binary, the graph is the same, so clearly an invertible relation exists. See Wikipedia for a more precise treatment: https://en.wikipedia.org/wiki/Bisimulation https://en.wikipedia.org/wiki/Bisimulation If you want, you can place further restrictions on the mapping, such as bounding its complexity to show tighter similarity. Here I show how you can describe an actual lattice relating programs to one another: https://pron.github.io/posts/tlaplus_part4#equivalence-abstraction-and-implementation https://pron.github.io/posts/tlaplus_part4#equivalence-abstr... The following section (which does not require any previous knowledge of TLA), specifically discusses (bi)simulation: https://pron.github.io/posts/tlaplus_part4#other-notions-of-equivalence-and-order https://pron.github.io/posts/tlaplus_part4#other-notions-of-...

by tome 9y ago

> All really express the same computation -- the operational semantics are isomorphic The operational semantics are certainly not isomorphic. fac1 consumes stack, for example, and fac2 doesn't.

pron 9y ago

So what? That's still isomorphic (I said isomorphic, not identical), as you can map a value to a stack state and vice-versa. See my Java programs in the comment below, where I explicitly perform a mapping on the state of the stack to map it to a variable in a different expression of the computation. My talk (https://www.youtube.com/watch?v=15uy9Ga-14I https://www.youtube.com/watch?v=15uy9Ga-14I) addresses this precise point.

tome 9y ago
I'm confused. It would be a very strange operational semantics that considered an O(n)-space program isomorphic to an O(1)-space program. What is your notion of "isomorphism" here?
- pron 9y ago
  > It would be a very strange operational semantics that considered an O(n)-space program isomorphic to an O(1)-space program. Why? Intuitively, wouldn't you consider Euclid's algorithm operating on unary and binary representations of numbers isomorphic despite the exponential difference in complexity? We can have complexity preserving isomorphisms and non-preserving isomorphisms, and it's quite easy to see from the mappings which is which. That's exactly why, if you're writing a reduction to prove complexity bounds, you must show that the reduction itself is polynomial. Otherwise, you get a mapping, but not one that preserves complexity. > What is your notion of "isomorphism" here? The usual one: bisimulation [1] (the operational semantics of the lambda calculus is just a state machine, where the current expression is the state, and the reductions are transitions), or refinement mappings in both directions, if you like, as in my talk. Also, you can clearly see in my Java examples how the imperative denotation is preserved in all versions of the program. [1]: https://en.wikipedia.org/wiki/Bisimulation https://en.wikipedia.org/wiki/Bisimulation
  - tome 9y ago
    > > It would be a very strange operational semantics that considered an O(n)-space program isomorphic to an O(1)-space program. > Why? Because the operational semantics is very specifically intended to capture how the program executes as a sequence of state changes happening over time, typically with reference to some stack and heap. It is the denotational semantics whose notion of meaning is what the program calculates, i.e. the "end result of the computation". > We can have complexity preserving isomorphisms and non-preserving isomorphisms, and it's quite easy to see from the mappings which is which. Those can't be isomorphisms of operational semantics because part of operational semantics is the complexity. How else would you define complexity other than by reference to operational semantics? Any "isomorphism" of operational semantics by definition preserves the complexity. > Wouldn't you intuitively consider Euclid's algorithm operating on unary and binary representations of numbers isomorphic No, not at all. In fact let's make it simpler: I wouldn't even consider addition of unary integers to be operationally isomorphic to addition of binary integers. Denotationally they're the same, of course. (There's a more subtle point which I think you're not making but I'll mention it all the same: yes, I consider the "Euclid's algorithm" part of "Euclid's algorithm operating on unary integers" to be the same as the "Euclid's algorithm" part of "Euclid's algorithm operating on binary integers".) > > What is your notion of "isomorphism" here? > The usual one: bisimulation (or a refinement mapping in both directions, if you like). I'm not especially familiar with the notion of bisimulation but if you can demonstrate that the addition of unary integers is bisimilar to the addition of binary integers then I would be very interested!
    - pron 9y ago
      > Because the operational semantics is very specifically intended to capture how the program executes as a sequence of state changes happening over time, typically with reference to some stack and heap. First, operational semantics is usually a state machine (e.g., in the case of lambda calculus, the current expression is the state and the reductions are transitions). Second, there is no a-priori requirement that mapping the states of two state machines preserve complexity. You can add this restriction if you want to show they have the same complexity (as in polynomial reduction when showing membership of complexity classes), but that's an additional constraint. > It is the denotational semantics whose notion of meaning is the "end result of the computation". No. That's just the functional denotational semantics (i.e., the matehmatical meaning of a program is a so-called "partial function", which resembles a function). Imperative programs can have a Hoare-logic denotation (which I used in my Java example). TLA has a behavior denotation (the mathematical meaning of a program is a set of its possible behaviors, where a behavior is an infinite sequence of states, where a "terminating" computation is defined to be one where some state is reached in a finite number of steps, and then "stutters" forever). A language such as Eve can use a denotation where every block is a relation on the current and next state, and the entire program is such a relation, made by intersecting all blocks. > No, not at all. In fact let's make it simpler: I wouldn't even consider addition of unary integers to be operationally isomorphic to addition of binary integers. Well, in program analysis, the ordinary (homo/iso)morphism between programs is the (bi)simulation relation, and in this case the two are isomorphic. > Denotationally they're the same, of course. No, again, this depends on what your denotation is. In Haskell, for example, even two instances of Euclid's algorithm using a binary representation may not be denotationally equivalent, as in my example, but in TLA, for example, they would be. > yes, I consider the "Euclid's algorithm" part of "Euclid's algorithm operating on unary integers" to be the same as the "Euclid's algorithm" part of "Euclid's algorithm operating on binary integers" Ah, and the simulation relation (or the much nicer refinement relation in TLA) precisely and mathematically captures the notion of what it means for two programs to implement the same algorithm. In TLA, A => S and B => S iff A and B implement the same algorithm S. I.e., in TLA, you have a very simple and precise operator that defines the notion of abstraction. > I'm not especially familiar with the notion of bisimulation but if you can demonstrate that the addition of unary integers is bisimilar to the addition of binary integers then I would be very interested! Picture a graph where each node is the state of the computation, and the edges signify transitions. If you want to think in terms of LC, the state can be some lambda expression, and the transitions are reductions. In the case of deterministic programs with a fixed input (let's say that we're only considering the computation of factorial(5)), it's a linear graph. There is a subtlety here, as the lambda calculus does not specify a reduction order and so creates a non-linear graph, with different paths representing different reduction orders. But normally, programming languages come with an evaluation strategy, a state machine, that accompanies the LC (by-name for Haskell, by-value for ML). BTW, if we label each node with the set of all atomic propositions that are true in that state, we get what is known as the Kripke structure of the program, which is the canonical program representation in all of program analysis. A simulation relation is a relation from program A to program B that maps states to states and transitions to transitions, such that for every transition that A makes, B can match it with a mapped transition that leads to a mapped state. If the relation is invertible, we say that it's a bisimulation, and it forms an isomorphism on programs. You can see that whether you label the states with a number in unary or in binary, the graph is the same, so clearly an invertible relation exists. See Wikipedia for a more precise treatment: https://en.wikipedia.org/wiki/Bisimulation https://en.wikipedia.org/wiki/Bisimulation If you want, you can place further restrictions on the mapping, such as bounding its complexity to show tighter similarity. Here I show how you can describe an actual lattice relating programs to one another: https://pron.github.io/posts/tlaplus_part4#equivalence-abstraction-and-implementation https://pron.github.io/posts/tlaplus_part4#equivalence-abstr... The following section (which does not require any previous knowledge of TLA), specifically discusses (bi)simulation: https://pron.github.io/posts/tlaplus_part4#other-notions-of-equivalence-and-order https://pron.github.io/posts/tlaplus_part4#other-notions-of-...