7.5 A topos of behavior types

7.5 A topos of behavior types#

Now that we have discussed logic in a sheaf topos, we return to our motivating example, a topos of behavior types. We begin by discussing the topological space on which behavior types will be sheaves, a space called the interval domain.

Remark 7.75. Note that above, we were thinking very intuitively about time, e.g. when we discussed people being worried about the news. Now we will be thinking about time in a different way, but there is no need to change your answers or reconsider the intuitive thinking done above.

This section constantly references the original research in Temporal Type Theory by Spivak for more details (notice nearly the same PDF style as 7S). From that book:

Some of these temporal logics have very powerful model checkers that can produce a proof or counterexample in finite (though often exponential or doubly-exponential) time, and we make no such claim: our logic is wildly undecidable.

See also Temporal logic. For more on the paper, see Temporal Type Theory | Semantic Scholar. The paper does not seem to be actively developed; search β€œmontonic” for a typo in the introduction.

7.5.1 The interval domain#

The interval domain 𝕀ℝ is a specific topological space, which we will use to model intervals of time. In other words, we will be interested in the category \(\textbf{Shv}(𝕀ℝ)\) of sheaves on the interval domain.

To give a topological space, one must give a pair \((𝑋, \textbf{Op})\), where \(𝑋\) is a set of β€˜points’ and \(\textbf{Op}\) is a topology on \(𝑋\); see Definition 7.25. The set of points for 𝕀ℝ is that of all finite closed intervals:

\[ 𝕀ℝ ≔ \{[𝑑,𝑒] βŠ† ℝ \enspace | \enspace 𝑑 ≀ 𝑒\} \]

For \(π‘Ž < 𝑏\) in \(ℝ\), let \(π‘œ_{[π‘Ž,𝑏]}\) denote the set \(π‘œ_{[π‘Ž,𝑏]} ≔ \{[𝑑,𝑒] βŠ† 𝕀ℝ \enspace | \enspace a < 𝑑 ≀ 𝑒 < b\}\); these are called basic open sets.

For more on basic open sets, see Base (topology). From Temporal Type Theory:

Namely, for any \(r < s\), the corresponding basic open is \((r, s) ≔ \{[d, u] \enspace | \enspace r < d ≀ u < s\} βŠ† 𝕀ℝ\).

Moving back to the primary text:

The topology \(\textbf{Op}\) is determined by these basic open sets in that a subset \(π‘ˆ\) is open if it is the union of some collection of basic open sets.

Thus for example, \(π‘œ_{[0,5]}\) is an open set: it contains every \([𝑑, 𝑒]\) contained in the open interval \(\{π‘₯ ∈ ℝ \enspace | \enspace 0 < π‘₯ < 5\}\). Similarly \(π‘œ_{[4,8]}\) is an open set, but note that \(π‘œ_{[0,5]} βˆͺ π‘œ_{[4,8]} β‰  π‘œ_{[0,8]}\). Indeed, the interval \([2, 6]\) is in the right-hand side but not the left.

β˜‘οΈ Exercise 7.76#

  1. Explain why [2, 6] ∈ \(π‘œ_{[0,8]}\)

  2. Explain why [2, 6] βˆ‰ \(π‘œ_{[0,5]} βˆͺ π‘œ_{[4,8]}\)

See also Exercise 7.76.

Topos of behavior types#

Let \(\textbf{Op}\) denote the open sets of 𝕀ℝ, as described above, and let \(\textbf{BT} := \textbf{Shv}(𝕀ℝ, \textbf{Op})\) denote the topos of sheaves on this space. We call it the topos of behavior types.

There is an important subspace of 𝕀ℝ, namely the usual space of real numbers ℝ. We see ℝ as a subspace of 𝕀ℝ via the isomorphism:

\[ ℝ β‰… \{[d,u] \in 𝕀ℝ \enspace | \enspace d = u\} \]

Notice that 𝕀ℝ is defined in terms of ℝ, and now we’re trying to map ℝ to a subspace of 𝕀ℝ. The set ℝ and this subspace are not the same; the first is the original definition of ℝ and the second is an infinite set of closed intervals that are essentially points. Let’s call the first ℝ and the second \(ℝ_s\) (for ℝ as a subspace of 𝕀ℝ).

We discussed the usual topology on ℝ in Example 7.26, but we also get a topology on ℝ because it is a subset of 𝕀ℝ; i.e. we have the subspace topology as described in Exercise 7.32. These agree, as the reader can check.

