A very nice fact that I coincidentally learned just yesterday, which is not in the linked answer but is touched on in one of the comments and in an edit on the accepted answer: there is an explicit bijection that maps a binary tree to seven binary trees (and vice-versa, by the inverse function).<p>Consider the definition of a binary tree: "a binary tree is either empty, or is a root with a left tree and a right tree". This we can write as<p><pre><code> T = 1 + T²
</code></pre>
Solving the analogous equation z = 1 + z² in the complex numbers gives z to be a primitive sixth-root of unity (<a href="https://www.wolframalpha.com/input?i2d=true&i=z+%3D+1+%2B+Power%5Bz%2C2%5D" rel="nofollow">https://www.wolframalpha.com/input?i2d=true&i=z+%3D+1+%2B+Po...</a>), i.e. z⁶ = 1, and so z⁷ = z. It turns out that we can similarly show T⁷ = T with some algebra (without subtractions) by repeatedly applying the transformations T→1+T² or 1+T²→T (a "game" version is at <a href="http://lebarde.alwaysdata.net/seventrees/" rel="nofollow">http://lebarde.alwaysdata.net/seventrees/</a>):<p><pre><code> T⁷
= T⁶ + T⁸
= T⁵ + T⁷ + T⁸
= T⁴ + T⁶ + T⁷ + T⁸
= T⁴ + 2T⁷
= T³ + T⁵ + 2T⁷
= T³ + T⁶ + T⁷
= T² + T⁴ + T⁶ + T⁷
= T² + T⁵ + T⁷
= T² + T⁶
= T + T³ + T⁶
= T + T² + T⁴ + T⁶
= T + T² + T⁵
= 2T + T³ + T⁵
= 2T + T⁴
= 1 + T + T² + T⁴
= 1 + T + T³
= 1 + T²
= T
</code></pre>
This can be used to give an explicit bijection: see Andreas Blass's paper "Seven trees in one": <a href="https://arxiv.org/pdf/math/9405205" rel="nofollow">https://arxiv.org/pdf/math/9405205</a> (via <a href="https://twitter.com/CihanPostsThms/status/1579017713527050241" rel="nofollow">https://twitter.com/CihanPostsThms/status/157901771352705024...</a> — see also <a href="https://math.ucr.edu/home/baez/week202.html" rel="nofollow">https://math.ucr.edu/home/baez/week202.html</a> which has more.)
as someone that's self taught, i really wish math was taught via stronly typed programming languages.<p>Math is so full of loosey-goosey context dependent ambiguous notation. It makes it easy to have a very terse expression communicate a powerful idea, but it makes it impossible to just parse an arbitrary expression.<p>Just as an example, look at the maclauren series as defined in the link. It uses f-dot, f-double-dot, then f^(n), having to note that (n) is the nth derivative rather than exponentiation. You have syntax switching and an ambiguity in the same expression.
Stuff like this is so cool. It reminds me of umbral calculus, another place where identities we’re used to from single variable calc apply correctly in other surprising places.<p>It’s especially amazing how we can invent “illegal operations” like the square root of a datatype (or the square root of minus one) and prove that we’ll get the right answer in the original domain if it exists. I’d bet I miss lots of opportunities to take advantage of inventing nonsensical operations to solve hard problems.<p>It seems like a lot of the logic we use for reasoning about complex systems has the same combinatorial underpinnings (e.g. continuous systems in calc, recurrence relations and polynomials elsewhere, and algebraic datatypes in OP). I’d love to see an intro to all these variations of “calculus” written up from those combinatorial foundations that applies to all of the different applications, rather than via epsilon-delta derivations that only apply to continuous systems.<p>Anybody seen a write-up like that anywhere?
Calculus already has types. The type of a function is f:R -> R.
If X and Y are normed linear spaces and f:X -> Y the type of the (Frechet) derivative is Df:X -> L(X,Y), where L(X,Y) is the space of linear operators from X to Y.