# Integral Cayley graphs of symmetric groups on transpositions

Alireza Abdollahi a 111E-mail<EMAIL_ADDRESS>(corresponding
author), Majid Arezoomand b 222Email<EMAIL_ADDRESS>and Mahdi Ebrahimi
c 333Email<EMAIL_ADDRESS>
a Department of Pure Mathematics, Faculty of Mathematics and Statistics,
University of Isfahan, Isfahan 81746-73441, Iran
b University of Larestan, Larestan 74317-16137, Iran
cSchool of Mathematics, Institute for Research in Fundamental Sciences (IPM),
Tehran 19395-5746, Iran

###### Abstract

We study subsets $T$ consisting of some transpositions $(i,j)$ of the
symmetric group $S_{n}$ on $\\{1,\dots,n\\}$ such that the Cayley graph
$\Gamma_{T}:=Cay(S_{n},T)$ is an integral graph, i.e., all eigenvalues of an
adjacency matrix of $\Gamma_{T}$ are integers. Graph properties of
$\Gamma_{T}$ are determined in terms of ones of the graph $G_{T}$ whose vertex
set is $\\{1,\dots,n\\}$ and $\\{i,j\\}$ is an edge if and only if $(i,j)\in
T$. Here we prove that if $G_{T}$ is a tree then $\Gamma_{T}$ is integral if
and only if $T$ is isomorphic to the star graph $K_{1,n-1}$, answering Problem
5 of [Electron. J. Comnin., 29(2) (2022) # P2.9]. Problem 6 of the latter
article asks to find necessary and sufficient conditions on $T$ for
integralness of $Cay(S_{n},T)$ without any further assumption on $T$. We show
that if $G_{T}$ is a graph which we call it a “generalized complete
multipartite graph” then $Cay(S_{n},T)$ is integral. We conjecture that
$Cay(S_{n},T)$ is integral only if $G_{T}$ is a generalized complete
multipartitie graph. To support the latter conjecture we show its validity
whenever $G_{T}$ is some classes of graphs including cycles and cubic graphs.

Keywords: Cayley graph; Symmetric group; Transposition; Spectra of graphs;
Eigenvalues of graphs; Integral graphs.
Mathematics Subject Classification: 05C50; 05C25.

##  1 Introduction

Let $G$ be a group and $S$ be a subset of $G$ such that $S$ is inverse closed
(i.e. $s\in S\Leftrightarrow s^{-1}\in S$) and the identity element $1$ of $G$
does not belong to $S$. Then the Cayley graph $Cay(G,S)$ is the graph whose
vertex set is the set of elements of $G$ and two vertices $g_{1},g_{2}\in G$
are adjacent if and only if $g_{1}g_{2}^{-1}\in S$. It is well known that
$Cay(G,S)$ is connected if and only if $G$ can be generated by $S$.

Let $S_{n}$ be the symmetric group on $[n]:=\\{1,\dots,n\\}$. For a set $T$ of
transpositions in $S_{n}$, $G_{T}$ is the graph with vertex set $[n]$ such
that $i,j\in[n]$ are adjacent if and only if $(i,j)\in T$. It is well known
that $Cay(S_{n},T)$ is connected if and only if $G_{T}$ is connected. The
(adjacency) spectrum of a finite simple graph $\Gamma$ is the multiset of
eigenvalues of an adjacency matrix of $\Gamma$. A graph is called integral if
and only if the spectrum consists of only integers.

Here we study the following problems proposed in [13].

######  Problem 1.

[13, Problem 5] Let $T$ be a set of transpositions in $S_{n}$ such that
$G_{T}$ is a tree, where $n\geq 2$. Give a necessary and sufficient condition
for $Cay(S_{n},T)$ to be integral.

######  Problem 2.

[13, Problem 6] Let $T$ be a set of transpositions in $S_{n}$ such that
$G_{T}$ is connected, where $n\geq 2$. Give a necessary and sufficient
condition for $Cay(S_{n},T)$ to be integral.

In Problem 1, a sufficient condition on $T$ is known to be $G_{T}\cong
K_{1,n-1}$ the star graph with $n$ vertices (see [1], [4, Theorem 5.3], [5],
[11]). We complete the answer to Problem 1 by showing that the latter
condition is also necessary (see part (b) of Corollary 1, below).

About Problem 2, we prove that if $G_{T}$ is a “generalized complete
multipartite graph” (see Definition 2) then $Cay(S_{n},T)$ is integral. We
propose as a conjecture (see Conjecture 1, below) that the converse of the
latter holds valid. To support Conjecture 1, we prove its validity for some
classes of graphs including cycles and cubic graphs (see Propositions 4, 5 and
6).

##  2 Preliminaries

Throughout the paper we use the following notations:

$C_{n}$: the cycle graph with $n$ vertices.

$K_{n}$: the complete graph with $n$ vertices.

$K_{n_{1},n_{2},\dots,n_{k}}$: the complete multipartite graph with $k$ parts
of sizes $n_{1},n_{2},\dots,n_{k}$.

For a given graph $\Gamma$:

$V(\Gamma)$: the set of vertices of $\Gamma$.

$E(\Gamma)$: the set of edges of $\Gamma$.

$n\Gamma$: the graph which is disjoint union of $n$ copies of the graph
$\Gamma$.

$\Gamma_{1}\cup\Gamma_{2}$: the disjoint union of graphs $\Gamma_{1}$ and
$\Gamma_{2}$.

$\Gamma_{1}*\Gamma_{2}$: the join graph of disjoint graphs $\Gamma_{1}$ and
$\Gamma_{2}$.

$\mathcal{L}(\Gamma)$: the Laplacian matrix of $\Gamma$ which is $D-A$, where
$D$ is the diagonal matrix of the vertex-degrees and $A$ is the adjacency
matrix of $\Gamma$ with the same row vertex-labeling as $D$.

$I_{\Gamma}$: the set of all isolated vertices of a graph $\Gamma$.

$\Gamma^{\\#}$ : the induced subgraph of $\Gamma$ on the set
$V(\Gamma)\setminus I_{\Gamma}$.

$\Gamma+v$: the graph obtained by adding the isolated vertex $v$ to the graph
$\Gamma$.

###  2.1 Eigenvalues of Cayley graphs

For the basic definitions and facts from representation theory of finite
groups, not defined here, we refer the reader to [14]. Let $G$ be a finite
group and ${\rm Irr}(G)=\\{\rho_{1},\ldots,\rho_{m}\\}$ be the set of all
inequivalent irreducible complex representations of $G$ and $\mathbb{C}G$ be
the group algebra of elements of the form $\sum_{g\in G}a_{g}g$, where
$a_{g}\in\mathbb{C}$. It is clear that $\mathbb{C}G$ is a vector space over
$\mathbb{C}$ of dimension $|G|$. The left regular representation
$\rho_{\textrm{reg}}:G\rightarrow GL(\mathbb{C}G)$ is the right translation
acting naturally on $\mathbb{C}G$:

$\rho_{\textrm{reg}}(g)(\sum_{h\in G}a_{h}h)=\sum_{h\in G}a_{h}(gh).$

It is well-know that $\rho_{\textrm{reg}}=d_{1}\rho_{1}\oplus\dots\oplus
d_{m}\rho_{m}$, where $d_{i}$ is the degree of $\rho_{i}$. Let $\Gamma={\rm
Cay}(G,S)$ be a Cayley (di)graph over $G$ with respect to a subset $S$ of $G$
and $A$ be the adjacency matrix of $\Gamma$. If we view $A$ as a linear map
$A:\mathbb{C}G\rightarrow\mathbb{C}G$, then $A=\sum_{g\in
G}\rho_{\textrm{reg}}(g)$ and the following result arises:

######  Proposition 1.

([2, Corollary 7] and [7]) Let $\Gamma={\rm Cay}(G,S)$ be an Cayley graph over
a finite group $G$ with irreducible matrix representations
$\rho_{1},\ldots,\rho_{m}$. Let $d_{l}$ be the degree of $\rho_{l}$. For each
$l\in\\{1,\ldots,m\\}$, define a $d_{l}\times d_{l}$ matrix
$A_{l}:=\rho_{l}(S)$, where $\rho_{l}(S)=\sum_{s\in S}\rho_{l}(s)$. Let
$\chi_{A_{l}}(\lambda)$ and $\chi_{A}(\lambda)$ be the characteristic
polynomials of $A_{l}$ and $A$, respectively. Then

  1. (1)

there exists a basis $\mathcal{B}$ such that $[A]_{\mathcal{B}}={\rm
Diag}(A_{1}\otimes I_{d_{1}},\ldots,A_{m}\otimes I_{d_{m}})$, where
$I_{d_{l}}$ is the $d_{l}\times d_{l}$ identity matrix.

  2. (2)

$\chi_{A}(\lambda)=\Pi_{l=1}^{m}\chi_{A_{l}}(\lambda)^{d_{l}}$.

A partition is a weakly decreasing finite sequence of positive integers
$\alpha=(\alpha_{1},\dots,\alpha_{l})$. We call
$|\alpha|=\alpha_{1}+\dots+\alpha_{l}$ the size of $\alpha$. The notation
$\alpha\vdash n$ is used for a partition $\alpha$ of a positive integer $n$.
It is well known that both the conjugacy classes of $S_{n}$ and the
irreducible characters of $S_{n}$ are indexed by partitions $\alpha$ of $[n]$
(see [8]). We denote the irreducible character corresponding to the partition
$\alpha\vdash n$ by $\chi^{\alpha}$ and its degree by $f_{\alpha}$.

######  Lemma 1.

Let $T$ be the set of all transpositions of $S_{n}$ or equivalently $G_{T}$ is
the complete graph. Then ${\rm Cay}(S_{n},T)$ is an integral graph and its
spectrum is

$\big{\\{}{q_{\alpha}:=\frac{n(n-1)}{2f_{\alpha}}\chi^{\alpha}((1,2))\;|\;\alpha\vdash
n\big{\\}}}.$

Proof. Since the set $T$ is a conjugacy class of $S_{n}$, the first part
follows from [7, Lemma 5]. Being integer of $q_{\alpha}$ follows from the fact
that the eigenvalues of a simple graph are algebraic integers and by [7, Lemma
7] that $q_{\alpha}$ is a rational number. $\hfill\blacksquare$

######  Proposition 2.

Let $T$ be a set of transpositions in $S_{n}$ such that $G_{T}$ is a disjoint
union of complete multipartite graphs. Then ${\rm Cay}(S_{n},T)$ is integral.

Proof. Since by Lemma 1 for every partition $\alpha\vdash n$, $q_{\alpha}$ is
an integer, it follows from [4, Theorem 5.3 and Proposition 5.2], that ${\rm
Cay}(S_{n},T)$ is integral. $\hfill\blacksquare$

##  3 Main results

Given a permutation $\pi\in S_{n}$, we denote by $P_{\pi}=(p_{ij})$ the
$n\times n$ permutation matrix with entries $p_{ij}=1$ if $i^{\pi}=j$, and $0$
otherwise.

Recall that a graph $\Gamma$ is called Laplacian integral if the spectrum of
$\mathcal{L}(\Gamma)$ consists of only integers.

######  Theorem 1.

Let $T$ be a set of transpositions in $S_{n}$, $n\geq 2$. If ${\rm
Cay}(S_{n},T)$ is integral then $G_{T}$ is Laplacian integral.

Proof. Given $\tau=(i,j)\in T$, we have
$P_{\tau}=I_{n}-e_{ii}-e_{jj}+e_{ij}+e_{ji}$, where $e_{rs}$ is the $n\times
n$ matrix that its $rs$-th entry is $1$ and the remaining entries are $0$. On
the other hand, $\sum_{(i,j)\in T}[e_{ii}+e_{jj}]$ and $\sum_{(i,j)\in
T}[e_{ij}+e_{ji}]$ are the degree matrix and the adjacency matrix of $G_{T}$,
respectively. Therefore, $\sum_{\tau\in
T}P_{\tau}=|T|I_{n}-\mathcal{L}(G_{T})$. On the other hand, each eigenvalue of
$\sum_{\tau\in T}P_{\tau}$ is an eigenvalue of ${\rm Cay}(S_{n},T)$, by [6,
Proposition 2.1]. Therefore integrality of ${\rm Cay}(S_{n},T)$ implies the
integrality of $\mathcal{L}(G_{T})$ as desired. $\hfill\blacksquare$

######  Remark 1.

One can see that the map

$\displaystyle\varphi$ $\displaystyle:$ $\displaystyle S_{6}\rightarrow
GL_{5}(\mathbb{C})$ $\displaystyle(1,2,3,4,5)$ $\displaystyle\mapsto$
$\displaystyle\begin{bmatrix}0&0&0&0&1\\\ 1&0&0&0&0\\\ 0&0&0&1&0\\\
0&0&1&0&0\\\ 0&1&0&0&0\end{bmatrix}$ $\displaystyle(1,2)$
$\displaystyle\mapsto$ $\displaystyle\begin{bmatrix}0&0&1&0&0\\\ 0&0&0&0&1\\\
1&0&0&0&0\\\ -1&-1&-1&-1&-1\\\ 0&1&0&0&0\end{bmatrix}$

is an irreducible representation of $S_{6}$. Let
$T=\\{(1,2),(2,3),(3,4),(4,5),(5,6),(6,1)\\}$. Then the characteristic
polynomial of $\sum_{t\in T}\varphi(t)$ is $x(x+1)^{2}(x^{2}+2x-12)$ has non-
integer roots, which means that ${\rm Cay}(S_{n},T)$ is non-integral Cayley
graph by Proposition 1. Since $G_{T}\cong C_{6}$ is Laplacian integral, this
means that the converse of Theorem 1 does not hold in general.

######  Definition 1.

Suppose $G_{1},\dots,G_{k}$, $k\geq 2$, are graphs with the same vertex set. A
graph $G$ is called weakly join of $G_{1},\dots,G_{k}$ if there exist
subgraphs $\Gamma_{i}$ of $G_{i}$, $1\leq i\leq k$ such that

  * (1)

for every $1\leq i\leq k$, $E(\Gamma_{i})=E(G_{i})$,

  * (2)

for every $i\neq j$, $V(\Gamma_{i})\cap V(\Gamma_{j})=\varnothing$, and

  * (3)

$G^{\\#}=\Gamma_{1}*\dots*\Gamma_{k}$.

We use the notation $\mathcal{WJ}(G_{1},\dots,G_{k})$ for the set of all
weakly join defined with respect to $G_{1},\dots,G_{k}$.

######  Theorem 2.

Let $T_{1}$, $T_{2}$ and $T$ be sets of transpositions in $S_{n}$ such that
$G_{T}\in\mathcal{WJ}(G_{T_{1}},G_{T_{2}})$. Suppose that ${\rm
Cay}(S_{n},T_{1})$ is integral. Then ${\rm Cay}(S_{n},T)$ is integral if and
only if ${\rm Cay}(S_{n},T_{2})$ is integral.

Proof. Let $T_{3}:=\\{(i,i^{\prime})\in S_{n}\mid\\{i,i^{\prime}\\}\in
E(G_{T})\setminus(E(G_{T_{1}})\cup E(G_{T_{2}}))\\}$. Consider the elements
$a_{i}:=\sum_{t\in T_{i}}t$ ($i=1,2,3$) in the group algebra
$\mathbb{C}S_{n}$. It is easy to see that $\sum_{t\in T}t=a_{1}+a_{2}+a_{3}$
and in the group algebra $\mathbb{C}S_{n}$, the elements $a_{1}$, $a_{2}$ and
$a_{3}$ are pairwise commuting.

Let $\rho_{1},\dots,\rho_{m}$ be all inequivalent irreducible representations
of $S_{n}$ and $d_{i}$ be the degree of $\rho_{i}$. Then, by Proposition 1,
the spectrum of ${\rm Cay}(S_{n},S)$ is the union of the spectra of
$\rho_{1}(S),\dots,\rho_{m}(S)$, where $S\in\\{T,T_{1},T_{2},T_{3}\\}$. Since
$a_{1}$, $a_{2}$ and $a_{3}$ commute pairwise and $\rho_{i}$ is an algebra
homomorphism, $\rho_{i}(a_{j})$s commute pairwise. Hence there exists a basis
$\mathcal{B}$ of the vector space $\mathbb{C}^{d_{i}}$ such that the matrices
$\rho_{i}(a_{j})$, $j=1,2,3$ are diagonizable with respect to $\mathcal{B}$.
We can assume that $\rho_{i}(a_{j})={\rm
diag}(\lambda^{i}_{1j},\lambda^{i}_{2j},\dots,\lambda^{i}_{d_{i}j})$ with
respect to the basis $\mathcal{B}$. On the other hand, since $\rho_{i}$ is an
algebra homomorphism, we have
$\rho_{i}(T)=\rho_{i}(a_{1})+\rho_{i}(a_{2})+\rho_{i}(a_{3})$. This implies
that the eigenvalues of $\rho_{i}(T)$ are
$\lambda^{i}_{k1}+\lambda^{i}_{k2}+\lambda^{i}_{k3}$, where $k=1,\dots,d_{i}$.
By Proposition 2, ${\rm Cay}(S_{n},T_{3})$ is integral. Thus ${\rm
Cay}(S_{n},T)$ is integral if and only if ${\rm Cay}(S_{n},T_{2})$ is
integral.$\hfill\blacksquare$

######  Remark 2.

Let $T_{1},\ldots,T_{k}$ be some sets of transpositions of $S_{n}$. Using
Theorem 2 and the induction on the number of graphs, one can easily see that
if for every $i=1,\ldots,k$, the graph ${\rm Cay}(S_{n},T_{i})$ is integral,
then ${\rm Cay}(S_{n},T)$ is integral, where
$G_{T}\in\mathcal{WJ}(G_{T_{1}},\dots,G_{T_{k}})$.

######  Remark 3.

Let $S=\\{(1,2),(1,3),\ldots,(1,n)\\}$ for some positive integer $n$. It is
conjectured that ${\rm Cay}(S_{n},S)$ is integral in [1]. Using certain
properties of the Jucys-Murphy elements, the validity of the latter conjecture
was confirmed in [5]. Since the star graph
$K_{1,n-1}\in\mathcal{WJ}(nK_{1},nK_{1})$, the latter conjecture is a direct
consequence of Theorem 2.

A vertex $v$ of a graph $\Gamma$ is called a complete vertex if it is adjacent
to each vertex $u\neq v$ of $\Gamma$. For a graph $\Gamma$ a cut vertex of
$\Gamma$ is a vertex $v$ of $\Gamma$ such that the number of connected
components of $\Gamma-v$ is more than the number of connected components of
$\Gamma$. As a direct consequence of the following result, we give a complete
solution to Problem 1.

######  Corollary 1.

Let $T$ be a set of transpositions in $S_{n}$. Then

  * (a)

If $G_{T}$ is a connected graph with a cut vertex $v$ then ${\rm
Cay}(S_{n},T)$ is integral if and only if $v$ is a complete vertex and ${\rm
Cay}(S_{n},T^{\prime})$ is integral, where $T^{\prime}$ is a set of
transpositions in $S_{n}$ such that $G_{T^{\prime}}=(G_{T}-v)+v$.

  * (b)

If $G_{T}$ is a tree, then ${\rm Cay}(S_{n},T)$ is integral if and only if
$G_{T}$ is the star graph $K_{1,n-1}$.

Proof. $(a)$ Suppose that ${\rm Cay}(S_{n},T)$ is integral. Then, by Theorem 1
and [10, Corollary 2.1], $v$ is a complete vertex. We know that
$T^{\prime\prime}$ is the set of transpositions in $S_{n}$ such that
$G_{T^{\prime\prime}}=nK_{1}$ then $T^{\prime\prime}=\varnothing$ and ${\rm
Cay}(S_{n},T^{\prime\prime})$ is integral. Thus as
$G_{T}\in\mathcal{WJ}(G_{T^{\prime}},nK_{1})$, by Theorem 2, ${\rm
Cay}(S_{n},T^{\prime})$ is integral. This proves one direction. Conversely,
suppose that ${\rm Cay}(S_{n},T^{\prime})$ is integral and $v$ is a complete
vertex. Then again as $G_{T}\in\mathcal{WJ}(G_{T^{\prime}},nK_{1})$, Theorem 2
implies that ${\rm Cay}(S_{n},T)$ is integral.

$(b)$ It is clear that if $G_{T}=K_{1}$ or $K_{2}$ there is nothing to prove.
So we may assume that $G_{T}$ has at least three vertices. Suppose that ${\rm
Cay}(S_{n},T)$ is integral. Then as $G_{T}$ is a tree, by part $(a)$, $G_{T}$
has a complete vertex and so it is $K_{1,n-1}$. The converse direction is
clear by Proposition 2. $\hfill\blacksquare$

######  Definition 2.

a) Let $\Gamma_{1},\dots,\Gamma_{k}$ be graphs with the same vertex set and
for each $i$, $\Gamma_{i}$ be a disjoint union of complete multipartite
graphs. Then a graph $\Gamma$ is called generalized complete multipartite
graph of type $1$ if $\Gamma\in\mathcal{WJ}(\Gamma_{1},\dots,\Gamma_{k})$.
b) For $n\geq 2$, we say that the graph $\Gamma$ is a generalized complete
multipartite graph of type $n$, if
$\Gamma\in\mathcal{WJ}(\Gamma_{1},\dots,\Gamma_{k})$, where
$\Gamma_{1},\dots,\Gamma_{k}$ are graphs with the same vertex set and for
every $i=1,2,\dots k$, the graph $\Gamma_{i}$ is a disjoint union of
generalized complete multipartite graphs of type at most $n-1$.

######  Proposition 3.

Let $T$ be a set of transpositions in $S_{n}$ such that $G_{T}$ is a
generalized complete multipartite graph of type $k$, for some positive integer
$k$. Then ${\rm Cay}(S_{n},T)$ is integral.

Proof. We prove by induction on $k$. The case $k=1$ is clear by Proposition 2
and Theorem 2. Suppose that the result is true for every generalized complete
multipartite graph of type at most $k-1$. Now the result follows from the
induction hypothesis, [4, Proposition 5.2] and Theorem 2. $\hfill\blacksquare$

By the above result in the sequel, we suggest the following conjecture and try
to show that this conjecture is true for some classes of Cayley graphs of
symmetric groups generated by transpositions.

######  Conjecture 1.

Let $T$ be a set of transpositions in $S_{n}$. Then ${\rm Cay}(S_{n},T)$ is
integral, if and only if for some positive integer $k$, the graph $G_{T}$ is a
generalized complete multipartite graph of type $k$.

The following results confirm Conjecture 1 for cycles.

######  Proposition 4.

Let $T$ be a set of transposition in $S_{m}$ such that $G_{T}\cong C_{m}$.
Then ${\rm Cay}(S_{m},T)$ is integral if and only if $m=3$ or $4$.

Proof. It is well-known that the only integral cycles are $C_{3}$, $C_{4}$ and
$C_{6}$, see for example [3, p. 43]. Since cycles are regular graphs, the
above cycles are the only Laplacian integral cycles. Thus, one direction is a
direct consequence of Theorem 1 and Remark 1. The converse direction is clear
by Proposition 2.$\hfill\blacksquare$

######  Proposition 5.

Let $T$ be a set of transpositions in $S_{n}$ such that $G_{T}$ is a connected
cubic graph. Then ${\rm Cay}(S_{n},T)$ is integral if and only if $G_{T}$ is
isomorphic to one of the graphs $K_{4}$ or $K_{3,3}$.

Proof. Since $G_{T}$ is a connected cubic integral graph, $G_{T}$ is one of
the thirteen graphs given in [15]. Suppose that ${\rm Cay}(S_{n},T)$ is
integral. Then $G_{T}$ is isomorphic to $K_{4}$ or $K_{3,3}$, by GAP [16],
Proposition 1 and Theorem 1. The converse direction is clear by Proposition
2.$\hfill\blacksquare$

A connected graph with $n$ vertices and $m$ edges is called a $k$-cyclic graph
if $k=m-n+1$. In the following result, we give a characterization of integral
Cayley graphs ${\rm Cay}(S_{n},T)$, where $G_{T}$ is a $k$-cyclic graph and
$k=1,2,3$ which confirms Conjecture 1.

######  Proposition 6.

Let $T$ be a set of transpositions in $S_{n}$ such that $G_{T}$ is a
$k$-cyclic graph.

  * (a)

If $k=1$ then ${\rm Cay}(S_{n},T)$ is integral if and only if $G_{T}$ is one
of the graphs $K_{3}$, $K_{2,2}$ or $(K_{2}\cup(n-3)K_{1})*K_{1}$.

  * (b)

If $k=2$ then ${\rm Cay}(S_{n},T)$ is integral if and only if $G_{T}$ is one
of the graphs $K_{2,3}$, $K_{2}*(2K_{1})$, $(2K_{2}\cup(n-5)K_{1})*K_{1}$ or
$(K_{1,2}\cup(n-4)K_{1})*K_{1}$.

  * (c)

If $k=3$ then ${\rm Cay}(S_{n},T)$ is integral if and only if $G_{T}$ is one
of the graphs $(3K_{2})*K_{1}$, $(K_{1,2}\cup K_{2})*K_{1}$, $K_{2,4}$,
$K_{1,3}*K_{1}$, $K_{4}$, $K_{2,3}$, $(3K_{2}\cup(n-7)K_{1})*K_{1}$,
$(K_{1,2}\cup K_{2}\cup(n-6)K_{1})*K_{1}$, $(K_{3}\cup(n-4)K_{1})*K_{1}$ or
$(K_{1,3}\cup(n-5)K_{1})*K_{1}$.

Proof. Suppose that ${\rm Cay}(S_{n},T)$ is integral. Then, by Theorem 1,
$G_{T}$ is Laplacian integral. If $k=1$, then [12, Theorem 3.2] and Remark 1
imply that $G_{T}$ is isomorphic to one of the graphs $K_{3}$, $K_{2,2}$ or
$(K_{2}\cup(n-3)K_{1})*K_{1}$.

If $k=2$ then by [12, Theorem 3.3], $G_{T}$ is one of the graphs
$(2K_{2}\cup(n-5)K_{1})*K_{1}$, $(K_{1,2}\cup(n-4)K_{1})*K_{1}$, $K_{2,3}$,
$K_{2}*(2K_{1})$ or $K_{1,2}\square K_{2}$, where $\square$ is the direct
product operation of graphs. In the last case, one can easily see that ${\rm
Cay}(S_{6},T)$ is not integral, by GAP [16] and Proposition 1.

If $k=3$ then by [9, Theorem 4.1 and Theorem 5.1], $G_{T}$ is one of the
thirteen graphs $(3K_{2})*K_{1}$, $(K_{1,2}\cup K_{2})*K_{1}$, $K_{2,4}$,
$K_{1,3}*K_{1}$, $K_{4}$, $K_{2,3}$, $(3K_{2}\cup(n-7)K_{1})*K_{1}$,
$(K_{1,2}\cup K_{2}\cup(n-6)K_{1})*K_{1}$, $(K_{3}\cup(n-4)K_{1})*K_{1}$,
$(K_{1,3}\cup(n-5)K_{1})*K_{1}$, or $\Gamma_{1}$, $\Gamma_{2}$ and
$\Gamma_{3}$ shown in Fig. 1. We see, by GAP [16] and Proposition 1, that in
the last three cases ${\rm Cay}(S_{n},T)$ is not integral. The converse
direction is clear by Proposition 3. This completes the
proof.$\hfill\blacksquare$

Figure 1: The Laplacian integral tricyclic graphs $\Gamma_{1}$, $\Gamma_{2}$
and $\Gamma_{3}$.

## Acknowledgments

The work of Mahdi Ebrahimi is supported in part by a grant from School of
Mathematics, Institute for Research in Fundamental Sciences (IPM).

## References

  * [1] A. Abdollahi and E. Vatandoost, Which Cayley graphs are integral? Electron. J. Combin. 16 (2009), no. 1, Research Paper 122, 17 pp.
  * [2] M. Arezoomand and B. Taeri, On the characteristic polynomial of $n$-Cayley digraphs. Electron. J. Combin. 20 (2013), no. 3, Paper 57, 14 pp.
  * [3] K. Balińska, D. Cvetković, Z. Radosavljević, S. Simić, and D. Stevanović, A survey on integral graphs. Univ. Beograd. Publ. Elektrotehn. Fak. Ser. Mat., 13 (2002) 42-65.
  * [4] F. Cesi, On the eigenvalues of Cayley graphs on the symmetric group generated by a complete multipartite set of transpositions, J. Algebraic Combin., 32(2) (2010) 155-185.
  * [5] G. Chapuy and V. Feray, A note on a Cayley graph of $S_{n}$, 2012. https://arxiv.org/abs/1202.4976
  * [6] C. Dalfo and M. A. Fiol, Spectra and eigenspaces from regular partitions of Cayley (di)graphs of permutation groups, Linear Algebra Appl., 597 (2020) 94-112.
  * [7] P. Diaconis and M. Shahshahani, Generating a random permutation with random transpositions, Z. Wahrsch. Verw. Gebiete, 57(2) (1981) 159-179.
  * [8] G. James and A. Kerber, The Representation Theory of the Symmetric Group, Addison-Wesley Publishing Company, 1981.
  * [9] X. Huang, Q. Huang and F. Wen, On the Laplacian integral tricyclic graphs, Linear and Multilinear Algebra, 63(7) (2015) 1356-1371.
  * [10] S. Kirkland, A bound on the algebraic connectivity of a graph in terms of the number of cut points, Linear and Multilinear Algebra, 47(1) (2000) 93-103.
  * [11] R. Krakovski and B. Mohar, Spectrum of Cayley graphs on the symmetric group generated by transpositions, Linear Algebra Appl., 437(3) (2012) 1033-1039.
  * [12] M. Liu and B. Liu, Some results on the Laplacian spectrum, Computers and Mathematics with Applications 59 (2010) 3612-3616.
  * [13] X. Liu and S. Zhou, Eigenvalues of Cayley graphs, Electron. J. Combin. 29 (2022), no. 2, Paper No. 2.9, 164 pp.
  * [14] J. P. Serre, Linear representations of finite groups, Translated from the second French edition by L. Scott. Graduate text in mathematics, Springer, Vol. 42. New York, 1997.
  * [15] A.J. Schwenk, Exactly thirteen connected cubic graphs have integral spectra, Theory and applications of graphs (Proc. Internat. Conf., Western Mich. Univ., Kalamazoo, Mich., 1976), pp. 516-533, Lecture Notes in Math., 642, Springer, Berlin, 1978.
  * [16] The GAP Group, GAP – Groups, Algorithms, and Programming, Version 4.12.2; 2022. (https://www.gap-system.org)


* [FGKO15] Nathanaël Fijalkow, Hugo Gimbert, Edon Kelmendi, and Youssouf Oualhadj.  Deciding the value 1 problem for probabilistic leaktight automata.  Logical Methods in Computer Science, 11(2), 2015.
  * [Fij17] Nathanaël Fijalkow.  Undecidability results for probabilistic automata.  SIGLOG News, 4(4):10–17, 2017.
  * [GO10] Hugo Gimbert and Youssouf Oualhadj.  Probabilistic automata on finite words: Decidable and undecidable problems.  In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages and Programming, 37th International Colloquium, ICALP 2010, Bordeaux, France, July 6-10, 2010, Proceedings, Part II, volume 6199 of Lecture Notes in Computer Science, pages 527–538. Springer, 2010.
  * [Har86] David Harel.  Effective transformations on infinite trees, with applications to high undecidability, dominoes, and fairness.  J. ACM, 33(1):224–248, 1986.
  * [HJ94] Hans Hansson and Bengt Jonsson.  A logic for reasoning about time and reliability.  Formal Asp. Comput., 6(5):512–535, 1994.
  * [HK97] Michael Huth and Marta Z. Kwiatkowska.  Quantitative analysis and model checking.  In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997, pages 111–122. IEEE Computer Society, 1997.
  * [KLB17] Naoki Kobayashi, Étienne Lozes, and Florian Bruse.  On the relationship between higher-order recursion schemes and higher-order fixpoint logic.  In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 246–259. ACM, 2017\.
  * [KLG19] Naoki Kobayashi, Ugo Dal Lago, and Charles Grellois.  On the termination problem for probabilistic higher-order recursive programs.  In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1–14. IEEE, 2019.
  * [KLG20] Naoki Kobayashi, Ugo Dal Lago, and Charles Grellois.  On the Termination Problem for Probabilistic Higher-Order Recursive Programs.  Logical Methods in Computer Science, Volume 16, Issue 4, October 2020.
  * [KNP11] Marta Z. Kwiatkowska, Gethin Norman, and David Parker.  PRISM 4.0: Verification of probabilistic real-time systems.  In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings, volume 6806 of Lecture Notes in Computer Science, pages 585–591. Springer, 2011.
  * [Koz83] Dexter Kozen.  Results on the propositional mu-calculus.  Theor. Comput. Sci., 27:333–354, 1983.
  * [KTW18] Naoki Kobayashi, Takeshi Tsukada, and Keiichi Watanabe.  Higher-order program verification via HFL model checking.  In Amal Ahmed, editor, Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10801 of Lecture Notes in Computer Science, pages 711–738. Springer, 2018.
  * [Loz15] Étienne Lozes.  A type-directed negation elimination.  In Ralph Matthes and Matteo Mio, editors, Proceedings Tenth International Workshop on Fixed Points in Computer Science, FICS 2015, Berlin, Germany, September 11-12, 2015, volume 191 of EPTCS, pages 132–142, 2015.
  * [Lub89] Robert S. Lubarsky.  mu-definable sets of integers.  In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS ’89), Pacific Grove, California, USA, June 5-8, 1989, pages 343–352. IEEE Computer Society, 1989.
  * [MKT20] Yo Mitani, Naoki Kobayashi, and Takeshi Tsukada.  A probabilistic higher-order fixpoint logic.  In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs, pages 19:1–19:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.
  * [MM97] Carroll Morgan and Annabelle McIver.  A probabilistic temporal calculus based on expectations.  In Proc. Formal Methods Pacific, pages 4–22. Springer, 1997.
  * [MS13] Matteo Mio and Alex Simpson.  Łukasiewicz mu-calculus.  In David Baelde and Arnaud Carayol, editors, Proceedings Workshop on Fixed Points in Computer Science, FICS 2013, Turino, Italy, September 1st, 2013, volume 126 of EPTCS, pages 87–104, 2013.
  * [Paz71] Azaria Paz.  Introduction to probabilistic automata.  Academic Press, 1971.
  * [Rab63] Michael O Rabin.  Probabilistic automata.  Information and control, 6(3):230–245, 1963.
  * [Tar51] Alfred Tarski.  A Decision Method for Elementary Algebra and Geometry.  University of California Press, 1951.
  * [VV04] Mahesh Viswanathan and Ramesh Viswanathan.  A higher order modal fixed point logic.  In Philippa Gardner and Nobuko Yoshida, editors, CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings, volume 3170 of Lecture Notes in Computer Science, pages 512–528. Springer, 2004.

##  Appendix A Proofs

This section proofs omitted in the main text.

###  A.1. Proof of Theorem 6

The following lemma states that the relation $\sim$ is preserved by the least
upper bound operation.

######  Lemma A.1.

Let $I$ be a set and $T$ be a type of $\mu$-arithmetic. Assume families
$\\{v_{i}\\}_{i\in I}$ and $\\{u_{i}\\}_{i\in I}$ of elements of $\llbracket
T\rrbracket_{\mu}$ and $\llbracket\textit{tr}(T)\rrbracket$, respectively, and
suppose that $v_{i}\sim_{T}u_{i}$ for every $i\in I$. Then $\bigsqcup_{i\in
I}v_{i}\sim_{T}\bigsqcup_{i\in I}u_{i}$.

######  Proof A.2.

By induction on the structure of $T$. The base case $T=\Omega$ is obvious.
Assume that $T=A\to T^{\prime}$.

Let $x\in\llbracket A\rrbracket_{\mu}$ and
$y\in\llbracket\textit{tr}(A)\rrbracket$ and assume that $x\sim_{A}y$. For
each $i\in I$, since $v_{i}\sim_{T}u_{i}$, we have
$v_{i}\,x\sim_{T^{\prime}}u_{i}\,y$. By the induction hypothesis,

$\bigsqcup_{i\in I}(v_{i}\,x)\sim_{T^{\prime}}\bigsqcup_{i\in I}(u_{i}\,y).$

Since the order on functions are component-wise, we have

$\left(\bigsqcup_{i\in I}v_{i}\right)\,x=\bigsqcup_{i\in
I}(v_{i}\,x)\quad\mbox{and}\quad\left(\bigsqcup_{i\in
I}u_{i}\right)\,y=\bigsqcup_{i\in I}(u_{i}\,y).$

So

$\left(\bigsqcup_{i\in I}v_{i}\right)\,x\sim_{T^{\prime}}\left(\bigsqcup_{i\in
I}u_{i}\right)\,y.$

Since $x\sim_{A}y$ is arbitrary, we have:

$\left(\bigsqcup_{i\in I}v_{i}\right)\sim_{A\to
T^{\prime}}\left(\bigsqcup_{i\in I}u_{i}\right).$

We are now ready to prove Theorem 6.

######  Proof A.3 (Proof of Theorem 6).

We prove the theorem by induction on the structure of $\varphi$. In this
proof, we omit the subscript $M$ of $\llbracket-\rrbracket_{M}$ for
simplicity.

  * •

Case $\varphi=X$. In this case, $\textit{tr}(\varphi)=X$ and $\Gamma(X)=A$.
Thus, we have:

$\llbracket\Gamma\vdash_{\mu}\varphi:A\rrbracket_{\mu}(\theta)=\theta(X)\sim_{\Gamma(X)}\rho(X)=\llbracket\textit{tr}(\Gamma)\vdash\textit{tr}(\varphi):\textit{tr}(A)\rrbracket(\rho),$

as required.

  * •

Case $\varphi=Z$. In this case, $\textit{tr}(\varphi)=p_{0}^{\prime}$ and
$A=N$. We have

$\llbracket\Gamma\vdash_{\mu}\varphi:A\rrbracket_{\mu}(\theta)=0\sim_{N}(1,0,0,0)=\llbracket\textit{tr}(\Gamma)\vdash\textit{tr}(\varphi):\textit{tr}(A)\rrbracket(\rho).$

  * •

Case $\varphi=S\,t$. In this case, $A=N$. Let
$n=\llbracket\Gamma\vdash_{\mu}t:N\rrbracket_{\mu}(\theta)$. By the induction
hypothesis, we have

$\llbracket\textit{tr}(\Gamma)\vdash\textit{tr}(t):\textit{tr}(N)\rrbracket(\rho)=\left(\frac{1}{2^{n}},\;1-\frac{1}{2^{n}},\;\\_,\;\\_\right).$

By the definition of $\textit{tr}(\varphi)$ and calculation, we have

$\llbracket\textit{tr}(\Gamma)\vdash\textit{tr}(\varphi):\textit{tr}(A)\rrbracket(\rho)=\left(\frac{1}{2^{n+1}},\;1-\frac{1}{2^{n+1}},\;\\_,\;\\_\right),$

which implies
$\llbracket\Gamma\vdash_{\mu}S\,t:A\rrbracket_{\mu}(\theta)=n+1\sim_{N}\llbracket\textit{tr}(\Gamma)\vdash\textit{tr}(\varphi):\textit{tr}(A)\rrbracket(\rho)$.

  * •

Case $\varphi=(s\leq t)$. In this case, $A=\Omega$. Let
$n=\llbracket\Gamma\vdash_{\mu}s:N\rrbracket_{\mu}(\theta)$ and
$m=\llbracket\Gamma\vdash_{\mu}t:N\rrbracket_{\mu}(\theta)$. By the induction
hypothesis, we have

$\displaystyle\llbracket\textit{tr}(\Gamma)\vdash\textit{tr}(s):\textit{tr}(N)\rrbracket(\rho)$
$\displaystyle=(\frac{1}{2^{n}},\;,1-\frac{1}{2^{n}},\;\\_,\;\\_)$
$\displaystyle\llbracket\textit{tr}(\Gamma)\vdash\textit{tr}(t):\textit{tr}(N)\rrbracket(\rho)$
$\displaystyle=(\frac{1}{2^{m}},\;,1-\frac{1}{2^{m}},\;\\_,\;\\_).$

By the definition of $\textit{tr}(s\leq t)$ and calculation, we have

$\llbracket\textit{tr}(\Gamma)\vdash\textit{tr}(s\leq
t):\textit{tr}(A)\rrbracket(\rho)=\begin{cases}(1,\\_,\\_,\\_)&\mbox{(if
$\frac{1}{2}\times\big{(}\frac{1}{2^{n}}+(1-\frac{1}{2^{m}})\big{)}\geq\frac{1}{2}$,
i.e. if $n\leq m$)}\\\ (0,\\_,\\_,\\_)&\mbox{(if
$\frac{1}{2}\times\big{(}\frac{1}{2^{n}}+(1-\frac{1}{2^{m}})\big{)}<\frac{1}{2}$,
i.e., if $n>m$).}\\\ \end{cases}$

Thus, we have $\llbracket\Gamma\vdash_{\mu}s\leq
t:A\rrbracket_{\mu}(\theta)\sim_{A}\llbracket\textit{tr}(\Gamma)\vdash\textit{tr}(s\leq
t):\textit{tr}(A)\rrbracket(\rho)$ as required.

  * •

Case $\varphi=\varphi_{1}\land\varphi_{2}$.

In this case, we have $A=\Omega$.

By the induction hypothesis, we have

$\llbracket\Gamma\vdash_{\mu}\varphi_{i}:A\rrbracket_{\mu}(\theta)\sim_{A}\llbracket\textit{tr}(\Gamma)\vdash\textit{tr}(\varphi_{i}):\textit{tr}(A)\rrbracket(\rho)$

for each $i=1,2$.

By the definition of $\sim_{\Omega}$, we have

$\llbracket\textit{tr}(\Gamma)\vdash\textit{tr}(\varphi_{i}):\textit{tr}(\Omega)\rrbracket(\rho)=(\llbracket\Gamma\vdash_{\mu}\varphi_{i}:\Omega\rrbracket_{\mu}(\theta),\;\\_,\;\\_,\;\\_)$

for each $i=1,2$. Therefore we have

$\displaystyle\llbracket\Gamma\vdash_{\mu}\varphi_{1}\land\varphi_{2}:\Omega\rrbracket_{\mu}(\theta)$
$\displaystyle=\llbracket\Gamma\vdash_{\mu}\varphi_{1}:\Omega\rrbracket_{\mu}(\theta)\textstyle{\bigsqcap_{\Omega}}\llbracket\Gamma\vdash_{\mu}\varphi_{2}:\Omega\rrbracket_{\mu}(\theta)$
$\displaystyle\sim_{\Omega}(\llbracket\Gamma\vdash\varphi_{1}:\Omega\rrbracket_{\mu}(\theta)\textstyle{\bigsqcap_{\Omega}}\llbracket\Gamma\vdash\varphi_{2}:\Omega\rrbracket_{\mu}(\theta),\;\\_,\;\\_,\;\\_)$
$\displaystyle=\llbracket\textit{tr}(\Gamma)\vdash\varphi_{1}:{\mathit{Prop}}\rrbracket(\rho)\textstyle{\bigsqcap}\llbracket\textit{tr}(\Gamma)\vdash\varphi_{2}:{\mathit{Prop}}\rrbracket(\rho)$
$\displaystyle=\llbracket\textit{tr}(\Gamma)\vdash\varphi_{1}\land\varphi_{2}:{\mathit{Prop}}\rrbracket(\rho)$

as desired.

  * •

Case $\varphi=\varphi_{1}\lor\varphi_{2}$. Similar to the above case.

  * •

Case $\varphi=\lambda X.\varphi^{\prime}$. In this case, $A$ is of the form
$B\to T$, with $\Gamma,X:B\vdash_{\mu}\varphi^{\prime}:T$. For any
$v\in\llbracket B\rrbracket$ and $u\in\llbracket\textit{tr}(B)\rrbracket$ such
that $v\sim_{B}u$, we have:

$\displaystyle\llbracket\Gamma\vdash_{\mu}\varphi:A\rrbracket_{\mu}(\theta)(v)$
$\displaystyle=\llbracket\Gamma,X:B\vdash_{\mu}\varphi^{\prime}:T\rrbracket_{\mu}(\theta[X\mapsto
v])$
$\displaystyle\sim_{T}\llbracket\textit{tr}(\Gamma,X:B)\vdash\textit{tr}(\varphi^{\prime}):\textit{tr}(T)\rrbracket(\rho[X\mapsto
u])$ (by the induction hypothesis)
$\displaystyle=\llbracket\textit{tr}(\Gamma)\vdash\textit{tr}(\varphi):\textit{tr}(A)x\rrbracket(\theta)(u)$

Therefore, we have

$\llbracket\Gamma\vdash_{\mu}\varphi:B\to T\rrbracket_{\mu}(\theta)\sim_{B\to
T}\llbracket\textit{tr}(\Gamma)\vdash\textit{tr}(\varphi):\textit{tr}(B\to
T)\rrbracket(\rho)$

as required.

  * •

Case $\varphi=\varphi_{1}\,\varphi_{2}$. We have $A=T$, with
$\Gamma\vdash_{\mu}\varphi_{1}:B\to T$ and $\Gamma\vdash_{\mu}\varphi_{2}:B$.

By the induction hypothesis, we have
$\llbracket\Gamma\vdash_{\mu}\varphi_{1}:B\to
T\rrbracket_{\mu}(\theta)\sim_{B\to
T}\llbracket\textit{tr}(\Gamma)\vdash\textit{tr}(\varphi_{1}):\textit{tr}(B\to
T)\rrbracket(\rho)$ and
$\llbracket\Gamma\vdash_{\mu}\varphi_{2}:B\rrbracket_{\mu}(\theta)\sim_{B}\llbracket\textit{tr}(\Gamma)\vdash\textit{tr}(\varphi_{2}):\textit{tr}(B)\rrbracket(\rho)$.
Therefore by the definition of $\sim_{B\to T}$, we have

$\displaystyle\llbracket\Gamma\vdash_{\mu}\varphi_{1}\,\varphi_{2}:A\rrbracket_{\mu}(\theta)$
$\displaystyle=\llbracket\Gamma\vdash_{\mu}\varphi_{1}:B\to
T\rrbracket_{\mu}(\theta)\,(\llbracket\Gamma\vdash_{\mu}\varphi_{2}:B\rrbracket_{\mu}(\theta))$
$\displaystyle\sim_{A}\llbracket\textit{tr}(\Gamma)\vdash\textit{tr}(\varphi_{1}):\textit{tr}(B\to
T)\rrbracket(\rho)\,(\llbracket\textit{tr}(\Gamma)\vdash\textit{tr}(\varphi_{2}):\textit{tr}(B)\rrbracket(\rho))$
$\displaystyle=\llbracket\textit{tr}(\Gamma)\vdash\textit{tr}(\varphi_{1}\,\varphi_{2}):\textit{tr}(A)\rrbracket(\rho)$

as required.

  * •

Case $\varphi=\mu X.\varphi^{\prime}$.

In this case, $A=T$, with
$\Gamma,X\mathbin{:}T\vdash_{\mu}\varphi^{\prime}:T$. By the induction
hypothesis, for any $v\in\llbracket T\rrbracket_{\mu}$ and
$u\in\llbracket\textit{tr}(T)\rrbracket$ such that $v\sim_{T}u$, we have

$\llbracket\Gamma,X\mathbin{:}T\vdash_{\mu}\varphi^{\prime}:T\rrbracket_{\mu}(\theta[X\mapsto
v])\sim_{T}\llbracket\textit{tr}(\Gamma),X\mathbin{:}\textit{tr}(T)\vdash\textit{tr}(\varphi^{\prime}):\textit{tr}(T)\rrbracket(\rho[X\mapsto
u]).$

Since $\textit{tr}(\mu X.\varphi^{\prime})=\mu
X.\textit{tr}(\varphi^{\prime})$, it suffices to show:

$\llbracket\Gamma\vdash_{\mu}\mu
X.\varphi^{\prime}:T\rrbracket_{\mu}(\theta)\sim_{T}\llbracket\textit{tr}(\Gamma)\vdash\mu
X.\textit{tr}(\varphi^{\prime}):\textit{tr}(T)\rrbracket(\rho).$

Let $\mathcal{F}:\llbracket T\rrbracket_{\mu}\to\llbracket T\rrbracket_{\mu}$
and
$\mathcal{G}:\llbracket\textit{tr}(T)\rrbracket\to\llbracket\textit{tr}(T)\rrbracket$
be the functions defined by:

$\displaystyle\mathcal{F}(v):=\llbracket\Gamma,X\mathbin{:}T\vdash_{\mu}\varphi^{\prime}:T\rrbracket_{\mu}(\theta[X\mapsto
v])$
$\displaystyle\mathcal{G}(u):=\llbracket\textit{tr}(\Gamma),X\mathbin{:}\textit{tr}(T)\vdash\textit{tr}(\varphi^{\prime}):\textit{tr}(T)\rrbracket(\rho[X\mapsto
u]).$

By the reasoning above, we have $\mathcal{F}\sim_{T\to T}\mathcal{G}$. By the
definitions of the semantics, we have $\llbracket\Gamma\vdash_{\mu}\mu
X.\varphi^{\prime}:T\rrbracket_{\mu}(\theta)=\mathit{LFP}(\mathcal{F})$ and
$\llbracket\textit{tr}(\Gamma)\vdash\mu
X.\textit{tr}(\varphi^{\prime}):\textit{tr}(T)\rrbracket(\rho)=\mathit{LFP}(\mathcal{G})$.
Then there exists an ordinal $\alpha$ such that

$\mathit{LFP}(\mathcal{F})=\mathcal{F}^{\alpha}(\bot_{T})\qquad\mbox{and}\qquad\mathit{LFP}(\mathcal{G})=\mathcal{G}^{\alpha}(\bot_{\textit{tr}(T)}),$

where $f^{\beta}(x)$ is defined by $f^{0}(x)=x$,
$f^{\beta+1}=f(f^{\beta}(x))$, and
$f^{\beta}=\mathbin{\textstyle{\bigsqcup}}_{\gamma<\beta}f^{\gamma}(x)$ if
$\beta$ is a limit ordinal. We shall prove by (transfinite) induction on
$\beta$ that
$\mathcal{F}^{\beta}(\bot_{{T}})\sim_{T}\mathcal{G}^{\beta}(\bot_{{\textit{tr}(T)}})$,
which would imply

$\mathit{LFP}(\mathcal{F})=\mathcal{F}^{\alpha}(\bot_{{T}})\sim_{T}\mathcal{G}^{\alpha}(\bot_{{\textit{tr}(T)}})=\mathit{LFP}(\mathcal{G})$

as required.

The base case
$\mathcal{F}^{0}(\bot_{{T}})=\bot_{{T}}\sim_{T}\bot_{{\textit{tr}(T)}}=\mathcal{G}^{0}(\bot_{{\textit{tr}(T)}})$
follows by a straightforward induction on the structure of $T$. The case where
$\beta$ is a successor ordinal follows immediately from the induction
hypothesis and $\mathcal{F}\sim_{T\to T}\mathcal{G}$. If $\beta$ is a limit
ordinal, then

$\mathcal{F}^{\beta}(\bot_{{T}})=\mathbin{\textstyle{\bigsqcup}}_{\gamma<\beta}\mathcal{F}^{\gamma}(\bot_{{T}})\qquad\mbox{and}\qquad\mathcal{G}^{\beta}(\bot_{{T}})=\mathbin{\textstyle{\bigsqcup}}_{\gamma<\beta}\mathcal{G}^{\gamma}(\bot_{{T}}).$

By the induction hypothesis (of the transfinite induction),

$\mathcal{F}^{\gamma}(\bot_{{T}})\sim_{T}\mathcal{G}^{\gamma}(\bot_{{T}})$

for every $\gamma<\beta$. By Lemma A.1 below, we have

$\mathcal{F}^{\beta}(\bot_{{T}})\sim_{T}\mathcal{G}^{\beta}(\bot_{{T}})$

as required.

  * •

Case $\varphi=\nu X.\varphi^{\prime}$. Similar to the case for $\varphi=\mu
X.\varphi^{\prime}$ above.

###  A.2. Proof of Lemma 5.15

The proof proceeds by induction on the derivation for
$\mathcal{K};\Delta\vdash_{M}\phi:\kappa$, with case analysis on the last rule
used.

  * •

Cases for T-WeakTU and T-Weak: Trivial by the induction hypothesis.

  * •

Cases for T-AP and T-Var: Since $\llbracket\lambda\Delta.\phi\rrbracket(\rho)$
does not depend on $\rho$, we have
$\llbracket\lambda\Delta.\phi\rrbracket(\rho)=\llbracket\lambda\Delta.\phi\rrbracket(\rho^{\prime})$.

  * •

Case for T-FVar: In this case, $\Delta=\emptyset$ and $\phi=X$. We have

$\llbracket\lambda\Delta.\phi\rrbracket(\rho)=\rho(X)\precsim_{\Delta\to\kappa}\rho^{\prime}(X)=\llbracket\lambda\Delta.\phi\rrbracket(\rho^{\prime}),$

as required.

  * •

Case for T-Mu: In this case, $\Delta=\emptyset$ and $\phi=\mu
X.\phi^{\prime}$, with
$\mathcal{K},X\mathbin{:}\kappa;\emptyset\vdash_{M}\phi^{\prime}:\kappa$,
where $\kappa$ is of the form $\cdots\to\mathit{Prop}^{T,\emptyset}$. Let
$h_{0}=\lambda x.\llbracket\phi\rrbracket{\rho\\{X\mapsto x\\}}$ and
$h_{1}=\lambda x.\llbracket\phi^{\prime}\rrbracket{\rho^{\prime}\\{X\mapsto
x\\}}$. By the induction hypothesis, $x_{0}\preceq_{\kappa}x_{1}$ implies
$h_{0}\,x_{0}\preceq_{\kappa}h_{1}\,x_{1}$. Thus, by Lemma 5.13, we have

$\llbracket\lambda\Delta.\phi\rrbracket(\rho)=\mathit{LFP}(h_{0})\precsim_{\kappa}\mathit{LFP}(h_{1})=\llbracket\lambda\Delta.\phi\rrbracket(\rho^{\prime}),$

as required.

  * •

Case for T-Nu: Similar to the case for T-Mu above.

  * •

Case for T-Abs: In this case, $\phi=\lambda X.\phi^{\prime}$. The result
follows immediately from the induction hypothesis, as $\lambda\Delta.\lambda
X.\phi^{\prime}=\lambda(\Delta,X\mathbin{:}\mathit{Prop}^{T,U}).\phi^{\prime}$.

  * •

Case for T-App: In this case, $\phi=\phi_{1}\phi_{2}$. By the induction
hypothesis, we have:
$\llbracket\lambda\Delta.\phi_{1}\rrbracket(\rho)\precsim_{\Delta\to\mathit{Prop}^{T,U}\to\kappa}\llbracket\lambda\Delta.\phi_{1}\rrbracket(\rho^{\prime})$
and
$\llbracket\lambda\Delta.\phi_{2}\rrbracket(\rho)\precsim_{\Delta\to\mathit{Prop}^{T,U}}\llbracket\lambda\Delta.\phi_{2}\rrbracket(\rho^{\prime})$.
Suppose
$\Delta=X_{1}\mathbin{:}\mathit{Prop}^{T_{1},U_{1}},\ldots,X_{k}\mathbin{:}\mathit{Prop}^{T_{k},U_{k}}$
and let $x_{i}\in\llbracket\mathit{Prop}^{T_{i},U_{i}}\rrbracket$ for each
$i\in\\{1,\ldots,k\\}$. Then, we have:

$\begin{array}[]{rl}\llbracket\lambda\Delta.\phi\rrbracket(\rho)\\\ =&\lambda
x_{1}\in\llbracket\mathit{Prop}\rrbracket.\cdots\lambda
x_{k}\in\llbracket\mathit{Prop}\rrbracket.\llbracket\phi\rrbracket{\rho\\{X_{1}\mapsto
x_{1},\ldots,X_{k}\mapsto x_{k}\\}}\\\ =&\lambda
x_{1}\in\llbracket\mathit{Prop}\rrbracket.\cdots\lambda
x_{k}\in\llbracket\mathit{Prop}\rrbracket.(\llbracket\lambda\Delta.\phi_{1}\rrbracket{\rho}\,x_{1}\,\cdots,x_{k})(\llbracket\lambda\Delta.\phi_{2}\rrbracket{\rho}\,x_{1}\,\cdots,x_{k})\\\
\precsim_{\Delta\to\kappa}&\lambda
x_{1}\in\llbracket\mathit{Prop}\rrbracket.\cdots\lambda
x_{k}\in\llbracket\mathit{Prop}\rrbracket.(\llbracket\lambda\Delta.\phi_{1}\rrbracket{\rho^{\prime}}\,x_{1}\,\cdots,x_{k})(\llbracket\lambda\Delta.\phi_{2}\rrbracket{\rho^{\prime}}\,x_{1}\,\cdots,x_{k})\\\
=&\llbracket\lambda\Delta.\phi\rrbracket(\rho^{\prime})\end{array}$

as required.

  * •

The remaining cases follow immediately from the induction hypothesis.