Curry and Howard Meet Borel

Melissa Antonelli, Ugo Dal Lago, Paolo Pistone

► To cite this version:

Melissa Antonelli, Ugo Dal Lago, Paolo Pistone. Curry and Howard Meet Borel. 2023. hal-03921649

HAL Id: hal-03921649

https://inria.hal.science/hal-03921649

Preprint submitted on 4 Jan 2023

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

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

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

Distributed under a Creative Commons Attribution 4.0 International License
Curry and Howard Meet Borel

Melissa Antonelli

University of Bologna, Italy

Ugo Dal Lago

University of Bologna, Italy

Paolo Pistone

University of Bologna, Italy

**Abstract**

We show that an intuitionistic version of counting propositional logic corresponds, in the sense of Curry and Howard, to an expressive type system for the probabilistic event $\lambda$-calculus, a vehicle calculus in which both call-by-name and call-by-value evaluation of discrete randomized functional programs can be simulated. Remarkably, proofs (respectively, types) do not only guarantee that validity (respectively, termination) holds, but also *reveal* the underlying probability. We finally show that by endowing the type system with an intersection operator, one obtains a system precisely capturing the probabilistic behavior of $\lambda$-terms.

# 1 Introduction

Among the many ways in which mathematical logic influenced programming language theory, the so-called Curry-Howard correspondence is certainly among the most intriguing and meaningful ones. Traditionally, the correspondence identified by Curry [13] and formalized by Howard [32] (CHC in the following) relates propositional intuitionistic logic and the simply-typed $\lambda$-calculus. As is well-known, though, this correspondence holds in other contexts, too. Indeed, in the last fifty years more sophisticated type systems have been put in relation with logical formalisms: from polymorphism [25, 26] to various forms of session typing [11, 52], from control operators [45] to dependent types [38, 50].

Nevertheless, there is a class of programming languages and type systems for which a correspondence in the style of the CHC has not yet been found. We are talking about languages with probabilistic effects, for which type-theoretic accounts have recently been put forward in various ways, e.g. type systems based on sized types [15], intersection types [9] or type systems in the style of so-called amortized analysis [56]. In all the aforementioned cases, a type system was built by modifying well-known type systems for deterministic languages *without* being guided by logic, and instead accepting inherently quantitative concepts directly from probability theory. So, one could naturally wonder if there is any logical system behind all this, or what kind of logic could possibly play the role of propositional logic in suggesting meaningful and expressive type systems for a $\lambda$-calculus endowed with probabilistic choice effects.

A tempting answer is to start from modal logic, which is known to correspond in the Curry-Howard sense to staged computation and to algebraic effects [12, 18, 60]. Nevertheless, there is one aspect of randomized computation that

modal logic fails to capture<fnref n="1" />, namely the *probability* of certain notable events, typically termination. Indeed, several other properties like reachability and safety can be reduced to the termination property (see, e.g., the discussion in [35]). In many of the probabilistic type systems mentioned above, for example, a term $t$ receives a type that captures the fact that $t$ has a certain probability $q$, perhaps strictly smaller than 1, of reducing to a value. This probability is an essential part of what we want to observe about the dynamics of $t$ and, as such, has to be captured by its type, at least if one wants the type system to be expressive.

Recently, the authors have proposed to use *counting quantifiers* [2, 3] as a means to express probabilities within a logical language. These quantifiers, unlike standard ones, determine not only *the existence* of an assignment of values to variables with certain characteristics, but rather count *how many* of those assignments exist. Recent works show that classical propositional logic enriched with counting quantifiers corresponds to Wagner’s hierarchy of counting complexity classes [55] (itself intimately linked to probabilistic complexity), and that Peano Arithmetics enriched with similar quantitative quantifiers yields a system capable of speaking of randomized computation in the same sense in which standard PA models deterministic computation [3]. One may now wonder whether all this scale to something like a proper CHC.

The aim of this work is precisely to give a positive answer to the aforementioned question, at the same time highlighting a few remarkable consequences of our study of probabilistic computation through the lens of logic. More specifically, the contributions of this paper are threefold:

* First of all, we introduce an intuitionistic version of Antonelli et al.'s counting propositional logic [2], together with a Kripke-style semantics based on the Borel $\sigma$-algebra of the Cantor space and a sound and complete proof-theory. Then, we identify a "computational fragment" of this logic and we design for it a natural deduction system in which proof normalization simulates well-known evaluation strategies for probabilistic programs. This is in Section 3.

* We then show that derivations can be decorated with terms of the *probabilistic event $\lambda$-calculus*, a $\lambda$-calculus for randomized computation introduced by Dal Lago et al. in [16]. This gives rise to a type-system called $C\lambda^{\{\}}$.

<footnote n="1">¹With a few notable exceptions, e.g. [23].</footnote>
Remarkably, the correspondence scales to the underlying dynamics, i.e. proof normalization relates to reduction in the probabilistic event $\lambda$-calculus. This is in Section 4 and Section 5.

* We complete the picture by giving an intersection type assignment system, derived from $C\lambda_{\frac{\{}}{}}$, and proving that it precisely captures the normalization probability of terms of the quoted $\lambda$-calculus. This is in Section 6.

Space limits prevent us from being comprehensive, meaning that many technical details will be unfortunately confined to the Appendix.

# 2 From Logic to Counting and Probability: a Roadmap

In this section we provide a first overview of our probabilistic CHC, at the same time sketching the route we will follow in the rest of the paper.

## 2.1 Randomized Programs and Counting Quantifiers

The first question we should ask ourselves concerns the kind of programs we are dealing with. What is a probabilistic functional program? Actually, it is a functional program with the additional ability of sampling from some distributions, or to proceed by performing some form of discrete probabilistic choice.<fnref n="2" /> This has a couple of crucial consequences: program evaluation becomes an essentially stochastic process, and programs satisfy a given specification *up to a certain probability*. As an example, consider the $\lambda$-term,

$$ \Xi_{\text{half}} := \lambda x. \lambda y. x \oplus y $$

where $\oplus$ is a binary infix operator for fair probabilistic choice. When applied to two arguments $t$ and $u$, the evaluation on $\Xi_{\text{half}}$ results in either $t$, with probability one half, or in $u$, again with probability one half.

But now, if we try to take $\Xi_{\text{half}}$ as a proof of some logical formula, we see that standard propositional logic is simply not rich enough to capture the behavior above. Indeed, given that $\Xi_{\text{half}}$ is a function of two arguments, it is natural to see it as a proof of an implication $A \to B \to C$, namely (following the BHK interpretation) as a function turning a proof of $A$ and a proof of $B$ into a proof of $C$. What is $C$, then? Should it be $A$ or should it be $B$? Actually, it could be both, with some degree of uncertainty, but propositional logic is *not* able to express all this. At this point, the recent work on *counting quantifiers* in propositional logic [2] comes to the rescue.

Another way to look at discrete probabilistic programs is as programs which are allowed to sample an element $\omega$ from the *Cantor space* $2^N$. For example, a probabilistic Turning machine $M$ can be described as a 2-tape machine where

the second tape is read-only and sampled from the Cantor space at each run. Similarly, the execution of $\Xi_{\text{half}}$ applied to programs $t$ and $u$ can be described as the result of sampling $\omega$ and returning either $t$ or $u$ depending on some read value, e.g. $\omega(0)$. Crucially, for each input $x$ and each possible output $y$ of a probabilistic program $f$, the set $S_{x,y}$ of elements in $2^N$, making $f(x)$ produce $y$, is a *Borel set*, so it makes sense to say that the probability that $f(x)$ yields $y$ coincides with the *measure* of $S_{x,y}$ (more on Borel sets and measures below).

Yet, what has all this to do with logic and counting? The fundamental observation is that formulas of classical propositional logic provide ways of denoting Borel sets. Let $x_0, x_1, \dots$ indicate a countable set of propositional variables (which can be seen as i.i.d. and uniformly distributed random variables $x_i \in \{0, 1\}$); each variable $x_i$ can be associated with the *cylinder set* (indeed, a Borel set of measure $1/2$) formed by all $\omega \in 2^N$ such that $\omega(i) = 1$ (i.e., in logical terms, such that $\omega \models x_i$). Then, any propositional formula $\mathcal{B}, \mathcal{c}, \dots$ formed by way of $\neg, \wedge, \vee$ can be associated with the Borel sets $\{\omega \in 2^N \mid \omega \models \mathcal{B}\}$ which can be constructed starting from cylinder sets by means of complementation, finite intersection and finite unions. In this way, for any Boolean formula $\mathcal{B}$, it makes sense to define *new formulas* like the formula $C^{1/2}\mathcal{B}$, which is true when the Borel set associated with $\mathcal{B}$ has measure greater than $1/2$ (i.e. when $\mathcal{B}$ is satisfied by *at least* $1/2$ of its models). For instance, for any two *distinct* indexes $i, j \in \mathbb{N}$ (so that the variables $x_i, x_j$ correspond to two independent events), the formula $C^{1/2}(x_i \vee x_j)$ is true, since the Borel set formed by the $\omega \in 2^N$ such that either $\omega(i) = 1$ or $\omega(j) = 1$ has measure greater than $1/2$ (equivalently, $x_i \vee x_j$ is satisfied by at least $1/2$ of its models). Instead, $C^{1/2}(x_i \wedge x_j)$ is false, since, $x_i$ and $x_j$ being independent, the Borel set associated with $x_i \wedge x_j$ has only measure $1/4$.

