4 ms·

My goal was to add more context to your (excellent and upvoted) original post, which in my opinion is basically the fundamental "proof" of why All([]) must be T

by feoren 3y ago

My goal was to add more context to your (excellent and upvoted) original post, which in my opinion is basically the fundamental "proof" of why All([]) must be TRUE, and I find beauty in this two-dimensional analogy: add | sum multiply | product and | all or | any concat | "flatten" (arguable name here) I also find beauty in the fact that the existence of a monoid on the left is sufficient for producing the aggregation on the right that behaves in the way we want. I see the monoid as the simple building block from which we produce more interesting and complicated structures. I enjoy the continued, unbroken thread of rigorous logic that connects everything. When you say that TRUE can be the identity of "an operator that extends 2-value Boolean operations to lists of N-elements", I just don't see the unbroken thread of rigorous logic behind that statement. Maybe it's there! But I don't see it. I can write down exactly what it means for some element i to be an identity of a binary operation @. It means i@x == x == x@i for all x in the set over which @ is defined. Whatever the rules of "identity" are that you're talking about, they're not this, so I'm just kinda struggling to accept it. I wonder whether maybe what you're thinking of deserves a different name than "identity". Does any of this matter? It does to me, because I actually use Monoids all the time in programming, where you can't afford any ambiguity at all. So again: maybe you see that unbroken chain of rigorous logic and know exactly what you mean when you say TRUE is the identity of "an operator that extends 2-value Boolean operations to lists of N-elements", but I'd need to see the exact laws that an element must follow to be such an operator or such an identity of that operator. I gave an example of how to turn associative binary operations with identity into a unary operator on lists of elements, but unary operators don't really have identity elements. Some unary operators have fixed points and eigenvalues, which are similar to identity, but such operators must have the same domain and codomain, and aggregate operators like SUM and ALL do not. So there's not really anything you define to be SUM's identity, since it does not accept 0 as an input.

Nevermark 3y ago
Ha! I agree, you are right. TRUE for a monoid can exist independently from any aggregator defined over that monoid. My bad :) The fractal lines between what is mathematically true, vs. what is practical or useful to be true, in coding are worth paying attention to! Thank you! And perhaps these relations can always hold, “without loss of generality”. In which case we need to formally define these monoid-aggregator relations so we all know when they are assumed to be in effect. — On the beauty side, I love how 0 = sum{} captures the semantic difference between zero and other numbers, with the syntax of nothing between two braces.
- feoren 3y ago
  I do think there was something interesting about the idea that adding the element to the input array doesn't change the result. It's a little tricky to formalize though. If we define an "aggregation" agg over some set S as a function from S* (the "Kleene star", AKA the free monoid over S, AKA really just simple arrays of S) to S, and we identify some element i such that agg([i] concat X) == agg(X) == agg(X concat [i]) for all X in S*, that does feel very "identity-ish". It's a little bit like saying [i] is an identity of concat under the equivalence relation on S* that X~Y iff agg(X) == agg(Y)? In the same way that 7 is an identity of + under the equivalence relation "mod 7" (paraphrasing). But note that: sum([-2, 2] concat X) == sum(X) == sum(X concat [-2, 2]) for all X as well. You could say "well obviously, because sum([-2, 2]) == sum([0]) and [0] is our identity element" but then we're implicitly assuming that agg(X concat Y) = agg(X) @ agg(Y) for some operator @. Which in turn is basically assuming we've built agg up from a monoid to begin with, and the novelty here would be what happens when we don't do that. There may be some interesting (if not useful) stuff here. if there exists some operator @: (S, S) -> S such that: agg(X concat Y) == agg(X) @ agg(Y) For all X, Y in S*, and if : agg([i] concat X) == agg(X) == agg(X concat [i]) for all X in S*, then must agg([i]) be an identity element of @? Certainly that's true if agg is onto (i.e. we can find every element of S via agg of some S*). But it can't really be true in general, because we could make degenerate agg functions like ignore(X) := 0 Now every element of S meets this condition: ignore([s] concat X) == ignore(X) == ignore(X concat [s]) So we have every element of S as this weird kind of "identity" of the "ignore" function. And we can find functions on S* with no "identity" of this kind: "count", for instance. Although that's cheating because it only works when S happens to be the natural numbers (otherwise agg is not a function from S* -> S).
  - Nevermark 3y ago
    Yes I think you hit it on the nail. My logic depended on the aggregator being a recursive monoid, with: 1) Special handling for a unit list, where the unitary element is returned, and 2) Special handling for an empty list, where the identity element of the monoid is returned OR we get explicit that the case of the empty list is simply already it’s simplest form, and we choose to define that equivalent to the monoid’s identity So i skipped a step by “finding” the identity from the aggregator’s behavior, instead of directly from the monoid it is based on. —— Alternatively, I am liking the idea of defining this list vs pair, aggregator vs monoid relations more tightly. Empty braces unify the syntax for “zero” with the semantics “nothing” between the braces. How else can you join those semantics and syntax? Likewise, starting with unary natural numbers, syntactically and semantically, a list of 1’s is the number. So which comes first? A unary monoid addition of 2 lists of ones (n-way concatenations of unitary 1), or an n-way sum-concatenation that each unary number actually consists of? I think they are more tightly bound definitions than our typical syntax suggests, when we get down to the semantics = syntax level.

