Rencontre, 20 octobre 2022
Programme
- 10:30 – 12:00
-
Marie Fortin (IRIF, CNRS)
It is well-known that linear orders have the 3-variable property, meaning that over linear orders, every monadic first-order formula with up to 3 free variables is equivalent to one that uses at most 3 variables in total. This is usually shown through Ehrenfeucht–Fraïssé games, or as a corollary of the expressive completeness of linear temporal logic (with Stavi connectives). Over the years, this has been extended to richer classes of structures, such as the real line with the +1 relation, Mazurkiewicz traces, or message sequence charts. In this talk, I will present a unifying proof that generalizes those facts. It is based on star-free PDL, a variant of propositional dynamic logic that is closely related to Tarski’s calculus of relations and captures precisely the 3-variable fragment of first-order logic. More precisely, I will show that over structures consisting of one linear order and arbitrarily many binary relations satisfying some monotonicity conditions, star-free PDL has the same expressive power as full first-order logic. This implies that any class of such structures has the 3-variable property.
- 14:00 – 15:00
-
Martin Baillon (Gallinette, LS2N)
We generalize to a rich dependent type theory a proof originally developed by Escardó that all System T functionals are continuous. It relies on the definition of a syntactic model of Baclofen Type Theory, a type theory where dependent elimination must be strict, into the Calculus of Inductive Constructions.
The model is given by three translations: the axiom translation, that adds an oracle to the context; the branching translation, based on the dialogue monad, turning every type into a tree; and finally, a layer of algebraic binary parametricity, binding together the two translations. In the resulting type theory, every function f : (N → N) → N is externally continuous.
- 15:30 – 16:30
-
Tito Nguyễn (LIP, ENS de Lyon)
Among the natural ways to define functions ℕ^k → ℕ in the simply typed λ-calculus, one of them allows hyperexponential growth (any tower of exponentials) but excludes many basic functions such as subtraction and equality, as was discovered by Statman in the 1980s. Until now, this function class did not have any characterization not mentioning the λ-calculus. We provide the first one, which more generally encompasses λ-definable tree-to-tree functions, using an automata model: "collapsible pushdown transducers". As the name of our machines suggests, we draw on the known connections between collapsible pushdown automata and simply typed λ-calculus with fixpoints; in fact, one might think of our results as being about recursion schemes parameterized by finite input trees. Other significant inspirations include:
Engelfriet et al.'s work on higher-order pushdown tree transducers, which are included in our model while already being to our knowledge the most expressive transducer model in the literature (polyregular functions, macro tree transducers, etc. define strict subclasses);
an old result of Plotkin, recently made available thanks to Urzyczyn
(https://arxiv.org/abs/2206.08413), showing that the presence of fixpoints does not affect what total functions can be expressed.
This (unpublished) work is a sequel to my collaboration with Pierre Pradic (Swansea University) on "implicit automata".
NDLR: the talk will be given on the blackboard, so it might be not so easy to follow at a distance, given the available technology
