janvier  2006  –  Journées  Francophones  des  Langages  Applicatifs–  JFLA06

Erasure and Duplication in Classical Computation

D. Žunić & P. Lescanne

Ecole Normale Supérieure de Lyon

46, Allée d’Italie, 69364 Lyon Cedex O7, France

                                       {pierre.lescanne, dragisa.zunic}@ens-lyon.fr

Abstract

We present the *X -calculus, a linear model of computation, which has a direct Curry-Howard correspondence with classical logic. The logical setting is classical sequent calculus. *X introduces terms for explicit erasure and duplication, which correspond to weakening and contraction on the logical side. Furthermore, it is a calculus of explicit substitutions. Non-confluence and interface preservation are also some of the features. Since λ-calculus is easily represented, the untyped language is Turing-complete.

1. Introduction

The fundamental connection between logic and computation is known as the Curry-Howard correspondence. Originally it was used to refer to the connection between simply typed λcalculus and intuitionistic logic. Later it became the ”Curry-Howard paradigm”, which means that this pattern of thinking was successfully applied to relate other calculi with their corresponding logics. Basically, it relates logical concepts term/reduction/type with computational concepts proof/normalization/proposition.

The first step in applying this paradigm to classical logic was done by T. Griffin [Gri90]. He noted the connection of classical logic with functional programming languages with control operators, which initiated the lively research in this area. After studying the computational content of classical natural deduction, for example the λ_{μ}-calculus of M. Parigot [Par92], people started considering classical sequent calculus, which exhibits various symmetries. There are several calculi that are based on sequent calculus formalism, for example one of the first was λ̄_{μμ̃}-calculus of P. L. Curien and H. Herbelin [CH00].

On the other side, although placed in the area of classical logic, our work has been strongly influenced by results in the field of intuitionistic logic and λ-calculus, namely by the results presented in [KL06] of D. Kesner and S. Lengrand. They designed the λ_{lxr}-calculus which is an extension of λ_{x} ([BR95]) with explicit operators for erasure and duplication.

X -calculus before *X -calculus The calculus we are presenting in this paper has its predecessor, it is the X -calculus of S. van Bakel, P. Lescanne and S. Lengrand [vBLL05]. The origin of the language X lies in the notations for the sequent calculus (variant G3 of [Kle52]) as presented first by C. Urban [UB99, Urb00] and later studied in relation with λ̄_{μμ̃}-calculus by S. Lengrand [Len03] via the calculus there called λ_{ϵ}. Another paper [LZ06] presents *X from the point of view of diagrams, whereas this paper insists mostly on the term-calculus and its connection with sequent calculus. Moreover it compares *X with X.

Dragiša Žunić & Pierre Lescanne

*X -calculus The *X -calculus can be seen as an extension of X -calculus. It has four extra sintactic elements, two for erasers and two for duplicators. Its logical setting is the formulation of classical sequent system known as G2 [Kle52]. It is a variant of Gentzen’s LK [Gen35] where structural rules are explicitly given, contexts are lists of formulas and inference rules are given in the context-splitting style. Thus as the reader may assume, the new syntactic elements - eraser and duplicator, have an intuitive and direct logical interpretation as weakening and contraction. We also introduce the notion of linearity in *X.

Substitution Our calculus is basically a calculus of explicit substitutions. A lot of research has been done on explicit substitutions, mostly in the context of λ-calculi, for example [ACCL91, Les94, BR95]. The main idea was to design calculi where the substitution will have a syntactic representation, unlike in λ-calculus where it is a meta-operation.

The main difference regarding explicit substitution, when we speak in the context of *X and classical logic, lies in the fact that here it can be applied to both sides, left or right. In λ_{x} we know that, once it is created, explicit substitution ⟨x = Q⟩ can be distributed only to the left-hand side

(λx.P)Q ⟶^{B} P ⟨x = Q⟩

whilst in *X it is not apriori decided which term will became substitution, the one on the left, or the one on the right. This has a simple syntactic representation

P α̂ † x̂Q

P α̂ † x̂Q P α̂ † x̂Q

