recognizability in the simply-typed λ-calculus at LaBRI: 5-6 December 2011, Bordeaux, France.
|14:00 - 15:00||Olivier 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:30||Coffee break|
|15:30 - 16:30||Christopher 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!
|09:00 - 10:00||Gé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:30||Coffee break|
|10:30 - 11:30||Sylvain 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:30||Lunch break|
|13:30 - 14:30||Igor 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:00||Coffee break|
|15:00 - 16:00||Laurent 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:30||Discussion|
This map shows the direction to follow to reach LaBRI from the bus/tram stops.
Sylvain Salvati (INRIA, )