Vorträge im WS 2015

Das Oberseminar des Lehrstuhls für Theoretische Informatik findet dienstags 14:15-15:45 in Raum 01.252-128 in der Cauerstr. 11 statt. Es steht Masterstudierenden und Doktoranden sowie bei Interesse Bachelorstudierenden offen. Die Themenwahl erfolgt nach Vereinbarung entsprechend den Schwerpunkten des Lehrstuhls. Nachfragen gerne per Mail an den Leiter des Lehrstuhls (mailto:lutz.schroeder@informatik.uni-erlangen.de).

Voraussichtlicher Plan für WS 2015

—

Bisherige Vorträge

 

Date Speaker, Topic Abstract
2-Feb Johannes Schilling, A typed Unix Shell Perhaps the most prevalent Unix design principle (right next to the file methaphor) is the composability of commands to form larger functional units using so-called pipes.

In this talk I will present my attempt to build a unix shell with type information. This enables checking the types of arguments and correctness of pipeline-composition.

A helpful tool in proving assertions about the correctnes of pipeline-composition is J. Ruetten’s coinductive calculus of streams, which I’ll explain briefly as well.
26-Jan Martin Schmitt, On knowledge-based approaches to text classification [pdf-embedder url=”/wp-content/uploads/media/ws15/ober/schmitt.pdf” ] Text classification aims to automatically categorise a given document into one or more predefined classes, such as genres or addressed topics. Current approaches typically use so-called bag-of-words-models to represent document content. In such a model every word (or typically word stem) constitutes either a binary feature indicating just presence/absence or is associated with a number, such as its frequency in the document. In either case, machine learning techniques are used to discover statistical regularities in a training set of already classified documents in order to derive a classification heuristic for unseen data.

In my talk, I want to outline the benefits of using lexical and domain knowledge as well as more complex semantic modelling of document content in the process of text classification. I will present several approaches to doing so with a special emphasis on topic identification in adhoc disclosures as a specific text classification problem.
19-Jan Christoph Egger, //Adding fix-point logic to COOL // [pdf-embedder url=”/wp-content/uploads/media/ws15/ober/egger.pdf” ] Fix-points are a common addition in modal logics materializing as (fragments) of the μ-Calculus. Common variants include logics such as CTL. So far, fix-points could not be used with the COOl solver.

