Since we have already established commutativity, it suffices to show that .
For the confused reader, the argument in more detail here is:
where is commutativity of tensor, is the fact claimed to suffice above, and is the implicitly assumed lemma that and implies (this is proved later but only for ).
minor typo in the indices here:
We will show that , and since the definition of is symmetric in swapping and , it will follow that
It seems like there has to be some kind of relationship between lollipop and the sub-agent relation, right? Like, they're both about one 'agent' sending info to another to combine to send something to the environment. But I'm not quite sure what the relationship is going to be: presumably it's going to be that if C ◃ D, then C ⊸ D is {equal, isomorphic, biextensionally equivalent} to some special object, but IDK what that object would be.
So, I'd have thought there would be a morphism from C ⊸ ⊥ to (C ⊸ D) ⊗ (D ⊸ ⊥). You get a function from hom(C,⊥) to hom(C,D) x hom(D,⊥) from C being a subagent of D. But you also need a convenient function from hom(C ⊸ D, dual(D ⊸ ⊥)) to env(C). Now, dual(D ⊸ ⊥) is just D, so it's really a function from hom(C ⊸ D, D) to env(C). But I have no idea what that function would be.
Reader's note: I wish there were somewhere I could look to see the definitions of 0, 1, null, top, and bottom, all in the same place.
For my personal use when I was helping review Scott's drafts, I made some mnemonics (complete with silly emojis to keep track of the small Cartesian frames and operations) here: https://docs.google.com/drawings/d/1bveBk5Pta_tml_4ezJ0oWiq-qudzgnsRlfbGJgZ1qv4/.
(Also includes my crude visualizations of morphism composition and homotopy equivalence to help those concepts stick better in my brain.)
And now I've made a LW post collecting most of the definitions in the sequence so far, so they're easier to find: https://www.lesswrong.com/posts/kLLu387fiwbis3otQ/cartesian-frames-definitions
You can prove there's a morphism the other way, but that doesn't rely on any subagency relationship.
I haven't put time into thinking about most of your comments yet, but I'm pretty sure the answer to this is yes.
EDIT: Oh, I just realized it wasn't a question.
This thread is mostly me trying to work something out and reporting the results. To the extent there's a question, it's this: if C ◃ D, is there something interesting to say about C ⊸ D?
I am not sure, but I think that the answer is that you can't say anything interesting with just , but can maybe say interesting things with and , which I am about to introduce. In the post that just went up, is the relationship between one of the components and a sub-sum, and is the relationship between one of the components and a sub-tensor. is the transitive closure of and .
I think that if , then there is a nice morphism from to , and if , there is a set of nice morphisms from to but in some degenerate cases that set is empty, which is how I constructed a counter example in my other comment.
I guess one version of this is that if C ◃ D, then for all e in the environment of C, there's some (g,h) in agent(C ⊸ D) and (a,f) in env(C ⊸ D) such that e = h(f). So for all (a,e) in agent(C) x env(C), there's (a', e') in agent(C ⊸ D) x env(C ⊸ D) so that a ⋅ e = a' ⋄ e'. Which I guess is something.
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 Agent(C) and a drilling robot Agent(D)) that have an override mode allowing an AI supervisor to take over that robot's decisions.
C⊗D represents an AI supervisor that controls both robots simultaneously. This lets Agent(C⊗D) direct Agent(C) and Agent(D) to work together as a team.
Definition: Let C=(A,E,⋅) and D=(B,F,⋆) be Cartesian frames over W. The tensor product of C and D, written C⊗D, is given by C⊗D=(A×B,hom(C,D∗),⋄), where hom(C,D∗) is the set of morphisms (g,h):C→D∗ (i.e., the set of all pairs (g:A→F,h:B→E) such that b⋆g(a)=a⋅h(b) for all a∈A, b∈B), and ⋄ is given by (a,b)⋄(g,h)=b⋆g(a)=a⋅h(b).
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 C=(A,E,⋅), and let Bob be an agent with Cartesian frame D=(B,F,⋆). The team consisting of Alice and Bob should have agent A×B, 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 A's environment, Bob's choices will now be additional options for the team A×B.
To do this, we want to first see Bob as being embedded in Alice's environment. This embedding is given by a function h:B→E, which extends each b∈B to a full environment e∈E. We will view Alice's possible environments as being constructed by combining a choice by Bob (that is, a b∈B) with a function from Bob's choices to possible environments (h:B→E). Then, we will move the B part across the Cartesian boundary into the agent.
Now, the agent looks like A×B, while the environment looks like B→E. However, we must have been able to do this starting from Bob as well, so a possible environment can also be viewed as function g:A→F.
Since we should get the same world regardless of whether we think of the team as starting with Alice or with Bob, these functions g and h 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, W={ε,J,K,L,JK,JL,KL,JKL}. Jack's perspective is given by the frame
CJ=(JJKJLJKLεKLKL),
Kate's perspective is given by the frame
CK=(KJKKLJKLεJLJL),
and Luke's perspective is given by the frame
CL=(LJLKLJKLεJKJK).
Since Luke's environment can be thought of as the team consisting of Jack and Kate, one might expect that CJ⊗CK≅C∗L. Indeed, we will show this is the case.
Let CJ=(A,E,⋅), and let CK=(B,F,⋆). We label the elements of A, E, B, and F as follows:
CJ=eεeKeLeKLaJaε(JJKJLJKLεKLKL), and CK=fεfJfLfJLbKbε(KJKKLJKLεJLJL).
We will first enumerate all of the morphisms from CJ to C∗K. A morphism (g,h):CJ→C∗K consists of a function g:A→F and a function h:B→E. There are 16 functions from A to F and 16 functions from B to E, but most of the 256 pairs do not form morphisms.
Let us break the possibilities into cases based on g(aJ). Observe that bK⋆g(aJ)=aJ⋅h(bK): 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 J in them, so g(aJ) must be either fJ or fJL.
If g(aJ)=fJ, then
aJ⋅h(bK)=bK⋆g(aJ)=JK,so h(bK)=eK. Similarly,
aJ⋅h(bε)=bε⋆g(aJ)=J,so h(bε)=eε, and
bK⋆g(aε)=aε⋅h(bK)=K,so g(aε)=fε.
Similarly, if g(aJ)=fJL, then h(bK)=eKL, h(bε)=eL, and g(aε)=fL.
Thus, there are only two candidate morphisms:
It is easy to see that these are both indeed morphisms, by checking the definition of morphism on all four pairs in A×B.
Thus, Env(CJ⊗CK)={ϕε,ϕL}, and Agent(CJ⊗CK)=A×B, and we can compute Eval(CJ⊗CK) from the definitions of the morphisms. The result is as follows:
CJ⊗CK=ϕεϕL(aJ,bK)(aJ,bε)(aε,bK)(aε,bε)⎛⎜ ⎜ ⎜⎝JKJKLJJLKKLεL⎞⎟ ⎟ ⎟⎠.
This is clearly C∗L, 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 1 is the identity of ⊗ (up to isomorphism).
Proof: Commutativity is clear from the definition of ⊗, once one unpacks the definition of hom(C,D∗).
To see that 1 is the identity of ⊗, let C=(A,E,⋅), let 1=({b},W,⋆), and let C⊗1=(A×{b},hom(C,1∗),⋄).
Consider the isomorphism (ι0,ι1):C→C⊗1 given by ι0(a)=(a,b) and ι1(g,h)=h(b). We need to show that (ι0,ι1) is a morphism, and that both ι0 and ι1 are bijective. To see that (ι0,ι1) is a morphism, observe that for all a∈A and (g,h):C→1∗,
ι0(a)⋄(g,h)=a⋅h(b)=a⋅ι1(g,h).Clearly, ι0 is a bijection, so all that remains to show is that ι1 is bijective.
To see that ι1 is injective, observe that if ι1(g0,h0)=ι1(g1,h1), then h0(b)=h1(b), so h0=h1, and
g0(a)=b⋆g0(a)=a⋅h0(b)=a⋅h1(b)=b⋆g1(a)=g1(a)for all a∈A, so g0=g1.
To see that ι1 is surjective, observe that for every e∈E, there exists a morphism (ge,he):C→1∗, given by he(b)=e and ge(a)=a⋅e. This is clearly a morphism, since
b⋆ge(a)=ge(a)=a⋅e=a⋅he(b),and ι1(ge,he)=e.
Next, we need to show that ⊗ is associative, which will be much more tedious. Let Ci=(Ai,Ei,⋅). Since we have already established commutativity, it suffices to show that (C0⊗C1)⊗C2≅(C0⊗C2)⊗C1.
Let D=(A0×A1×A2,F,⋆), where F is the set of all triples of functions (g0:A1×A2→E0,g1:A0×A2→E1,g2:A0×A1→E2), such that for all ai∈Ai, we have
a0⋅0g0(a1,a2)=a1⋅1g1(a0,a2)=a2⋅2g2(a0,a1),and ⋆ is given by
(a0,a1,a2)⋆(g0,g1,g2)=a0⋅0g0(a1,a2)=a1⋅1g1(a0,a2)=a2⋅2g2(a0,a1).We will show that (C0⊗C1)⊗C2≅D, and since the definition of D is symmetric in swapping C1 and C2, it will follow that (C0⊗C2)⊗C1≅D, so (C0⊗C1)⊗C2≅(C0⊗C2)⊗C1.
We construct a morphism (ι0,ι1) from (C0⊗C1)⊗C2 to D as follows. ι0 is just the identity on A0×A1×A2. We will let ι1(g0,g1,g2) be the morphism (g2,h):C0⊗C1→C∗2, where h:A2→hom(C0,C∗1) is given by h(a2)=(ha20,ha21):C0→C∗1, where ha20(a0)=g1(a0,a2), and ha21(a1)=g0(a1,a2).
First, we need to show that ι1 is well-defined, by showing that h(a2) is a morphism from C0 to C∗1, and that (g2,h) is a morphism from C0⊗C1→C∗2. To see that h(a2)=(ha20,ha21) is a morphism, observe that for a0∈A0 and a1∈A1,
a1⋅1ha20(a0)=a1⋅1g1(a0,a2)=a0⋅0g0(a1,a2)=a0⋅0ha21(a1).To see that (g2,h) is a morphism, observe for all (a0,a1)∈A0×A1 and all a2∈A2,
a2⋅2g2(a0,a1)=a0⋅0g0(a1,a2)=a0⋅0ha21(a1)=(a0,a1)⋄(ha20,ha21)=(a0,a1)⋄h(a2),where ⋄=Eval(C0⊗C1).
Now that we know ι1 is well-defined, we need to show that (ι0,ι1) is a morphism. Indeed, for all (a0,a1,a2)∈A0,A1,A2, and for all (g0,g1,g2)∈F, we have
ι0(a0,a1,a2)⋆(g0,g1,g2)=a2⋅2g2(a0,a1)=(a0,a1,a2)∙(g2,h)=(a0,a1,a2)∙ι1(g0,g1,g2),where ∙=Eval((C0⊗C1)⊗C2).
Finally, to show that (ι0,ι1) is an isomorphism, we need to show that ι0 and ι1 are bijective. ι0 is trivial, since it is the identity, so it suffices to show that ι1 is bijective.
To see that ι1 is surjective, let (g,h) be a morphism from C0⊗C1 to C∗2, so g:A0×A1→E2, and h:A2→hom(C0,C∗1). Again, let h(a2)=(ha20,ha21). We will define (g0,g1,g2) by g2=g, g1(a0,a2)=ha20(a0), and g0(a1,a2)=ha21(a1).
We need to show that (g0,g1,g2)∈F, by showing that for all (a0,a1,a2)∈A0×A1×A2, we have
a0⋅0g0(a1,a2)=a1⋅1g1(a0,a2)=a2⋅2g2(a0,a1).Observe that since (g,h) is a morphism,
a2⋅2g2(a0,a1)=a2⋅2g(a0,a1)=(a0,a1)⋆h(a2)=(a0,a1)⋆(ha20,ha21),where ⋆=Eval(C0⊗C1). Also, by the definition of C0⊗C1, we have that
(a0,a1)⋆(ha20,ha21)=a0⋅0ha21(a1)=a0⋅0g0(a1,a2),and similarly
(a0,a1)⋆(ha20,ha21)=a1⋅1ha20(a1)=a1⋅1g1(a0,a2).Thus,
a0⋅0g0(a1,a2)=a1⋅1g1(a0,a2)=a2⋅2g2(a0,a1),so (g0,g1,g2)∈F. Finally, observe that ι1(g0,g1,g2) is in fact (g,h).
To show that ι1 is injective, assume ι1(g0,g1,g2)=ι1(g′0,g′1,g′2)=(g,h), and given an a2∈A2, let h(a2)=(ha20,ha21). Clearly, this means g2=g=g′2. Further, for all a0∈A0, a1∈A1, and a2∈A2,
g0(a1,a2)=ha21(a1)=g′0(a1,a2)and
g1(a0,a2)=ha20(a0)=g′1(a0,a2).Thus (g0,g1,g2)=(g′0,g′1,g′2). Thus, ι1 is bijective, so (ι0,ι1) is an isomorphism, so (C0⊗C1)⊗C2≅D≅(C0⊗C2)⊗C1. □
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 C0≃C1 and D0≃D1, then C0⊗D0≃C1⊗D1.
Proof: It suffices to show that for all D, C0⊗D≃C1⊗D. Then, by commutativity of tensor,
C0⊗D0≃C0⊗D1≅D1⊗C0≃D1⊗C1≡C1⊗D1.Let Ci=(Ai,Ei,⋅i), and let D=(B,F,⋆). Since C0≃C1, there must exist morphisms (g0,h0):C0→C1 and (g1,h1):C1→C0 such that (g1∘g0,idE0):C0→C0 and (g0∘g1,idE1):C1→C1 are both morphisms.
Let Ci⊗D=(Ai×B,hom(Ci,D∗),⋄i). Consider the morphisms (g′i,h′i):Ci⊗D→C1−i⊗D, where g′i:Ai×B→A1−i×B is given by g′i(a,b)=(gi(a),b) and h′i:hom(C1−i,D∗)→hom(CI,D∗) is given by h′i(g,h)=(g,h)∘(gi,hi).
To see that these are morphisms, observe that for any (a,b)∈Ai×B and (g,h):C1−i→D∗, we have
g′i(a,b)⋄1−i(g,h)=(gi(a),b)⋄1−i(g,h)=b⋆g(gi(a))=b⋆(g∘gi)(a))=(a,b)⋄i(g∘gi,hi∘h)=(a,b)⋄ih′i(g,h).Finally, we need to show that (g′0,h′0) and (g′1,h′1) compose to something homotopic to the identity in both orders. This is equivalent to saying that (g′0∘g′1,idhom(C1,D∗)) and (g′1∘g′0,idhom(C0,D∗)) are both morphisms. Indeed, for all (a,b)∈Ai×B and (g,h):Ci→D∗, since (g1−i∘gi,idEi) is a morphism, we have
g′1−i(g′i(a,b))⋄i(g,h)=(g1−i(gi(a)),b)⋄i(g,h)=g1−i(gi(a))⋅ih(b)=a⋅ih(b)=(a,b)⋄i(g,h).□
2.3. Distributivity
Claim: ⊗ distributes over ⊕, so for all Cartesian frames C0, C1, and D,(C0⊕C1)⊗D≅(C0⊗D)⊕(C1⊗D).
Proof: Since ⊕ is the categorical coproduct, there exist morphisms ι0:C0→C0⊕C1 and ι1:C1→C0⊕C1 such that for any morphisms ϕ0:C0→D∗ and ϕ1:C1→D∗, there exists a unique morphism ϕ:C0⊗C1→D∗such that ϕi=ϕ∘ιi.
Let Ci=(Ai,Ei,⋅i), and let D=(B,F,⋆). Consider the isomorphism (g,h):(C0⊗D)⊕(C1⊗D)→(C0⊕C1)⊗D, where g:(A0×B)⊔(A1×B)→(A0⊔A1)×B is the natural bijection that sends (a,b) to (a,b), and h:hom(C0⊕C1,D∗)→hom(C0,D∗)×hom(C1,D∗) is given by h(ϕ)=(ϕ∘ι0,ϕ∘ι1).
Clearly, g is an bijection. h is also a bijection, since it is inverse to the function that sends (ϕ0,ϕ1) to the unique ϕ as above. Thus, all that remains to show is that (g,h) is a morphism.
Let ⋄=Eval((C0⊗D)⊕(C1⊗D)) and let ∙=Eval((C0⊕C1)⊗D). Given (a,b)∈(A0×B)⊔(A1×B) and (g′,h′)∈hom(C0⊕C1,D∗), without loss of generality, assume that a∈A0. Let (g′0,h′0)=(g′,h′)∘ι0. Observe that since the function on agents in ι0 is the inclusion of A0 into A0⊔A1, we have that g′0 is g′ restricted to A0. Thus, we have
g(a,b)∙(g′,h′)=(a,b)∙(g′,h′)=b⋆g′(a)=b⋆g′0(a)=(a,b)⋄(g′0,h′0)=(a,b)⋄h(g′,h′).□
2.4. Tensor is for Disjoint Agents
It doesn't really make sense to talk about C⊗D when C and D's agents are the same agent, or otherwise overlap. This is because C⊗D's agent can make choices for both C and D, and if C and D overlap, C⊗D'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 Ensure(C)∩Prevent(D) is nonempty, then C⊗D≃⊤.
Proof: Let C=(A,E,⋅), and let D=(B,F,⋆). Consider some S∈Ensure(C)∩Prevent(D). There is some a∈A such that a⋅e∈S for all e∈E, and some b∈B such that b⋆f∉S for all f∈F. First, observe that Agent(C⊗D) is nonempty, since it contains (a,b). Next, observe that Env(C⊗D) is empty, since if there were a morphism (g,h):C→D∗, it would need to satisfy b⋆g(a)=a⋅h(b), which is impossible since the left hand side is not in S, while the right hand side is in S. Thus, C⊗D has empty environment and nonempty agent, so C⊗D≃⊤. □
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 Ctrl(C) is nonempty, then C⊗C≃⊤.
Proof: Trivial. □
3. Tensor is Relative to a Coarse World Model
Recall that for any function p:W→V, the functor p∘:Chu(W)→Chu(V) preserves sums and products, meaning that for any Cartesian frames C and D over W, p∘(C⊕D)=p∘(C)⊕p∘(D) and p∘(C&D)=p∘(C)&p∘(D). 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 V={Y,N} be the two-element world that only tracks whether or not they have a party. Let p:W→V be the function such that p(ε)=p(J)=p(K)=p(L)=N and p(JK)=p(JL)=p(KL)=p(JKL)=Y. Then,
p∘(CJ)≅p∘(CK)≅(NYYYNNNY)≃(NYYNNY),
and
p∘(CJ⊗CK)≅p∘(C∗L)≅⎛⎜ ⎜ ⎜⎝YYNYNYNN⎞⎟ ⎟ ⎟⎠≃⎛⎜⎝YYNYNN⎞⎟⎠,
but
(NYYYNNNY)⊗(NYYYNNNY)/≄⎛⎜ ⎜ ⎜⎝YYNYNYNN⎞⎟ ⎟ ⎟⎠.
We can see that p∘(CJ⊗CK) is not equivalent to p∘(CJ)⊗p∘(CK) by observing that the latter has a constant N environment while the former doesn't.
Let p∘(CJ)≅p∘(CK)≅(A,E,⋅), and let eN∈E denote the environment such that a⋅eN=N for both a∈A. (In the matrix representation above, this is the first column.) Observe that there exists a morphism (g,h):(A,E,⋅)→(A,E,⋅)∗, where g and h are both the constant eN function. This is a morphism because for all a0,a1∈A, a0⋅h(a1)=a1⋅g(a0)=N. This gives an environment in p∘(CJ)⊗p∘(CK), all of whose entries must be N. p∘(CJ⊗CK) has no such environment, so p∘(CJ⊗CK) cannot be isomorphic to p∘(CJ)⊗p∘(CK), or even biextensionally equivalent. Indeed:
p∘(CJ)⊗p∘(CK)≃⎛⎜ ⎜ ⎜⎝NYYYYYNNNYYYNNYNYYNNNNNY⎞⎟ ⎟ ⎟⎠.
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:
Let us work up to biextensional collapse. Let DJ be the Cartesian frame over V representing Jack's perspective. We have
DJ≃(NYYNNY),
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 DK be the Cartesian frame over V representing Kate's perspective,
DK≃(NYYNNY).
Then,
DJ⊗DK≃⎛⎜ ⎜ ⎜⎝NYYYYYNNNYYYNNYNYYNNNNNY⎞⎟ ⎟ ⎟⎠.
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, DJ⊗DK looks more like what we would expect Jack and Kate working together on a team to look like. However, up to biextensional equivalence, DJ and DK are the same as p∘(CJ) and p∘(CK).
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 V 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 C=(A,E,⋅) and D=(B,F,⋆) be Cartesian frames over W. C⅋ D=(hom(C∗,D),E×F,⋄), where (g,h)⋄(e,f)=g(e)⋆f=h(f)⋅e.
Claim: ⅋ is De Morgan dual to ⊗, so C⅋ D=(C∗⊗D∗)∗.
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 C and D are not large enough, we will have that C⅋ D≃0. (I am being informal with the word "large" here.)
One way that C and D can fail to be large enough is if Ensure(C∗)∩Prevent(D∗) is nonempty, which is dual to the above result about tensor being for disjoint agents. It is actually pretty difficult for C and D to be large enough. If there is any fact about the world that is determined outside of both agents, C⅋ D 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 1∗≅⊥. □
Claim: If C0≃C1 and D0≃D1, then C0⅋ D0≃C1⅋ D1.
Proof: Trivial from the fact that ⅋ is De Morgan dual to ⊗, and ≃ is preserved by −∗. □
Claim: ⅋ distributes over &, so for all Cartesian frames C0, C1, and D, we have (C0&C1)⅋ D≅(C0⅋ D)&(C1⅋ D).
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 W, C=(A,E,⋅) and D=(B,F,⋆), we let C⊸D denote the Cartesian frame C⊸D=(hom(C,D),A×F,⋄), where ⋄ is given by (g,h)⋄(a,f)=g(a)⋆f=a⋅h(f).
One way to interpret C⊸D is as "D with a C-shaped hole in it." Indeed, let us think about Agent(C⊸D). and Env(C⊸D) separately.
Agent(C⊸D)=hom(C,D) is the collection of morphisms from C to D. Morphisms from C to D are exactly interfaces through which the agent of C can interact with the environment of D. We can also think of this as the collection of interfaces that allow the agent of C to fill the role of the agent of D. This makes sense. The collection of ways that a "D with a C-shaped hole in it" can be is exactly the collection of interfaces that allow us to get a possible agent of D from a possible agent of C.
Similarly, Env(C⊸D)=A×F makes sense as the environment of a "D with a C-shaped hole in it." The environment needs to supply an environment for D, and also fill in the hole with an agent for C.
Previously, C's agent might have been part of D's agent; in C⊸D, however, this part of D gets moved into the environment.
Imagine a football team D with one team member, C, removed—the team with a football-player-shaped hole in it. Its environment, naturally, is pairs of "the kind of environment you get for a football team" and "the removed teammate".
Lollipop can be easily constructed from our other operations.
Claim: C⊸D≅C∗⅋ D≅(C⊗D∗)∗.
Proof: Trivial. □
Lollipop is well-defined up to biextensional equivalence.
Claim: If C0≃C1 and D0≃D1, then C0⊸D0≃C1⊸D1.
Proof: Trivial. □
Lollipop also has some identity-like properties.
Claim: For all Cartesian Frames C, C≅1⊸C and C∗≅C⊸⊥.
Proof: 1⊸C≅(1⊗C∗)∗≅C∗∗≅C and C⊸⊥≅(C⊗1)∗≅C∗. □
This last result is especially interesting because we can actually think of C⊸⊥ as an alternative definition for C∗.
In "Tensor is Relative to a Coarse World Model" above, we noted that two agents working together might sometimes have strictly fewer possible environments than show up in the tensor. In the next post, we will introduce the concept of a sub-tensor, which allows us to represent teams that have fewer possible environments than the tensor. Similarly, sub-sum will be sum with spurious possible environments removed.