In the honor of my two esteemed colleagues (@abiteboul.com and Victor Vianu), the Abiteboul–Vianu theorem is now formalized and machine-proofed as part of my descriptive-complexity Lean 4 library.
pierresenellart.github.io/descriptive-...
![theorem DescriptiveComplexity.ifpDefinableFree_eq_pfpDefinableFree_iff_ptime_eq_pspace :
(∀ {L : FirstOrder.Language} [inst : L.IsRelational] (P : DecisionProblem L), IFPDefinableFree P ↔ PFPDefinableFree P) ↔ PTIME = PSPACE
The Abiteboul–Vianu theorem. The inflationary and partial fixed-point logics have the same expressive power on unordered finite structures exactly when polynomial time and polynomial space coincide.](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:fhv65kba5do4hgyf7yq4dtyo/bafkreifwpbn737bae4amsnmmns45sfqgsc6z22d3p7eaycq4adgtpsdf7u)
Pierre Senellart
@pierre.senellart.com
173 followers 64 following 115 posts
Professor of computer science at ENS-PSL @normalesup.bsky.social, head of Inria Valda team. VP Digital infrastructure and IT convergence, PSL University @psl-univ.bsky.social.
![Dans le projet de contrat d’objectifs, de moyens et de performance du CNRS pour la période 2024-2028, il est annoncé que «
le CNRS se propose de mettre en valeur, parmi les laboratoires dont il assure la tutelle, les plus remarquables d’entre eux, ceux qui sont réellement “de rang mondial” », dans lesquels « naturellement, l’implication du CNRS serait plus forte, et plus pérenne ». Cette proposition a été présentée par le Président Directeur général du CNRS, Antoine Petit, lors de la Convention CNRS des directeurs et directrices des laboratoires qui a eu lieu le 12 décembre 2024 : il s’agirait de concentrer plus de ressources humaines sur environ un quart des unités de recherche, les « CNRS key-labs ».
La C3N, instance de coordination entre le conseil scientifique du CNRS, les conseils scientifiques d'instituts, les sections et les CID reconnaît l'importance de positionner au niveau national et international les activités scientifiques des unités. Cependant
la C3N s'oppose à la proposition des CNRS Key labs, déplore les conditions d’élaboration de cette proposition et s'inquiète
vivement des conséquences scientifiques, organisationnelles et humaines qu’entrainerait sa mise en œuvre.
[...]](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:fhv65kba5do4hgyf7yq4dtyo/bafkreibt4jfrz5hiwcafjpiavh5eum3brxlhkkpasnjxr7k422dvkurmni)
