cms

A key concept underlying the research programme of Mikolaj Bojanczyk et al on "Nominal Computation" (LICS 2011, POPL 2012) turns out to coincide with one introduced (for quite different purposes) by David Turner in his PhD thesis "Nominal domain theory for concurrency" (Univ. Cambridge 2009). Let me explain...

This talk is about formal techniques for reasoning about names which have emerged in the last years. We will focus on game semantics, and in particular nominal game semantics. The latter constitutes a fresh strand of the theory, founded on nominal sets of Gabbay and Pitts, which provides models for programming languages with new resources such as fragments of ML. Moreover, nominal game models can be given algorithmic representations by means of newly introduced abstract machines, called Fresh- Register Automata, which operate on infinite alphabets of names.

We consider how languages over infinite alphabets can be represented in terms of nominal sets. We propose a variant of History-Dependent Automata for recognising such languages. We introduce the notion of language-accepting history-dependent automata over infinite alphabets and study their expressiveness relating them to existing formalisms for languages over infinite alphabets, in particular to the recently introduced Fresh-Register Automata.

Martin-Löf's dependent type theory is both a foundational framework for constructive mathematics and a functional programming language with a very rich type system. Of course, we want this language to have a rich notion of data structure as well. I will review some classes of data types (indexed inductive types, inductive-recursive types, inductive-inductive types, ...) that one can add to dependent type theory, especially focusing on inductive-inductive definitions and their axiomatisation and categorical semantics.

Note that Fredrik's talk will be a continuation of an earlier one he will give at our PhD seminar

Note this is an unathorized abstract by Alexander

Rob Myers thesis not only generalises and conceptually explains the important work of Bonsangue, Rutten and Silva on generalized Kleene theorems. It also breaks new ground in several important ways.

First, this is the first time different notions of presentations of functors have been systematically investigated and related to the existence and properties of algorithms (such as satisfiability and bisimilarity checking).

Second, the thesis shows how—moving from Set-functors to functors on varieties of algebras—it is possible to increase the computational power of the machines which are described by coalgebras. The important conceptual insight that makes this possible is to replace the finite set of states of the traditional set-based machines by infinite but finitely presentable algebras.

(joint work with A. Kurucz, F. Wolter and M. Zakharyaschev)

An extended abstract of Yoshihito's talk is here and slides are here.

The problems considered in this paper originate in recent applications of large scale ontologies in medicine and other life sciences. The profile OWLEL of the OWL Web Ontology Language, used for this purpose, is based on the description logic EL. The syntactic terms of EL, called concepts, are interpreted as sets in first-order relational models. Concepts are constructed from atomic concepts and constants for the whole domain and empty set using intersection and existential restrictions. From a modal logic point of view, concepts are modal formulas constructed from propositional variables and the constants top, bottom using conjunction and diamonds.

An EL-theory is a set of inclusions (or implications) between such concepts, and the main reasoning problem in applications of EL in life sciences is to decide whether an EL-theory entails a concept inclusion when interpreted over a class of relational structures satisfying certain constraints on its binary relations. Standard constraints in OWLEL are transitivity and reflexivity, for which reasoning in EL is PTime-complete, as well as symmetry and functionality, for which reasoning is ExpTime-complete.

