View: session overviewtalk overview

09:00 | Logic and regular cost functions SPEAKER: Thomas Colcombet ABSTRACT. Abstract—Regular cost functions offer a toolbox for automatically solving problems of existence of bounds, in a way similar to the theory of regular languages. More precisely, it allows to test the existence of bounds for quantities that can be defined in cost monadic second-order logic (a quantitative variant of monadic second-order logic) with inputs that range over finite words, infinite words, finite trees, and (sometimes) infinite trees. Though the initial results date from the works of Hashiguchi in the early eighties, it is during the last decade that the theory took its current shape and that many new results and applications have been established. In this tutorial, two connections linking logic with the theory of regular cost functions will be described. The first connection is a proof of a result of Blumensath, Otto and Weyer stating that it is decidable whether the fixpoint of a monadic second-order formula is reached within a bounded number of iterations over the class of infinite trees. The second connection is how non-standard models (and more precisely non-standard analysis) give rise to a unification of the theory of regular cost functions with the one of regular languages. |

10:30 | On Delay and Regret Determinization of Max-Plus Automata SPEAKER: unknown ABSTRACT. Decidability of the determinization problem for weighted automata over the semiring (Z ∪ {−∞}, max, +), WA for short, is a long-standing open question. We propose two ways of approaching it by constraining the search space of deterministic WA: k-delay and r-regret. A WA N is k-delay determinizable if there exists a deterministic automaton D that defines the same function as N and for all words α in the language of N, the accepting run of D on α is always at most k-away from a maximal accepting run of N on α. That is, along all prefixes of the same length, the absolute difference between the running sums of weights of the two runs is at most k. A WA N is r-regret determinizable if for all words α in its language, its non-determinism can be resolved on the fly to construct a run of N such that the absolute difference between its value and the value assigned to α by N is at most r. We show that a WA is determinizable if and only if it is k-delay determinizable for some k. Hence deciding the existence of some k is as difficult as the general determinization problem. When k and r are given as input, the k-delay and r-regret determinization problems are shown to be EXPTIME-complete. We also show that determining whether a WA is r-regret determinizable for some r is in EXPTIME. |

