3 ms·

Hopefully someone can explain here because I feel like equivalence fails in the same way equality does. Is 1 + 2 == 3? well, I understand they're equivalent,

Hopefully someone can explain here because I feel like equivalence fails in the same way equality does. Is 1 + 2 == 3? well, I understand they're equivalent, but they're not the same terms. Is (1+(1+1)) the same amount of equivalence to 3 as 1+2 is? I'd much prefer a notion that could look at how 'equivalent' terms are opposed to just looking at equality after β-reduction.

openfuture 5y ago
There is such a notion. You write a number on the equality sign saying essentially how many operations can be performed so 1+2 is equal to 3 if that number is larger than 0 (the special case of 0 is reflexivity, i.e. true equality). This is used a lot in some computer science stuff I've seen.
- VirusNewbie 5y ago
  thanks for letting me know, do you know if there's a term for that notation?
hither_shores 5y ago
That's the "infinity": ordinary (1-)categories have (1-)arrows between objects, 2-categories have 2-arrows between 1-arrows, 3-categories have 3-arrows between 2-arrows, and so on. Infinity-categories have (k+1)-arrows between k-arrows all the way up. (And a 0-category is just a set: objects, but no arrows) > Is (1+(1+1)) the same amount of equivalence to 3 as 1+2 is? I'd much prefer a notion that could look at how 'equivalent' terms are opposed to just looking at equality after β-reduction. "Amounts" of equivalence between terms isn't really the right notion here: there's not much you can do with "an equivalence exists", which is all that "X and Y are equivalent" really means. A 2-equivalence (which in this context I think is going to end up being something like a rewrite rule?) should be an equivalence between particular programs, not the whole space of programs implementing a given function.
edflsafoiewq 5y ago
In algebra, monads are used to reify the notion of an "explicit expression". So you have the integers, Z, and the monad m gives m(Z), the set of expressions (let's say sums) over Z. And then you have m(m(Z)) which is nested expressions and so on. An algebra for a monad evaluates an expression m(Z)->Z, and all the monad laws basically enforce the kind of equational reasoning ordinary notation takes for granted (eg sub-expressions can be replaced by their value, 1+(1+1)=1+2). So those would be related in this way join (1)+(1+1) : m(m(Z)) -----> 1+1+1 : m(Z) | | fmap(eval) | | eval v v 1+2 : m(Z) -----------> 3 : Z eval

openfuture 5y ago

There is such a notion. You write a number on the equality sign saying essentially how many operations can be performed so 1+2 is equal to 3 if that number is larger than 0 (the special case of 0 is reflexivity, i.e. true equality). This is used a lot in some computer science stuff I've seen.

VirusNewbie 5y ago
thanks for letting me know, do you know if there's a term for that notation?

hither_shores 5y ago

That's the "infinity": ordinary (1-)categories have (1-)arrows between objects, 2-categories have 2-arrows between 1-arrows, 3-categories have 3-arrows between 2-arrows, and so on. Infinity-categories have (k+1)-arrows between k-arrows all the way up. (And a 0-category is just a set: objects, but no arrows) > Is (1+(1+1)) the same amount of equivalence to 3 as 1+2 is? I'd much prefer a notion that could look at how 'equivalent' terms are opposed to just looking at equality after β-reduction. "Amounts" of equivalence between terms isn't really the right notion here: there's not much you can do with "an equivalence exists", which is all that "X and Y are equivalent" really means. A 2-equivalence (which in this context I think is going to end up being something like a rewrite rule?) should be an equivalence between particular programs, not the whole space of programs implementing a given function.

edflsafoiewq 5y ago

In algebra, monads are used to reify the notion of an "explicit expression". So you have the integers, Z, and the monad m gives m(Z), the set of expressions (let's say sums) over Z. And then you have m(m(Z)) which is nested expressions and so on. An algebra for a monad evaluates an expression m(Z)->Z, and all the monad laws basically enforce the kind of equational reasoning ordinary notation takes for granted (eg sub-expressions can be replaced by their value, 1+(1+1)=1+2). So those would be related in this way join (1)+(1+1) : m(m(Z)) -----> 1+1+1 : m(Z) | | fmap(eval) | | eval v v 1+2 : m(Z) -----------> 3 : Z eval