Comment by sharkbot | Hacker News Reader

Comment by sharkbot | Hacker News Reader

Parent Full thread

You’ve hit upon one of the key insights in category theory. It’s been awhile, let me see if I can remember enough to describe the sketch…

“Equality” is a tricky concept, and various branches of mathematics have slightly different ideas (or axioms) of equality. Simple arithmetic is based upon strict equality: two things are equal if and only if a sequence of logical steps are followed precisely and the final answer matches exactly. Other branches have looser (or just different) versions of equality: set theory may use a relation to induce an equivalence relation, topology may see things as equal based on structure preserving transformations, computer science has notions of program equivalence based on identical outputs given identical inputs, etc.

Category theory is an attempt to identify and unify various similar concepts across mathematical branches, including “equality”. Category theorists are limited to talking about objects (which are opaque), and arrows between those objects. Using those (incredibly) abstract tools, how does one define “equality”? The answer is, one can’t, so what are the closest things possible that capture “equality”, and can be specialized back into more traditional notions as needed.

Part of the confusion is that category theory is described from the “arrows and objects” perspective, when the really interesting stuff happens two layers higher (natural transformations and above). And another part of the confusion is that many mathematicians see category theory as needless nonsense :)

> “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.

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.

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.

> 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.

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.

Decisions Theory (so, statistics and economics) have also always relied on the idea of equivalence (I believe the notion is the set-theoretic one) for purely practical reasons.

So for instance (drawing on the other reply in this thread about Leibnitz), to say that

x = y => f(x) = f(y)

is not really useful when the meaning of the equality is contextual. If two choices are equal for one person (or prior distribution, utility function, uncertainty aversion etc.), they may not be "equal" if anything changes. And if they are, but other choices are not, the "equality" doesn't help.

By contrast, in if in the moment of where a context is fixed (we look at one potential set of decisions, one choice relation etc.) there exists an equivalence relation, then we can analyze the choice situation with math, and it's the equivalence of choices (with respect to this one relation) that does this. And then, naturally, if we conceive of a situation that we can analyze (or we have data on it), we can conceive the relationships that might have given rise to it.

And, as it turns out, there's typically infinitely many of those. And so, even lowly economists or statisticians must - in some simple way - grapple with what I would imagine categories are (?)

Would love to read more on this. Are there materials on category theory for non-mathematicians (and non-computer scientists thinking in terms of language theory)?

Heh, in programming the Leibniz rule is sometimes (often?) not true. x == y does not necessarily mean that, for example, &x == &y.

Reply on news.ycombinator.com