# Multi-focusing on extensional rewriting with sums

Gabriel Scherer

► To cite this version:

Gabriel Scherer. Multi-focusing on extensional rewriting with sums. Typed Lambda Calculi and Applications, Jun 2015, Warsaw, Poland. hal-01235372

HAL Id: hal-01235372

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

Submitted on 30 Nov 2015

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
# Multi-focusing on extensional rewriting with sums

Gabriel Scherer¹

1 Gallium, INRIA, France

## Abstract

We propose a logical justification for the rewriting-based equivalence procedure for simply-typed lambda-terms with sums of Lindley [Lin07]. It relies on maximally multi-focused proofs, a notion of canonical derivations introduced for linear logic. Lindley's rewriting closely corresponds to *preemptive rewriting* [CMS08], a technical device used in the meta-theory of maximal multi-focus.

1998 ACM Subject Classification F.4.1 Lambda calculus and related systems

Keywords and phrases Maximal multi-focusing, extensional sums, rewriting, natural deduction

Digital Object Identifier 10.4230/LIPIcs.xxx.yyy.p

## 1 Introduction

Deciding observational equality of pure typed lambda-terms in presence of sum types is a difficult problem. After several solutions based on complex syntactic [Gha95] or semantic [ADHS01, BCF04] techniques, Sam Lindley presented a surprisingly simple rewriting solution [Lin07]. While the underlying intuition (extrude contexts to move pattern-matchings as high as possible in the term) makes sense, the algorithm is still mysterious in many aspects: even though they were synthesized from the previous highly-principled approach, the rewriting rules may feel strangely ad-hoc.

In this paper, we will propose a *logical* justification of this algorithm. It is based on recent developments in proof search, maximally multi-focused proofs [CMS08]. The notion of *preemptive rewriting* was introduced in the meta-theory of multi-focusing as a purely technical device; we claim that it is in fact strongly related to Lindley's rewriting, and formally establish the correspondence.

The reference work on multi-focused systems [CMS08] has been carried in a sequent calculus for linear logic. We will first establish the meta-theory of maximal multi-focusing for intuitionistic logic (Section 2). We start from a sequent calculus presentation, which is closest to the original system. Our first contribution is to propose an equivalent multi-focusing system in natural deduction 2.2. We then define preemptive rewriting in this natural deduction 2.4 and establish canonicity of maximally multi-focused proofs 2.6.

In Section 3, we transpose the preemptive rewrite rules into a relation on proof terms. We can then formally study the correspondence between rewriting a multi-focused proof into a canonical maximally multi-focused one, and Lindley's $\gamma$-reduction on lambda-terms. We demonstrate that they compute the same normal forms, modulo a form of redundancy elimination that is missing in the multi-focused system.

We finally introduce redundancy-elimination rewriting and equivalence for the proof terms of the multi-focused natural deduction (Section 4). The resulting notion of canonical proofs, *simplified maximal proofs*, precisely corresponds to normal forms of Lindley's rewriting relation. The natural notion of local equivalence between simplified maximal proofs therefore captures extensional equality.

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

© Gabriel Scherer;

licensed under Creative Commons License CC-BY

Conference title on which this volume is based on.

Editors: Billy Editor and Bill Editors; pp. 1–26

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

LIPICS

Leibniz International Proceedings in Informatics

Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany
## 2 Intuitionistic multi-focusing

The space of proofs in sequent calculus or natural deduction exhibits a lot of redundancy: many proofs that are syntactically distinct really encode the same semantics. In particular, it is often possible to permute two inference rules in a way that preserves the validity of proofs, but also the reduction semantics of the corresponding proof terms. If a permutation transforms a proof with rule A applied above rule B into a proof with rule B applied above rule A, we say that it is an A/B permutation (A is above the slash, as in the source proof).

Focusing is a general discipline that can be imposed upon proof system, based on the separation of inference rules into two classes. *Invertible* rules (called as such because their inverse is admissible) always preserve provability, and can thus be applied as early as possible. *Non-invertible* rules may result in dead ends if they are applied too early (consider proving $A+B \vdash A+B$ by first introducing the sum on the right-hand side)). In focusing calculi, derivations are structured in “sequences” or “phases”, that either only apply invertible rules or only non-invertible rules. Focusing imposes that phases be as long as possible. During invertible phases, one must apply any valid invertible rule. During non-invertible phases, one *focuses* on a set of formulas, and applies non-invertible operations on those formulas as long as possible – if the phase is started too early, this may result in a dead end.

Invertibility determines a notion of polarity of logical connectives: we call *positive* those whose right-hand-side rule is non-invertible (they are “only interesting in positive position”), and *negative* those whose left-hand-side rule is non-invertible. In single-succedent intuitionistic logic, $(\rightarrow)$ is negative, $(+)$ is positive, and the product $(\times)$ may actually be assigned either polarity.

In single-sided calculi, non-invertible rules are those that introduce positive connectives, and are called “positive”. For continuity of vocabulary, we will also call non-invertible rules *positive*, and invertible rules *negative*. In particular, a permutation that moves a non-invertible rule below an invertible rule is a “pos/neg permutation”.

### 2.1 Multi-focused sequent calculus

Multi-focusing ([MS07, CMS08]) is an extension of focusing calculi where, instead of focusing on a single formula of the sequent (either on the left or on the right), we allow to simultaneously focus on several formulas at once. The multiple foci do not interact during the focusing phase, and this allows to express the fact that several focusing sequences are in fact independent and can be performed in parallel, condensing several distinct focused proofs into a single multi-focused derivation.

We start with a multi-focused variant of the intuitionistic sequent calculus, presented in Fig. 1. We denote focus using brackets: the rules with no brackets are invertible. This notation will change in natural deduction calculi.

In particular, we write $A_n$ or $\Delta_p$ for formula or contexts that must be all negative or positive, and $X$, $Y$ or $Z$ for atoms. We write $B_{pa}$ and $\Gamma_{na}$ when either a positive (resp. negative) or an atom is allowed. For readability reasons, we only add polarity annotations when necessary; if we consider only derivations whose end conclusion is unfocused, then the invariant holds that the unfocused left-hand-side context is always all-negative, while the unfocused right-hand-side formula is always positive.

Our intuitionistic calculi are, as is most frequent, single-succedent. The notation $A | B$ on the right does not denote a real disjunction but a single formula, one of the two variables being empty. The focusing rule *SEQ-FOCUS* with conclusion $\Gamma, \Delta \vdash A | B$ can be instantiated in two ways, one when A is empty, and the premise is $\Gamma, [\Delta] \vdash [B]$ (the succedent is part of
the multi-focus), and one when *B* is empty, and the premise is Γ, [Δ] ⊢ A (the succedent is not part of the multi-focus). Note that Δ is a set and may be empty, in which case the focus only happens on the right.

As a minor presentation difference to the reference work on multi-focusing [CMS08], our contexts are unordered multi-sets, and all the formulas under focus are released at once – by **SEQ-RELEASE**, which releases positives (resp. negatives) or atoms.

<figure><img src="image_4.png" /><figcaption>Figure 1 Multifocused sequent calculus for intuitionistic logic</figcaption></figure>

This multi-focused calculus proves exactly the same formulas as the singly-focused sequent calculus. The latter is trivially included in the former, and conversely one can turn a multi-focus into an arbitrarily ordered sequence of single foci. As a corollary, relying on non-trivial proofs from the literature (e.g., [Sim11]), it is equivalent in provability to the (non-focused) sequent calculus for intuitionistic logic.

## 2.2 Multi-focused natural deduction

While the multi-focusing sequent calculus closely corresponds to existing focused presentations, its natural deduction presentation in Fig. 2 is new. We took inspiration from the presentation of focused linear logic in natural deduction of [BNS10], in particular the `↑` and `↓` notations coming from intercalation calculi.

<figure><img src="image_5.png" /><figcaption>Figure 2 Multifocused natural deduction for intuitionistic logic</figcaption></figure>
There are three main judgments. $\Gamma \vdash A$ is the unfocused judgment with the invertible rules. $\Gamma; A \Downarrow B$ is the “elimination-focused” judgment, and $A \Uparrow B$ is the “introduction-focused” judgment (focused on $A$). $\Gamma; A \Downarrow B$ means that the assertion $B$ can be produced from the hypothesis $A$ by non-invertible elimination rules; the context $\Gamma$ is used in any non-focused subgoal. $A \Uparrow B$ means that proving the goal $A$ can be reduced, by applying non-invertible introduction rules, to proving the goal $B$. Those two judgments do not come separately, they are introduced by the focusing rule **NAT-FOCUS**.

In Fig. 2, we used auxiliary rules (**NAT-START-INTRO**, **NAT-START-NO-INTRO**, **NAT-START-ELIM**) to present the focusing compactly (this is important when rewriting proofs); those rules can only happen immediately above **NAT-FOCUS**, and can thus be considered definitional syntactic sugar – we used a double bar to reflect this. If we inlined these auxiliary rules, the focusing rule would read (equivalently):

