Temporal type theory. A topos-theoretic approach to systems and behavior (Q1791242): Difference between revisions

This book consisting of eight chapters together with two appendices presents a higher-order temporal logic for proving properties about the behavior of systems. The authors aim to explain what occurs when multiple, disctinct system components interact by using category-theoretic description of behavior types based on sheaves, demonstrating how to analyze the behaviors of elements in continuous and discrete dynamical systems so that each is to be translated and compared to one another. Chapter 2 consisting of five sections introduces the \textit{interval domain} \(\mathbb{IR}\)\ representing the line of time. The points of this space is to be thought of as compact intervals \(\left[ a,b\right] \)\ in \(\mathbb{R}\). \S 2.1 reviews sheaves on topological spaces, or more generally on posets equipped with a coverage. \S 2.2 reviews the theory of domains. \S 2.3 introduces the interval domain \(\mathbb{IR}\). \S 2.4 shows how to view the interval domain \(\mathbb{IR}\)\ in terms of the usual Euclidean upper half-plane. \S 2.5 discusses Grothendieck posites, enabling one to establish the equivalence between four different formulations of the topos of sheaves on the interval domain \(\mathbb{IR}\). That is to say, it is shown (Theorem 2.54) that the category \(\mathrm{Shv}\left( \Omega\left( \mathbb{IR}\right) \right) \)\ of sheaves on the frame of opens of \(\mathbb{IR}\) with the canonical coverage, the category \(\mathrm{Shv}\left( S_{\mathbb{IR}}^{\prime }\right) \)\ of sheaves on the interval posites \(S_{\mathbb{IR}}\), the category \(\mathrm{Shv}\left( S_{\mathbb{IR}}^{\mathbb{Q}}\right) \)\ of sheaves on the rational interval posite \(S_{\mathbb{IR}}^{\mathbb{Q}}\) and the category \(\mathrm{Cont}\left( \mathbb{IR}\right) \)\ of continuous (i.e., taking directed suprema in \(\mathbb{IR}\) to colimits in \(\boldsymbol{Set}\)) functors are all equivalent. Chapter 3 defines a topos \(\mathcal{B}\)\ of transition-invariant behavior types by defining a transition-invariant version of the interval domain \(\mathbb{IR}\)\ and a corresponding site, denoted \(\mathbb{IR}_{/\rhd}\)\ and \(S_{/\rhd}\), respectively, and letting \[ \mathcal{B}:=\mathrm{Shv}\left( S_{/\rhd}\right) \] Chapter 4, consisting of three sections, transitions from an external viewpoint to an internal one. \S 4.1 is an informal introduction to the authors' type theory and logic, as well as its relation to toposes. \S 4.2 addresses modalities, which are the internal view of what in topos theory literature are often called Lawvere-Tierney topologies. Logically speaking, modalities are internal monads on the type \(\mathsf{Prop}\) of propositions, corresponding semantically to subtoposes. \S 4.3 introduces ten Dedekind \(j\)-numeric types for an arbitary modality \(j\), namely, \(j\)-local lower and upper reals, improper and proper intervals and real numbers, as well as their unbounded counterparts: \[ \underline{\mathbb{R}}_{j},\overline{\mathbb{R}}_{j},\underline{\overline {\mathbb{R}}}_{j},\mathbb{IR}_{j},\mathbb{R}_{j},\underline{\mathbb{R}} _{j}^{\infty},\overline{\mathbb{R}}_{j}^{\infty},\underline{\overline {\mathbb{R}}}_{j}^{\infty},\mathbb{IR}_{j}^{\infty},\mathbb{R}_{j}^{\infty} \] Chapter 5 lays out the signature, for the specific topos \(\mathcal{B}\), consisting of no atomic type, one atomic term and ten axioms. The axiomatics refers only to three numetic types \[ \underline{\overline{\mathbb{R}}},\mathbb{R},\mathbb{R}^{\infty} \] which stand for \[ \underline{\overline{\mathbb{R}}}_{j},\mathbb{R}_{j}\mathbb{R}_{j}^{\infty}, \] with \(j=\mathrm{id}\). Chapter 6 establishes that the temporal type theory developed in Chapters 4 and 5 is sound in the topos \(\mathcal{B}\). Chapter 7 explores the more general \(j\)-numeric types, both type-theoretically and semantically in the topos \(\mathcal{B}\). Chapter 8 consisting of five sections is concerned with applications. \S 8.1 deals with hybrid dynamical systems. \S 8.2 addresses delays. \S 8.3 treats differential equations. \S 8.4 discusses a general framework on machines, systems and behavior contracts. \S 8.5 addresses an extremely simplified version of the National Airspace System as a toy example, establishing a safety property. Appendix A consisting of three sections addresses a notion of basis for \textit{domains}. called a \textit{predomain}. on the lines of [\textit{S. Vickers}, Theor. Comput. Sci. 114, No. 2, 201--229 (1993; Zbl 0779.06006)], where they were called \textit{information systems}. \S A.1 defines predomains, explaining how they generate domains. \S A.2 gives a notion of morphisms between predomains, called \textit{approximable mappings}, establishing that there is an equivalence between the category of predomains and approximable mappings and that of domains and Scott-continuous functions. The benefit of considering domains is that they have nice semantics, whereas the benefit of considering predomains is that they consist of much less data in general. \S A.3 discusses how the above work relates with subtoposes and modalities. Appendix B consisting of four sections is concerned with \(\mathbb{IR}_{/\rhd} \)\ as a \textit{continuous category}. \S B.1 reviews continuous categories introduced in [\textit{P. Johnstone} and \textit{A. Joyal}, J. Pure Appl. Algebra 25, 255--296 (1982; Zbl 0487.18003)]. They are a generalization of continuous posets. \S B.2 is concerned with the (connected, discrete bifibration) factorization system, assuming that the reader is familiar with the orthogonal factorization systems (final, discrete fibration) and (initial, discrete cofibration) on \(\boldsymbol{Cat}\)\ due to [\textit{R. Street} and \textit{R. F. C. Walters}, Bull. Am. Math. Soc. 79, 936--941 (1973; Zbl 0274.18001)]. \S B.3 gives a proof that \(\mathbb{IR}_{/\rhd}\)\ is a continous category by making use of the factorization system of the previous section. \S B.4 shows that the category \(\mathcal{B}\)\ is not just a category of sheaves (limit-preserving functors of a given sort) but is also a category of colimit-preserving functors of a given sort.