Sunday, June 6, 2021

Lens semigroups

Every programming language ought to have support for some kind of generalized variables. Common Lisp has place forms. Haskell has lenses which provide support for functional references. Java has support for lvalues, which greatly simplifies memory access in the JVM. In general, there are places in memory that support access and storage.

The pure mathematics of the subject is interesting in its own right. Let $S$ be a set of objects, then the generalized variables on $S$ are part of a lattice. Every mathematical model of state, change, or computation will need to make heavy use of lattice theory. State changes are handled by monoid actions, and so we will need to make equally heavy use of monoid theory. With these two tools in hand, we are ready to deal with generalized variables.

Introducing lens semigroups:

Recall that the categorical product in the topos of sets $A \times B$ is defined up to isomorphism by the effect of two projection functions $p_1, p_2$. These two projection functions $p_1, p_2$ are getters. They provide us, up to isomorphism with a way to access parts of a composite data structure. We now need a corresponding model of setters for product sets.

Up to isomorphism, every epimorphism is equivalent to a member of the lattice of partitions $Part(A)$. This is where lattice theory now comes in to play. We can now see that the two projection functions $p_1, p_2$ are actually fully determined by two equivalence relations $=_{p_1},=_{p_2}$. These two partitions have the following property which makes them a direct product.

Definition. let $P,Q \in Part(A)$ then $P$, $Q$ form a direct product provided that for each $c_1 \in P$ and $c_2 \in Q$ we have that $|c_1 \cap c_2| = 1$.

If $P,Q$ are direct products of one another then they satisfy the following system of lattice polynomial equations: \[ P \cap Q = \bot \] \[ P \vee Q = \top \] This makes $P,Q$ complements of one another. By this definition, we have characterized products of sets entirely using lattice theory.

In general, getters on any structure are always modeled by the lattice of partitions $Part(A)$. In this way, all the different properties that you can get of a structure are partially ordered. It takes a little bit more to define setters. It is not enough in that case to simply have a partition, in that case we need both two.

A setter is defined by taking two partitions that form a direct product of one another, like those formed by the projections of a categorical product, and then selecting one of the two of them for modification. We can say then that it is an ordered pair of partitions $(P,Q)$, forming a direct product of one another, such that the first of them $P$ is selected for modification.

It remains to define a monoid action on an ordered pair of this form $(P,Q)$, by which we can formally define a generalized variable. The key to solving this problem is action congruences. The monoid action on generalized variables is defined by turning both partitions into action congruences.

Definition. let $S$ be a set then a lens semigroup is defined for a pair of partitions $P,Q$ that form a direct product of one another by $L(P,Q) = Acs(P) \cap Ocs(Q)$.

By this approach, we have a distinction between two different lattice theoretic settings for getters and setters. Getters are always defined by the lattice of partitions $Part(A)$, while setters are defined by the lattice of subsemigroups of the full transformation semigroup. In either case, we can model state and change by a lattice of variables.

Example 1. the trivial lens $[\top,\bot]$ which includes only the identity transformation

Example 2. the full lens $[\bot, \top]$ which is equal to the full transformation semigroup $T_S$ itself.

Example 3. let $(x_1,...x_n)$ be an n-tuple and let $i \in [1,n]$ be some index then $[\{i\},\{i\}^C]$ forms the lens of all transformations at the index $i$.

Example 4. let $\mathbb{C}$ be the field of complex numbers. Then we can form real and imaginary lens semigroups from transformations of the real or imaginary parts. The Galois group $Gal(\frac{\mathbb{C}}{\mathbb{R}})$ contains only complex conjugation, so it is a subgroup of the imaginary lens semigroup.

Example 5. let $n$ be a member of a finite interval of numbers [1,n] and let $d \subseteq n$ then [mod_d,quot_d] is a generalized variable consisting of the value at the least significant place of the d-valued digit. In general, digits provide a collection of different types of generalized variables of numbers.

Relations among lenses:

Inclusion:
The set of all generalized variables on a set is a suborder of the lattice of transformation semigroups. Therefore, it is possible that one lens semigroup can contain another. The following is a set of sufficient conditions for lens semigroup inclusion.

