Browsing by Author "Cockett, Robin"

Now showing 1 - 17 of 17
  • Thumbnail Image
    ItemOpen Access
    ABOUT CHARITY
    (1992-06-01) Fukushima, Tom; Cockett, Robin
    Charity is a categorical programming language based on distributive categories (in the sense of Schanuel and Lawvere) with strong datatypes (in the sense of Hagino). Distributive categories come with a term logic which can express most standard programs; and they are fundamental to computer science because they permit proof by case analysis and, when strong datatypes are introduced, proof by structural induction. Charity is functional and polymorphic in style, and is strongly normalizing. As a categorical programming language it provides a unique marriage of computer science and mathematical thought. The above aspects are particularly important for the production of verified programs as the naturality of morphisms gives us ``theorems for free'', termination proofs are not required, and mathemathical specifications can be used.
  • Thumbnail Image
    ItemOpen Access
    An Analysis of Countable Sublattices of Free Lattices
    (2016) Chan, Brian; Laflamme, Claude; Woodrow, Robert; Seyffarth, Karen; Cockett, Robin; Laflamme, Claude; Woodrow, Robert
    This thesis investigates which lattices are countable sublattices of free lattices. This is equivalent to determining which lattices are sublattices of the free lattice on three generators. Our investigation is based on the following open problem (see \cite{FL}, 1995): ``Which lattices (and in particular which countable lattices) are sublattices of a free lattice?'' We describe how stronger variants of the semidistributive laws have contributed to our current understanding of sublattices of free lattices. In particular, we see how the strongest results known only apply to certain classes of countables lattices. Afterwards, we propose a strategy for analyzing the following class of countable lattices: finite width sublattices, L, of free lattices, where L is in a semidistributive variety.
  • Thumbnail Image
    ItemOpen Access
    An investigation of some theoretical aspects of reversible computing
    (2014-11-05) Giles, Brett; Cockett, Robin
    The categorical semantics of reversible computing must be a category which combines the concepts of partiality and the ability to reverse any map in the category. Inverse categories, restriction categories in which each map is a partial isomorphism, provide exactly this structure. This thesis explores inverse categories and relates them to both quantum computing and standard non-reversible computing. The former is achieved by showing that commutative Frobenius algebras form an inverse category. The latter is by establishing the equivalence of the category of discrete inverse categories to the category of discrete Cartesian restriction categories — this is the main result of this thesis. This allows one to transfer the formulation of computability given by Turing categories onto discrete inverse categories.
  • Thumbnail Image
    ItemOpen Access
    The Category of Kirchhoff Relations
    (2022-07-19) Kalra, Amolak Ratan; Cockett, Robin; Hoyer, Peter; Scandolo, Carlo Maria
    We define the category of Kirchhoff relations to consist of those Lagrangian relations that conserve total momentum – a condition that can also be interpreted as Kirchhoff’s current law. We study and characterize different subcategories of Kirchhoff relations and present universal sets of generators of the different subcategories of Kirchhoff relations. These generators can be interpreted as junctions of ideal wires, resistances, voltage sources and current sources
  • Thumbnail Image
    ItemOpen Access
    Convex Analysis in Quantum Information
    (2017) Girard, Mark; Gour, Gilad; Sanders, Barry; Cunningham, Clifton; Cockett, Robin; Gühne, Otfried; Zinchenko, Yuriy
    Convexity arises naturally in the study of quantum information. As a result, many useful tools from convex analysis can be used to give important results regarding aspects of quantum information. This thesis builds up methods using core concepts from convex analysis, including convex optimization problems, convex roof constructions, and conic programming, to study mathematical problems related to quantum entanglement. In this thesis, I develop a method for solving convex optimization problems that arise in quantum information theory by analyzing the corresponding converse problem. That is, given an element in a convex set, I determine a family of convex functions that are minimized at this point. This method is used find explicit formulas for the relative entropy of entanglement, as well as other important quantities used to quantify entanglement, and allows one to show important relationships between them. I also construct a practical algorithm that can be used to compute these quantities. This thesis also presents a method to compute convex roofs of arbitrary entanglement measures evaluated on highly symmetric bipartite states. I also establish a framework for completely characterizing quantum resource theories that are convex. For resource theories with a simple mathematical structure, this gives rise to a complete set of resource monotones that can be computed in practice using semidefinite programs. This has applications to the study of entanglement transformations.
  • Thumbnail Image
    ItemOpen Access
    Dagger Linear Logic and Categorical Quantum Mechanics
    (2021-09) Srinivasan, Priyaa Varshinee; Cockett, Robin; Gour, Gilad; Woelfel, Philipp; Bauer, Kristine
    This thesis develops the categorical proof theory for the non-compact multiplicative dagger linear logic, and investigates its applications to Categorical Quantum Mechanics (CQM). The existing frameworks of CQM are categorical proof theories of compact dagger linear logic, and are motivated by the interpretation of quantum systems in the category of finite dimensional Hilbert spaces. This thesis describes a new non-compact framework called Mixed Unitary Categories which can accommodate infinite dimensional systems, and develops models for the framework. To this end, it builds on linearly distributive categories, and *-autonomous categories which are categorical proof theories of (non-compact) multiplicative linear logic. The proof theory of non-compact dagger linear logic is obtained from the basic setting of an LDC by adding a dagger functor satisfying appropriate coherences to give a dagger LDC. From every (isomix) dagger LDC one can extract a canonical "unitary core" which up to equivalence is the traditional CQM framework of dagger monoidal categories. This leads to the framework of Mixed Unitary Categories (MUCs): every MUC contains a (compact) unitary core which is extended by a (non-compact) isomix dagger LDC. Various models of MUCs based on Finiteness Spaces, Chu spaces, Hopf modules, etc., are developed in this thesis. This thesis also generalizes the key algebraic structures of CQM, such as observables, measurement, and complementarity, to MUC framework. Furthermore, using the MUC framework, this thesis establishes a connection between the complementary observables of quantum mechanics and the exponential modalities of linear logic.
  • Thumbnail Image
    ItemOpen Access
    Efficient Bounded Timestamping from Standard Synchronization Primitives
    (2024-04-25) Jamadi, Ali; Woelfel, Philipp; Woelfel, Philipp; Jayanti, Prasad; Cockett, Robin; Denzinger, Jorg
    Timestamping systems are at the core of many solutions to fundamental problems in distributed algorithms [2, 4, 11, 13, 15, 22, 25, 27], and are well-studied. These systems allow processes to determine the temporal ordering of events by assigning a timestamp to each event and defining an ordering on the timestamps that corresponds to the temporal order of events. Israeli and Li [19] were the first to formalize a variation of these systems, called bounded timestamping systems (BTS), wherein the domain of timestamps is finite. They established a crucial lower bound that implies any BTS implementation, where the values of the timestamps assigned to events are sufficient to determine the temporal order of events, requires Ω(𝑛) bits to represent a timestamp. Existing BTS implementations [3, 6–8, 12, 20] have Ω(𝑛) step complexity and use registers of size Ω(𝑛) bits. This thesis introduces a novel specification for a bounded times- tamping system called marker based timestamping (MBT), which has a more efficient implementation than all prior BTS implementations and is still practical. An MBT object keeps track of 𝑚 markers where each marker belongs to a process and each process has at least one marker. It provides two functionalities: mark(𝑖) operation to mark the current point in time with marker 𝑖, and isEarlier(𝑖, 𝑗) to determine the temporal order of the events marked by markers 𝑖 and 𝑗. Note that the lower bound of Israeli and Li does not apply to an MBT object. We present a linearizable, wait-free MBT implementation with constant step complexity from 𝑂(𝑚 · 𝑛) Compare-And-Swap (CAS) objects and a single bounded Fetch-And-Add (FAA) object, where each base object stores only 𝑂(log 𝑚) bits.
  • Thumbnail Image
    ItemOpen Access
    Factorization Systems for Discrete Homotopy Theory
    (2024-09-23) Hardeman Morrill, Rachel; Bauer, Kristine; Laflamme, Claude; Cockett, Robin; Cunningham, Clifton; Scull, Laura
    Homotopy theory is a well-studied field of mathematics which allows us to determine which spaces can be obtained by a deformation of another. Analogous theories have been developed for the mathematical objects called graphs. In this thesis, I further develop one of these homotopy theories for graphs, called A-homotopy theory, by constructing a covering graph theory, completing the work of my Master’s thesis. Covering graphs allow us to factor graph homomorphisms through other graphs using lifts. Factoring morphisms is an important part of finding structure on a category, and that structure is necessary for us to have a fully developed homotopy theory on the category. An example of such a structure is Hurewicz model structure on the category of spaces, which involves covering spaces. We show that there is no analogous Hurewicz model structure on the category of graphs. Instead, we define a new homotopy equivalence for graphs and a cloven weak factorization system structure on the category of graphs using path objects. This structure allows us to factor any morphism by a strong deformation retract followed by a morphism with the homotopy lifting property. This is a particularly useful factorization, which leads to a complete re-framing of A-homotopy theory.
  • Thumbnail Image
    ItemOpen Access
    Implementation of Message Passing Language
    (2018-02) Kumar, Prashant; Cockett, Robin; Zach, Richard; Wang, Mea
    Message Passage Language (MPL) is a programming language based on the work of Cockett and Pastro. MPL is a statically typed concurrent programming language with message passing as the concurrency primitive. It brings communication safety to interacting processes using a type system. MPL consists of two languages, concurrent MPL and sequential MPL, which can interact with each other. Concurrent MPL programs are written using concurrency constructs built into the language and protocols, which are concurrent data types. These concurrency constructs allow intuitive modelling of real world concurrency scenarios. Sequential MPL is a functional programming language. In addition to data definitions, sequential MPL allows codata definitions, which can model infinite structures. Sequential MPL allows for disciplined recursion using folds and unfolds in addition to normal recursion. In this thesis, we develop the first prototype of a compiler for MPL. We reformulate MPL's design to allow normal recursion in addition to primitive recursion, the only form of recursion allowed in previous designs. In light of the changes made to MPL, we describe MPL's type system. Then we develop an algorithm for type inferencing MPL programs, and implement it. In addition, we develop and implement an abstract machine to run MPL programs. We also develop the intermediate languages through which MPL programs compile to the abstract machine. We describe and implement the algorithms used in the compilation of MPL programs to the abstract machines, namely lambda lifting and compilation of pattern-matching.
  • Thumbnail Image
    ItemOpen Access
    Integral Categories and Calculus Categories
    (2017) Lemay, Jean-Simon; Bauer, Kristine; Cockett, Robin; Laflamme, Claude; Brenken, Berndt; Tasson, Christine
    Differential categories are now a well-studied abstract setting for differentiation. However not much attention has been given to the process which is inverse to differentiation: integration. This thesis presents an analogous study of integral categories. Integral categories give an abstraction of integration by axiomatizing extra structure on a symmetric monoidal categories with a coalgebra modality using the primary rules of integration. The axioms for integrations include the analogues of integration by parts rule, also called the Rota-Baxter rule, the independence of the order of iterated integrals and that integral of any constant map is linear. We expect consequences of the compatible interaction between integration and differentiation to include the two fundamental theorems of calculus. A differential category with integration which satisfies these two theorem in a suitable sense is what we call a calculus category.
  • Thumbnail Image
    ItemOpen Access
    Linear Functors and their Fixed Points
    (2012-12-14) Yeasin, Masuka; Cockett, Robin
    In concurrent programming, message passing along channels plays a key role. This is a form of communication between two processes in which messages can be sent in both directions. To ensure the coherent sequencing of receiving and sending messages the communications on such a channel are goverened by a “protocol”. In this thesis, the categorical semantics of protocols for the message passing logic (introduced by Cockett and Pastro) is introduced. A special class of protocols, built on linear functors, is investigated and it is shown that these protocols naturally form linear functors.
  • Thumbnail Image
    ItemOpen Access
    Manipulation of dynamical resources in quantum information theory
    (2023-03-14) Saxena, Gaurav; Gour, Gilad; Muller, Markus; Cockett, Robin; Feder, David; Sanders, Barry
    Quantum channels can be regarded as the most fundamental objects in quantum mechanics. With the help of quantum resource theories, it was recently recognized that dynamical quantum systems (described by quantum channels) may exhibit phenomena such as entanglement and coherence, and can be utilized as resources in various operational tasks. In this dissertation, I characterize and quantify the coherence and magic of dynamical quantum systems, formulate interconversion conditions among pairs of channels, and quantify the performance of fixed programmable processors. Quantum resource theories are governed by constraints arising from physical or practical settings. Considering the absence of coherence and efficient classical simulability (two different notions of classicality) as practical constraints towards achieving quantum advantage, I develop the resource theories of dynamical coherence and dynamical magic, respectively. In developing the resource theory of coherence, the underlying principle I follow is that the free dynamical objects are those that can neither store nor manipulate coherence. This led me to identify classical channels as free elements in this theory. The development of the resource theory of multi-qubit magic channels is motivated by the need to estimate the classical simulation cost of multi-qubit quantum circuits. The set of completely stabilizer preserving operations is the largest known set of operations in the multi-qubit scenario that can be efficiently simulated classically, and as such, they are the perfect candidates for the free channels of this resource theory. In both these resource theories, I quantify the resources using various resource measures, and solve several single-shot resource interconversion problems including different types of resource cost and distillation. I also formulate a classical simulation algorithm to estimate the expectation value of an observable and show that its runtime depends on a dynamical magic monotone. Besides developing the above resource theories, I generalize Lorenz majorization to the channel domain and use it to find the necessary and sufficient conditions for interconversion among pairs of classical channels. Furthermore, I quantify the performance of a fixed programmable quantum processor and find a trade-off relation between the success probability and the average fidelity error in simulating a target unitary using the processor.
  • Thumbnail Image
    ItemOpen Access
    Quantum Resource Theories for Thermodynamics, Reference Frames, and Uncertainty
    (2016) Narasimhachar, Varun; Gour, Gilad; Sanders, Barry; Høyer, Peter; Cockett, Robin; Jennings, David
    Quantum information science is at the interface of physics and information theory, with applications including quantum computing and communication. Within this science, a resource theory is a detailed study of a particular class of physical processes, under which the possible state transitions are restricted. Given any initial physical state, the possible final states are also restricted. Initial states with a wealth of possible final states can then be considered more valuable than less versatile initial states, leading to a notion of "resourcefulness" of states. The broad goals of a resource theory include (1) to identify, characterize, and quantify resources; (2) to find an efficient way to determine whether an arbitrary instance of resource conversion is possible; and (3) to relate practical applications to resource conversion. In this thesis, we will take the resource-theoretic approach to understanding thermodynamics. The mathematical methods used in this work will enable us to also develop resource theories for measurement uncertainty and reference frames; in fact, the resource-theoretic treatment of thermodynamics is a combination of these two. Our approach is based on a model called thermal operations, applicable on individual quantum-mechanical systems out of thermal equilibrium. We study this model in detail, resulting in a better understanding of the resource of thermal inequilibrium. In a simplified version of the model where quantum coherence is neglected, we find that the conditions for state transitions are already more complex than the classical second law of thermodynamics. We extend the model to quantum systems controlled by classical circuitry. We also extend it to incorporate quantum coherence in the low-temperature limit. Measurement uncertainty is an important element in quantum mechanics. But its current understanding is through particular measures of uncertainty, such as the variance. We apply the resource theory approach to develop a measure-independent formalism for uncertainty, even in the case where the measurement is on part of a composite system with quantum correlations. Under physical processes restricted by some symmetry (e.g. rotational symmetry), asymmetric states act as resourceful reference frames. In this resource theory, we find the rate at which large quantities of resources can be interconverted through measurements.
  • Thumbnail Image
    ItemOpen Access
    Scoping and Execution Monitoring for IoT Middleware
    (2018-01-23) Fuentes Carranza, Juan Carlos; Fong, Philip; Cockett, Robin; Safavi-Naini, Rei; Fong, Philip
    Existing Internet of Things architectures rely on middleware (cloud services) to host coordination logic among devices. This middleware is based on Event Based Systems where the Broker architecture and the Publish/Subscribe design pattern are used to deal with heterogeneous environments and for decoupling purposes, being the MQTT protocol one of the most extensively used Event Based Systems for Internet of Things Solutions. Two prominent security issues in these type middleware are: possible network interruptions between devices and the middleware, and potentially compromised devices. This thesis proposes Scoping and Execution Monitoring in Event Based Systems to cope with possible network disconnections, and to deal with misbehavior of faulty or compromised devices. I define a mathematical model for Event Based Systems where the interplay between Scoping and Execution monitoring is formalized, and empirically evaluate the performance of these security mechanisms.
  • Thumbnail Image
    ItemOpen Access
    Siblings of Binary Relations: The Case of Direct Sums of Chains, NE-Free Posets and Trees
    (2022-09) Abdi Kalow, Davoud; Laflamme, Claude; Woodrow, Robert; Bezdek, Karoly; Cockett, Robin
    Two structures are called siblings when they mutually embed in each other. This dissertation mainly discusses Thomasse's conjecture and its alternate form for some binary relations. Thomasse's conjecture states that a countable relation has either one, countably many or continuum many siblings, up to isomorphism and the alternate form says that a relation of any cardinality has one or infinitely many siblings, up to isomorphism. There is also a conjecture due to Bonato-Tardif stating that a tree has one or infinitely many siblings in the category of trees. For a tree which is not a sibling of the graph obtained by adding an isolated vertex to the tree, the Bonato-Tardif conjecture and the alternate Thomasse conjecture are equivalent. Abdi, Laflamme, Tateno, Woodrow verified the ideas of a counterexample to the Bonato-Tardif conjecture claimed by Tateno and they confirmed that the example also disproves Thomasse's conjecture. This is a major development in the program of understanding siblings of a given mathematical structure. The counterexample is not a subject of this dissertation, however, determining which structures exactly do satisfy the conjectures is of interest. Laflamme, Pouzet and Woodrow verified both Thomasse's conjecture and its alternate form for chains. Moreover, the alternate Thomasse conjecture was proved for countable cographs by Hahn, Pouzet and Woodrow. In order to tackle the conjectures towards posets, we verify both Thomasse's conjecture and its alternate version for direct sums of chains. We also show that the alternate Thomasse conjecture is true for countable NE-free posets which have strong connections to cographs. Moreover, making use of decomposition trees, we give a proof that each cograph is the comparability graph of some NE-free poset. In order to pose more restriction on trees related to the Bonato-Tardif conjecture, we give a positive answer to one of the open cases of a result due to Hamann. Tyomkyn conjectured that if a locally finite tree has a non-surjective embedding, then it has infinitely many siblings, unless the tree is a one-way infinite path. We prove that if a locally finite tree has a non-surjective embedding preserving precisely one end, then it has infinitely many siblings, unless the tree is a one-way infinite path. This establishes both conjectures of Bonato-Tardif and Tyomkyn for locally finite trees which do not have non-surjective embeddings preserving precisely two ends. Finally, we give a representation of trees obtained by a technique which is similar to the Cantor-Bendixson derivative of a topological space. This representation helps us to verify the Bonato-Tardif conjecture in some cases.
  • Thumbnail Image
    ItemOpen Access
    The Type System for the Message Passing Language MPL
    (2014-01-30) chakraborty, subashis; Cockett, Robin
    We present a formal description of the Message Passing Language (MPL) which is based on the message passing logic proposed by Cockett and Pastro with the addition of concurrent datatypes or protocols. This thesis also provides a ``proof of concept'' of the language by developing substantial examples in MPL. We also present a complete type system for MPL which underpins both the type checking and the type inference of the language.
  • Thumbnail Image
    ItemOpen Access
    Turing Categories and Realizability
    (2017) Nester, Chad; Cockett, Robin; Eberly, Wayne; Zach, Richard; Woodrow, Robert; Cockett, Robin
    We present a realizability tripos construction in which the usual partial combinatory algebra is replaced with a Turing category, and the category of partial functions on sets is replaced with a discrete cartesian closed restriction category. As an intermediate step we construct in this setting a restriction category of assemblies. Our constructions generalize existing constructions in the field.