where in one case Q plays the role of explicit substitution (more precisely: [α̂ † x̂Q]) and in the other case it is P (or more precisely: [P α̂ † x̂]).

Duplication and Erasure The existence of an explicit term for duplication enables us to define a reduction engine which does not duplicate a term when there is no need. For comparison, in X -calculus we always duplicate a term. This is due to the fact that the duplicator is hidden, which means that we do not know if it is really there. Since we do not want to miss any, we always have to assume it implicitly exists.

Similarly, the existence of a term called eraser, allows us to perform the cancellation i.e. erasing when there is no need to propagate the term further. In X -calculus, terms that were supposed to be canceled, were propagated until they reach the level of ground terms (where the propagation must end) and only then would they get canceled.

Structure of the Paper The rest of the paper is organized as follows: in section 2 we present the calculus itself, with the notion of linearity; section 3 defines a typing system revealing the correspondence with sequential classical logic; section 4 describes a relation between X -calculus and *X; section 5 presents the encoding of λ-calculus and finally section 6 is a conclusion with future work.

Erasure and Duplication in Classical Computation

2. The Calculus

In this section we give the syntax of untyped *X -calculus as well as the set of reduction rules.

2.1. The Syntax

Terms are built from names. This concept differs essentially from one applied in λ-calculus, where the notion of a variable is essential. The difference lies in the fact that a variable can be substituted by an arbitrary term, while a name can be only renamed (substituted by another name). In our calculus the renaming is explicit, which means that it is expressed within the language itself. The reader will notice the presence of hats on some names. This notation has been borrowed from Principia Mathematica [WR25] and is used to denote the binding of a name.

An interesting feature of *X is that the same construction, e.g., an exporter, an importer, a cut and a duplicator, binds two names. A duplicator binds either two in-names or two out-names, whereas the other operators bind an in-name and an out-name. Moreover the names that are bound can belong to the same term, or to two different terms. For example, importer and cut, which are dyadic operations, bind an out-name in a term on the left and an in-name in a term on the right.

Definition 1 (*X -terms) The terms of the *X -calculus are given by the syntax represented by Figure 1, where x, y... range over the infinite set of in-names and α, β... over the infinite set of out-names.

P, Q ::= ⟨x.α⟩  capsule
| x̂ P β̂. α  exporter
| P α̂ [x] ŷQ  importer
| P α̂ † x̂Q  cut
| x ⊙ P  left-eraser
| P ⊙ α  right-eraser
| z< x̂ ; ŷ⟨P]  left-duplicator
| [P ⟩α̂ ; β̂ >γ  right-duplicator

Figure 1: The Syntax

The Components of the Syntax

CAPSULE : ⟨x.α⟩ It is the basic element for constructing terms, i.e. a ground term, as it can not be decomposed. It has one in-name x and one out-name α.

EXPORTER : (ŷP β̂. α) It is a term which binds two names, an in-name y and an out-name β of the subterm P. Together they represent a functionality which is made available on the new output α.

IMPORTER : (P β̂ [x] ŷQ) It consists of two subterms P and Q and it binds an out-name β of the first term, namely P, and an in-name x of the second, namely Q. These two names are meant to be connected to each other. Since their type can be different, a “mediation” is necessary. This is made through an in-name y of functional type. Eventually an importer is aimed to interact with an exporter. Thus, an importer is the counterpart of an exporter. The reduction rule that describes the interaction between an exporter and an importer is in fact the basic computational step in *X -calculus.

CUT : (P α̂ † x̂Q) It represents a direct connection between the two subterms P and Q. Cut connects α in P with x in Q. Actually, the terminology “cut” looks odd for a “connection” (the terminology comes from the proof theory). Here, “cut” † denotes something that links, or attempts to connect, but never something that separates or cuts. We could say, it ’cuts’ through the structure of a term in order to ’link’ two names (i.e., two terms over those two names).

ERASERS (Left and Right) : x ⊙ P and P ⊙ α The first one explicitly adds the in-name (which, in the linear case, does not occur in P) to be free in the expression x ⊙ P. Similarly P ⊙ α adds the free out-name to a term P. These operators corresponds to the inference rules called left and right weakening in the sequent calculus.

DUPLICATORS (Left and Right) : x< x̂_{1} ; x̂_{2}⟨P] and [P ⟩α̂_{1} ; α̂_{2} >α As we will deal only with linear terms, these operators are a way to simulate multiple occurrences of names in a term. More precisely x< x̂_{1} ; x̂_{2}⟨P] allows x to pretend it would occur twice in P, but the linearity of P is preserved. Actually x is duplicated into x_{1} and x_{2}.

