key: cord-028840-7n77vko9
authors: Chardonnet, Kostia; Saurin, Alexis; Valiron, Benoît
title: Toward a Curry-Howard Equivalence for Linear, Reversible Computation: Work-in-Progress
date: 2020-06-17
journal: Reversible Computation
DOI: 10.1007/978-3-030-52482-1_8
sha: 
doc_id: 28840
cord_uid: 7n77vko9

In this paper, we present a linear and reversible language with inductive and coinductive types, together with a Curry-Howard correspondence with the logic [Image: see text] : linear logic extended with least and greatest fixed points allowing inductive and coinductive statements. Linear, reversible computation makes an important sub-class of quantum computation without measurement. In the latter, the notion of purely quantum recursive type is not yet well understood. Moreover, models for reasoning about quantum algorithms only provide complex types for classical datatypes: there are usually no types for purely quantum objects beside tensors of quantum bits. This work is a first step towards understanding purely quantum recursive types.

Computation and logic are two faces of the same coin. For instance, consider a Fig. 1 features a graphical presentation of the corresponding proof. Horizontal lines stand for deduction steps-they separate conclusions (below) and hypotheses (above). These deduction steps can be stacked vertically up to axioms in order to describe complete proofs. In Fig. 1 the proofs of A and A → B are symbolized with vertical ellipses. The ellipsis annotated with s indicates that s is a complete proof of A → B while t stands for a complete proof of A.

This connection is known as the Curry-Howard correspondence [4, 8] . In this general framework, types correspond to formulas and programs to proofs, while program evaluation is mirrored with proof simplification (the so-called cutelimination). The Curry-Howard correspondence formalizes the fact that the proof s of A → B can be regarded as a function-parametrized by an argument of type A-that produces a proof of B whenever it is fed with a proof of A. Therefore, the computational interpretation of Modus-Ponens corresponds to the application of an argument (i.e. t) of type A to a function (i.e. s) of type A → B. When computing the corresponding program, one substitutes the parameter of the function with t and get a result of type B. On the logical side, this corresponds to substituting every axiom introducing A in the proof s with the full proof t of A. This yields a direct proof of B without any invocation of the "lemma" A → B.

Paving the way toward the verification of critical softwares, the Curry-Howard correspondence provides a versatile framework. It has been used to mirror first and second-order logics with dependent-type systems [3, 10] , separation logics with memory-aware type systems [9, 13] , resource-sensitive logics with differential privacy [6] , logics with monads with reasoning on side-effects [11, 17] , etc.

This paper is concerned with the case of reversible computation, a sub-class of pure quantum computation. In general quantum computation, one has access to a co-processor holding a "quantum" memory. This memory consists of "quantum" bits having a peculiar property: their state cannot be duplicated, and the operations one can perform on them are unitary, reversible operations. The co-processor comes with an interface to which one can send instructions to allocate, update or read quantum registers. Quantum memories can be used to solve classical problems faster than with purely conventional means. Quantum programming languages are nowadays pervasive [5] and several formal approaches based on logical systems have been proposed to relate to this model of computation [12, 14, 16] . However, all of these languages rely on a purely classical controlflow: quantum computation is reduced to describing a list of instructions-a quantum circuit-to be sent to the co-processor. In particular, in this model operations performed on the quantum memory only act on quantum bits and tensors thereof, while the classical computer enjoys the manipulation of any kind of data with the help of rich type systems.

This extended abstract aims at proposing a type system featuring inductive and coinductive types for a purely reversible language, first step towards a rich quantum type system. We base our study on the approach presented in [15] . In this model, reversible computation is restricted to two main types: the tensor, written a ⊗ b and the co-product, written a ⊕ b. The former corresponds to the type of all pairs of elements of type a and elements of type b, while the latter represents the disjoint union of all elements of type a and elements of type b. For instance, a bit can be typed with 1 ⊕ 1, where 1 is a type with only one element. The language in [15] offers the possibility to code isos-reversible maps-with pattern matching. An iso is for instance the swap operation, typed with a ⊗ b ↔ b ⊗ a. The language also permits higher-order operations on isos, so that an iso can be parametrized by another iso, and is extended with lists ). However, if [15] hints at an extension toward pure quantum computation, the type system is not formally connected to any logical system. The main contribution of this work is a Curry-Howard correspondence for a purely reversible typed language in the style of [15] . We capitalize on the logic [1, 2] : an extension of the additive and multiplicative fragment of linear logic with least and greatest fixed points allowing inductive and coinductive statements. This logic contains both a tensor and a co-product, and its strict linearity makes it a good fit for a reversible type system.

