{'fraction_non_alphanumeric': 0.06557909920159276, 'fraction_numerical': 0.01671982609755602, 'mean_word_length': 3.557355800388853, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 29, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A New Connective in Natural Deduction, and its Application to Quantum Computing

We investigate an unsuspected connection between logical connectives with non-harmonious deduction rules, such as Prior's tonk, and quantum computing. We argue these connectives model the information-erasure, the non-reversibility, and the non-determinism that occur, among other places, in quantum measurement. We introduce an intuitionistic propositional logic with a non-harmonious logical connective sup and two interstitial rules, and show that the proof language of this logic forms the core of a quantum programming language.


Introduction
A puzzling question in quantum physics is whether, in a quantum superposition α|φ + β|ψ of two states |φ and |ψ , there is the state |φ and the state |ψ or the state |φ or the state |ψ .
Indeed, when we build such a superposition, that is when we prepare it, we need to have |φ and |ψ , but when we use this state, that is when we measure it, we get |φ or |ψ . Thus, this superposition is similar to a conjunction when we build it, but to a disjunction when we use it. This discrepancy between the way such a superposition is built and used is reminiscent of the natural deduction rules of the nonharmonious connectives such as Prior's tonk, and others. We defend, in this paper, the thesis that these non-harmonious connectives model the information-erasure, the non-reversibility, and the non-determinism that occur, among other places, in quantum measurement, while the harmonious ones model information preservation, reversibility, and determinism.
More concretely, after discussing the notion of harmonious and non-harmonious deduction rules (Section 2), we introduce an intuitionistic propositional logic with a logical connective ⊙ (read: "sup", for "superposition") that has non-harmonious deduction rules, we introduce a language of proof-terms for this logic, the ⊙-calculus (read: "the sup-calculus"), and we prove its main properties: subject reduction, the termination of proof-reduction, the introduction property, and partial confluence (Section 3). These proofs mostly use standard techniques with some specificities, to be adapted to this calculus. We then extend this calculus, introducing scalars to quantify the propensity of a proof to reduce to another (Section 4) and show that this proof language contains the core of a quantum programming language (Section 5). Note that that intuitionistic propositional logic with ⊙ is not a logic to reason about quantum programs. It is a logic whose propositions are the types of quantum programs.
The idea to extend logic with a new connective for quantum superposition has already been investigated, for example in [32,33]. While these papers address the question of the models of such a logic, we address that of the dynamic of its proofs.
A preliminary version of this paper has been published in the proceedings of the International Colloquium on Theoretical Aspects of Computing, 2021. In this journal version, we have replaced the symbol δ ⊙ with the symbols δ 1 ⊙ , δ 2 ⊙ , clarifying the two-face nature of the connective ⊙. We have also introduced an elimination rule for the symbol ⊤. Such a rule is often considered as redundant, but it fully makes sense in natural deduction with generalized elimination rules, and even more in a proof system with scalars, such as that of Section 4. Besides providing the complete proofs of all theorems, we investigate, in this paper, the confluence of the deterministic part of the calculus, that was not addressed in the conference version. To our surprise, the system without scalars was confluent, but the system with scalars was not. This led us to modify the treatment of scalars and the definition of matrices to make this system confluent. Finally, the conference version of the paper only addressed quantum algorithms on one and two qubits. In this version, we have generalized this to arbitrary quantum algorithms, leading to a more systematic treatment of vectors, matrices, and measurement.

Logical connectives with insufficient, harmonious, and excessive deduction rules
In natural deduction, to prove a proposition of the form A △ B, where △ is an arbitrary connective, the introduction rules of this connective require to prove some propositions. Then, when we have a proof of A △ B and we want to prove a proposition C, the generalized elimination rules [29,8,21,14,22,19] of the connective △ provide some hypotheses for proving this proposition. In general, the propositions required by the introduction rules and those provided by the elimination rules are the same.
For example, to prove the proposition A ∧ B, the introduction rule of the conjunction requires proofs of A and of B and, to prove a proposition C, the generalized elimination rules of the conjunction reduces to (π 2 /B)π 3 . This property that the elimination rules provide exactly the propositions required by the introduction rules can be split into two properties, that it provides no more and no less (called "harmony" and "stability" in [12]).
It is of course possible to imagine other deduction rules that do not respect this harmony principle, either because the introduction rules do not require some propositions, that are provided by the elimination rules (such rules may be called insufficient ) or because the introduction rules require some propositions, that are not provided by the elimination rules (such rules may be called excessive) or both, such as Prior's tonk [25] Γ More generally, we can associate to each set of introduction rules a required proposition. When an introduction rule has several premisses, we take the conjunction of these premises, and when there are several such introduction rules, we take the disjunction of their premises. In the same way, we can associate to each set of elimination rules a provided proposition. As the provided propositions occur on the left of the sequent, when an elimination rule has several premisses, we take their disjunction, and when there are several such elimination rules, we take the conjunction of their premises. A set of rules is harmonious when the required and the provided propositions are the equivalent. It is excessive when the required proposition implies the provided proposition, but not the converse. It is insufficient when the provided proposition implies the required one, but not the converse. The connective ∧ and ∨ are thus harmonious. The connective ⌣ is insufficient. The connective ⌢ is excessive. And, as both A ⇒ B and B ⇒ A are unprovable, the connective tonk is neither. When a set of rule is excessive, a proof reduction process can still be defined, for example the proof can be reduced to (π 1 /A)π 3 , it can be reduced to (π 2 /B)π 4 , it also can be reduced, in a non-deterministic way, either to (π 1 /A)π 3 or to (π 2 /B)π 4 . This notion of harmony can also be extended to the rules of quantifiers. Then, the quantifier AE , whose introduction rule similar to that of the universal quantifier, requires a proof of A for all x and whose elimination rule -e x not free in Γ, C similar to that of the existential quantifier, provides a proof of A for some x, has excessive deduction rules. The proof π 1 . . . .
can be reduced, in a non-deterministic way, to ((t/x)π 1 /A)(t/x)π 2 , for any term t. The quantifier ∇ [18], defined in sequent calculus rather than natural deduction, may also be considered as a quantifier with excessive deduction rules, as it has the right rule of the universal quantifier and the left rule of the existential one. But it involves a clever management of variable scoping, which we do not address here.

Mixing excessiveness and harmony
The rules But, we can add another set of elimination rules for the connective ⊙, similar to those of conjunction Then, the connective ⊙, with its four rules ⊙-i, ⊙-e, ⊙-e1, and ⊙-e2, appears as a two-face connective: the subset of its deduction rules {⊙-i, ⊙-e} is excessive, while the subset {⊙-i, ⊙-e1, ⊙-e2} is harmonious. Note that the rules {⊙-i, ⊙-e1, ⊙-e2} are exactly those of the conjunction.

Information loss
We say that an occurrence of a sub-proof π 1 of a proof π is accessible, if there exists a context κ such that κ{π X }, where π X is obtained by replacing this occurrence of π 1 with a variable X, reduces to X.
that reduces to X. In other words, the rule ∧-i puts the proofs π 1 and π 2 in a box, but the box can be opened and the proofs can be taken out of it. With harmonious deduction rules, when a proof is built with an introduction rule, the proofs of its premises remain accessible. We call this property information preservation. The situation is different with excessive deduction rules: the excess of information, required by the introduction rule, and not returned by the elimination rule in the form of an extra hypothesis in the required proof of C is lost. For example, the occurrence of π 2 in the proof π 1 . . . .
is inaccessible as there is no context such that putting the proof in that context yields a proof that reduces to X. Again, the rule ⌢-i puts the proofs π 1 and π 2 in a box, the box can be partially opened and the proof π 1 can be taken out of it, but not the proof π 2 , that is inaccessible. The information it contains is lost.
The accessibility of the occurrences of π 1 and π 2 of the proof depends on the elimination rules we allow in the context and on the way we reduce the proof . . . .
If we allow the rule ⊙-e in the context, but neither ⊙-e1 nor ⊙-e2, and reduce this proof systematically to (π 1 /A)π 3 , then π 1 is accessible, but π 2 is not. If we reduce it systematically to (π 2 /B)π 4 , then π 2 is accessible, but π 1 is not. If we reduce it, in a non-deterministic way, to (π 1 /A)π 3 or to (π 2 /B)π 4 , then both π 1 and π 2 are accessible, but in a non-deterministic way. If we allow the rule ⊙-e1 and ⊙-e2 in the context, then both proofs are accessible. Once more, the rule ⊙-i puts the proofs π 1 and π 2 in a box, whether the box can be opened and the proofs taken out of it, depends on the tools we use to open it.
When a connective has non-harmonious deduction rules, its introduction rules alone do not define its meaning, and neither do the elimination rules alone. The discrepancy between the meaning conferred by the introduction rules and the elimination rules, and the information loss it implies, are part of the meaning of such a connective.
While connectives with harmonious deduction rules model information-preservation, reversibility, and determinism, those with excessive deduction rules model information-erasure, non-reversibility, and nondeterminism. In particular, the elimination rules ⊙-e1 and ⊙-e2 will be used to model informationpreservation, reversibility, and determinism, while the elimination rule ⊙-e will be used to model informationerasure, non-reversibility, and non-determinism.
Such information-erasure, non-reversibility, and non-determinism, occur, for example, in quantum physics, where the measurement of the superposition of two states does not yield both states back.

Quantum computing and quantum languages
In classical computing, the simplest datatype is that of bits, that contains two elements 0 and 1. In quantum computing, (see [20] for a more comprehensive introduction) this datatype is replaced with that of qubits, that contains all linear combinations α|0 + β|1 , of 0 and 1, then written |0 and |1 , with complex coefficients α and β such that |α| 2 + |β| 2 = 1. Thus, this datatype of qubits contains the vectors of norm 1 of the vector space C 2 .
In classical computing, a more complex datatype is that of n-bits. The elements of this datatype are n-tuples formed with 0 and 1, for instance the datatype of 3-bits contains the 8 elements 000, 001, 010, 011, 100, 101, 110, and 111. In quantum computing, this datatype is replaced with that of n-qubits, that contains all linear combinations of norm 1 of these tuples. The elements of this datatype are thus vectors of norm 1 of C 2 n . The canonical basis of C 2 n is made of the 2 n tuples formed with 0 and 1. For instance the canonical basis of C 8 is {|000 , |001 , |010 , |011 , |100 , |101 , |110 , |111 }. These vectors can also be written {|0 , |1 , |2 , |3 , |4 , |5 , |6 , |7 } identifying a natural number with its binary notation. More generally, the datataypes contain the vectors of norm 1 of some Hilbert space.
Quantum algorithms are formed with two ingredients: unitary transformations, that are linear transformations preserving inner product, and measurements, that are probabilistic operations. It is in fact enough to consider the projection to the canonical basis which acts as follows: the measurement of an arbitrary qubit |ψ = α|0 + β|1 yields the result 0 and transforms the qubit into |0 with probability |α| 2 and yields the result 1 and transform the qubit into |1 with probability |β| 2 . More generally, the measurement of the first qubit of the n-qubit 2 n −1 i=0 α i |i yields 0 and transforms it into |α i | 2 , and yields 1 and transforms it into Measuring any other of the n-qubits involves the swapping unitary transformation and consist into swapping each qubit to measure with the first one, perform the measurement, and swapping it back.
Several programming languages have been proposed to express quantum algorithms, for example [1,31,35,2,3,9,6]. The design of such quantum programming languages raises two main questions. The first is to take into account the linearity of the unitary operators and, for instance, avoid cloning, and the second is to express the information-erasure, non-reversibility, and non-determinism of the measurement. The ⊙ connective gives a new solution to this second problem. Qubits can be seen as proofs of the proposition ⊤ ⊙ ⊤, in contrast with bits which are proofs of ⊤ ∨ ⊤, and measurement can be easily expressed with the elimination rule ⊙-e (Section 5.5).
In previous works, we have attempted to formalize superposition and measurement in the λ-calculus. The calculus Lambda-S [9] contains a primitive constructor + and a primitive measurement symbol π, together with a rule reducing π(t + u), in a non-deterministic way, to t or to u. The superposition t + u can also be considered as the pair t, u . Hence, it should have the type A ∧ A. In other words, it should be a proof of the proposition A∧A. In System I [4], various type-isomorphisms have been taken as identities, in particular the commutativity isomorphism A ∧ B ≡ B ∧ A, hence t + u ≡ u + t. In such a system, where A ∧ B and B ∧ A are identical, it is not possible to define the two elimination rules as the two usual projections rules π 1 and π 2 of the λ-calculus. They were replaced with a single projection parametrized with a proposition A: π A , such that if t : A and u : B then π A (t + u) reduces to t and π B (t + u) to u. When A = B, hence t and u both have type A, the proof-term π A (t + u) reduces, in a non-deterministic way, to t or to u, like a measurement operator.
These works on Lambda-S and System I brought to light the fact that the pair superposition / measurement, in a quantum programming language, behaves like a pair introduction / elimination, for some connective, in a proof language, as the succession of a superposition and a measurement yields a term that can be reduced. In System I, this connective was assumed to be a commutative conjunction, with a modified elimination rule, leading to a non-deterministic reduction.
But, as the measurement of the superposition of two states does not yield both states back, this connective should probably be excessive. Moreover, as, to prepare the superposition α.|0 + β.|1 , we need both |0 and |1 and the measurement in the basis |0 , |1 yields either |0 or |1 , this connective should have the introduction rule of the conjunction, and the elimination rule of the disjunction. Hence, it should be the connective ⊙.

Intuitionistic propositional logic with ⊙
We consider an intuitionistic propositional logic with the usual connectives ⊤, ⊥, ⇒, ∧, and ∨ (as usual, negation is defined as ¬A = (A ⇒ ⊥)), and the extra connective ⊙. The syntax of the propositions of this logic is For simplicity, we have not included propositional constants in this syntax, so ⊤ ⇒ ⊤ is a proposition, but P ⇒ P is not. Adding such constants only requires minors modifications in the proofs below.
The deduction rules are given in Figure 1. We use the generalized elimination rules for all connectives, except implication, for which the elimination rule is the usual modus ponens. This yields the usual application in the language of proof-terms, making the examples more readable.
The rules axiom, ⊤-i, ⊤-e, ⊥-e, ⇒-i, ⇒-e, ∧-i, ∧-e1, ∧-e2, ∨-i1, ∨-i2, and ∨-e are the usual rules of intuitionistic propositional logic. The rules ⊙-i, ⊙-e, ⊙-e1, and ⊙-e2 are those of the connective ⊙. We also added two rules prod whose premises are identical to their conclusion. Although these rules are logically trivial, they introduce constructors in the proof language that will be of key importance when we extend the calculus with scalars, in Section 4. These rules are called interstitial as, as we shall see, they can create an interstice between the introduction rule of some connective and its elimination rule.

Proof reduction
The reduction rules in this logic are the usual ones for the connectives ⇒, ∧, and ∨, except that we use the generalized elimination rules for the conjunction.
For the connective ⊤, we have decided to take an elimination rule. This introduces a notion of reducible proof for the connective ⊤ and it reduces to π . . . .
that is to π with an added interstitial rule. The role of this prod rule will be made clear when we add scalars.
The reduction rules of the connective ⊙ are, as we have seen in a non-deterministic way, erasing some information Finally, adding the interstitial rules, permits to build proofs that cannot be reduced, because the sum rule or the prod rule creates an interstice between the introduction rule of some connective and its elimination rule. For example π 1 . . . .
Reducing such a proof requires rules to commute the rule sum either with the elimination rule below or with the introduction rules above.
As the commutation with the introduction rules above is not always possible, for example in the proof the commutation with the elimination rule below is often preferred. In this paper, we favour the commutation of the interstitial rules with the introduction rules, rather than with the elimination rules, whenever it is possible, that is for all connectives except disjunction. For example the proof Such a commutation yields a stronger introduction property for the considered connective (Theorem 3.32).
the prod rule and the ∨-i1 rule can be commuted. For coherence, we have decided to commute both the sum rule and the prod rule with the elimination rule of the disjunction, rather that with its introduction rules, but both choices are possible.

Proof-terms
We introduce a term language, the ⊙-calculus, for the proofs of this logic. Its syntax is The variables x express the proofs built with the rule axiom, the terms t + u those built with the rule sum, the terms •t those built with the rule prod, the term ⋆ that built with the rule ⊤-i, the terms δ ⊤ (t, u) those built with the rule ⊤-e, the terms δ ⊥ (t) those built with the rule ⊥-e, the terms λx.t those built with the rule ⇒-i, the terms t u those built with the rule ⇒-e, the terms t, u those built with the rule ∧-i, the terms δ 1 ∧ (t, x.u) and δ 2 ∧ (t, x.u) those built with the rules ∧-e1 and ∧-e2, the terms inl(t) and inr(t) those built with the rules ∨-i1 and ∨-i2, the terms δ ∨ (t, x.u, y.v) those built with the rule ∨-e, the terms [t, u] those built with the rule ⊙-i, and the terms δ ⊙ (t, x.u, y.v), δ 1 ⊙ (t, x.u), and δ 2 ⊙ (t, x.u) those built with the rules ⊙-e, ⊙-e1, and ⊙-e2.
x.u), and δ 2 ⊙ (t, x.u) eliminations. The variables and the proofs of the form t+u and •t are neither introductions nor eliminations.
The α-equivalence relation and the free and bound variables of a proof-term are defined as usual. Proofterms are defined modulo α-equivalence. A proof-term is closed if it contains no free variables. We write (u/x)t for the substitution of u for x in t.
The typing rules of the ⊙-calculus are given in Figure 2 and its reduction rules in Figure 3, they are the expression on proof-terms of the reduction rules presented above. An instance of the second rule of Figure 3 is (λx.x) y −→ y and an instance of the third is δ 1 ∧ ( ⋆, ⋆ , x.x) −→ ⋆ In this paper, we consider the usual reduction rules for natural deduction, but not the so-called commuting cuts, that yield the subformula property and the equivalence with cut-free sequent calculus. Although we believe proving the termination with commuting cuts is not difficult (in particular because we have included ultra-reduction rules), we leave this for future work.
Remark 3.1. This system is a higher-order rewrite system [13,16]. A more rigorous notation would be to consider the symbol . as the abstraction, to add a symbol app for application, and to add a rewrite rule β, app(x.t, u) −→ (u/x)t used to build the instances of the rules of Figure 3.
Hence, the second rule of Figure 3 would be expressed as Substituting the proof x.x for the variable T and the proof y for the variable U in the first rule and reducing, with the added rule, both sides of the rule yields the instance (λx.x) y −→ y and substituting ⋆ for the variables T and U and the proof x.x for the variable V , in the second, and reducing both sides of the rule, with the added rule, yields the instance

