Abstracts-Fmcs 2017

ABSTRACTS-FMCS 2017

Jerome Fortier: Restriction Lambda-Calculus
One of the most general, and therefore nicest, families of categories
where morphisms behave like partial maps is the family of restriction
categories. There is also a notion of a cartesian closed restriction
category (CCRC), analogous to the usual notion of a CCC, but in the
partial world. This work is an attempt to state and prove the
Curry-Howard property for CCRC's, by developing the corresponding
syntax. Our solution is something like simply typed lambda-calculus,
with a restriction operator. The resulting logic turns out to be
substructural, and therefore very nice!

Keith O’Neill: A Connection between Noncommutative and Commutative Codifferential Categories

Noncommutative geometry is characterized by a welter of examples of structures which are impervious to any semblance of visualization. Therefore, a mathematician embarking on the analysis of a noncommutative space is faced with a difficult dilemma: whether to aimlessly wander in a morass of pure formality or to utilize analogies to more tractable geometric structures. Whenever possible, we opt for the latter. However, the fallibility of such an approach is indicated by our inability to intuit the qualities of quantum phase space - a classic example of a noncommutative space.

A solution to this dilemma is the formalization of the analogy, a task for which category theory is quite apt. In this talk, we investigate one such for- malization which utilizes the apparatus of differential categories. Differential categories and their noncommutative variants distill the essential formal features of differential calculus to produce a compact and flexible theory. Here, we exploit this formalization to establish a tangible connection between dif- ferential structures in noncommutative contexts and those in commutative contexts.

Darien Dewolf: An Element-based Reformulation of Restriction Monads
Last year at FMCS, I introduced restriction monads: monads in a
bicategory equipped with a restriction 2-cell satisfying axioms reminiscent of
those satisfied in a restriction category. This talk will give a reformulation
of restriction monads in bicategories with an initial object. An immediate
benefit of this reformulation are one-to-one correspondences between (i) small
restriction categories and restriction monads in Span(Set) and (ii) small
restriction categories and restriction monads in Set-Mat. These
correspondences form the motivation for defining internal restriction
categories and restriction enriched categories, respectively.

TarmoUustalo: Container combinatorics: monads and lax monoidalfunctors
Abbott et al.'s containers are a "syntax" for a wide class of set
functors in terms shapes and positions. Containers whose "denotation"
carries a comonad structure can be characterized as directed
containers, or containers where a shape and a position in it determine
another shape, intuitively a subshape of the given shape rooted by the
given position. In this talk, I will discuss similar explicit
characterizations for container functors with a monad structure and
container functors with a lax monoidalfunctor structure, as well as
some variations. We argue that this type of characterizations make a
tool, e.g., for enumerating the monad structures that some set functor
admits. Such explorations are of interest, e.g., in the semantics
of effectful functional programming languages.

Rory Lucyshyn-Wright: Optimal updating of database views through functorial semantics and fibrations

