# On the reduction numbers and
the Castelnuovo-Mumford regularity
of projective monomial curves

Tran Thi Gia Lam  Phu Yen University, Tuy Hoa, Vietnam
<EMAIL_ADDRESS>
###### Abstract.

This paper gives explicit formulas for the reduction number and the
Castelnuovo-Mumford regularity of projective monomial curves.

###### Key words and phrases:

monomial curves, reduction number, Castelnuovo-Mumford regularity, Cohen-
Macaulay ring, Buchsbaum ring

###### 2010 Mathematics Subject Classification:

Primary 13D02, 13F65; Secondary 13H10, 14H20

## Introduction

Let $R$ be a Noetherian ring and $I$ an ideal in $R$. An ideal $J\subseteq I$
is called a reduction of $I$ if $JI^{r}=I^{r+1}$ for some $r\geq 0$. We denote
by $r_{J}(I)$ the least number $r$ with this property and call it the
reduction number of $I$ with respect to $J$. A reduction of $I$ is minimal if
it does not contain any other reduction of $I$. The reduction number of $I$ is
defined by

$r(I)=\min\\{r_{J}(I)|\ \text{$J$ is a minimal reduction of $I$}\\}.$

These notions were introduced by Northcott and Rees [7] and play an important
role in the theory of integral closure and in the study of the blow-up rings,
see e.g. [11, 15].

Let $R$ be a finitely generated standard graded algebra over a field $k$ and
let $R_{+}$ be its maximal graded ideal. One calls $r(R_{+})$ the reduction
number of the algebra $R$ [12, 14]. In this paper, we will investigate the
reduction number of the coordinate ring of projective monomial curves, which
are given parametrically by monomials of the same degree in two variables. Our
investigation is motivated by the fact that in this case, the reduction number
is a good approximation of the Castelnuovo-Mumford regularity
$\operatorname{reg}(R)$ of $R$, which is a universal bound for many important
invariants of $R$ [13]. For instance, $\operatorname{reg}(R)$ is an upper
bound for the maximal degree of the defining equations of $R$.

Let $M$ be a set of monomials of degree $d$ in two variables $x,y$. Without
restriction we may assume that $x^{d},y^{d}\in M$. Let $R$ be the coordinate
ring of the corresponding monomial curve. Then $R$ is isomorphic to the
subalgebra $k[M]$ of $k[x,y]$ generated by the monomials of $M$. Represent $R$
as a quotient of a polynomial ring $S$. Consider a minimal free resolution of
$R$ over $S$:

$0\to F_{p}\to\cdots\to F_{0}\to R\to 0$

where $F_{i}$ is a graded free module over $S$, $i=0,...,p$. Let $b_{i}$ be
the maximal degree of the generators of $F_{i}$. Then the Castelnuovo-Mumford
regularity of $R$ is the number

$\operatorname{reg}(R)=\max\\{b_{i}-i|\ i=0,...,p\\}.$

Roughly speaking, the behavior of the graded components of $R$ will become
regular in the degrees $\geq\operatorname{reg}(R)$. To compute
$\operatorname{reg}(R)$ is usually a hard problem. By a result of Gruson,
Lazarsfeld and Peskine [3] we know that $\operatorname{reg}R\leq d-|M|-2$.
Finer bounds for $\operatorname{reg}(R)$ in terms of $M$ have been given in
[1, 4, 6].

It is well known that $\operatorname{reg}(R)$ is also the regularity of $R$ as
a module over the ring $A=k[x^{d},y^{d}]$, which is a Noether normalization of
$R$. The minimal free resolution of $R$ over $A$ has the simple form

$0\to E_{1}\to E_{0}\to R\to 0,$

where $E_{i}$ is a graded free module over $A$, $i=0,1$. Let $c_{i}$ be the
maximal degree of the generators of $F_{i}$. Then

$\operatorname{reg}(R)=\max\\{c_{0},c_{1}-1\\}.$

Let $Q=(x^{d},y^{d})$ be the ideal generated by $x^{d},y^{d}$ in $R$. It is
easy to see that $Q$ is a minimal reduction of $R_{+}$ and
$r_{Q}(R_{+})=c_{0}$. Hence, $r_{Q}(R_{+})$ is a good approximation of
$\operatorname{reg}(R)$. In particular, $\operatorname{reg}(R)=r_{Q}(R_{+})$
if $R$ is a Cohen-Macaulay ring or a Buchsbaum ring [10]. It had been an open
question whether $\operatorname{reg}(R)=r_{Q}(R_{+})$ always holds until
Hellus, Hoa and Stückrad found a counter-example in [4].

The goal of this paper is to find explicit formulas for $r_{Q}(R_{+})$ in
terms of $M$. We will represent $M$ as a non-increasing sequence of non-
negative integers

$0=a_{0}\leq a_{1}<a_{2}\leq a_{3}<\ldots<a_{2m}\leq a_{2m+1}=d$

with $a_{2(i+1)}\geq a_{2i+1}+2$, $i=0,...,m$, such that

$M=\\{x^{\alpha}y^{d-\alpha}\ |\ \alpha\in[a_{2i},a_{2i+1}],i=0,...,m\\},$

where $[a_{2i},a_{2i+1}]$ denotes the set of integers ${\alpha}$,
$a_{2i}\leq{\alpha}\leq a_{2i+1}$. We may view $[a_{2i},a_{2i+1}]$ as an
interval in the segment $[0,d]$. Our main results give explicit formulas for
$r_{Q}(R_{+})$ and $\operatorname{reg}(R)$ in terms of $a_{1},...,a_{2m+1}$ in
the cases of Figure 1, where the given intervals are painted bold and the dots
mean intervals of one point.

Case A:

Case B:

Case C:

Case D:

Case E:

Figure 1.

Our results shows that the computation of $r_{Q}(R_{+})$ depends very much on
whether the two intervals on both ends consist of one point, i.e. $a_{1}=0$ or
$a_{2m}=d$, or not. This was already observed in [9], where the Cohen-
Macaulayness of projective monomial curves was studied. Case C follows from
results of Hellus, Hoa and Stückrad for smooth monomial curves [4]. Our
investigation can be served as a starting point for a systematic study of the
Castelnuovo-Mumford regularity of projective monomial curves via the reduction
number.

The paper is organized as follows. The main part of the paper is divided in 5
sections. In Section 1 we prepare some properties of the minimal reduction $Q$
of $R_{+}$ and translate the computation of $r_{Q}(R_{+})$ into a
combinatorial problems on lattice points. Sections 2-6 will deal with the
cases A–E, respectively.

##  1\. Preliminaries

Throughout this paper, let $R=k[M]$ be the algebra over a field $k$ generated
by a given set $M$ of monomials of degree $d>0$ in two variables $x,y$, which
contains $x^{d},y^{d}$. If we set $\deg f=1$ for all $f\in M$, then $R$
becomes a graded algebra. Suppose that $R=\oplus_{n\geq 0}R_{n}$. Let
$R_{+}=\oplus_{n\geq 1}R_{n}$, which is the maximal graded ideal of $R$.

######  Lemma 1.1.

Let $Q$ be a homogeneous ideal of $R$ generated by elements of degree 1. Then
$Q$ is a reduction of $R_{+}$ if and only if $R_{n}=Q_{n}$ for some $n\geq 1$,
and $r_{Q}(R_{+})$ is the least integer $n$ such that $R_{n+1}=Q_{n+1}$.

###### Proof.

Since $R$ is a standard graded algebra, i.e. it is generated by $R_{1}$,
$(R_{+})^{n}$ is generated by $R_{n}$. Similary, since $Q$ is generated by
$Q_{1}$, $Q^{n}$ is generated by $Q_{n}$. Therefore,
$(R_{+})^{n+1}=Q(R_{+})^{n}$ if and only if $R_{n+1}=Q_{n+1}$. Hence, the
conclusion follows from the definition of reduction and reduction number. ∎

The proof shows that Lemma 1.1 holds for any standard graded algebra.

From now on, let $Q=(x^{d},y^{d})$ be the ideal generated by $x^{d},y^{d}$ in
$R$.

######  Lemma 1.2.

$Q$ is the unique minimal reduction of $R_{+}$ generated by monomials.

###### Proof.

Let $f$ be an arbitrary monomial of degree $r(d-1)+1$ in $R$, where $r$ is the
number of monomials in $M$. Since $f$ is a product of $r(d-1)+1$ monomials in
$M$, $f$ is divisible by $g^{d}$ for some $g\in M$. Since $g=x^{a}y^{b}$ for
some $a,b\geq 0$, it follows that $f$ is divisible by $x^{d}$ or $y^{d}$ in
$R$. So we conclude that $R_{r(d-1)+1}=Q_{r(d-1)+1}$. By Lemma 1.1, $Q$ is a
reduction of $R_{+}$. Since $\dim R=2$, any reduction of $R_{+}$ generated by
two elements is a minimal reduction of $R_{+}$ [7, Theorem 2 of p. 151 and
Theorem 1 of p. 154]. Therefore, $Q$ is a minimal reduction of $R_{+}$.

If there were an other minimal reduction of $R_{+}$ generated by two monomials
$f,g$, then $f,g\in M$ and $x^{nd},y^{nd}$ must be divisible by $f$ or $g$ for
some $n\geq 1$. From this it follows that $f,g$ must be powers of $x$ or $y$.
Since $x^{d},y^{d}$ are the only generators of $M$ having these forms, we
conclude that $f,g$ are $x^{d},y^{d}$. ∎

Despite the uniqueness of $Q$ we may have $r_{Q}(R_{+})>r(R_{+})$. This can be
seen as follows.

Let $I$ be the ideal generated by $M$ in $k[x,y]$. Let ${\mathfrak{m}}$ be the
maximal graded ideal of $k[x,y]$. Let $F(I)=\oplus I^{n}/{\mathfrak{m}}I^{n}$,
which is the fiber ring of $I$. It is easy to see that $F(I)\cong R$. By [12,
Lemma 4.1], there is a one-to-one correspondence between the minimal
reductions of $I$ and the minimal reductions of $R_{+}$, which preserves the
reduction number. Huckaba showed that the reduction number of $I$ with respect
to a minimal reduction $J$ depens on the choice of $J$ [5, Example 3.1]. His
result leads to the following example.

######  Example 1.3.

Let $I=(x^{7},x^{6}y,x^{2}y^{5},y^{7})\subseteq k[x,y]$ and
$J_{1}=(x^{7},y^{7})$, $J_{2}=(x^{7},x^{6}y+y^{7})$. By [5, Example 3.1],
$r_{J_{1}}(I)=4>r_{J_{2}}(I)$. Hence, $r_{J_{1}}(I)>r(I)$. Let
$R=k[x^{7},x^{6}y,x^{2}y^{5},y^{7}]$ and $Q=(x^{7},y^{7})\subseteq R$. By [12,
Lemma 4.1], this implies $r_{Q}(R_{+})>r(R_{+})$.

On the other hands, there are many cases where $r_{Q}(R_{+})=r(R_{+})$. In the
following we say that $R$ is a Buchsbaum ring if the local ring of $R$ at the
prime ideal $R_{+}$ is a Buchsbaum ring. We refer the reader to [8] for the
definition of Buchsbaum local rings. Notice that this class of rings contains
all Cohen-Macaulay ring.

######  Proposition 1.4.

Let $R$ be a Buchsbaum ring. Then

$\operatorname{reg}(R)=r_{Q}(R_{+})=r(R_{+}).$

###### Proof.

This result follows from [10, Corollary 3.5]. Note that the reduction number
is defined there differently. ∎

We always have $\operatorname{reg}(R)\geq r_{Q}(R_{+})$ [10, Proposition 3.2].
There are examples showing that $\operatorname{reg}(R)>r_{Q}(R_{+})$ even when
the corresponding monomial curve is smooth. These examples are found first by
Hellus, Hoa and Stückrad [4, Example 3.2].

Now we will translate the computation of $r_{Q}(R_{+})$ into a combinatorial
problem of lattice points in $\mathbb{N}^{2}.$ For this purpose, we identify
any monomial $x^{\alpha}y^{\beta}$ with the point $({\alpha},{\beta})$.

For $n\geq 0$ let

$H_{n}=\\{(\alpha,\beta)\in{\mathbb{N}}^{2}|\ x^{\alpha}y^{\beta}\in
R,\alpha+\beta=nd\\}.$

Then $R_{n}$ is the vector space generated by the monomials
$x^{\alpha}y^{\beta}$, $(\alpha,\beta)\in H_{n}$. Let $e_{1}=(d,0)$ and
$e_{2}=(0,d)$. Then $Q_{n}$ is the vector space generated by the monomials
$x^{\alpha}y^{\beta}$, $(\alpha,\beta)\in H_{n-1}+\\{e_{1},e_{2}\\}$
(Minkowski sum). Using Lemma 1.1, we immediately get

$r_{Q}(R_{+})=\min\\{n\in{\mathbb{N}}|\ H_{n+1}=H_{n}+\\{e_{1},e_{2}\\}\\}.$

This formula can be simplified by considering the first components of the
elements of $H_{n}$.

######  Lemma 1.5.

Let $E_{n}=\\{\alpha|\ (\alpha,nd-\alpha)\in H_{n}\\}.$ Then

$r_{Q}(R_{+})=\min\\{n\in{\mathbb{N}}|\ E_{n+1}=E_{n}+\\{0,d\\}\\}.$

###### Proof.

We have

$H_{n+1}=\\{({\alpha},(n+1)d-{\alpha})|\ {\alpha}\in E_{n+1}\\},$
$H_{n}+\\{e_{1},e_{2}\\}=\\{({\alpha},(n+1)d-{\alpha})|\ {\alpha}\in
E_{n}+\\{0,d\\}\\}.$

Therefore, $H_{n+1}=H_{n}+\\{e_{1},e_{2}\\}$ if and only if
$E_{n+1}=E_{n}+\\{0,d\\}$. ∎

We will keep the notations of this section throughout this paper.

##  2\. Case A

In this section we study the ring $R=k[M]$, where $M$ is represented by the
union of a point and an interval (see Figure 2).

Figure 2.

######  Theorem 2.1.

