This is the seventh post in the Cartesian frames sequence.

Here, we introduce three new binary operations on Cartesian frames, and discuss their properties.


1. Tensor

Our first multiplicative operation is the tensor product, .

One way we can visualize our additive operations from before,  and , is to imagine two robots (say, a mining robot  and a drilling robot ) that have an override mode allowing an AI supervisor to take over that robot's decisions.

  •  represents the supervisor deciding which robot to take control of, then selecting that robot's action. (The other robot continues to run autonomously.)
  •  represents something in the supervisor's environment (e.g., its human operator) deciding which robot the supervisor will take control of. Then the supervisor selects that robot's action (while the other robot runs autonomously).

 represents an AI supervisor that controls both robots simultaneously. This lets  direct  and  to work together as a team.

Definition: Let  and  be Cartesian frames over . The tensor product of  and , written , is given by , where  is the set of morphisms  (i.e., the set of all pairs  such that  for all ), and  is given by .

Let us meditate for a moment on why this definition represents two agents working together on a team. The following will be very informal.

Let Alice be an agent with Cartesian frame , and let Bob be an agent with Cartesian frame . The team consisting of Alice and Bob should have agent , since the team's choices consist of deciding what Alice does and also deciding what Bob does.

The environment is a bit more complicated. Starting from Alice, to construct the team, we want to internalize Bob's choices: instead of just being choices in 's environment, Bob's choices will now be additional options for the team .

To do this, we want to first see Bob as being embedded in Alice's environment. This embedding is given by a function , which extends each  to a full environment . We will view Alice's possible environments as being constructed by combining a choice by Bob (that is, a ) with a function from Bob's choices to possible environments (). Then, we will move the  part across the Cartesian boundary into the agent.

Now, the agent looks like , while the environment looks like . However, we must have been able to do this starting from Bob as well, so a possible environment can also be viewed as function .

Since we should get the same world regardless of whether we think of the team as starting with Alice or with Bob, these functions  and  should agree with each other. This looks a bit like currying. The environment for an Alice-Bob team should be able to take in a Bob to create an environment for Alice, and it should also be able to take in an Alice to create an environment for Bob.


1.1. Example

We will illustrate this new operation using a simple formal example.

Jack, Kate, and Luke are simultaneously casting votes on whether to have a party. Each agent can vote for or against the party. The possible worlds are encoded as strings listing which people vote for the party, . Jack's perspective is given by the frame


Kate's perspective is given by the frame


and Luke's perspective is given by the frame


Since Luke's environment can be thought of as the team consisting of Jack and Kate, one might expect that . Indeed, we will show this is the case.

Let , and let . We label the elements of , and  as follows:

, and .

We will first enumerate all of the morphisms from  to . A morphism  consists of a function  and a function . There are 16 functions from  to  and 16 functions from  to , but most of the 256 pairs do not form morphisms.

