1. Introduction
The correspondences between logic and computation that can be found in the work of Curry-Howard Howard (Reference Howard1980) and Gentzen-Mints-Zucker Murfet and Troiani (Reference Murfet and Troiani2020) have as their deep content the observation that intuitionistic proofs can be understood as patterns of equality that relate differently named occurrences of the ‘same’ variable. Such patterns can be enacted on other patterns in a dynamical process that we call computation. By now, we have many useful ways of thinking about these patterns as static objects, but the mathematical theory of these patterns in motion, what Girard calls the geometry of interaction Girard (Reference Girard, Gray and Scedrov1989), is not yet as well-developed.
This paper is the first of a series in which we bring a fresh perspective to this geometry of interaction, using algebraic geometry. Here, we only consider the simplest kind of proof, multiplicative proof nets in linear logic, and their cut-elimination process. We assign to every multiplicative proof net
$\pi$
(from here on out just proof net) a polynomial ring
$P_\pi$
, in which the variables are occurrences of atomic propositions in the formulas labelling edges of
$\pi$
, and an ideal
$I_\pi$
in this ring (Definition 3.21). The generating set
$G_\pi$
for this ideal contains, in particular, for every
$(\!\operatorname {ax}\!)$
or
$(\!\operatorname {cut}\!)$
link in
$\pi$
on an atomic proposition
$A$
a polynomial
$A' - A$
where
$A, A'$
are two distinct copies of the same atomic proposition, one for each edge incident at the link (informally, both links say
$A = A$
and this equation is in
$G_\pi$
). For any reduction
$\gamma$
of
$\pi$
yielding another proof net
$\pi '$
, there is a natural inclusion
$P_{\pi '} \subseteq P_\pi$
where the variables in
$P_\pi$
not in
$P_{\pi '}$
are atomic propositions on edges eliminated by
$\gamma$
. The relationship between
$I_\pi$
and
$I_{\pi '}$
is straightforward (Corollary 4.7)
\begin{equation} I_{\pi '} = I_{\pi } \cap P_{\pi '}\,. \end{equation}
If we think of
$I_\pi$
as all consequences of the generating equations in
$G_\pi$
, then this says that the pattern of equalities between the occurrences of atomic propositions in
$\pi '$
derived from the equations in
$G_\pi$
is the same as the pattern we would write down directly from the structure of
$\pi '$
. There is, however, an important subtlety here: the generating set
$G_{\pi '}$
for
$I_{\pi '}$
cannot be derived from
$G_\pi$
by simple intersection, as
\begin{equation} G_{\pi '} \neq G_{\pi } \cap P_{\pi '}\,. \end{equation}
The difference between
$G_\pi$
and
$I_\pi$
is analogous to the difference between a set of axioms and the set of all propositions that may be derived from those axioms. The reason for the lack of equality in (2) is easy to understand: if
$\gamma$
eliminates a
$(\!\operatorname {cut}\!)$
link as above then
$A' - A \in G_\pi$
, and if
$A_1 - A', A - A_2 \in G_\pi$
are generators associated to other links in
$\pi$
then
\begin{equation*} A_1 - A_2 = (A_1 - A') + (A' - A) + (A - A_2) \in I_\pi \end{equation*}
and hence
$A_1 - A_2 \in I_{\pi '} = I_\pi \cap P_\pi$
. As we will see, this is one of the generators in
$G_{\pi '}$
(since in the reduced proof net
$A_1, A_2$
are incident at a single link). However, if we simply intersect
$G_\pi$
with
$P_\pi$
, then we delete all three of the equations
$A_1 - A', A' - A, A - A_2$
since each contains some eliminated variable, and the connection between
$A_1$
and
$A_2$
is lost.
In algebraic geometry, Elimination Theory (Cox et al. Reference Cox, Little and O’Shea2015, Ch. 3) provides a general framework for eliminating variables from systems of polynomial equations, in the sense that
$A', A$
have been eliminated from
$A_1 - A', A' - A, A - A_2$
to obtain
$A_1 - A_2$
. In our present circumstances, the theory says the following:
-
(1) Choose a lexicographic monomial order
$\lt _\gamma$
for
$P_\pi$
in which the variables eliminated by the reduction
$\gamma$
(e.g.
$A', A$
) are large. -
(2) Compute a Gröbner basis for
$I_\pi$
from
$G_\pi$
using this monomial order. -
(3) Intersect the resulting Gröbner basis with
$P_{\pi '}$
.
The main theorem of Elimination Theory (recalled as Theorem 5.7 here) says that the intersection in (3) is a Gröbner basis for
$I_{\pi '}$
. We prove in Theorem 7.2 that, if the monomial order is chosen carefully and a particular form of the Buchberger algorithm for computing Gröbner bases is used in (2), then (3) computes
$G_{\pi '}$
(which is a Gröbner basis for
$I_{\pi '}$
with respect to a monomial order determined by the ordering of atomic propositions along persistent paths). In this sense, the Buchberger algorithm can be viewed as an algebraic interpretation of cut-elimination for multiplicative proof nets.
The goals of this paper are to set up a basic dictionary between
-
• multiplicative proof nets and ideals
-
• reduction sequences and monomial orders
-
• cut-elimination and elimination
While there is some small novelty in the form of the Buchberger algorithm that makes this connection clearest (we call it Buchberger with Early Stopping), there is nothing deep here logically, algebraically or geometrically. Indeed, the ideals
$I_\pi$
do not have a very interesting geometry: the associated affine variety is just an intersection of pairwise diagonals. In subsequent papers in this series, we introduce, on top of the foundations laid here, more interesting algebra and geometry (see Section 8.1 for some hints).
Previous authors have also developed Girard’s Geometry of Interaction (GoI) programme; we mention a few here. In Abramsky et al. (Reference Abramsky., Haghverdi. and Scott1999), the connection between GoI and linear combinatory algebras is explored. There is also Abramsky (Reference Abramsky1994), which introduces traced monoidal categories as a framework for capturing feedback loops and iterative processes, making it particularly relevant to modelling GoI and cut-elimination. This work is built upon in Haghverdi and Scott (Reference Haghverdi. and Scott2006), which considers the cut-elimination process within the framework of Abramsky (Reference Abramsky1994). We believe that the work considered in the present paper can be organised into the language of GoI situations and traced monoidal categories, a connection that we plan to explore in future work.
2. Motivation: The Canonical Detour
The reader wishing to dive straight into the details should skip to Section 3. In this section, we recall some of the concepts behind proof nets, following (Girard Reference Girard2011, §11.2.2). The deduction rules for intuitionistic linear natural deduction include the introduction and elimination rules for linear implication:
Among other criticisms of this system of natural deduction, Girard points to the need for a non-local ‘gimmick’ (the de Bruijn index
$\textbf{1}$
) to ‘physically’ link the hypothesis
$A$
to the introduction rule (Girard Reference Girard2011, §11.2.1). This non-locality is resolved in proof nets, in two steps: firstly, by giving up active hypotheses and having only conclusions, and secondly by bringing these hypotheses-as-conclusions down to meet the introduction rule that employs them. The first step involves introducing the
$(\!\operatorname {ax}\!)$
and
$(\!\operatorname {cut}\!)$
links
which ‘replace a hypothesis by a conclusion and ‘vice versa’. The second step, in which
$\neg A$
is brought down to meet the introduction rule, is made clear by the proof net interpreting the introduction rule in (3)
To explain Girard’s ‘vice versa’ note that we can read the elimination rule of (3) as converting a proof of the conclusion
$A \multimap B$
into a proof of
$B$
on hypothesis
$A$
, and this is achieved in proof nets via
$(\!\operatorname {cut}\!)$
, as shown in the following diagram:
The reduction step in natural deduction is the elimination of the ‘detour’ created when the introduction rule in (3) appears as the proof of
$A \multimap B$
in the elimination rule; this detour is eliminated to obtain a more straightforward proof of
$B$
by combining the given proof of
$A$
and the proof of
$B$
on hypothesis
$A$
. The canonical example of a detour is shown below:
In the language of (linear) lambda terms, the proof net (4) is
$\lambda x \,.\, M$
for some term
$M$
determined by the proof of
$B$
from
$A$
in ellipsis. If the proof of
$A$
in ellipsis in (5) has term
$N$
, then the cut (6) corresponds to
$((\lambda x \,.\, M) N)$
reducing to
$M[ x := N ]$
with the ‘output’ routed through the
$(\!\operatorname {cut}\!)$
and
$\otimes$
links to the conclusion
$B$
on the left. We can imagine a path (a more refined version of which we will later call a persistent path) from the proof of
$A$
down through the
$\otimes$
link and
$(\!\operatorname {cut}\!)$
links, up through the
$\multimap$
link and around to the left through
$\neg A$
to the
$(\!\operatorname {ax}\!)$
link, then back down through the proof of
$B$
from
$A$
(the one with term
$M$
) through the
$\multimap$
and
$(\!\operatorname {cut}\!)$
links, then up through
$\otimes$
and the
$(\!\operatorname {ax}\!)$
for
$B$
until it exits the conclusion
$B$
. Along this path, ‘nothing happens’ except when we pass through the proof of
$B$
from
$A$
, and we will get the same result if we ‘straighten out’ the rest of the proof net, leaving just this interesting part with the proof of
$A$
feeding into it. This is the result of cut-elimination for this proof net.
Let us sketch the algebro-geometric point of view on this situation. We first distinguish every occurrence of the formulas
$A,B$
in the proof net above by giving it an indexFootnote
1
Suppose the atomic propositions occurring in
$A$
are
$X_1,\ldots ,X_n$
and label the occurrence of
$X_j$
in
$A_i$
by
$X^{(i)}_j$
. Similarly let
$Y_1,\ldots ,Y_m$
be the atomic propositions in
$B$
and write
$Y^{(i)}_j$
for the occurrence of
$Y_j$
in
$B_i$
. We let
$\mathbf{X}^{(i)}$
(resp.
$\mathbf{Y}^{(i)}$
) stand for all the
$X$
-variables (resp.
$Y$
-variables) with superscript
$i$
. Then, associated with the path described above through the proof net are the identifications
\begin{equation} \mathbf{X}^{(3)} = \mathbf{X}^{(4)} = \mathbf{X}^{(5)} = \mathbf{X}^{(1)} = \mathbf{X}^{(2)} \end{equation}
leading to the ‘input’ of the proof
$B$
of
$A$
, and the identifications
\begin{equation} \mathbf{Y}^{(3)} = \mathbf{Y}^{(5)} = \mathbf{Y}^{(4)} = \mathbf{Y}^{(2)} = \mathbf{Y}^{(1)} \end{equation}
leading from the ‘output’ back through the proof net to the conclusion
$B$
. Here,
$\mathbf{X}^{(i)} = \mathbf{X}^{(i')}$
stands for a sequence of equations
$X^{(i)}_j = X^{(i')}_j$
for
$1 \le j \le n$
. We have grouped these equations by how they appear on the path from
$A$
to
$B$
through the proof net, but we can also group them by link
\begin{align} (\!\operatorname {ax}\!)_B &\quad \mathbf{Y}^{(1)} = \mathbf{Y}^{(2)} \end{align}
\begin{align} (\!\operatorname {ax}\!)_A &\quad \mathbf{X}^{(1)} = \mathbf{X}^{(2)} \end{align}
\begin{align} (\!\otimes\!) &\quad \mathbf{X}^{(3)} = \mathbf{X}^{(4)}, \mathbf{Y}^{(2)} = \mathbf{Y}^{(4)} \end{align}
\begin{align} (\!\multimap\!) &\quad \mathbf{Y}^{(3)} = \mathbf{Y}^{(5)}, \mathbf{X}^{(1)} = \mathbf{X}^{(5)} \end{align}
\begin{align} (\!\operatorname {cut}\!) &\quad \mathbf{X}^{(4)} = \mathbf{X}^{(5)}, \mathbf{Y}^{(4)} = \mathbf{Y}^{(5)}\,. \end{align}
For some base field
$k$
, we consider the polynomial ring
$P$
generated by all the atomic propositions
\begin{equation} P = k[ \mathbf{X}^{(1)}, \ldots , \mathbf{X}^{(5)}, \mathbf{Y}^{(1)}, \ldots , \mathbf{Y}^{(5)}] \end{equation}
and to the sets of equations (9)–(13) we associate the ideals (one for each link)
\begin{align} I_{(\!\operatorname {ax}\!)_B} &= \langle \mathbf{Y}^{(1)} - \mathbf{Y}^{(2)}\rangle = \big\langle Y^{(1)}_1 - Y^{(2)}_1, \ldots , Y^{(1)}_m - Y^{(2)}_m\big\rangle \end{align}
\begin{align} I_{(\!\operatorname {ax}\!)_A} &= \langle \mathbf{X}^{(1)} - \mathbf{X}^{(2)} \rangle \end{align}
\begin{align} I_{\otimes } &= \langle \mathbf{X}^{(3)} - \mathbf{X}^{(4)}, \mathbf{Y}^{(2)} - \mathbf{Y}^{(4)} \rangle \end{align}
\begin{align} I_{\multimap } &= \langle \mathbf{Y}^{(3)} - \mathbf{Y}^{(5)}, \mathbf{X}^{(1)} - \mathbf{X}^{(5)} \rangle \end{align}
\begin{align} I_{(\!\operatorname {cut}\!)} &= \langle \mathbf{X}^{(4)} - \mathbf{X}^{(5)}, \mathbf{Y}^{(4)} - \mathbf{Y}^{(5)} \rangle \,. \end{align}
Assume that somehow ideals
\begin{equation} \mathfrak{n} \subseteq k[\mathbf{X}^{(3)}]\,, \qquad \mathfrak{m} \subseteq k[\mathbf{X}^{(2)}, \mathbf{Y}^{(3)}] \end{equation}
have been assigned to the proofs of
$A$
, and of
$B$
from
$A$
, in ellipsis. The ideal of the proof net (6) is (see Section 3 for the general definition)
\begin{equation} I = I_{(\!\operatorname {ax}\!)_B} + I_{(\!\operatorname {ax}\!)_A} + I_{\otimes } + I_{\multimap } + I_{(\!\operatorname {cut}\!)} + \mathfrak{m} + \mathfrak{n} \subseteq P\,. \end{equation}
This ideal represents the pattern of equality of the proof net in terms of the variables occurring on every edge. When it comes to the interaction of this proof net with other nets under cut-elimination, this pattern in the ‘interior’ only matters insofar as it implicitly determines a pattern of equality between the variables in
$\mathbf{X}^{(3)}$
and
$\mathbf{Y}^{(1)}$
, which live on the ‘boundary’ of the proof net. Computation is the process of making this implicit pattern in the interior explicit on the boundary (Section 7).
The pattern of equalities on the boundary is the set of equations between the variables
$\mathbf{X}^{(3)},\mathbf{Y}^{(1)}$
which are implied by the equations between the variables in the interior. These equations form an ideal
$J \subseteq k[\mathbf{X}^{(3)},\mathbf{Y}^{(1)}]$
and to say that the equations in
$J$
follow from those in
$I$
is to say that under the inclusion
\begin{equation*} \iota : k[\mathbf{X}^{(3)},\mathbf{Y}^{(1)}] \longrightarrow P \end{equation*}
we have
$\iota (J) \subseteq I$
. To say that every equation between the variables
$\mathbf{X}^{(3)},\mathbf{Y}^{(1)}$
implied by the equations in
$I$
is in
$J$
is to say further that
\begin{equation} J = I \cap k[\mathbf{X}^{(3)},\mathbf{Y}^{(1)}]\,. \end{equation}
So, what is a generating set for this ideal? With a little computation using the above equations, it is easy to see that
$J = \mathfrak{n} + \mathfrak{m}'$
is the sum of
$\mathfrak{n}$
with the ideal
$\mathfrak{m}'$
obtained from
$\mathfrak{m}$
by replacing every generator
$f(\mathbf{X}^{(2)}, \mathbf{Y}^{(3)})$
of this ideal with the polynomial
$f(\mathbf{X}^{(3)}, \mathbf{Y}^{(1)})$
obtained by substituting
$X^{(3)}_i$
for
$X^{(2)}_i$
in
$f$
for all
$1 \le i \le n$
and
$Y^{(1)}_j$
for
$Y^{(3)}_j$
for all
$1 \le j \le m$
. This parallels the substitution
$M[ x := N ]$
.
In this paper, we treat such substitution processes systematically from the point of view of Elimination Theory, as instances of the Buchberger algorithm for computing a Gröbner basis of
$J$
from
$I$
.
3. The Ideal of a Proof
To any proof structure
$\pi$
, we will associate a polynomial ring
$P_\pi$
. This is the universal algebraic object in which we can add and multiply the atomic propositions in the formulas adorning the edges of the proof structure (noting that each occurrence gets its own copy in the polynomial ring) and multiply them by scalars from some fixed base field
$k$
. The idea of making propositions into objects of arithmetic or algebra is due to Boole Boole (Reference Boole1854). The ring
$P_\pi$
only reflects the set of occurrences of atomic propositions in
$\pi$
not the structure of the proof; this structure is encoded in an ideal
$I_\pi \subseteq P_\pi$
(Definition 3.21).
3.1 Background
We assume familiarity with linear logic, for an introduction see Girard et al. (Reference Girard, Lafont and Taylor1989); Laurent (Reference Laurent2013); Murfet (Reference Murfet2017); Troiani (Reference Troiani2020).
Definition 3.1.
There is an infinite set of unoriented atoms
$X,Y,Z,\ldots$
and an oriented atom (or atomic proposition) is a pair
$(X,+)$
or
$(X,-)$
where
$X$
is an unoriented atom. Let
$\mathcal{A}$
denote the set of oriented atoms.
For
$x \in \{ +, - \}$
, we write
$\bar {x}$
for the negation, so
$\bar {+} = -, \bar {-} = +$
.
Definition 3.2. The set of pre-formulas is defined as follows:
-
• Any atomic proposition is a pre-formula.
-
• If
$A,B$
are pre-formulas then so are
$A \otimes B$
,
$A \unicode{x214B} B$
. -
• If
$A$
is a pre-formula then so is
$\neg A$
.
The set of formulas is the quotient of the set of pre-formulas by the equivalence relation
$=$
generated, for arbitrary formulas
$A,B$
and unoriented atom
$X$
, by
\begin{equation*} \neg (A \otimes B) = \neg B \unicode{x214B} \neg A,\qquad \neg (A \unicode{x214B} B) = \neg B \otimes \neg A,\qquad \neg (X, x) = (X, \bar {x}) \end{equation*}
Let
$\mathcal{F}$
denote the set of formulas.
The following easy lemma is left to the reader:
Lemma 3.3.
For all formulas
$A$
we have
$\neg \neg A = A$
.
Definition 3.4.
Let
$\mathcal{A}^\ast = \bigcup _{n \geq 0}\mathcal{A}^n$
be the set of sequences of oriented atoms of length
$\geq 0$
. We define an involution
$r$
on
$\mathcal{A}^\ast$
as follows:
\begin{align*} r: \mathcal{A}^\ast &\longrightarrow \mathcal{A}^\ast \\ \big ((X_1,x_1),\ldots ,(X_n,x_n)\big ) &\longmapsto \big ((X_n,\bar {x}_n),\ldots ,(X_1,\bar {x}_1)\big ) \end{align*}
For the empty string
$\emptyset \in \mathcal{A}^\ast$
, we define
$r(\emptyset ) = \emptyset$
.
The set
$\mathcal{A}^\ast$
is a monoid under concatenation
$c: \mathcal{A}^\ast \times \mathcal{A}^\ast \longrightarrow \mathcal{A}^\ast$
with identity
$\emptyset$
.
Definition 3.5.
We denote by
$\otimes : \mathcal{F} \times \mathcal{F} \longrightarrow \mathcal{F}$
the function which maps a pair of formulas
$(A,B)$
to the formula
$A \otimes B$
. Similarly,
$\unicode{x214B}: \mathcal{F} \times \mathcal{F} \longrightarrow \mathcal{F}$
denotes the function such that
$\unicode{x214B}(A,B) = A \unicode{x214B} B$
and
$\neg : \mathcal{F} \longrightarrow \mathcal{F}$
denotes the function such that
$\neg (A) = \neg A$
. We denote by
$\operatorname {inc}: \mathcal{A} \longrightarrow \mathcal{F}$
the map which sends an oriented atom
$(X,x)$
to itself
$(X,x)$
, and lastly we denote by
$\operatorname {\iota }: \mathcal{A} \longrightarrow \mathcal{A}^\ast$
the function which maps an oriented atom
$(X,x)$
to the sequence consisting only of
$(X,x)$
.
Lemma 3.6.
There is a unique map
$a: \mathcal{F} \longrightarrow \mathcal{A}^\ast$
making the following diagrams commute
Proof. Left to the reader.
Definition 3.7.
Let
$A$
be a formula. The sequence of oriented atoms of
$A$
is
\begin{equation*} a(A) = (X_1,x_1),\ldots ,(X_n,x_n) \end{equation*}
as defined by the previous lemma. The sequence of unoriented atoms of
$A$
is
$X_1,\ldots ,X_n$
and the set of unoriented atoms of
$A$
is the disjoint union
$U_A = \lbrace X_1 \rbrace \coprod \ldots \coprod \lbrace X_n \rbrace$
.
Our definition of multiplicative proof structures follows that of Laurent (Reference Laurent2013) but with edges labelled by formulas in the sense of Definition 3.2. We remind the reader of the notion of a multigraph (a graph with multiple edges between vertices).
Definition 3.8.
A directed multigraph is a triple
$(V,E,\varphi )$
where:
-
•
$V$
is a set of vertices or nodes.
-
•
$E$
is a set of edges.
-
•
$\Gamma : E \longrightarrow \lbrace (x,y) \mid x, y \in V\rbrace$
is a function from the set of edges to the set of ordered pairs of vertices.
For
$e \in E$
, the first element of
$\Gamma (e)$
is the source and the second element is the target.
Definition 3.9.
A proof structure is a directed multigraph with edges labelled by formulas and with vertices labelled by
$(\!\operatorname {ax}\!), (\!\operatorname {cut}\!), \otimes , \unicode{x214B}$
or
$\operatorname {c}$
. The incoming edges of a vertex are called its premises, the outgoing edges are its conclusions. Proof structures are required to adhere to the following conditions:
-
• Each vertex labelled
$(\!\operatorname {ax}\!)$
has exactly two conclusions and no premise, the conclusions are labelled
$A$
and
$\neg A$
for some
$A$
. We call this an axiom link.
-
• Each vertex labelled
$(\!\operatorname {cut}\!)$
has exactly two premises and no conclusion, where the premises are labelled
$A$
and
$\neg A$
for some
$A$
. We call this a cut link.
-
• Each vertex labelled
$\otimes$
has exactly two premises and one conclusion. The premises are ordered, the smallest one is called the left premise of the vertex, the biggest one is called the right premise. The left premise is labelled
$A$
, the right premise is labelled
$B$
and the conclusion is labelled
$A \otimes B$
, for some
$A,B$
. We call this a tensor link.
-
• Each vertex labelled
$\unicode{x214B}$
has exactly two ordered premises and one conclusion. The left premise is labelled
$A$
, the right premise is labelled
$B$
and the conclusion is labelled
$A \unicode{x214B} B$
, for some
$A,B$
. We call this a par link.
-
• Each vertex labelled
$\operatorname {c}$
has exactly one premise and no conclusion. Such a premise of a vertex labelled
$\operatorname {c}$
is called a conclusion of the proof structure.
A link is any of an axiom link, tensor link, par link, or cut link. Conclusions are not links.
Definition 3.10. A proof net is a proof structure which is the image under the translation map of a sequent calculus proof in multiplicative linear logic, see (Troiani Reference Troiani2020 , Definition 1.0.12).
Example 3.11. The smallest proof net with a single conclusion is
This is the translation of the following sequent calculus proof.
Example 3.12.
As in Section 2, the following proof net is the translation of the linear lambda term
$(\lambda x. x)x$
.
This is the translation of the following sequent style proof.
Example 3.13. The following is a proof structure which is not a proof net.
Suppose the above proof structure was equal to
$T(\pi )$
where
$\pi$
is a sequent calculus proof. Then there exist sequent calculus proofs
$\pi _1, \pi _2$
such that
$\pi$
is given by a cut rule with
$\pi _1$
on the left branch and
$\pi _2$
on the right branch. Since sequent calculus proofs are binary trees with leaves labelled by instances of the Axiom rule, it follows that
$\pi$
admits at least two instances of an Axiom rule, a contradiction.
3.2 The polynomial ring
Let
$k$
be a field.
Definition 3.14.
The polynomial ring of a formula
$A$
is the free commutative
$k$
-algebra
$P_A$
on the set
$U_A$
of unoriented atoms of
$A$
.
Remark 3.15. Some technical remarks:
-
• The algebra
$P_A$
does not depend on an ordering of the unoriented atoms in
$A$
. For example, we can take as our concrete realisation of
$P_A$
the symmetric algebra
$\operatorname {Sym}(V_A)$
on the free vector space
$V_A$
on the set
$U_A$
. -
• If we choose an ordering on
$U_A$
so that
$U_A = \{X_1,\ldots ,X_n\}$
then
$P_A \cong k[X_1,\ldots ,X_n]$
. It will be convenient to present
$P_A$
in this way in the following, but unless we explicitly introduce an ordering on
$U_A$
no meaning should be associated to the indices
$i$
in
$X_i$
. -
• The oriented atom
$(X,+)$
appears twice in
$A = (X,+) \otimes (X,+)$
, so the sequence of unoriented atoms of
$A$
is
$X,X$
and the set of unoriented atoms is a disjoint union
$\{ X, X' \} = \{ X \} \coprod \{ X \}$
inside which we can distinguish the two copies of
$X$
(the precise nature of these copies is not important here). Hence
$P_A \cong k[X, X']$
.
Definition 3.16.
The set of unoriented atoms of a proof structure
$\pi$
is the disjoint union
$U_\pi = \coprod _{e \in E} U_{A_e}$
where
$E$
is the set of edges in
$\pi$
and for each
$e \in E$
we write
$U_{A_e}$
for the set of unoriented atoms of the formula
$A_e$
labelling
$e$
.
Definition 3.17.
The polynomial ring of a proof structure
$\pi$
is the free commutative
$k$
-algebra on the set
$U_\pi$
of unoriented atoms of
$\pi$
.
The polynomial ring of a proof structure
$\pi$
is the polynomial ring with a generator for each pair consisting of an edge
$e$
in
$\pi$
and an unoriented atom of the formula labelling
$e$
. If we choose an ordering on the edges
$e$
of
$\pi$
, then we have an isomorphism
\begin{equation} P_\pi = k \Bigg[\coprod _{e \in E}U_{A_e}\Bigg] \cong \bigotimes _{e \in E}P_{A_e}\,. \end{equation}
3.3 The ideal of a link
The ideal generated by a set
$S$
is denoted
$\langle S \rangle$
. For each type of link
$l$
, we define the generating set
$G_l$
and link ideal
$I_l = \langle G_l \rangle$
in the polynomial ring generated by the set of unoriented atoms of formulas labelling edges incident at the link. Below
$(X_1,x_1),\ldots ,(X_n,x_n)$
is the sequence of oriented atoms of a formula
$A$
, and
$(Y_1,y_1),\ldots ,(Y_m,y_m)$
is the sequence of oriented atoms of
$B$
.
Definition 3.18 (Cut and Axiom). If
$l$
is one of the links
then in the polynomial ring generated by the disjoint union of unoriented atoms
$U_A \coprod U_{\neg A}$
\begin{equation} G_l = \big \{ X_i - X_i'\big \}_{i = 1}^n \end{equation}
where we write
$X'_i$
for the elements of
$U_{\neg A}$
.
Definition 3.19 (Tensor and Par links). If
$l$
is one of the links
then in polynomial ring generated by the disjoint union
$U_A \coprod U_{B} \coprod U_{A \boxtimes B}$
(where
$\boxtimes$
is either
$\otimes$
or
$\unicode{x214B}$
)
\begin{align*} G_l = \big \{ X_i - X_i'\big \}_{i = 1}^n \cup \big \{ Y_j - Y_j' \big \}_{j = 1}^m \end{align*}
where
$X'_i, Y'_j$
denote elements of
$U_{A \boxtimes B}$
.
In Definition 3.17, we defined the polynomial ring
$P_\pi$
of a proof structure
$\pi$
. If
$l$
is a link of
$\pi$
, then in the obvious way we can identify
$G_l$
with a subset of
$P_\pi$
.
Definition 3.20.
The ideal of a link
$l$
in a proof structure
$\pi$
is the ideal
$I_l = \langle G_l \rangle \subseteq P_\pi$
generated by
$G_l$
in
$P_\pi$
.
Definition 3.21.
Let
$\pi$
be a proof structure with set of links
$\mathcal{L}$
. Then,
\begin{equation} G_\pi := \bigcup _{l \in \mathcal{L}}G_l\,. \end{equation}
The defining ideal
$I_\pi$
is the ideal in
$P_\pi$
generated by
$G_\pi$
, or equivalently
\begin{equation} I_\pi = \sum _{l \in \mathcal{L}}I_l\,. \end{equation}
The coordinate ring of
$\pi$
is the quotient
$R_\pi = P_\pi /I_\pi$
.
Example 3.22.
Consider the proof net
$\pi$
of Example 3.11 in which we set
$A$
to be the atomic proposition
$A = (X,+)$
The set of unoriented atoms of
$\pi$
is
$\{ X, X', X'', X'''\}$
where we associate
$X$
to
$A$
,
$X'$
to
$\neg A$
and we let
$X'', X'''$
be the sequence of unoriented atoms of
$\neg A \unicode{x214B} A$
. Then
\begin{align*} G_{(\!\operatorname {ax}\!)} = \{ X - X' \}\, \qquad G_{\unicode{x214B}} = \{ X - X''', X' - X'' \}\,. \end{align*}
Hence,
\begin{equation*} R_\pi = P_\pi / I_\pi = k[X, X', X'', X''']/(I_{(\!\operatorname {ax}\!)} + I_{\unicode{x214B}}) \cong k[X, X']/I_{(\!\operatorname {ax}\!)} \cong k[X] \end{equation*}
in which
$X = X' = X'' = X'''$
.
Example 3.23.
Consider the proof structure
$\rho$
of Example 3.13 (which is not a proof net) with
$A = (X,+)$
. Then
$G_{(\!\operatorname {ax}\!)} = \{ X - X' \} = G_{(\!\operatorname {cut}\!)}$
so
$R_\rho = k[X, X']/(X - X') \cong k[X]$
.
4. Reduction
We have now associated to each proof structure
$\pi$
a pair
$(I_\pi , P_\pi )$
consisting of a polynomial ring
$P_\pi$
generated by the unoriented atoms of
$\pi$
and an ideal
$I_\pi$
in this ring generated by differences
$U - V$
where
$U,V$
are ‘the same’ variable on two different edges incident at a link in
$\pi$
. We now turn to the cut-elimination process for multiplicative proof nets and study how to think about a reduction
$\pi \longrightarrow \pi '$
in terms of
$(I_\pi , P_\pi ), (I_{\pi '}, P_{\pi '})$
.
Definition 4.1.
An
$a$
-redex in a proof structure
$\pi$
is a subgraph of the form
Definition 4.2.
An
$m$
-redex in a proof structure
$\pi$
is a subgraph of the form
Definition 4.3.
A reduction
$\gamma : \pi \longrightarrow \pi '$
between proof structures
$\pi , \pi '$
is an
$a$
-redex or
$m$
-redex
$\gamma$
in
$\pi$
such that reducing
$\gamma$
in
$\pi$
yields
$\pi '$
, where
-
• if
$\gamma$
is an
$a$
-redex (30), the reduction is the proof structure obtained by replacing this subgraph by what is displayed on the right in Figure 1. -
• if
$\gamma$
is an
$m$
-redex (31), the reduction is the proof structure obtained by replacing this subgraph by what is displayed on the bottom in Figure 2.
Definition 4.4.
Let
$\gamma : \pi \longrightarrow \pi '$
be a reduction of proof structures. We define morphisms
$S_\gamma , T_\gamma$
of
$k$
-algebras
as follows: an unoriented atom in
$\pi '$
(resp.
$\pi$
) not associated to an edge in the subgraph
$\gamma$
is sent to itself in
$\pi$
(resp.
$\pi '$
) by
$T_\gamma$
(resp.
$S_\gamma$
), other unoriented atoms are mapped according to the schematic in Figure
3
(resp. Figure
4
).
It is easily checked that
Reduction of an
$a$
-redex.
Reduction of a
$m$
-redex.
Lemma 4.5.
$S_\gamma T_\gamma = 1$
.
Schematic for
$T_\gamma$
.
Schematic for
$S_\gamma$
.
The maps
$T_\gamma , S_\gamma$
are morphisms of the pairs
$(I_\pi , P_\pi ), (I_{\pi '}, P_{\pi '})$
in the following sense:
Proposition 4.6.
If
$\gamma : \pi \longrightarrow \pi '$
is a reduction of proof structures then
\begin{equation} T_\gamma (I_{\pi '}) \subseteq I_\pi , \qquad S_\gamma (I_\pi ) \subseteq I_{\pi '} \end{equation}
and the induced morphisms of
$k$
-algebras
$\overline {T}_\gamma , \overline {S}_\gamma$
making the squares in the following diagram commute
are mutually inverse isomorphisms where
$p, p'$
are the quotient maps.
Proof.
To prove
$S_\gamma (I_\pi ) \subseteq I_{\pi '}$
, we first choose a link
$l$
in
$\pi$
. If
$l$
does not appear in the reduction (i.e. it is not the particular
$(\!\operatorname {ax}\!)$
or
$(\!\operatorname {cut}\!)$
involved in an
$a$
-redex nor the particular
$\otimes , \unicode{x214B},(\!\operatorname {cut}\!)$
in an
$m$
-redex) and no edge of
$l$
is in the redex, then every generator of
$I_l$
is in
$I_{\pi '}$
. If
$l$
does not appear in
$\gamma$
but
$l,\gamma$
share an edge, then
$S_\gamma (I_l) \subseteq I_{\pi '}$
clearly holds in the case where
$\gamma$
is an
$m$
-redex. In the case of
$(\!\operatorname {ax}\!)$
/
$(\!\operatorname {cut}\!)$
(as e.g., the red
$(\!\operatorname {ax}\!)$
link in Diagram (35) below)
the equations generating
$I_l$
are of the form
$X - X'$
, where
$X$
is an unoriented atom of the label of an edge in the redex and
$X'$
is an unoriented atom of the label of an edge occuring in
$l$
. By inspection of Figure 1, we see
$S_\gamma (X - X') \in I_{\pi '}$
.
Now, we consider the case where
$l$
is in the redex and
$\gamma$
reduces an
$a$
-redex. For all generators
$X - X'$
of
$I_l$
, we have
$S_\gamma (X) = S_\gamma (X')$
and so
$S_\gamma (X - X') = 0 \in I_{\pi '}$
. Now, consider the case where
$l$
is an
$m$
-redex. If
$l$
is the displayed tensor or par link then any generator
$X - X'$
of
$I_{\pi '}$
associated to
$l$
satisfies
$S_\gamma (X) = S_\gamma (X')$
and so just as we had in the previous case we have
$S_\gamma (X - X') = 0 \in I_{\pi '}$
. The final case to consider is when
$l$
is the displayed cut link. Let
$X - X'$
be a generator for
$I_l$
. Let
$l_1$
denote the cut link in
$\pi$
with premises labelled
$B, \neg B$
and
$l_2$
denote the cut link with premises
$A, \neg A$
. We have that
$S_\gamma (X) - S_\gamma (X') \in I_{l_1}$
if
$X$
is an undirected atom of
$A$
and
$S_\gamma (X) - S_\gamma (X') \in I_{l_2}$
if
$X$
is an undirected atom of
$B$
. In either case, we have that
$S_\gamma (X) - S_\gamma (X') \in I_{\pi '}$
.
Now, we prove
$T_\gamma (I_{\pi '}) \subseteq I_{\pi }$
. A generator
$X - X'$
of
$I_{\pi '}$
is associated to a link
$l$
of
$\pi '$
. If
$\gamma$
is a reduction of an
$a$
-redex then
$l$
is also present in
$\pi$
and it is clear
$T_{\gamma }(X -X') \in I_{\pi }$
. If
$\gamma$
is a reduction of an
$m$
-redex and
$l$
is not one of the cut links shown in the bottom diagram of Figure 2 then the same reasoning applies. If
$l$
is one of these cut links the generator is either
$X - X'$
for some unoriented atom
$X$
in
$A$
or
$Y - Y'$
for some unoriented atom
$Y$
in
$B$
, where we are using the notation of Figure 2. There exists unoriented atoms
$X'',X'''$
of
$A \otimes B$
and
$\neg A \unicode{x214B} \neg B$
, respectively, which satisfy
$X - X'', X'' - X''', X''' - X' \in I_{\pi }$
. Hence,
$T_{\gamma }(X - X') = (X - X'') + (X'' - X''') + (X''' - X') \in I_{\pi }$
, and similarly for
$Y - Y'$
. Hence,
$T_{\gamma }(I_{\pi '}) \subseteq I_{\pi }$
.
Hence,
$\overline {S}_\gamma , \overline {T}_\gamma$
exist. To prove they are mutually inverse, it suffices to prove:
\begin{align} \overline {T}_\gamma \overline {S}_\gamma p &= p \end{align}
\begin{align} \overline {S}_\gamma \overline {T}_\gamma p' &= p' \end{align}
as
$p,p'$
are surjective. By commutativity of (34), this is equivalent to showing
$p' S_\gamma T_\gamma = p', pT_\gamma S_\gamma = p$
, or
$p'(S_\gamma T_\gamma - 1) = 0, p(T_\gamma S_\gamma - 1)= 0$
. It suffices to check this on generators, that is, on unoriented atoms. It is clear that
$S_\gamma T_\gamma = 1$
, however, we have
$T_\gamma S_\gamma \neq 1$
. The circumstances where this is the case is indicated schematically in Figure 5.
First, we consider the case in the first diagram of Figure 5. Let
$l$
be the displayed
$(\!\operatorname {ax}\!)$
link and let
$X$
be an unoriented atom of
$A$
. Then, by inspection of the figure, we have
$TS(X) - X \in I_l$
. Now, let
$l'$
denote the displayed cut link. There exists an unoriented atom
$X'$
such that
$X - X' \in I_{l'}$
and
$TS(X) - X' \in I_{l}$
. Hence,
$TS(X) - X = TS(X) - X' + X' - X \in I_{\pi }$
. This shows that
$p(T_\gamma S_\gamma - 1)(X)= 0$
.
Now, we consider the case in the second diagram of Figure 5. Let
$X$
be an unoriented atom of
$A \otimes B$
and denote the displayed tensor link by
$l$
. There exists an unoriented atom
$X'$
either of
$A$
or of
$B$
such that
$X - X' \in I_l$
. In either case, we have that
$X - TS(X) = X - X' \in I_l$
and so
$p(T_\gamma S_\gamma - 1)(X)= 0$
. The remaining cases are similar.
Corollary 4.7.
Let
$\gamma : \pi \longrightarrow \pi '$
be a reduction of proof structures. Then,
$I_{\pi '} = T_\gamma ^{-1}(I_\pi )$
or, identifying
$P_{\pi '}$
as a subring of
$P_\pi$
with inclusion
$T_\gamma$
,
\begin{equation} I_{\pi '} = I_\pi \cap P_{\pi '}\,. \end{equation}
Proof.
Proposition 4.6 shows that
$T_\gamma (I_{\pi '}) \subseteq I_{\pi }$
, so we have
$I_{\pi '} \subseteq T_\gamma ^{-1}(I_\pi )$
. If
$T_\gamma (\, f) \in I_\pi$
then by Lemma 4.5
$f = S_\gamma T_\gamma (\, f) \in S_\gamma ( I_\pi ) \subseteq I_{\pi '}$
giving the reverse inclusion.
It is not difficult to understand the effect of taking the quotient of
$P_\pi$
by the ideal
$I_\pi$
. All those unoriented atoms connected across links (in the sense that
$U - V$
appears in
$G_\pi$
) are identified in
$R_\pi$
with each other. This common image can be thought of as the path which connects all these differently named occurrences of the ‘same’ variable; such paths are sometimes called persistent paths (see Definition 4.12).
Understanding the composite
$TS$
.
Definition 4.8.
Let
$\pi$
be a proof structure and
$U, V \in U_\pi$
. We write
$U \sim V$
if
$U - V \in G_\pi$
or
$V - U \in G_\pi$
. Let
$\approx$
be the equivalence relation on
$U_\pi$
generated by
$\sim$
.
Lemma 4.9.
If
$U, V \in U_\pi$
, then we have
$U \approx V$
if and only if
$U - V \in I_\pi$
.
Proof.
If
$U \approx V$
, then clearly
$U - V \in I_\pi$
. If
$U - V \in I_\pi$
, then we can write
$U - V = \sum _j q_j ( U_j - V_j )$
with
$U_j - V_j \in G_\pi$
. Comparing the degrees of the left and right hand side,
$q_j$
may be assumed to be in
$k$
, and in fact in
$\{ 1, -1 \}$
. From this sum, we deduce a chain of
$U_j \sim V_j$
relations leading from
$V$
to
$U$
as claimed.
Lemma 4.10.
Let
$\gamma : \pi \longrightarrow \pi '$
be a reduction of proof structures. Then, if
$U, V \in U_{\pi '}$
have
$T_\gamma (U) \approx T_\gamma (V)$
in
$U_\pi$
if and only if
$U \approx V$
in
$U_{\pi '}$
.
Recall that we call a formula
$A$
labelling an edge incident at a conclusion of
$\pi$
a conclusion of
$\pi$
. If the sequence of oriented atoms of
$A$
is
$(U_1,u_1),\ldots ,(U_n,u_n)$
then we say that
$U_i$
is positive in
$A$
if
$u_i = +$
and otherwise it is negative.
Proposition 4.11.
Let
$\pi$
be a proof net with single conclusion
$A$
, and let
\begin{equation} (Z_1,z_1),\ldots ,(Z_n,z_n) \end{equation}
be the sequence of oriented atoms of
$A$
. Then
$n = 2m$
is even, there are an equal number of positive and negative atoms, and if
$\mathbf{U} = U_1,\ldots ,U_m$
denotes the subsequence of positive unoriented atoms and
$\mathbf{V} = V_1,\ldots ,V_m$
the subsequence of negative unoriented atoms then
-
(i) The inclusions
$k[\mathbf{U}] \longrightarrow P_\pi$
and
$k[\mathbf{V}] \longrightarrow P_\pi$
followed by the quotient
$P_\pi \longrightarrow R_\pi$
are isomorphisms
$\beta _+,\beta _-$
as in the diagram
(40) -
(ii) The composite
$\beta _-^{-1}\beta _+: k[\mathbf{U}] \longrightarrow k[\mathbf{V}]$
is
(41)for some permutation
\begin{equation} \beta _-^{-1}\beta _+(U_i) = V_{\sigma (i)},\quad 1 \leq i \leq m \end{equation}
$\sigma _\pi$
of
$\lbrace 1,\ldots , m \rbrace$
.
-
(iii) Each equivalence class of the relation
$\approx$
is the underlying set of a sequence
(42)where for some
\begin{equation} \mathscr{P} = ( Z_1, \ldots , Z_r ) \end{equation}
$1 \le i \le m$
, we have
$Z_1 = V_{\sigma (i)}, Z_r = U_i$
and
$Z_i \sim Z_{i+1}$
for
$1 \le i \lt r$
.
Proof.
We define the weight of a proof net
$\pi$
to be the sum, over all
$(\!\operatorname {cut}\!)$
links on some formula
$A, \neg A$
, of the weight
$|A|$
of
$A$
which is defined by recursively as follows: if
$A$
is an atomic proposition, then
$|A| = 1$
, if
with
then
$|A| = |B| + |C| + 1$
, and
$|\neg A| = |A|$
. Note that the weight of a proof net strictly decreases under cut-elimination.
We prove the proposition by induction on the weight. All statements can be treated one persistent path at a time by Lemma 4.10. In the base case, a persistent path proceeds from a negative unoriented atom
$V$
in the conclusion up through
$\otimes , \unicode{x214B}$
links to an
$(\!\operatorname {ax}\!)$
link and then downwards through
$\unicode{x214B}, \otimes$
links to the positive unoriented atom
$U$
in the conclusion. If the unoriented atoms involved are
$V = Z_1, \ldots , Z_r = U$
, then (40) is
where
$I = (Z_2 - Z_1, \ldots , Z_r - Z_{r-1})$
so it is clear that
$\beta _+, \beta _-$
are isomorphisms, and that
$\beta _-^{-1} \beta _+(U) = V$
is the map sending the end of each persistent path to its beginning, a permutation of the set of unoriented atoms in the conclusion.
For the inductive hypothesis, suppose the proposition is true of
$\pi '$
and that there is a reduction
$\gamma : \pi \longrightarrow \pi '$
. Note
$\pi '$
has the same conclusion as
$\pi$
. The claims follow from commutativity of the diagram
and a similar one for
$\mathbf{V}$
.
Definition 4.12.
Let
$\pi$
be a proof net with single conclusion
$A$
. The sequences
$\mathscr{P}$
of (
42
) whose underlying sets are the equivalence classes of
$\approx$
are called persistent paths.
Example 4.13.
The proof net
$\pi$
in Figure
6
is the canonical detour (6) of the introduction with
$B = A$
,
$\multimap$
written in terms of
$\unicode{x214B}$
and the multiple conclusions combined with
$\unicode{x214B}$
to a single conclusion. With
$A_i = A = (X,+)$
for
$1 \le i \le 12$
the set of unoriented atoms of
$\pi$
is a disjoint union of twelve copies of
$\{ X \}$
and we name the atoms
$X_1,\ldots ,X_{12}$
.
In the notation of the proposition,
$\mathbf{U} = \{ X_{12} \}, \mathbf{V} = \{ X_1 \}$
and the single persistent path of
$\pi$
is
$X_1, X_2, \ldots , X_{12}$
. Note that the persistent path goes ‘through’ the
$(\!\operatorname {cut}\!)$
link twice, once in each direction.
Remark 4.14.
By the definition of persistent paths, it follows from Proposition 4.6 that given any reduction
$\gamma : \pi \longrightarrow \pi '$
and persistent path of a proof structure
$\pi$
, there is an associated persistent path
$\mathscr{P}'$
in
$\pi '$
given by removing the variables which occur in
$\pi$
but not in
$\pi '$
from
$\mathscr{P}$
. This will be used in the proofs of Theorems
7.2
,
7.11
.
Definition 4.15.
A reduction sequence
$\Gamma : \pi \longrightarrow \pi '$
between proof structures
$\pi , \pi '$
is a nonempty sequence of reductions (Definition 4.3)
This induces a sequence of
$k$
-algebra morphisms
The canonical detour as a proof net, with
$A_i = A = (X, +)$
for all i.
the composite of which we denote by
$T_\Gamma : P_{\pi '} \longrightarrow P_{\pi }$
.
5. Elimination Theory
5.1 Buchberger’s algorithm
The Buchberger algorithm computes, given a generating sequence for an ideal
$I$
, a Gröbner basis for that ideal. There are a number of variations on this algorithm in the literature. We present here an optimisation of the algorithm of (Cox et al. Reference Cox, Little and O’Shea2015, §2.10 Theorem 9) for the purposes of Elimination Theory, using a form of Euclidean Division with ‘early stopping’ (Algorithm 1).
In this section,
$k$
is a field and
$k[X_1,\ldots ,X_n]$
a polynomial ring with a monomial order. We use the terminology of leading terms
$\operatorname {LT}$
, leading monomials
$\operatorname {LM}$
, leading coefficient
$\operatorname {LC}$
, and multidegree (Cox et al. Reference Cox, Little and O’Shea2015, §2).
Euclidean Division with Early Stopping.
Lemma 5.1.
Let
$G = (\,f_1,\ldots ,f_s)$
be a sequence of elements of
$k[X_1,\ldots ,X_n]$
. Given
$f \in k[X_1,\ldots ,X_n]$
let
$(q_1,\ldots ,q_s,r)$
be the output of Algorithm
1
. Then,
\begin{equation} f = q_1 f_1 + \cdots + q_s f_s + r \end{equation}
and if
$r \neq 0$
the leading term of
$r$
is not divisible by any
$\operatorname {LT}(\,f_i)$
with
$1 \le i \le s$
. Furthermore, if
$q_i f_i \neq 0$
, then
$\operatorname {multideg}(\, f) \ge \operatorname {multideg}(q_i f_i)$
.
Proof.
The expression
$f = \sum _{i=1}^s q_i f_i + p + r$
holds at the end of every iteration of the outer while loop, and it terminates with
$p = 0$
so (47) holds. If the algorithm returns
$r \neq 0$
, then it came from
$r \gets p$
with
$\operatorname {DivOcc} = \texttt {false}$
, so the claim about divisibility of
$\operatorname {LT}(r)$
follows. Termination and the other property follow as in the proof of the standard division algorithm (Cox et al. Reference Cox, Little and O’Shea2015, §2.3).
Definition 5.2.
Let
$G = (\,f_1,\ldots ,f_s)$
be a sequence of polynomials and
$f$
a polynomial. We denote by
$\operatorname {div}(\,f,G)$
(resp.
$\operatorname {div}_{es}(\,f,G)$
) the remainder
$r$
produced by the Euclidean division (resp. Algorithm
1
).
To state our variation of Buchberger’s algorithm, we need some notation. For
$i \neq j$
set
\begin{equation*} [i,j] = \begin{cases} (i,j) &\text{if } i \le j\\ (j,i) &\text{if } i \ge j \end{cases} \end{equation*}
Recall that the
$S$
-polynomial of
$g,h \in k[X_1,\ldots ,X_n]$
is
\begin{equation} S(g,h) := \frac {X^\gamma }{\operatorname {LT}(g)}g - \frac {X^\gamma }{\operatorname {LT}(h)}h\,. \end{equation}
where
$X^\gamma = \operatorname {LCM}(\!\operatorname{LM}(g),\operatorname {LM}\!(h))$
. The only significant difference between Algorithm 2 below and the form of Buchberger’s algorithm in (Cox et al. Reference Cox, Little and O’Shea2015, §2.10 Theorem 9) is that we replace the line
$S \gets \operatorname {div}(S(\,f_i,f_j),G)$
using normal Euclidean division with the line
$S \gets \operatorname {div}_{es}(S(\,f_i, f_j),G)$
using the division algorithm with early stopping. We also divide
$S$
by its leading coefficient
$\operatorname {LC}(S)$
before adding it to
$G$
, but this is insignificant.
Buchberger with Early Stopping.
Definition 5.3.
Given a set
$G = \{\,f_1, \ldots , f_s \}$
of polynomials we say that
$f$
reduces to zero modulo
$G$
, written
$f \longrightarrow _G 0$
if
$f$
can be written in the form
$f = a_1 f_1 + \cdots + a_s f_s$
such that whenever
$a_i f_i \neq 0$
we have
$\operatorname {multideg}(\, f) \ge \operatorname {multideg}(a_if_i)$
(see [Cox et al. Reference Cox, Little and O’Shea2015
, §2.9 Definition 1]).
Proposition 5.4. Algorithm 2 terminates and the output is a Gröbner basis.
Proof.
Algorithm 2 is a variation on (Cox et al. Reference Cox, Little and O’Shea2015, §2.10 Theorem 9) and the proof here is similar. Suppose that in some pass through the while loop,
$G$
is enlarged to
$G \cup \{\,f_t \}$
. By Lemma 5.1, we have that
$\operatorname {LT}(\,f_t)$
is not divisible by
$\operatorname {LT}(\, f)$
for any
$f \in G$
, and therefore,
$\langle \operatorname {LT}(G) \rangle$
is a proper subset of
$\langle \operatorname {LT}(G \cup \{\,f_t \}) \rangle$
. Since
$k[X_1,\ldots ,X_n]$
is Noetherian this means that at some point
$G$
stops growing, but then in each subsequent step the size of
$B$
decreases by one. Hence, the Algorithm terminates in finitely many steps.
To prove the output is a Gröbner basis, we first establish the following claim: at the end of every pass through the while loop,
$B$
has the property that if
$1 \le i \lt j \le t$
and
$(i,j) \notin B$
, then
\begin{equation} S(\,f_i, f_j) \longrightarrow _G 0 \quad \text{ or } \quad \operatorname {Criterion}\!(\,f_i, f_j, B) \text{ holds}\,. \end{equation}
This is initially true since
$B$
is the set of all possible pairs. To prove the claim, we need to argue that if it holds for
$B$
, then it continues to hold when
$B$
changes to
$B'$
.
To prove this, assume
$(i,j) \notin B'$
. If
$(i,j) \in B$
then
$B' = B \setminus \{(i,j)\}$
. In the step, before
$(i,j)$
is removed if either
$\operatorname{LCM}\!(\!\operatorname{LT}(\,f_i),\operatorname {LT}(\,f_j)) = \operatorname {LT}(\,f_i) \operatorname {LT}(\,f_j)$
or
$\operatorname {Criterion}\!(\,f_i,f_j,B)$
is true, then one argues as in the original proof from Cox, Little, and O’Shea (Reference Cox, Little and O’Shea2015). If not, then the algorithm computes
$S \gets \operatorname {div}_{es}(S(\,f_i,f_j), G,$
). If
$S = 0$
, then
$S(\,f_i,f_j) \longrightarrow _G 0$
by Lemma 5.1. If
$S \neq 0$
then we enlarge
$G$
to
$G' = G \cup \{ \frac {1}{\operatorname {LC}(S)} S \}$
. Examining the division algorithm with early stopping it clear that
$\operatorname {div}_{es}(S(\,f_i, f_j),G') = 0$
so
$S(\,f_i,f_j) \longrightarrow _{G'} 0$
and (49) holds for
$B',G'$
.
It remains to consider the case
$(i,j) \notin B$
. Then, (49) holds for
$B$
. Let
$G, G'$
be the state of the sequence of polynomials in the two steps, so
$G' = G$
or
$G'$
has one additional element. If
$S(\,f_i, f_j) \longrightarrow _G 0$
then
$S(\,f_i, f_j) \longrightarrow _{G'} 0$
. If
$\operatorname {Criterion}\!(\,f_i, f_j, B)$
holds then there is some
$k \in \{i,j\}$
with
$k \le |G|$
such that
$[i,k],[j,k]$
are not in
$B$
and
$\operatorname {LT}(\,f_k)$
divides
$\operatorname {LCM}(\!\operatorname{LT}(\,f_i),\operatorname {LT}(\,f_j))$
. Any new pairs in
$B'$
involve
$|G| + 1$
, so
$[i,k],[j,k] \notin B'$
and hence
$\operatorname {Criterion}\!(\,f_i,f_j,B')$
holds.
The argument that
$G$
is a Gröbner basis when
$B = \emptyset$
goes through as before.
Definition 5.5.
Given a sequence
$F = (\,f_1,\ldots ,f_s)$
of polynomials and a monomial order
$\lt$
on
$k[X_1,\ldots ,X_n]$
, we denote by
$\mathbb{B}_{es}(F, \lt )$
the output of Algorithm
2
.
We state the main theorem of Elimination Theory. Let
$\mathbf{X} = \{X_1,\ldots ,X_n\}$
and
$\mathbf{Y} = \{Y_1,\ldots ,Y_m\}$
be variables. We suppose given an ideal
$I \subseteq k[\mathbf{X}, \mathbf{Y}]$
and we are interested to know the equations between the
$\mathbf{X}$
-variables that are implied by the equations in
$I$
. We call this set of equations the elimination ideal:
Definition 5.6.
The elimination ideal of
$I$
is the ideal
$I \cap k[\mathbf{X}]$
in
$k[\mathbf{X}]$
.
In the situation of Section 2, we can think of the
$\mathbf{X}$
-variables as living at the ‘boundary’ of the proof net, and
$\mathbf{Y}$
as being the ‘interior’ variables.
Theorem 5.7 (The Elimination Theorem). Let
$I \subseteq k[\mathbf{X}, \mathbf{Y}]$
be an ideal and
$G$
a Gröbner basis of
$I$
with respect to a lexicographic order where
$X_i \lt Y_j$
for all
$1 \le i \le n, 1 \le j \le m$
. Then,
$G \cap k[\mathbf{X}]$
is a Gröbner basis for
$I \cap k[\mathbf{X}]$
.
Proof. See (Cox et al. Reference Cox, Little and O’Shea2015, §3.1 Theorem 2).
5.2 Buchberger and falling roofs
We introduce graphical notation for understanding the operation of Algorithm 2 on a simple class of ideals. Fix a polynomial ring
$k[X_1,\ldots ,X_n]$
, let
$\lt$
be a total order on the set
$\{X_1,\ldots ,X_n\}$
and take the lexicographic monomial order determined by
$\lt$
. Let
$\sigma$
be the permutation uniquely defined by
\begin{equation*} X_{\sigma ^{-1} 1} \lt X_{\sigma ^{-1} 2} \lt \cdots \lt X_{\sigma ^{-1} n}\,. \end{equation*}
The position of
$X_i$
in this sequence is
$\sigma (i)$
. We view
$\sigma$
as assigning a height to variables:
Definition 5.8.
The realisation of
$\lt$
is the oriented graph
$\mathscr{R}_\lt$
with vertices
\begin{equation} \big \{(i, \sigma i) \,|\, 1 \le i \le n \big \} \subseteq \mathbb{R}^2 \end{equation}
with an edge between
$(i, \sigma i), (i+1, \sigma (i+1))$
for
$i \lt n$
, and
$(i, \sigma i)$
decorated with
$X_i$
. The orientation of the edge is from
$(i, \sigma i)$
to
$(j, \sigma j)$
if
$X_i \lt X_j$
.
Definition 5.9.
A
$\lt$
-graph is an oriented graph on the vertex set (
50
) with the property that if there is an edge from a vertex
$(i, \sigma i)$
decorated with
$X_i$
to a vertex decorated with
$X_j$
then
$X_i \lt X_j$
.
Definition 5.10.
A
$\lt$
-graph is linear if every vertex has valence at most two.
Clearly,
$\mathscr{R}_{\lt }$
is a linear
$\lt$
-graph. In this section, we simply write graph for
$\lt$
-graph, since the ordering
$\lt$
on the variables is fixed. We write
$e: X_i \longrightarrow X_j$
for an edge from a vertex decorated with
$X_i$
to a vertex decorated with
$X_j$
.
Example 5.11.
Let
$X_1, \ldots , X_6$
be ordered by
$X_5 \lt X_1 \lt X_6 \lt X_3 \lt X_2 \lt X_4$
. Then
$\mathscr{R}_\lt$
is
Remark 5.12.
The realisation involves two orderings on the variables: the order reading along the
$x$
-axis (the
$X_1,\ldots ,X_n$
order) and the order reading along the
$y$
-axis (the
$\lt$
-order). The realisation is a graphical presentation of the relation between these orders.
Definition 5.13.
A roof in a graph
$\mathscr{S}$
is an ordered pair
$(e,e')$
of edges
$e: X_i \longrightarrow X_l, e': X_k \longrightarrow X_l$
with the same endpoint
$X_l$
and
$X_i \lt X_k$
. We call
$X_l$
the tip of the roof.
Definition 5.14.
Given a graph
$\mathscr{S}$
, we define
\begin{equation*} G_{\mathscr{S}} = \big \{ X_j - X_i \,|\, e: X_i \longrightarrow X_j \text{ is an edge in } \mathscr{S} \big \}\,. \end{equation*}
Definition 5.15.
Let
$\mathscr{S}$
be a graph with edges
$e: X_i \longrightarrow X_j, e': X_k \longrightarrow X_l$
. Then,
$e \lt e'$
if the pair
$(X_j, X_i)$
precedes
$(X_l, X_k)$
lexicographically, that is, either
$X_j \lt X_l$
or
$X_j = X_l$
and
$X_i \lt X_k$
. This is a total order on the set of edges of
$\mathscr{S}$
.
The map sending
$e: X_i \longrightarrow X_j$
to
$X_j - X_i$
is a bijection between the edge set of
$\mathscr{S}$
and
$G_{\mathscr{S}}$
and we give the latter set the total order induced by this bijection and the total order on the former set just defined.
Definition 5.16.
A roof
$(e,e')$
precedes a roof
$(d, d')$
if
$e \lt d$
or
$e = d$
and
$e' \lt d'$
.
We will only consider roofs in linear graphs: since in a linear graph distinct roofs have distinct tips,
$(e,e') \lt (d,d')$
simply means that
$e \lt d$
, or what is the same, the tip of the first roof is lower in the realisation than the tip of the second.
We now explain the operation of Algorithm 2 on input
$(G_{\mathscr{S}}, \lt )$
for a linear graph
$\mathscr{S}$
by giving an ‘isomorphic’ algorithm (Algorithm 3 below), which is organised around roofs and is easier to understand. The algorithm works by marking a subset of edges in a graph
$\mathscr{N}\ $
derived from
$\mathscr{S}$
as dead (an edge i.e., not dead is live). A roof is live if both the edges in it are live. We indicate dead edges diagrammatically by dotted lines.
Falling Roofs.
Proposition 5.17.
For any linear graph
$\mathscr{S}$
:
-
(i) Algorithm 3 terminates.
-
(ii) At every step,
$\mathscr{N}\ $
is a graph and the subgraph of live edges in
$\mathscr{N}\ $
is linear.
-
(iii) If the output of of Algorithm 2 on input
$(G_{\mathscr{S}}, \lt )$
is
$G$
and the output of Algorithm
3
on input
$\mathscr{S}$
is
$\mathscr{N}\ $
then
$G = G_{\mathscr{N}}$
.
Proof.
Given an edge
$e: X_i \longrightarrow X_j$
, we write
$f_e$
for
$X_j - X_i$
. We prove (iii) and along the way (i), (ii) by stepping through Algorithm 2 on input
$G_{\mathscr{S}}$
(with intermediate variables
$G,B,S$
) and Algorithm 3 on input
$\mathscr{S}$
(with intermediate variable
$\mathscr{N}\ $
). At each step, let
$B_{rel} \subseteq B$
denote the set of pairs
$(e,e')$
which are relevant in the sense that
\begin{equation*} \operatorname {LCM}\!(\!\operatorname{LM}\!(\,f_e), \operatorname {LM}(\,f_{e'})) \neq \operatorname {LM}(\,f_e) \operatorname {LM}(\,f_{e'}) \textbf { and } \operatorname {Criterion}\!(\,f_e, f_{e'}, B) \textbf { is false}\,. \end{equation*}
We will prove by induction on the number of steps through Algorithm 2 that at each step the following proposition
$\textbf {IP}$
holds:
-
IP:
$\mathscr{N}\ $
is a graph, the live edges in
$\mathscr{N}\ $
form a linear graph, no dead edge in
$\mathscr{N}\ $
ends where a live edge begins,
$G = G_{\mathscr{N}}$
, and
$B_{rel}$
is the set of live roofs in
$\mathscr{N}\ $
.
It is clear that these conditions are all initially true, except perhaps the last claim about
$B_{rel}$
. To examine this condition at the beginning of the algorithm, let
$e: X_i \longrightarrow X_j$
and
$e': X_k \longrightarrow X_l$
be edges in
$\mathscr{N} = \mathscr{S}$
. Then
$\operatorname {LT}\!(\,f_{e}) = X_j, \operatorname {LT}\!(\,f_{e'}) = X_l$
and
\begin{equation*} \operatorname {LCM}\!(\!\operatorname{LM}\!(\,f_e), \operatorname{LM}\!(\,f_{e'})) = \operatorname {LCM}\!(X_j, X_l) = \begin{cases} X_j X_l & X_j \neq X_l \\ X_j & X_j = X_l \end{cases} \end{equation*}
so,
$\operatorname {LCM}(\!\operatorname{LM}(\,f_e), \operatorname {LM}(\,f_{e'})) \neq \operatorname {LM}(\,f_e) \operatorname {LM}(\,f_{e'})$
if and only if
$X_j = X_l$
, that is, if and only if
$e, e'$
have a common endpoint in
$\mathscr{N}\ $
. Suppose this is the case. Then,
$\operatorname {Criterion}\!(\,f_e, f_{e'}, B)$
is true if there exists some edge
$e'' \notin \{ e, e'\}$
for which
$[e,e''], [e',e'']$
are not in
$B$
and the edges
$e, e', e''$
all have the same endpoint. But since
$\mathscr{N}\ $
is linear this is impossible, so the criterion is false. Hence, a pair
$(e,e')$
is in
$B_{rel}$
if and only if it is a roof in
$\mathscr{S}$
, and since initially all roofs are live this proves the claim.
Suppose that IP is true up to some step of the outer while loops of the two algorithms. Let
$\mathscr{N}_0$
denote the state of
$\mathscr{N}\ $
at the beginning of this step of Algorithm 3. Algorithm 2 looks in order through pairs
$(e,e')$
for one that is relevant, or what is the same by the inductive hypothesis, for a live roof in
$\mathscr{N}\ $
. Let
$(e,e')$
be a live roof with
$e: X_i \longrightarrow X_j, e': X_k \longrightarrow X_j$
. Algorithm 2 computes the
$S$
-polynomial
\begin{equation} S := S(\,f_e, f_{e'}) = f_e - f_{e'} = X_k - X_i \end{equation}
which is
$f_d$
for
$d: X_i \longrightarrow X_k$
in Algorithm 3. The next step of Algorithm 2 is to compute
$\operatorname {div}_{es}(S,G)$
. By IP, we have
$G = G_{\mathscr{N}}$
. A polynomial in
$G$
with leading term
$X_k$
is an edge in
$\mathscr{N}\ $
ending at
$X_k$
, which must be live by IP as
$e'$
was live. If there is no polynomial in
$G$
with leading term
$X_k$
, then the division algorithm (with early stopping) returns
$S$
,
$\frac {1}{\operatorname {LC}(S)} S$
is added to
$G$
,
$d$
is added to
$\mathscr{N}\ $
,
$e,e'$
are marked as dead and the step is complete. It is straightforward to check that IP still holds.
Otherwise there is a polynomial
$f$
in
$G$
with leading term
$X_k$
. If
$f = S$
, then
$\operatorname {div}_{es}(S,G) = 0$
so nothing is added to
$G$
by Algorithm 2, nothing is added to
$\mathscr{N}\ $
by Algorithm 3 and the step is complete; again IP still holds. We are left with the case where
$f \neq S$
exists in
$G$
with leading term
$X_k$
. For this, we analyse the inner while loop in Algorithm 3. The key observations are that at the beginning of each step of this inner loop:
-
(a)
$d$
is part of at most one live roof in
$\mathscr{N}\ $
. -
(b) there is no dead edge in
$\mathscr{N}\ $
ending where
$d$
ends.
Both claims are true for the initial
$d$
by IP. We call
$d$
Type
$1$
if it comes from
$d'$
in (53) and Type
$2$
if it comes from
$d'$
in (54). If
$d$
is Type
$1$
both claims (a),(b) follow from IP. In Type
$2$
, we have to analyse the previous steps; if the previous step was Type
$2$
(or there was no previous step) then there is a live edge in
$\mathscr{N}_0$
beginning where
$d$
ends and from this we deduce (a),(b). Otherwise there are some Type
$1$
steps intervening between the current step and the most recent Type
$2$
step (or the original roof (52) if there are no previous Type
$2$
steps). However, in Type
$1$
, steps the
$d,d'$
edges start from the same vertex, so the most recent Type
$2$
step (or original roof) provides a live edge beginning where
$d$
ends, from which we deduce (a),(b) again from IP.
We now prove that the inner while loop of Algorithm 3 aligns with the division step of Algorithm 2. By (a), there is a unique polynomial
$f = f_{e''}$
in
$G$
with the same leading term as
$f_d$
. The division algorithm replaces
$S = f_d$
by the dividend
\begin{equation} S \leftarrow S - \!(\!\operatorname{LT}\!(S)/\operatorname {LT}\!(\,f_{e''})) f_{e''} = f_d - f_{e''} = \pm f_{d'} \end{equation}
There are two cases, corresponding to the two if statements in Algorithm 3. In the first case,
$f_{d'} = S$
, and in the second,
$f_{d'} = -S$
.
If
$f_{d'} \in G$
, then by linearity of
$\mathscr{N}_0$
and (b) there is no other polynomial in
$G$
with the same leading term as
$f_{d'}$
and so the division algorithm returns zero. Likewise, the inner while loop of Algorithm 3 terminates because there is no live roof involving
$d'$
. To prove IP note that the only changes to
$\mathscr{N}\ $
during the inner while loop are to mark some edges as dead. Marking the
$e''$
as dead does not change the set of live roofs by (a).
If
$f_{d'} \notin G$
then by (b) the leading term of
$f_{d'}$
is the same as the leading term of some element of
$G$
(i.e.,, division continues) if and only if
$d'$
is part of a live roof in
$\mathscr{N}\ $
(i.e.,, the inner while loop continues). If division and the while loop both stop, then
$f_{d'} = \frac {1}{\operatorname {LC}S} S$
is added to
$G$
and
$d'$
is added to
$\mathscr{N}\ $
. As before one can check that IP is still true. Otherwise the division and while loop continue, and we repeat the above analysis. This completes the proof of the inductive step, showing that IP holds in the next iteration of the outer while loop and so (iii) follows by induction.
(i) Algorithm 2 terminates when
$B$
is empty, at which step
$B_{rel}$
must be empty and so there are no live roofs in
$\mathscr{N}\ $
so Algorithm 3 also terminates.
Figure 7 shows the Falling Roofs algorithm applied to the graph of Example 5.11.
Corollary 5.18.
If
$\mathscr{S}$
is a linear graph and
$\mathscr{N}\ $
is the output of Algorithm
3
on
$\mathscr{S}$
, then
$G_{\mathscr{N}}$
is a Gröbner basis for the ideal generated by
$G_{\mathscr{S}}$
.
Examining the algorithm, it is easy to verify the following:
Lemma 5.19.
Let
$\mathscr{S}$
be a linear graph and
$\mathscr{N}\ $
the output of Algorithm
3
on
$\mathscr{S}$
. If a vertex has valence one in
$\mathscr{S}$
then it is incident with precisely one live edge in
$\mathscr{N}\ $
.
5.3 Falling roofs and elimination
We consider the Falling Roofs algorithm (Algorithm 3) in the context of Elimination Theory. Let
$\mathbf{Z} = \{Z_1,\ldots ,Z_r\}$
be a set of variables and
$\lt$
a total order on
$\mathbf{Z}$
. We denote the associated lexicographic monomial order also by
$\lt$
. We assume that given a partition
$\mathbf{Z} = \mathbf{X} \cup \mathbf{Y}$
such that if
$Z_i \in \mathbf{X}$
and
$Z_j \in \mathbf{Y}$
then
$Z_i \lt Z_j$
. That is, the
$\mathbf{X}$
-variables are ‘low’ and the
$\mathbf{Y}$
-variables are ‘high’. Let
$\mathscr{S}\ $
be a linear
$\lt$
-graph with associated ideal
\begin{equation*} I = \langle G_{\mathscr{S}}\rangle \subseteq k[\mathbf{X},\mathbf{Y}]\,. \end{equation*}
Let
$\mathscr{N}\ $
be the output of the Falling Roofs algorithm on
$\mathscr{S}$
. Then, by Corollary 5.18,
$G_{\mathscr{N}}\ $
is a Gröbner basis for
$I$
and hence by the Elimination Theorem (Theorem 5.7)
\begin{equation*} G_{\mathscr{N}}\ \cap k[\mathbf{X}] \text{ is a Gr}\unicode{x00F6}\text{bner basis for } I \cap k[\mathbf{X}]\,. \end{equation*}
If we write
$X_1,\ldots ,X_n$
for the variables in
$\mathbf{X}$
and similarly
$Y_1,\ldots ,Y_m$
for the variables in
$\mathbf{Y}$
then
$G_{\mathscr{N}}\ \cap k[\mathbf{X}]$
is simply all the polynomials
$f_e = X_j - X_i$
where
$e: X_i \longrightarrow X_j$
is an edge in
$\mathscr{N}\ $
between
$\mathbf{X}$
-variables, that is, we delete any edges involving
$\mathbf{Y}$
-variables. This has a natural interpretation as ‘cutting off the top’ of the realisation: If we draw a line through the realisation at the height of the highest
$\mathbf{X}$
-variable, intersecting with
$k[\mathbf{X}]$
means deleting any vertices above the line and all edges incident with such vertices.
Example 5.20.
In Example 5.11
, take
$\mathbf{X} = \{ X_1, X_5, X_6 \}$
and
$\mathbf{Y} = \{ X_2, X_3, X_4 \}$
. Then, the set
$G_{\mathscr{N}}\ \cap k[\mathbf{X}]$
is a Gröbner basis for
$I \cap k[\mathbf{X}]$
where
$G_{\mathscr{N}}\ \cap k[\mathbf{X}] = \{ X_6 - X_5, X_1 - X_5 \}$
is determined by the subgraph in the box below:
Note that we follow the notational convention introduced just prior to Proposition 5.17
, of denoting some edges of
$\mathscr{N}\ $
with solid lines (the live edges) and some with dotted lines (the dead) edges. Shown is the state of these labels at the end of the algorithm. These are all edges of
$\mathscr{N}\ $
and so for example
$X_3 - X_1 \in G_{\mathscr{N}}$
.
We assume
$X_1,\ldots ,X_n$
is the order these variables appear in the list
$Z_1,\ldots ,Z_r$
, that is, the order the
$\mathbf{X}$
-variables are enumerated is their order of appearance from left to right in the realisation (which is not necessarily the
$\lt$
order).
Proposition 5.21.
Suppose that
$\mathscr{S}$
is a subgraph of the realisation
$\mathscr{R}_{\lt }$
satisfying the following conditions
-
(i) Every vertex in
$\mathscr{S}$
of valence one is labelled with an element from
$\mathbf{X}$
. -
(ii) We have
$X_1 \lt X_2 \lt \cdots \lt X_n$
.
Let
$\mathscr{N}^{\ \, +}$
denote the subgraph of live edges in
$\mathscr{N}\ $
. Then,
$\mathscr{N\ }^{\ \, +}$
is a linear graph, every vertex of nonzero valence in
$\mathscr{N\ }^{\ \, +}$
is labelled with an element of
$\mathbf{X}$
, and
$G_{\mathscr{N\ }^{\ \, +}} = G_{\mathscr{N}}\ \cap k[\mathbf{X}]$
is a Gröbner basis for
$I \cap k[\mathbf{X}]$
.
Proof.
By Proposition 5.17(ii), the graph
$\mathscr{N\ }^{\ \, +}$
is linear and by construction it contains no roofs. Suppose there were a vertex with nonzero valence in
$\mathscr{N\ }^{\ \, +}$
labelled by
$Y \in \mathbf{Y}$
. By examination of the Falling Roofs algorithm, it is easy to see that
$Y$
must have had nonzero valence in
$\mathscr{S}$
. It belongs to a connected component of
$\mathscr{S}$
of the form
where
$Z_{i_1}, Z_{i_l} \in \mathbf{X}$
by (i). By Lemma 5.19, the vertices
$Z_{i_1}, Z_{i_l}$
have valence one in
$\mathscr{N\ }^{\ \, +}$
and again by examining the algorithm, we can see that
$Y$
is still connected to these vertices in
$\mathscr{N\ }^{\ \, +}$
(one proves by induction that if two vertices connected by an unoriented path in
$\mathscr{S}$
have nonzero valence in
$\mathscr{N\ }^{\ \, +}$
then they are still connected by an unoriented path in
$\mathscr{N\ }^{\ \, +}$
). That is, we have also in
$\mathscr{N\ }^{\ \, +}$
a connected component that looks like (57).
Now, we invoke a discrete version of Rolle’s theorem: since (57) starts low (at
$Z_{i_1}$
) ends low (at
$Z_{i_l}$
) and is high somewhere in between (at
$Y$
) it must have a local maxima (i.e.,, a roof) as is easily proven by induction. But this contradicts the non-existence of live roofs in
$\mathscr{N}\ $
. Hence, all vertices with nonzero valence in
$\mathscr{N\ }^{\ \, +}$
are labelled by
$\mathbf{X}$
.
For the last statement, since
$G_{\mathscr{N}}\ \cap k[\mathbf{X}]$
is a Gröbner basis for
$I \cap k[\mathbf{X}]$
, it suffices for the last claim to prove that
\begin{equation} G_{\mathscr{N\ }^{\ \, +}} = G_{\mathscr{N}}\ \cap k[\mathbf{X}]\,. \end{equation}
Suppose
$f \in G_{\mathscr{N}}\ \cap k[\mathbf{X}]$
is
$f = f_e$
for an edge
$e: X_i \longrightarrow X_j$
which is not live. In the Falling Roofs algorithm, the only way
$e$
can be marked as dead is if at some point during the algorithm there are two live edges with target
$X_j$
. Since by hypothesis every
$\mathbf{Y}$
variable is greater in the
$\lt$
-order than every
$\mathbf{X}$
variable, the source of both of these edges with target
$X_j$
must be in
$\mathbf{X}$
. But this is impossible by (ii). This contradiction proves (58).
6. Monomial Orders
Let
$\pi$
be a proof net with single conclusion
$A$
. We learned in Proposition 4.11 that the variables of
$P_\pi$
may be organised into sequences called persistent paths. It is natural to use these sequences to define a monomial order on
$P_\pi$
. Let
\begin{equation} \mathscr{P}_1,\ldots ,\mathscr{P}_m \end{equation}
be the persistent paths of
$\pi$
ordered so that if
$U_i$
is the last unoriented atom in
$\mathscr{P}_i$
, then
$U_1, \ldots , U_m$
is the order that these atoms appear in
$A$
. Let us name the variables
$X_i$
so that (59) is
$X_1, \ldots , X_n$
and
$P_\pi = k[X_1,\ldots ,X_n]$
.
Definition 6.1.
We write
$U \lt _0 V$
if
$U$
is before
$V$
in (
59
). The monomial order
$\lt _0$
on
$P_\pi$
is the lexicographic order determined by
$\lt _0$
on the variables.
In this section, the monomial order on
$P_\pi$
is
$\lt _0$
.
Lemma 6.2.
If
$f,g$
are distinct elements of
$G_\pi$
then
$\operatorname{LM}\!(\, f) \neq \operatorname {LM}\!(g)$
, where leading monomials are defined with respect to
$\lt _0$
.
Recall the relation
$\sim$
on the set
$U_\pi$
of unoriented atoms of
$\pi$
, which generates the equivalence relation
$\approx$
whose equivalence classes are persistent paths. We have
$U \sim V$
if
$U,V$
appear next to each other on a persistent path.
Definition 6.3.
Let
$\mathscr{S}_0$
be the oriented graph with vertex set
$U_\pi$
where two variables
$U, V \in U_\pi$
are connected by an edge
$e: U \longrightarrow V$
if
$U \sim V$
and
$U \lt _0 V$
.
In the terminology of Section 5.2, this is a linear
$\lt _0$
-graph. This is a subgraph of the realisation
$\mathscr{R}_{\lt _0}$
.
Definition 6.4.
We denote by
$G^{(0)}_\pi$
the ordered set of polynomials
$G_{\mathscr{S}_0}$
of Definition 5.14
,
\begin{equation} G^{(0)}_\pi = \{ V - U \,|\, e: U \longrightarrow V \text{ is an edge in } \mathscr{S}_0 \}\,. \end{equation}
Up to signs,
$G^{(0)}_\pi$
is just
$G_\pi$
.
Lemma 6.5.
If
$f,g$
are distinct elements of
$G = G^{(0)}_\pi$
, then
$S(\,f,g) \longrightarrow _G 0$
.
Proof.
Suppose
$f = X - X', g = Y - Y'$
. By Lemma 6.2, we may assume
$X \gt _0 Y$
. Then,
\begin{align*} S(\,f,g) &= \frac {XY}{X}(X - X') - \frac {XY}{Y}(Y - Y')\\[5pt] &= Y(X - X') - X(Y - Y')\\[5pt] &= XY' - X'Y \end{align*}
Hence,
$\operatorname {LT}(S(\,f,g)) = XY'$
. Rearranging
\begin{align*} &= Y'( X - X' ) - X'( Y - Y' )\\[5pt] &= Y'f - X' g \end{align*}
and
$\operatorname {LT}\!(Y'f) = XY'$
,
$\operatorname {LT}\!(X'g) = X'Y \lt XY'$
so
$S(\,f,g) \longrightarrow _G 0$
.
Proposition 6.6.
$G^{(0)}_\pi$
is a minimal Gröbner basis for
$I_\pi$
with respect to
$\lt _0$
.
Proof.
To prove
$G = G^{(0)}_\pi$
is a Gröbner basis, we need to (by (Cox et al. Reference Cox, Little and O’Shea2015, §2.9 Theorem 3)) prove that
$S(\,f,g) \longrightarrow _G 0$
for distinct elements
$f,g \in G$
. But this is Lemma 6.5. To prove
$G$
is a minimal Gröbner basis, we can treat each persistent path
$\mathscr{P} = X_1, \ldots , X_r$
separately. The part of
$G$
associated to
$\mathscr{P}$
is
$\{ X_{i+1} - X_i \}_{i=1}^{r-1}$
. With
$f = X_{i+1} - X_i$
, it is clear that
$\operatorname {LC}(\, f) = 1$
and
$\langle \operatorname {LT}(G \setminus \{\,f \}) \rangle = \langle X_2, \ldots , X_{i}, X_{i+2}, \ldots , X_r \rangle$
, which does not contain
$\operatorname {LT}(\, f)$
.
Corollary 6.7.
$G_\pi$
is a Gröbner basis for
$I_\pi$
.
Remark 6.8.
While
$G^{(0)}_\pi$
is minimal, it is not the reduced Gröbner basis of
$I_\pi$
as soon as there is a persistent path with more than two variables in
$\pi$
. The reduced Gröbner basis for
$I_\pi$
is the union, over all persistent paths
$\mathscr{P}$
in the above notation, of
$X_2 - X_1, \ldots , X_i - X_1, \ldots , X_r - X_1$
.
6.1 Reduction and monomial orders
In this section,
$\Gamma : \pi \longrightarrow \pi '$
is a reduction sequence between proof nets with single conclusion
$A$
. Let
$\mathscr{P}_1,\ldots ,\mathscr{P}_m$
denote the persistent paths of
$\pi$
ordered as in (59) and let us name the variables
$X_i$
so that
$\mathscr{P}_1,\ldots ,\mathscr{P}_m$
is
$X_1, \ldots , X_n$
and
$P_\pi = k[X_1,\ldots ,X_n]$
. That is, we name the variables according to their
$\lt _0$
-order.
Let
$\mathscr{Q}_i$
be the subsequence of
$\mathscr{P}_i$
consisting just of those unoriented atoms in
$\pi '$
(those in the image of
$T_\Gamma$
) so that
$\mathscr{Q}_1, \ldots , \mathscr{Q}_m$
is a partition of the unoriented atoms of
$\pi '$
. Let
$\mathscr{P}_i \setminus \mathscr{Q}_i$
denote the complement of the subsequence
$\mathscr{Q}_i$
. Then,
\begin{equation} \mathscr{Q}_1, \ldots , \mathscr{Q}_m, \mathscr{P}_1 \setminus \mathscr{Q}_1,\ldots ,\mathscr{P}_m \setminus \mathscr{Q}_m \end{equation}
is the set of unoriented atoms of
$\pi$
arranged in an order that depends on the reduction
$\Gamma$
. Note that
$\mathscr{P}_i \setminus \mathscr{Q}_i$
are the variables in
$\mathscr{P}_i$
eliminated during the reduction sequence.
Definition 6.9.
We write
$U \lt _\Gamma V$
if
$U$
is before
$V$
in (
61
), reading from left to right. The monomial order
$\lt _\Gamma$
on
$P_\pi$
is the lexicographic order determined by
$\lt _\Gamma$
on the variables.
From the point of view of the realisation
$\mathscr{R}_{\lt _\Gamma }$
of Section 5.2, the order
$\lt _\Gamma$
‘lifts’ the variables in
$P_\pi$
that are to be eliminated above those that persist in
$P_{\pi '}$
. Observe that this realisation refers to the relation between
$\lt _0$
and
$\lt _\Gamma$
(Remark 5.12).
Definition 6.10.
Let
$\mathscr{S}_\Gamma$
be the oriented graph with vertex set
$U_\pi$
, where two variables
$U, V \in U_\pi$
are connected by an edge
$e: U \longrightarrow V$
if
$U \sim V$
and
$U \lt _\Gamma V$
.
In the terminology of Section 5.2, this is a linear
$\lt _\Gamma$
-graph, which is a subgraph of the realisation
$\mathscr{R}_{\lt _\Gamma }$
. Note that the connected components of
$\mathscr{S}_\Gamma$
correspond to persistent paths, since unoriented atoms in different persistent paths are not related by
$\sim$
.
Definition 6.11.
Let
$G^{(\Gamma )}_\pi$
be the ordered set of polynomials
$G_{\mathscr{S}_\Gamma }$
of Definition 5.14
,
\begin{equation} G^{(\Gamma )}_\pi = \big \{ V - U \,|\, e: U \longrightarrow V \text{ is an edge in } \mathscr{S}_\Gamma \big \}\,. \end{equation}
Example 6.12.
Let
$\gamma$
be the reduction of the
$m$
-redex of the canonical detour
$\pi$
in Example 4.13
. The sequence (
61
) is
\begin{equation*} \mathscr{Q}, \underline {\mathscr{P} \setminus \mathscr{Q}} = X_1, X_2, X_3, X_6, X_7, X_{10}, X_{11}, X_{12}, \underline {X_4, X_5, X_8, X_9} \end{equation*}
where we underline the atoms in
$\mathscr{P} \setminus \mathscr{Q}$
for the reader’s convenience. The graph
$\mathscr{S}_\gamma$
is shown in Figure
8
.
The sequence
$G^{(\gamma )}_\pi$
is
\begin{align*} & X_2 - X_1, X_3 - X_2, X_7 - X_6, X_{11} - X_{10}, X_{12} - X_{11},\\ &\qquad X_4 - X_3, X_5 - X_6, X_5 - X_4, X_8 - X_7, X_9 - X_{10}, X_9 - X_8\,. \end{align*}
Note that the persistent path
$\mathscr{P}$
passes through the
$(\!\operatorname {cut}\!)$
link twice, which we can see clearly if we underline the atoms in
$\mathscr{P} \setminus \mathscr{Q}$
:
\begin{equation} X_1, X_2, X_3, \underline {X_4}, \underline {X_5}, X_6, X_7, \underline {X_8}, \underline {X_9}, X_{10}, X_{11}, X_{12}\,. \end{equation}
Each pass contributes two consecutive unoriented atoms in
$\mathscr{P} \setminus \mathscr{Q}$
. Note that the sequence (
63
), in which the atoms are ordered by appearance in the persistent path, is
$\lt _\gamma$
increasing except at two points of ‘defect’ where the path exits an edge incident at a
$(\!\operatorname {cut}\!)$
link:
\begin{equation} X_1 \lt _\gamma X_2 \lt _\gamma X_3 \lt _\gamma \underline {X_4} \lt _\gamma \underline {X_5} \gt _\gamma X_6 \lt _\gamma X_7 \lt _\gamma \underline {X_8} \lt _\gamma \underline {X_9} \gt _\gamma X_{10} \lt _\gamma X_{11} \lt _\gamma X_{12}\,. \end{equation}
These are of course the roofs in
$\mathscr{S}_{\gamma }$
.
Lemma 6.13.
$G^{(\Gamma )}_\pi$
is not a Gröbner basis for
$I_\pi$
with respect to
$\lt _\Gamma$
.
From this, it is also clear that
$G_\pi$
is not a Gröbner basis with respect to
$\lt _\Gamma$
.
Remark 6.14.
The definition of the monomial orders
$\lt _0, \lt _\Gamma$
involves ordering the persistent paths by the order of appearance of their last unoriented atom in
$A$
. This order could be chosen arbitrarily without changing our results; some choice must be made and this one appears relatively natural. The ordering on the persistent paths matters insofar as the Falling Roofs algorithm chooses roofs in earlier persistent paths before later ones.
The graph
$\mathscr{S}_\gamma$
for the canonical detour of Example 4.13.
7. Main Theorems
Let
$\pi$
be a proof net with single conclusion
$A$
. We wrote informally in Section 2 about how the structure of
$\pi$
implicitly defines a relationship between unoriented atoms on the ‘boundary’ of the proof net, and how computation is the process of making this implicit relationship explicit. Let us now make these comments more precise.
Let
$\mathbf{U}$
be the subsequence of positive unoriented atoms in
$A$
, and
$\mathbf{V}$
the subsequence of negative unoriented atoms in
$A$
. The composite
\begin{equation} k[\mathbf{U},\mathbf{V}] \longrightarrow P_\pi \longrightarrow P_\pi /I_\pi \end{equation}
is by Proposition 4.11 a surjective morphism of
$k$
-algebras, and we denote by
$I_{\partial \pi }$
the ideal which is its kernel. There is a commutative diagram
By Proposition 4.11(iii)
\begin{equation} I_{\partial \pi } = \big \langle \{ U_i - V_{\sigma i} \}_i \big \rangle \end{equation}
for a permutation
$\sigma$
, which contains the structural information of the normal form of
$\pi$
(see Appendix A). The structure of
$\pi$
, as represented say by the generating set
$G_\pi$
for the ideal
$I_\pi$
, contains the same information but in an implicit form; the computational process of reduction of
$\pi$
to normal form may thus be identified with a process of discovering the generating set
$\{ U_i - V_{\sigma i} \}_i$
for
$I_{\partial \pi }$
from the generating set
$G_\pi$
for
$I_\pi$
.
There are many such processes: indeed, we can now sketch a machine for generating them. Let
$\lt$
be a total order on the set of unoriented atoms in
$\pi$
\begin{equation*} U_\pi = \mathbf{U} \sqcup \mathbf{V} \sqcup \mathbf{W} \text{ with } \mathbf{V} \lt \mathbf{U} \lt \mathbf{W} \end{equation*}
in the sense that for any
$i,j,k$
, we have
$V_i \lt U_j \lt W_k$
. Let
$\mathscr{S} = \mathscr{S}_{\lt }$
denote the graph (see Section 6) with an edge
$X \longrightarrow X'$
if
$X \sim X'$
and
$X \lt X'$
. Then,
$G_{\mathscr{S}}$
is, up to signs, the generating set
$G_\pi$
of
$I_\pi$
. As our computational process we take the Buchberger Algorithm with Early Stopping applied to
$G_{\mathscr{S}}$
, or what is the same, the Falling Roofs algorithm applied to
$\mathscr{S}$
. These algorithms return
$G_{\mathscr{N}}\ $
and
$\mathscr{N}\ $
, respectively, (Proposition 5.17). Let
$\mathscr{N\ }^{\ \, +}$
be the subgraph of live edges in
$\mathscr{N}\ $
.
Theorem 7.1.
$G_{\mathscr{N\ }^{\ \, +}} = \big \{ U_i - V_{\sigma i} \big \}_i$
is a Gröbner basis for
$I_{\partial \pi }$
.
Proof.
The graph
$\mathscr{S}$
satisfies the hypotheses of Proposition 5.21 with
$\mathbf{X} = \mathbf{V} \cup \mathbf{U}$
, so the subgraph
$\mathscr{N\ }^{\ \, +}$
of live edges in
$\mathscr{N}\ $
satisfies that
$G_{\mathscr{N\ }^{\ \, +}} = G_{\mathscr{N}}\ \cap k[\mathbf{U}, \mathbf{V}]$
is a Gröbner basis of
$I_\pi \cap k[\mathbf{U},\mathbf{V}] = I_{\partial \pi }$
. For each
$i$
, there is a persistent path beginning at
$V_{\sigma i}$
and ending at
$U_i$
, and these endpoints maintain valence one in the graph of live edges throughout the Falling Roofs algorithm; since only vertices within the same persistent path may be connected by an edge in
$\mathscr{N}\ $
this means that only edges in
$\mathscr{N\ }^{\ \, +}$
are of the form
$V_{\sigma i} \longrightarrow U_i$
, as claimed.
In this section, we answer two further questions:
-
• Is there a choice of total order on
$U_\pi$
under which the Gröbner basis algorithms match the familiar process of cut-elimination as represented by the reduction rules of Definition 4.3? Theorem 7.2 answers this in the affirmative. -
• The normal form of
$\pi$
contains more unoriented atoms than just
$\mathbf{U}, \mathbf{V}$
, so is there a choice of total order on
$U_\pi$
for which the Gröbner basis algorithms produce the normal proof net
$\widetilde {\pi }$
with its ideal
$I_{\widetilde {\pi }}$
?
7.1 Elimination versus cut-elimination
Let
$\Gamma : \pi \longrightarrow \pi '$
be a reduction sequence between proof nets with single conclusion
$A$
. We view
$P_{\pi '}$
as a subring of
$P_\pi$
via the algebra homomorphism
$T_\Gamma$
of Definition 4.15. Recall the following notation:
-
•
$\lt _\Gamma$
is a monomial order; variables eliminated by
$\Gamma$
are ‘large’ (Definition 6.9). -
•
$G_{\pi }^{(\Gamma )}$
is a generating set for
$I_\pi$
(Definition 6.11). Up to signs, it is
$G_\pi$
. -
•
$\mathbb{B}_{es}(G_{\pi }^{(\Gamma )}, \lt _\Gamma )$
is a Gröbner basis for
$I_\pi$
obtained by applying the Buchberger with Early Stopping algorithm (Algorithm 2) to
$G_{\pi }^{(\Gamma )}$
. -
•
$G_{\pi '}^{(0)}$
is a (minimal) Gröbner basis for
$I_{\pi '}$
(Definition 6.4).
Theorem 7.2. There is an equality of sets
\begin{equation} G_{\pi '}^{(0)} = \mathbb{B}_{es}\big(G_{\pi }^{(\Gamma )}, \lt _\Gamma\! \big) \cap P_{\pi '}\,. \end{equation}
Proof.
By definition
$G^{(\Gamma )}_\pi = G_{\mathscr{S}}$
, where
$\mathscr{S}$
is the graph of Definition 6.10. If
$\mathscr{N}\ $
is the output of the Falling Roofs algorithm applied to
$\mathscr{S}$
, then by Proposition 5.17
\begin{equation} \mathbb{B}_{es}\big(G_{\pi }^{(\Gamma )}, \lt _\Gamma\! \big) = G_{\mathscr{N}}\,. \end{equation}
We are in the situation of Section 5.3, where the
$\mathbf{X}$
-variables are those in
$P_{\pi '}$
. The monomial order
$\lt _\Gamma$
satisfies the conditions of Proposition 5.21, from which we deduce that
$G_{\mathscr{N\ }^{\ \, +}} = G_{\mathscr{N}}\ \cap P_{\pi '}$
is a Gröbner basis for
$I_{\pi '}$
. Since the
$\mathbf{X}$
variables are ordered by
$\lt _\Gamma$
in
$P_{\pi }$
as they are by
$\lt _0$
in
$P_{\pi '}$
, it is clear that
$\mathscr{N\ }^{\ \, +}$
is just the graph
$\mathscr{S}_0$
of Definition 6.3 and hence
$G_{\mathscr{N\ }^{\ \, +}} = G^{(0)}_{\pi '}$
.
The core idea of the theorem can be seen in the following example.
The Falling Roofs algorithm on the canonical detour.
Example 7.3.
Let
$\pi$
denote the canonical detour as in Example 4.13
. We continue Example 6.12 by presenting the Falling Roofs algorithm on the graph of Figure
8
. The result of the algorithm is the graph
$\mathscr{N}\ $
in Figure
9
. Note that in the context of Section 5.3, if we partition the variables of our polynomial ring
\begin{equation*} P_\pi = k[X_1, X_2, X_3, \underline {X_4}, \underline {X_5}, X_6, X_7, \underline {X_8}, \underline {X_9}, X_{10}, X_{11}, X_{12}] \end{equation*}
into the set
$\mathbf{X}$
of those variables without underlines and the set
$\mathbf{Y}$
of those variables with underlines, then ‘cutting off the top’ of the graph
$\mathscr{N}\ $
means cutting it at a height with all the underlined variables above and all the other variables below. Recall from Proposition 5.17 that the Buchberger algorithm with Early Stopping on
$G^{(\gamma )}_\pi$
computes
$\mathscr{N}\ $
:
\begin{equation*} \mathbb{B}_{es}(G^{(\gamma )}_\pi , \lt _\gamma\! ) = G_{\mathscr{N}}\,. \end{equation*}
The Elimination Theorem (Theorem 5.7 ) says that
\begin{align*} G_{\mathscr{N}}\ \cap k[\mathbf{X}] &= \big \{ X_2 - X_1, X_3 - X_2, X_6 - X_3, X_7 - X_6,\\ &\qquad X_{10} - X_7, X_{11} - X_{10}, X_{12} - X_{11} \big \} \end{align*}
is a Gröbner basis for
$I_\pi \cap k[\mathbf{X}]$
. Note that eliminating the cut in the canonical detour leads to the proof net
$\pi '$
, the main part of which is shown in Figure
10
. By construction,
$T_\gamma : P_{\pi '} \longrightarrow P_{\pi }$
is the inclusion of
\begin{equation*} P_{\pi '} = k[\mathbf{X}] = k[X_1, X_2, X_3, X_6, X_7, X_{10}, X_{11}, X_{12}] \end{equation*}
into
$P_\pi$
(note that
$X_1, X_{12}$
are not shown in the Figure for compactness).
Cut reduction on the canonical detour.
7.2 Normal Buchberger and normal forms
In Theorem 7.2, we made a connection between our modification to the Buchberger algorithm (Algorithm 2) and single step cut-reduction. We now examine the ‘standard’ form of Buchberger’s Algorithm (Cox et al. Reference Cox, Little and O’Shea2015, §2.10 Theorem 9) and show that it relates to normalisation, that is, a maximal sequence of cut reductions yielding a normal form. In this section,
$\pi$
denotes a proof net with single conclusion
$A$
.
Lemma 7.4.
If
$\Gamma , \Omega : \pi \longrightarrow \pi '$
are reduction sequences between proof nets with
$\pi '$
cut-free then
$T_\Gamma = T_\Omega$
.
Proof. Let the reduction sequences be
with
$\Gamma$
on top and
$\Omega$
on the bottom. Recall that any two reduction paths have the same length (Troiani Reference Troiani2020, Corollary 3.0.7). Cut reduction is confluent (Troiani Reference Troiani2020, Proposition 3.0.3), so it suffices to show that any commutative diagram of reductions
induces a commutative diagram
For any reduction
$\gamma : \pi \longrightarrow \pi '$
, the schematics used to define
$T_\gamma$
indicate a mapping from the edges of
$\pi$
to the edges of
$\pi '$
. Commutativity of (71) amounts to confluence of this induced map. This follows from inspection of Figure 3.
Let
$\Gamma$
denote any reduction path from
$\pi$
to its normal form
$\widetilde {\pi }$
(the unique cut-free multiplicative proof net equivalent under cut-reduction to
$\pi$
). By the previous lemma, the
$k$
-algebra morphism
\begin{equation*} T = T_\Gamma : T_{\widetilde {\pi }} \longrightarrow T_\pi \end{equation*}
is independent of the choice of
$\Gamma$
, and in this section, we simply denote it by
$T$
. There is a simple characterisation of the variables of
$P_\pi$
in the image of
$T$
. Recall that a proof net is an oriented multigraph, and a directed path in
$\pi$
means a sequence of edges traversed in the same direction as the orientation.
Lemma 7.5.
An unoriented atom
$U$
of
$\pi$
is in the image of
$T$
if and only if it is above a conclusion in the sense that the unique maximal directed path in
$\pi$
starting at the edge associated to
$U$
ends at a conclusion.
Proof.
Let
$\rho$
be the maximal directed path whose first edge is the one associated to
$U$
. First, we prove that if
$\rho$
ends at a conclusion, then every unoriented atom of every formula labelling an edge in
$\rho$
is in the image of
$T$
.
Write
$\rho = (e_1,\ldots , e_n)$
and notice first that none of the edges
$e_2,\ldots , e_n$
can appear in any redex. So, we only need to consider
$e_1$
, which is labelled by
$A$
. If
$e_1$
is part of a redex, it is necessarily part of an
$a$
-redex. Inspection of (30) shows that reducing this
$a$
-redex results in a proof with the edge labelled
$A$
still present. This resulting edge now either may be part of an
$a$
-redex or not. Reducing any other
$a$
-redex not involving the edge labelled
$A$
does not remove this edge labelled
$A$
. Reducing any
$m$
-redex also does not remove this edge labelled
$A$
. It follows that the edge labelled
$A$
appears in the normal form
$\pi '$
. That is,
$U$
is in the image of
$T$
.
Now, we prove that if
$\rho$
ends at a cut link then none of the unoriented atoms of
$A$
are in the image of
$T$
. We proceed by induction on the length
$n$
of
$\rho$
. Say
$n = 1$
, if the edge labelled
$A$
is premise to a cut link, then it is part of an
$a$
-redex which when reduced, removes the edge labelled
$A$
. Thus,
$U$
cannot be in the image of
$T$
.
Now, assume that
$n \gt 1$
and the result has been proved in the setting where
$\rho$
is of length
$n-1$
. If
$A$
is above a cut link, then reducing this cut link results in a proof net where
$A$
is still above a cut link, the result follows directly from the inductive hypothesis.
Note that an unoriented atom of
$\pi$
, which is not above a conclusion must be above a cut in the sense that the unique maximal directed path in
$\pi$
starting at the edge associated to the atom ends at a cut link. These are the variables eliminated by
$\Gamma$
, or what is the same, the variables not in the image of
$T$
.
Lemma 7.6.
Let
$\mathscr{P} = (Z_1,\ldots , Z_r)$
be a persistent path in
$\pi$
which traverses a cut link. Then, there exists a (necessarily unique) pair of indices
$1 \lt t_1, t_2 \lt r$
such that
$Z_i$
is above a cut if and only if
$t_1 \le i \le t_2$
.
Proof.
Let
$Z$
be a variable above a conclusion. By Lemma 7.5, every unoriented atom of every formula labelling an edge in the directed path starting at the edge of
$Z$
and ending at a conclusion is also above a conclusion. Thus, either
$(Z_1,\ldots , Z)$
or
$(Z, \ldots , Z_r)$
is a subsequence of
$\mathscr{P}$
consisting only of variables above a conclusion. Thus,
$t_1$
can be taken to be the maximal integer such that
$(Z_1,\ldots , Z_{r_1-1})$
is a subsequence of
$\mathscr{P}$
consisting only of variables above a conclusion, and
$t_2$
can be taken to be the maximal integer such that
$(Z_{t_2+1},\ldots , Z_r)$
is a subsequence of
$\mathscr{P}$
consisting only of variables above a conclusion.
Let
$\mathscr{P}_1,\ldots , \mathscr{P}_m$
denote the persistent paths of
$\pi$
, ordered in the way described at the beginning of Section 6.1. Let
$\mathscr{Q}_i$
denote the subsequence of
$\mathscr{P}_i$
consisting of those unoriented atoms in the normalisation
$\widetilde {\pi }$
, that is, those atoms in the image of
$T$
. In light of Lemma 7.6, we can divide the sequence
$\mathscr{P}_i$
into three parts:
\begin{equation} \mathscr{P}_i = \mathscr{Q}_i^1, \mathscr{P}_i \setminus \mathscr{Q}_i, \mathscr{Q}_i^2 \end{equation}
where
$\mathscr{Q}_i^1$
is the subsequence of
$\mathscr{P}_i$
consisting of those unoriented atoms in the persistent path coming before all the atoms above a cut, and
$\mathscr{Q}_i^2$
is the subsequence of atoms coming after all those above a cut. By definition,
$\mathscr{Q}_i = \mathscr{Q}_i^1 \sqcup \mathscr{Q}_i^2$
.
Consider the following permutation of
$\mathscr{P}_i$
\begin{equation} \widetilde {\mathscr{\!\!P}}_i = (\mathscr{Q}_i^1)^{\textrm {op}}, \mathscr{Q}_i^2, (\mathscr{P}_i \setminus \mathscr{Q}_i)^{\textrm {op}} \end{equation}
where
$\mathscr{R}^{\textrm {op}}$
means the reversal of the sequence
$\mathscr{R}$
. Combining these re-ordered persistent paths we obtain a total order on the set of unoriented atoms of
$\pi$
:
\begin{equation} \widetilde{\mathscr{\!\!P}}_1, \ldots , \widetilde{\mathscr{\!\!P}}_m\,. \end{equation}
Definition 7.7.
We write
$U \lt _n V$
if
$U$
is before
$V$
in (
74
), reading from left to right. The monomial order
$\lt _n$
on
$P_\pi$
is the lexicographic order determined by
$\lt _n$
on the variables.
Definition 7.8.
Let
$\mathscr{S}_n$
be the oriented graph with vertex set
$U_\pi$
, where two variables
$U,V \in U_\pi$
are connected by an edge
$e: U \longrightarrow V$
if
$U \sim V$
and
$U \lt _n V$
.
Definition 7.9.
Let
$G^{(n)}_\pi$
be the ordered set of polynomials
$G_{\mathscr{S}_n}$
of Definition 5.14
,
\begin{equation} G^{(n)}_\pi = \big \{ V - U \,|\, e: U \longrightarrow V \text{ is an edge in } \mathscr{S}_n \big \}\,. \end{equation}
Example 7.10.
Let
$\Gamma$
be the normalisation of the canonical detour
$\pi$
in Example 4.13
. Then,
$X_1, X_2, X_{11}, X_{12}$
are above a conclusion and the rest are above a cut, so
$\mathscr{P}$
is
\begin{equation*} X_1, X_2, \underline {X_3, X_4, X_5, X_6, X_7, X_8, X_9, X_{10}}, X_{11}, X_{12} \end{equation*}
where we underline the atoms in
$\mathscr{P} \setminus \mathscr{Q}$
. Hence
$\mathscr{Q}^1$
is
$X_1,X_2$
,
$\mathscr{Q}^2$
is
$X_{11}, X_{12}$
and (
73
) is
\begin{equation*} (\mathscr{Q}^1)^{\textrm {op}}, \mathscr{Q}^2, (\mathscr{P} \setminus \mathscr{Q})^{\textrm {op}} = X_2, X_1, X_{11}, X_{12}, \underline {X_{10}, X_9, X_8, X_7, X_6, X_5, X_4, X_3}\,. \end{equation*}
The graph
$\mathscr{S}_n$
is shown in Figure
11
The graph
$\mathscr{S}_n$
for the canonical detour of Example 7.10.
We identify
$P_{\widetilde {\pi }}$
as a subring of
$P_\pi$
using
$T$
.
Theorem 7.11.
Let
$\pi$
be a proof net and
$\widetilde {\pi }$
the normal form. Let
$\mathbb{B}(G^{(n)}_\pi , \lt _n)$
denote the result of applying the Buchberger algorithm. Then there is an equality of sets
\begin{equation} G^{(n)}_{\widetilde {\pi }} = \mathbb{B}(G^{(n)}_\pi , \lt _n) \cap P_{\widetilde {\pi }}\,. \end{equation}
Proof.
We write
$G^{(n)}_\pi = \{\,f_1, \ldots , f_s \}$
. Buchberger’s Algorithm (Cox et al. Reference Cox, Little and O’Shea2015, §2.10 Theorem 9) begins by choosing a pair
$(i,j)$
with
$i \lt j$
and considering the
$S$
-polynomial
$S(\,f_i, f_j)$
. The only interesting case is when
$f_i, f_j$
share a leading term, so we assume this below.
The polynomials
$f_i, f_j$
must lie on a common persistent path
$\mathscr{P}$
, which traverses a cut. We have that
$f_i = Z_{r_1+1} - Z_{r_1 + 2}$
and
$f_j = Z_{r_1+1} - Z_{r_1}$
for some unoriented atoms in the persistent path
$\mathscr{P} = Z_1, \ldots , Z_l$
and
\begin{align*} S(\,f_i, f_j) &= (Z_{r_1+1} - Z_{r_1 + 2}) - (Z_{r_1+1} - Z_{r_1})\\ &= Z_{r_1 } - Z_{r_1 + 2}\,. \end{align*}
We now divide by the sequence
$(\,f_1,\ldots , f_s)$
.
The division algorithm necessarily terminates here as there is no polynomial in
$G^{(n)}_\pi$
with leading term either
$Z_{r_2}$
or
$Z_{r_1}$
. It remains to show that
$Z_{r_2} - Z_{r_1}$
appears in
$G^{(n)}_{\pi '}$
.
The sequence
$(Z_{r_1}, Z_{r_1+1}, \ldots , Z_{r_2-1}, Z_{r_2})$
is a subsequence of
$\mathscr{P}$
and there is an associated persistent path
$\mathscr{P}'$
in
$\pi '$
for which
$(Z_{r_1}, Z_{r_2})$
is a subsequence. By the way that
$\lt _n$
is defined, we have that
$Z_{r_2} - Z_{r_1} \in G^{(n)}_{\pi '}$
. This proves the containment
$\supseteq$
in (76).
Next, we show the reverse inclusion. Let
$f \in G^{(n)}_{\pi '}$
be given. If
$f \in G^{(n)}_\pi$
, then there is nothing to show, as
$G^{(n)}_\pi \subseteq \mathbb{B}(G^{(n)}_\pi , \lt _n)$
. So, suppose
$f \notin G^{(n)}_\pi$
. Then,
$f = X' - X$
for some persistent path in
$\pi$
with subsequence
$(X, W_1, \ldots , W_t, X')$
where
$W_1,\ldots , W_t$
are variables not in
$P_{\pi '}$
. Let
$g = W_1 - W_2$
and
$g' = W_1 - X$
. Then,
$g, g' \in G^{(n)}_\pi$
and the first half of this proof shows that division of
$S(g,g')$
by
$G^{(n)}_{\pi }$
yields
$f$
, so
$f \in \mathbb{B}(G^{(n)}_\pi , \lt _n)$
.
8. Conclusion
Let us summarise the dictionary between proofs and ideals developed in this paper. We have shown how to associate to a proof net
$\pi$
in multiplicative linear logic a triple
\begin{equation} \pi \longmapsto (P_\pi , G_\pi , \lt _0) \end{equation}
consisting of a polynomial ring
$P_\pi$
, a generating set
$G_\pi$
for an ideal
$I_\pi$
in this ring, and a monomial order
$\lt _0$
on
$P_\pi$
. We have shown that
$G_\pi$
is a Gröbner basis for
$I_\pi$
with respect to this monomial order (Proposition 6.6).
There are many other monomial orders on
$P_\pi$
. With respect to some monomial orders,
$G_\pi$
will be ‘stable’ in the sense that it is a Gröbner basis, while it will be ‘unstable’ (not a Gröbner basis) with respect to others and running the Buchberger algorithm makes nontrivial changes. The correspondence in (78) maps proof nets to stable triples. However, if
$\pi$
contains
$(\!\operatorname {cut}\!)$
links, then we can destabilise it by using a monomial order
$\lt _\Gamma$
derived from some reduction sequence. The ‘restabilisation’ of
$(P_\pi , G_\pi , \lt _\Gamma )$
is the process of running the Buchberger algorithm and intersecting with the subring
$P_{\pi '}$
of ‘low’ variables with respect to
$\lt _\Gamma$
. Our main Theorem says that this process ends with the image of the reduction
$\pi '$
under the map (78), or in other words the following diagram commutes:
The language of stability is best understood in the context of the realisations: the combinatorial
$1$
-manifolds together with a discrete Morse function (‘height on the page’) that we have associated to any pair
$(G_\pi , \lt )$
where
$\lt$
is a lexicographic monomial order. If the realisation contains no local maximum (that is, a roof) then by Corollary 5.18,
$G_\pi$
is a Gröbner basis with respect to
$\lt$
. Otherwise, the Buchberger algorithm (or equivalently Falling Roofs) proceeds to ‘straighten out’ the pair consisting of the
$1$
-manifold with its Morse function, until the subgraph of live edges contains no such local maxima. That is, the Falling Roofs algorithm transforms a segment looking like
into a segment looking like
The algebro-geometric procedure in the right column of (79) and the topological procedure in (80), (81) represent our attempt to find mathematical shadows of the process of cut-elimination process for multiplicative proof nets.
8.1 Towards geometry
Let
$\pi$
be a proof net with ideal
$I_\pi \subseteq P_\pi$
. The algebraic set
\begin{equation*} \mathbb{V}(I_\pi ) = \{ a \in \mathbb{A}^\pi \,|\, f(a) = 0 \,\text{for all } f \in I_\pi \} \end{equation*}
is an intersection of pairwise diagonals, which is not geometrically very interesting. More geometry can be introduced into the picture by considering pairs
$\mathbb{V}(I_\pi ) \subseteq V$
where
$V$
is an algebraic set. For example, given any
$N \ge 2$
, the polynomial
$W = \sum _{f \in G_{\pi }} f^N$
is contained in
$I_\pi$
and so we have an inclusion
\begin{equation*} \mathbb{V}(I_\pi ) \subseteq \mathbb{V}(W)\,. \end{equation*}
The subscheme
$\mathbb{V}(I_\pi )$
naturally determines an object in the bounded derived category of coherent sheaves of the singular hypersurface
$\mathbb{V}(W)$
, and in closely related categories like the category of matrix factorisations of
$W$
. In sequels to the present paper, we will explore this idea as a way of associating objects in triangulated categories to proofs; the role of the Buchberger algorithm in the present paper is played by constructions in homological algebra such as the perturbation lemma.
A. Geometry of Interaction: Multiplicatives
In Troiani (Reference Troiani2020), a permutation is associated to each proof net, as was originally done by Girard Girard (Reference Girard1987). In short, these permutations act on the disjoint union of all the unoriented atoms of all the conclusions to axiom links of
$\pi$
. The permutation of interest here is
$\alpha _\pi$
(Definition [Troiani Reference Troiani2020, 4.1.3]) which permutes two unoriented atoms
$X,Y$
if and only if
$X,Y$
are respectively unoriented atoms of formulas
$A,\neg A$
where
$A,\neg A$
are the conclusions of some axiom link in
$\pi$
, and
$X,Y$
appear at the same index of the sequences of unoriented atoms of
$A,\neg A$
. This permutation is equal to
$\sigma$
, which is introduced in Proposition 4.11.
Proposition A.1.
Let
$\pi$
be a proof net with single conclusion
$A$
with sequence of oriented atoms given by:
$\big ((U_{1},u_1),\ldots ,(U_n,u_n)\big )$
and let
$\sigma$
be as given in Proposition 4.11
. Let
$\delta _\pi$
be the permutation defined in (Troiani Reference Troiani2020
, Definition 4.2.10). Then for all
$i= 1,\ldots ,n$
we have:
\begin{equation} \delta _{\pi }(U_i) = U_{\sigma (i)} \end{equation}
Proof.
First, we consider the special case when there are no
$m$
-redexes in
$\pi$
, and all conclusions of all axiom links are atomic. We will use some structure of such proof nets proved in Troiani (Reference Troiani2020). First, we observe that all reductions are of the following form (see (Troiani Reference Troiani2020, Lemma 4.2.5)).
Hence, all the cut links of
$\pi$
appear inside ‘chains’ of axiom and cut links, as in the following Diagram.
Also, by Proposition (Troiani Reference Troiani2020, 4.1.7), a cut-free proof net with sole conclusion
$B$
satisfying the property that every conclusion of every axiom link is atomic, is unique up to axiom links. Since each chain of axiom and cut links can be replaced by a single axiom link, it follows from this Proposition that
$\pi$
is uniquely determined up to these chains. The proof net
$\pi$
is thus a root labelled
$\operatorname {c}$
with an incoming edge labelled
$A$
, the body of
$\pi$
is a finite binary tree uniquely determined by
$A$
, with some choice of chains connecting the leaves of the body of
$\pi$
. See Example (Troiani Reference Troiani2020, 4.1.9) for an example. Consider the subgraph of
$\pi$
given by removing the chains, we notice that the order of the atomic propositions at the leaves (read from left to right) is the same as the order of the sequence of oriented atoms of
$A$
. Hence,
$U_{\sigma (i)}$
is the unoriented atom corresponding to an atomic proposition connected via a chain to the formula whose corresponding unoriented atom is
$U_{i}$
.
On the other hand, as described in the proof of Theorem (Troiani Reference Troiani2020, 4.2.11), the permutation
$\delta _\pi$
is a product of transpositions, where two unoriented formulas
$X,Y$
are swapped if and only if they are at the extreme ends of a common chain. Hence,
$\delta _{\pi }(U_i) = U_{\sigma (i)}$
.
Now, we consider the case where
$\pi$
may admit
$m$
-redexes, we still assume that every conclusion of every axiom link is atomic though. Let
$\pi '$
denote the proof net obtained by reducing all
$m$
-redexes, by confluence of cut-reduction (Proposition [Troiani Reference Troiani2020, 3.0.3]),
$\pi '$
is independent of the order in which these
$m$
-redexes are reduced. We claim that
$\delta _{\pi } = \delta _{\pi '}$
and also that the permutation
$\sigma$
obtained from
$\pi$
is equal to the permutation
$\sigma '$
obtained from
$\pi '$
. Both of these facts follow from Lemma (Troiani Reference Troiani2020, 4.2.4).
Finally, we consider the general case. In (Troiani Reference Troiani2020, Definition 3.0.9) we defined an
$\eta$
-increx to be a subgraph of a proof net of the following form.
We can replace this by the subgraph (85) below, and then repeat that process to eventually obtain a proof net
$\pi '$
such that every every conclusion of every axiom link of
$\pi '$
is atomic.
One must check that
$\pi '$
is independent of the choice of
$\eta$
-expansion procedure, and also that this process terminates. This is done just after Lemma 3.0.10 in Troiani (Reference Troiani2020). It now remains to show that
$\delta _{\pi } = \delta _{\pi '}$
and that the permutation
$\sigma$
obtained from
$\pi$
is equal to the permutation
$\sigma '$
obtained from
$\pi '$
. Both of these facts follow from inspection of (85).
a
m
Tγ
Sγ
TS
Ai=A=(X,+)
Sγ
Sn
Open access
