abstract

USMC Workshop - Abstracts

Rob Goldblatt. A Kripke-Joyal Approach to Residuated and Linear Logics
Abstract:
The Kripke-Joyal semantics for intuitionistic logic is motivated by properties of open coverings in topological spaces. The talk will describe a similar cover-system modelling of propositional logics that lack distribution of conjunction over disjunction. This will be worked through for the residuated logic of the Lambek calculus, extended by left and right negation connectives, combining ideas about covers with orthogonality relations and the groupoid semantics for substructural logics. Introduction of double-negation elimination allows the model theory to be related to the phase-space semantics of linear logic. A negation-free analysis will also be given of a variant of Girard's modality "of course".
Robert K. Meyer. PRESTO-CHANGEO: Using Prop Quantifiers to Cook Up Relevant Connectives.
Abstract:

In Church's secret introduction [1] of his system ${\bf R\rightarrow}$ of pure relevant implication, propositional quantifiers played a key role. (They did not do so in his more accessible [2].) Anderson, Belnap and Dunn in [3, 4] also invoke such quantifiers to define various logical particles, while the present author has had a go in [5, 6, 7] at similar explorations. What all this (and related) work comes to is that propositional quantifiers are enormously powerful in cooking up some otherwise independent relevant connectives and constants in systems of relevant implication. Here we review some of the more spectacular definitional schemes, dividing them into two classes: (A) Definitions that supply ALL of the expected properties of a relevant connective. (Example: the definition of fusion o using $\rightarrow$ , $\forall$ , which goes back to [1].) (B) Definitions that require further axioms to get the relevantly expected properties of a particle. (Example: the definition of disjunction $\lor$ using $\rightarrow$ , $\land$ , $\forall$ , which delivers the lattice properties of $\lor$ from those of $\land$ , but which falls short of the distributive lattice properties that [4] imposes on R. On the other hand, if we are content to stop at the system LR of [8], the definition of $\lor$ is fully adequate.) We indicate a large supply of candidate definitions of particles under both headings, not only for R but for the related linear logic LL of Girard [9]. And we supply, in addition to a number of particular definitions, two powerful definitional schemes, an intensional (or multiplicative) one useful for defining particles like DeMorgan $\sim$ ; and an extensional (or additive) scheme that produces the corresponding Boolean $\neg$ .

[1] Church, A., The weak theory of implication, in A. Menne, A. Wilhelmy and H. Angsel, eds., ``Kontrolliertes Denken, Untersuchungen zum Logikkalkül und zur Logik der Einzelwissenschaften'', Munich (Kommissions-Verlag Karl Alber), 1951, pp. 22-37.

[2] Church, A., The weak positive implicational propositional calculus (abstract), The Journal of Symbolic Logic 16 (1951), p. 238.

[3] Anderson, A. R., and N. D. Belnap, Jr., Enthymemes, The Journal of Philosophy 58 (1961), pp. 713-723.

[4] Anderson, A. R., N. D. Belnap, Jr. and J. M. Dunn, ``Entailment: The Logic of Relevance and Necessity, Vol. II,'' Princeton (Princeton University Press), 1992.

[5] Meyer, R. K., Intuitionism, entailment, negation, in H. Leblanc, ed., ``Truth, Syntax and Modality,'' Proceedings of the Temple University conference on alternative semantics, Amsterdam (North-Holland Publishing Company), 1973, pp. 168-198.

[6] Meyer, R. K., Definition in relevant propositional theories, unpublished typescript, Canberra, 1978.

[7] Meyer, R. K., Improved decision procedures for pure relevant logics, in C. A. Anderson and M. Zeleny, eds., "Logic, Meaning and Computation, Essays in Memory of Alonzo Church," 2001 (Kluwer), pp. 191-217.

[8] Thistlewaite, P. B., M. A. McRobbie and R. K. Meyer, ``Automated Theorem-Proving in Non-Classical Logics,'' Research notes in theoretical computer science, London (Pitman) and New York (John Wiley & Sons), 1988.