Theorem. let $L(P_1,Q_1)$ and $L(P_2,Q_2)$ be lens semigroups on a set $S$. Then $L(P_1,Q_1) \subseteq L(P_2,Q_2)$ provided that $P_1,Q_1,P_2,Q_2$ satisfy the following system of lattice polynomial equations: \[ P_1 \vee P_2 = P_1 \] \[ Q_1 \vee Q_2 = Q_2 \] \[ (Q_1 \vee P_2) \wedge P_1 = P_2 \] Proof. the semigroup $L(P_1,Q_1)$ is a subsemigroup of $Ocs(Q_1)$. By the fact that any semigroup with a given orbit, has any parent partition orbit then $L(P_1,Q_1)$ also is a subsemigroup of $Ocs(Q_2)$. Again by the fact we can extend orbits, $(Q_1 \vee P_2)$ is an action congruence of $L(P_1,Q_1)$. Action congruences are intersection closed, so $(Q_1 \vee P_2) \cap P_1$ is again an action congruence, but by condition three it is equal to $P_2$ so it follows that $L(P_1,Q_1) \subset Acs(P_2)$. By combining both conditions we get $L(P_1,Q_1) \subseteq L(P_2,Q_2)$. $\square$

This establishes the hierarchy of generalized variables on a set. The first example is the smallest lens semigroup, and the second example is the largest. A hierarchy of generalized variables may exist in between.

Commutativity:
If we have a lens semigroup $L(P_1,Q_1)$ then it clearly has a complement $L(Q_1,P_1)$, which consists of all transformations of the uneffected part of the lens. These two semigroups form a commuting pair:

Theorem. $L(P_1,Q_1)$ and $L(Q_1,P_1)$ commute.

Proof. let $t_1 \in L(P_1,Q_1)$ and $t_2 \in L(Q_1,P_1)$. Then $P_1,Q_1$ are action congruences of both $t_2$ and $t_2$, and so they are also action congruences of the composition $t_1 \circ t_2$. Then $\frac{t_1 \circ t_2}{P_1}$ is equal to $\frac{t_1}{p_1} \circ id$ and $\frac{t_1 \circ t_2}{Q_1} = id \circ \frac{t_2}{q_1}$. Likewise, $\frac{t_2 \circ t_1}{P_1} = id \circ \frac{t_1}{p_1}$ and $\frac{t_2 \circ t_1}{Q_1} = \frac{t_2}{q_1} \circ id$. The identities cancel and then the two results coincide. $\square$

This formalizes the fact that you can perform transformations on two separate generalized variables and they will always commute because they don't effect each other's inputs or outputs. In general we have:

Corollary. let $S \subseteq L(P_1,Q_1)$ and $T \subseteq L(Q_1,P_2)$ then $S$ and $T$ commute.

This follows easily by the antitone relationship between inclusion and commutativity. The commutativity formed by different transformations applied to indepedent generalized variables is a stronger kind of commutativity then that encountered in general. It means not only do the two transformations commute, they don't effect each other in any other way.

Local actions:

Let $S$ be a set, then $T_S$ is the full transformation monoid on $S$. A monoid action of $M$ is then defined by a monoid homomorphism of the form: \[ M \to T_S \] A lens semigroup $L(P,Q)$ is a very special case, because it is a faithful monoid homomorphism from a full transformation monoid into the full transformation monoid: \[ T_P \to T_S \] By this process, we can define a local action on the lens semigroup by a monoid action on $T_P$, which will then be transformed into a monoid action on $T_S$ by the chain of homomorphisms: \[ N \to T_P \to T_S \] This defines the local action on a lens $T_P$. The global action on $T_S$ is defined by action on the maximal lens. By this approach, we can consider every action to be relative to some lens. Likewise, any sort of monoid action we already have can be cast to one on a lens.

A special case occurs when we have a sublens $L(P_1,Q_1) \subseteq L(P_2,Q_2)$. The action of $L(P_1,Q_1)$ can be applied locally to $L(P_2,Q_2)$ by inclusion, which produces a chain of monoid homomorphisms of the following form: \[ T_{P_1} \to T_{P_2} \to T_S \] Chains of lens correspond to chains of monoid homomorphisms. By this process, local actions can even be applied to other lens. This often occurs when modifications occur to generalized variabes that are contained in one another.

Local actions provide a much more realistic model of state and change then the global actions on a set. The real world is partially ordered and localistic. There are at any moment a number of diferent things happening independently at the same time. Each of these things are happening locally. Simultaneous local changes combine to create the reality we know.

The same is true in computing. Computation devices mostly modify the state that is most local to them. Programs actually deliberately try to localize their state to themselves, so that they are not effected by other programs. This is true even of individual subroutines. A realistic model of computation must take into account the locality of actions.

No comments:

Post a Comment