β˜‘οΈ Exercise 7.77#

Show that a subset \(π‘ˆ βŠ† ℝ\) is open in the subspace topology of \(ℝ βŠ† 𝕀ℝ\) iff \(π‘ˆ ∩ ℝ\) is open in the usual topology on \(ℝ\) defined in Example 7.26.

See also Exercise 7.77.

7.5.2 Sheaves on 𝕀ℝ#

We cannot go into much depth about the sheaf topos \(\textbf{BT} = \textbf{Shv}(𝕀ℝ, \textbf{Op})\), for reasons of space; we refer the interested reader to Section 7.6. In this section we will briefly discuss what it means to be a sheaf on 𝕀ℝ, giving a few examples including that of the subobject classifier.

What is a sheaf on 𝕀ℝ?#

A sheaf \(𝑆\) on the interval domain \((𝕀ℝ, \textbf{Op})\) is a functor \(𝑆 : \textbf{Op}^{op} β†’ \textbf{Set}\): it assigns to each open set \(π‘ˆ\) a set \(𝑆(π‘ˆ)\); how should we interpret this? An element \(𝑠 ∈ 𝑆(π‘ˆ)\) is an β€œevent that takes place throughout the interval \(π‘ˆ\).” Given this \(π‘ˆ\)-event \(𝑠\) together with an open subset of \(𝑉 βŠ† π‘ˆ\), there is a \(𝑉\)-event \(𝑠|_𝑉\) that tells us what \(𝑠\) is if we regard it as an event taking place throughout \(𝑉\). If \(π‘ˆ = \bigcup_{π‘–βˆˆπΌ} π‘ˆ_𝑖\) and we can find matching \(π‘ˆ_𝑖\)-events (\(𝑠_𝑖\)) for each \(𝑖 ∈ 𝐼\), then the sheaf condition (Definition 7.35) says that they have a unique gluing, i.e. a \(π‘ˆ\)-event \(𝑠 ∈ 𝑆(π‘ˆ)\) that encompasses all of them: \(𝑠|_{π‘ˆ_i} = 𝑠_𝑖\) for each \(𝑖 ∈ 𝐼\).

We said in Section 7.5.1 that every open set π‘ˆ βŠ† 𝕀ℝ can be written as the union of basic open sets \(π‘œ_{[π‘Ž,𝑏]}\) . This implies that any sheaf 𝑆 is determined by its values \(𝑆(π‘œ_{[π‘Ž,𝑏]})\) on these basic open sets. The sheaf condition furthermore implies that these vary continuously in a certain sense, which we can express formally as:

\[ 𝑆(π‘œ_{[π‘Ž,𝑏]}) = \lim\limits_{πœ–>0} 𝑆(π‘œ_{[π‘Žβˆ’πœ–,𝑏+πœ–]}) \]

The author may have meant to write \(\lim\limits_{πœ–β†’0}\) in this last equation.

However, rather than get into the details, we describe a few sorts of sheaves that may be of interest.

βœ… Example 7.78#

For any set \(𝐴\) there is a sheaf \(\mathtt{A} ∈ \textbf{Shv}(𝕀ℝ)\) that assigns to each open set \(π‘ˆ\) the set \(\texttt{A}(π‘ˆ) := 𝐴\). This allows us to refer to integers, or real numbers, or letters of an alphabet, as though they were behaviors. What sort of behavior is \(7 ∈ β„•\)? It is the sort of behavior that never changes: it’s always seven. Thus \(\mathtt{A}\) is called the constant sheaf on \(𝐴\).

See also Constant sheaf.

βœ… Example 7.79#

Fix any topological space \((𝑋, \textbf{Op}_𝑋)\). Then there is a sheaf \(𝐹_𝑋\) of local functions from \(𝕀ℝ\) to \(𝑋\). That is, for any open set \(π‘ˆ ∈ \textbf{Op}_{𝕀ℝ}\), we assign the set \(𝐹_𝑋(π‘ˆ) := \{𝑓: π‘ˆ β†’ 𝑋 \enspace | \enspace \text{𝑓 is continuous}\}\). There is also the sheaf \(𝐺_𝑋\) of local functions on the subspace \(ℝ βŠ† 𝕀ℝ\). That is, for any open set \(π‘ˆ ∈ \textbf{Op}_{𝕀ℝ}\), we assign the set \(𝐺_𝑋(π‘ˆ) := \{ 𝑓 : π‘ˆ ∩ ℝ β†’ 𝑋 \enspace | \enspace \text{𝑓 is continuous}\}\).

