JFLA 2023 - 34èmes Journées Francophones des
Langages Applicatifs

Timothy Bourke, Delphine Demange

► To cite this version:

Timothy Bourke, Delphine Demange. JFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs. JFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs, pp.1-308, 2023, Journées Francophones des Langages Applicatifs. hal-03962188v2

HAL Id: hal-03962188

https://inria.hal.science/hal-03962188v2

Submitted on 22 Feb 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
34èmes Journées Francophones
des
Langages Applicatifs

du 31 janvier au 3 février 2023 à Praz-sur-Arly (Haute-Savoie)
<figure><img src="image_2.png" /></figure>
# Préface

Les JFLA réunissent chaque année, dans un cadre convivial, concepteurs, développeurs et utilisateurs des langages fonctionnels, des assistants de preuve et des outils de vérification de programmes. Le spectre des travaux présentés aux JFLA est très large : il touche les aspects les plus théoriques de la conception des langages applicatifs jusqu'à ses applications industrielles. La 34ème édition des JFLA se déroulera à L'Alisier, à Praz-sur-Arly (Haute-Savoie).

Cette année, nous avons sélectionné 12 articles longs de recherche, 2 articles courts de recherche, et 3 démonstrations de prototypes. Cette sélection a été faite par les membres du comité de programme, que nous remercions chaleureusement, à partir de 21 soumissions initiales.

Nous aurons aussi le grand plaisir d'écouter un exposé invité de Sylvie Boldo sur l'agrégation externe d'informatique, un exposé invité de Xavier Leroy sur les effets en OCaml 5 et un cours invité de Cyril Cohen sur les bibliothèques de Mathematical Components.

**Contributions sélectionnées.** Les contributions sélectionnées pour ces JFLA couvrent des sujets allant des bibliothèques OCaml aux métathéories des langages, en passant par de la preuve formelle appliquée à des problèmes pratiques, et par des analyses statiques par interprétation abstraite.

Une extension de la bibliothèque OCaml unionFind aux références satisfaisant un mécanisme de retour arrière est proposée pour traiter efficacement la vérification de typage d'une extension de System F. Une autre bibliothèque OCaml est présentée qui permet la modélisation, la simulation et la compilation des programmes quantiques de bas niveau.

Pour un langage de programmation décrivant des modèles probabilistes synchrones, c'est-à-dire, des fonctions qui définissent et manipulent de suites de distributions, une méthode d'inférence est proposée pour traiter les paramètres constants des modèles.

En matière de métathéorie des langages, une première étude des modules génératifs ML propose un aller-retour entre les modules OCaml et un encodage en $F^ω$, identifiant au passage un système intermédiaire permettant d'éviter le fossé d'expressivité entre le langage des modules et celui des signatures. Une deuxième étude considère deux modèles de calcul équipés de leur modèle de réalisabilité, et s'intéresse à une traduction avec passage de continuation entre ces deux calculs, pour déterminer si elle peut préserver leurs réalisations.

Plusieurs contributions traitent de l'interprétation, concrète ou abstraite, des langages de programmation. Une première fait état d'une technique pour implémenter des interprètes modadiques en combinant, de façon modulaire et dans Coq, les signatures, les calculs et les règles de raisonnement. Une deuxième présente un outil pour générer des interprètes OCaml à partir d'un langage minimaliste de description de sémantiques. Une autre propose une interprétation abstraite des sémantiques squelettiques. Une dernière présente une technique d'interprétation abstraite pour un langage fonctionnel typé du premier ordre avec un traitement spécifique des types algébriques récursifs.

Plusieurs cas d'application de preuves formelles sont aussi présentés, qui utilisent des cadres de formalisation variés. $F^*$ est utilisé dans l'analyse de la sécurité de TreeSync, un sous-protocole d'authentification pour une messagerie de groupe sécurisée. Why3 sert de base à un logiciel pour prouver la sûreté des logiciels appris par des techniques d'intelligence artificielle. Coq est utilisé dans plusieurs contributions. Une formalisation est faite en Coq de la propriété de sûreté des équipements nucléaires, par analyse des modes de défaillance et de leurs effets. Pour un cadre d'optimisation de programmes par transformations source-à-source vérifiées en Coq, une nouvelle représentation des arbres de syntaxe abstraite intègre des invariants et les preuves associées. Un compilateur vérifié pour un langage synchrone est étendu à deux nouvelles structures d'activation, en complétant l'analyse des dépendances associées. Et une investigation est faite de la
problématique d'intégration au compilateur C formellement vérifié CompCert de flottants non conformes à la norme IEEE-754 et utilisés par certaines cibles embarquées.

D'autres contributions se concentrent sur les outils de preuve eux-mêmes. Une approche vise à rendre la preuve de programmes avec pointeurs à la portée des prouveurs automatiques en projetant une structure récursive sur un domaine numérique. Un traducteur automatique de Metamath vers Dedukti offre deux encodages possibles, permettant ainsi différents compromis en termes d'interopérabilité.

**Remerciements** Nous remercions en premier lieu les auteurs de tous les articles soumis aux JFLA 2023, sans qui les journées n'auraient pas lieu.

Nous tenons aussi à exprimer nos vifs remerciements aux rapporteurs du comité de programme et aux rapporteurs externes. Vous trouverez leurs noms sur les pages suivantes.

Nous remercions également nos chers orateurs invités, qui nous font l'honneur de partager leur expérience et leurs connaissances avec les participants des journées.

Pour l'organisation et la gestion financière, nous remercions les services d'Inria Paris, notamment Tiphaine Leblanc et Fodil Zaidi, et du CNRS à Rennes, notamment Antoine L'Azou. Leur soutien nous a été indispensable. Concernant la publication des actes, nous remercions le Centre pour la Communication Scientifique Directe, et notamment Hélène Lowinger.

Nous remercions enfin les sponsors, listés sur la couverture arrière des actes. Leur implication a permis de subventionner la venue de plusieurs doctorantes, doctorants, étudiantes et étudiants. Elle témoigne également de l'importance des travaux et résultats de recherche scientifique présentés aux JFLA, que leurs retombées pratiques, voire industrielles, soient immédiates ou bien envisagées à plus long terme.

Programmatiquement vôtre,
Timothy Bourke et Delphine Demange.
Comité de programme

Timothy Bourke

Delphine Demange

François Bobot

Lélio Brun

Raphaëlle Crubillé

Pierre-Evariste Dagand

Stefania Gabriela Dumbrava

Benjamin Farinier

Aymeric Fromherz

Diane Gallois-Wong

Assia Mahboubi

Gabriel Radanne

Laurence Rideau

Pierre Roux

Boris Yakobowski

Inria, ÉNS de Paris

Univ Rennes, Inria, CNRS, IRISA

CEA List

National Institute of Informatics

CNRS, LIS, Aix-Marseille

CNRS, IRIF, Paris

Institut Polytechnique de Paris / ENSIIE

Université Rennes 1 / IRISA

Inria de Paris

Nomadic Labs

Inria U. de Rennes, Nantes

LIP ENS Lyon / Inria U. GA, Lyon

Inria U. Côte d'Azur, Sophia Antipolis

Onera, Toulouse

AdaCore, Paris
Rapporteurs externes

Germán Andrés Delbianco

Nicolas Ayache

Guillaume Claret

Guillaume Geoffroy

Boubacar Sall
Table des matières

Exposés et cours invités

<table><tr><td>À propos de l'agrégation d'informatique<br><i>Sylvie Boldo</i></td><td>2</td></tr><tr><td>Tutoriel Mathematical Components<br><i>Cyril Cohen</i></td><td>3</td></tr><tr><td>Théorie et pratique des effets en OCaml 5<br><i>Xavier Leroy</i></td><td>4</td></tr></table>

Articles longs

<table><tr><td>Effectful programming across heterogeneous computation—Work in Progress<br><i>Jean Abou Samra, Martin Bodin et Yannick Zakowski</i></td><td>7</td></tr><tr><td>Filtrer sans s'appauvrir : Inférer les paramètres constants des modèles réactifs probabilistes<br><i>Guillaume Baudart, Grégoire Bussone, Louis Mandel et Christine Tasson</i></td><td>24</td></tr><tr><td>An AST for Representing Programs with Invariants and Proofs<br><i>Guillaume Bertholon et Arthur Charguéraud</i></td><td>43</td></tr><tr><td>Retrofitting OCaml modules : Fixing signature avoidance in the generative case<br><i>Clément Blaudeau, Didier Rémy et Gabriel Radanne</i></td><td>59</td></tr><tr><td>Analyse de dépendance vérifiée pour un langage synchrone à flot de données<br><i>Timothy Bourke, Basile Pesin et Marc Pouzet</i></td><td>101</td></tr><tr><td>Formal proofs applied to system models<br><i>Évelyne Contejean et Andrei Samokish</i></td><td>121</td></tr><tr><td>Do CPS translations also translate realizers?<br><i>Samuel Gardelle et Étienne Miquey</i></td><td>134</td></tr><tr><td>Building CFA for λ-calculus from Skeletal Semantics<br><i>Thomas Jensen, Vincent Rébiscoul et Alan Schmitt</i></td><td>152</td></tr><tr><td>Traduire l'univers des mathématiques en Dedukti, sans univers<br><i>Amélie Ledein et Elliot Butte</i></td><td>172</td></tr><tr><td>Backtracking reference stores<br><i>Gabriel Scherer</i></td><td>190</td></tr><tr><td>Analyse statique de valeurs par interprétation abstraite de programmes fonctionnels manipulant des types algébriques récursifs<br><i>Milla Valnet, Raphaël Monat et Antoine Miné</i></td><td>211</td></tr><tr><td>Vérification symbolique de protocoles cryptographiques en F* : application au sous-protocole TreeSync de MLS<br><i>Théophile Wallez</i></td><td>243</td></tr></table>
## Articles courts

<table><tr><td>Comment dompter un troupeau de flottants sauvages?..................................................</td><td>265</td></tr><tr><td colspan="2">Arthur Correnson</td></tr><tr><td>L'arithmétique de séparation ........................................................................</td><td>274</td></tr><tr><td colspan="2">Jean-Christophe Filliátre et Andrei Paskevich</td></tr></table>

## Démonstrations

<table><tr><td>Goose : an OCaml environment for quantum computing ........................................</td><td>285</td></tr><tr><td colspan="2">Denis Carnier, Arthur Correnson, Christopher McNally et Youssef Moawad</td></tr><tr><td>Décision automatique de relations inductives pour SMTCoq ....................................</td><td>288</td></tr><tr><td colspan="2">Louise Dubois de Prisque</td></tr><tr><td>Caractériser des propriétés de confiance d'IA avec Why3......................................</td><td>291</td></tr><tr><td colspan="2">Julien Girard-Satabin, Michele Alberti, François Bobot et Zakaria Chihani</td></tr><tr><td>Necro ML : Kit de Nécromancie ........................................................................</td><td>296</td></tr><tr><td colspan="2">Louis Noizet et Alan Schmitt</td></tr></table>
Exposés et cours invités
# À propos de l'agrégation d'informatique

Exposé invité

Sylvie Boldo

Université Paris-Saclay, Université Paris-Sud, CNRS, Inria

## Résumé

Cet exposé présentera l'agrégation externe d'informatique ainsi qu'un retour sur sa première session qui a eu lieu en 2022. Le rapport du jury sur la session 2022 se trouve en ligne.<fnref n="1" /> Plus d'informations (épreuves, annales, environnement informatique, FAQ, ...) se trouvent sur le site du jury : https://agreg-info.org/

<footnote n="1">1. https://media.devenirenseignant.gouv.fr/file/agreg_externe/84/0/rj-2022-agregation-externe-informatique_1428840.pdf</footnote>
# Mathematical Components

Tutoriel invité

Cyril Cohen

Inria Sophia Antipolis

## Résumé

Mathematical Components est un ensemble des bibliothèques de mathématiques formalisées développées avec l'assistant de preuve Coq. Ces bibliothèques ont été utilisées pour des projets de formalisation à grande échelle, tels que celle du théorème des quatre couleurs et du théorème de l'ordre impair (Feit-Thompson). Dans ce cours en deux partie, nous explorerons les bibliothèques Mathematical Components disponibles et je fournirai des éléments pour en lire le continu, les utiliser et y contribuer.

La première partie du cours donnera des clés de lecture de la bibliothèque, et en particulier comment y trouver et utiliser les résultats recherchés. Pour cela nous passerons en revue les conventions de nommage et d'usage en vigueur, afin de faire des recherches pertinentes dans le contenu des bibliothèques. Nous verrons également comment lire les scripts de preuve écrits avec le langage de tactique SSReflect, ainsi que les quelques tactiques indispensables pour utiliser des résultats de la bibliothèque. Cela sera illustré avec quelques exemples lors de session d'exercices encadrés.

La deuxième partie du cours sera consacrée aux hiérarchies de structures présentes dans les bibliothèques Mathematical Components et à la manière dont elles sont générées avec Hierarchy Builder à partir de la version 2.0+alpha1 de Mathematical Components. Je présenterai les motivations pour l'utilisation de Hierarchy Builder par rapport à une gestion manuelle avec des records, des classes ou des modules. Ensuite nous examinerons les différentes façons d'instancier des structures, puis comment ajouter des nouvelles structures en utilisant Hierarchy Builder, et enfin comment modifier du code tout en préservant la compatibilité arrière.
# Théorie et pratique des effets en OCaml 5

Cours invité

Xavier Leroy

Collège de France

## Résumé

La version 5 d'OCaml ajoute, sous forme de bibliothèque, un nouveau trait au langage Caml : les effets définis par l'utilisateur et les gestionnaires d'effets.

La première partie de ce cours illustrera la pratique des effets en OCaml 5 [1, 2]. On peut les voir comme une généralisation des exceptions : lever un effet interrompt le calcul en cours, tout comme lever une exception ; mais au contraire des exceptions, le calcul en cours peut être redémarré plus tard. C'est le gestionnaire de l'effet qui décide quand et avec quelle valeur redémarrer ce calcul.

Une première utilisation des effets est l'inversion du contrôle, comme par exemple transformer un itérateur fonctionnel « à la Caml » en itérateur générateur « à la Java ». Toutes sortes de coroutines peuvent également être définies par l'utilisateur en termes d'effets. Plus généralement, les effets d'OCaml 5 ont la puissance d'expression des continuations délimitées linéaires.

Nous terminerons ce tutoriel en esquissant l'implémentation d'une bibliothèque de fibres (lightweight threads) avec entrées/sorties non bloquantes, utilisables en style direct (pas de passage explicite de continuations comme avec la bibliothèque LWT). La bibliothèque EIO en cours de développement [3] pousse cette approche à base de fibres jusqu'à fournir une alternative performante et en style « direct » à LWT.

Dans la deuxième partie du cours, nous aborderons les fondations théoriques des effets et des gestionnaires d'effets. Nous partirons des monades, un concept issu de la théorie des catégories et appliqué à la sémantique dénotationnelle par Moggi en 1989 puis à la programmation fonctionnelle pure par Wadler et d'autres dès 1991. Les monades fournissent un cadre élégant pour décrire de nombreuses sortes d'effets allant de l'affectation à la programmation probabiliste.

Le lambda-calcul « computationnel » de Moggi [4] décrit de manière indépendante de la monade sous-jacente la propagation des effets. Mais la manière dont les effets sont engendrés et gérés est propre à chaque monade. La théorie des effets algébriques de Plotkin et Power [5] fournit un cadre général pour décrire la génération et le traitement des effets et les spécifier de manière algébrique via des équations, un peu comme dans les types abstraits algébriques [6]. Cette théorie débouche naturellement sur les gestionnaires d'effets comme nouvelle construction du langage permettant d'implémenter les effets algébriques.

Le cours se terminera par une brève discussion du typage statique des effets, qui n'est pas encore implémenté en OCaml 5 mais pour lequel plusieurs systèmes de types ont été proposés [7, 8], ainsi que de la preuve par vérification déductive de programmes utilisant des effets [9].

## Références

[1] KC Sivaramakrishnan, *The OCaml system release 5.0, Documentation and user's manual*, section 12.24, «Effect handlers», https://v2.ocaml.org/releases/5.0/htmlman/effects.html.

[2] Daniel Hillerström et KC Sivaramakrishnan, *Concurrent Programming with Effect Handlers*, https://github.com/ocammlabs/ocaml-effects-tutorial.
[3] Thomas Leonard et al., EIO: Effects-based direct-style IO for multicore OCaml, https://github.com/ocaml-multicore/eio.

[4] Eugenio Moggi, *Notions of computations and monads*, Inf. Comput. 93(1), 1991.

[5] Gordon Plotkin et John Power, *Algebraic Operations and Generic Effects*, Applied Categorical Structures 11:69–94, 2003.

[6] Andrej Bauer, *What is algebraic about algebraic effects and handlers?*, arXiv:1807.05923, 2019.

[7] Andrej Bauer et Matija Pretnar, *An effect system for algebraic effects and handlers*, Logical Methods in Computer Science 10(4), 2014.

[8] Daan Leijen, *Type directed compilation of row-typed algebraic effects*. In: *Principles of Programming Languages (POPL) 2017*.

[9] Paulo Emílio de Vilhena et François Pottier, *A separation logic for effect handlers*, Proc. ACM Program. Lang. 5(POPL) : 1-28, 2021.
Articles longs
Effectful Programming across Heterogeneous Computations
— Work in Progress

Jean Abou Samra<fnref n="1" />, Martin BodinD², and Yannick ZakowskiD³

¹ ENS, Paris, France

jean@abou-samra.fr

² Inria, Grenoble, France

martin.bodin@inria.fr

³ Inria, Lyon, France

yannick.zakowski@inria.fr

**Keywords:** Formal Semantics, Free Monad, Coq, Algebraic Effects.

**Abstract**

Monadic programming is a popular way to embed effectful computations in purely functional languages. In particular, the so-called free-monad comes with the promise of extensibility and modularity: computations are seen as syntax arising from a signature of operations they may perform. Popularized in a programming context, the approach is nowadays used for verification in proof assistants as well, as witnessed by frameworks such as FreeSpec or Interaction Trees.

In this work in progress, we investigate the following question. Can we type each sub-
computation with their minimal valid operation signature, and seamlessly combine all these
monadic computations of different natures? Furthermore, can we leverage this additional
precision in typing to derive monadic invariants for free?

We answer positively by suggesting two simple ideas. First, a bind operation between computations living in distinct monads can be defined by transporting them through monad morphisms. Second, to give more structure to the monads we manipulate by indexing them by a semi-lattice as a means to automatically infer the adequate morphisms. We illustrate the benefits on a minimal Coq example: a computation interacting with a memory cell.

# 1 Introduction

Monads were initially introduced as a semantic model for effectful computations [11]. Quickly, they have spread beyond this formal setup to become a popular programming device allowing for safely encapsulating effects in functional programs [4, 13], taking most famously a central role in Haskell's design.

Under the lens of programming, a given monad consists of three core components.<fnref n="1" /> First, a family of types specifies a domain of computations: the *Option* type constructor captures potentially failing computations, the *List* type constructor can be seen as specifying non-deterministic computations, state-threading functions may encapsulate stateful computations, and so on. Monads are furthermore equipped with two operations: the *ret* construct describes how to embed a pure computation into the domain of computations, while the *bind* operation describes how computations can be sequenced (hence its notation `x ← m ;; k`). Figure 1 illustrates the Coq definition of a stateful monad over a single memory *cell* storing a natural number.

<footnote n="1">¹In general, monads should also come equipped with a notion of equivalence of computation. We brush this detail under the rug in this presentation, pretending that we may work with Coq's equality `eq` everywhere. We refer the interested reader to our formal development for a proper setoid-based approach.</footnote>
Definition `monad` := `Type` → `Type`.

Definition `cell` : `Type` := `nat`.

Definition `state` : `monad` := `fun X → cell → cell * X`.

Definition `state_ret` : ∀ X, X → `state X` := `fun X × C ⇒ (C, X)`.

Definition `state_bind` : ∀ X Y, `state X → (X → `state Y`) → state Y` :=
`fun X Y m k c ⇒ let (c', x) := m c in k x c'.`

<caption>Figure 1: The state monad (q)</caption>

Definition `signature` := `Type` → `Type`.
Notation `"M ↪ N"` := (`∀ X, M X → N X`).
Inductive free (`E` : `signature`) (`X` : `Type`) :=
| `pure` (`x` : `X`)
| `op Y` (`e` : `E Y`) (`k` : `Y → free E X`).