Let $1<a<d$ be integers. Let $R=k[x^{\alpha}y^{d-\alpha}|\
\alpha\in\\{0\\}\cup[a,d]]$ and $Q=(x^{d},y^{d})$. Then $R$ is a Cohen-
Macaulay ring and

$\operatorname{reg}(R)=r_{Q}(R_{+})=\left\lceil\dfrac{d-1}{d-a}\right\rceil.$

###### Proof.

The Cohen-Macaulayness of $R$ follows from [9, Theorem 3.5]. By Proposition
1.4, it remains to show that
$r_{Q}(R_{+})=\left\lceil\dfrac{d-1}{d-a}\right\rceil,$ which will be proved
by using Lemma 1.5.

Let $E_{n}:=\\{{\alpha}|\ x^{\alpha}y^{nd-{\alpha}}\in R\\}$. It is easy to
see that $E_{n}=\bigcup_{i=0}^{n}[ia,id]$. Hence

(2.1) $E_{n+1}=E_{n}\cup[(n+1)a,(n+1)d],$ $\displaystyle E_{n}+\\{0,d\\}$
$\displaystyle=(E_{n}+0)\cup(E_{n}+d)$
$\displaystyle=E_{n}\cup\bigcup_{i=0}^{n}[ia+d,(i+1)d].$

For $i=0,...,n-1$, we have $[ia+d,(i+1)d]\subseteq[(i+1)a,(i+1)d]\subseteq
E_{n}$. Hence

(2.2) $E_{n}+\\{0,d\\}=E_{n}\cup[na+d,(n+1)d].$

Note that

$[(n+1)a,(n+1)d]\setminus[na+d,(n+1)d]=[(n+1)a,na+d-1].$

Then it follows from (2.1) and (2.2) that $E_{n+1}=E_{n}+\\{0,d\\}$ if and
only if

$[(n+1)a,na+d-1]\subseteq E_{n}.$

We have $na+d-1\in E_{n}$ if and only if $na+d-1\in[ia,id]$ for some
$i=0,...,n$, which implies $na+d+1\leq id\leq nd$. Since $na<(n+1)a$,
$[(n+1)a,na+d-1]\subseteq[na,nd]$. Therefore, $[(n+1)a,na+d-1]\subseteq E_{n}$
if and only if $[(n+1)a,na+d-1]\subseteq[na,nd]$. This condition is satisfied
if and only if $na+d-1\leq nd$. Thus, $E_{n+1}=E_{n}+\\{0,d\\}$ if and only if
$\dfrac{d-1}{d-a}\leq n$. By Lemma 1.5, this implies
$r_{Q}(R_{+})=\left\lceil\dfrac{d-1}{d-a}\right\rceil.$ ∎

From Theorem 2.1 we immediately obtain the following result on monomial space
curves.

######  Corollary 2.2.

Let $R=k[x^{d},x^{d-1}y,x^{d-2}y^{2},y^{d}],$ $d\geq 4$, and
$Q=(x^{d},y^{d})$. Then $R$ is a Cohen-Macaulay ring and

$\operatorname{reg}(R)=r_{Q}(R_{+})=\left\lceil\dfrac{d-1}{2}\right\rceil.$

######  Remark 2.3.

Theorem 2.1 also covers the case $R=k[x^{d-\alpha}y^{\alpha}|\
\alpha\in[0,a]\cup\\{d\\}]$ by permuting $x,y$.

##  3\. Case B

In this section we study the ring $R=k[M]$, where $M$ is represented by two
points at both ends and an interval in the middle (see Figure 3). In this
case, $R$ is always a Cohen-Macaulay ring [9, Theorem 2.1]. By Proposition
1.4, this implies $\operatorname{reg}(R)=r_{Q}(R_{+}).$

Figure 3.

If the middle interval consists of one point, we have the following simple
formula for $r_{Q}(R_{+})$.

######  Proposition 3.1.

Let $2\leq a<d$ be intergers such that $d\geq a+2$. Let
$R=k[x^{d},x^{a}y^{d-a},y^{d}]$ and $Q=(x^{d},y^{d})$. Then $R$ is a Cohen-
Macaulay ring and

$\operatorname{reg}(R)=r_{Q}(R_{+})=d/(a,d)-1,$

where $(a,d)$ denotes the greatest common divisor of $a,d$.

###### Proof.

It is easy to see that $r_{Q}(R_{+})$ is the least integer $n$ such that
$(x^{a}y^{d-a})^{n+1}$ is divided by $x^{d}$ or, equivalently, by $y^{d}$.
This number is clearly $d/(a,d)-1$. Actually, $R$ is defined by a binomial of
degree $d/(a,d)-1$. ∎

If the middle interval consists of more than one point, the computation of
$r_{Q}(R_{+})$ becomes very complicated. However, we can give explicit
formulas for $r_{Q}(R_{+})$ in many cases. This is based on the following
observation.

######  Lemma 3.2.

Let $0<a<b$ be integers. For any integer $m\geq\dfrac{a-1}{b-a}$, $n\geq m$,
and any number $c$, we have

$\bigcup_{i=m}^{n}[ia+c,ib+c]=[ma+c,nb+c].$

###### Proof.

We may assume that $n>m$. By induction on $n$ we may assume that

$\bigcup_{i=m}^{n-1}[ia+c,ib+c]=[ma+c,(n-1)b+c].$

Then

$\bigcup_{i=m}^{n}[ia+c,ib+c]=[ma+c,(n-1)b+c]\cup[na+c,nb+c].$

Since $n-1\geq\dfrac{a-1}{b-a}$, $(n-1)b+c\geq na+c$. Hence

$[ma+c,(n-1)b+c]\cup[na+c,nb+c]=[ma+c,nb+c].$

∎

######  Theorem 3.3.

Let $2\leq a<b\leq d-2$ be integers. Let
$R=k[x^{\alpha}y^{d-\alpha}|\alpha\in\\{0,d\\}\cup[a,b]]$ and
$Q=(x^{d},y^{d})$. Then $R$ is a Cohen-Macaulay ring and

  1. (1)

$\operatorname{reg}(R)=r_{Q}(R_{+})=\left\lceil\dfrac{a+d-1}{b}\right\rceil$
if $b\geq 2a-1,$

  2. (2)

$\operatorname{reg}(R)=r_{Q}(R_{+})=\left\lceil\dfrac{2a+d-1}{b}\right\rceil$
if $\dfrac{3a-1}{2}\leq b<2a-1.$

###### Proof.

We only need to prove the formulas for $r_{Q}(R_{+})$. For $i,j\geq 0$, let

$I_{i,j}:=[ia+jd,ib+jd].$

Let $E_{n}:=\\{{\alpha}|\ x^{\alpha}y^{nd-{\alpha}}\in R\\}$. It is easily
seen that

$E_{n}=\bigcup_{i+j\leq n}(i[a,b]+jd)=\bigcup_{i+j\leq n}I_{i,j},$
$E_{n+1}=\bigcup_{i+j\leq
n+1}I_{i,j}=E_{n}\cup\bigcup_{i+j=n+1}I_{i,j}=E_{n}\cup\bigcup_{i=0}^{n+1}I_{i,n+1-i}.$

Notice that $I_{i,j}+0=I_{i,j}$ and $I_{i,j}+d=I_{i,j+1}$. Then

$E_{n}+\\{0,d\\}=\bigcup_{i+j\leq n}(I_{i,j}\cup
I_{i,j+1})=E_{n}\cup\bigcup_{i=0}^{n}I_{i,n+1-i}.$

Therefore, $E_{n+1}=E_{n}+\\{0,d\\}$ if and only if

$I_{n+1,0}=[(n+1)a,(n+1)b]\subseteq E_{n}+\\{0,d\\}.$

We may assume that $n\geq 1$. Then

(3.1) $\begin{split}E_{n}+\\{0,d\\}&=\bigcup_{i+j\leq n}(I_{i,j}\cup
I_{i,j+1})=\bigcup_{i=0}^{n}\bigcup_{j=0}^{n+1-i}I_{i,j}\\\
&=\bigcup_{j=0}^{n+1}I_{0,j}\cup\bigcup_{i=1}^{n}I_{i,0}\cup\bigcup_{j=1}^{n}\bigcup_{i=1}^{n+1-j}I_{i,j}.\end{split}$

If $b\geq 2a-1,$ then $\left\lceil\dfrac{a-1}{b-a}\right\rceil=1$. By Lemma
3.2,

$\displaystyle\bigcup_{i=1}^{n}I_{i,0}$ $\displaystyle=[a,nb],$
$\displaystyle\bigcup_{i=1}^{n+1-j}I_{i,j}$
$\displaystyle=[a+jd,(n+1-j)b+jd].$

Hence we may rewrite (3.1) as

(3.2)
$E_{n}+\\{0,d\\}=\\{0,d,...,(n+1)d\\}\cup[a,nb]\cup\bigcup_{j=1}^{n}[a+jd,(n+1-j)b+jd].$

For any element
$p\in\\{2d,...,(n+1)d\\}\cup\displaystyle\bigcup_{j=1}^{n}[a+jd,(n+1-j)b+jd]$,
we have $p\geq a+d$. If $p\in[(n+1)a,(n+1)b]$, then $p\leq(n+1)b<nb+d$, hence
$p\in[a+d,nb+d].$ From this it follows that

$[(n+1)a,(n+1)b]\cap\big{(}\\{2d,...,(n+1)d\\}\cup\bigcup_{j=1}^{n}[a+jd,(n+1-j)b+jd]\big{)}\subseteq[a+d,nb+d].$

By (3.2), this implies that $[(n+1)a,(n+1)b]\subseteq E_{n}+\\{0,d\\}$ if and
only if

$[(n+1)a,(n+1)b]\subseteq\\{d\\}\cup[a,nb]\cup[a+d,nb+d].$

Since $a<(n+1)a\leq(n-1)a+b+1\leq nb$, we have

$[(n+1)a,(n+1)b]\setminus[a,nb]=[nb+1,(n+1)b].$

Therefore, $[(n+1)a,(n+1)b]\subseteq E_{n}+\\{0,d\\}$ if and only if

(3.3) $[nb+1,(n+1)b]\subseteq\\{d\\}\cup[a+d,nb+d].$

Assume that (3.3) satisfied. Since the interval $[nb+1,(n+1)b]$ contains $b>2$
points, $(n+1)b\in[a+d,nb+d]$. If $nb+1<a+d$, then (3.3) implies
$nb+1=d=a+d-1$. Hence, we get $a=1$, a contradiction. So we must have
$nb+1\geq a+d$. Conversely, if $nb+1\geq a+d$, then
$[nb+1,(n+1)b]\subseteq[a+d,nb+d].$ Therefore, (3.3) is satisfied if and only
if $nb+1\geq a+d$, which is equivalent to $n\geq\dfrac{a+d-1}{b}$.

Summing up, we have $E_{n+1}=E_{n}+\\{0,d\\}$ if and only if
$n\geq\dfrac{a+d-1}{b}$. By Lemma 1.5, this proves statement (1) of Theorem
3.3.

If $\dfrac{3a-1}{2}\leq b<2a-1,$ then $1<\dfrac{a-1}{b-a}\leq 2$. Hence
$\left\lceil\dfrac{a-1}{b-a}\right\rceil=2$. By Lemma 3.2,

$\displaystyle\bigcup_{i=2}^{n}I_{i,0}$ $\displaystyle=[2a,nb],$
$\displaystyle\bigcup_{i=2}^{n+1-j}I_{i,j}$
$\displaystyle=[2a+jd,(n+1-j)b+jd].$

Hence we may rewrite (3.1) as

(3.4) $E_{n}+\\{0,d\\}=\\\
\\{0,d,...,(n+1)d\\}\cup[a,b]\cup[2a,nb]\cup\bigcup_{j=1}^{n}[a+jd,b+jd]\cup\bigcup_{j=1}^{n}[2a+jd,(n+1-j)b+jd].$

Recall that $E_{n+1}=E_{n}+\\{0,d\\}$ if and only if

$[(n+1)a,(n+1)b]\subseteq E_{n}+\\{0,d\\}.$

Let $p$ be an element of $[(n+1)a,(n+1)b]$ such that

$p\in\displaystyle\\{3d,...,(n+1)d\\}\cup\bigcup_{j=2}^{n}[a+jd,b+jd]\cup\bigcup_{j=1}^{n}[2a+jd,(n+1-j)b+jd].$

Then $p\geq 2a+d$. Hence $p\in[2a+d,nb+d]$ because $p\leq(n+1)b<nb+d$. Thus,

$[(n+1)a,(n+1)b]\cap\big{(}\\{3d,...,(n+1)d\\}\cup\bigcup_{j=2}^{n}[a+jd,b+jd]\cup\bigcup_{j=1}^{n}[2a+jd,(n+1-j)b+jd]\big{)}\\\
\subseteq[2a+d,nb+d].$

Since $b<2a-1<(n+1)a$, $[(n+1)a,(n+1)b]\cap[a,b]=\emptyset$. Therefore, using
(3.4) we have $[(n+1)a,(n+1)b]\subseteq E_{n}+\\{0,d\\}$ if and only if

$[(n+1)a,(n+1)b]\subseteq\\{d,2d\\}\cup[2a,nb]\cup[a+d,b+d]\cup[2a+d,nb+d].$

Since $2a\leq(n+1)a\leq(n-2)a+2b+1\leq nb$, we have

$[(n+1)a,(n+1)b]\setminus[2a,nb]=[nb+1,(n+1)b].$

Therefore, $[(n+1)a,(n+1)b]\subseteq E_{n}+\\{0,d\\}$ if and only if

(3.5) $[nb+1,(n+1)b]\subseteq\\{d,2d\\}\cup[a+d,b+d]\cup[2a+d,nb+d].$

Note that $[nb+1,(n+1)b]$ has $b$ points and $\\{d,2d\\}\cup[a+d,b+d]$ has
$b-a+3$ points. Since $2a-1>b\geq 3$, we have $a\geq 3$, which implies
$b-a+3\leq b$. If $[nb+1,(n+1)b]\subseteq\\{d,2d\\}\cup[a+d,b+d]$, we would
get $[nb+1,(n+1)b]=\\{d,2d\\}\cup[a+d,b+d]$, which is a contradiction because
$\\{d,2d\\}\cup[a+d,b+d]$ is not an interval of integral points. Thus,
$[nb+1,(n+1)b]\not\subseteq\\{d,2d\\}\cup[a+d,b+d]$.