Free Names The set of free names, i.e. free in-names and free out-names is defined by Figure 2. We write fn to denote the set of names and f_{in} and f_{on} to denote the sets of in-names and out-names, respectively. Thus we have fn(P) = f_{in}(P) ∪ f_{on}(P). A name which is not free is called a bound name.

\begin{matrix}S & f_{in}(S) & f_{on}(S) \\ ⟨x.α⟩ & x & α \\ x̂ P β̂. α & f_{in}(P)\\{x\} & (f_{on}(P)\\{β\}) ∪ \{α\} \\ P α̂ [x] ŷQ & f_{in}(P) ∪ (f_{in}(Q)\\{y\}) ∪ \{x\} & (f_{on}(P)\\{α\}) ∪ f_{on}(Q) \\ P α̂ † x̂Q & f_{in}(P) ∪ (f_{in}(Q)\\{x\}) & (f_{on}(P)\\{α\}) ∪ f_{on}(Q) \\ x ⊙ P & f_{in}(P) ∪ \{x\} & f_{on}(P) \\ P ⊙ α & f_{in}(P) & f_{on}(P) ∪ \{α\} \\ x< x̂_{1} ; x̂_{2}⟨P] & (f_{in}(P)\\{x_{1}, x_{2}\}) ∪ \{x\} & f_{on}(P) \\ [P ⟩α̂_{1} ; α̂_{2} >α & f_{in}(P) & (f_{on}(P)\\{α_{1}, α_{2}\}) ∪ \{α\} \end{matrix}

Figure 2: Free Names

We are assuming that the terms are equal up to the α-conversion, which means up to the renaming of bound in-names or out-names.

We adopt a convention known as Barendregt’s convention on variables, which states that free and bound names are always considered to be distinct. In *X -calculus it will be a convention on names: “A name is never both, free and bound, in a term”.

If we wish to think of sets f_{n}(P), f_{in}(P) and f_{on}(P) as lists, we will use the notation Φ_{n}(P) (or simply Φ), Φ_{in}(P) and Φ_{on}(P), respectively. The simpler way would be to write Φ_{n}^{P}, Φ_{in}^{P} and Φ_{on}^{P}. If we wish to exclude the name, say out-name z, from the list, we write Φ_{on}^{P}\z

Indexing In what follows, free names will be renamed by indexing. Let i be an index (a natural), P a term and Φ a set of free names occurring in P. Then ind(P, Φ, i) means for example: a name x belonging to Φ is replaced in P by x_{i} and a name α belonging to Φ is replaced in P by α_{i}. To avoid losing linearity, we assume that we start with non-indexed names. The way we use it, indexing preserves linearity.

When Φ_{in} is a list of in-names, we write Φ_{in,i} for the same list of names indexed by i and similarly with Φ_{on} for out-names.

Linearity A term is linear if it satisfies the following:

• Every name has at most one free occurrence and

• Every binder does bind an occurrence of a name (does bind something)

In our calculus we consider only linear terms. Although the syntax in general produces non-linear terms, it appears that they have a linear representation. Take for example the term ⟨x.α⟩ ⊙ α, which is not linear since the out-name α has two free occurrences. It can be represented in *X by the term [⟨x.α_{1}⟩ ⊙ α_{2}⟩â_{1} ; â_{2} >a. The other cause of non-linearity is when we have a binder which binds no name, for example in a term x̂ ⟨x.α⟩ β̂. γ. The problematic binder is β̂, and this is solved by using *X -term x̂ (⟨x.α⟩ ⊙ β) β̂. γ. According to this, what enables us to stay linear is the presence of terms for weakening and contraction.

For the formal definition of linear terms, see Figure 3.

⟨x.α⟩ linear

P linear, x ∈ f_{in}(P), β ∈ f_{on}(P), α ∉ f_{on}(P)

x̂ P β̂. α linear
P, Q linear, α ∈ f_{on}(P), x ∈ f_{in}(Q), y ∉ f_{in}(P, Q), f_{n}(P) ∩ f_{n}(Q) = ∅
P α̂ [y] x̂ Q linear

P, Q linear, α ∈ f_{on}(P), x ∈ f_{in}(Q), f_{n}(P) ∩ f_{n}(Q) = ∅

P α̂ † x̂Q linear

P linear, x ∉ f_{in}(P)

x ⊙ P linear

P linear, α ∉ f_{on}(P)
P ⊙ α linear
P linear, x, y ∈ f_{in}(P), z ∉ f_{in}(P)

z< x̂ ; ŷ⟨P] linear

P linear, α, β ∈ f_{on}(P), γ ∉ f_{on}(P)

[P ⟩α̂ ; β̂ >γ linear

Figure 3: Linear Terms

2.2. Reduction Rules

In this section we define the reduction relation ⟶^{∗X}. As for the cut-elimination, this system has many rules. Therefore we found it convenient to split them into five classes, which are themselves split into symmetrical subclasses “left” and “right”, with the exception of logical rules.

We are also assuming some simple equivalences on terms, coming from the commutativity of weakenings, as well as from associativity and commutativity of formulas in contractions.

Reduction rules are divided into • Activation rules (left and right)

• Propagation rules (left and right)

• Actions (left and right)

• Deactivation rules (left and right)

• Logical rules

2.2.1. Activation Rules

Reduction rules proceed towards eliminating cuts in terms. In the process of reducing there are situations when one has to choose the side where cuts will be propagated. This choice will be explicitly represented by bending the cut towards either the left or the right. A bended cut is called an active cut. The syntax will be extendend so that it can show the direction of activation.

Definition 2 (Active Cuts) The syntax is extended with the two active cuts:

P, Q ::= … | P α̂ † x̂Q | P α̂ † x̂Q

Remark The terms P α̂ † x̂Q and P α̂ † x̂Q are essentially different. Perhaps this is best illustrated by Lafont’s example [GLT89]. Take P = M ⊙ α and Q = x ⊙ N, where M and N are arbitrary terms. Then we have

\begin{aligned}(M ⊙ α)α̂ † x̂(x ⊙ N) & → & Φ_{in}^{N} ⊙ M ⊙ Φ_{on}^{N} \\ (M ⊙ α)α̂ † x̂(x ⊙ N) & → & Φ_{in}^{M} ⊙ N ⊙ Φ_{on}^{M} \end{aligned}

On the other hand the actual activation is defined by the reduction rules. See Figure 4. In general, a cut can be activated in both ways.

(L − activation) : P α̂ † x̂Q → P α̂ † x̂Q, with P ≠ ŷP′ β̂. α and P ≠ ⟨y.α⟩
(R − activation) : P α̂ † x̂Q → P α̂ † x̂Q, with Q ≠ Q′ β̂ [x] ŷQ′′ and Q ≠ ⟨x.β⟩

Figure 4: Activation Rules

The existence of this choice has a consequence that *X is a non-confluent calculus. But if one is interested in the property of confluence, it is easily achievable by giving priority to either left or right-activation (in the case when both are possible). We can denote those reduction relations as ⟶^{∗X_{l}} and ⟶^{∗X_{r}}. Thus we obtain two calculi which are both confluent.

2.2.2. Propagation Rules

Propagation rules describe how cut is being propagated through the structure of terms. This is a step by step propagation (reduction rules “describe” propagation). It is significant to note that propagation of a cut over another inactive cut is enabled, which allows the possibility to elegantly represent βreduction. The rules are divided into “left” and “right” symmetric groups, see Figures 5 and 8.

Observe for example the first reduction rule (exp† − prop) from the left group; it shows how an active cut (or if you wish, an explicit substitution [β̂ † ŷR]) enters from the left through an export, and then stops at its immediate subterm.