4 ms·

> “Equality” is a tricky concept, and various branches of mathematics have slightly different ideas (or axioms) of equality. Due to my own circumstances I’m dr

by User23 5y ago

> “Equality” is a tricky concept, and various branches of mathematics have slightly different ideas (or axioms) of equality. Due to my own circumstances I’m drawn to notions of equality that have pragmatic value. One of my favorite is Leibniz’s rule x=y => f(x)=f(y) I use that rule so frequently and effectively when reasoning about programs that pragmatically I’m not interested in a model where it doesn’t hold. It looks very simple, but it’s practically foundational for reasoning about predicate transformers. Incidentally, I’d be really interested in a rigorous rendition of Dijkstra and Scholten’s work on program semantics in the language of category theory.

zozbot234 5y ago
Leibniz's rule does hold under these generalized notions of isomorphism and equivalence. Each of these notions implicitly sets apart some class of functions `f` as "not evil", i.e. as respecting Leibniz's rule wrt. that equivalence. So as long as your predicate transformers are not "evil" in that sense, you'll be covered. And in practice, trying to work with possibly "evil" functions without a clear notion of what equivalences would render them "not evil" is generally a waste of effort and leads to results that are not semantically useful.
jhanschoo 5y ago
Observe that when you identify x with y, you are already drawing an equivalence between their formal representations (i.e. x, y), and the rule holds only for f that is blind to the formal representations, and distinguishes only between these equivalence classes. But within math topics there are notions of equivalence that are stronger than just that that the topic is uninterested in "piercing through the equivalence veil". For example, computer scientists often talk about Turing machines being equal even when their alphabets are disjoint, as long as their structure is the same, reserving equivalence typically to mean accepting the same language.
a1369209993 5y ago
> Leibniz's rule > x=y => f(x)=f(y) Eh, it's useful in some cases, especially from a theoretical perspective, but... x = 0.0 y = -0.0 f = \x(copysign(1,x)) x = "foo" y = "f"+"o"+"o" f = debug.dump-pointer ...pragmatically I'm not interested in a programming language where it does hold. It prohibits too many important utility functions.
- User23 5y ago
  You’re not even wrong. I suggest that you at least take the five minutes to read the wikipedia summary on predicate transformers before posting a replying in which you observably have no idea what you’re talking about. Briefly, predicate transformers are functions about the behavior of a language, not functions in the language. In that model predicates are pure functions over the program state space and predicate transformers are functions from predicates to predicates. Clearly your objections are inapplicable.

by User23 5y ago

zozbot234 5y ago

Leibniz's rule does hold under these generalized notions of isomorphism and equivalence. Each of these notions implicitly sets apart some class of functions `f` as "not evil", i.e. as respecting Leibniz's rule wrt. that equivalence. So as long as your predicate transformers are not "evil" in that sense, you'll be covered. And in practice, trying to work with possibly "evil" functions without a clear notion of what equivalences would render them "not evil" is generally a waste of effort and leads to results that are not semantically useful.

jhanschoo 5y ago

Observe that when you identify x with y, you are already drawing an equivalence between their formal representations (i.e. x, y), and the rule holds only for f that is blind to the formal representations, and distinguishes only between these equivalence classes. But within math topics there are notions of equivalence that are stronger than just that that the topic is uninterested in "piercing through the equivalence veil". For example, computer scientists often talk about Turing machines being equal even when their alphabets are disjoint, as long as their structure is the same, reserving equivalence typically to mean accepting the same language.

a1369209993 5y ago

> Leibniz's rule > x=y => f(x)=f(y) Eh, it's useful in some cases, especially from a theoretical perspective, but... x = 0.0 y = -0.0 f = \x(copysign(1,x)) x = "foo" y = "f"+"o"+"o" f = debug.dump-pointer ...pragmatically I'm not interested in a programming language where it does hold. It prohibits too many important utility functions.

User23 5y ago
You’re not even wrong. I suggest that you at least take the five minutes to read the wikipedia summary on predicate transformers before posting a replying in which you observably have no idea what you’re talking about. Briefly, predicate transformers are functions about the behavior of a language, not functions in the language. In that model predicates are pure functions over the program state space and predicate transformers are functions from predicates to predicates. Clearly your objections are inapplicable.