Counting propositional logic (from now on CPL) is defined by enriching classical propositional logic with counting quantifiers $C^q$, where $q \in (0, 1] \cap \mathbb{Q}$. Following our sketch, CPL admits a natural semantics in the Borel $\sigma$-algebra of the Cantor space, together with a sound and complete sequent calculus [2]. Notice that measuring a Boolean formula actually amounts at *counting* its models, that is, to a purely recursive operation, albeit one which needs not be doable in polynomial time (indeed, CPL is deeply related to Wagner's counting hierarchy [2]).

Going back to the term $\Xi_{\text{half}}$, what seems to be lacking in intuitionistic logic is a way to express that $C$ could be $C^{1/2}A$, that is, that it could be $A$ with probability at least $1/2$, and, similarly, that it could be by $C^{1/2}B$. In Section 3 we introduce an intuitionistic version of CPL, called iCPL, which enriches intuitionistic logic with Boolean variables as well as the counting quantifier $C^q$. Intuitively, if a proof of a formula $A$ can be seen as a deterministic program satisfying

<footnote n="2">²Here we are not at all concerned with sampling from continuous distributions, nor with capturing any form of conditioning.</footnote>
the specification A, a proof of CqA will correspond to a probabilistic program that satisfies the specification A with probability q. Our main result consists in showing that proofs in iCPL correspond to functional probabilistic programs and, most importantly, that normalization in this logic describes probabilistic evaluation.

## 2.2 Can CbN and CbV Evaluation Coexist?

When studying probabilistic extensions of the λ-calculus, two different evaluation strategies are generally considered: the *call-by-name* (CbN) strategy, which (possibly) duplicates choices before evaluating them, and the *call-by-value* (CbV) strategy, which instead evaluates choices before (possibly) duplicating their outcomes. Importantly, the probability of termination of a program might differ depending on the chosen strategy. For example, consider the application of the term $2 := \lambda yx.y(yx)$ (i.e. the second Church numeral) to $I \oplus \Omega$, where $I = \lambda x.x$ and $\Omega$ is the diverging term $(\lambda x.xx)\lambda x.xx$. Under CbN, the redex $2(I \oplus \Omega)$ first produces $\lambda x.(I \oplus \Omega)((I \oplus \Omega)x)$, then reduces to any of the terms $\lambda x.u(vx)$, with $u, v$ chosen from $\{I, \Omega\}$, each with probability $\frac{1}{4}$. Since $\lambda x.u(vx)$ converges only when $u = v = I$, the probability of convergence is thus $\frac{1}{4}$. Under CbV, in $2(I \oplus \Omega)$ one first has to evaluate $I \oplus \Omega$, and then passes the result to 2, hence returning either the converging term $I(Ix)$ or the diverging term $\Omega(\Omega x)$, each with probability $\frac{1}{2}$.

If we now try to think of the Church numeral 2 as a proof of some counting quantified formula, we see that, depending on the reduction strategy we have in mind, it must prove a different formula. Indeed, given that $I \oplus \Omega$ proves $C^1_2(A \to A)$, in the CbN case, 2 proves $C^1_2(A \to A) \to A \to C^1_4 A$, since only in one over four cases it yields a proof of A, while in the CbV case, 2 proves the formula $C^1_2(A \to A) \to A \to C^1_4 A$, as it yields a proof of A in one case over two.

In the literature on probabilistic λ-calculi, the apparent incompatibility of CbN and CbV evaluation is usually resolved by restricting to calculi with one or the other strategy. However, the observation above suggests that, if functional programs are typed using counting quantifiers, it should become possible to make the two evaluation strategies coexist, by assigning them different types.

Actually, a few recent approaches [14, 16, 19, 21] already suggest ways to make CbN and CbV evaluation live together. In particular, in the probabilistic event λ-calculus [16] the choice operator $\oplus$ is decomposed into two different operators, yielding a confluent calculus: a choice operator $t \oplus_a u$, depending on some probabilistic event $a \in \{0, 1\}$, and a probabilistic event generator va.t, which actually “flips the coin”. In this language, the CbN and CbV applications of 2 to $I \oplus \Omega$ are encoded by two distinct terms $2(\text{va.}I \oplus_a \Omega)$ and $\text{va.}2(I \oplus_a \Omega)$, crucially distinguishing between generating a probabilistic choice before or after a duplication takes place.

This calculus constitutes then an ideal candidate for our CHC. Indeed, as we'll see, the logical rules for the counting quantifier Cq naturally give rise to typing rules for the event generator va. In Section 4 we introduce a variant $\Lambda_{\text{PE}}^{\{\}}$ of the calculus from [16], with the underlying probability space $\{0, 1\}$ replaced by the Cantor space, and in Section 5 we introduce a type system $C\lambda_{\text{PE}}^{\{\}}$ for simple types with counting quantifiers, showing that natural deduction derivations translate into typing derivations in $C\lambda_{\text{PE}}^{\{\}}$, with normalization precisely corresponding to reduction in $\Lambda_{\text{PE}}^{\{\}}$.

## 2.3 Capturing Probability of Normalization via Types

As observed in the Introduction, a fundamental quantitative property we would like to observe using types is the probability of termination. Nevertheless, given that the reduction of $\Lambda_{\text{PE}}^{\{\}}$ is purely deterministic, what notions of probabilistic termination should we actually observe?

Rather than evaluating programs by implementing probabilistic choices, reduction in the probabilistic event λ-calculus has the effect of progressively generating the full tree of outcomes of (sequences of) probabilistic choices, giving rise to a distribution of values. Therefore, given a term t, rather than asking whether some or all reductions of t terminate, it makes sense to ask with what probability a normal form is found by generating all probabilistic outcomes of t.

In Section 6 we will first show that when the type Cqσ is assigned to a program t, the value $q \in \mathbb{Q} \cap (0, 1]$ provides a lower bound for the actual probability of finding a (head) normal form in the development of t. Then we show that, by extending the type system with an intersection operator, one can attain an upper bound and thus fully characterize the distribution of values associated with a term.

## 2.4 Preliminaries on the Cantor Space

Throughout the paper, we exploit some basic facts about the Cantor space, its Borel σ-algebra, and their connections with Boolean logic, that we briefly recall here.

We consider a countably infinite set $\mathcal{A}$ of names, noted $a, b, c, \dots$. For any finite subset $X \subseteq \mathcal{A}$, we let $\mathbf{B}_X$ (resp. $\mathbf{B}_{\mathcal{A}}$) indicate the Borel σ-algebra on the $X$-th product of the Cantor space $(2^{\mathcal{N}})^X$ (resp. on the $\mathcal{A}$-th product $(2^{\mathcal{N}})^{\mathcal{A}}$), that is, the smallest σ-algebra containing all open sets under the product topology. There exists a unique measure $\mu$ of $\mathbf{B}_{\mathcal{A}}$ such that $\mu(C_{a,i}) = \frac{1}{2}$ for all cylinders $C_{a,i} = \{\omega | \omega(a)(i) = 1\}$. The measure $\mu$ restricts to a measure $\mu_X$ on $\mathbf{B}_X$ by letting $\mu_X(S) = \mu(S \times (2^{\mathcal{N}})^{\mathcal{A}-X})$.

Boolean formulas with names in $\mathcal{A}$ are defined by:

$$ \mathfrak{b} ::= \top | \bot | x_a^i | \neg \mathfrak{b} | \mathfrak{b} \wedge \mathfrak{b} | \mathfrak{b} \vee \mathfrak{b} $$

where $a \in \mathcal{A}$ and $i \in \mathbb{N}$. We let $\text{FN}(\mathfrak{b}) \subseteq \mathcal{A}$ be the set of names occurring in $\mathfrak{b}$. For all Boolean formula $\mathfrak{b}$ and $X \supseteq \text{FN}(\mathfrak{b})$, we let $[\mathfrak{b}]_X$ indicate the Borel set $\{\omega \in (2^{\mathbb{N}})^X | \omega \models$
$\mathfrak{b}\}$ (in particular, $\llbracket x_a^i \rrbracket_{\{a\}} = \{\omega \mid \omega(a)(i) = 1\}$. The value $\mu_X(\llbracket \mathfrak{b} \rrbracket_X) \in [0, 1] \cap \mathbb{Q}$ is independent from the choice of $X \supseteq \text{FN}(\mathfrak{b})$, and we will note it simply as $\mu(\mathfrak{b})$.

### 3 Intuitionistic Counting Propositional Logic

In this section we introduce a constructive version of CPL, that we call iCPL, which extends standard intuitionistic logic with Boolean variables and counting quantifiers. The logic iCPL combines constructive reasoning (corresponding, under CHC, to functional programming) with semantic reasoning on Boolean formulas and their models (corresponding, as we have seen, to discrete probabilistic reasoning). The formulas of iCPL are *hybrid*. that is, comprise both a countable set $\mathcal{P} = \{p, q, \dots \}$ of intuitionistic propositional variables, and named Boolean propositional variables $x_a^i$. For example, consider the formula below:

$$A := p \rightarrow q \rightarrow (x_a^0 \land p) \lor (\neg x_a^0 \land q).$$

Intuitively, proving A amounts to showing that, whenever $p$ and $q$ hold, given that either $x_a^0$ or $\neg x_a^0$ holds, in the first case $p$ holds, and in the second case $q$ holds.

Suppose we test A against some element $\omega$ from the Cantor space. A way of proving A, in the “environment” $\omega$, could then be as follows: given assumptions $p$ and $q$, conclude $p$ and $x_a^0$ if $\omega(0) = 1$ (i.e. if $\omega$ satisfies $x_a^0$), and conclude $q$ and $\neg x_a^0$ if $\omega(0) = 0$ (i.e. if $\omega$ does not satisfy $\neg x_a^i$). In other words, a proof of A under $\omega$ could be something like $\lambda xy.x \oplus_a y$. Assuming that $\omega$ is uniformly sampled, what are the chances that our strategy will actually yield a proof of A? Well, there are two possible cases, and in both cases we get a proof of one of the disjuncts $x_a^0 \land p$ and $\neg x_a^0 \land q$, thus a proof of A. We thus obtain a proof of A with probability 1 or, in other words, a proof of $C_a^1 A$ (no more depending on any “environment”). As a term, this proof looks then precisely as the closed term $\text{va.}\lambda xy.x \oplus_a y$.

Consider now another formula:

$$B := p \rightarrow q \rightarrow x_a^0 \land p.$$

Given some $\omega$, a proof B should conclude, from assumptions $p$ and $q$, both $p$ and $x_a^0$ when $\omega(0) = 1$, but when $\omega(0) = 0$, it needs not conclude anything, since we have nothing to prove in this case. A proof of B should then be something like $\lambda xy.x \oplus_a \lambda \neg x_a^i$, where $\lambda \neg x_a^i$ can be any program. By uniformly sampling $\omega$, we get then a proof of B only in one half of the cases, i.e. we get a proof of $C_a^1 B$.

#### 3.1 The Semantics and Proof-Theory of iCPL

The formulas of the logic just sketched are defined by:

$$A ::= \top \mid \bot \mid x_a^i \mid p \mid A \land A \mid A \lor A \mid A \rightarrow A \mid C_a^q A$$

where $p \in \mathcal{P}$ and $q \in (0, 1] \cap \mathbb{Q}$. A natural semantics for iCPL-formulas can be given in terms of Kripke-like structures:

**Definition 3.1.** An iCPL-structure is a triple $\mathcal{M} = (W, \leq, i)$ where $W$ is a countable set, $\leq$ is a preorder on $W$, and $i: \mathcal{P} \to W^\uparrow$, where $W^\uparrow$ is the set of upper subsets of $W$.

The interpretation of formulas in iCPL-structures combines a set $W$ of worlds (for the interpretation of intuitionistic propositional variables) with the choice of an element of the Cantor space (for the interpretation of Boolean variables): for any iCPL-structure $\mathcal{M} = (W, \leq, i)$ and finite set $X$, we define the relation $w, \omega \Vdash_X A$ (where $w \in W$, $\omega \in (2^N)^X$ and $\text{FN}(A) \subseteq X$) by induction as follows:

* $w, \omega \Vdash_X \bot$ and $w, \omega \Vdash_X \top$;

* $w, \omega \Vdash_X x_a^i$ iff $\omega(a)(i) = 1$;

* $w, \omega \Vdash_X p$ iff $w \in i(p)$;

* $w, \omega \Vdash_X A \land B$ iff $w, \omega \Vdash_X A$ and $w, \omega \Vdash_X B$;

* $w, \omega \Vdash_X A \lor B$ iff $w, \omega \Vdash_X A$ or $w, \omega \Vdash_X B$;

* $w, \omega \Vdash_X A \rightarrow B$ iff for all $w' \geq w$, $w', \omega \Vdash_X A$ implies $w', \omega \Vdash_X B$;

* $w, \omega \Vdash_X C_a^q A$ iff $\mu(\{\omega' \in 2^N \mid w, \omega + \omega' \Vdash_{\mathcal{M}}^{X \cup \{a\}} A\}) \geq q$, where $\omega + \omega' \in (2^N)^{X \cup \{a\}}$ is given by $(\omega + \omega')(b)(n) = \omega(b)(n)$, for $b \in X$, and $(\omega + \omega')(a)(n) = \omega'(n)$.

Using properties of the Borel $\sigma$-algebra $B_X$, it can be shown that for any $w \in W$ and formula $A$, the set $\{\omega \in (2^N)^X \mid w, \omega \Vdash_X A\}$ is a Borel set, and thus measurable. We write $\Gamma \Vdash_X A$ when for all $w \in W$ and $\omega \in (2^N)^X$, whenever $w, \omega \Vdash_X \Gamma$ holds, also $w, \omega \Vdash_X A$ holds. We write $\Gamma \vdash A$ when for any iCPL-structure $\mathcal{M}$ and $X \supseteq \text{FN}(A)$, $\Gamma \Vdash_X A$ holds.

A sound and complete proof system for iCPL can be defined. Indeed, starting from usual natural deduction for intuitionistic logic, one obtains a calculus $\text{ND}_{i\text{CPL}}$ for iCPL by adding the excluded middle $x_a^i \lor \neg x_a^i$ as an axiom for Boolean variables, as well as suitable rules and axioms for counting quantifiers (details can be found in App. A.1).

**Theorem 3.2.** $\Gamma \vdash A$ iff $\Gamma \vdash_{\text{ND}_{i\text{CPL}}} A$.

For example, $C^q$ admits an introduction rule as below

$$\frac{\Gamma, d \vdash A \quad \mu(d) \geq q}{\Gamma \vdash C_a^q A} \qquad (\text{CI})$$

with the proviso that $a$ does not occur in $\Gamma$, and is the only name occurring in $d$. Intuitively, this rule says that if we can prove $A$ under assumptions $\Gamma$ and $d$, and if a randomly chosen valuation of $a$ has chance $q$ of being a model of $d$, then we can build a proof of $C_a^q A$ from $\Gamma$. Observe that the rule (CI) has a semantic premise $\mu(d) \geq q$: we ask to an oracle to count the models of $d$ for us (this is similar to what happens in sequent calculi for CPL, see [2]).

### 3.2 The Computational Fragment of iCPL

From the perspective of the CHC, however, the natural deduction system just sketched is not what we are looking for. As iCPL contains Boolean logic, in order to relate proofs and
programs, one should first choose among the several existing constructive interpretations of classical logic. Yet, in our previous examples Boolean formulas were never those to be proved; rather, they were used as semantic constraints that programs may or may not satisfy (for example, when saying that a program, depending on some event $\omega$, yields a proof of A when $\omega$ satisfies $\mathfrak{b}$, or that a program has $q$ chances of yielding a proof of A when $\mathfrak{b}$ has measure at least $q$).

Would it be possible, then, to somehow separate purely constructive reasoning from Boolean semantic reasoning within formulas and proofs of iCPL? The following lemma suggests that this is indeed possible.

**Lemma 3.3 (Decomposition Lemma).** For any formula A of iCPL there exist Boolean formulas $\mathfrak{b}_v$ and purely intuitionistic formulas $A_v$ (i.e. formulas containing no Boolean variables), where $v$ varies over all possible valuations of the Boolean variables in A, such that

$$ \vdash A \leftrightarrow \bigvee_v \mathfrak{b}_v \wedge A_v $$

*Proof sketch.* The idea is to let $\mathfrak{b}_v$ be the formula characterizing $v$, i.e. the conjunction of all variables true in $v$ and of all negations of variables false in $v$, and let $A_v$ be obtained from A by replacing each Boolean variable by either $\top$ or $\bot$, depending on its value under $v$. □

By Lemma 3.3, any sequent $\Gamma \vdash A$ of iCPL can be associated with a family of intuitionistic sequents of the form $\Gamma_v, \mathfrak{b}_v \vdash A_v$ where $v$ ranges over all valuations of the Boolean variables of $\Gamma$ and $A$, and $\Gamma_v, \mathfrak{b}_v, A_v$ are as in Lemma 3.3. We will note such special sequents as $\Gamma_v \vdash \mathfrak{b}_v \vdash A_v$, in order to highlight the special role played by the Boolean formula $\mathfrak{b}_v$.

The sequents $\Gamma \vdash \mathfrak{b} \rightarrow A$ have a natural computational interpretation: they express program specifications of the form “$\Pi$ yields a proof of A from $\Gamma$ whenever its sampled function satisfies $\mathfrak{b}$”. By the way, Lemma 3.3, ensures that, modulo Boolean reasoning, logical arguments in iCPL can be reduced to (families of) arguments of this kind.

Let then $iCPL_0$ be the fragment formed by the purely intuitionistic formulas of iCPL, which are defined by:

$$ A ::= p \mid A \rightarrow A \mid C^q A $$

where $q \in (0, 1] \cap \mathbb{Q}$. For simplicity, and since this is enough for the CHC, we take here implication as the only connective, yet all other propositional connectives could be added. As formulas do not contain Boolean variables, counting quantifiers in $iCPL_0$ are not named. We use $C^{q_1 * \cdots * q_n} A$ (or even $C^{\vec{q}}$, for simplicity) as an abbreviation for $C^{q_1} \dots C^{q_n} A$.

The natural deduction system $ND_{iCPL_0}$ for iCPL$_0$ is defined by the rules illustrated in Fig. 1 (where in (CI) it is assumed that $\mathrm{FN}(\mathfrak{b}) \cap \mathrm{FN}(d) = \emptyset$). A few rules involve semantic premises of the forms $\mathfrak{b} \vdash c$ and $\mu(\mathfrak{b}) \geq q$. Beyond standard intuitionistic rules, $ND_{iCPL_0}$ comprises structural rules

$$ \begin{array}{c} \text{Identity Rule} \\ \Gamma, A \vdash \mathfrak{b} \rightarrow A \quad (\mathrm{id}) \end{array} $$

Structural Rules

$$ \frac{\mathfrak{b} \vdash \bot}{\Gamma \vdash \mathfrak{b} \rightarrow A} (\bot) $$

$$ \frac{\Gamma \vdash c \rightarrow A \qquad \Gamma \vdash d \rightarrow A \qquad \mathfrak{b} \vdash (c \wedge x_a^i) \lor (d \wedge \neg x_a^i)}{\Gamma \vdash \mathfrak{b} \rightarrow A} \quad (\mathrm{m}) $$

Logical Rules

$$ \frac{\Gamma, A \vdash \mathfrak{b} \rightarrow B}{\Gamma \vdash \mathfrak{b} \rightarrow (A \rightarrow B)} (\rightarrow I) $$

$$ \frac{\Gamma \vdash \mathfrak{b} \rightarrow (A \rightarrow B) \qquad \Gamma \vdash \mathfrak{b} \rightarrow A}{\Gamma \vdash \mathfrak{b} \rightarrow B} (\rightarrow E) $$

Counting Rules

$$ \frac{\Gamma \vdash \mathfrak{b} \wedge d \rightarrow A \qquad \mu(d) \geq q}{\Gamma \vdash \mathfrak{b} \rightarrow C^q A} \quad (\mathrm{CI}) $$

$$ \frac{\Gamma \vdash \mathfrak{b} \rightarrow C^q A \qquad \Gamma, A \vdash \mathfrak{b} \rightarrow B}{\Gamma \vdash \mathfrak{b} \rightarrow C^{qs} B} \quad (\mathrm{CE}) $$

<caption>**Figure 1.** Rules of $ND_{iCPL_0}$.</caption>

to manipulate Boolean formulas, and introduction and elimination rules for the counting quantifier. The rule ($\bot$) yields dummy proofs of any formula, i.e. proofs which are correct for no possible event; the rule (m) combines two proofs $\Pi_1, \Pi_2$ of the same formula into one single proof $\Pi'$, with the choice depending on the value of some Boolean variable $x_a^i$ ($\Pi'$ is thus something like $\Pi_1 \oplus_a \Pi_2$). The introduction rule for $C^q$ is similar to rule (CI). It is explained as follows: if $\Pi$, in the “environment” $\omega + \omega' \in (2^N)^{X \cup \{a\}} \simeq (2^N)^X \times 2^N$, yields a proof of A whenever $\omega + \omega'$ satisfies the two independent constraints $\mathfrak{b}$ and $d$ (i.e. $\omega \vdash \mathfrak{b}$ and $\omega' \vdash d$), then by randomly choosing $\omega' \in 2^N$, we have at least $q \ge \mu(d)$ chances of getting a proof of A ($\Pi'$ is thus something like $\mathrm{va.}\Pi$). Finally, the elimination rule (CE) essentially turns a proof of $A \rightarrow B$ into a proof of $C^q A \rightarrow C^{qs} B$. As we’ll see, this rule captures $\mathrm{CbV}$ function application.

**Example 3.4.** Fig. 2a illustrates a proof $\Pi_{1/2}^\top$ of $C^{1/2}(A \rightarrow A)$ obtained by first “mixing” an exact proof of $A \rightarrow A$ with a dummy one, and then introducing the counting quantifier. Fig. 2b illustrates a derivation of $C^q(A \rightarrow A) \rightarrow A \rightarrow C^{q*q}B$.

A precise connection between the proof systems for iCPL and $iCPL_0$ is discussed in Appendix A.2.

### 3.3 Normalization in iCPL$_0$

From the CHC perspective, natural deduction proofs correspond to programs, and normalization corresponds to execution. Let us look at normalization in $iCPL_0$, then.
$$
\Pi_{\oplus id} = \frac{\frac{A \vdash x_a^i \to A}{\vdash x_a^i \to (A \to A)} (\to I)}{\frac{\vdash \perp \to (A \to A)}{\vdash x_a^i \to (A \to A)}} (\perp) \frac{x_a^i \vdash (x_a^i \wedge x_b^i) \lor (\neg x_a^i \wedge \perp)}{\vdash x_a^i \to (A \to A)} (m) \frac{\mu(x_a^i) \ge \frac{1}{2}}{\vdash C^{\frac{1}{2}}(A \to A)} (\text{CI})}
\quad (a)
$$

$$
\Pi = \frac{\frac{C^q(A \to A), A \vdash C^q(A \to A)}{C^q(A \to A), A \vdash C^q A} \frac{A \to A, A \vdash A \to A}{A \to A, A \vdash A} \frac{A \to A, A \vdash A}{(CE)}}{(\to E)} \frac{\frac{C^q(A \to A), A, A \vdash C^q(A \to A)}{C^q(A \to A), A, A \vdash C^q A} \frac{A \to A, A, A \vdash A \to A}{A \to A, A, A \vdash A}}{(\to E)}
$$

<caption>Figure 2. Examples of derivations in $ND_{iCPL_0}$.</caption>

The two main normalization steps are ($\to I/\to E$) and (CI/CE).
The cuts ($\to I/\to E$) are eliminated, as usual, by means of the
admissible substitution rule

$$
\frac{\Gamma \vdash \mathbf{b} \to A}{\Gamma \vdash \mathbf{b} \to B} \quad \text{(subst)}
$$

The normalization step (CI/CE), illustrated in Fig. 3, also applies the rule (subst) to the premiss of (CI) and the minor premiss of (CE), and permutes the rule (CI) downwards. For example, if we cut the proof Π from Fig. 2b with Π<sub>1/2</sub><sub>id</sub> from Fig. 2a (by letting q = 1/2), normalization duplicates Π, that is, it duplicates the choice between the correct and the dummy proof of A → A, yielding a normal proof of A → C<sup>1/2</sup><sub>2</sub>\*<sup>1/2</sup><sub>2</sub>A. The other normalization steps (illustrated in App. A.5) permute (m) with other rules, and correspond to the *permuting reductions* for the probabilistic λ-calculus introduced in the next section. To make the study of normalization as simple as possible, we did not consider a “multiplication rule” to pass from C<sup>q</sup>A to C<sup>q</sup>A, as this would introduce other normalization steps. Nevertheless, in App. A.6 we study an alternative “CbN” proof-system ND<sub>iCPL<sub>0</sub></sub> also comprising this rule. As a by-product of the CHC developed in the following sections, we will obtain a strong normalization theorem for iCPL<sub>0</sub> (Corollary 5.5).

In Section 5 it will be shown (Prop. 5.4) that, once proofs
in $ND_{iCPL_0}$ are seen as probabilistic programs, the two nor-
malization steps ($\to I/\to E$) and (CI/CE) simulate CbN and
CbV evaluation, respectively.

**4 The Probabilistic Event Lambda Calculus**

In this section we introduce the computational side of the
CHC, that is, a variant of the probabilistic event λ-calculus
Λ<sub>PE</sub> from [16], with choices depending on events from the
Cantor space. We will then discuss how terms of Λ<sub>PE</sub> yield
distributions of values, and we define two notions of prob-
abilistic normalization for such distributions. We finally in-
troduce a further variant Λ<sub>PE</sub>{ of Λ<sub>PE</sub> which provides a smoother
representation of CbV functions.

4.1 A λ-Calculus Sampling from the Cantor Space

The terms of $\Lambda_{\text{PE}}$ are defined by the grammar below:

$$
t ::= x \mid \lambda x.t \mid tt \mid t \oplus_a^i u \mid va.t
$$

with $a \in \mathcal{A}$, and $i \in \mathbb{N}$. The intuition is that $va$ samples some function $\omega$ from the Cantor space, and $t \oplus_a^i u$ yields either $t$ or $u$ depending on the value $\omega(a)(i) \in \{0, 1\}$. In the following we let $t \oplus^i u$ be an abbreviation for $va.t \oplus_a^i u$ (supposing $a$ does not occur free in either $t$ or $u$). For any term $t$, finite set $X$ and $\omega \in (2^\mathbb{N})^X$, let $\pi_X^\omega(t)$, the “application of $\omega$ to $t$ through $X$”, be defined as:

$$
\begin{align*}
\pi_X^\omega(x) &= x \\
\pi_X^\omega(\lambda x.t) &= \lambda x.\pi_X^\omega(t) \\
\pi_X^\omega(tu) &= \pi_X^\omega(t)\pi_X^\omega(u) \\
\pi_X^\omega(t \oplus_a^i u) &= \begin{cases} \pi_X^\omega(t) & \text{if } a \in X \text{ and } \omega(a)(i) = 1 \\ \pi_X^\omega(u) & \text{if } a \in X \text{ and } \omega(a)(i) = 0 \\ \pi_X^\omega(t) \oplus_a^i \pi_X^\omega(u) & \text{otherwise} \end{cases} \\
\pi_X^\omega(vb.t) &= vb.\pi_X^\omega(t)
\end{align*}
$$

In usual randomized λ-calculi, program execution is de-
fined so as to be inherently probabilistic: for example a term
$t \oplus u$ can reduce to either $t$ or $u$, with probability $\frac{1}{2}$. In this
way, chains of reduction can be described as *stochastic Mark-
ovian sequences* [47], leading to formalize the idea of *nor-
malization with probability* $r \in [0, 1]$ (see [8]).

By contrast, reduction in Λ<sub>PE</sub> is fully deterministic: be-
yond the usual (and un-resticted) β-rule (λx.t)u →<sub>β</sub> t[u/x],
it comprises a *permutative reduction* t →<sub>p</sub> u defined by the
rules in Fig. 4 (where (a, i) < (b, j) if either vb occurs in the
scope of va, or a = b and i < j). Intuitively, permutative
reductions implement probabilistic choices by computing
the full tree of possible choices. For example, given terms
t<sub>1</sub>, t<sub>2</sub>, u<sub>1</sub>, u<sub>2</sub>, one can see that the term va.(t<sub>1</sub> ⊕<sub>a</sub><sup>0</sup> t<sub>2</sub>)(u<sub>1</sub> ⊕<sub>a</sub><sup>1</sup> u<sub>2</sub>)
reduces to va.(t<sub>1</sub>u<sub>1</sub>⊕<sub>a</sub><sup>1</sup>t<sub>1</sub>u<sub>2</sub>)⊕<sub>a</sub><sup>0</sup>(t<sub>2</sub>u<sub>1</sub>⊕<sub>a</sub><sup>1</sup>t<sub>2</sub>u<sub>2</sub>), hence displaying
all possible alternatives.

The fundamental properties of Λ<sub>PE</sub> are the following:

**Theorem 4.1** ([16]). $\dashv_p$ is confluent and strongly normalizing. Full reduction $\to := \dashv_p \cup \dashv_p$ is confluent.
$$ \frac{\Sigma \quad \mu(d) \ge q}{\frac{\Gamma \vdash \mathfrak{b} \wedge d \to A}{\Gamma \vdash \mathfrak{b} \to C^q A}} \quad \text{(CI)} \qquad \frac{\Pi}{\Gamma, A \vdash \mathfrak{b} \to B} \quad \text{(CE)} $$

$$ \sim \quad \frac{\Sigma \quad \Pi[\mathfrak{b} \mapsto \mathfrak{b} \wedge d] \quad \text{(subst)}}{\frac{\Gamma \vdash \mathfrak{b} \wedge d \to A}{\Gamma \vdash \mathfrak{b} \to B}} \quad \mu(d) \ge q_s \quad \text{(CI)} $$

<caption>Figure 3. Normalization step (CI)/(CE) of ND<sub>iCPL<sub>0</sub></sub>.</caption>

$$ \begin{align} & t \oplus_a^i t \to_p t \tag{i} \\ & (t \oplus_a^i u) \oplus_a^i v \to_p t \oplus_a^i v \tag{c1} \\ & t \oplus_a^i (u \oplus_a^i v) \to_p t \oplus_a^i v \tag{c2} \\ & \lambda x.(t \oplus_a^i u) \to_p (\lambda x.t) \oplus_a^i (\lambda x.u) \tag{⊕λ} \\ & (t \oplus_a^i u)v \to_p (tu) \oplus_a^i (uv) \tag{⊕f} \\ & t(u \oplus_a^i v) \to_p (tu) \oplus_a^i (tv) \tag{⊕a} \\ & (t \oplus_a^i u) \oplus_b^j v \to_p (t \oplus_b^j v) \oplus_a^i (u \oplus_b^j v) \tag{(a, i) < (b, j)} \quad (⊕⊕_1) \\ & t \oplus_b^j (u \oplus_a^i v) \to_p (t \oplus_b^j u) \oplus_a^i (t \oplus_b^j v) \tag{(a, i) < (b, j)} \quad (⊕⊕_2) \\ & vb.(t \oplus_a^i u) \to_p (vb.t) \oplus_a^i (vb.u) \tag{a ≠ b} \quad (⊕v) \\ & va.t \to_p t \tag{a ∉ FN(t))} \quad (¬v) \\ & \lambda x.va.t \to_p va.\lambda x.t \tag{vλ} \\ & (va.t)u \to_p va.(tu) \tag{vf} \end{align} $$

<caption>Figure 4. Permutative reductions.</caption>

The existence and unicity of normal forms for $\to_p$ (that we call *permutative normal forms*, PNFs for short) naturally raises the question of what these normal forms represent.

Let $\mathcal{T}$ indicate the set of PNFs containing no free name occurrence. For any $t \in \mathcal{T}$, the PNF of $t$ can be of two forms: either $t$ starts with a generator, i.e. $t = va.t'$, and $t'$ is a tree of $a$-labeled choices $\oplus_a^i$ whose leaves form a finite set of $\mathcal{T}$ (the *support* of $t'$, $\text{supp}(t)$). Otherwise, $t$ is of the form $\lambda x_1 \dots \lambda x_n.t' t_1 \dots t_p$, where $t'$ is either a variable or a $\lambda$. We call these last terms *pseudo-values*, and we let $\mathcal{V} \subseteq \mathcal{T}$ indicate the set formed by them.

Using this decomposition, any $t \in \mathcal{T}$ can be associated in a unique way with a *(sub-)*distribution of pseudo-values $\mathcal{D}_t: \mathcal{V} \to [0, 1]$ by letting $\mathcal{D}_t(v) = \delta_t$ when $t \in \mathcal{V}$, and

$$ \mathcal{D}_t(v) = \sum_{u \in \text{supp}(t')} \mathcal{D}_u(v) \cdot \mu(\{\omega \in 2^\mathbb{N} \mid \pi_{\{a\}}^{\omega}(t') = u\}) $$

if $t = va.t'$. Intuitively, $\mathcal{D}_t(v)$ measures the probability of finding $v$ by iteratively applying to $t$ random choices of events from the Cantor space any time a $v$ is found.

## 4.2 Probabilistic (Head) Normalization.

Given a term $t \in \mathcal{T}$, the questions “is $t$ in normal form?” and “does $t$ reduce to a normal form?” have univocal yes/no answers, because $\to$ is deterministic. However, if we think of $t$ rather as $\mathcal{D}_t$, the relevant questions become “with what probability is $t$ in normal form?” and “with what probability does $t$ reduce to normal form?”.

To answer this kind of questions we will introduce functions HNV<sub>→</sub>($t$), NF<sub>→</sub>($t$) measuring the probability that $t$ reduces to a normal form.

Let us consider head-normal forms, first. A head-reduction $t \to_h u$ is either a $\to_p$-reduction or a $\to_\beta$-reduction of the form $R[\lambda\tilde{x}.(\lambda y.t)u_1 \dots u_n] \to_\beta R[\lambda\tilde{x}.t[u/x]u_1 \dots u_n]$, where R is a *randomized context*, defined by the grammar

$$ R[\quad] ::= \quad | R[\quad] \oplus_a^i u | t \oplus_a^i R[\quad] | va.R[\quad]. $$

A head normal value (in short, HNV) is a $\to_h$-normal term which is also a pseudo-value, i.e. it is of the form $\lambda\tilde{x}.yu_1 \dots u_n$. We let HNV indicate the set of such terms.

**Definition 4.2.** For any $t \in \mathcal{T}$, HNV($t$) := $\sum_{v \in \text{HNV}} \mathcal{D}_t(v)$ and HNV<sub>→</sub>($t$) := $\sup\{\text{HNV}(u) \mid t \to_h^* u\}$. When HNV<sub>→</sub>($t$) $\ge$ $q$, we say that $t$ yields a HNV with probability at least $q$.

For example, if $t = va.(\lambda x.\lambda y.(y \oplus_a^I I)x)u$, where $u = I \oplus^j \Omega$, then HNV<sub>→</sub>($t$) = $\frac{3}{4}$. Indeed, we have

$$ t \to_h^* va.(\lambda y.y(vb.I \oplus_b^j \Omega)) \oplus_a^i (vb'.I \oplus_{b'}^j \Omega) $$

and three over the four possible choices (corresponding to choosing between either left or right for both $va$ and $vb'$) yield a HNV. Observe that the choice about $vb$ does not matter, since $\lambda y.yu$ is already a HNV.

Let us now consider normal forms. The first idea might be to define a similar function NF($t$) = $\sum_{v \in \text{normal form}} \mathcal{D}_t(v)$. However, with this definition a term like $t = \lambda x.x(\text{va.I}\oplus_a^0 \Omega)$ would have probability 0 of yielding a normal form. Instead, our guiding intuition here is that $t$ should yield a normal form with probability $\frac{1}{2}$, i.e. depending on a choice for $a$. This leads to the following definition:

**Definition 4.3.** For any $t \in \mathcal{T}$, NF($t$) is defined by:

* if $t = \lambda\tilde{x}.yu_1 \dots u_n \in \text{HNV}$, then NF($t$) := $\prod_{i=1}^n$ NF($u_i$);

* otherwise NF($t$) := $\sum_{u \in \text{HNV}}$ NF($u$) $\cdot \mathcal{D}_t(u)$.

We let NF<sub>→</sub>($t$) = $\sup\{\text{NF}(u) \mid t \to^* u\}$ and, if NF<sub>→</sub>($t$) $\ge$ $q$, we say that $t$ yields a normal form with probability at least $q$.

For example, for the term $t$ considered above, NF<sub>→</sub>($t$) = $\frac{4}{8} = \frac{1}{2}$: four over the eight possible choices for $va$, $vb$ and $vb'$ yield a normal form (i.e. either choose left for $va$ and $vb$ and choose anything for $vb'$, or choose right for $va$, left for $vb'$, and choose anything for $vb$).

## 4.3 Extending $\Lambda_{\text{PE}}$ with CbV Functions

$\Lambda_{\text{PE}}$ makes it possible to encode a CbV redex like $va.2(I \oplus_a^0 \Omega)$, as we have seen. However, in view of the functional interpretation of iCPL<sub>0</sub>, it would be convenient also to be able
to represent the CbV functions mapping $va.(u \oplus_a v)$ onto $va.2(u \oplus_a^0 v)$. A simple way to do this is by enriching the language of $\Lambda_{\text{PE}}$ with a “CbV application” operator $\{t\}u$, with suitable permutative rules. Let $\Lambda_{\text{PE}}^{\{\}}$ indicate this extension of terms of $\Lambda_{\text{PE}}$ with $\{\}$. While $\beta$-reduction for $\Lambda_{\text{PE}}^{\{\}}$ is the same as for $\Lambda_{\text{PE}}$, permutative reduction $\to_{p\{\}}$ is defined by all rules in Fig. 4 except for $(\neg v)$, together with the three permutations below

$$ \{t\}va.u \to_{p\{\}} va.tu \quad (\{\}\upsilon) $$

$$ \{t \oplus_a^i u\}v \to_{p\{\}} \{t\}v \oplus_a^i \{t\}v \quad (\{\}\oplus_1) $$

$$ \{t\}(u \oplus_a^i v) \to_{p\{\}} \{t\}u \oplus_a^i \{t\}v \quad (\{\}\oplus_2) $$

For instance, a CbV Church numeral can be encoded in $\Lambda_{\text{PE}}^{\{\}}$ as $2^{\text{CbV}} := \lambda f.\{2\}f$, since one has $2^{\text{CbV}}(va.u \oplus_a^i v) \to_{\beta} \{2\}va.u \oplus_a^i v \to_{p\{\}} va.2(u \oplus_a^i v)$.

The fundamental properties of $\Lambda_{\text{PE}}$ extend to $\Lambda_{\text{PE}}^{\{\}}$:

**Proposition 4.4.** $\to_{p\{\}}$ is confluent and strongly normalizing. Full reduction $\to_{\{\}} := \to_{\beta} \cup \to_{p\{\}}$ is confluent.

In the Appendix B it is shown how the definitions of $\mathcal{D}_t$ and $\text{HNV}_{\to}(t)$ extend to terms of $\Lambda_{\text{PE}}^{\{\}}$.

# 5 The Correspondence, Statically and Dynamically

In this section we present the core of the CHC. First, we introduce two type systems $C\lambda_{\to}$ and $C\lambda_{\to}^{\{\}}$ for $\Lambda_{\text{PE}}$ and $\Lambda_{\text{PE}}^{\{\}}$, respectively, which extend the simply typed $\lambda$-calculus with counting quantifiers. Then, we show that each proof $\Pi$ in $iCPL_0$ can be associated with a typing derivation in $C\lambda_{\to}^{\{\}}$ of some probabilistic term $t^{\Pi}$, in such a way that normalization of $\Pi$ corresponds to reduction of $t^{\Pi}$. Observe that translating the rule (CE) requires the CbV application operator $\{\}$. In the Appendix A.6 we show that an alternative “CbN” proof-system for $iCPL_0$ can be translated without $\{\}$, and thus into $C\lambda_{\to}$.

## 5.1 Two Type Systems with Counting Quantifiers

Both type systems $C\lambda_{\to}$ and $C\lambda_{\to}^{\{\}}$ extend the simply typed $\lambda$-calculus with counting quantifiers, but in a slightly different way: in $C\lambda_{\to}$ types are of the form $C^q s$, i.e. prefixed by exactly one counting quantifier, while in $C\lambda_{\to}^{\{\}}$ types are of the form $C^{\tilde{q}} s$, i.e. prefixed by a (possibly empty) list of counting quantifiers.

More precisely, the types (denoted $s, t$) of $C\lambda_{\to}$ and $C\lambda_{\to}^{\{\}}$ are generated by the grammars below:

$$ s ::= C^q \sigma \qquad \sigma ::= o \mid s \Rightarrow \sigma \qquad (C\lambda_{\to}) $$

$$ s ::= C^{\tilde{q}} \sigma \qquad \sigma ::= o \mid s \Rightarrow \sigma \qquad (C\lambda_{\to}^{\{\}}) $$

where, in both cases, the $qs$ are chosen in $(0, 1] \cap \mathbb{Q}$.

**Identity rule:**

$$ \frac{\text{FN}(\beta) \subseteq X}{\Gamma, x : s \vdash^X x : \beta \to \beta} \quad \text{(id)} $$

**Structural rule:**

$$ \frac{\{\Gamma \vdash^X t : \beta_i \to s\}_{i=1,\dots,n} \quad \beta \vdash^X \bigvee_i \beta_i}{\Gamma \vdash^X t : \beta \to s} \quad (\vee) $$

**Plus rule:**

$$ \frac{\Gamma \vdash^{X \cup \{a\}} t : c \to s \qquad \Gamma \vdash^{X \cup \{a\}} u : d \to s \qquad \beta \vdash (x_a^i \wedge c) \vee (\neg x_a^i \wedge d)}{\Gamma \vdash^{X \cup \{a\}} t \oplus_a^i u : \beta \to s} \quad (\oplus) $$

**Arrow rules:**

$$ \frac{\Gamma, x : s \vdash^X t : \beta \to C^{\tilde{q}} \tau}{\Gamma \vdash^X \lambda x.t : \beta \to C^{\tilde{q}}(s \Rightarrow \tau)} \quad (\lambda) $$

$$ \frac{\Gamma \vdash^X t : c \to C^{\tilde{q}}(s \Rightarrow \tau) \qquad \Gamma \vdash^X u : d \to s \qquad \beta \vdash^X c \wedge d}{\Gamma \vdash^X tu : \beta \to C^{\tilde{q}} \tau} \quad (\@) $$

$$ \frac{\Gamma \vdash^X t : c \to C^{\tilde{q}}(s \Rightarrow \tau) \qquad \Gamma \vdash^X u : d \to C^r s \qquad \beta \vdash^X c \wedge d}{\Gamma \vdash^X \{t\}u : \beta \to C^r s C^{\tilde{q}} \tau} \quad (\{\}) $$

**Counting rule:**

$$ \frac{\Gamma \vdash^{X \cup \{a\}} t : \beta \wedge d \to s \qquad \mu(d) \geq q}{\Gamma \vdash^X va.t : \beta \to C^q s} \quad (\mu) $$

<caption>**Figure 5.** Typing rules of $C\lambda_{\to}^{\{\}}$.</caption>

Judgements in both systems are of the form $\Gamma \vdash^X t : \beta \to s$, where $\Gamma$ is a set of type declarations $x_i : s_i$ of pairwise distinct variables, $t$ is a term of $\Lambda_{\text{PE}}$ (resp. of $\Lambda_{\text{PE}}^{\{\}}$), $\beta$ a Boolean formula, and $X$ a finite set of names with $\text{FN}(t)$, $\text{FN}(\beta) \subseteq X$. The intuitive reading of $\Gamma \vdash^X t : \beta \to s$ is that, whenever $\omega \in (2^{\mathbb{N}})^X$ satisfies $\beta$, then $\pi_X^\omega(t)$ is a program from $\Gamma$ to $s$.

The typing rules of $C\lambda_{\to}^{\{\}}$, which are essentially derived from those of $iCPL_0$, are illustrated in Fig. 5, where in the rule $(\mu)$ it is assumed that $\text{FN}(\beta) \subseteq X$, $\text{FN}(d) \subseteq \{a\}$ and $a \notin X$. The rule $(\vee)$ allows one to merge $n$ typing derivations for the same term; in particular, with $n = 0$, one has that $\Gamma \vdash^X t : \bot \to s$ holds for any term $t$. The rule $(\oplus)$ is reminiscent of the rule (m) of $iCPL_0$, the rule $(\mu)$ is reminiscent of the rule (CI) of $iCPL_0$, while the rule $(\{\})$ for CbV application is reminiscent of the rule (CE).

The typing rules of $C\lambda_{\to}$ coincide with those of $C\lambda_{\to}^{\{\}}$ (with $C^{\tilde{q}}$ replaced everywhere by $C^q$), except for the rule $(\{\})$, which is obviously absent, and for the rule $(\mu)$, which is adapted as follows to the presence of exactly one counting quantifier:

$$ \frac{\Gamma \vdash^{X \cup \{a\}} t : \beta \wedge d \to C^q \sigma \qquad \mu(d) \geq s}{\Gamma \vdash^X va.t : \beta \to C^q s \sigma} \quad (\mu') $$

Both systems enjoy the subject reduction property:

**Proposition 5.1 (Subject Reduction).** If $\Gamma \vdash^X t : \beta \to s$ in $C\lambda_{\to}$ (resp. in $C\lambda_{\to}^{\{\}}$) and $t \to u$ (resp. $t \to_{\{\}} u$), then $\Gamma \vdash^X u : \beta \to s$.

The choice of considering arrow types of the form $C^{\tilde{q}}(s \Rightarrow \sigma)$ (hence of never having a counting quantifier to the right
of $\Rightarrow$, as in e.g. $\mathfrak{s} \Rightarrow \mathfrak{C}^q\sigma$) was made to let the rule $(\lambda)$ be
permutable over $(\mu)$, as required by the permuting rule $(\nu\lambda)$.

**Example 5.2.** Fig. 6 illustrates typing derivations in $C\lambda_{\leftarrow}^{\{}}$ for a version of the CbN Church numeral $2^{\text{CbN}} = \lambda y.\lambda x.\{y\}(yx)$, with type $C^{q*}C^q(o \Rightarrow o) \Rightarrow (o \Rightarrow o)$), and for the CbV numeral $2^{\text{CbV}}$ with type $C^q(C^q(o \Rightarrow o) \Rightarrow (o \Rightarrow o))$.

Both $C\lambda_{\leftarrow}$ and $C\lambda_{\leftarrow}^{\{}}$ can type non-normalizable terms. For example, one can type all terms of the form $I \oplus^i \Omega$ with $C^\frac{1}{2}(o \Rightarrow o)$ in $C\lambda_{\leftarrow}^{\{}}$ and with $C^\frac{1}{2}(C^1o \Rightarrow o)$ in $C\lambda_{\leftarrow}$. Actually, the failure of normalization for typable programs can be ascribed to the rule $(\vee)$, as shown by the result below, proved in App. E.1 (where we let $\Gamma \vdash_{\neg\vee} t : \mathfrak{b} \rightarrow \mathfrak{s}$ indicate that $\Gamma \vdash t : \mathfrak{b} \rightarrow \mathfrak{s}$ is deduced without using the rule $(\vee)$).

**Theorem 5.3 (Deterministic Normalization).** In both $C\lambda_{\leftarrow}$ and $C\lambda_{\leftarrow}^{\{}}$, if $\Gamma \vdash_{\neg\vee} t : \mathfrak{b} \rightarrow \mathfrak{s}$, then $t$ is strongly normalizable.

As observed in the previous section, restricting to terms of $\Lambda_{\text{PE}}$ having a normal form excludes the most interesting part of the calculus, which is made of terms for which normalization is inherently probabilistic. Similarly, restricting to type derivations without $(\vee)$ trivializes the most interesting features of $C\lambda_{\leftarrow}$ and $C\lambda_{\leftarrow}^{\{}}$, that is, their ability to estimate probabilities of termination. We will explore the expressiveness of these systems in this sense in the next section.

## 5.2 Translating iCPL₀ into $C\lambda_{\leftarrow}^{\{}}$.

We now show how derivations in iCPL₀ translate into typing derivations in $C\lambda_{\leftarrow}^{\{}}$. In the Appendix A.6 a similar translation of a “CbN” proof-system for iCPL₀ into $C\lambda_{\leftarrow}$ is shown.

For any formula $A$ of iCPL$_0$, let us define a corresponding type $\mathfrak{s}_A$ by letting $\mathfrak{s}_\rho := o$, $\mathfrak{s}_{A \to C\bar{\mathfrak{a}}B} := C^{\bar{\mathfrak{a}}}(\mathfrak{s}_A \Rightarrow \mathfrak{s}_B)$ and $\mathfrak{s}_{Cq_A} := C^q\mathfrak{s}_A$. Fig. 7 shows how a derivation $\Pi$ of $\Gamma \vdash \mathfrak{b} \Rightarrow A$ in iCPL translates into a typing derivation $D^\Pi$ of $\mathfrak{s}_\Gamma \vdash t^\Pi : \mathfrak{b} \Rightarrow \mathfrak{s}_A$ in $C\lambda_{\leftarrow}^{\{}}$, with $\text{FN}(t^\Pi) \subseteq \text{FN}(\mathfrak{b})$, by induction on $\Pi$. Notice that we exploit a special constant $c$ to translate the rule $(\perp)$.

$$ \frac{\Gamma \vdash^X t : c \rightarrow \mathfrak{s} \qquad \mathfrak{b} \models c}{\Gamma \vdash^X t : \mathfrak{b} \rightarrow \mathfrak{s}} (\mathbf{F}) $$

Moreover, the rule $(\rightarrow \text{E})$ translates as CbN application $tu$, while the rule (CE) translates as CbV application $\{t\}u$.

As required by the CHC, normalization steps of iCPL₀ are simulated by $\rightarrow \{\}$-reductions:

**Proposition 5.4 (Stability Under Normalization).** If $\Pi \rightsquigarrow \Pi'$, then $t^\Pi \rightarrow \{\}^* t^\Pi'$.

*Proof sketch.* The normalization steps in Fig. ?? translate into the following reductions:

$$ \begin{align*} & (\lambda x^{q_{\mathfrak{s}_A} \cdot t^\Pi}) va.t^\Sigma \rightarrow \beta \quad t^\Pi[va.t^\Sigma/x] \\ & \{\lambda x^{s_{\mathfrak{s}_A} \cdot t^\Pi}\} va.t^\Sigma \rightarrow_{p\{\}} va.(\lambda x^{s_{\mathfrak{s}_A} \cdot t^\Pi}) t^\Sigma \rightarrow \beta \quad va.t^\Pi[t^\Sigma/x] \end{align*} $$

All other normalization steps translate into $\rightarrow_{p\{\}}$-reductions. $\square$

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

Notice that the normalization step $(\rightarrow I/\rightarrow \text{E})$ translates into CbN reduction (i.e. plain $\beta$-reduction): the “choice” $va.t^\Sigma$ is directly substituted, and thus possibly duplicated; instead the (CI/CE) translates into CbV reduction (i.e. $(\vee f)$ followed by $\beta$-reduction): the generator $va$ is first permuted down and only $t^\Sigma$ is substituted.

By observing that the only use of $(\vee)$ coming from the translation introduces a constant $c$, from Theorem 5.3 we deduce, as promised, the following:

**Corollary 5.5.** iCPL₀ is strongly normalizing.

# 6 From Type Soundness to Type Completeness: Intersection Types

In this section we first show that derivations in $C\lambda_{\leftarrow}$ and $C\lambda_{\leftarrow}^{\{}}$ provide sound approximations of $\text{HNV}(t)$ and $\text{NF}(t)$. In order to achieve completeness, we then introduce an extension $C\lambda_{\leftarrow,\cap}$ of $C\lambda_{\leftarrow}$ with intersection types and show that this system fully captures both deterministic and probabilistic notions of termination for $\Lambda_{\text{PE}}$.

## 6.1 From Types to Probability

We already observed, through examples, that if a term $t$ has a type like, e.g. $C^{\frac{1}{2}}(o \Rightarrow o)$, then $t$ has one chance over two of yielding a “correct” program for $o \Rightarrow o$. The result below makes this intuition precise, by showing that the probabilities derived in $C\lambda_{\leftarrow}$ and $C\lambda_{\leftarrow}^{\{}}$ are lower bounds for the function $\text{HNV}_{\rightarrow}(t)$, that is, for the actual probability of finding a head normalizable term in the distribution $\mathcal{D}_t$.

**Theorem 6.1.** If $\vdash_{C\lambda_{\leftarrow}} t : \mathbf{T} \rightarrow C^q\sigma$, then $\text{HNV}_{\rightarrow}(t) \ge q$. If $\vdash_{C\lambda_{\leftarrow}^{\{}} t : \mathbf{T}} \rightarrow C^{q_1*\cdots*q_n}\sigma$, then $\text{HNV}_{\rightarrow}(t) \ge \prod_{i=1}^n q_i$.

What about reduction to normal form, i.e. the function $\text{NF}_{\rightarrow}(t)$? A result like Theorem 6.1 cannot hold in this case. Indeed, consider the term $t = \lambda y.y(I \oplus^i \Omega)$. While $\text{NF}(t) = \frac{1}{2}$, $C\lambda_{\leftarrow}^{\{}}$ types $t$ with $\mathfrak{s} = C^1(C^1(C^{\frac{1}{2}}\sigma \Rightarrow \sigma) \Rightarrow \sigma)$, with $\sigma = o \Rightarrow o$. The problem in this example is that the type $\mathfrak{s}$ contains the “unbalanced” assumption $C^1(C^{\frac{1}{2}}\sigma \Rightarrow \sigma)$ (in logical terms, $C^{\frac{1}{2}}A \rightarrow C^1A$), i.e. it exploits the assumption of the existence of a function turning a $\frac{1}{2}$-correct input into a 1-correct output. Notice that such a function $f$ can only be one that erases its input, and these are the only functions such that $tf$ can reduce to a normal form.

Nevertheless, soundness with respect to $\text{NF}(t)$ can be proved, for $C\lambda_{\leftarrow}$, by restricting to those types not containing such “unbalanced” assumptions, i.e. to types whose programs cannot increase probabilities.

**Definition 6.2.** A type $C^q(\mathfrak{s}_1 \Rightarrow \dots \Rightarrow \mathfrak{s}_n \Rightarrow o)$ of $C\lambda_{\leftarrow}$ is balanced if all $\mathfrak{s}_i$ are balanced and $q \le \prod_{i=1}^n |\mathfrak{s}_i|$ (where for any type $\mathfrak{s} = C^q\sigma$, $|\mathfrak{s}| = q$).
$$
\begin{align*}
& \frac{y : C^q(o \Rightarrow o), x : C^q_o \cup y : \top \Rightarrow C^q(o \Rightarrow o)}{y : C^q(o \Rightarrow o), x : C^q_o \cup x : \top \Rightarrow o} (\text{@}) \\
& \frac{y : C^q(o \Rightarrow o), x : C^q_o \cup \{y\}(yx) : \top \Rightarrow C^{q \& q_o}}{\vdash 2^{\text{CbN}} : \top \Rightarrow C^{q \& q}(C^q(o \Rightarrow o) \Rightarrow (o \Rightarrow o))} (\lambda) \\
& \frac{y : C^q(o \Rightarrow o) \vdash 2 : \top \Rightarrow (o \Rightarrow o) \Rightarrow (o \Rightarrow o)}{y : C^q(o \Rightarrow o) \vdash y : \top \Rightarrow C^q(o \Rightarrow o)} (\text{@}) \\
& \frac{y : C^q(o \Rightarrow o) \vdash \{2\}y : \top \Rightarrow C^q(o \Rightarrow o)}{\vdash 2^{\text{CbV}} : \top \Rightarrow C^q(C^q(o \Rightarrow o) \Rightarrow (o \Rightarrow o))} (\lambda)
\end{align*}
$$

<caption>Figure 6. Typing of CbN and CbV Church numerals in $C\lambda_{\to}^{\{\}}$.</caption>

$$
\begin{align*}
\overline{\Gamma, A \vdash \mathfrak{b} \to A} \text{ (id)} &\mapsto \overline{\mathfrak{s}_\Gamma, x : \mathfrak{s}_A \vdash x : \mathfrak{b} \to \mathfrak{s}_A} \text{ (id)} \\
\overline{\mathfrak{b} \vdash \bot} \text{ (}\perp\text{)} &\mapsto \overline{\mathfrak{s}_\Gamma \vdash \mathfrak{c} : \mathfrak{b} \to \mathfrak{s}_A} \text{ (}\vee\text{)} \\
\frac{\Gamma \vdash c \to A \qquad \Gamma \vdash d \to A \qquad \mathfrak{b} \vdash (c \wedge x_a^i) \vee (d \wedge \neg x_a^i)}{\Gamma \vdash \mathfrak{b} \to A} \text{ (m)} &\mapsto \frac{D^\Pi \qquad D^\Pi' \qquad \mathfrak{s}_\Gamma \vdash t^\Pi : c \to A \qquad \mathfrak{s}_\Gamma \vdash t^\Pi' : d \to A \qquad \mathfrak{b} \vdash (c \wedge x_a^i) \vee (d \wedge \neg x_a^i)}{\mathfrak{s}_\Gamma \vdash t^\Pi \oplus_a^i t^\Pi' : \mathfrak{b} \to \mathfrak{s}_A} \text{ (}\oplus\text{)} \\
\frac{\Gamma, A \vdash \mathfrak{b} \to B}{\Gamma \vdash \mathfrak{b} \to (A \to B)} \text{ ($\to$I)} &\mapsto \frac{D^\Pi \qquad \mathfrak{s}_\Gamma, x : \mathfrak{s}_A \vdash t^\Pi : \mathfrak{b} \to \mathfrak{s}_B}{\mathfrak{s}_\Gamma \vdash \lambda x.t^\Pi : \mathfrak{b} \to (\mathfrak{s}_A \to B)} \text{ (}\lambda\text{)} \\
\frac{\Gamma \vdash \mathfrak{b} \to (A \to C^q B)}{\Gamma \vdash \mathfrak{b} \to C^q B} \text{ ($\to$E)} &\mapsto \frac{D^\Pi \qquad D^\Sigma \qquad \mathfrak{s}_\Gamma \vdash t^\Pi : \mathfrak{b} \to C^q(\mathfrak{s}_A \to \mathfrak{s}_B) \qquad \mathfrak{s}_\Gamma \vdash t^\Sigma : \mathfrak{b} \to \mathfrak{s}_A}{\mathfrak{s}_\Gamma \vdash t^\Pi t^\Sigma : \mathfrak{b} \to C^q \mathfrak{s}_B} \text{ (}\text{@}\text{)} \\
\frac{\Gamma \vdash \mathfrak{b} \wedge d \to A \qquad \mu(d) \ge q}{\Gamma \vdash \mathfrak{b} \to C^q A} \text{ (CI)} &\mapsto \frac{D^\Pi \qquad \mathfrak{s}_\Gamma \vdash t^\Pi : \mathfrak{b} \wedge d \to \mathfrak{s}_A \qquad \mu(d) \ge q}{\mathfrak{s}_\Gamma \vdash \text{va.t}^\Pi : \mathfrak{b} \to \mathfrak{s}_{C^q A}} \text{ (}\mu\text{)} \\
\frac{\Gamma \vdash \mathfrak{b} \to C^q A \qquad \Gamma, A \vdash \mathfrak{b} \to C^\Sigma B}{\Gamma \vdash \mathfrak{b} \to C^q \mathfrak{s}_A C^\Sigma B} \text{ (CE)} &\mapsto \frac{D^\Sigma \qquad \mathfrak{s}_\Gamma, x : \mathfrak{s}_A \vdash t^\Sigma : \mathfrak{b} \to C^\Sigma \mathfrak{s}_B}{\mathfrak{s}_\Gamma \vdash t^\Pi : \mathfrak{b} \to C^q \mathfrak{s}_A \qquad \mathfrak{s}_\Gamma \vdash \lambda x.t^\Sigma : \mathfrak{b} \to C^\Sigma(\mathfrak{s}_A \Rightarrow \mathfrak{s}_B)} \text{ (}\lambda\text{)} \\
& \phantom{\mapsto} \frac{D^\Sigma \qquad \mathfrak{s}_\Gamma \vdash \{\lambda x.t^\Sigma\} t^\Pi : \mathfrak{b} \to \mathfrak{s}_{C^q A C^\Sigma B}}{\mathfrak{s}_\Gamma \vdash \{\lambda x.t^\Sigma\} t^\Pi : \mathfrak{b} \to \mathfrak{s}_{C^q A C^\Sigma B}} \text{ (\{\})}
\end{align*}
$$

<caption>Figure 7. Translation $\Pi \mapsto D^\Pi$ from $ND_{iCP_{L_0}}$ to $C\lambda_{\to}^{\{\}}$.</caption>

**Theorem 6.3.** If $\Gamma \vdash t : \top \Rightarrow C^q\sigma$ holds in $C\lambda_{\to}$, where $\sigma$ is balanced, then $NF_{\to}(t) \ge q$.

Theorems 6.1 and 6.3 are proved by adapting the standard technique of *reducibility predicates* to the quantitative notion of probabilistic normal form (for further details, see App. E).

## 6.2 From Probability to (Intersection) Types

To achieve a type-theoretic characterization of $HNV_{\to}(t)$ and $NF_{\to}(t)$, we introduce an extension of $C\lambda_{\to}$ with intersection types. Like those of $C\lambda_{\to}$, the types of $C\lambda_{\to, \cap}$ are of the form $\mathfrak{s} = C^q\sigma$, but $\sigma$ is now defined as:

$$ \sigma ::= o \mid n \mid hn \mid \mathfrak{M} \Rightarrow \sigma \qquad \mathfrak{M} ::= [\mathfrak{s}, \dots, \mathfrak{s}] $$

where $[a_1, \dots, a_n]$ indicates a finite set. While $\mathfrak{M}$ intuitively stands for a finite intersection of types, the new ground

types $n$ and $hn$ basically correspond to the types of normalizable and head-normalizable programs.

We introduce a preorder $\sigma \le \tau$ over types by $\alpha \le \alpha$, for $\alpha = o, n, hn$, $C^q\sigma \le C^s\tau$ if $q \le s$ and $\sigma \le \tau$, and $(\mathfrak{M} \Rightarrow \sigma) \le (\mathfrak{M} \Rightarrow \tau)$ if $\sigma \le \tau$ and $\mathfrak{M} \le^* \mathfrak{M}$, where $[\mathfrak{s}_1, \dots, \mathfrak{s}_n] \le^* [t_1, \dots, t_m]$ holds if there exists an injective function $f : \{1, \dots, m\} \to \{1, \dots, n\}$ such that $\mathfrak{s}_{f(i)} \le t_i$.

A type judgment of $C\lambda_{\to, \cap}$ is of the form $\Gamma \vdash^X t : \mathfrak{b} \to \mathfrak{s}$, where $\Gamma$ is made of declarations of the form $x_i : \mathfrak{M}_i$. The typing rules of $C\lambda_{\to, \cap}$ are illustrated in Fig. 8. We omit the $(\vee)$- and $(\oplus)$-rules, which are as in $C\lambda_{\to}$. In the rule $(\mu_\Sigma)$ it is assumed that $\mathfrak{a}$ does not occur in $\mathfrak{b}$, is the only name in the $d_i$, and that for $i \ne j$, $d_i \wedge d_j \vdash \bot$.

The two rules $(hn)$ and $(n)$ are justified by Proposition 6.5 and Theorem 6.6 below. As rule $(n)$ must warrant a bound on normal forms, following Theorem 6.3, $\sigma$ has to be *safe*,
Identity rule:

$$ \frac{s_i \le t \quad \text{FN}(\beta) \subseteq X}{\Gamma, x : [s_1, \dots, s_n] \vdash^X x : \beta \to t} \quad (\text{id}_\le) $$

Ground types rules:

$$ \frac{\Gamma \vdash^X t : \beta \to C^q \sigma}{\Gamma \vdash^X t : \beta \to C^q \text{hn}} \quad (\text{hn}) \qquad \frac{\Gamma \vdash^X t : \beta \to C^q \sigma \quad \sigma \text{ safe}}{\Gamma \vdash^X t : \beta \to C^q \text{n}} \quad (\text{n}) $$

Arrow rules:

$$ \frac{\Gamma, x : \mathfrak{M} \vdash^X t : \beta \to C^q \tau}{\Gamma \vdash^X \lambda x.t : \beta \to C^q (\mathfrak{M} \Rightarrow \tau)} \quad (\lambda) $$

$$ \frac{\Gamma \vdash^X t : \beta \to C^q ([s_1, \dots, s_n] \Rightarrow \tau) \quad \{ \Gamma \vdash^X u : \beta \to s_i \}_{i=1, \dots, n}^{\phantom{\{\phantom{\beta \to s_i}}}}}{\Gamma \vdash^X tu : \beta \to C^q \tau} \quad (\text{@n}) $$

Counting rule:

$$ \frac{\{ \Gamma \vdash^{X \cup \{a\}} t : \beta \wedge d_i \to C^q i \sigma \}_{i=1, \dots, n+1} \quad \mu(d_i) \ge s_i}{\Gamma \vdash^X va.t : \beta \to C^{\Sigma_i q_i s_i \sigma}} \quad (\mu_\Sigma) $$

<caption>Figure 8. Typing rules of $C_{\lambda \to, \emptyset}$.</caption>

i.e. balanced<fnref n="3" /> and $[]$, $hn$-free. The rule $(\text{@n})$ is a standard extension of rule $(\text{@})$ of $C_{\lambda \to}$ to finite intersections.

The counting rule $(\mu_\Sigma)$ requires some discussion. The rule admits $n+1$ major premisses expressing typings for $t$ which depend on pairwise disjoint events (the Boolean formulas $d_i$). This is needed to cope with situations as follows: let

$$ t[a, b] = \left( (I \oplus_b^1 \Omega) \oplus_b^0 \Omega \right) \oplus_a^0 \left( \Omega \oplus_b^0 I \right) $$

$t[a, b]$ can be given type $\sigma = (C^1 o) \Rightarrow o$ under either of the two disjoint Boolean constraints $d_1 := x_a^0 \wedge (x_b^0 \wedge x_b^1)$ and $d_2 := \neg x_a^0 \wedge \neg x_b^0$. In $C_{\lambda \to}$, the best we can achieve to measure the probability that $va.vb.t[a, b]$ has type $\sigma$ is $\frac{1}{4}$. Indeed, the rule $(\mu')$ forces us to approximate $\mu(x_b^0 \wedge x_b^1)$ and $\mu(\neg x_b^0)$ to a common lower bound, i.e. $\frac{1}{4}$, in order to apply a $(\forall)$-rule as illustrated in Fig. 9. Instead, using $(\mu_\Sigma)$ we can compute (again, see Fig. 9), the actual probability $\mu(x_a^0)\mu(x_b^0 \wedge x_b^1) + \mu(\neg x_a^0)\mu(\neg x_b^0) = \frac{1}{2} \cdot \frac{1}{4} + \frac{1}{2} \cdot \frac{1}{2} = \frac{3}{8}$.

Thanks to the rule $(\mu_\Sigma)$, the generalized counting rule $(\mu^*)$ below becomes admissible in $C_{\lambda \to, \emptyset}$:

$$ \frac{\Gamma \vdash^{\{a_1, \dots, a_n\}} t : \beta \to C^q \sigma}{\Gamma \vdash^0 va_1 \dots va_n.t : \tau \to C^q \mu(\beta) \sigma} \quad (\mu^*) $$

This rule plays an essential role in the completeness results below, together with the standard result that both subject reduction and subject expansion hold for intersection types.

**Proposition 6.4 (Subject Reduction/Expansion).** If $\Gamma \vdash^X t : \beta \to s$ and either $t \to u$ or $t \to s$, then $\Gamma \vdash^X t : \beta \to s$.

We will now discuss how typings in $C_{\lambda \to, \emptyset}$ capture both deterministic and probabilistic properties of terms. First we

have the following facts, which show that the types $hn$ and $n$ capture deterministic termination.

**Proposition 6.5 (Deterministic Completeness).** For any closed term $t$,

(i.) $t$ is head-normalizable iff $\vdash_{\neg\vee} t : \tau \to C^1hn$;

(ii.) $t$ is normalizable iff $\vdash_{\neg\vee} t : \tau \to C^1n$.

(iii.) $t$ is strongly normalizable iff $\vdash_{\neg\vee} t : \tau \to C^1n$ and all types in the derivation are safe.

*Proof sketch.* Using standard intersection types arguments, it is shown that $\vdash_{\neg\vee} t : \tau \to C^1hn$ holds for any head-normal $t$. The first half of (i.) is deduced then using Proposition 6.4. The second half follows from a normalization argument similar to that of Theorem 5.3. Cases (ii.) and (iii.) are similar. $\square$

The probabilistic normalization theorems 6.1 and 6.3 (which extend smoothly to $C_{\lambda \to, \emptyset}$) ensure that if $t$ has type $C^qhn$ (resp. $C^qn$), then $HNV_{\to}(t) \ge q$ (resp. $NF_{\to}(t) \ge q$). Conversely, $HNV_{\to}(t)$ and $NF_{\to}(t)$ can be bounded by means of derivations in $C_{\lambda \to, \emptyset}$, in the following sense:

**Theorem 6.6 (Probabilistic Completeness).** For any closed term $t$,

$$ HNV_{\to}(t) = \sup\{q \mid \vdash t : \tau \to C^qhn\} $$

$$ NF_{\to}(t) = \sup\{q \mid \vdash t : \tau \to C^q n\} $$

*Proof sketch.* Suppose w.l.o.g. that $t = va_1 \dots va_k.t'$. For any $u \in \text{HNV}$ such that $\mathcal{D}_t(u) > 0$, we can deduce $\vdash u : \tau \to \text{hn}$. The sequence of probabilistic choices leading to $u$ is finite, and thus captured by a Boolean formula $\beta_{t \to u}$. Using subject reduction/expansion we thus deduce $\vdash t' : \beta_{t \to u} \to \text{hn}$. Hence, for any finite number of head normal forms $u_1, \dots, u_n$, we deduce $\vdash t' : \beta_{t \to u_i} \to \text{hn}$. Using $(\forall)$ and the generalized counting rule $(\mu^*)$ we deduce then $\vdash t : \tau \to C^s\text{hn}$, where $s = \sum_{i=1}^n \mu(\beta_{t \to u_i}) = \mu(\bigvee_{i=1}^n \beta_{t \to u_i})$. The argument for $NF(t)$ is similar. $\square$

# 7 Related Work

As discussed in the introduction, our results provide the first clear correspondence between a proof system and a probabilistic extension of the $\lambda$-calculus. This is not to say that our logic and calculi come from nowhere.

Different kinds of measure-theoretic quantifiers have been investigated in the literature, with the intuitive meaning of “A is true for almost all $x$”, see [41, 51] and more recently [39, 40], or “A is true for the majority of $x$” [44, 58, 59]. Our use of the term “counting quantifier” comes from [2], where an extension of classical propositional logic with such quantifiers is studied and related to Wagner’s counting operator on classes of languages [53–55]. To our knowledge, the present work is the first to apply some form of measure quantifier to typed probabilistic functional programs.

Despite the extensive literature on logical systems enabling (in various ways and for different purposes) some forms of

<footnote n="3">³Definition 6.2 extends to the types of $C_{\lambda \to, \emptyset}$ by letting $\lceil hn \rceil = \lceil \lbrack \rbrack \rceil = 0$, $\lceil n \rceil = 1$ and $\lceil [s_1, \dots, s_{n+1}] \rceil = \max \{\lceil s_i \rceil\}$.</footnote>
$$
\begin{array}{r@{\ }l@{\quad}l@{\quad}l@{\quad}l}
\frac{\Gamma \vdash^{(a,b)} t[a,b] : x_a^0 \wedge (x_b^0 \wedge x_b^1) \to C^1\sigma \qquad \mu(x_b^0 \wedge x_b^1) \ge 1/4}{\Gamma \vdash^{(a)} vb.t[a,b] : x_a^0 \to C^1\sigma} & (\mu') & \frac{\Gamma \vdash^{(a,b)} t[a,b] : \neg x_a^0 \wedge \neg x_b^0 \to C^1\sigma \qquad \mu(\neg x_b^0) \ge 1/4}{\Gamma \vdash^{(a)} vb.t[a,b] : \neg x_a^0 \to C^1\sigma} & (\mu') \\
& & \frac{\Gamma \vdash^{(a)} vb.t[a,b] : x_a^0 \vee \neg x_a^0 \to C^1\sigma}{\Gamma \vdash^0 va.vb.t[a,b] : \tau \to C^1\sigma} & (\mu') \\
\frac{\Gamma \vdash^{(a,b)} t[a,b] : x_a^0 \wedge (x_b^0 \wedge x_b^1) \to C^1\sigma \qquad \mu(x_b^0 \wedge x_b^1) \ge 1/4}{\Gamma \vdash^{(a)} vb.t[a,b] : x_a^0 \to C^1\sigma} & (\mu_\Sigma) & \frac{\Gamma \vdash^{(a,b)} t[a,b] : \neg x_a^0 \wedge \neg x_b^0 \to C^1\sigma \qquad \mu(\neg x_b^0) \ge 1/2}{\Gamma \vdash^{(a)} vb.t[a,b] : \neg x_a^0 \to C^1\sigma} & (\mu_\Sigma) \\
& & \frac{\Gamma \vdash^0 va.vb.t[a,b] : \tau \to C^1\sigma}{\Gamma \vdash^0 va.vb.t[a,b] : \tau \to C^1\sigma} & (\mu_\Sigma)
\end{array}
$$

<caption>Figure 9. Comparing probabilities derived with the rules (μ') and (μΣ).</caption>

probabilistic reasoning, there is not much about logics tied to computational aspects, as iCPL is. Most of the recent log- ical formalisms have been developed in the realm of modal logic, like e.g. [4–6, 22, 29, 30, 42, 43]. Another class of prob- abilistic modal logics have been designed to model Markov chains and similar structures [31, 36, 37]. With the sole ex- ception of Riesz modal logic [23], we are not aware of se- quent calculi for probability logic.

Intuitionistic modal logic has been related in the Curry-
Howard sense to monadic extensions of the λ-calculus [1,
7, 12, 18, 60]. Nevertheless, in these correspondences modal
operators are related to qualitative properties of programs
(typically, tracing algebraic effects), as opposed to the quan-
titative properties expressed by counting quantifiers. Our
Kripke structures for iCPL can be related to standard Kripke
structures for intuitionistic modal logic [46, 49]. These are
based on a set W with two pre-order relations ≤ and R en-
joying a suitable “diamond” property R; ≤ ⊆ ≤; R. We obtain
a similar structure by taking worlds to be pairs w, ω made
of a world and an outcome from the Cantor space, with
(w, ω) ≤ (w', ω) whenever w ≤ w', and (w, ω)R(w, ω + ω').
The clause for CqA can then be seen as a quantitative vari-
ant of the corresponding clause for ♦A. This is not very sur-
prising, given the similarity between the introduction and
elimination rules for Cq and those for ♦, see e.g. [1, 7].

On the other hand, quantitative semantics arising from
linear logic have been largely used in the study of proba-
bilistic λ-calculi, e.g. [14, 19, 21]. Notably, probabilistic co-
herence spaces [19, 20, 27] have been shown to provide a
fully abstract model of probabilistic PCF. While we are not
aware of correspondences relating probabilistic programs
with proofs in linear logic, it seems that the proof-theory
of counting quantifiers could be somehow related to that
of bounded exponentials [17, 28] and, more generally, to the
theory of graded monads and comonads [10, 24, 33, 34].

The calculus Λ<sub>PE</sub> derives from [16], which also introduces
a simple type system ensuring strong normalization, although
theanic types do not provide any quantitative information. Be-
yond this, several type systems for probabilistic λ-calculi
have been introduced in the recent literature. Among these,
systems based on type distributions [15], i.e. where a single
derivation assigns several types to a term, each with some
probability, and systems based on oracle intersection types

[9], where type derivations capture single evaluations as de-
termined by an oracle. Our type systems sit in between these
two approaches: like the first (and unlike the second), typing
derivations can capture a finite number of different evalua-
tions, although without using distributions of types; like the
second, typings reflect the dependency of evaluation on ora-
cles, although the latter are manipulated in a collective way
by means of Boolean constraints.

Finally, in [57] dependent type theory is enriched with a
probabilistic choice operator, yielding a calculus with both
term and type distributions. Interestingly, a fragment of this
system enjoys a sort of CHC with so-called *Markov Logic
Networks* [48], a class of probabilistic graphical models spec-
ified by means of first-order logic formulas.

8 Conclusions

The main contribution of this work consists in defining a
Curry-Howard correspondence between a logic with count-
ing quantifiers and a type system that expresses probability
of termination. Moreover, in analogy with what happens
in the deterministic case, extending the type system with
an intersection operator leads to a full characterization of
probability of termination. Even though intersection types
do not have a clear logical counterpart, the existence of this
extension convinces us that the correspondence introduced
is meaningful. The possibility of defining a Curry-Howard
correspondence relating algebraic effects, on the program
side, with a modal operator, on the logic side, is certainly
not surprising. Instead, it seems to us that the new and sur-
prising contribution of this work is showing that the pecu-
liar features of probabilistic effects can be managed in an
elegant way using ideas coming from logic.

Among the many avenues of research that this work opens,
the study of the problem of type inference must certainly be
mentioned, as well as the extension of the correspondence
to polymorphic types or to control operators. Particularly
intriguing, then, is the possibility of studying the system of
intersection types introduced to support the synthesis, al-
ways in analogy with what is already known in determinis-
tic calculations.
References

[1] N. Alechina, M. Mendler, V. de Paiva, and E. Ritter. Categorical and Kripke semantics for constructive S4 modal logic. In L. Fribourg, editor, *Proc. CSL'21*, volume 2142, pages 292–307. Springer, 2001.

[2] M. Antonelli, U. Dal Lago, and P. Pistone. On Counting Propositional Logic and Wagner's Hierarchy. In *Proc. ICTCS '21*, volume 3072, pages 107–121. CEUR Workshop Proceedings, 2021.

[3] M. Antonelli, U. Dal Lago, and P. Pistone. On Measure Quantifiers in First-Order Arithmetic. In *17th Conference on Computability in Europe Connecting with Computability, 17th Conference on Computability in Europe, CiE 2021*, volume 12813 of *Lecture Notes in Computer Science*, pages 12–24. Springer, 2021.

[4] F. Bacchus. Lp, a logic for representing and reasoning with statistical knowledge. *Comput. Intell.*, 6(4):209–231, 1990.

[5] F. Bacchus. On probability distributions over possible worlds. *Machine Intelligence and Pattern Recognition*, 9:217–226, 1990.

[6] F. Bacchus. *Representing and Reasoning with Probabilistic Knowledge*. MIT Press, 1990.

[7] N. P. Benton, G. M. Bierman, and V. C. V De Paiva. Computational types from a logical perspective. *Journal of Functional Programming*, 8(2):177–193, 1998.

[8] Olivier Bournez and Claude Kirchner. Probabilistic rewrite strategies. applications to elan. In Sophie Tison, editor, *Rewriting Techniques and Applications*, pages 252–266, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg.

[9] F. Breuvart and U. Dal Lago. On Intersection Types and Probabilistic Lambda Calculi. In *Proc. PPDP '18*, New York, NY, USA, 2018. Association for Computing Machinery.

[10] A. Brunel, M. Gaboardi, D. Mazza, and S. Zd舞cewic. A core quantitative coefficient calculus. In *Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410*, pages 351–370, Berlin, Heidelberg, 2014. Springer-Verlag.

[11] L. Caires, F. Pfenning, and B. Toninho. Linear logic propositions as session types. *Math. Struct. in Comput. Sci.*, 26(3):367–423, 2016.

[12] P.-L. Curien, M. Fiore, and G. Munch-Maccagnoni. A Theory of Effects and Resources: Adjunction Models and Polarised Calculi. In *Proc. POPL '16*, pages 44–56. Association for Computing Machinery, 2016.

[13] H. B. Curry and R. Feys. *Combinatory logic. Vol. I*. North-Holland, 1958.

[14] U. Dal Lago, C. Faggian, B. Valiron, and A. Yoshimizu. The Geometry of Parallelism: Classical, Probabilistic, and Quantum Effects. In *Proc. POPL '17*, pages 833–845. Association for Computing Machinery, 2017.

[15] U. Dal Lago and C. Grellois. Probabilistic Termination by Monadic Affine Sized Typing. *ACM TOPLAS*, 41(2):10–65, 2019.

[16] U. Dal Lago, G. Guerrieri, and W. Heijltjes. Decomposing Probabilistic Lambda-Calculi. In *FoSSaCS '20*, pages 136–156. Springer, 2020.

[17] U. Dal Lago and M. Hofmann. Bounded linear logic, revisited. In *Pierre-Louis Curien*, editor, *Typed Lambda Calculi and Applications*, pages 80–94, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg.

[18] R. Davies and F. Pfenning. A Modal Analysis of Staged Computation. *J. ACM*, 48(3):555–604, 2001.

[19] T. Ehrhard and C. Tasson. Probabilistic call by push value. *LMCS*, 15(1):1–46, 2018.

[20] T. Ehrhard, C. Tasson, and M. Pagani. Probabilistic coherence spaces are fully abstract for probabilistic pcf. In *Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, POPL '14, pages 309–320, New York, NY, USA, 2014. Association for Computing Machinery.

[21] C. Faggian and S. Ronchi della Rocca. Lambda-calculus and probabilistic computation. In *Proc. LICS '19*, pages 1–13, 2019.

[22] R. Fagin and J.Y. Halpern. Reasoning about Knowledge and Probability. *J. ACM*, 41(2):340–367, 1994.

[23] R. Furber, R. Mardare, and M. Mio. Probabilistic logics based on Riesz spaces. *LMCS*, 16, 2020.

[24] D. R. Ghica and A. I. Smith. Bounded linear types in a resource semiring. In *Proceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 8410*, pages 331–350, Berlin, Heidelberg, 2014. Springer-Verlag.

[25] J.-Y. Girard. *Interprétation fonctionnelle et élimination des coupures de l'arithmetique d'ordre supérieur*. PhD thesis, Université Paris VII, 1972.

[26] J.-Y. Girard, Y. Lafont, and P. Taylor. *Proofs and Types*, volume 7 of *Cambridge Tracts in Theoretical Computer Science*. Cambridge University Press, 1989.

[27] J.-Y. Girard, P. Ruet, P. Scott, and T. Ehrhard. *Between Logic and Quantic: a Tract*, pages 346–381. London Mathematical Society Lecture Note Series. Cambridge University Press, Cambridge, 2004.

[28] Jean-Yves Girard, Andre Scedrov, and Philip J. Scott. Bounded linear logic: a modular approach to polynomial-time computability. *Theoretical Computer Science*, 97(1):1–66, 1992.

[29] J.Y. Halpern. An Analysis of First-Order Logics for Probability. *Artif. Intell.*, 46(3):311–350, 1990.

[30] J.Y. Halpern. *Reasoning About Uncertainty*. MIT Press, 2003.

[31] H. Hansson and B. Jonsson. A logic for reasoning about time and reliability. *Form. Asp. Comput.*, 6(5):512–535, 1994.

[32] W.A. Howard. The formula-as-types notion of construction (1969). In *To H.B. Curry. Essays on Combinatory Logic, Lambda Calculus and Formalism*. Academic Press, 1980.

[33] S. Katsumata. Parametric effect monads and semantics of effect systems. In *Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages*, POPL '14, pages 633–645, New York, NY, USA, 2014. Association for Computing Machinery.

[34] S. Katsumata. A double category theoretic analysis of graded linear exponential comonads. In Christel Baier and Ugo Dal Lago, editors, *Foundations of Software Science and Computation Structures*, pages 110–127, Cham, 2018. Springer International Publishing.

[35] Naoki Kobayashi, Ugo Dal Lago, and Charles Grellois. On the Termination Problem for Probabilistic Higher-Order Recursive Programs. In *LICS 2019 - 34th Annual ACM/IEEE Symposium on Logic in Computer Science*, pages 1–14, Vancouver, France, 2019. IEEE.

[36] D. Kozen. Semantics of probabilistic programs. *JCSS*, 22(3):328 – 350, 1981.

[37] D. Lehmann and S. Shelah. Reasoning with time and chance. *Inf. Control.*, 53(3):165 – 198, 1982.

[38] P. Martin-Löf. An intuitionistic theory of types: predicative part. In *Proc. Logic Colloquium '73*, volume 80 of *Studies in logic and the foundations of mathematics*, pages 73–118. North-Holland, 1975.

[39] H. Michalewski and M. Mio. Measure quantifiers in monadic second order logic. *LFCS*, pages 267–282, 2016.

[40] M. Mio, M. Skrzypczak, and H. Michalewski. Monadic Second Order Logic with Measure and Category Quantifiers. *LMCS*, 8(2):1–29, 2012.

[41] C.F. Morgenstern. The Measure Quantifier. *J. Symb. Log.*, 44(1):103–108, 1979.

[42] N. J. Nilsson. Probabilistic logic. *Artif. Intell.*, 28(1):71–87, 1986.

[43] N. J. Nilsson. Probabilistic logic revisited. *Artif. Intell.*, 59(1/2):39–42, 1993.

[44] C.H. Papadimitriou. Games against nature. *JCSS*, 31(2):288–301, 1985.

[45] M. Parigot. $\lambda\mu$-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. In A. Voronkov, editor, *Logic Programming and Automated Reasoning*, pages 190–201. Springer Berlin Heidelberg, 1992.

[46] G. Plotkin and C. Stirling. A framework for intuitionistic modal logics: Extended abstract. In *Proc. TARK '86*, pages 399–406. Morgan Kaufmann Publishers Inc., 1986.

[47] M. L. Puterman. *Markov Decision Processes: Discrete Stochastic Dynamic Programming*. John Wiley & Sons, Inc., USA, 1st edition, 1994.
[48] M. Richardson and P. Domingos. Markov logic networks. *Machine Learning*, 62(1):107–136, 2006.

[49] A.K. Simpson. *The Proof Theory and Semantics of Intuitionistic Modal Logic*. PhD thesis, University of Edinburgh, 1994.

[50] M.H. Sorensen and P. Urzyczyn. *Lectures on the Curry-Howard isomorphism*, volume 149 of *Studies in Logic and the Foundations of Mathematics*. Elsevier, 2006.

[51] C.I. Steinhorn. *Borel Structures and Measure and Category Logics*, volume 8, pages 579–596. Springer-Verlag, 1985.

[52] P. Wadler. Propositions as Sessions. In *Proc. ICFP '12*, pages 273–286. Association for Computing Machinery, 2012.

[53] K.W. Wagner. Compact descriptions and the counting polynomial-time hierarchy. In *Frege Conference 1984: Proceedings of the International Conference held at Schwerin*, pages 383–392, 1984.

[54] K.W. Wagner. Some Observations on the Connection Between Counting and Recursion. *TCS*, 47:131–147, 1986.

[55] K.W. Wagner. The Complexity of Combinatorial Problems with Successive Input Representation. *Acta Informatica*, 23:325–356, 1986.

[56] D. Wang, D. M. Kahn, and J. Hoffmann. Raising expectations: Automating expected cost analysis with types. *Proc. ACM Program. Lang.*, 4(ICFP), aug 2020.

[57] J. Warrell and M. B. Gerstein. Dependent type networks: a probabilistic logic via the Curry-Howard correspondence in a system of probabilistic dependent types. Uncertainty in Artificial Intelligence, Workshop on Uncertainty in Deep Learning, 2018.

[58] S. Zachos. Probabilistic Quantifiers and Games. *JCSS*, 36(3):433–451, 1988.

[59] S. Zachos and H. Heller. A decisive characterization of BPP. *Inf. Control.*, pages 125–135, 69.

[60] N. Zyuzin and A. Nanevski. Contextual modal types for algebraic effects and handlers. *Proc. ICFP '21*, 5(ICFP):1–29, 2021.
# Appendices

<table><tr><td>A</td><td>Details about Intuitionistic Counting Propositional Logic</td><td>15</td></tr><tr><td>A.1</td><td>The Proof-Theory of iCPL.</td><td>15</td></tr><tr><td>A.2</td><td>Relating iCPL and iCPL<sub>0</sub>.</td><td>16</td></tr><tr><td>A.3</td><td>Normalization in ND<sub>iCPL</sub><sup>-</sup>.</td><td>17</td></tr><tr><td>A.4</td><td>Soundness and Completeness of ND<sub>iCPL</sub>.</td><td>18</td></tr><tr><td>A.5</td><td>Permutative Rules in iCPL<sub>0</sub>.</td><td>24</td></tr><tr><td>A.6</td><td>A “CbN” Proof-System.</td><td>24</td></tr><tr><td>B</td><td>Details about the Probabilistic Event λ-Calculus.</td><td>26</td></tr><tr><td>B.1</td><td>The Language Λ<sub>PE</sub>.</td><td>26</td></tr><tr><td>B.2</td><td>The Language Λ<sub>PE</sub><sup>{}</sup>.</td><td>28</td></tr><tr><td>C</td><td>Details about Cλ<sub>→</sub><sup>{}</sup>.</td><td>30</td></tr><tr><td>C.1</td><td>Subject Reduction.</td><td>30</td></tr><tr><td>D</td><td>Details about Cλ<sub>→,∩</sub>.</td><td>34</td></tr><tr><td>D.1</td><td>Subject Reduction.</td><td>34</td></tr><tr><td>D.2</td><td>Subject Expansion.</td><td>38</td></tr><tr><td>D.2.1</td><td>Subject β-Expansion</td><td>38</td></tr><tr><td>D.2.2</td><td>Subject Permutative Expansion</td><td>43</td></tr><tr><td>D.3</td><td>Completeness.</td><td>45</td></tr><tr><td>D.3.1</td><td>Deterministic Completeness</td><td>45</td></tr><tr><td>D.3.2</td><td>Probabilistic Completeness</td><td>46</td></tr><tr><td>E</td><td>Normalization Results</td><td>49</td></tr><tr><td>E.1</td><td>Deterministic Normalization.</td><td>49</td></tr><tr><td>E.1.1</td><td>Deterministic Normalization of Cλ<sub>→</sub><sup>{}</sup>.</td><td>49</td></tr><tr><td>E.1.2</td><td>Deterministic Normalization of Cλ<sub>→,∩</sub>.</td><td>52</td></tr><tr><td>E.2</td><td>Probabilistic Reducibility Candidates for Λ<sub>PE</sub>.</td><td>53</td></tr><tr><td>E.3</td><td>Probabilistic Reducibility Candidates for Λ<sub>PE</sub><sup>{}</sup>.</td><td>61</td></tr></table>

## A Details about Intuitionistic Counting Propositional Logic

In this section we introduce a proof-system ND<sub>iCPL</sub> for iCPL and describe the correspondence between proofs in iCPL and families of proofs iCPL<sub>0</sub>; then, we establish the soundness and completeness of ND<sub>iCPL</sub> with respect to iCPL-structures. Finally, we provide some more details about normalization in the “computational fragment” iCPL<sub>0</sub> and we describe an alternative “CbN” proof-system for iCPL<sub>0</sub>, whose derivations can be decorated with terms of Λ<sub>PE</sub>, yielding a CHC with the type system Cλ<sub>→</sub>.

### A.1 The Proof-Theory of iCPL.

The natural deduction system ND<sub>iCPL</sub> for iCPL is formed by the rules illustrated in Fig. 10, with the following proviso:

* it is everywhere assumed that in a sequent Γ ⊢ A, FN(Γ), FN(A) ⊆ X;

* in the rule (CI) and (CE<sub>3</sub>) it is assumed that FN(d) ⊆ {a}.

together with all instances of the two axiom schema below:

$$ \begin{array}{l@{\quad}l@{\quad}l} C_a^q(A \lor B) \rightarrow A \lor (C_a^q A) & (a \notin FN(A)) & (C\lor) \\ \neg C_a^q \neg b & (FN(b) \subseteq \{a\}, \mu(b) < q) & (C\perp) \end{array} $$

As usual, we take $\neg A$ as an abbreviation for $A \supset \perp$.

We let ND<sub>iCPL</sub><sup>-</sup> indicate ND<sub>iCPL</sub> without (C<sub>V</sub>) and (C<sub>⊥</sub>).

**Remark 1.** The reason for distinguishing between the systems ND<sub>iCPL</sub> and ND<sub>iCPL</sub><sup>-</sup> is somehow analogous to what happens in intuitionistic modal logic (IML). Indeed, standard axiomatizations of IML include two axioms

$$ \diamond(A \lor B) \rightarrow \diamond A \lor \diamond B \qquad (\diamond \lor) $$

$$ \neg \diamond \perp \qquad (\diamond \perp) $$
$$ \frac{\text{Classical Identity}}{\Gamma \vdash x_a^i \lor \neg x_a^i} \quad (\text{Cid}) $$

$$ \frac{\text{Intuitionistic Identity}}{\Gamma, A \vdash A} \quad (\text{lid}) $$

Logical Rules

$$ \frac{\Gamma \vdash \tau}{\Gamma \vdash \tau} (\tau I) $$

$$ \frac{\Gamma \vdash \perp}{\Gamma \vdash A} (\perp E) $$

$$ \frac{\Gamma \vdash A}{\Gamma \vdash A \land B} \frac{\Gamma \vdash A}{\Gamma \vdash A \land B} (\land I) $$

$$ \frac{\Gamma \vdash A \land B}{\Gamma \vdash A} (\land E_1) $$

$$ \frac{\Gamma \vdash A \land B}{\Gamma \vdash B} (\land E_2) $$

$$ \frac{\Gamma \vdash A}{\Gamma \vdash A \lor B} (\lor I_1) $$

$$ \frac{\Gamma \vdash A}{\Gamma \vdash A \lor B} (\lor I_2) $$

$$ \frac{\Gamma \vdash A \lor B}{\Gamma \vdash C} \frac{\Gamma, A \vdash C}{\Gamma, B \vdash C} (\lor E) $$

$$ \frac{\Gamma, A \vdash B}{\Gamma \vdash A \rightarrow B} (\rightarrow I) $$

$$ \frac{\Gamma \vdash A \rightarrow B}{\Gamma \vdash B} \frac{\Gamma \vdash A}{\Gamma \vdash B} (\rightarrow E) $$

Counting Rules

$$ \frac{\Gamma, d \vdash A \quad \mu(d) \geq q}{\Gamma \vdash C_a^q A} \quad (\text{CI}) \quad a \notin \Gamma $$

$$ \frac{\Gamma \vdash C_a^q A}{\Gamma \vdash A} (\text{CE}_1) \quad a \notin A $$

$$ \frac{\Gamma \vdash C_a^q A \quad \Gamma, A \vdash C}{\Gamma \vdash C_a^{qs} C} (\text{CE}_2) \quad a \notin \Gamma $$

<caption>**Figure 10.** Rules of ND<sub>iCPL</sub>.</caption>

which do not have a clear computational interpretation. Instead, a Curry-Howard correspondence can be defined for an axiomatization of IML (usually referred to as constructive modal logic) which does not include these two axioms.

In a similar way, we will show that provability in ND<sub>iCPL</sub><sup>-</sup> corresponds, under the decomposition provided by Lemma 3.3 to provability in the Curry-Howard proof-system ND<sub>iCPL<sub>0</sub></sub>, while axioms (C<sup>⊤</sup>) and (C<sup>⊥</sup>) cannot be similarly interpreted.

A formula A of iCPL is purely classical if A contains no intuitionistic propositional variable, and purely intuitionistic if A contains no classical propositional variable.

Let us list a few properties of iCPL.

**Lemma A.1.** For any purely Boolean formula $b$, $\vdash b$ is derivable in ND<sub>iCPL</sub> iff $b$ is a tautology.

**Lemma A.2.** The following are theorems of iCPL:

(i.) $C_a^q \perp \leftrightarrow$ and $C_a^q \vdash \leftrightarrow$;

(ii.) if $a \notin \text{FN}(A)$, $C_a^q(A \rightarrow B) \rightarrow (A \rightarrow C_a^q B)$.

(iii.) if $a \notin \text{FN}(A)$, $C_a^q(A \land B) \leftrightarrow A \land C_a^q B$.

iv. if $a \notin \text{FN}(A)$, then $C_a^q A \leftrightarrow A$.

**Lemma A.3.** For any Boolean formula $b$ with $\text{FN}(b) \subseteq \{a\}$, $C_a^q b \lor (\neg C_a^q b)$ is provable.

*Proof.* Two possibilities arise: if $\mu(b) \ge q$, then from $b \vdash b$ we deduce, by (CI), $\vdash C_a^q b$ as well as $\vdash C_a^q b \lor (\neg C_a^q b)$. if $\mu(b) > q$, then we deduce, using axiom C<sup>⊥</sup>, $\vdash \neg C_a^q b$, as well as $\vdash C_a^q b \lor (\neg C_a^q b)$. $\square$

## A.2 Relating iCPL and iCPL<sub>0</sub>.

Let us first provide a complete proof of the decomposition lemma (Lemma 3.3).

For any formula C and $b \in \{0, 1\}$, let $\neg^b C$ indicate the formula C if $b = 0$ and $\neg C$ if $b = 1$. For any $\omega \in (2^N)^{\mathcal{A}}$, let the theory of $\omega$ be the following set of Boolean formulas:

$$ \mathrm{Th}(\omega) = \{\neg^{(1-\omega)(a(i))} x_a^i \mid a, i \in \mathbb{N}\} $$

Moreover, for all $K \in \mathbb{N}$ and finite set X, let $\mathrm{Th}_X^K(\omega)$ be the Boolean formula below

$$ \mathrm{Th}_X^K(\omega) = \bigwedge_{a \in A, i \le K} \neg^{(1-\omega(a(i)))} x_a^i $$

Observe that the formula $\mathrm{Th}_X^K(\omega)$ only depends on a finite amount of information of $\omega$, namely, on the unique $v \in (2^{\{1,...,K\}})^X$ such that $v(a)(i) = \omega(a)(i)$. When $v$ is clear from the context, we will indicate $\mathrm{Th}_X^K(\omega)$ simply as $\mathrm{Th}(v)$.

The decomposition lemma can be reformulated then as follows:
**Lemma A.4** (decomposition lemma, syntactic formulation). For any formula $A$ of iCPL there exist intuitionistic formulas $A_v$, where $v$ varies over all possible valuations of the Boolean variables in $A$, such that $\vdash A \leftrightarrow \bigvee_v \mathrm{Th}(v) \wedge A_v$.

*Proof.* The formula $A_v$ is defined by induction on $A$ as follows:

* if $A = \top$, $A = \bot$, or $A = p$, then $A_v = A$;

* if $A = \alpha_a^i$, then $A_v = \top$ if $v(a)(i) = 1$, and $A_v = \bot$ if $v(a)(i) = 0$;

* if $A = \mathrm{BcC}$, where $c = \wedge, \vee, \rightarrow$, then $A_v = B_v c C_v$;

* if $A = C_a^q B$, then we consider two cases:

* if $a$ does not occur in $B$, then we let $A_v := B_v$;

* if $a$ does occur in $B$, then for all valuation $w$ of the variables of name $a$ in $B$, we can suppose that the formulas $B_{v+w}$ are well-defined. We let then $A_v = C_a^q \bigvee_w B_{v+w}$.

Let us show that for any formula $A$ and valuation $v$ of its Boolean variables, $\mathrm{Th}(v) \vdash_i \mathrm{CPL} \leftrightarrow A_v$. We argue by induction on $A$. Indeed, the only non-trivial case is that of $A = C_a^q B$. If $a$ does not occur in $B$, then we can conclude by the IH. Otherwise, by the IH we have that for any valuation $w$ of the Boolean variables of $B$ of name $a$, $\mathrm{Th}(v+w) \vdash B \leftrightarrow B_{v+w}$. Using the fact that $\bigvee_w \mathrm{Th}(w)$ is provable and that $\mathrm{Th}(v+w) \leftrightarrow (\mathrm{Th}(v) \wedge \mathrm{Th}(w))$, we deduce then $\mathrm{Th}(v) \vdash B \leftrightarrow \bigvee_w B_{v+w}$, from which we can deduce $\mathrm{Th}(v) \vdash A \leftrightarrow A_v$.

Using $\mathrm{Th}(v) \vdash A \leftrightarrow A_v$ and $\vdash \bigvee_v \mathrm{Th}(v)$, we can conclude $\vdash A \leftrightarrow \bigvee_v \mathrm{Th}(v) \wedge A_v$.

If $A$ is a formula of iCPL containing no Boolean variable, we let $|A|$ indicate the corresponding formula of $\mathrm{iCPL}_0$ obtained by deleting names from counting quantifiers, i.e. replacing $C_a^q$ by $C^q$.

In the following, we consider as $\mathrm{ND}_{\mathrm{iCPL}_0}$ the proof-system obtained by enriching the rules from Section 3 with all standard rules for intuitionistic connectives (straightforwardly adapted to the sequents of $\mathrm{ND}_{\mathrm{iCPL}_0}$ by adding everywhere a fixed Boolean formula $\cdots \vdash \beta \rightarrow \dots$).

**Lemma A.5.** In $\mathrm{ND}_{\mathrm{iCPL}_0}$, if $\Gamma \vdash \beta \wedge c \rightarrow A$, where $\beta \wedge c$ is satisfiable, then $\Gamma \vdash \beta \rightarrow A$.

*Proof.* By induction on the rules of $\mathrm{ND}_{\mathrm{iCPL}_0}$.

The following result describes the correspondence between the proof-theories of iCPL and $\mathrm{iCPL}_0$.

**Proposition A.6.** $\Gamma \vdash_{\mathrm{ND}_{\mathrm{iCPL}}^{-}} A$ iff for all valuations $v$, $|\Gamma_v| \vdash_{\mathrm{ND}_{\mathrm{iCPL}_0}} \mathrm{Th}(v) \rightarrow |A_v|$.

*Proof.* The first part follows from the decomposition lemma (Lemma 3.3) and from the fact that $|\Gamma| \vdash_{\mathrm{ND}_{\mathrm{iCPL}_0}} \beta \rightarrow |A|$ implies $\Gamma, \beta \vdash_{\mathrm{ND}_{\mathrm{iCPL}}^{-}} A$ (easily checked by induction on the rules of $\mathrm{ND}_{\mathrm{iCPL}_0}$).

For the only-if part we argue by induction on the rules of $\mathrm{ND}_{\mathrm{iCPL}}$. All propositional cases are straightforward, so we only focus here on the rules for counting quantifiers.

$$ \frac{\Gamma, \ d \vdash A \qquad \mu(d) \ge q}{\Gamma \vdash C_a^q A} \quad \mapsto \quad \frac{\left\{ \frac{|\Gamma_v| \vdash \mathrm{Th}(v) \wedge \mathrm{Th}(w) \rightarrow |A_{v+w}|}{|\Gamma_v| \vdash \mathrm{Th}(v) \wedge \mathrm{Th}(w) \rightarrow \bigvee_w |A_{v+w}|} \right\}_{w \ne d}}{(\mathrm{m})} \qquad \frac{|\Gamma_v| \vdash \mathrm{Th}(v) \wedge d \rightarrow \bigvee_w |A_{v+w}|}{|\Gamma_v| \vdash \mathrm{Th}(v) \rightarrow |(C_a^q A)_v|} \quad (\mathrm{CI}) $$

(CE)$_1$ Since $a \notin \mathrm{FN}(A)$, it follows that $(C_a^q A)_v = A_v$, so we can conclude by the IH.

$$ \frac{\Gamma \vdash C_a^q \qquad \Gamma, A \vdash B}{\Gamma \vdash C_a^{qs} B} \quad \mapsto \quad \frac{\left\{ \frac{|\Gamma_v|, |A_{v+w}| \vdash \mathrm{Th}(v) \wedge \mathrm{Th}(w) \rightarrow |B_{v+w}|}{|\Gamma_v|, |A_{v+w}| \vdash \mathrm{Th}(v) \rightarrow (\bigvee_w |B_{v+w}|)} \right\}_{w}}{|\Gamma_v| \vdash \mathrm{Th}(v) \rightarrow |(C_a^q A)_v|} \quad (\mathrm{CE}) $$

### A.3 Normalization in $\mathrm{ND}_{\mathrm{iCPL}}^{-}$

It is possible to define a normalization procedure for $\mathrm{ND}_{\mathrm{iCPL}}^{-}$. Cuts formed by propositional intro-elim rules are reduced as in standard intuitionistic logic. The cuts formed by counting rules are reduced as follows:
(CI/CE₁)

$$ \frac{\Pi_{\Gamma, d \vdash A \quad \mu(d) \ge q}}{\frac{\Gamma \vdash C_a^q A}{\Gamma \vdash A}} (\text{CI}) \rightsquigarrow \frac{\Pi^*_{\Gamma \vdash A}}{\Gamma \vdash A} $$

where the derivation $\Pi^*$ is obtained from Lemma A.7 below, easily established by induction.

**Lemma A.7.** If $\Gamma, \delta \vdash A$ is derivable in $ND_{iCPL}^{-}$, where $\text{FN}(\delta) \subseteq \{a\}$, and a does not occur in either $\Gamma$ nor $A$, then $\Gamma \vdash A$ is derivable with a derivation of same length and using the same rules.

(CI/CE₂)

$$ \frac{\Pi_{\Gamma, d \vdash A \quad \mu(d) \ge q}}{\frac{\Gamma \vdash C_a^q A}{\Gamma \vdash C_a^{qs} B}} (\text{CI}) \rightsquigarrow \frac{\Sigma_{\Gamma, d \vdash A \quad \Gamma, A \vdash B}}{\Gamma \vdash B} (\text{CE}_2) \rightsquigarrow \frac{\Pi_{\Gamma, d \vdash A \quad \Sigma_{\Gamma, d \vdash B}}}{\Gamma \vdash C_a^{qs} B} (\text{subst}) \frac{\mu(d) \ge q s}{\Gamma \vdash C_a^{qs} B} (\text{CI}) $$

where the admissibility of the rule (subst) is easily checked by induction.

The proof of Theorem A.6 yields a way to associate each proof $\Pi$ of $\Gamma \vdash A$ in $ND_{iCPL}^{-}$ with a family of proofs $\Pi_v$ of $|\Gamma_v| \vdash \text{Th}(v) \mapsto |A_v|$ in $ND_{iCPL_0}^{-}$. This association preserves normalization in the following sense:

**Lemma A.8.** For any two proofs $\Pi, \Sigma$ of $\Gamma \vdash A$ in $ND_{iCPL}^{-}$ and any valuation $v$ of the Boolean variables in $\Gamma$ and $A$, if $\Pi \rightsquigarrow^* \Sigma$, then $\Pi_v \rightsquigarrow^* \Sigma_v$.

The lemma above, easily checked, can be used to deduce the strong normalization of $ND_{iCPL}^{-}$ from that of $ND_{iCPL_0}$:

**Theorem A.9.** $ND_{iCPL}^{-}$ is strongly normalizing.

## A.4 Soundness and Completeness of $ND_{iCPL}$.

Let us first establish a few properties of Kripke Semantics. For this we first need to recall a fundamental property of Borel sets.

For any Borel set $S \in \mathcal{B}_{X \cup Y}$ and $\omega \in (2^{\mathbb{N}})^X$, let

$$ \Pi^{\omega}(S) = \{\omega' \in (2^{\mathbb{N}})^Y \mid \omega + \omega' \in S\} \subseteq (2^{\mathbb{N}})^X $$

Notice that $\Pi^{\omega}(S)$ is an analytic set and needs not be Borel. However, since the Lebesgue measure is defined on all analytic sets, the values $\mu(\Pi^{\omega}(S))$, for $S$ Borel (or more generally, analytic), are always defined. Moreover the following holds:

**Lemma A.10.** [[?], Theorem 14.11 + Theorem 29.26] For any $S \in \mathcal{B}_{X \cup Y}$, with $X \cap Y = \emptyset$, and $r \in [0, 1]$, $\{\omega \in (2^{\mathbb{N}})^X \mid \mu(\Pi^r(S)) \ge r\} \in \mathcal{B}_X$.

For any $S \subseteq \mathcal{B}_X$ and $Y \supseteq X$, let $S^{\uparrow Y} := S \times (2^{\mathbb{N}})^{Y-X}$.

Using Lemma A.10 we can show that for any iCPL-structure $\mathcal{M} = (W, \leq, i)$ and world $w \in W$, the set of functions $\omega \in (2^{\mathbb{N}})^X$ such that $w, \omega \models_{\mathcal{M}}^X A$ is a Borel set.

**Lemma A.11.** Given a iCPL-structure $\mathcal{M} = (W, \leq, i)$, for any finite set $X$, $w \in W$ and formula $A$ with $\text{FN}(A) \subseteq X$, the set

$$ \text{mod}_{\mathcal{M}}(A, X, w) = \{\omega \in (2^{\mathbb{N}})^X \mid w, \omega \models_{\mathcal{M}}^X A\} $$

is Borel.

*Proof.* We argue by induction on $A$:

* if $A = \perp$, then $\text{mod}_{\mathcal{M}}(A, X, w) = \emptyset$ is Borel; similarly, if $A = \top$, then $\text{mod}_{\mathcal{M}}(A, X, w) = (2^{\mathbb{N}})^X$ is Borel;

* if $A = x_a^i$, then $\text{mod}_{\mathcal{M}}(A, X, w)$ is the cylinder $\{f \mid f(a)(i) = 1\}$, so it is Borel;

* if $A = p$, then $\text{mod}_{\mathcal{M}}(A, X, w)$ is either $(2^{\mathbb{N}})^X$ or the empty set, which are both Borel;

* if $A = B \wedge C$, then $\text{mod}_{\mathcal{M}}(A, X, w) = \text{mod}_{\mathcal{M}}(B, X, w) \cap \text{mod}_{\mathcal{M}}(C, X, w)$, so we conclude by the I.H.;

* if $A = B \vee C$, then $\text{mod}_{\mathcal{M}}(A, X, w) = \text{mod}_{\mathcal{M}}(B, X, w) \cup \text{mod}_{\mathcal{M}}(C, X, w)$, so we conclude by the I.H.;

* if $A = B \rightarrow C$, then $\text{mod}_{\mathcal{M}}(A, X, w) = \bigcap_{w' \ge w} \text{mod}_{\mathcal{M}}(B, X, w') \cup \text{mod}_{\mathcal{M}}(C, X, w')$ is, by the I.H., a countable intersection of Borel sets, so it is Borel;
* if $A = C_a^q B$, then by the I.H., for all $w' \in W$, $\mathrm{mod}_{\mathcal{M}}(B, X \cup \{a\}, w')$ is Borel; using Lemma A.10 we then have that the set

$$ \mathrm{mod}_{\mathcal{M}}(A, X, w) = \bigcap_{w' \ge w} \{\omega \in (2^N)^X \mid \mu(\Pi^\omega (\mathrm{mod}_{\mathcal{M}}(B, X \cup \{a\}, w))) \ge q\} $$

is Borel.

□

**Lemma A.12 (monotonicity).** If $w, \omega \Vdash_{\mathcal{M}}^X A$ and $w \le w'$, then $w', \omega \Vdash_{\mathcal{M}}^X A$.

*Proof.* We argue by induction on A.

If $A = p$ the claim follows from the fact that $i(p)$ is an upper set;

If $A = x_a^i$ the claim is immediate.

If $A = B \wedge C$, the claim follows from the I.H.

If $A = B \to C$ and $w, \omega \Vdash_{\mathcal{M}}^X A$, then for all $w'' \ge w, w'', \omega \Vdash_{\mathcal{M}}^X B$ implies $w'', \omega \Vdash_{\mathcal{M}}^X C$. Hence, in particular, for all $w'' \ge w' \ge w, w'', \omega \Vdash_{\mathcal{M}}^X B$ implies $w'', \omega \Vdash_{\mathcal{M}}^X C$, and thus $w', \omega \Vdash_{\mathcal{M}}^X A$.

If $A = C_a^q B$ then by the I.H. for all $\omega' \in 2^N$, $w, \omega + \omega' \Vdash_{\mathcal{M}}^{X \cup \{a\}} B$ implies that for all $w' \ge w, w', \omega + \omega' \Vdash_{\mathcal{M}}^{X \cup \{a\}} B$; we deduce then that for all $w' \ge w$, for all $w'' \ge w' \ge w$, the set $\{\omega' \in 2^N \mid w'', \omega + \omega' \Vdash_{\mathcal{M}}^{X \cup \{a\}} B\}$ has measure $\ge q$, which implies $w', \omega \Vdash_{\mathcal{M}}^X A$. □

**Lemma A.13.** Let $\mathcal{M} = (W, \le, \alpha)$ be a iCPL-structure. For any finite set $X$ and $a \notin X$, for all $u \in W$ and $b \in B_X$, and for any formula $A \in \mathrm{Formula}_X$, if $u, \omega \Vdash_{\mathcal{M}}^X A$ holds, then $u, \omega' \Vdash_{\mathcal{M}}^{X \cup \{a\}} A$ holds for any $\omega' \in \{\omega\}^{\upharpoonright_{X \cup \{a\}}}$.

*Proof.* By induction on the rules.

**Lemma A.14.** Let $\mathcal{M} = (W, \le, i)$ be a iCPL-structure. For any finite set $X$, $a \notin X$, formula $A \in \mathrm{Formula}_X$, $q \in (0, 1]$ and $\omega \in B_X$,

$$ w, \omega \Vdash_{\mathcal{M}}^X C_a^q A \Rightarrow w, \omega \Vdash_{\mathcal{M}}^X A $$

*Proof.* $w', \omega \Vdash_{\mathcal{M}}^X C_a^q A$ implies that $\mu(\{\omega' \in 2^N \mid u, \omega + \omega' \Vdash_{\mathcal{M}}^{X \cup \{a\}} A\}) \ge q > 0$. From $u, \omega + \omega' \Vdash_{\mathcal{M}}^{X \cup \{a\}} A$ one can deduce by induction on $A$ that $u, \omega \Vdash_{\mathcal{M}}^X A$. Since there exists at least one such $f$, we conclude that $u, \omega \Vdash_{\mathcal{M}}^X A$ holds. □

We are now in a position to establish, by induction on the rules, the soundness of $\mathrm{ND}_{\mathrm{iCPL}}$.

**Proposition A.15 (soundness).** If $\Gamma \vdash \mathrm{ND}_{\mathrm{iCPL}} A$, then $\Gamma \vdash A$.

*Proof.* Let $\mathcal{M} = (W, \le, i)$ be a iCPL-structure. We argue by induction on the rules of $\mathrm{ND}_{\mathrm{iCPL}}$ (selected rules):

* if the last rule is $\Gamma, A \vdash A$, then for all $w \in W$ and $\omega \in B_X$, if $w, \omega \Vdash_{\mathcal{M}}^X \Gamma, A$, then $w, \omega \Vdash_{\mathcal{M}}^X A$.

* if the last rule is

$$ \frac{\Gamma, d \vdash^{X \cup \{a\}} A \qquad \mu(d) \ge q}{\Gamma \vdash C_a^q A} $$

then by the I.H. together with Lemma A.12, for all $w \in W$, for all $\omega \in B_X$ and $\omega' \in 2^N$, if $w, \omega \Vdash_{\mathcal{M}}^X \Gamma$ and $w, \omega' \Vdash^{\{a\}} d$ (where the latter condition only depends on $\omega'$), then for all $w' \ge w$, we have $w', \omega + \omega' \Vdash_{\mathcal{M}}^{X \cup \{a\}} A$.

Since $\mu(d) \ge q$, we deduce that for all $w' \ge w$,

$$ \{\omega' \mid w', \omega + \omega' \Vdash_{\mathcal{M}}^{X \cup \{a\}} A\} $$

has measure greater than $q$, and we conclude then that $w, \omega \Vdash_{\mathcal{M}}^X C_a^q A$.

* if the last rule is

$$ \frac{\Gamma \vdash C_a^q A \qquad \Gamma, A \vdash^{X \cup \{a\}} C}{\Gamma \vdash C} (CE_1) \quad a \notin \mathrm{FN}(\Gamma, C) $$

let $w \in W$, $\omega \in (2^N)^X$ and $w, \omega \Vdash_{\mathcal{M}}^X \Gamma$. By I.H. we deduce that the set

$$ S := \{\omega' \mid w, \omega + \omega' \Vdash_{\mathcal{M}}^{X \cup \{a\}} A\} $$

has measure greater than $q > 0$, and it is thus non-empty. Let $\omega'$ be an element of $S$; again, by the I.H. we deduce that $w, \omega + \omega' \Vdash_{\mathcal{M}}^{X \cup \{a\}} C$; since $a \notin \mathrm{FN}(C)$, by Lemma A.14, we conclude then that $w, \omega \Vdash_{\mathcal{M}}^X C$.
* if the last rule is

$$ \frac{\Gamma \vdash C_a^q A \qquad \Gamma, A \vdash^{X \cup \{a\}} C}{\Gamma \vdash C_a^{qs} C} \quad (\mathrm{CE}_2) \quad a \notin \mathrm{FN}(\Gamma) $$

let $w \in W$, $\omega \in (2^N)^X$ and $w, \omega \Vdash_{\mathcal{M}}^X \Gamma$. By I.H. we deduce that the set

$$ S := \{ \omega' | w, \omega + \omega' \Vdash_{\mathcal{M}}^{X \cup \{a\}} A \} $$

has measure greater than $q \ge q_s$ and is contained in the set $S' := \{\omega' | w, \omega + \omega' \Vdash_{\mathcal{M}}^{X \cup \{a\}} C\}$. We can conclude then that $w, \omega \Vdash_{\mathcal{M}}^X C_a^{qs} C$.

* Axiom (C$\vee$) is valid: suppose $w, \omega \Vdash_{\mathcal{M}}^X C_a^q(A \vee B)$, where $a \notin \mathrm{FN}(A)$. Then the set $\{\omega' | w, \omega + \omega' \Vdash_{\mathcal{M}}^{X \cup \{a\}} A \vee B\}$ has measure greater than $q$. Observe that $w, \omega + \omega' \Vdash_{\mathcal{M}}^{X \cup \{a\}} A$ holds iff $w, \omega \Vdash_{\mathcal{M}}^X A$; so suppose $w, \omega \Vdash_{\mathcal{M}}^X A$ does not hold; then for any $\omega'$, $w, \omega + \omega' \Vdash_{\mathcal{M}}^{X \cup \{a\}} A$ does not hold, and thus the set $\{\omega' | w, \omega + \omega' \Vdash_{\mathcal{M}}^{X \cup \{a\}} B\}$ must have measure greater than $q$. We have thus proved that either $w, \omega \Vdash_{\mathcal{M}}^X A$ holds or $w, \omega \Vdash_{\mathcal{M}}^X C_a^q B$ holds, and thus that $w, \omega \Vdash^X A \vee C_a^q B$.

* Axiom (C$\bot$) is valid: suppose $\mathrm{FN}(\mathfrak{b}) \subseteq \{a\}$ and $\mu(\mathfrak{b}) < q$; for any $w \in W$, the set $\{\omega' | w, \omega' \Vdash_{\mathcal{M}}^{\{a\}} \mathfrak{b}\}$ coincides with $[\mathfrak{b}]$, and has thus measure $< q$ by hypothesis; we deduce that for any $w' \ge w, w', * \Vdash_{\mathcal{M}}^\emptyset C_a^q \mathfrak{b}$ does not hold, and we conclude that $w, * \Vdash_{\mathcal{M}}^\emptyset C_a^q \mathfrak{b}$.

□

To prove the completeness theorem we first need to study provability in iCPL a bit further.

**Definition A.16.** For any formula $A$ and finite set $X$, $|A|_X := \max\{i \mid \exists a \in X \cap \mathrm{FN}(A) \text{ s.t. } x_a^i \text{ occurs in } A\}$. We use $|A|$ as a shorthand for $|A|_{\mathrm{FN}(A)}$. For any $\omega \in (2^N)^{\mathcal{A}}$, $A^\omega := \mathrm{Th}_{\mathrm{FN}(A)}^{|A|}(\omega) \to A$.

We will exploit the following relativized version of the decomposition lemma (Lemma 3.3), which is proved in a similar way:

**Lemma A.17.** Let $A$ be a formula with $\mathrm{FN}(A) \subseteq X \cup Y$, where $X \cap Y = \emptyset$. Then there exist formulas $A_w^X$, with $\mathrm{FN}(A_w^X) \subseteq X$, where $w$ ranges over the valuations of the variables of name in $Y$ in $A$, such that $\vdash A \leftrightarrow (\bigvee_w \mathrm{Th}(w) \wedge A_w^X)$.

**Definition A.18.** For each formula $A$, with $\mathrm{FN}(A) \subseteq \{a\}$, let $\mathfrak{b}_A := \bigvee_v \{\mathrm{Th}(v) \mid A_v \not\vdash_{\mathrm{ND}_{iCPL}} \bot\}$.

From $A \vdash \bigvee_v \mathrm{Th}(v) \wedge A_v$ and $A \vdash \neg \mathrm{Th}(w)$ for all $\mathrm{Th}(w)$ not occurring in $\mathfrak{b}_A$, we can deduce $A \vdash \mathfrak{b}_A$. The following result shows that measuring the formula $\mathfrak{b}_A$ provides a test to know if $C_a^q A$ is consistent:

**Corollary A.19.** Let $A$ be a formula with $\mathrm{FN}(A) \subseteq \{a\}$. Then for all $q \in (0, 1]$, $\mu(\mathfrak{b}_A) < q \Rightarrow C_a^q A \vdash \bot$

*Proof.* The claim follows from the observation that $A \vdash \mathfrak{b}_A$ by applying Axiom (C$\bot$) and the rule (CE$_2$).

**Remark 2** (relativizing $\mathfrak{b}_A$ to $\omega$). Suppose $A$ is a formula with $\mathrm{FN}(A) \subseteq X \cup \{a\}$ (with $a \notin X$). Then for each $\omega \in (2^N)^{\mathcal{A}}$, let $A_\omega^X$ be $A_w^X$, where $w$ is the restriction of $\omega$ to $(2^{|A|})^X$. Then, by applying the construction from Lemma A.17 to $A_\omega^X$ we can define a Boolean formula $\mathfrak{b}_A^\omega$ with $\mathrm{FN}(\mathfrak{b}_A^\omega) \subseteq \{a\}$ such that $\mathrm{Th}_X^{|A|}(\omega) \vdash A \to \mathfrak{b}_A^\omega$ and such that $\mu(\mathfrak{b}_A^\omega) < q \Rightarrow \mathrm{Th}_X^{|A|}(\omega) \vdash \neg C_a^q A$.

The proof of the completeness theorem relies on the construction of a suitable “canonical model” based on sets of formulas. Let us first introduce some terminology. Let $\Gamma$ be a (possibly infinite) set of formulas. We say that $\Gamma$ is

* A-consistent if $\Gamma \not\vdash A$;

* consistent if it is $\bot$-consistent;

* super-consistent if for all $\omega \in (2^N)^{\mathcal{A}}$, $\mathrm{Th}(\omega) \cup \Gamma$ is consistent;

* closed if $A_1, \dots, A_n \in \Gamma$ and $A_1, \dots, A_n \vdash_{\mathrm{ND}_{iCPL}} A$ implies $A \in \Gamma$, and if $(d \to A)^\omega \in \Gamma$ and $\mu(d) \ge q$ then $(C_a^q A)^\omega \in \Gamma$.

Let $\Theta$ be the set of all super-consistent and closed sets of formulas $\Gamma$ satisfying the following conditions, for all $\omega \in (2^N)^{\mathcal{A}}$:

$$ (A \vee B)^\omega \in \Gamma \Rightarrow A^\omega \in \Gamma \text{ or } B^\omega \in \Gamma \qquad (\vee\text{-closure}) $$

$$ (C_a^q A)^\omega \in \Gamma \Rightarrow \exists d \text{ s.t. } \mu(d) \ge q \text{ and } (d \to A)^\omega \in \Gamma \qquad (\text{C-closure}) $$

The fundamental ingredient for the completeness theorem is the lemma below, which will be used to lift any consistent set of formulas to an element of $\Theta$.
**Lemma A.20** (saturation lemma). Let $\Gamma$ be a super-consistent set and let $\omega_0 \in (2^N)^{\mathcal{A}}$ be such that $\text{Th}(\omega_0) \cup \Gamma$ is A-consistent.
Then there exists a set $\Gamma^* \supseteq \Gamma$ such that $\Gamma^* \in \Theta$ and $\text{Th}_X(\omega_0) \cup \Gamma^*$ is A-consistent.

*Proof.* Let us fix an enumeration $(a_i)_{i \in \mathbb{N}}$ of all names. For any $p, q \in \mathbb{N}$, Let $\mathcal{F}_{p,q}$ be the set of all formulas $B$ such that $\text{FN}(B) \subseteq \{a_0, \dots, a_{q-1}\}$ and $|B| \le p$. Let us fix, for all $p, q \in \mathbb{N}$ an enumeration $(C_n^{p,q})_{n \in \mathbb{N}}$ of $\mathcal{F}_{p,q}$.

For any natural number $N$, let $[N] := \{0, \dots, N-1\}$. Given $p \le p'$ and $q \le q'$, and finite matrices $s \in (2^{[p+1]})[q+1]$ $s' \in (2^{[p'+1]})[q'+1]$, let $s \sqsubseteq s'$ if for all $i \le p$ and $j \le q$ $s(j)(i) = s'(j)(i)$. We will often indicate as $p_s$ and $q_s$ the (unique) natural numbers such that $s \in (2^{[p+1]})[q+1]$.

Moreover, for all $\omega \in (2^N)^X$, let $s \sqsubseteq \omega$ hold if for all $i \le p_s$ and $j \le q_s$, $s(j)(i) = \omega(a_j)(i)$.

Observe that if $s \sqsubseteq \omega$, $\text{Th}(\omega) \vdash \text{Th}(s)$.

For all $p, q$ and $s \in (2^{[p+1]})[q+1]$, we define a set of formulas $\Gamma^{\langle p,q,s \rangle} \subseteq \mathcal{F}_{p,q}$ such that for all $p \le p'$ and $q \le q'$, $s \in (2^{[p+1]})[q+1]$ and $s' \in (2^{[p'+1]})[q'+1]$, $s \sqsubseteq s'$ implies $\Gamma^{\langle p,q,s \rangle} \subseteq \Gamma^{\langle p',q',s' \rangle}$.

We let $\Gamma^{\langle p,q,s \rangle} := \bigcup_n \Gamma_n^{\langle p,q,s \rangle}$, where the sets $\Gamma_n^{\langle p,q,s \rangle}$ are defined by a triple induction on $p, q$ and $n$ as follows:

* if $p = q = 0$ and $b = \omega_0(0)$,

* $\Gamma_0^{\langle 0,0,b \rangle} := \Gamma \cup \{\neg^{(1-b)} x_0^0\}$;

* $\Gamma_{n+1}^{\langle 0,0,b \rangle} := \Gamma_n \cup \{C_n^{0,0}\}$, if this is A-consistent, and $\Gamma_{n+1}^{\langle 0,0,b \rangle} := \Gamma_n^{\langle 0,0,b \rangle}$ otherwise.

If $b \neq \omega_0(0)$, the definition is the same, with $\perp$ in place of $A$;

* if $p > 0$ and $q = 0$, $\Gamma^{\langle p,0,s \rangle} = \bigcup_n \Gamma_n^{\langle p,0,s \rangle}$, where if $s \sqsubseteq \omega_0$,

* $\Gamma_0^{\langle p,0,s \rangle} := \Gamma^{\langle p-1,0,s|_{p-1,0} \rangle} \cup \{\neg^{(1-s(p)(0))} x_p^0\}$;

* $\Gamma_{n+1}^{\langle p,0,s \rangle} := \Gamma_n^{\langle p,0,s \rangle} \cup \{C_n^{p,0}\}$ if this is A-consistent, and $\Gamma_{n+1}^{\langle p,0,s \rangle} := \Gamma_n^{\langle p,0,s \rangle}$ otherwise;

and if $s \not\sqsubseteq \omega_0$, the definition is similar, with $\perp$ in place of $A$;

* if $p = 0$ and $q > 0$, $\Gamma^{\langle 0,q,s \rangle} = \bigcup_n \Gamma_n^{\langle 0,q,s \rangle}$, where if $s \sqsubseteq \omega_0$,

* $\Gamma_0^{\langle 0,q,s \rangle} := \Gamma^{\langle 0,q-1,s|_{0,q-1} \rangle} \cup \{\neg^{(1-s(0)(q))} x_0^q\}$;

* $\Gamma_{n+1}^{\langle 0,q,s \rangle} := \Gamma_n^{\langle 0,q,s \rangle} \cup \{C_n^{0,q}\}$ if this is A-consistent, and $\Gamma_{n+1}^{\langle 0,q,s \rangle} := \Gamma_n^{\langle 0,q,s \rangle}$ otherwise;

and if $s \not\sqsubseteq \omega_0$, the definition is similar, with $\perp$ in place of $A$;

* if both $p > 0$ and $q > 0$, $\Gamma^{\langle p,q,s \rangle} = \bigcup_n \Gamma_n^{\langle p,q,s \rangle}$, where if $s \sqsubseteq \omega_0$,

* $\Gamma_0^{\langle p,q,s \rangle} := \Gamma^{\langle p-1,q,s|_{p-1,q} \rangle} \cup \Gamma^{\langle p,q-1,s|_{p,q-1} \rangle} \cup \{\neg^{(1-s(p)(q))} x_p^q\}$;

* $\Gamma_{n+1}^{\langle p,q,s \rangle} := \Gamma_n^{\langle p,q,s \rangle} \cup \{C_n^{p,q}\}$ if this is A-consistent, and $\Gamma_{n+1}^{\langle p,q,s \rangle} := \Gamma_n^{\langle p,q,s \rangle}$ otherwise;

and if $s \not\sqsubseteq \omega_0$, the definition is similar, with $\perp$ in place of $A$.

In the following, whenever this creates no confusion, we will indicate $\Gamma^{\langle p,q,s \rangle}$ simply as $\Gamma^s$.

For all finite matrices $s, s'$, the following hold:

a. $\text{Th}(s) \subseteq \Gamma^s$;

b. if $s \sqsubseteq \omega_0$, $\Gamma^s$ is A-consistent;

c. if $s \not\sqsubseteq \omega_0$, $\Gamma^s$ is consistent;

d. if $s \sqsubseteq s'$, $\Gamma^s \subseteq \Gamma^{s'}$;

e. if $\Gamma^s \supset B$, then for all $t \supseteq s$ such that $B \in \mathcal{F}_{p_t,q_t}$, $B \in \Gamma^t$.

Facts a.-d. are verified by construction, so we only prove e.: suppose there exist $B_1, \dots, B_n \in \Gamma^s$ such that $B_1, \dots, B_n \vdash_{\text{NDICPL}} B$ and let $t \supseteq s$ be such that $B \in \mathcal{F}_{p_t,q_t}$. Suppose $B \notin \Gamma^t$: then for some $k \in \mathbb{N}$, $\Gamma_k^t \cup \{B\} \vdash \perp$; yet, from d. it follows that $B_1, \dots, B_n \in \Gamma^t$, and thus $\Gamma^t \vdash \perp$, contradicting c.

Given matrices $s_1, \dots, s_n \sqsubseteq \omega$, let $\vee^\omega\{s_1, \dots, s_n\}$ indicate the smallest sub-matrix of $\omega$ extending all $s_1, \dots, s_n$ (i.e. the restriction of $\omega$ to $p = \max\{p_{s_1}, \dots, p_{s_n}\}$ and $q = \max\{q_{s_1}, \dots, q_{s_n}\}$).

For any matrix $s$, let $\Gamma^{\dagger s} = \{A^s \mid A \in \Gamma^s\} = \{\text{Th}(s) \to A \mid A \in \Gamma^s\}$. Let $\Gamma^\dagger = \bigcup_s \Gamma^{\dagger s}$ and let $\Gamma^* = \text{the deductive closure of } \Gamma^\dagger$. We will establish the following properties of $\Gamma^*$:

a. $\Gamma^*$ is super-consistent;

b. $\text{Th}(\omega_0) \cup \Gamma^*$ is A-consistent;

c. $\Gamma \subseteq \Gamma^*$;

d. if $B^\omega \notin \Gamma^*$ and $B^\omega = B^s$, then $\text{Th}(s) \cup \Gamma^* \cup \{B\} \vdash \perp$; moreover, if $B^{\omega_0} \notin \Gamma^*$ and $B^{\omega_0} = B^s$, then $\text{Th}(s) \cup \Gamma^* \cup \{B\} \vdash A$;

e. $\Gamma^*$ is $\vee$-closed;

f. $\Gamma^*$ is C-closed.

This will conclude the proof of the theorem.

Let us preliminarily observe that any formula $B^\omega$ can be written as $B^s$ for a unique $s \sqsubseteq \omega$ such that $p_s = |B|$ and $q_s$ is minimum with the property that $\text{FN}(B) \subseteq \{a_0, \dots, a_{q_s-1}\}$.
α. Let us show that $\Gamma^\dagger$ is super-consistent. This immediately implies that $\Gamma^*$ is super-consistent too. Suppose $\text{Th}(\omega) \cup \Gamma^\dagger \vdash \perp$; then there exist $s_1, \dots, s_n$ and $B_1 \in \Gamma^{s_1}, \dots, B_n \in \Gamma^{s_n}$, such that $\text{Th}(\omega), B_1^{s_1}, \dots, B_n^{s_n} \vdash \perp$; we can suppose w.l.o.g. that $s_1, \dots, s_n \sqsubseteq \omega$, since if $s_i \not\sqsubseteq \omega$, $\text{Th}(\omega) \vdash \neg \text{Th}(s_i)$, and thus $\text{Th}(\omega) \vdash B_i^{s_i}$.
We have then $B_i^{s_i} = B_i^\omega$; by letting $s = \bigvee^\omega \{s_1, \dots, s_n\}$ we thus have $B_i^{s_i} = B_i^s$ and $\text{Th}(s), B_1^s, \dots, B_n^s \vdash \perp$, which implies $\text{Th}(s), B_1, \dots, B_n \vdash \perp$, and since $\text{Th}(s) \cup \{B_1, \dots, B_n\} \subseteq \Gamma^s$, we deduce $\perp \in \Gamma^s$, contradicting a.

β. The argument is similar to the one for α.

γ. Let $B \in \Gamma$ and $s$ be such that $B^\omega = B^s, p_s = |B|$ and $\text{FN}(B) \subseteq \{a_0, \dots, a_{q_s-1}\}$. For any $s' \in (2^{[p_s+1]})^{[q_s+1]}$, $B^{s'} \in \Gamma^{\dagger s'} \subseteq \Gamma^\dagger$. Hence, using the fact that $\bigvee_{s \in (2^{[p_s+1]})^{[q_s+1]}} \text{Th}(s)$, we deduce that $\{B^s \mid s \in (2^{[p_s+1]})^{[q_s+1]}\} \vdash B$, and thus that $\Gamma^\dagger \vdash B$, which implies $B \in \Gamma^*$.

δ. Let $s$ be such that $B^\omega = B^s$. We consider the case of $\omega = \omega_0$; the case $\omega \neq \omega_0$ is proved similarly with $\perp$ in place of A. We will prove the contrapositive, i.e. that if $\text{Th}(s) \cup \Gamma^\dagger \cup \{B\}$ is A-consistent, then $B^{\omega_0} = B^s \in \Gamma^*$, from which $\delta$. follows. Suppose that $\text{Th}(\omega) \cup \Gamma^\dagger \cup \{B\}$ is A-consistent. Suppose $B \notin \Gamma^s$: this implies $B \notin \Gamma$ and that for some $k \in \mathbb{N}$, $\Gamma_k^s \cup \{B\} \vdash A$. But this forces then $\Gamma^s \cup \{B\} \vdash A$; since for all $F \in \Gamma^s$, $F^s \in \Gamma^\dagger$, and $\text{Th}(s)$, $F^s \vdash F$, we deduce then $\text{Th}(s) \cup \Gamma^\dagger \cup \{B\} \vdash A$, which is absurd. We conclude then that $B \in \Gamma^s$, and thus $B^s = B^\omega \in \Gamma^\dagger \subseteq \Gamma^*$.

ε. Again, we consider the case of $\omega = \omega_0$; the case $\omega \neq \omega_0$ is proved similarly with $\perp$ in place of A. Let $s \sqsubseteq \omega_0$ be such that $(B \vee C)^\omega = (B \vee C)^s$ and suppose $(B \vee C)^s \in \Gamma^*$ but neither $B^s \in \Gamma^*$ nor $C^s \in \Gamma^*$; then by $\delta$, $\text{Th}(s) \cup \Gamma^* \cup \{B\} \vdash A$ and $\text{Th}(s) \cup \Gamma^* \cup \{C\} \vdash A$, hence $\text{Th}(s) \cup \Gamma^* \cup \{B \vee C\} \vdash A$; since $(B \vee C)^s \in \Gamma^*$ we have $\text{Th}(s) \cup \Gamma^* \vdash B \vee C$, so we deduce $\text{Th}(s) \cup \Gamma^* \vdash A$, and since $\text{Th}(s) \subseteq \text{Th}(\omega_0)$, we have $\text{Th}(\omega_0) \cup \Gamma^* \vdash A$, contradicting $\beta$.

η. Once more, we consider the case of $\omega = \omega_0$; the case $\omega \neq \omega_0$ is proved similarly with $\perp$ in place of A.

Let $s \sqsubseteq \omega_0$ be such that $(C_a^q B)^{\omega_0} = (C_a^q B)^s$ and suppose $(C_a^q B)^s \in \Gamma^*$.

We can suppose w.l.o.g. that $a = a_q$ with $q > q_s$. Hence we can suppose that the formula $B^{\omega_0}$ is of the form $B^{s+s'+s''}$, for some finite matrices $s', s''$, with $s'' \in 2^{[B]+1}$.

By Lemma A.17 and Remark 2 we have that $\Gamma^s \vdash B \leftrightarrow (\bigvee_{v \in 2^{[B]+1}} \text{Th}(v) \wedge B_{s+v})$, where $B_{s+v}$ has no free name. Let $S = \{v \in 2^{[B]+1} \mid B_{s+v} \in \Gamma^s\}$ and $d = \bigvee_{v \in S} \text{Th}(v)$. Observe that for any $v \in S$, $\Gamma^{s+s'} \vdash \text{Th}(v) \rightarrow B$. Let $v \in S$ and $\omega_v$ be such that $v \subseteq \omega_v$. Then $\Gamma^{s+s'} \vdash \text{Th}(\omega_v) \rightarrow B$. Using e. we have then that for all $t \in 2^{[B]+1}$, $\text{Th}(\omega_v) \rightarrow B \in \Gamma^{s+s'+t}$, so in particular, $\text{Th}(\omega_v) \rightarrow B \in \Gamma^{s+s'+s''}$, so $(\text{Th}(\omega_v) \rightarrow B)^{\omega_0} \in \Gamma^\dagger \subseteq \Gamma^*$. We thus have that for all $v \in S$, $\Gamma^* \vdash (\text{Th}(v) \rightarrow B)^{\omega_0}$, which implies $\Gamma^* \vdash (d \rightarrow B)^{\omega_0}$ and thus $(d \rightarrow B)^{\omega_0} \in \Gamma^*$.

At this point, if $\mu(d) \ge q$ we are done. Otherwise, suppose $\mu(d) < q$; if $v \notin S$, then $B_{s+v} \notin \Gamma^s$, which implies that for some $k$, $\Gamma_k^s \cup \{B_{s+v}\} \vdash A$; this implies that $\Gamma^s \vdash (\text{Th}(v) \wedge B_{s+v}) \rightarrow A$; we deduce then that $\Gamma^s \vdash B \rightarrow ((\bigvee_{v \in S} \text{Th}(v) \wedge B_{s+v}) \vee A)$, and in particular that $\Gamma^s \vdash B \rightarrow (d \vee A)$; this means that there exist formulas $B_1, \dots, B_n \in \Gamma^s \subseteq \mathcal{F}_{p_s, q_s}$, hence containing no occurrences of the name $a$, such that $B_1, \dots, B_n \vdash B \rightarrow (d \vee A)$; from this we deduce first $\text{Th}(s)$, $B_1^s, \dots, B_n^s \vdash B \rightarrow (d \vee A)$, and then, using $(\text{CE}_2)$, $\text{Th}(s)$, $C_a^q B, B_1^s, \dots, B_n^s \vdash C_a^q (d \vee A)$. Now, since $s \subseteq \omega_0$, $C_a^q A, B_1^s, \dots, B_n^s \in \Gamma^*$ and $C_a^q (d \vee A) \vdash (C_a^q d) \vee A$ (Axiom (C$\vee$)), since we can suppose w.l.o.g. that $a \notin \text{FN}(A)$, we have $\text{Th}(\omega_0) \cup \Gamma^* \vdash (C_a^q d) \vee A$; moreover, from $\mu(d) < q$ we get (by Axiom (C$\perp$)) $\vdash \neg C_a^q d$ and thus $(C_a^q d) \vee A \vdash A$, so we can conclude $\text{Th}(\omega_0) \cup \Gamma^* \vdash A$, which contradicts $\beta$.

□

**Lemma A.21.** Let $\Gamma$ be an A-consistent set of formulas. Then there exists a super-consistent set $\Delta$ and $\omega \in (2^\mathbb{N})^\mathcal{A}$ such that $\text{Th}(\omega) \cup \Delta$ is A-consistent and its closure contains $\Gamma$.

*Proof.* Let us define sets of formulae $\Gamma_{a,i}$ together with $\omega(\langle a, i \rangle)$ as follows:

* let $\omega(\langle 0, 0 \rangle) = 1$ if $\Gamma \cup \{x_0^0\}$ is A-consistent, and $\omega(\langle 0, 0 \rangle) = 0$ otherwise; moreover, let $\Gamma_{0,0} = \Gamma$;

* let $\omega(\langle a, i+1 \rangle) = 1$ if $\Gamma_{a,i} \cup \{x_a^{i+1}\}$ is A-consistent, and $\omega(\langle a, i+1 \rangle) = 0$ otherwise; moreover, let $\Gamma_{a,i+1} = \Gamma_{a,i} \cup \{\neg(1-\omega(\langle a,i+1 \rangle))x_a^{i+1}\}$;

* let $\omega(\langle a+1, 0 \rangle) = 1$ if $\bigcup_i \Gamma_{a,i} \cup \{x_{a+1}^0\}$ is A-consistent, and $\omega(\langle a, i+1 \rangle) = 0$ otherwise; moreover, let $\Gamma_{a+1,0} = \bigcup_i \Gamma_{a,i} \cup \{\neg(1-\omega(\langle a+1,0 \rangle))x_{a+1}^0\}$.

By construction we then have that $\text{Th}(\omega) \cup \Gamma = \bigcup_{a,i} \Gamma_{a,i}$; let us show that $\bigcup_{a,i} \Gamma_{a,i}$ is A-consistent:

* $\Gamma_{0,0} = \Gamma$ is A-consistent by hypothesis;

* suppose $\Gamma_{a,i}$ is A-consistent; if $\Gamma_{a,i+1} = \Gamma_{a,i} \cup \{x_a^{i+1}\}$ then by construction $\Gamma_{a,i+1}$ is A-consistent; if $\Gamma_{a,i+1} = \Gamma_{a,i} \cup \{\neg x_a^{i+1}\}$ then by construction $\Gamma_{a,i} \cup \{x_a^i\} \vdash A$; if moreover $\Gamma_{a,i} \cup \{\neg x_a^i\} \vdash A$, the $\Gamma_{a,i} \cup \{x_a^i \vee \neg x_a^i\} \vdash A$ and thus $\Gamma_{a,i} \vdash A$, which is absurd. We conclude then that $\Gamma_{a,i+1}$ is A-consistent.

* suppose $\Gamma_{a,i}$ is A-consistent for all $i \in \mathbb{N}$; first observe that $\Gamma_a := \bigcup_i \Gamma_{a,i}$ is A-consistent: if $\Gamma_a \vdash A$, then there exist $B_1 \in \Gamma_{a,i_1}, \dots, B_n \in \Gamma_{a,i_n}$ such that $B_1, \dots, B_n \vdash A$; since for $j \le k$, $\Gamma_{a,j} \subseteq \Gamma_{a,k}$, we deduce that $\Gamma_{a,\max\{i_1, \dots, i_n\}} \vdash A$, which is absurd.
Now, if $\Gamma_{a+1,0} = \Gamma_a \cup \{x_{a+1}^0\}$ then by construction $\Gamma_{a+1,0}$ is A-consistent; if $\Gamma_{a+1,0} = \Gamma_a \cup \{\neg x_{a+1}^0\}$ then $\Gamma_a \cup \{x_{a+1}^0\} \vdash A$; hence, if $\Gamma_{a+1,0} \vdash A$, we deduce $\Gamma_a \cup \{x_{a+1}^0 \lor \neg x_{a+1}^0\} \vdash A$, so we conclude $\Gamma_a \vdash A$, which is absurd.

Now, for each formula $B \in \Gamma$ let us define a formula $B^*$ as follows:

$$B^* := B \lor \left( \bigvee_{a \in \mathrm{FN}(B), i \le |B|} \neg^{\omega((a,i))} x_a^i \right)$$

Observe that $\mathrm{Th}(\omega) \cup \{B^*\} \vdash B$ and that for all $\omega' \in (2^N)^{\mathcal{A}}$, $\mathrm{Th}(\omega') \cup \{B^*\}$ is consistent.

Let then $\Delta = \{B^* | B \in \Gamma\}$. It is clear that $\mathrm{Th}(\omega) \cup \Delta \vdash B$ for all $B \in \Gamma$. Suppose $\mathrm{Th}(\omega) \cup \Delta \vdash A$, then there exists Boolean formulas $e_1, \dots, e_k \in \mathrm{Th}(\omega)$ and formulas $B_1, \dots, B_n \in \Gamma$ such that $e_1, \dots, e_k, B_1^*, \dots, B_n^* \vdash A$. Since $B_i \vdash B^*$, this implies then $e_1, \dots, e_k, B_1, \dots, B_n \vdash A$, and thus $\mathrm{Th}(\omega) \cup \Gamma$ is not A-consistent, which is absurd. $\square$

We now have all elements to proceed to the proof of the completeness theorem.

**Theorem A.22 (completeness).** If $\Gamma \vdash A$, then $\Gamma \vdash_{\mathrm{ND}_{iCPL}} A$.

*Proof.* Let $\mathcal{T} = \langle \Theta, \subseteq, i \rangle$, where $i(p) = \{\Gamma \mid p \in \Gamma\}$.

We will prove that for all $\Gamma \in \Theta$ and $\omega \in \mathbf{B}_X$, $\Gamma, \omega \vdash_{\mathcal{G}}^X A$ iff $A^\omega \in \Gamma$. From this claim the theorem is proved as follows: suppose $\Gamma \nvdash A$; by Lemma A.21 we obtain a super-consistent set $\Delta$ and $\omega_0 \in (2^N)^{\mathcal{A}}$ such that $\mathrm{Th}(\omega_0) \cup \Delta$ is A-consistent and its closure contains $\Gamma$. By Lemma A.20 $\Delta$ extends to $\Gamma^* \in \Theta$ such that $\Gamma^* \supseteq \Gamma$ and $\mathrm{Th}(\omega_0) \cup \Gamma^*$ is A-consistent. Then using the claim, from $\Gamma \subseteq \Gamma^*$, we deduce that $\Gamma^*, \omega_0 \vdash_{\mathcal{G}}^X \Gamma$, and from $A \not\in \Gamma^*$ we deduce that $\Gamma^*, \omega_0 \not\vdash_{\mathcal{G}}^X A$; we can conclude then that $\Gamma \not\vdash_{\mathcal{G}}^X A$, and thus that $\Gamma \not\vdash A$.

Let us now prove the claim, by arguing by induction on A:

* if $A = \perp$, from the vacuous assumption $\Gamma, \omega \vdash_{\mathcal{G}}^X \perp$ we can freely deduce $\perp^\omega \in \Gamma$; conversely, from the vacuous assumption $\perp^\omega \in \Gamma$ we can freely deduce $\Gamma, \omega \vdash_{\mathcal{G}}^X \perp$;

* if $A = \top$, since $\Gamma, \omega \vdash_{\mathcal{G}}^X \top$ always holds and $\top^\omega \in \Gamma$ always holds (since $\Gamma$ is closed), we can conclude;

* if $A = p, \Gamma, \omega \vdash_{\mathcal{G}}^X p$ iff $p \in \Gamma$ holds by definition (since $p \notin \mathrm{Th}(\omega)$);

* if $A = x_a^i$, if $\Gamma, \omega \vdash_{\mathcal{G}}^X A$ holds then $\omega(a)(i) = 1$, hence $\mathrm{Th}(\omega) \vdash x_a^i$, and thus $A^\omega$ is logically valid, which implies $A^\omega \in \Gamma$ by closure; conversely, if $A^\omega \in \Gamma$, since $\mathrm{Th}(\omega) \cup \Gamma$ is consistent, the only possibility is that $\omega(a)(i) = 1$, which forces $\Gamma, \omega \vdash_{\mathcal{G}}^X A$.

* if $A = B \land C$, then $\Gamma, \omega \vdash_{\mathcal{G}}^X A$ iff $\Gamma, \omega \vdash_{\mathcal{G}}^X B$ and $\Gamma, \omega \vdash_{\mathcal{G}}^X C$, which by the I.H. is equivalent to $B^\omega \in \Gamma$ and $C^\omega \in \Gamma$, which is in turn equivalent to $(B \land C)^\omega \in \Gamma$.

* if $A = B \lor C$, and $\Gamma, \omega \vdash_{\mathcal{G}}^X A$, then either $\Gamma, \omega \vdash_{\mathcal{G}}^X B$ or $\Gamma, \omega \vdash_{\mathcal{G}}^X C$ holds; if the first holds, then by the I.H. $B^\omega \in \Gamma$, which implies $(B \lor C)^\omega \in \Gamma$, and one can argue similarly if the second holds; conversely, if $(B \lor C)^\omega \in \Gamma$, by $\lor$-closure either $B^\omega \in \Gamma$ or $C^\omega \in \Gamma$, so by the I.H. in each case we deduce $\Gamma, \omega \vdash_{\mathcal{G}}^X A$.

* if $A = B \rightarrow C$, then suppose that $\Gamma, \omega \vdash_{\mathcal{G}}^X A$; then for all $\Gamma' \in \Theta$ such that $\Gamma' \supseteq \Gamma$ and $\Gamma', \omega \vdash_{\mathcal{G}}^X B$, also $\Gamma', \omega \vdash_{\mathcal{G}}^X C$ holds. Suppose $\Gamma \cup \{B^\omega\}$ is super-consistent.

Furthermore, suppose $\mathrm{Th}(\omega) \cup \Gamma \cup \{B^\omega\} \nvdash C^\omega$; then, by Lemma A.20 (with $\omega_0 = \omega$ and $A = C$) there exists $\Gamma' \in \Theta$ with $\Gamma' \supseteq \Gamma \cup \{B^\omega\}$ such that $C^\omega \notin \Gamma'$. Using the I.H. we deduce then that $\Gamma', \omega \vdash_{\mathcal{G}}^X B$ but $\Gamma', \omega \not\vdash_{\mathcal{G}}^X C$, against the assumption. We conclude then that $\mathrm{Th}(\omega) \cup \Gamma \cup \{B^\omega\} \vdash C^\omega$, and thus that $\Gamma \vdash (B \rightarrow C)^\omega$, which implies by closure $(B \rightarrow C)^\omega \in \Gamma$. Suppose now that $\Gamma \cup \{B^\omega\}$ is not super-consistent. There exists $\omega'$ such that $\mathrm{Th}(\omega') \cup \Gamma \cup \{B^\omega\} \vdash \perp$. Since $\mathrm{Th}(\omega') \cup \Gamma$ is consistent the only possibility is that $\mathrm{Th}(\omega') \vdash \mathrm{Th}_{\mathrm{FN}(B)}^{|B|}(\omega)$ (which forces $\omega|_{|B|,\mathrm{FN}(B)}$ to coincide with $\omega'|_{|B|,\mathrm{FN}(B)}$) and $\mathrm{Th}(\omega') \cup \Gamma \cup \{B\} \vdash \perp$; but then we also have that $\mathrm{Th}(\omega) \cup \Gamma \cup \{B\} \vdash \perp$, which implies $\mathrm{Th}(\omega) \cup \Gamma \vdash B \rightarrow C$ and thus $\Gamma \vdash (B \rightarrow C)^\omega$; by closure this implies then $(B \rightarrow C)^\omega \in \Gamma$.

Conversely, suppose $(B \rightarrow C)^\omega \in \Gamma$ and let $\Gamma' \in \Theta$ be such that $\Gamma' \supseteq \Gamma$ and $\Gamma', \omega \vdash_{\mathcal{G}}^X B$; by the I.H. this implies $B^\omega \in \Gamma'$, and since $(B \rightarrow C)^\omega \in \Gamma \subseteq \Gamma'$ we also deduce by closure $C^\omega \in \Gamma'$, which by the I.H. implies $\Gamma'$, $\omega \vdash_{\mathcal{G}}^X C$.

* if $A = C_a^q B$, then suppose that $\Gamma, \omega \vdash_{\mathcal{G}}^X A$; then by the I.H. the Borel set

$$S = \{\omega' | B^{\omega+\omega'} \in \Gamma\} \supseteq \{\omega' | \Gamma, \omega + \omega' \vdash_{\mathcal{G}}^{X \cup \{a\}} B\}$$

has measure greater than $q$. Observe that for all $\omega' \in 2^N$, $B^{\omega+\omega'}$ is equivalent to

$$\mathrm{Th}_X^{|B|\times}(\omega|_X) \rightarrow (\mathrm{Th}_{\{a\}}^{|B|\{|a\}}(\omega') \rightarrow B)$$
<figure><img src="image_3.png" /><figcaption>Figure 11. Permutative rules of $ND_{iCPL_0}$.</figcaption></figure>

Let $d := \bigvee \{\text{Th}_{\{a\}}^{|B|_{\{a\}}} (\omega') | \omega' \in S\}$; since $\Gamma$ is closed, we deduce then that $(d \to B)^\omega \in \Gamma$ and that $\mu(d) \ge q$; again, by closure, this implies $(C_d^q B)^\omega \in \Gamma$.

For the converse direction, suppose $(C_d^q B)^\omega \in \Gamma$ and let $\Gamma' \supseteq \Gamma$; since $\Gamma$ is C-closed, there exists a Boolean formula $d$ with $\mu(d) \ge q$ such that $(d \to B)^\omega \in \Gamma \subseteq \Gamma'$. This implies that for all $\omega' \in [d]$, $B^{\omega+\omega'} \in \Gamma'$; hence, by the I.H. for all $\omega' \in [d]$, $\Gamma', \omega + \omega' \models_{\mathcal{G}}^{X \cup \{a\}} B$. Since $\mu(d) \ge q$, the set of $\omega'$ such that $\Gamma', \omega + \omega' \models_{\mathcal{G}}^{X \cup \{a\}} B$ has measure greater than $q$, and we can conclude $\Gamma, \omega \models_{\mathcal{G}}^{X} A$.

□

## A.5 Permutative Rules in iCPL₀.

We complete the picture of the normalization rules of iCPL₀ by considering permutative rules for (m), illustrated in Fig. 11, where we let $D_a^i(\mathcal{b}, c)$ be an abbreviation for $(x_a^i \wedge \mathcal{b}) \vee (\neg x_a^i \wedge c)$.

It is easily checked that if $\Pi \to \Sigma$, $t^\Pi \to \{\}^\Sigma$, since the rules closely correspond to the permutation rules for $\oplus$ in $\Lambda_{\text{PE}}^{\{\}}$.

## A.6 A “CbN” Proof-System.

The CHC described in Section 5 relates the proof-system $ND_{iCPL_0}$ with the type system $C\lambda_{\to}^{\{\}}$. In this subsection we describe a “CbN” variant $ND_{iCPL_0}^{\text{CbN}}$ of the proof-system $ND_{iCPL_0}$, for which it is possible to describe a CHC with the type system $C\lambda_{\to}$.

In the correspondence from Section 5, CbV application $\{t\}u$ plays a fundamental role, as it translates the elimination rule of the counting quantifier. To obtain a translation into $\Lambda_{\text{PE}}$ we thus need to restrict the rule (CE).

A sequent of $ND_{iCPL_0}^{\text{CbN}}$ is of the form $\Phi; \Gamma \vdash \mathcal{b} \to A$, where $\Phi$ and $\Gamma$ are two sets of formulas, and $\Phi$ contains at most one formula. The fundamental intuition is that the formula, if any, in $\Phi$, has to be used linearly in the proof.

The rules of $ND_{iCPL_0}^{\text{CbN}}$ are illustrated in Fig. 13. Observe that, contrarily to $ND_{iCPL_0}$ (see Section 3), the rules include a “multiplication rule” ($C \times$) to pass from $C^q C^s A$ to $C^{qs} A$.

$ND_{iCPL_0}^{\text{CbN}}$ proves less formulas than $ND_{iCPL_0}$. Indeed, the restricted (CE)-rule allows to deduce $C^q B$ from $C^q A$ only when $B$ can be deduced linearly from $A$. For example, one cannot reproduce in $ND_{iCPL_0}^{\text{CbN}}$ the proof of $C^q(A \to A) \to (A \to C^q A)$ illustrated in Section 3, since the hypothesis $C^q(A \to A)$, which is used as major premiss in a (CE)-rule, should be used twice. From the programming perspective, this means that one cannot encode in $ND_{iCPL_0}^{\text{CbN}}$ the non-linear “CbV” function $\lambda y.\lambda x.\{\lambda f.f(fx)\}y$.
* if $H[ ] = [ ]$, the claim is immediate;

* if $H[ ] = \lambda x.H'[ ]$, then we have $H[va.t] = \lambda x.H'[va.t] \xrightarrow{\text{IH}} \lambda x.va.H'[t] \xrightarrow{\text{→}_p} va.\lambda x.H'[t] = va.H[t]$;

* if $H[ ] = H'[ ]u$, then we have $H[va.t] = H'[va.t]u \xrightarrow{\text{IH}} (va.H'[t])u \xrightarrow{\text{→}_p} va.H'[t]u = va.H[t]$.

□

In other words, whenever $t$ is a function of the form $\lambda x.H[x]$ for some head context $H[ ]$, $C_b$N and $C_b$V application of $t$ coincide, since $tva.v)$ and $va.tv$ have the same normal form.

This property is reflected in the following:

**Lemma A.24.** For any head context $H[ ]$, the following rule is derivable in $C_{\lambda\to}$:

$$ \frac{\Gamma \vdash t : \mathfrak{b} \to C^{qs}\sigma \quad x : C^q\sigma, \Gamma \vdash H[x] : \mathfrak{b} \to C^r\tau}{\Gamma \vdash H[t] : \mathfrak{b} \to C^{rs}\tau} \quad \text{(head-subst)} $$

*Proof.* By induction on $H[ ]$:

* if $H[ ] = [ ]$, then it must be $q = r$, and the claim is then immediate;

* if $H[ ] = \lambda y.H'[ ]$, then $\tau = t \Rightarrow \tau'$ and we must have $x : C^q\sigma, \Gamma, y : t \vdash H'[x] : \mathfrak{b} \to C^q\tau'$. Then by IH we deduce $\Gamma, y : t \vdash H'[t] : \mathfrak{b} \to C^{rs}\tau'$, and finally $\Gamma \vdash H[t] : \mathfrak{b} \to C^{rs}\tau$.

* if $H[ ] = H'[ ]u$, then we must have $x : C^q\sigma, \Gamma \vdash H'[x] : \mathfrak{b} \to C^q(t \Rightarrow \tau)$ and $x : C^q\sigma, \Gamma \vdash u : \mathfrak{b} \to t$. Then by IH we deduce $\Gamma \vdash H'[t] : \mathfrak{b} \to C^{rs}(t \Rightarrow \tau)$, and we can thus conclude $\Gamma \vdash H[t] : \mathfrak{b} \to C^{rs}\tau$.

□

To any formula $A$ of $iCPL_0$, we associate a non-quantified type $\sigma_A$ and a positive real $|A| \in (0, 1] \cap \mathbb{Q}$ of $C_{\lambda\to}$, as follows:

$$ \begin{array}{l@{\qquad}l} \sigma_p := 0 & |o| := 1 \\ \sigma_{A \to B} := (C^{|A|}\sigma_A) \Rightarrow \sigma_B & |A \to B| = |B| \\ \sigma_{C^q A} := \sigma_A & |C^q A| = q \cdot |A| \end{array} $$

We let then $s_A := C^{|A|}\sigma_A$ (observe that $s_{C^q A} = C^{q \cdot |A|}\sigma_A$).

The translation of a derivation $\Pi$ of $\Phi$; $\Gamma \vdash \mathfrak{b} \to A$ into a typing derivation $D^\Pi$ of $s_\Phi$, $s_\Gamma \vdash t^\Pi : \mathfrak{b} \to s_A$ in $C_{\lambda\to}$ is illustrated in Fig. 15, where we exploit the fact that if $\Phi = \{A\}$ is non-empty, then $t^\Pi = t^\Pi[x : s_A]$ is a head context (as it can be checked by induction on the construction). We omit the case of the rule $(C_\times)$, as it follows immediately from the induction hypothesis, since $s_{C^q C^s A} = s_{C^{qs} A}$.

The stability of the translation under normalization is easily checked using Lemma A.23.

# B Details about the Probabilistic Event $\lambda$-Calculus.

## B.1 The Language $\Lambda_{\text{PE}}$.

Let us first comment on how Theorem 4.1 (i.e. confluence and strong normalization of $\to_{p}$, and confluence of $\to$) follows from confluence of $\to$ in the calculus from [16]. The $\lambda$-calculus in [16] slightly differs from our presentation of $\Lambda_{\text{PE}}$, since choice operators do not depend on indexes $i \in \mathbb{N}$. However, if $\varphi$ is any bijection from $\mathbb{N}^2$ to $\mathbb{N}$, one can define an invertible embedding $t \mapsto t^\varphi$ from $\Lambda_{\text{PE}}$ to the calculus in [16] by replacing $t \oplus_a^i u$ with $t^\varphi \oplus_{\varphi(a,i)} u^\varphi$ and $(va.t)^\varphi = v\varphi(a, 0)\dots.v\varphi(a, \text{ord}_a(t)).t^\varphi$, where $\text{ord}_a(t)$ is the maximum $i$ s.t. $\oplus_a^i$ occurs in $t$. Since the permutative rules in [16] translate into those in Fig. 4 under this translation, the results from [16] can be transported to our language.

We now discuss PNFs in $\Lambda_{\text{PE}}$.

**Definition B.1.** Let $S$ be a set of name-closed $\lambda$-terms and $a$ be a name. For all $i \in \mathbb{N} \cup \{-1\}$, the set of $(S, a)$-trees of level $i$ is defined as follows:

* any $t \in S$ is a $(S, a)$-tree of level $-1$;

* if $t, u$ are $(S, a)$-trees of level $j$ and $k$, respectively, and $j, k < i$, then $t \oplus_a^i u$ is a $(S, a)$-tree of level $i$.

The support of a $(S, a)$-tree $t$, indicated as $\text{Supp}(t)$, is the finite set of terms in $S$ which are leaves of $t$.

**Definition B.2.** The sets $\mathcal{T}$ and $\mathcal{V}$ of name-closed terms are defined inductively as follows:

* all variable $x \in \mathcal{V}$;

* if $t \in \mathcal{V}$, $\lambda x.t \in \mathcal{V}$;

* if $t \in \mathcal{V}$ and $u \in \mathcal{T}$, then $tu \in \mathcal{V}$;

* if $t \in \mathcal{V}$, then $t \in \mathcal{T}$;
<figure><img src="image_4.png" /><figcaption>**Figure 15.** Translation $\Pi \mapsto D^\Pi$ from $ND_{iCPL0}^{CbN}$ to $C\lambda_-$.</figcaption></figure>

* if $t$ is a $(\mathcal{T}, a)$-tree, then $va.t \in \mathcal{T}$.

**Lemma B.3.** For all name-closed term $t \in \mathcal{T}$, $t \in \mathcal{V}$ iff it does not start with $v$.

*Proof.* First observe that if $t = va.b$, then $t \notin \mathcal{V}$. For the converse direction, we argue by induction on $t \neq va.b$:

* if $t = x$ then $t \in \mathcal{V}$;

* if $t = \lambda x.u$ then by IH $u \in \mathcal{V}$, so $t \in \mathcal{V}$;

* if $t = uv$, then the only possibility is that $t \in \mathcal{V}$;

* if $t = u \oplus_a^i v$, then $t$ is not name-closed, again the hypothesis.

□

For all term $t$ and $a \in \text{FN}(t)$, we let $I_a(t)$ be the maximum index $i$ such that $\oplus_a^i$ occurs in $t$, and $I_a(t) = -1$ if $\oplus_a^i$ does not occur in $t$ for all index $i$.

We now show that Definition B.2 precisely captures PNF.

**Lemma B.4.** A name-closed term $t$ is in PNF iff $t \in \mathcal{T}$.

*Proof.* (⇒) We argue by induction on $t$. If $t$ has no bound name, then $t$ is obviously in $\mathcal{T}$. Otherwise:

* if $t = \lambda x.u$, then $u$ is also name-closed. Hence, by IH $u \in \mathcal{T}$; observe that $u$ cannot start with $v$ (as $t$ would not be normal) so by Lemma B.3, $u \in \mathcal{V}$, which implies $t \in \mathcal{T}$;

* if $t = uv$, then $u$ and $v$ are both name-closed, and so by induction $u, v \in \mathcal{T}$; if $u$ started with $v$, then $t$ would not be normal, hence, by Lemma B.3, $u \in \mathcal{V}$, and we conclude then that $t \in \mathcal{T}$.

* if $t = u \oplus_a^i v$, then it cannot be name-closed;

* if $t = va.u$, then we show, by a sub-induction on $u$, that $u$ is a $(\mathcal{T}, a)$-tree of level $I_a(u)$: first note that $I_a(u)$ cannot be $-1$, since otherwise $va.u \to_p u$, so $u$ would not be normal. We now consider all possible cases for $u$:

* $u$ cannot be a variable, or $I_a(u)$ would be $-1$;

* If $u = \lambda x.v$, then $I_a(v) = I_a(u)$ and so by sub-IH $v$ is a $(\mathcal{T}, a)$-tree of level $I_a(u)$, which implies that $u = \lambda x.v_1 \oplus_a^{I_a(u)} v_2$, which is not normal. Absurd.
* if $u = vw$, then let $J = I_a(u) = \max\{I_a(v), I_a(w)\}$ cannot be $-1$, since otherwise $I_a(u)$ would be $-1$. Hence $J \ge 0$ is either $I_a(v)$ or $I_a(w)$. We consider the two cases separately:

* if $J = I_a(v)$, then by sub-IH, $v = v_1 \oplus_a^J v_2$, and thus $u = (v_1 \oplus_a^J v_2)w$ is not normal;

* if $J = I_a(w)$, then by sub-IH, $w = w_1 \oplus_a^J w_2$, and thus $u = v(w_1 \oplus_a^J w_2)$ is not normal.

In any case we obtain an absurd conclusion.

* if $u = u_1 \oplus_a^i u_2$, then if $u_1, u_2$ are both in $\mathcal{V}$, we are done, since $u$ is a $(\mathcal{T}, a)$-tree of level $i = I_a(u)$. Otherwise, if $i < I_a(u)$, then $J = I_a(u) = \max\{I_a(v), I_a(w)\}$, so we consider two cases:

* if $J = I_a(v) > i$, then by sub-IH, $v = v_1 \oplus_a^J v_2$, and thus $u = (v_1 \oplus_a^J v_2) \oplus_a^i u_2$ is not normal;

* if $J = I_a(w) > i$, then by sub-IH, $w = w_1 \oplus_a^J w_2$, and thus $u = v \oplus_a^i (w_1 \oplus_a^J w_2)$ is not normal.

We conclude then that $i = I_a(u)$; we must then show that $I_a(v), I_a(w) < i$. Suppose first $I_a(v) \ge i$, then $(v_1 \oplus_a^J v_2) \oplus_a^i u_2$ is not normal. In a similar way we can show that $I_a(w) < i$.

* if $u = vb.v$, then $I_a(u) = I_a(v)$, so by sub-IH $v = v_1 \oplus_a^{I_a(u)} v_2$, and we conclude that $u = vb.v_1 \oplus_a^i v_2$ is not normal. ($\Leftarrow$ It suffices to check by induction on $t \in \mathcal{T}$ that it is in PNF. $\square$)

**Corollary B.5.** A name-closed term of the form $va.t$ is in PNF iff $t$ is a $(\mathcal{T}, a)$-tree of level $I_a(t) \ge 0$.

Let us conclude by discussing *randomized trees* and *head-reduction*. With any term $t$ we associate a labeled finitely branching tree RBT($t$) as follows:

* if $t \to_h^* u$, where $u = \lambda x_1. \dots \lambda x_n. y u_1 \dots u_n$ is a HNV, then RBT($t$) only consists of one node labeled $u$;

* if $t \to_h^* u$, where $u$ is a PNF of the form $va.T$, $T$ is a $(\mathcal{T}, a)$-tree and $\text{supp}(T) = \{u_1, \dots, u_n\}$, then RBT($t$) has root labeled $va.T$ and coincides with the syntactic tree of $T$, with leaves replaced by $RBT(u_1), \dots, RBT(u_n)$;

* otherwise, RBT($t$) has a root labeled $\Omega$ and no sub-trees.

**Proposition B.6.** If $t$ reduces to $u$ by either $\to_p$ or head $\beta$-reduction, then RBT($t$) $\subseteq$ RBT($u$).

A *randomized path* in RBT($t$) is any path $\pi$ in RBT($t$) starting from the root and ending in a leaf. A randomized path in RBT($t$) is thus of one of the following two forms:

1. a finite path $\pi = \langle va_1.T_1, va_2.T_2, \dots, va_N.T_N, \lambda x_1 \dots x_n.y \rangle$, where $v \rightsquigarrow va_{i+1}.T_{i+1}$ holds for some $v \in \text{supp}(T_i)$;

2. an infinite path $\pi = \langle va_1.T_1, va_2.T_2, \dots, va_n.T_n, \dots \rangle$, where $v \rightsquigarrow va_{i+1}.T_{i+1}$ holds for some $v \in \text{supp}(T_i)$.

With any such path $\pi$ we can associate an (either finite or infinite) list of words $b_i^\pi \in \{0, 1\}^*$, where $b_i^\pi$ is the list of choices leading from $va.T_i$ to the unique term $v \in \text{supp}(T_i)$ such that $v \rightsquigarrow va_{i+1}.T_{i+1}$.

If $\pi$ is a finite randomized path in RBT($t$) ending in some $u \in \mathcal{V}$, we say that $\pi$ is a randomized path from $t$ to $u$ (noted $\pi : t \mapsto u$).

Let us consider the (unique) Borel $\sigma$-algebra $\mu$ on $2^{\mathbb{N} \times \mathbb{N}}$ satisfying $\mu(C_{i,j}) = 1/2$, where $C_{i,j}$ is the cylinder $\{\omega \mid \omega(i, j) = 1\}$.

Any randomized path $\pi$ yields a Borel set $B_\pi := \bigcap_{i,j} C_{i,(b_\pi^i)_j}$, so that two distinct paths $\pi \ne \pi'$ are such that $B_\pi \cap B_{\pi'} = \emptyset$.

Moreover, if $\pi$ is finite, the Borel set $B_\pi$ is captured by the Boolean formula $\mathfrak{b}_\pi := \bigwedge_i \mathfrak{b}_\pi^i$, where $\mathfrak{b}_\pi^i = \bigwedge_j (\neg)^{1+(b_\pi^i)_j} x_{a_i}^j$.

**Lemma B.7.** For all terms $t \in \mathcal{T}$ and $u \in \mathcal{V}$, $\mathcal{D}_t(u) = \mu(\bigcup\{B_\pi \mid \pi : t \mapsto u\}) = \sum_{\pi:t \mapsto u} \mu(\mathfrak{b}_\pi)$.

**Lemma B.8.** For all $t \in \mathcal{T}$, the following are equivalent:

(i.) $t$ has a head-normal form;

(iii.) RBT($t$) is finite.

*Proof.* (i.)$\Rightarrow$ (iii.) is proved by induction on the length of a reduction of $t$ to a head-normal form. For (iii.)$\Rightarrow$ (i.), observe that RBT($t$) contains an infinite path only if $t$ admits an infinite head-reduction. From (iii.) we deduce then that all head reductions of $t$ are finite, so $t$ has a head-normal form. $\square$

## B.2 The Language $\Lambda_{\text{PE}}^{\{\}}$.

In this section we study some properties of reduction $\to^{\{\}}$ in the calculus $\Lambda_{\text{PE}}^{\{\}}$. Most arguments closely resemble arguments from [16], so we omit several details.

**Lemma B.9.** $\to^{p\{\}}$ is strongly normalizing.
**Proof.** We follow the proof of [[16], Lemma 7], we define the partial order $<_M$ by

<table><tr><td>$\oplus_a^i <_M \oplus_b^j$</td><td>if $(a, i) <_M (b, j)$</td></tr><tr><td>$\oplus_a^i <_M v_b$</td><td>for all labels $a, b$</td></tr><tr><td>$v_a <_M @, \lambda x$</td><td>for any label $b$</td></tr><tr><td>$@, \lambda x <_M \{\}$</td><td></td></tr></table>

One can check then that the well-founded recursive path ordering $<_M$ defined by

$$ t < u \iff \begin{cases} [t_1, \dots, t_n] < [u_1, \dots, u_m] & \text{if } f = g \\ [t_1, \dots, t_n] < [u] & \text{if } f <_M g \\ [t] \le [u_1, \dots, u_m] & \text{if } f \not<_B g \end{cases} $$

where $t = f(t_1, \dots, t_n)$ and $u = g(u_1, \dots, u_n)$, with $f, g \in \{\oplus_a^i, v_a, @, \lambda x, \{\}\}$, is such that $t \to_{\to p\{\}} u$ implies $u < t$. $\square$

**Lemma B.10.** $\to_{\to p\{\}}$ is confluent.

**Proof.** By Lemma B.9 and Newman's Lemma, it suffices to check local confluence. All rules from $(c_1)$ to $(\oplus v)$ from Fig. 4, as well as rules $(\{\} \oplus_1)$ and $(\{\} \oplus_2)$, can be written under the general form

$$ C[t \oplus_a^i u] \to_{\to p\{\}} C[t] \oplus_a^i C[u] \qquad (\oplus \star) $$

where $C[ ]$ is defined by the grammar

$$ C[ ] ::= [ ] | \lambda x.C[ ] | C[ ] u | tC[ ] | C[ ] \oplus_a^i u | t \oplus_a^i C[ ] | v_a.C[ ] | \{C[ ]\}u | \{t\}C[ ] $$

We consider all rules against each other. All cases involving $(\oplus \star)$ can be treated as in the proof of [[16], Lemma 9]. Beyond these, the only new case with respect to those treated in [[16], Lemma 9] is the one below:

$$ \begin{array}{rcl} \{t\}va.u \oplus_b^i v & \xrightarrow{\oplus v} & \{t\}(va.u) \oplus_b^i (va.v) \\ \downarrow^{\{\}v} & & \downarrow^{\{\} \oplus_1} \\ va.t(u \oplus_b^i v) & & \{t\}va.u \oplus_b^i \{t\}va.v \\ \downarrow^{\oplus a} & & \downarrow^{\{\}v} \\ va.(tu) \oplus_b^i (tv) & \xrightarrow{\oplus v} & (va.tu) \oplus_b^i (va.tv) \end{array} $$

**Theorem B.11.** $\to_{\to p\{\}}$ is confluent.

**Proof.** The argument closely follows the one from [[16], pp. 9-12], using the observation that none of the permutations $(\{\}v)$-$(\{\} \oplus_2)$ can either block a $\beta$-redex or figure in a critical pair with a $\beta$-redex (in other words, $\beta$-reduction commutes with $(\{\}v)-(\{\} \oplus_2)$). $\square$

To conclude, let us study head-reduction $\to_{\to p\{\}}$ in $\Lambda_{\mathrm{PE}}^{\{\}}$.

Randomized contexts $R[ ]$ for $\Lambda_{\mathrm{PE}}^{\{\}}$ are defined as for $\Lambda_{\mathrm{PE}}$. Head-contexts $H[ ]$ for $\Lambda_{\mathrm{PE}}$ are defined by the grammar below:

$$ H[ ] := [ ] | \lambda x.H[ ] | H[ ] u | \{H[ ]\}u $$

Head-reductions $t \to_{\to p\{\}} u$ are defined inductively as being either a $\to_{\to p\{\}}$-reduction or a $\beta$-reduction of one of the following two forms

$$ \begin{array}{l} R[H[(\lambda y.t)u]] \to_{\beta} R[H[t[u/y]]] \\ R[H[\{t\}u]] \to R[H[\{t\}u')] \end{array} $$

where $u \to_{\to p\{\}} u'$.

Let $\mathcal{T}^{\{\}}$ be the set of PNF with respect to $\to_{\to p\{\}}$. A pseudo-value $t$ is a PNF which is either a $\lambda$, a variable, an application $tu$ or a CbV application $\{t\}u$. We let $\mathcal{V}^{\{\}}$ indicate the set of pseudo-values.

The definition of $\pi_X^{\omega}(t)$ is extended from $\Lambda_{\mathrm{PE}}$ to $\Lambda_{\mathrm{PE}}^{\{\}}$ simply by adding the condition $\pi_X^{\omega}(\{t\}u) = \{\pi_X^{\omega}(t)\}\pi_X^{\omega}(u)$. In this way, a sub-distribution $\mathcal{D}_t : \mathcal{V}^{\{\}} \to [0, 1]$ can be defined as in Section 3.
**Lemma B.12.** A pseudo-value $t \in \mathcal{V}^{\{\}}$ is in head normal form iff either $t = \mathbb{H}[x]$ or $t = \mathbb{H}[\{t\}u]$, where $u \in \mathcal{V}^{\{\}}$ and is $\to^{\{\}}$-normal.

A head normal value is defined as in $\Lambda_{\text{PE}}$ as a pseudo-value in head normal form. We let $\text{HNV}^{\{\}}$ indicate the set of head normal values. Using Lemma B.12 we can define, in analogy with the case of $\Lambda_{\text{PE}}$, the functions $\text{HNV}(t) := \sum_{v \in \text{HNV}^{\{\}}}{\mathcal{D}_t(v)}$, and $\text{HNV}_{\to^{\{\}}}(t) := \sup\{\text{HNV}(u) \mid t \to^{\{\}} u\}$.

# C Details about $C\lambda_{\to^{\{\}}}$.

## C.1 Subject Reduction.

The goal of this section is to establish the following result:

**Proposition C.1 (Subject Reduction).** If $\Gamma \vdash^X t : \mathfrak{b} \to \mathfrak{s}$ and $t \to^{\{\}} u$, then $\Gamma \vdash^X u : \mathfrak{b} \to \mathfrak{s}$.

With the goal of making proof slightly simpler, in the formulation of $C\lambda_{\to^{\{\}}}$ we replace the rule $(\oplus)$ with the two rules $(\oplus l)$ and $(\oplus r)$ below:

$$ \frac{\Gamma \vdash^{X \cup \{a\}} t : c \to \mathfrak{s} \qquad \mathfrak{b} \vdash c \wedge x_a^i}{\Gamma \vdash^{X \cup \{a\}} t \oplus_a^i u : \mathfrak{b} \to \mathfrak{s}} \quad (\oplus l) $$

$$ \frac{\Gamma \vdash^{X \cup \{a\}} u : c \to \mathfrak{s} \qquad \mathfrak{b} \vdash c \wedge \neg x_a^i}{\Gamma \vdash^{X \cup \{a\}} t \oplus_a^i u : \mathfrak{b} \to \mathfrak{s}} \quad (\oplus r) $$

It is easily checked that, in presence of the rule $(\vee)$, having the rule $(\oplus)$ is equivalent to having the rules $(\oplus l)$ and $(\oplus r)$.

To establish the subject reduction property, we first need to establish a few auxiliary lemmas.

**Lemma C.2.** If $\Gamma \vdash^X t : \mathfrak{b} \to \mathfrak{s}$ and $X \subseteq Y$, then $\Gamma \vdash^Y t : \mathfrak{b} \to \mathfrak{s}$.

*Proof.* By induction on a type derivation of $t$.

**Lemma C.3.** If $\Gamma \vdash^X t : \mathfrak{b} \to \mathfrak{s}$ holds and $c \vdash^X \mathfrak{b}$, then $\Gamma \vdash^X t : c \to \mathfrak{s}$ is derivable by a derivation of the same length.

*Proof.* By induction on a type derivation of $t$.

**Lemma C.4 (substitution lemma).** The following rule is derivable:

$$ \frac{\Gamma, x : s \vdash^X t : c \to t \qquad \Gamma \vdash^X u : d \to s \qquad \mathfrak{b} \vdash c \wedge d}{\Gamma \vdash^X t[u/x] : \mathfrak{b} \to t} \quad (\text{subst}) $$

*Proof.* We argue by induction on the typing derivation of $t$:

* if the last rule is

$$ \frac{\mathrm{FN}(\mathfrak{b}) \subseteq X}{\Gamma, x : s \vdash^X x : c \to s} \quad (\mathrm{id}) $$

then $t[u/x] = u$, so the claim can be deduced using Lemma C.3.

* if the last rule is

$$ \frac{\{\Gamma, x : s \vdash^X t : c_i \to t\}_i \qquad c \vdash^X \bigvee_i c_i}{\Gamma, x : s \vdash^X x : c \to t} \quad (\vee) $$

Then, by IH, we deduce $\Gamma, x : s \vdash^X t[u/x] : c_i \wedge d \to t$, and since $\mathfrak{b} \vdash^X \bigvee_i (c_i \wedge d)$ we conclude by applying an instance of $(\vee)$.

* if the last rule is

$$ \frac{\Gamma, x : s \vdash^{X \cup \{a\}} t_1 : c' \to t \qquad c \vdash^{X \cup \{a\}} x_a^i \wedge c'}{\Gamma, x : s \vdash^{X \cup \{a\}} t_1 \oplus_a^i t_2 : c \to t} \quad (\oplus l) $$

Then, by IH, we deduce $\Gamma \vdash^{X \cup \{a\}, q} t_1[u/x] : c' \wedge d$. From $t[u/x] = (t_1[u/x]) \oplus_a^i (t_2[u/x])$ and the fact that $\mathfrak{b} \vdash^{X \cup \{a\}} x_a^i \wedge (c' \wedge d)$, we deduce the claim by an instance of the same rule.

* if the last rule is

$$ \frac{\Gamma, x : s \vdash^{X \cup \{a\}} t_2 : c' \to t \qquad c \vdash^{X \cup \{a\}} \neg x_a^i \wedge c'}{\Gamma, x : s \vdash^{X \cup \{a\}} t_1 \oplus_a^i t_2 : c \to t} \quad (\oplus r) $$

we can argue similarly to the previous case.

* if the last rule is

$$ \frac{\Gamma, y : t', x : s \vdash^X t' : c \to C\bar{q}\tau}{\Gamma, x : s \vdash^X \lambda y.t' : c \to C\bar{q}(t' \Rightarrow \tau)} \quad (\lambda) $$
Then, by IH, we deduce $\Gamma, y : t' \vdash^X t'[u/x] : \mathfrak{b} \to C^{\bar{q}}\tau$ and since $t[u/x] = (\lambda y.t')[u/x] = \lambda y.t'[u/x]$ we conclude by applying an instance of the same rule.

* if the last rule is

$$ \frac{\Gamma, x : s \vdash^X t_1 : c_1 \to C^{\bar{q}}(t' \Rightarrow \tau) \qquad \Gamma, x : s \vdash^X t_2 : c_2 \to t' \qquad c \models^X c_1 \wedge c_2}{\Gamma, x : s \vdash^X t_1 t_2 : c \to C^{\bar{q}}\tau} (@) $$

Then, by IH, we deduce $\Gamma \vdash^X t_1[u/x] : c_1 \wedge d \to C^{\bar{q}}(t' \Rightarrow \tau)$ and $\Gamma \vdash^X t_2[u/x] : c_2 \wedge d \to t'$, and since $(t_1 t_2)[u/x] = (t_1[u/x])(t_2[u/x])$ and $\mathfrak{b} \models^X (c_1 \wedge d) \wedge (c_2 \wedge d)$, we conclude by applying an instance of the same rule.

* if the last rule is

$$ \frac{\Gamma, x : s \vdash^X t_1 : c_1 \to C^{\bar{q}}(t' \Rightarrow \tau) \qquad \Gamma, x : s \vdash^X t_2 : c_2 \to C^s t' \qquad c \models^X c_1 \wedge c_2}{\Gamma, x : s \vdash^X \{t_1\} t_2 : c \to C^s C^{\bar{q}}\tau} (\{\}) $$

Then, by IH, we deduce $\Gamma \vdash^X t_1[u/x] : c_1 \wedge d \to C^{\bar{q}}(t' \Rightarrow \tau)$ and $\Gamma \vdash^X t_2[u/x] : c_2 \wedge d \to C^s t'$, and since $\{t_1\} t_2[u/x] = \{t_1[u/x]\} (t_2[u/x])$ and $\mathfrak{b} \models^X (c_1 \wedge d) \wedge (c_2 \wedge d)$, we conclude by applying an instance of the same rule.

* if the last rule is

$$ \frac{\Gamma, x : s \vdash^{X \cup \{a\}} t : c' \wedge e \to t \qquad \mu(e) \geq s \qquad c \models^X c'}{\Gamma, x : s \vdash^X va.t : c \to C^s t} (\mu) $$

Then, by IH, $\Gamma \vdash^{X \cup \{a\}} t[u/x] : (c' \wedge d) \wedge e_i \to t$. Hence, from the fact that $\mathfrak{b} \models^X c \wedge d$ and that $a$ cannot occur in $d$, and since $(va.t)[u/x] = va.t[u/x]$, we can deduce the claim by applying an instance of the same rule.

□

We now have all ingredients to establish the subject reduction property of $C\lambda_{\to}^{}$.

*Proof of Proposition C.1.* First observe that if the typing derivation $D$ of $t$ ends by a ($\lor$)-rule, it suffices to establish the property for the immediate sub-derivations of $D$ and then apply an instance of ($\lor$)-rule to the resulting derivations. So we will always suppose that the typing derivation of $D$ does not end by a ($\lor$)-rule.

For the case of $\beta$-reduction it suffices to check the claim when $t$ is a redex $(\lambda x.t_1)t_2$ and $u$ is $t_1[t_2/x]$. From $\Gamma \vdash^X t : \mathfrak{b} \to s$ we can suppose w.l.o.g. that the typing derivation is as below:

$$ \frac{\left( \frac{\left\{ \Gamma, x : t \vdash^X t_1 : c_i \to C^{\bar{q}}\sigma \right\}_i}{\Gamma \vdash^X \lambda x.t_1 : c_i \to C^{\bar{q}}(t \Rightarrow \sigma)} \right)}{\Gamma \vdash^X \lambda x.t_1 : \mathfrak{b}_1 \to C^{\bar{q}}(t \Rightarrow \sigma)} (\lor) \qquad \frac{\left( \left\{ \Gamma \vdash^X t_2 : d_j \to t \right\}_j \right)}{\Gamma \vdash^X t_2 : \mathfrak{b}_2 \to t} (\lor) \qquad \mathfrak{b}_1 \models \bigvee_i c_i \qquad \mathfrak{b}_2 \models \bigvee_j d_j \qquad \mathfrak{b} \models \mathfrak{b}_1 \wedge \mathfrak{b}_2 $$

From Lemma C.4 we deduce the existence of derivations of $\Gamma \vdash^X u : c_i \wedge d_j \to C^{\bar{q}}\sigma$; from $\mathfrak{b} \models^X \mathfrak{b}_1 \wedge \mathfrak{b}_2$ we deduce then $\mathfrak{b} \models^X \bigvee_{i,j} c_i \wedge d_j$, using the fact that $\bigvee_i c_i \wedge \bigvee_j d_j \equiv \bigvee_{i,j} c_i \wedge d_j$. We can thus conclude as follows:

$$ \frac{\{\Gamma \vdash^X u : c_i \wedge d_j \to C^{\bar{q}}\sigma\}_{i,j}}{\Gamma \vdash^X u : \mathfrak{b} \to C^{\bar{q}}\sigma} (\lor) $$

For the case of $\to_{p\{\}}$ we consider reduction rules one by one.

$(t \oplus_a^i t \to_{p\{\}} t)$ The last rule of $t$ is either

$$ \frac{\Gamma \vdash^X t : \mathfrak{b}' \to s \qquad \mathfrak{b}' \models^X x_a^i \wedge \mathfrak{b}'}{\Gamma \vdash^X t \oplus_a^i t : \mathfrak{b} \to s} (\oplus l) $$

or

$$ \frac{\Gamma \vdash^X t : \mathfrak{b}' \to s \qquad \mathfrak{b}' \models^X \neg x_a^i \wedge \mathfrak{b}'}{\Gamma \vdash^X t \oplus_a^i t : \mathfrak{b} \to s} (\oplus r) $$

Then, in either case, from $\Gamma \vdash^X t : \mathfrak{b}' \to s$, $\mathfrak{b}' \models^X \mathfrak{b}'$, using Lemma C.3 we deduce $\Gamma \vdash^X t : \mathfrak{b} \to s$.

((t \oplus_a^i u) \oplus_a^i v \to_{p\{\}} t \oplus_a^i v) There are three possible sub-cases:

1. the type derivation is as follows:

$$ \frac{\frac{\Gamma \vdash^X t : \mathfrak{b}'' \to s \qquad \mathfrak{b}'' \models^X x_a^i \wedge \mathfrak{b}''}{\Gamma \vdash^X t \oplus_a^i u : \mathfrak{b}' \to s} (\oplus l)}{\Gamma \vdash^X (t \oplus_a^i u) \oplus_a^i : \mathfrak{b} \to s} (\oplus l) $$
Then from $\Gamma \vdash^X t : \mathfrak{b}'' \to s$ and since we have $\mathfrak{b} \vdash^X x_a^i \wedge \mathfrak{b}''$ we deduce $\Gamma \vdash^X t \oplus_a^i v : \mathfrak{b} \to s$.

2. the type derivation is as follows:

$$ \frac{\Gamma \vdash^X u : \mathfrak{b}'' \to s \qquad \mathfrak{b}' \vdash^X \neg x_a^i \wedge \mathfrak{b}''}{\Gamma \vdash^X t \oplus_a^i u : \mathfrak{b}' \to s \qquad \mathfrak{b} \vdash^X x_a^i \wedge \mathfrak{b}'} (\oplus r) $$ $$ \frac{\Gamma \vdash^X (t \oplus_a^i u) \oplus_a^i v : \mathfrak{b} \to s}{\Gamma \vdash^X (t \oplus_a^i v) : \mathfrak{b} \to s} (\oplus l) $$

Then, from $\mathfrak{b} \vdash^X x_a^i \wedge \mathfrak{b}'$ and $\mathfrak{b}' \vdash^X \neg x_a^i \wedge \mathfrak{b}''$ we deduce $\mathfrak{b} \vdash^X \perp$, so we conclude $\Gamma \vdash^X (t \oplus_a^i v) : \mathfrak{b} \to s$ using one of the initial rules.

3. the type derivation is as follows:

$$ \frac{\Gamma \vdash^X v : \mathfrak{b}'' \to s \qquad \mathfrak{b} \vdash^X \neg x_a^i \wedge \mathfrak{b}''}{\Gamma \vdash^X (t \oplus_a^i u) \oplus_a^i v : \mathfrak{b} \to s} (\oplus r) $$

Then from $\Gamma \vdash^X u : \mathfrak{b}' \to s$ and $\mathfrak{b} \vdash^X \neg x_a^i \wedge \mathfrak{b}''$ we deduce $\Gamma \vdash^X t \oplus_a^i v : \mathfrak{b} \to s$.

$(t \oplus_a^i (u \oplus_a^i v) \to_{\mathfrak{p}\{\}} t \oplus_a^i v)$ Similar to the case above.

$(\lambda x.(t \oplus_a^i u) \to_{\mathfrak{p}\{\}} (\lambda x.t) \oplus_a^i (\lambda x.u))$ There are two possible sub-cases:

$$ 1. \quad \frac{\Gamma, x : s \vdash^X t : \mathfrak{b}' \to C\bar{q}\tau \qquad \mathfrak{b} \vdash^X x_a^i \wedge \mathfrak{b}'}{(\oplus l)} $$ $$ \frac{\Gamma, x : s \vdash^X t \oplus_a^i u : \mathfrak{b} \to C\bar{q}\tau}{\Gamma \vdash^X \lambda x.(t \oplus_a^i u) : \mathfrak{b} \to C\bar{q}(s \Rightarrow \tau)} (\lambda) $$

Then, we deduce

$$ \frac{\Gamma, x : s \vdash^X t : \mathfrak{b}' \to C\bar{q}\tau \qquad (\lambda)}{\Gamma \vdash^X \lambda x.t : \mathfrak{b}' \to C\bar{q}(s \Rightarrow \tau) \qquad \mathfrak{b} \vdash^X x_a^i \wedge \mathfrak{b}'} (\oplus l) $$ $$ \frac{\Gamma \vdash^X (\lambda x.t) \oplus_a^i (\lambda x.u) : \mathfrak{b} \to C\bar{q}(s \Rightarrow \tau)}{\Gamma \vdash^X (\lambda x.t) \oplus_a^i (\lambda x.u) : \mathfrak{b} \to C\bar{q}(s \Rightarrow \tau)} (\oplus l) $$

$$ 2. \quad \frac{\Gamma, x : s \vdash^X u : \mathfrak{b}' \to C\bar{q}\tau \qquad \mathfrak{b} \vdash^X \neg x_a^i \wedge \mathfrak{b}'}{(\oplus r)} $$ $$ \frac{\Gamma, x : s \vdash^X t \oplus_a^i u : \mathfrak{b} \to C\bar{q}\tau}{\Gamma \vdash^X \lambda x.(t \oplus_a^i u) : \mathfrak{b} \to C\bar{q}(s \Rightarrow \tau)} (\lambda) $$

Then, we can argue similarly to the previous case.

((t \oplus_a^i u)v \to_{\mathfrak{p}\{\}} (tv) \oplus_a^i (uv)) There are two possible sub-cases:

$$ 1. \quad \frac{\Gamma \vdash^X t : \mathfrak{b}'' \to C\bar{q}(s \Rightarrow \tau) \qquad \mathfrak{b}' \vdash^X x_a^i \wedge \mathfrak{b}''}{\Gamma \vdash^X t \oplus_a^i u : \mathfrak{b}' \to C\bar{q}(s \Rightarrow \tau) \qquad \Gamma \vdash^X v : c \to s \qquad \mathfrak{b} \vdash^X \mathfrak{b}' \wedge c} (\oplus l) $$ $$ \frac{\Gamma \vdash^X (t \oplus_a^i u)v : \mathfrak{b} \to C\bar{q}\tau}{\Gamma \vdash^X (t \oplus_a^i u)v : \mathfrak{b} \to C\bar{q}\tau} (\text{@}) $$

Then, we deduce

$$ \frac{\Gamma \vdash^X t : \mathfrak{b}'' \to C\bar{q}(s \Rightarrow \tau) \qquad \Gamma \vdash^X v : c \to s \qquad \mathfrak{b}' \wedge c \vdash^X \mathfrak{b}'' \wedge c}{\Gamma \vdash^X tv : \mathfrak{b}' \wedge c \to C\bar{q}\tau \qquad \mathfrak{b} \vdash^X x_a^i \wedge \mathfrak{b}' \wedge c} (\text{@}) $$ $$ \frac{\Gamma \vdash^X (tv) \oplus_a^i (uv) : \mathfrak{b} \to C\bar{q}\tau}{\Gamma \vdash^X (tv) \oplus_a^i (uv) : \mathfrak{b} \to C\bar{q}\tau} (\oplus l) $$

$$ 2. \quad \frac{\Gamma \vdash^X u : \mathfrak{b}'' \to C\bar{q}(s \Rightarrow \tau) \qquad \mathfrak{b}' \vdash^X \neg x_a^i \wedge \mathfrak{b}''}{\Gamma \vdash^X t \oplus_a^i u : \mathfrak{b}' \to C\bar{q}(s \Rightarrow \tau) \qquad \Gamma \vdash^X v : c \to s \qquad \mathfrak{b} \vdash^X \mathfrak{b}' \wedge c} (\oplus r) $$ $$ \frac{\Gamma \vdash^X (t \oplus_a^i u)v : \mathfrak{b} \to C\bar{q}\tau}{\Gamma \vdash^X (t \oplus_a^i u)v : \mathfrak{b} \to C\bar{q}\tau} (\text{@}) $$

Then, we can argue similarly to the previous case.

($\{t \oplus_a^i u\}v \to_{\mathfrak{p}\{\}} (\{t\}v) \oplus_a^i (\{u\}v)$) Similar to the previous case.

$(t(u \oplus_a^i v) \to_{\mathfrak{p}\{\}} (tu) \oplus_a^i (tv))$ There are two sub-cases:

$$ 1. \quad \frac{\Gamma \vdash^X u : c' \to s \qquad c \vdash^X x_a^i \wedge c'}{\Gamma \vdash^X t \oplus_a^i u : v : c \to s \qquad \mathfrak{b} \vdash^X \mathfrak{b}' \wedge c} (\oplus l) $$ $$ \frac{\Gamma \vdash^X (t \oplus_a^i u)v : \mathfrak{b} \to C\bar{q}(s \Rightarrow \tau)}{\Gamma \vdash^X (t \oplus_a^i u)v : \mathfrak{b} \to C\bar{q}(s \Rightarrow \tau)} (\text{@}) $$

Then, we deduce that
$$ \frac{\Gamma \vdash^X t : \mathfrak{b}' \to C^{\bar{q}}(s \Rightarrow \tau) \qquad \Gamma \vdash^X u : \mathfrak{c}' \to s \qquad \mathfrak{b} \Vdash^X \mathfrak{b}' \wedge \mathfrak{c}' \qquad (\oplus)}{\Gamma \vdash^X tu : \mathfrak{b} \to C^{\bar{q}\tau} \qquad \mathfrak{b} \Vdash^X x_a^i \wedge \mathfrak{b} \qquad (\oplus r)} $$

$$ 2. \quad \frac{\Gamma \vdash^X v : \mathfrak{c}' \to s \qquad c \Vdash^X \neg x_a^i \wedge c' \qquad (\oplus r)}{\Gamma \vdash^X u \oplus_a^i v : c \to s \qquad b \Vdash^X \mathfrak{b}' \wedge c \qquad (\oplus)} $$

Then, we can argue similarly to the previous case.

($\{t\}(u \oplus_a^i v) \dashv_{p\{\}} (\{t\}u) \oplus_a^i (\{t\}v)$) Similar to the previous case.

($\{t \oplus_a^i u\} \oplus_b^j v \dashv_{p\{\}} (t \oplus_b^j v) \oplus_a^i (u \oplus_b^j v)$) We suppose here $a \neq b$ or $i < j$. There are three sub-cases:

$$ \frac{\Gamma \vdash^X t : \mathfrak{b}'' \to s \qquad \mathfrak{b}' \Vdash^X x_a^i \wedge \mathfrak{b}'' \qquad (\oplus l)}{\Gamma \vdash^X t \oplus_a^i u : \mathfrak{b}' \to s \qquad \mathfrak{b} \Vdash^X x_b^j \wedge \mathfrak{b}' \qquad (\oplus l)} $$

Then, we deduce

$$ \frac{\Gamma \vdash^X t : \mathfrak{b}'' \to s \qquad \mathfrak{b} \Vdash^X x_b^j \wedge \mathfrak{b}'' \qquad (\oplus l)}{\Gamma \vdash^X t \oplus_b^j v : \mathfrak{b}' \to s \qquad \mathfrak{b} \Vdash^X x_a^i \wedge \mathfrak{b} \qquad (\oplus l)} $$

$$ 2. \quad \frac{\Gamma \vdash^X u : \mathfrak{b}'' \to s \qquad \mathfrak{b}' \Vdash^X \neg x_a^i \wedge \mathfrak{b}'' \qquad (\oplus r)}{\Gamma \vdash^X t \oplus_a^i u : \mathfrak{b}' \to s \qquad \mathfrak{b} \Vdash^X x_b^j \wedge \mathfrak{b}' \qquad (\oplus l)} $$

Then, we can argue similarly to the previous case.

$$ 3. \quad \frac{\Gamma \vdash^X v : \mathfrak{b}' \to s \qquad \mathfrak{b} \Vdash^X x_b^j \wedge \mathfrak{b}' \qquad (\oplus r)}{\Gamma \vdash^X (t \oplus_a^i u) \oplus_b^j v : \mathfrak{b} \to s} $$

Then, we deduce (using the fact that $\mathfrak{b} \equiv_X (x_a^i \wedge \mathfrak{b}) \lor (\neg x_a^i \wedge \mathfrak{b})$)

$$ \frac{\Gamma \vdash^X v : \mathfrak{b}' \to s \qquad \mathfrak{b} \Vdash^X x_b^j \wedge \mathfrak{b}' \qquad (\oplus r)}{\Gamma \vdash^X t \oplus_b^j v : \mathfrak{b} \to s \qquad x_a^i \wedge \mathfrak{b} \Vdash^X x_a^i \wedge \mathfrak{b} \qquad (\oplus)} \qquad \frac{\Gamma \vdash^X v : \mathfrak{b}' \to s \qquad \mathfrak{b} \Vdash^X x_b^j \wedge \mathfrak{b}' \qquad (\oplus r)}{\Gamma \vdash^X u \oplus_b^j v : \mathfrak{b}' \to s \qquad \neg x_a^i \wedge \mathfrak{b} \Vdash^X x_a^i \wedge \mathfrak{b} \qquad (\oplus)} \qquad \frac{\Gamma \vdash^X (t \oplus_b^j v) \oplus_a^i (u \oplus_b^j v) : x_a^i \wedge \mathfrak{b} \to s \qquad \mathfrak{b} \Vdash^X (x_a^i \wedge \mathfrak{b}) \lor (\neg x_a^i \wedge \mathfrak{b}) \qquad (\oplus)}{\Gamma \vdash^X (t \oplus_b^j v) \oplus_a^i (u \oplus_b^j v) : \mathfrak{b}' \to s \qquad \mathfrak{b} \Vdash^X (x_a^i \wedge \mathfrak{b}) \land (\neg x_a^i \wedge \mathfrak{b}) \qquad (\lor)} $$

($t \oplus_b^j (u \oplus_a^i v) \dashv_{p\{\}} (t \oplus_b^j u) \oplus_a^i (t \oplus_b^j v)$) Similar to the case above.

($vb.(t \oplus_a^i u) \dashv_{p\{\}} (vb.t) \oplus_a^i (vb.u)$) We suppose $a \neq b$. There are two sub-cases:

1.

$$ \frac{\Gamma \vdash^{X \cup \{a,b\}} t : d \to s \qquad \mathfrak{b}' \wedge c \Vdash x_a^i \wedge d \qquad (\oplus l)}{\Gamma \vdash^{X \cup \{a,b\}} t \oplus_a^i u : \mathfrak{b}' \wedge c \to s \qquad \mu(c) \geq s \qquad \mathfrak{b} \Vdash \mathfrak{b}' \qquad (\mu)} $$

From $\mathfrak{b}' \wedge c_i \Vdash d$, by Lemma C.3, we deduce the existence of a derivation of $\Gamma \vdash^{X \cup \{a,b\}} t : \mathfrak{b}' \wedge c \to s$. Moreover, from $\mathfrak{b}' \wedge c_i \Vdash x_a^i \wedge d_i$ and the fact that $\mathrm{FN}(c_i) \subseteq \{b\}$ it follows that $\mathfrak{b}' \Vdash x_a^i$, so we can construct the following derivation:

$$ \frac{\Gamma \vdash^{X \cup \{a,b\}} t : \mathfrak{b}' \wedge c \to s \qquad \mu(c_i) \geq s \qquad (\mu)}{\Gamma \vdash^{X \cup \{a\}} vb.t : \mathfrak{b}' \to C^s \qquad \mathfrak{b} \Vdash x_a^i \wedge \mathfrak{b}' \qquad (\oplus l)} $$
2.

$$ \frac{\Gamma \vdash^{X \cup \{a,b\}} u : d \to s \quad b' \land c \vdash \neg x_a^i \land d}{\Gamma \vdash^{X \cup \{a,b\}} t \oplus_a^i u : b' \land c \to s} (\oplus r) \qquad \mu(c) \geq s \qquad b \vdash b' \qquad (\mu) \\ \frac{\Gamma \vdash^{X \cup \{a\}} v b . t \oplus_a^i u : b \to C^s \bar{q}}{\Gamma \vdash^{X} \lambda x . v a . t : b \to C^s C \bar{q} (s \Rightarrow \sigma)} (\lambda) $$

The we can argue similarly to the previous case.

($\lambda x.v a . t \to_{\rho\{\}} v a.\lambda x.t$) We have

$$ \frac{\Gamma, x : s \vdash^{X \cup \{a\}} t : b' \land c \to C \bar{q} \sigma \qquad \mu(c) \geq s \qquad b \vdash^{X} b'}{\Gamma, x : s \vdash^{X} v a . t : b \to C^{s} C \bar{q} \sigma} (\mu) \\ \frac{\Gamma \vdash^{X} \lambda x . t : b' \land c \to C \bar{q} (s \Rightarrow \sigma) \qquad \mu(c) \geq s \qquad b \vdash^{X} b'}{\Gamma \vdash^{X} \lambda x . v a . t : b \to C^{s} C \bar{q} (s \Rightarrow \sigma)} (\lambda) $$

from which we deduce:

$$ \frac{\frac{\Gamma, x : s \vdash^{X \cup \{a\}} t : b' \land c \to C \bar{q} \sigma}{\Gamma \vdash^{X} \lambda x . t : b' \land c \to C \bar{q} (s \Rightarrow \sigma)} (\lambda) \qquad \mu(c) \geq s \qquad b \vdash^{X} b'}{\Gamma \vdash^{X} v a . t : b'' \to C^{s} C \bar{q} (s \Rightarrow \sigma)} (\mu) \\ ((v a . t) u \to_{\rho\{\}} v a . (t u)) \qquad \text{We have} $$

$$ \frac{\frac{\Gamma \vdash^{X \cup \{a\}}, t : b' \land c \to C \bar{q} (s \Rightarrow \sigma) \qquad \mu(c) \geq s \qquad b'' \vdash b'}{\Gamma \vdash^{X} v a . t : b'' \to C^{s} C \bar{q} (s \Rightarrow \sigma)} \qquad \Gamma \vdash^{X} u : d \to s \qquad b \vdash b'' \land d}{\Gamma \vdash^{X} (v a . t) u : b \to C^{s} C \bar{q} \sigma} (@) $$

from which we deduce

$$ \frac{\Gamma \vdash^{X \cup \{a\}}, t : b' \land c \to C \bar{q} (s \Rightarrow \sigma) \qquad \Gamma \vdash^{X} u : d \to s \qquad b' \land c \vdash (b' \land c) \land d}{\Gamma \vdash^{X} t u : b' \land c \to C \bar{q} \sigma} (@) \qquad \mu(c) \geq s \qquad b'' \vdash b'} (\mu) \\ ((\{t\} v a . u \to_{\rho\{\}} v a . (t u)) \text{ We have}) $$

$$ \frac{\frac{\Gamma \vdash^{X \cup \{a\}} u : c' \land d \to s \qquad \mu(d) \geq s \qquad c' \vdash c}{\Gamma \vdash^{X} v a . u : c \to C^s s} (\mu) \qquad b \vdash b' \land c}{\Gamma \vdash^{X} \{t\} v a . u : b \to C^s C \bar{q} \sigma} (\{\}) $$

from which we deduce (using Lemma C.2)

$$ \frac{\frac{\Gamma \vdash^{X \cup \{a\}} t : b' \land c \to C \bar{q} (s \Rightarrow \sigma) \qquad \Gamma \vdash^{X \cup \{a\}} u : c' \land d \to s \qquad b' \land d \vdash b' \land (c \land d)}{\Gamma \vdash^{X} t u : b' \land d \to C \bar{q} \sigma} (@) \qquad \mu(d) \geq s \qquad b \vdash b'} (\mu) \\ \frac{\Gamma \vdash^{X} v a . t : c \to C^s C \bar{q} \sigma}{\Gamma \vdash^{X} v a . u : c \to C^s C \bar{q} \sigma} \qquad \square $$

# D Details about $C\lambda_{\to, \cap}$.

## D.1 Subject Reduction.

In this subsection we show that subject reduction holds for $C\lambda_{\to, \cap}$ (and a fortiori for $C\lambda_{\to}$).

**Proposition D.1 (Subject Reduction).** If $\Gamma \vdash^X t : b \to s$ and $t \to u$, then $\Gamma \vdash^X u : b \to s$.

As for $C\lambda_{\to}^{\{\}}$ (see Section C), we replace the rule $(\oplus)$ by the two rules $(\oplus l)$ and $(\oplus r)$. Moreover, we will ignore the rules $(\text{hn})$ and $(\text{n})$, as the result extends immediately to them.

To show the reduction property of $C\lambda_{\to, \cap}$ we need to establish a few lemmas, some of which are analogous to results for $C\lambda_{\to}^{\{\}}$, and proved in a similar way:

**Lemma D.2.** If $\Gamma \vdash^X t : b \to s$ and $X \subseteq Y$, then $\Gamma \vdash^Y t : b \to s$.

**Lemma D.3.** If $\Gamma \vdash^X t : b \to s$ holds and $c \vdash^X b$, then $\Gamma \vdash^X t : c \to s$ is derivable by a derivation of the same length.
The next lemmas are new:

**Lemma D.4.** The following rule is admissible in Cλ:

$$ \frac{\Gamma \vdash^X t : \mathfrak{b} \to \mathfrak{s} \qquad \mathfrak{s} \leq t}{\Gamma \vdash^X t : \mathfrak{b} \to t} \quad (\leq) $$

*Proof.* We will show the admissibility of a more general rule, namely

$$ \frac{\Gamma \vdash^X t : \mathfrak{b} \to t \qquad \Delta \leq \Gamma, \mathfrak{s} \leq t}{\Delta \vdash^X t : \mathfrak{b} \to t} \quad (\leq^*) $$

where $\Delta \leq \Gamma$ holds when $\Gamma = \{x_1 : \mathfrak{M}_1, \dots, x_n : \mathfrak{M}_n\}$, $\Delta = \{x_1 : \mathfrak{N}_1, \dots, x_n : \mathfrak{N}_n\}$ and $\mathfrak{M}_i \leq \mathfrak{N}_i$.

We argue by induction on a typing derivation D of t:

* if D is

$$ \frac{\mathrm{FN}(\mathfrak{b}) \subseteq X \qquad \mathfrak{s}_i \leq t}{\Gamma, x : [\mathfrak{s}_1, \dots, \mathfrak{s}_n] \vdash^X x : \mathfrak{b} \to t} $$

then from $\Delta \leq \Gamma$, $x : [\mathfrak{s}_1, \dots, \mathfrak{s}_n]$ we deduce that $\Delta$ contains $x : \mathfrak{M}$, with $\mathfrak{M} \leq [\mathfrak{s}_1, \dots, \mathfrak{s}_n]$. This implies that $\mathfrak{M}$ contains $u_i$, where $u_i \leq \mathfrak{s}_i$; by transitivity of $\leq$, from $u_i \leq \mathfrak{s}_i \leq t$, we deduce $u_i \leq t$, and thus we can construct the derivation below

$$ \frac{\mathrm{FN}(\mathfrak{b}) \subseteq X \qquad u_i \leq t}{\Delta \vdash^X x : \mathfrak{b} \to t} $$

* if D ends by any of the rules ($\vee$), ($\oplus l$), ($\oplus r$) or ($\mu_\Sigma$), then we can directly conclude by applying the I.H.

* if D is

$$ \frac{\Gamma, x : \mathfrak{M} \vdash^X t : \mathfrak{b} \to C^q \sigma}{\Gamma \vdash^X \lambda x.t : \mathfrak{b} \to C^q(\mathfrak{M} \Rightarrow \sigma)} \quad (\lambda) $$

then from $C^q(\mathfrak{M} \Rightarrow \sigma) \leq t$ we deduce $t = C^s(\mathfrak{M}' \Rightarrow \sigma')$, with $s \leq q$, $\mathfrak{M} \leq \mathfrak{M}'$ and $\sigma \leq \sigma''$, and from $\Delta \leq \Gamma$, we deduce $\Delta, x : \mathfrak{M}' \leq \Gamma, x : \mathfrak{M}$. So by the I.H. we deduce the existence of a derivation of $\Delta, x : \mathfrak{M}' \vdash^X t : \mathfrak{b} \to C^s \sigma'$ and we can conclude by applying an instance of $(\lambda)$.

* if D is

$$ \frac{\Gamma \vdash^X t : c \quad \dots \quad C^q(\mathfrak{M} \Rightarrow \sigma) \quad \left\{ \begin{array}{c} \vdots \\ \Gamma \vdash^X u : d_i \to s_i \end{array} \right\}_i \quad \begin{array}{l} c \vdash c \wedge \bigwedge_i d_i \\ \Gamma \vdash^X tu : c \to C^q \sigma \end{array} \quad @\cap $$

where $\mathfrak{M} = [\mathfrak{s}_1, \dots, \mathfrak{s}_n]$. Then from $C^q \sigma \leq s$ we deduce $\tau = C^s \sigma'$, with $s \leq q$ and $\sigma \leq \sigma'$, and thus $C^q(\mathfrak{M} \Rightarrow \sigma) \leq C^s(\mathfrak{M} \Rightarrow \sigma')$, so by the I.H. applied to the left-hand side sub-derivation we obtain a the existence of a derivation of $\Gamma \vdash^X t : c \to C^s(\mathfrak{M} \Rightarrow \sigma')$, and thus we can conclude by applying an instance of $(@\cap)$.

□

**Lemma D.5.** Let $\mathfrak{b}, \mathfrak{b}_1, \dots, \mathfrak{b}_n$ and $c, c_1, \dots, c_n$ be such that $\mathrm{FN}(\mathfrak{b})$, $\mathrm{FN}(\mathfrak{b}_i) \subseteq X$ and $\mathrm{FN}(c), \mathrm{FN}(c_i) \subseteq \{a\}$, where $a \notin X$. If $c$ is satisfiable, then if $\mathfrak{b} \wedge c \models^{X \cup \{a\}} \bigvee_i^n \mathfrak{b}_i \wedge c_i$ holds, also $\mathfrak{b} \models^X \bigvee_i^n \mathfrak{b}_i$ holds.

*Proof.* Let $v \in 2^X$ be a model of $\mathfrak{b}$. Since $c$ is satisfiable, $v$ can be extended to a model $v' \in 2^{X \cup \{a\}}$ of $\mathfrak{b} \wedge c$. By hypothesis, then $v'$ satisfies $\bigvee_i^n \mathfrak{b}_i \wedge c_i$, so for some $i_0 \leq n$, it satisfies $\mathfrak{b}_{i_0} \wedge c_{i_0}$. We deduce then that $v$ satisfies $\mathfrak{b}_{i_0}$, and thus $v$ satisfies $\bigvee_i^n \mathfrak{b}_i$. □

**Lemma D.6.** If $\Gamma \vdash^{X \cup Y} t : \mathfrak{b} \wedge c \to s$ is derivable, where $X \cap Y = \emptyset$, $\mathrm{FN}(t) \subseteq X$, $\mathrm{FN}(\mathfrak{b}) \subseteq X$, $\mathrm{FN}(c) \subseteq Y$, and $c$ is satisfiable, then $\Gamma \vdash^X t : \mathfrak{b} \to s$ is also derivable.

*Proof.* By induction on a typing derivation of t:

* if the last rule is

$$ \frac{\mathfrak{s}_i \leq t \qquad \mathrm{FN}(\mathfrak{b} \wedge c) \subseteq X \cup Y}{\Gamma, x : [\mathfrak{s}_1, \dots, \mathfrak{s}_n] \vdash^{X \cup \{a\}} x : \mathfrak{b} \wedge c \to t} \quad (\mathrm{id}_\cap) $$

then the claim can be deduced by an instance of the same rule.

* if the last rule is
$$ \frac{\{\Gamma \vdash^{XUY} t : \mathfrak{b}_i \to \mathfrak{s}\}_i \quad \mathfrak{b} \wedge \mathfrak{c} \models^{XUY} \bigvee_i \mathfrak{b}_i}{\Gamma \vdash^{XUY} x : \mathfrak{b} \wedge \mathfrak{c} \to \mathfrak{s}} \quad (\mathcal{V}) $$

Let $\bigvee_j \mathfrak{b}_{ij} \wedge \mathfrak{d}_{ij}$ be weak Y-decompositions of the $\mathfrak{b}_i$ (see [[?], p. 17]); since $\mathfrak{b}_{ij} \wedge \mathfrak{d}_{ij} \models \mathfrak{b}_i$, by Lemma D.3 we deduce that $\Gamma \vdash^{XUY} t : \mathfrak{b}_{ij} \wedge \mathfrak{d}_{ij} \to \mathfrak{s}$ is derivable for all $i$ and $j$, by a derivation of same length as the corresponding derivation of $\Gamma \vdash^{XUY} t : \mathfrak{b}_i \to \mathfrak{s}$; hence we can apply the I.H. to such derivations, yielding derivations of $\Gamma \vdash^X t : \mathfrak{b}_{ij} \to \mathfrak{s}$.
Using Lemma D.5, from $\mathfrak{b} \wedge \mathfrak{c} \models \bigvee_i \mathfrak{b}_i$ and $\bigvee_i \mathfrak{b}_i \equiv \bigvee_{ij} \mathfrak{b}_{ij} \wedge \mathfrak{c}_{ij}$, we deduce $\mathfrak{b} \models \bigvee_{ij} \mathfrak{b}_{ij}$, so we conclude

$$ \frac{\{\Gamma \vdash^X t : \mathfrak{b}_{ij} \to \mathfrak{s}\}_{ij} \quad \mathfrak{b} \models^X \bigvee_{ij} \mathfrak{b}_{ij}}{\Gamma \vdash^X x : \mathfrak{b} \to \mathfrak{s}} \quad (\mathcal{V}) $$

* if the last rule is

$$ \frac{\Gamma \vdash^{XUY} t_1 : \mathfrak{b}' \to \mathfrak{s} \quad \mathfrak{b} \wedge \mathfrak{c} \models \mathfrak{x}_i^b \wedge \mathfrak{b}'}{\Gamma \vdash^{XUY} t_1 \oplus_b^i t_2 : \mathfrak{b} \wedge \mathfrak{c} \to \mathfrak{s}} \quad (\oplus l) $$

Then, let $\bigvee_j \mathfrak{d}_{ij} \wedge \mathfrak{c}_j$ be a Y-decomposition of $\mathfrak{b}'$; by Lemma D.3 there exist derivations of $\Gamma \vdash^{XUY} t_1 : \mathfrak{d}_{ij} \wedge \mathfrak{c}_j \to \mathfrak{s}$ of same length as the derivation $\Gamma \vdash^{XUY} t_1 : \mathfrak{b}' \to \mathfrak{s}$, so by I.H. we obtain derivations of $\Gamma \vdash^{XUY} t_1 : \mathfrak{d}_{ij} \to \mathfrak{s}$.
From $\mathfrak{b} \wedge \mathfrak{c} \models \mathfrak{x}_i^b \wedge \mathfrak{b}'$ we deduce $\mathfrak{b} \wedge \mathfrak{c} \models \bigvee_j (\mathfrak{x}_i^b \wedge \mathfrak{d}_{ij}) \wedge \mathfrak{c}_j$, and using Lemma D.5 we deduce $\mathfrak{b} \models \bigvee_j \mathfrak{x}_i^b \wedge \mathfrak{d}_{ij} \equiv \mathfrak{x}_i^b \wedge \bigvee_j \mathfrak{d}_{ij}$.
We can thus conclude as follows:

$$ \frac{\{\Gamma \vdash^X t_1 : \mathfrak{d}_{ij} \to \mathfrak{s}\}_j}{\Gamma \vdash^X t_1 : \bigvee_j \mathfrak{d}_{ij} \to \mathfrak{s}} \quad (\mathcal{V}) \qquad \mathfrak{b} \models^X \mathfrak{x}_i^b \wedge \bigvee_j \mathfrak{d}_{ij} \qquad (\oplus l) $$

* if the last rule is

$$ \frac{\Gamma \vdash^{XUY} t_2 : \mathfrak{b}' \to \mathfrak{s} \quad \mathfrak{b} \wedge \mathfrak{c} \models \neg \mathfrak{x}_i^b \wedge \mathfrak{b}'}{\Gamma \vdash^{XUY} t_1 \oplus_b^i t_2 : \mathfrak{b} \wedge \mathfrak{c} \to \mathfrak{s}} \quad (\oplus r) $$

then we can argue similarly to the previous case.

* if the last rule is

$$ \frac{\Gamma, y : \mathfrak{M} \vdash^{XUY} t : \mathfrak{b} \wedge \mathfrak{c} \to \mathfrak{C}^q \sigma}{\Gamma \vdash^{XUY} \lambda y.t : \mathfrak{b} \wedge \mathfrak{c} \to \mathfrak{C}^q(\mathfrak{M} \Rightarrow \sigma)} \quad (\lambda) $$

Then, the claim follows from the I.H. by applying an instance of the same rule.

* if the last rule is

$$ \frac{\Gamma \vdash^{XUY} t_1 : \mathfrak{b}_1 \to \mathfrak{C}^q(\mathfrak{M} \Rightarrow \sigma) \quad \{\Gamma \vdash^{XUY} t_2 : \mathfrak{b}_i \to \mathfrak{s}_i\}_i \quad \mathfrak{b} \wedge \mathfrak{c} \models^{XUY\{a\}} \mathfrak{b}_1 \wedge (\wedge_i \mathfrak{b}_i)}{\Gamma \vdash^{XUY} t_1 t_2 : \mathfrak{b} \wedge \mathfrak{c} \to \mathfrak{C}^q \sigma} \quad (@ \cap) $$

Then let $\bigvee_j \mathfrak{c}'_j \wedge \mathfrak{d}'_j$ and $\bigvee_k \mathfrak{c}''_{ik} \wedge \mathfrak{d}''_{ik}$ be weak Y-decompositions of $\mathfrak{b}_1$ and $\mathfrak{b}_i$. By Lemma D.3 there exist then derivations of $\Gamma \vdash^{XUY} t_1 : \mathfrak{c}'_j \wedge \mathfrak{d}'_j \to \mathfrak{C}^q(\mathfrak{M} \Rightarrow \sigma)$ and $\Gamma \vdash^{XUY} t_2 : \mathfrak{c}''_{ik} \wedge \mathfrak{d}''_{ik} \to \mathfrak{s}_i$ of same length as the corresponding derivations.
By applying the I.H. to such derivations we obtain then derivations of $\Gamma \vdash^X t_1 : \mathfrak{c}'_j \to \mathfrak{C}^q(\mathfrak{M} \Rightarrow \sigma)$ and $\Gamma \vdash^X t_2 : \mathfrak{c}''_{ik} \to \mathfrak{s}_i$, respectively.
Moreover, from $\mathfrak{b} \wedge \mathfrak{c} \models \mathfrak{b}_1 \wedge \wedge_i \mathfrak{b}_i$ we deduce $\mathfrak{b} \wedge \mathfrak{c} \models \bigvee_j \mathfrak{c}'_j \wedge \mathfrak{d}'_j$ and $\mathfrak{b} \wedge \mathfrak{c} \models \bigvee_{ik} \mathfrak{c}''_{ik} \wedge \mathfrak{d}''_{ik}$, so by Lemma D.5 we deduce $\mathfrak{b} \models \bigvee_j \mathfrak{c}'_j$ and $\mathfrak{b} \models \wedge_i \bigvee_{ik} \mathfrak{c}''_{ik}$.
Thus, we can conclude as follows:

$$ \frac{\{\Gamma \vdash^X t_1 : \mathfrak{c}'_j \to \mathfrak{C}^q(\mathfrak{M} \Rightarrow \sigma)\}_j}{\Gamma \vdash^X t : \bigvee_j \mathfrak{c}'_j \to \mathfrak{C}^q(\mathfrak{M} \Rightarrow \sigma)} \quad (\mathcal{V}) \qquad \left\{ \frac{\{\Gamma \vdash^X t_2 : \mathfrak{c}''_{ik} \to \mathfrak{s}_i\}_k}{\Gamma \vdash^X t_2 : \bigvee_{ik} \mathfrak{c}''_{ik} \to \mathfrak{s}_i} \right\}_i \quad (\mathcal{V}) \qquad \mathfrak{b} \models^X (\bigvee_j \mathfrak{c}'_j) \wedge (\wedge_i \bigvee_{ik} \mathfrak{c}''_{ik}) \qquad (@) $$

* if the last rule is

$$ \frac{\{\Gamma \vdash^{XUY \cup \{b\}, q_u} t : \mathfrak{b}' \wedge \mathfrak{f}_u \to \mathfrak{C}^{q_u} \sigma\}_u \quad \mu(\mathfrak{f}_u) \geq s_u \quad \mathfrak{b} \wedge \mathfrak{c} \models \mathfrak{b}'}{\Gamma \vdash^{XUY} v.b.t : \mathfrak{b} \wedge \mathfrak{c} \to \mathfrak{C}^r \sigma} \quad (\mu_{\Sigma}) $$
where $r = \sum_u q_u s_u$, then let $\bigvee_i c_i \wedge d_i$, be a weak $a$- decomposition of $b$. By Lemma C.3 there exist derivations of $\Gamma \vdash^{X\cup Y\cup\{b\}} t : c_i \wedge d_i \wedge f_u \rightarrow C^{q_u}\sigma$ of same length as the corresponding derivation of $\Gamma \vdash^{X\cup Y\cup\{b\}} t : b' \wedge f_u \rightarrow C^{q_u}\sigma$. Hence, by the I.H. there exist derivations of $\Gamma \vdash^{X\cup\{b\}} t : c_i \wedge f_u \rightarrow C^{q_u}\sigma$.

From $b \wedge c \models^{X\cup\{a\}} b'$ we deduce by Lemma D.5 $b \models \bigvee_i c_i$ and so we can conclude as follows:

$$ \frac{\left\{ \frac{\{\Gamma \vdash^{X\cup\{b\}} t : c_i \wedge f_u \rightarrow C^{q_u}\sigma\}_i}{\Gamma \vdash^{X\cup\{b\}} t : \bigvee_i c_i \wedge f_u \rightarrow C^{q_u}\sigma} \right\}_u}{\Gamma \vdash^X v b . t : b \rightarrow C^r \sigma} \qquad (\mu_\Sigma) $$

□

The proof of the substitution lemma below is analogous to the proof of Lemma C.4.

**Lemma D.7 (substitution lemma).** *The following rule is derivable:*

$$ \frac{\Gamma, x : [s_1, \dots, s_n] \vdash^X t : c \rightarrow C^q \tau \qquad \{\Gamma \vdash^X u : d_i \rightarrow s_i\}_{i=1,\dots,n} \qquad b \models c \wedge (\wedge_i d_i) \qquad (\text{subst}_\emptyset) \\ \qquad \Gamma \vdash^X t[u/x] : b \rightarrow C^q \tau}{\Gamma \vdash^{X\cup\{a\}} v b . t \oplus_a^i u \rightarrow C^{\Sigma_i q_i s_i} \sigma} $$

We now have all elements to establish the subject reduction property.

*Proof of Proposition D.1.* As in the proof of Prop. C.1, observe that if the typing derivation $D$ of $t$ ends by a ($\vee$)-rule, it suffices to establish the property for the immediate sub-derivations of $D$ and then apply an instance of ($\vee$)-rule to the resulting derivations. So we will always suppose that the typing derivation of $D$ does not end by a ($\vee$)-rule.

The argument for $\beta$-reduction works similarly to the one in the Prop. C.1, using Lemma D.7 in place of Lemma C.4. (subst$_\emptyset$)

For the case of $\rightarrow_p$ we consider reduction rules one by one. Most cases are analogous to those from the proof of Prop. C.1. We limit ourselves to the case of the permutation rule ($\neg\vee$) (not considered before), and to those permutations that involve the rule $(\mu_\Sigma)$:

$(vb.(t \oplus_a^i u) \rightarrow_p (vb.t) \oplus_a^i (vb.u))$ We suppose $a \neq b$. As in the proof of Prop. C.1 there are two sub-cases, we only consider the first one (the second one being treated similarly):

$$ \frac{\left\{ \frac{\Gamma \vdash^{X\cup\{a,b\}} t : d_i \rightarrow C^{q_i}\sigma \qquad b' \wedge c_i \models x_a^i \wedge d_i}{\Gamma \vdash^{X\cup\{a,b\}} t \oplus_a^i u : b' \wedge c_i \rightarrow C^{q_i}\sigma} \right\}_i}{\Gamma \vdash^{X\cup\{a\}} v b . t \oplus_a^i u \rightarrow C^{\Sigma_i q_i s_i} \sigma} \qquad (\mu_\Sigma) $$

From $b' \wedge c_i \models d_i$, by Lemma C.3, we deduce the existence of a derivation of $\Gamma \vdash^{X\cup\{a,b\}} t : b' \wedge c_i \rightarrow C^{q_i}\sigma$. Moreover, from $b' \wedge c_i \models x_a^i \wedge d_i$ and the fact that $\text{FN}(c_i) \subseteq \{b\}$ it follows that $b' \models x_a^i$, so we can construct the following derivation:

$$ \frac{\left\{ \frac{\{\Gamma \vdash^{X\cup\{a,b\}} t : b' \wedge c_i \rightarrow C^{q_i}\sigma\}_i}{\Gamma \vdash^{X\cup\{a\}} v b . t : b' \rightarrow C^{\Sigma_i q_i s_i} \sigma} \right\} \qquad (\mu_\Sigma)}{\Gamma \vdash^{X\cup\{a\}} (vb.t) \oplus_a^i (vb.u) : b \rightarrow C^{\Sigma_i q_i s_i} \sigma} \qquad (\oplus l) $$

$(va.t \rightarrow_p t)$ We have

$$ \frac{\left\{ \frac{\{\Gamma \vdash^{X\cup\{a\}} t : b' \wedge c_i \rightarrow C^{q_i}\sigma\}_i}{\Gamma \vdash^{X\cup\{a\}} va.t : b \rightarrow C^{\Sigma_i q_i s_i} \sigma} \right\} \qquad (\mu_\Sigma)}{\Gamma \vdash^X va.t : b \rightarrow C^{\Sigma_i q_i s_i} \sigma} \qquad (\mu_\Sigma) $$

Since the $c_i$ are pairwise disjoint, from $\mu(c_i) \geq s_i$ it follows that $\sum_i s_i \leq 1$. Hence, by letting $Q = \max_i\{q_i\}$, we have $\sum_i q_i s_i \leq \sum_i Q s_i = Q \cdot \sum_i s_i \leq Q$. Let $i_0$ be the index such that $Q = q_{i_0}$. Since $a \notin \text{FN}(t)$, by applying Lemma D.6 to the derivation of $\Gamma \vdash^{X\cup\{a\}} t : b' \wedge c_{i_0} \rightarrow C^Q\sigma$, we deduce $\Gamma \vdash^X t : b' \rightarrow C^Q\sigma$, and since $C^Q\sigma \leq C^{\Sigma_i q_i s_i}\sigma$ and, we deduce, by Lemma D.4, $\Gamma \vdash^X t : b' \rightarrow C^{\Sigma_i q_i s_i}\sigma$, and by Lemma D.3, $\Gamma \vdash^X t : b \rightarrow C^{\Sigma_i q_i s_i}\sigma$.

$(\lambda x.va.t \rightarrow_p \lambda a.\lambda x.t)$ We have

$$ \frac{\left\{ \frac{\{\Gamma, x : \mathfrak{M} \vdash^{X\cup\{a\}} t : b' \wedge c_i \rightarrow C^{q_i}\sigma\}_i}{\Gamma, x : \mathfrak{M} \vdash^X va.t : b \rightarrow C^{\Sigma_i q_i s_i} \sigma} \right\} \qquad (\mu_\Sigma)}{\Gamma \vdash^X \lambda x.va.t : b \rightarrow C^{\Sigma_i q_i s_i}(\mathfrak{M} \Rightarrow \sigma)} \qquad (\lambda) $$
from which we deduce:

$$
\frac{
  \left\{
    \begin{array}{@{}l@{}}
      \displaystyle \frac{\Gamma, x : \mathfrak{M} \vdash^{X \cup \{a\}} t : \mathfrak{b}' \wedge c_i \to C^{q_i \sigma}}{\Gamma \vdash^X \lambda x.t : \mathfrak{b}' \wedge c_i \to C^{q_i}(\mathfrak{M} \Rightarrow \sigma)} (\lambda) \\
      \displaystyle \frac{\mu(c_i) \ge s_i}{\Gamma \vdash^X \text{va.t} : \mathfrak{b} \to C^{\Sigma_i q_i s_i}(\mathfrak{M} \Rightarrow \sigma)} (\mu_{\Sigma})
    \end{array}
  \right\}
  \quad
  \begin{array}{@{}l@{}}
    \mathfrak{b} \nvDash^X \mathfrak{b}' \\
    \mu(d_i) \ge s_i
  \end{array}
}{
  \Gamma \vdash^X \text{va.t} : \mathfrak{b} \to C^{\Sigma_i q_i s_i}(\mathfrak{M} \Rightarrow \sigma)
}
\quad (\mu_{\Sigma})
$$
$$
\frac{
  \left\{
    \begin{array}{@{}l@{}}
      \displaystyle \frac{\Gamma \vdash^{X \cup \{a\}} t : c' \wedge d_i \to C^{q_i}(\mathfrak{M} \Rightarrow \tau)}{\Gamma \vdash^X \text{va.t} : c \to C^{\Sigma_i q_i s_i}(\mathfrak{M} \Rightarrow \tau)} (\mu_{\Sigma}) \\
      \displaystyle \frac{\{\Gamma \vdash^X u : e_j \to s_i\}_j \qquad \mathfrak{b} \wedge d_i \nvDash (e' \wedge d_i) \wedge (\wedge_j e_j)}{\Gamma \vdash^X \text{tu} : \mathfrak{b} \wedge d_i \to C^{q_i \tau}} (@_{\wedge})
    \end{array}
  \right\}
  \quad
  \begin{array}{@{}l@{}}
    \mathfrak{b} \nvDash c \wedge (\wedge_j e_j) \\
    \mu(d_i) \ge s_i
  \end{array}
}{
  \Gamma \vdash^X \text{va.t} : \mathfrak{b} \to C^{\Sigma_i q_i s_i \tau}
}
\quad (\mu_{\Sigma})
$$

where $\mathfrak{M} = [s_1, \dots, s_n]$, from which we deduce

$$
\frac{
  \left\{
    \begin{array}{@{}l@{}}
      \displaystyle \frac{\Gamma \vdash^{X \cup \{a\}} t : c' \wedge d_i \to C^{q_i \sigma} \quad \{\Gamma \vdash^X u : e_j \to s_i\}_j \quad \mathfrak{b} \wedge d_i \nvDash (e' \wedge d_i) \wedge (\wedge_j e_j)}{\Gamma \vdash^X \text{tu} : \mathfrak{b} \wedge d_i \to C^{q_i \tau}} (@_{\wedge}) \\
      \displaystyle \frac{\mu(d_i) \ge s_i}{\Gamma \vdash^X \text{va.t} : \mathfrak{b} \to C^{\Sigma_i q_i s_i \tau}}
    \end{array}
  \right\}
  \quad
  \begin{array}{@{}l@{}}
    \mathfrak{b} \nvDash^X \mathfrak{b}' \\
    \mu(d_i) \ge s_i
  \end{array}
}{
  \Gamma \vdash^X \text{va.t} : \mathfrak{b} \to C^{\Sigma_i q_i s_i \tau}
}
\quad \square
$$

## D.2 Subject Expansion.

The goal of this section is to establish the following result for $C\lambda_{\to, \cap}$:

**Proposition D.8 (subject expansion).** If $\Gamma \vdash^X t : \mathfrak{b} \to s$ and $u \to t$, then $\Gamma \vdash^X t : \mathfrak{b} \to s$.

As for subject reduction, we will ignore the rules (hn) and (n), as the result extends immediately to them.

We will consider first the (more laborious case) of $\beta$-reduction, and then the more direct case of permutative reduction.

**D.2.1 Subject $\beta$-Expansion.** To establish the subject expansion property we need to develop a finer analysis of typing derivations. In particular we will need to prove that derivations can be turned into a canonical form. The main idea is to reduce to a case where $(\vee)$-rules are always applied “as late as possible”, that is, either at the end of the derivation or right before a counting rule. Moreover, we will require that if a $(\vee)$-rule occurs before a counting rule for some name $a$, then these two rule follow a specific pattern, defined below, which ensures that no information is lost about other names.

**Definition D.9** $(\vee\mu$-pattern). For any name $a \in \mathbb{N}$ and typing derivation $D$, a $\vee\mu$-pattern on $a$ in $D$ is given by the occurrence in $D$ of $(\mu)$-rule preceded by multiple occurrences of $(\vee)$-rules in a configuration as illustrated below:

$$
\frac{
  \left\{
    \begin{array}{@{}l@{}}
      \displaystyle \frac{\{\Gamma \vdash^{X \cup \{a\}} t : \mathfrak{b} \wedge d_{ij} \to C^{q_i \sigma}\}_{j=1,\dots,L_i}}{\Gamma \vdash^{X \cup \{a\}} t : \mathfrak{b} \wedge d_i \to C^{q_i \sigma}} (\vee) \\
      \displaystyle \frac{\mu(d_i) \ge s_i}{\Gamma \vdash^X \text{va.t} : \mathfrak{b} \to C^{\Sigma_i q_i s_i \sigma}}
    \end{array}
  \right\}
  \quad
  \begin{array}{@{}l@{}}
    \mathfrak{b} \wedge d_i \nvDash^X \vee_l \mathfrak{b} \wedge d_{ij} \\
    \mu(d_i) \ge s_i
  \end{array}
}{
  \Gamma \vdash^X \text{va.t} : \mathfrak{b} \to C^{\Sigma_i q_i s_i \sigma}
}
\quad (1)
$$

where $\text{FN}(c) \subseteq X$, $\text{FN}(d_{ij}) \subseteq \{a\}$, and $c$ and the $d_{ij}$ are conjunctions of literals.

**Definition D.10** (canonical and pseudo-canonical derivation). A typing derivation $D$ is said *canonical* when the following hold:

a. all Boolean formulas occurring in $D$ are conjunctions of literals, except for those which occur either in the conclusion of a $(\vee)$-rule or in the major premis of a $(\mu_{\Sigma})$-rule;

b. any occurrence of the $(\vee)$ rule in $D$ occurs in a $\vee\mu$-pattern.

A typing derivation $D$ is said *pseudo-canonical* when $D$ is obtained by one application of the $(\vee)$-rule where all premises are conclusions of canonical sub-derivations.

The fundamental property of canonical derivations that we will exploit is the following:

**Lemma D.11.** Suppose $D$ is a canonical derivation of conclusion $\Gamma \vdash^X t : \mathfrak{b} \to s$. If $c$ is a Boolean formula $c$ with $\text{FN}(c) \subseteq X$ occurring in an axiom of $D$, then $\mathfrak{b} \nvDash^X c$.

*Proof.* By induction on $D$:

* if $D$ only consists in an axiom, the claim is trivial;