Compositional Structures for Systems Engineering and Design

Agenda (View/Download)

speaker abstracts

Speaker: Fabrizio Genovese
Title: Compositionality and categorical thinking [TUTORIAL]
Abstract: Category theory and formal methods can be interesting for engineers, but often it is not possible to completely formalizing a problem categorically as doing it can take years and thousands of man hours. Yet, one can still apply categorical thinking: a set of heuristics that help with asking the right questions, such as What is interesting about my system?, How can I chop my system into subsystems? How do these subsystems compose? and How about the interesting stuff? How does it flow from a subsystem to another?

By using this sort of mindset the engineer can design anything in a much better and proficient way, without necessarily going hard on the mathematical formalization. I will provide a very gentle introduction to categorical thinking using examples. We will go all the way from the definition of process theory to the definition of optics. I will use almost zero formal category theory, and I will use diagrammatic reasoning as much as possible.

Speaker: David Spivak
Title: What are we tracking? How applied category theory puts thinking on rails [TUTORIAL]
Abstract: Preservation of value is of key importance in all walks of life. Whatever it is we value, and however strongly, this is what we want to obtain and preserve. It's almost definitional that when something is important and can be lost, we have a need to watch it, track it, consider it, and account for it. In order to work coherently towards a goal, either by oneself or with a team, accountability is essential: accounting is producing language about something of value and it is at the heart of coordination and collective sense-making. Mathematics, and category theory in particular, provides many excellent accounting systems, from arithmetic for finance, to Hilbert spaces for quantum mechanics.

In this talk, I will explain what I consider the main value proposition of category theory: the ability to track values as they move through different systems in such a way that the change in accounting is well-regulated as we move between different perspectives on those systems. As this talk is being considered to be a tutorial, I will attempt to guide participants through the process of doing good applied category theory, according to me. Participants will consider the merits of helping people and organizations make better sense of the world by providing custom accounting systems to track the key variables they consider valuable. Just as dollars can be added and scaled but are never multiplied together ("Did you say $5 times $3 ??"), we will see how these accounting systems put thinking on rails: they facilitate logical deductions and hence rational conversations by regulating language games and preventing costly type errors. Further, these accounting systems can often be instantiated in computers.

Speaker: Georgios Bakirtzis
Title: Categories, formal methods, learning and compositional problems in autonomy [45 mins]
Abstract: There is a rich interplay between formal methods, control theory, and learning in autonomous systems applications. Namely, formal methods guarantee particular behaviors we can encode in a mathematical language that arise from algorithms that learn from historical data to control an autonomous system. If we squint a little bit, we can see that formal methods and (some) reinforcement learning are structural in nature, e.g., it is often a direct translation from one domain (say logic) to another valid representation (say automata) and then applied to Markov decision processes. Since these methods are at the forefront of assurance, e.g., for safety and liveness conditions, and they seem compositional, it is reasonable to ask: What is the connection to the notion of categories, and, further, what can categories give rise to in this intersectional domain?

Speaker: Zinovi Diskin
Title: Multiple model synchronization with multiary delta lenses
Abstract: Complex system design necessarily deals with multiple interrelated models modelling different parts and views of the system. When one of these models changes, others should be changed accordingly to restore the intermodel consistency; this is often termed 'change propagation'. Delta lenses are a popular mathematical model of change propagation between two models, and the talk will discuss their adaptation to the multimodel case called a multiary delta lens (mx-lens). A crucial ingredient of the framework is mx-lens composition, which shows how to build a complex model synchronization mechanism from elementary components. The talk is meant to be a survey of basic ideas of change propagation and their categorical modelling with mx-lenses favoring arrows and arrow diagrams over formulas.

Speaker: Jules Hedges
Title: Emergent effects and contextual behaviours in categorical systems theory [45 mins]
Abstract:  One of the most exciting ideas in categorical systems theory is being able to give a clean definition to “emergent effects”, namely failure of a lax functor to be a functor. But there is a lack of theoretical tools to do useful things after identifying this common situation. I will present work in progress towards a “theory of contexts”, talking formally about the idea that an open system’s behaviour can depend on what other systems are nearby. By a change of perspective this allows situations with emergent effects to be seen as an ordinary functor, so that (theoretical and software) tools that assume your semantics is a functor might still be useful.

Speaker: Alan Hylton
Title:  Mathematics of the solar system internet [45 mins]
Abstract: Networked communications is about a return to scale with communicating nodes. The Internet is a powerful example of this, with an estimated 21.5 billion devices. As we try to bring a networking to space, the problem should get easier as the number of nodes decreases by many orders of magnitude. However, the assumptions that the Internet is based upon get stripped away. We will go into these in the talk, and how the generalization of problem space turns out to be vast and naturally lead us to the application of generalized tools, such as category theory, sheaf theory, and hypergraphs. An overview of our results will be provided along with our notion of the treacherous transfer function from theory to reality as we look at implementation.

Speaker: Pawel Sobocinski
Title: Electrical circuits with string diagrams
Abstract: I will outline a formal string diagrammatic approach to manipulating open electrical circuits and reasoning about them. Treating electrical circuits this way is fruitful because one obtains a formal, compositional, sound and complete equational theory for reasoning about circuits, while retaining elements of the intuitive, classical diagrammatic syntax. This is based on previous work on Affine Graphical Algebra, and is joint work with Guillaume Boisseau.

Speaker: Derek Wise
Title: Higher Knowledge Representation [45 mins]
Abstract: Rigorous knowledge representation is essential to modeling engineered systems, ensuring interoperability and extensibility, and to the design of systems with artificial intelligence capable of processing knowledge autonomously or in collaboration with humans. Using category theory for knowledge representation is appealing because of the compositional nature of human knowledge. I will describe an approach to mathematical foundations of knowledge engineering using ‘higher category theory’ to capture two dimensions of relationships: both relationships between individual entities and relationships between the ‘types’ of those entities and relationships.