Fixpoint interp `E M` (`MM`: `Monad M`
(h : E ↪ M) X (`m` : `free E X`) : M X :=
match `m` with
| `pure x` ⇒ `ret x`
| `op e k` ⇒
    bind (`h e`) (`fun x` ⇒ `interp h` (`k x`))
end.

Variant `Rd` : `signature` :=
| `rd` : `Rd cell`.
Variant `Wr` : `signature` :=
| `wr` (`c` : `cell`) : `Wr unit`.

Definition `h_state`
: `Rd + Wr ↪ state :=`
fun _ e c ⇒ `match e with`
| `inl1 rd` ⇒ (`c`, `c`)
| `inr1 (wr c')` ⇒ (`c'`, `tt`)
end.

<caption>Figure 2: The free monad (q) and its use for stateful computations (q)</caption>

Perhaps more surprisingly, monads offer a solution to Wadler's expression problem. The *free monad* (Figure 2) acts as an extensible syntax [12] for effectful computations: effects are thought of as arising from the use of effectful operations described via an interface *E*. A computation is then essentially encoded as a tree where leaves contain pure computations, and nodes contains operations. The relationship between a node and its children arises from a continuation indexed by the type of answer expected from a valid implementation of the operation. This tree structure is naturally equipped with a monadic structure: leaves directly act as *ret* operations, while *bind* attaches the appropriate continuation to the leaves of the first part of the computation (q).

The right hand-part of Figure 2 illustrates the approach when declaring computations manipulating the previously mentioned cell. The `rd` event specifies the *read* operation: the fact that one expects to get back the content of the cell following this operation is reflected in its type `rd: Rd cell`. In contrast, a *write* event `wr c` is intended to update the content of the cell, but does not entail any informative answer: its return type is merely an acknowledgement, embodied by the *unit* type. From there, one can write rich programs manipulating this memory cell as elements of the monad `free (Rd +' Wr)` where `+` is the disjoint sum of both signatures. Read operations give rise to an infinite branching, with a branch per natural number, while write operations have a single child. In concrete syntax, a computation doubling the current content of the cell becomes:

Definition `double` : `free (Rd + ' Wr) unit` := `n ← rd;; wr (2 * n)`.

The final crucial ingredient to our story is hidden behind the *free monad’s name*: except for their return type, the operations are free of constraints, no semantics is attached to them! Because of this freedom, one can plug’n’play the monadic implementation of one’s choice: by folding over the tree, substituting nodes for their implementations, the `interp` function lifts
monadic implementations of operations into implementations of computations. For instance, `h_state` provides a typical stateful implementation to read and write operations, such that `interp h_state double` becomes the expected executable function of an initial cell.

Monadic interpreters built atop of the free monad are an increasingly popular way to formalize the semantics of programming languages in proof assistants based on dependent typed theories, such as Coq for instance. Indeed, via variants of the *delay* monad [2, 10], divergence can be internalized, freeing us from Coq's termination checker when writing monadic definitional interpreters. When applicable, the approach offers the benefits of compositionality — in the traditional sense of denotational semantics —, of modularity — effects are specified in isolation and modularly composed —, and of executability — through extraction to OCaml for instance, testing is made possible, including when dealing with non-terminating programs.

Specifically in the Coq ecosystem, the approach has been implemented in the FreeSpec library [7, 6, 8] and the Interaction Tree (ITree) project [14, 15]. The viability of the method has been shown to scale to realistic settings such as for modelling LLVM IR [16], or to support non-determinism and model concurrency [5, 3]. In this context, *formal reasoning* about these monadic computations takes back a central place, combining the algebraic reasoning enabled by the monadic setup to unary or relational Hoare style reasoning.

The extensibility of the free approach is central to these large scale projects to enable modularity: orthogonal effects are specified in isolation, and theories can be reused across projects. It is additionally used as a means to painlessly link computations arising from different sources: one can always *translate* free computations into free computations over larger interfaces. However, in our experience, these projects have vastly shied away from leveraging the extensibility as a means to facilitate reasoning. Indeed, signatures can be thought of as a primitive type and effect system. As such, one could play the game of typing as precisely as possible every computation. Coming back to our cell example, we should benefit when possible from reflecting in the type of a computation that the cell is never written to, by typing the computation at type `free Rd X` rather than the larger `free (Rd +' Wr) X`. But we should be able to go further: if considering now a stateful computation over several cells, one should be able to reflect in the signature an over-approximation of the read and write location sites of the computation. Speculating even further, invariants could be encoded in dependent types, specifying for instance that the cell may be written to, but only in an increasing fashion.

*In this work in progress*, we ask the question: is this ambition practical? Can we meaningfully and painlessly combine a zoo of computations of different natures, both as free computations over diverse signatures, but also as their semantic implementations in monads of diverse complexities? Can we leverage this additional typing information to ease the reasoning in two directions: transporting invariants for free, and allowing for reasoning in simpler monadic structures?

We introduce the following early contributions that lead us believe these question should find a positive answer:

* we observe that monadic computations of distinct natures can be bound, provided there is a pair of monad morphisms into a common target (Section 3.1);

* we propose to index the subset of monads of interest by first a partial order (Section 3.2), then a directed set (Section 3.3), in order to remove the need for outrageous explicit type annotations;

* moving to a setup based on the free monad, we propose an axiomatized interface to program with the free and concrete views of the indexing domain of computations (Section 4);
<figure><img src="image_3.png" /><figcaption>Figure 3: Read only, write only, and pure monads ({)}</figcaption></figure>

* we provide a minimal instance of this interface to the case of a stateful computation over a cell (Section 2), and offer some thoughts as to how this work can lead to nicer reasoning principles (Section 5).

All our results are formalized in Coq<fnref n="2" />. This paper can naturally be read as plain text, but we additionally provide hyperlinks to our source code as a support for the interested reader: those are indicated by a ‘{)}’ symbol.

## 2 Running Example