The logic [1, 2] is an extension of the additive and multiplicative fragment of linear logic [7] . The syntax of linear logic is extended with the formulas μX.A and its dual νX.A (where X is a type variable occuring in A), which can be understood at the least and greatest fixed points of the operator X → A. These permit inductive and coinductive statements. We are only interested in a fragment of which contains the tensor, the plus, the unit and the μ and ν connectives. Note that our system only deals with closed formulas. Our syntax of formulas is A, B ::

The derivation rules are shown in Fig. 2 . They defined a binary relation Δ Γ on set of formulas defined inductively. For each rule the assumptions are above the line while the conclusion is under. In the rules, the comma stands for the disjoint union: observe that each formula has to be used exactly once and cannot be duplicated or erased. In one can for instance define the type of natural numbers as μX.1 ⊕ X, of lists of type A as μX.1 ⊕ (A ⊗ X) and of streams of type A as νX.A ⊗ X.

We consider proofs to be potentially non-well-founded derivation trees: they are not necessarily finite as we can for instance consider the formula μX.X and apply the rule μ R an infinite number of times. Among non well-founded proof-objects we distinguish the regular derivation trees that we call circular pre-proofs. These trees can then be represented in a compact manner, see Fig. 3 .

One problem with such a proof-system is to determine whether or not infinite derivations are indeed proofs. Indeed, if every infinite derivation is accepted as a proof, it would be possible to prove any formula F, as shown in Fig. 4 .

To answer this problem, comes with a validity criterion for derivations. It roughly says that a derivation is valid if, in every infinite branch of the derivation, there exists an infinite number of rules μ L or an infinite number of rules ν R . The intuition is that since μX.A formulas represent least fixed points, their objects are finite. An infinite number of rule μ R would mean producing an infinite object, which is not possible. On the other hand, we can explore an arbitrarily large object as input with the rule μ L . For the other case, since νX.A formulas represent greatest fixed points, their object are infinite. We therefore want to ensure that we can produce infinite objects: hence the infinite number of rules ν R . This criterion can be understood in a more operational way as a requirement for productivity.

Our language is based on the one presented in [15] . We build on the reversible part of the paper by extending the language to support both a more general rewriting system and inductive and coinductive types. The language is defined by layers. Terms and types are presented in Table 1 , while typing derivations, based on ,can be found in Tables 2 and 3 . The language consists of the following pieces.

Basic Type. They are first-order and typed with base types. The constructors inj l and inj r represent the choice between either the left or right-hand side of a type of the form A ⊕ B; the constructor , builds pairs of elements (with the corresponding type constructor ⊗); fold and pack respectively represent inductive and coinductive structure for the types μX.A and νX.A. A value can serve both as a result and as a pattern in the clause of an iso. Generalized patterns are used as special patterns: v g : A can match any value of type A. Terms are expressions at "surface-level": applying an iso always gives a term, whereas it is an expression only when the argument is a generalized pattern. 

First-Order Isos. An iso of type α acts on terms of base types. An iso is a function of type A ↔ B, defined as a set of clauses of the form

The tokens e i and e i in the clauses are expressions. Compared to the original language in [15] , we allow general expressions both on the left and on the right of a clause. In order to apply an iso to a term, the iso must be of type A ↔ B and the term of type A. In the typing rules of isos, the OD predicate (taken from [15] and not described in this paper) syntactically enforces the exhaustivity and non-overlapping conditions that the left-hand-side and right-hand-side of clauses should satisfy. Exhaustivity for an iso {e 1 ↔ e 1 | . . . | e n ↔ e n } of type A ↔ B means that the expressions on the left (resp. on the right) of the clauses describe all possible values for the type A (resp. the type B). Non-overlapping means that two expressions cannot match the same value. For instance, the left and right injections inj l e and inj r e are non-overlapping while a pattern v g is always exhaustive.

