Rencontre, 19 septembre 2024
Programme
- 10:30 – 12:00
-
Clovis Eberhart (NII, Japon)Invited talk: A Compositional Approach to Verification Models
We present a compositional approach to graph-like verification models (e.g., parity games, Markov decision processes, or Petri nets) based on "open" structures. Such open structures are graphs with potentially dangling edges called "open ends", and which form interfaces along which open structures can be composed. We thus define a syntactic category of interfaces and open structures between them. We then define a semantic category representic relevant information about the structure (e.g., a category of probabilistic rewards). Finding an interpretation functor from the syntactic category to the semantic one shows that these structures' sematics can be computed compositionally.
- 13:45 – 14:45
-
Vincent Moreau (IRIF - Université Paris Cité)Invited talk: Profinite trees, through monads and the lambda-calculus
In its simplest form, the theory of regular languages is the study of sets of finite words recognized by finite monoids. The finiteness condition on monoids gives rise to a topological space whose points, called profinite words, encode the limiting behavior of words with respect to finite monoids. Yet, some aspects of the theory of regular languages are not particular to monoids and can be described in a general setting. On the one hand, Bojańczyk has shown how to use monads to generalize the theory of regular languages and has given an abstract definition of the free profinite structure, defined by codensity, given a fixed monad and a notion of finite structure. On the other hand, Salvati has introduced the notion of language of λ-terms, using denotational semantics, which generalizes the case of words and trees through the Church encoding. In recent work, the author and collaborators defined the notion of profinite λ-term using semantics in finite sets and functions, which extend the Church encoding to profinite words.
In this work, we prove that these two generalizations, based on monads and denotational semantics, coincide in the case of trees. To do so, we consider the monad of abstract clones which, when applied to a ranked alphabet, gives the associated clone of ranked trees. This induces a notion of free profinite clone, and hence of profinite trees. The main contribution is a categorical proof that the free profinite clone on a ranked alphabet is isomorphic, as a Stone-enriched clone, to the clone of profinite λ-terms of Church type. Moreover, we also prove a parametricity theorem on families of semantic elements which provides another equivalent formulation of profinite trees in terms of Reynolds parametricity.
- 15:15 – 16:15
-
Zeinab Galal (Università di Bologna)Invited talk: Combining fixpoint and differentiation theory
Interactions between derivatives and fixpoints have many important applications in both computer science and mathematics. In this paper, we provide a categorical framework to combine fixpoints with derivatives by studying Cartesian differential categories with a fixpoint operator. We introduce an additional axiom relating the derivative of a fixpoint with the fixpoint of the derivative. We show how the standard examples of Cartesian differential categories where we can compute fixpoints provide canonical models of this notion. We also consider when the fixpoint operator is a Conway operator, or when the underlying category is closed. As an application, we show how this framework is a suitable setting to formalize the Newton-Raphson optimization for fast approximation of fixpoints and extend it to higher order languages.
see https://arxiv.org/abs/2407.12691
This is joint work with Jean-Simon Pacaud Lemay.