Assume that (3.5) is satisfied. Then
$[nb+1,(n+1)b]\cap[2a+d,nb+d]\neq\emptyset$. Hence $(n+1)b\in[2a+d,nb+d]$. If
$nb+1<2a+d$, then $2a+d-1\in\\{2d\\}\cup[a+d,b+d]$. Since $b+d<2a+d-1$, this
implies $2a+d-1=2d$. Hence, $2a-1=d$. Since $b+d+1<2d$, we also have
$b+d+1\not\in\\{2d\\}\cup[2a+d,nb+d]$. From this it follows that $b+d+1<nb+1$.
Hence, $nb+1\in\\{2d\\}\cup[2a+d,nb+d]$. Therefore, $nb+1=2d$, which implies
$n\geq 3$ because $b\leq d-2$. Since $2b\geq 3a-1$, $nb+1\geq 3a+b\geq
4a+1>2d$, a contradiction. So we must have $nb+1\geq 2a+d$. Conversely, if
$nb+1\geq 2a+d$, then $[nb+1,(n+1)b]\subseteq[2a+d,nb+d].$ So we have shown
that (3.5) is satisfied if and only if $nb+1\geq 2a+d$, which is equivalent to
$n\geq\dfrac{2a+d-1}{b}$.

Summing up, we have $E_{n+1}=E_{n}+\\{0,d\\}$ if and only if
$n\geq\dfrac{2a+d-1}{b}$. By Lemma 1.5, this proves statement (2) of Theorem
3.3. ∎

From Theorem 3.3 we immediately obtain the following results on monomial space
curves.

######  Corollary 3.4.

Let $R=k[x^{d},x^{3}y^{d-3},x^{2}y^{d-2},y^{d}]$, $d\geq 5$, and
$Q=(x^{d},y^{d})$. Then $R$ is a Cohen-Macaulay ring and

$\operatorname{reg}(R)=r_{Q}(R_{+})=\left\lceil\dfrac{d+1}{3}\right\rceil.$

######  Corollary 3.5.

Let $R=k[x^{d},x^{4}y^{d-4},x^{3}y^{d-3},y^{d}]$, $d\geq 6$, and
$Q=(x^{d},y^{d})$. Then $R$ is a Cohen-Macaulay ring and

$\operatorname{reg}(R)=r_{Q}(R_{+})=\left\lceil\dfrac{d+5}{4}\right\rceil.$

The proof of Theorem 3.3 leads to the following problem.

######  Question 3.6.

Let $2\leq a<b\leq d-2$ be integers and
$r=\left\lceil\dfrac{a-1}{b-a}\right\rceil$. Let
$R=k[x^{\alpha}y^{d-\alpha}|\alpha\in\\{0,d\\}\cup[a,b]]$ and
$Q=(x^{d},y^{d})$. Is it true that

$\operatorname{reg}(R)=r_{Q}(R_{+})=\left\lceil\dfrac{ra+d-1}{b}\right\rceil?$

##  4\. Case C

In this section we study the ring $R=k[M]$, where $M$ is represented by the
union of two integral intervals which consist of more than one point (see
Figure 4).

Case C: Figure 4.

It is known that a projective monomial curve parametrized by $M$ is smooth if
and only if the two intervals at both ends of $M$ consist of one point.
Hellus, Hoa and Stückrad [4] did give explicit formulas for the reduction
number of a few sporadic smooth monomial curves. The following result is an
easy consequence of [4, Proposition 3.4].

######  Proposition 4.1.

Let $1\leq a<b<d$ be intergers such that $b\geq a+2$. Let
$R=k[x^{\alpha}y^{d-\alpha}|\ \alpha\in[0,a]\cup[b,d]]$ and $Q=(x^{d},y^{d})$.
Then

$\operatorname{reg}(R)=r_{Q}(R_{+})=\begin{cases}&\ \ \
\left\lceil\dfrac{b-1}{a}\right\rceil\ \ \ \ \ \mbox{ if }\ d-b\geq a,\\\
&\left\lceil\dfrac{d-a-1}{d-b}\right\rceil\quad\mbox{ if }\ d-b<a.\end{cases}$

###### Proof.

By symmetry, we may assume that $d-b\geq a$. Then $R$ satisfies the
assumptions of [4, Proposition 3.4]. From this it follows that

$\operatorname{reg}(R)=r_{Q}(R_{+})=\left\lfloor\dfrac{b-a-2}{a}\right\rfloor+2.$

It is easy to check that
$\left\lfloor\dfrac{b-a-2}{a}\right\rfloor+2=\left\lceil\dfrac{b-1}{a}\right\rceil$.
∎

From Proposition 4.1 we immediately obtain the following result on monomial
space curves.

######  Corollary 4.2.

[2, Theorem 3.6(i)] Let $R=k[x^{d},x^{d-1}y,xy^{d-1},y^{d}],$ $d\geq 4$, and
$Q=(x^{d},y^{d})$. Then

$\operatorname{reg}(R)=r_{Q}(R_{+})=d-2.$

######  Remark 4.3.

Under the assumption of Theorem 4.1, $R$ is never a Cohen-Macaulay ring. This
fact follows from [9, Theorem 4.7].

There is the following interesting relationship between the Buchsbaumness of
$R$ and the reduction number.

######  Proposition 4.4.

Let $1\leq a<b<d$ be intergers such that $b\geq a+2$. Let
$R=k[x^{\alpha}y^{d-\alpha}|\ \alpha\in[0,a]\cup[b,d]].$ Then the following
conditions are equivalent:

  1. (1)

$R$ is a Buchsbaum ring,

  2. (2)

$2a+1\geq b$ and $a+d+1\geq 2b$,

  3. (3)

$r_{Q}(R_{+})=2$.

###### Proof.

By [9, Theorem 4.3], $R$ is a Buchsbaum ring if and only if $2a+1\geq b$ and
$a+d+1\geq 2b$.111Actually, this is the case of [9, Corollary 4.3], which
contains some misprints. By symmetry we may assume, without loss of
generality, that $d-b\geq a$. Then
$r_{Q}(R_{+})=\left\lceil\dfrac{b-1}{a}\right\rceil$ by Proposition 4.1. It is
clear that $\left\lceil\dfrac{b-1}{a}\right\rceil=2$ if and only if $2a+1\geq
b$, which implies $a+d+1\geq 2a+b+1\geq 2b$. These facts show that (1)-(3) are
equivalent. ∎

######  Corollary 4.5.

Let $R=k[x^{d},x^{d-1}y,xy^{d-1},y^{d}],$ $d\geq 4$, and $Q=(x^{d},y^{d})$.
Then $R$ is a Buchsbaum ring if and only if $d=4$. In this case,

$\operatorname{reg}(R)=r_{Q}(R_{+})=2.$

##  5\. Case D

In this section we study the ring $R=k[M]$, when $M$ is represented by one
point at one end and two intervals (see Figure 5).

Figure 5.

The following result gives a large class of monomial curves of this case for
which we can compute the reduction number.

######  Theorem 5.1.

Let $1<a\leq b<c<d$ be integers. Let $R=k[x^{\alpha}y^{d-\alpha}|\
\alpha\in\\{0\\}\cup[a,b]\cup[c,d]]$ and $Q=(x^{d},y^{d})$. Assume that $c\leq
2a$ and $2b\leq d$. Then $R$ is a Cohen-Macaulay ring and

$\operatorname{reg}(R)=r_{Q}(R_{+})=\left\lceil\dfrac{a-1}{d-c}\right\rceil+1.$

###### Proof.

By [9, Theorem 3.5], $R$ is a Cohen-Macaulay ring if

$\left\lfloor\dfrac{a}{c-a}\right\rfloor>\min\left\\{\left\lfloor\dfrac{c-b-2}{d-c}\right\rfloor,\left\lfloor\dfrac{b-1}{d-b}\right\rfloor\right\\}.$

This condition is satisfied because

$\dfrac{a}{c-a}\geq\dfrac{a}{2a-a}=1\geq\dfrac{b}{d-b}>\dfrac{b-1}{d-b}.$

By Lemma 1.4, it remains to show that
$r_{Q}(R_{+})=\left\lceil\dfrac{a-1}{d-c}\right\rceil+1,$ which will be proved
by using Lemma 1.5. For $n\geq 0$ let $E_{n}:=\\{{\alpha}|\
x^{\alpha}y^{nd-{\alpha}}\in R\\}$. We have

$E_{n}=\bigcup_{i+j\leq n}(i[a,b]+j[c,d])=\bigcup_{i+j\leq n}[ia+jc,ib+jd].$

From this it follows that

$\displaystyle E_{n+1}$
$\displaystyle=E_{n}\cup\bigcup_{i+j=n+1}[ia+jc,ib+jd]$
$\displaystyle=E_{n}\cup\bigcup_{i=0}^{n+1}[ia+(n+1-i)c,ib+(n+1-i)d].$
$\displaystyle E_{n}+\\{0,d\\}$ $\displaystyle=E_{n}\cup\bigcup_{i+j\leq
n}[ia+jc+d,ib+(j+1)d]$
$\displaystyle=E_{n}\cup\bigcup_{i+j=n}[ia+jc+d,ib+(j+1)d]$
$\displaystyle=E_{n}\cup\bigcup_{i=0}^{n}[ia+(n-i)c+d,ib+(n+1-i)d].$

We have $2[a,b]=[2a,2b]\subseteq[c,d]$ because $c\leq 2a$ and $2b\leq d$.
Therefore, $i[a,b]\subset E_{i-1}$ for $i\geq 2$. Hence,

$\displaystyle[ia+(n-i)c+d,ib+(n+1-i)d]$
$\displaystyle\subset[ia+(n+1-i)c,ib+(n+1-i)d]$
$\displaystyle=i[a,b]+(n+1-i)[c,d]\subset E_{n}$

for $i\geq 2$. From this it follows that

(5.1) $\displaystyle E_{n+1}$
$\displaystyle=E_{n}\cup[(n+1)c,(n+1)d]\cup[a+nc,b+nd],$ (5.2) $\displaystyle
E_{n}+\\{0,d\\}$ $\displaystyle=E_{n}\cup[nc+d,(n+1)d]\cup[a+(n-1)c+d,b+nd].$

By (5.1) we have $E_{n+1}=E_{n}+\\{0,d\\}$ if and only if

$[(n+1)c,(n+1)d]\cup[a+nc,b+nd]\subseteq E_{n}+\\{0,d\\}.$

Let $p$ be an arbitrary element of $[a+nc,b+nd]\cap E_{n}$. Then $p\geq
a+nc>nc$ and $p\leq nd$. Hence,

(5.3) $[a+nc,b+nd]\cap E_{n}\subseteq[nc,nd],$

Using (5.2) we have $[a+nc,b+nd]\subseteq E_{n}+\\{0,d\\}$ if and only if

$[a+nc,b+nd]\subseteq[nc,nd]\cup[nc+d,(n+1)d]\cup[a+(n-1)c+d,b+nd].$

It is easy to check that

$[a+nc,b+nd]\cap[nc+d,(n+1)d]\subseteq[nc+d,b+nd]\subseteq[a+(n-1)c+d,b+nd].$

Therefore, $[a+nc,b+nd]\subseteq E_{n}+\\{0,d\\}$ if and only if

$[a+nc,b+nd]\subseteq[nc,nd]\cup[a+(n-1)c+d,b+nd].$

The last condition is satisfied if and only if

$[nc,nd]\cup[a+(n-1)c+d,b+nd]=[nc,b+nd],$

which is equivalent to $nd\geq a+(n-1)c+d-1$.

Similarly as above, we have $[(n+1)c,(n+1)d]\subseteq E_{n}+\\{0,d\\}$ if and
only if

$[(n+1)c,(n+1)d]\subseteq[nc,nd]\cup[nc+d,(n+1)d]\cup[a+(n-1)c+d,b+nd].$

If $nd\geq a+(n-1)c+d-1$, then $b+nd\geq nc+d-1$ because $a+b\geq 2a\geq c$.
From this it follows that

$\displaystyle[nc,nd]\cup[nc+d,(n+1)d]\cup[a+(n-1)c+d,b+nd]$
$\displaystyle=[nc,(n+1)d]$ $\displaystyle\supseteq[(n+1)c,(n+1)d].$

Therefore, $[(n+1)c,(n+1)d]\subseteq E_{n}+\\{0,d\\}$ if $nd\geq
a+(n-1)c+d-1$, which is equivalent to $n\geq\dfrac{d-c+a-1}{d-c}$.

Summing up, we have $E_{n+1}=E_{n}+\\{0,d\\}$ if and only if
$n\geq\dfrac{d-c+a-1}{d-c}$. By Lemma 1.5, this implies
$r_{Q}(R_{+})=\left\lceil\dfrac{d-c+a-1}{d-c}\right\rceil=\left\lceil\dfrac{a-1}{d-c}\right\rceil+1.$
∎

From Theorem 5.1 we immediately obtain the following consequence on monomial
space curves.

######  Corollary 5.2.

Let $R=k[x^{d},x^{d-1}y,x^{a}y^{d-a},y^{d}]$, $d\geq 5$,
$a=\left\lceil\dfrac{d-1}{2}\right\rceil$, and $Q=(x^{d},y^{d})$. Then $R$ is
a Cohen-Macaulay ring and

$\operatorname{reg}(R)=r_{Q}(R_{+})=\left\lceil\dfrac{d-1}{2}\right\rceil.$

##  6\. Case E

In this section we study the ring $R=k[M]$ in the case $M$ is represented by
the union of three intervals, where the two intervals at both ends consist of
more than one point (see Figure 6).

Figure 6.

Using [4, Proposition 3.4] we obtain the following partial result.

######  Proposition 6.1.

