In this blog post, we give an insight into the confluence of the sequent calculus, a property mainly considered since the discovery of the so-called Curry-Howard correspondence [1]. Confluence is often thought to be part of the well-understood folklore. For people already aware of the links between intuitionism and computation, it may feel natural and intuitive to think that LJ (intuitionistic sequent calculus [2]) should “behave well”, hence be both terminating and confluent. However, as we will show in the post, it appears that the subject is more subtle than expected.
Confluence and cut-elimination
First, we make clear what we mean by confluence. Cut-elimination evaluates a proof by eliminating an occurrence of cut-rule while preserving the hypothesis sequents (possibly with a different number of occurrences) and the concluding sequent.
Sometimes, it happens that there are several sequences of reductions possible: 
. If all paths lead to the same result, i.e. we have 
, we say that the system is confluent. The possibility of reducing to two different proofs is computationally problematic: imagine a program which can have two different results depending on how we evaluate it.
A crucial point of confluence is what we mean when we say that two proofs are equal. We first naively consider that two proofs are equal when they are identical.
The failure of Classical Logic
Cut-elimination for classical sequent calculus is known to have non-deterministic behaviour. We illustrate this with a simple example from Girard’s Proofs and Types [3]. In order to keep track of the location of formulas, we set 
. We have:
This can be reduced to one of these two proofs:
We obtain two structurally different proofs (because different rules are used but also because 
and 
can be different). Through the Curry-Howard interpretation, it corresponds to the fact that a program can be reduced to two different results depending on the evaluation strategy considered, which is something we usually do not want.
Two natural solutions are suggested by Lafont [3]:
- forbid the right-contraction rule and limit the right-hand side of sequents to at most one formula. This leads to intuitionistic logic (LJ) where this problem does not appear;
- more brutally, forbid all structural rules except exchange and obtain the linear fragment of linear logic.
The success of Intuitionistic Logic
Notice that the previous example does not apply in LJ since LJ limits the conclusion of sequents to at most one formula, i.e. sequents are of the form 
such that 
is either empty or a single formula. It is not even possible to use the same trick. Consider the same example as before with the on the left instead of the right (since contraction is only allowed on the left). We have the following cut-elimination:
If we think of the cut rule as using a lemma, we notice that the lemma 
introduced is erased by a weakening rule in the right-hand side. Since the only purpose of was to prove that lemma , it shows that is not needed in the proof and can be erased. Therefore, the cut-elimination yields a unique proof.
Confluence still fails with the commutation of rules
Although LJ has a better behaviour than LK, it is still easy to find counter-examples related to the commutation of rules:
This proof can be reduced as follows:
However one can reduce it in another way as follows:
So, we ended up with two proofs that are same up to the permutation of rules 
and 
. The same happens with a very trivial proof with cut and playing with exponentials (where 
):
This proof can be reduced either to the left or right branch. The problem is that applying weakening on a contracted formula does nothing, so the two proofs are essentially the same but still make confluence fail.
Solution for irrelevant differences: refining proof equivalence
The previous failure of confluence for LJ shows that the sequent calculus is actually not convenient to speak about confluence. However, it is not a sufficient reason to abandon the pursuit of confluence. Two proofs differing only from the order of application of rules or some irrelevant use of structural rules are essentially the same, logically speaking. Particularly, if we consider those proofs in the natural deduction, we will have again the same proofs since the translation from NJ to LJ is not injective, hence NJ yields a quotienting of LJ proofs [3]. And indeed, this idea of quotienting proofs is one of the reason to work with proof-nets of linear logic [4, 5] which are non-sequential representation of proofs where the the order of rules is irrelevant. Other representation of proofs attempted at capturing the “essence” of proofs such as expansion trees [6] or deep inference [7]. Denotational or categorical semantics can also be consider in order to quotient proofs [8, 9].
However, this approach has a dramatic consequence for most interpretations (especially for LK). Consider a semantic interpretation ![[[\pi]]](https://prooftheory.blog/wp-content/ql-cache/quicklatex.com-a388c8e5d91ed84eed40bb70acec5a7f_l3.png "Rendered by QuickLaTeX.com")
associating a mathematical object to a proof 
. If we would like to have the preservation of the semantics by cut-elimination, i.e. if 
implies ![[[\pi_1]]=[[\pi_2]]](https://prooftheory.blog/wp-content/ql-cache/quicklatex.com-0b4af759cdd855a6642bc5c70f122c59_l3.png "Rendered by QuickLaTeX.com")
, then in the case of the example above for LK where we have a reduction into two different proofs, we need to have . That means any proofs of 
are associated to the same object: they all collapse.
However, this is not the case in LJ because we could have two really different interpretations of the same sequent. If we follow the Curry-Howard correspondence between proofs and terms of the 
-calculus, one can consider two terms 
and 
. Although coming from NJ, their associated NJ proofs come from the following different LJ proofs:
Solution for non-determinism in LK: restricting rules
It has been shown that it is still possible to keep classical logic by using more sophisticated and fine-grained restrictions on the interaction between formulas in a proof (typically, restricting the allowed uses of the cut rule). These restrictions use the idea of polarisation and focussing respectively associated to Girard [10] and Andreoli [11].
The idea of polarisation that formulas are divided into two classes, positive and negative, and that rules take polarity into account. Some early polarised systems are Girard’s 
system [10], Danos et al.’s 
and 
systems [12] and Danos et al.’s 
system [13].
Recently, Liang and Miller’s defined a new system 
system [14] from which both and can be retrieved. It includes the following features in order to solve the non-determinism caused by structural rules:
- restriction of weakening on the axiom rule so that it cannot interfere with a cut rule;
- the cut rule can only take place between a positive and negative formula;
- contraction is limited to positive formulas.
As stated by Liang and Miller [14], the system , in particular, has the advantage to keep a presentation very close to the usual sequent calculus while obtaining determinism. The irrelevancy of rule order is handled with the idea of focussing which enforces an order while preserving provability (rules are divided into reversible and irreversible ones then in a bottom-up reading, it is always possible to focus on the reversible ones when possible).
We would like to thank Olivier Laurent for his useful opinion on the subject.
References
[Bibtex]
@article{howard1980formulae,
title={The formulae-as-types notion of construction},
author={Howard, William A},
journal={To HB Curry: essays on combinatory logic, lambda calculus and formalism},
volume={44},
pages={479--490},
year={1980}
}[Bibtex]
@book{dragalin1988mathematical,
title={Mathematical intuitionism},
author={Dragalin, Albert Grigorevich and Mendelson, Elliott},
year={1988},
publisher={American Mathematical Society}
}[Bibtex]
@book{girard1989proofs,
title={Proofs and types},
author={Girard, Jean-Yves and Taylor, Paul and Lafont, Yves},
volume={7},
year={1989},
publisher={Cambridge university press Cambridge}
}[Bibtex]
@incollection{girard2017proof,
title={Proof-nets: the parallel syntax for proof-theory},
author={Girard, Jean-Yves},
booktitle={Logic and Algebra},
pages={97--124},
year={2017},
publisher={Routledge}
}[Bibtex]
@article{girard1987linear,
title={Linear logic},
author={Girard, Jean-Yves},
journal={Theoretical computer science},
volume={50},
number={1},
pages={1--101},
year={1987},
publisher={Elsevier}
}[Bibtex]
@article{miller1987compact,
title={A compact representation of proofs},
author={Miller, Dale A},
journal={Studia Logica},
volume={46},
number={4},
pages={347--370},
year={1987},
publisher={Springer}
}[Bibtex]
@article{guglielmi2007system,
title={A system of interaction and structure},
author={Guglielmi, Alessio},
journal={ACM Transactions on Computational Logic (TOCL)},
volume={8},
number={1},
pages={1--es},
year={2007},
publisher={ACM New York, NY, USA}
}[Bibtex]
@article{lambek1968deductive,
title={Deductive systems and categories},
author={Lambek, Joachim},
journal={Mathematical Systems Theory},
volume={2},
number={4},
pages={287--318},
year={1968},
publisher={Springer}
}[Bibtex]
@article{lambek1974functional,
title={Functional completeness of cartesian categories},
author={Lambek, Joachim},
journal={Annals of Mathematical Logic},
volume={6},
number={3-4},
pages={259--292},
year={1974},
publisher={North-Holland}
}[Bibtex]
@article{girard1991new,
title={A new constructive logic: classic logic},
author={Girard, Jean-Yves},
journal={Mathematical structures in computer science},
volume={1},
number={3},
pages={255--296},
year={1991},
publisher={Cambridge University Press}
}[Bibtex]
@article{andreoli1992logic,
title={Logic programming with focusing proofs in linear logic},
author={Andreoli, Jean-Marc},
journal={Journal of logic and computation},
volume={2},
number={3},
pages={297--347},
year={1992},
publisher={Dov Gabbay}
}[Bibtex]
@article{danos1995lkq,
title={LKQ and LKT: sequent calculi for second order logic based upon dual linear decompositions of classical implication},
author={Danos, Vincent and Joinet, Jean-Baptiste and Schellinx, Harold},
journal={Advances in Linear Logic},
volume={222},
pages={211--224},
year={1995}
}[Bibtex]
@article{danos1997new,
title={A new deconstructive logic: Linear logic},
author={Danos, Vincent and Joinet, Jean-Baptiste and Schellinx, Harold},
journal={The Journal of Symbolic Logic},
volume={62},
number={3},
pages={755--807},
year={1997},
publisher={Cambridge University Press}
}@article{liang2020focusing,
title={Focusing Gentzen’s LK proof system},
author={Liang, Chuck and Miller, Dale},
journal={Submitted, April},
year={2020}
}
Hi Boris, Farzad, thanks for the nice post! Let me kick things off with some naive questions, since I have not played so much with this stuff:
Hi Anupam, thanks for your questions.
Re your first question, I am not completely sure if I understand the mix rule you are mentioning. For instance, I think the cut rule is not drivable using this mix and the other inferences rules.
Do you mean having mix instead of cut, and try to do mix-elimination?
If yes, there is a non-symmetrical mix elimination rule by G. Gentzen, which is the following:
And I think even this system is not confluent.
let us take the following proof:
And this proof can be reduced to two different proofs:
1)
2)
We can find this kind of example (not exactly this one) in the paper “Strong Normalisation Proofs for Cut Elimination in Gentzen’s Sequent Calculi” by Elias Tahhan.
About your second question, what do you mean by multi-conclusion calculus for intuitionistic logic?
No I do not mean the (full) mix of Gentzen that you describe, but a comment on your example: the two derivations (1) and (2) are still equivalent up to structural rules. It is not as extreme as the non-equivalence of Lafont’s wkR-wkL counterexample that you describe in your post. Can we say something formal here about confluence ‘up to an equivalence’ with respect to Gentzen’s mix-elimination? Such an equivalence might induce a reasonable computational interpretation associated with mix-elimination.
Now, what I meant was really adding my simplified mix rule to the system with cut. I believe that cut is internally eliminable in this system, but the wkR-wkL example can now be made to reduce to a unique derivation that ‘merges’ the two. It seems like this system might be confluent up to rule permutations (e.g. for reducing a cut between two mixes) and perhaps some structural rules. Do you know if this is true?
Regarding multi-conclusion version of LJ, this is usually attributed to Dummett I believe. See the following note by Valeria de Paiva: https://www.cs.bham.ac.uk/~vdp/publications/fil.pdf .
For your example of a cut between wR and wL in LJ, I believe it makes sense to erase π₁ when C is negative but π₂ when C is positive. Indeed, this is how polarised LK solves the dilemma, and the same cut-elimination strategy works for LJ. Consequently it makes sense to me to see this example as being non-confluent a priori. Does your argument for confluence on this counter-example assumes a particular computational interpretation?
Regarding the solution for non-determinism in LKF based on restricting rules, it looks like you are referring to the claim at the end of §2.1 in Liang and Miller (2021) (p.5 of http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lkf-2021-03-31.pdf). I find this remark cryptic, because indeed those problematic examples cannot be written in LKF due to the restricted shape of proofs, but in order to obtain a proof of the restricted shape, one has to first normalise it in a certain way, and how this reshaping is done is hidden in the admissibility proofs of many principles (notably cuts and structural rules). So once a restricted proof is obtained, it is possible that some arbitrary choices have been made already.
(Girard’s LC and Danos-Joinet-Schellinx’s LK^η, mentioned by Liang and Miller, solve the non-determinism by determining the reduction of proofs rather than by restricting proof rules, in the sense that rules of LK are derivable instead of merely admissible. This makes it easier to properly talk about confluence and preservation of a denotation.)
But! If we try and see where the choices might be made in Liang and Miller’s proof of cut-elimination, I do not think it appears in an obvious manner. There is a subtlety in how (and to which extent) the restrictions “solve” the problem of non-determinism.
Fortunately, there are some results that help us understand what is going on. Danos-Joinet-Schellinx (1997) remarked that the drive to reduce proofs in a way compatible η-expansions orients the cut-elimination in a certain way; more precisely that:
– the strategy that apparently arbitrarily favours one side according to the polarity (including by revealing cuts hidden in irreversible rules), introduced by LC,
– a strategy that applies reversion on-the-fly when there would be a dilemma, and
– a strategy that requires the least amount of modalities when translating into linear logic
coincide, and that in the proof system thus determined, η-equivalence is preserved by normalisation.
Consequently, they note, one is tempted to only work with maximally reversed proofs (as is done in LFK), which could be seen as representatives for a “quotient” of classical proofs up to reversion, and in which this strategy is enforced implicitly. Such a restriction was first studied by Quatrini and Tortora de Falco (“Polarisation des preuves classiques et renversement”, 1996), and a correspondence with (Krivine-style) negative translations into intuitionistic logic was shown by Laurent (“Étude de la polarisation en logique”, 2001). (Also, as mentioned in these works, this is a trick that breaks down with 2nd order quantifications.)
Girard’s proof sketch for cut-elimination in LK in the Blind Spot (2006, §3.4) seems to have been influenced by these works, and interestingly it has many similarities with Liang and Miller’s proof. Girard comments that such restrictions make the classical logic “locally” intuitionistic, which is one way to see polarisation.
As the Eng & Jafarrahmani article points out, there are two broad ways to make cut elimination more deterministic.
1) Lafont suggested forbidding structural rules—either on the right – yielding intuitionistic logic or on the left and right – yielding linear logic—can make cut-elimination deterministic.
2) We can use polarization in classical logic using (something like) the LKF proof system. Since the cut rule is applied to a positive and negative formula, and since only positive formulas are subjected to structural rules, non-determinism is also avoided.
There is a big difference between these two approaches. In the first approach, a global solution is enforced (structural rules are forbidden uniformly on the full proof), and classical logic is, essentially, forbidden. In the second approach, there is non-determinism in how one can polarize a classical formula, but once that choice is made, the rest is deterministic.
The latter approach has the merit of leaving the resolution of the non-determinism to the person writing the classical logic specification. For example, the programmer must say, for every occurrence of a conjunction and disjunction, whether or not it is additive or multiplicative. This approach should appeal to functional programmers trying to write classical logic specifications.