††Dedicated to Bhagawan Sri Sathya Sai Baba

# An Algebraic Approach to
Degenerate Bernoulli Numbers

N. Uday Kiran and Sampath Lonka  Department of Mathematics and Computer
Science
Sri Sathya Sai Institute of Higher Learning
INDIA<EMAIL_ADDRESS>
<EMAIL_ADDRESS>
###### Abstract.

In this work we study the properties of a new algebraic variant of the
degenerate Bernoulli polynomial $\tilde{\beta}_{k}(m,x)$ and study the
corresponding degenerate Bernoulli number
$\tilde{\beta}_{k}(m,1)=m^{k}\beta_{k}(1/m)$, where
$\beta_{k}(\lambda),\lambda\neq 0$ is the standard degenerate Bernoulli
number. Our approach relies on a new algebraic framework for generating
functions and the action of a symbolic evaluation function on powers of
polynomials. We show that $\tilde{\beta}_{k}(m,x)$ displays surprising links
with other mathematical objects (such as Circulant matrices and Galois fields)
and enjoys many interesting algebraic, symmetric and dynamical properties that
could be deployed to perform efficient computations.

###### Key words and phrases:

Degenerate Bernoulli Number, Sum of Product formula, Galois Fields, Palindrome
Polynomials of a Darga, Circulant Matrices

###### 1991 Mathematics Subject Classification:

Primary 11B68 Secondary 11B83

##  1\. Introduction

Degenerate Bernoulli numbers $\beta_{k}(\lambda)$, where $\lambda\neq 0$, were
proposed by Carlitz [5], and are of contemporary interest (see [11, 9]). He
defined them by means of the generating function

$\frac{t}{(1+\lambda
t)^{1/\lambda}-1}=\sum_{k=0}^{\infty}\beta_{k}(\lambda)\frac{t^{k}}{k!}.$
(1.1)

These numbers are related to the Bernoulli numbers by
$\displaystyle\lim_{\lambda\rightarrow 0}\beta_{k}(\lambda)=B_{k}$.

In this paper, our interest is to study the properties of
$\tilde{\beta}_{k}(m)=m^{k}\beta_{k}(1/m)$ for $m$ a positive integer. As
observed in [13], by setting $x=(1+\lambda t)$ and $\lambda=1/m$ in (1.1) we
have the simpler generating function

$m\frac{1-x}{1-x^{m}}=\frac{m}{\Psi_{m}(x)}=\sum_{k=0}^{\infty}\frac{(-1)^{k}}{k!}\tilde{\beta}_{k}(m)(1-x)^{k},$

where the polynomial $\Psi_{m}(x)=\displaystyle\sum_{j=0}^{m-1}x^{j}$. This
generating function can be studied through a special $m-2$ degree polynomial
which emerges as a remainder of powers of a polynomial

$f^{(m)}_{k}(x)=\frac{(-1)^{k}}{k!}\tilde{\beta}_{k}(m,x)=\left(\frac{1}{m}x\Psi_{m}^{\prime}(x)\right)^{k}\textnormal{
rem }\Psi_{m}(x),$ (1.2)

where rem stands for the polynomial remainder operator. It should be noted
that the $k^{th}$ polynomial is obtained by taking remainder of the $k^{th}$
power of a polynomial through another polynomial. Thus, these polynomials are
obtained through polynomial manipulation and are different from other the
degenerate Bernoulli polynomials defined in the literature (see [5, 11, 16, 9]
and the references therein).

Upon substitution of $x=1$ in (1.2) we have

$f^{(m)}_{k}(1)=\frac{(-1)^{k}}{k!}\tilde{\beta}_{k}(m,1)=\frac{(-1)^{k}}{k!}\tilde{\beta}_{k}(m).$

Gessel [8] showed that the number $\tilde{\beta}_{k}(m)$ can be expressed
through a trigonometric sum and obtained an explicit formula.

######  Theorem 1.1 (Gessel [8]).

