Temporal Type Theory | springerprofessional.de

Springer Professional

Top

2019 | Book

Read chapter Read first chapter

Temporal Type Theory

A Topos-Theoretic Approach to Systems and Behavior

Authors: Patrick Schultz, David I. Spivak

Publisher: Springer International Publishing

Book Series : Progress in Computer Science and Applied Logic (PCS)

Part of: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Login to get access

About this book

This innovative monograph explores a new mathematical formalism in higher-order temporal logic for proving properties about the behavior of systems. Developed by the authors, the goal of this novel approach is to explain what occurs when multiple, distinct system components interact by using a category-theoretic description of behavior types based on sheaves. The authors demonstrate how to analyze the behaviors of elements in continuous and discrete dynamical systems so that each can be translated and compared to one another. Their temporal logic is also flexible enough that it can serve as a framework for other logics that work with similar models.
The book begins with a discussion of behavior types, interval domains, and translation invariance, which serves as the groundwork for temporal type theory. From there, the authors lay out the logical preliminaries they need for their temporal modalities and explain the soundness of those logical semantics. These results are then applied to hybrid dynamical systems, differential equations, and labeled transition systems. A case study involving aircraft separation within the National Airspace System is provided to illustrate temporal type theory in action.
Researchers in computer science, logic, and mathematics interested in topos-theoretic and category-theory-friendly approaches to system behavior will find this monograph to be an important resource. It can also serve as a supplemental text for a specialized graduate topics course.

Advertisement

Table of Contents

Frontmatter

Chapter 1. Introduction

Abstract

In this book, we provide a new mathematical formalism for proving properties about the behavior of systems. A system is a collection of interacting components, each of which may have some internal implementation that is reflected in some external behavior. This external behavior is what other neighboring systems interact with, through a shared environment. Properties of a behavior can be established over a given duration (sometimes called frame or window) of time, and we propose a mathematical language for working with these behavioral properties.

Patrick Schultz, David I. Spivak

Chapter 2. The Interval Domain

Abstract

In this chapter, we will introduce the interval domain \(\mathbb {I\hspace {1.1pt} R}\), which is a topological space that represents the line of time in our work to come. The points of this space can be thought of as compact intervals [a, b] in \(\mathbb {R}\). The specialization order on points gives \(\mathbb {R}\) a non-trivial poset structure—in fact it is a domain—and as such it is far from Hausdorff.

Patrick Schultz, David I. Spivak

Chapter 3. Translation Invariance

Abstract

As discussed in Sect. 1.2.2, the topos \(\mathsf {Shv}(S_{\mathbb {I\hspace {1.1pt} R}})\) of sheaves on the interval domain is slightly unsatisfactory as a model of behaviors. For example, to serve as a compositional model of dynamical systems, we do not want the set of possible behaviors in some behavior type to depend on any global time. In this chapter, we define a topos \(\mathcal {B}\) of “translation-invariant behavior types” by defining a translation-invariant version of the interval domain and a corresponding site, denoted \(\mathbb {I\hspace {1.1pt} R}_{/\rhd }\) and \(S_{\mathbb {I\hspace {1.1pt} R}/\rhd }\), respectively, and letting \(\mathcal {B}\mathrel{\mathop:}= \mathsf {Shv}(S_{\mathbb {I\hspace {1.1pt} R}/\rhd })\).

Patrick Schultz, David I. Spivak

Chapter 4. Logical Preliminaries

Abstract

In this chapter, we transition from an external point of view to an internal one. In Chap. 2 we defined the interval domain \(\mathbb {I\hspace {1.1pt} R}\), and in Chap. 3 we defined a quotient \(\mathcal {B}\cong \mathsf {Shv}(S_{\mathbb {I\hspace {1.1pt} R}/\rhd })\) of its topos of sheaves. A main goal of this book is to define a temporal type theory—including one atomic predicate and ten axioms—that has semantics in \(\mathcal {B}\); we do this in Chap. 5. In the present chapter, we attempt to provide the reader with a self-contained account of the sort of type theory and logic we will be using, as well as some important concepts definable therein.

Patrick Schultz, David I. Spivak

Chapter 5. Axiomatics

Abstract

In Chap. 4, we explained a connection between toposes, type theory, and logic. We also discussed modalities and numeric types in an arbitrary topos. In the current chapter, we will lay out the signature—meaning the atomic types, atomic terms, and axioms—for our specific topos, \(\mathcal {B}\). It turns out that our signature consists of no atomic types, one atomic term, and ten axioms.

Patrick Schultz, David I. Spivak

Chapter 6. Semantics and Soundness

Abstract

In this chapter, we prove that the temporal type theory developed in Chaps. 4 and 5 is sound in the topos \(\mathcal {B}\). To do so, we begin in Sect. 6.1 by recalling the Kripke–Joyal semantics by which to interpret type-theoretic formulas in the topos \(\mathcal {B}\). Then in Sect. 6.3 we discuss the sheaf of real numbers and Time. We then proceed to our main goal: proving that our type signature—i.e., the one atomic predicate symbol and the ten axioms presented in Chap. 5—are sound in \(\mathcal {B}\). This is done in Sect. 6.5, which begins with a Table 6.2 summarizing the type signature.

Patrick Schultz, David I. Spivak

Chapter 7. Local Numeric Types and Derivatives

Abstract

In Sect. 4.3 we introduced ten Dedekind j-numeric types for an arbitrary modality j. Namely, we have the j-local lower and upper reals, improper and proper intervals, and real numbers, as well as their unbounded counterparts. They are denoted

Patrick Schultz, David I. Spivak

Chapter 8. Applications

Abstract

As mentioned in the introduction, we believe that our temporal type theory can serve as a “big tent” into which to embed many disparate formalisms for proving property of behaviors. In this chapter we discuss a few of these, including hybrid dynamical systems in Sect. 8.1, delays in Sect. 8.2, differential equations in Sect. 8.3, and labeled transition systems in Sect. 8.4.4. This last occurs in Sect. 8.4 where we briefly discuss a general framework on machines, systems, and behavior contracts. Next in Sect. 8.5 we give a toy example—an extreme simplification of the National Airspace System—and prove a safety property. The idea is to show that we really can mix continuous, discrete, and delay properties without ever leaving the temporal type theory. We conclude this chapter by discussing how some temporal logics, e.g., metric temporal logic, embeds into the temporal type theory.

Patrick Schultz, David I. Spivak

Backmatter

Title: Temporal Type Theory
Authors: Patrick Schultz
David I. Spivak
Copyright Year: 2019
Publisher: Springer International Publishing
Electronic ISBN: 978-3-030-00704-1
Print ISBN: 978-3-030-00703-4
DOI: https://doi.org/10.1007/978-3-030-00704-1

Premium Partner