166 karma · joined March 9, 2017
In any case, the fact that the compiler knows what code needs to be updated is a real superpower.
- PUSH(n) where n is a floating-point number
- POP
- CLEAR
- ADD, SUB, MUL, DIV
- ID
These can be interpreted as operations on a stack of floating-point numbers in the obvious way, PUSH(1.2) * [3.14] == [1.2, 3.14], POP * [1, 2, 3] == [2, 3], ADD * [1, 2, 5] == [3, 5], CLEAR * [1, 2, 3] == [], ID * [1, 2, 3] == [1, 2, 3], etc. However, not all of the compositions of stack operations are legal. For example, ADD * PUSH(1) * PUSH(2) is fine and equivalent to PUSH(3), but ADD * PUSH(1) * CLEAR is illegal.
Ok, so our stack operations don't form a monoid. But they obviously can still be composed, sometimes, so what do we have if not a monoid? They form a category! There is one object for each natural number, representing the height of the stack. So there are arrows like PUSH(3.14) : Height_{n} -> Height_{n+1} for all n, and POP : Height_{n} -> Height_{n-1} whenever n >= 1, and ADD : Height_{n} -> Height_{n-2} whenever n >= 2.
Another common example is matrices. Square matrices form a monoid, but what about arbitrary rectangular matrices? They don't form a monoid, but they do form a category where the objects are natural numbers, and the arrows N -> M are just the MxN matrices. You can't multiply any two matrices, but if you have a P -> Q matrix (QxP) and a Q -> R (RxQ) matrix then you can multiply them to get a P -> R matrix (RxP).
- Moggi was studying the problem of equivalence of programs, and noted that the traditional approach to modeling a program as a total function Input -> Output is problematic. He pioneered the use of monads and Kleisli categories as a foundation for reasoning about equivalence of real programs, including all the real-world nastiness like non-termination, partiality (e.g. throwing an exception that kills the program), non-determinism, and so on. https://person.dibris.unige.it/moggi-eugenio/ftp/lics89.pdf
- Linear logic (and it's close relative affine logic) was the inspiration behind Rust's ownership model, from what I understand. Linear logic was originally described in terms of the sequent calculus by Girard (http://girard.perso.math.cnrs.fr/linear.pdf), but later work used certain categories as a model of linear logic (https://ncatlab.org/nlab/files/SeelyLinearLogic.pdf). This answered and clarified a number of questions stemming from Girard's original work.
- Cartesian-closed categories (CCCs) form models of the simply-typed lambda calculus, in the sense that any lambda term can be interpreted as a value in a CCC. Conal Elliott pointed out that this means that a lambda term doesn't have just one natural meaning; it can be given a multitude of meanings by interpreting the same term in different CCCs. He shows how to use this idea to "interpret" a program into a circuit that implements the program. http://conal.net/papers/compiling-to-categories/
- Mokhov, Mitchell, and Jones studied the similarities and differences between real-world build systems and explained them using different kinds of categories. https://www.microsoft.com/en-us/research/uploads/prod/2018/0...
- There is a classical construction about minimizing a DFA due to Brzozowski which is a bit magical. Given a DFA, do the following process twice: (a) get an NFA for the reverse language by reversing all edges in the DFA and swapping start / accept nodes, then (b) drop any nodes which are not reachable from a start node in the NFA. The result will be the minimal DFA that accepts the same language as your original DFA! Bonchi, Bonsangue, Rutten, and Silva analyzed Brzozowski's algorithm from a categorical perspective, which allowed them to give a very clear explanation of why it works along with a novel generalization of Brzozowski's algorithm to other kinds of automata. https://alexandrasilva.org/files/RechabilityObservability.pd...
- I would also put the development of lenses in this list, but they haven't leaked very far outside of the Haskell universe yet so I don't think they are a compelling example. Check back in 5 years perhaps. Here's a blog post describing how lenses relate to jq and xpath: https://chrispenner.ca/posts/traversal-systems
- I've personally had success in finding useful generalizations of existing algorithms by finding a monoid in the algorithm and replacing it with a category, using the fact that categories are like "many-kinded monoids" in some sense. I haven't written any of these cases up yet, so check back in 2 years or so. In any case, they've been useful enough to drive some unique user-facing features.
Generally speaking, Cantor–Schröder–Bernstein does not give you a (finite) construction of the bijection, because you have to follow the inverses of f and g back until you either end up with something from the first set with no preimage under g, or something from the second set with no preimage under f, or you find that you are iterating forever. You have to make a decision based on whether or not a certain computation terminates. That's essentially why it is a non-constructive theorem (in fact, it even implies the law of excluded middle)
But in your specific case, we're kind of in luck. The injections are simple enough that you can work out the bijection that you'd get from König's proof manually, and it goes like this:
Concretely, let's write (AB) for the tree with left subtree A and right subtree B, and write . for the empty tree. Your injections are f(A,B) = (AB) and g(T) = (T.). Alternately applying f/g partitions the set of trees into a bunch of infinite sequences. Your bijection is given by: if T is part of the sequence that begins with the empty tree, pair T with (T,.). If T is part of some other sequence, then T is not the empty tree; it is of the form T = (LR), and you should pair T with (L,R). Concretely, the sequence that starts with the empty tree looks like:
. -> . . -> (..) -> (..) . -> ((..).) -> ((..).) . -> (((..).).) -> **
In other words, the single trees that appear in the empty list's sequence are the fully-left-leaning trees like ((((..).).).); all other trees are in the other sequences. So to decide where your tree goes in the bijection, you have to do this:
if (T is fully left-leaning) then (T,.) else (left-child(T), right-child(T))
And computing whether or not T is fully left-leaning involves an unbounded amount of computation. You have to actually walk the whole tree. So this bijection won't correspond to a finite, non-looping program. In a sense, the algorithm you get from Cantor–Schröder–Bernstein is not "continuous", but the one you get from the Seven Trees In One construction is.
The paper is quite good, but Dan Piponi has a great blog post that recasts the isomorphism as a game of "nuclear pennies", which is a fun puzzle to work out yourself: http://blog.sigfpe.com/2007/09/arboreal-isomorphisms-from-nu...
- Elliptic curve cryptography (https://en.wikipedia.org/wiki/Elliptic-curve_cryptography)
- Grobner bases, with many applications. Example domains: coding theory, robotics, signal processing... (https://math.stackexchange.com/questions/32421/applications-...)
- Physics [solitons] (https://kasmana.people.cofc.edu/SOLITONPICS/)
- Physics [string theory] (https://royalsociety.org/~/media/people/new-fellows-2014/Pre...)
- Automata theory, via "tropical" algebraic geometry (https://link.springer.com/article/10.1007/s00233-019-09999-8)
This is not even considering applications of AG to other areas of pure mathematics, which are extensive.
There is nothing basis-dependent in Geometric Algebra. This presentation started from a basis, but then again so do many presentations of differential forms, leading to 2-forms like dx \wedge dy and so on.
The actual difference is that Geometric Algebra requires a choice of inner product (actually, you can get away with any bilinear form), while differential forms do not. However, some of the important operations on differential forms in physics do require an inner product (e.g. the hodge star operator and the codifferential), so you end up back on equal footing with GA again.
As a concrete example, consider the elements 1 + x and 1 - x. Their product is 1 + x - x - xx = 1 + x - x - 1 = 0. So certainly 1 + x doesn't have an inverse, either.
This honors project has what looks like an accurate write up of the construction along with proofs of some of the main theorems: https://ideaexchange.uakron.edu/cgi/viewcontent.cgi?article=...
The usual construction of the hyperreals replaces real numbers with sequences of real numbers, and also introduces a nontrivial equivalence relation on the sequences, making two sequences equivalent if they agree on a “large” set of terms. The real numbers get represented by the constant sequences, infinitesimals get represented by sequences that approach 0, and infinite numbers are represented by sequences that grow without bound.
The magic is in how “large set of terms” is defined. You need a “large set” relation with the property that finite sets are not large, and for any set either the set or its complement is large. Then we can resolve your question: say you had two not-always-zero sequences that multiply to give the all-zero sequence. Then the set of zero positions is large for one of those two sequences. And that means one of your sequences is equivalent to the zero sequence. The field axioms are saved!
> The reason we care about Church-encoding is because not all programming languages natively support sum types or recursion (although most programming languages support product types in the form of records / structs).
> However, most programming languages do support functions, so if we have functions then we can use them as a “backdoor” to introduce support for sum types or recursion into our language. This is the essence of the visitor pattern: using functions to Church-encode sum types or recursion into a language that does not natively support sum types or recursion.
The fact that method selectors only appear very rarely as first-class values in most languages means that most people aren’t tuned in to scenarios where they could be applied. But I bet you’ve invented special cases of this yourself, when you had a function that needed to dig data out of one of several locations, depending on other inputs.