David Jaz Maiers - Compositionality via 2-algebra

If I do a Google search for 2-Algebra then it says "Algebra 2 is the second math course typically taken in high school, building directly on the foundations of Algebra 1. It expands on linear equations, quadratics, and graphing, while introducing more advanced concepts like polynomial, exponential, logarithmic, and trigonometric functions." See (infinity,n)-module in nlab. 

From the video description:

Abstract: A complex system may be designed modularly by putting together interacting component subsystems. Since analyses of complex systems can often scale very poorly with their size, it pays to use the modular structure of such systems to divide the task of analysis across the component subsystems.

Many analyses of systems may be encoded as homomorphism search problems between systems of the same sort. This suggests attending to categories of systems and their homomorphisms. In this talk, we'll consider the modular structure of a class of systems as a 2-algebra — an algebraic structure on categories of systems (and their interfaces and interaction patterns). We'll see compositionality theorems as (lax) homomorphisms of these 2-algebraic structures, and survey a number of techniques for proving them using 2-categorical algebra.

Seems like a lot to learn just to understand how to compose interpreters for a modular language, but it doesn't seem so bad when you think about the problem. Imagine you have a domain-specific language for some class of structures which includes a field of some kind, then you would like to use a standard module to implement the various operators, according to the types of object to which they're being applied. So now imagine that you have some sort of type classes or parametric polymorphism and you want a modular structure that defines all the concrete syntax as well as the mapping to the semantic representation of the abstract elements such as the operators and operands. So you are trying to design a domain-specific language where the domain is the set of language interpreters that can be composed from modules of this sort. To give a motivating example, you may want a language for defining elements in a Hilbert-Schmidt operator space, and applying them to various Hilbert spaces, both finite and infinite-dimensional. So you would want your system to be able to compose these different modules together: take two different instantiations of the field module to define a real and complex field, then maybe you would want to be able to compose these with an inner product space module to define both a complex and a real-valued Hilbert space for some reason. Such a language could be instantiated in a theorem prover so that it could be used to produce proofs, or it could be instantiated in a program to do numerical simulations, or perhaps both to prove properties of numerical solutions in some model. (13:35). 

The question is then "What sort of properties do you want modules specified in this way to have?" And you might think that it would be a good start if they at least were capable of being composed into the objects of this domain of composable language interpreters. So you would be defining an initial layer of a tower of such domains. (22:11). Perhaps this initial layer would need to be capable of expressing type theories, then models of those theories,... I don't know: see Formalising Foundations in Dependent Type Theories. 

7:49 Those first three lines seem quite closely related. I had never even heard the terms Continuous-time stochastic process or Infinitesimal generator until now. 

I like the order in which he presents these three classes of system. It suggests a kind of duality between automata and stochastic processes with continuous differential equations in the middle. These high-level patterns are sometimes significant because they can be formalised very efficiently. See adjoint modality in nlab, also Assumptions of Physics - From Classical Mechanics to Field Theory and William Lawvere on the Dialectic of the Continuous and Discrete in About Logic Interview with Urs Schreiber. 

10:00 Process of taking representations and solving them. Sheaves as time or context-dependent relations. 

23:22 On the difficulty of explaining these things: like how to even parse the sentence "Your examples need examples need examples" let alone interpret it! 

38:19 Topos Institute develop software for scientific collaboration: see CatColab. But that software is presented as a collection of five logics, not as a single sorted system. Maybe the top bit is not for public consumption? But see 1:03:33.

Subscribe to Topos Institute. 

See John Baez on Cospans of Finite Sets also Brendan Fong and David Spivak - Seven Sketches in Compositionality: An Invitation to Applied Category Theory, and John Baez on Symmetric Monoidal Categories A Rosetta Stone and Noson S. Yanofsky on Diagonalization, Fixed Points, and Self-reference. 

I think it's time to start a new essay, entitled Real Greek Λέγω. See Global Virtual Four Season School in The Foundations of Mathematics and Physics.

See Compiler Coffee Club - Interning Cyclic Types in a Compiler and System Fω And ML Module Semantics: 

Joined up! See 1:00:33 in David's talk:

... a few moments later,... 

See my comment:

10:19 Is the difference between a static structure and a time-varying process in some sense a question of locality or context-dependence of description? I am wondering about a possible duality between, say transition systems and stochastic processes on the one hand and Markov kernels and traces on the other.