10:55 | On Strong Determinacy of Countable Stochastic Games SPEAKER: unknown ABSTRACT. We study 2-player turn-based perfect-information stochastic games with countably infinite state space. The players aim at maximizing/minimizing the probability of a given event (i.e., measurable set of infinite plays), such as reachability, Buchi, ω-regular or more general objectives. These games are known to be weakly determined, i.e., they have value. However, strong determinacy of quantitative objectives (given by an event E and a threshold c in [0,1]) was open in many cases: is it always the case that the maximizer or the minimizer has a winning strategy, i.e., one that enforces, against all strategies of the other player, that E is satisfied with probability >=c (resp. We show that almost-sure objectives (where c=1) are strongly determined. This vastly generalizes a previous result on finite games with almost-sure tail objectives. On the other hand we show that >= 1/2 (co-)Buchi objectives are not strongly determined, not even if the game is finitely branching. Moreover, for almost-sure reachability and almost-sure Buchi objectives in finitely branching games, we strengthen strong determinacy by showing that one of the players must have a memoryless deterministic (MD) winning strategy. |

11:20 | Perfect Half Space Games SPEAKER: Sylvain Schmitz ABSTRACT. We introduce perfect half space games, in which the goal of Player 2 is to make the sums of encountered multi-dimensional weights diverge in a direction which is consistent with a chosen sequence of perfect half spaces (chosen dynamically by Player 2). We establish that the bounding games of Jurdziński et al. (ICALP 2015) can be reduced to perfect half space games, which in turn can be translated to the lexicographic energy games of Colcombet and Niwiński, and are positionally determined in a strong sense (Player 2 can play without knowing the current perfect half space). We finally show how perfect half space games and bounding games can be employed to solve multi-dimensional energy parity games in pseudo-polynomial time when both the numbers of energy dimensions and of priorities are fixed, regardless of whether the initial credit is given as part of the input or existentially quantified. This also yields an optimal 2EXPTIME complexity with given initial credit, where the best known upper bound was non-elementary. |

11:45 | On shift-invariant maximal filters and hormonal cellular automata SPEAKER: unknown ABSTRACT. This paper deals with the construction of shift-invariant maximal filters on $\mathbb{Z}$ and their relation to hormonal cellular automata, a generalization of the cellular automata computation model with some information about the global state shared among all the cells. We first design shift-invariant maximal filters in order to define this new model of computation. Starting from different assumptions, we show how to construct such filters, and analyze the computation power of the induced cellular automata computation model. |

13:40 | Quotients in monadic programming: Projective algebras are equivalent to coalgebras SPEAKER: unknown ABSTRACT. In monadic programming, datatypes are presented as free algebras, generated by data values, and by the algebraic operations and equations capturing some computational effects. These algebras are free in the sense that they satisfy just the equations imposed by their algebraic theory, and remain free of any additional equations. The consequence is that they do not admit quotient types. This is, of course, often inconvenient. Whenever a computation involves data with multiple representatives, and they need to be identified according to some equations that are not satisfied by all data, the monadic programmer has to leave the universe of free algebras, and resort to explicit destructors. We characterize the situation when these destructors are preserved under all operations, and the resulting quotients of free algebras are also their subalgebras. Such quotients are called *projective*. Although popular in universal algebra, projective algebras did not attract much attention in the monadic setting, where they turn out to have a surprising avatar: for any given monad, a suitable category of projective algebras is equivalent with the category of coalgebras for the comonad induced by any monad resolution. For a monadic programmer, this equivalence provides a convenient way to implement polymorphic quotients as coalgebras. The dual correspondence of injective coalgebras and all algebras leads to a different family of quotient types, which seems to have a different family of applications. Both equivalences also entail several general corollaries concerning monadicity and comonadicity. |

14:05 | Herbrand Property: Finite Quasi-Herbrand Models and Lifting Chandra-Merlin Theorem to Quantified Conjunctive Queries SPEAKER: unknown ABSTRACT. A structure enjoys the Herbrand property if, whenever it satisfies an equality between terms, all these terms are unifiable. The expressive power of equalities is, thus, trivialized, as their satisfiability is reduced to a purely-syntactic check. In this paper, we introduce the concept of Herbrand property and study its consequences on both a finite-model theoretic and a structural-complexity theoretic level. We first show that the Herbrand property can be implemented in the finite, by what we call quasi-Herbrand models. In particular, this result holds in presence of functions in the vocabulary, in stark contrast to the naive implementation of the property via Herbrand models, showing that the intrinsic infinity of Herbrand universes is somehow inessential. Finite quasi-Herbrand models allow to prove the finite-model property and a decidable finite-satisfiability problem for previously unsettled fragments of first-order logic, where known techniques fail, was it only for the presence of functions in the vocabulary. We then use the Herbrand property to establish computational-complexity results. We obtain, indeed, tight bounds for satisfiability and entailment problems for several fragments of first-order logic. Most prominently, we show that the entailment problem for quantified conjunctive positive relational logic, also known as the quantified conjunctive query containment problem, is in \NPTime. This amounts to a remarkable result both from a logical perspective, boiling down to a generalization of the classic characterization of conjunctive query containment via polynomial-time verifiable homomorphisms (due to Chandra and Merlin, STOC'77), and from a complexity, even algorithmic, perspective, tightening to \NPTime the known 3\ExpTime upper bound (due to Chen, Madelaine, and Martin, LICS'08). |

14:30 | The primitivity of operators in the algebra of binary relations under conjunctions of containments SPEAKER: unknown ABSTRACT. The algebra of binary relations provides union and composition as basic operators, with the empty set as neutral element for union and the identity relation as neutral element for composition. The basic algebra can be enriched with additional features. We consider the diversity relation, the full relation, intersection, set difference, projection, coprojection, and transitive closure. It is customary to express boolean queries on binary relational structures as finite sets of quasi-equations (finite conjunctions of containments). We investigate which features are primitive in this setting, in the sense that omitting the feature would allow strictly less boolean queries to be expressible. Our main result is that, modulo a finite list of elementary interdependencies among the features, every feature is indeed primitive. |

14:55 | A Crevice on the Crane Beach: Finite-Degree Predicates SPEAKER: Michaël Cadilhac ABSTRACT. First-order logic (FO) over words is shown to be equiexpressive with FO equipped with a restricted set of numerical predicates, namely the order, a binary predicate MSB_0, and the *finite-degree* predicates: FO[Arb] = FO[<, MSB_0, Fin]. The Crane Beach Property (CBP), introduced more than a decade ago, is true of a logic if all the expressible languages admitting a neutral letter are regular. Although it is known that FO[Arb] does not have the CBP, it is shown here that the (strong form of the) CBP holds for both FO[<, Fin] and FO[<, MSB_0]. Thus FO[<, Fin] exhibits a form of locality and the CBP, and can still express a wide variety of languages, while being one simple predicate away from the expressive power of FO[Arb]. Some applications to counting are presented. |

15:50 | Data structures for quasistrict higher categories SPEAKER: unknown ABSTRACT. We present new data structures for quasistrict higher categories, in which associativity and unit laws hold strictly. Our approach has low axiomatic complexity compared to traditional algebraic definitions of higher categories, and we use it to give a practical definition of quasistrict 4-category. This definition is amenable to computer implementation, and we use it to give a new machine-verified algebraic proof that every adjunction of 1-cells in a quasistrict 4-category can be promoted to a coherent adjunction satisfying the butterfly equations. |

16:15 | Foundational Nonuniform (Co)datatypes for Higher-Order Logic SPEAKER: Dmitriy Traytel ABSTRACT. Nonuniform (or "nested" or "heterogeneous") datatypes are recursively defined types in which the type arguments vary recursively. They arise in the implementation of finger trees and other efficient functional data structures. We show how to reduce a large class of nonuniform datatypes and codatatypes to uniform types in higher-order logic. We programmed this reduction in the Isabelle/HOL proof assistant, thereby enriching its specification language. Moreover, we derive (co)recursion and (co)induction principles based on a weak variant of parametricity. |

16:40 | A monad for full ground reference cells SPEAKER: unknown ABSTRACT. We present a denotational account of dynamic allocation of potentially cyclic memory cells using a monad on a functor category. We identify the collection of heaps as an object in a different functor category equipped with a monad for adding hiding/encapsulation capabilities to the heaps. We derive a monad for full ground references supporting effect masking by applying a state monad transformer to the encapsulation monad. To evaluate the monad, we present a denotational semantics for a call-by-value calculus with full ground references, and validate associated code transformations. |

17:05 | Effectful Applicative Bisimilarity: Monads, Relators, and Howe's Method SPEAKER: unknown ABSTRACT. We study Abramsky's applicative bisimilarity abstractly, in the context of call-by-value $\lambda$-calculi with algebraic effects. We first of all introduce a computational lambda-calculus, and endow it with a monadic operational semantics. We then show how the theory of relators provides precisely what is needed to generalise applicative bisimilarity to such a calculus, and to single out those monads and relators for which the obtained notion of applicative bisimilarity is a congruence, thus a sound methodology for program equivalence. This is done by studying Howe's method in the abstract. |

**Closing Remarks**