# Do CPS translations also translate realizers?

Samuel Gardelle¹ and Étienne Miquey²

¹ ÉNS de Lyon, France

samuel.gardelle@ens-lyon.fr

² Aix-Marseille Université, France

etienne.miquey@univ-amu.fr

## Abstract

In the realm of the proofs-as-programs correspondence, continuation-passing style (CPS) translations are known to be twofold: they bring both a program translation and a logical translation. In particular, when using the former to compile a language with a control operator, the latter ensures the soundness of the compilation with respect to types.

This work is inspired by [OS08], in which Oliva and Streicher explained how Krivine realizability could be rephrased as the composition of a CPS and an intuitionistic realizability model. In this paper, we propose to push one step forward the analysis of the relation between realizability models and CPS translations to investigate the following question: assume that two realizability models are defined using the source and the destination of a CPS translation, is it the case that the CPS translates realizers of a given formula into realizers of the translated formulas?

# 1 Introduction

Continuation-passing style translations, which where first introduced by Sussman and Steel [SS75], constitute a great tool when it comes to studying operational semantics of calculi: by making explicit the order in which reduction steps are computed, CPS translations indirectly specify an evaluation strategy for the translated calculus. In particular, continuation-passing style translations have a lot of applications in terms of compilation and have been widely studied for call-by-name and call-by-value strategies of the λ-calculus [Plo75, App92, SF93].

From a logical perspective, CPS translations are also very informative insofar as they induce a translation at the level of types that mostly amounts to a syntactical model allowing to transfer logical properties (coherence, normalization) from the target calculus [BPT17]. For instance, standard CPS translations are known to correspond to embeddings of classical logic into intuitionistic logic through variants of Gödel's negative translation [Gri90, Mur90]. Computationally, the latter corresponds to Griffin's seminal observation that a classical Curry-Howard correspondence can be obtained by extending the λ-calculus with control operators, e.g. Scheme's *call/cc*. These operators provides a *direct* handle on continuations (allowing in particular the definition of backtracking programs), as opposed to the *indirect* one provided by CPS translations. Several calculi were born from this idea, amongst which Krivine's λ_c-calculus [Kri04].

Elaborating on this calculus, Krivine developed in the late 90s the theory of classical realizability, which is a complete reformulation of its intuitionistic twin. This theory has shown to be particularly fruitful, both to analyze the computational content of proofs [Kri03, Miq11b, Miq18] or to define new models of classical theories [Kri12, Kri21].

Studying the structure of Krivine's classical realizability, Oliva and Streicher showed how the latter could in fact be viewed as the composition of a CPS with a traditional intuitionistic realizability interpretation [OS08]. This observation unveils a somewhat surprising situation: the very nature of a CPS translation is *syntactical* and as such, it is quite unexpected that this
turns out to be well-behaved with respect to realizability, a semantic notion. In fact, taking a
closer look at Oliva and Streicher's work [OS08], their (classical) realizers are defined through
the computational behavior of their CPS translation. In line with this work, Frey also defines a
notion of classical realizability directly within the target of a CPS translation [Fre16]. In both
cases, realizers are thus compatible with the CPS by definition. In a slightly different setting,
Miquel studied the witness extraction mechanism of classical realizability for Σ₀¹ formulas
through the CPS translation, but his results only apply to typed terms [Miq11b].

Therefore, none of these works tackle the following question: *do CPS translations also translate realizers?* To phrase it a bit more precisely, let us consider a CPS translation [·] from a (classical) source calculus, say Krivine $\lambda_c$-calculus, to an intuitionistic calculus, say the $\lambda$-calculus, and let us write $[·]$ for the translation on types it induces. Assume besides that these two calculi serve as the underlying language of realizers for two realizability interpretations, say for second-order classical and intuitionistic arithmetic (**PA2** and **HA2**) respectively. Now, if $t$ is a term of type $A$ (in the source), then $[t]$ is of type $[A]$ (in the destination); but *is it the case that if $t$ realizes $A$ then $[t]$ realizes $[A]$?*

To investigate this question, we will use a very convenient tool to reason about realizability
models: *evidenced frames* [CMT21] which, as we will see in Section 2.2, capture the algebraic
structure of realizability interpretations. In fact, this work was also an excuse to put this recent
notion in practice and to test the companion notion of morphism against a concrete candidate.
One can think of an evidenced frames morphism as a functional embedding of a realizability
interpretation into another one, and as such, CPS translations provide us with very natural
nontrivial candidates. The main question of this paper could indeed be rephrased in these
terms: *do CPS translations define evidenced frame morphisms?* As we shall see in Section 3.2,
the answer is nuanced in that in general a CPS translation does not induce an evidences frame
morphism, but we can nonetheless introduce another evidenced frame, which corresponds to
the image of the source calculus through the translation and can serve as the codomain of an
evidenced frame morphism.

**Outline of the paper** We start by giving a standard example of a realizability interpretation for **HA2** based on the $\lambda$-calculus in Section 2, which we will later use as the destination of the CPS translation we will consider. We take advantage of this section to recall the definition of evidenced frames, and illustrate how the interpretation for **HA2** naturally induces an evidenced frame $\mathcal{E}_{HA2}$. We then introduce (a call-by-value presentation of) Curien-Herbelin's $\lambda\mu\tilde{\mu}$-calculus in Section 3, together with its CPS translation into the (pure) $\lambda$-calculus. Finally, in Section 4 we define an evidenced frame $\mathcal{E}_{\mu\tilde{\mu}}^{\text{bv}}$ corresponding to a Krivine realizability interpretation based on the $\lambda\mu\tilde{\mu}$-calculus, and we investigate the CPS translation in terms of evidenced frame morphisms. In particular, we show that in general it does not define a morphism from $\mathcal{E}_{\mu\tilde{\mu}}^{\text{bv}}$ to $\mathcal{E}_{LJ2}$, but that another evidenced frame $\mathcal{E}_{fw}$ (which also defines a realizability interpretation for **HA2**) can be introduced for the CPS to define an appropriate morphism $\mathcal{E}_{\mu\tilde{\mu}}^{\text{bv}} \to \mathcal{E}_{fw}$.

*Due to the page limit, some proofs are only sketched and others have been omitted, an extended version with complete proofs is accessible at: https://hal.inria.fr/hal-03910311.*

## 2 Evidenced frames

Before introducing evidenced frames, we give a first example of a (very standard) realizability
interpretation that will serve both as the destination of the CPS translation considered in the
<figure><img src="image_74.png" /><figcaption>Figure 1: A type system for HA2</figcaption></figure>

sequel and as an introducing example for evidenced frames.

## 2.1 Realizability interpretation of HA2

### 2.1.1 Heyting second-order arithmetic

We start by introducing the terms and formulas of Heyting second-order arithmetic, for which we mostly follow Miquel's presentation [Miq11a]. Second-order formulas are built on top of first-order arithmetical expressions, by means of logical connectives, first- and second-order quantifications and primitive predicates. We use upper case letters for second-order variables and lower case letters for first-order ones.

We consider the usual $\lambda$-calculus terms extended with (positive) pairs and the corresponding destructor (written $\lambda(x, y).t$). In the last sections of the paper, we will also include primitives for booleans for technical purposes. The syntax of formulas and terms is given by

$$
\begin{array}{lll}
\textbf{1st-order exp.} & e ::= x \mid f(e_1, \dots, e_n) & \\
\textbf{Formulas} & A, B ::= X(e_1, \dots, e_n) \mid A \rightarrow B \mid A \land B \mid \forall x.A \mid \exists x.A \mid \forall X.A \mid \exists X.A & \\
\textbf{Terms} & t, u ::= \lambda x.t \mid t u \mid (t, u) \mid \mathbf{let} (x, y) = t \mathbf{in} u &
\end{array}
$$

where $f: \mathbb{N}^n \rightarrow \mathbb{N}$ is any primitive recursive function. We write $\Lambda$ for the set of all closed $\lambda$-terms, and we may use the following usual shorthands: $\top \triangleq \exists X.X$, $\bot \triangleq \forall X.X$ and $\neg A \triangleq A \rightarrow \bot$.

To simplify the use of existential quantifiers, as in [Miq11a], we introduce the following congruence rules, where the variables $x, X$ are not free in $B$

$$ (\exists x.A) \rightarrow B \cong \forall x.(A \rightarrow B) \qquad (\exists X.A) \rightarrow B \cong \forall X.(A \rightarrow B) \qquad (1) $$

These congruences allow us to avoid having elimination rules for the existential quantifiers, thus simplifying the resulting type system. The type system, which is given in Figure 1, corresponds to the usual rules of natural deduction. The reader may observe that in particular, no computational content is given to quantifiers in the type system.

The one-step (weak head-) reduction over terms is defined by the following rules:

$$ \frac{\overline{(\lambda x.t)u \triangleright_{\beta} t[u/x]}}{\mathbf{let} (x, y) = (u, v) \mathbf{in} t \triangleright_{\beta} t[u/x][v/y]} \qquad \frac{t \triangleright_{\beta} t'}{C[t] \triangleright_{\beta} C[t']}
where $C[] ::= [] | C[[]u] | C[let (x, y) = [] in t]$. We write $\to_\beta$ for the reflexive-transitive closure of $\triangleright_\beta$, which is known to be deterministic<fnref n="1" />, type-preserving and normalizing on typed terms [Bar92].

### 2.1.2 Realizability interpretation

We will now see how to define a realizability interpretation relying on the type system defined in Figure 1. Formulas are interpreted as saturated sets of terms, i.e. as sets of closed terms $S \subseteq \Lambda$ such that $t \to_\beta t'$ and $t' \in S$ imply that $t \in S$. We write **SAT** to denote the set of all saturated sets and, given a formula A, we call truth value its realizability interpretation.

**Definition 1 (Valuation).** A valuation is a function $\rho$ that associates a natural number $\rho(x)$ to every first-order variable $x$ and a truth value function $\rho(X)$, i.e. a function in $N^k \to \mathbf{SAT}$ to every second-order variable $X$ of arity $k$.

1. Given a valuation $\rho$, a first-order variable $x$ and a natural number $n$, we denote by $\rho, x \mapsto n$ the valuation defined by $(\rho, x \mapsto n) \triangleq \rho|_{\text{dom}(\rho)\setminus\{x\}} \cup \{x \mapsto n\}$.

2. Given a valuation $\rho$, a second-order variable $X$ of arity $k$ and a truth value function $F : N^k \to \mathbf{SAT}$, the valuation defined by $(\rho, X \mapsto F) \triangleq \rho|_{\text{dom}(\rho)\setminus\{X\}} \cup \{X \mapsto F\}$ will be denoted by $\rho, X \mapsto F$.

We say that a valuation $\rho$ is closing the formula A if $FV(A) \subseteq \text{dom}(\rho)$.

**Definition 2 (Realizability interpretation).** We interpret closed arithmetical expressions $e$ in the standard model of first-order Peano arithmetic $\mathbb{N}$. Given a valuation $\rho$ and a first-order expression $e$ (whose variables are in the domain of $\rho$) we denote its interpretation by $\llbracket e \rrbracket_\rho$. The interpretation of a formula $A$ together with a valuation $\rho$ closing $A$ is the set $|A|_\rho$ defined inductively according to the following clauses:

$$ 
\left| 
\begin{array}{l@{\quad}l}
|X(e_1, \dots, e_n)|_\rho \triangleq \rho(X)(\llbracket e_1 \rrbracket_\rho, \dots, \llbracket e_n \rrbracket_\rho) & 
  \begin{array}{@{}l@{}}
  |\forall x.A|_\rho \triangleq \bigcap_{n \in \mathbb{N}} |A|_{\rho, x \mapsto n} \\
  |\exists x.A|_\rho \triangleq \bigcup_{n \in \mathbb{N}} |A|_{\rho, x \mapsto n}
  \end{array} \\
|A \to B|_\rho \triangleq \{t \in \Lambda : \forall u \in |A|_\rho. (tu \in |B|_\rho)\} & 
  \begin{array}{@{}l@{}}
  |\forall X.A|_\rho \triangleq \bigcap_{F:N^k \to \mathbf{SAT}} |A|_{\rho, X \mapsto F} \\
  |\exists X.A|_\rho \triangleq \bigcup_{F:N^k \to \mathbf{SAT}} |A|_{\rho, X \mapsto F}
  \end{array} \\
|A \wedge B|_\rho \triangleq \{t \in \Lambda : \exists u \in |A|_\rho. \exists v \in |B|_\rho. t \to_\beta (u, v)\} & 
  \begin{array}{@{}l@{}}
  |\forall x.A|_\rho \triangleq \bigcap_{n \in \mathbb{N}} |A|_{\rho, x \mapsto n} \\
  |\exists x.A|_\rho \triangleq \bigcup_{n \in \mathbb{N}} |A|_{\rho, x \mapsto n}
  \end{array}
\end{array}
\right| 
$$

Observe that in the previous definition, the universal quantification cannot be seen as a generalized conjunction. Indeed, the conjunction is given computational content through pairs, while the universal quantifications are defined as intersections of truth values.

It is easy to see that for any formula $A$ and any valuation $\rho$ closing $A$, one has $|A|_\rho \in \mathbf{SAT}$. As it turns out, the congruences defined by Equation (1) are sound w.r.t. the interpretation.

**Proposition 3 ( [Miq11a] ).** If $A$ and $A'$ are two formulas of **HA2** such that $A \cong A'$, then for all valuations $\rho$ closing both $A$ and $A'$ we have $|A|_\rho = |A'|_\rho$.

To express that the realizability interpretation is sound with respect to the type system we need the following preliminary notions.

<footnote n="1">¹We also could have considered a non-deterministic reduction relation (i.e.. without enforcing any evaluation strategy) without altering the forecoming definition of the realizability interpretation. Nonetheless, this choice will provide us with a tighter preservation of reduction through the CPS translation.</footnote>
**Definition 4 (Substitution).** A *substitution* is a finite function $\sigma$ from $\lambda$-variables to closed $\lambda$-terms. Given a substitution $\sigma$, a $\lambda$-variable $x$ and a closed $\lambda$-term $u$, we denote by $(\sigma, x := u)$ the substitution defined by $(\sigma, x := u) \triangleq \sigma|_{\text{dom}(\sigma)\setminus\{x\}} \cup \{x := u\}$.

**Definition 5.** Given a context $\Gamma$ and a valuation $\rho$ closing the formulas in $\Gamma$, we say that a substitution $\sigma$ *realizes* $\rho(\Gamma)$ and write $\sigma \Vdash \rho(\Gamma)$ if $\text{dom}(\Gamma) \subseteq \text{dom}(\sigma)$ and $\sigma(x) \in |A|_{\rho}$ for every declaration $(x: A) \in \Gamma$.

**Definition 6.** A typing judgement $\Gamma \vdash t : A$ is *adequate* if for all valuations $\rho$ closing $A$ and $\Gamma$ and for all substitutions $\sigma \Vdash \rho(\Gamma)$ we have $\sigma(t) \in |A|_{\rho}$. More generally, we say that an inference rule $\frac{J_1 \quad \dots \quad J_n}{J_0}$ is adequate if the adequacy of all typing judgements $J_1, \dots, J_n$ implies the adequacy of the typing judgement $J_0$.

**Theorem 7 (Adequacy [Miq11a])**. The typing rules of Figure 1 are adequate.

The adequacy theorem is the key result when defining realizability interpretations in that fundamental properties stem from it. For example, we have the following corollary.

**Corollary 8 (Consistency).** There is no proof term $t$ such that $\vdash t : \bot$.

*Proof.* The proof is by *reductio ad absurdum*. It follows from Theorem 7 that if $\Gamma \vdash t : A$ is derivable, then it is adequate. In this case, this entails $t \in |\bot|_{\rho} = |\forall X.X|_{\rho} = \bigcap_{S \in \mathbf{SAT}} S = \emptyset$. $\square$

While a complete introduction to realizability interpretations and their benefits to prove properties such as soundness or normalization of typed calculi is out of the scope of this paper<fnref n="2" />, we would like to point out nonetheless that the proof of adequacy is very flexible. Indeed, if one wants to add a new instruction to the language of terms via its typing rule, it is enough to check that this typing rule is adequate while the remainder of the proof is exactly the same. For instance, to extend the present setting with booleans (as we shall do later on) it is enough to introduce terms $tt, ff$, if $b$ then $t$ else $u$ with their typing rules and to prove that the latter are adequate with the realizability interpretation.

## 2.2 Evidenced frames

In the previous section, we have seen an example of a proof system labelled with proof terms derived from the $\lambda$-calculus. Note that if proof terms are indeed realizers, there exists realizers that are not typable. Take for example a non-typable term $\Omega$, and observe that $(\lambda\_.\lambda x.x)\Omega$ is not typable but realizes $\forall X.X \to X$ because $\lambda x.x$ does. The realizability interpretation generalizes this proof system in that it is only concerned with the behavior (semantic) of proof terms and not their syntax. Note that we loose decidability but we are not concerned about it since we only want to build interpretations. The essence of a realizability interpretation lies between the interaction of a programming language and a language of formulas. The formalism of evidenced frames seeks to abstract in a unified way this structure. It is composed of a triple (with axioms) that contains two languages: evidences (programs) and proposition (formulas) as well as a relation $\cdot \to \cdot$ that connects them.

<footnote n="2">²We refer the reader interested in this to the existing literature on classical realizability, e.g. [Rie14, Lep17, Miq17].</footnote>
**Definition 9** ([CMT21]). An *evidenced frame* is a triple $(\Phi, E, \cdot, \to \cdot)$, where $\Phi$ is a set of propositions, $E$ is a collection of evidences, and $\phi_1 \stackrel{e}{\to} \phi_2$ is a ternary evidence relation on $\Phi \times E \times \Phi$, along with the following$^3$:

*Reflexivity* There exists evidence $e_{id} \in E$:

$$ - \forall \phi, \phi \stackrel{e_{id}}{\to} \phi $$

*Transitivity* There exists an operator $; \in E \times E \to E$:

$$ - \forall \phi_1, \phi_2, \phi_3, e, e'. \phi_1 \stackrel{e}{\to} \phi_2 \text{ and } \phi_2 \stackrel{e'}{\to} \phi_3 \implies \phi_1 \stackrel{e; e'}{\to} \phi_3 $$

*Top* A proposition $\top \in \Phi$ such that there exists evidence $e_{\top} \in E$:

$$ - \forall \phi, \phi \stackrel{e_{\top}}{\to} \top $$

*Conjunction* An operator $\wedge \in \Phi \times \Phi \to \Phi$ such that there exists an operator $\langle \cdot, \cdot \rangle \in E \times E \to E$ and evidences $e_{fst}, e_{snd} \in E$:

$$ - \forall \phi_1, \phi_2. \phi_1 \wedge \phi_2 \stackrel{e_{fst}}{\to} \phi_1 \qquad - \forall \phi, \phi_1, \phi_2, e_1, e_2. \phi \stackrel{e_1}{\to} \phi_1 \text{ and } \phi \stackrel{e_2}{\to} \phi_2 \implies \phi \stackrel{\langle e_1, e_2 \rangle}{\to} \phi_1 \wedge \phi_2 $$

$$ - \forall \phi_1, \phi_2. \phi_1 \wedge \phi_2 \stackrel{e_{snd}}{\to} \phi_2 $$

*Universal Implication* An operator $\supset \in \Phi \times \mathcal{P}(\Phi) \to \Phi$ such that there exists an operator $\lambda \in E \to E$ and evidence $e_{eval} \in E$:

$$ - \forall \varphi_1, \varphi_2, \vec{\phi}, e. (\forall \phi \in \vec{\phi}. \phi_1 \wedge \phi_2 \stackrel{e}{\to} \phi) \implies \phi_1 \stackrel{\lambda e}{\to} \phi_2 \supset \vec{\phi} $$

$$ - \forall \phi_1, \vec{\phi}, \phi \in \vec{\phi}. (\phi_1 \supset \vec{\phi}) \wedge \phi_1 \stackrel{e_{eval}}{\to} \phi $$

Given an evidenced frame $(\Phi, E, \cdot, \to \cdot)$, we say that $e \in E$ is *evidence* of $\phi \in \Phi$ if $\top \stackrel{e}{\to} \phi$ holds. The evidenced frame is said to *model* $\phi$ if it has evidence of $\phi$. An evidenced frame is *consistent* if it does not model $\bot$.

Note that contrary to cartesian closed categories, this formalism does not enforce any equation between arrows, in fact it does not allow for the axiomatization of reductions: we only require that the languages of propositions and evidences are expressive enough.

**Remark 10.** If there exists a huge literature describing realizability interpretations for different theories based on different notions of computations, the notion of “realizability interpretation” itself does not have a formal definition. The best approximation that one could come up with would probably be an interpretation of formulas as sets of computing terms plus some extra intuitions on how terms should compute accordingly to the connectives they realize. The study of its categorical counterpart gives a more precise picture: the interpretation should induce a tripos [Pit02, vO08]. As shown in [CMT21], evidenced frames are complete with respect to triposes, and reflect the structure of a realizability interpretations in a much more faithful way than triposes do. As such, “it is an evidenced frame” is probably the best definition one could give of a realizability interpretation, the definition of an evidenced frame and of its different components specifying how formulas are interpreted and what “to realize” means. In the next section, we will show how the realizability interpretation given for HA2 indeed defines an evidenced frame, but in the sequel of the paper, the reader should understand the existence of an evidenced frame as the definition of a realizability interpretation.

<footnote>$^3$Observe that the different construct on propositions and evidences are actually part of the definition of an evidenced frame (in particular, several different evidenced frames may be induced from one given triple $(\Phi, E, \cdot, \to \cdot)$). In the sequel, for conciseness we may nonetheless only state the existence of evidenced frames through this triple, giving the other defining constructs in the proofs.</footnote>
**Definition 11.** A morphism$^4$ from $\mathcal{EF}_1 = \langle \Phi_1, E_1, \cdot \to_1 \cdot \rangle$ to $\mathcal{EF}_2 = \langle \Phi_2, E_2, \cdot \to_2 \cdot \rangle$ is a function $F : \Phi_1 \to \Phi_2$ satisfying the following properties:

1. $\forall e_1. \exists e_2. \forall \varphi_1, \varphi'_1. \varphi_1 \xrightarrow{e_1} \varphi'_1 \implies F(\varphi_1) \xrightarrow{e_2} F(\varphi'_1)$

2. $\exists e_2. \top \xrightarrow{e_2} F(\top_1)$

3. $\exists e_2. \forall \varphi_1, \varphi'_1. F(\varphi_1) \wedge_2 F(\varphi'_1) \xrightarrow{e_2} F(\varphi_1 \wedge_1 \varphi'_1)$

4. $\exists e_2. \forall \varphi_1, \vec{\varphi}'_1. F(\varphi_1) \supset_2 \{F(\varphi'_1) | \varphi'_1 \in \vec{\varphi}'_1\} \xrightarrow{e_2} F(\varphi_1 \supset_1 \vec{\varphi}'_1)$

5. $\exists f \in \Phi_2 \to \Phi_1. \left( \left( \exists e_2. \forall \varphi_2. \varphi_2 \xrightarrow{e_2} F(f(\varphi_2)) \right) \wedge \left( \exists e_2. \forall \varphi_2. F(f(\varphi_2)) \xrightarrow{e_2} \varphi_2 \right) \right)$

In broad lines, an evidenced frame morphism $F$ from $\mathcal{EF}_1$ to $\mathcal{EF}_2$ mostly ensures (first item) that if any two propositions that are logically connected by an evidence, so are their images through $F$, and guarantees (second to fourth item) the existence of a uniform evidence that witnesses that the image of the conjunction of two propositions (and similarly for other connectives) is the logical consequence of the conjunction of images of these propositions. The last condition in turns provides us with a constructive mean to relate any proposition in the codomain $\Phi_2$ of the morphism with the image of a proposition in $\Phi_1$ that is logically equivalent to it (which is, again, witnessed by a pair of uniform evidences that do not depend of the considered proposition).

This notion of morphism provides us with the definition of a category **EF**, whose objects are evidenced frames and whose structure can be further enriched, for instance to equip morphisms from $\mathcal{EF}_1$ to $\mathcal{EF}_2$ with a preorder relation $F \preceq G$, defined to hold when there exists evidence $e_2 \in E_2$ satisfying $\forall \varphi_1 \in \Phi_1. F(\varphi_1) \xrightarrow{e_2} G(\varphi_1)$. Again, for a more detailed introduction on evidenced frame we refer the reader to the corresponding paper [CMT21], but it is worth mentioning that any evidenced frame induces a tripos (via a uniform construction that does not depend on the considered evidenced frame), and that evidenced frames are complete with respect to triposes in the sense that the category **EF** is actually equivalent to the category **Trip** of triposes.

## 2.3 The induced evidenced frame $\mathcal{EF}_{HA2}$

The interpretation of **HA2** given above induces an evidenced frame $\mathcal{EF}_{HA2}$ whose definition simply reflects the structure of the interpretation: propositions are defined by saturated sets of terms, evidences are just $\lambda$-terms and the evidence relation is given by:

$$ \psi \xrightarrow{t} \varphi \iff \forall u \in \psi.(t \ u) \in \varphi $$

This definition is reminiscent of the ordering relation on predicates induced by realizability interpretations, for instance to define triposes [Pit02].

**Proposition 12 (EF$_{HA2}$).** The triple (SAT, $\Lambda$, $\cdot \to \cdot$) defines an evidenced frame.

*Proof.* As hinted by the realizability interpretation in Definition 2, one can simply define

$$ \rho \wedge \theta \triangleq \{t \in \Lambda : \exists u \in \rho. \exists v \in \theta. t \to_{\beta} (u, v)\} \qquad \rho \supset \vec{\Theta} \triangleq \{t \in \Lambda : \forall u \in \rho. \forall \theta \in \vec{\Theta}. (t \ u) \in \theta\} $$

which both define saturated sets. Proving the existence of the required evidences is then an easy exercise of $\lambda$-calculus, which amounts to proving that the corresponding realizers exist. $\square$

<footnote>$^4$For simplicity reasons, we adopt here an extensional presentation of evidenced frames and thus of morphisms, see [CMT21] for further discussion on intensional/extensional aspects of evidenced frames and their morphisms.</footnote>
**Remark 13.** Even though we started from an interpretation of second-order Heyting arithmetic, we should insist on the fact that an evidenced frame always provides us with a model of higher-logic. Indeed, since propositions are viewed through their semantic counterpart (here as saturated sets of terms), this allows us to define a (semantic) quantification over any set of propositions regardless of what the syntax of the language accounts for. In fact, should we have considered a concrete example for an even simpler theory (say an interpretation of intuitionistic propositional logic based on the simply-typed λ-calculus), the induced evidenced frame would still give us an interpretation of higher-order logic.

Conversely, the definition of an evidenced frame only specifies the minimal requirements for the interpretation to give such a model, but the language of propositions and evidences can actually be richer. For instance, in Section 4.3 we shall use a primitive data type for booleans, while in [CMT21] an evidenced frame is build from a computational system allowing for stateful computations.

# 3 Classical logic, the λμμ-calculus and CPS translation

We present Curien-Herbelin’s λμμ-calculus [CH00], which we use afterwards as the source calculus of a CPS translation. To illustrate the flexibility of evidenced frame, we chose on purpose to pick a call-by-value source calculus. Besides, to ease the later definition of the CPS translation, we opted for a sequent calculus as advocated by [DMMZ10,DMAJ16,MM13], hence the choice of Curien-Herbelin’s λμμ-calculus<fnref n="5" />.

We first recall the syntax and operational semantics of the λμμ-calculus, before defining a well-behaved CPS that translates it to the λ-calculus defined in Section 2.1.1. We will then study the corresponding evidenced frame $\mathcal{E}_{\mu\tilde{\mu}}^{\text{bv}}$ and its relation to the CPS in Section 4. For the sake of simplicity, we will use the simply-typed version with pairs of the λμμ-calculus. Quantifications (both first and second order) will be implicitly taken care of when we define the corresponding evidenced frame $\mathcal{E}_{\mu\tilde{\mu}}^{\text{bv}}$ in the next section.

## 3.1 Curien-Herbelin's λμμ-calculus

We recall here the spirit of the Curien-Herbelin λμμ-calculus [CH00]. The key notion of the λμμ-calculus is the notion of *command*. A command $\langle t \mid e \rangle$ can be understood as a state of an abstract machine, representing the evaluation of a term *t* (the program) against a co-proof *e* (the stack) that we call *context*. The syntax and reduction rules (parameterized over a subset of terms $\mathcal{V}$ and a subset of evaluation contexts $\mathcal{E}$) are given in Figure 2, where $\tilde{\mu}x.c$ can be read as a context *let x = [·] in c*. The $\mu$ operator comes from Parigot’s λμ-calculus [Par97], $\mu\alpha$ binds a context to a context variable $\alpha$ in the same way that $\tilde{\mu}x$ binds a proof to some proof variable *x*.

The λμμ-calculus can be seen as a proof-as-program correspondence between sequent calculus and abstract machines. Right introduction rules correspond to typing rules for

<footnote n="5">⁵In fact, an even better choice when it comes to defining operational semantics and CPS translations of calculus could have been to rely upon Munch-Maccagnoni’s system L [MM13], which can be seen as a finer-grained variant of λμμ-syntax where the evaluation order is driven by the polarity of terms. In such a syntax, continuation-passing style translations are really easy to define in that the operational semantics is that of an abstract machine specifying at each step whether the term or the evaluation context is given the priority. We mostly chose to stick to Curien-Herbelin’s λμμ-calculus for the simplicity of the presentation, as its types system shares the same connectives than the one for HA2 (rather than their decompositions into linear logic). In fact, call-by-value/call-by-name variants of the λμμ-calculus are expressible and correspond to a fixed choice of polarities when decomposing the different connectives.</footnote>
<figure><img src="image_75.png" /><figcaption>Figure 2: The simply-typed $\lambda\mu\tilde{\mu}$-calculus with pairs</figcaption></figure>

proofs, while left introduction are seen as typing rules for evaluation contexts. In contrast with Gentzen's original presentation of sequent calculus, the type system of the $\lambda\mu\tilde{\mu}$-calculus explicitly identifies at any time which formula is being worked on. In a nutshell, this presentation distinguishes between three kinds of sequents: sequents of the form $\Gamma \vdash t : A \mid \Delta$ for typing terms, where the focus is put on the (right) formula $A$; sequents of the form $\Gamma \mid e : A \vdash \Delta$ for typing contexts, where the focus is put on the (left) formula $A$; sequents of the form $c : (\Gamma \vdash \Delta)$ for typing commands, where no focus is set. In a right (resp. left) sequent $\Gamma \vdash t : A \mid \Delta$, the singled out formula$^6$ $A$ reads as the conclusion "where the proof shall continue" (resp. hypothesis "where it happened before").

Regarding the reduction rules, observe that if $V$ and $\mathcal{E}$ are not restricted enough, these rules admit a critical pair:

$$c[\tilde{\mu}x.c'/\alpha] \triangleleft \langle\mu\alpha.c \parallel \tilde{\mu}x.c'\rangle \triangleright c'[\mu\alpha.c/a].$$

The difference between call-by-name and call-by-value can be characterized by how this critical pair is solved, by defining $V$ and $\mathcal{E}$ in such a way that the two rules do not overlap. This justifies the definition of a subcategory $V$ of proofs, that we call *values*, and of the dual subset $E$ of contexts that we call *co-values* (following Downen and Ariola's denomination [DA14]):

$$\textbf{Values} \quad V ::= x \mid \lambda x.t \mid (V_1, V_2)$$

$$\textbf{Co-values} \quad E ::= \alpha \mid t \cdot e$$

The call-by-name evaluation strategy amounts to the case where $V \triangleq \text{Terms}$ and $\mathcal{E} \triangleq \text{Co-values}$, while call-by-value corresponds to $V \triangleq \text{Values}$ and $\mathcal{E} \triangleq \text{Contexts}$. In the sequel, we

<footnote>$^6$This formula is often referred to as the formula in the *stoup*, a terminology due to Girard.</footnote>
will focus on the latter and we write ▷bv for the corresponding reduction steps and →bv for its reflexive-transitive closure. Since the by-value reduction rule for $\tilde{\mu}(x, y).c$ only computes in front of a pair of values, we restrict the syntax to these pairs and define pairs of (non-evaluated) terms through the shorthand (which simulate the left-to-right opening of such pairs):

$$ (t, u) \triangleq \mu\alpha.\langle t \parallel \tilde{\mu}x.\langle u \parallel \tilde{\mu}y.\langle (x, y) \parallel \alpha \rangle \rangle $$

Readers more accustomed to the $\lambda$-calculus may wonder why the syntax of terms does not include the usual application (which we write $t@u$ below), but this can be expressed as a macro, as well as the let $\cdot = \cdot$ in construct:

$$ t@u \triangleq \mu\alpha.\langle t \parallel u \cdot \alpha \rangle $$

$$ \text{let } x = t \text{ in } u \triangleq \mu\alpha.\langle t \parallel \tilde{\mu}x.\langle u \parallel \alpha \rangle \rangle $$

In particular, the $\beta$-reduction is simulated by the reduction of $\lambda\mu\tilde{\mu}$ commands, since if $t, u \in \Lambda$ are such that $t \to_{\beta} u$, then for any stack $e$ we have $\langle t \parallel e \rangle \to_{\beta}^{*} \langle u \parallel e \rangle$. In our setting, we can observe that the relation ▷bv induces a (weak-head) call-by-value evaluation strategy for the application, since if $u$ reduces (in front of any context) to value $V$, we have:

$$ \langle \lambda x. t @ u \parallel e \rangle \to_{bv} \langle u \parallel \tilde{\mu} x. \langle t \parallel e \rangle \rangle \to_{bv} \langle V \parallel \tilde{\mu} x. \langle t \parallel e \rangle \rangle \to_{bv} \langle t [V/x] \parallel e \rangle $$

that is analogous to the expected reduction thread in a call-by-value evaluated $\lambda$-calculus:

$$ (\lambda x.t)u \to_{\beta} \text{let } x = u \text{ in } t \to_{\beta} \text{let } x = V \text{ in } t \to_{\beta} t[V/x] $$

Readers familiar with control operators may observe that we can implement call/cc as well as continuations in this calculus as follows:

$$ \text{call/cc} \triangleq \lambda x. \mu \alpha. \langle x \parallel \mathbf{k}_{\alpha} \cdot \alpha \rangle $$

$$ \mathbf{k}_e \triangleq \lambda y. \mu_. \langle y \parallel e \rangle $$

Forgetting a minute about the call-by-value restriction, we can check that these definitions yield the expected computational behavior of call/cc: in front of a stack $t \cdot e$, it catches the context $e$ thanks to the $\mu\alpha$ binder and reduces as follows:

$$ \langle \text{call/cc} \parallel t \cdot e \rangle = \langle \lambda x. \mu \alpha. \langle x \parallel \mathbf{k}_{\alpha} \cdot \alpha \rangle \parallel t \cdot e \rangle \triangleright \langle \mu \alpha. \langle t \parallel \mathbf{k}_{\alpha} \cdot \alpha \rangle \parallel e \rangle \triangleright \langle t \parallel \mathbf{k}_e \cdot e \rangle $$

In turns, in front of a stack $u \cdot e'$, the continuation $\mathbf{k}_e$ will now catch the context $e'$ and throw it away to restore the former context $e$:

$$ \langle \mathbf{k}_e \parallel u \cdot e' \rangle = \langle \lambda y. \mu_. \langle y \parallel e \rangle \parallel u \cdot e' \rangle \triangleright \langle \mu_. \langle u \parallel e \rangle \parallel e' \rangle \triangleright \langle u \parallel e \rangle $$

From a logical perspective, it is an easy exercise to check that call/cc can be typed with Peirce's law.

## 3.2 Continuation-passing style translation of the call-by-value $\lambda\mu\tilde{\mu}$-calculus

We define a CPS translation for the call-by-value variant of the $\lambda\mu\tilde{\mu}$-calculus introduced previously which is analogous to the translations in [CH00, Miq17]. The definition of the translation can be mechanically derived from the operational semantics of the calculus, following the methodology of Danvy's semantic artifacts described in [ADH+12, Miq17], or the decomposition of the $\lambda\mu\tilde{\mu}$-calculus into Munch-Maccagnoni's system L [MM13]. As is usual in
call-by-value, the translation is defined on three layers, reflecting the three syntactic categories at play: $[\cdot]_t$ on terms, $[\cdot]_e$ on contexts and $[\cdot]_v$ on values.

$$ \begin{array}{l@{\qquad}l} \llbracket t \parallel e \rrbracket_c & \triangleq [t]_t [e]_e \\ [\mu\alpha.c]_t & \triangleq \lambda e.(\lambda\alpha.[c]_c) e \\ [V]_t & \triangleq \lambda e.e [V]_v \\ [u \cdot e]_e & \triangleq \lambda V.V [u]_t [e]_e \\ [\tilde{\mu}x.c]_e & \triangleq \lambda V.(\lambda x.[c]_c) V \end{array} \qquad \begin{array}{l} [\tilde{\mu}(x, y).c]_e \triangleq \lambda V.\mathbf{let} (x, y) = V \mathbf{in} [c]_c \\ [\alpha]_e \triangleq \alpha \\ [x]_v \triangleq x \\ [(V_1, V_2)]_v \triangleq ([V_1]_v, [V_2]_v) \\ [\lambda x.t]_v \triangleq \lambda u.e.u (\lambda x.[t]_t e) \end{array} $$

The computational translation induces the following translation on types:

$$ \begin{array}{l@{\qquad}l} \llbracket A \rrbracket_t & \triangleq \llbracket A \rrbracket_e \rightarrow \mathcal{R} \\ \llbracket A \rrbracket_e & \triangleq \llbracket A \rrbracket_v \rightarrow \mathcal{R} \end{array} \qquad \begin{array}{l} \llbracket A \rightarrow B \rrbracket_v \triangleq \llbracket A \rrbracket_t \rightarrow \llbracket B \rrbracket_e \rightarrow \mathcal{R} \\ \llbracket A \wedge B \rrbracket_v \triangleq \llbracket A \rrbracket_v \wedge \llbracket B \rrbracket_v \\ \llbracket X \rrbracket_v \triangleq X \end{array} $$

where $\mathcal{R}$ is the return type of continuations, usually defined as $\mathcal{R} \triangleq \perp$. This translation extends naturally to contexts, where the translation of $\Gamma$ is defined in terms of values while $\Delta$ is translated in terms of contexts:

$$ \llbracket \Gamma, x : A \rrbracket_v \triangleq \llbracket \Gamma \rrbracket_v, x : [A]_v \qquad \llbracket \Delta, \alpha : A \rrbracket_e \triangleq \llbracket \Delta \rrbracket_e, \alpha : [A]_e $$

**Remark 14.** Usually, the return type $\mathcal{R}$ is chosen to be some specific formula of the target language (here **HA2**). Actually, we can even consider an even more general settings, where we extend the language of formulas with a new constant $\mathcal{R}$ for which we only have to provide its realizability interpretation as a saturated set of terms (i.e. $|\mathcal{R}| \in \mathbf{SAT}$). Since no typing rule is provided for $\mathcal{R}$, it can be understood as a generalization of $\perp$: any derivation of $\mathcal{R}$ can be turned into a derivation of $\perp$ (and vice-versa), but contrarily to $|\perp| = |\forall X.X| = \emptyset$, the semantic interpretation of $\mathcal{R}$ can be chosen not to be empty.

The translation of terms, contexts and commands is sound with respect both to types and computations$^7$, as shown by the following propositions:

**Proposition 15** (CH00, Miq17]). For any contexts $\Gamma$ and $\Delta$, we have

1. if $\Gamma \vdash t : A \mid \Delta$ then $\llbracket \Gamma \rrbracket_v, \llbracket \Delta \rrbracket_e \vdash [t]_t : \llbracket A \rrbracket_t$

2. if $\Gamma \mid e : A \vdash \Delta$ then $\llbracket \Gamma \rrbracket_v, \llbracket \Delta \rrbracket_e \vdash [e]_e : \llbracket A \rrbracket_e$

3. if $c : \Gamma \vdash \Delta$ then $\llbracket \Gamma \rrbracket_v, \llbracket \Delta \rrbracket_e \vdash [c]_c : \mathcal{R}$

**Proposition 16** (Simulation). For any $c, c'$, we have: $c \rightarrow_{bv} c'$ if and only if $[c]_c \rightarrow_{\beta} [c']_c$.

*Proof.* The direct implication is standard and proven by induction on $\triangleright_{bv}$ [Miq17]. The “only if” part is proven by contradiction, by considering $c$ and $c'$ with the shortest reduction path $[c]_c \rightarrow_{\beta} [c']_c$ possible, then reasoning by induction on $c$. $\square$

# 4 CPS translation of realizers

We are now ready to examine Oliva and Streicher result through the lens of evidenced frames, and investigate the main question of this paper.

<footnote>$^7$To be even more precise, we could restrict ourselves to a weak-head call-by-name evaluation strategy with the same result.</footnote>
## 4.1 A call-by-value classical realizability interpretation

We begin by defining the evidenced frame induced by the realizability interpretation that the call-by-value $\lambda\mu\tilde{\mu}$-calculus yields. The structure of this interpretation differs from the (intuitionistic) interpretation introduced in Section 2.1.2 mostly for two reasons: a) it is a classical (à la Krivine) interpretation, and b) it is based on a call-by-value calculus.

As in intuitionistic realizability, every formula $A$ is interpreted in classical realizability as a set $|A|_t$ of terms (the realizers) that share a common computational behavior determined by the structure of the formula $A$ [Kri04]. However the difference between intuitionistic and classical realizability is that in the latter, the set of realizers of $A$ is defined indirectly, that is from a set $\|A\|_e$ of contexts that are intended to challenge the truth of $A$. Intuitively, the set $\|A\|_e$ (which we shall call the falsity value of $A$) can be understood as the set of all possible counter-arguments to the formula $A$. In this framework, a program realizes the formula $A$ if and only if it is able to defeat all the attempts to refute $A$ by a context in $\|A\|_e$.

When defining such an interpretation on a call-by-value calculus, the falsity value itself is in fact defined in terms of a more primitive notions of truth values of values [MM09]. This set, which we write $|A|_V$, can be understood as the values that any test challenging $A$ should accept as a valid answer.

The last ingredient peculiar to Krivine realizability is the fact that realizability interpretations are parameterized by a set of commands, the pole, which intuitively represents the valid computations.

**Definition 17 (Pole).** A pole $\perp$ is a saturated set of commands, i.e. a set such that if $c \to_{bv} c'$ and $c' \in \perp$ then $c \in \perp$. It should be seen as a set of commands whose computations end with success.

**Definition 18 (Orthogonal).** Given a pole $\perp$, we define $A^\perp$ to be the orthogonal of $A$: if $A$ is a set of terms (resp. contexts), it is the set of contexts $e$ (resp. terms $t$) such that $\langle t \| e \rangle \in \perp$.

The complete definition of the realizability interpretation based on the call-by-value $\lambda\mu\tilde{\mu}$-calculus introduced before would require once again to define the appropriate notions of valuations, adequate judgements, etc... Such definitions can be found for analogous interpretation in [MM09, Lep16, Miq20], and will be somewhat hidden here between the lines of the definition of the induced evidenced frame $\mathcal{E}_{\mu\tilde{\mu}}^{\text{bv}}$. Let us however explain how connectives are interpreted in terms of values. The aforementioned sets of truth and falsity values are then defined by orthogonality to each others, i.e. $|A|_t = \|A\|_e^\perp$ and $\|A\|_e = |A|_V^\perp$, which in particular implies that $|A|_V \subseteq |A|_t$. For $A$ and $B$ two closed formulas, values realizing implication (resp. the conjunction) are the expected ones, namely functions (resp. pairs):

$$|A \to B|_V = \{\lambda x.t : \forall V \in |A|_V : t[V/x] \in |B|_t\} \qquad |A \wedge B|_V = \{(V_1, V_2) : V_1 \in |A|_V \wedge V_2 \in |B|_V\}$$

Recall that even if the type system introduced earlier does not include quantifiers, we can nevertheless define them through their semantic interpretation in terms of values, namely as an intersection of primitive truth values (where $\rho$ should be the appropriate notion of valuation for this setting, and $X$ ranges over propositions):

$$|\forall x.A|_V^\rho = \bigcap_{n \in \mathbb{N}} |A|_V^{\rho, x \to n} \qquad |\forall X.A|_V^\rho = \bigcap_{F \in \mathcal{P}(V)} |A|_V^{\rho, X \to F}$$

The corresponding evidenced frame thus uses sets of values as propositions, terms as evidences (we write $\mathcal{T}$ for the set of closed terms) and the following evidence relation

$$\varphi \xrightarrow{t} \psi \iff \forall V \in \varphi : t@V \in \psi^{\perp\perp}$$
**Theorem 19** ($\mathcal{E}\mathcal{F}_{\mu\tilde{\mu}}^{\text{bv}}$). The triple $\mathcal{E}\mathcal{F}_{\mu\tilde{\mu}}^{\text{bv}} \triangleq (\mathcal{P}(V), \mathcal{T}, \cdot \to \cdot)$ defines an evidenced frame.

## 4.2 CPS as a morphism

We now wish to investigate whether the CPS translation defined in Section 3.2 defines an evidenced frame morphism from $\mathcal{E}\mathcal{F}_{\mu\tilde{\mu}}^{\text{bv}}$ to $\mathcal{E}\mathcal{F}_{\text{HA2}}$. To be precise, recall that so far our definitions for the interpretations of the source and destination of the translation leave us two degrees of liberty: the choice of pole in $\mathcal{E}\mathcal{F}_{\mu\tilde{\mu}}^{\text{bv}}$, which we shall write $\perp_s$; and the realizability interpretation of the return type $\mathcal{R}$, which we write $|\mathcal{R}| = \perp_d$. As we shall see in Section 4.3, we cannot build a morphism that works for any choice for these parameters and these two evidenced frames. However, we investigate the following questions: given an interpretation $\perp_s$, can we find a pole $\perp_d$ for $\mathcal{R}$ such that $[\cdot]_\mathcal{V}$ defines an evidenced frame morphism? Reciprocally, given a pole $\perp_d$, can we find an appropriate $\perp_s$?

### 4.2.1 The forward evidenced frame

We first tackle the first problem, that is to define from a fixed pole $\perp_s$ in the source an interpretation $\perp_d$ for $\mathcal{R}$ such that the CPS induces a morphism, we can restrict ourselves to consider instead the image of $\mathcal{E}\mathcal{F}_{\mu\tilde{\mu}}^{\text{bv}}$ through the CPS translation as an evidenced frame itself (as is done in [OS08]). To begin with, we define the interpretation of the return type $\mathcal{R}$ as the saturation of the image of the pole $\perp_s$ through the CPS:

$$ \perp_d \triangleq \{t : \exists c \in \perp_s.t \to \beta [c]_c\} $$

We take as propositions the images of sets of values through the translation of values $[\cdot]_\mathcal{V}$, i.e. $\Phi_{fw} \triangleq [\mathcal{P}(\text{values})]_\mathcal{V}$. Similarly, we take evidences to be translated terms: $E_{fw} \triangleq [\text{terms}]_t$. As for the evidence relation, we can see it as the image of the evidence relation in $\mathcal{E}\mathcal{F}_{\mu\tilde{\mu}}^{\text{bv}}$ through the translation (up to some technical details), that is:

$$ \varphi \xrightarrow{t}_{fw} \psi \triangleq \forall V \in \phi. \forall e \in \text{contexts.} [ (\forall [V']_\mathcal{V} \in \psi : [V']_t [e]_e \in \perp_d) \Rightarrow (t \# V) [e]_e \in \perp_d ] $$

where $a\#b \triangleq \lambda\alpha.a$ ($\lambda V.V$ ($\lambda e.e$ b) $\alpha$). This operator is solely motivated by technical reasons, in order to satisfy the equation $[t@V]_t = [t]_t \# [V]_\mathcal{V}$.

**Theorem 20.** $\mathcal{E}\mathcal{F}_{fw} = (\Phi_{fw}, E_{fw}, \cdot \to_{fw})$ defines an evidenced frame and the map $F : V \mapsto [V]_\mathcal{V}$ induces a morphism from $\mathcal{E}\mathcal{F}_{\mu\tilde{\mu}}^{\text{bv}}$ to $\mathcal{E}\mathcal{F}_{fw}$.

*Proof.* The first part mostly relies on the observation that $[\cdot]_t$ is injective and admits an inverse (see the proof of Prop. 22). The evidences that make the morphism well-behaved w.r.t. the connectives are just obtained as the translation $[\cdot]_t$ of the corresponding evidences in $\mathcal{E}\mathcal{F}_{\mu\tilde{\mu}}^{\text{bv}}$. $\square$

As the proof of Theorem 20 shows, not only does the CPS translation induce a morphism, but it does so while preserving evidences. In other words, in this setting, we can actually conclude that the CPS translation does preserve realizers. Observe nonetheless that this is almost a tautology, in that evidences in $\mathcal{E}\mathcal{F}_{fw}$ are by definition translated terms. In particular, if $\mathcal{E}\mathcal{F}_{fw}$ defines a model for HA2, it is by nature very different from the one that $\mathcal{E}\mathcal{F}_{HA2}$ provides.

### 4.2.2 The backward evidenced frame

We now tackle the other question, that is, we consider a fixed interpretation $\perp_d \in \text{SAT}$ of the return type $\mathcal{R}$ in the realizability interpretation. To define a pole in the source of the
translation, we simply pick the sets $\perp_s = \{c : [c]_c \in \perp_d\}$ of commands whose translations belong to $\perp_d$. This indeed defines a saturated set of commands, since the translation $[\cdot]_c$ preserves computation and $\perp_d$ is itself a saturated set of terms.

For technical reasons, we now take propositions to be pairs made of the translation of a proposition in $\mathcal{E}\mathcal{F}_{\mu\tilde{\mu}}^{\text{bv}}$ and the translation of its orthogonal set: $\Phi_{bw} = \{([S]_V, [S^{\perp}]_e) : S \in \mathcal{P}(V)\}$. Evidences are again defined as translation of terms $E_{bw} = [\text{terms}]_t$ while the evidence relation is given by:

$$ (\varphi^V, \varphi^e) \xrightarrow{t}^{\text{bw}} (\psi^V, \psi^e) \iff \forall V \in \varphi^V. \forall e \in \psi^e. (t \# V) e \in \perp_d $$

**Theorem 21.** The triple $\mathcal{E}\mathcal{F}_{bw} = (\Phi_{bw}, E_{bw}, \xrightarrow{\cdot}^{\text{bw}})$ defines an evidenced frame and the map $F : V \mapsto ([V]_V, [V^{\perp}]_e)$ induces a morphism from $\mathcal{E}\mathcal{F}_{\mu\tilde{\mu}}^{\text{bv}}$ to $\mathcal{E}\mathcal{F}_{bw}$.

The proof is analogous to the one of Theorem 20 (in particular, realizers are also trivially preserved in this case), and actually unveils that $\mathcal{E}\mathcal{F}_{fw}$ and $\mathcal{E}\mathcal{F}_{bw}$ are essentially the same.

**Proposition 22.** For any term $t$, we have: $(\varphi^V, \varphi^e) \xrightarrow{[t]_t}^{\text{bw}} (\psi^V, \psi^e) \iff \varphi^V \xrightarrow{[t]_t}^{\text{fw}} \psi^V$.

*Proof.* We prove that both statements are equivalent to $[\varphi]_V^{-1} \xrightarrow{t}^{\perp_d} [\psi]_V^{-1}$, where $[\cdot]_V^{-1}$ is the inverse of the injective map $[\cdot]_V$. This relies in turn on the definitions of the poles $\perp_d$, $\perp_s$ and on the fact that the CPS translation simulates computations (Proposition 16). $\square$

## 4.3 A counter-example

We shall now give an example of a pole $\perp_s$ together with a term that is a realizer in the interpretation based on the $\lambda\mu\tilde{\mu}$-calculus, but whose translation is not a realizer of the translated formula. We follow here the lines of Oliva-Streicher's presentation of Krivine realizability through a CPS translation, in particular we assume that an interpretation of the return type $\perp_d$ is given and we define the pole $\perp_s \triangleq \{c : [c]_c \in \perp_d\}$ consequently. In the rest of this section, we write $t \Vdash_s A$ when $t$ is a $\lambda\mu\tilde{\mu}$-term which realizes $A$ in the source, and $t \Vdash_d A$ when $t$ is a $\lambda$-term realizing $A$ in the destination.

To give a simple example, we will extend thereafter the definitions of the source and destination of the CPS to include a type $\mathbb{B}$ of booleans, whose translation at the level of types will be given by: $[\mathbb{B}]_t = (\mathbb{B} \to \mathcal{R}) \to \mathcal{R}$, and we will present a term $t$ such that $t \Vdash_s \mathbb{B}$ but $[t]_t \nVdash_d [\mathbb{B}]_t$. Let us briefly guide the reader through the rationale of our construction. To prove that $[t]_t \nVdash_d [\mathbb{B}]_t$, we shall exhibit a continuation $k \Vdash_d \mathbb{B} \to \mathcal{R}$ such that $[t]_t k \notin \perp_d$. By definition, if $t \Vdash_s \mathbb{B}$ in particular for any context $e \in \|\mathbb{B}\|_e$, the fact that $\langle t \| e \rangle \in \perp_s$ means that $[t]_t [e]_e \in \perp_d$. Therefore we should look for a continuation that is not in the image of the CPS translation. Besides, $[t]_t k$ should not reduce to $kb$ where $b$ is a boolean, since otherwise the fact that $k \Vdash_d \mathbb{B} \to \mathcal{R}$, $b \Vdash_d \mathbb{B}$ and antireduction would also entail that $[t]_t k \in \perp_d$. For these reasons, we will pick an inert constant $\kappa$ for $t$, define the pole $\perp_d$ to enforce $\kappa \Vdash_d \mathbb{B}$ and select a continuation $k$ that will be syntactically discriminated for any translated context.

### 4.3.1 Extension with booleans

We briefly review the extensions of the $\lambda\mu\tilde{\mu}$-calculus and of the $\lambda$-calculus to include a type $\mathbb{B}$ of booleans in the corresponding languages of formulas. We first extend the syntax and reduction rules of the $\lambda\mu\tilde{\mu}$-calculus to account for boolean values $tt$ and $ff$, a context to eliminate booleans and an inert term $\kappa$:

<table><tr><td>Terms</td><td>t ::= ... | κ</td><td>⟨tt⟩ ||<sub>μB.[c<sub>1</sub> | c<sub>2</sub>]</sub> ▷<sub>bw</sub> c<sub>1</sub></td></tr><tr><td>Values</td><td>V ::= ... | tt | ff</td><td>⟨ff⟩ ||<sub>μB.[c<sub>1</sub> | c<sub>2</sub>]</sub> ▷<sub>bw</sub> c<sub>2</sub></td></tr><tr><td>Contexts</td><td>e ::= ... | μ̃B.[c<sub>1</sub> | c<sub>2</sub>]</td><td></td></tr></table>
These terms can be typed with the following rules:

$$ \frac{c_1 : (\Gamma \vdash \Delta) \qquad c_1 : (\Gamma \vdash \Delta)}{\Gamma \mid \tilde{\mu}\mathbb{B}.[c_1 \mid c_2] : \mathbb{B} \vdash \Delta} \quad (\mathbb{B}_t) \qquad \frac{\Gamma \vdash \mathrm{tt} : \mathbb{B} \mid \Delta}{\Gamma \vdash \mathrm{ff} : \mathbb{B} \mid \Delta} \quad (\mathrm{ff}) $$

Similarly, the $\lambda$-calculus that serves as a destination of the CPS translation can be extended with booleans and an inert constant, for which we use the same notations:

$$ t, u ::= \dots \mid \kappa \mid \mathrm{ff} \mid \mathrm{tt} \mid \text{if } t \text{ then } u \text{ else } v \quad \big| \quad \text{if } \mathrm{tt} \text{ then } u \text{ else } v \triangleright_{\beta} u \quad \text{if } \mathrm{ff} \text{ then } u \text{ else } v \triangleright_{\beta} v $$

Once again, we can give typing rules to the terms computing with booleans:

$$ \frac{\Gamma \vdash b : \mathbb{B} \qquad \Gamma \vdash t : A \qquad \Gamma \vdash u : A}{\Gamma \vdash \text{ if } b \text{ then } t \text{ else } u : A} \quad (\text{if}) \qquad \frac{\Gamma \vdash \mathrm{tt} : \mathbb{B}}{\Gamma \vdash \mathrm{ff} : \mathbb{B}} \quad (\text{ff}) $$

The CPS translation is then naturally extended (following what is already defined for values and base types):

$$ [[\mathbb{B}]]_v \triangleq \mathbb{B} \quad | \quad [[\mathrm{tt}]]_v \triangleq \mathrm{tt} \quad | \quad [[\mathrm{ff}]]_v \triangleq \mathrm{ff} \quad | \quad [\tilde{\mu}\mathbb{B}.[c_1 \mid c_2]]_e \triangleq \lambda b. \text{ if } b \text{ then } [c_1]_c \text{ else } [c_2]_c \quad | \quad [\kappa]_t \triangleq \kappa $$

It is straightforward to verify that the different properties of the CPS translation still hold for the extended calculi.

### 4.3.2 An untranslatable realizer

It now only remains to extend the realizability interpretation, in the $\lambda\mu\tilde{\mu}$-calculus we simply define the primitive truth value of $\mathbb{B}$ as the set containing the two boolean values

$$ |\mathbb{B}|_v \triangleq \{\mathrm{tt}, \mathrm{ff}\} $$

while for the intuitionistic interpretation based on the target calculus, we consider the set of terms reducing to a boolean value:

$$ |\mathbb{B}| \triangleq \{t \to_{\beta} \mathrm{tt}\} \cup \{t \to_{\beta} \mathrm{ff}\} $$

These definitions make the typing rules for booleans adequate with the corresponding realizability interpretations.

Finally, we define the pole (and thus the realizability interpretations), which will allow us to complete the construction of the counter-example:

$$ \perp_{\mathrm{d}} \triangleq \{u \in \Lambda : u \to_{\beta} [t]_t \lambda x.v \text{ for some term } v\} \qquad \perp_{\mathrm{s}} \triangleq \{c : [c]_c \in \perp_{\mathrm{d}}\} $$

**Lemma 23.** We have $\kappa \Vdash_{\mathrm{s}} \mathbb{B}$

*Proof.* Since any context $e$ translates into a function of the shape $\lambda x.v$, for any context $e \in \|\mathbb{B}\|_e$, we have in particular $[\langle\kappa\|e\rangle]_c = \kappa[e]_e \in \perp_{\mathrm{d}}$, and then $\langle\kappa\|e\rangle \in \perp_{\mathrm{s}}$. $\square$

**Lemma 24.** Let us fix $p \in \perp_{\mathrm{d}}$, and define $\mathbf{k} \triangleq (\lambda x.x)\lambda b.p$. Then it holds that $\mathbf{k} \Vdash_{\mathrm{d}} \mathbb{B} \to \mathcal{R}$.

*Proof.* Recall that we define $|\mathcal{R}| = \perp_{\mathrm{d}}$ and $|\mathbb{B}| = \{t : t \to_{\beta} b \text{ with } b \in \mathbb{B}\}$. Let $b \in \mathbb{B}$, and $t$ be such that $t \to_{\beta} b$. We have

$$ \mathbf{k}t = ((\lambda x.x)\lambda b.p)t \to_{\beta} (\lambda b.p)t \to_{\beta} p \in \perp_{\mathrm{d}} $$

hence the fact that $\mathbf{k} \Vdash_{\mathrm{d}} \mathbb{B} \to \mathcal{R}$ by antireduction. $\square$
We can now check that :

**Proposition 25.** We have $[\kappa]_t \nvdash_d [[\mathbb{B}]_t]$.

*Proof.* We have $[\kappa]_t \mathbf{k} = \kappa \mathbf{k}$. Since this term does not reduce (recall that $\beta$ is a weak-head reduction relation) and $\mathbf{k}$ is not of the shape $\lambda x.v$, it does not belong to $\perp_d$. The result then follows from Lemma 24. □

Nonetheless, this example is not entirely satisfying in that the subsequent realizability interpretation is not coherent:

**Proposition 26.** The closed term $t_\perp \triangleq \mu\alpha.\langle\kappa \parallel \tilde{\mu}x.\langle x \parallel \alpha\rangle$ satisfies $t_\perp \nvdash_s \perp$.

*Proof.* Indeed, for any context $e$ we have:

$$ \langle t_\perp \parallel e \rangle \triangleright_{bv} \langle \kappa \parallel \tilde{\mu}x. \langle x \parallel e \rangle \rangle $$

Since $[\tilde{\mu}x.\langle x \parallel e \rangle]_e = \lambda x.(\lambda k.k x)[e]_e$, in particular we have $\kappa [\tilde{\mu}x.\langle x \parallel e \rangle]_e \in \perp_d$ and thus $\langle t_\perp \parallel e \rangle \in \perp_s$ by antireduction. □

# 5 Conclusion

As mentioned in the introduction, the motivation behind this work was twofold. On the one hand, from a methodological perspective, this work also was a pretext to experiment with evidenced frames as a tool to reason on realizability interpretation. As such, the result of this experimentation turns out to be pretty satisfactory, for they have shown to be very helpful during the research process to identify the key ingredients necessary for the different results exposed. In particular, they provided us with a precious algebraic viewpoint to avoid loosing ourselves in the implementation details of realizers and translations. In particular, we could easily reproduce Oliva-Streicher's construction while using different calculi.

On the other hand, from a logical perspective, we were actually really interested in the question raised in the title. In that regards, we gave here partial answers, by giving some sufficient conditions, namely the restriction to the backward and forward evidenced frame, for CPS translations to be well-behaved with respect to the realizability interpretations; as well as an example of two realizability interpretations where the translation does not preserve realizers. Many interesting questions remain to be explored in that direction: are there counter-examples that do not require an incoherent pole? What can be said in general of realizers that are compatible with the CPS translation? In particular, which are the terms that are always compatible (i.e. regardless of the choice of $\perp_d$ and $\perp_s$) with a CPS? In particular, it would be very interesting to wonder whether universal realizers (i.e. compatible with any pole) are soundly CPS translated. This can be shown for simple data types (for instance boolean or natural numbers) by means of specification techniques [GM16a, GM16b] (but more details on this would drive us out of the scope of this paper), and is still to be investigated for more complex types (functions, etc.).

It is worth mentioning that all these questions go beyond the sole case of CPS translations and also extend to other syntactic translations, and in particular to a wide range of effects accounted for by monads. On a long-term perspective, a lot is yet to be learned on the syntactic translations that are compatible with semantics interpretations, that is, which yield EF morphisms preserving evidences.
References

[ADH<sup>+</sup>12] Zena M. Ariola, Paul Downen, Hugo Herbelin, Keiko Nakata, and Alexis Saurin. Classical call-by-need sequent calculi: The unity of semantic artifacts. In Tom Schrijvers and Peter Thiemann, editors, *Functional and Logic Programming - 11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012. Proceedings*, Lecture Notes in Computer Science, pages 32–46. Springer, 2012.

[App92] Andrew W. Appel. *Compiling with Continuations*. Cambridge University Press, New York, NY, USA, 1992.

[Bar92] Henk Barendregt. Lambda calculi with types. In S. Abramsky, Dov M. Gabbay, and S. E. Maibaum, editors, *Handbook of Logic in Computer Science (Vol. 2)*, pages 117–309. Oxford University Press, Inc., New York, NY, USA, 1992.

[BPT17] Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau. The next 700 syntactical models of type theory. In *Proceedings of CPP 2017*, pages 182–194, New York, NY, USA, 2017. ACM.

[CH00] Pierre-Louis Curien and Hugo Herbelin. The duality of computation. In *Proceedings of ICFP 2000*, SIGPLAN Notices 35(9), pages 233–243. ACM, 2000.

[CMT21] Liron Cohen, Étienne Miquey, and Ross Tate. Evidenced frames: A unifying framework broadening realizability models. In *2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)*, pages 1–13, 2021.

[DA14] Paul Downen and Zena M. Ariola. The duality of construction. In Zhong Shao, editor, *Programming Languages and Systems*, pages 249–269, Berlin, Heidelberg, 2014. Springer Berlin Heidelberg.

[DMAJ16] Paul Downen, Luke Maurer, Zena M. Ariola, and Simon Peyte Jones. Sequent calculus as a compiler intermediate language. In *ICFP 2016*, 2016.

[DMMZ10] Olivier Danvy, Kevin Millikin, Johan Munk, and Ian Zerny. *Defunctionalized Interpreters for Call-by-Need Evaluation*, pages 240–256. Springer Berlin Heidelberg, Berlin, Heidelberg, 2010.

[Fre16] Jonas Frey. Classical Realizability in the CPS Target Language. *Electronic Notes in Theoretical Computer Science*, 325(Supplement C):111 – 126, 2016. The Thirty-second Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXII).

[GM16a] Mauricio Guillermo and Alexandre Miquel. Specifying Peirce’s law in classical realizability. *Mathematical Structures in Computer Science*, 26(7):1269–1303, 2016.

[GM16b] Mauricio Guillermo and Étienne Miquey. Classical realizability and arithmetical formulæ. *Mathematical Structures in Computer Science*, page 1–40, 2016.

[Gri90] Timothy Griffin. A formulae-as-type notion of control. In *Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, POPL '90, pages 47–58, New York, NY, USA, 1990. ACM.

[Kri03] Jean-Louis Krivine. Dependent choice, ‘quote’ and the clock. *Th. Comp. Sc.*, 308:259–276, 2003.

[Kri04] Jean-Louis Krivine. A call-by-name lambda-calculus machine. In *Higher Order and Symbolic Computation*, 2004.

[Kri12] Jean-Louis Krivine. Realizability algebras II : new models of ZF + DC. *Logical Methods in Computer Science*, 8(1):10, February 2012. 28 p.

[Kri21] Jean-Louis Krivine. A program for the full axiom of choice. *Logical Methods in Computer Science*, Volume 17, Issue 3, September 2021.

[Lep16] Rodolphe Lepigre. A classical realizability model for a semantical value restriction. In Peter Thiemann, editor, *Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016*,
*Proceedings*, volume 9632 of *Lecture Notes in Computer Science*, pages 476–502. Springer, 2016.

[Lep17] Rodolphe Lepigre. *Semantics and Implementation of an Extension of ML for Proving Programs*. (Sémantique et Implantation d'une Extension de ML pour la Preuve de Programmes). PhD thesis, Grenoble Alpes University, France, 2017.

[Miq11a] Alexandre Miquel. Existential witness extraction in classical realizability and via a negative translation. *Logical Methods in Computer Science*, 7(2):188-202, 2011.

[Miq11b] Alexandre Miquel. Forcing as a program transformation. In *Proceedings of the 2011 IEEE 26th Annual Symposium on Logic in Computer Science*, LICS '11, page 197-206, USA, 2011. IEEE Computer Society.

[Miq17] Étienne Miquey. *Classical realizability and side-effects*. Ph.D. thesis, Université Paris Diderot; Universidad de la República, Uruguay, November 2017.

[Miq18] Étienne Miquey. A sequent calculus with dependent types for classical arithmetic. In *LICS 2018*, pages 720-729. ACM, 2018.

[Miq20] Étienne Miquey. Revisiting the Duality of Computation: An Algebraic Analysis of Classical Realizability Models. In Maribel Fernández and Anca Muscholl, editors, *28th EACSL Annual Conference on Computer Science Logic (CSL 2020)*, volume 152 of *Leibniz International Proceedings in Informatics (LIPIcs)*, pages 30:1-30:18, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik.

[MM09] Guillaume Munch-Maccagnoni. Focalisation and Classical Realisability. In Erich Grädel and Reinhard Kahle, editors, *Computer Science Logic '09*, volume 5771 of *Lecture Notes in Computer Science*, pages 409-423. Springer, Heidelberg, 2009.

[MM13] Guillaume Munch-Maccagnoni. *Syntax and Models of a non-Associative Composition of Programs and Proofs*. PhD thesis, Univ. Paris Diderot, 2013.

[Mur90] Chetan Murthy. *Extracting constructive content from classical proofs*. Ph.D. thesis, Cornell University, 1990.

[OS08] P. Oliva and T. Streicher. On Krivine's realizability interpretation of classical second-order arithmetic. *Fundam. Inform.*, 84(2):207-220, 2008.

[Par97] M. Parigot. Proofs of strong normalisation for second order classical natural deduction. *J. Symb. Log.*, 62(4):1461-1479, 1997.

[Pit02] Andrew M. Pitts. Tripos theory in retrospect. *Mathematical Structures in Computer Science*, 12(3):265-279, 2002.

[Plo75] Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. *Theor. Comput. Sci.*, 1(2):125-159, 1975.

[Rie14] Lionel Rieg. *On Forcing and Classical Realizability*. Theses, Ecole normale supérieure deyon - ENS LYON, June 2014.

[SF93] Amr Sabry and Matthias Felleisen. Reasoning about programs in continuation-passing style. *Lisp and Symbolic Computation*, 6(3-4):289-360, 1993.

[SS75] Gerald J. Sussman and Guy L. Steele, Jr. An interpreter for extended lambda calculus. Technical report, Massachusetts Institute of Technology, Cambridge, MA, USA, 1975.

[vO08] Jaap van Oosten. *Realizability: an introduction to its categorical side*, volume 152 of *Studies in Logic and the Foundations of Mathematics*. Elsevier B. V., Amsterdam, 2008.
# Building CFA for λ-calculus from Skeletal Semantics

Thomas Jensen, Vincent Rébiscoul, and Alan Schmitt

INRIA Rennes

## Abstract

This paper describes a method to define a correct abstract interpretation from a formal description of the semantics of a programming language. Our approach is based on Skeletal Semantics. We extend it with a notion of program points, in order to differentiate two fragments of the program that are syntactically equivalent but appear at different locations. We introduce a methodology for deriving an abstract interpretation from a Skeletal Semantics that is correct by construction: given a program, abstract states are computed for each program points. We apply our method by defining a Control Flow Analysis for λ-calculus from its Skeletal Semantics.

## 1 Introduction

As the complexity of software increases, building static analyses becomes more and more important. Analyzers have improved for years and many companies use them to save time by detecting bugs [2], or prove some properties on their code [4]. In both cases, the soundness of the analysis is paramount. Methods to develop analyses from a description of a language are useful because they are systematic, even if done by hand. One of the most famous example is Abstract Interpretation [3], which explains how to define an abstract semantics from an operational semantics and how to prove that the abstract semantics is sound using a Galois connection. Other works used abstract interpretation, for example to build an abstract semantics from a big-step semantics [10].

In order to mechanize the design of sound analyses, one should start from a mechanized semantics. Several tools provide such semantics, such as K [7], a framework to mechanize semantics using rewriting rules. This makes the formal definition of a semantics easier, and allows to mechanically derive objects from the semantics: for example in K, one can automatically derive an interpreter from the mechanization of a language. However, K is not an extensible framework and it is unclear how to derive an analysis from a mechanization in K.

In this paper we describe the first steps towards the generation of analyses from a Skeletal Semantics. Skeletal Semantics [1] is a recent proposal for machine-representable semantics of programming languages, using a minimalist functional language, Skel. From the Skeletal Semantics of a language, a semantics can be derived by meta-interpretation of Skel, as a big-step semantics [6]. Abstract Interpretation is a powerful framework to build analyses, thus our work focuses on building an abstract interpretation from a Skeletal Semantics. Because both big-step semantics and abstract interpretations stem from the same syntactic object, the proof of soundness of the abstract interpretation is in large part independent from the language considered. Proving the correctness of the abstract interpretation and the big-step semantics given a particular Skeletal Semantics is therefore dependent on small lemmas only.

Our goal is to provide a methodology to easily define several semantics for a language that can be related to one another. Skeletal Semantics [1] is a recent proposal for machine-representable semantics of programming languages. The Skeletal Semantics of a language is a partial description of the language. Several meanings, called interpretations, can be given to this
description like a big-step semantics [6]. However, because the description is partial, some parts
are left unspecified, and to fully define a semantics, one needs to provide specifications to the
unspecified parts. There are two benefits to this approach. First, the different interpretations
are language independent: an interpretation can be used with any Skeletal Semantics. Second,
two interpretations can be related to one another: for example, in this paper we present an
abstract interpretation that is a correct approximation of the big-step interpretation.

One benefit to this approach is that the interpretations of Skel can be used for any language with a Skeletal Semantics, the definition of a semantics is done by only specifying the language dependent unspecified parts. Because it is often easy to define relations between interpretations, the different semantics of one language can also be related to by proving small lemmas on the specifications that depend on the interpretations. For example, we present a method in this paper to define an abstract interpretation from a Skeletal Semantics that is a sound approximation of the big-step semantics, provided that some lemmas about the

**Contributions** We propose a new interpretation of Skel that includes program points in a systematic way. We define an abstract interpretation for Skel which is correct: the set of all the executions of the big-step semantics is safely over-approximated. We provide a modular methodology to prove correctness at the skeletal meta-level. We give an example of how to define a CFA analysis for λ-calculus using the abstract interpretation of Skel. This work has been implemented in a small OCaml program which takes as inputs a Skeletal Semantics and the definitions of unspecified types and terms, and returns an abstract interpreter.

In Section 2, we introduce the syntax of Skeletal Semantics. In Section 3, we present a big-step semantics (or concrete interpretation) of Skel. In Section 4, we show how to modify the big-step semantics to use program points of a given program. In Section 5, we present an abstract interpretation of Skel, used to define abstract interpretation for any language with a Skeletal Semantics, with a theorem of soundness between the Skel abstract interpretation and big-step semantics. Finally, in Section 6, we use the abstract interpretation to define a CFA analysis for the λ-calculus

## 2 Skeletal Semantics and their Syntax

Skeletal Semantics is a recent approach to mechanize semantics for programming languages [1]. It uses a minimalist, functional, and strongly typed language called Skel [6]. The Necro library [5] is a tool to manipulate Skeletal Semantics. Given Skel code, it can generate OCaml code, Coq code, step by step debuggers, and more.

The mechanization of a semantics of a language using Skeletal Semantics is done by meta-interpretation of the Skel language, therefore *interpretations* must be provided. In this paper, we will present two interpretations: a big-step semantics and an abstract interpretation.

A Skeletal Semantics is a syntactic object, written in Skel, describing a language. We present the Skeletal Semantics of the call-by-value λ-calculus with environments. We start by defining useful types for our language:

1. type ident

2. type env

3.

4. type clos =

5. | Clos (ident, lterm, env)

6.
7 type lterm =
8 | Lam (ident, lterm)
9 | Var ident
10 | App (lterm, lterm)

It starts with two definitions of *unspecified types*, and two definitions of *specified types*. The types refer, in that order, to identifiers, environments, closures, and λ-terms. Having unspecified types is a unique trait of Skel. Keeping some types unspecified is useful because their instantiation can depend on the interpretation of Skel. Specified types are algebraic data types (ADT). The *clos* type contains only one constructor which parameter is a triplet with an identifier (representing a variable), a λ-term, and an environment, which is a usual definition for a closure. The type *lterm* is the definition of λ-terms: it can be a λ-abstraction, a variable or an application.

Moreover, a Skeletal Semantics contains terms:

12 val extEnv : (env, ident, clos) → env
13 val getEnv : (ident, env) → clos

The term `getEnv(x, e)` is a lookup function: it returns the closure associated to `x` in `e`. The term `extEnv(e, x, v)` returns a new environment equals to `e` but with the new binding where `x` maps to `v`. Terms must be explicitly typed. Moreover, both terms are *unspecified*: like types, terms do not need to be completely defined in the Skeletal Semantics. In fact, as `env` is unspecified, functions to access or extend it must be unspecified.

A Skeletal Semantics also contains specified terms:

15 val eval (s:env) (l:lterm) : clos =
16 branch
17 let Lam (x, t) = l in
18 Clos (x, t, s)
19 or
20 let Var x = l in
21 getEnv (x, s)
22 or
23 let App (t1, t2) = l in
24 let Clos (x, t, s') = eval s t1 in
25 let w = eval s t2 in
26 let s'' = extEnv (s', x, w) in
27 eval s'' t
28 end
29

This specified term is the function detailing how a *lterm* should be computed given an environment. For example, the `eval` function starts with a branching with three branches, and each branch is guarded by a let-binding doing pattern-matching: this particular branching acts as a case analysis. Indeed, a branching is used to cover several cases: here, there is one case per constructor in the *lterm* type. The first branch evaluates a λ-abstraction by returning a closure, the second branch evaluates a variable by using the `getEnv` function. The final branch evaluates an application: first `t1` is evaluated, which gives a closure `Clos(x, t, s')` representing the function with parameter `x` and body `t`, and where environment `s'` gives meaning to free variables in `t`. Then `t2` is evaluated to another closure `w`, and `s'` is extended such that `x` maps
$$
\begin{align*}
\text{TERM } t &::= x \mid C t \mid (t, \dots, t) \mid \lambda p : \tau \rightarrow S \\
\text{SKELETON } S &::= t_0 t_1 \dots t_n \mid \text{let } p = S \text{ in } S \mid \text{branch } S \text{ or } \dots \text{ or } S \text{ end } \mid t \\
\text{PATTERN } p &::= x \mid - \mid C p \mid (p, \dots, p) \\
\text{TYPE } \tau &::= b \mid \tau \rightarrow \tau \mid (\tau, \dots, \tau) \\
\text{TERM DECL } r_t &::= \mathbf{val} \ x : \tau \mid \mathbf{val} \ x : \tau = t \\
\text{TYPE DECL } r_\tau &::= \mathbf{type} \ b \\
&\qquad \mid \mathbf{type} \ b = |C1 \ \tau_1 \dots |Cn \ \tau_n
\end{align*}
$$

<caption>Figure 1: The Syntax of Skeletal Semantics</caption>

to w, giving a new environment s". Finally, the body of the function t is evaluated with the
new environment s". This should not be too surprising for people familiar with the semantics
of λ-calculus with environments.

Formally, the syntax of Skel is given in Figure 1: it is similar to λ-calculus where the syntax ensures that programs are in A-Normal Form [9]. A specified term is either a variable, a constructor applied to a term, a tuple, or a function. Intuitively, a term is a construct that is fully computed. A skeleton is either an application, a let-binding, a branching, or a term. Intuitively, a skeleton is a computation. Branching is the most exotic construct of the language, it will be explained in more depth later on. Skel uses patterns, notably to perform pattern-matching with let-bindings. A term declaration introduces a top-level term. It can either be unspecified, in which case only its name and type are given, or specified, in which case the specification is a term. A type declaration introduces a type that may be unspecified, or it can be the declaration of an algebraic datatype.

A Skeletal Semantics is a set of type definitions and term definitions, that can be specified or unspecified. In the following, for any constructor C of a specified algebraic data type τ, we write C : (τᵢ, τ) to state that C belongs to type τ and expects an argument of type τᵢ.

3 Big-step Semantics of Skel

To give meaning to a Skeletal Semantics, we provide interpretations of Skel. In this section, we give the big-step semantics of Skel.

The predicate na(τ) is true when τ is not an arrow type. The *arity* of a function *f*, *arity(f)*, is *n* if *f* has type τ₁ → ... → τn → τ, where na(τ). Let *S* be an arbitrary Skeletal Semantics. We write Funs(*S*) for the set of pairs (Γ, λp : τ₁ → S₀) such that λp : τ₁ → S₀ appears in Skeletal Semantics *S*. The typing environment Γ gives types to the free variables of λp : τ₁ → S₀. Typing rules are given in the Appendix B and Funs(·) is formally defined in the Appendix C.

3.1 From Types to Concrete Values

We call the interpretation of types the function $V(\tau)$, that given a type $\tau$ returns the set of
values of that type. These sets are defined with the relation $\vdash \cdot \in V(\cdot)$ in Figure 2. These rules
are language independent and are completed with language-dependent rules upon instantiation.
$$
\frac{\begin{array}{l}
\forall 1 \le i \le n \quad \vdash v_i \in V(\tau_i) \\
\vdash (v_1, \dots, v_n) \in V(\tau_1 \times \dots \times \tau_n)
\end{array}}{\text{TUPLE}}
\qquad
\frac{\begin{array}{l}
\vdash v \in V(\tau) \qquad C : (\tau, \tau_a) \\
\vdash C \quad v \in V(\tau_a)
\end{array}}{\text{ADT}}
\\
\frac{\begin{array}{l}
(\Gamma, \lambda p : \tau_1 \to S) \in \text{Funs}(S) \qquad \Gamma \vdash E \qquad \Gamma + p \leftarrow \tau_1 \vdash S : \tau_2 \\
\vdash (p, S, E) \in V(\tau_1 \to \tau_2)
\end{array}}{\text{CLOS}}
\\
\frac{\begin{array}{l}
\mathbf{val} \ f : \tau_1 \to \dots \to \tau_n \to \tau \quad [f] \in S \qquad \text{na}(\tau) \\
\vdash (f, \text{arity}(f)) \in V(\tau_1 \to \dots \to \tau_n \to \tau)
\end{array}}{\text{DEF}}
\\
\frac{\begin{array}{l}
\text{dom} \ \Gamma = \text{dom} \ E \qquad \forall x \in \text{dom} \ E, \Gamma \vdash E(x) : \Gamma(x) \\
\qquad \qquad \qquad \qquad \Gamma \vdash E
\end{array}}{\text{IENV}}
$$

<caption>Figure 2: Rules to Build Values</caption>

The TUPLE and ADT rules build tuples and values of ADTs. The CLOS rule builds a closure, which is a triplet (*p*, *S*, *E*). *p* is the pattern that contains the parameters of the function, *S* is the body of the function and *E* an environment for the free variables in *S*. Note that this environment must be compatible with the typing of the free variables of the function (Rule IENV). The DEF rule builds named closures for application of unspecified and specified terms with arrow type. The closure contains only the name and the arity of the function.

An instantiation of a Skeletal Semantics must define the values belonging to unspecified types. We now show how this is done by example. In the case of λ-calculus, the unspecified types are ident and env, thus we provide rules to build these values.

$$
\frac{\begin{array}{l}
id \in \mathcal{V} = \{x, y, z\dots\} \\
\vdash id \in V(\mathbf{ident})
\end{array}}{\mathbf{IDENT}}
\qquad
\frac{\begin{array}{l}
\vdash [\quad] \in V(\mathbf{env}) \\
\mathbf{ENV-EMPTY}
\end{array}}{\mathbf{ENV-CONS}}
\\
\frac{\begin{array}{l}
\vdash id \in V(\mathbf{ident}) \\
\vdash c \in V(\mathbf{clos}) \\
\vdash e \in V(\mathbf{env})
\end{array}}{\mathbf{ENV-CONS}}
\qquad
\frac{\begin{array}{l}
id, c \in V(\mathbf{env}) \\
\vdash (id, c) :: e \in V(\mathbf{env})
\end{array}}{\mathbf{ENV-CONS}}
$$

Identifiers are variables from a countable set of variables $\mathcal{V}$, and an environment is an association list: it can be empty or built from a new binding and another environment.

## 3.2 Interpretation of Unspecified Terms

If $X$ is a set, $\mathcal{P}_f(X)$ is the set of finite parts of $X$.

Now that values are defined, there remains to give definitions to unspecified terms. Take an unspecified term **val** *t* : τ₁ → ... → τn → τ such that na(τ), then an instantiation of *t*, written [[*t*]], is a function such that: [[*t*]] ∈ (V(τ₁) × ... × V(τn)) → P<sub>f</sub>(V(τ)). In particular, if **val** *t* : τ and na(τ), then [[*t*]] ⊆ V(τ). Allowing the specification of a term to be a function returning a set is useful to model non-determinism.
For our λ-calculus, the specifications of unspecified terms are:

$$
\begin{align*}
& \llbracket \text{getEnv} \rrbracket(x, (x, c) :: e) = \{c\} \\
& \llbracket \text{getEnv} \rrbracket(x, (y, c) :: e) = \llbracket \text{getEnv} \rrbracket(x, e) \qquad x \neq y \\
& \llbracket \text{getEnv} \rrbracket(x, [] ) = \{ \} \\
& \llbracket \text{extEnv} \rrbracket(e, x, c) = (x, c) :: e
\end{align*}
$$

The interpretation $[[getEnv]](x,e)$ is defined with three equations: the first equation returns the closure when the correct binding is at the head of the environment, the second equation is a recursive call when the first binding is not the correct one, and in last equation, $getEnv$ returns the empty set because the environment is empty. $[[extEnv]](e, x, c)$ returns a similar environment to $e$, but with a new binding where $x$ is associated to $c$.

3.3 Big-step Semantics

We now define the big-step semantics of Skel. $E, S \Downarrow v$ is a relation from a skeletal environment $E$, mapping skeletal variables to values, and a skeleton $S$ to a value $v$. The relation is defined in Figure 3a.

There are four rules to evaluate variables, depending on how the variable was defined and its type. If the variable was defined in a 'let' expression, the environment $E$ maps the variable to its value (Rule VAR). Otherwise, assuming the Skeletal Semantics is well typed, the variable must be the name of a specified or unspecified term. If this term has an arrow type, we simply return a named closure, whether the variable is specified or not. A named closure is a pair of the name and arity of the function (Rule TERMCLOS). If the variable is declared in the Skeletal Semantics, then it is bound to a closed term $t$, which is evaluated in the empty environment because it only depends on term declarations of the Skeletal Semantics (Rule TERMSPEC). If the variable is unspecified, a value of the provided instantiation is returned (Rule TERMUNSPEC). Rules CONST and TUPLE are usual. Rule CLOS returns a skeletal closure. One may observe a similarity between this meta-rule and the corresponding object rule in the λ-calculus; this is because Skel is a meta-language that is an extension of the λ-calculus, but the meta-language and the object language should not be confused.

We now turn to the evaluation of skeletons. Rule LETIN is usual. Rule BRANCH evaluates a branching by non-deterministically returning the result of the evaluation of a branch. To evaluate an application, we define another relation, defined in Figure 3b with four rules. Rule BASE returns the result when all arguments have been processed. Rule CLOS is the application of a closure. Rules SPEC and UNSPEC are the application of a named closure to a list of arguments. The first evaluates the corresponding definition while the second one uses the user-provided instantiation. Non-specified functions may be non-deterministic since their instantiation may return a set. Note that we only consider full application of named functions: all arguments must be provided. Extending this semantics to partial application is easy, although verbose, but it is not necessary to describe our contributions. Finally, the pattern matching rules for environment extension are given in Figure 4.
$$ \frac{E(x) = v}{E, x \Downarrow v} \text{ VAR} \qquad \frac{\text{val } f : \tau_1 \to \dots \to \tau_n \to \tau[= t] \quad \text{na}(\tau) \quad n \ge 1}{E, f \Downarrow (f, n)} \text{ TERMCLOS} $$

$$ \frac{\text{val } x : \tau = t \in S \quad \text{na}(\tau) \quad \emptyset, t \Downarrow v}{E, x \Downarrow v} \text{ TERMSPEC} $$

$$ \frac{\text{val } x : \tau \in S \quad \text{na}(\tau) \quad v \in [x]}{E, x \Downarrow v} \text{ TERMUNSPEC} \qquad \frac{E, t \Downarrow v}{E, (Ct) \Downarrow C v} \text{ CONST} $$

$$ \frac{E, t_1 \Downarrow v_1 \quad \dots \quad E, t_n \Downarrow v_n}{E, (t_1, \dots, t_n) \Downarrow (v_1, \dots, v_n)} \text{ TUPLE} \qquad \frac{E, (\lambda p : \tau \to S) \Downarrow (p, S, E)}{E} \text{ CLOS} $$

$$ \frac{E, S_1 \Downarrow v \quad \vdash E + p \leftarrow v \rightsquigarrow E' \quad E', S_2 \Downarrow w}{E, \text{let } p = S_1 \text{ in } S_2 \Downarrow w} \text{ LETIN} \qquad \frac{E, S_i \Downarrow v}{E, (S_1, \dots, S_n) \Downarrow v} \text{ BRANCH} $$

$$ \frac{\forall i \in [0..n]. E, t_i \Downarrow v_i \quad v_0 v_1 \dots v_n \Downarrow_{app} w}{E, (t_0 t_1 \dots t_n) \Downarrow w} \text{ APP} $$

(a) Rules for the Big-step Semantics of Skeletons and Terms

$$ \frac{\vdash E + p \leftarrow v_1 \rightsquigarrow E' \quad E', S \Downarrow v \quad v v_2 \dots v_n \Downarrow_{app} w}{v \Downarrow_{app} v} \text{ CLOS} $$

$$ \frac{\text{val } f : \tau_1 \to \dots \to \tau_n \to \tau = t \in S \quad \text{na}(\tau) \quad \emptyset, t \Downarrow v \quad v v_1 \dots v_n \Downarrow_{app} w}{(f, n) v_1 \dots v_n \Downarrow_{app} w} \text{ SPEC} $$

$$ \frac{\text{val } f : \tau_1 \to \dots \to \tau_n \to \tau \in S \quad \text{na}(\tau) \quad w \in [f](v_1, \dots, v_n)}{(f, n) v_1 \dots v_n \Downarrow_{app} w} \text{ UNSPEC} $$

(b) Rules for Application for the Big-step Semantics

<caption>Figure 3: Interpretation rules of the Big-step Semantics</caption>

$$ \begin{array}{l} \frac{\vdash E + _{-} \leftarrow v \rightsquigarrow E}{\text{ASN-WILDCARD}} \qquad \frac{\vdash E + x \leftarrow v \rightsquigarrow (x, v) :: E}{\text{ASN-VAR}} \\ \qquad \frac{\vdash E + p \leftarrow v \rightsquigarrow E'}{\vdash E + C p \leftarrow C v \rightsquigarrow E'} \text{ ASN-CONSTR} \\ \qquad \frac{\vdash E + p_1 \leftarrow v_1 \rightsquigarrow E_2 \quad \dots \quad \vdash E_n + p_n \leftarrow v_n \rightsquigarrow E'}{\vdash E + (p_1, \dots, p_n) \leftarrow (v_1, \dots, v_n) \rightsquigarrow E'} \text{ ASN-TUPLE} \end{array} $$

<caption>Figure 4: Rule of Extension of Environment through Pattern Matching</caption>
# 4 Big-step Semantics with Program Points

## 4.1 Program Points and New Values

We present our first contribution, which is a method to use program points in the big-step semantics of a Skeletal Semantics. This methodology is reused later for the abstract interpretation of Skel. Let $S$ be a Skeletal Semantics. It usually contains one or more specified algebraic data types that define the syntax of the language, i.e., programs. We call these types program types. In the case of $\lambda$-calculus, $lterm$ is the only program type. Let $\tau$ a program type in $S$ and $prg \in V(\tau)$ a program, we can refer to sub-terms of $prg$ using program points. A program point is a path from the root of $prg$ to one of its sub-term. Given a program point pp, $prg@pp$ is the sub-term of $prg$ obtained by following path pp. A program point pp is an element of $ppt = N^*$, the set program points. $\epsilon$ is the empty path and $i \cdot pp$ is a path with first element $i$, and pp is the rest of the path. The @ operator is formally defined as:

$$v@\epsilon = v \\ C(v_0, \dots, v_{n-1})@i \cdot pp = v_i@pp \quad \text{when } 0 \le i \le n-1$$

To give an example, for $\lambda$-calculus, let $prg = Lam(x, Var x)$. Then, $prg@0 = x$ and $prg@1 = Var x$.

Our approach is to replace values of program types with program points. Each program point refers to a sub-term of the main program: $prg$, which is now a parameter of the interpretation. Let $\mathcal{T}$ be the set of program types from $S$ and $prg$ a program. Therefore, all values of $\tau \in \mathcal{T}$ are program points and represent sub-terms of $prg$. In particular, because $prg$ is a program, its type should be in $\mathcal{T}$.

For each type $\tau$, a set of values is built using previously defined rules 2 except for program types that are defined by the equation:

$$\tau \in \mathcal{T} \implies V_{prg}^{ppt}(\tau) = \{ pp \in ppt \mid prg@pp \in V(\tau) \}$$

The set $V_{prg}^{ppt}(\tau)$ is the set of program points that refer to sub-terms of $prg$ of type $\tau$. This is an important restriction because if $\tau \in \mathcal{T}$, then a value $v \in V_{prg}^{ppt}(\tau)$ is a program point and therefore necessarily represent a fragment of $prg$ and not an arbitrary program.

$\mathcal{T}$ is a set because some languages may have many types for different parts of programs: an imperative language would need at least one type for statements and one type for expressions. Let us give an example with the $\lambda$-calculus. We take our program to be $prg = App(Lam(x, Var x), Var y)$ and $\mathcal{T} = \{lterm\}$. The interpretation of the $\lambda$-terms is defined in the next equation. The program points are underlined to differentiate them from natural numbers.

$$V_{prg}^{ppt}(lterm) = \{ \epsilon, \emptyset, \underline{1}, \underline{01} \}$$

For example, we have $prg@\underline{1} = Var y$

The interpretation of unspecified types does not change and other types are built using previous rules in Figure 2. However, we assume new specifications of unspecified terms. Indeed, some unspecified terms may depend on types in $\mathcal{T}$, therefore, for all unspecified terms $x$ in $S$, we suppose that new specifications are provided: $[x]^{ppt}$.

## 4.2 Pattern Matching with Program Points

The interpretation of skeletons with program points does not fundamentally change: only the pattern matching is modified and uses an unfolding mechanism. Unfolding matches a program
$$
\begin{align*}
NC(\tau_1 \to \tau_2) &= \left\{ (f, n) \middle| \begin{array}{l} \mathbf{val} \ f : \tau_1 \to \tau_2[=t] \in \mathcal{S} \\ \text{arity}(f) = n \end{array} \right\} \\
C(\tau_1 \to \tau_2) &= \left\{ (p, S, E^\sharp) \middle| \begin{array}{l} \exists(\Gamma, \lambda p : \tau_1 \to S) \in \text{Funs}(\mathcal{S}), \\ \Gamma \vdash E^\sharp \wedge \Gamma + p \leftarrow \tau_1 \vdash S : \tau_2 \end{array} \right\}
\end{align*}
$$

<caption>Figure 5: Sets of Abstract Named Closures and Closures</caption>

point with a constructor pattern and is described by the following rule.

$$
\frac{\mathbf{prg}@\text{pp} = C(v'_0, \dots, v'_{n-1}) \qquad C : (\tau_0 \times \dots \times \tau_{n-1}, \tau)}{v_j = \mathbf{if} \ \tau_j \in \mathcal{T} \ \mathbf{then} \ \text{pp} \cdot j \ \mathbf{else} \ \mathbf{v}'_j \qquad \mathcal{T}, \mathbf{prg} \vdash E + p \leftarrow (v_0, \dots, v_{n-1}) \leadsto E' \qquad \mathbf{asn}\text{-}\mathbf{unfold}}
$$

When a program point pp is matched with a constructor pattern C p, **prg**@pp is expected to
have the form C(v'<sub>0</sub>,...,v'<sub>n-1</sub>). Then, for 0 ≤ j ≤ n − 1, v<sub>j</sub> is **pp**·*j* if v'<sub>j</sub> has a program type
τ<sub>j</sub> ∈ T, or v'<sub>j</sub> otherwise. Then the pattern *p* is matched with (v<sub>1</sub>,...,v<sub>n</sub>). The unfolding rule
exhibits the constructor and its parameters at program point **pp**, then continues the pattern
matching recursively.

We give an example for λ-calculus, let **prg** = App(Lam(x, Var x), Var y). To compute
T, **prg** ⊢ E + Lam(p) ← 0 ⇝ E' where p is a pattern, by applying the **asn-unfold** rule, it
comes that: T, **prg** ⊢ E + p ← (x, 01) ⇝ E' Indeed, **prg**@0 = Lam(x, Var x) and Var x has
program point 01, therefore p is matched with (x, 01)

The big-step semantics of skeletons and the big-step semantics of skeletons with program
points are closely related. We formalize this connection through a theorem presented in Ap-
pendix D.

5 Abstract Interpretation

We define an abstract interpretation of Skel that is sound with respect to the big-step semantics of Section 4. The abstract interpretation is used in the next section to define a Control Flow Analysis for λ-calculus.

We define the abstract values, comparison functions and upper bounds in Section 5.1. We define the state of the abstract interpretation in Section 5.2. We present the interpretation rules of skeletons for an abstract interpretation in Section 5.3, We present how the abstract values are linked to the concrete values by defining concretization functions in Section 5.4. Finally, we formulate a theorem of soundness in Section 5.5. In the following sections, S denotes an arbitrary Skeletal Semantics.

**5.1 Definition of Abstract Values**

The abstract values are defined similarly to the concrete ones. In Figure 5 we define the set
of abstract named closures and the set of abstract closures. Abstract named closures are pairs
of a name of a function defined in the skeletal semantics and its arity. Abstract closures are a
triplet with a pattern, a skeleton and an abstract environment. The abstract environment is
defined later in the this section.
$$
\begin{array}{l@{\qquad}l@{\qquad}l}
\overline{\vdash^\sharp \perp_\tau \in V^\sharp(\tau)} & \text{BOTTOM} & \overline{\vdash^\sharp \top_\tau \in V^\sharp(\tau)} & \text{TOP} \\[1.5ex]
\frac{\forall (v_1^\sharp, \dots, v_n^\sharp) \in t^\sharp \quad \forall 1 \le i \le n, \quad \vdash^\sharp v_i^\sharp \in V^\sharp(\tau_i) \wedge v_i^\sharp \ne \perp_{\tau_i}}{\vdash^\sharp t^\sharp \in V^\sharp(\tau_1 \times \dots \times \tau_n)} & & \text{TUPLE} \\[1.5ex]
\frac{\vdash^\sharp v^\sharp \in V^\sharp(\tau) \quad C : (\tau, \tau_a) \quad v^\sharp \ne \perp_\tau}{\vdash^\sharp C \ v^\sharp \in V^\sharp(\tau_a)} & & \text{ADT} \\[1.5ex]
\frac{nc \subseteq \mathrm{NC}(\tau_1 \to \tau_2) \quad c \subseteq \mathrm{C}(\tau_1 \to \tau_2)}{\vdash^\sharp c \cup nc \in V^\sharp(\tau_1 \to \tau_2)} & & \text{FUNS} \\[1.5ex]
\frac{\mathrm{dom} \ \Gamma = \mathrm{dom} \ E^\sharp \quad \forall x \in \mathrm{dom} \ E^\sharp, \Gamma \vdash E^\sharp(x) : \Gamma(x)}{\Gamma \vdash E^\sharp} & & \text{IENV}
\end{array}
$$

<caption>Figure 6: Rules to Build Abstract Values</caption>

The rules to define abstract values are presented on Figure 6. The BOTTOM and TOP rules define a least and a greatest element for each type. The TUPLE rule define the abstract tuples, that are a set of tuples of abstract values. Because one of our target is CFA analysis for λ-calculus, having a set is necessary not to loose too much precision during the analysis. On line 24 of the Skeletal Semantics of the λ-calculus A, eval s t1 returns a closure, Clos(x, t, s) which is essentially a triplet. The relation between identifier, term and environment must be preserved. Values of algebraic types, defined by the rule ADT, are constructors applied to abstract values. Abstract functions, defined by the rule FUNS, is the union of a subset of abstract named closures, and a subset of abstract closures. For instance for the λ-calculus, the set {{(eval, 2), (s, λ1:lterm.Seval, ∅)} belongs to V#(env → lterm → clos), where Seval is the body of the eval specified term. Finally, the rule IENV defines abstract environments, that are partial functions mapping skeletal variables to abstract values.

To compare abstract values, we define partial orders. For every unspecified type $\tau_u$, we assume comparison function $\sqsubseteq_{\tau_u}^\sharp$ which is an order and with the constraint that $\top_{\tau_u}$ and $\bot_{\tau_u}$ are the greatest and smallest elements of $V_{\mathrm{prg}}^\sharp(\tau_u)$ respectively. For every other types, the comparison function is the smallest order that satisfies the following equations:

$$
\begin{align*}
C v^\sharp \sqsubseteq_{\tau_a}^\sharp C w^\sharp &\iff v^\sharp \sqsubseteq_\tau^\sharp w^\sharp \text{ with } C : (\tau, \tau_a) \\
t_1^\sharp \sqsubseteq_{\tau_1 \times \dots \times \tau_n}^\sharp t_2^\sharp &\iff \forall (v_1^\sharp, \dots, v_n^\sharp) \in t_1^\sharp, \exists (w_1^\sharp, \dots, w_n^\sharp) \in t_2^\sharp, \forall i, 1 \le i \le n, v_i^\sharp \sqsubseteq_{\tau_i}^\sharp w_i^\sharp \\
F_1 \sqsubseteq_{\tau_1 \to \tau_2}^\sharp F_2 &\iff \begin{cases} (f, n) \in F_1 \implies (f, n) \in F_2 \\ (p, S, E_1^\sharp) \in F_1 \implies \exists (p, S, E_2^\sharp) \in F_2, E_1^\sharp \sqsubseteq_{\mathrm{env}}^\sharp E_2^\sharp \end{cases} \\
E_1^\sharp \sqsubseteq_{\mathrm{env}}^\sharp E_2^\sharp &\iff \Gamma \vdash E_1^\sharp \wedge \Gamma \vdash E_2^\sharp \wedge \forall x \in \mathrm{dom} \ E_1^\sharp, E_1^\sharp(x) \sqsubseteq_{\Gamma(x)}^\sharp E_2^\sharp(x) \\
v^\sharp \sqsubseteq_\tau^\sharp \top_\tau \\
\bot_\tau \sqsubseteq_\tau^\sharp v^\sharp
\end{align*}
$$

To compare algebraic values, their parameters are compared. Tuples are compared by checking
that all tuples of abstract values of the left tuple are smaller than a tuple of abstract values in the right tuple. To compare two functions, all named closures of the left function must be in the right function. Moreover, for all closures in the left function, there must be a closure in the right function with the same pattern and skeleton, but with a bigger abstract environment. Abstract environments are compared using point-wise lifting. For each type, top and bottom are respectively the smallest and greatest elements of the type.

For each type, an upper bound (or join) is defined. For every non-specified type $\tau_u$, we assume an upper bound $\sqcup^{\#}_{\tau_u}$. We define an upper bound $\sqcup^{\#}_{\tau}$ for every other types.

$$ (C v^{\#}) \sqcup^{\#}_{\tau_a} (C w^{\#}) = C (v^{\#} \sqcup^{\#}_{\tau} w^{\#}) \text{ with } C : (\tau, \tau_a) $$

$$ (C v^{\#}) \sqcup^{\#}_{\tau_a} (D w^{\#}) = \top_{\tau_a} \text{ with } C : (\tau, \tau_a) \wedge D : (\tau', \tau_a) $$

$$ t_1^{\#} \sqcup^{\#}_{\tau_1 \times \dots \times \tau_n} t_2^{\#} = t_1^{\#} \cup t_2^{\#} $$

$$ F_1 \sqcup^{\#}_{\tau_1 \to \tau_2} F_2 = F_1 \cup F_2 $$

$$ E_1^{\#} \sqcup^{\#}_{env} E_2^{\#} = \{ x \in \text{dom } E_1^{\#} \mapsto E_1^{\#}(x) \sqcup^{\#} E_2^{\#}(x) \} $$

$$ v^{\#} \sqcup^{\#}_{\tau} \top_{\tau} = \top_{\tau} \sqcup^{\#}_{\tau} v^{\#} = \top_{\tau} $$

$$ v^{\#} \sqcup^{\#}_{\tau} \bot_{\tau} = \bot_{\tau} \sqcup^{\#}_{\tau} v^{\#} = v^{\#} $$

Joining two algebraic values with the same constructor is joining their parameters, and joining algebraic values with different constructors yield top. Joining abstract tuples our abstract functions is set union. Joining abstract environments is done by point-wise lifting. For each type, top is an absorbing element, and bottom is the neutral element.

## 5.2 State of the Abstract Interpretation

The state of the abstract interpretation $\mathcal{A}$ is a machine representable state that contains information collected throughout the abstract interpretation. It is dependent on the analysis and the language, and therefore is non-generic and must be specified. To give an example, when defining a CFA in the next section, the abstract state will contain a mapping from program points to sets of $\lambda$-abstraction, that can be viewed as the potential results when evaluating a sub-term at some program point of the analyzed program. We require an order on the abstract states. Intuitively, we should only add information in the states throughout the analysis, and therefore at each step of the analysis, the states should only increase.

A state contains several components: $\mathcal{A} \cdot c$ is the component $c$ of the abstract state $\mathcal{A}$. The notation $\{ \mathcal{A} \text{ with } c = v \}$ denotes a new state equals to $\mathcal{A}$, excepts for the $c$ component which is equal to $v$.

## 5.3 The Abstract Interpretation of Skel

The abstract interpretation maintains a callstack of specified function. This is used for loop detection and prevent infinite computations: the idea is to inspect the callstack at each call to a specified function to detect identical nested calls. Callstacks are ordered list of frames,
formally defined as:

$\epsilon \in \mathbf{callstack}$

A an abstract state

$$ \mathbf{val}f : \tau_1 \to \dots \to \tau_n \to \tau = t \in \mathcal{S} \quad \text{na}(\tau) \quad v_i \in V_{\text{prg}}^{\sharp}(\tau_i) \quad \pi \in \mathbf{callstack} $$

$$ (f, \mathcal{A}, [v_1, \dots, v_n]) :: \pi \in \mathbf{callstack} $$

The abstract interpretation of skeletons is given on Figure 7a. The abstract interpretation of skeletons is similar to the big-step interpretation: the evaluation of terms is almost unchanged except that evaluating a closure or a tuple returns a singleton. When evaluating a skeleton (branch, let-binding, or application), a state of the abstract interpretation is carried through the computations. In the BRANCH rule, all branches are evaluated and joined instead of only one branch being evaluated. The pattern matching now returns sets of environments rather than one, and this will be detailed later, but in consequence the LETIN rule may evaluate $S_2$ in several abstract environments. The APP rule evaluates all terms and pass a list of values to the application relation. There are separate rules to handle applications on Figure 7b. Because the abstraction of a function is a set of closures and named closures, the APP-SET rule evaluates each one individually. The BASE rule returns the remaining value when all arguments have been processed. Because the extension of environments returns a set of abstract environment, the CLOS rule is modified accordingly and the body of the function $S$ is evaluated in all abstract environments. The SPEC rule evaluates the call to a specified function by doing three things:

* it uses an update<sup>in</sup><sub>f</sub>(·) function which is language dependent and must be specified. It can modify the arguments and the state of the abstract interpretation.

* the call is performed (a frame is added to the callstack at that point).

* an update<sup>out</sup><sub>f</sub>(·) function can modify the state of the interpretation and the returned value.

These update functions are used to maintain invariants and update the state of the abstract interpretation. An example of their use will be presented in the next section. The update functions must respect the following constraints to ensure soundness:

**Remark 1.**

$$ \text{update}_{f}^{\text{in}}(\mathcal{A}, [v_{1}^{\sharp}, \dots, v_{k}^{\sharp}]) = [v'_{1}^{\sharp}, \dots, v'_{k}^{\sharp}], \mathcal{A}' \implies (v_{1}^{\sharp}, \dots, v_{k}^{\sharp}) \sqsubseteq^{\sharp} (v'_{1}^{\sharp}, \dots, v'_{k}^{\sharp}) \wedge \mathcal{A} \sqsubseteq^{\sharp} \mathcal{A}' $$

$$ \text{update}_{f}^{\text{out}}(\mathcal{A}, [v_{1}^{\sharp}, \dots, v_{k}^{\sharp}], v^{\sharp}) = v^{\prime \sharp}, \mathcal{A}' \implies v^{\sharp} \sqsubseteq^{\sharp} v^{\prime \sharp} \wedge \mathcal{A} \sqsubseteq^{\sharp} \mathcal{A}' $$

The extension of environments, or pattern matching, presented on Figure 8 is modified such that it returns a set of abstract environments. This is necessary because our abstraction of tuples is a finite set of tuples of abstract values. In order not to lose too much precision, we return one abstract environment per tuple of abstract values in our abstract tuple. The rules are similar to the big-step semantics, excepts that there are two rules for tuples: the rule ASN-TUPLE-SINGLETON extends the environment with a tuple of abstract values, the ASN-TUPLE forwards all tuples of abstract values in $t^{\sharp}$ to the ASN-TUPLE-SINGLETON rule.
$$ \frac{E^{\sharp}(x) = v^{\sharp}}{E^{\sharp}, x \Downarrow v^{\sharp}} \text{ VAR} $$

$$ \frac{\text{val } f : \tau_1 \to \dots \to \tau_n \to \tau[=t] \in \mathcal{S} \quad \text{na}(\tau)}{E^{\sharp}, f \Downarrow \{(f, \text{arity}(f))\}} \text{ TERMCLOS} $$

$$ \frac{\text{val } x : \tau = t \in \mathcal{S} \quad \emptyset, t \Downarrow v^{\sharp} \quad \text{na}(\tau)}{E^{\sharp}, x \Downarrow v^{\sharp}} \text{ TERMSPEC} $$

$$ \frac{\text{val } x : \tau \in \mathcal{S} \quad \text{na}(\tau)}{E^{\sharp}, x \Downarrow [[x]]^{\sharp}} \text{ TERMUNSPEC} $$

$$ \frac{E^{\sharp}, t \Downarrow v^{\sharp}}{E^{\sharp}, C t \Downarrow C v^{\sharp}} \text{ CONST} $$

$$ \frac{E^{\sharp}, t_1 \Downarrow v_1^{\sharp} \quad \dots \quad E^{\sharp}, t_n \Downarrow v_n^{\sharp}}{E^{\sharp}, (t_1, \dots, t_n) \Downarrow \{(v_1^{\sharp}, \dots, v_n^{\sharp})\}} \text{ TUPLE} $$

$$ \frac{\pi, A, E^{\sharp}, \lambda p : \tau \cdot S \Downarrow^{\sharp} \{(p, S, E^{\sharp})\}}{\text{CLOS}} $$

$$ \frac{\pi, A, E^{\sharp}, S_i \Downarrow^{\sharp} v_i^{\sharp}, A_i}{\pi, A, E^{\sharp}, (S_1 \dots S_n) \Downarrow^{\sharp} \sqcup^{\sharp} v_i^{\sharp}, \sqcup^{\sharp} A_i} \text{ BRANCH} $$

$$ \frac{\pi, A, E^{\sharp}, S_1 \Downarrow^{\sharp} v^{\sharp}, A'}{\mathcal{T}, \text{ prg} \vdash E^{\sharp} + p \leftarrow v^{\sharp} \rightsquigarrow \{E_1^{\sharp}, \dots, E_n^{\sharp}\}} \quad \pi, A', E_i^{\sharp}, S_2 \Downarrow^{\sharp} w_i^{\sharp}, A_i $$

$$ \frac{\pi, A, E^{\sharp}, \text{let } p = S_1 \text{ in } S_2 \Downarrow^{\sharp} \sqcup^{\sharp} w_i^{\sharp}, \sqcup^{\sharp} A_i}{\text{LETIN}} $$

$$ \frac{E^{\sharp}, t_i \Downarrow v_i^{\sharp}}{\pi, A, E^{\sharp}, t_0 t_1 \dots t_n \Downarrow^{\sharp} v^{\sharp}, A'} \text{ APP} $$

(a) Rules for the Abstract Interpretation of Skeletons and Terms

$$ v_0^{\sharp} = \bigcup_{i=1}^{n} \{w_i\} \quad \pi, A, w_i, v_1^{\sharp} \dots v_n^{\sharp} \Downarrow_{app} v_{w_i}^{\sharp}, A_i $$

$$ \frac{\pi, A, v^{\sharp} \Downarrow_{app} v^{\sharp}, A}{\pi, A, v^{\sharp} \Downarrow_{app} v^{\sharp}, A} \text{ BASE} $$

$$ \frac{\mathcal{T}, \text{ prg} \vdash E^{\sharp} + p \leftarrow^{\sharp} v_1^{\sharp} \rightsquigarrow \{E_1^{\sharp}, \dots, E_m^{\sharp}\}}{\forall E_i^{\sharp} \in \{E_1^{\sharp}, \dots, E_m^{\sharp}\}} \quad \pi, A, E_i^{\sharp}, S \Downarrow w_i^{\sharp}, A_i \quad \pi, A_i, w_i^{\sharp} \Downarrow v_2^{\sharp} \dots v_n^{\sharp} \Downarrow_{app} u_i^{\sharp}, A_i' $$

$$ \frac{\text{val } f : \tau_1 \to \dots \to \tau_n \to \tau = t \in \mathcal{S}}{\emptyset, t \Downarrow v^{\sharp}} \text{ na}(\tau) \quad \text{update}_f^{\text{in}}(A, [v_1^{\sharp}, \dots, v_n^{\sharp}]) = A', [v_1'^{\sharp}, \dots, v_n'^{\sharp}] \\ (f, [v_1'^{\sharp}, \dots, v_n'^{\sharp}]) \notin \pi \quad (f, [v_1^{\sharp}, \dots, v_n^{\sharp}]) \because \pi, A', v^{\sharp} \Downarrow_{app} w^{\sharp}, A'' $$

$$ \frac{\text{update}_f^{\text{out}}(A'', [v_1''^{\sharp}, \dots, v_n''^{\sharp}], w^{\sharp}) = w^{\prime\sharp}, A'''}{\pi, A, (f, n) v_1^{\sharp} \dots v_n^{\sharp} \Downarrow_{app} w^{\prime\sharp}, A'''} \text{ SPEC} $$

$$ \frac{\text{val } f : \tau_1 \to \dots \to \tau_n \to \tau = t \in \mathcal{S} \quad \text{na}(\tau)}{\emptyset, t \Downarrow v^{\sharp}} \text{ update}_f^{\text{in}}(A, [v_1^{\sharp}, \dots, v_n^{\sharp}]) = A', [v_1^{\sharp}, \dots, v_n^{\sharp}] \quad (f, [v_1^{\sharp}, \dots, v_n^{\sharp}]) \in \pi} \text{ SPEC-LOOP} $$

$$ \frac{\text{val } f : \tau_1 \to \dots \to \tau_n \to \tau \in \mathcal{S} \quad \text{na}(\tau)}{\pi, A, (f, n) v_1^{\sharp} \dots v_n^{\sharp} \Downarrow_{app} w^{\sharp}, A'} \text{ UNSPEC} $$
<figure><img src="image_76.png" /><figcaption>Figure 8: Extension of Environment through Pattern Matching for Abstract Interpretation</figcaption></figure>

## 5.4 Concretization Function

To define concretization functions for abstract values, we assume monotonic concretization functions for abstract values of non-specified types. Concretization functions are defined for every specified types, and take the state of the abstract interpretation as a parameter:

$\gamma_{\tau}(\mathcal{A}, \cdot) : V_{\text{prg}}^{\sharp}(\tau) \to \mathcal{P}_f(V_{\text{prg}}^{\text{pp}^{\sharp}}(\tau))$. We also define a function of concretization $\gamma_{\text{env}}$ which maps abstract skeletal environments to concrete skeletal environments.

$$
\begin{align*}
\gamma_{\tau_a}(\mathcal{A}, C v^{\sharp}) &= \{ C v \mid C : (\tau, \tau_a), v \in \gamma_{\tau}(\mathcal{A}, v^{\sharp}) \} \\
\gamma_{\tau_1 \times \dots \times \tau_n}(\mathcal{A}, t^{\sharp}) &= \bigcup_{(v_1^{\sharp}, \dots, v_n^{\sharp}) \in t^{\sharp}} \gamma_{\tau_1}(\mathcal{A}, v_1^{\sharp}) \times \dots \times \gamma_{\tau_n}(\mathcal{A}, v_n^{\sharp}) \\
\gamma_{\tau_1 \to \tau_2}(\mathcal{A}, F) &= \{ (f, n) \mid (f, n) \in F \} \cup \{ (p, S, E) \mid (p, S, E^{\sharp}) \in F \land E \in \gamma_{\text{env}}(\mathcal{A}, E^{\sharp}) \} \\
\gamma_{\text{env}}(\mathcal{A}, E^{\sharp}) &= \left\{ E \mid \begin{array}{l} \Gamma \vdash E \quad \Gamma \vdash E^{\sharp} \quad \Gamma \vdash E^{\sharp} \\ \text{dom } E = \text{dom } E^{\sharp}, E(x) \in \gamma_{\tau}(\mathcal{A}, E^{\sharp}(x)) \end{array} \right\} \\
\gamma(\mathcal{A}, \perp_{\tau}) &= \emptyset \\
\gamma(\mathcal{A}, \top_{\tau}) &= V^{\sharp}(\tau)
\end{align*}
$$

**Lemma 1.** If for all unspecified types $\tau_u$, $\gamma_{\tau_u}$ is monotonic on both arguments, then for all $\tau$, $\gamma_{\tau}$ is also monotonic on both arguments.
## 5.5 Correctness of the Abstract Interpretation

**Definition 1.** Let $f$ be an unspecified term of type $\tau_1 \to \dots \to \tau_n \to \tau$ where $na(\tau)$. We say that $[[f]]^\sharp$ is a sound approximation of $[[f]]^{\text{ppt}}$ iff $\forall v_i \in V_{\text{prg}}^{\text{ppt}}(\tau_i), \forall v_i^\sharp \in V_{\text{prg}}^{\sharp}(\tau_i)$, and for all abstract state $A$, if

$$v_i \in \gamma_{\tau_i}(A, v_i^\sharp) \implies [[f]]^{\text{ppt}}(v_1, \dots, v_n) \subseteq \gamma_{\tau}(A', w^\sharp) \\ [[f]]^\sharp(A, v_1^\sharp, \dots, v_n^\sharp) = A', w^\sharp$$

We state the following theorem of correction that states that the abstract interpretation computes a sound approximation of the big-step interpretation.

**Theorem 1.** Suppose $E, S \Downarrow v$ and $\epsilon, A_0, E^\sharp, S \Downarrow v^\sharp, A$ and $\Gamma \vdash E$ and $\Gamma \vdash E^\sharp$ and $\Gamma \vdash S : \tau$ and $E \in \gamma(A, E^\sharp)$.

Suppose $\forall (\text{val } x : \tau) \in S, [[x]]^\sharp$ is a sound approximation of $[[x]]^{\text{ppt}}$.

Then, $v \in \gamma_\tau(A, v^\sharp)$.

Therefore, to prove the soundness of the analysis, it is sufficient to prove that the abstract specifications of terms are sound approximation of the concrete specifications of terms.

# 6 Toward a Control Flow Analysis for $\lambda$-calculus

In this section we show how the abstract interpretation of Skel can be used to define a Control Flow Analysis (CFA) from the Skeletal Semantics of $\lambda$-calculus. A Control Flow Analysis computes an approximation of the Control Flow for higher-order languages. We aim at defining an analysis similar to 0-CFA for $\lambda$-calculus. Let $t$ be a $\lambda$-term, the result of a 0-CFA for term $t$ is two maps. The first one maps variables of $t$ to an approximation of the values the variable can be bound to. The second one maps sub-terms of $t$ to an approximation of the results of the evaluation of the sub-term.

In this section, we call prg the $\lambda$-term to be analyzed.

## 6.1 The State of the Abstract Interpretation

For our analysis, the state of the abstract interpretation contains two maps that we call $C$ and $\rho$:

$$A \cdot C : \text{ppt} \to \mathcal{P}_f(V_{\text{prg}}^{\sharp}(ident) \times V_{\text{prg}}^{\sharp}(lterm))$$

$$A \cdot \rho : \text{ppt} \to V_{\text{prg}}^{\sharp}(ident) \to \mathcal{P}_f(V_{\text{prg}}^{\sharp}(ident) \times V_{\text{prg}}^{\sharp}(lterm))$$

The $C$ function maps a program point to an approximation of the result of evaluation of the sub-term of prg at the program point. For a program point pp, $C(pp)$ is a set of pairs $(x, t)$, that are really $\lambda$-abstractions $\lambda x.t$.

$\rho$ is a function from program points to some abstraction of an environment of $\lambda$-calculus. In classic 0-CFA, there is only one global environment, whereas in our analysis, there is one environment per program point. Practically, it means that to evaluate term $t$, a subterm of the main program prg at program point pp, we use the abstract environment $A \cdot \rho(pp)$.
## 6.2 Specification of the Unspecified Types and Unspecified Terms

As for the big-step semantics with program points, the $\lambda$-terms are program types: $\mathcal{T} = \{\mathbf{lterm}\}$.

We give the specifications of the unspecified types.

$$ \frac{\mathit{id} \in \{x, y, z\dots\} \qquad \mathit{IDENT}}{\vdash^{\sharp} \mathit{id} \in V_{\mathbf{prg}}^{\sharp}(\mathit{ident})} $$

$$ \frac{\mathit{pp} \in \mathbf{ppt}}{\vdash^{\sharp} \mathit{pp} \in V_{\mathbf{prg}}^{\sharp}(\mathit{env})} \qquad \mathit{ENV} $$

$V_{\mathbf{prg}}^{\sharp}(\mathit{ident})$ is a set of variables. An abstract environment $\mathit{pp}_e \in V_{\mathbf{prg}}^{\sharp}(\mathit{env})$ is a program point and refers to $\mathcal{A} \cdot \rho(\mathit{pp}_e)$ which maps variables to a set of pairs representing $\lambda$-abstractions. The definitions of the unspecified terms are:

$$ [[\mathit{getEnv}]^{\sharp}(\mathcal{A}, x, \mathit{pp}_e) = \mathcal{A}, \mathit{Clos}(\{(y, \mathit{pp} \cdot 1, \mathit{pp}) \mid (y, \mathit{pp} \cdot 1) \in \mathcal{A} \cdot \rho(\mathit{pp}_e)(x) \})] $$

$$ [[\mathit{extEnv}]^{\sharp}(\mathcal{A}, \mathit{pp}_e, x, c) = \{ \mathcal{A} \ \mathbf{with} \ \rho = \rho[\mathit{pp}_v \to \mathcal{A} \cdot \rho(\mathit{pp}_e)][x \to \mathcal{A} \cdot \rho(\mathit{pp}_e)(x) \cup c] \}, \mathit{pp}_v \ \mathit{pp}_v \ \mathit{fresh} $$

$\mathcal{A} \cdot \rho(\mathit{pp}_e)(x)$ contains pairs of the form $(y, \mathit{pp} \cdot 1)$ representing $\lambda$-abstractions, therefore $\mathbf{prg}@\mathit{pp} = \mathit{Lam}(y, t)$. $t$ has a program point that ends with 1 because it is the second element of the $\mathit{Lam}$ constructor. getEnv type constraint the result to be in $V_{\mathbf{prg}}^{\sharp}(\mathbf{clos})$, so we need to attach an environment to our pairs $(y, \mathit{pp} \cdot 1)$. Because $(y, \mathit{pp} \cdot 1)$ denotes a $\lambda$-abstraction defined at program point $\mathit{pp}$, the associated environment is $\mathit{pp}$.

[[extEnv]]$^{\sharp}(\mathcal{A}, \mathit{pp}_e, x, c)$ does two things: it modifies the state of the interpretation, and returns a virtual program point. Indeed, extEnv returns a new environment, therefore a program point, but what program point should be returned? We do not know until we evaluate a new $\mathbf{lterm}$ with this environment. Therefore, we create virtual program point that will be linked to a real program point later. The [[extEnv]]$^{\sharp}$ modifies the abstract state such that $\rho(\mathit{pp}_v)$ contains $\rho(\mathit{pp}_e)$ plus the following constraint: $\rho(\mathit{pp}_v)(x) = \rho(\mathit{pp}_e)(x) \cup c$.

There remains to define our update functions:

$$ \mathit{update}_{\mathit{eval}}^{\mathit{in}}(\mathcal{A}, [\mathit{pp}_e, \mathit{pp}_t]) = \{ \mathcal{A} \ \mathbf{with} \ \rho = \mathcal{A} \cdot \rho[\mathit{pp}_t \to \mathcal{A} \cdot \rho(\mathit{pp}_t)] \sqcup^{\sharp} \mathcal{A} \cdot \rho(\mathit{pp}_e)] \}, [\mathit{pp}_t, \mathit{pp}_t] $$

$$ \mathit{update}_{\mathit{eval}}^{\mathit{out}}(\mathcal{A}, [\mathit{pp}_e, \mathit{pp}_t], c) = \{ \mathcal{A} \ \mathbf{with} \ C = C[\mathit{pp}_t \to \mathcal{A} \cdot C(\mathit{pp}) \cup c] \}, c $$

The first update function is used before performing the call `eval pp_e pp_t`, and the second update function is used after the call was done.

$\mathit{pp}_e$ has type `env` and therefore is a program point which refers to $\mathcal{A} \cdot \rho(\mathit{pp}_e)$. $\mathit{pp}_t$ has type `lterm`, and therefore is also a program point denoting the sub-term of `prg` at $\mathit{pp}_t$. Because we want to compute the sub-term at program point $\mathit{pp}_t$, we should use the abstract environment $\mathcal{A} \cdot \rho(\mathit{pp}_t)$. Therefore, the abstract state needs to be modified such that $\mathcal{A} \cdot \rho(\mathit{pp}_e)$ is included into $\mathcal{A} \cdot \rho(\mathit{pp}_t)$, and this is what the first update function does.

The second update function is called after the call is performed. The only thing does is to record the result into the map $\mathcal{A} \cdot C$.

A derivation gives a CFA:

$$ \epsilon, \mathcal{A}_0, \{e \mapsto [] , l \mapsto \epsilon\}, \mathit{eval} \ e \ l \ \mathbf{down}^{\sharp} \ \mathcal{A}, v^{\sharp} $$

The derivation is implicitly parameterized by the $\lambda$-term `prg`. In the initial environment, $l$ is mapped to the program point $\epsilon$, the root of the $\lambda$-term `prg`. $e$ is mapped to an empty
environment of λ-calculus. $A_0$ is the initial state of the abstract interpretation with empty mappings $A_0 \cdot \rho$ and $A_0 \cdot C$. The result of the derivation is a value $v^#$, but most importantly a new state of the interpretation $A$, that contains mappings $A \cdot \rho$ and $A \cdot C$ that are the results of the CFA: $A \cdot \rho$ gives an abstraction of what closures the variables in prg can be bound to, and $A \cdot C$ gives an abstraction of the closures that can appear at a given program point.

# 7 Implementation

This work resulted in an implementation of an Abstract Interpreter Generator [8]: given a skeletal semantics, a specification of unspecified types and terms, it generates an abstract interpreter. We have used it to try our CFA analysis defined in previous sections, and we experimentally compared its output to another CFA program and we found no differences on the examples we tested. So far, our CFA has not been proven incorrect but it remains to do a formal proof or correction.

Moreover, the Abstract Interpreter Generator has been used to generate an abstract interpreter for a small imperative language, with basic integer arithmetic, conditional branchings and loops. For instance, one can do a basic interval analysis. However, we did not do relational analyses.

# 8 Conclusion

We presented our work to generate a CFA analysis for λ-calculus from a skeletal semantics. We presented what are Skeletal Semantics and how they can be interpreted to define a semantics. The strength of this approach is that one only needs to define the unspecified types and terms to mechanize a big-step semantics for a language that has a Skeletal Semantics. An example of how the big-step semantics of λ-calculus could be mechanized using Skeletal Semantics was given using the big-step semantics of Skel. Then we presented our first contribution which is a big-step semantics of Skel with program points. Our second contribution which is an abstract interpretation of Skel, and we stated a theorem of correction. The proof is a work in progress. Our final contribution is a CFA analysis built using the abstract interpretation of Skel for λ-calculus. We implemented an abstract interpreter generator that produces an analyzer from a Skeletal Semantics. We used this program to generate a CFA analyzer for λ-calculus. Our analyzer was experimentally tested and gives similar results to other 0-CFA analyzers.

However, when mechanizing a semantics using an intermediate language like Skel, we expect to lose precision compared to a language specific semantics. Moreover, there are several possible definitions of a Skeletal Semantics for given a language, the abstract interpretation precision may depend on the definition of the Skeletal Semantics. It is a language-independent approach to generate an abstract interpretation for languages with a Skeletal Semantics.

The proof of correction between the big-step semantics and the abstract interpretation must be mechanized. Moreover, our CFA analysis must be compared to other CFA analyses, in particular 0-CFA analysis and verify if we are systematically at least as precise as 0-CFA. Finally, there are not proofs of termination of the abstract interpretation, and this should be addressed.
## References

[1] Bodin, M., Gardner, P., Jensen, T., Schmitt, A.: Skeletal semantics and their interpretations. Proceedings of the ACM on Programming Languages 3(POPL), 1–31 (2019)

[2] Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O’Hearn, P., Pakonstantinou, I., Purbrick, J., Rodriguez, D.: Moving fast with software verification. In: NASA Formal Methods Symposium. pp. 3–11. Springer (2015)

[3] Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. pp. 238–252 (1977)

[4] Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The astrée analyzer. In: European Symposium on Programming. pp. 21–30. Springer (2005)

[5] Noizet, L.: Necro Library, https://gitlab.inria.fr/skeletons/necro, https://gitlab.inria.fr/skeletons/necro

[6] Noizet, L., Schmitt, A.: Semantics in Skel and Necro. In: ICTCS 2022 - Italian Conference on Theoretical Computer Science. CEUR Workshop Proceedings, Rome, Italy (Sep 2022)

[7] Rosu, G., Serbănută, T.F.: An overview of the k semantic framework. The Journal of Logic and Algebraic Programming **79**(6), 397–434 (2010)

[8] Rébiscoul, V.: Abstract Interpreter Generator, https://gitlab.inria.fr/skeletons/abstract-interpreter-generator

[9] Sabry, A., Felleisen, M.: Reasoning about programs in continuation-passing style. In: LISP AND SYMBOLIC COMPUTATION. pp. 288–298 (1993)

[10] Schmidt, D.A.: Natural-semantics-based abstract interpretation (preliminary version). In: International Static Analysis Symposium. pp. 1–18. Springer (1995)

## A Skeletal Semantics of λ-calculus

```
type ident

type env

type clos =
  | Clos (ident, lterm, env)
```

```
type lterm =
  | Lam (ident, lterm)
  | Var ident
  | App (lterm, lterm)
```

```
val extEnv : (env, ident, clos) → env
val getEnv : (ident, env) → clos
```

```
val eval (s:env) (l:lterm): clos =
    branch
        let Lam (x, t) = l in
        Clos (x, t, s)
    or
        let Var x = l in
        getEnv (x, s)
```
or

let App (t1, t2) = l in

let Clos (x, t, s') = eval s t1 in

let w = eval s t2 in

let s'' = extEnv (s', x, w) in

eval s'' t

end

## B Typing Rules of Skeletons and Terms

$$ \frac{\Gamma(x) = \tau}{\Gamma \vdash x : \tau} \text{ VAR} $$

$$ \frac{\textbf{val } x : \tau[= t] \in \mathcal{S}}{\Gamma \vdash x : \tau} \text{ TERMDEF} $$

$$ \frac{\Gamma \vdash t : \tau \quad C : (\tau, \tau')}{\Gamma \vdash C t : \tau'} \text{ CONST} $$

$$ \frac{\forall i, \Gamma \vdash t_i : \tau_i}{\Gamma \vdash (t_1, \dots, t_n) : (\tau_1, \dots, \tau_n)} \text{ TUPLE} $$

$$ \frac{\Gamma + p \leftarrow \tau \vdash S : \tau'}{\Gamma \vdash (\lambda p : \tau \rightarrow S) : \tau \rightarrow \tau'} \text{ FUN} $$

$$ \frac{\Gamma \vdash S_1 : \tau \quad \dots \quad \Gamma \vdash S_n : \tau}{\Gamma \vdash (S_1 \dots S_n) : \tau} \text{ BRANCH} $$

$$ \frac{\Gamma \vdash S : \tau \quad \Gamma + p \leftarrow \tau \vdash S' : \tau'}{\Gamma \vdash \text{let } p = S \text{ in } S' : \tau'} \text{ LETIN} $$

$$ \frac{\Gamma \vdash t_0 : \tau_1 \rightarrow \dots \rightarrow \tau_n \rightarrow \tau \quad \forall i \ \Gamma \vdash t_i : \tau_i}{\Gamma \vdash (t_0 \ t_1 \dots t_n) : \tau} \text{ APP} $$

## C The Functions of a Skeletal Semantics S

$$ \text{Funs}(\Gamma, \text{let } p = S_1 \text{ in } S_2) = \text{Funs}(\Gamma, S_1) \cup \text{Funs}(\Gamma + p \leftarrow \tau, S_2) $$

$$ \text{Funs}(\Gamma, \text{branch } S_1 \dots S_n \text{ end}) = \bigcup_{i=1}^{n} \text{Funs}(\Gamma, S_i) \quad \text{Funs}(\Gamma, t_0 t_1 \dots t_n) = \bigcup_{i=0}^{n} \text{Funs}(\Gamma, t_i) $$

$$ \text{Funs}(\Gamma, \lambda p : \tau \rightarrow S_0) = \{ \Gamma, \lambda p : \tau \rightarrow S_0 \} \cup \text{Funs}(\Gamma + p \leftarrow \tau, S_0) $$

$$ \text{Funs}(\Gamma, (t_1, \dots, t_n)) = \bigcup_{i=1}^{n} \text{Funs}(\Gamma, t_i) $$

$$ \text{Funs}(\Gamma, C t) = \text{Funs}(\Gamma, t) $$

$$ \text{Funs}(\Gamma, x) = \emptyset $$

The set of λ-abstractions in the Skeletal Semantics S is:

$$ \text{Funs}(S) \equiv \bigcup_{\text{val } x:\tau=t \in S} \text{Funs}(\emptyset, t) $$
# D Correction of Big-Step Interpretation with Program Points

**Definition 2.** To relate element with or without program points, we define the following function $\gamma$, such that $\forall \tau, \gamma_{\tau} \in V_{\text{prg}}^{\text{ppt}}(\tau) \rightarrow V(\tau)$. The function $\gamma$ is parameterized by the global value of type $\tau \in \mathcal{T}$ and satisfies the following constraints.

* $\gamma_{\tau}(\text{pp}) = \text{prg}@\text{pp}$ and $\tau \in \mathcal{T}$

* $\gamma_{\tau_1} \times \dots \times \tau_n((v'_1, \dots, v'_n)) = (\gamma_{\tau_1}(v'_1), \dots, \gamma_{\tau_n}(v'_n))$

* $\gamma_{\tau_a}(C v') = C \gamma_{\tau}(v')$ with $C : (\tau, \tau_a)$

* Suppose $\Gamma \vdash E$, and $\Gamma \vdash E'$
  $\gamma_{\text{env}}(E') = E \iff \text{dom } E' = \text{dom } E \land \forall x \in \text{dom } E', \gamma_{\Gamma}(x)(E'(x)) = E(x)$

* $\gamma_{\tau_1 \rightarrow \tau_2}((p, S, E')) = (p, S, \gamma_{\text{env}}(E'))$

* Suppose $\text{val } f : \tau_1 \rightarrow \dots \rightarrow \tau_n \rightarrow \tau[=t] \in S$, then
  $\gamma_{\tau}((f, [v'_1, \dots, v'_n], k)) = (f, [\gamma_{\tau_1}(v'_1), \dots, \gamma_{\tau_n}(v'_n)], k)$

**Definition 3.** Take $f$ such that $\text{val } f : \tau_1 \rightarrow \dots \rightarrow \tau_n \rightarrow \tau \in S$:

$$ \gamma_{\text{unspec}}([f]^{\text{ppt}}) = [f] \iff \forall (v'_i, v_i) \in V_{\text{prg}}^{\text{ppt}}(\tau_i) \times V(\tau_i) \text{ such that } \gamma_{\tau_i}(v'_i)v_i \\ \qquad \gamma_{\tau}([f]^{\text{ppt}}(v'_1, \dots, v'_n)) = [f](v_1, \dots, v_n) $$

**Theorem 2.** Let $\gamma_{\text{env}}(E') = E$, and suppose for all unspecified functions $f$, $\gamma_{\text{unspec}}([f]^{\text{ppt}}) = [f]$, then:

$$ E, S \Downarrow v \implies \exists v', E', S \Downarrow^{PP} v' \text{ and } \gamma_{\tau}(v') = v $$
Traduire l'univers des mathématiques en DEDUKTI,
sans univers

Amélie Ledein<fnref n="1" />* et Elliot Butte<fnref n="2" />

Ces dernières années, le nombre d'assistants à la preuve, de prouveurs automatiques et de vérificateurs de preuve n'a cessé de croître. L'un d'entre eux, le framework logique DEDUKTI, a pour objectif de rendre ces outils formels interopérables, c'est-à-dire rendre possible la réutilisation des preuves d'un outil A dans un outil B. Un autre outil formel, METAMATH, a la particularité d'être à la 4e place dans la liste des systèmes possédant le plus grand nombre de preuves parmi la liste des 100 théorèmes à prouver de Freek Wiedijk, tout en étant constitué de très peu de fonctionnalités : pas de type dépendant, pas de polymorphisme, ni de notion d'univers.

Afin d'agrémenter le nombre de preuves qu'il est possible de traduire dans DEDUKTI, nous présentons Mathiilde, un traducteur automatique de METAMATH vers DEDUKTI. Comme ce traducteur peut utiliser deux encodages différents de METAMATH vers DEDUKTI, nous discutons les avantages et les inconvénients du point de vue de l'interopérabilité.

# 1 Introduction

DEDUKTI [3], un framework logique basé sur le $\lambda\Pi-CALCUL MODULO THÉORIE$, a pour principal objectif l'interopérabilité en se voulant être un standard dans lequel il est possible de définir n'importe quelle logique, mais également avec lequel la traduction d'une logique vers une autre est plus aisée.

Deux cas d'étude sont basés sur une approche utilisant la théorie $\mathcal{U}$ [5], c'est-à-dire ayant pour objectif de simplifier la preuve pour qu'elle soit exprimable dans une logique plus faible, ici une extension, nommée $STT\forall$ [15], de la Théorie des Types Simples avec du polymorphisme prénexe et des opérateurs de type, afin de pouvoir la traduire plus facilement vers d'autres assistants de preuve. En effet, F. Thiré a traduit le petit théorème de Fermat [14, 15], écrit en MATITA, tandis que Y. Géran a traduit le livre I des Éléments d'Euclide [2], écrit en COQ, vers HOL Light, LEAN, MATITA, OpenTheory (donc ISABELLE/HOL et HOL 4), et PVS.

Une autre approche, utilisant l'alignement des concepts, a été suivie dans un autre cas d'étude. A. Assaf, R. Cauderlier et C. Dubois [4, 9] ont reconstruit au sein de DEDUKTI la preuve du Cribble d'Eratosthène initialement écrite en COQ, avec les entiers naturels de HOL. Pour ce faire, il a fallu démontrer des relations de morphisme entre les entiers de COQ et les entiers de HOL. Des travaux en cours s'intéressent également à l'alignement des concepts, c'est-à-dire à des procédés permettant d'identifier des concepts équivalents, comme par exemple les entiers naturels de HOL, de PVS ou encore de COQ, et ainsi éviter la redondance de ces concepts lors de la traduction.

<footnote n="1">¹ Université Paris-Saclay, Inria, CNRS, ENS Paris-Saclay,
Laboratoire Méthodes Formelles, France
amelie.ledein@inria.fr</footnote>

<footnote n="2">² ENSIIE, France</footnote>

<footnote>elliot.butte@ensiie.fr</footnote>

<footnote>*Financée par Digicosme.</footnote>
METAMATH [13] est un *framework* logique dans lequel de nombreux résultats mathématiques ont été formalisés, comme par exemple 74 problèmes sur les 100 faisant partie de la liste de Freek Wiedijk [1]. Ce résultat est particulièrement surprenant au vu du langage décrit dans le Metamath-book [13], puisque celui-ci ne permet de définir que des constantes, des axiomes et des preuves, sans type dépendant, ni polymorphisme, ni univers. Malheureusement, à notre connaissance, de très rares références existent à propos de METAMATH [1, 9, 5, 8], comme une formalisation en METAMATH de la Matching Logic [10], mais ces références ne sont pas suffisantes pour formaliser ce *framework* logique. La référence principale est le Metamath-book [13] mais, par exemple, celui-ci ne présente pas de grammaire formelle du langage de METAMATH, mais seulement une description en anglais.

Ainsi, la première contribution de cet article est constituée d'une proposition d'une grammaire formelle du langage de METAMATH ainsi que d'une formalisation papier de l'étape de normalisation effectuée par au moins l'implémentation de référence d'un vérificateur de preuve pour METAMATH. En plus de cette formalisation partielle de METAMATH, cet article propose deux encodages de METAMATH vers DEDUKTI, l'un plus proche de la philosophie de METAMATH, l'autre plus proche des fonctionnalités courantes d'un assistant de preuve. La traduction automatique de ces encodages est en cours de développement<fnref n="1" />, mais le prototype actuel permet déjà de récupérer une part non-négligeable de la bibliothèque standard de METAMATH à l'aide de notre premier encodage, mais également environ 1 000 preuves écrites dans la logique propositionnelle à la Hilbert à l'aide du deuxième encodage. Ce prototype peut également être vu comme un nouveau vérificateur de METAMATH écrit en OCAML, puisque la construction du λ-terme vérifié par la suite en DEDUKTI est similaire à la méthode de vérification de preuve effectuée par METAMATH.

Après une brève présentation de DEDUKTI (Section 2), nous présentons plus en détails METAMATH, notamment à l'aide d'un exemple d'axiomatisation et de preuve, mais également en expliquant la notion de portée et comment normaliser tout fichier METAMATH (Section 3). Ensuite, nous proposons un premier encodage profond de METAMATH en DEDUKTI, qui se veut être au plus proche de la philosophie même de METAMATH (Section 4). De plus, nous proposons un deuxième encodage en DEDUKTI, plus lisible, qui est cette fois superficiel (Section 5). Ces deux encodages se basent sur une forme normalisée des fichiers METAMATH, comme le montre la figure 1. Enfin, nous présentons les résultats de traduction de la bibliothèque standard de METAMATH pour les différents encodages proposés (Section 6).

<figure><img src="image_77.png" /><figcaption>FIGURE 1 – Vue d'ensemble des deux traductions possibles de METAMATH vers DEDUKTI</figcaption></figure>

Dans la suite, les mots-clefs d'un langage ou ce qui est natif dans un langage seront distingués par de la couleur. Le langage de DEDUKTI se différenciera par une **couleur bleue**, tandis que le langage de METAMATH sera différencié par une **couleur bordeaux**. Celles-ci facilitent la lecture, mais ne sont pas nécessaires à la compréhension.

<footnote n="1">1. https://gitlab.com/semantiko/MM2DK/translator</footnote>
## 2 Dedukti

DEDUKTI [3] est un *framework* logique basé sur le $\lambda\Pi$-CALCUL MODULO THÉORIE, abrégé $\lambda\Pi\equiv_{\tau}$, un $\lambda$-calcul avec types dépendants introduit par Cousineau et Dowek [11], et ayant la particularité de posséder une notion primitive de calcul définie à l'aide de règles de réécriture [12]. Plusieurs logiques ont déjà été encodées au sein de DEDUKTI, comme la logique des prédicats ou encore le Calcul des Constructions Inductives. Diverses logiques ont pu être encodées au sein de DEDUKTI, ce qui favorise la possibilité de rendre interopérables les preuves entre différents outils formels comme Coq ou PVS (Figure 2).

<figure><img src="image_78.png" /><figcaption>FIGURE 2 – L'interopérabilité des preuves grâce à DEDUKTI.</figcaption></figure>

Dans cette section, nous ne présentons que les fonctionnalités disponibles dans DEDUKTI sur lesquelles nous nous appuyons dans la suite et qui permettront de faciliter, ultérieurement, les traductions vers d'autres formalismes.

**Typage et symboles.** La syntaxe du $\lambda\Pi\equiv_{\tau}$ est directement accessible dans DEDUKTI : **TYPE** (sorte native), $\lambda$ (abstraction) et $\Pi$ (produit dépendant). Quand le produit dépendant $\Pi$ ($x$ : $A$), $B$ est en réalité non-dépendant, c'est-à-dire quand $x$ n'est pas une variable libre de $B$, nous notons $A \to B$.

La signature est définie à partir de symboles qui sont composés d'un nom et d'un type exprimable dans le $\lambda\Pi\equiv_{\tau}$. Si la déclaration d'un symbole est faite avec le mot-clé **symbol** seul, on dit que le symbole est défini, sans aucune propriété particulière, alors qu'avec le mot-clé supplémentaire **constant**, le symbole est dit **constant** et ne peut pas être réduit par une règle de réécriture.

L'exemple suivant définit le type des entiers naturels ainsi que les deux constructeurs usuels.

1. **constant symbol** Nat : TYPE;

2. **constant symbol** 0 : Nat;

3. **constant symbol** S : Nat $\to$ Nat;

**Règles de réécriture.** Dans DEDUKTI, une règle de réécriture s'écrit **rule LHS $\leftrightarrow$ RHS** dans laquelle les variables libres sont notées $\$x$, $\$y$, etc. Il est possible d'y utiliser un joker ($\_$) à gauche (LHS) lorsqu'une variable n'est pas utilisée dans la partie droite (RHS). L'exemple suivant définit l'addition sur les entiers naturels définis précédemment.

4. **symbol** + : Nat $\to$ Nat $\to$ Nat;

5. **rule** $\$m + 0 \leftrightarrow \$m$;

6. **rule** $\$m + (S \$n) \leftrightarrow S (\$m + \$n)$;

Les règles de réécriture autorisent l'ordre supérieur, peuvent être non linéaires et ne s'appliquent pas forcément en tête de terme, mais ne sont pas conditionnelles.
## 3.2 Faire une preuve

Le mécanisme de vérification de preuve de METAMATH est basé sur la substitution de variables à l'aide d'une pile. La sous-section 3.2.1 illustre ce mécanisme sur un exemple, tandis que la sous-section 3.2.2 présente plus en détails les contraintes qu'il est possible d'exprimer sur les variables lors de la substitution.

### 3.2.1 Mécanisme général

Un théorème en METAMATH est composé d'un énoncé, lui-même composé ou non de plusieurs hypothèses, et d'une preuve, c'est-à-dire d'une liste de labels. Un label est associé à une *f-hypothèse*, une *e-hypothèse*, un axiome ou un théorème. Par exemple, la preuve du théorème
$$ \vdash (\phi \rightarrow (\psi \rightarrow \chi)) $$
$$ \vdash ((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \chi)) $$
$$ \frac{a2i, \text{ écrite en METAMATH, est disponible à la figure 4.}}{\text{hyp } $e \mid- (\phi \rightarrow (\psi \rightarrow \chi)) $.} $$
$$ a2i \ $p \mid- ((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \chi)) \ $= $$
$$ \begin{array}{l} \text{wph ① wps wch ② wi ③ wi ④} \\ \text{wph wps wi wph wch wi wi ⑤} \\ \text{hyp ⑥} \\ \text{wph wps wch a2 ⑦} \\ \text{mp ⑧ $.} \end{array} $$

<caption>FIGURE 4 – Exemple de preuve écrite en METAMATH</caption>

Sur le même principe que la notation polonaise inversée, le mécanisme de vérification de preuve de METAMATH utilise une pile évitant toute ambiguïté sans avoir recours à l'utilisation de parenthèses au sein de la preuve. Les figures 5 à 12 illustrent ce mécanisme de vérification sur la preuve du théorème a2i. La pile de la figure 5 contient uniquement wff $\phi$, qui correspond au contenu associé au label wph. La pile de la figure 6 est obtenue en empilant du haut vers le bas les éléments wff $\psi$ et wff $\chi$, respectivement associés aux labels wps et wch. Ensuite, comme l'axiome wi possède deux variables, deux *f-hypothèses* lui sont associées, et donc deux éléments sont dépilés du bas vers le haut de la pile. METAMATH cherche ensuite à unifier le premier élément récupéré de la pile avec la *f-hypothèse* wps, et le deuxième élément récupéré de la pile avec la *f-hypothèse* wph. La substitution $\{ \phi \mapsto \psi ; \psi \mapsto \chi \}$ est ainsi obtenue, et le nouvel élément wff $(\psi \rightarrow \chi)$ est mis sur la pile, comme le montre la figure 7. Le même procédé permet d'obtenir la pile de la figure 8, avec la substitution $\{ \phi \mapsto \phi ; \psi \mapsto (\psi \rightarrow \chi) \}$. La suite de labels wph wps wi wph wch wi wi permet de construire la pile de la figure 9 en empilant le nouvel élément wff $((\phi \rightarrow \psi) \rightarrow (\phi \rightarrow \chi))$. Ensuite, le label hyp met le contenu de l'hypothèse hyp sur la pile, comme le montre la figure 10. Enfin, l'élément en tête de la pile de la figure 11 est obtenu grâce à la suite de labels wph wps wch a2, et le label mp permet de finir la preuve, puisque le résultat de l'unification est syntaxiquement égal au contenu associé au label a2i, comme le montre la figure 12.

<figure><img src="image_79.png" /><figcaption>FIGURE 5 – État de la pile en ①</figcaption></figure>

<figure><img src="image_80.png" /><figcaption>FIGURE 6 – État de la pile en ②</figcaption></figure>
wff φ
wff ( φ -> χ )

<caption>FIGURE 7 – État de la pile en ③</caption>

wff ( φ -> ( ψ -> χ ) )

<caption>FIGURE 8 – État de la pile en ④</caption>

wff ( φ -> ( ψ -> χ ) )
wff ( ( φ -> ψ ) -> ( φ -> χ ) )

wff ( φ -> ( ψ -> χ ) )
wff ( ( φ -> ψ ) -> ( φ -> χ ) )
|- ( φ -> ( ψ -> χ ) )

<caption>FIGURE 9 – État de la pile en ⑤</caption>

<caption>FIGURE 10 – État de la pile en ⑥</caption>

wff ( φ -> ( ψ -> χ ) )
wff ( ( φ -> ψ ) -> ( φ -> χ ) )
|- ( φ -> ( ψ -> χ ) )
|- ( ( φ -> ( ψ -> χ ) ) -> ( ( φ -> ψ ) -> ( φ -> χ ) ) )

|- ( ( φ -> ψ ) -> ( φ -> χ ) )

<caption>FIGURE 11 – État de la pile en ⑦</caption>

<caption>FIGURE 12 – État de la pile en ⑧</caption>

La sous-section suivante explique comment sont utilisées les déclarations imposant des contraintes sur les substitutions de variables ($d), lors du processus d'unification.

3.2.2 Une fonctionnalité un peu particulière

La section 3.1 mentionnait des déclarations imposant des contraintes sur les substitutions de variables qu'il est possible d'effectuer. Ces déclarations commencent par la balise $d et ont la sémantique suivante : $d x y $. signifie que pour toute substitution [x ↦→ t₁, y ↦→ t₂, ...] :

— t₁ et t₂ n'ont pas de variable en commun

— Pour toutes variable v de t₁ et variable w de t₂, $d v w $. est vrai dans le contexte local. Cette fonctionnalité permet par exemple de modéliser le λ-calcul comme écrit ci-dessous, où Subst l y v l' signifie que l' correspond à la substitution de y par v dans l.

$c term var lam app Subst $.
$v x y l l' v $.
vx $f var x $. vy $f var y $.
tl $f term l $. tb $f term l' $. tv $f term v $.
$d x y $. $d x v $.
he $e Subst l y v l' $. as $a Subst (lam x l) y v (lam x l') $.

Aucune indication n'existe dans la preuve pour vérifier ces contraintes. METAMATH vérifie en interne les contraintes imposées par ces déclarations, à chaque fois qu'il effectue une substitution.
## 3.3 Utiliser la notion de portée

Le langage de METAMATH offre un peu plus de souplesse que ce que nous avons pu présenter à la section précédente. En effet, il est possible d'importer un fichier METAMATH dans un autre fichier à l'aide de la commande $[filename$], mais il est également possible de jouer sur la portée des hypothèses pour éviter des redondances (${section}$). L'exemple de la figure 3 est très verbeux car il nécessite de recopier à de nombreuses reprises des déclarations de variables et d'hypothèses identiques (seul le label qui leur est associé est différent car tous les labels doivent être uniques). Plus concrètement, les fichiers A et B de la figure 13 sont définis sur la même signature $\Sigma \triangleq \{(\quad); nat; 0; not; =; +; *; /\}$, et sont sémantiquement équivalents. En effet, le fichier A peut se lire ainsi :

Axiome comm-plus : Posons $a$ et $b$, des entiers naturels. Alors $a + b = b + a$.

Axiome eq-div : Posons $a, b, c$ et $d$, des entiers naturels.

Si $c$ n'est pas égal à 0 et que $a * b = d * c$, alors $(a * b) / c = d$.

Le fichier B peut se lire ainsi :

Posons $a, b, c$ et $d$, des entiers naturels.

Axiome comm-plus : $a + b = b + a$.

Axiome eq-div : Si $c$ n'est pas égal à 0 et que $a * b = d * c$, alors $(a * b) / c = d$.

Les fichiers A et B sont donc sémantiquement équivalents.

<table><caption>FIGURE 13 – Deux exemples de fichiers METAMATH</caption><thead><tr><th>Fichier A</th><th>Fichier B</th></tr></thead><tbody><tr><td><pre>$c ( ) nat 0 not = + * / $.<br>$ {<br> $v a b $.<br> nata-p $f nat a $.<br> natb-p $f nat b $.<br> comm-plus $a a + b = b + a $.<br> $}<br><br>$ {<br> $v a b c d $.<br> nata-m $f nat a $.<br> natb-m $f nat b $.<br> natc-m $f nat c $.<br> natd-m $f nat d $.<br> notzero $e not ( c = 0 ) $.<br> eq-mult $e a * b = d * c $.<br> eq-div $a ( a * b ) / c = d $.<br> $}</pre></td><td><pre>$c ( ) nat 0 not = + * / $.<br>$v a b c d $.<br> nata $f nat a $.<br> natb $f nat b $.<br> natc $f nat c $.<br> natd $f nat d $.<br> comm-plus $a a + b = b + a $.<br><br>$ {<br> notzero $e not ( c = 0 ) $.<br> eq-mult $e a * b = d * c $.<br> eq-div $a ( a * b ) / c = d $.<br> $}<br></pre></td></tr></tbody></table>

Il est également possible d'imbriquer des sections les unes dans les autres. La grammaire complète du langage METAMATH que nous proposons est disponible à la figure 14. A notre connaissance, cette grammaire constitue la première formalisation du langage utilisé par METAMATH. Celle-ci découle de notre lecture du Metamath-book [13], ainsi que de l'observation d'une multitude d'exemples.
<table><caption>FIGURE 14 – Grammaire de METAMATH</caption><thead><tr><th></th><th></th><th></th></tr></thead><tbody><tr><td rowspan="10">Basic terminals</td><td>carac ::=</td><td>a-z | A-Z | 0-9</td></tr><tr><td>special-carac ::=</td><td>! | " | # | % | & | ' | ( | ) | * | + | , | - | . | / | : | ; |</td></tr><tr><td></td><td>&lt; = | &gt; | ? | @ | [ | \ | ] | ^ | - | ' | { | " | " | } | ~</td></tr><tr><td>white-space ::=</td><td>| \t | \r | \n | \f</td></tr><tr><td>text ::=</td><td>(carac | special-carac | white-space | $)+</td></tr><tr><td>filename ::=</td><td>((carac | special-carac)+).mm</td></tr><tr><td>math-symbol ::=</td><td>(carac | special-carac)+</td></tr><tr><td>variable ::=</td><td>math-symbol (declared in variable symbol declaration)</td></tr><tr><td>typecode ::=</td><td>math-symbol (declared in constant symbol declaration)</td></tr><tr><td>label ::=</td><td>(carac | - | - | .)+</td></tr><tr><td>Comment</td><td>comment ::=</td><td>$(text $) (not nested)</td></tr><tr><td>Included source file name</td><td>import ::=</td><td>$$[filename+ $]$$</td></tr><tr><td>Constant symbol declaration</td><td>c-decl ::=</td><td>$c math-symbol+ $.</td></tr><tr><td>Variable symbol declaration</td><td>v-decl ::=</td><td>$v math-symbol+ $.</td></tr><tr><td>Block</td><td>b-decl ::=</td><td>$$\{ (comment | v-decl | b-decl | hypothesis | assertion)* $\}$$</td></tr><tr><td>Disjoint-variable restriction</td><td>d-hypo ::=</td><td>$d variable variable+ $.</td></tr><tr><td>Variable-type hypothesis</td><td>f-hypo ::=</td><td>label $f typecode variable $.</td></tr><tr><td>Logical hypothesis</td><td>e-hypo ::=</td><td>label $e typecode math-symbol* $.</td></tr><tr><td>Axiomatic assertions</td><td>a-assert ::=</td><td>label $a typecode math-symbol* $.</td></tr><tr><td>Provable assertions</td><td>p-assert ::=</td><td>label $p typecode math-symbol* $= (label | ?)* $.</td></tr><tr><td>File</td><td>declaration ::=</td><td>c-decl | v-decl | b-decl</td></tr><tr><td></td><td>hypothesis ::=</td><td>d-hypo | f-hypo | e-hypo</td></tr><tr><td></td><td>assertion ::=</td><td>a-assert | p-assert</td></tr><tr><td></td><td>file ::=</td><td>(comment | import | declaration | hypothesis | assertion)*</td></tr></tbody></table>

De plus, le langage de METAMATH possède très peu de sucre syntaxique. La déclaration $\$c c_1 \dots c_d \$. \text{ est équivalente aux déclarations } \$c c_1 \$. \dots \$c c_d \$. \text{, de même que la déclaration } \$v v_1 \dots v_d \$. \text{ est équivalente aux déclarations } \$c v_1 \$. \dots \$c v_d \$. \text{. La déclaration qui impose des contraintes sur les variables } \$d v_1 \dots v_b \$. \text{ correspond aux déclarations } \$d v_i v_j \$. \text{ pour tout } (i,j) \in [1; b-1] \times [i+1; b].

L'étude de l'exemple de la figure 13 illustre que deux fichiers METAMATH peuvent être sémantiquement équivalents mais syntaxiquement très différents. D'après le Metamath-book [13], une étape de normalisation est effectuée au moins par le vérificateur de référence de METAMATH, afin d'en simplifier la vérification. Cette étape de normalisation permet de réécrire le fichier B (Figure 13) et ainsi d'obtenir le fichier A (Figure 13), mais cette étape n'est pas formalisée dans le Metamath-book [13]. La section suivante propose une définition d'un fichier dit normalisé, tel que tout fichier METAMATH puisse se réécrire en un fichier normalisé.

## 3.4 Normaliser un fichier Metamath

Jusqu'à présent, nous avons illustré comment écrire une axiomatisation en METAMATH (Section 3.1) ainsi que comment faire une preuve (Section 3.2), mais également expliqué qu'il est possible d'écrire un fichier METAMATH moins verbeux à l'aide de la notion de portée (Section 3.3). Cette section donne un peu plus de sémantique à la syntaxe vue précédemment, en définissant ce qu'est un fichier METAMATH normalisé, puis en proposant une formalisation papier d'une transformation de tout fichier METAMATH en une version normalisée.

### 3.4.1 Définition d'un fichier normalisé

Par la suite, nous définissons ce qu'est un axiome normalisé, un théorème normalisé ainsi qu'un fichier METAMATH normalisé. Un axiome normalisé, une section constituée, dans l'ordre,
d'une liste de variables, d'une liste de *f*-hypothèses, d'une liste de contraintes sur ces variables, d'une liste de *e*-hypothèses et d'un énoncé. Un théorème normalisé est une section constituée, dans l'ordre, d'une liste de variables, d'une liste de *f*-hypothèses, d'une liste de contraintes sur ces variables, d'une liste de *e*-hypothèses, d'un énoncé et d'une preuve de cet énoncé. Un *f*ichier normalisé est donc composé, dans l'ordre, d'une ou de plusieurs déclarations de constantes puis d'une liste d'axiomes normalisés ou de théorèmes normalisés.

Notre formalisation de la transformation d'un fichier *METAMATH* quelconque en une version normalisée est proposée à la section suivante.

### 3.4.2 Transformation en un fichier Metamath normalisé

Notre formalisation a besoin d'un contexte global noté $\Gamma = (\Sigma, \mathcal{A}, \mathcal{T})$, où $\Sigma$ correspond à la signature, $\mathcal{A}$ est l'ensemble des axiomes et $\mathcal{T}$ est l'ensemble des théorèmes. Nous utilisons également un contexte local noté $\Delta = [ \Delta_0 ; \dots ; \Delta_{n-1} ; \Delta_n ]$ avec $\Delta_i = (\mathcal{V}_i, \mathcal{F}_i, \mathcal{D}_i, \mathcal{E}_i)$, où $\mathcal{V}_i$ est l'ensemble des variables à la profondeur $i$, $\mathcal{F}_i$ est l'ensemble des *f*-hypothèses à la profondeur $i$, $\mathcal{D}_i$ est l'ensemble des *d*-hypothèses à la profondeur $i$ et $\mathcal{E}_i$ est l'ensemble des *e*-hypothèses à la profondeur $i$. La notion de profondeur ici modélise la profondeur d'imbrication : une variable définie à la racine du fichier est à la profondeur 0, donc appartient à $\mathcal{V}_0$, tandis qu'une variable définie dans une section elle-même définie dans une section, sera à la profondeur 2, donc appartient à $\mathcal{V}_2$.

La formalisation que nous proposons est disponible à la figure 15, où $l \ge 0$, $d \ge 1$ et $i \ge 0$. Comme les constantes ne peuvent apparaître qu'à la profondeur 0 d'un fichier, leur traduction n'est valide que pour $i$ valant 0.

<figure><img src="image_81.png" /><figcaption>FIGURE 15 – Formalisation de l'étape de normalisation d'un fichier *METAMATH*</figcaption></figure>

Initialement $\Gamma_{init} = (\emptyset, [ ], [ ]) \text{ et } \Delta_{init} = [ \Delta_0 ]$ où $\Delta_0 = \Delta_{emp} \triangleq ([ ], [ ], [ ], [ ])$. Il faut préserver l'ordre des axiomes et théorèmes car leurs labels peuvent être utilisés dans l'élaboration des preuves des théorèmes, et nous avons vu que la vérification d'une preuve nécessite une pile dont l'ordre des éléments est important car l'inversion de deux hypothèses donnera un résultat tout à fait différent après substitution. Ainsi, nous utilisons rarement la structure mathématique d'ensemble car celle-ci ne préserve pas l'ordre des éléments. Nous optons plutôt pour la structure de liste, et notons $[]$ la liste vide et @ l'opération de concaténation de deux listes.

Le résultat de notre traduction est un couple formé d'un contexte global et d'une liste de contextes locaux. La notation $T_1 \mapsto T_2$ indique que la traduction $T_2$ débute avec le contexte
global et la liste de contextes locaux résultant de la traduction $T_1$. La notation $\Delta \stackrel{X_i}{\leftarrow} Y$ indique que nous remplaçons la composante $X$ par $Y$ dans $\Delta_i$, c'est-à-dire dans le $i$-ème élément de la liste $\Delta$. Enfin, la notation $\bar{\Delta}^{<i}$ correspond à la concatenation, composante par composante, des $i$ premiers éléments de la liste $\Delta$. Les variables, ainsi que les $f$-hypothèses et $d$-hypothèses associées, ne sont gardées que si les variables apparaissent dans les $e$-hypothèses ou dans l'énoncé.

Le fichier normalisé correspond au contexte global $\Gamma_{final} \triangleq (\Sigma_{final}, \mathcal{A}_{final}, \mathcal{T}_{final})$ obtenu à la fin de la traduction. Il est presque possible d'obtenir un fichier METAMATH valide en affichant successivement tous les éléments de $\Sigma_{final}$, puis de $\mathcal{A}_{final}$ et enfin de $\mathcal{T}_{final}$. Pour obtenir un fichier complètement valide, il faut assurer que tous les labels sont uniques, et donc procéder à certaines renommages lors de certaines déclarations, mais également dans les preuves. Nous n'avons pas formalisé ce renommage afin de ne pas alourdir notre formalisation.

Les deux encodages proposés par la suite se basent sur cette forme normalisée.

# 4 Un encodage profond de Metamath en Dedukti

Cette section propose un encodage profond de METAMATH en DEDUKTI, c'est-à-dire un encodage au plus proche de la philosophie actuelle de METAMATH.

## 4.1 Formalisation de l'encodage profond

La normalisation proposée à la section 3.4 nous indique que METAMATH utilise deux méta-opérateurs afin de *lier* les variables, les différentes hypothèses et l'énoncé entre-eux : une quantification universelle, que nous notons $\forall_{MM}$, et une implication, que nous nous notons $\Rightarrow_{MM}$. Ces deux méta-opérateurs manipulent des *tokens*. Nous avons donc besoin de typer chacun des *tokens* :

7 symbol token : TYPE;

A présent, nous pouvons définir les méta-opérateurs notés $\forall_{MM}$ et $\Rightarrow_{MM}$ :

8 symbol $\forall_{MM}$ : (token $\rightarrow$ token) $\rightarrow$ token ;

9 symbol $\Rightarrow_{MM}$: token $\rightarrow$ token ;

10 notation $\Rightarrow_{MM}$ `infix right 10;

En DEDUKTI, il est usuel de définir un symbole permettant de passer d'une formule au type de ses preuves. Ici, ce symbole est noté Prf et est défini à la ligne 11.

11 injective symbol Prf : token $\rightarrow$ TYPE ;

Nous pouvons alors définir un token $\phi$, et une preuve du token $\phi$, notée $\psi$, comme ce qui suit :

12 symbol $\phi$ : token;

13 symbol $\psi$ : Prf $\phi$;

Il nous est maintenant possible d'expliciter un lien entre les méta-opérateurs de METAMATH, et ceux de DEDUKTI, où $b.[a]$ signifie que $a$ peut apparaître dans $b$ :

14 rule Prf ($\forall_{MM}(\lambda a, \$b.[a])$) $\leftrightarrow$ $\Pi a, \$b.[a]$;

15 rule Prf ($\$a \Rightarrow_{MM} \$b$) $\leftrightarrow$ Prf $\$a \rightarrow$ Prf $\$b$ ;
## 4.2 Premières conclusions liées à cet encodage

Ce premier encodage respecte profondément la philosophie propre de METAMATH. Toutes les constantes jouent le même rôle, et le contenu des énoncés des hypothèses, des axiomes et des théorèmes sont des listes de *tokens*. Certains *tokens* ont du être renommés car certains caractères valides pour METAMATH ne sont pas supportés par DEDUKTI comme "`, |, . ou encore ( et ). Finalement, cet encodage préserve la structure de liste initialement donnée par l'utilisateur, mais n'est très pas lisible pour un être humain, comme c'est le cas pour l'énoncé du théorème a2i. Ce premier encodage permet cependant de traduire un très grand nombre de preuves de la bibliothèque standard de METAMATH, comme nous le verrons à la section 6.

Afin de gagner en lisibilité, nous proposons un second encodage qui tente de donner un peu plus de sémantique aux *tokens* à l'aide du typage. En DEDUKTI, ainsi que dans de nombreux autres outils formels, les éléments constituant la signature possèdent un nom et un type (et donc une arité). En METAMATH, les éléments constituant la signature possèdent un nom et sont d'arité 0. La section suivante propose un encodage superficiel qui tente de trouver une structure d'arbre appropriée à partir de cette structure de liste. Cela revient à tenter de trouver les types des éléments constituant la signature (et donc leur arité).

# 5 Vers un encodage superficiel de Metamath en Dedukti

Cette section présente un encodage superficiel de METAMATH en DEDUKTI dont l'objectif principal est de gagner en lisibilité en déterminant le type de chaque symbole de la signature.

## 5.1 La philosophie de notre encodage superficiel

L'idée générale est de considérer que les éléments de la signature qui sont des *typecodes* de *f*-hypothèses sont en réalité des types. Les axiomes qui ont pour *typecode* un type sont donc des axiomes de bonne formation et sont appelés des *axiomes syntaxiques*. Les autres axiomes sont appelés des *axiomes sémantiques*.

Il nous est donc possible de découper notre signature en trois sous-ensembles : l'ensemble des symboles qui sont des types, comme *wff*, l'ensemble des symboles qui apparaissent en tant que *typecode* mais qui ne sont pas des types, comme $|-$, et l'ensemble des symboles, nommés *opérateurs*, qui n'apparaissent jamais en tant que *typecode*, comme $->$. Ces ensembles forment une partition disjointe de la signature initiale.

A partir de ces trois ensembles, nous donnons le type **TYPE** aux symboles de typage. Par exemple, la ligne suivante correspond à la traduction en DEDUKTI du token *wff* :
*constant symbol wff : TYPE ;*

De plus, les axiomes syntaxiques nous permettent d'inférer le type des opérateurs. Par exemple, l'axiome *wi* nous permet d'inférer le type du symbole *->*, et ainsi d'obtenir la traduction suivante en DEDUKTI :
*constant symbol -> : wff -> wff -> wff ;*

Cependant, il ne nous est pas toujours possible d'inférer toutes les informations voulues, comme par exemple le type du symbole $|-$. Cela fait l'objet de la sous-section suivante.
## 5.2 Quelques limites

Cette sous-section liste quelques difficultés rencontrées lorsque nous avons voulu traduire des fichiers *METAMATH* en *DEDUKTI* avec notre second encodage.

**Inférer le type de certains symboles.** Certains symboles sont plus difficiles à typer que d'autres. C'est en particulier le cas des symboles qui apparaissent en tant que *typecode* mais qui ne sont pas des types, comme $|-$.

**Inférer le parsing des opérateurs.** Sous certaines hypothèses, il possible de se passer des informations de précédence et d'associativité, en connaissant, par exemple, le *token* associé à la parenthèse fermante et le *token* associé à la parenthèse ouvrante. Cependant, il est possible que le nom d'un opérateur soit composé de plusieurs *tokens*, comme par exemple l'opérateur de branchement *if-then-else* qui peut s'écrire avec trois *tokens* : *if* _ *then* _ *else* _ . Ce cas de figure est très difficile à identifier syntaxiquement.

**Détecter le sous-typage.** *METAMATH* permet de définir du sous-typage, comme le montre la déclaration suivante :

```
xnat $f nat x $.
xfloat $a float x $.
```

Cette déclaration indique que si $x$ appartient à l'ensemble des entiers, alors $x$ appartient aussi à l'ensemble des nombres à virgule. Il est possible traduire ce type de définition en *DEDUKTI* à l'aide d'une injection de l'ensemble de départ vers celui d'arrivée. Cette partie de la traduction n'a pas encore été implémentée à l'heure actuelle.

## 5.3 Une solution avec des annotations

Pour pallier aux problèmes liés à l'inférence de type et de parsing, il possible non plus de traduire un fichier *METAMATH*, mais plutôt de traduire un fichier *METAMATH* modulo d'autres informations fournies par l'utilisateur, à l'aide d'un fichier JSON par exemple.

A ce stade, nous proposons uniquement à l'utilisateur de préciser un nom de substitution valide pour *DEDUKTI* (*name_dedukti*), le type du symbole (*type*), la manière dont il faut le parser (*mixfix* et *precedence*) ou si le symbole est à considérer comme une parenthèse ouvrante ou fermante. Un exemple de fichier JSON est disponible à la figure 16 : celui-ci permet de traduire le symbole $|-$ vu précédemment.

```json
{
  name_metamath: "|-",
  name_dedukti: "taquet",
  type: "wff -> TYPE,"
  mixfix: "prefix",
  precedence: 40
}

constant symbol taquet : wff -> TYPE ;
```

<caption>FIGURE 16 – Exemple de traduction d'un symbole à partir d'un fichier JSON</caption>

Ainsi, à l'aide du type précisé dans le fichier JSON, *DEDUKTI* est capable de vérifier le typage de la traduction de l'axiome du modus ponens : *constant symbol mp* : Π ($\phi$ : wff), Π ($\psi$ : wff), $|-\phi \rightarrow |- (\phi \rightarrow \psi) \rightarrow |-\psi ;$.
De plus, la traduction d'une preuve *METAMATH* en $\lambda$-terme est illustrée aux figures 17 à 24. Cette traduction suit le même mécanisme que celui que *METAMATH* utilise pour vérifier une preuve. La subtilité est que c'est le contenu des *f*-hypothèses, des *e*-hypothèses et des axiomes syntaxiques qui est mis sur la pile, tandis que pour les axiomes sémantiques, nous utilisons le label qui lui est associé, en utilisant les arguments qui sont sur la pile. Ainsi, il est possible d'obtenir le $\lambda$-terme $\lambda\varphi$, $\lambda\psi$, $\lambda\chi$, $\lambda$hyp, mp $\alpha\beta$ hyp (a2 $\varphi\psi\chi$) avec $\alpha \triangleq (\varphi \rightarrow (\psi \rightarrow \chi))$ et $\beta \triangleq ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \chi))$ à partir de la preuve de la figure 4.

<figure><img src="image_82.png" /><figcaption>FIGURE 17 – État de la pile en ①</figcaption></figure>

<figure><img src="image_83.png" /><figcaption>FIGURE 18 – État de la pile en ②</figcaption></figure>

<figure><img src="image_84.png" /><figcaption>FIGURE 19 – État de la pile en ③</figcaption></figure>

<figure><img src="image_85.png" /><figcaption>FIGURE 20 – État de la pile en ④</figcaption></figure>

<figure><img src="image_86.png" /><figcaption>FIGURE 21 – État de la pile en ⑤</figcaption></figure>

<figure><img src="image_87.png" /><figcaption>FIGURE 22 – État de la pile en ⑥</figcaption></figure>

<figure><img src="image_88.png" /><figcaption>FIGURE 23 – État de la pile en ⑦</figcaption></figure>

<figure><img src="image_89.png" /><figcaption>FIGURE 24 – État de la pile en ⑧</figcaption></figure>

L'ajout d'un fichier JSON lors du processus de traduction semble être la seule manière de contourner les différents problèmes que nous rencontrons lorsque nous cherchons à obtenir un encodage superficiel de *METAMATH* en *DEDUKTI*. Cependant, cette solution n'est pas complètement satisfaisante puisque la vérification d'un fichier *METAMATH* ne dépend plus uniquement du fichier lui-même, mais également du fichier JSON fourni par l'utilisateur. Un fichier *METAMATH* vérifié par *DEDUKTI* est donc correct modulo les informations fournies à l'aide du fichier JSON donné par l'utilisateur lors de la traduction. Une question ouverte résiste donc : quelle(s) propriété(s) les informations données dans le fichier JSON doivent-elles vérifier pour que la traduction soit pertinente et correcte ?
# 6 Traduction de la bibliothèque standard de Metamath

Cette section étudie la traduction de la bibliothèque standard de METAMATH avec nos deux encodages, afin de valider les encodages proposés. Après avoir présenté les résultats obtenus, nous proposons une extension commune à l'encodage superficiel et l'encodage profond.

## 6.1 Résultats de la traduction pour chaque encodage

La bibliothèque standard de METAMATH est composée de neuf fichiers disponibles sur GitHub : https://github.com/metamath/set.mm. Les résultats obtenus avec les implémentations actuelles des traductions utilisant nos deux encodages sont disponibles à la figure 25.

<table><caption>FIGURE 25 – Pourcentage de traduction de la bibliothèque standard de METAMATH pour les différents encodages proposés</caption><thead><tr><th></th><th>demo0.mm</th><th>miu.mm</th><th>peano.mm</th><th>big-unifier.mm</th><th>hol.mm</th><th>ql.mm</th><th>nf.mm</th><th>iset.mm</th><th>set.mm</th></tr></thead><tbody><tr><td>Taille du fichier</td><td>1.4K</td><td>4.6K</td><td>28K</td><td>39K</td><td>231K</td><td>1.8M</td><td>8.3M</td><td>11M</td><td>273M</td></tr><tr><td>Nombre de :</td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>- déclaration(s)</td><td>19</td><td>27</td><td>116</td><td>29</td><td>2 768</td><td>936</td><td>24 967</td><td>30 813</td><td>196 976</td></tr><tr><td>- axiome(s)</td><td>7</td><td>10</td><td>48</td><td>4</td><td>77</td><td>71</td><td>363</td><td>467</td><td>2711</td></tr><tr><td>- preuve(s)</td><td>1</td><td>1</td><td>0</td><td>2</td><td>1 138</td><td>138</td><td>5 966</td><td>8 990</td><td>38 766</td></tr><tr><td>Pourcentage traduit avec l'encodage :</td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>- profond</td><td>100</td><td>0</td><td>100</td><td>100</td><td>95,87</td><td>100</td><td>79,07</td><td>80,29</td><td>65,26*</td></tr><tr><td>- profond étendu</td><td>100</td><td>0</td><td>100</td><td>100</td><td>100</td><td>100</td><td>100</td><td>100</td><td>100*</td></tr><tr><td>- superficiel</td><td>100</td><td>0</td><td>0</td><td>100</td><td>0</td><td>0+</td><td>0+</td><td>0+</td><td>2,52+</td></tr></tbody></table>

Les pourcentages obtenus indiquent la proportion traduite pour chaque fichier et pour chaque encodage. Les fichiers obtenus ont pu être vérifiés par DEDUKTI, sauf pour les pourcentages ayant une étoile (*). Le fichier set.mm étant très volumineux, nous n'avons pas encore réussi à vérifier le typage de la totalité des deux fichiers de traduction obtenus, alors que METAMATH n'a besoin que de quelques secondes pour vérifier le fichier set.mm. Cette différence s'explique en partie car notre traducteur ne fonctionne qu'avec des fichiers METAMATH décompressés. Par exemple, la taille du fichier set.mm compressé est de 40.8M, et il faut plusieurs heures pour décompresser ce fichier. De plus, nous n'avons pas pu traduire le fichier miu.mm car celui-ci autorise la substitution d'une variable par *rien*, fonctionnalité considérée *unsafe* par METAMATH lui-même.

Dans le cas de l'encodage profond présenté à la section 4, la quasi-totalité des axiomatisations et des preuves a pu être traduite. Les preuves non traduites utilisent des variables libres, ce qui est possible car METAMATH fait l'hypothèse que tous les types qu'il manipule sont non vides. Les fichiers hol.mm, nf.mm, iset.mm et set.mm possèdent respectivement 47, 1 249, 1 772 et 13 466 preuves nécessitant la traduction de ce cas de figure. Nous avons donc implémenté un encodage profond étendu afin de pouvoir traduire ces preuves : cette extension est suffisante pour traduire
toutes les preuves restantes, comme le montre la figure 25. Ce cas de figure est illustré dans la sous-section suivante, ainsi qu'une explication plus détaillée de l'extension codée pour traduire la totalité des preuves de la bibliothèque standard de METAMATH avec notre encodage profond. Cette extension est également nécessaire pour notre encodage superficiel.

Dans le cas de l'encodage superficiel présenté à la section 5, nous nous sommes principalement concentrés sur la traduction de la logique propositionnelle à la Hilbert (extrait du fichier set.mm), dont nous avons réussi à traduire en DEDUKTI environ 1 000 preuves. Le fichier peano.mm n'a pas pu être traduit car nous n'avons pas encore implémenté la génération d'injections à partir des axiomes de sous-typage. Le fichier hol.mm n'a également pas pu être traduit car il nécessite la traduction d'un opérateur d'application n'ayant pas de token, comme le montre la figure 26.

$c term ( ) $.  
$( Term variables $)  
$v F T $.  
tf $f term F $.  
tt $f term T $.  
$( A combination (function application). $)  
kc $a term ( F T ) $.

<caption>FIGURE 26 – Extrait du fichier hol.mm</caption>

Le pourcentage de traduction des fichiers ql.mm, nf.mm, iset.mm et set.mm est certainement plus élevé que celui annoncé car nous n'avons pas cherché à écrire la totalité des fichiers JSON nécessaires. En effet, cette tâche est longue et fastidieuse car il faut réussir à inférer manuellement un parsing et un typage correcte pour tous les tokens dont cela est nécessaire. Il nous semble plus judicieux d'essayer de trouver une méthode automatique pour trouver ces informations, vérifier la conformité du fichier traduit en DEDUKTI, puis essayer une nouvelle possibilité de parsing ou de typage en cas d'échec.

## 6.2 Une extension commune pour chaque encodage

Certaines preuves utilisent des variables qui ne sont pas liées dans l'énoncé du théorème. Cela est possible car, implicitement, METAMATH fait l'hypothèse que tout type est habité : il existe donc au moins une variable pour chaque type. Cependant, ces preuves utilisent des variables libres, qui n'existent plus lors de l'étape de normalisation. Considérons la formalisation en METAMATH suivante afin d'illustrer nos propos :

$c ( ) -> <- > wff |- $.      $c A. setvar class = T. $.  
$v ph ps $.      ${ $v x $.  
wph $f wff ph $.      vx.wal $f setvar x $.  
wps $f wff ps $.      wal $a wff A. x ph $. $}  
wi $a wff ( ph -> ps ) $.      ${ $v x $.  
vx.cv $f setvar x $.  
cv $a class x $. $}  
id $p |- ( ph -> ph ) $= ... $.      ${ $v A B $.  
${ mpbir.min $e |- ps $.      cA.wceq $f class A $.  
mpbir.maj $e |- ( ph <- > ps ) $.      cB.wceq $f class B $.  
mpbir $p |- ph $= ... $. $}      wceq $a wff A = B $. $}  
wtru $a wff T. $.
$$
\begin{array}{l}
\$ v x $. \\
\qquad vx.tru $f setvar x $. \\
\qquad df-tru $a |- ( T. <-> ( A. x x = x -> A. x x = x ) ) $. \\
\qquad tru $p |- T. $= \\
\qquad \qquad wtru vx.tru cv vx.tru cv wceq vx.tru wal vx.tru cv vx.tru cv \\
\qquad \qquad wceq vx.tru wal wi vx.tru cv vx.tru cv \\
\qquad \qquad wceq vx.tru wal id vx.tru df-tru mpbir $. \$
\end{array}
$$

La preuve du théorème tru utilise le label vx.tru introduisant la variable x dans la pile. Lors
de la traduction vers DEDUKTI, la variable x sera libre car elle n'apparait pas dans l'énoncé du
théorème tru. En effet, la forme normalisée de la section précédente est :

$$
\begin{array}{l}
\$ v x $. \\
\quad vx.tru $f setvar x $. \\
\quad df-tru $a |- ( T. <-> ( A. x x = x -> A. x x = x ) ) $. \$
\end{array}
$$
$$
\begin{array}{l}
\text{tru } \$ p \mid - \text{ T. } \$ = \\
\qquad \text{wtru } \text{vx.tru cv } \text{vx.tru cv wceq } \text{vx.tru wal } \text{vx.tru cv } \text{vx.tru cv} \\
\qquad \text{wceq } \text{vx.tru wal wi } \text{vx.tru cv } \text{vx.tru cv} \\
\qquad \text{wceq } \text{vx.tru wal id } \text{vx.tru df-tru mpbir } \$ .
\end{array}
$$

Ainsi, la preuve du théorème tru utilise le label vx.tru qui n'est plus dans la portée du théorème tru. Nous devons étendre les encodages proposés afin de générer les habitants nécessaires pour chaque type. Dans le cadre de notre exemple, nous devons donc également générer le symbole suivant en DEDUKTI : constant symbol vxDottru : Prf ( setvar # x ) ;.

Cette extension est suffisante pour traduire les preuves restantes de la bibliothèque standard de METAMATH, dans le cas de notre encodage profond.

7 Conclusion

Nous venons de présenter deux encodages de *METAMATH* vers *DEDUKTI*, l'un profond, l'autre superficiel.

L'encodage profond de *METAMATH* en *DEDUKTI* nous apprend que la logique de *METAMATH* est faible puisqu'elle n'est constituée que d'un opérateur de quantification et d'un opérateur d'implication. Cette logique semble suffisamment faible pour utiliser les travaux effectués par F. Thiré [14] afin de traduire le résultat obtenu vers *COQ*, *ISABELLE* ou encore *PVS*.

L'encodage superficiel, plus lisible pour un être humain, permet de mettre en lumière les fonctionnalités usuelles modélisées dans une formalisation écrite en *METAMATH*, comme le sous-typage. Cependant, cet encodage pose de nombreuses questions sur comment utiliser *DEDUKTI* pour traduire le résultat obtenu vers *COQ*, *ISABELLE* ou encore *PVS*. De plus, il semble difficile de pouvoir complètement automatiser la traduction de fichiers *METAMATH* dans cet encodage.

La traduction des *d*-hypothèses n'a jamais été présentée, car celles-ci ne sont utilisées que
dans un mécanisme de vérification interne à *METAMATH* dont aucune information n'apparaît
dans la preuve écrite en *METAMATH*. Il semble cependant possible d'étendre notre encodage
profond pour également encoder cette vérification.

Cet article constitue donc une étape important pour permettre l'interopérabilité des preuves écrites en *METAMATH* à l'aide de *DEDUKTI*, en utilisant l'approche basée sur la théorie *U* [5].

De plus, nous envisageons d'étendre le nombre de fichiers *METAMATH* traduits, comme par
exemple grâce à la formalisation en *METAMATH* de la MATCHING LOGIC [10].
Enfin, M. Carneiro a proposé des modèles pour les différentes parties de la bibliothèque standard de METAMATH [7]. Nous envisageons une comparaison plus approfondie de ces tra vaux avec les nôtres. M. Carneiro a également proposé METAMATH-Zero [8], un outil formel inspiré de METAMATH mais qui n'utilise pas de pile de preuves, et qui considère ses expressions comme des arbres et non comme des listes. Nous envisageons de mieux comprendre les liens entre METAMATH et METAMATH-Zero, afin d'évaluer la difficulté à récupérer des preuves de METAMATH-Zero dans DEDUKTI.

**Remerciements** : Nous remercions Catherine DUBOIS, Chantal KELLER et Andrei PASKEVICH pour les remarques, commentaires et conseils qu'ils nous ont apportés tout au long de ce travail. Nous remercions également les reviewers anonymes pour leurs remarques et suggestions.

Références

[1] Formalizing 100 Theorems - Freek Wiedijk. https://www.cs.ru.nl/~freek/100/.

[2] Translation of proofs of Euclid's book I into HOL Light, Lean, Matita, OpenTheory and PVS, note = https://github.com/karnaj/sttfa_geocoq_euclid.

[3] Ali Assaf, Guillaume Burel, Raphal Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant, and Ronan Saillard. Expressing theories in the λΠ-calculus modulo theory and in the Dedukti system. In TYPES : Types for Proofs and Programs, Novi SAd, Serbia, May 2016.

[4] Ali Assaf and Raphaël Cauderlier. Mixing HOL and Coq in Dedukti (Extended Abstract). In Cezary Kaliszyk and Andrei Paskevich, editors, Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015, volume 186 of EPTCS, pages 89–96, 2015.

[5] Frédéric Blanqui, Gilles Dowek, Émilie Grienenberger, Gabriel Hondet, and François Thiré. Some axioms for mathematics. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference), volume 195 of LIPIcs, pages 20:1–20:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.

[6] Mario Carneiro. Conversion of HOL Light proofs into Metamath, 2014.

[7] Mario Carneiro. Models for Metamath, 2016.

[8] Mario Carneiro. Metamath Zero : The Cartesian Theorem Prover, 2019.

[9] Raphaël Cauderlier and Catherine Dubois. FoCaLiZe and Dedukti to the Rescue for Proof Interoperability. In Mauricio Ayala-Rincón and César A. Muñoz, editors, Interactive Theorem Proving, pages 131–147, Cham, 2017. Springer International Publishing.

[10] Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, and Grigore Roșu. Towards a Trustworthy Semantics-Based Language Framework via Proof Generation. In Proceedings of the 33rd International Conference on Computer-Aided Verification. ACM, July 2021.

[11] D. Cousineau and Gilles Dowek. Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo. In TLCA, 2007.

[12] Nachum Dershowitz and Jean-Pierre Jouannaud. Rewrite systems. In Handbook of Theoretical Computer Science, Volume B : Formal Models and Semantics, pages 243–320, 1990.

[13] Norman D. Megill. Metamath : A Computer Language for Mathematical Proofs. Lulu Press, Morrisville, North Carolina, 2019. http://us.metamath.org/downloads/metamath.pdf.

[14] François Thiré. Sharing a Library between Proof Assistants : Reaching out to the HOL Family. Electronic Proceedings in Theoretical Computer Science, 274 :57–71, jul 2018.

[15] François Thiré. Interoperability between proof systems using the logical framework Dedukti. (Interopérabilité entre systèmes de preuve en utilisant le cadre logique Dedukti). PhD thesis, École normale supérieure Paris-Saclay, Cachan, France, 2020.
# Backtracking reference stores

Camille Noûs¹ and Gabriel Scherer²

¹ Laboratoire Cogitamus

² INRIA

## Abstract

François Pottier's unionFind library is parameterized over an underlying store of mutable references, and provides the usual references, transactional reference stores (for rolling back some changes in case of higher-level errors), and persistent reference stores. We extend this library with a new implementation of backtracking reference stores, to get a Union-Find implementation that efficiently supports arbitrary backtracking and also subsumes the transactional interface.

Our backtracking reference stores are not specific to unionFind, they can be used to build arbitrary backtracking data structures. The natural implementation, using a journal to record all writes, provides amortized-constant-time operations with a space overhead linear in the number of store updates. A refined implementation reduces the memory overhead to be linear in the number of store cells updated, and gives performance that match non-backtracking references in practice.

# 1 Introduction

Our own use-case for the present work comes from implementing a type-checker for an explicitly-typed (no inference required) extension of System F with Guarded Algebraic Datatypes (GADTs). With GADTs, datatype constructors may witness equalities between types. For example, matching on the constructor `Int` at type `α` reveal that the (universally quantified) type variable `α` is in fact equal to `int`, that is, introduce the equality (`α` = `int`) in the typing context. Then under this context we have to type-check a sub-expression, the right-hand-side of the pattern matching clause, which in particular involves checking many type equalities (`Γ` ⊢ `τ₁ = τ₂`) modulo the equations in `Γ`. For example, the types (`α` → `int`) and (`int` → `α`) are distinct in general, but they are equal under the assumption (`α` = `int`).

Union-Find is the perfect data structure to efficiently check equalities in presence of equality assumptions. Our type-checker carries a global Union-Find graph, we create nodes for bound type variables, equality assumptions add unification edges in the graph, and equality checking can be implemented efficiently – even in presence of cyclic graphs / equi-recursive types. But adding a *local* equality assumption, as required by GADTs, requires a form of *backtracking*: we add unification edges before checking the sub-expressions of the GADT pattern clause, but these edges should not remain present when type-checking the rest of the term outside this clause.

A simple solution to this problem is to use a *persistent* Union-Find; there is a generic way to implement a persistent version of a mutable data-structure, which is to replace all mutable references by indices into a persistent map. When we extend a persistent Union-Find graph `G` with a new equality, we get a new Union-Find graph `G'`; we can type-check the clause right-hand-side using `G'` and then go back to `G` to check the rest of the type derivation.
```javascript
let rec typeof env = function (* ... *)
| Use (t, u) ->
  match typeof env t with
| TyEq (ty1, ty2) ->
  let env = introduce_equalities env ty1 ty2 in
  typeof env u
| ty -> raise (TypeError (NotAnEquality ty))
```

However, this solution imposes a logarithmic overhead to all accesses and updates, which adds a noticeable constant factor on reasonably-large programs. This is especially frustrating given that GADTs are a relatively rare language feature; the whole type-checker pays for a feature that may not even occur in the program being type-checked.

Another solution is to use a mutable, constant-time-access Union-Find graph, but perform a copy of the graph when entering a GADT equality assumption. This has cost linear in the number of type variables in context, which is unpleasant, but the cost is localized to GADT use sites. This is a reasonable solution that, let's be frank, would probably be fine in practice for our use-case.

```javascript
match typeof env t with
| TyEq (ty1, ty2) ->
  let env = { env with store = StoreVector.copy store } in
  introduce_equalities env ty1 ty2;
  typeof env u
```

We want to do better by implementing a Union-Find that supports both constant-time access/update and (amortized) constant-time backtracking.

```javascript
match typeof env t with
| TyEq (ty1, ty2) ->
  BtRef.branch env.store;
  let finally () = BtRef.terminate_rollback env.store in
  Fun.protect ~finally @@ fun () ->
  introduce_equalities env ty1 ty2;
  typeof env u
```

## 1.1 A trusted ally: a modular Union-Find library

François Pottier's `unionFind` library provides an efficient implementation of Union-Find parameterized over a notion of *mutable store*, which allows to choose the implementation of mutable references used in the Union-Find graph. At the time of writing, it provides four implementations of this store interface:

**`StoreRef`** uses OCaml references directly. This gives the standard UnionFind behavior.

**`StoreMap`** uses indices into a persistent map. This gives a mutable API that operates on a persistent graph under the hood, providing a constant-time operation to copy (share) the whole graph. Algorithmically this corresponds exactly to the persistent approach we discussed above.

**`StoreVector`** uses indices into a dynamic array. This gives constant-time access and update, but tracks the set of nodes of the graph (and refers them through indices, a portable indirection) which allows copying the whole graph in linear time. This corresponds exactly to the copying approach we discussed above.
**StoreTransactionalRef** implements a *transactional* reference store, which allow starting a global transaction with the ability to either commit all changes that happened during the transaction or to roll them back. This is important for type-checking algorithms that provide partial operations (typically unification) on top of the Union-Find graph. An operation may perform several unifications in sequence, but it should leave the graph unchanged in case the operation fails – typically to print error messages to the user without showing an inconsistent, in-progress state. Transactions cannot be nested.

## 1.2 Our contribution

We implement a *backtracking reference store* that allows to backtrack to previous versions of the store in amortized constant time. A store contains many references that are versioned together. There are explicit operations to *branch* the store into a new version, or return a store to its parent version. In particular, if we roll back to a previous version, this rolls back the value of all references in the store that were modified since the last branch. We can instantiate François Pottier’s *unionFind* implementation with our new store, solving our quest for Union-Find with backtracking.

**Implementation** The implementation of our structure is fairly simple, Intuitively the store maintains a *journal*, or *undo log*, of all reference updates, which allows to roll back to previous versions. In fact we have two implementations:

* In our first, simplest implementation, all updates are logged in the journal. Read/write operations are constant-time, backtracking to the parent version is amortized constant-time. But the journal adds a space overhead linear in the number of updates and branches performed. (This is just fine for Union-Find, where the number of updates per node is less than logarithmic. But our store may have other users without such guarantee.)

* We then propose a *record-eliding* optimization that uses timestamps to avoid recording a given reference twice for the same version of the structure. The space overhead is linear in the number of references updated in each version, rather than the number of writes.

**Interface** The building blocks of our implementations subsume two different flavors of interfaces that we can express on top of our work:

* We can provide a semi-persistent interface in the sense of Conchon and Filliâtre (2008).

* We provide a transactional interface, subsuming François Pottier’s transactional references, but in addition we support arbitrary nesting of transactions.

**Terminology:** *backtracking, semi-persistent, transactional* Conchon and Filliâtre (2008) proposes a specific API design for *semi-persistent* structures where backtracking to a previous version is implicit. It happens on-demand when we start again to work on an older version, the first access to this older version implicitly invalidates/backtrack any more recent version. This gives a very declarative programming style, close in spirit to programming with persistent data structures, hence the name *semi-persistent*.

Our core API is different, more imperative. Terminating a version is explicit; this works better with the transactional interface that gives two different ways to terminate a version (*commit* or *abort*), making the implicit choice awkward. But one can easily build the semi-persistent API on top of our existing interface – we do it in Section 4.2. We call our API a *backtracking* API, although it is a bit more expressive than typical backtracking APIs that
only allow to rollback or abort changes, while we can also commit them – as with transactional interfaces.

A more precise name may be *transactional*, but we already use it in the context of François Pottier's *StoreTransactionalRef* stores that do not support nested transactions. We could call them *one-transactional*, or call ours *nested-transactional*, but we stick with the more common *backtracking*.

**Generality** We emphasize that while our own use-case is a backtracking Union-Find, our backtracking (and transactional) references are of general interest and could be used to implement basically any backtracking data-structure.

For example, you can rebuild backtracking arrays by simply using arrays of references in a shared backtracking store – at the constant-factor cost of an extra isndirection per array element. This would be silly for backtracking or semi-persistent arrays where specialized implementations are already available, or for structures that are naturally built by composing existing backtracking libraries, in the same way Conchon and Filliâtre (2008) builds semi-persistent hashtables out of semi-persistent dynamic arrays and semi-persistent stacks. But you may be interested in backtracking doubly-linked lists, backtracking quad-trees, backtracking skiplists, etc.

## 1.3 Early challengers: (semi-)persistent dynamic arrays

As we were considering this journey of implementing our own backtracking references, the wizard Jean-Christophe Filliâtre sent us the following remark to test our resolve.

> It is possible to implement a Union-Find graph backed by a dynamic array, so you get a semi-persistent Union-Find by using an existing library of semi-persistent dynamic arrays.

This solution has in fact already been presented in Conchon and Filliâtre (2007), which proposes a persistent Union-Find implementation backed by a dynamic array, but tweaks it slightly to be only semi-persistent in its Section 2.3.3.

Our justification for writing our own code is that array-backed Union-Find graphs – including the use of François Pottier’s *unionFind* instantiated with its *StoreVector* module we mentioned above – do not play nicely with garbage collection. All nodes of the graph remain alive as long as the graph lives. In contrast, direct representations where the Union-Find graph is realized by pointers in memory preserve the liveliness of individual nodes, which can be collected as soon as they are not used in the program anymore.

This makes a difference in our use-case of using a Union-Find graph on the fly for type-checking: when we traverse our typing derivation, we generate many Union-Find nodes on the fly, each time we check an equality between types. But they are extremely short-lived, we do not use them after we have checked those equalities. We expect those dead fragments of the Union-Find graph to be collected promptly, while they leak when using an array-backed implementation.

Note that transactional or backtracking references also extend the lifetime of values in certain circumstances: to allow rolling back to a previous version we necessarily keep those previous versions alive in memory. But this lifetime-extension ends when the corresponding transaction or version is terminated. In our Union-Find use-case, this means that the garbage-collection behavior of Union-Find nodes is unchanged by these journaling mechanisms.

Finally, (semi-)persistent arrays, in existing OCaml implementations, do not provide the equivalent of our record-eliding optimization – their memory overhead is linear in the total
number of writes, instead of the number of distinct positions written. It may be possible
to implement it; we suspect that it is non-obvious for semi-persistent arrays and difficult for
persistent arrays. If we want record elision, we need to write new code anyway.

**Remark: persistent vs. semi-persistent** Semi-persistent data-structures were introduced in Conchon and Filliâtre (2008) as an optimization of fully-persistent data structures for scenarios where backtracking is required, but not more complex reuse scenarios. We mentioned earlier a naive strategy for persistence adding a logarithmic overhead on all access. But note that persistent data-structures can also be fast thanks to rerooting as presented in Conchon and Filliâtre (2007), almost as fast as semi-persistent data structures.

Reusing the existing implementation of a Union-Find graph backed by a persistent array
would certainly be fine performance-wise; as with any array-backed approach it prevents garbage
collection, and we believe that implementing the record-eliding optimization would be more dif-
ficult. Our record-eliding optimization relies on the fact that valid versions of a semi-persistent
data structure form a linear structure, so they can be denoted by integers, with a fast check of
whether a version is an ancestor of another. On the other hand, fully persistent data structures
have a tree of versions, so our approach does not work.

2 Specification

In this section we present the set of primitive operations supported by our backtracking
store of references, just their specification.

Note: we did not start by writing down a specification, we started by writing an implemen-
tation with a bug on nested transactions. We had to work out a clear specification to avoid the
bug in the future.

## 2.1 Specifying backtracking data structures

Let us first recall the vocabulary to specify semi-persistent data structures proposed in
Conchon and Filli\`atre (2008).

In a semi-persistent implementation, there are several *versions* of the same mutable struc-
tures, in our case a store, that is, a set of references. Each version of the data-structure has a
corresponding state, independent of the other versions.

There is a *current* (most recent) version.

We can *branch* a new version from the current version: it is a child of the current version
and becomes the new current version. This new version starts in exactly the same state as its
parent version – the previous current version.

We can *terminate* the current version, if it has a parent version. This parent version becomes
the new current version. (Note: Conchon and Filli\`atre (2008) does not discuss termination
explicitly, so we are deviating slightly here.)

Remark that versions form a linear path, not a tree. We would have a tree if we could
branch from any version, not just the current one, in particular we could have a version with
several children. This would correspond to a fully persistent implementation.

There is a *root version* that is the current version when the store is just created, and has
no parent version.

## 2.2 Backtracking store of references

Our backtracking data-structure is a *store* of *references*. We follow François Pottier’s design
for stores of references (modulo simplifications for presentation). A store is a set of references
and each references belongs to exactly one store.
## Usual store operations

```
type store
val new_store : unit -> store
```

```
type 'a rref
val make: store -> 'a -> 'a rref
val get: store -> 'a rref -> 'a
val set: store -> 'a rref -> 'a -> unit
```

The *state* of a (usual) store of references is just a mapping from each reference to a value of its content type; *get* and *set* operations modify the state as expected.

With our backtracking stores, a store has several versions, and the logical state of each version is exactly this mapping from each reference in the store to a value.

*make* adds a new reference to the store. Note that this operation is independent from the current version: the state of all versions of the store now has a mapping for this reference.

*get* and *set* operate on the current version of the store, as expected.

## Creating new versions

```
val branch : store -> unit
val terminate_nodiff : store -> unit
```

*branch* has the usual specification for a semi-persistent data structure: it creates a new version, child of the current version, which becomes the new current version, and initially has the same state as the previous current version.

We provide a *terminate_nodiff* function to terminate the current version; its parent version becomes the new parent version. For reasons that will become apparent in the next paragraph, this function assumes that the state of the current version is equal to the state of its parent. (It fails if the current version is the root version.)

## Transactions

```
val commit : store -> unit
val rollback : store -> unit
```

Those functions provide the necessary primitives to implement François Pottier's transactional interface on top of our backtracking store – and a bit more. They require the current version to have a parent version, and fail if the current version is the root version.

*commit* changes the state of the parent version to become identical to the state of the current version.

*rollback* changes the state of the current version to become identical to the state of the parent version.

Those operations do not terminate the current version, but one can call *terminate_nodiff* after them – it expects the current and parent version to be in the same state, which they both enforce.

Note: it would be natural to provide a higher-level interface that offers only *terminate_commit* and *terminate_rollback*, hiding the harder-to-use *terminate_nodiff* function.

**Performance** We expect a *fast path* behavior of *get* and *set* when no version has been branched (see below). In that case, *set* should write the content of the reference without any extra book-keeping, so that the performance is very close to standard references. Backtracking must be a *low-cost* abstraction, that only adds noticeable overhead when it is actually
used. (This fast path behavior is also present in the `StoreTransactionalRef` implementation of François Pottier, so it is important that we support it to subsume that implementation.)

# 3 Implementation(s)

Our references are implemented as record with a mutable field. (Our record-eliding implementation will get an extra metadata field, discussed in the relevant section.)

```typescript
type 'a rref = { mutable current: 'a; }
```

We maintain the invariant that the *global state* of a store, the content of the *current* field of each reference, is equal to the logical state of the current version of the store. This guarantees in particular that `get` can be implemented with a single read of a mutable field.

The general idea of our implementations is that the store maintains a journal of writes to its references, so that those writes can be rolled back when backtracking.

To undo a write/set, we need the reference that was written and the value of the reference before the write:

```typescript
type undo_action =
  | Set: 'a rref * 'a -> undo_action
```

Note that if we supported other types of backtracking mutable objects in the store, for example arrays, we could add more undo actions (for an array write we would store the array, the index and the old value at this index).

We went through three different implementations, from the less to the more sophisticated. They differ by the data-structure used to store undo actions, and whether we record an undo action for all writes or only some of them.

## 3.1 Stack of stacks

In our first implementation, the difference between a version and its parent version is stored as a stack of undo actions. Our versioned store is just a mutable list of such differences from the current version to the root version.

```typescript
type diff = undo_action Stack.t
type store = diff list ref
```

When the store is empty, the current version is the root version. The root version has no parent, so it does not store a diff. When the store is of the form `d::ds`, `d` is a diff from the current version to its parent, and `ds` a list of diffs from the parent version to the root version. In other words, a store keeps the whole journal of all writes, but segmented in separate stacks, one for each parent-child relationship between versions.

```typescript
let new_store () = ref []
let make (_s : store) (v : 'a) : 'a rref = { current = v; }
let get (_s : store) (x : 'a rref) : 'a = x.current
```

**Set** The specification of `set` says that it operates on the state of the current version of the store. In our representation, we maintain the invariant that the state of the current version is equal to the global state of the references, so `set` must update this global state. We also maintain the invariant that the store `diff` list relates the state of the current version to the state of the root version; the current version changes, so `set` must also update the *current* `diff`, the diff between the current version and its parent.