Let us break the possibilities into cases based on . Observe that : the possible worlds where (from Kate's perspective) Kate votes for the party and Jake-interfacing-with-Kate's-perspective votes for the party too, are the same as the possible worlds where (from Jake's perspective) Jake votes for the party and Kate-interfacing-with-Jake's-perspective does too. These possible worlds must have a  in them, so  must be either  or .

If , then

so . Similarly,

so , and

so .

Similarly, if , then , and .

Thus, there are only two candidate morphisms:

  • The first, which we will call , is given by , and .
  • The second, , is given by , and .

It is easy to see that these are both indeed morphisms, by checking the definition of morphism on all four pairs in .

Thus, , and , and we can compute  from the definitions of the morphisms. The result is as follows:


This is clearly , up to reordering and relabeling rows and columns.


2. Properties of Tensor

Tensor introduces a lot of categorical structure to Chu spaces, in fact giving us a star-autonomous category. This post and the ones to come will be ignoring connections to larger topics in category theory, but only because my time and my familiarity with category theory are limited, not because these connections are unimportant.

I encourage the interested reader to learn more about the structure of Chu spaces on the excellent category theory wiki nLab, beginning with their article on the Chu construction.


2.1. Commutativity, Associativity, and Identity

Claim:  is commutative and associative, and  is the identity of  (up to isomorphism).

Proof: Commutativity is clear from the definition of , once one unpacks the definition of .

To see that 1 is the identity of , let , let , and let .

Consider the isomorphism  given by  and  We need to show that  is a morphism, and that both  and  are bijective. To see that  is a morphism, observe that for all  and ,

 Clearly,  is a bijection, so all that remains to show is that  is bijective.

To see that  is injective, observe that if , then , so , and

for all , so .

To see that  is surjective, observe that for every , there exists a morphism , given by  and . This is clearly a morphism, since 

and .

Next, we need to show that  is associative, which will be much more tedious. Let . Since we have already established commutativity, it suffices to show that .

Let , where  is the set of all triples of functions , such that for all , we have

 and  is given by

We will show that , and since the definition of  is symmetric in swapping  and , it will follow that , so .

We construct a morphism  from  to  as follows.  is just the identity on . We will let  be the morphism , where  is given by , where , and .

First, we need to show that  is well-defined, by showing that  is a morphism from  to , and that  is a morphism from . To see that  is a morphism, observe that for  and ,

To see that  is a morphism, observe for all  and all ,

where .

Now that we know  is well-defined, we need to show that  is a morphism. Indeed, for all , and for all , we have

where .

Finally, to show that  is an isomorphism, we need to show that  and  are bijective.  is trivial, since it is the identity, so it suffices to show that  is bijective.

To see that  is surjective, let  be a morphism from  to , so , and . Again, let . We will define  by , and .

We need to show that , by showing that for all , we have

Observe that since  is a morphism,

where . Also, by the definition of , we have that

and similarly


so . Finally, observe that  is in fact .

To show that  is injective, assume , and given an , let . Clearly, this means . Further, for all , and ,


Thus . Thus,  is bijective, so  is an isomorphism, so 


2.2. Biextensional Equivalence

Since many of our intuitions about Cartesian frames are up to biextensional equivalence, we should verify that tensor is well-defined up to biextensional equivalence.

Claim: If  and , then .

Proof: It suffices to show that for all . Then, by commutativity of tensor, 

Let , and let . Since , there must exist morphisms  and  such that  and  are both morphisms.

Let . Consider the morphisms , where  is given by  and  is given by .

To see that these are morphisms, observe that for any  and , we have

Finally, we need to show that  and  compose to something homotopic to the identity in both orders. This is equivalent to saying that  and  are both morphisms. Indeed, for all  and , since  is a morphism, we have


2.3. Distributivity

Claim:  distributes over , so for all Cartesian frames , and ,.

Proof: Since  is the categorical coproduct, there exist morphisms  and  such that for any morphisms  and , there exists a unique morphism such that .

Let , and let . Consider the isomorphism , where  is the natural bijection that sends  to , and  is given by .

Clearly,  is an bijection.  is also a bijection, since it is inverse to the function that sends  to the unique  as above. Thus, all that remains to show is that  is a morphism.

Let  and let . Given  and , without loss of generality, assume that . Let . Observe that since the function on agents in  is the inclusion of  into , we have that  is  restricted to . Thus, we have


2.4. Tensor is for Disjoint Agents

It doesn't really make sense to talk about  when  and 's agents are the same agent, or otherwise overlap. This is because 's agent can make choices for both  and , and if  and  overlap, 's agent could make choices for the intersection in two contradictory ways.

If you try to take the tensor of two frames whose agents overlap, you get a frame with an agent but no possible worlds.

Claim: If  is nonempty, then .

Proof: Let , and let . Consider some . There is some  such that  for all , and some  such that  for all . First, observe that  is nonempty, since it contains . Next, observe that  is empty, since if there were a morphism , it would need to satisfy , which is impossible since the left hand side is not in , while the right hand side is in . Thus,  has empty environment and nonempty agent, so 

Tensoring an agent with itself lets you play "both" agents, which has the neat consequence that if the agent has any control, you can have the agent make two different choices that put you in two different possible worlds, which is a contradiction. The result is that the agent has no possible worlds.

Corollary: If  is nonempty, then .

Proof: Trivial. 


3. Tensor is Relative to a Coarse World Model

Recall that for any function , the functor  preserves sums and products, meaning that for any Cartesian frames  and  over  and . However, the same is not true for . To see this, let's go back to the voting example above.

Let's assume that Jack, Kate, and Luke have a party if and only if a majority vote in favor, and let  be the two-element world that only tracks whether or not they have a party. Let  be the function such that  and . Then, 






We can see that  is not equivalent to  by observing that the latter has a constant  environment while the former doesn't.

Let , and let  denote the environment such that  for both . (In the matrix representation above, this is the first column.) Observe that there exists a morphism , where  and  are both the constant  function. This is a morphism because for all . This gives an environment in  , all of whose entries must be  has no such environment, so  cannot be isomorphic to , or even biextensionally equivalent. Indeed:


To see what is going on here, consider another example where Jack and Kate and Luke vote on whether to have a party, but whether or not the party happens is not just a function of the majority's vote. Instead, after the three people cast their votes, a coin is flipped:

  • If heads, the votes are tallied and majority wins as normal.
  • If tails, one of the three voters is selected at random to be dictator, and the party happens if and only if they voted in favor.

Let us work up to biextensional collapse. Let  be the Cartesian frame over  representing Jack's perspective. We have


where the top row represents voting for the party, and the bottom row represents voting against.

The first column represents environments where the party does not happen and Jack's vote didn't matter—either the coin came up heads and the others both voted against, or Kate or Luke became dictator and voted against. The third column similarly represents outcomes where the party happens regardless of how Jack votes. The second column represents all environments in which Jack's vote matters, so either he is dictator, or Kate and Luke's votes were split.

Similarly, let  be the Cartesian frame over  representing Kate's perspective,




The rows represent, in order: both voting in favor; Jack voting in favor but Kate voting against; Kate voting in favor but Jack voting against; and both voting against.

The columns represent, in order: Luke is dictator and votes against; majority rules and Luke votes against; Kate is dictator; Jack is dictator; majority rules and Luke votes in favor; and Luke is dictator and votes in favor.

Here,  looks more like what we would expect Jack and Kate working together on a team to look like. However, up to biextensional equivalence,  and  are the same as  and .

When we forget the actual votes and only look at whether the party happens, then up to biextensional collapse, the Cartesian frame representing Jack's perspective no longer has any way to distinguish between the simple majority rule vote and the complicated voting system with coins and dictators.

In general, just looking at two Cartesian frames does not tell you all of the information about the relationships between the people we might be using the frames to model. The Cartesian frames over  representing Jack and Kate's perspectives do not have any information that distinguishes between the two vote counting schemes.

When taking a tensor, we automatically include all of the possible ways the two agents can embed in each other's environments, even if a given embedding doesn't make sense in a given interpretation.


4. Par

Our next multiplicative operation is , which is pronounced "par."

Definition: Let  and  be Cartesian frames over , where .

Claim:  is De Morgan dual to , so .

Proof: Trivial. 

 has much less of an intuitive interpretation than . One reason for this is that in order to par two agents together, they have to be large enough that each other's environments embed within them. If  and  are not large enough, we will have that . (I am being informal with the word "large" here.)

One way that  and  can fail to be large enough is if  is nonempty, which is dual to the above result about tensor being for disjoint agents. It is actually pretty difficult for  and  to be large enough. If there is any fact about the world that is determined outside of both agents,  will be trivial.

We had a dual restriction for , but it didn't get in the way nearly as often: simple intuitive examples tend to be about small agents interacting with a large environment, so it is easy to imagine two agents that are disjoint. It is much harder to imagine simple examples of two agents that cover, which (informally) is what you would have to have for  to be nontrivial.

I expect to not use  very often, but I am including it here for completeness.

Claim:  is commutative and associative, and  is the identity of  (up to isomorphism).

Proof: Trivial from the fact that  is De Morgan dual to  and 

Claim: If  and , then .

Proof: Trivial from the fact that  is De Morgan dual to , and  is preserved by 

Claim:  distributes over , so for all Cartesian frames , and , we have .

Proof: Trivial from the fact that  is De Morgan dual to , and  is De Morgan dual to  


5. Lollipop

We have one more operation to introduce,  (pronounced "lollipop"), which is a Cartesian frame that can be thought of as representing the collection of morphisms between two Cartesian frames.

Definition: Given two Cartesian frames over  and , we let  denote the Cartesian frame