Rencontre, 10 mars 2022

Programme

10:30 – 12:00

Denis Kuperberg (CNRS - LIP)

Invited talk: Positive First-order Logic on Words and Graphs

[The talk will take place in room M7 411, 4th floor, turn left when you exit the elevator.]

We will investigate the gap between syntactically and semantically positive first-order logic formulas.

A formula is syntactically positive if it does not contain negated predicates, while it is semantically positive when the class of structures it defines is monotone, i.e. closed under making the predicates true on more tuples.

Starting with finite words, I will present the logic FO+, where letter predicates are required to appear positively. The words considered here are on a "powerset alphabet": predicates a(x) and b(x) can be true simultaneously on the same position x of the word. We will ask a syntax versus semantics question: FO+-definable languages are monotone in the letters, but can every FO-definable monotone language be expressed in FO+ ? On general structures, Lyndon's theorem gives a positive answer to this question, but it is known to fail on finite structures. We will see that it already fails on finite words, by giving a simple counter-example language. This gives a new proof for the failure of Lyndon's theorem on finite structures, that is much more elementary than previous proofs.

We will also study the problem on finite graphs: if a class of finite graphs is FO-definable and closed under edge addition, can it be defined with a negation-free formula ? To our knowledge this was an open question, which we can answer negatively via a suitable encoding of our counter-example language.

Finally, if time permits, we will go back to regular languages of finite words and see that FO+-definability is surprisingly undecidable in this framework.

This talk is based on work published in LICS 2021, with a full version currently submitted to a special issue of LMCS, available on Arxiv.

14:00 – 15:00

Loïc Pujet (Gallinette, INRIA)

Invited talk: Extensionality in intensional type theory

[The talk will take place in amphi A, 3rd & 4th floors, at the other end of the corridor w.r.t. amphi B, if you know where this is.]

Martin-Löf Type Theory is a sweet spot in the correspondence between proofs and programs: dependent types and inductive types allow for remarkably expressive program specifications, and adding a universe hierarchy results in a theory with enough logical power to encode most day-to-day mathematical constructions -- an all-around foundational tool for proof assistants.

However the inductive equality supplied by MLTT is not quite suitable for mathematical reasoning, because it encodes program equality ("intensionality") instead of behavioral equality ("extensionality"). This has unfortunate consequences: one cannot prove that the functions n -> n+2 and n -> 2+n are equal, there is no way to quotient a type by an equivalence relation, etc.

Observational Type Theory was designed to remediate to this very state of affairs. A complete implementation of OTT would feature these desired extensionality principles, while preserving the philosophy of the correspondence between proofs and programs and the nice properties that come with it (normalization, canonicity, decidability of typing...).

In my talk, after some preliminary exposition about dependent types, I will introduce TT^obs, a conceptually simple extension of Martin-Löf Type Theory that turns it into a fully observational type theory. I will illustrate with some use cases, and if time allows I will go over its meta-theory.

15:30 – 16:30

Marie Kerjean (CNRS - LIPN)

Invited talk: ∂ is for Dialectica

[The talk will take place in amphi A, 3rd & 4th floors, at the other end of the corridor w.r.t. amphi B, if you know where this is.]

Dialectica is a proof transformation acting of intuitionnistic logic which factors through Girard's translation, allowing the realization of several semi-classical axioms such as Markov's principle. By taking the viewpoint of differential lambda-calculus and recent developments in differentiable programming, we will show how Dialectica computes higher-order backward differentiation. We will illustrate this through the lens of categories, types and lambda-terms.

This is joint work with Pierre-Marie Pédrot.