$$ \frac{(A_n^i)^{i \in I} \subseteq \Gamma_{na} \quad (\Gamma_{na}; A_n^i \Downarrow A_{pa}^{i'})^{i \in I} \quad (B_p \Uparrow B'_{na} \mid B = B') \quad \Gamma_{na}, (A_{pa}^{i'})^{i \in I} \vdash B'_{a}}{\Gamma_{na} \vdash B_{pa}} $$

This rule can only be used when all invertible rules have been performed: the context must be negative or atomic, and the goal positive or atomic. It selects set of foci on the left, the family of strictly negative assumptions $(A_n^i)^{i \in I}$ (we consistently use the superscript notation for family indices), and optionally a focus on the right; if the goal is focused it must be strictly positive. All foci must be as long as possible: elimination foci go from a variable down to a positive or atomic $A_{pa}^{i'}$, and the introduction focus goes up until it encounters a negative or atomic $B'_{na}$.

In comparison to the sequent calculus, the positive or atomic formulas $(A_{pa}^{i'})^{i \in I}$ appearing at the *start* of the elimination-focus correspond to the formulas *released* at the *end* of a multi-focus in a sequent proof; natural deduction, when compared to the sequent calculus, has elimination rules “upside down”. Also characteristic of natural deduction is the horizontal parallelism between eliminations and introductions; for example, the following two partial derivations correspond to the same natural deduction:

$$ \frac{\frac{A_{pa} \times B, A_{pa} \vdash C_{na}}{A_{pa} \times B, [A_{pa}] \vdash [C_{na}]} \qquad \frac{A_{pa} \times B, A_{pa} \vdash C_{na}}{A_{pa} \times B, [A_{pa}] \vdash [C_{na}]} \qquad \frac{A_{pa} \times B, A_{pa} \times B \Downarrow [C_{na}]}{A_{pa} \times B, [A_{pa} \times B] \vdash [C_{na}]} \qquad \frac{A_{pa} \times B, [A_{pa} \times B] \vdash [C_{na}]}{A_{pa} \times B, [A_{pa} \times B] \vdash [C_{na} + D]} \qquad \frac{A_{pa} \times B \vdash C_{na} + D}{A_{pa} \times B \vdash C_{na} + D}$$
$$ \frac{\overline{A_{pa} \times B; A_{pa} \times B \Downarrow A_{pa} \times B}}{A_{pa} \times B; A_{pa} \times B \Downarrow A_{pa}} \qquad \frac{\overline{C_{na} \Uparrow C_{na}}}{C_{na} + D \Uparrow C_{na}} \qquad \frac{A_{pa} \times B, A_{pa} \vdash C_{na}}{A_{pa} \times B, A_{pa} \vdash C_{na}}$$
$$ \frac{A_{pa} \times B \vdash C_{na} + D}{A_{pa} \times B \vdash C_{na} + D} $$

On the other hand, we kept the less important invertible rules in sequent style: the sum elimination is a left introduction. Invertible rules being morally “automatically” applied, the sequent-style left introduction, which is directed by the type of its conclusion, is more natural in this context. Ironically, this brings us rather close to the sequent calculus of Krishnaswami [Kri09] which, for presentation purposes, preserved a function-elimination rule in natural deduction style.

**► Lemma 1.** The multi-focused natural deduction system proves exactly the same non-focused judgments as the multi-focused sequent calculus.
**Proof.** See Appendix C.1.

## 2.3 A preemptive variant of multi-focused natural deduction

$$ \frac{\frac{\text{PREEMPT-FOCUS}}{\Gamma_{npa} \vdash \Delta'_{pa} \quad B_p \Uparrow^? B'_{na} \quad \Gamma_{npa}, \Delta'_{pa} \vdash A_{npa} | B'_{na}} \quad \text{PREEMPT-ELIM}}{\Gamma_{npa} \vdash A_{npa} | B_p} \quad \frac{\Gamma_{npa} \vdash \Delta'_{pa} \quad \Gamma_{npa}, \Delta'_{pa}; A \vdash A'}{\Gamma_{npa}; A \vdash A'} $$

<caption>Figure 3 Preemptive rules for intuitionistic multifocused natural deduction</caption>

Multi-focusing was introduced to express the idea of *parallelism* between non-invertible rules on several independent foci. A proof has more parallelism than another if two sequential foci of the latter are merged (through rule permutations) in a single multi-focus in the former. A natural question is whether there exists “maximally parallel proofs”. To answer it (affirmatively), the original article on multi-focusing ([CMS08]) introduced a rewriting relation that permutes non-invertible phases down in proof derivations, until they cannot go any further without losing provability – neighboring phases can then be merged into a maximally focused proof.

In the process of moving down, a non-invertible phase will traverse invertible phases below. The intermediary states of this reduction sequence may break the invariant that invertible rules must be applied as early as possible; we say that the non-invertible phase *preempts* (a part of) the invertible phase. As this intermediary state is not a valid proof in off-the-shelf multi-focusing systems, the original article introduced a relaxed variant called a preemptive system, in which the phase-sinking transformation, called *preemptive rewriting*, can be defined following [CMS08].

We present in Fig. 3 a preemptive variant of multi-focused natural deduction, except for the invertible and focused-introduction rules that are strictly unchanged from the previous multi-focusing rules in Fig. 2. There are two important differences:

- Preemption of invertible phases. To allow the start of a focusing phase when some invertible rules could still be applied, we lifted the polarity constraints for starting focusing. In the rule `PREEMPT-FOCUS`, the goal $\Gamma_{npa} \vdash A_{npa}$ may be of any polarity. We use a tautological $\Gamma_{npa}$ annotation to emphasize this change.

- Preemption of non-invertible phases. This is expressed by the rule `PREEMPT-ELIM`, where an ongoing focus on $A$ is preempted by a complete focus on $\Delta'_{pa}$. Note that stored contexts are *not* available during the current elimination phase (they are unused in `NAT-END-ELIM`); they are only available to non-focused phases that appear as subgoals (in the arrow elimination rule). This preserves the central idea that the simultaneous foci of a single focusing rule are *independent*.

## 2.4 Preemptive rewriting

We can then define in Fig. 4 the rewriting relation on the preemptive calculus, that lets any non-invertible phase move as far as possible down the derivation tree. Maximally multi-focused proofs, which can be characterized on permutation-equivalence classes of multi-focused proofs, correspond to normal forms of this rewriting relation.

A focused phase cannot move below an inference rule if some of the foci depend on this inference rule. Instead of expressing the non-dependency requirement by implicit absence of the foci, we have explicitly canceled out the foci that *must be absent* to improve readability.
$$ \frac{\Gamma, A \Downarrow \Delta \quad B \Uparrow B' \quad \Gamma, A, \Delta \vdash B}{\Gamma, A \vdash B} \quad \rightarrow \quad \frac{\Gamma, \Delta, A \vdash B}{\Gamma \Downarrow \Delta \quad \Gamma, \Delta \vdash A \rightarrow B} \quad \rightarrow \quad \Gamma \vdash A \rightarrow B $$

$$ \frac{\Gamma \Downarrow \Delta \quad A \Uparrow A' \quad \Gamma, \Delta \vdash A}{\Gamma \vdash A} \quad \rightarrow \quad \frac{\Gamma, \Delta \vdash A \quad \Gamma \vdash B}{\Gamma \Downarrow \Delta \quad \Gamma, \Delta \vdash A \times B} \quad \rightarrow \quad \Gamma \vdash A \times B $$

$$ \frac{\left( \frac{\Gamma, A \Downarrow \Delta \quad C \Uparrow^? D \quad \Gamma, A, \Delta \vdash D}{\Gamma, A \vdash C} \right)}{\left( \frac{\Gamma, B \Downarrow \Delta \quad C \Uparrow^? D \quad \Gamma, B, \Delta \vdash D}{\Gamma, B \vdash C} \right)} \quad \rightarrow \quad \frac{\Gamma \Downarrow \Delta \quad C \Uparrow^? D}{\Gamma, A + B \vdash C, D} $$

$$ \frac{\frac{\Gamma \Downarrow \Gamma' \quad \Gamma, \Gamma'; A \Downarrow B_1 \times B_2}{\Gamma; A \Downarrow B_1 \times B_2}}{\Gamma, \Gamma'; A \Downarrow B_i} \quad \rightarrow \quad \frac{\frac{\Gamma, \Gamma'; A \Downarrow B_1 \times B_2}{\Gamma, \Gamma'; A \Downarrow B_i}}{\Gamma; A \Downarrow B_i} $$

$$ \frac{\frac{\Gamma \Downarrow \Gamma' \quad \Gamma, \Gamma'; A \Downarrow B \rightarrow C}{\Gamma; A \Downarrow B \rightarrow C} \quad B \Uparrow B' \quad \Gamma \vdash B'}{\Gamma; A \Downarrow C} \quad \rightarrow \quad \frac{\Gamma \Downarrow \Gamma' \quad \Gamma, \Gamma'; A \Downarrow B \rightarrow C \quad B \Uparrow B' \quad \Gamma \vdash B'}{\Gamma, \Gamma' \Downarrow B \rightarrow C} \quad \rightarrow \quad \Gamma; A \Downarrow C $$

$$ \frac{\frac{\Gamma \Downarrow \Gamma' \quad \Gamma, \Gamma' \vdash B'_{na}}{\Gamma; A \Downarrow B \rightarrow C \quad B \Uparrow B'_{na}} \quad \rightarrow \quad \frac{\Gamma \Downarrow \Gamma' \quad \Gamma; A \Downarrow B \rightarrow C \quad B \Uparrow B'_{na} \quad \Gamma, \Gamma' \vdash B'_{na}}{\Gamma, \Gamma'; A \Downarrow C}}{\Gamma; A \Downarrow C} $$

$$ \frac{\frac{\Gamma \Downarrow \Delta \quad \Gamma, \Delta; A_n \Downarrow A'}{\Gamma \Downarrow \Gamma' \quad A_n \in \Gamma} \quad \rightarrow \quad \frac{\Gamma \Downarrow \Gamma', A'}{\Gamma \vdash B} \quad B \Uparrow^? B' \quad \Gamma, \Gamma', A' \vdash B'}{\Gamma \vdash B} $$

$$ \frac{\frac{\Gamma \Downarrow \Gamma' \quad A_n \in \Gamma \quad \Gamma, \Delta; A_n \Downarrow A'}{\Gamma, \Delta \Downarrow \Gamma', A'} \quad \rightarrow \quad \frac{\Gamma \Downarrow \Delta \quad \Gamma, \Delta \vdash B}{\Gamma \vdash B} \quad B \Uparrow^? B' \quad \Gamma, \Gamma', A' \vdash B'}{\Gamma \vdash B} $$

$$ \frac{\frac{\Gamma \Downarrow \Delta' \quad B \Uparrow^? C \quad \Gamma, \Delta, \Delta' \vdash C}{\Gamma, \Delta \vdash B} \quad \rightarrow \quad \frac{\Gamma \Downarrow \Delta, \Delta' \quad A \Uparrow^? C \quad \Gamma, \Delta, \Delta' \vdash C}{\Gamma \vdash A}}{\Gamma \vdash A} \quad \leftrightarrow \quad \frac{\Gamma \Downarrow \Delta, \Delta' \quad A \Uparrow^? C \quad \Gamma, \Delta, \Delta' \vdash C}{\Gamma \vdash A} $$

<figure><img src="image_6.png" /><figcaption>**Figure 4** Preemptive rewriting for multifocused natural deduction for intuitionistic logic</figcaption></figure>

In the first rule for example, $\Gamma, A \Downarrow \Delta$ means that the A hypothesis must be weakened (not used) in the derivation of $\Gamma \Downarrow \Delta$, or else it cannot move below the introduction of A.

In this situation, it may be the case that other parts of the multi-focus do not depend on the rule below, and those should not be blocked. To allow rewriting to continue, the
last rewrite of our system is bidirectional. It allows to separate the foci of a multi-focus, in particular separate the foci that depend on the rule below from those that do not – and can thus permute again. This corresponds to the first rule of the original preemptive rewriting system [CMS08], which splits a multi-focus in two. We only need to apply this rule when the result can make one more unidirectional rewrite step – this strategy ensures termination.

In the left-to-right direction, this rule relies on the possibility of merging together two elimination-focused derivations, or two optional introduction-focused derivations, with the implicit requirement that at least one of them is empty.

## 2.5 Reinversion

After the preemptive rewriting rules have been applied, the result is not, in general, a valid derivation in the non-preemptive system. Consider for example the following rewriting process:

$$ \begin{bmatrix} \nu_3 \\ \pi_3 \\ \nu_2 \\ \pi_2 \\ \nu_1 \\ \pi_1 \end{bmatrix} \to^* \begin{bmatrix} \nu_2 & \nu_3 \\ \pi_2 & \pi_3 \\ \nu_1 & \pi_1 \end{bmatrix} \to^* \begin{bmatrix} \nu_2 & \nu_3 \\ \pi_2 & \pi_3 \\ \nu_1 & \pi_1 \end{bmatrix} \to^* \begin{bmatrix} \nu_2 & \nu_3 \\ \pi_2; \nu_3 \\ \nu_1 \\ \pi_1; \nu_1 \end{bmatrix} \to^* \begin{bmatrix} \nu_2 & \nu_3 \\ \pi_2; \nu_3 \\ \nu_1 \\ \pi_1 \end{bmatrix} $$

We are here representing derivations from a high-level point of view, by naming complete sequences of rules of the same polarity. Sequences of positive (non-invertible) are named $\pi_n$, and sequences of negative (invertible) rules $\nu_m$. We use horizontal position to denote parallelism, or dependencies between phases: each dipole ($\pi_k, \nu_k$) is vertically aligned as the invertibles of $\nu_k$ have been produced by the foci of $\pi_k$, but we furthermore assume that the second dipole depends on formulas released by the first, while the third dipole is independent.

The third dipole is independent from the others, and its foci in $\pi_3$ move downward in the derivation as expected in the preemptive system. After the first step, its negative phase has preempted the invertible phase $\nu_2$, and it is thus written $\pi_3; \nu_2$ to emphasize that any rule of this sequence will have all the invertible formulas of $\nu_2$ in non-focused positions (positives in the hypotheses, and negatives in the succedent). It can then be merged with the foci of $\pi_2$, in which case it does not see the invertibles of $\nu_2$ anymore. When it moves further down, the invertible formulas in its topmost sequent, those consumed by $\nu_3$, are present/preempted by all the non-invertible rules of $\pi_2$. It is eventually merged with $\pi_1$.

The normal form of this rewrite sequence could be considered a maximally multi-focused proof, in the sense that the foci happen as soon as possible in the derivation – which was not the case in the initial proof, where $\pi_3$ was delayed. However, while the initial proof is a valid proof in the non-preemptive system, the last derivation is not: the invertible formulas produced by $\pi_3$ are not consumed as early as possible, but only at the very end of the derivation, and the foci of $\pi_2$ therefore happen while there are still invertible rules to be applied.

We introduce a *reinversion* relation between proofs, written $D \triangleright \mathcal{E}$, that turns the proof $D$ with possible preemption into a proof $\mathcal{E}$ valid in the non-preemptive system, by doing the inversions where they are required, without changing the structure of the negative phases –
the foci are exactly the same. In our example, we have:

$$ \begin{bmatrix} \nu_2 & \nu_3 \\ \pi_2; \nu_3 \\ \nu_1 \\ \pi_1 \end{bmatrix} \triangleright \begin{bmatrix} \nu_2 \\ \pi_2 \\ \nu_1 & \nu_3 \\ \pi_1 & \pi_3 \end{bmatrix} $$

**Definition 2 (Rewriting relation).** If $\mathcal{D}$ and $\mathcal{E}$ are proofs of the non-preemptive system, we write $\mathcal{D} \Rightarrow \mathcal{E}$ if there exists a $\mathcal{E}'$ such that $\mathcal{D} \to^* \mathcal{E}' \triangleright \mathcal{E}$.

Reinversion was not discussed directly in the original multi-focusing work [CMS08], but it plays an important role and can be described and understood in several fairly different ways. For lack of space, we only discuss those points of view in Appendix A, and will only formally define reinversion as a relation on the (more concise) proof terms in Section 3.1, Definition 4.

## 2.6 Maximal multi-focusing and canonicity

Now that we have defined the focusing-lowering rewrite ($\Rightarrow$) between non-preemptive proof, we can define the notion of maximal multi-focusing and its meta-theory. It is defined by looking at the width of multi-focus phases in equivalence classes of rule permutations; but it can also be characterized as the normal forms of the ($\Rightarrow$) relation.

For lack of space, we have reserved this development (which is a mere adaptation of the previous work [CMS08]) to Appendix B. The central result is summarized below.

**Definition.** We say that two proofs $\mathcal{D}$ and $\mathcal{E}$ are locally equivalent, or iso-polar, written $\mathcal{D} \approx_{\text{loc}} \mathcal{E}$, if one can be rewritten into the other using only local positive/positive and negative/negative permutations, preserving their initial sequents.

**Definition.** We say that two proofs $\mathcal{D}$ and $\mathcal{E}$ are globally equivalent, or iso-initial, written $\mathcal{D} \simeq_{\text{glob}} \mathcal{E}$, when one can be rewritten into the other using local permutations of any polarity (so when seen as proofs in a non-focused system), preserving their initial sequents.

**Corollary (28).** Two multi-focused proofs are globally equivalent if and only if they are rewritten by ($\Rightarrow$) in locally equivalent maximal proofs.

# 3 On the side of proof terms

## 3.1 Preemption and reinversion as term rewriting

Now that we have a notion of maximally multi-focused proofs in natural deduction, we can cross the second bridge between multi-focusing and Lindley's work by moving to a term system. We define in Figure 5 a term syntax for multi-focused derivations in natural deduction.

As the distinction between the preemptive and the non-preemptive systems are mostly about invariants of the focusing rule, the same term calculus is applicable to both. The only syntactic difference is that preemptive terms allow a multi-focusing $f[n]$ to preempt an ambient elimination focus $n'$.

Structural constraints on the multi-focusing system (preemptive or not) guarantee that strong typing invariants are verified. In particular, in a focused term ($\text{let } \bar{x} = \bar{n} \text{ in } p^2 t$), the $\bar{n}$ are typed by the formulas in $\Delta$ at the end of a $\Gamma \downarrow \Delta$ elimination phase: by our release discipline they have a positive or atomic type, so the $\text{let}$-introduced $\bar{x}$ are always bound to
$$
\begin{array}{l@{\hspace{2em}}l@{\hspace{2em}}l}
t ::= & \text{terms} & \\
\mid x, y, z & \text{variable} & \\
\mid \lambda(x)t & \text{lambda} & \frac{X \text{ atomic}}{\Gamma_{na}, x : X \vdash x : X} \\
\mid (t,t) & \text{pair} & \\
\mid \delta(x, x.t, x.t) & \text{case} & \\
\mid f[t] & \text{focusing} &
\end{array}
$$

$$
\frac{\Gamma, x : A \vdash t : C \qquad \Gamma, x : B \vdash u : C}{\Gamma, x : A + B \vdash \delta(x, x.t, x.u) : C} \qquad \frac{\Gamma \vdash t : A \qquad \Gamma \vdash u : B}{\Gamma \vdash (t, u) : A \times B} \qquad \frac{\Gamma, x : A \vdash t : B}{\Gamma \vdash \lambda(x) t : A \to B}
$$

$$
f[\Box] ::= \mathbf{let} \bar{x} = \bar{n} \text{ in } p^? \Box \quad \begin{array}{l} \text{multi-focusing} \\ \qquad \begin{array}{l} p^? ::= \\ \qquad | \emptyset \text{ no introduction} \\ \qquad | p \text{ introduction focus} \end{array} \end{array}
$$

$$
\frac{\Gamma_{na} \Downarrow \mathbf{let} \bar{x} = \bar{n} : \Gamma' \qquad A_{pa} \Uparrow p' : A' \qquad \Gamma_{na}, \Gamma' \vdash t : A'}{\Gamma_{na} \vdash \mathbf{let} \bar{x} = \bar{n} \text{ in } p't : A_{pa}}
$$

$$
\frac{A \Uparrow^? \emptyset : A}{A \Uparrow^? \emptyset : A} \qquad \frac{A_p \Uparrow p : B_{na}}{A_p \Uparrow^? p : B_{na}} \qquad \frac{(x^i : A_n^i)^{i \in I} \subseteq \Gamma \qquad (\Gamma; x^i : A_n^i \Downarrow n^i : A_{pa}^{i^I})^{i \in I}}{\Gamma \Downarrow \mathbf{let} (x^i)^{i \in I} = (n^i)^{i \in I} : (A_{pa}^{i^I})^{i \in I}}
$$

$$
n ::= \begin{array}{ll}
& \text{negatives} \\
\mid x, y, z & \text{variable} \\
\mid \pi_i n & \text{pair projection} \\
\mid n p(t) & \text{function application} \\
\mid \mathbf{let} \bar{x} = \bar{n} \text{ in } n & \text{focusing (only in the preemptive calculus)}
\end{array}
$$

$$
\frac{\Gamma; A \Downarrow n : B \to C \qquad B \Uparrow p : B' \qquad \Gamma \vdash t : B'}{\Gamma; A \Downarrow n p(t) : C} \qquad \frac{\Gamma; A \Downarrow n : B_1 \times B_2}{\Gamma; A \Downarrow \pi_i n : B_i} \quad i \in \{1, 2\}
$$

$$
\frac{\Gamma_{npa} \Downarrow \mathbf{let} (x^i)^{i \in I} = (n^i)^{i \in I} : \Delta'_{pa} \qquad \Gamma_{npa}, \Delta'_{pa}; A \Downarrow n' : A'}{\Gamma_{npa}; A \Downarrow \mathbf{let} (x^i)^{i \in I} = (n^i)^{i \in I} \text{ in } n' : A'}
$$

$$
p ::= \begin{array}{ll}
& \text{positives} \\
\mid \star & \text{identity} \\
\mid \sigma_i p & \text{sum injection}
\end{array}
\qquad
\frac{A_i \Uparrow p : B}{A_1 + A_2 \Uparrow \sigma_i pB} \quad i \in \{1, 2\}
$$

Figure 5 Preemptive term calculus

positive types. The rewriting rules corresponding to the preemptive rewriting relation are
defined in Figure 6.

► **Lemma 3.** If *t* is a proof term for the preemptive derivation *D*, then *t* → *u* if and only if *u* is a proof term for a preemptive derivation *E* with *D* → *E*.

**Proof.** Immediate by inspection on both rewriting relations.

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

The reinversion relation also has a corresponding term-rewriting interpretation. To
<figure><img src="image_8.png" /><figcaption>Figure 6 Preemptive rewriting on proof terms</figcaption></figure>

perform each invertible rule as early as it should be, it suffices to let any invertible rule skip over a non-invertible phase it does not depend on. Depending on the order of the invertible rules after this phase, the invertible rule we want to move may be after a series of invertible rules that cannot be moved.

We “skip” over invertible contexts, we reduce invertible rules happening inside contexts of the form $C_{ni}[C_i[\quad]]$, where $C_i[t]$ is a notation for invertible contexts (defined using invertible frames $F_i[t]$), and $C_{ni}[t]$ for non-invertible contexts. Defining the latter requires describing negative/elimination contexts $C_{neg}[t]$, with holes where a term may appear in a series of elimination-focused terms.

<figure><img src="image_9.png" /><figcaption>Figure 7 Invertible frames and contexts, non-invertible contexts and elimination contexts.</figcaption></figure>

**► Definition 4.** Reinversion can be precisely defined as the transitive congruence closure of the rewrite rules listed in Figure 8.

<figure><img src="image_10.png" /><figcaption>Figure 8 Reinversion rewrite rules</figcaption></figure>

The rewrite conditions are expressed in terms of a $C[\Box] \prec c$ relation (read “context C”
blocks term-constructor c”) that indicates a dependency of an invertible construction c on a given context C[□]. For example, it would make no sense to extrude a λ in argument position in a destructor, or move a sum-elimination δ(x) across the frame that defined the variable x. This blocking relation is defined in Figure 9 – (A | B) in a rule means that the rule holds with either A or B in place of (A | B).

$$
\begin{align*}
& c ::= (,) | \lambda | \delta(x) \\
& \frac{y \in \bar{x} \qquad p \neq \emptyset \qquad C_{\text{neg}}[\Box] \prec c}{\text{let } \bar{x} = \bar{n} \text{ in } p^2\Box \prec \delta(y) \qquad \text{let } \bar{x} = \bar{n} \text{ in } p\Box \prec (,) | \lambda \qquad \text{let } \bar{x}, y = \bar{n}, C_{\text{neg}}[\Box] \text{ in } p^2t \prec c} \\
& ((\Box, t) | (t, \Box) | \lambda(x)\Box) \prec ((,) | \lambda) \qquad \lambda(x)\Box \prec \delta(x) \qquad (\delta(x, y.\Box, z.t) | \delta(x, z.t, y.\Box)) \prec \delta(y) \\
& \frac{n p(\Box) \prec (,) | \lambda \qquad C_{\text{neg}}[\Box] \prec c}{C_{\text{neg}}[\Box] p(t) | \pi_i C_{\text{neg}}[\Box] | C_{ni}[C_{\text{neg}}[\Box]] \prec c} \\
& \frac{C_{ni}[\Box] \prec c | C_{\text{neg}}[\Box] \prec c}{C_{ni}[C_{\text{neg}}[\Box]] \prec c} \qquad \frac{F_i[\Box] \prec c | C_i[\Box] \prec c}{F_i[C_i[\Box]] \prec c} \qquad \frac{C_{ni}[\Box] \prec c | C_i[\Box] \prec c}{C_{ni}[C_i[\Box]] \prec c}
\end{align*}
$$

<caption>Figure 9 Reinversion blocking relation</caption>

It may at first seem surprising that reinversion rules have instances that are the *opposite* of some of the preemptive rewriting rules – those about pos/neg permutations. But that is precisely one of the purposes of reinversion: after preemptive rewriting rules have been fully applied, we undo those that have gone “too far”, in the sense that they let a non-invertible phase preempt a portion of an invertible phase below, but were blocked by dependencies without reaching the next non-invertible phase. This blocked phase does not increase the parallelism of multi-focusing in the proof, but stops the derivation from being valid in the original multi-focusing system, so reinversion undoes its preemption.

Remark, in relation to this situation, that preemptive rewriting cannot be easily defined on equivalence classes of neg/neg permutations (or other presentations of focusing that crush the invertible phase in one not-so-interesting step, such as higher-order focusing), as the order of the invertible rules in a single phase may determine where a non-invertible phase stops its preemption and is blocked in the middle of the invertible phase. Reinversion restores this independence on invertible ordering. This explains why the meta-theory of maximal multi-focusing was conducted in the non-preemptive system, using the relation between proofs that always applies reinversion after preemptive rewriting.

The other interesting case is a non-invertible phase $\pi_0$ having traversed a family of non-invertible phases $(\pi'_i)_{i \in I}$, before merging into some non-invertible phase $\pi_1$. Reinversion will move its negative phase $\nu_0$, reverting the preemption of the $(\pi'_i)$ on the invertible formulas introduced by $\pi_0$. But the important preemptions that happened, namely the traversal by $\pi_0$ of each of the invertible phases $(\nu'_i)_{i \in I}$, are not reverted: each $\nu'_i$ is blocked by the $\pi'_i$ below and thus cannot be reverted below $\pi_0$. As $\pi_0$ traversed both the $\nu'_i$ and the $\pi'_i$, it does not have the corresponding invertible formulas in its context anymore, and is well-positioned even in a non-preemptive proof.

**Lemma 5.** If *t* is the proof term of the preemptive derivation *D* : Γ ⊢ A, and *u* is such that *t* ▷ *u*, then *u* is a valid (preemptive) proof term for Γ ⊢ A.

**Proof.** See Appendix C.2.

<figure><img src="image_11.png" /></figure>
**▶ Lemma 6.** If $u$ is a valid proof term in the preemptive system, and a normal form of the relation ($\triangleright$), then $u$ is also a valid proof term for the non-preemptive system.

**Proof.** See Appendix C.4

**▶ Theorem 7.** If $t$ is a proof term for $\mathcal{D}$ and $u$ for $\mathcal{E}$, then $\mathcal{D} \Rightarrow \mathcal{E}$ if and only there is a $u'$ such that $t \to^* u' \triangleright u$, and $u$ is a normal form for ($\triangleright$).

## 3.2 Multi-focused terms as lambda-terms

There is a natural embedding $\lfloor t \rfloor$ of a multi-focused term $t$ into the standard lambda-calculus, generated by the following transformation, where $t[\bar{x} := \bar{u}]$ represents simultaneous substitution:

$$ \lfloor \text{let } \bar{x} = \bar{n} \text{ in } p^? t \rfloor := \lfloor p^? \rfloor(\lfloor t \rfloor[\bar{x} := \lfloor \bar{n} \rfloor]) $$

$$ \lfloor \emptyset \rfloor(t) := t $$

$$ \lfloor \star \rfloor(t) := t $$

$$ \lfloor \sigma_i p \rfloor(t) := \sigma_i \lfloor p \rfloor(t) $$

The substitutions break the invariant that the scrutinee of a sum-elimination construct is always a variable. However, as only negative terms are substituted, sum-elimination scrutinee are always neutrals – embedding of negative terms. In particular, this embedding does not create any $\beta$-redex. Proof terms coming from non-preemptive multi-focusing are also always in $\eta$-long form, and this is preserved by the embedding; with the restriction present in Lindley’s work that only neutral terms (eliminations) are expanded – this avoids issues of commuting conversions. We mean here the weak $\eta$-long form, determined by the weak equation ($m : A + B$) $=_{\text{weak-}\eta} \delta(m, x_1.\sigma_1 x_1, x_2.\sigma_2 x_2)$.

**▶ Lemma 8.** If $\Gamma \vdash t : A$ in the preemptive multi-focused system, then $\Gamma \vdash \lfloor t \rfloor : A$ in simply-typed lambda-calculus, and $\lfloor t \rfloor$ is in $\beta$-normal form. If $t$ is valid in the non-preemptive system, then the pure neutral subterms of $\lfloor t \rfloor$ are also in weak $\eta$-long form.

**Proof.** See Appendix C.3.

## 3.3 Lindley’s rewriting relation

The strong $\eta$-equivalence for sums makes lambda-term equivalence a difficult notion. For any term $m : A+B$ and well-typed context $C[\Box]$, it dictates that $C[m] \approx \delta(m, x_1.C[x_1], x_2.C[x_2])$. In his article [Lin07], Sam Lindley breaks it down in four simpler equations, including in particular the “weak”, non-local $\eta$-rule (where $F$ represents a frame, that is a context of term-size exactly 1):

$$ m \approx \delta(m, x_1.\sigma_1 x_1, x_2.\sigma_2 x_2) \quad (+.\eta) $$

$$ F[\delta(p, x_1.t_1, x_2.t_2)] \approx \delta(p, x_1.F[t_1], x_2.F[t_2]) \quad (\text{move-case}) $$

$$ \delta \left( p, \begin{array}{l} x_1.\delta(p, y_1.t_1, y_2.t_2), \\ x_2.\delta(p, z_1.u_1, z_2.u_2) \end{array} \right) \approx \delta(p, x_1.t_1[y_1 := x_1], x_2.u_2[z_2 := x_2]) \quad (\text{repeated-guard}) $$

$$ \delta(p, x_1.t, x_2.t) \stackrel{x_1, x_2 \notin t}{\approx} t \quad (\text{redundant-guard}) $$

Lindley further refines the *move-case* equivalence into a less-local *hoist-case* rule. Writing $D$ for a frame that is either $\delta(p, x_1.\Box, x_2.t)$ or $\delta(p, x_1.t, x_2.\Box)$, $D^*$ for an arbitrary (possibly empty) sequence of them, and $H$ any frame that is not of this from, *hoist-case* is defined as:

$$ H[D^*[\delta(t, x_1.t_1, x_2.t_2)]] \to \delta(t, x_1.H[D^*[t_1]], x_2.H[D^*[t_2]]) $$
Lindley's equivalence algorithm (Theorem 36, p. 13) proceeds in three steps: rewriting terms in $\beta\eta\gamma_E$-normal forms (using the weak $(+\cdot\eta)$ on sums), then rewriting them in $\gamma$-normal form, and finally using a decidable redundancy-eliminating equivalence relation called $\sim$. The rewriting relation $\gamma$ is defined as the closure of repeated-guard, redundant-guard (when read left-to-right) and hoist-case; $\gamma_E$ is a weak restriction of it defined below. The equivalence $\sim$ is the equivalence closure of the equivalence repeated-guard, redundant-guard, and move-case restricted to D-frames – clauses of a sum elimination.

We discuss redundancy elimination, that is aspects related to repeated-guard and redundant guard, in Section 4, and focus here on explanation of the other rewriting processes ($\beta\eta\gamma_E$ and hoist-case) in logical terms. We show that multi-focused terms in ($\Rightarrow$)-normal form embed into $\beta\eta\gamma_E\gamma$-normal forms. As we ignore redundancy elimination, this is modulo $\sim$.

The $\beta$ and $\eta$ rewriting rules are standard – for sums, this is the weak, local $\eta$-relation, and not the strong $\eta$-equivalence. As explained in the previous subsection, embeddings of proof terms valid in the non-preemptive system – as are ($\Rightarrow$)-normal forms – are in $\beta\eta$-normal form. The rewriting $\gamma_E$ is defined as the extrusion of a sum-elimination out of an elimination context: $\Box t \mid \pi_i \Box \mid \delta(\Box, x_1.t, x_2.t)$.

**Lemma 9.** *Terms for valid preemptive multi-focusing derivations are in $\gamma_E$-normal form.*

**Proof.** This comes from the static structure of valid focused proofs: contexts $\Box t$ and $\pi_i \Box$ may only contain negative terms, which exclude sum eliminations, and variables of sum-elimination scrutinees may only be bound to negative terms, so their embedding cannot be a sum elimination either. $\quad \blacksquare$

This rigid structure of focused proofs is well-known, just as $\beta\eta$-normality or commuting conversions are not the interesting points of Lindley's work. The crux of the correspondence is between the transformation to maximal proofs, computed by ($\Rightarrow$), and his $\gamma$-rewriting relation. There is an interesting dichotomy:

- Preemptive rewriting, which merges non-invertible phases, is where most of the work happens from a logical point of view. Yet this transformation, on the embeddings of the multi-focused proof terms, corresponds to the identity!

- Reinversion, which is obvious logically as it only concerns invertible rules which commute easily, corresponds to $\gamma$-rewriting on the embeddings.

Of course, preemptive rewriting is in fact crucial for $\gamma$-rewriting. It is the one that determines upto where negative terms can move in the derivation, and in particular the scrutinees of sum eliminations. Reinversion would not work without the first preemptive rewriting step, and applying reinversion on a proof term that is not in preemptive-normal form may not give a $\gamma$-normal embedding. Note that the proof of the last theorem in this section makes essential use of the confluence of $\gamma$-rewriting, one of Lindley's key results.

**Lemma 10.** If $t \to u$, then $\lfloor t \rfloor =_\alpha \lfloor u \rfloor$.

**Proof.** Immediate by inspection of the term-level preemptive-rewriting rules. $\quad \blacksquare$

**Lemma 11.** If $t \triangleright u$, then $\lfloor t \rfloor \to_{\gamma}^* \lfloor u \rfloor$.

**Proof.** See Appendix C.5. $\quad \blacksquare$

**Lemma 12.** If $u$ is in ($\Rightarrow$)-normal form, then for some $u' \approx_{loc} u$, $\lfloor u' \rfloor$ is in $\gamma$-normal form modulo $\sim$.

**Proof.** See Appendix C.5. $\quad \blacksquare$
14 Multi-focusing on extensional rewriting with sums

**Theorem 13** ($\gamma$-normal forms are embeddings of maximally-focused proofs). If $[t] \to_{\gamma}^* n$ and $n$ is $\gamma$-normal, then there are $u \approx_{\text{loc}} u'$ such that $t \Rightarrow u$ and $[u'] \sim n$. In particular, $u$ is maximally multi-focused.

**Proof.** See Appendix C.5

4 Redundancy elimination

In the previous section, we have glossed over the fact that Lindley's $\gamma$-reduction also simplifies redundant and duplicated sum-eliminations. Those simplifications are *not* implied by multi-focusing – they are not justified by proof theory alone. Our understanding is that they correspond to purity assumptions that are stronger than the natural equational theory of focused proofs. On the other hand, starting from maximally multi-focused forms is essential to being able to define those extra simplifications. We do so in this section, to obtain a system that is completely equivalent to Lindley's.

We simply have to add the following simplifications on proof terms:

REDUNDANT-FOCUS

$$ \text{let } \bar{x}, y, z = \bar{n}, n', n' \text{ in } p^2 t \to_s \text{ let } \bar{x}, y = \bar{n}, n' \text{ in } p^2 t[z:=y] $$

REDUNDANT-GUARD

$$ \delta(x, x_1.t, x_2.t) \stackrel{x_1, x_2 \notin t}{\approx_{\text{loc}}} t $$

REPEATED-CASE-1

$$ \delta(x, x_1.\delta(x, y_1.u_1, y_2.u_2), x_2.t_2) \approx_{\text{loc}} \delta(x, x_1.u_1[y_1:=x_1], x_2.t_2) $$

REPEATED-CASE-2

$$ \delta(x, x_1.t_1, x_2.\delta(x, y_1.u_1, y_2.u_2)) \approx_{\text{loc}} \delta(x, x_1.y_1, x_2.u_2[y_2:=x_2]) $$

While those rules are not implied by focusing, they are reasonable in a focused setting, as they respect the phase separation. As the redundancy-elimination rules test for equality of subterms, they have an unpleasant non-atomic aspect (repeated cases only test variables), but this seems unavoidable to handle sum equivalence (Lindley [Lin07], or Balat, Di Cosmo and Fiore [BCF04], have a similar test in their normal form judgments), and have also been used previously in the multi-focusing literature, for other purposes; in Alexis Saurin's PhD thesis [Sau08], an equality test is used to give a convenient $\otimes/\&$ permutation rule (p. 231).

One should however remark that they break the property of preserving the initial sequents of proofs (when seen as a multiset), property which was carefully preserved by our previous notions of equivalence. Yet we only apply these simplifications after reduction to maximally multi-focused proofs, they do not interfere with previous canonicity results for maximal multi-focusing.

**Definition 14.** We define the relation $t \Rightarrow_s u$ between proof terms of the (preemptive) multi-focusing calculus as follows, where $t_1$ is a preemptive normal form, $t_2$ is a redundant-foci normal form, and $u_0$ is a ($\vdash$)-normal form: $t \to^* t_1 \to_s^* t_2 \vdash^* u_0 \approx_{\text{loc}} u$

**Definition 15.** We call the $u$ in the target of the ($\Rightarrow_s$) relation simplified maximal forms.

Having embedded redundancy-elimination in the definition of maximal forms, we can now get strong correspondence results between ($\Rightarrow_s$)-normal and $\gamma$-normal forms.

**Theorem 16 (Simplified maximal forms are $\gamma$-normal).** Given a multi-focused term $t$, there exists some $u$ such that $t \Rightarrow_s u$, $[t] \to_{\gamma}^* [u]$, and $[u]$ is in $\gamma$-normal form. This $u$ is unique modulo local equivalence.

**Proof.** See Appendix C.6.
**► Corollary 17.** *Two multi-focused proof terms are extensionally equivalent if their maximally multi-focused normal forms are locally equivalent (modulo redundancy elimination).*

## Related and Future work

Maximally multi-focused proofs were previously used to bridge the gap between sequent calculus, as a rather versatile way of defining proof systems, and specialized proof structures designed to minimize redundancy for a fixed logic. The original paper on multi-focusing [CMS08] demonstrated an isomorphism between maximal proofs and proof nets for a subset of linear logic. In recent work [CHM12], maximally multi-focused proof of a sequent calculus for first-order logic have been shown isomorphic to *expansion proofs*, a compact description of first-order classical proofs.

There are some recognized design choices in the land of equivalence-checking presentation that can now be linked to design choices of focused system. For example, Altenkirch et al. [ADHS01] proposed to make the syntax more canonical with respect to redundancy-elimination by using a n-ary sum elimination construct, while Lindley prefers to quotient over local reorderings of unary sum-eliminations. This sounds similar to the choice between higher-order focusing ([Zei09]), where all invertible rules are applied at once, or quotienting of concrete proofs by neg/neg permutations as used here.

When we started this work, we planned to also study the proof-term presentation of preemptive rewriting, in a term language for sequent calculus. We have been collaborating with Guillaume Munch-Maccagnoni to study the normal forms of an intuitionistic restriction of System L, with sums. In this untyped calculus, syntactic phases appear that closely resemble a focusing discipline, and equivalence relations can be defined in a more uniform way, thanks to the symmetric status of the (non)-invertible rules that “change the type of the result” (terms, values) and those that only manipulate the environments (co-terms, stacks).

## Conclusion

We propose a multi-focused calculus for intuitionistic logic in natural deduction, and establish the canonicity of maximally multi-focused proofs by transposing the preemptive rewriting technique [CMS08] in our intuitionistic, natural deduction setting. By studying the computational effect of preemptive rewriting on proof terms, we demonstrate the close correspondence with the rewriting on lambda-terms with sums proposed by Lindley [Lin07] to compute extensional equivalence. Adding a notion of redundancy elimination to our multi-focused system makes preemptive rewriting precisely equivalent to Lindley’s $\gamma$-rules. In particular, the resulting canonical forms, *simplified maximal proofs*, capture extensional equality.

## Acknowledgements

The author thanks his advisor, Didier Rémy for the freedom of making an overly long detour through the proof search literature; Alexis Saurin for his advice, and Pierre-Évariste Dagand, Sam Lindley, and anonymous reviewers for their helpful comments.

## References

* ADHS01 Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Philip J. Scott. Normalization by evaluation for typed lambda calculus with coproducts. In *LICS*, 2001.
BCF04 Vincent Balat, Roberto Di Cosmo, and Marcelo P. Fiore. Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums. In *POPL*, 2004.

BNS10 Taus Brock-Nannestad and Carsten Schürmann. Focused natural deduction. In *LPAR (Yogyakarta)*, 2010.

CHM12 Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller. A Systematic Approach to Canonicity in the Classical Sequent Calculus. In *21st EACSL Annual Conference on Computer Science Logic*, volume 16, September 2012.

CMS08 Kaustuv Chaudhuri, Dale Miller, and Alexis Saurin. Canonical sequent proofs via multi-focusing. In *IFIP TCS*, 2008.

Gha95 N Ghani. Beta-eta equality for coproducts. In *Proceedings of TLCA '95*, number 902 in Lecture Notes in Computer Science. Springer-Verlag, 1995.

Kri09 Neelakantan R. Krishnaswami. Focusing on pattern matching. In *POPL*, 2009.

Lin07 Sam Lindley. Extensional rewriting with sums. In *TLCA*, 2007.

MS07 Dale Miller and Alexis Saurin. From proofs to focused proofs: A modular proof of focalization in linear logic. In *CSL*, 2007.

Sau08 Alexis Saurin. *Une étude logique du contrôle (appliquée à la programmation fonctionnelle et logique)*. PhD thesis, École Polytechnique, 2008.

Sim11 Robert J. Simmons. Structural focalization. CoRR, abs/1109.6273, 2011.

Zei09 Noam Zeilberger. *The Logical Basis of Evaluation Order and Pattern-Matching*. PhD thesis, Carnegie Mellon University, 2009.
# A The many faces of reinversion

## Reinversion as a rewriting relation

We can define reinversion by permuting some invertible phases downward in the derivation. We know this is always possible as neg/neg and neg/pos permutations, those where an invertible rule is originally at the top, always preserve provability. Invertibility properties are clearly explained in Alexis Saurin's thesis.

We will show (Corollary 28) that global equivalence, that is equivalence modulo arbitrary rule permutations, can be decided by complete preemptive rewriting followed by reinversion. This is a sequentialization of permutations (after quotienting on "local" pos/pos and neg/neg permutations): instead of an arbitrary sequence of permutations, we can just perform a series of pos/neg permutations (preemptive rewriting), followed by a series of neg/pos permutations (reinversion).

While rewriting is the simplest way to define reinversion, we will refrain from defining it explicitly now as it is quite verbose, and less interesting than the preemptive rewriting rules. The rewrite steps will be written in full in Section 3.1 on proof terms for multi-focusing, where they can be more concisely expressed.

## Reinversion as partial evaluation

Instead of moving some invertible phases downwards in the derivation, we could traverse it from the root to the leaves. Each time we encounter a positive phase $\pi$; $\nu$ that preempts some invertible formulas, we could change it to first perform the necessary invertible phase, then $\pi$. We can do that without looking at $\nu$, the actual positive phase that was preempted, and is above in the derivation, as invertibility guarantees that any application order will be equivalent – this is thus fairly different from seeing reinversion as a rewriting relation, although it is equivalent modulo permutation of invertible rules.

In each leaf of the invertible phase, we can then add the negative phase $\pi$ and continue traversing the original derivation. When we encounter the original phase $\nu$, we should simplify it, according to the branch we are in. For example, if one of the invertible rules was an elimination of $A+B$, this elimination has been reenacted below $\pi$; we are either in the $A$ or the $B$ branch and can remove the sum-elimination accordingly.

It is very easy to define this transformation formally by relying on a cut-elimination result. Consider the following derivation, preempting the non-invertible phase $\pi$ over the invertible hypothesis $A+B$:

$$ \frac{S}{\pi; (A+B)} \Gamma_n, A+B \vdash C $$

Assuming the admissibility of a cut rule, we can transform it into:

$$ \begin{array}{ccc} \text{CUT} & & \text{CUT} \\ \begin{array}{c} \vdots \\ A \vdash A+B \end{array} & & \begin{array}{c} S \\ \pi; (A+B) \end{array} \\ & \Gamma_n, A+B \vdash C & \vdots \\ & & B \vdash A+B \\ & & \begin{array}{c} S \\ \pi; (A+B) \end{array} \\ & & \Gamma_n, A+B \vdash C \\ & \Gamma_n, A \vdash C & \Gamma_n, B \vdash C \\ & & \Gamma_n, A+B \vdash C \end{array} $$
More generally, for any proof $S$ against a positive context $\Sigma_p$, we can first perform an identity-expansion of $\Sigma_p$ and, at each leaf, cut against $S$. The cut-elimination process then removes any invertible rules against $\Sigma$ in $S$. If a negative is the succedent, we can similarly $\eta$-expand then cut.

Reinversion corresponds to performing that transformation, on all invertible formulas of the sequents before any multi-focusing rule of the input derivation.

## Reinversion as completeness of focusing

In Alexis Saurin's PhD thesis [Sau08], the reinversion operation is somewhat hidden in the proof that two multi-focusing phases can be merged by moving non-invertible phases downward (Theorem 10.16, p. 234): it simply mentions that reconstructing a valid multi-focused proof is exactly the same technique as the one used to establish the completeness of (single)-focusing in the first place.

In the present work, we are interested in the computational meaning of reinversion, to be able to see where it fits in Lindley's algorithm. We therefore present it as an explicit computation, instead of the implicit application of a proof.

# B Maximal multi-focusing and canonicity

**Definition 18.** We say that two proofs $\mathcal{D}$ and $\mathcal{E}$ are locally equivalent, or iso-polar, written $\mathcal{D} \approx_{\text{loc}} \mathcal{E}$, if one can be rewritten into the other using only local positive/positive and negative/negative permutations, preserving their initial sequents.

**Definition 19.** We say that two proofs $\mathcal{D}$ and $\mathcal{E}$ are globally equivalent, or iso-initial, written $\mathcal{D} \simeq_{\text{glob}} \mathcal{E}$, when one can be rewritten into the other using local permutations of any polarity (so when seen as proofs in a non-focused system), preserving their initial sequents.

**Definition 20.** We define $\text{roots}(\mathcal{D})$, where $\mathcal{D}$ is a derivation in the non-preemptive multi-focusing calculus, as the set of formulas over focus in its lowest multi-focusing rule, or $\emptyset$ if it has none.

**Definition 21.** A derivation $\mathcal{D}$ is maximally multi-focused, or maximal, if, for any sub-derivation $\mathcal{D}'$ of $\mathcal{D}$, for any proof $\mathcal{E}' \simeq_{\text{glob}} \mathcal{D}'$ we have $\text{roots}(\mathcal{E}') \subseteq \text{roots}(\mathcal{D}')$.

**Lemma 22 (Soundness and monotonicity of preemptive rewriting).** If $\mathcal{D} \Rightarrow \mathcal{E}$ then $\mathcal{D} \simeq_{\text{glob}} \mathcal{E}$ and $\text{roots}(\mathcal{D}) \supseteq \text{roots}(\mathcal{E})$.

*Proof.* Immediate, by inspection of each rewrite rule.

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

**Lemma 23 (Maximal proofs are normal forms (left decomposition)).** If $\mathcal{D}$ is maximal and $\mathcal{D} \Rightarrow \mathcal{E}$, then $\mathcal{D} \approx_{\text{loc}} \mathcal{E}$.

*Proof.* The proof is essentially identical to the original one [CMS08]. In each of the preemptive rewrite rules, a focusing rule is brought closer to the root of the derivation, and the rest of the structure is preserved.

For any subderivation $\mathcal{D}'$ of $\mathcal{D}$, there is a corresponding subderivation $\mathcal{E}'$ of $\mathcal{E}$ with $\mathcal{D}' \Rightarrow \mathcal{E}'$ – even if no rewrite happened in this subderivation, we take $\mathcal{E}' = \mathcal{D}'$. By monotonicity we have $\text{roots}(\mathcal{D}') \subseteq \text{roots}(\mathcal{E}')$. By soundness we have $\mathcal{D}' \simeq_{\text{glob}} \mathcal{E}'$ and, by maximality, $\text{roots}(\mathcal{D}') \supseteq \text{roots}(\mathcal{E}')$. So we have $\text{roots}(\mathcal{D}') = \text{roots}(\mathcal{E}')$: the multi-focusing rules in $\mathcal{D}$ and $\mathcal{E}$ are equivalent modulo local permutations. As the rest of the rules also are, we have $\mathcal{D} \approx_{\text{loc}} \mathcal{E}$.

<figure><img src="image_13.png" /></figure>
To our knowledge, the following lemma was not part of previous characterizations of maximal proofs.

**Lemma 24 (Normal forms are maximal).** If $\mathcal{D}$ is such that $\mathcal{D} \approx_{\text{loc}} \mathcal{E}$ whenever $\mathcal{D} \Rightarrow \mathcal{E}$, then $\mathcal{D}$ is maximal.

**Proof.** By contraposition, let us assume that $\mathcal{D}$ is not maximal and rewrite it into some $\mathcal{E}$ such that $\mathcal{D} \not\approx_{\text{loc}} \mathcal{E}$.

If $\mathcal{D}$ is not maximal, there is a subderivation $\mathcal{D}'$ of it and a counter-example $\mathcal{E}'$ such that $\mathcal{D}' \simeq_{\text{glob}} \mathcal{E}'$ but $\text{roots}(\mathcal{E}') \not\subseteq \text{roots}(\mathcal{D}')$. We call interesting the foci that are in $\text{roots}(\mathcal{E}')$ but not in $\text{roots}(\mathcal{D}')$ – there is at least one. Given that those two subproofs are globally equivalent, they can still be found somewhere in $\mathcal{D}'$, just not in the first multi-focusing rule; they are in another, separated by a non-empty sequence of invertible rules – as those are proofs in the non-preemptive system.

We claim that these interesting foci could be moved down in $\mathcal{D}'$ – along with their complete sequences of non-invertible rules. A focus can only be moved down if it does not depend on the rules below, or if they can themselves be moved down. But we know that they do not depend on any other focus of $\mathcal{D}'$, as they are present in the very first multi-focusing rule of $\mathcal{E}'$ and global rule permutations do preserve dependencies. We can therefore move them to the root of $\mathcal{D}'$.

This gives a new sub-proof, $\mathcal{D}''$, that is globally equivalent to $\mathcal{E}'$ and $\mathcal{D}'$, but not locally equivalent to $\mathcal{D}'$: we permuted non-invertible rules below invertible rules. We conclude by defining $\mathcal{E}$ as $\mathcal{D}[\mathcal{D}''/\mathcal{D}']$, or $\mathcal{D}$ where its subproof $\mathcal{D}'$ is replaced by $\mathcal{D}''$. We have $\mathcal{D}' \Rightarrow \mathcal{D}''$, hence $\mathcal{D} \Rightarrow \mathcal{E}$, but $\mathcal{D} \not\approx_{\text{loc}} \mathcal{E}$.

These two lemmas provide a computable characterization of maximal proofs: they are the normal forms of the preemptive rewriting relation.

**Theorem 25 (Characterization of maximality).** Maximal proofs are exactly the normal form, upto local equivalence, of the rewriting relation.

We can also prove that they are unique modulo global equivalence.

**Lemma 26 (Completeness of preemptive rewriting (right decomposition)).** If $\mathcal{D} \simeq_{\text{glob}} \mathcal{E}$ and $\mathcal{E}$ is maximal, then $\mathcal{D} \Rightarrow \mathcal{E}$.

**Proof.** As in the original paper [CMS08]. We proceed by case analysis on rule permutations that send a focus down. For each, we can verify that it is a valid preemptive rewriting.

**Theorem 27 (Canonicity).** If two maximally multi-focused proofs are globally equivalent, they are in fact locally equivalent.

**Proof.** As in the original paper [CMS08]: if $\mathcal{D} \simeq_{\text{glob}} \mathcal{E}$ are both maximal, then $\mathcal{D} \Rightarrow \mathcal{E}$ by completeness (Lemma 26), but the maximal proof $\mathcal{D}$ is a normal form (Lemma 23) so $\mathcal{D} \approx_{\text{loc}} \mathcal{E}$.

**Corollary 28.** Two multi-focused proofs are globally equivalent if and only if they are rewritten by (⇒) in locally equivalent maximal proofs.
C Additional proofs

C.1 Equivalence of sequent-calculus and natural-deduction
multifocused calculi

**Proof of Lemma 1.** Our proof is similar in spirit to the usual proofs of equivalence between sequent calculus and natural deduction: reversing a sequence of left-focusing rules in sequent calculus upside-down gives a sequence of elimination-focused rules in natural deduction – and conversely.

For an example, consider the following proof:

$$
\frac{
  \frac{
    \frac{
      (X \times Y) \times Z, X \vdash X
    }{
      (X \times Y) \times Z, [X] \vdash X
    }
  }{
    (X \times Y) \times Z, [X \times Y] \vdash X
  }
  \frac{
    (X \times Y) \times Z, [(X \times Y) \times Z] \vdash X
  }{
    (X \times Y) \times Z \vdash X
  }
}{
  (X \times Y) \times Z \vdash X
}
$$

It gets reversed into the corresponding natural deduction derivation:

$$
\frac{
  \frac{
    (X \times Y) \times Z \vdash (X \times Y) \times Z
  }{
    (X \times Y) \times Z \vdash (X \times Y)
  }
  \frac{
    (X \times Y) \times Z \vdash X
  }{
    (X \times Y) \times Z \vdash X
  }
}{
  (X \times Y) \times Z \vdash X
}
$$

We show how to map each fragment of a derivation starting with a focusing rule and
ending with release rules – in fact exactly one release rule – from one system to another.
This is sufficient, as we can then rewrite whole derivations by structural induction from the
leaves to the root.

Let us now consider the general case of a focused sequence *S* surrounded by a multi-
focusing and a release rule

$$
\frac{
  \frac{\pi}{\Gamma_{na}, \Delta'_{pa} \vdash B_{pa} \mid C'_{na}}
}{
  \frac{S}{\Gamma_{na}, [\Delta'_{pa}] \vdash B_{pa} \mid [C'_{na}]}
}
\frac{
  \Gamma_{na}, [\Delta_n] \vdash B_{pa} \mid [C_p]
}{
  \Gamma_{na}, \Delta_n \vdash B_{pa} \mid C_p
}
$$

The contexts $\Delta_n$ and $\Delta'_{pa}$ are multisets of the same cardinality (as can be checked by a direct induction on the non-invertible left-introduction rules); let $I$ be a family of indices over those multisets, such that $\Delta_n$ is some family $(A_n^i)_{i \in I}$ and $\Delta'_{pa}$ is $(A_{pa}^i)_{i \in I}$.

We rewrite it into the following derivation fragment in multi-focused natural deduction:

$$
\frac{
  \frac{
    \begin{array}{c}
      \overline{\Gamma_{na}; A_n^i \Leftrightarrow A_n^i} \\
      \text{elim}(S, A_n^i)
    \end{array}
  }{
    \forall i \in I, \quad \overline{\Gamma_{na}; A_n^i \Leftrightarrow A_{pa}^i}
  }
  \frac{
    \begin{array}{c}
      \overline{B'_{na} \Uparrow B'_{na}} \\
      \text{intro}(S, B'_{na})
    \end{array}
  }{
    B_p \Uparrow^2 B'_{na}
  }
  \frac{
    \pi
  }{
    \overline{\Gamma_{na}, \Delta'_{pa} \vdash A_p \mid B'_{na}}
  }
  \begin{array}{c}
    \Gamma_{na}, \Delta_n \vdash A_p \mid B_p
  \end{array}
}{
  \Gamma_{na}, \Delta_n \vdash A_p \mid B_p
}
$$
Where intro($S$, $B$) and elim($S$, $A^{i \in I}$) are sequences of focusing rules defined by induction on $S$:

$$ \frac{\begin{array}{c} S \\ \Gamma, [\Delta'] \vdash [B_i] \\ \Gamma, [\Delta'] \vdash [B_1 + B_2] \end{array}}{\begin{array}{c} S \\ \Gamma, [\Delta', C_k] \vdash A \mid [B] \\ \Gamma, [\Delta', (C_1 \times C_2)^i] \vdash A \mid [B] \end{array}} \quad \mapsto \quad \begin{array}{c} \text{intro}(S, B') \\ \frac{B_i \uparrow B'}{B_1 + B_2 \uparrow B'} \quad , \quad i \in I \mapsto \text{elim}(S, A^i) \\ \text{intro}(S, B') \quad , \quad \left\{ \begin{array}{c} i \mapsto \frac{\Delta; A^i \llcorner C_1 \times C_2}{\Delta; A^i \llcorner C_k} \\ j \neq i \mapsto \text{elim}(S, A^i) \\ j \neq i \mapsto \text{elim}(S, A^j) \end{array} \right. \end{array} $$

$$ \frac{\begin{array}{c} S \\ \Gamma, [\Delta', D] \vdash A \mid [B] \\ \Gamma, [\Delta', (C \to D)^i] \vdash A \mid [B] \end{array}}{\emptyset} \quad \mapsto \quad \text{intro}(S, B'), \quad \left\{ \begin{array}{c} \Gamma; A^i \llcorner C \to D \\ i \mapsto \frac{C \uparrow C}{C \uparrow C'_{na}} \quad \frac{\text{intro}(S_{arg}, C'_{na})}{\Gamma \vdash C'_{na}} \\ \Gamma; A^i \llcorner D \\ \text{elim}(S, A^i) \\ j \neq i \mapsto \text{elim}(S, A^j) \\ (\emptyset, \emptyset) \end{array} \right. $$

Note that applying an inference rule on top of elim($S$, $A^i$) is well-defined because elimination-focused rules always have exactly one elimination-focused premise, which we will call its top judgment.

Remark that the mapping we have defined is bijective on the top and bottom judgments of the focused derivation fragments – it preserves provability back and forth – but not on the derivation themselves. Indeed, several distinct focusing fragments of the sequent calculus may map to the same natural deduction fragment, if they only differ in the ordering of left- and right-introduction rules. We recover the well-known fact that natural deduction (and lambda-calculus as its term language) has less bureaucracy than sequent calculus. The sequent calculus allows for insignificant ordering that must be eliminated by quotienting over pos/pos permutations, or fixing a forced order; whereas the syntax of natural deduction exhibits a spatial parallelism between the introduction and elimination rules of a focusing sequence that structurally removes (some of the) redundancy. ◀

## C.2 Soundness of reinversion

**Proof of Lemma 5.** We will list here the derivation-level transformations that correspond to reinversion rewriting. We express them as a judgment $\Gamma \vdash A \triangleright F$, where $F$ is an invertible multi-hole context $(\lambda(x), (\Box, \Box))$ or $\delta(x, x_1, \Box, x_2, \Box)$) that is allowed to permute below a derivation for $\Gamma \vdash A$. The derivations for this judgment correspond to the (context, constructor) pairs that are absent from the blocking relation $\prec$.

$$ \overline{\Gamma \vdash A \to B \triangleright \lambda} $$

$$ \overline{\Gamma \vdash A \times B \triangleright (,)} $$

$$ \overline{\Gamma, x: A + B \vdash C \triangleright \delta(x)} $$
$$ \frac{\Gamma, x: A + B \vdash C \triangleright \delta(x)}{\Gamma, x: A + B \vdash D} \qquad \frac{\Gamma, x: A + B \vdash C \times D \triangleright \delta(x)}{\Gamma, x: A + B \vdash C} $$

$$ \frac{\Gamma, x: A + B \vdash C \quad \Gamma, x: A + B \vdash D \triangleright \delta(x)}{\Gamma, x: A + B \vdash C \times D \triangleright \delta(x)} $$

$$ \frac{\Gamma, x: A + B, \mathfrak{a}C \vdash D \triangleright \delta(x)}{\Gamma, x: A + B \vdash C \to D \triangleright \delta(x)} $$

$$ \frac{\Gamma, A \vdash c \quad \Gamma, B \vdash c}{\Gamma, A + B \vdash c} c \in \{((), \lambda)\} $$

$$ \frac{\Gamma, x: A + B, \mathfrak{a}C \vdash E \triangleright \delta(x)}{\Gamma, x: A + B \vdash E \triangleright \delta(x)} \qquad \frac{\Gamma, x: A + B, D \vdash E}{\Gamma, x: A + B \vdash D \triangleright \delta(x)} $$

$$ \frac{\Gamma, x: A + B, C \vdash E \quad \Gamma, x: A + B, \mathfrak{a}D \vdash E \triangleright \delta(x)}{\Gamma, x: A + B \vdash E \triangleright \delta(x)} $$

$$ \frac{\Gamma \Downarrow \Delta \quad \mathfrak{a} \triangleq \mathfrak{a}' \quad \Gamma, \Delta \vdash A \triangleright c}{\Gamma \vdash A \triangleright c} c \in \{((), \lambda)\} $$

$$ \frac{\Gamma, x: A + B \Downarrow \bar{y} : \Delta \quad \mathfrak{x} \in \bar{y} \quad C \triangleq^? D \quad \Gamma, x: A + B, \Delta \vdash D \triangleright \delta(x)}{\Gamma, x: A + B \vdash C \triangleright \delta(x)} $$

$$ \frac{\Gamma \Downarrow \Delta \triangleright c \quad A \triangleq^? B \quad \Gamma, \Delta \vdash B}{\Gamma \vdash A \triangleright c} $$

$$ \frac{\Gamma; \Gamma' \Downarrow \Delta, C_1 \times C_2 \triangleright \delta(x)}{\Gamma; \Gamma' \Downarrow \Delta, C_i \triangleright \delta(x)} $$

$$ \frac{\Gamma, \Gamma' \vdash C \quad \Gamma; \Gamma' \Downarrow \Delta, C \to D \triangleright \delta(x)}{\Gamma; \Gamma' \Downarrow \Delta, D \triangleright \delta(x)} $$

$$ \frac{\Gamma \Gamma' \vdash C \triangleright \delta(x) \quad \Gamma; \Gamma' \Downarrow \Delta, C \to D}{\Gamma; \Gamma' \Downarrow \Delta, D \triangleright \delta(x)} $$

$$ \frac{\Gamma; \Gamma' \Downarrow \Delta' \triangleright \delta(x) \quad \Gamma; \Gamma', \Delta' \Downarrow \Delta}{\Gamma; \Gamma' \Downarrow \Delta \triangleright \delta(x)} $$

$$ \frac{\Gamma; \Gamma' \Downarrow \Delta' \quad \Gamma; \Gamma', \bar{y} : \Delta' \Downarrow \Delta \triangleright \delta(x) \quad \mathfrak{x} \in \bar{y}}{\Gamma; \Gamma' \Downarrow \Delta \triangleright \delta(x)} $$

This shows preservation of preemptive well-typing as one then simply has to check that each inference rule

$$ \frac{\Gamma' \vdash A' \triangleright F}{\Gamma \vdash A \triangleright F} $$

verifies that if applying the rule corresponding to the constructor *F* is a correct way to start a proof of $\Gamma' \vdash A'$, then it is also a correct way to start a proof of $\Gamma \vdash A$. ◀

### C.3 beta-short eta-long normal forms of embeddings

**Lemma 8.** The (unsurprising) typing rules that connect the term syntax with the preemptive calculus for multi-focused natural deduction are given explicit in Figure 5.

Assuming $\Gamma \vdash t : A$ in the preemptive multi-focused system, we prove that $[t]$ has no constructor inside a matching destructor: it is in $\beta$-normal form.

Assuming that it in fact belongs to the non-preemptive system (or to the non-preemptive restriction of the preemptive system), we will prove that its *pure neutral subterms* are also in
η-long normal form: each subterm with a non-atomic type starts with the constructor for its head type constructor (η-expansion is already done), or is inside a destructor context for this constructor, and η-expansion would create a β-redex, or is case split δ(x,...), that is not a pure neutral term.

Note that in the case of sums, this only captures the weak η-expansion, not the general one, because this restriction only imposes adding “destructors” (δ(x)) immediately above non-constructor uses, instead of above an arbitrary context.

We will reason by case analysis on the several possible type constructors.

## Arrows

### β-short

The only possible occurrence of applications is in neutrals of the form $n p(t)$, where $n$ cannot be a λ-abstraction.

### η-long

Terms of type $A \to B$ can be produced by the judgment $\Gamma \vdash t : A \to B$, or the judgment $\Gamma \vdash A \Downarrow n : B \to C$.

A term of the form $\Gamma \vdash t : A \to B$ may either start with a right-introduction ($t = \lambda x t'$ for some $t'$), in which case it is already η-expanded, or a sum elimination ($t = \delta(x, ...)$), in which case its embedding is not a *pure neutral term* as we assumed. Note that the restriction of the axiom rule to atomic types is crucial here – otherwise $\Gamma, x : A \to B \vdash x : A \to B$ could be a non-η-long proof.

In the second case $\Gamma \vdash A \Downarrow n : B \to C$, we know that this subterm must itself be included in an inference of the form

$$ \frac{\Gamma; A \Downarrow n : B \to C \qquad B \Uparrow p : B' \qquad \Gamma \vdash t : B'}{\Gamma; A \Downarrow n p(t) : C} $$

Indeed, $B \to C$ is a negative type so it cannot be at the bottom of the focused elimination phase: the rule **NAT-START-ELIM** only accepts judgments of restricted polarity $\Gamma$; $A_n \Downarrow A'_{pa}$. This means that $n : B \to C$ appears in applied position, and η-expanding it would create a β-redex.

Remark that in the preemptive calculus, the rule below may also be a focusing let $\bar{x} = n'$ in $n$, but this gets substituted away by the embedding into λ-calculus $[\text{let } \bar{x} = n' \text{ in } n]$.

## Products

### β-short

The only possible occurrence of projections is in neutrals of the form $\pi_i n$, where $n$ cannot be a product.

### η-long

Terms of type $A \times B$ can be produced by the judgment $\Gamma \vdash t : A \times B$, or the judgment $\Gamma \vdash A \Downarrow n : B_1 \times B_2$.

A term of the form $\Gamma \vdash t : A \times B$ may either start with a right-introduction ($t = (t', u')$ for some $t', u'$), in which case it is already η-expanded, or a sum elimination ($t = \delta(x, ...)$), in which case its embedding is not a *pure neutral term* as we assumed. Note that the restriction
of the axiom rule to atomic types is crucial here – otherwise $\Gamma, x : A \times B \vdash x : A \times B$ could be a non-$\eta$-long proof.

In the second case $\Gamma \vdash A \Downarrow n : B_1 \times B_2$, we know that this subterm must itself be included in an inference of the form

$$ \frac{\Gamma; A \Downarrow n : B_1 \times B_2}{\Gamma; A \Downarrow \pi_i n : B_i} $$

Indeed, $B \times C$ is a negative type so it cannot be at the bottom of the focused elimination phase: the rule NAT-START-ELIM only accepts judgments of restricted polarity $\Gamma$; $A_n \Downarrow A'_{pa}$. This means that $n : B \times C$ appears in projected position, and $\eta$-expanding it would create a $\beta$-redex.

## Sums

### $\beta$-short

The destructor for sums only appears applied to variables: $\delta(x, x.t, x.u)$. We could have a $\beta$-redex if one of the substitutions provoked by embedding a focused term into the $\lambda$-calculus substituted a term of head $\sigma_i t$ for $x$. But this cannot happen, as only elimination neutral terms of the form $\Gamma; A \Downarrow n : A'$ are substituted, and those cannot start with a term injection.

### $\eta$-long

Conversely, whenever we have a subderivation $\Gamma; A \Downarrow n : B_1 + B_2$, it is the end of an elimination phase (no elimination rules have positive premises) and thus appear directly as a let-bound term let $x = n$ in $t$.

This binder $x$ is of positive type and it is thus necessarily eliminated in the following invertible phase. This is because in our system, all focused derivations have at least one invertible premise, and they necessarily destruct all sums in context. Note that this is not true in the preemptive system where invertible phases may stop earlier – this is where our non-preemptive assumption comes into action. The variable $x$ thus appears (and only once) in a subterm of the form $\delta(x, x.t, x.u)$.

This means that such $n$ only appear in the embedded (substituted) forms $\lfloor t \rfloor$ in the form of case-splits $\delta(\lfloor n \rfloor, x.\lfloor t \rfloor, x.\lfloor u \rfloor)$. It is not $\eta$-expansible without creating a $\beta$-redex. ◀

## C.4 Preempted proofs that are normal for reinversion are also valid non-preempted proof

**Proof of Lemma 6.** By contraposition, we show that if $u$ does use preemption, that is if a multi-focusing happens while an invertible rule is applicable, then $(\triangleright)$ can rewrite $u$ into a different proof.

A preemptive focusing is of the form

$$ \frac{\Gamma_{na}, \Sigma_p \Downarrow \Delta_p \quad A \Uparrow^? B \quad \Gamma_{na}, \Sigma_p, \Delta_p \vdash B}{\Gamma_{na}, \Sigma_p \vdash A} $$

where either $\Sigma$ is non-empty, or $A$ is negative (and $A = B$).

Supposing $\Sigma$ is non-empty, there is a non-atomic positive formula in the context of our derivation. It cannot be used by the axiom rule, which requires the variable type to be atomic, nor in the variable rule of the elimination-focused judgment which only uses negative
formulas. If it is used, it is in an invertible sum-elimination judgment higher in the derivation. This judgment either happens in the invertible phase directly above the current focusing, or later, after some other focusing higher in the derivation. In any case, the positive formula is in the context of this last focusing, and can be reinverted to be sum-eliminated just below it, which produces a distinct reinverted proof.

(If the positive hypothesis is never used, we could claim that weakening the derivation to remove it gets us closer to a valid preemptive proof. Alternatively, we have a negativity restriction on the context of the axiom rule, which enforces that it must be eliminated somewhere in any complete proof. We prefer to avoid discussing this axiom rules and potential atomic polarity assignment, as those concerns are orthogonal to the present work; we insist that this “negative axiom context” technique is not crucial to the present proof.)

Similarly, if the succedent of the focusing rule is a non-atomic negative formula, then it is either introduced in the following invertible phase, or one just after some focusing rule of the same succedent – in any case, it must be introduced before the axiom rules which requires an atomic succedent. We can move that inversion rule below the closest focusing, which produces a distinct reinverted proof. ◀

## C.5 Lindley's rewriting relation

**Proof of Lemma 11.** Our reinversion contexts $C_{ni}[C_i[ ]]$ were naturally motivated by the translation from one logical system to another – from preemptive to non-preemptive proofs; yet they closely correspond to Lindley's notion of hoisting contexts $H[D^*\square]$. However, while we permute all the syntactic construction corresponding to invertible rules, in particular lambdas and pairs, the hoist-case rule only moves sum-eliminations. We can however show that our other permutations are invisible on the embedded term:

$$ 
\begin{align*}
& C_{ni}[C_i[\lambda(x) t]] \triangleright \lambda(x) C_{ni}[C_i[t]] \\
\Rightarrow & \qquad [C_{ni}[C_i[\lambda(x) t]]] = [\lambda(x) C_{ni}[C_i[t]]] \\
& C_{ni}[C_i[(t_1, t_2)]] \triangleright (C_{ni}[C_i[t_1]], C_{ni}[C_i[t_2]]) \\
\Rightarrow & \qquad [C_{ni}[C_i[(t_1, t_2)]]] = [(C_{ni}[C_i[t_1]], C_{ni}[C_i[t_2]])]
\end{align*}
$$

This crucially relies on the blocking relation: we can immediately verify that for any $C_{ni}[C_i[ ]] such that $[C_{ni}[C_i[\lambda(x) t]]] \neq [\lambda(x) C_{ni}[C_i[t]]]$, we have $C_{ni}[C_i[ ]] \prec \lambda$, and therefore the ($\triangleright$)-reduction hypothesis cannot hold – and similarly for pairs.

In the last case where we hoist sum-eliminations, we still have to be careful because of the non-locality of the embedding $[t]$: negative terms at the very root of the focused proofs may find themselves substituted very far inside the lambda-term. The interesting case is the following rewrite, where $E[\square]$ is an arbitrary term context with $x \notin E$:

$$ \text{let } x = \delta(y, y_1.t_1, y_2.t_2) \text{ in } E[x] \qquad \triangleright \delta(y, y_1.\text{let } x = t_1 \text{ in } E[x], y_2.\text{let } x = t_2 \text{ in } E[x]) $$

While this rewrite is very local in nature, the corresponding embedding is not:

$$ [E][\delta(y, y_1.\lfloor t_1 \rfloor, y_2.\lfloor t_2 \rfloor)] \rightarrow_{\gamma}^{*} \delta(y, y_1.\lfloor E[t_1] \rfloor, y_2.\lfloor E[t_2] \rfloor) $$

The sum-elimination has been extruded out of the whole context $E$, which may be arbitrarily large and use arbitrary term constructors. This is allowed by $\rightarrow_{\gamma}$.

Furthermore, if $E$ is not linear (the hole $\square$ occurs several times in $E$), what is a single sum-elimination extrusion in the multi-focused term may in fact translate into several sum-eliminations (on the same scrutinee) in its embedding. Just applying hoist-case as many times does not produce the desired reduced term, we also have to use repeated-guard. ◀
**Proof of Lemma 12.** Even if we have $[u] \to_{\gamma} m$ for some $m$, it is impossible that a case elimination of $[u]$ could be hoisted over the constructor of a non-invertible rule: that would amount to permuting an invertible rule below a non-invertible phase, which would allow to make a step of $(\to)$-reduction from $u$ – assuming that the preemptive rewrites have been fully applied, which is the case here.

Any step of reduction from $[u]$ then corresponds to permuting a sum-elimination over a lambda or a pair constructor inside an invertible phase. We can apply those permutations fully, and get a $u' \approx_{\text{loc}} u$ such that $[u']$ is in $\gamma$-normal form. ◀

**Theorem 13.** Simply using $(\to)$ on $t$ is not enough, as a sum-elimination may then be blocked by where the focus on its scrutinee happens in $t$, while $\to^{\gamma}$ would still be able to move the elimination and its scrutinee below in the proof. We have to first rewrite $t$ into $t'$, a normal form for preemptive rewriting, and then apply reversion completely on $t'$ to get $u$. We have $[t] = [t']$ from Lemma 10, and $[t'] \to_{\gamma}^* [u]$ from Lemma 11.

Applying Lemma 12 gives us a $u' \approx_{\text{loc}} u$ such that $[u']$ is a $\gamma$-normal form modulo $\sim$. The term $n$ is also $\gamma$-normal, and both can be reached from $[t]$. Lindley proved confluence of $\gamma$-rewriting modulo $\sim$ (Proposition 28, p. 11), and we therefore have $[u] \sim n$ as desired. ◀

## C.6 Simplified maximal forms are $\gamma$-normal

**Theorem 16.** We have already shown that $(\Rightarrow)$-normal forms are $\gamma$-normal form modulo redundancy elimination and hoisting of $\delta$ over $\lambda$. A $(\Rightarrow_s)$-normal form is a $(\Rightarrow)$-normal form where *repeated-guard* and *redundant-guard* have been eliminated. Furthermore, in the $\approx_{\text{loc}}$-equivalence class of proofs $u$ such that $t \Rightarrow_s u$, we can pick the one in which invertible phases always have all sum-eliminations before any lambda or pair constructor. By construction, $[u]$ is then a $\gamma$-normal form.

Note that it is not completely obvious, a priori, that $(\Rightarrow_s)$-normal forms always embed into $\gamma$-normal form, and this crucially relies on the REDUNDANT-FOCUS rule. Indeed, consider for example the term $\text{let } y_1, y_2 = fx, fx$ in $\delta(z, z_1.y_1, z_2.y_2)$. While it is in REDUNDANT-GUARD-normal form, its embedding $\delta(z, z_1.fx, z_2.fx)$ is not. The source of the problem is that redundancy rules rely on term equality, and we may have $t \neq u$ but $[t] = [u]$.

We can prove however that maximal proofs that are REDUNDANT-FOCUS-normal forms are normal for the REPEATED-GUARD or REDUNDANT-GUARD only if their embedding is as well. It suffices to prove that if $t, u$ have no redundant cases, then $[t] = [u]$ implies $t = u$. Consider for example terms of the form $C[\pi_1 x], C[\pi_2 y]$, where $C$ is a common context – the following proof generalizes to all other cases. If $[C[\pi_1 x]] = [C[\pi_2 y]]$, there is a substitution $\sigma$ such that $x[\sigma] = y[\sigma]$, which means that either $x = y$ or they have been substituted terms of equal embedding: $\sigma$ is of the form $[x := |n_1|, y := |n_2|, \dots]$ with $|n_1| = |n_2|$. Inductively (the chain of nested substitutions is finite), we can assume that $n_1 = n_2$. As our terms are maximally preempted, the definitions $\text{let } x = n_1$ in and $\text{let } y = n_2$ in therefore happen in the same non-invertible phase ($n_1$ and $n_2$ being equal, they have the same dependencies), and can be merged by the REDUNDANT-FOCUS rule. ◀