Alongside basic database concepts such as tables, schemas, and queries, many database systems include `virtual' tables called views, whose content is automatically derived from the database by means of a fixed query. Views are typically read-only, since the problem of implementing updatable views entails a challenging theoretical problem that has been studied by many authors. Johnson and Rosebrugh have studied this problem by means of a category-theoretic formalism for database theory through functorial semantics. Therein, schemas are certain limit-colimit sketches and hence are presentations of theories relative to a doctrine, in the Beck-Lawvere sense, so that database states are precisely models of these theories. Concretely, such theories are (structured) categories, and their models are (structure-preserving) set-valued functors. Correspondingly, every view defines a structure-preserving functor between theories and so induces a functor between the categories of models. It is an insight of Johnson and Rosebrugh that a view is updatable, in an optimal way, if and only if the latter functor is both a fibration and an op-fibration. Spivak (2012) has also employed the paradigm of functorial semantics for databases, in a setting where the theories are mere small categories. In this talk, we observe that the problem of optimal view updating in this setting admits a natural solution: Given any functori:S --> T between small categories S and T, the induced functor [T,Set] --> [S,Set] is a Street fibration if and only if it is a Street op-fibration, if and only if i is fully faithful. Further, we apply similar methods to study the extent to which related results are available for finite limit theories as well as the algebraic databases of Schultz, Spivak, Vasilakopoulou, and Wisnesky (2017).

PolinaVinogradova: Formalizing abstract computability: Turing Categories in Coq

The concept of a recursive function has been extensively studied using traditional tools of computability theory. However, with the development of category-theoretic methods it has become possible to study recursion in a more abstract sense. The particular model this paper is structured around is known as a Turing category. The structure within a Turing category models the notion of partiality as well as recursive computation, and equips us with the tools of category theory to study these concepts. The goal of this work is to build a formal language description of this categorical model. Specifically, we use the Coq proof assistant to formulate informal definitions, propositions and proofs pertaining to Turing categories in the underlying formal language of Coq, the Calculus of Co-inductive Constructions (CIC). Furthermore, we instantiate the more general Turing category formalism with a CIC description of the category which explicitly models the language of partial recursive functions.

Geoff Cruttwell- General connections in tangent categories

Connections are a fundamental tool of differential geometry. However, there are various formulations of the connection notion; in particular, there are definitions of connections on both vector bundles and on the more general fibre bundles.

In the axiomatic abstract setting of tangent categories, previous work has shown how to define connections on differential bundles (the analog of vector bundles). In this talk, we discuss how to define connections in tangent categories in the more general sense (that is, on the analog of fibre bundles) and look at the example of connections on G-principal bundles in this setting.

Jonathan Gallagher: Coherently closed tangent categories

There are two developments of type theory which describe logic for

reasoning about smooth maps. The first is synthetic differential

geometry; here one uses the type theory of a smooth topos to reason about

microlinear spaces. The second is the differential lambda calculus; here an

explict type theory was developed for reasoning in smooth models of linear

logic(Kˆthe sequence spaces, convenient vector spaces).

It turns out that these two models are intimately related, and this

talk will give a direct link. In particular, we will show that the

the differential lambda calculus is the logic in the category of

euclidean or differential bundles over an object, in a coherent,

locallycartesian closed tangent category. This then describes a

dependently typed variant of the differential lambda calculus for these

settings. For example, this means that one can use the differential lambda

calculus to reason about the Euclidean vector bundles of SDG.

Jason Parker: Isotropy Groups of Algebraic Theories

Every first-order geometric theory T has a classifying topos C, which contains acanonical group object called its ‘isotropy group’, which we may call the isotropy group of the theory T. In this talk I will present several new results about the isotropy groups of equational algebraic theories. After reviewing the fact that the isotropy group of a geometric theory is isomorphic to the automorphism group of its universal model, I will explain how we can use this characterization to obtain an even more concrete description of the isotropy group of an equational algebraic theory. I will then illustrate how to compute the isotropy groups of several popular algebraic theories, including the theories of (commutative) monoids, (abelian) groups, and commutative rings. Finally, I’ll touch upon some current results and future questions about how to compute the isotropy groups of algebraic theories that have been constructed by means of operations on theories (e.g. disjoint union and tensor product).

DorettePronk: What are orbifolds?
An orbifold, also called a V-manifold, was originally defined by Satake as a paracompactHausdorff space with an atlas of charts consisting of open subsets of Euclidean space with an action of a finite group and a homeomorphism from the orbit space to an open subset of the underlying space. Two atlases were considered equivalent of they had a common refinement. The problem with this definition was that it was far from obvious what the definition of a map between orbifolds should be. This was partially resolved when a new representation in terms of proper etalegroupoids was introduced, with bothgroupoidhomomorphisms and Hilsum-Skandalis bimodules, or equivalently, generalized maps, as maps.

Describing these maps in terms of atlases has resulted in rather technical descriptions that are not easy to work with. For differential geometers who are interested in the local structure of maps like embeddings and immersions, this has proven to be very challenging. Furthermore, with the change to not necessarily effective group actions, there is added confusion about what atlases should be.
I will introduce a new notion of atlas for orbifolds which are the objects of a pseudo double category with horizontal maps given in terms of profunctors and vertical maps in terms of functors. We will show that this pseudo double category is weakly equivalent to the pseudo double category of orbigroupoids with Hilsum Skandalis maps as horizontal maps and groupoidhomomorphisms as vertical maps.
If there is time I will add some examples of notions of suborbifolds and how they can be expressed in this formalism. This is joint work with my student, AlanodSibih.

PriyaaSrinivasan: Categorical description of completely positive maps

In my talk, I would be presenting categorical descriptions of completely positive maps indagger compact closed categories and dagger symmetric monoidal categories. Completely positive maps have applications in physics, for example, they are used to model quantum channels. Completely positive maps between endomorphism monoids were first categorically represented by Selinger. Later, Coeckeet. al. described completely positive maps between any normalizableFrobenius Algebras in a dagger compact closed category. In my talk, I will present completely positive maps between normalizableFrobenius algebras in dagger symmetric monoidal categories. The material I present is adapted from the work of Vicary and Heunen. In my talk, I will also present CP construction on dagger symmetric monoidal categories.

Cole Comfort: The Category CNOT

We exhibit a complete set of identities by CNOT, the symmetric monoidal category generated by the controlled-not gate, the swap gate, and the computational ancillae. We prove that CNOT is a discrete inverse category. Moreover, we prove that CNOT is equivalent to the category of partial isomorphisms of finitely-generated non-empty commutative torsors of characteristic 2. This is equivalently the category of affine partial isomorphisms between $\mathbb{Z}_2$ vector spaces.

Francisco Rios-A categorical model for a quantum circuit description language

Quipper is a practical programming language for describing families of quantum circuits. In this talk, we formalize a small, but useful fragment of Quipper called Proto-Quipper-M. Unlike its parent Quipper, this language is type-safe and has a formal denotational and operational semantics. Proto-Quipper-M is also more general than Quipper, in that it can describe families of morphisms in any symmetric monoidal category, of which quantum circuits are but one example. We design Proto-Quipper-M from the ground up, by first giving a general categorical model of parameters and states. After finding some interesting categorical structures in the model, we then define the programming language to fit the model. We cement the connection between the language and the model by proving type safety, soundness, and adequacy properties. This is joint work with Peter Selinger.

Zamdzhiev-A DCPO-enriched linear/non-linear model

Rios and Selinger have recently proposed a categorical model for the quantum programming lan- guageProto-Quipper-M, which is an important fragment of the Quipper language. In this work, we describe an extension to their categorical model with the additional property that it is DCPO- enriched, bringing us closer to modeling general recursion in the language. Similar to their model, our model exhibits a symmetric monoidal adjunction between a cartesian closed category and a sym- metric monoidal closed category that previously has been shown to be a sound categorical model for a mixed linear/non-linear (and not necessarily quantum) programming language by Benton. Our model is built upon a generalisation of the well-known families construction on categories, which retains some crucial properties from the theory of fibrations which allows us to prove our model is complete and cocomplete.

Prashant Kumar: Introduction to MPL Programming Language

MPL(Message Passing Language) is a concurrent, functional and strictly typed language with message passing as the concurrency primitive. Concurrent MPL programs comprise of processes with channels connecting them. Processes communicate by passing messages along the channels. MPL brings the convenience of type safety to the concurrent world by typing the channels. This is achieved by associating every channel with a protocol/coprotocol which deteremines permissible actions on a channel. Protocol/Coprotocol can be considered as the data types of the councurrent world. MPL also has a sequential side which resembles a strictly typed functional programming language like Haskell along with the additional facilities of defining and using codata types and writing disciplined recursive programs using folds and unfolds.

In the talk, the basic constructs used to develop councurrent programs in MPL will be described with examples that will be run on the MPL’s compiler.

Leila Leganeh:Pullback complements in partial morphism categories

In my thesis I investigate pullback complements in partial morphism categories. I characterize the existence of pullback comple- ments in a category in terms of the existence of exponentials in an associated slice category. The existence of pullback complements in partial morphism categories can be characterized in terms of the ex- istence of pullback complements in the base category. Finally, for an admissible match I compare partial pullback complement rewriting and sesqui-pushout, double- pushout and single pushout rewritings.

Ben Macadam: Storage tangent categories

In classical differential geometry, a vector bundle associates each point of a manifold to a vector space. This structure was first explored in tangent categories as differential bundles by Robin Cockett and Geoff Cruttwell. In this talk, we consider the linear-logical structure of the category of vector bundles and how this relates to classical constructions in differential geometry, such as differential forms and their exterior algebra.

Bob Rosebrugh-Universal updates for symmetric lenses

A "symmetric lens" between two model domains has state synchronization data and resynchronization operations while an "asymmetric lens" provides a strategy to lift updates in a model domain along a morphism of model domains. When the model domains are categories we call them delta-lenses (or d-lenses). We showed that (certain equivalence classes of) spans of asymmetric d-lenses represent symmetric d-lenses. The c-lenses are a special case of asymmetric d-lenses whose update lifting satisfies a universal property that makes them "least change". If we define (equivalence classes of) spans of c-lenses to be symmetric c-lenses, then we naturally hope that they characterize the symmetric d-lenses satisfying a "least change" universal property. However, we'll explain why we do not expect this. Instead we consider cospans of c-lenses and show that they do generate symmetric d-lenses with a universal property. We also explore how to characterize those symmetric d-lenses that arise from cospans of c-lenses.