Let $1\leq a<b\leq c<e<d$ be intergers such that $d-e\leq a$ and $b-a\geq
e-c$. Let $R=k[x^{\alpha}y^{d-\alpha}|\ \alpha\in[0,a]\cup[b,c]\cup[b,d]]$ and
$Q=(x^{d},y^{d})$. Then

$\operatorname{reg}(R)=r_{Q}(R_{+})=\left\lceil\dfrac{b-1}{a}\right\rceil.$

###### Proof.

Actually, [4, Proposition 3.4] gives the formula

$\operatorname{reg}(R)=r_{Q}(R_{+})=\left\lfloor\dfrac{b-a-2}{a}\right\rfloor+2.$

It is easy to check that
$\left\lfloor\dfrac{b-a-2}{a}\right\rfloor+2=\left\lceil\dfrac{b-1}{a}\right\rceil$.
∎

The following result gives another large class of monomial curves for which we
can compute the reduction number.

######  Theorem 6.2.

Let $1\leq a<b\leq c<e<d$ be intergers such that $e\leq 2b$ and $2c\leq a+d$.
Let $R=k[x^{\alpha}y^{d-\alpha}|\ \alpha\in[0,a]\cup[b,c]\cup[b,d]]$ and
$Q=(x^{d},y^{d})$. Then

$r_{Q}(R_{+})=\max\left\\{\left\lceil\dfrac{b-1}{a}\right\rceil,\left\lceil\dfrac{e-c+a-1}{a}\right\rceil,\left\lceil\dfrac{d-c-1}{d-e}\right\rceil,\left\lceil\dfrac{d-e+b-a-1}{d-e}\right\rceil\right\\}.$

###### Proof.

For $n\geq 0$ let $E_{n}:=\\{{\alpha}|\ x^{\alpha}y^{nd-{\alpha}}\in R\\}$ and
$F_{n}:=\\{{\alpha}|\ x^{\alpha}y^{nd-{\alpha}}\in S\\},$ where
$S=k[x^{\alpha}y^{d-\alpha}|\ \alpha\in[0,a]\cup[e,d]]$. It is easy to see
that

$E_{n}=\bigcup_{i=0}^{n}(F_{n-i}+i[b,c]).$

The assumption $e\leq 2b$ and $2c\leq a+d$ implies
$2[b,c]=[2b,2c]\subseteq[e,a+d]=[0,a]+[e,d]\subseteq F_{2}$. From this it
follows that

$E_{n}=F_{n}\cup(F_{n-1}+[b,c])$

for $n\geq 1$. Therefore,

(6.1) $\displaystyle E_{n+1}$ $\displaystyle=F_{n+1}\cup(F_{n}+[b,c]),$ (6.2)
$\displaystyle E_{n}+\\{0,d\\}$
$\displaystyle=(F_{n}+\\{0,d\\})\cup(F_{n-1}+[b,c]+\\{0,d\\}).$

We have

$F_{n}=\bigcup_{i+j=n}(i[0,a]+j[e,d])=\bigcup_{i+j=n}[je,ia+jd]=\bigcup_{j=0}^{n}[je,(n-j)a+jd].$

From this it follows that

(6.3) $\displaystyle F_{n+1}$
$\displaystyle=[0,(n+1)a]\cup\bigcup_{j=1}^{n}[je,(n+1-j)a+jd]\cup[(n+1)e,(n+1)d],$
(6.4) $\displaystyle F_{n}+[b,c]$
$\displaystyle=[b,na+c]\cup\bigcup_{j=1}^{n-1}[b+je,c+(n-j)a+jd]\cup[b+ne,c+nd].$

Note that $F_{n}+\\{0,d\\}=(F_{n}+0)\cup(F_{n}+d)$. Then

(6.5)
$F_{n}+\\{0,d\\}=\bigcup_{j=0}^{n}[je,(n-j)a+jd]\cup\bigcup_{j=0}^{n}[je+d,(n-j)a+(j+1)d].$

For $j=1,...,n$, we have $(n-j)a+jd\geq(j-1)e+d$, hence

$[je,(n-j)a+jd]\cup[(j-1)e+d,(n-j+1)a+jd]=[je,(n-j+1)a+jd].$

Therefore, we may rewrite (6.5) as

(6.6)
$F_{n}+\\{0,d\\}=[0,na]\cup\bigcup_{j=1}^{n}[je,(n+1-j)a+jd]\cup[ne+d,(n+1)d],$

From this it follows that

(6.7) $F_{n-1}+[b,c]+\\{0,d\\}=\\\
[b,(n-1)a+c]\cup\bigcup_{j=1}^{n-1}[b+je,(n-j)a+c+jd]\cup[b+(n-1)e+d,c+nd].$

Comparing (6.3) and (6.4) with (6.6) and (6.7) we have

$\displaystyle
F_{n+1}\setminus(F_{n}+\\{0,d\\})\subseteq([0,(n+1)a]\cup[(n+1)e,(n+1)d]),$
$\displaystyle(F_{n}+[b,c])\setminus(F_{n-1}+[b,c]+\\{0,d\\})\subseteq[b,na+c]\cup[b+ne,c+nd].$

From (6.1) and (6.2) it follows that $E_{n+1}=E_{n}+\\{0,d\\}$ if and only if

(6.8) $[0,(n+1)a]\cup[(n+1)e,(n+1)d]\cup[b,na+c]\cup[ne+b,nd+c]\subseteq
E_{n}+\\{0,d\\}.$

Now we are going to check when $[0,(n+1)a]\cup[b,na+c]$ is contained in
$E_{n}+\\{0,d\\}.$ Let $p$ is an element of $[0,(n+1)a]$. If
$p\in\displaystyle\bigcup_{j=1}^{n}[je,(n+1-j)a+jd]$ or $p\in[ne+d,(n+1)d]$,
then $p\geq e$, which implies $p\in[e,na+d]$ because $p\leq(n+1)a<na+d$.
Therefore, using (6.6) we have

(6.9) $[0,(n+1)a]\cap(F_{n}+\\{0,d\\})\subseteq[0,na]\cup[e,na+d].$

Similarly, if $p\in\displaystyle\bigcup_{j=1}^{n-1}[b+je,(n-j)a+c+jd]$ or if
$p\in[b+(n-1)e+d,c+nd]$, then $p\in[e,na+d]$. Therefore, using (6.7) we have

(6.10)
$[0,(n+1)a]\cap(F_{n-1}+[b,c]+\\{0,d\\})\subseteq[b,(n-1)a+c]\cup[e,na+d].$

By (6.2), it follows that $[0,(n+1)a]\subseteq F_{n}+\\{0,d\\}$ if and only if

(6.11) $[0,(n+1)a]\subseteq[0,na]\cup[b,(n-1)a+c]\cup[e,na+d].$

Similarly, we can show that $[b,na+c]\subseteq F_{n}+\\{0,d\\}$ if and only if

(6.12) $[b,na+c]\subseteq[0,na]\cup[b,(n-1)a+c]\cup[e,na+d].$

It is easily seen that if (6.11) is satisfied, then $na+1\geq b$ and that if
(6.12) is satisfied, then $(n-1)a+c+1\geq e$. Conversely, if $na+1\geq b$ and
$(n-1)a+c+1\geq e$, then

$[0,na]\cup[b,(n-1)a+c]\cup[e,na+d]=[0,na+d]\supseteq[0,(n+1)a]\cup[b,na+c],$

hence (6.11) and (6.12) are satisfied. Thus, $[0,(n+1)a]\cup[b,na+c]\subseteq
E_{n}+\\{0,d\\}$ if and only if

$n\geq\max\left\\{\dfrac{b-1}{a},\dfrac{e-c+a-1}{a}\right\\}.$

By symmetry, we have $[(n+1)e,(n+1)d]\cup[ne+b,nd+c]\subseteq E_{n}+\\{0,d\\}$
if and only if

$n\geq\max\left\\{\dfrac{d-c-1}{d-e},\dfrac{d-e+b-a-1}{d-e}\right\\}.$

Therefore, (6.9) and hence the condition $E_{n+1}=E_{n}+\\{0,d\\}$ are
satisfied if and only if

$n\geq\max\left\\{\dfrac{b-1}{a},\dfrac{e-c+a-1}{a},\dfrac{d-c-1}{d-e},\dfrac{d-e+b-a-1}{d-e}\right\\}.$

By Lemma 1.5, this implies

$r_{Q}(R_{+})=\max\left\\{\left\lceil\dfrac{b-1}{a}\right\rceil,\left\lceil\dfrac{e-c+a-1}{a}\right\rceil,\left\lceil\dfrac{d-c-1}{d-e}\right\rceil,\left\lceil\dfrac{d-e+b-a-1}{d-e}\right\rceil\right\\}.$

∎

We are not able to give an answer to the following question.

######  Question 6.3.

Is it true that $\operatorname{reg}(R)=r_{Q}(R_{+})$ under the assumption of
Theorem 6.2?

Acknowledgement. This paper is partially supported by grant 101.04-2019.313 of
Vietnam National Foundation for Science and Technology Development.

## References

  * [1] I. Bermejo, E. García-Llorente, I. García-Marco, M. Morales, Noether resolutions in dimension 2, J. Algebra 482 (2017), 398–426.
  * [2] I. Bermejo, P. Gimenez and M. Morales, Castelnuovo-Mumford regularity of projective monomial varieties of codimension two, J. Symbolic Comput. 41 (2006), no. 10, 1105–1124.
  * [3] L. Gruson, R. Lazarsfeld and C. Peskine, On a theorem of Castelnuovo, and the equations defining space curves, Invent. Math. 72 (1983), no. 3, 491–506.
  * [4] M. Hellus, L. T. Hoa, J. Stückrad, Castelnuovo-Mumford regularity and the reduction number of some monomial curves, Proc. Amer. Math. Soc. 138 (2010), 27–35.
  * [5] S. Huckaba, Reduction numbers for ideals of higher analytic spread, Math. Proc. Cambridge Philos. Soc. 102 (1987), 49–57.
  * [6] S. L’vovsky, On inflection points, monomial curves and hypersurfaces containing projective curves, Math. Ann. 306 (1996), 719–735.
  * [7] D.G. Northcott, D. Rees, Reductions of ideals in local rings, Proc. Cambridge Philos. Soc. 50 (1954), 145–158.
  * [8] J. Stückrad, W. Vogel, Buchsbaum rings and applications. An interaction between algebra, geometry, and topology. Mathematische Monographien 21, VEB Deutscher Verlag der Wissenschaften, Berlin, 1986.
  * [9] Ngo Viet Trung, Projections of one-dimensional Veronese varieties, Math. Nachr. 118 (1984), 47–67.
  * [10] Ngo Viet Trung, Reduction exponent and degree bound for the defining equations of graded rings, Proc. Amer. Math. Soc. 101 (1987), 229–236.
  * [11] Ngo Viet Trung, The Castelnuovo regularity of the Rees algebra and the associated graded ring, Trans. Amer. Math. Soc. 350 (1998), 2813–2832.
  * [12] Ngo Viet Trung, Constructive characterization of the reduction numbers, Compositio Math. 137 (2003), 99–113.
  * [13] Ngo Viet Trung, Castelnuovo-Mumford regularity and related invariants, in: Commutative algebra and combinatorics, Ramanujan Math. Soc. Lect. Notes Ser. 4, 2007, 157–180.
  * [14] W. Vasconcelos, The reduction number of an algebra, Compositio Mathematica 104 (1996), p. 189–197.
  * [15] W. Vasconcelos, Integral closure. Rees algebras, multiplicities, algorithms, Springer, 2005.


20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\overline{a}\Leftarrow\Delta$}}}}\vbox{}}}\over\hbox{\hskip
24.23608pt\vbox{\vbox{}\hbox{\hskip-24.23607pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\mathit{K}\,\overline{a}\Rightarrow\mathit{T}\,$}}}}}}$

We need to check that list against the telescope for the constructor, using
the judgment $\Gamma\vdash\overline{a}\Leftarrow\Delta$.

In this judgment, each argument must have the right type. Furthermore, because
of dependency, we substitute that argument for the variable in the rest of the
telescope.

tele-sig $\displaystyle\displaystyle{\hbox{\hskip
56.25002pt\vbox{\hbox{\hskip-56.25002pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\mathit{a}:\mathit{A}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\overline{a}\Leftarrow\Delta[\mathit{a}/\mathit{x}]$}}}}\vbox{}}}\over\hbox{\hskip
32.56944pt\vbox{\vbox{}\hbox{\hskip-32.56944pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\mathit{a}\,\overline{a}\Leftarrow\mathit{x}:\mathit{A},\Delta$}}}}}}$

Furthermore, we also substitute when the telescope contains definitions.

tele-def $\displaystyle\displaystyle{\hbox{\hskip
31.04167pt\vbox{\hbox{\hskip-31.04167pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\overline{a}\Leftarrow\Delta[\mathit{a}/\mathit{x}]$}}}\vbox{}}}\over\hbox{\hskip
30.48613pt\vbox{\vbox{}\hbox{\hskip-30.48613pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\overline{a}\Leftarrow\mathit{x}=\mathit{a},\Delta$}}}}}}$

When we get to the end of the argument list (i.e. there are no more arguments)
we should also get to the end of the telescope.

tele-nil $\displaystyle\displaystyle{\hbox{}\over\hbox{\hskip
12.56943pt\vbox{\vbox{}\hbox{\hskip-12.56943pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\Leftarrow$}}}}}}$

$\Gamma\vdash\overline{a}\Leftarrow\Delta$ | tcArgTele | Type check a list of arguments against a telescope
---|---|---
$\Gamma\vdash\mathit{pat}:\mathit{A}\Rightarrow\Delta$ | declarePat | Create telescope containing all of the
|  | variables from the pattern
$\vdash\mathit{a}\sim\mathit{b}\Rightarrow\Delta$ | unify | Compare two terms to create a list of definitions
$\Delta[\mathit{a}/\mathit{x}]$ | doSubst | Substitute through a telescope
$\Delta_{{\mathrm{1}}}[\overline{a}/\Delta_{{\mathrm{2}}}]$ | substTele | Substitute a list of args for the variables
|  | declared in a telescope
Figure 8: Functions for checking datatypes and case expressions

