I really like TodePond's video "Screens in Screens in Screens". I've been wanting to do the same kinda thing with mathematical formulas instead of shapes, a kind of "formulas in formulas in formulas", but I'm an awful programmer so I'll describe some math you can do to that effect. Apologies in advance for the shoddy explanation though.
Here's a thing you can do with "screens". You can name screens. Start with some screens A B C. Then if C is inside A, and A and B are the same color, then there is a copy of C inside B. What do you call this copy? "The copy of B from A to C"? It will be convenient if we give it a symbolic name. Call it (A->B)C. Or if you are really hardcore you can call it just t(A,B,C) where t is a ternary operator describing the result of copying C from A to B. You may think to only consider (A->B)C when C is inside A, but the math becomes tractable if you consider all screens at once. Then we can stipulate some axioms:
(A->A)B = B
(A->B)A=B
(B->C)(A->B)=(A->C)
(A->(X->Y)A)=(X->Y)
The first axiom means if you are copying a screen from one screen to itself, you aren't changing anything. The second axiom is "obvious" except for considering (A->B)A in the first place. The third axiom means if you copy a screen from A to B and then from B to C that is the same as if you were to copy it from A to C directly. It is also shorthand for (B->C)((A->B)D) = (A->C)D for all screens D. The fourth axiom takes a bit more explaining. Basically we want this equation to be true whenever A is in X, and both sides are being used to copy something from A. But our theory at this point doesn't have a predicate for "A is contained in X" so we say it holds in all cases.
With these axioms you can show the operators (A->B) form an algebraic structure called a group: You can multiply them by performing one copy after the other (C->D)(A->B). This operation is associative (I mean, it must be), and has an identity element and inverses. The identity being (A->A) and the inverse of (A->B) being (B->A).
Another perspective is to view screens as points in an affine space (i.e. vector space without a specified origin). Then (A->B)C can be thought of as (B-A)+C, and each of the axioms above can be interpreted as vector equations. This isn't a good model though because it ends up saying some screens are the same when they should be different. You can still take the above axioms and show that screens form a generalization of affine spaces called torsors.
I'll share more if anybody is interested. It really needs a much longer write up, but I thought somebody might know if its already been done before.
hey interesting! I'm not sure I completely understand, but it's nice to see how different people might model this sort of thing. i know @Elliot has been working on a screens-like thing recently, and he modelled it completely differently from me.
I'd love to write up a blog post explaining how I model it. it would be nice to see what people think of it
Cool! I really like screens too. I also like this mathematical modeling of screens! I like the idea to model screens as a group. I have been trying out some models related to the following model: screens as a category: the objects are screens and the arrows mean "contains".
I originally thought about this model when I was using it to solve some puzzles in "Patrick's Parabox" which also involves some recursive box stuff 🙂
You can turn this category into a groupoid by adding in an inverse arrow for every "contains" arrow. The inverse arrows mean "contained by".
The spatial relationships between screens is a functor from this category (or groupoid) to spatial transformations like Affine Transformations (Although Lu Wilson told me that screens actually uses a different type of spatial transformation).
The functor is really just saying "write down a specific transformation next to each arrow"
IRT your axioms: I have trouble understanding 2 and 4. I can't figure out how to interpret (A -> B)A. I guess it would be "The copy of A from A to B" based on your paragraph above the axioms, but I'm not sure what that means.
I think axiom 2 is hard to picture because in the expression (A->B)C you normally think of C as lying inside A. But in the case of (A->B)A, where C is A, C is no longer strictly inside A, since it coincides with A. Maybe a better way to think of it is to let C vary in size and shape inside A, and let it "tend to A", making the size shape and position approach that of A. Then in the limit as C approaches A in size shape and position, the copy (A->B)C approaches B in size shape and position. Then if copying is a continuous function we are justified in inferring (A->B)A=B. Sorry for the math-speak.
Some diagrams will probably help. This is what (A->B)C looks like in the normal case when C is inside A:
Ah I see! It is maybe quite different than how I've been thinking about things! Can you share how you came up with these axioms? It's starting to make sense but I'm wondering what your intuition was when you were making them.
Oh, that question is so open ended, I love it but I'm really stumped on how to answer it! There is a lot of context I haven't shared, but much of it would be only marginally useful. Maybe I can say this though. A key component of the system I am trying to build are one way live copies. These copies would not only reflect the contents of their source but also the 'behavior' at their source. For instance in the image below the arrows indicate that we are copying from X to Y, from A to C, and from C to B. Then from the point of view of X, we are effectively copying from A to B, so this should be reflected in their copies in Y. One way to ensure this is to also formally copy C from X to Y, even though C isn't inside X, and ensure we copy from (X->Y)A to (X->Y)C, and from (X->Y)C to (X->Y)B. This was my motivation for considering all copies (A->B)C even if C isn't in A. This example also illustrates how my model really only answers how to name the different copies, and not how it is carried out in practice.
I don't know if that is all useful to you, but I'm curious, in your implementation of screens is everything two way copies (plus transforms), or are there one way copies too? Is this the difference taking the category as is or making it into a groupoid first makes?
Okay, I've been thinking how my more abstract ideas can be applied to model screens, like the actual kind that make for cool looking programs and videos. I've described how screens can be modeled using four axioms. Pictures seem useful so I'll give a picture for axiom 4 first.
Explanation: Axiom 4 given above said that (A->(X->Y)A) = (X->Y). This was shorthand for (A->(X->Y)A)M=(X->Y)M for all screens M. You can also make this look a little nicer by giving the name B to (X->Y)A. Then axiom 4 just states (A->B)M=(X->Y)M. The case where M is in A and A is in X is depicted in the image. Then the axiom says you only get one little square inside B by copying M. Whether you are copying from A to B or from X to Y, it doesn't make a difference.
Hopefully that clears up axiom 4. Now if you take all these axioms you find that the this formal algebra comprises a structure called a torsor. If you stipulate there are no additional relations except those implied by the four axioms then you can probably term the structure a free torsor. The significance of this is that the actual visual objects and transformations between them (rectangles of different sizes and affine maps, and I would expect Lu's transformation group also) form torsors and you can map from free objects very easily by giving a handful of shapes. That's the birds eye view and takes a bit of unpacking.
The idea of torsors is essential so I'll start with that. Rectangles in the plane almost form a torsor. For any two rectangles you can map one to the other by an affine transformation (the composition of a translation and a linear map). This isn't quite unique though because you can always then flip the target rectangle across its major or minor axis, resulting in a distinct transformation.
However, if the rectangles are "framed", by specifying a corner and an orientation then there is a unique affine map from one to the other. The flip map F changes the orientation to in the example above T no longer maps to the same framed rectangle as S. A framed rectangle can be formally specified by a point (designating a corner) and an ordered pair of vectors (designating the two sides to the corner, and the order giving the orientation). Call the framed rectangles A and B. We can think of the transformation turning A into B as a difference B-A and think of applying this transformation to A as adding it to A, so formally B=(B-A)+A.
Because the transformation from A to B was unique the difference B-A is well defined, and we can apply it to any other framed rectangle C to get a transformed rectangle (B-A)+C. This is I think the main point of torsors: You can subtract any two elements of a torsor to get a transformation mapping one to the other. In general this transformation is an element of a group (abstract algebra) and that is called the structure group of the torsor. In the case of framed rectangles I think the structure group is all affine transformations. The other point of torsors is you can apply the transformation B-A to any other element C of the torsor to get a new element (B-A)+C. In the context of framed rectangles, if B is inside A then the transform B-A can be applied to B to get another rectangle (B-A)+B inside B, and you can apply B-A again to get another rectangle inside that.
I hope that explains torsors, at least enough to make my next point. I've mentioned that a system satisfying the four axioms I gave form a torsor. I don't know a simple rigorous proof of this. (I know how to show it forms a heap which is a known equivalent of torsors). But we can also give some intuition for this. To distinguish this from the more visual system, let us call elements of a system to which the axioms apply 'places' rather than 'screens'. Then for any places A B C you can form a new place (A->B)C. Then the set of places forms a torsor whose structure group consists of all transformations A->B. The expression A->B stands for an abstract operator mapping A to B, and this operator can be applied to any other place. You can also think of A->B as the difference B-A. So this abstract system at least has the main features of torsors. The structure group can also be verified to be a group, with A->A being the identity and B->A being the inverse of A->B.
Now suppose you start with some places A B C and consider the set of all places you can build up from those, so you have A, B, C, (A->B)C, (A->(A->B)C)A, (B->A)C, to name a few at random. If the only relations (equalities) between these are those implied by the axioms then I think the resulting algebraic object can be described as a free torsor on the set {A, B, C}. I imagine this notion could be made precise but I can't find it anywhere in the mathematical literature. The key property of a free torsor on a set X (in this case X={A,B,C}) should be that for any torsor T, any function from X to T extends to a homomorphism of torsors from the free torsor on X to T. In particular if T is the torsor of framed rectangles then by assigning framed rectangles to A, B, and C we automatically get framed rectangles for all places A, B, C, (A->B)C, (A->(A->B)C)A, (B->A)C, etc. that you can think of. These represent all possible copies and transforms of rectangles or more general shapes, not only those that display because one box is in another.
The last point I want to make is what I expect these free torsors look like. Briefly, I expect both the structure group and the torsor itself embed in the free group on X, with the structure group being the subgroup of the free group generated by all elements xy^{-1} with x and y in X, and the torsor itself consisting of all products tx with t in the structure group and x in X. And (A->B)C is represented as AB^{-1}C. If this is indeed isomorphic to the free torsor on X, then it gives us a much more convenient way of establishing algebraic identities of places without appealing directly to the axioms. For instance, try proving ((X->Y)A->B) = (A->B)(Y->X) from the axioms. You can do it, but it is much easier writing each side as words in A,B,X,Y, and their inverses, and simplifying.
Anyway, Lu Wilson and @Elliot, this gets a bit closer to actual screens, so you might find it interesting.