See Sheaf (mathematics) for some mentions of a more general idea:

In mathematics, a sheaf (pl.: sheaves) is a tool for systematically tracking data (such as sets, abelian groups, rings) attached to the open sets of a topological space and defined locally with regard to them. For example, for each open set, the data could be the ring of continuous functions defined on that open set.

In many mathematical branches, several structures defined on a topological space \(X\) (e.g., a differentiable manifold) can be naturally localised or restricted to open subsets \(U βŠ† X\): typical examples include continuous real-valued or complex-valued functions,

Many examples of presheaves come from different classes of functions: to any \(U\), one can assign the set \(C^0(U)\) of continuous real-valued functions on \(U\). The restriction maps are then just given by restricting a continuous function on \(U\) to a smaller open subset \(V\), which again is a continuous function.

The presheaf consisting of continuous functions mentioned above is a sheaf. This assertion reduces to checking that, given continuous functions \(f_i: U_i β†’ R\) which agree on the intersections \(U_i ∩ U_j\), there is a unique continuous function \(f: U β†’ R\) whose restriction equals the \(f_i\).

β˜‘οΈ Exercise 7.80#

Let’s check that Example 7.79 makes sense. Fix any topological space \((𝑋, \textbf{Op}_𝑋)\) and any subset \(𝑅 βŠ† 𝕀ℝ\) of the interval domain. Define \(H_𝑋(π‘ˆ) := \{ 𝑓 : π‘ˆ ∩ R β†’ 𝑋 \enspace | \enspace \text{𝑓 is continuous}\}\).

  1. Is \(𝐻_𝑋\) a presheaf? If not, why not; if so, what are the restriction maps?

  2. Is \(𝐻_𝑋\) a sheaf? Why or why not?

See also Exercise 7.80.

βœ… Example 7.81#

Another source of examples comes from the world of open hybrid dynamical systems. These are machines whose behavior is a mixture of continuous movementsβ€”generally imagined as trajectories through a vector fieldβ€”and discrete jumps. These jumps are imagined as being caused by signals that spontaneously arrive. Over any interval of time, a hybrid system has certain things that it can do and certain things that it cannot. Although we will not make this precise here, there is a construction for converting any hybrid system into a sheaf on 𝕀ℝ; we will give references in Section 7.6.

We refer to sheaves on 𝕀ℝ as behavior types because almost any sort of behavior one can imagine is a behavior type. Of course, a complex behavior typeβ€”such as the way someone acts when they are in loveβ€”would be extremely hard to write down. But the idea is straightforward: for any interval of time, say a three-day interval \((𝑑, 𝑑 + 3)\), let \(𝐿(𝑑, 𝑑 + 3)\) denote the set of all possible behaviors a person who is in love could possibly do. Obviously it’s a big, unwieldy set, and no one would want to make it precise. But to the extent that one can imagine that sort of behavior as occurring through time, they could imagine the corresponding sheaf.

The subobject classifier as a sheaf on 𝕀ℝ.#

In any sheaf topos, the subobject classifier \(\Omega\) is itself a sheaf. It is responsible for the truth values in the topos. As we said in Section 7.4.1, when it comes to sheaves on a topological space \((𝑋, \textbf{Op})\), truth values are open subsets \(π‘ˆ ∈ \textbf{Op}\).

\(\textbf{BT}\) is the topos of sheaves on the space \((𝕀ℝ, \textbf{Op})\), as defined in Section 7.5.1. As always, the subobject classifier \(\Omega\) assigns to any \(π‘ˆ ∈ \textbf{Op}\) the set of open subsets of \(π‘ˆ\), so these are the truth values. But what do they mean? The idea is that every proposition, such as β€œBob likes the weather” returns an open set \(π‘ˆ\), as if to respond that Bob likes the weather β€œβ€¦throughout time period \(π‘ˆ\).” Let’s explore this just a bit more.

Suppose Bob likes the weather throughout the interval \((0, 5)\) and throughout the interval \((4, 8)\). We would probably conclude that Bob likes the weather throughout the interval (0, 8). But what about the more ominous statement β€œa single pair of eyes has remained watching position \(𝑝\).” Then just because it’s true on \((0, 5)\) and on \((4, 8)\), does not imply that it’s been true on \((0, 8)\): there may have been a change of shift, where one watcher was relieved from their post by another watcher. As another example, consider the statement β€œthe stock market did not go down by more than 10 points.” This might be true on \((0, 5)\) and true on \((4, 8)\) but not on \((0, 8)\). In order to capture the semantics of statements like theseβ€”statements that take time to evaluateβ€”we must use the space 𝕀ℝ rather than the space ℝ.