Subject reduction
To prove subject reduction, we first prove, as usual, a substitution property.
Proof. By induction on the structure of t.
And use it to prove the theorem itself. Proof. By induction on the definition of the relation −→.

Confluence
The introduction of the connective ⊙ leads to a non-deterministic calculus with the rules Hence, the system presented in Figure 3 is trivially non-confluent. But if we drop these two rules, the rest of the system is confluent.
Theorem 3.4 (Confluence). The system of Figure 3 without the rules Proof. This system is left linear and it has no critical pairs. And, as proved in [16, Theorem 6.8], higher-order left linear systems without critical pairs are confluent.
Note that the untyped calculus does have critical pairs, for example the proof δ ∨ (⋆ + ⋆, x.x, y.y) reduces in two different ways, but these critical pairs are not well-typed.

Termination
We now prove the strong termination of proof reduction, that is that all reduction sequences are finite. The proof follows the same pattern as that for intuitionistic propositional natural deduction, that we recall in the Appendix.
The ⊙-calculus introduces two new features: the connective ⊙, its associated proof constructors [, ], δ ⊙ , δ 1 ⊙ , and δ 2 ⊙ , and the constructors + and •. The termination proof of intuitionistic propositional natural deduction extends smoothly when we add the connective ⊙, but adding the constructors + and • is a bit more challenging. To handle these symbols, we prove the strong termination of an extended reduction system, in the spirit of Girard's ultra-reduction [11], whose strong termination obviously implies that of the rules of Figure 3.
Definition 3.5 (Ultra-reduction). Ultra-reduction is defined with the rules of Figure 3, plus the rules  18 in the strong termination of proof reduction for intuitionistic propositional natural deduction (except that the references to Propositions Appendix A.6, Appendix A.7, and Appendix A.8 must be replaced with references to Propositions 3.10, 3.11, and 3.12). So we will omit these proofs. Propositions 3.11, 3.12, 3.21, and 3.26 have proofs similar to those of Propositions Appendix A.7, Appendix A.8, Appendix A.14, and Appendix A.19, but these proofs require minor tweaks. In contrast, Propositions 3.7, 3.8, 3.13, 3.14, 3.20, 3.27, 3.28, and 3.29 are specific. Definition 3.6 (Length of reduction). If t is a strongly terminating proof, we write |t| for the maximum length of a reduction sequence issued from t. Proposition 3.7 (Termination of a sum). If t and u strongly terminate, then so does t + u.
Proof. We prove that all the one-step reducts of t + u strongly terminate, by induction first on |t| + |u| and then on the size of t.
If the reduction takes place in t or in u we apply the induction hypothesis. Otherwise the reduction is at the root and the rule used is either In the first case, the proof ⋆ is irreducible, hence it strongly terminates. In the second, by induction hypothesis, the proof t ′ + u ′ strongly terminates, thus so does the proof λx.(t ′ + u ′ ). In the third and the fourth, by induction hypothesis, the proofs t ′ 1 + u ′ 1 and t ′ 2 + u ′ 2 strongly terminate, hence so do the proofs In the fifth and the sixth, the proofs t and u strongly terminate.
Proposition 3.8 (Termination of a product). If t strongly terminates, then so does •t.
Proof. We prove that all the one-step reducts of •t strongly terminate, by induction first on |t| and then on the size of t.
If the reduction takes place in t, we apply the induction hypothesis. Otherwise the reduction is at the root and the rule used is either In the first case, the proof ⋆ is irreducible, hence it strongly terminates. In the second, by induction hypothesis, the proof •t ′ strongly terminates, thus so does the proof λx. • t ′ . In the third and the fourth, by induction hypothesis, the proofs •t ′ 1 and •t ′ 2 strongly terminate, hence so do the proofs •t ′ 1 , •t ′ 2 and In the fifth, the proof t strongly terminates.
Definition 3.9. We define, by induction on the proposition A, a set of proofs A : • t ∈ ⊤ if t strongly terminates, • t ∈ ⊥ if t strongly terminates, • t ∈ A ⇒ B if t strongly terminates and whenever it reduces to a proof of the form λx.u, then for • t ∈ A ∧ B if t strongly terminates and whenever it reduces to a proof of the form u, v , then u ∈ A and v ∈ B , • t ∈ A ∨ B if t strongly terminates and whenever it reduces to a proof of the form inl(u), then u ∈ A , and whenever it reduces to a proof of the form inr(v), then v ∈ B , • t ∈ A ⊙ B if t strongly terminates and whenever it reduces to a proof of the form [u, v], then u ∈ A and v ∈ B .  Proof. If t −→ * t ′ and t strongly terminates, then t ′ strongly terminates. Furthermore, if A has the form B ⇒ C and t ′ reduces to λx.u, then so does t, hence for every v ∈ B , If A has the form B ∧ C and t ′ reduces to u, v , then so does t, hence u ∈ B and v ∈ C . If A has the form B ∨ C and t ′ reduces to inl(u), then so does t, hence u ∈ B and if A has the form B ∨ C and t ′ reduces to inr(v), then so does t, hence v ∈ C .
And if A has the form B ⊙ C and t ′ reduces to [u, v], then so does t, hence u ∈ B and v ∈ C .
Proposition 3.12 (Girard's lemma). Let t be a proof that is not an introduction, such that all the one-step reducts of t are in A . Then, t ∈ A .
Proof. Let t, t 2 , . . . be a reduction sequence issued from t. If it has a single element, it is finite. Otherwise, we have t −→ t 2 . As t 2 ∈ A , it strongly terminates and the reduction sequence is finite. Thus, t strongly terminates. Furthermore, if A has the form B ⇒ C and t −→ * λx.u, then let t, t 2 , . . . , t n be a reduction sequence from t to λx.u. As t n is an introduction and t is not, n ≥ 2.
If A has the form B ∧ C and t −→ * u, v , then let t, t 2 , . . . , t n be a reduction sequence from t to u, v . As t n is an introduction and t is not, n ≥ 2. Thus, t −→ t 2 −→ * t n . We have t 2 ∈ A , thus u ∈ B and v ∈ C .
If A has the form B ∨ C and t −→ * inl(u), then let t, t 2 , . . . , t n be a reduction sequence from t to inl(u). As t n is an introduction and t is not, n ≥ 2. Thus, t −→ t 2 −→ * t n . We have t 2 ∈ A , thus u ∈ B .
If A has the form B ∨ C and t −→ * inr(v), then let t, t 2 , . . . , t n be a reduction sequence from t to inr(v). As t n is an introduction and t is not, n ≥ 2. Thus, t −→ t 2 −→ * t n . We have t 2 ∈ A , thus v ∈ C .
And if A has the form B ⊙ C and t −→ * [u, v], then let t, t 2 , . . . , t n be a reduction sequence from t to [u, v]. As t n is an introduction and t is not, n ≥ 2. Thus, t −→ t 2 −→ * t n . We have t 2 ∈ A , thus u ∈ B and v ∈ C .
In Propositions 3.13 to 3.29, we prove the adequacy of each proof constructor. Proposition 3.13 (Adequacy of +). If t 1 ∈ A and t 2 ∈ A , then t 1 + t 2 ∈ A .
In the second and the third, by Proposition 3.11, λx.v ∈ A hence, for every w in B , (w/x)v ∈ C .
• If the proposition A has the form B ∧ C, and In the first case, by Proposition 3.11, the proofs u 1 , u ′ 1 and u 2 , u ′ 2 are in A . Thus, u 1 and u 2 are in B and u ′ 1 and u ′ 2 are in C . By induction hypothesis, u 1 + u 2 ∈ B and u ′ 1 + u ′ 2 ∈ C and by Proposition 3.11, v ∈ B and v ′ ∈ C .
In the second and the third, by Proposition 3.11, v, v ′ ∈ A hence, v ∈ B and v ′ ∈ C .
• If the proposition A has the form B ⊙ C, and In the first case, by Proposition 3.11, the proofs [u 1 , u ′ 1 ] and [u 2 , u ′ 2 ] are in A . Thus, u 1 and u 2 are in B and u ′ 1 and u ′ 2 are in C . By induction hypothesis, u 1 + u 2 ∈ B and u ′ 1 + u ′ 2 ∈ C and by Proposition 3.11, v ∈ B and v ′ ∈ C .
In the second and the third, by Proposition 3.11, Proposition 3.14 (Adequacy of •). If t ∈ A , then •t ∈ A .

Proof. By induction on A.
The proofs t strongly terminates. Thus, by Proposition 3.8, the proof •t strongly terminates. Furthermore: • If the proposition A has the form B ⇒ C, and •t −→ * λx.v then either t −→ * λx.u, and •u −→ * v, or t −→ * λx.v.
In the first case, by Proposition 3.11, the proof λx.u is in A . Thus, for every w in B , (w/x)u ∈ C . By induction hypothesis, (w/x) • u = •(w/x)u ∈ C and by Proposition 3.11, (w/x)v ∈ C .
In the second, by Proposition 3.11, λx.v ∈ A hence, for every w in B , (w/x)v ∈ C .
• If the proposition A has the form B ∧ C, and In the first case, by Proposition 3.11, the proof u, u ′ is in A . Thus, u is in B and u ′ is in C . By induction hypothesis, •u ∈ B and •u ′ ∈ C and by Proposition 3.11, v ∈ B and v ′ ∈ C .
In the second, by Proposition 3.11, v, v ′ ∈ A hence, v ∈ B and v ′ ∈ C .
• If the proposition A has the form B ∨ C, and •t −→ * inl(v) then t −→ * inl(v). Thus, by Proposi- The proof is similar if •t −→ * inr(v).
• If the proposition A has the form B ⊙ C, and In the first case, by Proposition 3.11, the proofs [u, u ′ ] is in A . Thus, u is in B and u ′ is in C . By induction hypothesis, •u ∈ B and •u ′ ∈ C and by Proposition 3.11, v ∈ B and v ′ ∈ C .
In the second, by Proposition 3.11,      Proof. The proofs t 1 and t 2 strongly terminate. Consider a reduction sequence issued from [t 1 , t 2 ]. This sequence can only reduce t 1 and t 2 , hence it is finite. Thus, [t 1 , t 2 ] strongly terminates.
Proof. The proofs t 1 and t 2 strongly terminate. We prove, by induction on |t 1 | + |t 2 |, that δ ⊤ (t 1 , t 2 ) ∈ C . Using Proposition 3.12, we only need to prove that every of its one step reducts is in C . If the reduction takes place in t 1 or t 2 , then we apply Proposition 3.11 and the induction hypothesis. Otherwise, the proof t 1 is ⋆ and the reduct is •t 2 . We conclude with Proposition 3.14.
Proposition 3.23 (Adequacy of application). If t 1 ∈ A ⇒ B and t 2 ∈ A , then t 1 t 2 ∈ B .
Proposition 3.24 (Adequacy of δ 1 ∧ ). If t 1 ∈ A∧B and, for all u in A , (u/x)t 2 ∈ C , then δ 1 Proposition 3.25 (Adequacy of δ 2 ∧ ). If t 1 ∈ A∧B and, for all u in B , (u/x)t 2 ∈ C , then δ 2 Proof. By Proposition 3.10, x ∈ A , thus t 2 = (x/x)t 2 ∈ C . In the same way, t 3 ∈ C . Hence, t 1 , t 2 , and t 3 strongly terminate. We prove, by induction on |t 1 | + |t 2 | + |t 3 |, that δ ∨ (t 1 , x.t 2 , y.t 3 ) ∈ C . Using Proposition 3.12, we only need to prove that every of its one step reducts is in C . If the reduction takes place in t 1 , t 2 , or t 3 , then we apply Proposition 3.11 and the induction hypothesis. Otherwise, either: • The proof t 1 has the form inl(w 2 ) and the reduct is Hence, (w 2 /x)t 2 ∈ C .
Proof. By Proposition 3.10, x ∈ A , thus t 2 = (x/x)t 2 ∈ C . In the same way, t 3 ∈ C . Hence, t 1 , t 2 , and t 3 strongly terminate. We prove, by induction on |t 1 | + |t 2 | + |t 3 |, that δ ⊙ (t 1 , x.t 2 , y.t 3 ) ∈ C . Using Proposition 3.12, we only need to prove that every of its one step reducts is in C . If the reduction takes place in t 1 , t 2 , or t 3 , then we apply Proposition 3.11 and the induction hypothesis.
Otherwise, the proof t 1 has the form [u, v] and the reduct is either (u/x) Proposition 3.28 (Adequacy of δ 1 ⊙ ). If t 1 ∈ A⊙B and, for all u in A , (u/x)t 2 ∈ C , then δ 1 Proof. By Proposition 3.10, x ∈ A , thus t 2 = (x/x)t 2 ∈ C . Hence, t 1 and t 2 strongly terminate. We prove, by induction on |t 1 | + |t 2 |, that δ 1 ⊙ (t 1 , x.t 2 ) ∈ C . Using Proposition 3.12, we only need to prove that every of its one step reducts is in C . If the reduction takes place in t 1 or t 2 , then we apply Proposition 3.11 and the induction hypothesis.
Otherwise, the proof t 1 has the form [u, v] and the reduct is (u/x)t 2 . As [u, v] ∈ A ⊙ B , we have u ∈ A . Hence, (u/x)t 2 ∈ C . Proposition 3.29 (Adequacy of δ 2 ⊙ ). If t 1 ∈ A⊙B and, for all u in B , (u/x)t 2 ∈ C , then δ 2 Proof. Similar to that of Proposition 3.28.
Theorem 3.30 (Adequacy). Let t be a proof of A in a context Γ = x 1 : A 1 , . . . , x n : A n and σ be a substitution mapping each variable x i to an element of A i , then σt ∈ A .
Proof. By induction on the structure of t.
If t is a variable, then, by definition of σ, σt ∈ A . For the seventeen other proof constructors, we use the Propositions 3.15 to 3.29. As all cases are similar, we just give a few examples.
where u is a proof of B and v a proof of C, then, by induction hypothesis, σu ∈ B and σv ∈ C . Hence, by Proposition 3.20, [σu, σv] ∈ B ⊙ C , that is σt ∈ A .  Proof. Let σ be the substitution mapping each variable x i : A i of Γ to itself. Note that, by Proposition 3.10, this variable is an element of A i . Then, t = σt is an element of A . Hence, it strongly terminates.

Introduction property
Theorem 3.32 (Introduction). Let t be a closed irreducible proof of A.
• If A has the form ⊤, then t is ⋆.
• The proposition A is not ⊥.
• If A has the form B ⇒ C, then t has the form λx.u.
• If A has the form B ∧ C, then t has the form u, v .
• If A has the form B ∨ C, then t has the form inl(u), inr(u), u + v, or •u.
• If A has the form B ⊙ C, then t has the form [u, v].
Proof. By induction on the structure of t.
We first remark that, as the proof t is closed, it is not a variable. Then, we prove that it cannot be an elimination.
• If t = δ ⊤ (u, v), then u is a closed irreducible proof of ⊤, hence, by induction hypothesis, it is ⋆ and the proof t is reducible.
, then u is a closed irreducible proof of ⊥ and, by induction hypothesis, no such proof exists.
• If t = u v, then u is a closed irreducible proof of B ⇒ A, hence, by induction hypothesis, it has the form λx.u 1 and the proof t is reducible.
, then u is a closed irreducible proof of B ∧ C, hence, by induction hypothesis, it has the form u 1 , u 2 and the proof t is reducible.
, then u is a closed irreducible proof of B ∧ C, hence, by induction hypothesis, it has the form u 1 , u 2 and the proof t is reducible.
• If t = δ ∨ (u, x.v, y.w), then u is a closed irreducible proof of B ∨ C, hence, by induction hypothesis, it has the form inl(u 1 ), inr(u 1 ), u 1 + u 2 , or •u 1 and the proof t is reducible.
, then u is a closed irreducible proof of B ⊙ C, hence, by induction hypothesis, it has the form [u 1 , u 2 ] and the proof t is reducible.
Hence, t is an introduction, a sum, or a product. It t is ⋆, then A is ⊤. If it has the form λx.u, then A has the form B ⇒ C. If it has the form u, v , then A has the form B ∧ C. If it has the form inl(u) or inr(u), then A has the form B ∨ C. If it has the form [u, v] then A has the form B ⊙ C. We prove that, if it has the form u + v or •u, A has the form B ∨ C.
• If t = u + v, then the proofs u and v are two closed and irreducible proofs of A. If A = ⊤ then, by induction hypothesis, they are both ⋆ and the proof t is reducible. If A = ⊥ then, they are closed irreducible proofs of ⊥ and, by induction hypothesis, no such proofs exist. If A has the form B ⇒ C then, by induction hypothesis, they are both abstractions and the proof t is reducible. If A has the form B ∧ C, then, by induction hypothesis, they are both pairs and the proof t is reducible. If A has the form B ⊙ C, then, by induction hypothesis, they are both superpositions and the proof t is reducible. Hence, A has the form B ∨ C.
• If t = •u, then the proof u is a closed and irreducible proof of A. If A = ⊤ then, by induction hypothesis, u is ⋆ and the proof t is reducible. If A = ⊥ then, it is a closed irreducible proof of ⊥ and, by induction hypothesis, no such proof exists. If A has the form B ⇒ C then, by induction hypothesis, it is an abstraction and the proof t is reducible. If A has the form B ∧C, then, by induction hypothesis, it is a pair and the proof t is reducible. If A has the form B ⊙ C, then, by induction hypothesis, it is a superposition and the proof t is reducible. Hence, A has the form B ∨ C.
Note that we reap here the benefit of commuting, when possible, the interstitial rules with the introduction rules, as, except for the disjunction, closed irreducible proofs are genuine introductions. Proof. Consider a closed proof of A ∨ B and its irreducible form t. We prove, by induction on the structure of t, that A has a closed proof or B has a closed proof. By Theorem 3.32, t has the form inl(u), inr(u), u + v, or •u. If it has the form inl(u), u is a closed proof of A. If it has the form inr(u), u is a closed proof of B. If it has the form u + v or •u, u is a closed irreducible proof of A ∨ B. Thus, by induction hypothesis, A has a closed proof or B has a closed proof.

Quantifying non-determinism
When we have a non-deterministic reduction system, we often want to quantify the propensity of a proof to reduce to another.
One way to do so is to consider a field (S, +, ×) of scalars, for instance Q, R, or C, with the usual sum + and product ×, take a different rule ⊤-i for each scalar and a different rule prod for each scalar. So, for each scalar a, we have a closed irreducible proof of ⊤ and we write a.⋆ for this proof. In the same way, we write a • t for the proof obtained by applying, to the proof t, the rule prod corresponding to the scalar a. As the closed irreducible proofs of ⊤ are in one-to-one correspondence with the elements of S, those of ⊤ ⊙ ⊤ are in one-to-one with the elements of S 2 , those of (⊤ ⊙ ⊤) ⊙ (⊤ ⊙ ⊤) are in one-to-one correspondence with the elements of S 4 , etc.
In the ⊙-calculus, the proof ⋆ + ⋆ reduces to ⋆. Now, the proof a.⋆ + b.⋆ reduces to (a + b).⋆, where the scalars are added. In the same way the proof a • b.⋆ reduces to (a × b).⋆, where the scalars are multiplied. In the ⊙-calculus, the proof δ ⊤ (⋆, t) reduces to •t. Now, the proof δ ⊤ (a.⋆, t) reduces neither to t, as it does in the usual intuitionistic propositional logic, nor to •t as it does in the system of Section 3, but to a • t.

The ⊙ S -calculus
We define the ⊙ S -calculus (read: "the sup-S-calculus"), by extending the grammar of proofs as follows where a is a scalar. The typing rules are similar to those of Figure 2 except the rule and the rule The reduction rules are those of Figure 4. Note that the scalar computation is implicit and the terms expressing scalars are just constants. For instance 2. ⋆ +3.⋆ reduces directly to 5.⋆.
The ⊙ S -calculus is thus a λ-calculus equipped with a notion of linear combination of terms, such as Lineal [2], the Algebraic λ-calculus [34], etc.

Properties
Proof. This system also is left linear and it has no critical pairs. Thus, by [16,Theorem 6.8] it is confluent.  • If A has the form ⊤, then t is a.⋆. • If A has the form B ⇒ C, then t has the form λx.u.
• If A has the form B ∧ C, then t has the form u, v .
• If A has the form B ∨ C, then t has the form inl(u), inr(u), u + v, or a • u.
• If A has the form B ⊙ C, then t has the form [u, v].
Proof. Similar to that of Theorem 3.32.

Quantifying non-determinism
When S is Q, R, or C, we can use the scalars a and b to assign probabilities to the reductions In this case, if a and b are not both 0, we assign the probabilities |a| 2 |a| 2 +|b| 2 and |b| 2 |a| 2 +|b| 2 to the reductions And if either a = b = 0 or t and u are proofs of propositions different from ⊤, we assign any probability, for instance 1 2 , to these reductions.

Application to quantum computing
We now show that the ⊙ C -calculus, with the reduction strategy of Example 4.5, restricting the reduction of δ ⊙ ([t, u], x.v, y.w) to the cases where t and u are closed irreducible proofs, contains the core of a small quantum programming language. Note that the proofs inl(1.⋆) and inr(1.⋆) are not the only closed irreducible proofs of B, for example inl(2.⋆) and inl(1.⋆) + inr(1.⋆) also are.

Definition 5.2 (Test). The test operator is defined as
where x and y are variables not occurring in u and v. Note that If(0, u, v) −→ u and If(1, u, v) −→ v.

Qubits
A n-qubit, for n ≥ 1, is a vector of C 2 n of norm 1. We show now how n-qubits, and more generally vectors of C 2 n , for n ≥ 0, can be expressed as proofs in the ⊙ C -calculus.
Definition 5.3 (The proposition Q ⊗n ). The proposition Q ⊗n is defined by induction on n as follows Note that, in this definition, the binary connective ⊙ is always used with two identical propositions: The proposition Q ⊗1 = ⊤ ⊙ ⊤ is sometimes written Q.
The closed irreducible proofs of Q ⊗n and the vectors of C 2 n are in one-to-one correspondence: to each closed irreducible proof t of Q ⊗n , we associate a vector t of C 2 n and to each vector u of C 2 n , we associate a closed irreducible proof u of Q ⊗n . Definition 5.4 (One-to-one correspondance). To each closed irreducible proof t of Q ⊗n , we associate a vector t of C 2 n as follows.
• If n = n ′ + 1, then t = [u, v]. We let t be the vector with two blocks u and v: t = ( u v ).
To each vector u of C 2 n , we associate a closed irreducible proof u of Q ⊗n .
In particular, the proof 0 Q ⊗n is defined as 0, where 0 is the zero vector of C 2 n .
We extend the definition of t to any closed proof of Q ⊗n , t is by definition t ′ , where t ′ is the irreducible form of t.
We also take the convention that any closed irreducible proof u of Q ⊗n , expressing a non-zero vector u ∈ C 2 n , is an alternative expression of the n-qubit u u . For example, the qubit 1 Proof. By induction on n.

Matrices
The information-preserving, reversible, and deterministic unitary operators are expressed with the proof constructors δ 1 ⊙ and δ 2 ⊙ .
Theorem 5.8 (Matrices). Let M be a matrix with 2 m columns and 2 n lines, then there exists a closed proof t of Q ⊗m ⇒ Q ⊗n such that, for all vectors u ∈ C 2 m , t u = M u.
Proof. By induction on A.
• If m = 0, then M is a matrix of one column and 2 n lines. Hence, it is also a vector of 2 n lines. We take t = λx.δ ⊤ (x, M ) Let u ∈ S 1 , u has the form ( a ) and u = a.⋆.
Then, using Proposition 5. By induction hypothesis, there exist closed proofs t 1 and t 2 of the proposition Q m ′ ⇒ Q n such that, for all vectors u 1 , u 2 ∈ C 2 m ′ , we have t 1 u 1 = M 1 u 1 and t 2 u 2 = M 2 u 2 . We take Let u ∈ C 2 m , and u 1 and u 2 be the two blocks of 2 m ′ lines of u, so u = ( u1 u2 ), and u = [u 1 , u 2 ]. Then, using Proposition 5.
is expressed as the proof

Probabilities
Definition 5.10 (Norm). Let t be a closed irreducible proof of Q ⊗n , we define the square of the norm t 2 of t by induction on n.
If t is a closed irreducible proof of Q ⊗n of the form [u 1 , u 2 ], where u 1 2 and u 2 2 are not both 0, then we assign the probability and the probability u2 2 u1 2 + u2 2 to the reduction If u 1 2 = u 2 2 = 0, or u 1 and u 2 are proofs of propositions of a different form, we associate any probability, for example 1 2 , to both reductions. Example 5.11. If t is a closed irreducible proof of Q of the form [a.⋆, b.⋆], where a and b are not both 0, then we assign the probability |a| 2 |a| 2 +|b| 2 to the reduction

Measure
The information-erasing, non-reversible, and non-deterministic measurement operators are expressed with the proof constructor δ ⊙ .
Several such operators are defined in Figure 5. Let n be a non-zero natural number and t be a closed irreducible proof of Q ⊗n of the form [u 1 , u 2 ], such that t 2 = u 1 2 + u 2 2 = 0, expressing the state of an n-qubit. The proof π n t of the proposition Q ⊗n reduces, with probabilities u1 2 u1 2 + u2 2 and u2 2 u1 2 + u2 2 to [u 1 , 0 Q ⊗n−1 ] and to [0 Q ⊗n−1 , u 2 ]. It is the state of the n-qubit, after the partial measure of the first qubit. The proof π ′ n t of the proposition B reduces, with the same probabilities, to 0 and to 1. It is the "classical" result of the measure. The proof π ′′ n t of the proposition Q ⊗n ∧ B reduces, with the same probabilities, to [u 1 , 0 Q ⊗n−1 ], 0 and to [0 Q ⊗n−1 , u 2 ], 1 . It is the pair formed with the state of the n-qubit, after the measure, and the "classical" result of the measure.
Example 5.12. In the case n = 1, if t is a closed irreducible proof of Q ⊗1 of the form [a.⋆, b.⋆], such that a and b are not both 0, then the proof π 1 t of the proposition Q ⊗1 reduces, with probabilities |a| 2 |a| 2 +|b| 2 and |b| 2 |a| 2 +|b| 2 , to [a.⋆, 0.⋆], that is an expression of |0 , and to [0.⋆, b.⋆], that is an expression of |1 . The proof π ′ 1 t of the proposition B reduces, with the same probabilities, to 0 and to 1. The proof π ′′ 1 t of the proposition Q ⊗1 ∧ B reduces, with the same probabilities, to [a.⋆, 0.⋆], 0 and to [0.⋆, b.⋆], 1 . Using the representation of matrices, it is possible to define measurement operators that measure in any basis, by changing basis, measuring, and changing basis again. This way, it is also possible to define measurement operators that partially measure, not the first qubit of a n-qubit, but any.

An example: Deutsch's algorithm
Deutsch's algorithm allows to decide whether a 1-bit to 1-bit function f is constant or not, applying an oracle U f , implementing f , only once. It is an algorithm operating on 2-qubits. It proceeds in four steps. In the ⊙ C -calculus, the initial state is

Conclusion
We have extended intuitionistic propositional logic with a connective ⊙, that has both excessive and harmonious deduction rules, and with interstitial rules. We have then extended this logic again with scalars. We have shown that the proof language of this logic forms the core of a quantum programming language.
The connective ⊙, with its elimination symbol δ ⊙ , models information-erasure, non-reversibility, and non-determinism, that occur, for example, in quantum measurement. With its elimination symbols δ 1 ⊙ and δ 2 ⊙ , it models the information-preservation, reversibility, and determinism that occur, for example, in unitary transformations.
There are several points that we did not address in this paper. First, we leave open the question of the interpretation of this logic in a model, in particular a categorical one, besides the obvious Lindenbaum algebra.
Then, these notions of insufficient and excessive deduction rules are not specific to natural deduction and similar notions could be defined and investigated, for instance, in sequent calculus. Note that in the sequent calculus, harmony can be defined in a stronger sense, that includes, not only the possibility to reduce proofs, but also to reduce the use of the rule axiom on non-atomic propositions to smaller ones [17]-an analogue of the η-expansion, but generalized to arbitrary connectives.
Finally, the ⊙ C -calculus can express all quantum circuits, as it can express matrices and measurement operators. However, it is not restricted to quantum algorithms, since the ⊙ connective addresses the question of the information-erasure, non-reversibility, and non-determinism of measurement, but not that of linearity and unitarity. We have started investigating, in [5], a restriction of the ⊙-calculus to linear operators, forbidding, for example, the non-linear proof of the proposition Q ⇒ Q ⊗2 x.v, y.w) −→ (t/x)v δ ∨ (inr(u), x.v, y.w) −→ (u/y)w Definition Appendix A.4. We define, by induction on the proposition A, a set of proofs A : • t ∈ ⊤ if t strongly terminates, • t ∈ ⊥ if t strongly terminates, • t ∈ A ⇒ B if t strongly terminates and whenever it reduces to a proof of the form λx.u, then for every v ∈ A , (v/x)u ∈ B , • t ∈ A ∧ B if t strongly terminates, whenever it reduces to a proof of the form u, v , then u ∈ A and v ∈ B , • t ∈ A ∨ B if t strongly terminates, whenever it reduces to a proof of the form inl(u), then u ∈ A , and whenever it reduces to a proof of the form inr(v), then v ∈ B .
Corollary Appendix A.21 (Termination). Let t be a proof of A in a context Γ. Then, t strongly terminates.
Proof. Let σ be the substitution mapping each variable x i : A i of Γ to itself. Note that, by Proposition Appendix A.6, this variable is an element of A i . Then, t = σt is an element of A . Hence, it strongly terminates.