As a means to guide our intuition, we consider as a minimal concrete example stateful computations over a single memory cell as introduced in Section 1. To work with such effects, one would typically (1) assemble pieces of computations written in the *free* (Rd + ' Wr) monad, (2) interpret these computations into the *state* monad, and (3) perform any reasoning, of functional correctness for instance, in this structure.

We propose ourselves to leverage three simple pieces of static information we may collect: a computation might only read the cell, it might only write to the cell, or it might perform neither operation. On the syntactic side, a sufficient condition to ensure these invariants is to type a piece of computation in respectively the *free* Rd, *free* Wr, or *free* θ<fnref n="3" /> monad. We hence have naturally four signatures in mind, organized into a diamond w.r.t. a form of signature inclusion.

So far, little differs from previous work: we could translate the simpler signatures into the largest one when combining computations. However, this would mean that semantically, we still see all computations through the lens of the overly general state monad. Having made the existence of these four kinds of typed computations explicit, the temptation is great to instead interpret each of them into the simplest structure possible. Figure 3 suggests such structures: read only computations should not need to return an updated cell; write only ones should not

<footnote n="2">²https://gitlab.inria.fr/yzakowsk/ordered-signatures/-/tree/jfla23/theories</footnote>

<footnote n="3">³Where θ is the empty signature.</footnote>
<figure><img src="image_4.png" /><figcaption>Figure 4: Flavors of stateful computations: syntax and semantics</figcaption></figure>

have to take the initial cell as argument; and pure computation should live in the identity
monad. We omit the formal definitions here ({) but analogues to `h_state` can be defined to
interpret each signature at play into its corresponding implementation monad.

We hence have a diamond of free monads, upon which we can climb by translation, and
an isomorphic diamond of concrete monads. Although less explicit, the intuition according to
which monads get “more general” when climbing in the diamond is valid in the concrete one
as well. Here, the arrow between two monads M and N represents a monad morphism, i.e., an
operation `fmap`: `M` `~` `N` commuting with `ret` and `bind`. For instance, the morphism between
the read monad and the state monad simply exposes that the cell has been left untouched:

Definition read_state_map: read `~` state := fun X m c ⇒ (c, m c).

<figure><img src="image_5.png" /></figure>

Figure 4 sums up the eight monads we are tempted to manipulate, four on the syntactic side, connected via interpretation to the four on the semantic side. We aim to identify the right interface necessary to program with no overhead with this heterogeneous syntax, as well as to benefit from the additional typing annotations to compose pieces of reasoning in the simplest possible structures. As a simplistic but illustrative example, we consider the following program.

Variable init : cell → free Wr unit.
Variable fetch : free Rd cell.
Definition main (n : cell) : free (Rd + ' Wr) bool :=
    init n ;;
v1 ← fetch ;;
v2 ← fetch ;;
ret (v1 =? v2).

The goal is twofold. Can we write this syntax, despite `init` and `fetch` living in different
syntax than `main`? And second, can we frame the right theory allowing us to leverage the
typing information to prove that `main n` will always return `true` while keeping the definitions of
`init` and `fetch` completely opaque? We already intuitively observe that the second goal requires
us to know how to combine heterogeneous computations not only across the syntactic diamond,
but also across the semantic one: the interpretation of a heterogeneous bind should commute
into a heterogeneous bind of interpretations into distinct monads.

## 3 Monadic Programming

We set aside the free monad temporarily, and first focus on developing the right mathematical
framework to painlessly program with monadic computations living in different structures.
This amounts to binding together computations from different monads: a value `m : M X` in a
first monad `M` and a continuation `k : X → N Y` in a second monad `N`. In other words, we are
trying to define a practical structure with a heterogeneous bind operator with the following type, for several monads M, N, and T.

bind : ∀ X Y, M X → (X → N Y) → T Y

We furthermore ask this heterogeneous bind operator extends the usual monadic laws: `ret` should be a unit for `bind` on both sides, and `bind` should be associative.

## 3.1 Monad Morphisms to Transport

We start with a very simple observation: two computations can always be sequenced as soon as we know how to transport both arguments into a common monad. We hence request the existence of monad morphisms from M to T and from N to T and compose `bind` with the appropriate `fmaps`. Coq automatically infers the type of these `fmaps`, but for better readability, we annotate them in grey in the code.

Definition bindH M N T (MM : Monad M) (MN : Monad N) (MT : Monad T) (MMT : MonadMorphism M T) (MNT : MonadMorphism N T) : ∀ X Y, M X → (X → N Y) → T Y := fun X Y m k ⇒ v ← fmapM ↦→ T m;; fmapN ↦→ T (k v).

Where `Monad M` is a type class constraint asserting the existence of the monadic operations over `M`, and `MonadMorphism N T` a type class constraint ensuring the existence of a morphism `fmapN ↦→ T` from `N` to `T`. In the rest of this subsection, we omit these constraints to lighten the presentation.

By identifying all three monads and using the identity morphism, we show that the heterogeneous bind is indeed an extension of the usual monadic bind.

Lemma bindH_extracts_bind : ∀ M X Y (m : M X) (k : X → M Y), bindH M X → (X → M Y) → M Y m k = bind m k.

Furthermore, the monadic laws remain valid, once appropriately generalized. The left and right `ret` laws simply have to manually `fmap` the unbound pure computations.

Lemma bindH_ret_l : ∀ M N T X Y (x : X) (k : X → N Y), bindH M X → (X → N Y) → T Y (ret x) k = fmapN ↦→ T (k x).

Lemma bindH_ret_r : ∀ M N T X (c : M X), bindH M X → (X → N X) → T X c (fun x ⇒ ret x) = fmapM ↦→ T c.

The associativity of the heterogeneous bind operator is a bit more of a mouthful. We need to consider six monads: three “base” monads `A`, `B`, and `C` for the arguments of the bind (`mx`, `kxy`, and `kyz`), one general monad into which the final result is computed, and two pivot monads `AB` and `BC` for the intermediary results. Figure 5 represents these structures, as well as the various morphisms each bind operator requires to state the lemma. We furthermore assume that the three subdiagrams of Figure 5 commute.

Lemma bindH_bindH : ∀ A B C AB BC T (commAB : ∀ X (m : A X), fmapAB ↦→ T (fmapA ↦→ AB m) = fmapA ↦→ T m) (commBC : ∀ X (m : C X), fmapBC ↦→ T (fmapC ↦→ BC m) = fmapC ↦→ T m) (commBT : ∀ X (m : B X), fmapAB ↦→ T (fmapB ↦→ AB m) = fmapBC ↦→ T (fmapB ↦→ BC m)), ∀ X Y Z (mx : A X) (kxy : X → B Y) (kyz : Y → C Z), bindH (bindH mx kxy) kyz = bindH mx (fun x ⇒ bindH (kxy x) kyz).

One may ponder: have we already solved our programming challenge, can we not write `main` using `bindH`? Well yes, but at great cost! Looking at the type of `bindH`, the unifying monad `T`
<figure><img src="image_6.png" /><figcaption>Figure 5: Monads and their morphisms used to state bindH_bindH</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>Figure 6: Partial Order interface ({)}</figcaption></figure>

cannot be inferred from the type of the computations *m* and *k*: the programmer would essentially have to annotate it manually at every binding point. Furthermore, while the inference of the morphisms involved via instance declarations would be possible, this definition provides no safeguard to guide the programmer, they would have to foresee those they will need. We can do better.

## 3.2 A Partial Order to Index

While the bind operator from Section 3.1 captures semantically what we are looking for, its generality, working over arbitrary monads, leaves both our type checker and our programmer quite in the dark. Looking back at Figure 4, we had identified the constellation of monads at play starting from observing that we might work with some signatures ($\emptyset$, $Rd$, $Wr$, $Rd + '$ Wr), and that these signatures are naturally ordered by inclusion.

We follow this intuition by requesting the user to provide the interface described in Figure 6. We assume a domain of indices *D* equipped with a partial order $\sqsubseteq$ — for our running example, we build the four valued diamond $\{v,r,w,rw\}$. Indices are mapped to the monads of interest via a *reify* function (written $[[\_]]$).

Intuitively, the ordering placed over our indices abstracts the ability to transport computations across monadic structures. We formalize this requisite in the *reify_le* field: we request the user to explicit how to map proofs of inequality between indices to monad morphisms between their respective reification. We define *climbPO* as the function associating the corresponding *fmap* to a given inequality. Finally, we must ensure some coherence: given two monads *M* and
<figure><img src="image_8.png" /><figcaption>Figure 7: Hasse Diagram of the order used in `bindPO_bindPO`</figcaption></figure>

N, we intuitively want to consider at most one way to transport computations from M to N. In particular, the provided morphisms must be compatible with the associativity of the partial order, as spelled out in *reify_le_trans*.

Given such an interface, we can provide a specialization of Section 3.1’s operation: rather than provide a common target monad and morphisms, all we need is to pick an index above the two indexes involved in the computations being sequenced.

Definition bindPO i1 i2 i3 (LT1 : i1 ⊑ i3) (LT2 : i2 ⊑ i3) :
∀ X Y, [[i1]] X → (X → [[i2]] Y) → [[i3]] Y :=
bindH (MMT := reify_le LT1) (MNT := reify_le LT2).

<figure><img src="image_9.png" /></figure>

As before, the extended monadic laws remain valid. But where they used to depend on arbitrary morphisms, they are now specialized to ordered indices: everything relies on the canonical morphism specified by `reify_le`.

Lemma bindPO_ret_l : ∀ i1 i2 i3 (I13 : i1 ⊑ i3) (I23 : i2 ⊑ i3),
∀ X Y (k : X → [[i2]] Y) (x : X),
bindPO I13 I23 (ret x) k = climbPO I23 (k x).

<figure><img src="image_10.png" /></figure>

Lemma bindPO_ret_r : ∀ i1 i2 i3 (I13 : i1 ⊑ i3) (I23 : i2 ⊑ i3),
∀ X (m : [[i1]] X),
bindPO I13 I23 m (ret (X := X)) = climbPO I13 m.

<figure><img src="image_11.png" /></figure>

Lemma bindPO_bindPO : ∀ i1 i2 i3 i4 i5 i6,
(I16 : i1 ⊑ i6) (I46 : i4 ⊑ i6) (I56 : i5 ⊑ i6) (I36 : i3 ⊑ i6)
(I14 : i1 ⊑ i4) (I24 : i2 ⊑ i4) (I25 : i2 ⊑ i5) (I35 : i3 ⊑ i5),
∀ X Y Z (m : [[i1]] X) (k1 : X → [[i2]] Y) (k2 : Y → [[i3]] Z),
bindPO I46 I36 (bindPO I14 I24 m k1) k2
= bindPO I16 I56 m (fun x ⇒ bindPO I25 I35 (k1 x) k2).

<figure><img src="image_12.png" /></figure>

As for `bindH_bindH`, the associativity law is based on a hierarchy of monads. But this time, their relation is expressed as an ordering of their indices, represented in Figure 7. Interestingly, the hypotheses of commutativity are now systematic consequences of `reify_le_trans`, and can therefore be omitted.

At its core, no work has of course been saved, all the morphisms at play must still be provided. But the necessary proof obligations are now cleanly identified, and the arguments to `bind` and to the monadic laws are now drawn from a much simpler structure.

We have shed some light on how to structure the constructions at hand, but have not addressed the other running issue: the unifying monad T from Section 3.1 has now become a unifying index i3, but it still needs to be provided. We remove this thorn in the side by adding slightly more structure to our indexing domain.
## 3.3 A Directed Set to Resolve Indecisiveness

The heterogeneous bind still has too much freedom: from having the luxury of picking the target monad T of its choice, it can now pick its favourite target index `i3`. As a consequence, programmers have to either manually specify `i3` for each call of `bindPO`, or to explicit the return type of each bind operation.

This freedom feels superfluous when coding: taking inspiration from our running example once again, it seems always safe to look at our index domain as having the structure of a semi-lattice and taking as target the join of the indices involved. In practice, picking the smallest upper bound does not matter for soundness, all we care about is to have a canonical way to choose a binary upper bound: we request the user to additionally equip their partial order with the structure of a directed set.

Variable join : D → D → D.
Infix "□" := join.
Hypothesis join_le_1 : ∀ i1 i2, i1 ⊑ i1 ▔ i2.
Hypothesis join_le_r : ∀ i1 i2, i2 ⊑ i1 ▔ i2.

<figure><img src="image_13.png" /></figure>

The heterogeneous bind specialises `bindPO` with the two inequalities about ▔. This time Coq can infer all type arguments from (`m` : `[i1]` X) and (`k` : X → `[i2]` Y), discharging a lot of annotations from the programmer.

Definition bindL i1 i2 :
∀ X Y, [[i1]] X → (X → [[i2]] Y) → [[i1] ▔ i2] Y :=
bindPO (join_le_1 i1 i2) (join_le_r i1 i2).

<figure><img src="image_14.png" /></figure>

The `main` function constituting our running example can thus be written with the desired syntax, with no additional notation, provided that the extended interface is provided. We furthermore observe that the user can provide a reification of the indexing diamond into either the free diamond (left part in Figure 4) or the semantic diamond (right part in Figure 4).

Definition main (n : data) :=
  init n ;;
v1 ← fetch ;;
v2 ← fetch ;;
ret (v1 =? v2).

<figure><img src="image_15.png" /></figure>

Depending on their choice, the exact same syntax, depicted to the right will be valid against opaque computations `init` and `fetch` living in respectively `free Wr` and `free Rd`, or in `write` and `read`. Its return type will be directly inferred as respectively `free (Rd + ' Wr)` or `state` from the joins involved.

We have overlooked one detail in the code above: the typing of `ret (v1 =? v2)` remains ambiguous. However this is easily resolved. By definition, `ret` performs no effect in the monads, hence if the lattice is equipped with a `⊥` element (typically reified into the `pure` monad), then it is safe to always use this element as an index for `ret`: we can thus redefine `ret` to always live in this “minimal” monad.

In order to guide the type inference when performing a bind, we have added a computational device, `join`, to compute the index governing the monadic type of the result. Pandora's box is open, we are performing non-trivial dependent programming. The consequences show up the moment we turn our attention to the monadic laws for `bindL`. Things remain straightforward for the two `ret` laws:

Lemma bindL ret_l : ∀ i1 i2,
∀ X Y (k : X → [[i2]] Y) (x : X),
bindL (ret (M := [[i1]])) x k = climbPO (join_le_r i1 i2) (k x).

<figure><img src="image_16.png" /></figure>

Lemma bindL ret_r : ∀ i1 i2,
∀ X (m : [[i1]] X),
bindL m (ret (M := [[i2]])) = climbPO (join_le_l i1 i2) m.

<figure><img src="image_17.png" /></figure>
But the obvious statement for associativity does not even type check!

```pascal
Fail Lemma bindL_bindL_fail : ∀ i1 i2 i3,
                             ∀ X Y Z (m : [[i1]] X) (k1 : X → [[i2]] Y) (k2 : Y → [[i3]] Z),
                             bindL (bindL m k1) k2 = bindL m (fun x ⇒ bindL (k1 x) k2).
```

Indeed, the expression `bindL (bindL m k1) k2` has type `[[i1] ∪ i2] ∪ i3] Z` while the expression `bindL m (fun x ⇒ bindL (k1 x) k2)` has type `[[i1] ∪ (i2 ∪ i3)] Z`. In other words, we need to assume the associativity of our domain of indices to express the associativity of our heterogeneous bind.

```pascal
Hypothesis joinnell Assoc : ∀ i1 i2 i3, i1 ∪ (i2 ∪ i3) = (i1 ∪ i2) ∪ i3.
```

<figure><img src="image_18.png" /></figure>

Luckily, `climbPO` allows us to follow any inequality proof along our index domain. It can hence in particular be used to transport equality proofs in our types: by instantiating it over `joinAssoc`, we get the `climbAssoc` transport function (we omit its code here) needed to state the bind associativity.

```pascal
Definition climbAssoc : ∀ i1 i2 i3 : [[i1] ∪ (i2 ∪ i3)] ↦→ [[(i1 ∪ i2) ∪ i3]].
```

<figure><img src="image_19.png" /></figure>

```pascal
Lemma bindL_bindL : ∀ i1 i2 i3,
  ∀ X Y Z (m : [[i1]] X) (k1 : X → [[i2]] Y) (k2 : Y → [[i3]] Z),
  bindL (bindL m k1) k2 = climbAssoc (bindL m (fun x ⇒ bindL (k1 x) k2)).
```

<figure><img src="image_20.png" /></figure>

At this point, we have reached a first milestone: we have identified a suitable interface to program in a heterogeneous way across a set of monads organised as the reification of a pointed set. We now turn our attention back to the free monad.

# 4 Support for the Free Monad

In the previous section, we have seen that indexing monads by a directed set whose order maps to monad morphisms between the reified monad provides an adequate interface to support heterogeneous programming among those monads. Looking once again back at Figure 4, one gets the feeling that we did not quite strike the bullseye. First, we had not one but two structured sets of monads in mind — the syntactic world with the various free monads, and the semantic counterpart with their interpretations. Furthermore, signatures themselves seemed to play a specific role. In this section, we provide yet another interface, from which we will derive two instances of the directed one, respectively for the syntax and the semantics. The full interface is depicted on Figure 8: we motivate and walk through its components in this section. As an additional visual support, Figure 9 depicts the data contained in the interface when instantiated to our running example.

A first intuition could be to consider that signatures themselves should form the indexing structure. After all, the disjoint sum (`+`)' could be a candidate for `join`, while signature inclusion, written `-<' and defined by the existence of an injection between the signatures, would constitute a valid order. However, disjoint sum is much too crude a `join` — at the very least, we would like to look more closely to a set-theoretical join — and we therefore still need to introduce a proper pointed set `D`. But on the syntactic side, we are indeed indexing signatures rather than monads: this is the purpose of the part of Figure 8 describing the first layer of reification. In contrast to the previous case, two ordered indices must here map to reified signatures such that the smallest one can be injected into the largest one, as witnessed by `Sinj`. We impose three coherence properties on this first layer of reification: the injections should be proof irrelevant, proofs of self relation should map to the identity injection, and proofs by transitivity should map to the composition of their respective injections.
(* The directed domain by which we index *)

Variable D : Type.

Djoin_le_1 : ∀ d1 d2, d1 ⊑ d1 ⊔ d2;

Djoin_le_r : ∀ d1 d2, d2 ⊑ d1 ⊔ d2;

Djoinnell : ∀ d1 d2 d3, d1 ⊔ (d2 ⊔ d3) = d1 ⊔ d2 ⊔ d3;

( * First layer of reification : in terms of signatures *)

Sreify : D → signature;

Notation "'[' i ']'" := (Sreify i);

( * To the order must correspond injections *)

Sinj : ∀ d1 d2, d1 ⊑ d2 → [[d1]] < [[d2]];

( * Coherence properties of these injections *)

Sinj_proper : ∀ d1 d2 (I12 I12' : d1 ⊑ d2), Sinj I12 = Sinj I12';

Sinj_refl : ∀ d (I : d ⊑ d), Sinj I = inject_id;

Sinj_trans : ∀ d1 d2 d3 (I12 : d1 ⊑ d2) (I23 : d2 ⊑ d3),
(Sinj I12) ○ (Sinj I23) = Sinj (PreOrder_Transitive _ _ _ I12 I23);

( * Via the free construction, D reifies into the corresponding free monads *)

Freify d := free [[d]];

Notation "'{ i ']'" := (Freify i);

Ffmap d1 d2 (I : d1 ⊑ d2) : {d1} ↦→ {d2} := fun m ⇒ translate (Sinj I) m;

( * Second layer of reification : in terms of concrete monads *)

Mreify : D → monad;

Notation "'«' i '»" := (Mreify i).

Mmonad : ∀ d, Mmonad «d»;

( * To the order must correspond morphisms *)

Mmorph : ∀ d1 d2, d1 ⊑ d2 → MmonadMorphism «d1» «d2»;

( * Coherence properties of these morphisms *)

Mfmap {d1 d2} (I : d1 ⊑ d2) X : «d1» ↦→ «d2» :=

Mfmap «d1» «d2» (Morphism := Morph (Mmorph I)) X;

Mmorph_proper : ∀ d1 d2 (I J : d1 ⊑ d2), (Mfmap I) = (Mfmap J);

Mmorph_refl : ∀ d (I : d ⊑ d) X (m : «d» X), Mfmap I m = m;

Mmorph_trans : ∀ d1 d2 d3 (I12 : d1 ⊑ d2) (I23 : d2 ⊑ d3),
(Mfmap I12) ○ (Mfmap I23) = Mfmap (PreOrder_Transitive I12 I23);

( * Both layers are finally connected by handlers *)

Dh : ∀ d, [[d]] ↦→ «d»;

Id : {d} ↦→ «d» := interp (Dh d);

( * Climbing in the syntax and then interpreting or interpreting and then climbing in the semantics should commute *)

I_commut : ∀ d1 d2 (I : d1 ⊑ d2) X (m : {d1} X),

I (Ffmap I m) = Mfmap I (I m)

<caption>Figure 8: Interface for free monadic computations (�)</caption>

Turning our eye to Figure 9, we have so far covered the upper part of the figure. The indexing diamond maps to the one containing the four signatures introduced in Section 2 via Sreify (also noted [[_]]). By the free construction, signatures get mapped to all the free monads at which we might want to write programs — hence by composition, reification into signature induces a reification Freify (noted {\_}) into free monads. Non-explicitly represented are the nature and relationship between the arrows in each of these three boxes: to a proof of inequality corresponds an injection of signatures, to which correspond a monad morphism between the corresponding free monads — the latter is derived for free.
<figure><img src="image_21.png" /><figcaption>Figure 9: The full picture instantiated on our running example (�)</figcaption></figure>

We now bring into the picture the monads in which we concretely implement our effectful operations. This is the purpose of the second layer of reification from Figure 8: Mreify (also noted «_») maps the same domain of indices D to concrete monads. This part of the interface is very close to the one developed in Section 3.3: indices must be reified into monads, and proofs of inequality must map to monad morphisms. The coherence properties are identical to the ones for the first layer of reification. On Figure 9, we have now introduced a fourth diamond, containing the state monad and its simplified versions, and the left arrow.

It remains only to relate the “free” diamond to the concrete one: we need to explain how we
can implement the relevant signatures — this is captured by Dh. The user must provide at each
index d a handler (Dh d : [[d]] ↛ «d»): the Rd events must be implemented in the read monad,
the Rd + Wr ones in the state monad, and so on. Much like the reification into signatures gives
rise to a reification into the free monads, this family of handlers entails a bridge I between the
diamond of free monads and the one of concrete monads via the interp function, completing
the picture.

There remains one unstated coherence condition. Given two indices *i* and *j* such that *i* ⊑ *j*, one may now follow two paths, represented in Figure 10. On one hand, we can translate the signature [[*i*]] into [[*j*]] (property *Sinj* in Figure 8), and thus translate any tree in {{ *i* }} into {{ *j* }}—this is the role of the *translate* function in the definition of *Ffmap*. We can then interpret the resulting computation into «*j*». On the other hand, we may interpret [[*i*]] into «*i*», and then transport «*i*» into «*j*». Condition *I_commut* ensures that this diagram commutes.

From an instance of the interface from Figure 8, we derive three essential facts. The first is
an instance of the directed interface indexed by D w.r.t. Freify. The second is an instance of
the directed interface indexed by D w.r.t. Mreify. We can hence sequence heterogeneous com-
<figure><img src="image_22.png" /><figcaption>Figure 10: Representation of the *I_commut* property</figcaption></figure>

putations in both the syntactic and semantic world: let us write these operations respectively *Fbind* and *Mbind*. The last important result we derive is a theorem for commuting interpretation with binds in this melting pot:

Theorem bind_I : ∀ d1 d2 X Y (m : free [[d1]] X) (k : X → free [[d2]] Y),
I (Fbind m k) = Mbind (I m) (fun x ⇒ I (k x)).

<figure><img src="image_23.png" /></figure>

We have fulfilled the core of our contract by axiomatizing an interface allowing us to write
the tightly typed version of main without additional crust. But even more importantly, it allows
us to switch the perspective we have on the semantics of a compound computation, obtained
by monadic interpretation, into the composition of the generally simpler implementation of
its sub-components. Equipped with the minimal ingredients necessary to express and leverage
effect typing information, we now sketch some early avenues to try and take advantage of it.

5 Reasoning

Sections 3 and 4 have depicted the core of our current contribution: a clean specification of the necessary interface to enable (1) programming in the free monad over a variety of signatures, (2) mapping each computation to an adequate structure of implementation, (3) retaining equational reasoning through notably generalized monadic laws and commutation of interpretation with heterogeneous binds. We now reach the current limits of this work in progress: the principled way to leverage typing information has yet to be identified, and no case study at sufficient scale has yet been performed to back up a particular ad-hoc approach. We hence only modestly present a few directions we have been exploring, and ornate them with preliminary remarks.

Recall Section 2's task: can we prove that main n will always return true. This could be
specified extensionally, breaking the monadic abstraction: ∀ c, snd (*I* (call n)) = true. It
seems more appealing to introduce a unary Hoare logic over state.

Definition pre_state := (cell → Prop).
Definition post_state X := (X → cell → Prop).
Definition Hoare_state X : pre_state → state X → post_state X → Prop :=
fun P m Q ⇒ ∀ c, P c → let ' (c', x) := m c in Q x c'.

<figure><img src="image_24.png" /></figure>

Our goal hence become:

Theorem main correct : ∀ (n : nat),
Hoare_state (fun _ ⇒ True) (*I* (main n)) (fun v _ ⇒ v = true).

Using bind_I, the computation becomes explicitly the sequence of a computation in write
with a computation in read. Using a cut rule for our Hoare logic, we can eliminate the former
at the trivial postcondition, and are hence left with reasoning about the remaining read only
computation. A quite adhoc way to conclude is to prove a general law of read only computations:
when called twice in sequence, they lead to the same result.
Lemma read_twice (m : free Rd nat) :
∀ c, I (v1 ← m ; ;
v2 ← m ; ;
ret (v1 =? v2)) c = true.

<figure><img src="image_25.png" /></figure>

This lemma breaks the abstraction introduced by `read`, but solves our goal immediately. It leverages our ability to keep track of the type of `fetch` to derive a generic invariant of the computation. From this perspective, it is a satisfying result, and the one we currently propose in our formal development.

In the remaining of this section, we discuss potential avenues to go further.

**Finer grain invariants breaking abstraction.** Although `read_twice` is generic over arbitrary computations (`m : free Rd nat`), it still fills handcrafted specifically for our problem. One may wonder whether the primitive fact expressing that `read` only computations may not affect the cell may suffice. Similarly, pure and write-only computations can be explicitly proved to not depend on the initial state.

Lemma read_invariant_explicit : ∀ X (m : read X) c,
let (cf,x) := fmap read ↦→ state m c in c = cf.

<figure><img src="image_26.png" /></figure>

Lemma write_invariant_explicit : ∀ X (m : write X) c c',
let (cf,x) := fmap write ↦→ state m c in
let (cf',x') := fmap write ↦→ state m c' in
x = x' ∧ ((cf = c ∧ cf' = c') ∨ cf = cf').

Lemma pure_invariant_explicit : ∀ X (m : pure X) c c',
let (cf,x) := fmap pure ↦→ state m c in
let (cf',x') := fmap pure ↦→ state m c' in
x = x' ∧ cf = c ∧ cf' = c'.

However, these invariants require to completely break the abstractions in order to be useful. On a simple example such as `main`, managing to reduce enough the computation to exhibit the sub-parts needed without simply computing the whole thing has proved unreasonably cumbersome for the expected benefit. It would nonetheless be interesting to see if it can be done, and may be worth it when working with coinductive computations such as the ones generated by `ITrees`, as (internal to `Coq`) reduction is not possible in this context.

**Internalizing read_state_invariant_explicit into hoare_state.** Rather than explicitly expos-
ing the underlying computation, one could try to express the invariants as state_hoare triplets
valid for any computation lifted from a given monad. Expressing that the state is left unchanged
in this style is however quite annoying. One option is to change the postcondition so that it
quantifies additionally over the initial state before the execution as well. Another is to use a
meta-variable in order to bind as an equality in the precondition the initial value of the cell,
and use the same meta-variable in the postcondition.

Lemma read_state_invariant : ∀ X v (m : read X),
Hoare_state (fun c ⇒ c = v) (fmap read ↦→ state m) (fun _ c ⇒ c = v)

<figure><img src="image_27.png" /></figure>

However, in both cases, there seems to be no obvious way to leverage such a rule to ensure that
the second call to `fetch` would return the same value.

Furthermore, it is unclear how one would internalize in `state_hoare` the write only invariant `write_invariant_explicit`.
Definition post_pure X := (X → Prop).
Definition Hoare_pure X : pure X → post_pure X → Prop :=
fun m Q ⇒ Q m.

<figure><img src="image_28.png" /></figure>

Definition pre_read := (cell → Prop).

Definition post_read X := (X → Prop).

Definition Hoare_read X : pre_read → read X → post_read X → Prop :=
fun P m Q ⇒ ∀ c, P c → let x := m c in Q x.

Definition post_write X := ((X → Prop) * (cell → Prop)).

Definition Hoare_write X : write X → post_write X → Prop :=
fun m' (Qx, Qc) ⇒ let' (x, mc) := m in
match mc with
| None ⇒ Qx x
| Some c ⇒ Qx x ∧ Qc c
end.

<caption>Figure 11: Hoare-style proof system for pure, read only and write only monads</caption>

**Hoare-style abstraction at each level.** A strong temptation is to avoid breaking any abstraction. We have worked hard to preserve information about the structure in which each computation has been built, in a way compatible with equational reasoning. We would like to follow the usual approach and pair it cleanly with Hoare-style reasoning in the appropriate structure.

Naturally, this suggests that we should associate a Hoare-style proof system to each monad at play. For our running case study, we hence need a diamond of hoare systems: the missing components can be found in Figure 11. While more appealing, similar difficulties arise: for instance, read only computations seem to require a meta-variable to be lifted.

Lemma read_invariant : ∀ X v (m : read X) (P : pre_read) (Q : post_read X),
Hoare_read P m Q →
Hoare_state (fun c ⇒ P c ∧ c = v) (fmap read ~ state m) (fun x c ⇒ c = v ∧ Q x).

<figure><img src="image_29.png" /></figure>

Furthermore, we are here working in an ad-hoc fashion, handcrafting proof systems for our case study. In order to state generic laws about these systems, and notably w.r.t. their interactions with `fmap`, we would need to move them to the interface. However identifying a universal shape to monadic deductive systems is non-trivial: it would likely have to rely on porting Maillard et al.'s work on Dijkstra monads [9].

We plan on conducting additional case studies at medium scale to better identify the kind of reasoning we may want to perform, and hopefully derive the adequate framework to do so.

# 6 Discussion and Future Work

The initial motivation for this work emerged from a Coq formalisation of R [1]. This formalisation is a large monadic interpreter of roughly 18,000 lines of code, with about two thousand bind applications. Proving some safety invariant within this formalisation (for instance memory safety) is doable, but requires a substantial proof effort due to the size of the interpreter: invariant lemmas have to be stated and proven for every function. Frustratingly, a lot of these lemmas felt obvious, as most functions only use a small subset of effects.

To illustrate this intuition, we categorised the interpreter functions involved in the formalization by the effects they used: Figure 12 shows the different categories that we identified.
<figure><img src="image_30.png" /><figcaption>Figure 12: Hasse diagram for the different effects within a R monadic interpreter [1].</figcaption></figure>

Effects used by each category:

r: reading global variables

w: writing global variables

h: heap operations

e: throwing errors

f: function calls

l: low-level operations

An interesting part of this diagram are the categories that are not shown: for instance, we did not find any interpreter functions that could raise an error (effect *e*) without reading the interpreter's global variables (effect *r*), thus the *re* category is shown in the diagram, but not *e*. Almost all interpreter functions read these global variables, but only a small number write them: these are the functions initialising the interpreter at the very beginning of the execution, never to be called back again. In figure 12, these initialising functions fall into the *rwh* category. As a consequence, for most of the interpreter execution, these variables are constant by construction: no interpreter function syntactially call the write operations. The invariant that these global variables are constant after the initialisation phase thus ought to be simple to prove, but it turned out to be cumbersome in practice. We expect the *⊤* category to be almost empty, with the sole exception of the main function that sets up the initialisation and calls the read-eval-print loop.

We believe that the ongoing work we present in this paper may help ease the points observed in this large scale project: the categories of Figure 12 fit well into the directed set of Section 3.3. We could thus imagine rewriting the interpreter within this formalism. As the approach presented in this work is based on a *bind* operation whose usage is very close to the usual monadic *bind*, we do not expect this conversion to require a significant amount of work. During type inference, Coq will compute where each interpreter function falls within the directed set. This enables a first phase of verification for the programmer: for instance, if a function is inferred to be of type *⊤* (which in the context of R is expected to be very rare), something may be wrong and is worth inspecting. Furthermore, each of these categories provides some invariants: the sketches of methodology presented in Section 5 should be improved upon to cleanly state, prove, and leverage these invariants. In the case of this R interpreter, the size of the interpreter is large compared to the number of monads involved: we expect to get similar results to the ones presented in a cumbersome way in [1], but with less work.
References

[1] Martin Bodin, Tomás Diaz, and Éric Tanter. A trustworthy mechanized formalization of R. In *Dynamic Languages Symposium, DLS*, 2018.

[2] Venanzio Capretta. General recursion via coinductive types. *Log. Methods Comput. Sci.*, 1(2), 2005.

[3] Nicolas Chappe, Paul He, Ludovic Henrio, Yannick Zakowski, and Steve Zdancewic. Choice trees. *POPL*, 2023.

[4] Simon L. Peyton Jones and Philip Wadler. Imperative functional programming. In Mary S. Van Deusen and Bernard Lang, editors, *Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, USA, January 1993*, pages 71–84. ACM Press, 1993.

[5] Mohsen Lesani, Li-yao Xia, Anders Kaseorg, Christian J. Bell, Adam Chlipala, Benjamin C. Pierce, and Steve Zdancewic. C4: Verified transactional objects. *Proc. ACM Program. Lang.*, 6(OOPSLA1), apr 2022.

[6] Thomas Letan and Yann Régis-Gianas. Freespec: specifying, verifying, and executing impure computations in Coq. In Jasmin Blanchette and Catalin Hritcu, editors, *Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020*, pages 32–46. ACM, 2020.

[7] Thomas Letan, Yann Régis-Gianas, Pierre Chiflier, and Guillaume Hiet. Modular verification of programs with effects and effect handlers in Coq. In Klaus Havelund, Jan Peleska, Bill Roscoe, and Erik P. de Vink, editors, *Formal Methods - 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FLOC 2018*, volume 10951 of *Lecture Notes in Computer Science*, pages 338–354. Springer, 2018.

[8] Thomas Letan, Yann Régis-Gianas, Pierre Chiflier, and Guillaume Hiet. Modular verification of programs with effects and effect handlers in Coq. In *Formal Methods - 22nd International Symposium, FM 2018*, pages 338–354, 2018.

[9] Kenji Maillard, Cătălin Hrițcu, Exequiel Rivas, and Antoine Van Muylder. The next 700 relational program logics. *POPL*, 4, 2020.

[10] Conor McBride. Turing-completeness totally free. In *Mathematics of Program Construction - 12th International Conference, MPC 2015, Königswinter, Germany, June 29 - July 1, 2015. Proceedings*, pages 257–275, 2015.

[11] Eugenio Moggi. *Computational Lambda-Calculus and Monads*. IEEE Computer Society Press, 1989.

[12] Wouter Swierstra. Data types à la carte. *Journal of Functional Programming*, 18(4):423–436, 2008.

[13] Philip Wadler. Monads for functional programming. In Johan Jeuring and Erik Meijer, editors, *Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques, Båstad, Sweden, May 24-30, 1995, Tutorial Text*, volume 925 of *Lecture Notes in Computer Science*, pages 24–52. Springer, 1995.

[14] Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C. Pierce, and Steve Zdancewic. Interaction trees. *POPL*, 4, 2020.

[15] Irene Yoon, Yannick Zakowski, and Steve Zdancewic. Formal reasoning about layered monadic interpreters. *Proc. ACM Program. Lang.*, 6(ICFP):254–282, 2022.

[16] Yannick Zakowski, Calvin Beck, Irene Yoon, Ilia Zaichuk, Vadim Zaliva, and Steve Zdancewic. Modular, compositional, and executable formal semantics for LLVM IR. *ICFP*, 5, aug 2021.
# Filtrer sans s'appauvrir : inférer les paramètres constants des modèles réactifs probabilistes

Guillaume Baudart,¹² Grégoire Bussone,²³
Louis Mandel,<fnref n="4" /> et Christine Tasson<fnref n="3" />

## Résumé

ProbZelus étend le langage synchrone Zelus pour permettre de décrire des modèles probabilistes synchrones. Là où la programmation synchrone implémente des fonctions de suites, un langage probabiliste synchrone permet de décrire des modèles qui calculent des suites de distributions. On peut par exemple estimer la position d'un objet en mouvement à partir d'observations bruitées ou estimer l'incertitude d'un capteur à partir d'une suite d'observations. Ces problèmes mêlent des flots de variables aléatoires – les *paramètres d'état* qui changent au cours du temps – et des variables aléatoires constantes – les *paramètres constants*.

Pour estimer les paramètres d'état, les algorithmes d'inférence bayésienne de Monte Carlo séquentiels reposent sur des techniques de filtrage. Le filtrage est une méthode approchée qui consiste à perdre volontairement de l'information sur l'approximation actuelle pour recentrer les estimations futures autour de l'information la plus significative. Malheureusement, cette perte d'information est dommageable pour l'estimation des paramètres constants qui n'évoluent pas au cours du temps. Ce phénomène s'appelle l'appauvrissement.

Inspérés de la méthode d'inférence *Assumed Parameter Filter* (APF), nous proposons (1) une analyse statique, (2) une passe de compilation et (3) une nouvelle méthode d'inférence modulaire pour ProbZelus qui évite l'appauvrissement pour les paramètres constants tout en gardant les performances des algorithmes de Monte Carlo séquentiels pour les paramètres d'états.

# 1 Introduction

La programmation synchrone flot de données [5] est un paradigme dans lequel les fonctions, appelées nœuds, manipulent des suites infinies, appelées flots. Ces flots progressent au même rythme, de manière synchrone. L'expressivité des langages synchrones est volontairement restreinte, ce qui permet à des compilateurs spécialisés de générer du code efficace et correct par construction avec de fortes garanties sur le temps d'exécution et sur l'utilisation de la mémoire [19]. Le langage industriel Scade est notamment utilisé pour la conception de systèmes embarqués critiques [13].

Les langages probabilistes [6, 14, 17, 18] étendent des langages de programmation généralistes avec des constructions probabilistes. Suivant la méthode bayésienne, un modèle probabiliste décrit une distribution de probabilité (la distribution *a posteriori*) à partir d'une croyance initiale (la distribution *a priori*) et d'observations concrètes (les entrées).

Dans la même lignée de langages, ProbZelus [2] est une extension probabiliste du langage synchrone flot de données Zelus [8]. Ce langage permet de décrire des modèles réactifs probabilistes. Là où la programmation synchrone implémente des fonctions de suites, un langage probabiliste synchrone permet de décrire des modèles qui calculent des suites de distributions.

<footnote n="1">¹ Inria Paris</footnote>

<footnote n="2">² École normale supérieure – PSL university</footnote>

<footnote n="3">³ Sorbonne Université</footnote>

<footnote n="4">⁴ IBM Research</footnote>
Un exemple est le problème de localisation et cartographie simultanées (SLAM pour *Simultaneous Localization and Mapping*) [20]. Un robot cherche à inférer à la fois sa position et une carte de son environnement. La position est un *paramètre d'état* représenté par un flot de variables aléatoires. À chaque instant, une nouvelle position doit être estimée à partir de la position précédente et des nouvelles observations. La carte est un *paramètre constant* représenté par une variable aléatoire dont la valeur est progressivement affinée à chaque nouvelle observation à partir d'une croyance initiale, la distribution *a priori*. Ce type de problème qui mêle paramètres constants et paramètres d'état qui changent au cours du temps est appelé *State-Space Models* (SSM) [10]. Tout programme probabiliste synchrone peut s'exprimer comme un SSM.

Pour estimer les paramètres d'état, les algorithmes d'inférence de Monte Carlo séquentiels (SMC pour *Sequential Monte Carlo*) reposent sur des techniques de filtrage [10, 15]. Le filtrage est une méthode approchée qui consiste à perdre volontairement de l'information sur l'approximation actuelle pour recentrer les estimations futures autour de l'information la plus significative. Ces méthodes sont donc particulièrement bien adaptées au contexte réactif où un système en interaction avec son environnement ne s'arrête jamais et doit donc s'exécuter avec des ressources bornées. Toutes les méthodes d'inférence de ProbZelus appartiennent à cette famille [1–3]. Malheureusement, cette perte d'information est dommageable pour l'estimation des paramètres constants qui n'évoluent pas au cours du temps. Ce phénomène s'appelle l'appauvrissement.

Pour éviter ce problème, l'algorithme d'inférence *Assumed Parameter Filter* (APF) [16] propose, à chaque instant, de décomposer l'inférence en deux temps : (1) estimation des paramètres d'état, et (2) mise à jour des paramètres constants. Cette méthode suppose que les paramètres constants sont bien identifiés et que le modèle est écrit sous une forme qui permet de mettre à jour les distributions des paramètres constants sachant la valeur des paramètres d'état.

Dans cet article, nous proposons une nouvelle méthode d'inférence fondée sur APF pour ProbZelus. Nous présentons en particulier les contributions suivantes : Section 3 une analyse statique pour identifier les paramètres constants, Section 4 une passe de compilation pour générer un modèle exploitable par APF, Section 5 une implémentation de l'algorithme APF pour les modèles ProbZelus. Nous évaluons cette nouvelle méthode d'inférence sur un ensemble de modèles ProbZelus. Le code et une annexe contenant la preuve du théorème principal sont disponibles à l'adresse suivante : https://github.com/rpl-lab/jfla23-apf.

# 2 Motivation

Pour motiver notre approche, considérons l'exemple d'un radar adapté de [10, Section 2.4.1] illustré Figure 1. On cherche à estimer la position $x_t$ d'un bateau au cours du temps à partir d'une mesure de distance (par exemple à l'aide d'un sonar), et d'une mesure angulaire. On suppose que le bateau dérive à vitesse constante $\theta$ et on cherche également à estimer cette vitesse. Ce modèle est donc un *State-Space Model* (SSM). On s'intéresse à la distribution d'un paramètre d'état (le flot de variables aléatoires $x_t$) et d'un paramètre constant (la variable aléatoire $\theta$).

## 2.1 Un modèle de radar en ProbZelus

Un premier modèle probabiliste décrit le mouvement du bateau, c'est-à-dire à chaque instant $t > 0$, la distribution *a priori* des variables $\theta$ et $x_t$ en fonction de la position précédente $x_{t-1}$.

```r
proba move x0 = theta, x where
    rec init theta = sample(mv_gaussian(zeros, i2))
    and x = x0 --> sample(mv_gaussian(pre x +@ theta, 0.5 *@ i2))
```
<figure><img src="image_31.png" /><figcaption>FIGURE 1 – Le radar cherche à estimer la position courante du bateau $x_t$ et sa vitesse de dérive constante $\theta$ à partir du délai de rebond d'un sonar $\delta_t$ et d'une observation angulaire $\alpha_t$.</figcaption></figure>

Le mot-clé **proba** introduit un modèle probabiliste appelé **move** qui prend en argument la position initiale $x_0$ et renvoie, à chaque instant, la vitesse **theta** et la position courante **x**. Les variables $x_0$, **theta**, et **x** sont des vecteurs à deux dimensions dans $\mathbb{R}^2$. Le paramètre constant **theta** est introduit par le mot-clé **init**. Ici, on suppose *a priori*, que **theta** est échantillonnée dans une gaussienne multivariée centrée sur $(0,0)^T$ et de covariance $I_2$, la matrice identité de dimension 2 (on suppose que les deux composantes de la vitesse ne sont pas corrélées). La définition de la position **x** utilise les opérateurs d'initialisation $\rightarrow$ et de délai unitaire **pre**. Au premier instant, $x_0 = x_0$. Puis, aux instants $t > 0$ suivants, $x_t$ est échantillonnée dans une gaussienne centrée sur la valeur précédente $x_{t-1}$ translatée de **theta** et de covariance $0.5 * I_2$. Le paramètre d'état **x** est donc un flot de variables aléatoires.

Le modèle de radar suivant définit, à chaque instant, la distribution *a posteriori* de la vitesse du bateau et de sa position à partir des distributions *a priori* générées par **move**, et de deux observations bruitées : **delta** le délai de rebond du sonar et **alpha** la mesure angulaire.

```R
proba radar (delta, alpha) = theta, x where
  rec theta, x = move x0
  and d = sqrt((vec_get x 0) ** 2. + (vec_get x 1) ** 2.)
  and a = atan(vec_get x 1 / vec_get x 0)
  and () = observe(gaussian(2. * d / c, delta_noise), delta)
  and () = observe(gaussian(a, alpha_noise), alpha)
```

À partir de la vitesse **theta** et de la position courante **x** = ($x_1, x_2$)$^T$ estimée, on calcule la distance $d = \sqrt{x_1^2 + x_2^2}$, et l'angle $\alpha = atan(x_2/x_1)$. La construction **observe** permet ensuite de contraindre le modèle en supposant (1) que le temps de rebond observé **delta** a été échantillonné dans une gaussienne centrée sur $2d/c$ (où c est la vitesse du signal envoyé par le sonar), et (2) que la mesure angulaire $\alpha$ a été échantillonnée dans une gaussienne centrée sur $\alpha$.

Finalement, le nœud **main** prend en argument les flots d'observations **delta** et **alpha** et lance l'inférence sur le modèle **radar** pour calculer à chaque instant une approximation $d\_\theta$ de la distribution de la vitesse **theta** et une approximation $d\_x$ de la distribution de la position **x**.

```R
node main (delta, alpha) = d_theta, d_x where
  rec d = infer radar (delta, alpha)
  and d_theta, d_x = Dist.split d
```
**Données** : le modèle *model*, l'entrée $y_t$ et le résultat précédent $\mu_{t-1}$.

**Résultat** : $\mu_t$ une approximation de la distribution de $p_t$.

pour chaque particule $i = 1 \text{ à } N$ faire

$$ \left| \begin{array}{l} p_t^i = \text{sample}(\mu_{t-1}) \\ p_t^i, w_t^i = \text{model}(y_t | p_{t-1}^i) \end{array} \right. $$

$$ \mu_t = \mathcal{M}(\{w_t^i, p_t^i\}_{1\le i\le N}) $$

renvoyer $\mu_t$

**Algorithme 1** : Filtre particulaire.

Le mot-clé *node* introduit un nœud déterministe classique. La fonction *Dist.split* sépare une distribution sur des paires (ici *theta*, et *x*) en une paire de distributions. On peut ensuite analyser ces distributions en calculant moyennes, quantiles, etc. ou en affichant un nuage d'échantillons tirés dans la distribution comme dans la Figure 2.

## 2.2 Le filtrage et ses limites

Les méthodes d'inférence proposées par ProbZelus [1–3] appartiennent à la famille des algorithmes de Monte Carlo séquentiels [10, 15].

Ces méthodes reposent sur un ensemble de simulations indépendantes, appelées *particules*. Chaque particule renvoie une valeur de sortie associée à un score. Le score représente la qualité de la simulation. Un grand nombre de particules permet d'approximer la distribution recherchée. La construction *sample(d)* tire aléatoirement une valeur dans la distribution *d*, et la construction *observe(d, x)* modifie le score courant de la particule en lui ajoutant la *vraisemblance* de l'observation *x* par rapport à la distribution *d*. À chaque instant, l'opérateur *infer* accumule les valeurs calculées par chaque particule pondérées par leurs scores pour approximer la distribution *a posteriori*.

**Filtre particulaire.** Si le modèle fait appel à l'opérateur *sample* à chaque instant, par exemple pour estimer la position du bateau, la méthode précédente implémente une simple marche aléatoire pour chaque particule. À mesure que le temps avance, il devient de plus en plus improbable qu'une des marches aléatoires coïncide avec le flot d'observations. Le score associé à chaque particule dégringole rapidement vers 0.

Pour régler ce problème, les méthodes de Monte Carlo séquentielles ajoutent une étape de filtrage. L'Algorithme 1 décrit ainsi l'exécution d'un instant pour un filtre particulaire. À chaque instant $t$, une particule $1 \le i \le N$ correspond à une valeur possible des paramètres (i.e., variables aléatoires) $p_t^i$ du modèle. On commence par échantillonner un nouvel ensemble de particules dans la distribution obtenue à l'instant précédent. Les particules les plus probables sont ainsi dupliquées et les moins probables sont éliminées. On recentre ainsi l'inférence autour de l'information la plus significative tout en conservant le même nombre de particules tout au long de l'exécution. Sachant l'état précédent $p_{t-1}^i$, chaque particule exécute ensuite un pas du modèle pour obtenir un échantillon des paramètres $p_t^i$ associé à un score $w_t^i$. À la fin de l'instant, on construit une distribution $\mu_t$ où chaque particule est associée à son score. $\mathcal{M}(\{w_t^i, p_t^i\}_{1\le i\le N})$ est une distribution multinomiale, où la valeur $p_t^i$ est associée à la probabilité $w_t^i$.<fnref n="1" />

**Appauvrissement.** Malheureusement, cette approche engendre une perte d'information dommageable pour l'estimation de paramètres constants. Sur l'exemple du radar, au premier

<footnote n="1">1. On note $\overline{w}_t^i = w_t^i / \sum_{i=1}^N w_t^i$ les scores normalisés.</footnote>
<figure><img src="image_32.png" /><figcaption>FIGURE 2 – Estimations du paramètre theta de l'exemple du radar au cours du temps avec un filtre particulaire (PF, en haut) et Assumed Parameter Filter (APF, en bas). La vraie vitesse de dérive est indiquée par une croix verte. Le gradient de couleur représente la densité de points. L'échelle change au cours du temps. Les résultats peuvent différer d'une exécution à l'autre.</figcaption></figure>

instant, chaque particule tire une valeur aléatoire pour le paramètre theta. À chaque instant, les particules dupliquées partagent la même valeur pour theta. La quantité d'information utile pour estimer theta décroît donc à chaque nouveau filtrage et, au bout d'un certain temps, il ne reste plus qu'une seule valeur possible. La partie haute de la Figure 2 illustre graphiquement ce phénomène.

Plus formellement, on peut montrer que le filtre particulaire souffre d'appauvrissement sur les paramètres constants quel que soit le modèle.

**Proposition 1 (Appauvrissement).** *Considérons un filtre particulaire avec $N \in \mathbb{N}^*$ particules pour estimer un paramètre constant $\theta$ à valeur dans $V$. À chaque instant, on note $\Theta_t \in V^N$ l'estimation obtenue à l'instant $t \in \mathbb{N}$, par définition un ensemble de valeurs possibles pour $\theta$. Il existe presque sûrement un instant $T \in \mathbb{N}$ tel que $\forall t > T, |\Theta_t| = 1$.*

*Démonstration.* On note à chaque instant $t \in \mathbb{N}$, $\Theta_t = \{\theta_t^i\}_{1\le i\le N}$ l'ensemble des valeurs possibles et $w(\theta_t^i) \in ]0, \infty[$ le score associé à la valeur $\theta_t^i$. À chaque filtrage, $\theta_t^i$ est dupliquée avec la probabilité $w(\theta_t^i)$ (le score normalisé de $\theta_t^i$). Pour $t \in \mathbb{N}$, s'il reste au moins deux particules distinctes $|\Theta_t| \ge 2$, on note $A$ la valeur de $\Theta_t$ associée au score minimal qui a donc le plus de chances d'être éliminée : $A = \underset{a \in \Theta_t}{\operatorname{argmin}} \sum_{\theta_t^i=a} w(\theta_t^i)$. On a donc $\forall 1 \le i \le N$, $\mathbb{P}(\theta_{t+1}^i = A) \le \frac{1}{2}$ et :

$$ \mathbb{P}(\exists a. a \in \Theta_t \text{ et } a \notin \Theta_{t+1}) \geq \mathbb{P}(A \notin \Theta_{t+1}) = \prod_{i=1}^{N} \mathbb{P}(\theta_{t+1}^i \neq A) \geq \frac{1}{2^N} = \epsilon > 0. $$

Comme $\epsilon$ ne dépend que de $N$, $\forall n \in \mathbb{N}$, on a : $\mathbb{P}(\Theta_{t+n} = \Theta_t) \le (1-\epsilon)^n$. Il existe donc presque sûrement $t' > t$ tel que $\Theta_{t'} \subsetneq \Theta_t$. Par récurrence sur la taille de $\Theta_0$, il existe presque sûrement $T \in \mathbb{N}$ tel que $|\Theta_T| = 1$. $\square$
**Données** : le modèle *model*, l'entrée $y_t$ et le résultat précédent $\mu_{t-1}$.

**Résultat** : $\mu_t$ une approximation de la distribution de $x_t$ (état) et $\theta$ (constant).

pour chaque particule $i = 1 \text{ à } N$ faire
$$ 
\begin{aligned}
x_{t-1}^i, \Theta_{t-1}^i &= \text{sample}(\mu_{t-1}) \\
\theta^i &= \text{sample}(\Theta_{t-1}^i) \\
x_t^i, w_t^i &= \text{model}(y_t | \theta^i, x_{t-1}^i) \\
\Theta_t^i &= \text{Udpate}(\Theta_{t-1}^i, \lambda\theta. \text{model}(y_t | \theta, x_{t-1}^i, x_t^i))
\end{aligned}
$$
$\mu_t = \mathcal{M}(\{w_t^i, (x_t^i, \Theta_t^i)\}_{1\le i\le N})$
renvoyer $\mu_t$

<caption>**Algorithme 2** : *Assumed Parameter Filter* [16]</caption>

## 2.3 Assumed Parameter Filter

Plutôt que d'échantillonner au début de l'exécution un ensemble de valeurs pour les paramètres constants qui s'appauvrira à chaque filtrage, dans l'algorithme *Assumed Parameter Filter* (APF) [16], chaque particule calcule une distribution symbolique de paramètres constants. Lors de l'exécution, l'inférence alterne ensuite entre une passe d'échantillonnage pour estimer les paramètres d'état, et une passe d'optimisation qui permet de mettre à jour les paramètres constants. On évite ainsi l'appauvrissement pour l'estimation des paramètres constants. La partie basse de la Figure 2 illustre les résultats de APF sur l'exemple du radar.

Plus formellement, l'Algorithme 2 décrit l'exécution d'un instant de APF. À chaque instant $t$, une particule $1 \le i \le N$ correspond maintenant à une valeur possible des paramètres d'état $x_i^t$ et une distribution de paramètres constants $\Theta_i^t$. Comme pour le filtre particulaire, on commence par échantillonner un ensemble de particules dans la distribution obtenue à l'instant précédent. On échantillonne ensuite une valeur $\theta^i$ dans $\Theta_{t-1}^i$. Sachant la valeur des paramètres constants $\theta^i$ et l'état précédent $x_{t-1}^i$, on peut exécuter un pas du modèle pour obtenir un échantillon des paramètres d'état $x_t^i$ associé à un score $w_t^i$. Il reste alors à calculer $\Theta_t^i$ en explorant les autres valeurs possibles pour $\theta$ sachant que la particule a choisi la transition $x_{t-1}^i \to x_t^i$. À la fin de l'instant, comme pour le filtre particulaire de l'Algorithme 1, on construit une distribution $\mu_t$ où chaque particule est associée à son score.

La difficulté principale est qu'à chaque instant, l'Algorithme 2 doit ré-exécuter plusieurs fois le modèle en fixant la valeur de certaines variables aléatoires. D'abord pour calculer les paramètres d'état sachant la valeur échantillonnée $\theta^i$, puis pour mettre à jour la distribution $\Theta_t^i$ en explorant plusieurs valeurs possibles pour $\theta$, sachant la transition $x_{t-1}^i \to x_t^i$.

Pour implémenter APF pour des modèles ProbZelus arbitraires, nous proposons donc une analyse statique pour identifier les paramètres constants et leur distributions *a priori* (Section 3) et une passe de compilation qui transforme ces paramètres en entrée supplémentaire du modèle (Section 4).

## 3 Analyse Statique

Dans cette section, nous présentons un noyau de ProbZelus. L'ensemble du langage, y compris les structures de contrôle de haut niveau comme les automates hiérarchiques, peut être compilé vers ce noyau [12]. Nous présentons ensuite l'analyse statique qui permet d'identifier les paramètres constants et leur distribution *a priori* sur ce noyau.
<figure><img src="image_33.png" /><figcaption>FIGURE 3 – Syntaxe du noyau de ProbZelus</figcaption></figure>

## 3.1 Un noyau de ProbZelus

La syntaxe du noyau de ProbZelus est présentée dans la Figure 3. Un programme est une série de déclarations *d*. Une déclaration peut donner un nom au résultat d'une expression (*let* *x* = *e*) ou définir un nœud déterministe (*node* *f* *x* = *e*) ou probabiliste (*proba* *f* *x* = *e*). Le nom de chaque déclaration est unique. Une expression peut être une constante (*c*), une variable (*x*), une paire ((*e*, *e*)), l'application d'une primitive (*op*(*e*)), un appel de nœud (*f*<sup>α</sup>(*e*)), un délai (*last* *x*), un ensemble d'équations locales mutuellement récursives (*e* where *rec* *E*), une structure de contrôle (*present* *e* -> *e* *else* *e*), une structure de réinitialisation (*reset* *e* every *e*) ou une construction probabiliste (*sample*(*e*), *observe*(*e*, *e*) ou *infer*(*f*(*e*)).

On impose que toutes les variables initialisées soient définies par une équation, quitte à ajouter *x* = *last* *x*, et que les équations soient ordonnancées. Dans une expression de la forme *e* where *rec* (*init* *x*<sub>*i*</sub> = *e*<sub>*i*</sub>)<sub>1≤*i*≤*k*</sub> and (*y*<sub>*j*</sub> = *e*'<sub>*j*</sub>)<sub>1≤*j*≤*n*</sub>, on a donc {*x*<sub>*i*</sub>}<sub>1≤*i*≤*k*</sub> ⊂ {*y*<sub>*j*</sub>}<sub>1≤*j*≤*n*</sub> et *e*'<sub>*j*</sub> ne peut dépendre de *y*'<sub>*j*</sub> avec *j* ≤ *j*' qu'à travers l'opérateur *last*.

Ce noyau est proche de celui utilisé pour définir la sémantique formelle de ProbZelus [2]. La différence principale est qu'il est possible d'initialiser une variable avec une expression arbitraire là où le noyau original limitait la construction *init* à des constantes : *init* *x* = *c*. On autorise ainsi *init* *x* = *sample*(*d*) and *x* = *last* *x* pour définir des paramètres constants. Par ailleurs, on autorise la définition des variables globales dans les déclarations. Enfin, l'appel de nœud *f*<sup>α</sup>(*e*) est ici annoté avec un nom d'instance *α* ajouté automatiquement par le compilateur qui permet de différencier les appels à une même fonction. Par exemple, l'expression *f*(*θ*) + *f*(*1*) devient dans ce noyau *f*<sup>α<sub>1</sub></sup>(*θ*) + *f*<sup>α<sub>2</sub></sup>(*1*).

**Sémantique.** La sémantique formelle de ProbZelus est définie dans [2]. Dans un environnement *γ* qui associe les noms de variables à leur valeur, les expressions déterministes sont des machines à états caractérisées par un état initial [[*e*]]<sub>*γ*</sub><sup>init</sup> de type *S* et une fonction de transition [[*e*]]<sub>*γ*</sub><sup>step</sup> de type *S* → *O* × *S*. La fonction de transition prend en entrée un état et renvoie une sortie et l'état suivant. On obtient un flot de données en itérant la fonction de transition depuis l'état initial.

Les expressions probabilistes sont elles aussi caractérisées par un état initial de type *S*, mais la fonction de transition [[*e*]]<sub>*γ*</sub><sup>step</sup> de type *S* → Σ<sub>*O*×*S*</sub> → [0, ∞) renvoie une mesure qui associe un score positif à chaque ensemble mesurable de paires (sortie, état suivant) ∈ Σ<sub>*O*×*S*</sub>.

## 3.2 Identifier les paramètres constants

L'analyse statique est définie par un jugement ∅, ∅ ⊢ *prog* : *H*, *C* qui, pour un programme *prog*, construit un environnement *H* associant à chaque nœud probabiliste un type *ξ* qui identifie les paramètres constants du nœud et leur distribution *a priori* (l'environnement *C* contient les variables globales constantes). Pour un nœud *proba* *f* *x* = *e*, le type *ξ* est une fonction telle que chaque variable *x* dans *dom*(*ξ*) est un paramètre constant dans *e* de distribution *a priori* *ξ*(*x*).
<figure><img src="image_34.png" /><figcaption>FIGURE 4 – Identification des paramètres constants avec leurs distributions a priori.</figcaption></figure>

<figure><img src="image_35.png" /><figcaption>FIGURE 5 – Distribution échantillonnée.</figcaption></figure>

Le jugement de typage des expressions est de la forme $C \vdash e : \xi$ et repose sur deux jugements auxiliaires : le jugement $\vdash^p e : d$ qui extrait la distribution $d$ échantillonnée par $e$, et le jugement $C \vdash^l e$ qui garantit que l'expression $e$ est constante et ne dépend que des variables constantes définies dans l'ensemble $C$.

**Paramètres constants.** Le jugement principal $C \vdash e : \xi$ est défini Figure 4. Pour simplifier l'analyse, on suppose que toutes les variables et les instances ont des noms différents. Une passe de renommage des variables permet facilement de satisfaire cette précondition. Toutes les règles parcourent les sous-expressions pour collecter les paramètres constants. La règle pour reset $e_1$ every $e_2$ parcourt uniquement $e_2$ car l'expression $e_1$ peut être réinitialisée et donc n'est pas constante. Pour une raison similaire, la règle pour present $e_1$ $\rightarrow$ $e_2$ else $e_3$ ne parcourt que $e_1$. La règle pour $f^\alpha(e)$ associe dans $\xi$ le nom d'instance $\alpha$ avec la distribution a priori de $f$ que l'on suppose définie dans la variable $f\_prior$ (qui sera ajoutée par la compilation). La règle pour l'expression e where rec (init $x_i = e_i$)$_{1\le i\le k}$ and ($y_j = e'_j$)$_{1\le j\le n}$ ajoute dans $\xi$ les variables $x_i$ qui respectent les conditions suivantes.

1. Elle n'est pas modifiée par la fonction de transition ($x_i = y_j \land e'_j = \text{last } y_j$).

2. Elle échantillonne une distribution $d_i$ ($\vdash^p e_i : d_i$).

3. La distribution $d_i$ est constante et ne dépend que des constantes dans $C$ ($C \vdash^l d_i$).
<figure><img src="image_36.png" /><figcaption>FIGURE 6 – Expressions constantes.</figcaption></figure>

L'analyse d'un nœud probabiliste f type le corps e du nœud et ajoute ce type dans l'environnement H associé au nom f. Les nœuds déterministes n'ont pas de variables aléatoires par définition. Les déclarations globales doivent être constantes, leurs noms sont ajoutés dans l'ensemble C des variables constantes.

**Distributions.** Le jugement $\vdash^p e : d$, défini Figure 5, garantit que l'expression e échantillonne une distribution d. La règle principale est donc celle de `sample(d)` qui renvoie la distribution d. La règle pour where rec autorise l'utilisation de variables locales pour définir la distribution échantillonnée.

**Constantes.** Le jugement $C \vdash^l e$, défini Figure 6, garantit que l'expression e est constante en vérifiant que toutes les sous-expressions sont constantes et ne dépendent que de variables constantes.

*Exemple. Illustrons l'analyse statique sur l'exemple du nœud move de la Section 2. L'équation theta = last theta est ajoutée automatiquement par le compilateur.*

```
prob a move x0 = theta, x where
    rec init theta = sample(mv_gaussian(zeros, i2))
    and x = x0 --> sample(mv_gaussian(pre x +@ theta, 0.5 *@ i2))
    and theta = last theta
```

La règle `prob a` type le corps du nœud en utilisant la règle `where rec`. Le typage de chaque sous-expression renvoie un ensemble vide (aucun paramètre constant local n'est défini). Le système détecte que `theta` est un flot constant (`init theta = ...` and `theta = last theta`), donc l'expression `sample(mv_gaussian(zeros, i2))` est analysée avec le jugement $\vdash^p$ qui renvoie la distribution `mv_gaussian(zeros, i2)`. Cette distribution est typée avec succès par le jugement $\vdash^l$ dans l'environnement C qui contient les constantes zeros et i2. Ainsi le corps du nœud `move` a le type `{ theta ← mv_gaussian(zeros, i2) }` et le nœud a le type `{ move ← { theta ← mv_gaussian(zeros, i2) } }`.

# 4 Compilation

Pour exécuter l'algorithm e APF présenté en Section 2.3, il faut maintenant compiler les modèles probabilistes pour que les paramètres constants deviennent une entrée supplémentaire. On pourra ainsi ré-exécuter le modèle en explorant différentes valeurs pour mettre à jour la distribution des paramètres constants. La compilation est définie Figure 7 par induction sur la syntaxe du noyau. On commence par typer le programme complet, c'est-à-dire une liste de déclarations $p = d_1 ... d_n$ dans un environnement vide : $\emptyset, \emptyset \vdash p : H, C$. La fonction de compilation C est ensuite paramétrée par l'environnement de typage H pour les déclarations, et le type $\xi$ pour les expressions (voir Section 3).
<figure><img src="image_37.png" /><figcaption>FIGURE 7 – Fonction de compilation d'un programme ProbZelus pour APF. La fonction de compilation est paramétrée par le type $\xi$ pour les expressions et l'environnement de typage $H$ pour les déclarations (voir Section 3).</figcaption></figure>

**Modèles.** Pour un modèle `proba f x = e`, si après l'analyse statique $H(f) = \xi$ (i.e., $C \vdash e : \xi$), alors $f$ est compilé en deux déclarations :

- `let f prior = img(\xi)` : la distribution a priori des paramètres constants dans $e$, et

- `proba f model (dom(\xi), x) = C_\xi(e)` : un nouveau modèle qui prend en argument supplémentaire `dom(\xi)` pour les paramètres constants.

**Expressions.** La fonction de compilation d'une expression est paramétrée par le type $\xi$ du nœud qui la contient. Cette fonction supprime les définitions de paramètres constants, $x \in dom(\xi)$, qui sont passés en entrée du nouveau modèle. Les premiers cas dans la Figure 7, de $c$ à `observe`, implémentent une simple descente récursive sur les sous-expressions. Le cas `where/rec` supprime effectivement les paramètres constants en ne gardant que les équations définissant les variables $x$ telles que $x \notin dom(\xi)$.

*Exemple.* Après compilation, le nœud `move` de l'exemple de la Section 2 devient :

```
let move prior = mv_gaussian(zeros, i2)
proba move model (theta, x0) = theta, x where
    rec x = x0 -> sample(mv_gaussian(pre x +@ theta, 0.5 *@ i2))
```
**Appel de nœud.** La difficulté principale est de faire remonter les paramètres constants introduits par les appels de nœud. On distingue trois cas.

— Si le nœud est déterministe, il n'y a pas de paramètre constant possible.

— Si les paramètres constants de l'appel de nœud sont également des paramètres constants dans le contexte d'appel, on a $\alpha \in \text{dom}(\xi)$ et on se contente de remplacer l'appel à $f^{\alpha}$ par un appel à $f\_\text{model}$ en utilisant le nom frais d'instance pour les paramètres constants.

— Sinon, il existe des paramètres constants dans $f$ qui ne sont pas constants dans le contexte d'appel car l'instance $f^{\alpha}$ est utilisée à l'intérieur d'un reset/every ou d'un present/else. Dans ce cas, on redéfinit localement ces paramètres en échantillonnant leur distribution a priori $f\_\text{prior}$.

Par ailleurs, dans les nœuds déterministes, on substitue l'appel à $\text{infer}(f(e))$ par un appel à APF.infer($f\_\text{prior}, f\_\text{model}, e$).

Exemple. Le nœud radar de la Section 2 devient :

```python
let radar_prior = move_prior
proba radar_model (i_move_0, (delta, alpha)) = theta, x where
    rec theta, x = move_model (i_move_0, x0)
    and d = sqrt((vec_get x 0) ** 2. + (vec_get x 1) ** 2.)
    and a = atan(vec_get x 1 / . vec_get x 0)
    and () = observe(gaussian(2. *. d / . c, delta_noise), delta)
    and () = observe(gaussian(a, alpha_noise), alpha)
```

La variable $i_move_0$ est le nom frais associé à l'instance de move appelée dans radar. Il faut enfin substituer l'appel à infer par un appel à APF.infer dans le nœud main.

```python
node main (delta, alpha) = d_theta, d_x where
    rec d = APF.infer(radar_prior, radar_model, (delta, alpha))
    and d_theta, d_x = Dist.split d
```

**Correction.** La propriété de correction établit que l'inférence appliquée sur un modèle et son compilé définissent les mêmes flots de distributions pour la sémantique idéale de ProbZelus.

Pour tout programme prog tel que $\emptyset, \emptyset \vdash \text{prog} : H, C$, pour tout modèle probabiliste m de prog,

$$[[\text{infer}(m(\text{obs}))]] \equiv [[\text{APF}.\text{infer}(m\_\text{prior}, m\_\text{model}, \text{obs})]]$$

En pratique, le calcul de la distribution a posteriori est un problème intractable, on utilise donc des méthodes approchées. Nous montrons ici que la compilation préserve la sémantique idéale du modèle, mais permet d'utiliser APF pour calculer une meilleure approximation de la distribution définie par le modèle.

**Notations.** Pour une mesure $\mu$, on note $\bar{\mu}$ la distribution normalisée $\mu/\mu(\mathbb{T})$ où $\mathbb{T}$ représente l'ensemble du domaine de définition de $\mu$. On note $f_*(\mu)$ la mesure image par une fonction mesurable $f$ (par exemple, les mesures images par les fonctions de projection $\pi_1$ et $\pi_2$ permettent de séparer une distribution sur des paires en une paire de distributions). On note $\lambda U. \delta(v)(U)$ la mesure de Dirac au point $v$ ($\delta(v)(U) = 1$ si $v \in U$ et $0$ sinon). Enfin on note $\int \mu(dt)f(t)$ l'intégrale de la fonction $f$ le long de la mesure $\mu$ où $t$ est la variable d'intégration.

La sémantique de APF.infer est définie en appliquant infer après avoir échantillonné le paramètre constant $\alpha$ au début de l'exécution.

$$[[\text{APF}.\text{infer}(m\_\text{prior}, m\_\text{model}, \text{obs})]] = [[\text{infer}(m\_\text{model}(\alpha, \text{obs}) \text{ where } \text{rec init } \alpha = \text{sample}(m\_\text{prior}) \text{ and } \alpha = \text{last } \alpha)]]$$
Deux expressions probabilistes sont équivalentes si elles définissent les mêmes flots de distributions. La sémantique est exprimée en terme d'état initial et de fonction de transition, l'équivalence s'exprime donc avec une relation de bisimilarité [22] initialisée sur les états initiaux et propagée à travers les fonctions de transition [9]. La bisimilarité sur les environnements $\gamma_1$ et $\gamma_2$ met en rapport les nœuds probabilistes avec leur version compilée et garantit que toutes les autres valeurs sont identiques.

**Définition 1** (Bisimilarité d'environnements). Pour tout programme prog, pour tous $\gamma_1, \gamma_2, \gamma_1 \equiv \gamma_2$ si pour toute variable $x \in dom(\gamma_1) \cap dom(\gamma_2)$, $\gamma_1(x) = \gamma_2(x)$ et pour tout nœud probabiliste proba $m x = e$ tel que $C \vdash e : \xi$ dans prog.

$$ \left\{ \begin{array}{l} \gamma_1(m\_init) = \llbracket e \rrbracket_{\gamma_1}^{\text{init}} \\ \gamma_1(m\_step) = \lambda v. \llbracket e \rrbracket_{\gamma_1[x \leftarrow v]}^{\text{step}} \quad \text{et} \\ \qquad \gamma_2(m\_model\_init) = \llbracket C_{\xi}(e) \rrbracket_{\gamma_2}^{\text{init}} \\ \qquad \gamma_2(m\_model\_step) = \lambda(\theta, v). \llbracket C_{\xi}(e) \rrbracket_{\gamma_2[dom(\xi) \leftarrow \theta][x \leftarrow v]}^{\text{step}} \\ \qquad \gamma_2(m\_prior) = \text{img}(\xi) \end{array} \right. $$

La bisimilarité sur les expressions probabilistes met en rapport les flots de mesures renvoyées à chaque instant par les fonctions de transition.

**Définition 2** (Bisimilarité probabiliste). Soient $e_1$ et $e_2$ des expressions probabilistes, et une bisimulation $\mathcal{P} \subseteq S$ dist $\times$ S dist entre les distributions d'états. $\llbracket e_1 \rrbracket \equiv_{\mathcal{P}} \llbracket e_2 \rrbracket$ lorsque :

- pour tout $\gamma_1 \equiv \gamma_2$, $\delta(\llbracket e_1 \rrbracket_{\gamma_1}^{\text{init}}), \delta(\llbracket e_2 \rrbracket_{\gamma_2}^{\text{init}})) \in \mathcal{P}$ et

- pour tout $\gamma_1 \equiv \gamma_2$, si $(\sigma_1, \sigma_2) \in \mathcal{P}$

$$ \left\{ \begin{array}{l} \mu_1 = \lambda U. \int \sigma_1(ds_1) \llbracket e_1 \rrbracket_{\gamma_1}^{\text{step}}(s_1)(U), \quad o_1 = \pi_{1*}(\bar{\mu}_1), \sigma'_1 = \pi_{2*}(\bar{\mu}_1) \\ \mu_2 = \lambda U. \int \sigma_2(ds_2) \llbracket e_2 \rrbracket_{\gamma_2}^{\text{step}}(s_2)(U), \quad o_2 = \pi_{1*}(\bar{\mu}_2), \sigma'_2 = \pi_{2*}(\bar{\mu}_2) \end{array} \right. \quad \text{alors} \quad \left\{ \begin{array}{l} (\sigma'_1, \sigma'_2) \in \mathcal{P} \\ o_1 = o_2 \end{array} \right. $$

Nous prouvons la correction de la compilation dans un cadre simplifié.

**Théorème 1.** Pour tout programme prog tel que $\emptyset, \emptyset \vdash \text{prog} : H, C$, pour tout modèle probabiliste $m$ de prog sous la forme proba $m x = e$ where rec init $\theta = \text{sample}(d)$ and $\theta = \text{last } \theta$, avec $H(m) = \{\theta \leftarrow d\}$, où $e$ ne contient pas d'appel de nœud, alors $\llbracket \text{infer}(m(\text{obs})) \rrbracket \equiv \llbracket \text{APF}.\text{infer}(m\_prior, m\_model, \text{obs}) \rrbracket$.

Les contraintes sur $m$ ne sont pas excessives : $e$ peut contenir des définitions locales, $\theta$ peut être un tuple de paramètres constants, et on peut inliner les appels de nœuds. De plus, on peut imaginer une analyse statique qui permet de vérifier que $m$ est sous la bonne forme.

**Démonstration.** Vue la sémantique de infer et APF.infer, il suffit de montrer que : $\llbracket m(\text{obs}) \rrbracket \equiv_{\mathcal{P}} \llbracket m\_model(\alpha, \text{obs}) \text{ where rec init } \alpha = \text{sample}(m\_prior) \text{ and } \alpha = \text{last } \alpha \rrbracket$ pour une bisimulation $\mathcal{P}$. Comme $H(m) = \{\theta \leftarrow d\}$, alors $C \vdash e : \emptyset$ car le seul paramètre constant, $\theta$, est défini à l'extérieur de $e$ et donc $C_\emptyset(e) = e$. On pose $(\sigma_1, \sigma_2) \in \mathcal{P}$ ssi il existe $\sigma$ tel que $\sigma_1 = \lambda U. \int \sigma(dm, ds)\delta((\cdot), (m, (\cdot), s))(U)$ et $\sigma_2 = \lambda U. \int \sigma(dm, ds)\delta(m, (\cdot), (((\cdot), (\cdot), s))(U)$. On vérifie alors que $\mathcal{P}$ relie les états initiaux et se propage à travers les fonctions de transition ce qui suppose de dérouler et faire commuter les intégrales imbriquées introduites par les environnements locaux. $\square$

# 5 Implémentation

Il reste maintenant à implémenter la construction APF.infer. Dans cette section, nous décrivons d'abord comment implémenter les méthodes de Monte Carlo séquentielles (SMC) pour les machines à états produites par la compilation d'un programme synchrone. Nous détaillons ensuite l'implémentation de Assumed Parameter Filter comme un cas particulier de SMC.
## 5.1 Méthodes de Monte Carlo séquentielles

Zelus compile les nœuds en machines à états. Une machine est une structure qui définit les méthodes suivantes : `alloc` alloue la mémoire nécessaire pour stocker l'état, `reset` réinitialise l'état en place, et `step` implémente la fonction de transition qui met à jour l'état en place. La mémoire est donc allouée statiquement avant l'exécution. Pour implémenter le filtrage, le compilateur génère également une méthode `copy` qui copie l'état d'une particule source dans celui d'une particule cible. En OCaml, on a ainsi<fnref n="2" /> :

```hml
type (α, β) cnode = Cnode: { alloc : unit → 's;
                                reset : 's → unit;
                                step : 's → α → β;
                                copy : 's → 's → unit; } → (α, β) cnode
```

Les nœuds probabilistes sont également des machines à état mais la fonction `step` prend un argument supplémentaire `prob` qui contient les informations nécessaires à l'inférence :

```hml
type (α, β) pnode = (prob * α, β) cnode
```

Les méthodes de Monte Carlo séquentielles utilisent un ensemble de simulations indépendantes, les *particules*, associées à un score pour approximer la distribution recherchée. En pratique, au cours d'une simulation les constructions probabilistes `sample` et `observe` utilisent l'argument supplémentaire `prob` pour mettre à jour le score de la particule.

```hml
type prob = {id : int; scores : float array}
```

```hml
let sample (prob, d) = draw d
```

```hml
let observe (prob, d, x) = prob.scores.(prob.id) ← prob.scores.(prob.id) +. logpdf d x
```

Le type `prob` contient un identifiant de particule `id`, et le tableau de scores `scores`. `sample` tire un échantillon aléatoire dans la distribution `d`, et `observe` incrémente le score de la particule avec la vraisemblance de l'observation, *i.e.*, la valeur de la densité au point d'observation $d_{pdf}(x)$. On calcule les scores en échelle logarithmique pour des raisons de stabilité numérique.

L'opérateur `infer` est un nœud d'ordre supérieur qui transforme une machine probabiliste de type $(\alpha, \beta)$ `pnode` en une machine déterministe de type $(\alpha, \beta \text{ dist})$ `cnode` qui calcule un flot de distributions. L'implémentation de `infer` suit de près l'Algorithmme 1 présenté dans la Section 2.

```hml
type α infer_state = {mutable sigma : α dist}
```

```hml
let infer n particle =
```

```hml
let Cnode {alloc; reset; step; copy} = particle in
```

```hml
let i_alloc () = {sigma = dirac (alloc ())) in
```

```hml
let i_reset state =
```

```hml
let s = Dist.draw state.sigma in
```

```hml
reset s; state.sigma ← dirac (s)
```

```hml
in
```

```hml
let i_step state obs =
```

```hml
let particles = Array.init n (fun _ → let p = alloc () in
```

```hml
let s = Dist.draw state.sigma in
```

```hml
copy s p; p) in
```

```hml
let scores = Array.make n 0. in
```

```hml
let values = Array.mapi (fun i s → step s ({id = i; scores}, obs)) particles in
```

<footnote n="2">2. Voir le fichier `lib/std/ztype.ml` du compilateur Zelus https://github.com/inria/zelus.</footnote>
```
state.sigma ← multinomial particles scores;
multinomial values scores
in
let i_copy src dst = dst.sigma ← src.sigma in
Cnode {alloc = i_alloc; reset = i_reset; step = i_step; copy = i_copy}
```

L'opérateur infer prend en arguments un nombre de particules n et une machine probabiliste particle. L'état mémoire de infer est une distribution d'états possibles initialisé par la fonction i_alloc avec une distribution de Dirac sur l'état initial des particules. La fonction de transition i_step commence par échantillonner un tableau de particules dans la distribution d'états : c'est le filtrage. On itère ensuite la fonction de transition des particules step sur le tableau particles pour mettre à jour l'état de chaque particule et calculer les valeurs de sortie. On utilise un tableau scores pour stocker les scores obtenus. Pour chaque particule l'argument prob prend la valeur `{id = i; scores}` qui permet de lier la case scores.(i) à la particule i. On peut enfin mettre à jour l'état de infer avec une distribution multinomiale sur les particules, et renvoyer la distribution de sortie : une distribution multinomiale sur les valeurs.

Un filtre particulaire est un cas particulier simple de SMC où chaque particule se contente d'exécuter le modèle pour obtenir une valeur de sortie et un score.

```
let infer_pv n model = infer n model
```

*Remarque.* Cette implémentation suit de près la sémantique idéale de ProbZelus [2] mais la fonction de transition alloue de la mémoire à chaque itération. En pratique, le nombre de particules est fixé. On peut donc allouer statiquement toute la mémoire nécessaire dans l'état et utiliser uniquement des modifications en place dans la fonction de transition.

## 5.2 Assumed Parameter Filter

*Assumed Parameter Filter* est également un cas particulier de SMC qui utilise des particules plus avancées. La fonction de transition des particules suit l'Algorithme 2 décrit dans la Section 2.3. En plus de l'état et du score, chaque particule maintient une distribution de paramètres constants $\Theta^i$ qui est mise à jour à chaque instant.

Pour mettre à jour $\Theta^i$, il faut être capable de mesurer la vraisemblance d'une exécution où seule la valeur des paramètres constants $\theta$ a changé : $\Theta_t^i = \text{Udpate}(\Theta_{t-1}^i, \lambda\theta. \text{model}(y_t | \theta, x_{t-1}^i, x_t^i))$ dans l'Algorithme 2. Il faut donc trouver un moyen de rejouer un pas d'exécution en fixant la valeur de tous les paramètres d'état.

**Mémoriser les échantillons.** On peut implémenter l'opérateur *sample* comme une machine à état et utiliser l'état mémoire pour mémoriser les valeurs échantillonnées lors de la première exécution du modèle : $x_t^i, w_t^i = \text{model}(y_t | \theta^i, x_{t-1}^i)$ dans l'Algorithme 2. Malheureusement, l'exécution du modèle modifie l'état du programme en place. Si on ne fait pas attention, la fonction *Udpate* utilise donc $\lambda\theta. \text{model}(y_t | \theta, x_{t-1}^i, x_t^i)$ au lieu de $\lambda\theta. \text{model}(y_t | \theta, x_{t-1}^i, x_t^i)$.

Pour résoudre ce problème, nous proposons de stratifier la mémoire. Avant l'exécution du modèle, on copie superficiellement l'état qui contient des pointeurs vers l'état *profond* de chaque *sample*. Après l'exécution, on peut ainsi réutiliser cette copie de l'état où seul l'état des *sample* a été modifié. L'état de *sample* ne stocke donc pas directement la valeur échantillonnée, mais un pointeur vers une mémoire partagée. On distingue alors deux modes d'exécution gardés par une variable *booléenne* replay. Si replay est faux, l'appel à *sample(d)* tire un nouvel échantillon dans d et met à jour la mémoire partagée. Si replay est vrai, la valeur est déjà connue et l'appel à *sample(d)* se comporte comme *observe(d, m)* où m est le contenu de la mémoire partagée.
```typescript
type prob = {id: int; scores: float array; replay: bool}
```

```typescript
let sample = 
  let alloc () = ref (ref None) in
  let reset state = !state := None in
  let step state (prob, dist) =
    match prob.replay with
    | false -> let v = Dist.draw dist in !state := Some (v); v
    | true  -> let v = Option.get (! (!state)) in observe (prob, (dist, v)); v in
let copy src dst = dst := !src in
Cnode { alloc; reset; copy; step; }
```

La méthode copy implémente la copie superficielle qui ne duplique que les pointeurs en préservant l'état profond.

On peut maintenant définir une fonction apf.particle qui prend en argument le résultat de la compilation de la Section 4 et qui construit une particule qui implémente l'algorithme APF.

```typescript
type (α, β) apf_state = {p_state: α; mutable d_theta: β dist}

let apf.particle m_model m prior =
  let Cnode {alloc; reset; step; copy} = m_model in
  let p_alloc () = {p_state = alloc (); d_theta = m prior} in
  let p_reset state = reset state.p_state; state.d_theta ← m prior in
  let p_step ({p_state; d_theta} as state) (prob, obs) =
    let start_state = alloc () in copy p_state start_state;
    let theta = Dist.draw d_theta in
    let o = step p_state ({ prob with replay = false }, (theta, obs)) in
    let tmp_state = alloc () in
    state.d_theta ← update
    (fun theta →
      copy start_state tmp_state;
      let prob = {id = 0; replay = true; scores = [|0.|]} in
      let _ = step tmp_state (prob, (theta, obs)) in
      prob.scores.(prob.id))
    d_theta;
    o
  in
  let p_copy src dst = copy src.p_state dst.p_state; dst.d_theta ← src.d_theta in
  Cnode {alloc = p_alloc; reset = p_reset; step = p step; copy = p_copy}
```

En plus de l'état du modèle, l'état de chaque particule contient une distribution de paramètres constants d_theta initialisée par la fonction p_alloc avec m prior. La fonction de transition p step d'une particule se décompose ensuite de la manière suivante :

1. Copier superficiellement l'état de départ p_state dans une variable start_state.

2. Échantillonner une valeur theta dans d_theta.

3. Exécuter la fonction de transition de m_model, step avec replay = false pour mettre à jour l'état et mémoriser les valeurs de tous les paramètres d'état.

4. Mettre à jour la distribution d_theta en utilisant une fonction qui prend en argument theta, copie superficiellement l'état start_state dans une variable tmp_state et renvoie le score obtenu en ré-exécutant step à partir de tmp_state avec replay = true et un score réinitialisé pour rejouer l'instant courant en réutilisant les valeurs des paramètres d'état.

5. Renvoyer la sortie o calculée à l'étape 3.
Finalement, APF.infer est un cas particulier de SMC qui utilise apf.particle.

let apf_infer n m prior m model = infer n (apf.particle m model m prior)

**Modularité.** Notre implémentation ne fait pas d'hypothèse sur la fonction *Update* de l'Algorithmme 2 qui peut donc implémenter diverses heuristiques. L'article original [16] se concentre sur la méthode de correspondance des moments. À chaque instant, on tire un ensemble d'échantillons aléatoires dans *d_theta* et on mesure les scores obtenus. *d_theta* devient alors la distribution gaussienne qui approxime le mieux ces échantillons pondérés.

Nous avons également implémenté l'échantillonnage préférentiel, une méthode d'inférence sans filtrage. Au premier instant, on tire un ensemble de valeurs aléatoires pour les paramètres constants. Puis, à chaque instant, on met à jour le score associé à chacune de ces valeurs.

# 6 Évaluation

Dans cette section, nous validons expérimentalement notre implémentation d'APF sur un ensemble de modèles ProbZelus. Notre évaluation répond aux questions suivantes : (QR1) Quel est l'impact d'APF sur la précision des estimations à ressources fixées ? (QR2) APF résout-il le problème d'appauvrissement sur les estimations de paramètres constants ?

**Méthode expérimentale.** Pour chacun des exemples, on mesure l'évolution sur 500 pas d'exécution pas de l'erreur quadratique moyenne (*Mean Square Error*, MSE) pour les paramètres d'état et les paramètres constants. Pour mesurer l'appauvrissement, on regarde également l'évolution de la taille effective d'échantillonnage (*Effective Sample Size*, ESS), une métrique qui indique le nombre d'échantillons utiles. Les expériences ont été réalisées avec un processeur Intel Core i5-6200U (2.30GHz) avec 8Go de mémoire vive.

On compare les performances d'APF avec deux autres méthodes d'inférence : l'échantillonnage préférentiel (*Importance Sampling*, IS), une méthode de Monte Carlo élémentaire sans filtrage, et le filtre particulaire (*Particle Filter*, PF), une méthode de Monte Carlo séquentielle avec filtrage à chaque instant. Pour chacune des méthodes d'inférence, on fixe les ressources à $10^4$ particules. Sauf mention contraire, APF répartit les ressources disponibles avec 100 particules de filtrage et 100 particules d'échantillonnage pour le calcul de la correspondance des moments.

Pour comparer l'ESS d'APF avec celui des autres méthodes, on génère ensuite le même nombre d'échantillons en tirant une valeur aléatoire dans la distribution des paramètres constants pour chaque particule d'échantillonnage. Si $n_e$ est le nombre de particules d'échantillonnage et $n_f$ le nombre de particules de filtrage utilisées par APF, chaque particule génère donc $n_e$ échantillons qui sont tous associés au score de la particule. On obtient donc à chaque instant $n_e * n_f$ échantillons, soit le nombre d'échantillons produit par les autres méthodes.

Nous avons sélectionné des modèles qui illustrent plusieurs types de dépendances entre paramètres d'état et paramètres constants. **Coin** infère le biais d'une pièce à partir d'une série de jets [2]. Ce modèle n'a pas de paramètre d'état. APF utilise $10^4$ particules d'échantillonnage. **Kalman** estime la position d'un agent à partir d'observations bruitées [2]. Ce modèle n'a pas de paramètre constant. APF utilise $10^4$ particules de filtrage. **Sin** est similaire à Kalman, mais le modèle de mouvement fait intervenir une relation non-linéaire entre un paramètre constant et la position. C'est le modèle utilisé pour motiver APF dans l'article original [16]. **Split** fusionne deux problèmes indépendants : l'inférence d'un paramètre constant à partir d'observations bruitées et un filtre de Kalman. **Radar** est le modèle de radar de la Section 2.
<figure><img src="image_38.png" /><figcaption>Filtrer sans s'appauvrir</figcaption></figure>

G. Baudart, G. Bussone, L. Mandel, C. Tasson

FIGURE 8 - (a) PF, (b) IS, (c) APF. Pour chacun des 5 modèles on mesure l'évolution sur 500 pas d'exécution du *mean square error* (MSE) pour les paramètres d'état et les paramètres constants, et le *effective sample size* (ESS) des paramètres constants. Les marqueurs indiquent les valeurs médianes et les barres d'erreur correspondent aux quantiles 90% et 10% sur 10 exécutions.

**QR1 : Précision.** Les résultats de précision sont présentés Figures 8a et 8b. On remarque que, sur tous les exemples, la précision d'APF est équivalente à celle de PF pour l'estimation des paramètres d'état et des paramètres constants. Les courbes bleue et rouge sont quasiment identiques. On note cependant une plus grande variabilité dans les résultats d'APF sur les paramètres constants, notamment sur les derniers pas d'exécution. Ce comportement s'explique par le phénomène d'appauvrissement : après autant de filtrages successifs, l'estimation de PF pour les paramètres constants ne repose plus que sur une unique valeur et on a perdu toute mesure sur l'incertitude de l'estimation.
**QR2 : Appauvrissement.** Les résultats d'appauvrissement sont présentés Figure 8c. L'ESS pour APF reste quasiment constant autour du nombre d'échantillons total. Tous les échantillons générés ajoutent de l'information sur la distribution recherchée.

Sans surprise, on observe que l'ESS pour PF décroît strictement à chaque nouveau filtrage. L'ESS pour IS s'effondre lui aussi mais pour une raison différente. Aucune particule n'est éliminée, mais la plupart des valeurs tirées initialement deviennent tellement improbables que leur score tombe à 0. Ces particules n'ajoutent plus d'information pour le calcul de la distribution et ne sont donc plus comptées dans l'ESS.

**Coût.** Sur les trois exemples précédents où APF répartit les ressources entre filtrage et échantillonnage APF est en moyenne 1.43x plus lent que PF (Sin : 1.32x, Radar : 1.65x, Split : 1.33x). Pour les modèles avec un seul type de paramètre où APF utilise toutes les ressources soit en filtrage, soit en échantillonnage, APF est en moyenne 2.63x plus lent que PF. Ce ralentissement s'explique par le fait que APF ré-exécute plusieurs fois une même itération du modèle pour mettre à jour la distribution des paramètres constants puis générer les échantillons, là où le filtre particulaire n'exécute le modèle qu'une fois par instant. Ces performances sont correctes si l'appauvrissement n'est pas acceptable et que l'on cherche à estimer précisément l'incertitude sur la valeur des paramètres constants.

# 7 Conclusion

Nous avons montré comment estimer les paramètres constants des modèles ProbZelus en évitant le problème d'appauvrissement grâce à l'algorithme d'inférence *Assumed Parameter Filter*. Notre implémentation repose sur une nouvelle analyse statique, une nouvelle passe de compilation, et un nouveau moteur d'inférence pour ProbZelus. Nos résultats expérimentaux montrent que cette méthode d'inférence permet d'éviter le problème d'appauvrissement pour les paramètres constants sans pénaliser la précision des estimations pour les paramètres d'état.

**Travaux connexes.** L'analyse statique de la Section 3 est inspirée d'analyses spécifiques aux langages synchrones flot de données, en particulier l'analyse d'initialisation [11], qui vérifie que tous les flots sont bien définis au premier instant, et le typage des arguments statiques de Zelus, qui vérifie que certaines valeurs peuvent être calculées dès la compilation [7].

La compilation présentée en Section 4 se concentre uniquement sur les paramètres constants. C'est le moteur d'exécution qui se charge de fixer la valeur des paramètres d'état à l'aide d'une mémoire partagée pour rejouer un instant. Une alternative possible est de se rapprocher de la compilation des modèles hybrides de Zelus [4] et ajouter des entrées/sorties pour toutes les variables aléatoires introduites dans le modèle. On pourrait ainsi simplifier le moteur d'exécution au prix d'une compilation plus avancée.

La méthode d'inférence privilégiée de ProbZelus est *Delayed Sampling* [2], une méthode de Monte Carlo séquentielle qui calcule autant que possible des solutions analytiques exactes et n'échantillonne une variable aléatoire que lorsque le calcul symbolique échoue [21]. *Delayed Sampling* peut ainsi éviter l'appauvrissement si les paramètres constants n'ont jamais besoin d'être échantillonnés. Malheureusement, le moteur symbolique ne sait exploiter que des relations de conjugaison entre variables aléatoires, ou des relations affines [1]. On pourrait cependant combiner APF et *Delayed Sampling* pour améliorer la précision de ces deux méthodes.

**Remerciements.** Nous remercions les relecteurs et le suiveur pour leurs conseils. Ce travail a été en partie financé par le projet ReaLiSe, un projet Émergence(s) de la Ville de Paris.
Références

[1] Eric Atkinson, Charles Yuan, Guillaume Baudart, Louis Mandel, and M. Carbin. Semi-symbolic inference for efficient streaming probabilistic programming. In *OOPSLA*, 2022.

[2] Guillaume Baudart, Louis Mandel, Eric Atkinson, Benjamin Sherman, Marc Pouzet, and Michael Carbin. Reactive probabilistic programming. In *PLDI*. ACM, 2020.

[3] Guillaume Baudart, Louis Mandel, and Reyyan Tekin. Jax based parallel inference for reactive probabilistic programming. In *LCTES*, San Diego, USA, June 2022.

[4] Albert Benveniste, Timothy Bourke, Benoit Caillaud, and Marc Pouzet. Divide and recycle : types and compilation for a hybrid synchronous language. In *LCTES*, April 2011.

[5] Albert Benveniste, Paul Caspi, Stephen A. Edwards, Nicolas Halbwachs, Paul Le Guernic, and Robert de Simone. The synchronous languages 12 years later. *Proc. IEEE*, 91(1):64–83, 2003.

[6] Eli Bingham, Jonathan P. Chen, Martin Jankowiak, Fritz Obermeyer, Neeraj Pradhan, Theofanis Karaletsos, Rohit Singh, Paul A. Szerlip, Paul Horsfall, and Noah D. Goodman. Pyro : Deep universal probabilistic programming. *J. Mach. Learn. Res.*, 20:28 :1–28 :6, 2019.

[7] Timothy Bourke, Francois Carcenac, Jean-Louis Colaço, Bruno Pagano, Cédric Pasteur, and Marc Pouzet. A synchronous look at the simulink standard library. *ACM Trans. Embed. Comput. Syst.*, 16(5s):176:1–176:24, 2017.

[8] Timothy Bourke and Marc Pouzet. Zélus : a synchronous language with ODEs. In *HSCC*, pages 113–118. ACM, 2013.

[9] Paul Caspi and Marc Pouzet. A co-iterative characterization of synchronous stream functions. In *CMCS*, volume 11 of *Electronic Notes in Theoretical Computer Science*. Elsevier, 1998.

[10] Nicolas Chopin and Omiros Papaspiliopoulos. *An introduction to sequential Monte Carlo*. Springer, 2020.

[11] Jean-Louis Colaço and Marc Pouzet. Type-based Initialization Analysis of a Synchronous Data-flow Language. *International Journal on Software Tools for Technology Transfer*, 6(3):245–255, 2004.

[12] Jean-Louis Colaço, Grégoire Hamon, and Marc Pouzet. Mixing signals and modes in synchronous data-flow systems. In *EMSOFT*, 2006.

[13] Jean-Louis Colaço, Bruno Pagano, and Marc Pouzet. SCADE 6 : A formal language for embedded critical software development. In *TASE*, pages 1–11. IEEE Computer Society, 2017.

[14] Marco F. Cusumano-Towner, Feras A. Saad, Alexander K. Lew, and Vikash K. Mansinghka. Gen : a general-purpose probabilistic programming system with programmable inference. In *PLDI*, pages 221–236. ACM, 2019.

[15] Pierre Del Moral, Arnaud Doucet, and Ajay Jasra. Sequential Monte Carlo samplers. *J. Royal Statistical Society : Series B (Statistical Methodology)*, 68(3):411–436, 2006.

[16] Yusuf Bugra Erol, Yi Wu, Lei Li, and Stuart Russell. A nearly-black-box online algorithm for joint parameter and state estimation in temporal models. In *AAAI*, 2017.

[17] Hong Ge, Kai Xu, and Zoubin Ghahramani. Turing : A language for flexible probabilistic inference. In *Proceedings of Machine Learning Research*, 2018.

[18] Noah D. Goodman and Andreas Stuhlmüller. The design and implementation of probabilistic programming languages, 2014. Accessed April 2020.

[19] N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language LUSTRE. *Proceedings of the IEEE*, 79(9):1305–1320, September 1991.

[20] Michael Montemerlo, Sebastian Thrun, Daphne Koller, and Ben Wegbreit. Fastslam : A factored solution to the simultaneous localization and mapping problem. In *AAAI*, 2002.

[21] Lawrence M. Murray, Daniel Lundén, Jan Kudlicka, David Broman, and Thomas B. Schön. Delayed sampling and automatic rao-blackwellization of probabilistic programs. In *AISTATS*, 2018.

[22] David Michael Ritchie Park. Concurrency and automata on infinite sequences. In *Theoretical Computer Science*, 1981.
An AST for Representing Programs
with Invariants and Proofs

Guillaume Bertholon¹,² and Arthur Charguéraud²,¹

¹ Université de Strasbourg, CNRS, ICube, France

² Inria, Strasbourg, France

Abstract

Deductive verification enables one to check that a program satisfies its specification. There are mainly two approaches: either the user provides invariants in the form of annotations and use a tool to extract proof obligations, like in, e.g., Why3; or the user verifies the program through interactive proofs, like in, e.g., CFML, by providing invariants during the proof steps.

We are interested in expressing in Coq the representation of a program, accompanied
with not only its invariants but also its proof terms. Concretely, we present an AST for
representing source code and specification in a deep embedding style, and embedded lem-
mas in shallow embedding style. Such lemmas can be established using the full capabilities
of the prover.

We develop a way to build these ASTs from source code using CFML-style interactive tactics. We also develop a way to build these ASTs by extracting proof obligations from source code already annotated with its invariants. Besides, we provide a way to validate our ASTs by reifying them as Coq proof terms.

This work is a first step towards a long term project to devise a trustworthy, user-
guided, source-to-source optimization framework. On the one hand, we may need to exploit
invariants to justify the correctness of code transformations. On the other hand, to be
able to chain transformations, we also need every transformation to update the program
annotations.

# 1 Introduction

Producing programs without bugs is known to be a hard task. In order to guarantee the absence of bugs, programmers can use deductive verification. Deductive verification is a technique that allows programmers to state the formal specification, and statically check that they hold on the program. The link between the code and the specification must be guaranteed by a proof. In practice however, verifying a program requires a lot of effort. Indeed, the amount of effort grows even larger when targeted program grow in size or in in complexity. The formal verification of realistic high performance code, appears prohibitively costly.

In our long term project, we aim to develop a methodology for deriving programs that are
both highly optimized and formally verified. Our plan is to start from unoptimized code that
is easier to verify, and progressively refine this code into a more performant version. Such
source-to-source code refinement process has already been shown in the OptiTrust framework
to be expressive enough to match the performance of a numerical simulation optimized by
hand [3]. However, OptiTrust does not yet provide formal guarantees about the correctness
of the output code. To ensure that a source-to-source transformation preserves correctness, it
may be needed to exploit the existing invariants of the input code. Therefore to support chain
of transformation, each transformation will need to maintain program invariants.

In this paper, we present an abstract syntax tree (AST) data structure for representing pro-
grams, together with their invariants and proofs. We also give practical methods to build these
ASTs, and to validate the proof they carry. However, we leave to future work the implementa-
tion of practical transformations, e.g., function inlining, arithmetic rewriting (such as replacing
a division by a shift), loop reordering, or even replacing a part of the program by a semanti-
cally equivalent but arbitrary code. Nonetheless, our AST provides a way for transformations
to access those invariants and proofs and maintain both while changing the code.

Before explaining in more details how our AST is represented, let us recall the ways in which invariants are provided and proofs are constructed in state-of-the-art deductive verification tools. Typically, the specification of a program is expressed with a Hoare triple stating what pre-condition must be true before the execution, and what post-condition is true after the execution. In addition, one needs to describe the mutable state, and express the fact that pointers may or may not overlap, i.e., do not alias. These memory properties can be stated concisely using Separation Logic [11]. Given a specification, the verification of a program includes three kind of steps: (1) semantic steps, which process one construct of the source code; (2) structural steps, which refine invariants at a given program point, possibly exploiting the rules of separation logic; and (3) pure steps, which do not involve the program or the data it manipulates directly but are mathematical arguments needed to conclude. Throughout the paper, we call such pure steps *proof leaves*, since they can only appear at the end of proof branches.

These proof steps can be organized in different ways depending on the approach followed
to construct a proof that a program satisfies its specification. There are mainly two kind of
approaches.

* One can use an annotation strategy. In this case, the user starts with adding annotations to the program. These annotations must contain the specification but also useful invariants that are hard to deduce (e.g. loop invariants). Then, a tool extracts proof leaf goals to ensure that assertions are satisfied using the semantics of the programming language. Doing so, it automatically applies semantics and structural proof steps. These generated proof leaves can then be discharged using automated provers such as SMT solvers. If the solvers are unable to conclude, the user can add more annotations, as intermediate assertions. This is the approach used by, for instance, Why3 [5].

* Or, the user can verify the program through an interactive proof. There the tool let the user interactively choose a semantic or structural step and update the remaining program code and pre-condition accordingly. In particular, at any point the user can either weaken the pre-condition or strengthen the post-condition. Some of the steps generate proof leaves to justify their correctness. Such proof leaves can also be proven interactively; they correspond to standard Coq lemmas. This second approach is used, for instance, by CFML [4].

Both approaches have their strengths for representing program with invariants and proofs.
The annotation approach anchors the invariants directly at the relevant place in the code,
in a very natural way. The interactive proof approach gives a fully interactive construction
method. Moreover it produces statements that can be easily related to the formal semantics of
the programming language, in a *foundational* way.

In Section 2, we explain how programs with invariants can be described in both approaches.
In Section 3, we present our AST data structure as a Coq inductive type. As we will argue,
our AST can be either viewed as a *deep embedding* of a proof derivation; or as an annotated
source code, furthermore decorated with proof environments and proof terms. All proof leaves
remain represented by means of a *shallow embedding*, that is, as Coq proof terms. In Section 4,
we explain how instances of our AST can be built using either of the two aforementioned
approaches: either via annotation and extraction of proof obligations, or via fully interactive processing. In section §5, we present a *reification* technique for validating that an instance of our AST indeed satisfies the reasoning rules of the program logic. Concretely, the AST is translated into a Coq proof term using lemmas and semantic definitions from CFML. This reification procedure will be helpful in future work to validate the correctness of any source-to-source transformation step.

# 2 Representing Proofs

As said in the introduction, our AST for representing program with invariants and proofs will be inspired by the two classical approaches for doing program verification, namely program annotation and interactive proofs.

Before getting into the details of our AST, let's review how proofs that an imperative program satisfies a specification are usually made in both styles.

## 2.1 Program Annotations

The program annotation approach gives a direct link between code and attached invariants. This is an important property for transformations because we need to find which invariants need a modification when updating the code.

Let's consider as example program, the function `ref_move`.

```h
let ref_move r n =
  let m = get r in
  let s = ref m in
  set r n;
  s
```

This function can be specified by the following lemma:

$$ \forall r, n, m. \{r \leftrightarrow m\} (\mathbf{ref\_move} r n) \{\lambda s. r \leftrightarrow n \star s \leftrightarrow m\} $$

This lemma indicates that under the pre-condition that the cell at address `r` contains the value `m`, the function will return a new pointer `s` that points to `m` and that `r` will now point to `n`. Here, the symbol `\star` denotes the separating conjunction of the logic. It implies in particular that `r \neq s`. Following the annotation approach, we then decorate the source code with separation logic assertions at all key program points, yielding the program below.

```h
let ref_move r n =
  r \leftrightarrow a
  let m = get r in
    [m = a] \star r \leftrightarrow a
  let s = ref m in
    [m = a] \star r \leftrightarrow a \star s \leftrightarrow a
  set r n;
  r \leftrightarrow n \star s \leftrightarrow m
  s
  \lambda s. r \leftrightarrow n \star s \leftrightarrow m
```
With such an annotated program, one can run a tool to extract, for each block of instruction between annotation, a set of proof leaf obligations that is sufficient for guaranteeing the specification. Typically, such tools are implemented using weakest precondition (WP) computation. With separation logic style specifications, this technique is used by tools such as VeriFast [12], and Viper [10].

In more complicated examples, the memory state contains representation predicates to express recursive data-structures. For instance, a mutable linked list with head at address $p$, storing the values described by the list $L$, could be described by a predicate $p \rightsquigarrow \text{Mlist } L$ recursively defined as:

$$p \rightsquigarrow \text{Mlist } L \equiv \begin{array}{l} \text{match } L \text{ with} \\ \quad \mid \text{nil} \Rightarrow [p = \text{null}] \\ \quad \mid x :: L' \Rightarrow \exists q. (p.\text{head} \leftrightarrow x) \star (p.\text{tail} \leftrightarrow q) \star q \rightsquigarrow \text{Mlist } L'. \end{array}$$

To manipulate those representation predicates, one may need to add some ghost instructions in the annotated program specifically to change the vision of the memory state, by unfolding or folding back a Mlist predicate.

The advantage of the annotated program representation for program transformations is that intermediate assertions are attached to program points, so it is easy to tell which assertions need to be updated when local changes are applied to the code. For example, for a transformation that inlines a function, we can specialize the invariants of the body of the function and use these specialized invariants for the inlined code. All the rest of the code can keep its invariants unchanged. As another example, consider the reordering of independent let-bindings. We need to generate new intermediate annotations, but all the annotations before the first let-binding and in the continuation of the second let-binding can be directly reused. In that example, checking that we are able to generate the intermediate annotations effectively proves the absence of dependence between the two bindings. In most cases, such a check is purely syntactic and only use the commutativity of the separating conjunction.

## 2.2 Interactive Construction of Derivations

The interactive proof strategy provides a way to build a *derivation tree*. These trees perfectly capture the proof steps applied, their required hypotheses, and the links with the program semantics. This is an important property for proof validation, and gives a practical method for the construction of the AST. In this approach, proof are carried out inside an interactive proof assistant, by exploiting reasoning rules of the program logic expressed as lemmas.

Foundational systems such as CFML [4], VST [6] or Iris [7] are built using rules stated as lemmas. These lemmas are proved with respect to the programming language semantics and the logical framework. This foundational approach reduces the trusted code base.

In the derivation trees produced by such frameworks, every node corresponds to a logic rule. Reasoning rules with hypotheses correspond to nodes with sub-trees in the derivation. Interactive verification frameworks typically provide tactics for applying the reasoning rules. They thereby give the illusion to the user of following the code line by line, while building the proof. When invoking these tactics, the user provides the program invariants that cannot be automatically inferred.

Our AST features constructors to match both *structural reasoning rules* and *semantic reasoning rules*. In these reasoning rules, we choose to make the context, written $\Gamma$, explicit. This context consists of a list of bindings, for variables and pure facts (i.e., hypotheses). In many presentation, the context, which corresponds to the Coq context, is left implicit, but we find is useful to make context explicit in order to better explain the transitions that affect the context.
Below, the symbol $\vdash$ denotes the heap entailment: $H \vdash H'$ holds iff all heaps satisfying $H$ also satisfy $H'$. Post-conditions are represented by functions from program return values to heap predicates and we define their point-wise entailment $Q \vdash Q'$ as $\forall v : \mathbf{Val}, Q v \vdash Q' v$. The notation $[P]$ corresponds to the pure heap predicate $P$. The judgement $\Gamma \vdash \{H\} t \{Q\}$ asserts that the term $t$ admits $H$ as a pre-condition and $Q$ as a post-condition, in the environment $\Gamma$. For details, we refer to Charguéraud's survey [2].

We consider the 4 following structural rules of Separation Logic.<fnref n="1" />

$$
\begin{array}{l@{\qquad}l}
\begin{array}{c} \text{CONSEQUENCE} \\ \Gamma \models H \vdash H' \end{array} &
\begin{array}{c} \text{FRAME} \\ \Gamma \models \{H\} t \{Q\} \\ \hline \Gamma \models \{H \star H'\} t \{Q \star H'\} \end{array} \\[1.5em]
\begin{array}{c} \text{PROP} \\ \Gamma, -, P \models \{H\} t \{Q\} \\ \hline \Gamma \models \{[P] \star H\} t \{Q\} \end{array} &
\begin{array}{c} \text{EXISTS} \\ \Gamma, x : T \models \{H\} t \{Q\} \\ \hline \Gamma \models \{\exists x : T. H\} t \{Q\} \end{array}
\end{array}
$$

There is one semantic rule per term construct. We show below a few of them.

$$
\begin{array}{l@{\qquad}l}
\begin{array}{c} \text{VAL} \\ \Gamma \models \{ \} \} v \{ \lambda r. [r = v] \} \end{array} &
\begin{array}{c} \text{LET} \\ \Gamma \models \{H\} t_1 \{Q'\} \\ \hline \Gamma \models \{H\} \text{ (let } x = t_1 \text{ in } t_2 \text{)} \{Q\} \end{array} \\[1.5em]
\begin{array}{c} \text{IF} \\ \Gamma, -, b = \text{true} \models \{H\} t_1 \{Q\} \\ \hline \Gamma \models \{H\} \text{ (if } b \text{ then } t_1 \text{ else } t_2 \text{)} \{Q\} \end{array} &
\begin{array}{c} \Gamma, -, b = \text{false} \models \{H\} t_2 \{Q\} \\ \hline \Gamma \models \{H\} \text{ (if } b \text{ then } t_1 \text{ else } t_2 \text{)} \{Q\} \end{array}
\end{array}
$$

# 3 Definition of an AST for Representing Programs with Invariants and Proofs

We want to benefit from the strength of both program annotation and proof derivation in our AST. From the annotated program vision we want to keep the ability to read back the program and find where to apply a transformation, and which invariants need a change. From the logical derivation vision, we want to keep the ability to give the invariants along the proof, and the foundational relation with the semantics of the programming language. In this section, we present our AST data structure expressed a Coq inductive type, which can be interpreted both as an annotated program and as a derivation.

In order to manipulate and transform invariants, we will need an explicit representation not only of the program syntax, but also of program invariants and program proofs that we can manipulate. Therefore, we need program invariants to be represented using a *deep embedding*. On the contrary, the proof leaves (i.e., proof elements that do not refer to program code) correspond to Coq proof terms, and are encoded using a *shallow embedding*. The next section explains what is a deep embedding and how it compares to a shallow embedding.

## 3.1 Shallow vs Deep Embeddings

To represent the syntax of a programming language in Coq (or other similar proof assistants), there are two methods. Either one defines the language as a new inductive type with a fixed

<footnote n="1">¹We can notice that the PROP and the EXISTS rules are essentially the same, we can exploit this fact encoding $[P]$ by $(\exists : P. \}$).</footnote>
set of constructors, or one directly use Coq functions. The first style is called *deep embedding* and the second one is called *shallow embedding*. The question of whether to use a deep or a shallow embedding actually applies not only to the representation of program syntax, but also to the representation of program invariants, and to the representation of proofs.

In a deep embedding, the predefined list of constructors allows for pattern matching. However, binders and contexts need to be manually managed, for example with a definition of substitution and an explicit encoding of variable (either De Brujn or identifier strings). Similarly, typing is not provided unless explicitly implemented. In a shallow embedding however, since one defines usual Coq terms, binders and typing are directly provided by the proof assistant. As these terms can contain arbitrary elements with arbitrary types, we cannot pattern-match them, and thus have no way to inspect, modify or reuse sub-terms.

Regarding program syntax, a shallow embedding represents program functions as Coq functions, whereas a deep embedding represents it as data constructor carrying name of its arguments and a description of the body. Regarding program invariants, a shallow embedding corresponds to a term in **Prop**, whereas a deep embedding corresponds to a value from a custom inductive type. Regarding proofs, shallow embedded proofs correspond to the usual Coq proof terms, whereas deeply embedded proofs correspond to trees in a custom inductive data type, where each constructor correspond to a reasoning rule. Note that deeply embedded proofs are not natively verified.

Recall that our motivation is to define program transformation. Such transformations need to manipulate the program, its invariants and its proofs. Such manipulations can include the identification or the modification of sub-terms that cannot be done with a shallow embedding. We therefore need to use deep embeddings in this work.

In our AST, program syntax is essentially represented using a deep embedding. Program invariants are also represented using a deep embedding. This corresponds to a (simplified) representation of Coq terms, as we show in Section 3.2. For representing the proof terms, we need to be able to manipulate the part of the proofs that correspond to the application of the reasoning rules of the program logic. We represent the application of these rules using a deep embedding. Regarding proof leaves, we have a choice: we can use either a deep or a shallow embedding. It would be technically possible to encode the full calculus of construction in a deep embedded way, as it is done in "Coq in Coq" [1]. However, providing a construction method for such proofs would require reimplementing all Coq tactics. Instead, we choose to represent the proof leaves as *shallowly embedded closed lemmas with deeply embedded arguments*, as we detail in Section 3.4.

In Section 3.3, we will show how we manage the explicit binders in our deep embedded proofs. In Section 3.5, we present our AST as a deep embedding of the proof with strict restrictions on the rules allowed inside the derivation. Those restrictions make the proof look like an annotated program.

## 3.2 A Deep Embedding of Coq Terms

As we have seen in the previous section, we need a deep embedding for expressing program invariants. Those invariants might contain arbitrary logical formulae. Therefore, we choose to represent them with a simplified deep embedding of Coq terms, as shown below.

Inductive coq :=
  | coq_sort (S: sort)
  | coq_val (v: val)
  | coq_var (x: var)
| coq_app (u1 u2: coq) (* <[ u1 u2 ]> *)
| coq_forall (z: bind) (Uz P: coq) (* <[ ∀z: Uz, P ]> *)
| coq Fun (z: bind) (Uz u: coq) (* <[ fun z: Uz, u ]> *)
| coq_eq (u1 u2: coq) (* <[ u1 = u2 ]> *)

This deep embedding mostly consists of lambda calculus, with an additional constructor (coq_val) to quickly include values of the manipulated programming language. The variables (type var) are defined as Coq strings. We prefer explicit naming to De Bruijn indices to ease printing of the terms and retain user given names. This means, however, that we need to compare terms up to alpha equivalence. The binders are defined with the type bind and can either contain a fresh variable name, or be anonymous and not introduce any new variable in the context. Free variables are interpreted in a global environment. This environment contains the encoding of the separation logic, and all the relevant predicates for expressing the specification, with definitions close to their CFML analogues. Advanced constructions, such as recursive functions are not handled because we are not yet sure that they will be useful for our application.

For the goals of this paper, we do not need to formalize the typing judgement of these deep
embedded Coq terms. As explained in Section 5, proofs and the invariants they refer to will be
ultimately type checked during their reification.

Our embedded terms can be written in a human readable manner thanks to the use of
notation. For example, the predicate $∃L$. `[∀i, 0 ≤ i < 5 → L[i] = 0] ★ p ↛ MList L$^{can}$ be
written as follows<fnref n="2" />:

`<[∃L: "list", \[ ∀i: "nat", 0 ≤ i < 5 → "get" 'L' i = 0 ] ★ "MList" 'L' p ]>.`

## 3.3 Manipulation of the Proof Environment

In our AST which represents proof trees, we call *environment* the context of all entities syn-
tactically introduced by the parents of a node and therefore available at that point. Since this
AST represents a proof that a program respects a specification, we have several kinds of entities
in the context:

* Program variables, which are manipulated by the program instructions;

• Pure facts, which represent mathematical properties true at a given program point;

• Ghost variables, which are additional variables used to state specifications;

* Linear resources, which are linear heap predicates in Separation Logic; each resource can be consumed only once.

These environments can be represented by 3 distinct binding lists. One is used for program variables and is called *program environment*. Another is used for ghost variables and pure facts (which can be seen as pure variables with a type in *Prop*) and is called *pure environment*. The last one is for linear resources and is called *linear environment*.

Each element of the environment can be accessed by a name. This includes linear resources as in Iris [7]. The type of each environment entity is defined using the previously introduced deep embedding, and can refer to the entities defined before itself (considering that linear resources always come last).

<footnote n="2">²With notation such as $H * H' \equiv \text{"hstar" H H'}$, and $∃x: ux, H \equiv \text{"hexists" ux (fun x: ux \Rightarrow H)}$</footnote>
Our AST will not contain an explicit representation of environments because their contents can be computed by traversing the AST. However, such explicit representation of the environments is used for the construction of our AST. Moreover, since nodes in the AST correspond to reasoning rules, they act on this environment, either by using or adding entities in it.

Environments are extended with bindings when, for example, entering the scope of a let-construct. Consider the program snippet `let p = ref 2 in c`, in a given environment *E*. Suppose that the body `ref 2` is specified using the post condition $∃n, [even n] \star p \leftrightarrow n$. In the continuation *c* the environment *E* is extended with a program variable *p*, a ghost variable *n*, a pure fact of type `even n` and its linear environment is replaced by a single binding of type $p \leftrightarrow n$.

To assign names to these bindings, in our AST we need to introduce annotations for the binders, with square brackets to denote pure arguments and curly braces to denote linear resources.

let p [n: nat] [Pn: even n] {Hp: p↔n} = ref 2 in c

This annotated let-construct, adds *p* as a program variable, *n* and *Pn* to the pure environment and sets the pure environment to only contain *Hp* when processing the *c* continuation branch. Dually, it requires that the let body returns a value *p* such that the environment `[n: nat] [Pn: even n] {Hp: p↔n]` can be built.

Concretely, we will represent these annotations in our AST using the record *binds* shown below.

Record binds := {
    binds_vars: list bind;
    binds_pure: list (bind * coq);
    binds_linea: list (bind * coq)
}.

Two instances of this *binds* record are also involved in function specifications: one describes the input of the function, including its pre-condition, the other describes its output, including its post-condition. Annotated functions are represented using the record shown below, where *annot_trm* is explained further on.

Record annot_fn := {
    annot_fn_input: binds;
    annot_fn_body: annot_trm;
    annot_fn_output: binds
}.

## 3.4 Shallow Embedding of Proof Leaves

Proof leaves appear as hypotheses of the derivation rules applied in our AST, by definition, they correspond to the proof obligations that do not directly involve the program.

Proving these leaves can involve the application of arbitrary mathematical theorems. Therefore, it is very likely that all code transformations would consider all the proof leaves as axioms, and at most reuse, maybe combine, but never modify or inspect what is inside the leaf. Because of that, we choose to encode proof leaves with a shallow embedding in our AST. This brings two main advantages: it removes the need to support most of the features of the calculus of construction in the deep embedded proof rules, and it gives the user the full set of Coq tactics to build the lemmas in the leaves.
However, incorporating a shallow embedded proof inside a deep embedded one brings some issues. Most of the proof leaf obligations refer to the deep embedded proof environment. There is no hope to use the deep embedded environment from a shallow embedded proof since the shallow proof needs to be closed to pass the type checking.

One approach could be to build a shallow lemma taking the environment as argument. This has the main drawback that environment can contain bindings of any type, and we then need to guarantee that all the accesses fetch a variable with the right type, which would be quite heavy or impractical. We prefer to implement shallow embedded proof leaves as Coq functions that take all the relevant elements of the environment as arguments.

Since our shallow embedded goals have arbitrary types, we are forced to store their proofs in dependant pairs. This dependant pair does not enforce by itself a link between the proven lemma type and the deep embedded proof obligation but we will show in Section 5 how to check this property.

Concretely, we represent prove leaves as follows, where we call `pure_lemma` a dependant pair, and `proof_leaf` a shallow embedded lemma instantiated with deep embedded arguments. These arguments are directly given in the Coq term deep embedding..

```
Record pure_lemma := {
    pure_lemma_stmt: Type;
    pure_lemma_proof : pure_lemma_stmt
}.
```

```
Record proof_leaf := {
    proof_leaf lemma: pure_lemma;
    proof_leaf_args: list coq
}.
```

To keep maximal freedom in transformations, lemmas should only take as argument useful hypotheses; indeed, a modified piece of code could have a smaller environment than the original.

## 3.5 An AST Representing Both a Proof Derivation and an Annotated Program

We are now ready to present an AST that can be viewed either as a deep embedding of a proof derivation, or as an annotated program decorated with its invariants and proofs.

In our AST, we allow incomplete proofs. This means that annotations are optional. This includes, for instance, all the proof leaves.

When interpreting our AST as a proof derivation, all the constructors in our AST correspond to one derivation rule, either structural or semantic. On the contrary, when interpreting our AST as an annotated program, semantic constructors become annotated program syntax, and structural constructors are ghost instructions. In particular, if we ignore all the annotations and skip all the structural rules, we can directly recover the source code of the program.

The AST can be given by the following type, where `val_or_var` contains either a program value or a program variable name and `hyp` and `hvar` are aliases to `var` to respectively denote a name bound in the pure environment and a name bound in the linear environment.

```
Inductive annot_trm :=
    (*** Semantic ***)
  | annot_trm_val (tv: val_or_var)
  | annot_trm_call (fn: var) (args: list val_or_var) (spec: option (hyp*list coq))
```
| annot_trm_let (binds: binds) (body: annot_trm) (cont: annot_trm)
| annot_trm_if (uvc: val_or_var) (hyp_name: option bind) (brt: annot_trm) (brf: annot_trm)
| ... (* One rule for each construction in the program language *)
| ... (*** Structural ***)
| annot_trm_frame (frame: list hvar) (cont: annot_trm)
| annot_trm_change_pre (pure_clear: list hyp) (linear_in: list hvar)
| ... (output: binds) (change lemma: option proof leaf) (cont: annot_trm)
| annot_trm_change_post (pure_clear: list hyp) (linear_in: list hvar)
| ... (output: binds) (change lemma: option proof leaf) (cont: annot_trm)

The semantic constructors correspond both to annotated program constructions and to the
application of a semantic rule.

* The constructor `annot_trm_val` represents a return value at the end of a program expression. It corresponds as well to the VAL semantic rule.

$$ \frac{\text{VAL}}{\Gamma \models \{ \} v \{ \lambda r. [r = v] \}} $$

As this rule has no parameters except the return value itself, there is no need for any annotation on the `annot_trm_val` constructor. However, it only occurs in fully proven programs with an empty linear environment and a matching post-condition: in particular, all linear resources must have been framed out above in the AST.

* The constructor `annot_trm_let` represents a let-construct. Without annotation its `binds` argument contains only program variables. However, when annotated, it contains as well new environment bindings for the continuation, that correspond to the environment specification of the body. The `annot_trm_let` constructor also corresponds to the following `LET` semantic rule where $Q'$ is given in the `binds` argument.

$$ \frac{\text{LET} \quad \Gamma \models \{H\} t_1 \{Q'\} \quad \Gamma, v : \text{Val} \models \{Q'v\} ([v/x] t_2) \{Q\}}{\Gamma \models \{H\} (\text{let } x = t_1 \text{ in } t_2) \{Q\}} $$

* Similarly `annot_trm_if`, is both an if-construct and the application of the `IF` rule, where `hyp_name` is the name given to the new hypothesis $p$ generated by that rule application.

$$ \frac{\text{IF} \quad \Gamma, p : b = \text{true} \models \{H\} t_1 \{Q\} \quad \Gamma, p : b = \text{false} \models \{H\} t_2 \{Q\}}{\Gamma \models \{H\} (\text{if } b \text{ then } t_1 \text{ else } t_2) \{Q\}} $$

* `annot_trm_call` encodes a function call with a provided list of arguments. It does not have a corresponding rule because it is supposed to use a function specification. This specification can be given in the annotation `spec` as an instantiated lemma from the pure environment (either local or global).

Structural constructors can appear anywhere in a derivation and correspond to structural rules, or ghost instructions:
* `annot_trm_frame` constructor encodes an application of the `FRAME` rule.

$$ \frac{\Gamma \models \{H\} t \{Q\}}{\Gamma \models \{H \star H'\} t \{Q \star H'\}} $$

The `frame` argument contains a list of linear resource bindings that correspond to `H` in the rule above. `H'` can be automatically deduced by taking the remaining elements in the current context. `Q` is similarly deduced by subtracting `H'` from the output specification at this point.

* There is no constructor for the rules `PROP` or `EXISTS` since we apply them implicitly when adding bindings to the pure environment.

* To be able to pinpoint easily which parts of the environment are modified when using the `CONSEQUENCE` rule, we split it into two different constructors `annot_trm_change_pre` and `annot_trm_change_post`, one for each side of the Hoare triple. Moreover, we identify with `linear_in` which subset of the linear environment will be modified, and with `pure_clear` which pure bindings will be cleared in the process, while giving binding names to all the introduced entities with `output`. This corresponds to the following rules that can be derived from the `CONSEQUENCE` rule, where $\Gamma$ is a pure environment, and $\Gamma'$ is a subset of $\Gamma$.

$$ \frac{\text{CHANGE-PRE} \quad \Gamma \models H \vdash H' \quad \Gamma' \models \{H' \star R\} t \{Q\}}{\Gamma \models \{H \star R\} t \{Q\}} $$

$$ \frac{\text{CHANGE-POST} \quad \Gamma' \models \{H\} t \{Q' \star R\} \quad \Gamma \models Q' \vdash Q}{\Gamma \models \{H\} t \{Q \star R\}} $$

This is the only construction introducing a shallow proof leaf, to prove the heap entailment hypothesis. With an empty `linear_in` list, it can be used to add arbitrary assertions in the environment at any program point, as long as it is provable.

With Coq notation, and if we mask proof leaves, we can actually print a term of type `annot_trm` as an annotated program.

This representation of a proof derivation is a good candidate for the kind of proof manipulation required by source-to-source transformations because by replacing any sub-tree in a derivation with another valid sub-tree of the same specification, we maintain the validity of the full tree, while changing the source code of a branch. It means that transformations can be local and ignore all the derivation rules above a relevant application point.

The AST does not by itself enforce its validity: at this stage, nothing checks the typing of the environment variables or that proof leaves assert what they should. This is not a problem since we show in the two next sections how to build a self-consistent tree and how to verify its validity.

# 4 Building Annotated Programs

In the previous section, we described an AST that can be seen either as an annotated program or as a proof derivation. This section shows that we can use these two views to build the trees. Given a program annotated with invariants but without proofs, one may want to build the same annotated program with its proof leaves filled in, using the annotation and extraction workflow presented in section §2.1. Besides, given a program without any annotation, one may want to
interactively build, in CFML fashion, the proof derivation that ensures the program follows its specification, as presented in section §2.2.

We explain how to perform both kinds of tasks, interactively in Coq. We start by presenting the CFML approach. Indeed, we will see how the case where program invariants are already present can also be handled with CFML style tactics, with the only difference being taking into account the existing invariants.

## 4.1 Building Interactively

We first describe how to interactively build a derivation, in CFML fashion, since we reuse most of the components in our proposed system.

From the user point of view, a CFML proof follow a simple workflow. At each step, the theorem prover shows the program that still need to be processed along with the environment at this program point. It also shows what invariants need to hold after the execution. Seeing these goals, the user will apply CFML tactics to apply structural of semantic rules at the current program point. These tactics produce sub-goals corresponding either to sub-programs verification or proof leaves.

Internally, these CFML tactics call shallow embedded lemmas. These lemmas produce a Coq proof term corresponding to a proof in the shallow embedding of Separation Logic and program semantics. Since this output proof term is in Prop, there is no simple way to inspect it, to extract an instance of our AST. Technically Ltac manipulation, to transfer this shallow proof in a deep embedding of Coq is possible (as it is done in the MetaCoq [13] plugin for instance), but the proof terms would have no canonical form anyway, so we cannot convert them into our AST.

Instead, we provide our own set of tactics. These new tactics display the same kind of goals as CFML and generate the same kind of proof obligations. However, their output is an AST in our format. This AST corresponds to a deep embedding of the derivation, except for proof leaves which are shallowly embedded.

The challenge in designing those tactics is that the proof obligations that we would like to show to the user are propositions, in Prop. However, their output is an instance of our AST, in Type. There is no fundamental difficulty, we simply need to find an appropriate way to state the proof obligations on which the tactics apply. To that end, we introduce a predicate, written `refine_pred E t F t`, where *t* is the input program, *E* and *F* correspond to pre- and post-conditions represented as environments with named elements; and *t* is an *evar* that gets refined along the proof. When the proof is completed the *t* variable gets instantiated with the desired output.

We display the `refine_pred E t F t` predicate to the user using a notation that hides `t`. What remains looks seemingly like a CFML proof obligation. We show below an example where *E* and *F* are displayed with a notation that separates the three components of the environments (program variable, pure facts, and linear resources).

PRE
  'x, 'p
  ----
  ['n : int]
  ["Px": 'x = 3]
  ["Pn": 'n = 1]
  ----
  {"Pp": 'p ↔ 'n}
CODE
let 'y = get 'p in
'x + 'y
POST
'r
---
["Pr": 4 = 'r]
---
{"Pp": 'p ↪ → 1}

This example corresponds to the following Hoare triple:

$$
\{\exists n.[x = 3] \star [n = 1] \star p \leftrightarrow n\} \texttt{let y = get p in x + y} \{\lambda r.[4 = r] \star p \leftrightarrow 1\}.
$$

During an interactive proof all goals except proof leaves are displayed using such notation
for `refine_pred`.

Reasoning steps of separation logic in such proofs are carried out using CFML style tactics. For instance, the tactic `xlet ["Py": 'y = 3] {"Pp": 'p ↪ → 1}` applies to the proof obligation shown above. As in CFML, this tactic generates two sub-goals (one for the body, one for the continuation). The argument provided to `xlet` describes the post-condition for the body. It is optional, and if not provided, an evar is introduced for this post-condition, which like in CFML gets instantiated during the verification of the body.

Internally, `xlet` applies to a goal of the form `refine_pred E (let x = t_body in t_cont) F t`.
It produces two sub goals `refine_pred E t_body E' t_b` and `refine_pred E'' t_cont F t_c`, where
`t_b` and `t_b` are newly generated evars, and `E''` corresponds to the concatenation of `E` with `E'` in
the program and pure environments and only `E'` in the linear environment. While doing so, it
instantiates `t` as `(let x E' = t_b in t_c)`.

At some points in the proof, the user reaches proof leaves, that is, proof obligations not establishing Hoare triples. Such proof leaves are represented in our AST using the type `proof_leaf` introduced in Section 3.4. Recall that `proof_leaf` contains a closed shallowly embedded lemma and a list of deeply embedded arguments.

Our framework present proof leaves obligations as the predicate `prove E G p̂`, where *E* is an environment without linear ressources, *G* is the deep embedding of the property we want to prove and *p̂* is an evar for the desired value of type `proof_leaf`. We provide a tactic `xprove` that applies to a goal of the form `prove E G p̂`. This tactic takes as argument a subset of the keys of *E* that corresponds to the hypotheses the user wants to exploit to establish a proof of *G*. The tactic then leaves a standard Coq proof obligation of a shallow version of *G* obtained using the reification mechanism described further on in Section 5. The resolution of this goal yields a proof term, which ends up being recorded in our AST.

## 4.2 Completing an Annotated Program with Proofs

In the previous section, we saw how to build an AST fully annotated with invariants and proofs
starting from an unannotated program. In this section, we explain how to build a similar AST
starting from a program annotated with invariants. Concretely, we need to fill the missing proof
leaves. This consists of extracting proof obligations and proving them, like e.g. in Why3.

Our implementation leverages the same mechanisms based on `refine_pred` as in the previous
section. The key difference is that the source program contains invariants. In particular, there
is no need to provide a post-condition when calling tactics such as `xlet` because this post-
condition already appears as a program annotation. More generally, CFML style tactics, can
all be invoked without arguments simply following the structure of the annotated program. As a result, all the tactics processing the code can be automatically handled.

A number of these tactics produce proof leaves. These proof leaves correspond to what is called extracted proof obligations in the tools taking the annotation and extraction approach.

There is another application of refining a partially complete AST into a fully complete one, related to program transformations that we intend to work on in the long term. The user may wish to introduce an arbitrary piece of code into an already verified program. Then, thanks to this construction method, we can extract proof obligations concerning exclusively the new piece of code.

# 5 A Reification Process to Validate our AST

The AST we presented in Section 3, does not include any guarantees about the validity of the proof it represents. Indeed, nothing prevents using an unbound environment variable or using a rule that do not apply at a given program point. In Section 4, we gave a methodology to build derivations. The derivations built that way are in principle well formed. However, their validity directly depends on the implementation of the construction tactics. Exactly like in Coq, we do not want our tactics to be inside the trusted code base, since they can have rather complicated implementations, and therefore may contain bugs.

A standard approach to provide a stronger validity guarantee on deep embedded proofs is to define a validity predicate. Such predicate ensures that each node in a derivation correspond to valid rule application. This is what we initially tried, but we quickly noticed that establishing and maintaining a validity predicate across transformations would require a lot of work.

To keep strong guarantees without too much effort, we introduce in this section a reification procedure. This will translate a complete proof derivation expressed in our AST into a standard shallow embedded CFML lemma. The obtained Coq proof is therefore directly using the defined semantics of our programming language, in a foundational way.

During reification, both the proof derivation and the invariants represented inside are translated in their shallow embedded counterparts. For specifying the type of the root of the derivation, we also extract an unannotated version of the program syntax as a CFML deeply embedded program term.

One technical aspect of the reification process is that we need to maintain the mapping between binding names from the AST environment, and corresponding Coq variables that appear in the produced proof term. This can be done by maintaining, during the reification process, a table between names in the deep embedding and identifiers in the shallow version. Since invariants can also refer to a global environment, we also need to provide a Coq implementation for each of these global terms.

When reaching proof leaves, our reification procedure will use the pure lemma stored inside the leaf and call it with reified versions of its deeply embedded arguments. This is enough to force the Coq type checker to verify that the lemma indeed proves the obligation it is applied on.

Concretely, the reification process is implemented as a recursive Ltac function parameterized by the mapping between binding names and Coq variables. On the proof parts, it applies rules expressed as CFML lemmas simply following the derivation. For invariants, it follows the structure of the deeply embedded term to progressively refine the corresponding shallow embedded Coq term.

In order to improve the user experience, when extracting program invariants, we want to reuse the names of the deeply embedded binders for the shallow embedded ones. This is possible
only if our Ltac procedure can convert a Coq string into a Coq identifier. Such translation
cannot be expressed natively in Ltac but can be implemented using a Coq plugin or a piece of
Ltac2 code.

In the end, the Ltac function implementing the reification process is not part of the trusted code base. What goes in the trusted base is the Coq kernel, the language semantics, and the definition of triples regarding the semantics. In addition, for each program, one needs to trust that the shallow embedding of the specification is correct. This shallow specification can be read as the type of the reified verification proof, but it also corresponds to a shallow embedded version of the specification that appears at the root of the annotated AST.

6 Conclusion

In this paper, we aimed at providing a representation for programs annotated with their invari-
ants and proofs, such that we can easily manipulate them.

We achieved that using a deep embedding of the proof derivation with shallow proof leaves
and explicit environment manipulations. We provided a method for constructing these anno-
tated programs either interactively or by filling missing proofs.

In the long term, we want to propose an interactive framework for code transformation that preserves proofs and can be used for source-to-source optimization. Using it, one should be able to write a naive version of a program, verify it, and then progressively transform it into a highly optimized code. After the last step we should be able to provide a proof of the final program. By combining such framework with verified compilers such as CakeML [8] or CompCert [9], we could then obtain binaries that are both trustworthy and efficient.

References

[1] Bruno Barras and Benjamin Werner. Coq in coq. Available on the WWW, 1997.

[2] Arthur Charguéraud. Separation logic for sequential programs (functional pearl). *Proc. ACM Program. Lang.*, 4(ICFP), August 2020.

[3] Arthur Charguéraud, Begatim Bytyqi, Damien Rouhling, and Yann A Barsamian. OptiTrust: an Interactive Framework for Source-to-Source Transformations. working paper or preprint, September 2022.

[4] Arthur Charguéraud. Characteristic Formulae for the Verification of Imperative Programs. In *Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming*, ICFP '11, page 418–430, New York, NY, USA, 2011. Association for Computing Machinery.

[5] Jean-Christophe Filliâtre and Andrei Paskevich. Why3 — where programs meet provers. In Matthias Felleisen and Philippa Gardner, editors, *Proceedings of the 22nd European Symposium on Programming*, volume 7792, pages 125–128, March 2013.

[6] Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. Oracle Semantics for Con- current Separation Logic. In Sophia Drossopoulou, editor, *Programming Languages and Systems*, page 353–367, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.

[7] Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. RustBelt: Securing the Foundations of the Rust Programming Language. *Proc. ACM Program. Lang.*, 2(POPL), dec 2017.

[8] Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. CakeML: A Verified Implementation of ML. In *Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, POPL '14, page 179–191, New York, NY, USA, 2014. Association for Computing Machinery.
[9] Xavier Leroy. Formal Verification of a Realistic Compiler. *Commun. ACM*, 52(7):107–115, jul 2009.

[10] Peter Müller, Malte Schwerhoff, and Alexander J. Summers. Viper: A Verification Infrastructure for Permission-Based Reasoning. In Barbara Jobstmann and K. Rustan M. Leino, editors, *Verification, Model Checking, and Abstract Interpretation*, page 41–62, Berlin, Heidelberg, 2016. Springer Berlin Heidelberg.

[11] O'Hearn, Reynolds, and Yang. Local reasoning about programs that alter data structures. In *CSL: 15th Workshop on Computer Science Logic*. LNCS, Springer-Verlag, 2001.

[12] Pieter Philippaerts, Jan Tobias Mühlberg, Willem Penninckx, Jan Smans, Bart Jacobs, and Frank Piessens. Software verification with VeriFast: Industrial case studies. *Science of Computer Programming*, 82:77–97, 2014. Special Issue on Automated Verification of Critical Systems (AV-oCS’11).

[13] Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. The MetaCoq Project. *Journal of Automated Reasoning*, 64(5):947–999, Jun 2020.
# Retrofitting OCAML modules
Fixing signature avoidance in the generative case

Clément Blaudeau¹, Didier Remy¹, and Gabriel Radanne²

¹ Cambium, Inria, France

² CASH, Inria, EnsL, UCBL, CNRS, LIP, France

## Abstract

ML modules are offer large-scale notions of composition and modularity. Provided as an additional layer on top of the core language, they have proven both vital to the working OCaml and SML programmers, and inspiring to other use-cases and languages. Unfortunately, their meta-theory remains difficult to comprehend, requiring heavy machinery to prove their soundness. Building on a previous translation from ML modules to $F^ω$, we propose a new comprehensive description of a generative subset of OCAML modules, embarking on a journey right from the *source* OCAML module system, up to $F^ω$, and back. We pause in the middle to uncover a system, called *canonical* that combines the best of both worlds. On the way, we obtain type soundness, but also and more importantly, a deeper insight into the *signature avoidance problem*, along with ways to improve both the OCAML language and its typechecking algorithm.

# 1 A powerful but imperfect module system

Modularity is a key technique to break down a complex program into parts at different levels of abstraction. Instead of dealing with technical details and complex invariants at all times, programmers can split the code-base into manageable parts, called *modules*, and structure the relationship between those modules by specifying their interfaces and interactions. Code might be packed into a module to make a component, such as the implementation of a data-structure, reusable and often polymorphic—effectively factorizing development. Controlling the interactions between modules through a cautious choice of interfaces is not only a tool for correctness; using abstraction, it is also a way to enforce invariants and to allow for several teams of developers to work independently on different parts of the same program while enjoying a language-level guarantee that they respect the invariants of other parts.

A wide variety of techniques can be used to apply modularity concepts to software development: simple compilation units, classes, packages, crates, etc. In languages of the ML-family, modularity is provided by *modules*, which form a language layer built on top of the core language. The interactions between modules are controlled statically by a strict type system, making modularity work in practice and with little run-time overhead. A module is described by its interface, called a *signature*, which serves as both a light specification and an API.

The OCAML module system is especially rich and still under development for new features. It provides both developer-side and user-side abstraction mechanisms: developers can control the outside view of a module by explicitly restricting its interface, while users can abstract over a module with a given interface using a *functor*. The signature language allows to both *restrict* and *control* the interface of a module, specifically by *hiding* fields (which corresponds to the distinction between *public* and *private* fields in Object-Oriented Programming), or by abstracting type components—keeping types accessible while hiding their definitions.

The OCAML module system is renowned for its expressiveness, ease of use, and the properties it can statically enforce. All sizable OCAML projects use modules to access libraries or define
<figure><img src="image_39.png" /><figcaption>Figure 1: A representation of the mismatch between the *reachable space* of module expressions (outer-most circle) and the *describable space* of signatures (inner ellipse). The common use-cases of OCAML are mainly within the area where the type-checker behaves correctly. In some cases, the current OCAML typechecker can lose type-equalities while still being in the describable space. This may lead to (1) producing a signature where some type fields are unnecessarily made abstract (over-abstraction) or (2) failing at inferring the signature (incorrect avoidance).</figcaption></figure>

parametric instances of data structures (sets, hashtables, streams, etc.). Several successful projects have made heavy use of modules, as in MirageOS [Madhavapeddy et al., 2013] where modules and functors are even assembled on demand using a DSL [Radanne et al., 2019]. Despite the successes and the interest of the community regarding ML modules, giving it a formal type-theoretic definition and establishing its properties has proven to be a difficult task.

Besides the academic interest, having a formal semantics is made even more necessary to envision extensions such as modular implicits [White et al., 2014] where new modules could be built automatically from their signatures by applications of functors to other modules.

## 1.1 The signature avoidance problem

The *signature avoidance* problem is a key issue of ML-module systems. It originates from a mismatch, illustrated in Figure 1, between the expressiveness of the module and signature languages: the *reachable space* of possible module expressions is larger than the *describable space* of signatures: some modules can't be described by a signature. This issue can be solved either by sticking to the describable space and ensuring that the typechecker correctly covers it or by extending signatures to make the reachable and describable spaces coincide.

This mismatch is caused by the interaction of three mechanisms. First, type abstraction, which is key to control access and protect invariants by typing, creates new types that are only compatible with themselves (or aliases of themselves). Second, sharing abstract types between modules, which is essential for module interactions, produces trees of type-alias equalities. Finally, hiding type components (through either explicit projections or implicit subtyping during functor applications) can remove abstract type aliases from scope, while other components (values or types) kept in scope may refer to them (for instance, removing an abstract type *t* while keeping a value of type *t list*). In some situations, there is no possible signature to infer for a module; in other situations, there are several incompatible ones.

We illustrate this abstraction mechanism in Example 1. Each source code comes with a representation of the type equalities and aliases as a *tree of type equalities*. The connected components of the tree represent equal, interchangeable types that all belong to the same equivalence class. They can be rooted with base types (*int*, *bool*, *string*, etc.) or constructed over other types (like *int list*, *int* → *int*, *int* × *bool*, etc.) or previously defined *abstract types*. Abstracting a type effectively removes a link in the type-sharing tree, which splits a connected component.

Example 1 precisely illustrates this potential loss of type sharing when using module oper-
<figure><img src="image_40.png" /></figure>

<figure><img src="image_41.png" /></figure>

<figure><img src="image_42.png" /></figure>

<figure><img src="image_43.png" /><figcaption>Example 1: Two examples of modules and associated type-sharing trees.</figcaption></figure>

ations. On the left-hand side, restricting the signature of the module X to the module type S removes the link between X.t and int (grayed out in the type-sharing tree): this becomes hidden to the typechecker outside of the body of the module X. On the right-hand side, the projection on the submodule Y removes X.t and X.u. The types Y.a, Y.b, and Y.c are pointing to *out-of-scope* types: they must be changed or deleted. This shows why expressing membership to an equivalence class through paths is fragile: the removal of type fields can split connected components apart, resulting in a loss of type-sharing or incorrect signatures.

**Strategies for solving signature avoidance** When a type declaration is referring to an out-of-scope type, there are mainly three strategies to correct the signature: (1) abstracting the type (effectively ignoring the previous link in the tree), (2) rewriting the type equalities using in-scope aliases (effectively rewiring the tree to maintain connected components), or (3) extending the signature syntax with existential types. The first strategy can lead to loss of type sharing, but is easy to implement—it is the one currently in use in the OCAML typechecker. The cases where the second strategy succeeds constitute the *solvable* cases of signature avoidance. The OCAML type-checker only tries to follow directed edges of the tree until it finds an accessible type, but does not follow reverse edges and thus does not have a notion of *connected components*. In *Example 1*, it would fail at finding that Y.a, Y.b and Y.c are aliases. Sometimes, no *in-scope* alias is available and signature avoidance cannot be solved without an extended syntax: those are the *general* cases of signature avoidance.

**Signature avoidance in practice** OCAML developers usually get around this limitation by explicitly naming modules before using them, which adds always-accessible root points to the graph. The module syntax of OCAML actually encourages this approach by limiting the places where inlined, unnamed modules and signatures can be used. In particular, projection on an unnamed module (as done in *Example 1*) is forbidden. However, explicit naming is sometimes cumbersome, which can limit the usability of module-based programming patterns such as modular implicits. It also prevents a fine-grained management of types shown in public APIs.

## 1.2 Related work

Previous work has provided solid formal foundations for ML-modules. The link between abstract types in ML-module systems and existential types in $F^\omega$ was already explored by Mitchell
<figure><img src="image_44.png" /><figcaption>Figure 2: The different systems: their links, with theorems and sections.</figcaption></figure>

and Plotkin [1985]. This vision was opposed by MacQueen [1986], who considered existential types to be too weak, and proposed using a restriction of dependent types (strong sums) to describe module systems. Further work, notably on phase separation by Harper et al. [1989], supported the idea that dependent types may actually be too powerful (thus, unnecessarily complex) for module systems. SML modules were first described by Harper et al. [1989]. Two approaches for the formalization and improvement of abstract types in SML were later concomitantly described by Leroy [1994] (through manifest types) and Harper and Lillibridge [1994] (via an adapted $F^\omega$ with translucent sums). The OCaml module system itself was specified by Leroy [1994, 2000], and later with an extension to applicative functors [Leroy, 1995].

The use of existential types to interpret signatures by Russo [2004] opened the door for a simplified link between modules and $F^\omega$. Type generativity is also explored by DREYER [2007], using stamps in place of existential types. A similar, but logically-based approach was later developed by Montagu and Rémy [2009] introducing the concept of open existential types. Pushing Russo's idea further, a closer correspondence between ML-modules and $F^\omega$ was achieved by Rossberg et al. [2014] by elaborating a significant subset of the SML module syntax into $F^\omega$. The type system is safe by construction, inheriting the property from $F^\omega$. A limit of this approach is that, since the definition of modules is only given by translation, the programmer must think in terms of the elaboration and only sees the elaborated types instead of the usual signatures. This makes direct reasoning on the source program more difficult. Their work, called the F-ing approach, also covered some difficult points like applicative functors and first-class modules, and was partially mechanized in Coq. Moving one step further, Rossberg [2018] achieved a unification of the core and module languages (thus, un-stratified) using $F^\omega$ as the underlying programming language and seeing module constructs as syntactic sugar. More recently, Crary [2020] used involved focusing techniques to solve the signature avoidance problem in the singleton-type approach (for SML modules) in a manner that turns out to have some similarities with that of F-ing.

## 1.3 A journey into OCaml modules

Our approach is strongly inspired by previous works, which we re-explore in the context of OCAML modules. Our goal is to provide a simpler and comprehensive type system for OCAML modules, which could first serve as a specification, then help correct and improve the current implementation, and, finally, serve as a basis for future extensions of the module language. Our contributions are summarized in Figure 2.

We start by presenting a (mostly standard) self-contained specification of the OCAML module system in §2, adapted from previous works. Critically, like the current OCAML implementation, this presentation suffers from the signature avoidance problem.

Then, we build on the insights of the F-ing [Rossberg et al., 2014] translation into $F^\omega$ to present a new set of typing rules. However, reasoning only by elaboration in $F^\omega$ is hard, as the elaboration introduces encoding layers and, crucially, uses a very different way of handling
abstract types, making the correspondence between source and $F^ω$ terms and types rather obscure. Instead, as hinted in the work of Russo [2004], we introduce a light extension of the syntax for signatures with $F^ω$-style quantifiers, which we call *canonical signatures*. They act as a middle point between the path-based approach of the source and the quantified approach of $F^ω$, effectively splitting the translation effort in two steps. We introduce in §3 a new type system for OCAML modules, called *canonical*, where the source module expressions are typed with canonical signatures and source signatures translated into canonical ones. This system is simpler than the source one and doesn't suffer from the signature avoidance problem. Using our one-way translation, we revisit and explain the ad-hoc techniques (strengthening, equivalence) of the source presentation. We finally give the main result of this section: all source typing derivations can be translated into canonical typing derivations (Theorem 1).

The reverse translation of signatures (from the canonical system to the source one) is not always possible, as the former is more expressive than the latter. In §4 we explore *when* and *how* we can translate canonical signatures back into OCAML signatures, which uncovers precisely why the signature syntax lacks expressivity. This reverse process, called *anchoring*, is one of our main contributions. We then show that we can restrict the canonical system at one specific point to *mimic* the source system and only produce signatures that are valid regarding the source typing (Theorem 2). Some details are also given in the appendix A.

The link between the canonical system and $F^ω$ is conceptually easier while presenting some technical challenges. For lack of space, it is only detailed in the appendix B. We introduce an *hybrid* system that produces both canonical and $F^ω$ objects in correspondence. The hybrid system acts a central justification, as it can yield both the canonical system and the *F-ing* style elaboration by projections. The canonical system was actually designed by erasing the terms from the $F^ω$ encoding which can still be seen as implicit *proof terms* justifying the canonical rules.

In this work, we restricted our system to a generative subset of the language. We believe our approach also extends to applicative functors and other features (first-class modules, module aliases, abstract signatures, etc.), which are left for future work. Our long term goal is to extend OCAML signatures following the canonical system, thus completely solving the signature avoidance problem. The canonical system would then be a standalone *source* system which can be used by programmers to reason about OCaml programs, with the $F^ω$ elaboration ensuring its soundness.

# 2 A generative subset of the OCaml module system

In this section we present a module system that models a generative subset of OCaml. We present its grammar, several auxiliary judgments used, and end with its typing judgment.

## 2.1 Grammar and syntactic choices

Figure 3 gives the grammar for a generative subset of the module language. The language of modules is built on top of a core language of expressions *e* and types *τ* which we leave abstract, except for value identifiers *x* and type identifiers *t*, so that we can extend expressions with qualified variables and types with qualified types.

**Syntactic choices** The language of module expressions and signatures is rather standard, except for a few minor design choices. We consider the following conventions: module related meta-variables use *uppercase letters*, *M*, *X*, etc. while lowercase letters are used for expressions
<figure><img src="image_45.png" /><figcaption>Figure 3: Syntax of the module language</figcaption></figure>

and types of the core language. Lists are written with an overhead bar: $\overline{D}$ is a list of $D$. In order to simplify the treatment of scoping and shadowing, we use self-references, ranged over by letter $A$, in both structures and signatures to refer to the current object; their binding occurrence appears as a subscript to the structure or signature they belong to, so that self-references can freely be renamed. Abstract types are specified as types pointing to themselves, e.g., $type t = A.t$ where $A$ is the self-reference of the current structure. In typing contexts $\Gamma$, identifiers, denoted by $I$, are prefixed by the self-reference $A$ of the structure or signature they are meant to belong to. As an implicit convention, in entries $A.I : D$, the identifier extracted from $D$ is $I$. We introduce prefixes, written with the letter $Q$, to range over either a path $P$ or a self reference $A$. We use a distinct class of variables, written $Y$, for functor parameters, which can be freely renamed. By contrast, and as usual with modules, neither identifiers $X$ and $T$ for module expressions and signatures, nor the identifiers $x$ and $t$ for core language expressions and types can be renamed, as they also play the role of an external name.

**Projections and accesses** Several restrictions are built into the grammar: field accesses inside a module type are forbidden, since prefixes $Q$ may not originate from a module type identifier $T$; and paths cannot contain functor applications, which makes the system fully *generative*. We allow projection on any module expression, but we restrict functor application to paths. Current OCAML does the opposite, mainly to prevent cases prone to trigger signature avoidance. Our choice is more general, as the OCAML one can be encoded, while the converse requires an explicit signature annotation on the functor argument.

**Omitted constructs** In addition to restricting the system to be generative, we omit some constructs for the sake of simplicity: the include operator, explicit constraints $S$ with $type t = \tau$