Luigi Santocanale
(Department of Computer Science, University of Calgary)
Parity Games: How to Play with Induction and Coinduction
ABSTRACT: I'll begin from automata theory: I'll recall theorems by Büchi and Rabin relating sets of (infinite) objects definable by means of Monadic Second Order Logic and sets of (infinite) objects recognized by automata. I'll point out that one can find automata in normal form: these are characterized by the parity acceptance condition. I'll explain the close relationship of these automata with parity games.
I'll show then how to associate to each parity game an algebraic expression, based on the categorical notions of products coproducts, initial algebras and final coalgebras (the last two are categorical formulations of induction and coinduction). I'll show that parity games can be considered as terms of a categorical theory, which turn out to be equivalent to categorical $\mu$-terms defining the property of a category of being $\mu$-bicomplete.
The category of sets and functions is $\mu$-bicomplete and when a parity game is algebraically interpreted in this category what we obtain is the set of deterministic winning strategies for a chosen player in this game.
Richard Zach
(Department of Philosophy, University of Calgary)
Intuitionistic Propositional Logic and S4 with Quantification over Propositions
In Kripke semantics for propositional intuitionistic and modal logic, a proposition can be identified with the set of worlds in which a propositional variable or a sentence is true. We accordingly obtain propositionally quantified intuitionistic or modal logics by adding quantifiers which range over subsets of the possible worlds. In general, this seemingly innocuous extension actually results in a significant increase in complexity of the resulting logics. For instance, Kremer has shown that both quantified propositional intuitionistic logic and S4 are recursively isomorphic to full-second order logic (and hence far from decidable), Antonelli established a similar result for bimodal S5. We show that quantified propositional logic and S4 remain decidable if the Kripke frames are restricted to trees.
Peter Zvengrowski
(Department of Mathematics, University of Calgary)
Categorical Properties of Compactly Generated Spaces I&II
ABSTRACT:
As the part of topology known as homotopy theory grew rapidly in the 1950s, the need for a "convenient" category of topological spaces which could be used to carry out the operations of homotopy theory (especially taking function spaces) became clear. In the period 1959-1964 several quite different solutions were proposed, notably by Milnor, Michael, and Spanier. However, a very influential paper by Steenrod in 1967 discusses the category of compactly generated Hausdorff spaces (which was by no means new) and shows that this category is indeed convenient (in a sense made precise by Steenrod). Since that time the textbooks on the subject have all adopted his approach and used this category.
In this talk, which will cover $n$ lectures ($1\leq n\leq 2$), the basic ideas of homotopy theory leading to these problems will first be discussed. Then the necessary topology to understand the compactly generated spaces will be developed, and some of the nice categorical properties such as regular, cartesian closed for this category. A couple of new results showing that certain very common function spaces of homotopy theory are indeed compactly generated will be given. A good exposition of all of this material and much more is in the M. Sc. thesis of my student A. Odunuga.
Dana Harrington
(Department of Computer Science, Calgary University)
Models of Uniqueness Logic
ABSTRACT: Uniqueness types capture the `single use' property for values. They enable many optimizations in programming languages, in particular unique types permit in-place updates of `unique' values. Uniqueness categories supply the proof theory for the logic of uniqueness types. We will review the definition of uniqueness categories and examine several models.
Luigi Santocanale
(Department of Computer Science, University of Calgary)
Fixed Point Logics and Circular Proofs
ABSTRACT: Fixed point logics and $\mu$-calculi are obtained from previously existing logical or algebraic frameworks by the addition of least and greatest fixed point operators. The propositional modal $\mu$-calculus or modal $\mu$-logic, useful for model checking, arises from modal logic exactly in this way.
A proposition-term in a $\mu$-calculus has a circular structure: it is possible to travel along subformulas and come back to the starting point using regenerations of fixed point. The circularity is inherited by proof-terms. Normally cut-free proofs in sequent calculi are finite because premiss sequents are always strictly smaller than conclusions. However, in settings where the propositions themselves can be circular, there exists the possibility of having circular or infinite proofs as well. Remarkably, in the theories of fixed points, these kind of proofs happen to be the most useful. Thus, the mathematics suggests that we are indeed allowed to make circular reasonings.
In this talk I'll explain this apparent paradox, using the concept of initial algebra of a functor. I'll point out the sense for which initial algebras of functors are a generalization of least fixed points and the relationship to inductively constructed sets (such as lists, finite tress, etc.).
I will interpret circular proofs as sort of functions (more precisely, arrows of a category) having as domain an inductively constructed set. Recall that recursively defined functions are uniquely determined by their defining system of equations. Similarly it is possible to transform a circular proof in a system of equations and then prove that this system admit a unique solution.
John Aldwinkle
(Department of Computer Science, University of Calgary)
Modal Logic for Model Checking
ABSTRACT:
King Henry the Fourth
Act III. Scene I.
Glendower I can call spirits from the vasty deep.
Hotspur Why, so can I, or so can any man;
But will they come when
you do call for them?
Glendower: I can write multi-threaded protocols.
Hotspur: Why, so can I, or so can any man;
But will
they work when you run them?
(apologies to Shakespeare)
Building concurrent systems, such as CPU's or other VLSI devices or writing computer communications protocols is fraught with peril; people are not good at recognising the implications of their designs.
Modal Logic is a language for reasoning about these systems, and Model Checkers perform this sort of reasoning automatically. For this reason, Model checking has become widely used by VLSI designers. The modal Mu logic underlies many of these model checkers.
This logic is the familiar modal logic K, augmented with fixed points.
I will give a tutorial level talk about the modal Mu logic and give some examples of how it can be used to check some VLSI devices.
John Aldwinckle
Richard J. Wood
(Department of Mathematics, Dalhousie University)
Tensor Products of Sup-lattices
ABSTRACT: We provide an alternate explicit description of the tensor product, M*N, of sup-lattices which facilitates discussion of sup-enriched categories and suggests generalization to total categories.
John Aldwinkle
(Department of Computer Science, Calgary University)
A Lightning Fast Introduction to Partial Orders, Lattices and Fixed Points
ABSTRACT: This talk is aimed at first year grad students. It consists
mainly of definitions and examples with a few simple theorems. Definitions
include, preorder, partial order, lattice, filter, ideal, equivalence relation/partition
(as examples of non distributive lattices), boolean lattices and chains.
It culminates with definitions of monotonic maps, prefixed point, post
fixed point, and least and greatest fixed point, and, finally, with Tarski's
fixed point theorem.
Some familiar examples of fixed points are presented, such at the transitive
closure of a set of relations (R*) and the "reachability" relation.
If there is time, I will have handouts.
Dana Harrington
(Department of Computer Science, Calgary University)
Uniqueness Logic and Uniqueness Categories
ABSTRACT: Uniqueness types are used in the Clean programming language to permit in-place modification of values without violating referential transparency. I will introduce `uniqueness logic', a logic whose formulae are equivalent to uniqueness types via a Curry-Howard `types as formulae' equivalence. Uniqueness logic is similar in spirit to linear logic in the sense of moderating the weakening and contraction rules via a modality. I will conclude with a discussion of `uniqueness categories', the categorical proof theory for uniqueness logic.
Xiuzhan Guo
(Department of Computer Science, Calgary University)
Descent Equivalences
ABSTRACT: Descent Theory was developed by Grothendick in Algebraic Geometry.
We shall give a brief introduction to Descent Theory, introduce the notion
of descent equivalence, and characterize absolute descent
equivalences.
Robin Cockett.
(Department of Computer Science, Calgary University)
The Free Restriction Category Generated by a Graph
ABSTRACT: A restriction category is a category X equipped with a combinator
f: A -> A |---> {f}:A -> A
satisfying the following four (independent )equations:
The free restriction category R(G) generated by a graph G has a particularly simple form:
(s,S):A -> B |----> ((A,[],A),S): A -> A
The category can be most clearly be presented by trees whose arcs are
labeled by the arrows in G and in which a node has been selected
to be the codomain.