Figure 8 lists the relevant judgments for type checking the use of datatypes
and the corresponding functions in the pi-forall implementation. The
$\Gamma\vdash\overline{a}\Leftarrow\Delta$ judgment, described above, is
implemented by the tcArgTele function in TypeCheck.hs. This function has the
following type in the implementation: (For reasons that we explain below, we
have a special type Arg for the arguments to the data constructor.)

    tcArgTele :: [Arg] -> Telescope -> TcMonad [Arg]

The tcArgTele also function relies on the substitution function for
telescopes, written $\Delta[\mathit{a}/\mathit{x}]$ in the rules above:

    doSubst :: [(TName, Term)] -> [Decl] -> TcMonad [Assn]

This substitution function propagates the substitution through the telescope.

###  9.4 Pattern matching with dirt simple datatypes

In your homework assignment, we used a special if term to eliminate boolean
types. Now, we would like to replace that with the more general case
expression, of the form
$\mathbf{case}\,\mathit{a}\,\mathbf{of}\,\\{\,\overline{\mathit{pat_{\mathit{i}}}\to\mathit{a_{\mathit{i}}}}^{\,\mathit{i}}\,\\}$
that works with any form of datatype. What should the typing rule for that
sort of expression look like? There is a lot of work to do.

c-case-simple $\displaystyle\displaystyle{\hbox{\hskip
121.06956pt\vbox{\hbox{\hskip-18.81944pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\mathit{a}\Rightarrow\mathit{A}$}}}\vbox{\hbox{\hskip-121.06956pt\hbox{\hbox{$\displaystyle\displaystyle\mathbf{whnf}\
\mathit{A}\leadsto\mathit{T}\,$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\overline{\Gamma\vdash\mathit{pat_{\mathit{i}}}:\mathit{T}\,\Rightarrow\Delta_{\mathit{i}}}^{\,\mathit{i}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\overline{\vdash\mathit{a}\sim\mathit{pat_{\mathit{i}}}\Rightarrow\Delta^{\prime}_{\mathit{i}}}^{\,\mathit{i}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\overline{\Gamma,\Delta_{\mathit{i}},\Delta^{\prime}_{\mathit{i}}\vdash\mathit{a_{\mathit{i}}}:\mathit{A}}^{\,\mathit{i}}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\mathbf{branches}\,\mathbf{exhaustive}$}}}}}}}\vbox{}}}}\over\hbox{\hskip
44.87492pt\vbox{\vbox{}\hbox{\hskip-44.87492pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\mathbf{case}\,\mathit{a}\,\mathbf{of}\,\\{\,\overline{\mathit{pat_{\mathit{i}}}\to\mathit{a_{\mathit{i}}}}^{\,\mathit{i}}\,\\}\Leftarrow\mathit{A}$}}}}}}$

Mathematically, this rule first checks that the scrutinee has the type of some
datatype $\mathit{T}$. Then, for each case of the pattern match, this rule
looks at the pattern $\mathit{pat_{\mathit{i}}}$ and uses the context to
calculate a telescope $\Delta_{\mathit{i}}$ containing declarations of all of
the variables bound in that pattern. That telescope is added to the context to
type check each branch $\mathit{a_{\mathit{i}}}$ against the type of the
entire expression $\mathit{A}$. Furthermore, when checking the type of each
branch, we can refine that type because we know that the scrutinee is equal to
the pattern. To reflect this information during type checking, we also
construct the telescope $\Delta^{\prime}_{\mathit{i}}$.

How do we implement this rule in our language? The general strategy is as
follows:

  1. 1.

Infer type of the scrutinee $\mathit{a}$ (inferType)

  2. 2.

Make sure that the inferred type is some type constructor $\mathit{T}$
(ensureTCon)

  3. 3.

For each case alternative $\mathit{p_{\mathit{i}}}\to\mathit{a_{\mathit{i}}}$:

     * •

Create the declarations $\Delta_{\mathit{i}}$ for the variables in the pattern
(declarePat)

     * •

Create a list of definitions $\Delta^{\prime}_{\mathit{i}}$ that follow from
unifying the scrutinee $\mathit{a}$ with the pattern $\mathit{p_{\mathit{i}}}$
(unify)

     * •

Check the body of the case $\mathit{a_{\mathit{i}}}$ in the extended context
against the expected type $\mathit{A}$ (checkType)

  4. 4.

Make sure that the patterns in the cases are exhaustive (exhausivityCheck)

###  9.5 Datatypes with parameters

The first extension of the above scheme is for _parameterized datatypes_. For
example, in pi-forall we can define the Maybe type with the following
declaration. The type parameter A can be referred to in any of the telescopes
for the data constructors.

⬇

data Maybe (A : Type) : Type where

Nothing

Just of (A)

Because this is a dependently-typed language, the variables in the telescope
can be referred to later in the telescope. For example, with parameters, we
can implement $\Sigma$-types as a datatype, instead of making them primitive.

⬇

data Sigma (A: Type) (B : A $\rightarrow\;$ Type) : Type

Prod of (x:A) (B)

The general form of datatype declaration with parameters includes a telescope
for the type constructor, as well as a telescope for each of the data
constructors.

⬇

data T D : Type where

K1 of D1

...

Kn of Dn

That means that when we check an occurrence of a type constructor, we need to
make sure that its actual arguments match up with the parameters in the
telescope. For this step, we can reuse the same argument checking judgment as
we used for data constructor applications.

i-tcon $\displaystyle\displaystyle{\hbox{\hskip
69.44427pt\vbox{\hbox{\hskip-69.44426pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{T}:\Delta\to\,\mathbf{Type}\,\in\,\Gamma$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\overline{a}\Leftarrow\Delta$}}}}\vbox{}}}\over\hbox{\hskip
30.76389pt\vbox{\vbox{}\hbox{\hskip-30.76389pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\mathit{T}\,\overline{a}\Rightarrow\mathbf{Type}$}}}}}}$

Now, to type check data constructor applications for parameterized types, we
need to modify the typing rule for data constructors. This rule below
separates the type constructor telescope ($\Delta_{{\mathrm{1}}}$) from the
data constructor telescope $\Delta_{{\mathrm{2}}}$ when looking up the data
constructor from the context. When type checking the arguments of the data
constructor $\overline{a}$, we first substitute the arguments of the type
constructor $\overline{b}$ into the data constructor telescope.

c-dcon $\displaystyle\displaystyle{\hbox{\hskip
85.73877pt\vbox{\hbox{\hskip-85.73877pt\hbox{\hbox{$\displaystyle\displaystyle\mathit{K}:\Delta_{{\mathrm{1}}}\to\Delta_{{\mathrm{2}}}\to\mathit{T}\,\,\in\,\Gamma$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\overline{a}\Leftarrow\Delta_{{\mathrm{2}}}[\overline{b}/\Delta_{{\mathrm{1}}}]$}}}}\vbox{}}}\over\hbox{\hskip
26.73608pt\vbox{\vbox{}\hbox{\hskip-26.73608pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash\mathit{K}\,\overline{a}\Leftarrow\mathit{T}\,\overline{b}$}}}}}}$

For example, if we are trying to check the expression Just True, with expected
type Maybe Bool, we will first see that Maybe requires the telescope (A :
Type). That means we need to substitute Bool for A in (_ : A), the telescope
for Just. That produces the telescope (_ : Bool), which we will use to check
the argument True.

In TypeCheck.hs, the function

    substTele :: [Decl] -> [Arg] -> [Decl] -> TcMonad [Decl]

implements this operation of substituting the actual data type arguments for
the parameters.

Note that by checking the type of data constructor applications (instead of
inferring them) we don’t need to explicitly provide the parameters to the data
constructor. The type system can figure them out from the provided type.

Also, note that checking mode also enables _data constructor overloading_. In
other words, we can have multiple datatypes that use the same data
constructor. Having the type available allows us to disambiguate.

For added flexibility, we can also add code to _infer_ the types of data
constructors when they are not actually parameterized and when there is no
ambiguity due to overloading. For example, if we see True, we would like to
infer that it has type Bool without any annotation.

###  9.6 Datatypes with indices

The final step is to index our datatypes with constraints on the parameters.
Indexed types let us express inductively defined relations, such as beautiful
from Software Foundations.

    Inductive beautiful : nat -> Prop :=
      b_0 : beautiful 0
    | b_3 : beautiful 3
    | b_5 : beautiful 5
    | b_sum : forall n m, beautiful n -> beautiful m -> beautiful (n+m).

Even though beautiful has type nat -> Prop, we call the nat argument an
_index_ instead of a _parameter_ because it varies in the result type of each
data constructor. It is not used uniformly in each case.

In pi-forall, we implement indices by explicitly _constraining_ parameters.
These constraints are just expressed as equalities written in square brackets.
In other words, we define beautiful this way:

⬇

data Beautiful (n : Nat) : Type where

B0 of [n = 0]

B3 of [n = 3]

B5 of [n = 5]

Bsum of (m1:Nat)(m2:Nat)(Beautiful m1)(Beautiful m2)[m = m1+m2]

Constraints can appear anywhere in the telescope of a data constructor.
However, they are not arbitrary equality constraints—we want to consider them
as deferred substitutions. Therefore, the term on the left must always be a
variable.

These constraints interact with the type checker in a few places:

  * •

When we use data constructors we need to be sure that the constraints are
satisfied, by appealing to definitional equality when we are checking
arguments against a telescope (in tcArgTele).

  * •

When we substitute through telescopes (in doSubst), we may need to rewrite a
constraint x = b if we substitute for x.

  * •

When we add the pattern variables to the context in each alternative of a case
expression, we need to also add the constraints as definitions (see
declarePats).

For example, if we check an occurrence of B3, i.e.

⬇

threeIsBeautiful : Beautiful 3

threeIsBeautiful = B3

this requires substituting 3 for n in the telescope [n = 3]. That produces an
empty telescope.

####  9.6.1 Homework: finite numbers in FinHw.pi

The module FinHw.pi declares the type of numbers that are drawn from some
bounded set. For example, the type Fin 1 only includes one number (called
Zero), Fin 2 includes two numbers, etc. More generally, Fin n is the type of
all natural numbers smaller than n, i.e. of all valid indices for lists of
size n.

⬇

data Fin (n : Nat) : Type where

Zero of (m:Nat)[n = Succ m]

Succ of (m:Nat)[n = Succ m] (Fin m)

The file FinHw.pi includes a number of definitions that use these types. Two
of these definitions are marked with TRUSTME. Replace these expressions with
appropriate definitions.

###  9.7 Irrelevance and datatypes

Datatypes may wish to mark some of their arguments as irrelevant, so that
these components of the data structure can be erased at run time. For example,
the Vec type in Section 2 marked the length of the tail of the vector as
irrelevant in the telescope for the Cons constructor.

The mechanisms that we have set up so far extend naturally to irrelevant data
constructor arguments. Note however: we can only erase _data_ constructor
arguments; pi-forall does not allow marking arguments to _type_ constructors
as irrelevant. This is not a significant limitation as we almost always want
these arguments to actually be relevant—we don’t want to equate Vec 0Int with
Vec 1 Bool. However, these type parameters are never relevant when they are
used with data constructors—we don’t even include them in the abstract syntax.

####  9.7.1 Homework: Erasure and Indexed datatypes: finite numbers in
FinHw.pi

Now take your code in FinHw.pi and see if you can mark some of the components
of the Fin datatype as erasable. Where do we need to pass the length of a list
around at run time?

##  10 Where to go next?

###  10.1 Other tutorials on the implementation of dependent type systems

  * •

A. Löh, C. McBride, W. Swierstra, _A tutorial implementation of a dependently
typed lambda calculus_ [LMS10].

This tutorial implements the “LambdaPi” language and is accompanied by a
Haskell implementation available online 161616https://www.andres-
loeh.de/LambdaPi/. The tutorial starts with an implementation of the simply-
typed lambda calculus, using a locally nameless representation and
bidirectional type checking, and then extends to core type system with type-
in-type and uses normalization-by-evaluation for equivalence checking. It also
adds natural numbers and vectors along with their eliminators, but does not
include a general form of (inductive) datatypes.

  * •

Lennart Augustsson. _Simple, Easier!_ [Aug07]

The goal of Augustsson’s tutorial, inspired by an earlier version of LambdaPi,
is to be the simplest implementation possible. Therefore, he uses a string
representation of variables and binding and weak-head normalization for the
implementation of equality. His version is a Haskell implementation of
Barendregt’s lambda cube [Bar93].

  * •

Coquand, Kinoshita, Nordstrom, Takeyama. _A simple type-theoretic language:
Mini-TT_ [CKNT09]

Coquand et al. describe another Haskell implementation of dependent types,
called “Mini-TT”, which shows how to implement (in about 400 lines of code) a
small dependently-typed language that includes $\Sigma$-types, void, unit, and
sums. The language does not include propositional equality or indexed
datatypes, nor does it enforce termination. The implementation uses strings to
represent variable binding, which are converted to de Bruijn indices during
normalization-by-evaluation.

  * •

Andrej Bauer, _How to implement dependent type theory_ [Bau12]

Bauer explores several different implementations of dependent type theory in a
series of blog posts using the OCaml language. The first version uses a named
representation (i.e., strings) and generates fresh names during substitution
and alpha-equality. This version uses full normalization to implement
definitional equality. Then, in the second version, Bauer revises the
implementation to use normalization by evaluation. In the third version, he
revises again to use de Bruijn indices, explicit substitutions, and switches
back to weak-head normalization.

  * •

Tiark Rompf, _Implementing Dependent Types_ [Rom20].

In a recent blog post tutorial, Rompf uses Javascript to implement a core
dependent type theory using higher-order abstract syntax.

  * •

Andras Kovacs, _Elaboration Zoo_ [Kov]

Kovacs’ GitHub repository includes several different implementations of
evaluation and type checking for a minimal dependently typed languages. These
implementations are accompanied by video recordings of a seminar that goes
over this code. Notably, this tutorial includes implicit argument synthesis
via (higher-order) unification.

###  10.2 Related work for pi-forall

##### Section 3: Core Dependent Types

