Crossposted from the AI Alignment Forum. May contain more technical jargon than usual.

This is the fifth post in the Cartesian frames sequence. Read the first post here.

Up until this point, we have only been working with Cartesian frames over a fixed world . Now, we are going to start talking about Cartesian frames over different worlds.


1. Functors from Functions Between Worlds

In the Cartesian frames framework, a world is a set of possible worlds  that can all potentially occur in the same frame.

I find it useful to think about "different worlds"  and  in the case where  and  are different world models that carve up a situation in two different ways.  might be a refined world model, one that describes a situation in more detail; while  is a coarser model of the same situation that elides some distinctions in .

Returning to an example from "Biextensional Equivalence,"  could be a world model that includes details about what the agent is thinking ( for a thought about the color green,  for red), as shown in


while  could be a world model that leaves out this information, representing the same real-world situation with the frame


To move between frames like  and  and compare their properties, we will need a way to send agents and environments of frames defined over one world, to agents and environments of frames over an entirely different world. Functors will allow us to do this.

Definition: Given two sets  and and , and a function , let  denote the functor that sends the object  to the object , where , and sends the morphism  to the morphism with the same underlying functions, .

To visualize this functor, you can imagine  as a graph, with matrices as nodes (in the finite case) and arrows representing morphisms.  is another graph made of matrices and arrows. To move each frame  from  to , we use  to entrywise replace the possible worlds in 's matrix with elements of , without changing the functional properties of the rows and columns; and then we move all the arrows from  to , which is possible because no functional properties of the original matrices were lost. (Frames and morphisms may or may not be added when we move to .)

In the cases where we say " is a refined version of " or " is a coarse version of ," all we mean is that the function  is surjective.

Claim:  is well-defined.

Proof: We need to show that  actually sends objects and morphisms of  to objects and morphisms of , and that it preserves identity morphisms and composition.  clearly sends objects to objects. To see that  sends morphisms to morphisms, observe that if , and , then for all  and ,

so  is a morphism. It is clear that  preserves identity  and composition, since it has no effect on morphisms. 

We also have that  preserves all of our additive operations.

Claim: , and .

Proof: Trivial. 

Our new functor's relationship with  and  is more interesting. In particular, we can define  and  from  and  using functors.

Claim: Let  and let  be the inclusion of  in . Then  and . (Here, the  and  are from , not .)

Proof: Trivial. 