Higher-Order Isos. An iso of type T manipulate other isos as basic blocks. Since isos represent closed computations, iso-variable are non-linear and can be duplicated at will while term-variable are linear. The constructions λf.ω and ω 1 ω 2 represent respectively the abstraction of a function and the application of an iso to another. The construction μg.ω represents the creation of a recursive function, rewritten as ω[g := μg.ω] by the operational semantics. The typing rule for μg.ω has a productivity criterion. Indeed, since isos can be non-terminating (because of coinduction), productivity is important to ensure that we work with total functions. These checks are crucial to make sure that our isos are indeed bijections in the mathematical sense. The construction inv ω corresponds to the inversion of the iso ω. If ω is of type A ↔ B then inv ω is of type B ↔ A. Finally, our language is equipped with a rewrite system (→) on terms. The evaluation of an iso applied to an argument works with pattern-matching. The 

non-overlapping and exhaustivity conditions guarantee subject-reduction (see Proposition 3.1). 

We can define the iso of type :

Remark 3.1. In our two examples, the left and right-hand side of the ↔ on each function respect both the criteria of exhaustivity-every-value of each type is being covered by at least one expression-and non-overlapping-no two expressions cover the same value. Both isos are therefore bijections.

t : A and t → t then we have t : A. Moreover, it enjoys confluence: Let → * be the reflexive, transitive closure of →. If t → * t 1 and t → * t 2 then there exists t 3 such that t 1 → * t 3 and t 2 → * t 3 .

We conjecture that well-typed isos are indeed isomorphisms:

An iso ω : A ↔ B corresponds to both a computation sending a value of type A to a result of type B and a computation sending a value of type B to a result of type A. We can mechanically translate such an iso to a pair of derivations π, π ⊥ in , where π is a proof of A B and π ⊥ is a proof of B A. This mechanical translation constructs circular pre-proofs, as discussed in Sect. 2. We however still need to show that the obtained derivations respect the validity criterion for circular proof.

Once proven, we would obtain a static correspondence between programs and proofs. We would however still need to show that this entails a dynamic correspondence between the evaluation procedure of our language and the cutelimination procedure of . For that, we would need to make sure that the proofs we obtain are indeed isomorphisms, meaning that if we cut the aforementioned proofs π and π ⊥ , performing the cut-elimination procedure would give either the identity on A or the identity on B. Isomorphism of Proofs. Provided that the above holds, we moreover have

Simulation of Evaluation. Provided that t is a value and v is a normal form, if ω t → * v, if π is the proof corresponding to ω t, and if π is the proof corresponding to v, then π → * π with the cut-elimination procedure. 

We define the two mutually recursive proofs π 1 and π 2 by π 1 = Π(ψ f , π 2 ) and π 2 = Π(ψ f ⊥ , π 1 ) where ψ f and ψ f ⊥ correspond to the isos f and inv f . The proof associated with the iso in Eq. (1) is π 1 . The proof Π(φ 1 , φ 2 ) is shown in Fig. 5 . 

We presented a higher-order, linear, reversible language with inductive and coinductive types together with an interpretation of programs into derivations in the logic . This work is still in progress: A number of proofs still need to be completed. After completing the proofs of our current conjectures, we want to extend our language to linear combinations of terms in order to study purely quantum recursive types and generalized quantum loops: in [15] , lists are the only recursive type which is captured and recursion is terminating. The logic would help providing a finer understanding of termination and non-termination.

Infinitary proof theory: the multiplicative additive case

Least and Greatest Fixed Points in Linear Logic

Interactive Theorem Proving and Program Development -Coq'Art

Functionality in combinatory logic

Open source software in quantum computing

Linear dependent types for differential privacy

Linear logic

The formulae-as-types notion of construction

RustBelt: securing the foundations of the Rust programming language

Formal verification of a realistic compiler

The next 700 relational program logics. PACMPL 4(POPL)

QWIRE: a core language for quantum circuits

Separation logic: a logic for shared mutable data structures

A categorical model for a quantum circuit description language

From Symmetric Pattern-Matching to Quantum Control

A lambda calculus for quantum computation with classical control

Dependent types and multi-monadic effects in F