Speaker: Evan Patterson 
Title: AlgebraicJulia: a compositional approach to technical computing [30 mins]
Abstract: AlgebraicJulia is a multi-institution project to realize applied category theory in the form of open source software for scientific and technical computing. The project comprises Catlab, a Julia package providing generic category-theoretic tools; Semagrams, an interactive graphical editor for combinatorial data structures; and a family of domain-specific packages that implement open dynamical systems, open Petri nets, span rewriting, and other ideas from applied category theory. This talk will survey the capabilities of the AlgebraicJulia ecosystem and its applications in scientific modeling, particularly in epidemiology and computational physics.

Speaker: Ryan Wisnesky
Title: Algebraic Databases - Lessons Learned [Demo - 30 mins]
Abstract: Algebraic methods for data specification and integration have seen a resurgence of interest as the field of applied category grows. In this talk we describe one such method of Spivak et al, based on computing Kan extensions, taking colimits, and solving lifting problems over finitely-presented co-presheaves using automated theorem provers. We also describe how this method must be generalized, for example to taking psuedo-colimits and using automated term normalizers, to be practical on real-world examples, such as integrating spreadsheets at an energy company.

Speaker: Angeline Aguinaldo
Title: A contextual affordance model for autonomous systems [20 mins]
Abstract: Context-aware autonomous systems possess the desirable ability to adjust their behavior in response to dynamic context information such as location and other percepts. The increasing availability and capability of sensors is resulting in an ever-increasing context with which an unmanned autonomous system (UAS) must reason with. As a result, more algorithms, and therefore more compute power, need to be deployed. Because of this, methods for selective contextual reasoning in UAS are critical for resource-constrained, namely low-SWaP, configurations. Most modern contextual reasoning methods are data- and pattern-driven evidenced by the predominant use of deep neural networks and reinforcement learning methods. This limits our ability to select, isolate, and simulate the effect certain context information has on the agent's ability to plan tasks and achieve goals prior to being deployed in the environment. Symbolic reasoning methods provide opportunities to use mathematical constructions to synthesize task capabilities, task plans, and important context without the need for in situ data. This talk will discuss a formal contextual affordance model which encompasses a bidirectional model transformation framework that relates formal models of context and formal models of task plans, both described using categorical semantics, for a given autonomous agent. In particular, I will present a general-purpose framework that allows you to query for what context is important given a description of an agent's capabilities.

Speaker: Pascal Le Masson
Title: Sheafification as a critical design technique for creative preservation in complex systems – principles, illustrations and first applications [20 mins]
Abstract: It is today recognized that category theory with a topos perspective provides solid foundations to model complex systems and their evolution in design processes. Category theory can account for a (C-K) design process inside a given “theory of the object”; even more, one can rely on topos theory and design theory to propose design model that account for the (counterintuitive) phenomena where design process is innovative while preserving knowledge structure and more precisely is innovative to preserve knowledge structure. At the heart of this creative preservation is sheafification, a critical process in topos theory that enables to transform every presheaf on a site (C, J) into a sheaf. In this talk we will show in depth the sheafification process, with the help of design theory. We first characterize the principles of sheafification from a design perspective, clarifying the roles of the base category C and the topology J; we propose a very simple illustration of sheafification of a presheaf on Ordinal-2 category; we finally show how sheafification can be applied to design ‘creative preservation’ in specific complex systems.

Speaker: Esteban Montero
Title: TBA [20 mins]
Abstract:  TBA

Speaker: David Perner
Title: Category Theory as a possible theoretical foundation for Systems Engineering [20 mins]
Abstract: The goal of this presentation is to show how category theory may be relevant to systems engineering and, if so, to start building the argument for why category theory should serve as a mathematical foundation for the field. In this presentation, we will review plain English descriptions of systems and systems engineering from multiple sources, showing their common elements, and how they may be expressed categorically. Finally, we show how these categorical representations may contain connections to Systems Engineering topics like verification, validation, requirements, and scenarios.

Speaker: Donald Thompson, Joshua Shinavier 
Title: Azure Knowledge Marketplace: Categories for Scale [20 mins]
Abstract:  The talk will introduce the new Azure initiative and its 3 opportunities for category theory: 1) as the core compositional engine (main part of talk), 2) managed CT services (e.g., Conexus), and 3) a catalog of hosted models for domain-specific reasoning (e.g., Chevron's cybersecurity).

Speaker: Priyaa Varshinee Srinivasan
Title: Compassionate Mathematics [20 mins]
Abstract: Our current rigid way of communicating Mathematics caters only a small proportion of the population leading to widespread (and accepted) attitudes in our society that someone is not a math person and that is relatable to be bad at Math. Compassionate Mathematics is about acknowledging the fundamental fact that there are different roads to approaching the same Mathematical truth and incorporating this awareness in our communications of Math. We see Compassionate Math as an effective solution to poor gender diversity in STEM and improving mental health of our school-goers. In this talk, we will introduce this new educational initiative which has been recently founded in collaboration with Prof. Pawel Sobocinski, Namista Tabassum and Dr. Niels Voorneveld and with support and inspiration from Brandon Baylor and Esteban Montero. We will also demo a prototype game designed to teach basic linear algebra using string diagrams. 

Speaker: Joe Moeller
Title: TBA  [20 mins]
Abstract:  TBA

Speaker: Daniel Rosiak
Title: TBA  [20 mins]
Abstract:  TBA