Because they lack a rule for conversion, the typing rules for the core
dependent type system presented in Section 3 do not correspond to any existing
type system. However, jumping ahead, the core language with the inclusion of
conversion (rule t-conv) has been well-studied.

As a foundation of logic, the inclusion of rule rule t-type makes the system
inconsistent. Indeed, Martin-Löf’s original formulation of type theory [ML71]
included this rule until the resulting paradox was demonstrated by Girard.
This inconsistency was resolved in later versions of the systems [ML75] and in
the Calculus of Constructions [CH86] by stratifying $\mathbf{Type}$: first
into two levels and then into an infinite hierarchy of universes [Luo90].

The inconsistency of this system as a logic does not prevent its use as a
programming language. Cardelli [Car86] showed that this language was type
sound and explored applications for programming.

##### Section 4: Bidirectional type checking

The expressiveness of dependently-typed programming languages put them out of
reach of the Hindley Milner type inference algorithm found in Haskell and ML.
As a result, type checkers and elaborators for these languages must abandon
complete type inference and require users to annotate their code.

Bidirectional type systems provide a platform for propagating type annotations
through judgments, and notably, support a syntax-directed specification of
where to apply the conversion rule during type checking. As a result, such
type systems are frequently used as the basis for type checking, with
elaboration for implicit arguments layered on top.

Pierce and Turner [PT00] popularized the use of bidirectional type systems, in
the context of polymorphic languages with subtyping. The Haskell language uses
bidirectional type checking layered on top of Hindley-Milner unification in
order to support type inference for higher-rank polymorphism [PVWS07]. This
type system extension allows functions to take polymorphic functions as
arguments. Notably, the paper includes a well-documented reference
implementation of the type system in the appendix.

David Christiansen’s tutorial [Chr13] introduces the idea of bidirectional
type checking as an independent topic. For another description of the role of
bidirectional type systems in the context of dependent types, see Löh, McBride
and Swierstra’s tutorial [LMS10]. Unlike pi-forall, this tutorial separates
the syntax of terms based whether they are inferable or checkable.

Finally, Dunfield and Krishnaswami’s extensive survey paper [DK21] catalogs
and organizes recent results in this area.

##### Section 6: Definitional equality

Many implementations, such as Coq and Agda, use a procedure called
_normalization-by-evaluation_ to decide whether two terms are equivalent. In
general, this algorithm is favored due to its speed (it can avoid
interpretation overhead by relying on an evaluator) and because it can be
extended with typed equalities that derive from $\eta$-equivalence. In Coq,
this procedure is implemented by compilation to OCaml bytecode, through the
procedure described in this paper [GL02]. More detailed information about NbE
is available in Abel’s habilitation thesis [Abe13]. A simple implementation of
NbE as described in this document is available
171717https://github.com/jozefg/nbe-for-mltt.

##### Sections 7 and 9: Dependently-typed pattern matching

The implementation of indexed datatypes in pi-forall is inspired by the
compilation of _Generalized Algebraic Datatypes_ in Haskell [VPJSS11, VWPJ06].
The distinguishing feature of this formalization is that internally, datatype
indices are represented by constrained parameters and so are an extension of
the parameterized recursive sums of products found in functional programming
languages.

In contrast, the theory of inductive datatypes found in Coq and Agda must
ensure that they cannot be used to implement nonterminating functions. This
means that there are several restrictions that must be applied: inductive
datatypes must be strictly positive, their eliminators must be defined
separately, and they must satisfy constraints based on universe-levels. For
more information about how inductive definitions work in these settings, see
the Coq 181818https://coq.inria.fr/refman/language/core/inductive.html#theory-
of-inductive-definitions or Agda
191919https://agda.readthedocs.io/en/v2.6.2.2/language/data-types.html
manuals.

##### Section 8: Compile-time and run-time irrelevance

The implementation of irrelevance in pi-forall is inspired by the Dependent
Dependency Calculus (DDC) [CEIW22], a pure type system parameterized by a
dependency lattice. The selection of the lattice determines the precise form
of irrelevance described by the type system: does the system include run-time
irrelevance only, compile-time irrelevance only, both sorts of irrelevance
combined together (as in pi-forall), or both sorts and allow them to be
distinguished.

##### Compile-time irrelevance only

Pfenning [Pfe01] used a modal type system to identify arguments that can be
ignored when checking equivalence. This system, extended by Abel and Scherer
[AS12], became the basis for Agda’s implementation of compile-time
irrelevance.

##### Run-time irrelevance only

The Coq proof assistance distinguishes the Prop universe from the Type
universe for several reasons. However, one feature of this distinction is that
all terms in the Prop universe can be erased prior to execution, leading to
faster evaluation of extracted code.

More recently, _quantitative type theory_ [Atk18] unifies run-time irrelevance
and linear type systems by restricting the number of times that variables may
be used in a given context. This resulting system has been adopted for the
implementations of irrelevance in the Agda and Idris [Bra21] languages.

##### Both run-time and compile-time irrelevance, but no distinction

The Implicit Calculus of Constructions [Miq01] ensures that some arguments are
treated irrelevantly (at both run time and compile time) by simply not
including them in the syntax of terms. This work was extended to decidable
type checking through the use of an erasure operation—terms may include
irrelevant arguments, but these arguments must be erased prior to run time and
equality checking[BB08]. This approach lead to Erasure Pure Type Systems
(EPTS) [MLS08], and the treatment of irrelevance in Dependent Haskell
[WVdAE17].

## Acknowledgments

Thanks to “Team Weirich” from OPLSS 2022 (Kartik Singhal, Jonathan Chan,
Shengyi Jiang and Thomas Binetruy), the Penn PLClub, and the attendees of
OPLSS 2022, OPLSS 2014 and OPLSS 2013, for feedback and suggestions about
these lecture notes. Some parts of the implementation This work was supported
by the National Science Foundation under grants NSF 2006535, NSF 1703835 and
NSF 0910786.

## References

  * [Abe13] Andreas Abel.  Normalization by Evaluation: Dependent Types and Impredicativity.  Habilitation thesis, Ludwig-Maximilians-Universität München, 2013.  URL: http://www.cse.chalmers.se/~abela/habil.pdf.
  * [AS12] Andreas Abel and Gabriel Scherer.  On Irrelevance and Algorithmic Equality in Predicative Type Theory.  Logical Methods in Computer Science, 8(1), 2012.  doi:10.2168/lmcs-8(1:29)2012.
  * [Atk18] Robert Atkey.  Syntax and Semantics of Quantitative Type Theory.  In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’18, pages 56–65, New York, NY, USA, 2018. Association for Computing Machinery.  doi:10.1145/3209108.3209189.
  * [Aug07] Lennart Augustsson.  Simpler, Easier!, 2007.  Available from https://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html.
  * [Bar93] H. P. Barendregt.  Lambda Calculi with Types, pages 117–309.  Oxford University Press, Inc., USA, 1993.
  * [Bau12] Andrej Bauer.  How to implement dependent type theory, 2012.  Available from http://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i/.
  * [BB08] Bruno Barras and Bruno Bernardo.  The Implicit Calculus of Constructions as a Programming Language with Dependent Types.  In Roberto Amadio, editor, Foundations of Software Science and Computational Structures, pages 365–379, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.  doi:10.1007/978-3-540-78499-9_26.
  * [Bra21] Edwin C. Brady.  Idris 2: Quantitative Type Theory in Practice.  In Anders Møller and Manu Sridharan, editors, 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Conference), volume 194 of LIPIcs, pages 9:1–9:26. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021.  doi:10.4230/LIPIcs.ECOOP.2021.9.
  * [Car86] Luca Cardelli.  A Polymorphic $\lambda$ Calculus with Type:Type.  Technical Report 10, Digital Equipment Corporation, SRC, 1986.  URL: http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-RR-10.pdf.
  * [CEIW22] Pritam Choudhury, Harley Eades III, and Stephanie Weirich.  A Dependent Dependency Calculus.  In Ilya Sergey, editor, Programming Languages and Systems, ESOP 2022, volume 13240 of Lecture Notes in Computer Science, pages 403–430, Cham, 2022. Springer International Publishing.  URL: https://github.com/sweirich/graded-haskell, doi:10.1007/978-3-030-99336-8_15.
  * [CH86] T. Coquand and Gérard Huet.  The calculus of constructions.  Technical Report RR-0530, INRIA, 1986.  URL: https://hal.inria.fr/inria-00076024.
  * [Chr13] David Raymond Christiansen.  Bidirectional Typing Rules: A Tutorial.  Tutorial, 2013.  URL: http://davidchristiansen.dk/tutorials/bidirectional.pdf.
  * [CKNT09] Thierry Coquand, Yoshiki Kinoshita, Bengt Nordström, and Makoto Takeyama.  A simple type-theoretic language: Mini-TT.  In Yves Bertot, Gérard Huet, Jean-Jacques Lévy, and Gordon Plotkin, editors, From Semantics to Computer Science: Essays in Honour of Gilles Kahn, pages 139–164. Cambridge University Press, 2009.  doi:10.1017/CBO9780511770524.007.
  * [dB72] Nicolaas Govert de Bruijn.  Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem.  Indagationes Mathematicae (Proceedings), 75(5):381–392, 1972.  doi:10.1016/1385-7258(72)90034-0.
  * [DK21] Jana Dunfield and Neel Krishnaswami.  Bidirectional Typing.  ACM Comput. Surv., 54(5), 2021.  doi:10.1145/3450952.
  * [GL02] Benjamin Grégoire and Xavier Leroy.  A Compiled Implementation of Strong Reduction.  In Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming, ICFP ’02, pages 235–246, New York, NY, USA, 2002. Association for Computing Machinery.  doi:10.1145/581478.581501.
  * [Har16] Robert Harper.  Practical Foundations for Programming Languages.  Cambridge University Press, USA, 2nd edition, 2016.
  * [Kov] Andras Kovacs.  Elaboration Zoo.  2022\.  https://github.com/AndrasKovacs/elaboration-zoo/.
  * [LMS10] Andres Löh, Conor McBride, and Wouter Swierstra.  A Tutorial Implementation of a Dependently Typed Lambda Calculus.  Fundam. Inform., 102:177–207, 2010.  Available from http://www.andres-loeh.de/LambdaPi/.  doi:10.3233/FI-2010-304.
  * [Luo90] Zhaohui Luo.  An Extended Calculus of Constructions.  PhD thesis, University of Edinburgh, 1990.  URL: http://hdl.handle.net/1842/12487.
  * [Miq01] Alexandre Miquel.  The Implicit Calculus of Constructions Extending Pure Type Systems with an Intersection Type Binder and Subtyping.  In Samson Abramsky, editor, Typed Lambda Calculi and Applications, pages 344–359, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg.  doi:10.1007/3-540-45413-6_27.
  * [ML71] Per Martin-Löf.  A Theory of Types.  Preprint, Stockholm University, 1971.  URL: https://raw.githubusercontent.com/michaelt/martin-lof/master/pdfs/martin-loef1971%20-%20A%20Theory%20of%20Types.pdf.
  * [ML75] Per Martin-Löf.  An intuitionistic theory of types: predicative part.  In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium ’73, Proceedings of the Logic Colloquium, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73–118. North-Holland, 1975.  doi:10.1016/S0049-237X(08)71945-1.
  * [MLS08] Nathan Mishra-Linger and Tim Sheard.  Erasure and Polymorphism in Pure Type Systems.  In Proceedings of the Theory and Practice of Software, 11th International Conference on Foundations of Software Science and Computational Structures, FOSSACS’08/ETAPS’08, pages 350–364, Berlin, Heidelberg, 2008. Springer-Verlag.  doi:10.1007/978-3-540-78499-9_25.
  * [Pfe01] Frank Pfenning.  Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory.  In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, LICS ’01, pages 221–230, Washington, DC, USA, 2001. IEEE Computer Society.  URL: https://www.cs.cmu.edu/~fp/papers/lics01.pdf, doi:10.1109/LICS.2001.932499.
  * [Pie02] Benjamin C. Pierce.  Types and Programming Languages.  The MIT Press, 1st edition, 2002.
  * [PT00] Benjamin C. Pierce and David N. Turner.  Local Type Inference.  ACM Trans. Program. Lang. Syst., 22(1):1–44, 2000.  doi:10.1145/345099.345100.
  * [PVWS07] Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields.  Practical type inference for arbitrary-rank types.  Journal of Functional Programming, 17(1), 2007.  doi:10.1017/S0956796806006034.
  * [Rom20] Tiark Rompf.  Implementing Dependent Types, 2020.  Available from https://tiarkrompf.github.io/notes/?/dependent-types/.
  * [SNO+07] Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge, Susmit Sarkar, and Rok Strniša.  Ott: Effective Tool Support for the Working Semanticist.  In Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP ’07, pages 1–12, New York, NY, USA, 2007. Association for Computing Machinery.  doi:10.1145/1291151.1291155.
  * [Ste17] Guy L. Steele.  It’s Time for a New Old Language.  In Proceedings of the 22nd ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, PPoPP ’17, page 1, New York, NY, USA, 2017\. Association for Computing Machinery.  doi:10.1145/3018743.3018773.
  * [VPJSS11] Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin Sulzmann.  OutsideIn(X): Modular type inference with local assumptions.  Journal of Functional Programming, 21:333–412, 2011.  doi:10.1017/S0956796811000098.
  * [VWPJ06] Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones.  Simple unification-based type inference for GADTs.  In International Conference on Functional Programming (ICFP’06). ACM SIGPLAN, 2006.  2016 ACM SIGPLAN Most Influential ICFP Paper Award.  URL: https://www.microsoft.com/en-us/research/publication/simple-unification-based-type-inference-for-gadts/, doi:10.1145/1159803.1159811.
  * [WVdAE17] Stephanie Weirich, Antoine Voizard, Pedro Henrique Avezedo de Amorim, and Richard A. Eisenberg.  A Specification for Dependent Types in Haskell.  Proc. ACM Program. Lang., 1(ICFP):31:1–31:29, 2017.  doi:10.1145/3110275.


# Dr-SAM: An End-to-End Framework for Vascular Segmentation, Diameter
Estimation, and Anomaly Detection on Angiography Images.