This gives us a more categorical definition of  and  from  and . We will give a more categorical definition of  and  later, when we talk about multiplicative operations.

 also preserves biextensional equivalence in one direction. (Two equivalent frames in  will always be equivalent in , but two inequivalent frames in  won't necessarily be inequivalent in .)

Claim: If , then .

Proof: Let  and let . Let  and  compose to something homotopic to the identity in both orders. We want to show that  and  compose to something homotopic to the identity in both orders. Indeed  for all  and , and  for all  and 

We also have that  preserves what's ensurable, where we transition from subsets of  to subsets of  in the obvious way.

Claim: Let , and let . If , then .

Proof: Trivial from the original definition of ensurables

We also get a stronger result when dealing with subsets of  and  that correspond exactly.

Claim: Let , and let  and  be such that for all , we have  if and only if . Then  if and only if , and  if and only if .

Proof: Trivial from the original definitions of ensurables and controllables

The relationship between observability and functors is quite interesting. We will devote the next section to discussing this relationship and its philosophical consequences.


2. What's Observable is Relative to a Coarse World Model

Since observability is not closed under supersets, we can only really hope to get a result for observables in the stronger case where  and  correspond exactly; but interestingly, even then, the preservation result for observables is only one-directional.

Claim: Let  and let  and  be such that for all , we have  if and only if . Then if , then .

Proof: If , with  and , then , and , while 

The most interesting thing here is that the converse is not also true. There are examples where , even though .

When  is surjective, we think of  as a coarse world model that forgets some details from . Sometimes, an agent can be able to observe  relative to a coarse description of the world, but not in the more refined description, even in cases where  is definable in both the coarse and refined descriptions.


2.1. Example

Let us look at an example. In this example, the agent is an AI that will be given a number and asked whether it is prime or not. There are two possible environments .

The agent  has six strategies:

  • It can compute whether the number is prime and answer correctly (), or it can compute whether the number is prime and answer incorrectly . In both of these cases, it has to use a lot of energy and will become hotter.
  • It can also just not think and say that the number is prime , or it can not think and say that the number is not prime ().
  • Finally, it can deliberately waste a lot of energy for no reason and say the number is prime or waste a lot of energy and say the number is not prime ( and  respectively).

Finally, , where the first letter indicates whether the AI was given a prime or nonprime number, the second letter indicates whether the AI's answer was accurate or inaccurate, and the third letter indicates whether the AI is hot. The Cartesian frame, , looks like this.

We will let  be the coarse description of the world in which we only pay attention to the input/output behavior of the AI and ignore whether or not it becomes hot. , and we will let  be the function that deletes the third letter. This gives us the following for .

The important thing to notice here is that —when we ignore heat, the agent can base conditional strategies on whether the number is prime—but .

In particular, , where

 and ,

while it is easy to see that , because there is no .


2.2. Discussion

The above example illustrates something interesting about observables. It shows that what's observable is not only a function of the observing agent and the thing that is observed. It is also a function of the level of description of the world!

This makes sense because we are thinking of observation as the ability to implement conditional policies. To implement a conditional policy is to be indistinguishable from the constant policy  in worlds in  and indistinguishable from the constant policy  in worlds outside of . This indistinguishability makes observables relative to the level of description of the world.

There is something internal to the agent that is different between the world where it implements a conditional policy and the world where it implements a constant policy. However, when we talk of  being an observable for the agent, we are working relative to a level of description that does not track that internal difference.


3. Functors from Cartesian Frames

When  is surjective,  will send Cartesian frames over the more refined  to Cartesian frames over the less refined . What if we want to go in the other direction?

While there is a unique function from less refined worlds to more refined worlds, there are many functions in the other direction. Luckily, we have an object that lets us deal with many functions at once.

Definition: Let  be a Cartesian frame over , with . Then  is the functor that sends  to , where , and sends the morphism  to , where .

(Notice how this definition looks a bit like currying.)

Claim:  is well-defined.

Proof: We need to show that  actually sends objects and morphisms of  to objects and morphisms of , and that it preserves identity morphisms and composition.

 clearly sends objects to objects. To see that it sends morphisms to morphisms, let  be a morphism in , let , and let .

We want to show that  is a morphism, which is true because

for all  and  clearly preserves identity morphisms and composition. 

The coarse-to-refined functor  preserves , and , but not , or , which make sense, since  is violating the symmetry between agent and environment.

Claim: , and .

Proof: Trivial. 

Claim: .

Proof: Let  and let . We have that  and . The agent and environment are the same, so we just need to check that .

Take  and . Without loss of generality, assume . Observe that

One way to see that  does not preserve  is to see that the environments are different, since  has one copy of  in the environment, while  has two copies.

We also have that  preserves biextensional equivalence.

Claim: if , then .

Proof: Let , and let . Let  and  compose to something homotopic to the identity in both orders. It suffices to show that  is homotopic to the identity on , since the other composition will be symmetric. Indeed

 for all , and 

Before we talk about the relationship between functors from functions and functors from Cartesian frames, I want to pause to talk about how to view Cartesian frames as sets of functions.


4. Cartesian Frames as Sets of Functions

One way to view (some) Cartesian frames is as sets of functions.

Definition: Given a set  of functions from  to , let  denote the Cartesian frame over  given by , where .

Claim:  is well-defined.

Proof: Trivial. 

Not every Cartesian Frame is expressible this way: every Cartesian frame is biextensionally equivalent to a Cartesian frame with duplicate columns and rows, and these uncollapsed frames are excluded because sets do not allow multiplicity.

Claim: For every Cartesian frame  over , there exists a set of functions , such that .

Proof: Take , and take  to be the set of all  such that there exists an  such that for all . Take  and , given as follows:  is the identity on  is the function , and  is some  such that . These are both clearly morphisms, and they compose to something homotopic to the identity, since  and  are both the identity. 

This give us an alternate definition of Cartesian frames up to biextensional equivalence. This almost gives a complete alternate definition of Cartesian frames; if we instead took  to be a multiset, then we could identify the Cartesian frame  with the multiset .

Note that this is not as symmetric as our original definition of Cartesian frames. The "sets of functions" approach here thinks of a Cartesian frame as a set of functions from the environment to the world, but we could instead think of it as a set of functions from the agent to the world.

Definition: Given a set  of functions for  to , let  denote the Cartesian frame over  given by , where .

Claim: .

Proof: Trivial. 

Thinking of Cartesian frames in this way is not particularly different from our original definition. It is just thinking about a function with two inputs as a parameterized function with one input and one parameter. However, this way of understanding Cartesian frames will allow us to more easily relate functors from functions to functors from Cartesian frames.


5. Relationship Between the Two Functor Definitions

Functors from functions are a special case of functors from Cartesian frames. Indeed, they correspond when  is a singleton.

Claim: For any . Conversely, if  is a Cartesian frame over  with singleton environment, then , where .

Proof: Observe that , where . That  is trivial from considering the definition of  in the special case where  is a singleton. 

However, we can do a lot more with functors from Cartesian frames. In the case where  is a surjection,  shows how to send Cartesian frames over the more refined  to the less refined . We want to go in the other direction using an inverse of .

Since  is a surjection, it has a right inverse, but it might have many right inverses. If we want to go from Cartesian frames over  to Cartesian frames over , we could pick any right inverse to , but since we have functors from Cartesian frames, we don't have to.

Claim: For any surjective , let  be the set of all  such that  is the identity on . Then for any Cartesian frame  over . Thus  is right inverse to  up to biextensional equivalence.

Proof: Let . Then , where  and  where

(Viewed as a matrix,  is isomorphic to  with  copies of each column.)

To explicitly see the homotopy equivalence, take  by  and , and take  by  and  for some fixed . These are clearly morphisms and clearly compose to something homotopic to the identity in both orders, since the  are the identity. Note that we used the surjectivity of  when we said "for some fixed ," since the surjectivity of  is what makes  nonempty. 


Functors from Cartesian frames will prove useful in the next section, when we finally introduce the concept of subagent.

New Comment
3 comments, sorted by Click to highlight new comments since: Today at 7:59 PM

minor typo:

and take  to be the set of all  such that

should have 

Also I think later in that proof some of the 's (like in ) should be 's instead.

Fixed, Thanks. 

I think the 's are correct. Any morphism in which either component is the identity must be homotopic to the identity, since homotopic is symmetric. In this proof, checking the 's is easier.

Nice! I'm glad I asked, since I hadn't realised those sufficient conditions for being homotopic to the identity. That's useful in several proofs I suspect. (For anyone following along, I believe this only holds for a morphism from a frame to itself.)