by feoren 3y ago

Nevermark 3y ago

Ha! I agree, you are right. TRUE for a monoid can exist independently from any aggregator defined over that monoid. My bad :) The fractal lines between what is mathematically true, vs. what is practical or useful to be true, in coding are worth paying attention to! Thank you! And perhaps these relations can always hold, “without loss of generality”. In which case we need to formally define these monoid-aggregator relations so we all know when they are assumed to be in effect. — On the beauty side, I love how 0 = sum{} captures the semantic difference between zero and other numbers, with the syntax of nothing between two braces.

feoren 3y ago
I do think there was something interesting about the idea that adding the element to the input array doesn't change the result. It's a little tricky to formalize though. If we define an "aggregation" agg over some set S as a function from S* (the "Kleene star", AKA the free monoid over S, AKA really just simple arrays of S) to S, and we identify some element i such that agg([i] concat X) == agg(X) == agg(X concat [i]) for all X in S*, that does feel very "identity-ish". It's a little bit like saying [i] is an identity of concat under the equivalence relation on S* that X~Y iff agg(X) == agg(Y)? In the same way that 7 is an identity of + under the equivalence relation "mod 7" (paraphrasing). But note that: sum([-2, 2] concat X) == sum(X) == sum(X concat [-2, 2]) for all X as well. You could say "well obviously, because sum([-2, 2]) == sum([0]) and [0] is our identity element" but then we're implicitly assuming that agg(X concat Y) = agg(X) @ agg(Y) for some operator @. Which in turn is basically assuming we've built agg up from a monoid to begin with, and the novelty here would be what happens when we don't do that. There may be some interesting (if not useful) stuff here. if there exists some operator @: (S, S) -> S such that: agg(X concat Y) == agg(X) @ agg(Y) For all X, Y in S*, and if : agg([i] concat X) == agg(X) == agg(X concat [i]) for all X in S*, then must agg([i]) be an identity element of @? Certainly that's true if agg is onto (i.e. we can find every element of S via agg of some S*). But it can't really be true in general, because we could make degenerate agg functions like ignore(X) := 0 Now every element of S meets this condition: ignore([s] concat X) == ignore(X) == ignore(X concat [s]) So we have every element of S as this weird kind of "identity" of the "ignore" function. And we can find functions on S* with no "identity" of this kind: "count", for instance. Although that's cheating because it only works when S happens to be the natural numbers (otherwise agg is not a function from S* -> S).
- Nevermark 3y ago
  Yes I think you hit it on the nail. My logic depended on the aggregator being a recursive monoid, with: 1) Special handling for a unit list, where the unitary element is returned, and 2) Special handling for an empty list, where the identity element of the monoid is returned OR we get explicit that the case of the empty list is simply already it’s simplest form, and we choose to define that equivalent to the monoid’s identity So i skipped a step by “finding” the identity from the aggregator’s behavior, instead of directly from the monoid it is based on. —— Alternatively, I am liking the idea of defining this list vs pair, aggregator vs monoid relations more tightly. Empty braces unify the syntax for “zero” with the semantics “nothing” between the braces. How else can you join those semantics and syntax? Likewise, starting with unary natural numbers, syntactically and semantically, a list of 1’s is the number. So which comes first? A unary monoid addition of 2 lists of ones (n-way concatenations of unitary 1), or an n-way sum-concatenation that each unary number actually consists of? I think they are more tightly bound definitions than our typical syntax suggests, when we get down to the semantics = syntax level.