7.5.2 Safety proofs in temporal logic#

We now have at least a basic idea of what goes into a proof of safety, say for autonomous vehicles, or airplanes in the national airspace system. In fact, the underlying ideas of this chapter came out of a project between MIT, Honeywell Inc., and NASA (q.v. Abstraction, Composition and Contracts). The background for the project was that the National Airspace System consists of many different systems interacting: interactions between airplanes, each of which is an interaction between physics, humans, sensors, and actuators, each of which is an interaction between still more basic parts. The same sort of story would hold for a fleet of autonomous vehicles, as in the introduction to this chapter.

Suppose that each of the systemsβ€”at any levelβ€”is guaranteed to satisfy some property. For example, perhaps we can assume that an engine is either out of gas, has a broken fuel line, or is following the orders of a human driver or pilot. If there is a rupture in the fuel line, the sensors will alert the human within three seconds, etc. Each of the components interact with a number of different variables. In the case of airplanes, a pilot interacts with the radio, the positions of the dials, the position of the thruster, and the visual data in front of her. The componentβ€”here the pilotβ€”is guaranteed to keep these variables in some relation: β€œif I see something, I will say something” or β€œif the dials are in position \(\mathtt{bad\_pos}\), I will engage the thruster within 1 second.” We call these guarantees behavior contracts.

All of the above can be captured in the topos \(\textbf{BT}\) of behavior types. The variables are behavior types: the altimeter is a variable whose value \(πœƒ ∈ ℝ_{β‰₯0}\) is changing continuously with respect to time. The thruster is also a continuously-changing variable whose value is in the range \([0, 1]\), etc.

The guaranteed relationshipsβ€”behavior contractsβ€”are given by predicates on variables. For example, if the pilot will always engage the thruster within one second of the display dials being in position \(\mathtt{bad\_pos}\), this can be captured by a predicate \(𝑝 : \mathtt{dials} Γ— \mathtt{thrusters} β†’ \Omega\). While we have not written out a formal language for \(𝑝\), one could imagine the predicate \(𝑝(𝐷,𝑇)\) for \(𝐷: \mathtt{dials}\) and \(𝑇: \mathtt{thrusters}\) as:

\[ βˆ€(𝑑 : ℝ ). @_𝑑 \left(\mathtt{bad\_pos}(𝐷)\right) β‡’ βˆƒ(π‘Ÿ : ℝ). (0 < π‘Ÿ < 1) ∧ βˆ€(π‘Ÿ': ℝ ). 0 ≀ π‘Ÿ' ≀ 5 β‡’ @_{𝑑+π‘Ÿ+π‘Ÿ'} \left(\mathtt{engaged}(𝑇)\right) \hspace{4em} (7.82) \]

Here \(@_𝑑\) is a modality, as we discussed in Definition 7.69; in fact it turns out to be one of type 3. from Proposition 7.71, but we cannot go into that. For a proposition \(π‘ž\), the statement \(@_𝑑(π‘ž)\) says that \(π‘ž\) is true in some small enough neighborhood around \(𝑑\). So (7.82) says β€œstarting within one second of whenever the dials say that we are in a bad position, I’ll engage the thrusters for five seconds.”

Given an actual playing-out-of-events over a time period \(π‘ˆ\), i.e. actual section \(𝐷 ∈ \mathtt{dials}(π‘ˆ)\) and section \(𝑇 ∈ \mathtt{thrusters}(π‘ˆ)\), the predicate Eq. (7.82) will hold on certain parts of \(π‘ˆ\) and not others, and this is the truth value of \(𝑝\). Hopefully the pilot upholds her behavior contract at all times she is flying, in which case the truth value will be \(\mathtt{true}\) throughout that interval π‘ˆ. But if the pilot breaks her contract over certain intervals, then this fact is recorded in \(\Omega\).

The logic allows us to record axioms like that shown in Eq. (7.82) and then reason from them: e.g. if the pilot and the airplane, and at least one of the three radars upholds its contract then safe separation will be maintained. We cannot give further details here, but these matters have been worked out in detail in Temporal Type Theory; see Section 7.6.