As in modal logic, apart from reasoning over relational models, one can try to develop a purely syntactical reasoning machinery using a calculus. In other words, we can define a more general algebraic semantics for EL: the underlying algebras are bounded meet-semilattices with monotone operators (SLOs, for short), constraints are given by equational theories of SLOs, and the reasoning problem is validity of quasi-equations in such equational theories. The resulting more general entailment problem is not necessarily complete with respect to the `intended' relational semantics. This paper presents our initial results in an attempt to clarify which equational theories of SLOs are complete in this sense and which are not. We also prove that the completeness problem---given a finitely axiomatised equational theory of SLOs, decide whether it is complete with respect to the relational semantics---is algorithmically undecidable, which establishes a principle limitation regarding possible answers to our research question.

With the notable exception of Moss's treatment of coalgebraic logic for measurable spaces, most of the literature on coalgebraic logic takes the intended semantics to be coalgebras in the category Set. That is, the state spaces are discrete, and the logics are classical. And yet, we know that the duals of Boolean algebras are Stone spaces, and hence are not discrete. We also know that a satisfactory treatment of probabilistic transitions will need to deal with non-discrete spaces in order to capture distributions other than the finitely supported ones.

This talk builds coalgebraic logic for Stone spaces, spectral spaces, compact Hausdorff spaces and stably compact spaces in one go, in that precisely the same machinery is used in all four cases to obtain coalgebraic logics for suitable functors. In particular, in each case we define a dcpo of logics tailored to the desired category of state spaces, and show that the coalgebraic logic asssociated to a functor is the least fixpoint of a related Scott continuous function. One pleasant by-product of this approach is that in order to get the right dcpos, the logics must be equipped with a proof theoretic notion of entailment. Thus one can ask about soundness and completeness. We show that the resulting logics are indeed sound and complete for "strong entailment", as well as being expressive (bisimilarity is captured by agreement on formulas). For many functors this also yields decidability of entailment.

I will discuss our recent work with Dirk Pattinson and Katsuhiko Sano on the right correspondence language for coalgebras, i.e., the coalgebraic counterpart of predicate logic. As it turns out, the invention can be traced back to a relatively unknown paper by C.C Chang. I begin with some examples of properties expressible in the new language. Later on, I discuss its relationship with the modal language and more powerful coalgebraic languages and briefly sketch how to prove its completeness for some general classes of functors and predicate liftings. I conclude outlining open questions and directions for future research.

Lutz's talk was also our External Seminar for this week. Please see our External Seminar webpage.

The slides of Lutz's talk are here.

Modal logic is currently one of the most successful logical formalisms in computer science, in particular through its role as the basis for temporal logics on the one hand, and for description logics on the other hand. While modal logics are standardly equipped with a relational semantics, many modes of expression found both in knowledge representation and in the more detailed modelling of reactive systems, in particular where these involve uncertainty or multiple agents, require substantial extensions or modifications of relational semantics. Coalgebraic logic serves as a unified semantic and algorithmic framework for such modalities. We give an introduction to coalgebraic logic and then present a specific result on timed-out tableaux for coalgebraic fixed point logics (joint work with Yde Venema) in more detail.

The slides of Paul's talk are here.

We give a general framework connecing a branching time relation on nodes of a transition system to a final coalgebra for a suitable endofunctor. Examples of relations treated by our theory include bisimilarity, similarity, upper and lower similarity for transition systems with divergence, similarity for discrete probabilistic systems, and nested similarity. Our results describe firstly how to characterize the relation in terms of a given final coalgebra, and secondly how to construct a final coalgebra using the relation.

Our theory uses a notion of ``relator'' based on earlier work of Thijs. But whereas a relator must preserve binary composition in Thijs' framework, it only laxly preserves composition in ours. It is this weaker requirement that allows nested similarity to be an example.

The slides of Rob's presentation are here.

The talk was an overview of dr Tanaka's work in infinitary and predicate modal/superintuitionistic logic. In particular, we focused on the use of Rasiowa-Sikorski Lemma in completeness proofs: a subject recurrent in several papers of dr Tanaka. The last part was devoted to his more recent work on generalization of Yankov formulas in infinitary setting. Slides are here. Yoshihito also took part in the B'ham-Le'ster seminar next day and we devoted a part of it to Rasiowa-Sikorski Lemma.

We present the results of a preliminary investigation on a theory of automata with names. The recognised languages are (nominal) sets of strings over an alphabet with names. More expressive power is obtained by adding the ability to bind names along transitions. These nominal automata can be represented in two ways: either as coalgebras over the nominal sets by Gabbay and Pitts, or as history dependent automata (Montanari-Pistore). Using the latter, more compact representation, we can allocate names over a loop. This results in a "finite memory effect" which is made formal by proving that the finite memory automata of Kaminski and Francez can be encoded as history-dependent automata. It turns out that the recognized languages have an implicit notion of symmetry, which can be used to compress large, symmetric data-sets, by representing groups of permutations using their generators. Joint work with Emilio Tuosto.

We introduce formal languages with binders based on nominal algebras so to characterise classes of nominal formal languages with respect to different types of binders in a uniform way. More precisely, we show initial nominal monoids, which are monoids on nominal algebras, of typical classes of nominal languages, and axiomatise them in a hierarchy of all nominal monoids. Moreover, we extend history dependent automata (HD-automata) by adding stack, and study the recognisability of nominal languages. This is a joint work with Alexander Kurz and Tomoyuki Suzuki.

Boolean algebras capture truth-values of classical logic; Heyting algebras capture truth-values of intuitionistic logic; cylindric algebras capture truth-values of predicate logic. I will discuss a (nominal) algebraic presentation of one-and-a-halfth order logic which, it has been proved, also captures truth values in predicate logic, using nominal algebra. I will briefly sketch nominal algebra and speculate that this nominal algebraic presentation is a useful and natural algebraic notion of truth-value to use in the study of predicate logic. I hope to stimulate discussion on how to turn this speculation into proper research papers. See also the one-and-a-halfth order logic paper.

(joint work with D. Petrişan and J. Velebil) Nominal sets were introduced by Gabbay/Pitts. Two different notions of equational logic over nominal sets were studied by Gabbay/Mathijssen and Clouston/Pitts. In this talk, we introduce the general notion of a based monad and show that finitary based monads give rise to equational theories in the standard sense of many-sorted set-based universal algebra. We further show that restricting these many-sorted equational theories to `uniform' ones brings us back to the equational logics of Gabbay/Mathijssen and Clouston/Pitts. A benefit of our approach is that it allows to apply known results from universal algebra to algebras over nominal sets.

Graph transformation (GT) is a modelling technique based on the representation of states as graphs (or hyper-graphs) and transitions as application of transformation rules. In the DPO algebraic approach, a rule is represented as a span of total graph morphisms, and its application as a double pushout diagram. We have tried to give a formalisation of DPO-GT using intuitionistic linear logic (ILL). ILL allows for a straightforward encoding of DPO-GT at a basic propositional level. In order to deal with rule pattern matching and in particular with renaming associated to injective morphisms, we have introduced a resource-bound existential quantifier that has some features of freshness quantification --- though generally weaker and lacking self-duality.

The paper is based on a joint paper with Reiko Heckel.

Click here to read the full abstract with more background

(ongoing work with A. Kurz and J. Velebil) In this talk we'll have a closer look at the uniform theories introduced in this paper on universal algebra over nominal sets. I will discuss several attempts to define and characterize uniform theories at a more conceptual level.

I will discuss to what extent classical algebraic logic (Tarskian-Hungarian style) can be thought of as a one-and-a-halfth-order logic in Jamie Gabbay's sense. Those who attended our AQSN seminar series so far should be familiar with most of the contents of this mostly improvised talk.