$\tilde{\beta}_{k}(m)=\left\\{\begin{array}[]{@{}l@{\thinspace}l}\displaystyle\frac{1-m}{2}&\textnormal{
if }k=1\\\ \displaystyle
k\sum^{k}_{j=2}(-1)^{k-j}\frac{B_{j}}{j}\textnormal{stirl}(k-1,j-1)(m^{j}-1)&\textnormal{
if }k\geq 2.\\\ \end{array}\right.$ (1.3)

In [13], the first author showed that $\tilde{\beta}_{k}(m)$ is a polynomial
in $m$ only through algebraic considerations. Further, it was shown in [13],
that there is a sum of product based formula for the polynomial part of the
Sylvester Denumerants (aka Restricted Partitions) given by

$\displaystyle W_{1}(t;\textbf{A})$ $\displaystyle=$
$\displaystyle\frac{1}{a_{1}\cdots
a_{r}}\sum^{r-1}_{j=0}\sum_{j_{1}+\cdots+j_{r}=j}\begin{pmatrix}t+r-j-1\\\
t\end{pmatrix}f_{j_{1}}^{(a_{1})}(1)\cdots f_{j_{r}}^{(a_{r})}(1)$
$\displaystyle=$ $\displaystyle\frac{1}{a_{1}\cdots
a_{r}}\sum^{r-1}_{j=0}\sum_{j_{1}+\cdots+j_{r}=j}(-1)^{j}\begin{pmatrix}t+r-j-1\\\
t\end{pmatrix}\frac{\tilde{\beta}_{j_{1}}(a_{1})\cdots\tilde{\beta}_{j_{r}}(a_{r})}{j_{1}!\cdots
j_{r}!},$

where $\textbf{A}=(a_{1},\cdots,a_{r})$ is a tuple of positive integers.
Theses numbers have also been found useful in identities of falling factorials
(for instance, see [16, 9, 17] and the references therein).

These above observations motivate us to study the properties of the degenerate
Bernoulli numbers with a view to efficient computation of
$W_{1}(t;\textbf{A})$. In this direction, we study the polynomial (1.2) from
algebraic, symmetric and dynamical viewpoints. Our contributions in this paper
are the following results on $\tilde{\beta}_{k}(m,x)/k!$:

  1. (1)

Periodicity in a modulo $p$ (a prime) and $(m,p)=1$. As a consequence of this
property and the reciprocity law we show that several $\tilde{\beta}_{k}(m)$
vanish mod $p$.

  2. (2)

For $m$ odd number, $\tilde{\beta}_{md+2}(m,x)$ is a palindrome of darga
$(m-2)$ if $d$ is even and anti-palindrome of darga $(m-2)$ if $d$ is odd.
Using this fact, we can provide an algebraic proof for the well know fact
$\tilde{\beta}_{md+2}(m)=0$ for $d$ odd given in [16].

  3. (3)

A sum of products formula holds for relatively coprime $m_{1}$ and $m_{2}$:

$\sum_{j_{1}+j_{2}=k}\frac{\tilde{\beta}_{j_{1}}(m_{1})}{j_{1}!}\frac{\tilde{\beta}_{j_{2}}(m_{2})}{j_{2}!}=\sum^{m_{1}+m_{2}}_{j=0}a_{j}\frac{\tilde{\beta}_{j}(m_{1})}{j!}+b_{j}\frac{\tilde{\beta}_{j}(m_{2})}{j!}.$

For the case $m_{1}=m_{2}$ the sum of products result is given in [17].

  4. (4)

The set of all polynomials $\tilde{\beta}_{k}(m)$ for $k\in\mathbb{Z}$ form an
infinite abelian group under multiplication mod $\Psi_{m}(x)$. In
$\mathbb{F}_{p}$, this group becomes finite and is isomorphic to a subgroup of
$\mathbb{F}_{p^{m-1}}^{*}$. Moreover, under certain mild conditions, the
subgroup is equidistributed in $\mathbb{F}_{p^{m-1}}^{*}$.

  5. (5)

The matrix representation of the $m-2$ degree polynomials
$\tilde{\beta}_{k}(m,x)/k!$ for varying $k$ are related to powers of a certain
Circulant matrix [6], which in turn has a special feature of being
diagonalizable by DFT matrix. We call these matrices the Degenerate Bernoulli
Matrices.

Our approach through polynomials can be considered as an alternative approach
to the matrix approach to studying sequences satisfying linear recurrence
relations. This is presented in Section 5.

##  2\. An Algebraic Framework for Sequences Generated by Rational Polynomials

Given two non-zero polynomials $p(x),q(x)\in\mathbb{Q}[x]$ we say $p(x)/q(x)$
is a rational polynomial. Further, if
$\textnormal{deg}(p)<\textnormal{deg}(q)$ then we say that it is a proper
rational polynomial. In order to provide an algebraic framework for sequences
generated by a rational polynomial we define an operator from commutative
algebra.

######  Definition 2.1.

Given non-constant polynomials $r(x),s(x),a(x)\in\mathbb{Q}[x]$ and
$s(x),a(x)$ are relatively prime, we define the evaluation of the fraction
$\frac{r(x)}{s(x)}$ with respect to $a(x)$

$\textnormal{eval}\left(\frac{r(x)}{s(x)};a(x)\right)=\alpha(x)r(x)\textnormal{
rem }a(x),$

where $\alpha(x)s(x)\equiv 1\textnormal{ mod }a(x)$ and rem is the polynomial
remainder operator.

In simple terms, the eval of $r(x)/s(x)$ takes the remainder of $r(x)$
multiplied by the inverse of $s(x)$ modulo $a(x)$. The eval operator is based
on the principles of substitution and localization. The following properties
can be easily proved.

######  Lemma 2.2.

Given $a(x),r_{i}(x),s_{i}(x)\in\mathbb{Q}[x]$ and
$\textnormal{gcd}(s_{i}(x),a(x))=1$ for $i=0,1$. The following are some
properties of eval function:

  1. (1)

$\textnormal{eval}\left(r_{0};a(x)\right)=r_{0}(x)\textnormal{ rem }a(x).$

  2. (2)

$\textnormal{eval}\left(\alpha_{0}r_{0}(x)+\alpha_{1}r_{1}(x);a(x)\right)=\alpha_{0}\textnormal{eval}\left(r_{0}(x);a(x)\right)+\alpha_{1}\textnormal{eval}\left(r_{1}(x);a(x)\right)$.

  3. (3)

$\textnormal{eval}\left(\frac{r_{0}(x)r_{1}(x)}{s_{0}(x)s_{1}(x)};a(x)\right)=\textnormal{eval}\left(\frac{r_{0}(x)}{s_{0}(x)};a(x)\right)\textnormal{eval}\left(\frac{r_{1}(x)}{s_{1}(x)};a(x)\right).$

  4. (4)

$\textnormal{eval}\left(\frac{r_{0}(x)-p_{0}(x)a(x)}{s_{0}(x)-q_{0}(x)a(x)};a(x)\right)=\textnormal{eval}\left(\frac{r_{0}(x)}{s_{0}(x)};a(x)\right)$
for some $p_{0}(x),q_{0}(x)\in\mathbb{Q}[x].$

For a rigorous treatment of this operator and its properties we refer to [13].
The operator eval was shown to be an effective tool to handle partial
fractions. The following result was indeed proved.

######  Theorem 2.3 (Extended Cover-Up Method, [13]).

Let $p_{1}(x),\cdots,p_{n}(x)\in\mathbb{Q}[x]$ be pairwise relatively prime
polynomials and let $f(x)\in\mathbb{Q}[x]$ satisfying $deg(f)<deg(p_{1}\cdots
p_{k})$. Then, we have the following identity

$f(x)\prod_{j=1}^{k}\frac{1}{p_{j}(x)}=\sum^{k}_{j=1}\frac{f(x)\textnormal{eval}\left(\displaystyle\prod_{\begin{subarray}{c}i=1\\\
i\neq j\end{subarray}}^{n}\frac{1}{p_{i}(x)};p_{j}(x)\right)}{p_{j}(x)}.$

As an immediate corollary we prove the following useful partial fraction
decomposition result.

######  Lemma 2.4.

Given $p(x),q(x)\in\mathbb{Q}[x]$ with
$\textnormal{deg}(p)<\textnormal{deg}(q)$ and $\textnormal{gcd}(p(x),q(x))=1$.
Suppose $p(x)$ and $q(x)$ are non-vanishing at $x=a$ we have the partial
fraction identity

$\frac{p(x)}{(x-a)q(x)}=\frac{p(a)}{q(a)(x-a)}+\frac{\textnormal{eval}\left(p(x)/(x-a);q(x)\right)}{q(x)},$
(2.1)

where

$\textnormal{eval}\left(\frac{p(x)}{x-a};q(x)\right)=\frac{q(a)p(x)-p(a)q(x)}{q(a)(x-a)}.$
(2.2)

###### Proof.

By the Extended Cover-Up method we have

$\frac{p(x)}{(x-a)q(x)}=\frac{\textnormal{eval}\left(p(x)/q(x);x-a\right)}{(x-a)}+\frac{\textnormal{eval}\left(p(x)/(x-a);q(x)\right)}{q(x)}.$

Since $q(a)\neq 0$, we have $q(x)$ and $(x-a)$ to be coprimes. By Bezout’s
identity, there exist $\alpha(x),\beta(x)$ such that
$\alpha(x)q(x)+\beta(x)(x-a)=1$. Without loss of generality we may assume that
$\alpha(x)$ is a remainder when divided by $(x-a)$, i.e., $\alpha(x)$ is a
constant. Otherwise, we can write $\alpha(x)=\tilde{\alpha}(x)(x-a)+r(x)$
where $\textnormal{deg}(r)=0$ and express the above equation as
$r(x)q(x)+(\beta(x)+\tilde{\alpha}(x))(x-a)=1$.

Substituting $x=a$ we obtain $\alpha(x)=1/q(a)$. Further, by the definition of
eval and the Remainder Theorem we have
$\textnormal{eval}(p(x)/q(x);(x-a))=p(a)/q(a)$. Upon rearranging terms in
(2.1) we obtain (2.2). ∎

The above lemma is a general partial fraction formula that can be inductively
extended to higher powers case.

######  Lemma 2.5.

Given two polynomials $p(x),q(x)$ with
$\textnormal{deg}(p)<\textnormal{deg}(q)$ and both $p(a)$ and $q(a)$ are non-
zero. For $k\geq 1$ the following partial fraction holds

$\frac{p(x)}{(x-a)^{k}q(x)}=\frac{1}{q(a)}\sum_{j=0}^{k-1}\frac{g_{j}(a)}{(x-a)^{k-j}}+\frac{g_{k}(x)}{q(x)},$
(2.3)

where $g_{k}(x)=\textnormal{eval}(p(x)/(x-a)^{k};q(x))$ and $g_{0}(x)=p(a)$.

###### Proof.

We prove the result by induction on $k$. The case $k=1$ is given in Lemma 2.4.
Suppose the result holds for $k=n$, i.e.

$\frac{p(x)}{(x-a)^{n}q(x)}=\frac{1}{q(a)}\sum_{j=0}^{n-1}\frac{g_{j}(a)}{(x-a)^{n-j}}+\frac{g_{k}(x)}{q(x)}.$

Dividing both sides of the above equation by $(x-a)$ we have

$\frac{p(x)}{(x-a)^{n+1}q(x)}=\frac{1}{q(a)}\sum_{j=0}^{n-1}\frac{g_{j}(a)}{(x-a)^{n-j+1}}+\frac{g_{n}(x)}{(x-a)q(x)}.$

Applying Lemma 2.4 on the last term we have

$\frac{g_{n}(x)}{(x-a)q(x)}=\frac{g_{n}(a)}{q(a)(x-a)}+\frac{\textnormal{eval}(g_{n}(x)/(x-a);q(x))}{q(x)}.$

It is easy to see that $g_{n+1}(x)=\textnormal{eval}(g_{n}(x)/(x-a);q(x))$.

∎

Similar to the partial fractions formula we can also prove a result on the
long division.

######  Lemma 2.6.

Given two polynomials $p(x),q(x)$ with
$\textnormal{deg}(p)<\textnormal{deg}(q)$ and both $p(a)$ and $q(a)$ are non-
zero. For $k\geq 1$ the following repeated division result holds

$\frac{p(x)(x-a)^{k}}{q(x)}=\frac{-1}{q(a)}\sum_{j=1}^{k}g_{-j}(a)(x-a)^{k-j}+\frac{g_{-k}(x)}{q(x)},$
(2.4)

where $g_{k}(x)=\textnormal{eval}(p(x)/(x-a)^{k};q(x))$.

###### Proof.

Let $p(x)(x-a)=s(x)q(x)+r(x)$ for $\textnormal{deg}(r)<\textnormal{deg}(q)$.
Then, by $\textnormal{deg}(p)<\textnormal{deg}(q)$ we can easily deduce that
$\textnormal{deg}(s)=0$, i.e., $s(x)=c$ a constant. By the definition of eval
operator we have $r(x)=\textnormal{eval}(p(x)(x-a);q(x))=g_{-1}(x)$. Thus,
upon substitution by $x=a$ and $r(x)=g_{-1}(x)$ into the above equation we
have

$0=cq(a)+g_{-1}(a),\ \textnormal{ implies }c=-\frac{g_{-1}(a)}{q(a)}.$

Inducting on $k$ one can easily prove the result. ∎

Equipped with the above lemmas we now construct an algebraic framework for
sequences generated by rational polynomials. A generating function $F(x-a)$
about the point $x-a=0$ is the formal power series

$F(x-a)=\sum^{\infty}_{k=0}b_{k}(x-a)^{k}.$

whose coefficients form the sequence $(b_{k})$.

If the sequence $(b_{k})$ satisfies a finite linear recurrence relation then
one can show that $F(x-a)$ can be expressed as a rational polynomial
$p(x)/q(x)$ where $p(x),q(x)$ and $q(a)\neq 0$ [3]. In this work, we only
consider sequences generated by proper rational polynomials.

A formal power series expansion of $F(x)$ can also be obtained about the point
$x-a=\infty$ which yields the sequence $(b_{-k})$ with negative indices. In
order to obtain the coefficients with negative index

$F^{o}(x-a)=\sum_{k=1}^{\infty}b_{-k}(x-a)^{k}.$

The coefficients of the negative index is given by [3]

$F^{o}(x-a)=-F\left(\frac{1}{x-a}\right).$

Based on the above lemmas we now define the generating polynomial of a
sequence given by the generating $p(x)/q(x)$ with a formal power series
centered about $x=a$ by

$g_{k}(x)=\textnormal{eval}\left(p(x)(x-a)^{-k};q(x)\right)$

for $k\in\mathbb{Z}$ and $b_{k}=g(a)/q(a)$.

We can prove the following result immediately from Lemma 2.5 and Lemma 2.6.

######  Theorem 2.7 (Generating Polynomials).

The generating function $p(x)/q(x)$ (with $q(a)\neq 0$) for the sequence
$(b_{k})$ centered about $x=a$, i.e.,

$\frac{p(x)}{q(x)}=\sum^{\infty}_{k=0}b_{k}(x-a)^{k}$

has the generating polynomial

$g_{k}(x)=\textnormal{eval}\left((x-a)^{-k}p(x);q(x)\right)$

and $b_{k}=g_{k}(a)/q(a)$. Furthermore, the negative indexed coefficient
associated with the recurrence relation on the coefficients $(b_{k})$ can also
be obtained using $g_{k}(x)$ by considering negative values of $k$.

The relation between the positive and negative index polynomials can be stated
succinctly for a special case.

######  Corollary 2.8 (Reciprocity Law).

If $p(x)=1$ then the generating polynomial $g_{k}(x)$ and $g_{-k}(x)$ are
reciprocal of each other mod $q(x)$, i.e.,

$g_{k}(x)g_{-k}(x)=1\mod\ q(x).$

Therefore, the set of generating polynomials

$G=\left\\{\textnormal{eval}\left((x-a)^{-k};q(x)\right):k\in\mathbb{Z}\right\\}$
(2.5)

forms an infinite abelian group under multiplication modulo $q(x)$.

The generating polynomials also satisfy a recurrence relation mod $q(x)$.
Indeed, suppose $q(x)=\sum_{j=0}^{s}\alpha_{j}(x-a)^{j}$. Consider the
expression mod $q(x)$

$\sum^{s}_{j=0}\alpha_{j}g_{k+s-j}(x)=\sum_{j=0}^{s}\alpha_{j}\textnormal{eval}\left((x-a)^{k+s-j};q(x)\right).$

By the linearity of the eval operator we have

$\displaystyle\sum^{s}_{j=0}\alpha_{j}g_{k+s-j}(x)$ $\displaystyle=$
$\displaystyle\textnormal{eval}\left(\sum_{j=0}^{s}\alpha_{j}(x-a)^{k+s-j};q(x)\right)$
$\displaystyle=$
$\displaystyle\textnormal{eval}\left(q(x)(x-a)^{k};q(x)\right)$
$\displaystyle=$ $\displaystyle\beta(x)q(x)\textnormal{ rem }q(x)=0,$

where $\beta(x)(x-a)^{k}=1\mod q(x)$ if $k$ is negative; otherwise,
$\beta(x)=(x-a)^{k}$.

Before we proceed to the degenerate Bernoulli polynomials we demonstrate
through an example the generality of our algebraic framework. We consider the
Fibonacci sequence.

######  Example 2.9 (Fibonacci Sequence).

It is well known that the Fibonacci sequence is given by the generating
function

$\frac{x}{1-x-x^{2}}=\sum^{\infty}_{k=0}F_{k}x^{k},$

where $p(x)=x,q(x)=1-x-x^{2}$, and $a=0$.

By the above lemmas we have the Fibonacci polynomial defined as

$F_{k}(x)=\textnormal{eval}\left(x^{-k+1};1-x-x^{2}\right).$

Since $(1+x)x=1\mod(1-x-x^{2})$ we can easily see that

$\textnormal{eval}(x^{-1};1-x-x^{2})=1+x.$

Thus by the property of eval

$\textnormal{eval}(x^{-k};1-x-x^{2})=(1+x)^{k}\textnormal{ rem }(1-x-x^{2}).$

Now, by a direct computation one can easily check that
$F_{0}(x)=x,F_{1}(x)=1,F_{2}(x)=1+x,F_{3}(x)=2+x$ which when evaluated at
$x=0$ we obtain the required sequence. Moreover, for negative indices we have
$F_{-1}(x)=1,F_{-2}(x)=x,F_{-3}(x)=1-x$ which again when evaluated at $x=0$
give us the Fibonacci numbers with negative indices.

Furthermore,

$\textnormal{eval}(x^{-k};1-x-x^{2})=(1+x)^{k}\textnormal{ rem }(1-x-x^{2}).$

Therefore, we can write a recursive relation

$F_{n+1}(x)=(x+1)F_{n}(x)\textnormal{ rem }(1-x-x^{2}),$

and $F_{0}(x)=x$. If we set $F_{n}(x)=a_{0}+a_{1}x$ then we can compute
$F_{n+1}(x)=(a_{0}+a_{1})+a_{0}x$. A matrix realization of this transformation
is given by

$\begin{pmatrix}1&1\\\ 1&0\end{pmatrix}\begin{pmatrix}a_{0}\\\
a_{1}\end{pmatrix}=\begin{pmatrix}a_{0}+a_{1}\\\ a_{0}\end{pmatrix},$

which, although derived by a different approach, is the well known Fibonacci
Q-matrix [1].

##  3\. The Polynomial $\Psi_{m}(x)$

For $m$ a positive integer. We denote the polynomial

$\Psi_{m}(x)=\frac{1-x^{m}}{1-x}.$

The eval operator behaves in a very simpler manner with respect to
$\Psi_{m}(x)$.

######  Rule 3.1 (Substitution Rule).

$\textnormal{eval}(x^{j};\Psi_{m}(x))=x^{j}\textnormal{ rem
}\Psi_{m}(x)=\left\\{\begin{array}[]{@{}l@{\thinspace}l}x^{j\%m}&\textnormal{
if }j\%m\neq m-1\\\ -\sum^{m-2}_{i=0}x^{i}&\textnormal{ if }j\%m=m-1.\\\
\end{array}\right.$ (3.1)

where $\%$ operator is the remainder in the ring of integers.

###### Proof..

Suppose $j=md+r$, for $0\leq r<m$. Then, the result follows from
$x^{md+r}=((x^{m}-1)+1)^{d}x^{r}=q(x)(x^{m}-1)+x^{r}=q(x)(x-1)\Psi_{m}(x)+x^{r}.$
∎

In [13], the first author showed that $\Psi_{m}(x)$ is naturally related to
the degenerate Bernoulli numbers. Indeed, the degenerate Bernoulli numbers
$\beta_{k}(\lambda)$, where $\lambda\neq 0$, is given by the generating
function

$\frac{t}{(1+\lambda
t)^{1/\lambda}-1}=\sum_{k=0}^{\infty}\beta_{k}(\lambda)\frac{t^{k}}{k!}.$
(3.2)

By setting $x=(1+\lambda t)$ and $\lambda=1/m$ in (3.2) we obtain the
generating function

$m\frac{1-x}{1-x^{m}}=\frac{m}{\Psi_{m}(x)}=\sum_{k=0}^{\infty}(-1)^{k}\frac{\tilde{\beta}_{k}(m)}{k!}(1-x)^{k}.$

Also, note that $B_{k}=\beta_{k}(1/m)$ as $m\rightarrow\infty$.

By the framework developed in Section 2 for $p(x)/q(x)=1/\Psi_{m}(x)$ and
obtaining power series about $x=1$ we have

$f_{k}^{(m)}(x)=\textnormal{eval}\left((1-x)^{-k};\Psi_{m}(x)\right),$

and $f^{(m)}_{k}(1)=(-1)^{k}\tilde{\beta}_{k}(m)/k!$. Furthermore, we can also
define the above polynomial for negative $k$. So, we have the following
result.

######  Proposition 3.2.

$f_{-k}^{(m)}(1)=0\textnormal{ for }1\leq k<(m-1).$

###### Proof.

For $k$ with $1\leq k<(m-1)$ we have

$f_{-k}^{(m)}(x)=\textnormal{eval}((1-x)^{k};\Psi_{m}(x))=(1-x)^{k}.$

The above equations holds because the degree of $(1-x)^{k}$ is less than that
of $\Psi_{m}(x)$. Substituting $x=1$ in the above equation we have the result.
∎

######  Remark 3.3.

Note that we can also define $\tilde{\beta}_{k}(-m)$ for positive integer $m$.
But the analysis is similar to positive case. Indeed, consider the generating
function

$\frac{t}{(1-\frac{t}{m})^{-m}-1}.$

Let $x=1-t/m$. Then, $t=m(1-x)$. Upon substitution we have

$\displaystyle\frac{m(1-x)}{x^{-m}-1}$ $\displaystyle=$
$\displaystyle\frac{m(1-x)x^{m}}{1-x^{m}}=\frac{m}{\Psi_{m}(x)}-m(1-x)$
$\displaystyle=$
$\displaystyle\sum^{\infty}_{k=0}(-1)^{k}\tilde{\beta}_{k}(m)\frac{(1-x)^{k}}{k!}-m(1-x).$

Therefore we have

$\tilde{\beta}_{k}(-m)=\begin{cases}(-1)^{k}\tilde{\beta}_{k}(m),&\text{if
}m\neq 1\\\ -\tilde{\beta}_{1}(m)-m&\text{if }m=1.\end{cases}$

We now derive the explicit formula (1.2).

######  Lemma 3.4.

$f_{k}^{(m)}(x)=\textnormal{eval}\left(\frac{1}{(x-1)^{k}};\Psi_{m}(x)\right)=\left(\frac{1}{m}x\Psi^{\prime}_{m}(x)\right)^{k}\textnormal{
rem }\Psi_{m}(x).$

###### Proof.

Differentiating and multiplying by $x$ both sides of the equation

$(x-1)\Psi_{m}(x)=x^{m}-1$

we get

$x\Psi^{\prime}_{m}(x)(x-1)+(x)\Psi_{m}(x)=mx^{m}.$

Thus by taking mod $\Psi_{m}(x)$ we have

$x\Psi^{\prime}_{m}(x)(x-1)=m\mod\Psi_{m}(x).$

Raising both sides of the above equation by $k$ we have the result. ∎

By Lemma 2.4 we can also write

$f_{k}^{(m)}(x)=\left(\frac{\Psi_{m}(x)-m}{x-1}\right)^{k}\textnormal{ rem
}\Psi_{m}(x).$

##  4\. Periodicity of $f_{k}^{(m)}(x)=(-1)^{k}\tilde{\beta}_{k}(m,x)/k!$

In this section, we show that the polynomial $f_{k}^{(m)}(x)$ given in (1.2)
are periodic modulo a prime $p$ that are coprime to $m$, that is taking the
coefficients of $f_{k}^{(m)}(x)$ mod $p$ in $\mathbb{F}_{p}$. A direct
consequence is that the infinite abelian group formed by the generating
polynomials becomes isomorphic to a multiplicative subgroup of
$\mathbb{F}_{p^{m-1}}^{*}$ the Galois Field without the zero element.

Consider $p$ a prime satisfying $(m,p)=1$. We prove that the polynomial
$f_{k}^{(m)}(x)$ is periodic in $k$ with periodicity $p^{s}-1$, where $s$ is
smallest positive integer such that $p^{s}=1\mod m$. Notice that, although the
field we consider is $\mathbb{F}_{p}$, the condition we impose is based on the
mod $m$. Results with this type of role reversal of $p$ and $m$ are generally
classified as reciprocity laws [14].

In the following result we use the well known fact raising a polynomial
$g(x)\in\mathbb{F}_{p}[x]$ to power $p$ gives us $g(x)^{p}=g(x^{p}).$

######  Theorem 4.1 (Periodicity).

$f_{p^{s}-1+n}^{(m)}(x)=f_{n}^{(m)}(x)\mod p,$

for $n$ a positive integer and $p^{s}=1\mod m$.

###### Proof.

Let $g(x)=\frac{1}{m}x\Psi_{m}^{\prime}(x)$. Then, by (1.2) and the
substitution rule in Lemma 3.1 we have

$\displaystyle f_{p^{s}-1+n}^{(m)}(x)$ $\displaystyle=$ $\displaystyle
g(x)^{p^{s}-1+n}\textnormal{ rem
}\Psi_{m}(x)=\left(g(x^{p^{s}})g(x)^{n-1}\right)\textnormal{ rem }\Psi_{m}(x)$
$\displaystyle=$
$\displaystyle\left(g(x^{p^{s}\%m})g(x)^{n-1}\right)\textnormal{ rem
}\Psi_{m}(x).$

By the hypothesis we have $p^{s}=1\mod m$. Thus
$f^{(m)}_{p^{s}-1+n}(x)=g(x)^{n}\textnormal{ rem }\Psi_{m}(x)$. ∎

Thus the degenerate Bernoulli polynomials are periodic with a periodicity
$p^{s}-1$ for the smallest $s$ satisfying $p^{s}=1\mod m$. In particular,
$f^{(m)}_{p^{s}-1}(x)=f^{(m)}_{0}(x)=1$.

As a consequence of this result we observe that the polynomial in
$\mathbb{F}_{p}$

$f^{(m)}_{k}(x)=\textnormal{eval}\left(\frac{1}{(1-x)^{k}};\Psi_{m}(x)\right)$

can be written as

$f^{(m)}_{k}(x)=\textnormal{eval}\left((1-x)^{p^{s}-1-k};\Psi_{m}(x)\right)=(1-x)^{n(p^{s}-1)-k}\textnormal{
rem }\Psi_{m}(x)$

for some large $n$, which amounts to only polynomial evaluation.

######  Corollary 4.2.

$\tilde{\beta}_{k}(m)\equiv 0\mod p$ for $p^{s}-1-k<m-1$.

It can be easily shown that the set

$G=\\{f_{k}^{(m)}(x):k\in\mathbb{Z}\\}$

is an infinite abelian group under multiplication modulo $\Psi_{m}(x)$. With
the above periodicity condition one can show that when we reduce the
coefficient of the polynomials in $G$ modulo $p$ then we have a finite abelian
group with at most $p^{s}-1$ elements where $s$ is the smallest positive
integer such that $p^{s}=1\mod m$.

######  Corollary 4.3.

Let $G_{p}=\\{f_{p}(x):f(x)\in G\\},$ where $f_{p}(x)$ is the polynomial
obtained by taking $\mod p$ of the coefficients of $f(x)$. Then, $G_{p}$ is a
subgroup of $\mathbb{F}^{*}_{p^{m-1}}$, where $s$ is the smallest positive
integer such that $p^{s}=1\mod m$.

By [4], if $p^{m-1}$ is sufficiently large, we can in fact show that $G_{p}$
is equidistributed in $\mathbb{F}_{p^{m-1}}$. The elements of $G_{p}$ span
whole of $\mathbb{F}_{p^{m-1}}$ over $\mathbb{F}_{p}$. Indeed, the following
elements of $G_{p}$

$\textnormal{eval}\left((1-x)^{k};\Psi_{m}(x)\right)=(1-x)^{k}\textnormal{ for
}0\leq k\leq m-2$

form a linearly independent set with $m-1$ elements. Therefore, no proper
subfield $S$ of $\mathbb{F}_{p^{m-1}}$ contains $G_{p}$. Hence, one can find a
$\eta\in(0,1]$ such that

$|S\cap G_{p}|\leq|G_{p}|^{1-\eta},$

where $|A|$ is the cardinality of $A$.

######  Theorem 4.4 (Bourgain et.al.[4]).

Let $0<\eta\leq 1$ be an arbitrary number and $H$ be a multiplicative subgroup
of $\mathbb{F}^{*}_{p^{n}}$ with

$|H|\geq p^{n\max\\{135/\eta,180000\\}/\log_{2}n\log_{2}p}.$

Suppose that for any proper subfield $S$ the condition $|H\cap
S|\leq|H|^{1-\eta}$ holds. Then for sufficiently large $p^{n}$, there is an
exponential sum estimate

$|\sum_{h\in H}\psi(h)|<100|H|2^{-4.5\cdot 10^{-3}(n\log_{2}p)^{0.1}},$

where $\psi$ is the additive character $\psi(t)=e^{2\pi iTr(at)/p}$ for some
given $a\neq 0$.

From the above result we can justify that for a sufficiently large $p^{m-1}$
the subgroup $G_{p}$ is equidistributed in $\mathbb{F}_{p^{m-1}}^{*}$.

##  5\. Computing $f_{k}^{(m)}(x)$ via Linear Algebra

In the previous sections we have seen that the degenerate Bernoulli polynomial
$f_{k}^{(m)}(x)=(-1)^{k}\tilde{\beta}_{k}(m)/k!$ is computed by means of
taking the remainder of the power of the polynomial
$((1/m)x\Psi^{\prime}_{m}(m))$ with $\Psi_{m}(x)$. It is well known that one
can formulate these operations in terms of matrix representation.

In order to obtain a matrix realization of the process involved in computing
$f_{k}^{(m)}(x)$ notice that the following recurrence relation holds

$f_{k+1}^{(m)}(x)=(\frac{1}{m}x\Psi^{\prime}_{m}(x)f_{k}^{(m)}(x))\textnormal{
rem }\Psi_{m}(x)$

and $f^{(m)}_{0}(x)=1$. For convenience we will ignore the $(1/m)$ factor in
the expression.

By the linearity of the remainder operator, it suffices to consider the action
of multiplying by $x\Psi_{m}^{\prime}(x)$ with $x^{j}$ for $j=0,\cdots,(m-2)$.
We have

$x^{j}\mapsto\left(x^{j+1}\Psi_{m}^{\prime}(x)\right)\textnormal{ rem
}\Psi_{m}(x).$

One can easily obtain a matrix representation of this mapping taking the set
$\\{1,x,\cdots,x^{m-2}\\}$ as the basis.

######  Example 5.1.

For $m=4$ we will have a $3\times 3$ matrix

$\begin{pmatrix}-3&1&1\\\ -2&-2&2\\\ -1&-1&-1\end{pmatrix}.$

Fortunately, we can provide a more elegant formulation through Circulant
matrices - thanks to the substitution rule given in Lemma 3.1. The
substitution rule can be expressed in two stages by deferring the
substitution. The substitution is realized as a multiplication of matrices
from each stage.

######  Rule 5.2 (Deferred Substitution Rule).

While applying the Substitution Rule 3.1 first substitute $x^{j}$ with
$x^{j\%m}$ for all $j$ to produce polynomials of degree $m-1$. Later
substitute $x^{m-1}$ factors with $-\sum^{m-2}_{j=0}x^{j}$.

We first consider the product

$g(x)=x\Psi^{\prime}_{m}(x)f_{k}^{(m)}(x)=(x+2x^{2}+\cdots+(m-1)x^{m-1})(\alpha_{0}+\cdots+\alpha_{m-1}x^{m-1}).$

On application of the Deferred Substitution Rule 5.2 we first replace $x^{j}$
with $x^{j\%m}$ to obtain

$\displaystyle g(x)$ $\displaystyle=$
$\displaystyle(0\alpha_{0}+(m-1)\alpha_{1}+\cdots+\alpha_{m-1})$
$\displaystyle+(\alpha_{0}+0\alpha_{1}+(m-1)\alpha_{2}+(m-2)\alpha_{3}+\cdots+2\alpha_{m-2})x$
$\displaystyle+(2\alpha_{0}+1\alpha_{1}+0\alpha_{2}+(m-1)\alpha_{3}+\cdots+3\alpha_{m-2})x^{2}$
$\displaystyle+\cdots+$
$\displaystyle+\cdots+((m-1)\alpha_{0}+\cdots+0\alpha_{m-1})x^{m-1}$

The above product can be expressed in terms of a Circulant matrix as follows

$C_{m}=\left(\begin{array}[]{cccccc}0&m-1&m-2&\cdots&2&1\\\
1&0&m-1&\cdots&3&2\\\ 2&1&0&\cdots&4&3\\\
\vdots&\vdots&\vdots&\ddots&\vdots&\vdots\\\ m-2&m-3&m-4&\cdots&0&m-1\\\
m-1&m-2&m-3&\cdots&1&0\\\ \end{array}\right)_{m\times m}$

This is a right circulant matrix, in which each row is obtained from the
preceding row by a cyclic shift of the entries to the right.

Now, we apply the second substitution $x^{m-1}$ with $-\sum^{m-2}_{j=0}x^{j}$
and retaining $x^{j}$ fixed for $j\neq m-1$ to obtain the matrix

$R_{m}=\begin{pmatrix}1&0&0&\cdots&0&-1\\\ 0&1&0&\cdots&0&-1\\\
\vdots&\cdots&\ddots&\cdots&0&-1\\\ 0&0&0&\cdots&1&-1\\\
0&0&0&\cdots&0&0\end{pmatrix}_{m\times m}.$

######  Definition 5.3 (Degenerate Bernoulli Matrix).

Given two integers $m>0$ and $k\geq 0$, we define the degenerate Bernoulli
matrix as the

$\mathcal{B}_{m}=-mR_{m}C_{m}.$

Note the $m$ factor which we skipped at the beginning for simplifying the
discussion. The degenerate Bernoulli number is given by

$\tilde{\beta}_{k}(m)=\frac{1}{k!}\mathcal{B}_{m}^{k}e_{1},$

where $e_{1}=(1,0,\cdots,0)^{T}$.

One can further simplify the multiplications by the following lemma.

######  Lemma 5.4.

$R_{m}C_{m}R_{m}=R_{m}C_{m}$.

###### Proof.

We write the matrices $R_{m}$ and $C_{m}$ in block matrix form

$R_{m}=\left(\begin{array}[]{c|c}I_{(m-1)\times(m-1)}&-\mathbbmtt{1}_{(m-1)\times
1}\\\ \hline\cr O_{1\times(m-1)}&0\end{array}\right)$

and

$C_{m}=\left(\begin{array}[]{c|c}A&X\\\ \hline\cr Y&0\end{array}\right)$

where $\mathbbmtt{1}_{(m-1)\times 1}$ is a column matrix with all entries
being 1, $Y=\begin{pmatrix}m-1&m-2&\ldots&1\end{pmatrix},$
$X=(1,2,\cdots,m-1)^{T},$ and

$A=\begin{pmatrix}0&m-1&m-2&\cdots&2\\\ 1&0&m-1&\cdots&3\\\ 2&1&0&\cdots&4\\\
\vdots&\vdots&\vdots&\ddots&\vdots\\\ m-2&m-3&m-4&\cdots&0\\\ \end{pmatrix},$

By a direct computation we have

$R_{m}C_{m}=\left(\begin{array}[]{c|c}I&-\mathbbmtt{1}\\\ \hline\cr
O&0\end{array}\right)\left(\begin{array}[]{c|c}A&X\\\ \hline\cr
Y&0\end{array}\right)=\left(\begin{array}[]{c|c}A-\mathbbmtt{1}Y&X\\\
\hline\cr O&0\end{array}\right)$

and

$R_{m}C_{m}R_{m}=\left(\begin{array}[]{c|c}A-\mathbbmtt{1}Y&X\\\ \hline\cr
O&0\end{array}\right)\left(\begin{array}[]{c|c}I&-\mathbbmtt{1}\\\ \hline\cr
O&0\end{array}\right)=\left(\begin{array}[]{c|c}A-\mathbbmtt{1}Y&-A\mathbbmtt{1}+\mathbbmtt{1}Y\mathbbmtt{1}\\\
\hline\cr O&0\end{array}\right).$

It is easy to see that

$\mathbbmtt{1}Y\mathbbmtt{1}=\frac{m(m-1)}{2}\mathbbmtt{1}\textnormal{ and
}A\mathbbmtt{1}=\frac{m(m-1)}{2}\mathbbmtt{1}-X.$

Thus $-A\mathbbmtt{1}+\mathbbmtt{1}Y\mathbbmtt{1}=X$ and hence
$R_{m}C_{m}R_{m}=R_{m}C_{m}.$ ∎

It is easy to see that $R_{m}^{2}=R_{m}$. Therefore, by the above lemma we can
easily deduce $(R_{m}C_{m}R_{m})^{k}=R_{m}C_{m}^{k}$. Indeed, inductively
arguing on $k$, we have by Lemma 5.4

$\displaystyle(R_{m}C_{m})^{k+1}$ $\displaystyle=$
$\displaystyle(R_{m}C_{m})(R_{m}C_{m})^{k}=(R_{m}C_{m})R_{m}C_{m}^{k}$
$\displaystyle=$ $\displaystyle(R_{m}C_{m}R_{m})C^{k+1}_{m}=R_{m}C^{k+1}_{m}.$

By the above discussion we can see the following result.

######  Theorem 5.5.

The $k^{th}$ degenerate Bernoulli number is given by the $t^{k}$ term in
$R_{m}e^{-tmC_{m}}$, where we use the notation of exponentiation of a matrix
$e^{tB}=\sum_{t=0}^{\infty}\frac{t^{k}}{k!}B^{k}$.

A special feature of the circulant matrix is that they are diagonalizable with
the discrete fourier transform $F$ [6]. We can write

$C_{m}=F^{-1}D_{m}F$

so that $R_{m}C^{k}_{m}=R_{m}F^{-1}D^{k}_{m}F$. The exponential form is given
by $R_{m}F^{-1}_{m}e^{-tmD_{m}}F$. From the diagonalization of the circulant
matrices we can easily see that the eigenvalues $\lambda_{j}$ of $C_{m}$ are
given by

$\lambda_{j}=\sum_{i=0}^{m-2}i\omega_{m}^{ij},$

where $\omega_{m}\neq 1$ and $\omega_{m}^{m}=1$.

The matrix representation for the negative index is simpler as the recursive
formula is simpler

$f_{-k-1}^{(m)}(x)=(1-x)f_{-k}^{(m)}(x)\textnormal{ rem }\Psi_{m}(x).$

The representation is again a right circulant matrix given by
$R_{m}\tilde{C}_{m}$, where

$\tilde{C}_{m}=\begin{pmatrix}1&-1&0&\cdots&0&0\\\ 0&1&-1&\cdots&0&0\\\
\vdots&&\ddots&\cdots&&\vdots\\\ 0&0&0&\cdots&1&-1\\\ -1&0&0&\cdots&0&1\\\
\end{pmatrix}_{m\times m},$

whose eigenvalues are

$\tilde{\lambda}_{j}=\omega_{m}^{j^{2}}-\omega_{m}^{j(j+1)},$

where $\omega_{m}\neq 1$ satisfying $\omega_{m}^{m}=1$.

##  6\. Palindrome and Anti-Palindrome Property

In this section, we show that the degenerate Bernoulli polynomial
$\tilde{\beta}_{k}(m,x)$ has palindromic properties if $m$ is odd. A
consequence of this is that the degenerate Bernoulli numbers vanish for
certain $k$ depending on $m$.

######  Definition 6.1 (Palindromic Polynomial [12, 18]).

Let $p(x)=\alpha_{r}x^{r}+\cdots+\alpha_{s}x^{s}$ be a non-zero polynomial,
with real coefficents and $\alpha_{r},\alpha_{s}\neq 0$. The darga of $p$ is
$\textnormal{dg}(p)=r+s$. We say that a polynomial $p$ of darga $n$ is
palindromic if $x^{n}p(1/x)=p(x)$ i.e., $\alpha_{j}=\alpha_{n-j}$ for all $j$.
We say that the polynomial $p$ is anti-palindromic if $x^{n}p(-1/x)=p(x)$
i.e., $\alpha_{j}=-\alpha_{n-j}$ for all $j$. Collection of palindromic and
anti-palindromic polynomials of darga $n$ are denoted by $\mathscr{P}^{(n)}$
and $\mathscr{A}^{(n)}$ respectively.

Note that, if the zero polynomial is included, we could consider both
$\mathscr{P}^{(n)}$ and $\mathscr{A}^{(n)}$ as vector spaces over
$\mathbb{R}$. So, for convenience we assume that $0$ polynomial is of any
darga. It is easy to see that the set

$\\{x^{j}+x^{n-j}:j=0,\cdots,n\\}$

is a basis set for $\mathscr{P}^{(n)}$ and

$\\{x^{j}-x^{n-j}:j=0,\cdots,n\\}$

for $\mathscr{A}^{(n)}$. We prove the following result.

######  Theorem 6.2.

Let $m$ be an odd integer and $d$ an integer. Then the following relation
holds

$\tilde{\beta}_{k}(md+2,x)\in\begin{cases}\mathscr{P}^{(m-2)}&\textnormal{ for
}$d$\textnormal{ even }\\\ \mathscr{A}^{(m-2)}&\textnormal{ for
}$d$\textnormal{ odd }.\end{cases}$

Thus, $\tilde{\beta}_{k}(md+2)=0$ for $d$ odd.

The proof of this result relies on a multiplication modulo $\Psi_{m}(x)$
operator $M_{m}$ on polynomials of degree $(m-2)$ by

$M_{m}(p(x))=\left((1-x)^{m}p(x)\right)\textnormal{ rem }\Psi_{m}(x).$

######  Lemma 6.3.

For $m$ an odd integer, the linear map

$M_{m}:\mathscr{P}^{(m-2)}\rightarrow\mathscr{A}^{(m-2)}$

is an isomorphism.

###### Proof.

It is easy to show that $M_{m}$ is a linear operator modulo $\Psi_{m}(x)$.
Thus it suffices to prove that on a basis element $x^{j}+x^{m-2-j}$, for
$0\leq j\leq m-2$, the mapping $M_{m}$ yields an anti-palindromic polynomial
of darga $(m-2)$.

By the substitution rule (3.1) and a rearrangement of terms the following
equations hold modulo $\Psi_{m}(x)$:

$\displaystyle x^{j}(1-x)^{m}$ $\displaystyle=$
$\displaystyle\sum^{m-j-2}_{\alpha=0}(-1)^{\alpha}\begin{pmatrix}m\\\
\alpha\end{pmatrix}x^{j+\alpha}$
$\displaystyle+(-1)^{m-j-1}\left(\begin{pmatrix}m\\\
m-j-1\end{pmatrix}(-1-x-\cdots-x^{m-2})\right)$
$\displaystyle+\sum_{\beta=0}^{j+1}(-1)^{m-j+\beta}\begin{pmatrix}m\\\
m-j+\beta\end{pmatrix}x^{\beta}$

and

$\displaystyle x^{m-2-j}(1-x)^{m}$ $\displaystyle=$
$\displaystyle\sum^{j}_{\beta=0}(-1)^{j-\beta}\begin{pmatrix}m\\\
j-\beta\end{pmatrix}x^{m-2-\beta}$
$\displaystyle+(-1)^{j+1}\left(\begin{pmatrix}m\\\
m-j-1\end{pmatrix}(-1-x-\cdots-x^{m-2})\right)$
$\displaystyle+\sum_{\alpha=0}^{m-j-2}(-1)^{m-\alpha}\begin{pmatrix}m\\\
m-\alpha\end{pmatrix}x^{m-j-\alpha-2}$

It is given that $m$ is odd so we have $(-1)^{k}=-(-1)^{m-k}$. By the well-
known combinatorial identity

$\begin{pmatrix}m\\\ k\end{pmatrix}=\begin{pmatrix}m\\\ m-k\end{pmatrix}$

we have $x^{j}(1-x)^{m}\pm x^{m-j-2}(1-x)^{m}$ modulo $\Psi_{m}(x)$ equal to

$\displaystyle\sum_{\alpha=0}^{m-j-2}(-1)^{\alpha}\begin{pmatrix}m\\\
\alpha\end{pmatrix}\left(x^{j+\alpha}\mp
x^{m-j-s-2}\right)+\sum_{\beta=0}^{j-1}(-1)^{j-\beta}\begin{pmatrix}m\\\
j-\beta\end{pmatrix}(x^{m-2-\beta}\mp x^{\beta})$
$\displaystyle+2\delta(-1)^{j}\begin{pmatrix}m\\\
m-j-1\end{pmatrix}(1+x+\cdots+x^{m-2}),$

where $\delta=0$ if $+$ is chosen; otherwise $\delta=1$. Thus palindromic is
transformed to anti-palindromic and vice-versa.

The map $M_{m}$ is one-one. To see this suppose $(1-x)^{m}p(x)\textnormal{ rem
}\Psi_{m}(x)=0$ for some $p(x)\in\mathscr{P}^{(m-2)}$. Then, we can write
$(1-x)^{m}p(x)=\Psi_{m}(x)q(x)$ for some polynomial $q(x)$. Since
$\Psi_{m}(1)\neq 0$, this means all the roots of $\Psi_{m}(x)$ have to be
shared by a polynomial of degree atmost $(m-2)$ degree. Therefore, this is
possible only if $p(x)=0$.

∎

###### Proof of Theorem 6.2.

It is enough if the result is proved for $\mod p$ case for an arbitrary prime
$p$, of course, relatively coprime to $m$. Further, by the periodicity of
$f_{k}^{(m)}(x)$ we have to just show for the case multiplications by
$(1-x)^{m}$ modulo $\Psi_{m}(x)$. By Lemma 6.3, all that remains to show that
is $f_{2}^{(m)}(x)\in\mathscr{P}^{(m-2)}$ i.e.,
$(x\Psi^{\prime}_{m}(x))^{2}\textnormal{ rem }\Psi_{m}(x).$ By the matrix
representation… it is sufficient to look at the $j^{th}$ row and
$(m-2-j)^{th}$ row for $j=0,\cdots,(m-2)$. The $j^{th}$ row in the matrix is
given by

$(j,\cdots,1,0,m-1,\cdots,(2j+2),(2j+1),\cdots,(j-1))$

and the $(m-2-j)^{th}$ row is given by

$((m-2j),\cdots,(m-2j-2),(m-2j-3),\cdots,0,(m-1),\cdots,(m-3-j)).$

The difference of both the above rows give us

$(\underbrace{a,\cdots,a}_{(j+1)\textnormal{
terms}},\underbrace{a-m,\cdots,a-m}_{(m-2j-2)\textnormal{ terms
}},\underbrace{a,\cdots,a}_{(j+1)\textnormal{ terms }})$

where $a=(m-2j-2)$. Taking dot product of the above vector with the vector
$(0,1,2,\cdots,m-1)$ we get the expression

$\frac{(m-2j-2)m(m-1)}{2}-m\left(\frac{(m-2-j)(m-1-j)}{2}-\frac{j(j+1)}{2}\right)=0$

Hence the $j^{th}$ term is equal to $(m-2-j)^{th}$ term for $j=0,\cdots,(m-2)$
in the polynomial which means it is a palindrome of darga $(m-2)$. ∎

Thus we have given an algebraic proof for the following result. Analytic proof
was given by Young [16].

######  Corollary 6.4.

$\tilde{\beta}_{md+2}(m)=0\textnormal{ for }m,d\textnormal{ odd. }$

##  7\. Sums of Products

Inspired by the formula (1) we look for a sum of products formula for the
degenerate Bernoulli numbers. For any real number $r,$ the falling factorial
defined as $(r)_{k}=r(r-1)\cdots(r-k+1)$ and generalized falling factorial
defined as $(r|\lambda)_{k}=r(r-\lambda)\cdots(r-(k-1)\lambda),$ for
$k\in\mathbb{N}.$ For a positive integer $a,$ we denote
$\sigma_{k}(\lambda,a)=\displaystyle\sum_{i=0}^{a}(i|\lambda)_{k}.$ We note
that

$\lambda^{k}\sigma_{k}(1/\lambda,a)=\displaystyle\sum_{i=0}^{a}(\lambda
i|1)_{k}=\sum_{i=0}^{a}(\lambda i)_{k}.$

Also note that $(-r)_{k}=(-1)^{k}\langle r\rangle_{k},$ where $\langle
r\rangle_{k}$ is a rising factorial and is defines as $r(r+1)\cdots(r+k-1).$
Further, we denote that

$\widetilde{\sigma}_{k}(\lambda,a)=\lambda^{k}\sigma_{k}(1/\lambda,a).$

The following remark is useful.

######  Remark 7.1.

  1. (1)

For a positive integer $a,$ the generating function expressed as below (see
[16]):

$\frac{(1+\lambda t)^{(a+1)\mu}-1}{(1+\lambda
t)^{\mu}-1}=\sum_{k=0}^{\infty}\sigma_{k}(\lambda,a){t^{k}\over k!}$ (7.1)

  2. (2)

The following Cauchy product formulae is well-known for the exponential
generating functions:

$\left(\sum_{k=0}^{\infty}a_{k}{x^{k}\over
k!}\right)\left(\sum_{k=0}^{\infty}b_{k}{x^{k}\over
k!}\right)=\left(\sum_{k=0}^{\infty}c_{k}{x^{k}\over k!}\right),$

where
$c_{k}=\displaystyle\sum_{k_{1}+k_{2}=k}\binom{k}{k_{1},k_{2}}a_{k_{1}}b_{k_{2}}.$

  3. (3)

For any non-zero rational number $r,$ the Taylor’s series expansion about
$x=1$ is given as

$x^{r}=\sum_{k=0}^{\infty}(-1)^{k}(r)_{k}\frac{(1-x)^{k}}{k!},$ (7.2)

We have the following corollary.

######  Corollary 7.2.

For positive integers $a,\ b,\ n_{1}$ and $n_{2},$ the following hold:

$\Psi_{a}(x^{n_{1}})=\displaystyle\sum_{k=0}^{\infty}(-1)^{k}\widetilde{\sigma}_{k}(n,a-1){(1-x)^{k}\over
k!}$

and

$x^{-bn_{1}}{\Psi_{a}(x^{n_{2}})}=\sum_{k=0}^{\infty}\binom{k}{k_{1},k_{2}}(-1)^{k_{2}}\langle
bn_{1}\rangle_{k_{1}}\widetilde{\sigma}_{k_{2}}(n_{1},a-1){(1-x)^{k}\over k!}$

###### Proof.

First equation is immediate if we write $(1+\lambda t)=x$ and $\lambda={1\over
n}$ in the equation (7.1).

By using Taylor series expansion (7.2), we have

$\displaystyle x^{-bn_{1}}$
$\displaystyle=\sum_{k=0}^{\infty}(-1)^{k}(-bn_{1})_{k}\frac{(1-x)^{k}}{k!}$
$\displaystyle=\sum_{k=0}^{\infty}\langle
bn_{1}\rangle_{k}\frac{(1-x)^{k}}{k!}$

Then it is easy to see that the second equation holds using Cauchy product for
exponential generating functions for $x^{-bn_{1}}$ and $\Psi_{a}(x^{n_{2}}).$
∎

Now, we have sums of product formulae

######  Theorem 7.3.

Let $m\geq 2$ and $n\geq 3$ be two integers that are co-prime. Assume that
$a,b,\alpha$ and $\beta$ are smallest possible positive integers such that
$an-bm=1$ and $\alpha m-\beta n=1.$ For $k\in\mathbb{N},$ if $a>\beta$ then we
have

$\sum_{k_{1}+k_{2}=k}{\widetilde{\beta}_{k_{1}}(m)\over
k_{1}!}{\widetilde{\beta}_{k_{2}}(n)\over
k_{2}!}=n\sum_{k_{1}+k_{2}=k}\sum_{s_{1}+s_{2}=k_{1}}\frac{\left(-bm\right)_{s_{1}}}{s_{1}!}\frac{\widetilde{\sigma}_{s_{2}}(n,a-1)}{s_{2}!}\frac{\widetilde{\beta}_{k_{2}}(m)}{k_{2}!}\\\
-m\sum_{k_{1}+k_{2}=k}\sum_{s_{1}+s_{2}=k_{1}}\frac{\left(-bm\right)_{s_{1}}}{s_{1}!}\frac{\widetilde{\sigma}_{s_{2}}(m,b-1)}{s_{2}!}\frac{\widetilde{\beta}_{k_{2}}(n)}{k_{2}!}$

else if $a<\beta$

$\sum_{k_{1}+k_{2}=k}{\widetilde{\beta}_{k_{1}}(m)\over
k_{1}!}{\widetilde{\beta}_{k_{2}}(n)\over
k_{2}!}=m\sum_{k_{1}+k_{2}=k}\sum_{s_{1}+s_{2}=k_{1}}\frac{\left(-\beta
n\right)_{s_{1}}}{s_{1}!}\frac{\widetilde{\sigma}_{s_{2}}(m,\alpha-1)}{s_{2}!}\frac{\widetilde{\beta}_{k_{2}}(n)}{k_{2}!}\\\
-n\sum_{k_{1}+k_{2}=k}\sum_{s_{1}+s_{2}=k_{1}}\frac{\left(-\beta
n\right)_{s_{1}}}{s_{1}!}\frac{\widetilde{\sigma}_{s_{2}}(n,\beta-1)}{s_{2}!}\frac{\widetilde{\beta}_{k_{2}}(m)}{k_{2}!}$

###### Proof.

We prove the case $an-bm=1$ with $a>\beta.$ Now consider the generating
function

$\displaystyle\frac{x-1}{\Psi_{m}(x)\Psi_{n}(x)}$ $\displaystyle=\frac{x^{an-
bm}-1}{\Psi_{m}(x)\Psi_{n}(x)}$
$\displaystyle=\frac{x^{-bm}(x^{an}-x^{bm})}{\Psi_{m}(x)\Psi_{n}(x)}$
$\displaystyle=\frac{x^{-bm}(x^{an}-1)}{\Psi_{m}(x)\Psi_{n}(x)}-\frac{x^{-bm}(x^{bm}-1)}{\Psi_{m}(x)\Psi_{n}(x)}$
$\displaystyle=\frac{x^{-bm}(x-1)\Psi_{a}(x^{n})}{\Psi_{m}(x)}-\frac{x^{-bm}(x-1)\Psi_{b}(x^{m})}{\Psi_{n}(x)}$

Therefore

$\frac{1}{\Psi_{m}(x)\Psi_{n}(x)}=\frac{x^{-bm}\Psi_{a}(x^{n})}{\Psi_{m}(x)}-\frac{x^{-bm}\Psi_{b}(x^{m})}{\Psi_{n}(x)}$
(7.3)

We note that

$\displaystyle\frac{1}{\Psi_{m}(x)\Psi_{n}(x)}$
$\displaystyle=\left(\sum_{k=0}^{\infty}(-1)^{k}{\widetilde{\beta}_{k}(m)\over
m}\frac{(1-x)^{k}}{k!}\right)\left(\sum_{k=0}^{\infty}(-1)^{k}{\widetilde{\beta}_{k}(n)\over
n}\frac{(1-x)^{k}}{k!}\right)$
$\displaystyle=\sum_{k=0}^{\infty}(-1)^{k}\sum_{k_{1}+k_{2}=k}\binom{k}{k_{1},k_{2}}{\widetilde{\beta}_{k_{1}}(m)\over
m}{\widetilde{\beta}_{k_{2}}(n)\over n}\frac{(1-x)^{k}}{k!},$

${x^{-bm}\Psi_{a}(x^{n})\over\Psi_{m}(x)}=\left(\sum_{k=0}^{\infty}\sum_{k_{1}+k_{2}=k}\binom{k}{k_{1},k_{2}}(-1)^{k}\left(-bm\right)_{k_{1}}\widetilde{\sigma}_{k_{2}}(n,a-1){(1-x)^{k}\over
k!}\right)\times\\\
\left(\sum_{k=0}^{\infty}(-1)^{k}{\widetilde{\beta}_{k}(m)\over
m}\frac{(1-x)^{k}}{k!}\right)$ $\hskip 56.9055pt={1\over
m}\sum_{k=0}^{\infty}\sum_{k_{1}+k_{2}=k}\sum_{s_{1}+s_{2}=k_{1}}k!(-1)^{k}\frac{\left(-bm\right)_{s_{1}}}{s_{1}!}\frac{\widetilde{\sigma}_{s_{2}}(n,a-1)}{s_{2}!}\frac{\widetilde{\beta}_{k_{2}}(m)}{k_{2}!}\frac{(1-x)^{k}}{k!}$

Similarly, we have

${x^{-bm}\Psi_{b}(x^{m})\over\Psi_{n}(x)}={1\over
n}\sum_{k=0}^{\infty}\sum_{k_{1}+k_{2}=k}\sum_{s_{1}+s_{2}=k_{1}}k!(-1)^{k}\frac{\left(-bm\right)_{s_{1}}}{s_{1}!}\frac{\widetilde{\sigma}_{s_{2}}(m,b-1)}{s_{2}!}\frac{\widetilde{\beta}_{k_{2}}(n)}{k_{2}!}\frac{(1-x)^{k}}{k!}$

Now collect the coefficients of $\displaystyle{(1-x)^{k}\over k!}$ in the
equation (7.3), we get the desire result.

$\sum_{k_{1}+k_{2}=k}{\widetilde{\beta}_{k_{1}}(m)\over
k_{1}!}{\widetilde{\beta}_{k_{2}}(n)\over
k_{2}!}=n\sum_{k_{1}+k_{2}=k}\sum_{s_{1}+s_{2}=k_{1}}\frac{\left(-bm\right)_{s_{1}}}{s_{1}!}\frac{\widetilde{\sigma}_{s_{2}}(n,a-1)}{s_{2}!}\frac{\widetilde{\beta}_{k_{2}}(m)}{k_{2}!}\\\
-m\sum_{k_{1}+k_{2}=k}\sum_{s_{1}+s_{2}=k_{1}}\frac{\left(-bm\right)_{s_{1}}}{s_{1}!}\frac{\widetilde{\sigma}_{s_{2}}(m,b-1)}{s_{2}!}\frac{\widetilde{\beta}_{k_{2}}(n)}{k_{2}!}$

The other case $\alpha m-\beta n=1$ with $a<\beta$ can be proved similarly. ∎

## References

  * [1] Basin, S., Hoggatt, V. Jr., A primer on the Fibonacci sequence: Part II, Fib. Quart. 1, 61-68, (1963).
  * [2] Beck, M., and Robins, S., Computing the continuous discretely: Integer-point enumeration in polyhedra. Undergraduate Texts in Mathematics. Springer, New York, (2007).
  * [3] Beck, M., Sanyal, R.: Combinatorial Reciprocity Theorems.  American Mathematical Society, (2018).
  * [4] Bourgain, J., Glibichuk, A., Exponential sum estimates over a subgroup in an arbitrary finite field, Journal D’Analyse Mathematicque, 115, 51-70 (2011).
  * [5] Carlitz, L., Degenerate Stirling, Bernoulli and Eulerain Numerbs, Utilitas Math. 15 (1979), 51-88.
  * [6] Davis, J. P., Circulant Matrices, A Wiley-Interscience Publication, Jhon Wiley $\&$ Sons, Inc. 1979.
  * [7] A. J. Duran, A sequence of polynomials related to roots of unity, Problem E 3339, Solution by R. J. Chapman and R. W. K. Odoni, Amer. Math. Monthly 98 (1991), 269-271.
  * [8] Gessel, I., Generating functions and generalized Dedekind sums, Electron. J. Combin. 4 (1997), no. 2, Research Paper 11, 17 pp.
  * [9] Cenkci, M., Howard, F., Notes on degenerate Numbers, Discrete Mathematics 307(2007), 2359-2375.
  * [10] Kim, T., Kim, D., Jang, L., Lee, H., Kwon, J., Some results on degenerate Daehee and Bernoulli numbers and polynomials, Advances in Difference Equations, 311 (2020).
  * [11] Kim, T., Kim, D., Jang, L., Lee, H., Kim, H., Generalized degenerate Bernoulli numbers and polynomials arising from Gauss hypergeometric function, Advances in Difference Equations, 175, (2021).
  * [12] Mandel, A., Robins, S., Dragging the roots of a polynomial to the unit circle, arXiv:1908.03208[math.CO], 2019.
  * [13] Uday Kiran, N., An algebraic approach to $q$-partial fractions and Sylvester denumerants, arXiv:2104.10989v2[math.NT], 2021.
  * [14] Wyman, B., What is a reciprocity law?, The American Mathematical Monthly, 79(6), 571-586 (1972).
  * [15] Wilf, H., Generatingfunctionology, Academic Press, 1994.
  * [16] Young, P.: Degenerate Bernoulli polynomials, generalized factorial sums, and their applications.  Journal of Number Theory 128(4), 738–758 (2008).
  * [17] Zhang, Z., Yang, J., On sums of products of the degenerate Bernoulli numbers, 20(10), 751-755 (2009).
  * [18] Zeilberger, D., A one-line high school algebra proof of the unimodality of the Gaussian polynomials $\begin{pmatrix}n\\\ k\end{pmatrix}$ for $k<20$, q-series and partitions (Minneapolis, MN, 1988), Vol. 18. IMA VOl. Math. Appl. Springer, New York, 1989, pp. 67-72.


<EMAIL_ADDRESS>Ezra e. k. Cooper Theory of
computation Rewrite systems

# The Marriage of Effects and Rewrites

Ezra e. k. Cooper

###### Abstract

In the research on computational effects, defined algebraically, effect
symbols are often expected to obey certain equations. If we orient these
equations, we get a rewrite system, which may be an effective way of
transforming or optimizing the effects in a program. In order to do so, we
need to establish strong normalization, or termination, of the rewrite system.
Here we define a framework for carrying out such proofs, and extend the well-
known Recursive Path Ordering of Dershowitz to show termination of some effect
systems.

###### keywords:

term rewriting, strong normalization, termination, algebraic effects,
functional programming

##  1 Introduction

Plotkin and Power [15] introduced a view on computational effects as algebraic
terms. Their operational semantics shows how a source term containing effects
within it can reduce to a final effect term that represents a trace of the
effects performed by the program, or indeed a tree of all possible linear
traces. That line of work discusses equations between effect operators, which
define their essence in relation to one another.

We add to that work with an observation: by orienting the equations as a
system of _rewrite rules_ for the effect system, we can mechanically reduce an
effect term (as a _trace_) to something more compact, a _state_. The rewrite
rules in this case can be thought of as taking the place of the language
implementation or indeed the hardware which makes the effect “take effect.”
Alternatively, such rewrite rules can be an elegant way of defining and
implementing optimizations for effectful programs.

A general rewrite system is not the only way to work from an effectful term or
trace to a final state. Ahman and Staton [1] give a Normalization By
Evaluation strategy for doing just that. However, we find it interesting to
study the behavior of generalized rewrite systems. The freedom to apply
rewrite rules arbitrarily could be useful in a compiler implementation or
other program-transformation engine.

Having applied general term-rewriting to algebraic effects, the researcher
will want to know whether common properties apply, such as confluence and
strong normalization. While an ad-hoc proof may be given, it would be
preferable to factor the problem so that a proof about the termination of the
term-rewrite system alone would easily lift to a proof about the system in the
context of Moggi’s computational metalanguage [13].

Now, in the literature of term-rewriting there are many techniques for showing
strong normalization, for example the “recursive path ordering” or RPO [5].
With this technique, the practitioner merely exhibits an ordering on the
function-symbols and shows that each rewrite rule obeys this ordering in a
certain way. Thus an intricate inductive proof is replaced by some relatively
simple (albeit recursive) checks on the rewrite rules. The RPO is extended to
a calculus with $\lambda$-abstraction and with $\beta$-reduction in the
literature on the “higher-order recursive path ordering,” HORPO [9]. But that
leaves us to wonder, what about a calculus with the let-construct? If we can
extend RPO or HORPO to the computational metalanguage, then we will have an
easy way of proving termination of some systems of effects.

In this paper, we make the following contributions:

  * •

We show how to interpret a variety of computational effects operationally as
rewrite-rules, rather than equations, giving a more operational flavor to the
workings of effect symbols,

  * •

We show a new technique for proving strong normalization for rewriting
algebraic-effect systems by lifting the recursive path ordering into Moggi’s
metalanguage.

  * •

We use the technique to prove termination of an effect system for global
state, which shows how to reduce its _traces_ to _states_.

Our central proof will not be surprising to anyone familiar with RPO, with the
Tait-Girard proof of strong normalization [7] and the Lindley-Stark method for
extending Tait-Girard to the computational metalanguage [11]. But by combining
all these things, we get a compelling result that can be used directly to show
termination of languages in the presence of algebraic effects, where the
effects themselves are subject to rewrite rules.

##  2 Algebraic effects

Let’s review the basic framework of algebraic effects, introduced by Plotkin
and Power [15] (and Bauer [2]) as extended in Plotkin and Pretnar [17] with
the $\mathop{\mathsf{let}}$-construct. A programming language is defined with
effect symbols representing individual atomic effects that can be performed.
The symbols build on two kinds of syntactic roles, parameters $p$ and
arguments $a$, as $e_{\vec{p}}(\vec{a})$. The parameters represent data that
is used by the effect, such as a message to print to the terminal, while the
arguments represent possible continuation terms, depending on the _result_ of
the effect. An effect $readbit$ which reads a single bit from some input
source would naturally have two argument positions, representing the behavior
the program will follow if it reads a 0 or a 1, respectively:
$readbit(zeroContinuation,oneContinuation)$.

Another effect, $print_{m}$ could be used to print a corresponding message:

$readbit(print_{\mathtt{cold}}(30),\,print_{\mathtt{hot}}(70))$

will print cold or hot correspondingly, then return a number, say 30 or 70 for
a number of degrees celsius. Any pure (effect-free) term placed as an effect
argument represents an ultimate return _value_ of the computation, dependent
upon the path taken from root to leaf.

The Plotkin and Power semantics lets the effect symbols commute out of
evaluation contexts, essentially floating to the top of the term at evaluation
time, so that the normal forms are trees of effect symbols, representing
possible traces, whose leaves are the corresponding return values. Thus we
could apply the lambda-term $\lambda x.x+5$ to the above effectful term and it
would rewrite as follows:

$\displaystyle(\lambda
x.x+5)readbit(print_{\mathtt{cold}}(30),print_{\mathtt{hot}}(70))$
$\displaystyle\leadsto$ $\displaystyle readbit((\lambda
x.x+5)print_{\mathtt{cold}}(30),(\lambda x.x+5)print_{\mathtt{hot}}(70))\hskip
50.00008pt$ (eff-assoc) $\displaystyle\leadsto$ $\displaystyle
readbit(print_{\mathtt{cold}}((\lambda
x.x+5)\>30),print_{\mathtt{hot}}((\lambda x.x+5)\>70))\hskip 50.00008pt$ (eff-
assoc) $\displaystyle\leadsto$ $\displaystyle
readbit(print_{\mathtt{cold}}(30+5),print_{\mathtt{hot}}(70+5)\hskip
50.00008pt$ (abs-$\beta$) $\displaystyle\leadsto$ $\displaystyle
readbit(print_{\mathtt{cold}}(35),print_{\mathtt{hot}}(75)$ (abs-$\beta$)

The final row is a normal form, which shows a tree where the $readbit$
operation can choose either of two paths; on each path some specific message
is printed; and finally each path terminates in a value, which was computed by
applying the $\lambda$-abstraction to the _result_ of the original side-
effecting expression.

In the present work, we explore what happens when these computation (effect)
trees are further exposed to their own rewrite rules, which can be applied in
source terms or in these final computation trees. Such reduction loses the
“trace” nature of the tree, but gives us a way of simulating the machinery of
the effects, something like an abstract machine for effects.

We do not make use of the effect parameters in our proofs, so we do not write
them.

###  2.1 Examples

When we are talking about the semantics of a programming language, the rewrite
rules for the effects can be seen as implementing the machinery of the
language implementation which reduces the individual effects to a state,
itself represented as a normal form of an effect-term.

#### Example: Global State

Global state is modeled as a single global location which can hold a value of
some type $T$. The signature of the global-state effect system is

$\displaystyle arity(assign_{i})=1$ $\displaystyle arity(get)=T$

Note $assign_{i}$ is parameterized by the value $i$, to assign into the global
variable. Plotkin and Power distinguish “parameters” and “arguments”. The
arguments of $get$ are indexed by the values of the storage type $T$: its
“arity” is $T$.

If the symbols are uninterpreted (subject to no rewrites) then the result of a
rewrite sequence is just a computation tree, which acts as a tree of all
possible traces of the program. But we may alternatively assign a meaning
which is the actual final state of this computation, in cases where there is
one. To that end, we can assign rewrite rules (adapted from Plotkin and Power
[16]) that perform the trace-reduction:

$\displaystyle assign_{i}(get(t_{1},\,\dots,\,t_{n}))$ $\displaystyle\leadsto
assign_{i}(t_{i})$ $\displaystyle assign_{i}(assign_{j}(s))$
$\displaystyle\leadsto assign_{j}(s)$ $\displaystyle
get(t_{1},\,\dots,\,t_{i},\,\dots,\,t_{n})$ $\displaystyle\leadsto
get(t_{1},\,\dots,\,s_{i},\,\dots,\,t_{n})$ where
$t_{i}=get(s_{1},\,\dots,\,s_{n})$

The normal forms of this system have no adjacent $\mathit{get}$-$\mathit{get}$
pairs, no adjacent $\mathit{assign}$-$\mathit{assign}$ pairs, and no
$\mathit{get}$ inside an $\mathit{assign}$, so they are really just a single
$\mathit{assign}$, or a single $\mathit{get}$, with argument as the final
value result of the program. The single $\mathit{assign}$ indicates to us what
the final state of the global variable was, by its _parameter_. A single
$\mathit{get}$ would represent a read of an uninitialized variable, or a
nondeterministic one; in a particular setting this might be disallowed by
other mechanisms which don’t interest us here.

Contrast this rewriting approach with the examples given in Johann, et al. [8]
where global-state computation-trees are mapped to their final state by a
function defined outside the calculus.

#### Example: Nondeterminism

There is one effect, $or$, with $arity(or)=2$, and one rewrite rule:

$or(or(s_{1},s_{2}),s_{3})\leadsto or(s_{1},or(s_{2},s_{3}))$

The rule has the purpose of normalizing a branching tree of possible
computations to a flat list of possible outcomes, and so works more like a
list.

#### Example: a looping effect

This effect has not been proposed in the literature to our knowledge, but to
motivate our work, we explore the idea of something that looks like an
“effect” but has some complex rewriting behavior.

In the practice of programming with external services (for example, database
servers, or web-based APIs), one frequently wants to make one’s own service
robust in the face of a brief interruption to the external service. To that
end, the programmer builds a finite number of retries into their system. If
the external service begins functioning during the retries, the program will
continue normally, but if the finite retries are exhausted, an error is
returned to the user.

We model such a system using a pair of effects, request and retry. Each time
the program makes a _request_ to the service, that request may fail (a
possibility whose continuation is represented by a first parameter, $t$), or
it may return a meaningful value (represented by an indexed set of parameters,
$s_{1},\,\dots,\,s_{n}$). So we introduce an effect
$request(t,\,s_{1},\,\dots,\,s_{n})$. We also introduce an effect
$retry(u,\,r)$ which represents the effect of retrying the computation $r$ a
number of times indicated by $u$. In $u$ we will find a number represented
through rewrite symbols $zero()$ and $succ(u)$, i.e. Peano numerals (we use
Peano numerals to make the arithmetic amenable to rewriting).

$\displaystyle retry(zero(),request(t,s_{1},\,\dots,\,s_{n}))$
$\displaystyle\leadsto$ $\displaystyle t$ $\displaystyle
retry(succ(u),request(t,s_{1},\,\dots,\,s_{n}))$ $\displaystyle\leadsto$
$\displaystyle request(retry(u,t^{\prime}),s_{1},\,\dots,\,s_{n})$

This effect-rewrite system produces something more like a trace than a final
state, since it replicates the $request$ effect $u$ times in the computation
tree. To evaluate the trace, we could choose further rewrite rules that make
$request$ act like $get$ in the global-state example, flattening successive
$request$s and choosing a single outcome for the whole set.

This may be a contrived model for a retry-loop of effects, but it demonstrates
our technique on a slightly more complex system than the other examples.

#### Example: Parallelism

A binary effect, $\mathit{par}$, represents parallel evaluation of two streams
of effects. We assume it is used in combination with other effects. The
following rewrite rules are replicated for each other effect $e$ in the
system:

$\displaystyle par(e(s_{1},\,\dots,\,s_{n}),t)\leadsto
e(par(s_{1},t),\,\dots,\,par(s_{n},t))$ $\displaystyle
par(s,e(t_{1},\,\dots,\,t_{n}))\leadsto
e(par(s,t_{1}),\,\dots,\,par(s,t_{n}))$

These rules are not in general confluent, so several different final states
can be derived from a single source term. That is of course in the nature of
parallelism.

In the tradition of fork-join parallelism, we could also add an effect
$\mathit{join}$ which brings together the two results in one result term, for
further computation. Here $\langle\cdot,\cdot\rangle$ represents ordinary data
pairing into a product type ($S\times T$):

$join(par(v,w))\leadsto\mathit{pure}(\langle v,w\rangle)$

##  3 Two kinds of effectful metalanguage

We must pause to reconcile two syntactic treatments of effects in the
literature. One marks the monad type explicitly, the other leaves it implicit.
Both treatments appear in Moggi’s early work and in the literature are often
referred to as $\lambda_{ml}$ and $\lambda_{c}$.

The first approach ($\lambda_{ml}$) uses a computation type while the other
($\lambda_{c}$) treats effect operations as transparent to the type system.
The latter notation predominates in Plotkin and Power [15] and other
algebraic-effects research. Sabry and Wadler [19] establish a close
correspondence between them.

The key typing rule for each is given below. We write $\mathsf{E}(T)$ for the
type of an effectful computation giving result type $T$. (A single such effect
constructor implies one global monad for effects throughout the system.)

Explicit computation types ($\lambda_{ml}$)

Γ⊢t : E(S)
Γ, x : S ⊢u : E(T) Γ⊢letx ⇐t inu : E(T)

Effects as type-transparent ($\lambda_{c}$)

Γ⊢t : S
Γ, x : S ⊢u : T Γ⊢letx ⇐s inu : T

In $\lambda_{ml}$, we perform beta-reduction on lets with explicitly-
constructed pure subjects:

$\mathop{\mathsf{let}}x\mathop{\Leftarrow}pure(t)\mathop{\mathsf{in}}u\leadsto
u\\{t/x\\}$

In $\lambda_{c}$, beta-reduction is triggered by the syntactic class of a
value in the subject position (assume $v$ describes a syntactic class of
values):

$\mathop{\mathsf{let}}x\mathop{\Leftarrow}v\mathop{\mathsf{in}}u\leadsto
u\\{v/x\\}$

Values $v$ in $\lambda_{c}$ are defined by a grammar, which prohibits
$\mathsf{let}$ and effect application, at least when not embedded in a
$\lambda$-body.

The main proofs in this paper use $\lambda_{ml}$ as the substrate.

##  4 A Metalanguage With Explicit Effects

Now we define our core object: a metalanguage for computational effects, based
on the basic syntax of Moggi [13] with the algebraic-effect rules of Plotkin
and Pretnar [17]. As a blend of those languages, it includes explicit effect
symbols and a let-construct.

Unlike some later work on algebraic effects, we don’t use the _fine-grain
call-by-value_ of Levy, et al. [10], and in fact do not assume a call-by-value
evaluation order, because we want to cast as wide a net as possible for the
interesting rewrite systems that can be proven strongly-normalizing with our
technique. In fact, one of our motivating examples (NRC) benefits from
allowing rewrites in arbitrary position and from allowing arbitrary term-term
applications (in distinction to FGCBV).

Here is the grammar of our metalanguage:

$\displaystyle s,t,u$ $\displaystyle::=$ $\displaystyle x\mid\lambda
x.u\mid\mathit{pure}(t)\mid
st\mid\gamma(t_{1},...,t_{n})\mid\mathop{\mathsf{let}}x\mathop{\Leftarrow}t\mathop{\mathsf{in}}u$
$\displaystyle\gamma$ $\displaystyle::=$ $\displaystyle e\mid f$ (rewritable
symbols)  $\displaystyle e,e^{\prime},e^{\prime\prime}$ (effect symbols)
$\displaystyle f,g$ (function symbols)

We distinguish two classes of rewritable symbols: the effect symbols and
function symbols. These two classes have their own typing rules, but are often
treated the same in the rewrite theory, so we use $\gamma$ to range over both,
$e$ (and its primes) to range over effect symbols, and $f,g,...$ to range over
non-effect function symbols. Both subclasses are subject to some metalanguage
rewrites as motivated by the Plotkin-Power framework.

Types are defined by this grammar:

$\displaystyle S,\,T$ $\displaystyle::=$ $\displaystyle B\mid\mathsf{E}(T)\mid
S\to T$ $\displaystyle B$ (basic types)

The language has a special type constructor for effect types: $\mathsf{E}(T)$
is the type of computations that may be effectful, returning a value of type
$T$. The type of functional abstractions is $S\to T$.

Typing rules are given in Figure 1. To give types to the rewritable symbols,
we assume a signature $\Sigma$ which maps each effect symbol to an arity and
each function symbol to a type signature of the form $S_{1}\times\cdots\times
S_{n}\to T$. Throughout the paper we will use series of terms like
$s_{1},\,\dots,\,s_{n}$ or a vector notation $\vec{s}$ interchangeably. There
may be a distinct term called $s$ in such a context.

Figure 1: Typing rules

Γ, x : S ⊢u : T Γ⊢λx. u : S →T Γ⊢s : S →T
Γ⊢t : S Γ⊢st : T Γ⊢t : E(S)
Γ, x : S ⊢u : E(T) Γ⊢letx ⇐t inu : E(T) Γ⊢t : T Γ⊢pure(t) : E(T) for each
$t_{i}$,  Γ⊢t_i : E(T)
Σ(e) = n Γ⊢e(t_1, …, t_n) : E(T) for each $s_{i}$,  Γ⊢s_i : S_i
Σ(f) = S_1 ×⋯×S_n →T Γ⊢f(s_1, …, s_n) : T

Figure 2: Rewrite rules of the metalanguage. $\displaystyle(\lambda x.u)t$
$\displaystyle\leadsto_{ml}$ $\displaystyle t\\{u/x\\}$ (abs-$\beta$)
$\displaystyle\mathop{\mathsf{let}}x\mathop{\Leftarrow}\mathit{pure}(t)\mathop{\mathsf{in}}u$
$\displaystyle\leadsto_{ml}$ $\displaystyle t\\{u/x\\}$ (let-$\beta$)
$\displaystyle\mathop{\mathsf{let}}y=(\mathop{\mathsf{let}}x\mathop{\Leftarrow}t_{1}\mathop{\mathsf{in}}t_{2})\mathop{\mathsf{in}}u$
$\displaystyle\leadsto_{ml}$
$\displaystyle\mathop{\mathsf{let}}x\mathop{\Leftarrow}t_{1}\mathop{\mathsf{in}}\mathop{\mathsf{let}}y\mathop{\Leftarrow}t_{2}\mathop{\mathsf{in}}u\hskip
20.00003pt$ when $x\not\in FV(u)$
$\displaystyle\mathop{\mathsf{let}}x\mathop{\Leftarrow}e(t_{1},\,...,\,t_{n})\mathop{\mathsf{in}}u$
$\displaystyle\leadsto_{ml}$ $\displaystyle
e(t_{1}^{\prime},\,...,\,t_{n}^{\prime})$ (eff-assoc)  where
$t_{i}^{\prime}=\mathop{\mathsf{let}}x\mathop{\Leftarrow}t_{i}\mathop{\mathsf{in}}u$

Rewrite rules for the metalanguage are given in Figure 2. The eff-assoc rule
is adapted from a similar equation in Plotkin and Pretnar [17]. Significantly,
eff-assoc does _not_ apply to function symbols, only effect symbols. We omit
eta-reduction, which is found in Moggi [13] and in much of the other work, but
it doesn’t serve our proof or our examples.

Having prepared the metalanguage as a broth, the soup will be made by adding
further rewrite rules, all algebraic in nature, and specific to a domain area,
as shown in the Examples. So, assume we are given an underlying rewrite
system, defined by a signature $\Sigma$ of rewritable symbols with arities and
their rewrite rules $l\leadsto r$. We require that $l$ and $r$ are symbolic
terms, rather than arbitrary terms:

$l,r::=x\mid\gamma(l_{1},\,l_{2},\,...,\,l_{n})$

Thus, the _symbolic_ rewrite system is ignorant of the let-construct, of
lambda abstractions, and of applications.

#### Rewriting contexts

For this work, we assume that all the rewrite relations (including those
marked $\leadsto$, $\leadsto_{ml}$, $\succ$ and $\mathrel{\dot{\succ}}$) are
compatibly-closed, so they can be applied in any term context. This is a
fairly standard assumption for rewrite systems.

In some application areas, one may wish to constrain the eligible rewrite
contexts, for example to a call-by-value evaluation order. Doing so is normal
in the study of computational effects. But by allowing rewrites anywhere, our
result remains more general.

##  5 The Recursive Path Ordering Defined

Now we define the recursive path ordering $\succ$, which relates terms of the
symbolic part of the language, and which is the key tool of the normalization
proof.

The RPO is defined with respect to an ordering $>_{\Sigma}$ on rewritable
symbols. We will write $>$ for the symbol ordering when it is clear from
context. The relation $\succ$ is extended to a lexicographical ordering on a
sequence of terms by writing $\succ_{lex}$. (The (HO)RPO usually allows
symbols whose args are ordered either by a multiset ordering or a
lexicographical ordering. Presently we only defines the lexicographical one.)
We use $\succeq$ for the union of $\succ$ with $=$.

######  Definition 5.1 (RPO).

Define $s\succ t$ to hold when one of the following does:

  1. 1.

$s=\gamma(s_{1},\,\dots,\,s_{n})$, $t=\gamma(t_{1},\,\dots,\,t_{n})$ and
$\vec{s}\succ_{lex}\vec{t}$ and for all $j$, $s\succ t_{j}.$

  2. 2.

$s=\gamma(s_{1},\,\dots,\,s_{m})$, $t=\gamma^{\prime}(t_{1},\,\dots,\,t_{n})$
and $\gamma>\gamma^{\prime}$ and for all $j$, $s\succ t_{j}.$

  3. 3.

$s=\gamma(s_{1},\,\dots,\,s_{m})$ and for some $i$, $s_{i}\succeq t.$

It is easy to miss that this relation is inductively defined, and there is a
base case hidden in case (3), in the $=$ part of the $\succeq$ relation. All
derivations of the RPO end in leaves which are assertions of the right-hand
term being equal to an immediate subterm of the left-hand term.

Let’s take a moment to understand the purpose of this step intuitively, and
where it fits in the larger proof. The $\succ$ relation essentially captures a
large class of terminating rewrite systems that could be defined for a given
effect-signature $\Sigma$ and an ordering among the symbols. The ordering will
be specific to the particular rewrite system, but the $\succ$ relation
abstracts slightly from the rewrite rules themselves. It is usually a superset
of the relation $(\leadsto)$ of interest, so $(\leadsto)\subseteq(\succ)$. The
user must also check their rewrite rules ($\leadsto$) do in fact meet the
above criteria (qualifying as a $(\succ)$ relation), but this is often easy to
do, and one then gets a big termination proof “for free,” as it were.

The $\succ$ relation abstracts only the symbol-rewriting rules; to extend it
through the metalanguage, we define

$(\mathrel{\dot{\succ}})\triangleq(\succ)\cup(\leadsto_{ml}).$

And this $\mathrel{\dot{\succ}}$ is the relation for which we will prove
strong normalization. As a result, the target calculus where
$(\leadsto)\cup(\leadsto_{ml})$ is the relation of interest must also be
strongly normalizing.

We can also present the RPO in terms of two powerful inference rules: [rpo-
subterm]s_i ⪰t  for some $s_{i}$ γ(s_1, …, s_n) ≻t [rpo-symbol](γ, →s) >_RPO
(γ’, →t)
s ≻t_i  for each $t_{i}$ γ(s_1, …, s_n) ≻γ’(t_1, …, t_m) Where the $>_{RPO}$
ordering is defined as a lexicographical ordering with the components
$>_{\Sigma}$ and $\succ_{lex}$.

In what follows, a _reduct_ of $t$ is a term $t^{\prime}$ for which
$t\mathrel{\dot{\succ}}t^{\prime}$, and we write $SN(t)$ if $t$ strongly
normalizes under the relation $\mathrel{\dot{\succ}}$. When a term is strongly
normalizing, we can perform induction on its reduction tree (we only use this
for the reduction tree under ($\mathrel{\dot{\succ}}$), not the other term
relations); to invoke this principle we will write “induction on $t$, ordered
by $\mathrel{\dot{\succ}}$.” When we have several normalizing terms handy, we
might use simultaneous induction on all of them, where the proposition is
assumed to hold for the group where any one is reduced.

###  5.1 Continuations

A key difficulty in the proof is showing strong normalization in the presence
of the let-assoc rule, which reorganizes the term in a progress-making way,
but does not make it smaller. Thus we need a construct to allow tracking and
inducting on that progress. In the let-assoc rule,
$\mathop{\mathsf{let}}x\mathop{\Leftarrow}(\mathop{\mathsf{let}}y\mathop{\Leftarrow}s_{1}\mathop{\mathsf{in}}s_{2})\mathop{\mathsf{in}}s_{3}$
has a let on its inner left-hand side, and we want to see that go away. The
reduct of this form,
$\mathop{\mathsf{let}}y\mathop{\Leftarrow}s_{1}\mathop{\mathsf{in}}\mathop{\mathsf{let}}x\mathop{\Leftarrow}s_{2}\mathop{\mathsf{in}}s_{3}$,
has the let form on its inner right-hand-side, which is closer to a normal
form. We have decreased the number of let-forms that are in the left-hand-
sides of other let-forms. Therefore, following Lindley and Stark [11], we
define continuations, which are a stack of the “wrong kind” of let context—the
$\mathop{\mathsf{let}}x\mathop{\Leftarrow}{[\hskip
5.0pt]}\mathop{\mathsf{in}}s_{3}$ of the foregoing explanation. A let-assoc
rewrite will reduce the size of this stack, so in inductive proofs we have a
way to prove progress is being made.

Define continuations $K$ as follows:

$\displaystyle K$ $\displaystyle::=$ $\displaystyle\epsilon\mid K\circ F$
$\displaystyle F$ $\displaystyle::=$
$\displaystyle\mathop{\mathsf{let}}x\mathop{\Leftarrow}{[\hskip
5.0pt]}\mathop{\mathsf{in}}u$

Write $F[t]$ for the term that results from filling the hole in $F$ with $t$.
Write $K@t$ for that which results from filling the holes recursively, so
$\epsilon@t=t$ and $K\circ F@t=K@F[t]$. Write $|K|$ for the number of frames
in $K$, so $|\epsilon|=0$, $|K\circ F|=1+|K|$.

Write $K\mathrel{\dot{\succ}}K^{\prime}$ if
$K@x\mathrel{\dot{\succ}}K^{\prime}@x$ for some fresh $x$. Note that for an
individual frame, the only rewrites are of the form
$\mathop{\mathsf{let}}x\mathop{\Leftarrow}{[\hskip
5.0pt]}\mathop{\mathsf{in}}u\mathrel{\dot{\succ}}\mathop{\mathsf{let}}x\mathop{\Leftarrow}{[\hskip
5.0pt]}\mathop{\mathsf{in}}u^{\prime}$ with
$u\mathrel{\dot{\succ}}u^{\prime}$.

##  6 Strong Normalization

Following Lindley-Stark, define a type-indexed reducibility predicate as
follows:

$\displaystyle\mathsf{Red}_{B}(t)$ $\displaystyle\triangleq$ $\displaystyle
SN(t)$ $\displaystyle\mathsf{Red}_{S\to T}(s)$ $\displaystyle\triangleq$
$\displaystyle\mathsf{Red}_{T}(st)\hbox{ for all $t$ where
$\mathsf{Red}_{S}(t)$}$ $\displaystyle\mathsf{Red}_{\mathsf{E}(T)}(t)$
$\displaystyle\triangleq$ $\displaystyle SN(K@t)\hbox{ for all $K$ where
$\mathsf{Red}_{T}^{\top}(K)$}$ $\displaystyle\mathsf{Red}_{T}^{\top}(K)$
$\displaystyle\triangleq$ $\displaystyle SN(K@\mathit{pure}(t))\hbox{ for all
$t$ where $\mathsf{Red}_{T}(t)$}$

We will write, equivalently, $t\in\mathsf{Red}_{T}$ or $\mathsf{Red}_{T}(t)$
as is convenient for the prose.

Define the set of _neutral_ terms to be these:

  * •

An application, $st$.

  * •

A variable, $x$.

We have four standard properties of $\mathsf{Red}_{-}$ with standard proofs.

######  Lemma 6.1.

For any $T$, $\mathsf{Red}_{T}$ is inhabited by some term.

######  Proof 6.2.

By induction on $T$.

  * •

case $B$. A term which is a free variable satisfies this.

  * •

case $S\to T^{\prime}$. By IH we have a term $t\in\mathsf{Red}_{T^{\prime}}$
and so $\lambda x.t\in\mathsf{Red}_{S\to T^{\prime}}$.

  * •

case $\mathsf{E}(T^{\prime})$. By IH we have a term
$t\in\mathsf{Red}_{T^{\prime}}$ and so
$pure(t)\in\mathsf{Red}_{\mathsf{E}(T^{\prime})}$.

######  Lemma 6.3.

For any $T$, $t$, if $t\in\mathsf{Red}_{T}$ then $t$ strongly normalizes.

######  Proof 6.4.

By induction on $T$ and appeal to the $\mathsf{Red}_{T}$ definition. In the
$\mathsf{E}(T^{\prime})$ case, $t$ is a subterm of something directly asserted
to be SN. In the $T_{1}\to T_{2}$ case, the IH gives strong normalization of a
term which has $t$ as a subterm. We need that $\mathsf{Red}_{S}$ is inhabited,
which Lemma 6.1 shows.

######  Lemma 6.5.

For any $s\in\mathsf{Red}_{T}$ with $s\mathrel{\dot{\succ}}s^{\prime}$, we
have $s^{\prime}\in\mathsf{Red}_{T}$.

######  Proof 6.6.

By induction on $T$.

  * •

case $B$. $s^{\prime}$ merely needs to be SN, and it is by virtue of being a
reduct of $s$.

  * •

case $T_{1}\to T_{2}$. To show that $s^{\prime}t\in\mathsf{Red}_{T_{2}}$ for
any $t\in\mathsf{Red}_{S_{1}}$. We have that $st\in\mathsf{Red}_{T_{2}}$. But
$st\mathrel{\dot{\succ}}s^{\prime}t$ so the conclusion follows from the IH.

  * •

case $\mathsf{E}(T^{\prime})$. To show that $K@s^{\prime}\in SN$ for
$K\in\mathsf{Red}_{T}^{\top}$. Again, $K@s$ reduces to $K@s^{\prime}$ and
since the former is SN, the latter is too.

######  Lemma 6.7.

Given a neutral $s$, if each of its reducts is in $\mathsf{Red}_{T}$ then $s$
is in $\mathsf{Red}_{T}$.

######  Proof 6.8.

By induction on the structure of $T$.

  * •

case $B$ Since the reducts are in $\mathsf{Red}_{B}$, they are in SN, and this
satisfies the definition of $\mathsf{Red}_{B}$.

  * •

case $S\to T^{\prime}$ To show that $st\in\mathsf{Red}_{T^{\prime}}$ for each
$t\in\mathsf{Red}_{S}$. We have that $t$ is SN; proceed by induction on the
reduction tree of $t$. Examine reductions of $st$. Since $s$ is neutral, it is
not a $\lambda$-abstraction, so there is no $\beta$-reduction at the head. The
only reducts are $s^{\prime}t$ (where $s\mathrel{\dot{\succ}}s^{\prime}$) and
$st^{\prime}$ (where $t\mathrel{\dot{\succ}}t^{\prime}$). In the first case,
the lemma hypothesis is sufficient. In the second case, the inner IH is
sufficient.

  * •

case $\mathsf{E}(T^{\prime})$ Given $K\in\mathsf{Red}_{T^{\prime}}^{\top}$, we
want to show $SN(K@s)$. By induction on $K$. Since $s$ is neutral, the only
reducts are $K^{\prime}@s$ (where $K\mathrel{\dot{\succ}}K^{\prime}$) and
$K@s^{\prime}$ (where $s\mathrel{\dot{\succ}}s^{\prime}$). (Note there is no
metalanguage rule rewriting the frame $F$ into the application $st$ in $F[st]$
and one cannot be supplied by the symbol-rewrites.) In the first case, the
inner IH is sufficient. In the second case, the lemma hypothesis is
sufficient.

######  Lemma 6.9.

If $SN(u\\{t/x\\})$ then $SN(u)$.

######  Proof 6.10.

Constructively, every reduction in the reduction tree of $u$ has an analogue
in that of $u\\{t/x\\}$. As a consequence, the tree for $u$ can be no larger
than that of the other term, and cannot be divergent when the latter is
convergent.

Now we show that each term-former can construct a reducible term, given
appropriate conditions.

######  Lemma 6.11.

If $\mathsf{Red}_{S\to T}(s)$ and $\mathsf{Red}_{S}(t)$ then
$\mathsf{Red}_{T}(st)$.

######  Proof 6.12.

Immediate from the definition of $\mathsf{Red}_{S\to T}$.

######  Lemma 6.13.

If $\mathsf{Red}_{T}(u\\{t/x\\})$ for every $t$ in $\mathsf{Red}_{S}$ then
$\mathsf{Red}_{S\to T}(\lambda x.u)$.

######  Proof 6.14.

Since $(\lambda x.u)t$ is neutral, it is sufficient to show that all its
reducts are reducible. We have that $t$ is SN by virtue of being in
$\mathsf{Red}_{S}$. We have that $u$ is SN by Lemma 6.9, and therefore we can
apply simultaneous induction on the two rewrite trees. The inductive
hypotheses are that $(\lambda x.u^{\prime})t$ is reducible, for any
$u\mathrel{\dot{\succ}}u^{\prime}$, and that $(\lambda x.u)t^{\prime}$ is
reducible, for any $t\mathrel{\dot{\succ}}t^{\prime}$. Now we take those cases
on the reducts of $(\lambda x.u)t$.

  * •

case $(\lambda x.u)t\mathrel{\dot{\succ}}(\lambda x.u^{\prime})t$ for
$u\mathrel{\dot{\succ}}u^{\prime}$; this is reducible by IH.

  * •

case $(\lambda x.u)t\mathrel{\dot{\succ}}(\lambda x.u)t^{\prime}$ for
$t\mathrel{\dot{\succ}}t^{\prime}$; this is reducible by IH.

  * •

case $(\lambda x.u)t\mathrel{\dot{\succ}}u\\{t/x\\}$; this is reducible by
lemma hypothesis.

######  Lemma 6.15.

If $K\mathrel{\dot{\succ}}K^{\prime}$ then $|K|\geq|K^{\prime}|$.

######  Proof 6.16.

By structural induction on K. If $K=\epsilon$, there is no reduction. If
$K=K_{0}\circ F$, we have reductions
$K_{0}\mathrel{\dot{\succ}}K_{0}^{\prime}$ and
$F\mathrel{\dot{\succ}}F^{\prime}$, which conserve length (the former by IH).

Via (let-assoc), we also have $K=K_{0}\circ
F_{1}\circ(\mathop{\mathsf{let}}x\mathop{\Leftarrow}{[\hskip
5.0pt]}\mathop{\mathsf{in}}u)\circ K_{1}$ and
$K^{\prime}=K_{0}\circ(\mathop{\mathsf{let}}x\mathop{\Leftarrow}{[\hskip
5.0pt]}\mathop{\mathsf{in}}F_{1}[u])\circ K_{1}$. And this is one frame
shorter.

######  Lemma 6.17.

If $t\in\mathsf{Red}_{T}$ then
$\mathit{pure}(t)\in\mathsf{Red}_{\mathsf{E}(T)}$.

######  Proof 6.18.

To show: that $K@\mathit{pure}(t)\in\mathsf{Red}_{\mathsf{E}(T)}$ for any
$K\in\mathsf{Red}_{T}^{\top}$. But this is immediate from the definition of
$\mathsf{Red}_{T}^{\top}$.

######  Lemma 6.19.

If $s\in SN$ and $K@(u\\{s/x\\})\in SN$, then
$K@(\mathop{\mathsf{let}}x\mathop{\Leftarrow}pure(s)\mathop{\mathsf{in}}u)\in
SN$.

######  Proof 6.20.

By induction on $(|K|,\,(s,\,u,\,K))$ ordered by
$(>,\,(\mathrel{\dot{\succ}}_{lex}))$. Proceed by showing all reducts of
$K@\mathop{\mathsf{let}}x\mathop{\Leftarrow}pure(s)\mathop{\mathsf{in}}u$ are
in $SN$.

  * •

case
$K^{\prime}@\mathop{\mathsf{let}}x\mathop{\Leftarrow}pure(s)\mathop{\mathsf{in}}F[u]$
where $K^{\prime}\circ F=K$, by let-assoc. To apply the IH, we need to show
that $K$ and $F[u]$ meet the lemma premises, that
$K^{\prime}@(F[u]\\{s/x\\})\in SN$. Note $K^{\prime}@F[u]=K@u$ and $x$ cannot
be free in $F$, by the let-assoc side condition, therefore
$K^{\prime}@(F[u]\\{s/x\\})=K^{\prime}@(F[u\\{s/x\\}]])$.) Furthermore
$|K^{\prime}|<|K|$, so the metric decreases.

  * •

case The reduct is $K@u\\{s/x\\}$. By hypothesis.

  * •

case The reduct is
$K@\mathop{\mathsf{let}}x\mathop{\Leftarrow}pure(s^{\prime})\mathop{\mathsf{in}}u$
where $s\mathrel{\dot{\succ}}s^{\prime}$. By IH.

  * •

case The reduct is
$K@\mathop{\mathsf{let}}x\mathop{\Leftarrow}pure(s)\mathop{\mathsf{in}}u^{\prime}$
where $u\mathrel{\dot{\succ}}u^{\prime}$. By IH.

  * •

case The reduct is
$K^{\prime}@\mathop{\mathsf{let}}x\mathop{\Leftarrow}pure(s)\mathop{\mathsf{in}}u$
where $K\mathrel{\dot{\succ}}K^{\prime}$. By IH.

######  Lemma 6.21.

If $s\in\mathsf{Red}_{\mathsf{E}(S)}$ and $u$ is such that for all
$s^{\prime}\in\mathsf{Red}_{S}$ we have
$u\\{s^{\prime}/x\\}\in\mathsf{Red}_{\mathsf{E}(T)}$, then
$\mathop{\mathsf{let}}x\mathop{\Leftarrow}s\mathop{\mathsf{in}}u\in\mathsf{Red}_{\mathsf{E}(T)}$.

######  Proof 6.22.

We show that
$SN(K@\mathop{\mathsf{let}}x\mathop{\Leftarrow}s\mathop{\mathsf{in}}u)$ for
any $K\in\mathsf{Red}_{T}^{\top}$. First, we show
$K^{\prime}=K\circ(\mathop{\mathsf{let}}x\mathop{\Leftarrow}{[\hskip
5.0pt]}\mathop{\mathsf{in}}u)\in\mathsf{Red}_{S}^{\top}$, which in other words
says that
$SN(K@\mathop{\mathsf{let}}x\mathop{\Leftarrow}pure(s^{\prime\prime})\mathop{\mathsf{in}}u)$
for any $s^{\prime\prime}\in\mathsf{Red}_{S}$. This we get from Lemma 6.19 (by
hypothesis, $u\\{s^{\prime\prime}/x\\}\in\mathsf{Red}_{T}$ and further
$K^{\prime}@(u\\{s^{\prime\prime}/x\\})\in SN$ as required by Lemma 6.19). Now
it follows by the definition of $s\in\mathsf{Red}_{S}$ that
$K^{\prime}@s=K@\mathop{\mathsf{let}}x\mathop{\Leftarrow}s\mathop{\mathsf{in}}u\in
SN$.

The next lemma shows a property of the undotted $\succ$, that is, the raw RPO
relation, which will be used as a subroutine in some inductive proofs to
follow. Since this is an extraction of an inductive step, it is stated in
terms of a “lemma hypothesis” which will align with some outer induction
hypothesis in the cases where it is used.

To make the lemma appropriately general, we define _contexts_ to encompass the
various kinds of settings in which terms can be placed to prove reducibility:

$\displaystyle C$ $\displaystyle::=$ $\displaystyle K\bigm{|}{[\hskip
5.0pt]}t\bigm{|}{[\hskip 5.0pt]}$

And write $C[s]$ to denote filling the context with a term:

$\displaystyle C[s]=\begin{cases*}K@s&when $C=K$\\\ st&when $C={[\hskip
5.0pt]}t$\\\ s&when $C={[\hskip 5.0pt]}$\end{cases*}$

######  Lemma 6.23 (RPO step).

Given some context $C$, and $\gamma(s_{1},\,\dots,\,s_{n})=s\succ t$, with
each $C[s_{i}]\in SN$, and a “lemma hypothesis” that

  * •

Given any $(\gamma^{\prime}$, $\vec{t})$ having $(\gamma,\,\vec{s})$ greater
than $(\gamma^{\prime},\,\vec{t})$ under the lexicographic ordering
$((>_{\Sigma}),\,(\mathrel{\dot{\succ}}_{lex}))$, we have
$C[\gamma^{\prime}(t_{1},\,\dots,\,t_{n})]\in SN$,

then $C[t]\in SN$.

######  Proof 6.24.

We show that $C[t]$ is SN by induction on the size of $t$, and take cases on
the RPO rule that proves $s\succ t$:

  * •

case (1) $t=\gamma(t_{1},\,\dots,\,t_{n})$. First we show $C[t_{i}]$ is SN,
which is given by the induction hypothesis (noting $t_{i}$ is smaller than
$t$). Then by the lemma hypothesis,
$C[t]=C[\gamma^{\prime}(t_{1},\,\dots,\,t_{n})]$ is SN. Satisfying the
ordering required by the lemma hypothesis, $\gamma$ has not changed and the
RPO rule has offered $\vec{s}\succ_{lex}\vec{t}$, in turn implying
$\vec{s}\mathrel{\dot{\succ}}_{lex}\vec{t}$. Also note that the lemma
hypothesis itself is preserved, when inducting.

  * •

case (2) $t=\gamma^{\prime}(t_{1},\,\dots,\,t_{m})$ and
$\gamma>_{\Sigma}\gamma^{\prime}$. First we show $C[t_{i}]$ is SN, which is
given by the induction hypothesis (noting $t_{i}$ is smaller than $t$). Then
by the lemma hypothesis, $C[t]=C[\gamma^{\prime}(t_{1},\,\dots,\,t_{m})]$ is
SN. The lemma hypothesis is satisfied by $\gamma>_{\Sigma}\gamma^{\prime}$.

  * •

case (3) $s_{i}\succeq t$. Here $C[t]$ is in the reduction tree of $C[s_{i}]$,
which was assumed SN, so then $C[t]\in SN$.

######  Lemma 6.25.

Let $s=\gamma(s_{1},\,\dots,\,s_{n})$. Given a context $C$, if each $s_{i}$
has $C[s_{i}]\in SN$, then $C[s]\in SN$.

######  Proof 6.26.

By cases on the type of $s$. In each case, we study the possible terms $C[s]$
and show that their reducts are all SN, and thus that $C[s]$ is.

  * •

case $B$. It must be that $C={[\hskip 5.0pt]}$ so we just study the term $s$
itself. By induction on the tuple $(\gamma,\,\vec{s})$ lexicographically
ordered by

$((>_{\Sigma}),\,(\mathrel{\dot{\succ}}_{lex})).$

By cases on the reducts of $s$:

    * –

case $\gamma(s_{1},\,\dots,\,s_{i}^{\prime},\,\dots,\,s_{n})$ for some index
$i$ and $s_{i}\mathrel{\dot{\succ}}s_{i}^{\prime}$. The inner inductive
hypothesis applies because $\gamma$ is unchanged, while $\vec{s}$ has
decreased under $\mathrel{\dot{\succ}}_{lex}$.

    * –

case $t$ where $s\succ t$. (Under the un-dotted $\succ$ relation.) Lemma 6.23
applies. Our inner induction hypothesis implies the “lemma hypothesis” of
Lemma 6.23.

  * •

case $T_{1}\to T_{2}$. The context $C$ is either ${[\hskip 5.0pt]}$ or
${[\hskip 5.0pt]}s^{\prime}$. Showing that $ss^{\prime}$ is SN covers all the
cases for $s$ alone, so we only show those. Proceed by lexicographical
induction on $(s^{\prime},\,\gamma,\,\vec{s})$, ordered by
$(\mathrel{\dot{\succ}},\,>_{\Sigma},\,\mathrel{\dot{\succ}}_{lex})$.

    * –

case a subterm reduces: either some $s_{i}\mathrel{\dot{\succ}}s^{\prime}_{i}$
or the applicand $s^{\prime}\mathrel{\dot{\succ}}s^{\prime\prime}$. By IH,
with reduction sequence decreasing.

    * –

case $s\succ t$. Lemma 6.23 applies. Our induction hypothesis implies the
“lemma hypothesis”.

  * •

case $\mathsf{E}(T^{\prime})$. Here $C=K$. Since $K@s_{i}\in SN$, we know that
$K$ itself is SN. We proceed by an lexicographic induction on the tuple

$(|K|,\,K,\gamma,\,\vec{s})\text{ ordered by
}(>,\,\mathrel{\dot{\succ}},\,>_{\Sigma},\,\mathrel{\dot{\succ}}_{lex}).$

We show that every reduct of $K@s=K@\gamma(s_{1},\,\dots,\,s_{n})$ is
strongly-normalizing, and thus that the term itself is. By cases on those
reducts:

    * –

case $K@\gamma(s_{1},\,\dots,\,s_{i}^{\prime},\,\dots,\,s_{n})$ for some index
$i$ and $s_{i}\mathrel{\dot{\succ}}s_{i}^{\prime}$. The IH applies: $K$ and
$\gamma$ are unchanged and the arguments $\vec{s}$ have lexicographically
reduced under $\mathrel{\dot{\succ}}$.

    * –

case $K^{\prime}@s$ where $K\mathrel{\dot{\succ}}K^{\prime}$. The IH applies
because the continuation has gotten no longer (Lemma 6.15) and $K^{\prime}$ is
in the reduction tree of $K$.

    * –

case $K^{\prime}@\gamma(F[s_{1}],\,\dots,\,F[s_{n}])$ where $K=K^{\prime}\circ
F$ and $\gamma$ is an effect symbol (eff-assoc). The IH applies because $K$
has gotten shorter (as $K^{\prime}$). We also need that $K^{\prime}@F[s_{i}]$
is SN, to satisfy the IH, but $K^{\prime}@F[s_{i}]=K@s_{i}$, which we already
know is SN.

    * –

case $K@t$ where $s\succ t$. (Under the un-dotted $\succ$ relation.) Lemma
6.23 applies.

######  Lemma 6.27.

For a rewritable symbol $\gamma:S_{1}\times\cdots\times S_{n}\to T$, if each
$s_{i}\in\mathsf{Red}_{S_{i}}$, then
$s=\gamma(s_{1},\,\dots,\,s_{n})\in\mathsf{Red}_{T}$.

######  Proof 6.28.

By cases on the type of $s$.

  * •

case $B$. To show $s\in\mathsf{Red}_{B}$ for which we only need that $s\in
SN$, and we get this from Lemma 6.25.

  * •

case $T_{1}\to T_{2}$. To show $ss^{\prime}\in\mathsf{Red}_{T_{2}}$ for any
$s^{\prime}\in\mathsf{Red}_{T_{1}}.$ Because $ss^{\prime}$ is neutral, we can
show just that all the reducts of $ss^{\prime}$ are reducible. By induction on
$((\gamma,\vec{s}),s^{\prime})$ ordered by
$((>_{\Sigma},\mathrel{\dot{\succ}}_{lex}),\mathrel{\dot{\succ}}_{lex})_{lex}$.
The only reductions of $ss^{\prime}$ are in $s$ or in $s^{\prime}$. If in
$s^{\prime}$, the IH suffices. If in $s$, there are two possibilities:

    * –

case the reduction is of the form $s=\gamma(s_{1},\,\dots
s_{i},\,\dots,\,s_{n})\mathrel{\dot{\succ}}\gamma(s_{1},\,\dots
s_{i}^{\prime},\,\dots,\,s_{n})$ with
$s_{i}\mathrel{\dot{\succ}}s_{i}^{\prime}$, in which case the IH suffices.

    * –

case $s\succ t$. If it reduces by $s\succ
t=\gamma^{\prime}(t_{1},\,\dots,\,t_{m})$ with
$(\gamma,\vec{s})>_{RPO}(\gamma^{\prime},\vec{t})$, then IH proves the point.
On the other hand, if it is $s_{i}\succeq t$ then $t\in\mathsf{Red}_{S_{i}}$
by virtue of the $s_{i}\in\mathsf{Red}_{S_{i}}$ assumption.

  * •

case $\mathsf{E}(T^{\prime})$. To show $K@s\in SN$ for any
$K\in\mathsf{Red}_{T^{\prime}}^{\top}$. Because
$s_{i}\in\mathsf{Red}_{S_{i}}$, we have $K@s_{i}\in SN$, which satisfies the
premises of Lemma 6.25, thus $K@s\in SN$ as needed.

Write $s\\{\vec{s}/\vec{x}\\}$ for the operation of simultaneously
substituting each $s_{i}$ for the free variable $x_{i}$ within $s$:
$s\\{\vec{s}/\vec{x}\\}=s\\{s_{1}/x_{1},\,\dots,\,s_{n}/x_{n}\\}$.

######  Lemma 6.29 (Reducibility).

Given $x_{1}:S_{1},\,\dots,\,x_{n}:S_{n}\vdash t:T$, for all
$\vec{s}\in\mathsf{Red}_{\vec{S}}$, we have
$t\\{\vec{s}/\vec{x}\\}\in\mathsf{Red}_{T}$.

######  Proof 6.30.

By structural induction on $t$.

  * •

case $x_{i}$. Then $S_{i}=T$. Now $s_{i}\in\mathsf{Red}_{S_{i}}$ and
$x_{i}\\{s_{i}/x_{i}\\}=s_{i}\in\mathsf{Red}_{S_{i}}=\mathsf{Red}_{T}$.

  * •

case $s^{\prime}t^{\prime}$. Immediate from Lemma 6.11 and the IH.

  * •

case $\lambda x.u$. The type derivation has $\Gamma,\,x:S\vdash u:T^{\prime}$.
Let $s^{\prime}$ be in $\mathsf{Red}_{S}$. By inductive hypothesis, using
$\Gamma$ extended with $s^{\prime}$, we have
$u\\{\vec{s}/\vec{x},s^{\prime}/x\\}=u\\{\vec{s}/\vec{x}\\}\\{s^{\prime}/x\\}\in\mathsf{Red}_{T}$,
and thence by Lemma 6.13, $\lambda x.u\in\mathsf{Red}_{S\to T^{\prime}}$.

  * •

case $\mathit{pure}(M)$. Immediate from Lemma 6.17 and the IH.

  * •

case $\gamma(t_{1},t_{2},...,t_{n})$. Immediate from Lemma 6.27 and the IH.

  * •

case
$\mathop{\mathsf{let}}x\mathop{\Leftarrow}t^{\prime}\mathop{\mathsf{in}}u$.
The type derivation is such that $\Gamma\vdash t^{\prime}:S$ and
$\Gamma,x:S\vdash u:T$. By IH, we have
$t^{\prime}\\{\vec{s}/\vec{x}\\}\in\mathsf{Red}_{S}$ and then
$u\\{t^{\prime}/x\\}\\{\vec{s}/\vec{x}\\}=u\\{\vec{s}/\vec{x},t^{\prime}\\{\vec{s}/\vec{x}\\}/x\\}\in\mathsf{Red}_{T}$
and from there, Lemma 6.27.

##  7 Revisiting the Examples

So what does all this give us? Can we use this technique to show termination
for some interesting calculi?

#### Global state

Recall the rewrite rules of global state given earlier:

$\displaystyle assign_{i}(get(t_{1},\,\dots,\,t_{n}))$ $\displaystyle\leadsto
assign_{i}(t_{i})$ $\displaystyle assign_{i}(assign_{j}(s))$
$\displaystyle\leadsto assign_{j}(s)$ $\displaystyle
get(t_{1},\,\dots,\,t_{i},\,\dots,\,t_{n})$ $\displaystyle\leadsto
get(t_{1},\,\dots,\,s_{i},\,\dots,\,t_{n})$ where
$t_{i}=get(s_{1},\,\dots,\,s_{n})$

These are easily shown to be normalizing: each only needs the RPO(3) case once
or twice.

#### Nondeterminism

$or(or(s,t),u))\leadsto or(s,or(t,u))$

With one effect symbol, the $>_{\Sigma}$ relation is empty. But we check the
RPO conditions on the solitary rule. Because the function symbols match, we
use RPO(1). We have to check the lexicographical ordering of the arguments:
$or(s,\,t)\succ s$ (by RPO(3)) so we don’t need to check the second argument.
Then each argument on the RHS must be less than the whole term on the left,
which is easily done (recursively applying RPO(3) or (1)). Note that the
lexicographical ordering was crucial to ensuring this rule makes progress
toward termination.

#### Parallelism

For parallelism, set $par>_{\Sigma}e$ for each other effect symbol $e$.
Recursive comparisons can then be carried out. Note for example that
$par(e(s_{1},\dots,s_{n}),\,t)\succ par(s_{i},\,t)$ under RPO(1), the
arguments are lexicographically decreasing, and $s_{i}$ and $t$ can each be
found as subterms.

#### Request-retry

Restating the rewrite rules:

$\displaystyle retry(zero(),request(t,s_{1},\,\dots,\,s_{n}))$
$\displaystyle\leadsto$ $\displaystyle t$ $\displaystyle
retry(succ(u),request(t,s_{1},\,\dots,\,s_{n}))$ $\displaystyle\leadsto$
$\displaystyle request(retry(u,t^{\prime}),s_{1},\,\dots,\,s_{n})$

Let $\mathit{retry}>_{\Sigma}\mathit{request}.$ The first rule has $t$ as a
subterm of the left-hand side, so it is in RPO. The second rule has
$\mathit{retry}>_{\Sigma}\mathit{request}$ and then we need to show

$retry(succ(u),request(t,s_{1},\,\dots,\,s_{n}))\succ retry(u,t^{\prime})$

and each $s_{i}$ has

$retry(succ(u),request(t,s_{1},\,\dots,\,s_{n}))\succ s_{i}.$

The latter is easy, via the subterm rule. For the former, the head symbol
matches, and then the immediate subterms $u$ and $t^{\prime}$ can both be
found as subterms of the left-hand side.

##  8 Related Work

Johann, et al. [8] give “a generic operational metatheory for algebraic
effects”. The authors work with computation trees, or traces, like those which
are the normal forms of algebraic-effect systems in the absence of equations.
An equivalence (in fact, a preorder), between computation trees is given for
each kind of effect system, but it is given through a separate definition
which simulates the operation of each effect on a separate state-
representation (a kind of abstract machine). By contrast, we have explored
what happens when the effects can be defined by rewrites on the effect symbols
themselves. Gavazzo and Faggian [6] explain monadic effects in rewrite
systems. This work interprets the rewrite relation _itself_ as
monadic/effectful, so for example the rewrite relation can have a
probabilistic distribution on its possible right-hand terms.

We have set out to show that a set of rewrite rules can be applied in any
order and still normalize. But one may instead choose a _particular_ rewriting
or normalization strategy. Normalization By Evaluation is one such approach,
and Ahman and Staton [1] have shown how to perform NBE on a calculus with
algebraic effects and a sequencing form (like our $\mathsf{let}$).

We build on the long history of rewrite-rule orderings to prove termination.
Dershowitz [5] gives the original RPO ordering and termination proof. That
proof is entirely different from the reducibility method, which is
necessitated by the difficulties of the let-assoc rule. Okada [14] is the hero
of our present work, as it is the first paper to show a general proof for
strong normalization of any SN rewrite system crossed with the syntax of
simply-typed lambda-calculus. Showing such orthogonality between rewrites and
other syntax features is the spirit of the present work.

##  9 Future Work

So far, we have only shown a modest improvement on existing strong-
normalization systems. The symbols in the system have their own rewrite rules,
but are allowed to interact with $\mathsf{let}$ in just one way, commuting out
of the subject position. We hope to give similar strong-normalization proofs
for systems in which the rewrite system can specify further interactions with
$\mathsf{let}$ (although some restrictions may remain). Our grand “test cases”
for the technique are the systems in Cooper [3] and Ricciotti and Cheney [18]:
when we can prove these strongly-normalizing with only a symbol-ordering, we
will have succeeded.

#### Thanks

Thanks to Sam Lindley, Matija Pretnar, and Wilmer Ricciotti for helpful
comments shaping this work.

## References

  * [1] Danel Ahman and Sam Staton.  Normalization by evaluation and algebraic effects.  Electronic Notes in Theoretical Computer Science, 298:51–69, 2013\.
  * [2] Andrej Bauer.  What is algebraic about algebraic effects and handlers?, 2018.  URL: https://arxiv.org/abs/1807.05923, doi:10.48550/ARXIV.1807.05923.
  * [3] Ezra Cooper.  The script-writer’s dream: How to write great SQL and be sure it will succeed.  International Symposium on Database Programming Languages, 2009\.
  * [4] Ezra Cooper, Sam Lindley, Philip Wadler, and Jeremy Yallop.  Links: Web programming without tiers.  In International Symposium on Formal Methods for Components and Objects, pages 266–296. Springer, 2007.
  * [5] Nachum Dershowitz.  Orderings for term-rewriting systems.  Theoretical Computer Science, 17(3):279–301, 1982.
  * [6] Francesco Gavazzo and Claudia Faggian.  A relational theory of monadic rewriting systems, part I.  In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–14. IEEE, 2021.
  * [7] Jean-Yves Girard, Paul Taylor, and Yves Lafont.  Proofs and types.  Cambridge University Press, 1989.
  * [8] Patricia Johann, Alex Simpson, and Janis Voigtländer.  A generic operational metatheory for algebraic effects.  In 2010 25th Annual IEEE Symposium on Logic in Computer Science, pages 209–218. IEEE, 2010.
  * [9] Jean-Pierre Jouannaud and Albert Rubio.  The higher-order recursive path ordering.  In Proceedings. 14th Symposium on Logic in Computer Science, pages 402–411. IEEE, 1999.
  * [10] Paul Blain Levy, John Power, and Hayo Thielecke.  Modelling environments in call-by-value programming languages.  Information and computation, 185(2):182–210, 2003.
  * [11] Sam Lindley and Ian Stark.  Reducibility and $\top\top$-lifting for computation types.  In International Conference on Typed Lambda Calculi and Applications, pages 262–277. Springer, 2005.
  * [12] Erik Meijer, Brian Beckman, and Gavin Bierman.  LINQ: Reconciling object, relations and XML in the .NET framework.  In Proceedings of the 2006 ACM SIGMOD International Conference on Management of Data, pages 706–706, 2006.
  * [13] Eugenio Moggi.  Computational lambda-calculus and monads.  University of Edinburgh, Department of Computer Science, Laboratory for Foundations of Computer Scence, 1988.
  * [14] Mitsuhiro Okada.  Strong normalizability for the combined system of the typed lambda calculus and an arbitrary convergent term rewrite system.  In Proc. of the ACM-SIGSAM 1989 International Symposium on Symbolic and Algebraic Computation, pages 357–363, 1989.
  * [15] Gordon Plotkin and John Power.  Adequacy for algebraic effects.  In International Conference on Foundations of Software Science and Computation Structures, pages 1–24. Springer, 2001.
  * [16] Gordon Plotkin and John Power.  Notions of computation determine monads.  In International Conference on Foundations of Software Science and Computation Structures, pages 342–356. Springer, 2002.
  * [17] Gordon Plotkin and Matija Pretnar.  A logic for algebraic effects.  In 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pages 118–129. IEEE, 2008.
  * [18] Wilmer Ricciotti and James Cheney.  Strongly normalizing higher-order relational queries.  In Zena Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction, pages 28:1–28:22. Schloss Dagstuhl, 2020.
  * [19] Amr Sabry and Philip Wadler.  A reflection on call-by-value.  ACM Transactions on Programming Languages and Systems, 19(6):916–941, 1997.
  * [20] Limsoon Wong.  Normal forms and conservative properties for query languages over collection types.  In Proceedings of the twelfth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, pages 26–36, 1993.