Vazgen Zohranyan${}^{1,4\;*}$ Vagner Navasardyan${}^{2,6\;{\dagger}*}$ Hayk
Navasardyan${}^{3\;*}$
Jan Borggrefe${}^{2,6\;{\dagger}}$ Shant Navasardyan1,5
1 Yerevan State University (YSU) 2 Ruhr-Universität Bochum (RUB) 3 Synopsys
Armenia CJSC
4 ServiceTitan, Inc. 5 Picsart AI Research (PAIR) 6 Johannes Wesling
University Hospital
https://github.com/vazgenzohranyan/Dr.SAM

###### Abstract

Recent advancements in AI have significantly transformed medical imaging,
particularly in angiography, by enhancing diagnostic precision and patient
care. However existing works are limited in analyzing the aorta and iliac
arteries, above all for vascular anomaly detection and characterization. To
close this gap, we propose Dr-SAM, a comprehensive multi-stage framework for
vessel segmentation, diameter estimation, and anomaly analysis aiming to
examine the peripheral vessels through angiography images. For segmentation we
introduce a customized positive/negative point selection mechanism applied on
top of the Segment Anything Model (SAM), specifically for medical
(Angiography) images. Then we propose a morphological approach to determine
the vessel diameters followed by our histogram-driven anomaly detection
approach. Moreover, we introduce a new benchmark dataset for the comprehensive
analysis of peripheral vessel angiography images which we hope can boost the
upcoming research in this direction leading to enhanced diagnostic precision
and ultimately better health outcomes for individuals facing vascular issues.

Figure 1: As an end-to-end framework for angiography image analysis, Dr-SAM
first extracts the segments of blood vessels, then detects the centerlines and
estimates the diameters of the vessels (shown with circles), then, finally,
recognizes the anomaly points indicating stenoses or aneurysms (green points).

**footnotetext: Equal contribution.††footnotetext: Department of Radiology,
Neuroradiology and Nuclear Medicine

##  1 Introduction

The blood supply to the lower body, including the legs and pelvic organs,
relies heavily on the infrarenal aorta and pelvic arteries. Any narrowing
(stenosis) [19] or widening (aneurysms) in these vessels can lead to serious
health issues. Angiography, an imaging technique that uses X-rays and contrast
agents, is utilized for the precise diagnosis and treatment of these
conditions. This imaging technique is particularly effective in identifying
stenosis and aneurysms in the infrarenal aorta and pelvic arteries. With the
advancement of technology and the introduction of minimally invasive
procedures, angiography has significantly enhanced the outcomes for patients
with vascular diseases. With the raise of AI angiography images got a chance
to be analyzed semantically and assist the doctors more effectively in
diagnosis forecasting.

To conduct an angiographic examination, the doctor inserts a catheter into the
arteries and through the catheter injects a contrast agent containing iodine
into the blood vessel. The vessels can now be visualized using x-rays, usually
in a substraction technique, to identify potential narrowing or widening.
These images are used to evaluate the vessel diameter, stenoses or aneurysms,
as well as the precise localization. If a relevant stenosis is detected during
angiography, immediate treatment may be required, especially if it
significantly impairs blood flow. In such cases, balloon or stent angioplasty
may be an effective intervention. In this procedure, a small balloon at the
end of the catheter is introduced to the narrowed area and then inflated to
widen the narrowing and restore normal blood flow. For this reason, rapid and
precise assessment of vascular diameters and their changes are crucial for
stenosis/aneurysm detection and characterization.

Simultaneous treatment of stenoses during angiographic examination offers a
number of advantages. First, it can reduce the risk of complications that
could arise if the patient had to return later for a separate operation.
Second, it allows blood flow to be restored more quickly, minimizing the risk
of tissue damage and complications such as tissue loss or necrosis. In
addition, prompt treatment of stenosis may reduce the need for repeat
interventions and improve long-term prognosis. For this reason, rapid and
precise assessment of vascular changes is crucial.

With the assistance of our tool, doctors can analyze images more quickly than
manual examination allows. This efficiency shortens the time between diagnosis
and the start of treatment, which is essential for conditions that need quick
action. It also importantly minimizes the risk of diagnostic errors that can
occur due to human factors like fatigue or subjective interpretation.

For this purpose we develop Dr-SAM, an end-to-end framework designed for
vascular angiograpgy image analysis with vessel segmentation, diameter
determination, and anomaly detection/characterization.

Various filter-based, learning-based, or regionally growing approaches have
been developed for angiographic segmentation [11, 6] including a wide usage of
convolutional neural networks (CNNs [3, 17]). CNNs have proven effective in
segmentation across various applications and offer a potential solution to
address the shortcomings of traditional methods in this complex area.

Recently, with the advancements of CNNs in the general domain segmentation
task the Segment Anything Model (SAM) [10] was developed as an interactive
tool for ultimate segmentation. However directly using SAM for vessel
segmentation in angiography images usually leads to incorrect region
selections (see Fig. 2) due to the limitation of SAM requiring positive label
points for precise segmentation. Therefore we designed a special positive
point selection mechanism, tailored to use with SAM for the vascular
angiography images.

Figure 2: SAM result on X-Ray image without any prompts. Middle - ground truth
mask, right - SAM predicted mask.

After segmenting the vessels in their corresponding regions, we further
estimate vessel diameters and analyze stenosis/aneurysm anomalies. To achieve
this, we utilize the topological skeleton of the binary mask by pruning
certain branches. Due to the noise from the binary mask, the topological
skeleton [2] may contain branches that are not actual vessel branches. Our
algorithm identifies these branches by their size and prunes them, resulting
in a clean tree-based vessel structure. This process improves the accuracy of
approximate diameter estimation for vessel segments, aiding in the
identification of stenosis/aneurysms.

Furthermore, we introduce a benchmark dataset for the segmentation and anomaly
detection on vascular angiography images crafted by domain specialists. We
validate our approach on the proposed benchmark, and hope our dataset can
further boost the research in this direction.

To summarize, our contributions are three-fold:

  * •

We propose a positive point selection mechanism for segmenting blood vessels
from angiographic X-ray images using SAM.

  * •

We introduce an algorithm for detecting stenoses and aneurysms over binary
masks of the vessels.

  * •

We introduce a new benchmark dataset containing X-ray images of peripheral
vessels along with the vessel binary masks and anomaly point labels.

##  2 Related work

###  2.1 Segmentation of blood vessels in x-ray images

In our study, we explored both image processing [23] and learning-based [10]
methods for angiography image segmentation. The lack of data in the community
and also the novelity of the problem itself are limiting the fine-tuning or
training specialized models. Hence we choose to go with a zero-shot approach
by leveraging pre-trained segmentation models. The Segment Anything Model
(SAM) [10] from Meta AI showcases the advancement, providing a system that can
identify and segment a wide range of objects without needing prior training on
them.

Similar to this paper, some existing works [20, 12, 4, 21] leverage SAM for
medical image segmentation. However they majorly choose to fine-tune SAM on
medical 2D and 3D images of wide range, including ophtalmology images. [5]
employs multi-box prompts to segment the optic disc. In [15] the authors use
SAM to annotate their dataset for training a new network for OCTA vessel
segmentation. [16] suggests a new learnable prompt layer for segmenting
ophthalmology images. In [22] the authors have trained a model on 64 open-
source medical datasets and added prompt options.

Regardless impressive results of the previous works, most of them either
segment convex regions in medical images or vessels of different regions. To
the best of our knowledge Dr-SAM is the first end-to-end pipeline for
angiography image analysis, including the vessel segmentation stage specified
on peripheral vascular angiography images. Our contribution on segmentation
part extends SAM’s utility through a novel methodology of positive point
selection which, along with user-specified bounding boxes, is guiding SAM for
refined vascular segmentation.

###  2.2 Anomaly detection

Some previous works [9, 14, 13] also touch the anomaly detection problem on
medical images. To detect anomalies, AngioNet [9] segments vessels and
calculates the minimum and maximum diameters within each segment. In contrast,
our approach identifies extremum points within each segment and designates
anomalies in the areas between these extremum points. For finding diameters,
we use skeleton detection algorithm [2], which is a tool used for thinning or
skeletonizing objects within an image to a single-pixel wide skeleton. The
algorithm iteratively removes pixels from the edges of objects until only the
minimal set of pixels that constitutes the ”skeleton” remains, preserving the
topology and general shape of the original object.

In [14] the authors utilize Coronary CT Angiography (CCTA) to extract coronary
artery characteristics and assess stenosis significance with a CNN, focusing
on artery geometry’s impact on blood flow and local appearance for accurate
stenosis assessment. In [13] the authors enhance key frame detection with
vessel extraction and employ CNN models with self-attention modules to
classify stenosis, validating the algorithm through extensive cross-validation
and external dataset evaluation, highlighting the use of heatmaps for
visualization. These methods illustrate the evolving complexity and
specificity of techniques in detecting coronary anomalies, contrasting with
our extremum point identification strategy for anomaly detection.

##  3 Method

In this section we introduce Dr-SAM, a universal algorithm for anomaly
detection in blood vessels, incorporating zero-shot technology for vessel
extraction followed by anomaly detection with the integration of topological
skeleton. Moreover, here we also present our benchmark dataset collected for
thorough evaluation of our method and other approaches.

Our streamlined approach for anomaly detection not only reduces computational
costs having pipeline without training process, but also ensures applicability
demonstrating effectiveness on angiographic images. The overview of the
framework can be found in Fig. 3.

Figure 3: The overview of Dr-SAM: For each bounding box provided by the user,
first we determine five positive points using our point finder algorithm. This
is followed by vessel extraction by SAM [10] conditioned on our positive
points. Then for anomaly detection we extract the centerline of the binary
mask, obtained from the previous stage, by finding its skeleton, and use that
skeleton for estimating vessel diameters, which are later being used to detect
anomaly points on the vessels.

###  3.1 Vessel extraction using point-conditioned SAM

We employ SAM [10] for extracting vessels from X-ray images. In order to
enhance results, we tailor SAM’s prompt, particularly focusing on input
points. In our approach, we propose a novel algorithm for identifying positive
points to feed SAM during segmentation (see Fig. 3).

It is worth to mention that due to our experiments, incorporating negative
points does not significantly impact segmentation outcomes hence we choose to
design a special algorithm only for positive point selection. For the initial
point, we select the most probable vessel point within the bounding box
through the following procedure:

  1. 1.

We generated a probability map for each pixel being a vessel pixel, assigning
higher probabilities to pixels with lower values by assuming that darker
points in the X-ray angiographic images are part of the vessel. We obtained
the probability map by scaling and reverting the input values to [0, 1] (255
to 0 and 0 to 1, i.e. $x\mapsto 1-x/255=\mbox{Probability}(x\mbox{is a vessel
pixel})$ for $x\in[0,255]$).

  2. 2.

Excluded the pixels with probabilities lower than pre-defined threshold.

  3. 3.

Sampled 100 random points from the remaining set to prevent concentration of
points in densely populated areas.

  4. 4.

Selected a point with the highest number of neighboring points within the
predefined radius of $SelectionRadius$ from the sampled set as a positive
point.

For the second step, we select the most probable point that lies outside the
region defined by the $ExcludeRadius$ from the first point and with the radius
of $SecondPointSelectionRadius$.

To further enhance results, we implement a repeatable algorithm for
identifying positive points. In simple words, the algorithm starts segmenting
images by available points described in the previous paragraph. After
segmentation, for selecting the next positive point, the algorithm avoids
considering points on the previously predicted mask, selecting the most
possible positive point from the remaining image in the same way as described
in the previous paragraph. For each iteration algorithm uses all available
positive points collected from previous steps for segmentation, thereby
ensuring consistent results after each iteration. However, to preserve
previously segmented good results with minimal changes, we repeat this process
three times at the result having overall 5 positive points, including 2 points
from last paragraph, for the final segmentation.

###  3.2 Anomaly detection using topological skeleton

For anomaly detection, we utilized a topological skeleton [2], a method widely
employed in X-ray image studies within Computer Vision. The topological
skeleton is a vital component in identifying or approximating the centerline
of a vessel, aiding in the determination of its diameter in specific regions.
Our proposed algorithm involves the use of a topological skeleton, which is
subsequently pruned by removing unnecessary branches while preserving the
vessel’s structural integrity.

To do so, our algorithm uses PlantCV [7] techniques to extract branches from
the topological skeleton. After getting the branches separated, we identified
low-length branches. Our consideration was that branches with the length less
then $MinBranchLength$ are not real branches of the blood vessel and were
generated because of the anomalies in it. Removing low-length branches, we get
tree-like structured skeleton of the blood vessel, which is better to estimate
diameters along the segments.

Further, we leveraged extracted segments of the skeleton to examine anomaly
regions within the vessel segment. Treating segment-approximated diameters as
values of a function, we conducted anomaly detection on each segment. Our
primary consideration was that anomaly points constitute a subgroup of
extremum points of the real function. However, the challenge arises from
noise, which generates inaccuracies in the sequence’s highs and lows. The
primary contribution of our approach lies in mitigating noise by clustering
close values in one region, facilitating the more accurate identification of
highs and lows. By applying a threshold of $MinChangeThreshold$ to the
variations between these extremum point values and the mean of surrounding
point values, we identify anomaly points within the segment. For details see
Algorithm 1.

After detecting the anomaly points we leverage the distance transform [18]
technique to better estimate the diameters near the anomaly points. To do so
for each centerline point we calculate the distance between that point and the
nearest non-vessel point in the image by so estimating the radius of the
vessel at that particular location of centerline. After that we estimate the
percentage of the anomaly as follows:

  1. 1.

Extract branch from the skeleton as an array of points.

  2. 2.

Calculate the distance transform of anomaly point.

$dt_{p}=distanceTransform(segment[i])$ (1)

  3. 3.

Calculate the distance transform of points located before and after anomaly
point with the step equal to $length(segment)//5$.