[9] Girard, J-Y., Linear logic, Theoretical Computer Science 50 (1987), pp. 1-102.
Tomasz Kowalski. Self-implications in BCI.
Abstract:

The logic BCI is usually defined as a Hilbert system with the following axioms

(B)

$(\phi\rightarrow \psi)\rightarrow ((\chi\rightarrow \phi) \rightarrow (\chi\rightarrow \psi)$

(C)

$(\phi\rightarrow (\psi\rightarrow \chi))\rightarrow (\psi\rightarrow (\phi\rightarrow \psi))$

(I)

$\phi\rightarrow \phi$

and the sole rule of modus ponens. An extension of BCI by the axiom

( $\star$ )

$(\phi\rightarrow \phi)\rightarrow (\psi\rightarrow \psi)$

has also received some attention. Humberstone calls this logic BCI ${}^\star$ in [1] and conjectures that it is the smallest extension of BCI in which all theorems are provably equivalent. He also shows that his conjecture follows from another one, namely:

$\begin{displaymath} \hbox{BCI${}^\star$}\vdash\phi\quad\hbox{ implies }\quad \h... ...i\rightarrow (\chi\rightarrow \chi)\quad \hbox{for some }\chi. \end{displaymath}$ (1)

Humberstone's conjecture was confirmed in [2], but the harder question, also posed in [1], whether the property (1) above holds with BCI in place of BCI ${}^\star$ , remained open. Meyer conjectured (in private communication) that the axiom B is a likely counterexample. We attack this conjecture armed with a cut-free sequent calculus for BCI, and the lemma below.
Lemma 1 The sequent $\Gamma\Rightarrow x$ , with a variable, is provable if and only if there exists a $\gamma = \gamma_n\rightarrow (\gamma_{n-1}\rightarrow \dots\rightarrow (\gamma_1\rightarrow \gamma_0)\dots)\in\Gamma$ such that
1. $\gamma_0 = x$
2. for every $i\in\{1,\dots,n\}$ there is a $\Gamma_i\subseteq\Gamma$ such that $\Gamma_i\Rightarrow \gamma_i$ is provable
3. $\sum_{i=1}^{n}\Gamma_i = \Gamma\setminus\{\gamma\}$
We call the formula satisfying the conditions of Lemma 1 a split formula. Using these we analyse possible proofs of a sequent $B\Rightarrow \phi\rightarrow \phi$ for an arbitrary $\phi$ , always arriving at a contradiction. Someone with a taste for paradox might call this a constructive nonexistence proof. Thus, we show

Theorem 1 The axiom does not imply any self-implication in BCI.

References

[1] L. Humberstone, Variations on a theme of Curry, Notre Dame Journal of Formal Logic 47 (2006), 101-131.

[2] S. Butchard, T. Kowalski, A note on monothetic BCI, Notre Dame Journal of Formal Logic, 47 (2006), 541-544.
Glynn Winskel. Event Structures with Symmetry.
Abstract:

This talk will introduce a model of computation called event structures, in which a process is represented by its events, their causal dependency and conflict. It will motivate and outline very recent work on event structures with symmetry, and sketch applications to the semantics of higher order processes, nondeterministic dataflow and the unfolding of Petri nets.
Rob van Glabbeek. Higher-Dimensional Automata and Other Models of Concurrency.
Abstract:

I will compare the expressiveness of several models of concurrency that could be thought of as formalisations of higher dimensional automata: cubical sets, presheaves over a category of bipointed sets, automata with a predicate on hypercube-shaped subgraphs, labelled step transition systems, and higher dimensional transition systems. A series of counterexamples will illustrate the limitations of each of these models. Additionally I recall a few results relating higher dimensional automata to ordinary automata, Petri nets, and various kinds of event structures.
Michael Norrish. Mechanizing and Using Nominal Recursion Principles.
Abstract?
Brian Davey. Canonical extensions of distributive-lattice-based algebras via Boolean topological algebras
Abstract:
Canonical extensions originated in the famous 1951 work of Jónsson and Tarski, Boolean algebras with operators. Fifty years later, the concept has been extended by an array of authors (Jónsson, Gehrke, Harding, Venema, ...) to distributive lattices, arbitrary lattices and even ordered sets with additional operations. These extensions were motivated by applications to the semantics of various logics, but also by a desire to understand what is going on at an algebraic level.
We present a new slant on canonical extensions of distributive-lattice-based algebras by linking them with Boolean topological algebras. This leads to very natural interpretations of the abstract conditions that characterise the canonical extension of a distributive lattice and yields new insights. For example, it allows us to show in a natural way that the variety generated by a finite distributive-lattice-based algebra is closed under forming canonical extensions. We shall illustrate our approach by giving a simple conceptual proof of the fact that the profinite completion and the canonical extension of a distributive lattice coincide.
Rob van Glabbeek. Proof nets for multiplicative-additive linear logic.
Abstract:

In this talk I will review the definition of MALL proof net of Dominic Hughes and myself, and compare it with Girard's proof nets. I will discuss a couple of alternatives to deal with cut, and state precisely how proof nets capture proofs modulo inessential rule commutations.
Jeremy E. Dawson. Compound Monads and Models of Computation.
Abstract:
We consider several formal systems for describing program semantics and find that each of these is based on a compound monad. We show how the model of computation implicit in each of these theories is based on a compound monad; we discuss these compound monads, showing how some provide examples of a distributive law for monads. We have used the theorem prover Isabelle to formalise and machine-check our results.
Keywords: compound monads, distributive law for monads, generalised substitution, demonic choice, angelic choice.
Adam Eppendahl. Knot Theory and Data Distribution.
Abstract:
In the early nineties, Bill Roscoe gave a scalable algorithm for passing updates around a distributed database and proved that the algorithm maintains database consistency. The proof goes via an algebraic structure that obeys a law used in knot theory, the rack law. We observe that when the paths of updates are drawn in space- time the connection with knot theory stands out clearly. This leads to a simple topological proof of the original algorithm and to extensions of the algorithm. The applications to concurrency actually suggest a weaker theory of demi-racks, which may be related to directed homotopies (although I'm not sure about this yet).
Marcel Jackson (Joint work with Tim Stokes, University of Waikato, NZ). On the algebra of partial maps.
Abstract:

The algebraic properties of the set of all binary relations on a set have been heavily investigated in the context of universal algebra, algebraic logic and their application in theoretical computer science.

In comparison, the study of partial maps is far less developed. This can be at least partly attributed to the failure of the set of partial maps on a set to be closed under many of the basic operations typically considered for binary relations: composition and intersection survive, but (for example) complementation and union do not.

A closer inspection reveals that partial maps are closed under a surprising number of quite expressive operations, and suggests some possible "Master Objects" for the algebraic study of partial maps and their application. We give an introductory survey of some of the existing approaches and present a recent (finite, and equational) characterisation of one of the Master Objects. If time (and expertise!) permit, we will discuss the potential of these approaches to emulate some of the typical applications of algebras of binary relations, and to offer some possible connections between category theory and semigroup theory.
Belinda Trotta. Axiomatising classes of graphs.
Abstract:

A graph is a set of vertices together with a binary relation corresponding to the set of edges. In this language, many familiar classes of graphs can be described by sets of first-order sentences, and in particular by quasi-identities and universal Horn sentences. For example, the class of simple graphs (i.e. those whose edge relation is anti-reflexive and symmetric) is the class of graphs satisfying

$\begin{displaymath} (\forall x) \neg x \sim x \hbox{ and } (\forall x,y) x \sim y \longrightarrow y \sim x, \end{displaymath}$

and the class of graphs whose edge relation is a partial order is the class of graphs satisfying

$\begin{displaymath} (\forall x) x \sim x \hbox{ and } (\forall x,y) x \sim y \l... ...rall x,y,z) x \sim y \land y \sim z \longrightarrow x \sim z. \end{displaymath}$

We consider some questions about using quasi-identities to describe classes of graphs and Boolean topological graphs (i.e. graphs with a compact, totally disconnected topology); for example, when can a class of graphs be axiomatised by only finitely many quasi-identities.
Michael Stevens. Simple unavoidable words.
Abstract:

The unavoidable words problem is concerned with repetition in strings of symbols. There are two main ways to identify a word as unavoidable, one based on generalised pattern matching and one from an algorithm. Both methods are in NP, but do not appear to be in P. We define the simple unavoidable words as a subset of the standard unavoidable words that can be identified by the algorithm in P time. We define depth separating homomorphisms as an easy way to generate a subset of the unavoidable words using the pattern matching method. We then show that the two simpler problems are equivalent to each other.
Ross Street. Feedback equals trace.
Abstract:
Monoidal categories provide a setting where the concept of trace in algebra agrees with the concept of feedback in computer science. The talk will: (a) review the appropriate concepts from category theory, (b) explain the use of string and ribbon diagrams, (c) provide axioms for trace (= feedback), and (d) present the environment where this all becomes formal linear algebra.
Dominic Verity. A Simplicial Approach to Weak $\omega$ -Categories and Directed Homotopy Theory.
Abstract:

In this talk, we introduce a simplicial approach to the theory of weak $\omega$ -categories which directly generalises Kan's classical homotopy theory of simplicial sets, Joyal's theory of quasi-categories and the algebraic theory of strict $\omega$ -categories. In keeping with the theme of this workshop, we also examine how this theory of weak complicial sets might be applied to gaining a better understanding of the directed algebraic topology of concurrent processes and re-writing systems.
Jonathan Cohen. Solving coherence problems with term rewriting.
Abstract:

The coherence problem for an added structure on a category roughly asks "What diagrams commute purely in virtue of the extra structure?". This problem is related to, amongst others, the proof theory of substructural logics and the semantics of concurrent programs. Inspired by work of Kelly on abstract coherence properties, we show how to use term rewriting techniques to efficiently solve several variants of the coherence problem. We then apply this machinery to obtain a new proof of coherence for iterated monoidal categories and interpret this result in terms of compositions of processes in higher dimensional automata.
Grant Pogosyan. Irreducible Elements of Algebraic Clones Lattices.
Abstract:

Clones of -valued logic functions, i.e., composition closed classes of operations on a -element universe that include all projections, form an algebraic and dually algebraic lattice. An element of such lattice is called join- (meet-) irreducible if it cannot be expressed as a join (meet) of other clones, in the usual meaning of these two lattice operations. Such irreducible elements are important since they can serve as generators of the lattice. We present some major results obtained during the past decade or so, which include existence of countable chains of such elements and general criteria for both types of irreducible clones. We also answer some particular questions regarding the irreducible elements located in the `lower part' of the lattice, such as minimal and monoidal clones.
Mike Johnson. Logic, universal algebra and category theory of databases.
Abstract?
Frank Valckenborgh. Some universal constructions in quantum logic.

Abstract:

The last couple of decennia have witnessed an explosion in the number of mathematical structures that pretend to capture various aspects of the properties of physical systems. On the other hand, physical history has shown that the representation theory of various symmetry groups is of the utmost importance to understand physical reality, and the domain of quantum logic has not paid much attention to the integration of symmetry in the operationally motivated structures it proposes for the description of physical systems. It seems that this integration is necessary to make the bridge to the standard descriptions of classical and quantum systems in terms of manifolds and complex Hilbert spaces respectively. In this talk, I want to investigate some of the general structural similarities that arise when one tries to combine group representation theory and quantum logic, and some of the universal constructions that arise.
Yutaka Miyazaki. All splitting logics in NEXT(KTB).

Abstract:

In this talk, we will show that there are only two logics that split the lattice of normal extensions of the modal logic KTB, and that no other logics can split the lattice. They are (1) the logic of the frame of one reflexive point and (2) the logic of the frame of two reflexive points jointed with a symmetric relation. This is a joint work with Tomasz Kowalski (ANU) and Tadeus Litak (JAIST).