In this presentation I will show how to integrate Daniel Hausmann’s global caching Algorithm for the alternation-free μ-Calculus for use in COOL allowing both CTL Formulas as well as plain Fix-point formulas (from the alternation-free fragment). We’ll also cover some simplifications that can be made to the algorithm for implementation purposes concerning the concept of “deferrals”.
12-Jan Lutz Schröder, //Regular bar expressions and name dropping // Nominal Kleene algebra (NKA) is a formalism to specify trace languages with name generation; it extends standard regular expressions with a name binding construct. NKA has been proved complete over a natural nominal language model. Moreover, it has been shown that NKA expressions can be translated into a species of nondeterministic nominal automata, thus providing one half of a Kleene theorem. The other half is known to fail, i.e. there are nominal languages that can be accepted by a nominal automaton but are not definable in NKA. In the present work, we introduce a calculus of regular expressions with dynamic name binding. It satisfies the full Kleene theorem, i.e.~it is equivalent to a natural species of nominal automata, and thus strictly more expressive than NKA. We show that containment checking in our calculus is decidable in ExpSpace, and in fact has polynomial fixed-parameter space complexity. The known ExpSpace bound for containment of NKA expressions follows.
15-Dec Daniel Hausmann, Deciding the μ-Calculus without Automata or Games [pdf-embedder url=”/wp-content/uploads/media/ws15/ober/hausmann.pdf” ] We resume our endeavour to provide sound, complete and optimal single-pass algorithms for fixpoint logics by extending our attention to the most general logic in this context, i.e. the full relational μ-calculus. To this end I will talk about ongoing work on accommodating the previously seen global caching algorithm [1] to this logic. As fixpoints are allowed to be arbitrarily nested in the full μ-calculus, the conditions for successful proof-graphs (i.e. tableaux) are more involved than e.g. for the alternation-free fragment: least fixpoint literals are allowed to appear infinitely often on circular parts of a tableau, as long as they are always eventually dominated by an overlying greatest fixpoint literal.
This reflects the course of action in previous (multi-pass) algorithms (e.g. [2]) for the μ-calculus which typically first build an exponential-sized pre-tableau, equip it with a complex parity condition and then solve a parity game with respect to the obtained structure, where the winning condition of the game ensures that least fixpoint literals which occur infinitely often always eventually evolve to a greatest fixpoint literal with higher priority.
The propagation in our algorithm essentially corresponds to solving this parity game, however, we are able to propagate at any point during the construction of the pre-tableau (which in spirit corresponds to trying to solve the parity game “before it has been fully built”)\; for formulas that have tableaux (or refutations) of sub-exponential size, this allows our algorithm to finish “early”, i.e. before reaching exponential runtime.[1] D. Hausmann, L. Schröder: Global Caching for the Flat Coalgebraic μ-Calculus, TIME 2015
[2] O. Friedmann, M. Lange: The Modal μ-Calculus Caught Off Guard, TABLEAUX 2011
8-Dec Peter Trommler, //Certified Compilers for Functional Programming Languages // [pdf-embedder url=”/wp-content/uploads/media/ws15/ober/trommler.pdf” ] The Lambda Tamer by Adam Chlipala provides Coq formalizations of programming languages and proof automation for those. In my talk I will present “A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language”, which is the first paper in a series of papers on the Lambda Tamer.
The compiler uses the standard technique of compiling through a series of intermediate languages. The correctness proof for each transformation to an intermediate language is carried out using denotational semantics. All languages are represented as dependent types and denotational semantics are specified as dependently-typed functions.
With the strong dependent types representing language syntax coercion functions need to be introduced for each language. The coercion functions are generated automatically from primitive generic functions for each language and correctness proofs are generated as well. The correctness of each transformation is established by logical relations arguments. The proofs can be automated by greedy quantifier instantiation. Finally, the correctness proofs for individual phases of the compiler are combined into a correctness proof of the complete compiler.
1-Dec Thorsten Wissmann, Regular Behaviours with Names [pdf-embedder url=”/wp-content/uploads/media/ws15/ober/wissmann.pdf” ] Nominal sets provide a framework to study key notions of syntax and semantics such as fresh names, variable binding and α-equivalence on a conveniently abstract categorical level. Coalgebras for endofunctors on nominal sets model, e.g., various forms of automata with names as well as infinite terms with variable binding operators (such as λ-abstraction). The rational fixpoint is the subcoalgebra of the final coalgebra containing precisely the collection of behaviours of orbit-finite coalgebras. For two classes of functors, I present a characterization their rational fixpoint without requiring a characterization of their final coalgebra:
Firstly, I show for functors that are the (so called) localizable lifting of a Set-functor that their rational fixpoint is just that of the underlying Set-functor equipped with canonical nominal structure.
Secondly, if a functor is the quotient of another one (fulfilling a technical condition), then its rational fixpoint is a quotient of the other.
Finally, we will see that the functors for nominal automata and λ-trees modulo α-equivalence are not only instances of this framework but also show that the above two properties fail for the final coalgebra.
26-Nov Paul Blain Levy, Oles embeddings [pdf-embedder url=”/wp-content/uploads/media/ws15/ober/levy2.pdf” ] Oles embeddings are a way of generalizing the notion of injection in the category of sets (and decidable subobject in an extensive category) to an arbitrary category with finite coproducts. The concept is dual to that of Oles expansions, also known as very well-behaved lenses, which have played a role in the semantics of state.
We also introduce notions of Oles inverse image, intersection and union, generalizing the corresponding notions from the category of sets and satisfying several of their properties.
We then further generalize these notions to the setting of a category acting on another category, and we see various examples from the semantics of effects arising as special cases. These include the lookup/update algebras (mnemoids) of Plotkin and Power, and monads supporting exceptions and other kinds of handling.
23-Nov Paul Blain Levy, Transition systems over games [pdf-embedder url=”/wp-content/uploads/media/ws15/ober/levy1.pdf” ] This talk combines two areas of computer science.
(1) The notions of *labelled transition system* (a set of states, starting from which an action may be performed, leading to another state), *trace* (a possible sequence of actions from a starting state) and *bisimulation* (a relation that guarantees two states have matching behaviour) have provided a useful way of reasoning about computational systems.
(2) *Game semantics* is a compositional way of describing the behaviour of higher-⁠order programs employing private state, providing a high-⁠level description in the sense that state is not mentioned.
We want to represent game semantics using transition systems, but traditional systems are too rigid because they have a fixed set of actions. So instead we develop a version of transition system in which each state sits in a position of our game. The actions are the currently available moves.
How do we make this compositional? We do it with a *transfer*, a kind of program that converts moves between two games, giving an operation on strategies. The agreement between the transition systems and the transfer is given by a relation called a *stepped bisimulation*.
(Joint work with Sam Staton)
17-Nov Christoph Rauch, Complete Elgot Monads and Complete Elgot Algebras [pdf-embedder url=”/wp-content/uploads/media/ws15/ober/rauch-talk.pdf” ] In previous work, we established a connection between the generalised resumption monad transformer and so-called complete Elgot monads, which are monads equipped with an iteration operator satisfying certain axioms. Specifically, if a monad T is a complete Elgot monad, there is a unique way of defining a complete Elgot monad structure on the transformed monad such that the defined structure is compatible with the one on T. In view of this result, it is of interest to us to know what the algebras of Elgot monads look like. I present a connection between these algebras and the algebras of the generalised resumption monad, which are in turn related to a concept called Elgot algebras, due to Adámek, Milius and Velebil. In part, this is a generalisation of their work on bases and (Elgot) base algebras, not restricted to the finitary case.
10-Nov Ulrich Dorsch, Generic Expressions from Predicate Liftings [pdf-embedder url=”/wp-content/uploads/media/ws15/ober/dorsch.pdf” ] I will present a generic language of expressions describing coalgebraic behaviour/automata in a similar fashion to regular expressions describing (non-)deterministic finite automata, including a Kleene theorem for the generic expression language and coalgebras of finitary functors that permit predicate liftings with a certain set of properties. Predicate liftings are borrowed from coalgebraic modal logic to define the semantics of generic expressions. Functors covered by this approach are, among others, polynomial functors, finite powerset and finite distribution functor. Equivalence of such generic expressions can be decided efficiently, provided the predicate liftings for the functor at hand can be evaluated efficiently. A prototype algorithm for equivalence checking has been implemented in python.
3-Nov Sergey Goncharov, T-Automata and Reactive Expressions [pdf-embedder url=”/wp-content/uploads/media/ws15/ober/goncharov-talk.pdf” ] The Coalgebraic Chomsky Hierarchy is a generic framework providing a uniform description of state machines and formal languages. It is based on two elementary semantic gadgets, viz, coalgebras and monads, and covers various notions of machines, such as finite state machines, push-down automata, Turing machines, weighted automata, valence automata. Any such machine is associated with a specific type of effect, formalized as a finitary monad over Set and conversely, any finitary monad T over Set yields a corresponding notion of a T-automaton. Any T-automaton is related side by side with a corresponding language of reactive expressions. I present a generic version of Kleene theorem relating reactive expressions with the corresponding T-automata and, like in the classical case, showing their equiexpressivity.
27-Oct Tadeusz Litak, Certified cycles and propositional fixpoints [pdf-embedder url=”/wp-content/uploads/media/ws15/ober/litak-talk.pdf” ] In 1984, Wim Ruitenburg published a paper establishing a surprising property of the intuitionistic propositional calculus, which yields, for example, theorems on definability of fixpoints as immediate corollaries. The proof is heavily syntactic and it seems safe to say the result has not got the attention it deserves. Its computational content and Curry-Howard aspects also have never been analyzed.
I have produced a full Coq formalization of Ruitenburg’s result. Hopefully, it will help the theorem become more widely used and better understood. The formalization can be used for actual computation of fixpoints, including program extraction. Furthermore, I have also analyzed his result from a theoretical point of view, discussing the connections between Ruitenburg’s property and, e.g., local finiteness or uniform interpolation. Spoiler alert: the more one thinks about this theorem, the more unexpected it becomes.
If time, I will tell you about my present work with Albert Visser which led me to be interested in this crazy result in the first place. I may, or may not tell you about surprising corollaries of results on definability of fixpoints (spoiler alert: even with the classical propositional base, results by Bojanczyk&Walukiewicz or Dawar&Otto on expressivity of XPath query languages are such corollaries, as we learned with Balder ten Cate and Gaelle Fontaine many years ago). But this would perhaps make a better material for a follow-up presentation a few weeks later.
20-Oct Lutz Schröder, Regular Expressions with Dynamic Name Binding Nominal Kleene algebra (NKA) is a formalism to specify trace languages with name generation\; it extends standard regular expressions with a name binding construct. NKA has been proved complete over a natural nominal language model. Moreover, it has been shown that NKA expressions can be translated into a species of nondeterministic nominal automata, thus providing one half of a Kleene theorem. The other half is known to fail, i.e. there are nominal languages that can be accepted by a nominal automaton but are not definable in NKA. In the present work, we introduce a calculus of regular expressions with dynamic name binding. It satisfies the full Kleene theorem, i.e. it is equivalent to a natural species of nominal automata, and thus strictly more expressive than NKA. We show that containment checking in our calculus is decidable in ExpSpace, and in fact has polynomial fixed-parameter space complexity. The known ExpSpace bound for containment of NKA expressions follows.