$dt_{e1}=distanceTrasform(segment[i-step]$ (2)
$dt_{e2}=distanceTransform(segment[i+step])$ (3)

  4. 4.

For getting the percentage of the anomaly:

$change_{p}=\frac{abs(mean(dt_{e1},dt_{e2})-dt_{p})}{mean(dt_{e1},dt_{e2})}$
(4)

And finally, to get the type of the anomaly, we compare
$mean(dt_{e1},dt_{e2})$ and $dt_{p}$. If the first is more than the second, we
have stenosis and our percentage change will be with $-$ sign. Otherwise, we
will have an aneurysm, and the percentage change will have $+$ sign.

1

Input : 2D Predicted binary mask

Output : List of anomaly points

2

3$anomalyPoints=[\ ]$;

4 $segmentedSkeleton\leftarrow segmentize(skeletonize(mask))$;

5 $skeletonThickness\leftarrow getThickness(mask)$;

6

7for  _$seg$ in $segmentedSkeleton$_ do

8 $seg\leftarrow segmentedSkeleton[i]$;

9 $thickness\leftarrow skeletonThickness[seg]$;

10 $eps\leftarrow length(seg)/10$;

11 $minSamples\leftarrow 1$;

12 $localExtremums\leftarrow findLocalExtremums(thickness)$;

13 $clusters\leftarrow DBSCAN(localExtremums,eps,minSamples)$;

14

15 $newExtremums=[\ ]$;

16 for  _$c$ in $clusters$_ do

17 $indices\leftarrow c.indices$;

18 $center\leftarrow int(mean(indices))$;

19 $newExtremums.add([center,thickness[center]])$

20 end for

21

22 $filteredExtremums=[\ ]$;

23 $N\leftarrow length(newExtremums)$;

24 for  _$i\leftarrow 1$ to $N-1$_ do

25 $current\leftarrow filteredExtremums[i][1]$;

26 $previous\leftarrow filteredExtremums[i-1][1]$;

27 $next\leftarrow filteredExtremums[i+1][1]$;

28 if  _$current <previous\And current<next$_ then

29 $filteredExtremums.add(current)$;

30

31 end if

32 if  _$current >previous\And current>next$_ then

33 $filteredExtremums.add(current)$;

34

35 end if

36

37 end for

38

39 $radius\leftarrow length(seg)//5$;

40 for  _$point$ in $filteredExtremums$_ do

41 $index\leftarrow point[0]$;

42 $meanThickness\leftarrow(thickness[index-
radius]+thickness[index+radius])/2$;

43

44 if  _$abs(point[1]-meanThickness)/meanThickness >0.5$_ then

45 $anomalyPoints.add(seg[index])$;

46

47 end if

48

49 end for

50

51 end for

return _$anomalyPoints$_

Algorithm 1 Anomaly detection algorithm

###  3.3 Benchmark Dataset

Our dataset consists of carefully selected images from 500 angiographic
examinations of the pelvic-iliac arteries, carried out between 2018 and 2024
at Bad Oeynhausen Hospital and JWK Klinikum Minden, within their radiology
departments. The focus of these examinations was the abdominal aorta below the
renal arteries and the pelvic arteries. Using Adobe Lightroom, only the
pertinent areas of these examinations were cropped to isolate the regions of
interest. Of these images, 450 have a resolution of 386x448 pixels, and 50
have a resolution of 819x950 pixels. The dataset includes 170 images featuring
at least one stenosis and 64 images with at least one aneurism. Following this
initial selection, Adobe Photoshop [1] was employed to create a vessel mask
for each cropped image, which outlines the arterial structure. Additionally,
any narrowing and widening observed within the arterial regions were
meticulously marked. This dataset is a comprehensive compilation that provides
a significant resource for studying the conditions affecting the pelvic-iliac
arteries, demonstrating a targeted approach to vascular imaging research.

##  4 Experiments

In this section we first discuss some implementation details of Dr-SAM, then
make thorough analysis of its segmentation and anomaly detection (including
the centerline detection, diameter and anomaly estimations) stages.

Figure 4: Qualitative comparison of three different approaches for
segmentation. From left to right: SAM, naive approach of selecting the
positive point as the most probable vascular pixel, our method Figure 5: Dr.
SAM pipeline results for each step

###  4.1 Implementation details

The experiments were conducted on a diverse set of angiography images,
encompassing various structures and anomalies. We utilized angiographic X-ray
images with bounding boxes and anomaly points validated by two professional
doctors in the field of vascular imaging. Throughout the experiments, we
configured parameters as follows: $SelectionRadius=75$,
$SecondPointSelectionRadius=50$, $ExcludeRadius=100$, $MinBranchLength=40$,
$MinChangeThreshold=50\%$. Our code is implemented using PyTorch. The mean
time for the segmentation part takes $0.66$ seconds on average, while the
anomaly detection part takes $0.65$ seconds on average.

###  4.2 Segmentation Analysis

For the segmentation aspect, we aim to evaluate our methodology against two
established techniques: The first technique involves applying the Segment
Anything Model (SAM) to the original images, employing bounding boxes as
prompts without any enhancement or additional prompts. The second, a naive
positive point selection approach, attempts to identify the pixel with the
lowest value (i.e. the highest probability of being a vascular pixel) within
each specified bounding box on the original image (normalized to have values
from the range [0,1]), and gives it as a positive point prompt. We present the
analysis both visually and through quantitative measures. For our quantitative
metric, we use the Intersection over Union (IoU) [8] to compare our
predictions with the ground truths. The ground truth is derived from binary
masks of each box, meticulously annotated by experts.

In Tab. 1 we present the mean Intersection over Union calculated on 450
various angiography images segmented by 1. standalone SAM; 2. SAM with
additional positive point naively chosen as the highest probable point of
being a vascular pixel; 3. SAM with additional positive points gathered by our
method. The experiments clearly show the advantage of our method for
segmenting the vessels in angiography images.

| SAM | Naive approach | Our method
---|---|---|---
MIoU | 0.754 | 0.807 | 0.859
Table 1: Quantitative comparison by using the mean IoU metric.

We also perform qualitative analysis of our method by comparing it with the
above mentioned approaches of vanilla SAM and highest probable positive point
selection approach. Fig. 4 shows the clear advantage of our method in
comparison, different colors are applied for more visually appealing
demonstration.

###  4.3 Anomaly detection

For centerline estimation, our objective is to assess its performance relative
to the topological skeleton. As depicted in Figure 6, the distinction between
skeletons is clearly illustrated. Our proposed algorithm effectively
eliminates extra branches from the skeleton (indicated by red circles) that do
not belong to the vessel structure.

Figure 6: Topological skeleton in (a), and processed skeleton by our algorithm
(b)

In Figure 5, we present the successful centerline estimation results. These
results clearly demonstrate the adaptability of the centerline algorithm to
anomalies, leading to improved accuracy in diameter estimation. Following
successful centerline detection, the distance transform method yields
excellent results in diameter estimation, including in challenging anomal
regions. And finally, our anomaly detection algorithm excellently finds both
stenosis and aneurysm parts of the segments, giving good results in indicating
the level of anomaly.

##  5 Conclusion

In this paper, we present Dr-SAM, a novel approach for an end-to-end detection
of stenoses and aneurisms in peripheral blood vessels. We introduce a
customized positive point detection for Segment Anything Model (SAM) to
capture blood vessels in X-ray angiographic images without the need for any
additional training.

Through a series of experiments, we demonstrate the effectiveness of our
approach in vessel extraction and anomaly detection. Our method offers
significant advancements over existing segmentation techniques in this
particular task.

Additionally, we introduce a benchmark dataset of 450 angiography images of
peripheral vessels, annotated and labeled by highly qualified experts. We plan
to make the dataset and the codes publicly available.

In conclusion, our work contributes to expanding research on medical image
processing by introducing new ideas and tools for future work. Addressing
limitations of the naive approaches, our approach has the potential to advance
the state-of-the-art in anomaly detection in blood vessels research, providing
a more effective and efficient solution for a wide range of applications.

## References

  * Adobe Systems Incorporated [Year of Version] Adobe Systems Incorporated.  _Adobe Photoshop_ , Year of Version.  Software available from Adobe Systems Incorporated.
  * Blum [1967] Harry Blum.  A transformation for extracting new descriptors of shape.  In _Models for the Perception of Speech and Visual Form_ , pages 362–380. MIT Press, Cambridge, Massachusetts, 1967.
  * Chen et al. [2018] Liang-Chieh Chen, Yukun Zhu, George Papandreou, Florian Schroff, and Hartwig Adam.  Encoder-decoder with atrous separable convolution for semantic image segmentation.  In _ECCV_ , 2018.
  * Cheng et al. [2023] Junlong Cheng, Jin Ye, Zhongying Deng, Jianpin Chen, Tianbin Li, Haoyu Wang, Yanzhou Su, Ziyan Huang, Jilong Chen, Lei Jiangand Hui Sun, Junjun He, Shaoting Zhang, Min Zhu, and Yu Qiao.  Sam-med2d, 2023.
  * Deng et al. [2023] Guoyao Deng, Ke Zou, Kai Ren, Meng Wang, Xuedong Yuan, Sancong Ying, and Huazhu Fu.  Sam-u: Multi-box prompts triggered uncertainty estimation for reliable sam in medical image.  _arXiv:2307.04973_ , 1, 2023.
  * Franchi et al. [2008] Danilo Franchi, Pasquale Gallo, and Giuseppe Placidi.  A novel segmentation algorithm for digital subtraction angiography images: First experimental results.  In _Advances in Visual Computing_ , pages 612–623, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg.
  * Gehan et al. [2017] Malia A Gehan, Noah Fahlgren, Arash Abbasi, Jeffrey C Berry, Steven T Callen, Leonardo Chavez, Andrew N Doust, Max J Feldman, Kerrigan B Gilbert, John G Hodge, J Steen Hoyer, Aanika Lin, Siobhan Liu, Carolina Lizárraga, Argelia Lorence, Michael Miller, Eric Platon, Monica Tessman, and Tony Sax.  Plantcv v2: Image analysis software for high-throughput plant phenotyping.  _PeerJ_ , 5:e4088, 2017.
  * Jaccard [1901] Paul Jaccard.  Distribution de la flore alpine dans le bassin des dranses et dans quelques régions voisines.  _Bulletin de la Société Vaudoise des Sciences Naturelles_ , 37:241–272, 1901.
  * K. et al. [2021] Iyer K., Najarian C. P., Fattah A. A., Arthurs C. J., Soroushmehr S. M. R., V. Subban, and C. A. Figueroa.  Angionet: a convolutional neural network for vessel segmentation in x-ray angiography.  _Scientific Reports_ , 11(1), 2021.
  * Kirillov et al. [2023] Alexander Kirillov, Eric Mintun, Nikhila Ravi, Hanzi Mao, Chloe Rolland, Laura Gustafson, Tete Xiao, Spencer Whitehead, Alexander C. Berg, Wan-Yen Lo, Piotr Dollár, and Ross Girshick.  Segment anything.  _arXiv:2304.02643_ , 2023.
  * Luo and Sun [2023] Yanping Luo and Linggang Sun.  Digital subtraction angiography image segmentation based on multiscale hessian matrix applied to medical diagnosis and clinical nursing of coronary stenting patients.  _Journal of Radiation Research and Applied Sciences_ , 16(3):100603, 2023.
  * Ma et al. [2024] Jun Ma, Yuting He, Feifei Li, Lin Han, Chenyu You, and Bo Wang.  Segment anything in medical images.  _Nature Communications_ , 15:1–9, 2024.
  * Moon et al. [2021] Jong Hak Moon, Da Young Lee, Won Chul Cha, Myung Jin Chung, Kyu-Sung Lee, Baek Hwan Cho, and Jin Ho Choi.  Automatic stenosis recognition from coronary angiography using convolutional neural networks.  _Computer Methods and Programs in Biomedicine_ , 198:105819, 2021.
  * N et al. [2022] Hampe N, van Velzen SGM, Planken RN, Henriques JPS, Collet C, Aben JP, Voskuil M, Leiner T, and Išgum I.  Deep learning-based detection of functionally significant stenosis in coronary ct angiography.  _Front Cardiovasc Med._ , 9:964355, 2022.
  * Ning et al. [2023] Haojian Ning, Chengliang Wang, Xinrun Chen, and Shiying Li.  An accurate and efficient neural network for octa vessel segmentation and a new dataset.  _arXiv:2309.09483_ , 1, 2023.
  * Qiu et al. [2023] Zhongxi Qiu, Yan Hu†, Heng Li, and Jiang Liu.  Learnable ophthalmology sam.  _arXiv:2304.13425_ , 1, 2023.
  * Ronneberger et al. [2015] O. Ronneberger, P.Fischer, and T. Brox.  U-net: Convolutional networks for biomedical image segmentation.  In _Medical Image Computing and Computer-Assisted Intervention (MICCAI)_ , pages 234–241. Springer, 2015.  (available on arXiv:1505.04597 [cs.CV]).
  * Rosenfeld and Pfaltz [1969] Azriel Rosenfeld and John L Pfaltz.  Distance functions on digital pictures.  _Pattern Recognition_ , 1(1):33–61, 1969.
  * Thiriet et al. [2015] Marc Thiriet, Michel Delfour, and André Garon.  _Vascular Stenosis: An Introduction_ , pages 781–868.  Springer Berlin Heidelberg, Berlin, Heidelberg, 2015.
  * Wang et al. [2023a] Chengliang Wang, Xinrun Chen, Haojian Ning, and Shiying Li.  Sam-octa: A fine-tuning strategy for applying foundation model to octa image segmentation tasks.  _arXiv:2309.11758_ , 1, 2023a.
  * Wang et al. [2023b] Haoyu Wang, Sizheng Guo, Jin Ye, Zhongying Deng, Junlong Cheng, Tianbin Li, Jianpin Chen, Yanzhou Su, Ziyan Huang, Yiqing Shen, Bin Fu, Shaoting Zhang, Junjun He, and Yu Qiao.  Sam-med3d, 2023b.
  * Wu et al. [2023] Junde Wu, Jiayuan Zhu, Yuanpei Liu, Yueming Jin, and Min Xu.  One-prompt to segment all medical images.  _arXiv:2305.10300_ , 3, 2023.
  * Yin and Xu [2022] Zong-Xian Yin and Hong-Ming Xu.  An unsupervised image segmentation algorithm for coronary angiography.  _BioData Mining_ , 15(27), 2022.