Réunion d'hiver SMC 2015
Université McGill, 4 - 7 décembre 2015
- JOHN BAEZ, U. C. Riverside
Categories in Control [PDF]
-
Control theory is the branch of engineering that studies dynamical systems with inputs and outputs, and seeks to stabilize these using feedback. Control theory uses 'signal-flow diagrams' to describe processes where real-valued functions of time are added, multiplied by scalars, differentiated and integrated, duplicated and deleted. In fact, these are string diagrams for the symmetric monoidal category of finite-dimensional vector spaces and the monoidal structure is direct sum. Jason Erbele and I found a presentation for this symmetric monoidal category, which amounts to saying that it is the PROP for bicommutative bimonoids with some extra structure.
A broader class of signal-flow diagrams also includes extra morphisms to model feedback. This amounts to working with the symmetric monoidal category where objects are finite-dimensional vector spaces and the morphisms are linear relations. Erbele also found a presentation for this larger symmetric monoidal category. It is the PROP for a remarkable thing: roughly speaking, an object with two commutative Frobenius algebra structures, such that the multiplication and unit of either one and the comultiplication and counit of the other fit together to form a bimonoid.
In electrical engineering we also need a category where a morphism is a circuit made of resistors, inductors and capacitors. Brendan Fong and I proved there is a functor mapping any such circuit to the relation it imposes between currents and potentials at the inputs and outputs. This functor goes from the category of circuits to the category of finite-dimensional vector spaces and linear relations.
- MARC BAGNOL, University of Ottawa
Proofnets and the Complexity of Proof Equivalence [PDF]
-
Also known as the word problem in category theory, the equivalence problem of a logic asks whether two proofs are related by a set of rule permutation that reflect the commutative conversions of the logic. On the other hand, proofnets for a logic can be broadly defined as combinatorial objects offering canonical representatives for equivalence classes of proofs, enjoying good computational properties.
A notion of proofnet for a logic therefore induces a way to solve the equivalence problem of this logic. This has been used recently to show that the multiplicative fragment (with units) of linear logic cannot have a low-complexity notion of proofnets, by proving that the equivalence problem for this fragment is PSpace-complete.
We will look into the situation for another small fragment of linear logic: the multiplicative-additive (without units) fragment, which intuitionistic part can be seen as a very basic linear $\lambda$-calculus with co-products.
- RICHARD BLUTE, University of Ottawa
Towards a Theory of Integral Linear Logic via Rota-Baxter algebras [PDF]
-
Differential linear logic, as introduced by Ehrhard and Regnier, extends linear logic with an inference rule which is a
syntactic version of differentiation. The corresponding categorical structures, called differential categories, were
introduced by Blute, Cockett and Seely. Differential categories are monoidal categories equipped with a comonad
which endows objects in its image with a cocommutative coalgebra structure. There is also a natural transformation,
called the deriving transform, which models the differential inference rule. The large number of examples of differential categories demonstrate the utility of the idea. These include the convenient vector spaces of Frohlicher and Kriegl.
It is an ongoing project to develop similar notions of integral linear logic and integral categories. An appropriate place to draw inspiration for this is the theory of Rota-Baxter algebras. Rota-Baxter algebras are associative algebras with an endomorphism which satisfies an abstraction of the integration by parts formula. There are many examples of such algebras and multi-object versions of these examples should provide important examples of models of integral linear logic.
- ANDREW CAVE, McGill
Linear temporal logic proofs as reactive programs [PDF]
-
In this talk I describe a constructive variant of linear temporal logic, and describe its interpretation as a reactive programming language via the propositions-as-types correspondence. The upshot is that the type discipline enforces causality and liveness properties of its programs. I will also discuss a variant system which realizes a version of the Gödel-Löb principle.
- FLORENCE CLERC, McGill
Presenting a Category Modulo a Rewriting System [PDF]
-
Presentations of categories is a useful tool to describe categories by the means of generators for objects and morphisms and relations on morphisms. However problems arise when trying to generalize this construction when objects are considered modulo an equivalence. Three different constructions can be used to describe such generalization : localization, quotient and considering only normal forms with respect to a certain rewriting system.
I will present some work done in collaboration with S.Mimram and P.L.Curien. We assume two kinds of hypotheses, namely convergence and cylinder property (which is some higher-dimensional convergence). Under these assumptions, we prove that there is an equivalence of categories between the quotient and the localization, and an isomorphism of categories between the quotient and the category of normal forms.
- ROBIN COCKETT, University of Calgary
The Basics of Integral Categories [PDF]
-
Differential categories of both tensor and Cartesian stripes have been around for quite a while: what do the corresponding structures for integral categories look like?
The talk will describe integral categories and their relationship to differential categories. It will also describe the more general notion of an anti-derivative (due to Ehrhard), how these arise in this context, and how they produce integration. Some models of integral categories will be described. If time permits, the Cartesian version of these notions will be discussed.
- JOSEE DESHARNAIS, Université Laval
Almost Sure Bisimulation in Labelled Markov Processes [PDF]
-
In this talk we propose a notion of bisimulation for labelled Markov processes parameterised by negligible sets (LMPns). The point is to allow us to say things like two LMPs are “almost surely” bisimilar when they are bisimilar everywhere except on a negligible set. Usually negligible sets are sets of measure 0, but we work with abstract ideals of negligible sets and so do not introduce an ad-hoc measure.
The construction is given in two steps. First a refined version of the category of measurable spaces is set up, where objects incorporate ideals of negligible subsets, and arrows are identified when they induce the same homomorphisms from their target to their source $\sigma$-algebras up to negligible sets. Epis are characterised as arrows reflecting negligible subsets. Second, LMPns are obtained as coalgebras of a refined version of Giry’s probabilistic monad. This gives us the machinery to remove certain counterintuitive examples where systems were bisimilar except for a negligible set. Our new notion of bisimilarity is then defined using cospans of epis in the associated category of coalgebras, and is found to coincide with a suitable logical equivalence given by the LMP modal logic. This notion of bisimulation is given in full generality - not restricted to analytic spaces. The original theory is recovered by taking the empty set to be the only negligible set.
- NORM FERNS, York University
Bisimulation Through Markov Decision Process Coupling [PDF]
-
Markov decision processes (MDPs) are a popular mathematical model for sequential decision-making under uncertainty. Many standard solution methods are based on computing or learning the optimal value function, which reflects the expected return one can achieve in each state by choosing actions according to an optimal policy. In order to deal with large state spaces, one often turns to approximation.
Bisimulation metrics have been used to establish approximation bounds for state aggregation and other forms of value function approximation in MDPs. In this talk, we show that a bisimulation metric defined on the state space of an MDP in previous work can be viewed as the optimal value function of an optimal coupling of two copies of the original model, and discuss the consequences thereof.
This is joint work with Doina Precup.
- JÉRÔME FORTIER, Université d'Ottawa
Circular Proofs [PDF]
-
Self-referential objects such as natural numbers, infinite words, languages accepted by abstract machines, finite and infinite trees and so on, live in the world of $\mu$-bicomplete categories, where they arise from the following operations: finite products and coproducts, initial algebras (induction) and final coalgebras (coinduction). Circular proofs were introduced by Santocanale in order to provide a logical syntax for defining morphisms between such objects. We have indeed shown full completeness of circular proofs with respect to free $\mu$-bicomplete categories. The main practical advantage of having such a syntax is that it provides a general evaluation algorithm, via a cut-elimination procedure. We can then see circular proofs as a new kind of abstract machine, for which we will explore some computability-related questions.
- PIETER HOFSTRA, University of Ottawa
Monads and Isotropy [PDF]
-
In joint work with Funk and Steinberg (``Isotropy and Crossed Toposes", TAC, 2012), a new algebraic invariant of Grothendieck toposes was introduced: just as every topos contains a canonical locale (its subobject classifier), it also contains a canonical group, called its \emph{isotropy group}. In this talk, I will survey some of the recent developments concerning isotropy groups of toposes and of small categories, and in particular explain how this gives rise to some new monads on the category of small categories, one of which can be viewed as encoding formal conjugation in a category.
- ANDRÉ JOYAL, UQAM
Simplicial tribes for homotopy type theory [PDF]
-
A tribe is a categorical model of homotopy type theory.
We would like to show that the category of tribes has the structure of a fibration category,
but path objects are missing.
To correct this, we introduce the notion of simplicial tribes.
- BRIGITTE PIENTKA, McGill University
Mechanizing Meta-Theory in Beluga [PDF]
-
Mechanizing formal systems, given via axioms and inference rules,
together with proofs about them plays an important role in
establishing trust in formal developments. In this talk, I will
survey the proof environment Beluga. To specify formal systems and
represent derivations within them, Beluga provides a sophisticated
infrastructure based on the logical framework LF; to reason about formal
systems, Beluga provides a dependently typed functional language for
implementing inductive proofs about derivation trees as recursive functions
following the Curry-Howard isomorphism. Key to this approach is the ability to
model derivation trees that depend on a context of assumptions using a
generalization of the logical framework LF, i.e. contextual LF which supports
first-class contexts and simultaneous substitutions.
Our experience has demonstrated that Beluga enables direct and compact mechanizations of the meta-theory of formal systems, in particular programming languages and logics. To demonstrate Beluga's strength in this talk, we develop a weak normalization proof using logical relations.
- PHIL SCOTT, University of Ottawa
AF Inverse Monoids and the Coordinatization of MV-algebras [PDF]
-
MV-algebras are the algebras associated to many-valued logics, analogous to the way that Boolean algebras are associated to classical propositional logics. In the mid-1980's, D. Mundici established an equivalence between the category of MV-algebras and the category of $\ell$-groups (with archimedean order unit). This restricts to a correspondence between countable MV-algebras and AF C*-algebras with lattice-ordered $K_0$ group. We introduce a class of AF inverse Boolean
monoids and prove a coordinatization theorem (in the spirit of von Neumann's Continuous Geometry). This theorem states that every countable MV-algebra can be coordinatized (i.e. is isomorphic to the
lattice of principal ideals of some AF Boolean inverse monoid). Techniques involve use of Bratteli diagrams and colimits of semisimple inverse monoids. We shall illustrate this in the case of certain
specific AF C*-algebras (e.g. the CAR algebra of a Fermi gas). If time permits, we will mention related work, e.g. relations with Effect Algebras (B. Jacobs) and a general coordinatization theorem in recent work of F. Wehrung. [Joint work with Mark Lawson (Heriot-Watt)]
- ROBERT SEELY, McGill University \& John Abbott College
Two categorical approaches to differentiation [PDF]
-
In the past decade, we (coauthors Rick Blute, Robin Cockett and I) have formulated two different abstract categorical approaches to differential calculus, based on the structure of linear logic (an idea of Ehrhard and Regnier). The basic idea has two types of maps (``analytic'' or ``smooth'', and ``linear''), a comonad $S$ (a ``coalgebra modality''), somewhat like the {\bf!} of linear logic, and a differentiation operator. In our first approach ({\bf monoidal differential categories}), the coKleisli category (the category of cofree coalgebras) of $S$ consists of smooth maps, and differentiation operates on coKleisli maps to smoothly produce linear maps. Our second approach ({\bf Cartesian differential categories}) reversed this orientation, directly characterizing the smooth maps and situating the linear maps as a subcategory. If $S$ is a ``storage modality'', meaning essentially that the ``exponential isomorphisms'' from linear logic ($S(X\times Y)\simeq S(X)\otimes S(Y)$ and $S(1)\simeq S(\top)$) hold, we get a tight connection between these approaches in the Cartesian (monoidal) closed cases: the linear maps of a Cartesian closed differential storage category form a monoidal closed differential storage category, and the coKleisli category of a monoidal closed differential storage category is a Cartesian closed differential storage category. Two technical aides in proving these results are the development of a graphical calculus as well as a term calculus for the maps of these categories. With the term calculus, one can construct arguments using a language similar to that of ordinary undergraduate calculus.
- PETER SELINGER, Dalhousie University
Number-theoretic methods in quantum computing [PDF]
-
An important problem in quantum computation is the so-called
approximate synthesis problem: to find a circuit, preferably as short
as possible, that approximates a given unitary operator up to given
epsilon. For nearly two decades, the standard solution to this problem
was the Solovay-Kitaev algorithm, which is based on geometric
ideas. This algorithm produces circuits of size $O(\log^c(1/\epsilon))$,
where $c$ is approximately 3.97. It was a long-standing open problem
whether this exponent $c$ could be reduced to 1.
In this talk, I will report on a new class of number-theoretic algorithms that achieve circuit size $O(\log(1/\epsilon))$, thereby answering the above question positively. In certain important cases, such as the commonly used Clifford+$T$ gate set, one can even find algorithms that are optimal in an absolute sense: the algorithm finds the shortest circuit whatsoever for the given problem instance. This is joint work with Neil J. Ross.
- DAVID THIBODEAU, McGill University
Programming Infinite Structures Using Copatterns [PDF]
-
Infinite structures are an integral part of computer science as
they serve to represent concepts such as constantly running
devices and processes or data communication streams. Due to their
importance, it is crucial for programming languages to be equipped
with adequate means to encode and reason about them.
This talk investigates the recent idea of copatterns, a device to
represent corecursive datatypes, and thus infinite structures,
dually to the usual definitions of recursive datatypes which
encode finite data. While the latter defines and analyzes data
via constructors and pattern matching, respectively, copatterns
bring to type theory a definition of corecursion using observations
and copattern matching.
- FRANK VAN BREUGEL, York University
Behavioural Distances and Simple Stochastic Games [PDF]
-
Behavioural pseudometrics map each pair of states of a model to
a number in the unit interval. The smaller that number, the more
alike the states behave. By identifying states that are close to
each other, we obtain a smaller model that is easier to analyze.
Several algorithms to compute behavioural pseudometrics have been developed. In this talk, we focus on the algorithm proposed by Bacci, Bacci, Larsen and Mardare in 2013. We show that the algorithm can be viewed as a strategy improvement algorithm of a simple stochastic game. As a consequence, the correctness of the algorithm follows from the fact that strategy improvement leads to an optimal strategy for simple stochastic games.
This is joint work with Norm Ferns and Qiyi Tang.
