Schedule of the meeting[.ics]


Monday December the 5th, 2011

14:00 - 15:00Olivier Serre, What are collapsible pushdown automata good for? [.pdf]

In this talk, I will start by giving the definition of collapsible pushdown automata and explain their relations with higher-order recursion schemes. I will then discuss on specific problems on collapsible pushdown automata arising from games (decidability, winning regions, winning strategy). Then I will discuss about how these results can be used to obtain results on recursion schemes.

15:00 - 15:30Coffee break
15:30 - 16:30Christopher Broadbent, Adventures in Logical Reflection: Abbreviating runs of (C)PDA

Serre et al. [LICS2010] show that a CPDA can be extended with `mu-calculus tests'. That is CPDA can be extended with the ability to `know' whether a given mu-calculus sentence holds at the current configuration in its transition graph. A very useful special case is when the sentence makes a reachability assertion. This allows one to construct a sound approximation of a CPDA that skips out large chunks of the runs of the original.

We illustrate two applications of this technique. The first shows the decidability of the existential fragment of first-order logic on the configuration graphs of a restricted class of CPDA. Whilst this may seem to be a weak result, even existential first-order logic is undecidable on CPDA graphs in general.

The second can be used to implement a proof idea due to Arnaud Carayol that shows the entire n-PDA hierarchy to be non-deterministic context sensitive. This is a result previously stated by Aho and Ullman and recently (re)proved as a consequence of a result by Maneth and Inaba concerning the images of macro tree transducers. (In fact their result establishes the stronger claim of deterministic context sensitivity)

We believe, however, that there is interest in a proof operating directly on higher-order automata. In particular it provides a vehicle to investigate the extent to which the result can be extended to unsafe languages. As a first step in this direction we show that the 3-CPDA languages are context sensitive.

This is not-completely-certain work in progress!

20:00Meeting dinner

Tuesday December the 6th, 2011

09:00 - 10:00Géraud Sénizergues, Pushdown automata of order 2 and applications to recognizability [.pdf]

We characterize the sequences of words (indexed by words) that are computable by p.d.a. of level 2. This characterization is based on endomorphisms of free monoids. Leaning on this characterization we give new proofs or new properties for rational series (over non-commutative undeterminates) and rational subsets of the monoid of endomorphims of a free monoid. (The talk is based on a joint work with N. Marin and J. Ferté).

10:00 - 10:30Coffee break
10:30 - 11:30Sylvain Salvati, Recognizability in the lambda-calculus intersection types and standard finite models

We present the notion of recognizability in the simply typed lambda-calculus by showing the equivalence between intersection types and finite standard models. We then show this notion of recognizability does not coincide with locally finite congruences of the lambda-calculus. This result is similar to the incompleteness of higher order logic with respect to standard models.

11:30 - 13:30Lunch break
13:30 - 14:30Igor Walukiewicz, A transfer theorem for the infinite tree

MSOL-transfer theorems allow us to construct complicated trees with decidable monadic-second order logic (MSOL) theory. A good example is the unfolding theorem: MSOL theory of an unfolding of a graph can be algorithmically reduced to the MSOL theory of the graph. Since an unfolding of a one vertex graph is an infinite sequence, we obtain Buechi's result on decidability of the MSOL theory of an infinite sequence. Iterating unfolding operation followed by an MSOL interpretation we get Caucal hierarchy of graphs having decidable MSOL theory. More recently Ong has shown that MSOL theory of the tree of executions of a recursive scheme is decidable. It is conjectured that MSOL interpretations over such trees give the class of graphs strictly containing the Caucal hierarchy. We will show that the theorem of Ong is an instance of a more general transfer theorem talking about trees resulting from the evaluation of lambda-terms.

14:30 - 15:00Coffee break
15:00 - 16:00Laurent Braud, Order-2 morphic words and recursion schemes [.pdf]

We investigate the infinite-words which are frontiers of solutions of recursive schemes, i.e. leaves by lexicographic order of infinite trees. For order-1 schemes, they are exactly the morphic words, i.e. images of fixpoints of morphisms of words. We extend this result to solutions of order-2 schemes, and introduce 2-morphic words. Safety is not a restriction when considering a specific tree shape, so these words are exactly the words of the corresponding level in the pushdown hierarchy and enjoy the associated properties.

16:00 - 16:30Discussion



The meeting is taking place in room 178 at LaBRI (University of Bordeaux). You can reach LaBRI as follows:

This map shows the direction to follow to reach LaBRI from the bus/tram stops.

Display LaBRI venue on a larger map


Sylvain Salvati (INRIA, )