Hugo Herbelin and Arnaud Spiwack Billy Editor, Bill Editors2Conference title
on which this volume is based on111 10.4230/LIPIcs.xxx.yyy.p

# The Rooster and the Syntactic Bracket111This research has received funding
from the European Research Council under the FP7 grant agreement 278673,
Project MemCAD

Hugo Herbelin  Inria Paris-Rocquencourt
Paris, France
<EMAIL_ADDRESS>Arnaud Spiwack  Inria Paris-Rocquencourt
Paris, France
<EMAIL_ADDRESS>
###### Abstract.

We propose an extension of pure type systems with an algebraic presentation of
inductive and co-inductive type families with proper indices. This type theory
supports coercions toward from smaller sorts to bigger sorts via explicit type
construction, as well as impredicative sorts. Type families in impredicative
sorts are constructed with a bracketing operation. The necessary restrictions
of pattern-matching from impredicative sorts to types are confined to the
bracketing construct. This type theory gives an alternative presentation to
the calculus of inductive constructions on which the Coq proof assistant is an
implementation.

###### Key words and phrases:

Coq, Calculus of inductive constructions, Impredicativity, Strictly positive
type families, Inductive type families

###### 1991 Mathematics Subject Classification:

F.3.3 Studies of Program Constructs

##  1\. Introduction

In the Coq proof assistant [14] inductive types are treated as toplevel
definitions. If it makes sense from a convenience or an efficiency point of
view, the monolithic nature of the definitions make it hard to describe what
they precisely mean. As a matter of fact, inductive definitions mean different
things depending on the type they are defined in: specifically, some types are
interpreted differently in impredicative sorts like Prop or the impredicative
variant of Set.

In this article, we present a calculus of inductive and co-inductive
constructions where inductive and co-inductive types are presented
algebraically. The algebraic presentation is an extension of a PTS [3] with
inductive and co-inductive type families. Thanks to its modularity, it is
meant to serve as a description which is simpler to expose and more
mathematically amenable than the monolithic scheme which is found in a
practical system such as Coq. For the sake of clarity, the system is given
with a single universe and explicit subtyping, although Coq has an unbounded
cumulative hierarchy of universes and implicit subtyping. Apart from these
technicalities, it is believed that our calculus of algebraic inductive and
co-inductive constructions expresses all the features of the Set-impredicative
Calculus of Inductive Constructions that Coq implements, _e.g._ in its version
8.4 when launched with option -impredicative-set.

This work draws most of its inspiration from Morris & al [9, 10] for the
algebraic presentation of inductive type families in a predicative sort, and
Awodey & Bauer [2] for the treatment of impredicative sorts.

We use examples from Coq to illustrate the algebraic presentation. To
differentiate expressions in Coq from expressions in the algebraic
presentation, the former are typeset in a sans-serif font and the latter in a
roman font.

##  2\. Pure type systems

To model the type system of Coq, we start with the classic presentation of
pure type systems (pts) of Barendregt [3], which we will then extend to model
type families. A pts is characterised by a _single_ syntactic category of
terms which are used both as ${\lambda}$-terms and as types. It has a single
form of typing judgment $\Gamma\vdash u:A$, where $u$ and $A$ are terms, and
$\Gamma$ a context assigning terms to variables. A pts has a set of _sorts_ ,
which we shall denote schematically by the symbol $s$. Every sort is an atomic
term. A pts has a conversion relation $u\equiv v$. Here we diverge from the
presentation of [3] which always uses ${\beta}$-conversion. Coq, on the other
hand, uses ${\beta}$${\eta}$-conversion on the fragment described in this
section. In this article we will take the conversion rule as abstract, not
even requiring it to be decidable. We will only require that it contains all
the reduction rules which are given in the form $u\leadsto v$ (in this
section, we only have ${\beta}$-reduction).

$\Gamma,x{:}A\vdash x:A\lx@proof@logical@and\Gamma\vdash A:sx\mbox{{ is fresh
in }}\Gamma$ $\Gamma,x{:}B\vdash u:A\lx@proof@logical@and\Gamma\vdash
u:A\Gamma\vdash B:sx\mbox{{ is fresh in }}\Gamma$
$\Gamma\vdash\lambda{x}^{A}.\,u:\prod_{x{:}A}B\lx@proof@logical@and\Gamma\vdash\prod_{x{:}A}B:s\Gamma,x{:}A\vdash
u:B$
$\Gamma\vdash{u}\,{v}:{B}{\left[\,x\,{\setminus}\,v\,\right]}\lx@proof@logical@and\Gamma\vdash
u:\prod_{x{:}A}B\Gamma\vdash v:A$
$\Gamma\vdash u:B\lx@proof@logical@and\Gamma\vdash u:A\Gamma\vdash B:sA\equiv
B$
${\left(\lambda{x}^{A}.\,u\right)}\,{v}\leadsto{u}{\left[\,x\,{\setminus}\,v\,\right]}$

Figure 1. Generic rules of pts

The typing rules of a pts comprise of a set of generic rules given in Figure
1, together with a number of rules of the form

$\vdash{s}_{1}:{s}_{2}$

called axioms, and rules of the form

$\Gamma\vdash\prod_{x{:}A}B:{s}_{3}\lx@proof@logical@and\Gamma\vdash
A:{s}_{1}\Gamma,x{:}A\vdash B:{s}_{2}$

of product formation rules. As usual we write $A\rightarrow B$ for
$\prod_{x{:}A}B$ when $x$ does not bind a variable in $B$.

As a starting point of the algebraic presentation, we shall use a pts with two
sorts, $\mathrm{Type}$ and $\Box$, together with the following axiom:

$\Gamma\vdash\mathrm{Type}:\Box$

and the following product formation rule:

$\Gamma\vdash\prod_{x{:}A}B:{\mathrm{max}}\,{{s}_{1}}\,{{s}_{2}}\lx@proof@logical@and\Gamma\vdash
A:{s}_{1}\Gamma,x{:}A\vdash B:{s}_{2}$

where ${\mathrm{max}}\,{s}\,{s}=s$ and
${\mathrm{max}}\,{\mathrm{Type}}\,{\Box}={\mathrm{max}}\,{\Box}\,{\mathrm{Type}}=\Box$

The sorts $\mathrm{Type}$ and $\Box$ are predicative. The sort $\Box$ plays a
technical role in allowing type variable and the formation of type-level
functions; it cannot, however, be referenced in terms. In the following
sections, $\Box$ will also be used to be able to define types by pattern-
matching (_strong elimination_).

To model the entire Coq system, $\mathrm{Type}$ and $\Box$ would be replaced
with a hierarchy of predicative sorts ${\mathrm{Type}}_{i}$, such that

$\Gamma\vdash{\mathrm{Type}}_{i}:{\mathrm{Type}}_{i+1}$

are axioms. Adapting the presentation to a hierarchy of sorts is
straightforward, but in the interest of keeping to the heart of the matter we
give a presentation with two sorts.

##  3\. Inductive type families

We shall now extend the algebraic presentation with a notion of _inductive
type families_ to model (dependent) datatypes. In this section we will stay in
the predicative fragment of Coq.

Contrary to the inductive types of Coq, where inductive definitions must be
_named_ at _toplevel_ , like in:

Inductive Even : Type := ${\mid}$ eo : Even
${\mid}$ es : Odd ${\rightarrow}$ Even
with Odd : Type := ${\mid}$ os : Even ${\rightarrow}$ Odd.

the presentation given here is essentially anonymous, and inductive families
need not be defined at toplevel prior to use. Mutually inductive types such as
Even and Odd are not modelled directly, rather they are encoded using an
index:

Inductive EvenOdd : bool ${\rightarrow}$ Type := ${\mid}$ eo : EvenOdd true
${\mid}$ es : EvenOdd false ${\rightarrow}$ EvenOdd true
${\mid}$ os : EvenOdd true ${\rightarrow}$ EvenOdd false. Definition Even :=
EvenOdd true. Definition Odd := EvenOdd false.

This encoding works as long as all the mutual definitions are all in the same
sort. A variant for mutual definition involving Type and Prop is demonstrated
in Section 4.3. When the types being defined are in different predicative
sorts, however, we have to resort to another encoding which involves nested
datatypes [4, Section 8.6].

We will not explore the latter kind of mutual definition. However, nested
datatypes – where recursive calls occur as arguments of another type – such
as:

Inductive List (A:Type) : Type := ${\mid}$ nil : List A
${\mid}$ cons : A ${\rightarrow}$ List A ${\rightarrow}$ List A. Inductive
Tree : Type := ${\mid}$ node : List Tree ${\rightarrow}$ Tree.

are indeed modelled in the algebraic presentation.

###  3.1. Regular types

To be able to traverse terms of inductive type, the core pts constructions is
extended with a _recursive fixed point_ on functions:

$\Gamma\vdash\mathrm{fix}\leavevmode\nobreak\ f\leavevmode\nobreak\
{x}_{1}{:}{A}_{1}\leavevmode\nobreak\ \mbox{\ldots}\leavevmode\nobreak\
{x}_{n-1}{:}{A}_{n-1}\leavevmode\nobreak\ {x}_{n}{:}{A}_{n}\Rightarrow
u:\prod_{{x}_{1}{:}{A}_{1},\mbox{\ldots},{x}_{n-1}{:}{A}_{n-1},{x}_{n}{:}{A}_{n}}B\begin{array}[]{c}\eqmakebox[tag1]{$\Gamma\vdash\prod_{{x}_{1}{:}{A}_{1},\mbox{\ldots},{x}_{n-1}{:}{A}_{n-1},{x}_{n}{:}{A}_{n}}B
:
s$${\qquad}$${\mathrm{guarded}}\,{f}\,{{x}_{1}}\,{\mbox{\ldots}}\,{{x}_{n-1}}\,{{x}_{n}}\,{u}$}\\\
\eqmakebox[tag1]{$\Gamma,
f{:}\prod_{{x}_{1}{:}{A}_{1},\mbox{\ldots},{x}_{n-1}{:}{A}_{n-1},{x}_{n}{:}{A}_{n}}B,
{x}_{1}{:}{A}_{1}, \mbox{\ldots}, {x}_{n-1}{:}{A}_{n-1},
{x}_{n}{:}{A}_{n}\vdash u : B$}\\\ \end{array}$

Recursive fixed points are unfolded when fully applied

${\left(\mathrm{fix}\leavevmode\nobreak\ f\leavevmode\nobreak\
{x}_{1}{:}{A}_{1}\leavevmode\nobreak\ \mbox{\ldots}\leavevmode\nobreak\
{x}_{n}{:}{A}_{n}\Rightarrow
u\right)}\,{{v}_{1}}\,{\mbox{\ldots}}\,{{v}_{n}}\leadsto{u}{\left[\,{x}_{i}\,{\setminus}\,{v}_{i}\,\right]}$

To ensure strong normalisation, this reduction rule is limited, and a guard
condition is imposed on the recursive calls to $f$. It is not, however, the
object of this article to discuss these restriction or the guard condition.
Briefly, Coq currently relies on a single _structural_ argument in the block
${x}_{1}$, …, ${x}_{n}$: fixed points are not unfolded until their structural
argument starts with a constructor, and the guard condition ensures that each
recursive call is performed on a subterm of said structural argument, for a
relaxed notion of subterm. Other possibilities exist: Agda2 [11] uses any
number of arguments as structural, and tries to find a lexicographic ordering.
Yet another possibilities is to use sized types [1]. We shall simply assume
that an adequate guard condition is given.

We now extend the grammar of type constructors. The presentation of this
article is largely inspired by the synthetic definition of _strictly positive
families_ by Morris & al [9, 10], but is adapted to _intensional type theory_.
The presentation of [9, 10] is designed for generic programming inside a type
theory, they give codes for strictly positive families which are then decoded
into an actual type of the ambient theory. No elimination principle needs to
be given for the strictly positive families, as they are implicit in their
decoding. Here, we are defining the syntax of inductive type families,
including their elimination rules.

Sum type
$\Gamma\vdash A+B:\mathrm{Type}\lx@proof@logical@and\Gamma\vdash
A:\mathrm{Type}\Gamma\vdash B:\mathrm{Type}$
$\Gamma\vdash{\mathrm{inl}}\,{t}:A+B\lx@proof@logical@and\Gamma\vdash
A+B:s\Gamma\vdash t:A$
$\Gamma\vdash{\mathrm{inr}}\,{u}:A+B\lx@proof@logical@and\Gamma\vdash
A+B:s\Gamma\vdash u:B$
$\Gamma\vdash\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
u\leavevmode\nobreak\ \mathrm{as}\leavevmode\nobreak\ x\leavevmode\nobreak\
\mathrm{return}\leavevmode\nobreak\ P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\mathrm{inl}}\,{y}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &v\\\
{\mathrm{inr}}\,{z}\hfil\leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\
&w\\\ \end{array}\\\
\end{array}:{P}{\left[\,x\,{\setminus}\,u\,\right]}\lx@proof@logical@and\Gamma\vdash
u:A+B\Gamma,x{:}A+B\vdash P:s\Gamma,y{:}A\vdash
v:{P}{\left[\,x\,{\setminus}\,{\mathrm{inl}}\,{y}\,\right]}\Gamma,z{:}A\vdash
w:{P}{\left[\,x\,{\setminus}\,{\mathrm{inr}}\,{z}\,\right]}$
$\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
{\mathrm{inl}}\,{u}\leavevmode\nobreak\ \mathrm{as}\leavevmode\nobreak\
x\leavevmode\nobreak\ \mathrm{return}\leavevmode\nobreak\
P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\mathrm{inl}}\,{y}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &v\\\
{\mathrm{inr}}\,{z}\hfil\leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\
&w\\\ \end{array}\\\
\end{array}\leadsto{v}{\left[\,y\,{\setminus}\,u\,\right]}$
$\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
{\mathrm{inr}}\,{u}\leavevmode\nobreak\ \mathrm{as}\leavevmode\nobreak\
x\leavevmode\nobreak\ \mathrm{return}\leavevmode\nobreak\
P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\mathrm{inl}}\,{y}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &v\\\
{\mathrm{inr}}\,{z}\hfil\leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\
&w\\\ \end{array}\\\
\end{array}\leadsto{w}{\left[\,z\,{\setminus}\,u\,\right]}$
Unit type
$\Gamma\vdash 1:\mathrm{Type}$ $\Gamma\vdash():1$
$\Gamma\vdash\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
u\leavevmode\nobreak\ \mathrm{as}\leavevmode\nobreak\ x\leavevmode\nobreak\
\mathrm{return}\leavevmode\nobreak\ P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}()\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &v\\\ \end{array}\\\
\end{array}:{P}{\left[\,x\,{\setminus}\,u\,\right]}\lx@proof@logical@and\Gamma\vdash
u:1\Gamma,x{:}1\vdash P:s\Gamma\vdash
v:{P}{\left[\,x\,{\setminus}\,()\,\right]}$
$\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
()\leavevmode\nobreak\ \mathrm{as}\leavevmode\nobreak\ x\leavevmode\nobreak\
\mathrm{return}\leavevmode\nobreak\ P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}()\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &v\\\ \end{array}\\\ \end{array}\leadsto v$
Empty type
$\Gamma\vdash 0:\mathrm{Type}$ $\Gamma\vdash\mathrm{match}\leavevmode\nobreak\
u\leavevmode\nobreak\ \mathrm{return}\leavevmode\nobreak\
A\leavevmode\nobreak\ \mathrm{with}\leavevmode\nobreak\
\cdot:A\lx@proof@logical@and\Gamma\vdash u:0\Gamma\vdash A:\mathrm{Type}$

Figure 2. Regular type constructors

The regular type constructors, whose typing rules are given in Figure 2, are
the empty type $0$, the unit type $1$, and the sum of two types. The
elimination rules are given in the form of _dependent pattern-matching_ with a
syntax made to remind of that of Coq. We shall often omit the typing predicate
when it is clear from the context, especially when it does not depend on the
branch. With this material we can define a first example type, namely the
booleans:

$\left\\{\begin{aligned} \mathbb{B}&=1+1\\\
\mathrm{true}&={\mathrm{inl}}\,{()}\\\
\mathrm{false}&={\mathrm{inr}}\,{()}\end{aligned}\right.$

###  3.2. Inductive type families

Inductive families differ from regular inductive types in that they are
parametrised by _indices_ , that is they are functions
$F:A\rightarrow\mathrm{Type}$ for some $A$. An inductive family of the form
$\lambda{x}^{A}.\,R$, is said to be _uniformly parametrised_ by $A$. In
general, inductive families are not uniformly parametrised: the value of the
index is allowed to vary in recursive calls, and constructors may build values
of ${F}\,{x}$ for certain $x$ only. Remember, for instance, the EvenOdd
family:

Inductive EvenOdd : bool ${\rightarrow}$ Type := ${\mid}$ eo : EvenOdd true
${\mid}$ es : EvenOdd false ${\rightarrow}$ EvenOdd true
${\mid}$ os : EvenOdd true ${\rightarrow}$ EvenOdd false.

The inductive family constructors, presented in Figure 3, warrant individual
discussion. First, notice that as a simplifying hypothesis, inductive families
have exactly one index. This is, of course, not a limitation in expressive
power as multiple indices can be encoded as a dependent sum, and the unit type
allows us to write families without an index.

Inductive fixed point
$\Gamma\vdash\mu{X}^{A\rightarrow\mathrm{Type}}.\,F:A\rightarrow\mathrm{Type}\lx@proof@logical@and\Gamma\vdash
A:s\Gamma,X{:}A\rightarrow\mathrm{Type}\vdash
F:A\rightarrow\mathrm{Type}{{\mbox{{sp}}}_{X}}\,{F}$
$\mu{X}^{A\rightarrow
s}.\,F\equiv{F}{\left[\,X\,{\setminus}\,\mu{X}^{A\rightarrow s}.\,F\,\right]}$
Proper indices
$\Gamma\vdash{\sum}_{x{:}A}^{f}T:B\rightarrow\mathrm{Type}\lx@proof@logical@and\Gamma\vdash
A:\mathrm{Type}\Gamma\vdash B:\mathrm{Type}\Gamma,x{:}A\vdash
T:\mathrm{Type}\Gamma,x{:}A\vdash f:B$
$\Gamma\vdash{\left(u,v\right)}_{x{:}A.T}^{f}:{\left({\sum}_{x{:}A}^{f}T\right)}\,{\left({f}{\left[\,x\,{\setminus}\,u\,\right]}\right)}\lx@proof@logical@and\Gamma\vdash{\sum}_{x{:}A}^{f}T:B\rightarrow
s\Gamma\vdash u:A\Gamma\vdash v:{T}{\left[\,x\,{\setminus}\,u\,\right]}$
$\Gamma\vdash\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
u\leavevmode\nobreak\ \mathrm{as}\leavevmode\nobreak\ z\leavevmode\nobreak\
\mathrm{in}\leavevmode\nobreak\ y\leavevmode\nobreak\
\mathrm{return}\leavevmode\nobreak\ P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\left(i,j\right)}_{x{:}A.T}^{f}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &v\\\ \end{array}\\\
\end{array}:{P}{\left[\,y\,{\setminus}\,b\,,\,z\,{\setminus}\,u\,\right]}\begin{array}[]{c}\eqmakebox[tag2]{$\Gamma\vdash
u : {\left( {\sum}_{x{:}A}^{f}T\right) }\,{b}$${\qquad}$$\Gamma, y{:}B,
z{:}{\left( {\sum}_{x{:}A}^{f}T\right) }\,{y}\vdash P : s$}\\\
\eqmakebox[tag2]{$\Gamma, i{:}A, j{:}{T}\,{i}\vdash v : {P}{\left[
\,y\,{\setminus}\,{f}\,{i}\,,\,z\,{\setminus}\,{\left( i, j\right)
}_{x{:}A.T}^{f}\,\right] }$}\\\ \end{array}$
$\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
{\left(u,v\right)}_{x{:}A.T}^{f}\leavevmode\nobreak\
\mathrm{as}\leavevmode\nobreak\ z\leavevmode\nobreak\
\mathrm{in}\leavevmode\nobreak\ y\leavevmode\nobreak\
\mathrm{return}\leavevmode\nobreak\ P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\left(i,j\right)}_{x{:}A.T}^{f}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &w\\\ \end{array}\\\
\end{array}\leadsto{w}{\left[\,i\,{\setminus}\,u\,,\,j\,{\setminus}\,v\,\right]}$

Figure 3. Inductive type families

${{\mbox{{sp}}}_{X}}\,{y}$ ${{\mbox{{sp}}}_{X}}\,{0}$
${{\mbox{{sp}}}_{X}}\,{1}$
${{\mbox{{sp}}}_{X}}\,{\left(\prod_{x{:}A}B\right)}\lx@proof@logical@and
X\mbox{{ is fresh in }}A{{\mbox{{sp}}}_{X}}\,{B}$
${{\mbox{{sp}}}_{X}}\,{\left(A+B\right)}\lx@proof@logical@and{{\mbox{{sp}}}_{X}}\,{A}{{\mbox{{sp}}}_{X}}\,{B}$
${{\mbox{{sp}}}_{X}}\,{\left(\mu{Y}^{A}.\,F\right)}\lx@proof@logical@and
X\mbox{{ is fresh in }}A{{\mbox{{sp}}}_{X}}\,{F}$
${{\mbox{{sp}}}_{X}}\,{\left(\lambda{x}^{A}.\,T\right)}\lx@proof@logical@and
X\mbox{{ is fresh in }}A{{\mbox{{sp}}}_{X}}\,{T}$
${{\mbox{{sp}}}_{X}}\,{\left({U}\,{t}\right)}\lx@proof@logical@and{{\mbox{{sp}}}_{X}}\,{U}X\mbox{{
is fresh in }}t$
${{\mbox{{sp}}}_{X}}\,{A}\lx@proof@logical@and{{\mbox{{sp}}}_{X}}\,{B}B\equiv
A$
${{\mbox{{sp}}}_{X}}\,{\left({\sum}_{x{:}A}^{f}T\right)}\lx@proof@logical@and
X\mbox{{ is fresh in }}f{{\mbox{{sp}}}_{X}}\,{A}{{\mbox{{sp}}}_{X}}\,{T}$

Figure 4. Strict positivity condition

The construction $\mu{X}^{A\rightarrow\mathrm{Type}}.\,F$ constructs the
_inductive fixed point_ of $F$. It acts on type families, because indices vary
through recursive calls to $X$. To be able to form an inductive fixed point,
occurrences of $X$ must be strictly positive in $F$, rules for strict
positivity are given in Figure 4. The rules of Figure 4 are a simple set which
suits the needs of this article, however in practice, we may want to consider
strict positivity rules involving elimination rules and a finer treatment of
application. Strict positivity ensures that no non-terminating term can be
written without recursive fixed points, so that the guard condition suffices
to enforce termination. Paradoxes which can be derived from non-positive or
non-strictly positive inductive fixed points can be found in [13, Chapter 4,
Section 4.2][8, Chapter 3][4, Chapter 8]. To avoid clutter, we give a
presentation where inductive fixed points can be freely rolled and unrolled
thanks to the conversion. An alternative can be to give an explicit term
constructor for fixed points, see Section 3.4.

We will also use an inductive fixed point on nullary families, defined as:

$\displaystyle\mu{X}^{\mathrm{Type}}.\,F$
$\displaystyle={\left(\mu{Y}^{1\rightarrow\mathrm{Type}}.\,{F}{\left[\,X\,{\setminus}\,{Y}\,{()}\,\right]}\right)}\,{()}$

from which we have that $\mu{X}^{\mathrm{Type}}.\,F$ can be freely rolled from
or unrolled to
${F}{\left[\,X\,{\setminus}\,\mu{X}^{\mathrm{Type}}.\,F\,\right]}$.

With inductive fixed points, we can, for instance, define the accessibility
predicate. In Coq:

Inductive Acc (A:Type) (R:A${\rightarrow}$A${\rightarrow}$Type) (x:A) : Type
:= ${\mid}$ acc_intro : (forall y:A, R y x ${\rightarrow}$ Acc A R y)
${\rightarrow}$ Acc A R x.

This type represents the generic form of termination proofs: any terminating
recursive fixed point can be made structural over a proof of accessibility. In
the algebraic presentation, it is defined as:

$\left\\{\begin{aligned}
\mathrm{Acc}&=\lambda{A}^{\mathrm{Type}}\,{R}^{A\rightarrow
A\rightarrow\mathrm{Type}}.\,\mu{\mathrm{Acc}}^{A\rightarrow\mathrm{Type}}.\,\lambda{x}^{A}.\,\prod_{y{:}A}{R}\,{y}\,{x}\rightarrow{\mathrm{Acc}}\,{y}\\\
{\mathrm{acc}}_{\mathrm{intro}}&=\lambda{A}^{\mathrm{Type}}\,{R}^{A\rightarrow
A\rightarrow\mathrm{Type}}\,{x}^{A}\,{f}^{\prod_{y{:}A}{R}\,{y}\,{x}\rightarrow{\mathrm{Acc}}\,{A}\,{R}\,{y}}.\,f\end{aligned}\right.$

Because inductive fixed points are treated transparently, the constructor is
rather trivial. However, notice how, in the definition of $\mathrm{Acc}$, the
parameter $x$ is treated differently from $A$ and $R$. The reason is that $A$
and $R$ are _uniform parameters_ , in that they do not vary through recursive
calls, whereas $x$ does: it is a _non-uniform parameter_. The parameter $x$
is, hence, represented as an index. However, such an index is not sufficient
to encode types like EvenOdd.

Representing proper indices requires a new type construction, which we write
${\sum}_{x{:}A}^{f}T$. This construction comes from [9, 10], where it is
inspired by a categorical point of view: in a sufficiently extensional
setting, ${\sum}_{x{:}A}^{f}T$ is the right adjoint to a pullback functor. The
similarity with the usual notation of dependent sum is not fortuitous, indeed
we can define dependent sum as a special case of proper indexing:

$\left\\{\begin{aligned}
\sum_{x{:}A}B&={\left({\sum}_{x{:}A}^{()}B\right)}\,{()}\\\
{\left(u,v\right)}_{{\mbox{\scriptsize{$x${:}$A$.$B$}}}}&={\left(u,v\right)}_{x{:}A.B}^{()}\end{aligned}\right.$

We also write $A\times B$ and $\left(u,v\right)$ for $\sum_{x{:}A}B$ and
${\left(u,v\right)}_{{\mbox{\scriptsize{$x${:}$A$.$B$}}}}$, respectively, when
$x$ is not free in $B$.

In the case of dependent sums, the index is trivial. When it is not, however,
the pattern matching return clause $P$ is allowed to depend on the value of
the index. This is the purpose of Coq’s in-pattern. With the algebraic
presentation, the in-pattern has the pleasant property of being confined to
the proper indexing construction, hopefully making its meaning more explicit.
The syntax differs a little from that of Coq, however: Coq renders the in
clause as a pattern with the type name at the head:

match n as n’ in EvenOdd b return P n’ b with
… end.

In the algebraic presentation, types not having a name, the in clause simply
consists of a name for the index.

The prototype of proper indexing is the identity type, which we name
$\mathrm{Eq}$. In Coq:

Inductive Eq (A:Type) (x:A) : A ${\rightarrow}$ Type := ${\mid}$ eq_refl : Eq
A x x

in the algebraic presentation:

$\left\\{\begin{aligned}
\mathrm{Eq}&=\lambda{A}^{\mathrm{Type}}\,{x}^{A}.\,{\sum}_{\\_{:}1}^{x}1\\\
{\mathrm{eq}}_{\mathrm{refl}}&=\lambda{A}^{\mathrm{Type}}\,{x}^{A}.\,{\left((),()\right)}_{\\_{:}1.1}^{x}\end{aligned}\right.$

In fact, dependent sums and identity types are sufficient to define proper
indexing. Indeed ${\sum}_{x{:}A}^{f}T$ can be redefined as:

$\left\\{\begin{aligned}
{\sum}_{x{:}A}^{f}T&=\lambda{y}^{B}.\,\sum_{x{:}A}\left({\mathrm{Eq}}\,{B}\,{y}\,{f}\right)\times
T\\\
{\left(u,v\right)}_{x{:}A.T}^{f}&={\left(u,\left({{\mathrm{eq}}_{\mathrm{refl}}}\,{B}\,{{f}{\left[\,x\,{\setminus}\,u\,\right]}},v\right)\right)}_{{\mbox{\scriptsize{$x${:}$A$.$\left({\mathrm{Eq}}\,{B}\,{\left({f}{\left[\,x\,{\setminus}\,u\,\right]}\right)}\,{f}\right)$${\times}$$T$}}}}\end{aligned}\right.$

It is closer to the spirit of Coq, but in no way essential, to take a proper
indexing construction rather than equality as primitive. In Morris & al [9,
10], the dependent sum and equality of the ambient type theory is used to
define ${\sum}_{x{:}A}^{f}T$ which is then taken as primitive.

An other choice lies in the use of $A+B$ as primitive. It is the only type
construction which allows to define a type with distinct elements. However, a
common alternative is to take $\mathbb{B}$ as primitive, in which case we can
define $A+B$ as:

$\left\\{\begin{aligned}
A+B&=\sum_{b{:}\mathbb{B}}\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
b\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}\mathrm{true}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &A\\\ \mathrm{false}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &B\\\ \end{array}\\\ \end{array}\\\
\mathrm{inl}&=\lambda{x}^{A}.\,{\left(\mathrm{true},x\right)}_{{\mbox{\scriptsize{$b${:}$\mathbb{B}$.$\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
b\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}\mathrm{true}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &A\\\ \mathrm{false}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &B\\\ \end{array}\\\ \end{array}$}}}}\\\
\mathrm{inr}&=\lambda{y}^{B}.\,{\left(\mathrm{false},y\right)}_{{\mbox{\scriptsize{$b${:}$\mathbb{B}$.$\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
b\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}\mathrm{true}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &A\\\ \mathrm{false}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &B\\\ \end{array}\\\
\end{array}$}}}}\end{aligned}\right.$

###  3.3. Examples

The previous section concludes the description of the predicative fragment of
the algebraic presentation. We can now give definitions of the remaining
inductive families we have encountered in terms of the algebraic presentation.
Starting with EvenOdd:

Inductive EvenOdd : bool ${\rightarrow}$ Type := ${\mid}$ eo : EvenOdd true
${\mid}$ es : EvenOdd false ${\rightarrow}$ EvenOdd true
${\mid}$ os : EvenOdd true ${\rightarrow}$ EvenOdd false.

translates, in the algebraic presentation, to:

$\left\\{\begin{aligned}
\mathrm{EvenOdd}&=\mu{\mathrm{EvenOdd}}^{\mathbb{B}\rightarrow\mathrm{Type}}.\,\left({\sum}_{\\_{:}1}^{\mathrm{true}}1+{\mathrm{EvenOdd}}\,{\mathrm{false}}\right)+\left({\sum}_{\\_{:}1}^{\mathrm{false}}{\mathrm{EvenOdd}}\,{\mathrm{true}}\right)\\\
\mathrm{eo}&={\mathrm{inl}}\,{{\left((),{\mathrm{inl}}\,{()}\right)}_{\\_{:}1.1}^{\mathrm{true}}}\\\
\mathrm{es}&=\lambda{x}^{{\mathrm{EvenOdd}}\,{\mathrm{false}}}.\,{\mathrm{inl}}\,{{\left((),{\mathrm{inr}}\,{x}\right)}_{\\_{:}1.1}^{\mathrm{true}}}\\\
\mathrm{os}&=\lambda{x}^{{\mathrm{EvenOdd}}\,{\mathrm{true}}}.\,{\mathrm{inr}}\,{{\left((),x\right)}_{\\_{:}1.1}^{\mathrm{false}}}\end{aligned}\right.$

Here is the definition of List in Coq:

Inductive List (A:Type) : Type := ${\mid}$ nil : List A
${\mid}$ cons : A ${\rightarrow}$ List A ${\rightarrow}$ List A.

and in the algebraic presentation:

$\left\\{\begin{aligned}
\mathrm{List}&=\lambda{A}^{\mathrm{Type}}.\,\mu{\mathrm{List}}^{\mathrm{Type}}.\,1+A\times\mathrm{List}\\\
\mathrm{nil}&=\lambda{A}^{\mathrm{Type}}.\,{\mathrm{inl}}\,{()}\\\
\mathrm{cons}&=\lambda{A}^{\mathrm{Type}}\,{x}^{A}\,{l}^{{\mathrm{List}}\,{A}}.\,{\mathrm{inr}}\,{\left(x,l\right)}\end{aligned}\right.$

Finally the definition of Tree:

Inductive Tree : Type := ${\mid}$ node : List Tree ${\rightarrow}$ Tree.

translates to:

$\left\\{\begin{aligned}
\mathrm{Tree}&=\mu{\mathrm{Tree}}^{\mathrm{Type}}.\,{\mathrm{List}}\,{\mathrm{Tree}}\\\
\mathrm{node}&=\lambda{f}^{{\mathrm{List}}\,{\mathrm{Tree}}}.\,f\end{aligned}\right.$

Note that in the definition of $\mathrm{Tree}$, we must ${\beta}$-reduce
${\mathrm{List}}\,{\mathrm{Tree}}$ for the recursive definition to be strictly
positive.

A more complex example is given by the type of lists indexed by their length,
often called _vectors_ :

Inductive Nat : Type := ${\mid}$ o : Nat
${\mid}$ s : Nat ${\rightarrow}$ Nat. Inductive Vector (A:Type) : Nat
${\rightarrow}$ Type := ${\mid}$ vnil : Vector A o
${\mid}$ vcons : forall n, A ${\rightarrow}$ Vector A n ${\rightarrow}$ Vector
A (s n).

It is encoded in the algebraic presentation as:

$\left\\{\begin{aligned}
\mathrm{Nat}&=\mu{\mathrm{Nat}}^{\mathrm{Type}}.\,1+\mathrm{Nat}\\\
o&={\mathrm{inl}}\,{()}\\\
s&=\lambda{n}^{\mathrm{Nat}}.\,{\mathrm{inr}}\,{n}\\\
\mathrm{Vector}&=\lambda{A}^{\mathrm{Type}}.\,\mu{V}^{\mathrm{Nat}\rightarrow\mathrm{Type}}.\,\lambda{n}^{\mathrm{Nat}}.\,{\left({\sum}_{\\_{:}1}^{o}1\right)}\,{n}+{\left({\sum}_{n^{\prime}{:}\mathrm{Nat}}^{{s}\,{n^{\prime}}}A\times{V}\,{n^{\prime}}\right)}\,{n}\\\
\mathrm{vnil}&=\lambda{A}^{\mathrm{Type}}.\,{\mathrm{inl}}\,{{\left((),()\right)}_{\\_{:}1.1}^{o}}\\\
\mathrm{vcons}&=\lambda{A}^{\mathrm{Type}}\,{n}^{\mathrm{Nat}}\,{a}^{A}\,{v}^{{\mathrm{Vector}}\,{n}\,{a}}.\,{\mathrm{inr}}\,{{\left(n,\left(a,v\right)\right)}_{n^{\prime}{:}\mathrm{Nat}.A\times{V}\,{n^{\prime}}}^{{s}\,{n^{\prime}}}}\end{aligned}\right.$

Contrary to proper indices, the types of non-uniform parameters are allowed to
be in $\Box$, this allows the definition of types such as the binary lists
[12]:

Inductive BList (A:Type) : Type := ${\mid}$ one : A ${\rightarrow}$ BList A
${\mid}$ twice : BList (A$*$A) ${\rightarrow}$ BList A
${\mid}$ stwice : A ${\rightarrow}$ BList (A$*$A) ${\rightarrow}$ BList A

which are rendered in the algebraic presentation as:

$\left\\{\begin{aligned}
\mathrm{BList}&=\mu{\mathrm{BList}}^{\mathrm{Type}\rightarrow\mathrm{Type}}.\,\lambda{A}^{\mathrm{Type}}.\,A+\left({\mathrm{BList}}\,{\left(A\times
A\right)}+A\times\left({\mathrm{BList}}\,{\left(A\times
A\right)}\right)\right)\\\
\mathrm{one}&=\lambda{A}^{\mathrm{Type}}\,{x}^{A}.\,{\mathrm{inl}}\,{x}\\\
\mathrm{twice}&=\lambda{A}^{\mathrm{Type}}\,{l}^{{\mathrm{BList}}\,{\left(A\times
A\right)}}.\,{\mathrm{inr}}\,{\left({\mathrm{inl}}\,{l}\right)}\\\
\mathrm{stwice}&=\lambda{A}^{\mathrm{Type}}\,{x}^{A}\,{l}^{{\mathrm{BList}}\,{\left(A\times
A\right)}}.\,{\mathrm{inr}}\,{\left({\mathrm{inr}}\,{\left(a,l\right)}\right)}\end{aligned}\right.$

In Coq, where there is a hierarchy of universe, types of proper indices can be
in any sort. However, a proper index whose type is in ${\mathrm{Type}}_{i}$
constrains the final type to be in ${\mathrm{Type}}_{i+1}$ or higher. Uniform
parameters, of any type, do not constrain the type they parametrise.

Inductive types are consumed by recursive fixed points. Using the implicit
unfolding of inductive fixed points, we can pattern-match over the top
constructor directly. The Coq function

Fixpoint add (x y:Nat) : Nat := match y with
${\mid}$ o ${\Rightarrow}$ x
${\mid}$ s y’ ${\Rightarrow}$ s (add x y’) end

is rendered in the algebraic presentation as

$\displaystyle\mathrm{add}$ $\displaystyle=\mathrm{fix}\leavevmode\nobreak\
\mathrm{add}\leavevmode\nobreak\ x{:}\mathrm{Nat}\leavevmode\nobreak\
y{:}\mathrm{Nat}\Rightarrow\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
y\leavevmode\nobreak\ \mathrm{as}\leavevmode\nobreak\ \\_\leavevmode\nobreak\
\mathrm{return}\leavevmode\nobreak\ \mathrm{Nat}\leavevmode\nobreak\
\mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\mathrm{inl}}\,{\\_}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &x\\\
{\mathrm{inr}}\,{y^{\prime}}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\
&{s}\,{\left({\mathrm{add}}\,{x}\,{y^{\prime}}\right)}\\\ \end{array}\\\
\end{array}$

###  3.4. Co-induction

In addition to inductive fixed points, Coq also has support for co-inductive
fixed points. Co-inductive fixed points are required to be strictly positive,
like inductive fixed points. We choose in this section, a presentation of co-
inductive data where fixed points are explicitly introduced with a
constructor. Below we will use this explicit presentation to give a variation
on Coq’s co-inductive fixed points.

$\parbox{433.62pt}{ \begin{center} \makebox[433.62pt]{\parbox{433.62pt}{
\begin{center}
$\Gamma\vdash\nu{X}^{A\rightarrow\mathrm{Type}}.\,F:A\rightarrow\mathrm{Type}\lx@proof@logical@and\Gamma\vdash
A:s\Gamma,X{:}A\rightarrow\mathrm{Type}\vdash
F:A\rightarrow\mathrm{Type}{{\mbox{{sp}}}_{X}}\,{F}$ \end{center} }}\\\
\makebox[433.62pt]{\parbox{433.62pt}{ \begin{center}
$\Gamma\vdash{\mathrm{forced}}\,{u}:{\left(\nu{X}^{A\rightarrow
s}.\,F\right)}\,{i}\lx@proof@logical@and\Gamma\vdash\nu{X}^{A\rightarrow
s}.\,F:A\rightarrow s\Gamma\vdash i:A\Gamma\vdash
u:{{F}{\left[\,X\,{\setminus}\,\nu{X}^{A\rightarrow s}.\,F\,\right]}}\,{i}$
\end{center} }}\\\ \makebox[433.62pt]{\parbox{433.62pt}{ \begin{center}
$\Gamma\vdash\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
u\leavevmode\nobreak\ \mathrm{as}\leavevmode\nobreak\ x\leavevmode\nobreak\
\mathrm{return}\leavevmode\nobreak\ P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\mathrm{forced}}\,{y}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &v\\\ \end{array}\\\
\end{array}:{P}{\left[\,x\,{\setminus}\,u\,\right]}\begin{array}[]{c}\eqmakebox[tag3]{$\Gamma\vdash\nu{X}^{A\rightarrow
s}.\,F : A\rightarrow s$${\qquad}$$\Gamma\vdash i : A$${\qquad}$$\Gamma\vdash
u : {\left( \nu{X}^{A\rightarrow s}.\,F\right) }\,{i}$}\\\
\eqmakebox[tag3]{$\Gamma, x{:}{\left( \nu{X}^{A\rightarrow s}.\,F\right)
}\,{i}\vdash P : s'$${\qquad}$$\Gamma, y{:}{{F}{\left[
\,X\,{\setminus}\,\nu{X}^{A\rightarrow s}.\,F\,\right] }}\,{i}\vdash v :
{P}{\left[ \,x\,{\setminus}\,{\mathrm{forced}}\,{y}\,\right] }$}\\\
\end{array}$ \end{center} }}\\\ \makebox[433.62pt]{\parbox{433.62pt}{
\begin{center} $\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
{\mathrm{forced}}\,{u}\leavevmode\nobreak\ \mathrm{as}\leavevmode\nobreak\
x\leavevmode\nobreak\ \mathrm{return}\leavevmode\nobreak\
P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\mathrm{forced}}\,{y}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &v\\\ \end{array}\\\
\end{array}\leadsto{v}{\left[\,y\,{\setminus}\,u\,\right]}$ \end{center} }}\\\
\end{center} }$
$\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
{\mathrm{forced}}\,{u}\leavevmode\nobreak\ \mathrm{as}\leavevmode\nobreak\
x\leavevmode\nobreak\ \mathrm{return}\leavevmode\nobreak\
P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\mathrm{forced}}\,{y}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &v\\\ \end{array}\\\
\end{array}\leadsto{v}{\left[\,y\,{\setminus}\,u\,\right]}$

Just like inductive data is _destructed_ by a recursive fixed point operation,
co-inductive data is _constructed_ by a co-recursive fixed point operation,
allowing co-inductive data to be infinite. The guard condition on co-recursive
fixed points ensures that a finite number of unfolding will eventually produce
a forced value.

$\Gamma\vdash\mathrm{cofix}\leavevmode\nobreak\ f\leavevmode\nobreak\
{x}_{1}{:}{A}_{1}\leavevmode\nobreak\ \mbox{\ldots}\leavevmode\nobreak\
{x}_{n}{:}{A}_{n}\Rightarrow
u:\prod_{{x}_{1}{:}{A}_{1},\mbox{\ldots},{x}_{n}{:}{A}_{n}}{\left(\nu{X}^{A\rightarrow
s}.\,F\right)}\,{i}\begin{array}[]{c}\eqmakebox[tag4]{$\Gamma\vdash\prod_{{x}_{1}{:}{A}_{1},\mbox{\ldots},{x}_{n}{:}{A}_{n}}{\left(
\nu{X}^{A\rightarrow s}.\,F\right) }\,{i} :
s$${\qquad}$${\mathrm{coguarded}}\,{f}\,{{x}_{1}}\,{\mbox{\ldots}}\,{{x}_{n}}\,{u}$}\\\
\eqmakebox[tag4]{$\Gamma,
f{:}\prod_{{x}_{1}{:}{A}_{1},\mbox{\ldots},{x}_{n}{:}{A}_{n}}{\left(
\nu{X}^{A\rightarrow s}.\,F\right) }\,{i}, {x}_{1}{:}{A}_{1}, \mbox{\ldots},
{x}_{n}{:}{A}_{n}\vdash u : {\left( \nu{X}^{A\rightarrow s}.\,F\right)
}\,{i}$}\\\ \end{array}$

Co-recursive fixed-point are meant to represent infinite data: they cannot be
unfolded eagerly, lest they would fail to terminate. They are unfolded only
when they appear at the head of a pattern-matching expression:

$\begin{array}[]{ll}&\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
{\left(\mathrm{cofix}\leavevmode\nobreak\ f\leavevmode\nobreak\
{x}_{1}{:}{A}_{1}\leavevmode\nobreak\ \mbox{\ldots}\leavevmode\nobreak\
{x}_{n}{:}{A}_{n}\Rightarrow
u\right)}\,{{v}_{1}}\,{\mbox{\ldots}}\,{{v}_{n}}\leavevmode\nobreak\
\mathrm{as}\leavevmode\nobreak\ x\leavevmode\nobreak\
\mathrm{return}\leavevmode\nobreak\ P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\mathrm{forced}}\,{y}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &v\\\ \end{array}\\\ \end{array}\\\
\leadsto&\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
{u}{\left[\,f\,{\setminus}\,\left(\mathrm{cofix}\leavevmode\nobreak\
f\leavevmode\nobreak\ {x}_{1}{:}{A}_{1}\leavevmode\nobreak\
\mbox{\ldots}\leavevmode\nobreak\ {x}_{n}{:}{A}_{n}\Rightarrow
u\right)\,,\,{x}_{i}\,{\setminus}\,{v}_{i}\,\right]}\leavevmode\nobreak\
\mathrm{as}\leavevmode\nobreak\ x\leavevmode\nobreak\
\mathrm{return}\leavevmode\nobreak\ P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\mathrm{forced}}\,{y}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &v\\\ \end{array}\\\ \end{array}\\\
\end{array}$

The dependent elimination rule for co-inductive fixed points asserts, in
essence, that every co-inductive data is of the form ${\mathrm{forced}}\,{u}$.
Even though it would be fine for inductive fixed points – this is why we could
leave the unrolling to the conversion – this does not reflect well the
computational aspects of co-inductive data: suspended co-recursive fixed
points are values, and won’t be evaluated until the context demands it. The
fact that the elimination for co-inductive data claims that all values are
forced gives rise to undesirable behaviour.

Take for instance the following simple co-inductive type, and data:

$\left\\{\begin{aligned} T&=\nu X.\,X\\\ i&=\mathrm{cofix}\leavevmode\nobreak\
i\Rightarrow{\mathrm{forced}}\,{i}\end{aligned}\right.$

So that $i$ is effectively an infinite sequence of $\mathrm{forced}$. Using
the elimination principle above, it is possible to give a _closed_ proof that
${\mathrm{Eq}}\,{T}\,{i}\,{\left({\mathrm{forced}}\,{i}\right)}$:

$\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\ i\leavevmode\nobreak\
\mathrm{as}\leavevmode\nobreak\ x\leavevmode\nobreak\
\mathrm{return}\leavevmode\nobreak\
{\mathrm{Eq}}\,{T}\,{x}\,{\left({\mathrm{forced}}\,{\left(\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
x\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\mathrm{forced}}\,{y}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &y\\\ \end{array}\\\
\end{array}\right)}\right)}\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\mathrm{forced}}\,{y}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &{{\mathrm{eq}}_{\mathrm{refl}}}\,{T}\,{y}\\\
\end{array}\\\ \end{array}$

However, $i$ and $\left({\mathrm{forced}}\,{i}\right)$ are not convertible,
yet, as every closed proof of equality does, this proof reduces to
${\mathrm{eq}}_{\mathrm{refl}}$, hence should relate convertible terms. The
dependent elimination rule of co-inductive fixed points compromises the type
safety of the logic.

Coq uses the above dependent elimination rule for co-inductive fixed points.
It was a deliberate decision made for practical purposes. Nonetheless, one may
want to weaken it to avoid the incompatibility between equality and
conversion. To do so, it suffices to erase the dependency of the return
predicate over the matched term:

$\Gamma\vdash\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
u\leavevmode\nobreak\ \mathrm{return}\leavevmode\nobreak\
P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\mathrm{forced}}\,{y}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &v\\\ \end{array}\\\
\end{array}:P\lx@proof@logical@and\Gamma\vdash\nu{X}^{A\rightarrow
s}.\,F:A\rightarrow s\Gamma\vdash i:A\Gamma\vdash
u:{\left(\nu{X}^{A\rightarrow s}.\,F\right)}\,{i}\Gamma\vdash
P:s^{\prime}\Gamma\vdash v:P$

##  4\. Prop

With all the common baggage for predicative sorts set in place, we can add
impredicative sorts to the algebraic presentation. The main such sort in Coq
is the sort Prop of propositions. The design of Prop is guided by _proof
irrelevance_ : even if it is not actually provable in Coq, different proofs of
a proposition are thought of as being equal. This property is useful for
program extraction: only the _computationally relevant_ parts of a program
need to be executed to get the final result. In other words: propositions are
considered as _static_ data. It is why, with disjunction and existential
defined as:

Inductive Or (A B:Prop) : Prop := ${\mid}$ or_introl : A ${\rightarrow}$ A
${\lor}$ B
${\mid}$ or_intror : B ${\rightarrow}$ A ${\lor}$ B. Inductive Ex (A:Type)
(P:A${\rightarrow}$Prop) : Prop := ${\mid}$ ex_intro : forall x:A, P x
${\rightarrow}$ Ex A P.

the following terms are refused by type-checking:

match x with
${\mid}$ or_introl $\\_$ ${\Rightarrow}$ true
${\mid}$ or_intror $\\_$ ${\Rightarrow}$ false
end.

and

match x with
${\mid}$ ex_intro x $\\_$ ${\Rightarrow}$ x
end.

On the other hand, it is not the case of every inductive type defined in Prop,
that they cannot be eliminated into Type. Conjunction and falsity are two
counter-examples:

Inductive False : Prop := . Inductive And (A B:Prop) : Prop := ${\mid}$ conj :
A ${\rightarrow}$ B ${\rightarrow}$ A ${\land}$ B.

Coq allows elimination over these two propositions into Type, and both
following terms are well-typed:

match x return Bool with end.

and

match x with
${\mid}$ conj $\\_$ $\\_$ ${\Rightarrow}$ true
end.

The object of this section is to make syntactically explicit what happens when
an inductive type of Coq is declared to be of sort Prop. The description
elaborated in this section has strong similarities with the system of bracket-
types proposed by Awodey & Bauer [2]. They describe the propositions as the
subset of types with at most one element, and introduce a left adjoint,
written as brackets, to the inclusion of propositions into types. We will
reuse their notation, even though, in our intensional setting, T:Prop does not
enforce that T has a most one element, and the bracketing operation does not
properly form an adjunction with the inclusion from Prop to Type.

###  4.1. Impredicativity

Let us start by introducing the new sort $\mathrm{Prop}$ in the algebraic
presentation:

$\Gamma\vdash\mathrm{Prop}:\mathrm{Type}$

As in [2], propositions form a subset of types. Coq has a subtyping rule (also
known as _cumulativity_) to make the inclusion transparent. We will, however,
render it with a syntactic construct:

$\Gamma\vdash\left\\{A\right\\}:\mathrm{Type}\Gamma\vdash A:\mathrm{Prop}$
$\Gamma\vdash{\mathrm{prf}}\,{u}:\left\\{A\right\\}\Gamma\vdash u:A$
$\Gamma\vdash\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
u\leavevmode\nobreak\ \mathrm{as}\leavevmode\nobreak\ x\leavevmode\nobreak\
\mathrm{return}\leavevmode\nobreak\ P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\mathrm{prf}}\,{y}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &v\\\ \end{array}\\\
\end{array}:{P}{\left[\,x\,{\setminus}\,u\,\right]}\lx@proof@logical@and\Gamma\vdash
u:\left\\{A\right\\}\Gamma,x{:}\left\\{A\right\\}\vdash P:s\Gamma,y{:}A\vdash
v:{P}{\left[\,x\,{\setminus}\,{\mathrm{prf}}\,{y}\,\right]}$
$\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
{\mathrm{prf}}\,{u}\leavevmode\nobreak\ \mathrm{as}\leavevmode\nobreak\
x\leavevmode\nobreak\ \mathrm{return}\leavevmode\nobreak\
P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\mathrm{prf}}\,{y}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &v\\\ \end{array}\\\
\end{array}\leadsto{v}{\left[\,y\,{\setminus}\,u\,\right]}$

This definition simply makes $\left\\{A\right\\}$ a synonym of $A$, except of
sort $\mathrm{Type}$. It is strictly positive in $A$:

${{\mbox{{sp}}}_{X}}\,{\left\\{A\right\\}}{{\mbox{{sp}}}_{X}}\,{A}$

The fact that $\mathrm{Prop}$ is impredicative – _i.e._ supports the following
product formation rules:

$\Gamma\vdash\prod_{x{:}A}B:\mathrm{Prop}\lx@proof@logical@and\Gamma\vdash
A:s\Gamma,x{:}A\vdash B:\mathrm{Prop}$

is easily understood in terms of proof irrelevance. Indeed, if for all $x$,
$B$ has at most one element, so has the product over $x$. Even though it uses
functional extensionality, which is not provable.

###  4.2. Singleton rules

The types which (ideally) preserve the proof irrelevance property are
sometimes called singleton types in the setting of Coq. In our algebraic
presentation, they correspond to inductive type family constructors with extra
formation rules to make them preserve propositions. The rules are shown in
Figure 5.

$\Gamma\vdash 0:\mathrm{Prop}$ $\Gamma\vdash 1:\mathrm{Prop}$
$\Gamma\vdash{\sum}_{x{:}A}^{f}T:B\rightarrow\mathrm{Prop}\lx@proof@logical@and\Gamma\vdash
A:\mathrm{Prop}\Gamma\vdash B:\mathrm{Prop}\Gamma,x{:}A\vdash
T:\mathrm{Prop}\Gamma,x{:}A\vdash f:B$

Figure 5. Singleton rules

This elucidates why Coq allows elimination over False and And into arbitrary
type: False is implemented as $0$ and And A B and $A\times B$. The elimination
rules being unchanged, pattern-matching over proofs of False and And are
unrestricted. Because restricted pattern-matching is often seen as the
default, singleton types are said to enjoy _singleton elimination_.

Remark that, proofs of propositions being uninformative, there is essentially
nothing to be gained from depending on, or being indexed over a proposition.
In consequence, the type formation rule for proper indexing in Figure 5 is
only useful, in practice, for the subcase of cartesian product.

Coq actually implements two other singleton rules. The first one is for
inductive fixed points. In our algebraic presentation:

$\Gamma\vdash\mu{X}^{A\rightarrow\mathrm{Prop}}.\,F:A\rightarrow\mathrm{Prop}\lx@proof@logical@and\Gamma\vdash
A:s\Gamma,X{:}A\rightarrow\mathrm{Prop}\vdash
F:A\rightarrow\mathrm{Prop}{{\mbox{{sp}}}_{X}}\,{F}$

It allows to type the accessibility predicate $\mathrm{Acc}$ in
$\mathrm{Prop}$. This rule is sound in that fixed points indeed preserve proof
irrelevance in presence of functional extensionality. It is also very useful
for extraction: structural recursion over $\mathrm{Acc}$ allows the definition
of functions whose termination cannot be proved automatically by the guard
condition. However, the proof is no longer needed to ensure termination in the
target languages of extraction. In this sense, at least, it is static data.

The last singleton rule allows properly indexed families in $\mathrm{Prop}$
(not how it is stronger than the rule dependent sum of Figure 5):

$\Gamma\vdash{\sum}_{x{:}A}^{f}T:B\rightarrow\mathrm{Prop}\lx@proof@logical@and\Gamma\vdash
A:\mathrm{Prop}\Gamma\vdash B:\mathrm{Type}\Gamma,x{:}A\vdash
T:\mathrm{Prop}\Gamma,x{:}A\vdash f:B$

It turns the identity type $\mathrm{Eq}$ into a proposition. It is known to be
sound to accept that $\mathrm{Eq}$ is proof irrelevant [6]. It is also useful
for extraction, as equal types, in a closed environment, are extracted to the
same type. Hence a program may safely eliminate over $\mathrm{Eq}$ knowing
that it will not affect the performances of the extracted code. In Coq, the
index $B$ in the rule above can be of any sort ${\mathrm{Type}}_{i}$, however,
this wisdom has been challenged in recent years with the formulation of the
_univalence principle_ [15], of which a simple consequence is that
$\mathrm{Eq}$ is _not_ proof irrelevant at every type. Indeed, some extracted
Coq programs written assuming the univalence principle crash.

To correct for the univalence principle, the singleton rule for proper indices
can be simply dropped; but it can also be restricted to the lowest sort:
$B:{\mathrm{Type}}_{0}$. More precisely the conjunction of the univalence
principle and the proof irrelevance principle is consistent as long as the
singleton rule of proper indices is restricted to sorts $s$ such that there is
no sort $s^{\prime}$ other than $\mathrm{Prop}$ such that $s^{\prime}:s$.
Because, if such a sort $s^{\prime}$ exists, $\mathbb{B}:s^{\prime}$ and by
univalence, ${\mathrm{Eq}}\,{\mathbb{B}}$ has two distinct elements
contradicting proof irrelevance.

For types which do not enjoy singleton elimination, turning them into
propositions means restricting their elimination. We achieve this effect by
adding a single type construction coercing from $\mathrm{Type}$ to
$\mathrm{Prop}$:

$\Gamma\vdash\left[A\right]:\mathrm{Prop}\Gamma\vdash A:\mathrm{Type}$
$\Gamma\vdash\left\langle u\right\rangle:\left[A\right]\Gamma\vdash u:A$
$\Gamma\vdash\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
u\leavevmode\nobreak\ \mathrm{as}\leavevmode\nobreak\ x\leavevmode\nobreak\
\mathrm{return}\leavevmode\nobreak\ P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}\left\langle
y\right\rangle\hfil\leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\ &v\\\
\end{array}\\\
\end{array}:{P}{\left[\,x\,{\setminus}\,u\,\right]}\lx@proof@logical@and\Gamma\vdash
u:\left[A\right]\mbox{${\quad}$$\Gamma,x{:}\left[A\right]\vdash
P:\mathrm{Prop}$${\quad}$}\Gamma,y{:}A\vdash
v:{P}{\left[\,x\,{\setminus}\,\left\langle y\right\rangle\,\right]}$
$\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\ \left\langle
u\right\rangle\leavevmode\nobreak\ \mathrm{as}\leavevmode\nobreak\
x\leavevmode\nobreak\ \mathrm{return}\leavevmode\nobreak\
P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}\left\langle
y\right\rangle\hfil\leavevmode\nobreak\ \Rightarrow\leavevmode\nobreak\ &v\\\
\end{array}\\\ \end{array}\leadsto{v}{\left[\,y\,{\setminus}\,u\,\right]}$

The important rule is the elimination rule, where the return clause is limited
to be of sort $\mathrm{Prop}$, whereas every other type construction can be
eliminated to any sort. Apart from this restriction $\left[A\right]$ is a
synonym of $A$, except in $\mathrm{Prop}$. In [2], the type theory is
extensional, in that the identity type and the conversion relation coincide.
The elimination rules for bracket is much finer and reflects precisely the
fact that propositions are proof-irrelevant. In an intensional type theory,
restricting with respect to sorts approximates this behaviour: even if we
constrained propositions to be proof-irrelevant, not every proof irrelevant
type will have type $\mathrm{Prop}$. The bracketing construction is also
strictly positive:

${{\mbox{{sp}}}_{X}}\,{\left[A\right]}{{\mbox{{sp}}}_{X}}\,{A}$

It is actually possible, using only the impredicative dependent product to
define a bracketing operation: $\prod_{P{:}\mathrm{Prop}}\left(A\rightarrow
P\right)\rightarrow P$. Like $\left[A\right]$ it behaves as $A$ except it can
only be used to form a proposition. However, the impredicative encoding is
positive but not strictly, which motivates the introduction of the extra
construction.

###  4.3. Examples

The logical connectives can be defined as follows:

$\left\\{\begin{aligned} \mathrm{False}&=0\\\
\mathrm{And}&=\lambda{A}^{\mathrm{Prop}}\,{B}^{\mathrm{Prop}}.\,A\times B\\\
\mathrm{pair}&=\lambda{A}^{\mathrm{Prop}}\,{B}^{\mathrm{Prop}}\,{x}^{A}\,{y}^{B}.\,\left(x,y\right)\\\
\mathrm{Or}&=\lambda{A}^{\mathrm{Prop}}\,{B}^{\mathrm{Prop}}.\,\left[A+B\right]\\\
{\mathrm{or}}_{\mathrm{introl}}&=\lambda{A}^{\mathrm{Prop}}\,{B}^{\mathrm{Prop}}\,{x}^{A}.\,\left\langle{\mathrm{inl}}\,{x}\right\rangle\\\
{\mathrm{or}}_{\mathrm{intror}}&=\lambda{A}^{\mathrm{Prop}}\,{B}^{\mathrm{Prop}}\,{y}^{B}.\,\left\langle{\mathrm{inr}}\,{y}\right\rangle\\\
\mathrm{Ex}&=\lambda{A}^{\mathrm{Type}}\,{P}^{A\rightarrow\mathrm{Prop}}.\,\left[\sum_{x{:}A}{P}\,{x}\right]\\\
{\mathrm{ex}}_{\mathrm{intro}}&=\lambda{A}^{\mathrm{Type}}\,{P}^{A\rightarrow\mathrm{Prop}}\,{x}^{A}\,{p}^{{P}\,{x}}.\,\left\langle{\left(x,p\right)}_{{\mbox{\scriptsize{$x${:}$A$.$P$}}}}\right\rangle\end{aligned}\right.$

Note how, because of the brackets, existentials and disjunctions are
prohibited from being eliminated to non-propositional types. Thanks to the
singleton rules, however, conjunction and falsity do not require brackets.

As a final example, consider the type Ascending n p of ascending sequences of
integers between p and n defined by mutual recursion with the proposition Ge m
p which stands from m is greater than or equal to p:

Inductive Ascending : Nat ${\rightarrow}$ Nat ${\rightarrow}$ Type := ${\mid}$
top : forall n, Ascending n n
${\mid}$ up : forall n p m, Ge m (s p) ${\rightarrow}$ Ascending n m
${\rightarrow}$ Ascending n p
with Ge : Nat ${\rightarrow}$ Nat ${\rightarrow}$ Prop := ${\mid}$ ascend :
forall m p, Ascending m p ${\rightarrow}$ Ge m p.

As Ascending has type Type, whereas Ge has type Prop, the translation to a
single inductive type is not as straightforward as Even and Odd. The
translation requires the use of brackets around the recursive calls:

$\left\\{\begin{aligned}
\mathrm{AscendingGe}&=\begin{array}[]{l}\mu{X}^{\left(\mathrm{Nat}\times\mathrm{Nat}\right)+\left(\mathrm{Nat}\times\mathrm{Nat}\right)\rightarrow\mathrm{Type}}.\,\lambda{i}^{\left(\mathrm{Nat}\times\mathrm{Nat}\right)+\left(\mathrm{Nat}\times\mathrm{Nat}\right)}.\,\mbox{\phantom{a}}\\\
\begin{array}[]{cl}&{\left({\sum}_{n{:}\mathrm{Nat}}^{{\mathrm{inl}}\,{\left(n,n\right)}}1\right)}\,{i}\\\
+&{\left({\sum}_{j{:}\mathrm{Nat}\times\mathrm{Nat}}^{{\mathrm{inl}}\,{j}}\sum_{m{:}\mathrm{Nat}}\left[{X}\,{\left({\mathrm{inr}}\,{\left(m,{s}\,{\left({{\pi}_{2}}\,{j}\right)}\right)}\right)}\right]\times{X}\,{\left({\mathrm{inl}}\,{\left({{\pi}_{1}}\,{j},m\right)}\right)}\right)}\,{i}\\\
+&{\left({\sum}_{j{:}\mathrm{Nat}\times\mathrm{Nat}}^{{\mathrm{inr}}\,{j}}{X}\,{\left({\mathrm{inl}}\,{j}\right)}\right)}\,{i}\\\
\end{array}\\\ \end{array}\\\
\mathrm{Ascending}&=\lambda{n}\,{p}.\,{\mathrm{AscendingGe}}\,{\left({\mathrm{inl}}\,{\left(n,p\right)}\right)}\\\
\mathrm{Ge}&=\lambda{m}\,{p}.\,\left[{\mathrm{AscendingGe}}\,{\left({\mathrm{inr}}\,{\left(m,p\right)}\right)}\right]\end{aligned}\right.$

##  5\. Impredicative Set

In addition to the impredicative sort $\mathrm{Prop}$, Coq has a sort
$\mathrm{Set}$ which is predicative by default but can be turned impredicative
with a flag. Where $\mathrm{Prop}$ is meant to be used in the context of
separating static and dynamic information, the spirit of the impredicative
sort $\mathrm{Set}$ is to be as powerful as possible without being
inconsistent. In the algebraic presentation, that means being stable by every
construction except dependent sums with the first projection in an arbitrary
sort (_strong sums_).

To mirror the optional nature of the impredicativity of $\mathrm{Set}$, the
rules for a predicative sort $\mathrm{Set}$ are given in Figure 6; to turn
impredicativity on, the rules of Figure 7 must be used _in addition_ to those
of predicative $\mathrm{Set}$. This presentation makes immediately apparent
that impredicative $\mathrm{Set}$ is an extension of predicative
$\mathrm{Set}$, in that every program of the latter typechecks in the former.

The rules of $\mathrm{Set}$ are the same as those of $\mathrm{Prop}$, with the
exception of $A+B$ which is in $\mathrm{Set}$ when both $A$ and $B$ are – even
with predicative $\mathrm{Set}$. Hence, there are types in $\mathrm{Set}$ with
several elements – _e.g._ $\mathbb{B}$. As a consequence, the bracketing
operation which coerces types in $\mathrm{Type}$ to $\mathrm{Set}$ does not
enjoy an explanation in terms of proof irrelevance, as was the case in
$\mathrm{Prop}$. As a matter of fact, there is no clear set-theoretical
description at all. A close cousin of $\mathrm{Set}$ bracketing, however, can
be found in homotopy type theory [15], where, roughly, groupoids are
_truncated_ to sets through a quotient of their homsets by the total relation.

$\Gamma\vdash\mathrm{Set}:\mathrm{Type}$
$\Gamma\vdash\prod_{x{:}A}B:\mathrm{Set}\lx@proof@logical@and\Gamma\vdash
A:\mathrm{Set}\Gamma,x{:}A\vdash B:\mathrm{Set}$
$\Gamma\vdash\sum_{x{:}A}P:\mathrm{Set}\lx@proof@logical@and\Gamma\vdash
A:\mathrm{Set}\Gamma,x{:}A\vdash P:\mathrm{Set}$
$\Gamma\vdash A+B:\mathrm{Set}\lx@proof@logical@and\Gamma\vdash
A:\mathrm{Set}\Gamma\vdash B:\mathrm{Set}$ $\Gamma\vdash 1:\mathrm{Set}$
$\Gamma\vdash 0:\mathrm{Set}$
$\Gamma\vdash\mu{X}^{A\rightarrow\mathrm{Set}}.\,F:A\rightarrow\mathrm{Set}\lx@proof@logical@and\Gamma\vdash
A:s\Gamma,X{:}A\rightarrow\mathrm{Set}\vdash
F:A\rightarrow\mathrm{Set}{{\mbox{{sp}}}_{X}}\,{F}$
$\Gamma\vdash{\sum}_{x{:}A}^{f}T:B\rightarrow\mathrm{Set}\lx@proof@logical@and\Gamma\vdash
A:\mathrm{Set}\Gamma\vdash B:\mathrm{Set}\Gamma,x{:}A\vdash
T:\mathrm{Set}\Gamma,x{:}A\vdash f:B$
$\Gamma\vdash\nu{X}^{A\rightarrow\mathrm{Set}}.\,F:A\rightarrow\mathrm{Set}\lx@proof@logical@and\Gamma\vdash
A:s\Gamma,X{:}A\rightarrow\mathrm{Set}\vdash
F:A\rightarrow\mathrm{Set}{{\mbox{{sp}}}_{X}}\,{F}$
$\Gamma\vdash{\left\\{A\right\\}}_{\mathrm{Set}}:\mathrm{Type}\Gamma\vdash
A:\mathrm{Set}$
$\Gamma\vdash{\mathrm{elt}}\,{u}:{\left\\{A\right\\}}_{\mathrm{Set}}\Gamma\vdash
u:A$
$\Gamma\vdash\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
u\leavevmode\nobreak\ \mathrm{as}\leavevmode\nobreak\ x\leavevmode\nobreak\
\mathrm{return}\leavevmode\nobreak\ P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\mathrm{elt}}\,{y}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &v\\\ \end{array}\\\
\end{array}:{P}{\left[\,x\,{\setminus}\,u\,\right]}\lx@proof@logical@and\Gamma\vdash
u:{\left\\{A\right\\}}_{\mathrm{Set}}\Gamma,x{:}{\left\\{A\right\\}}_{\mathrm{Set}}\vdash
P:s\Gamma,y{:}A\vdash
v:{P}{\left[\,x\,{\setminus}\,{\mathrm{elt}}\,{y}\,\right]}$
$\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
{\mathrm{elt}}\,{u}\leavevmode\nobreak\ \mathrm{as}\leavevmode\nobreak\
x\leavevmode\nobreak\ \mathrm{return}\leavevmode\nobreak\
P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\mathrm{elt}}\,{y}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &v\\\ \end{array}\\\
\end{array}\leadsto{v}{\left[\,y\,{\setminus}\,u\,\right]}$
${{\mbox{{sp}}}_{X}}\,{{\left\\{A\right\\}}_{\mathrm{Set}}}{{\mbox{{sp}}}_{X}}\,{A}$

Figure 6. Rules for predicative $\mathrm{Set}$

$\Gamma\vdash\prod_{x{:}A}B:\mathrm{Set}\lx@proof@logical@and\Gamma\vdash
A:s\Gamma,x{:}A\vdash B:\mathrm{Set}$
${{\mbox{{sp}}}_{X}}\,{{\left[A\right]}_{\mathrm{Set}}}{{\mbox{{sp}}}_{X}}\,{A}$
$\Gamma\vdash{\left[A\right]}_{\mathrm{Set}}:\mathrm{Set}\Gamma\vdash
A:\mathrm{Type}$ $\Gamma\vdash{\left\langle
u\right\rangle}_{\mathrm{Set}}:{\left[A\right]}_{\mathrm{Set}}\Gamma\vdash
u:A$
$\Gamma\vdash\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\
u\leavevmode\nobreak\ \mathrm{as}\leavevmode\nobreak\ x\leavevmode\nobreak\
\mathrm{return}\leavevmode\nobreak\ P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\left\langle
y\right\rangle}_{\mathrm{Set}}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &v\\\ \end{array}\\\
\end{array}:{P}{\left[\,x\,{\setminus}\,u\,\right]}\lx@proof@logical@and\Gamma\vdash
u:{\left[A\right]}_{\mathrm{Set}}\Gamma,x{:}{\left[A\right]}_{\mathrm{Set}}\vdash
P:\mathrm{Set}\Gamma,y{:}A\vdash v:{P}{\left[\,x\,{\setminus}\,{\left\langle
y\right\rangle}_{\mathrm{Set}}\,\right]}$
$\begin{array}[]{@{}l}\mathrm{match}\leavevmode\nobreak\ {\left\langle
u\right\rangle}_{\mathrm{Set}}\leavevmode\nobreak\
\mathrm{as}\leavevmode\nobreak\ x\leavevmode\nobreak\
\mathrm{return}\leavevmode\nobreak\ P\leavevmode\nobreak\ \mathrm{with}\\\
\begin{array}[]{|l@{~\Rightarrow~}l}{\left\langle
y\right\rangle}_{\mathrm{Set}}\hfil\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ &v\\\ \end{array}\\\
\end{array}\leadsto{v}{\left[\,y\,{\setminus}\,u\,\right]}$

Figure 7. Rules for impredicative $\mathrm{Set}$

##  6\. Conclusion

The algebraic presentation of Coq makes the conversion between sorts explicit.
The toplevel inductive definitions of Coq can be understood as implicitly
inserting canonical bracketing operations when an inductive type is declared
inside an impredicative sort but should be of a different sort due to its
form; and inserting type coercion from a smaller sort to a bigger sort when
applying a cumulativity rule.

Monolithic type definitions like in Coq have a number of advantages over the
algebraic presentation, they boil down to better type errors due to naming,
better type inference and better memory representation due to $n$-ary sums and
products. However, the value of the implicit coercions between sorts is less
clear. In particular, the bracketing operation to impredicative sorts is
probably a better guide for program extraction than the current method of
figuring whether or not a given type is a proposition, which interacts badly
with universe polymorphism [7]. Explicit coercions for extraction are also in
the spirit of [5].

All of the algebraic type constructors can actually be defined in Coq, except
the two fixed-points because there is no way to abstract over strictly
positive type families. So is it clear that expressions of the algebraic
presentation which do not use inductive or co-inductive fixed points can be
translated into Coq. Occurrences of the fixed points in a type must be
${\lambda}$-lifted and given a toplevel name. Some care must be given to
avoiding the duplication of such definitions otherwise types which must be
convertible for the expression to typecheck, might be seen as different in the
Coq translation. Apart from this technicality, translation from the algebraic
presentation to Coq is straightforward. We claim that, at least if we extend
the algebraic presentation to a hierarchy of universes and the strict
positivity condition is made a bit more fine-grained, Coq terms can be,
conversely, translated into the algebraic presentation.

## References

  * [1] Andreas Abel.  A polymorphic lambda-calculus with sized higher-order types.  PhD thesis, 2006.
  * [2] Steve Awodey and Andrej Bauer.  Propositions as [Types].  Journal of Logic and Computation, 14(4):447–471, August 2004.
  * [3] Henk Barendregt.  Lambda calculus with types.  Handbook of logic in computer science, 1992.
  * [4] Bruno Barras.  Semantical Investigations in Intuitionistic Set Theory and Type Theories with Inductive Families.  Thèse d’Habilitation, 2013.
  * [5] Bruno Barras and Bruno Bernardo.  The implicit calculus of constructions as a programming language with dependent types.  Foundations of Software Science and Computational Structures, 4962:365–379, 2008.
  * [6] Gyesik Lee and Benjamin Werner.  Proof-irrelevant model of CC with predicative induction and judgmental equality.  2011\.
  * [7] Pierre Letouzey and Bas Spitters.  Implicit and noncomputational arguments using monads.  pages 1–16, 2005.
  * [8] Peter Morris.  Constructing Universes for Generic Programming.  PhD thesis, 2007.
  * [9] Peter Morris and Thorsten Altenkirch.  Constructing strictly positive families.  CATS ’07 Proceedings of the thirteenth Australasian symposium on Theory of computing, pages 111–121, 2007.
  * [10] Peter Morris, Thorsten Altenkirch, and Neil Ghani.  A universe of strictly positive families.  IInternational journal of foundations of computer science, pages 83–107, 2009.
  * [11] Ulf Norell.  Towards a practical programming language based on dependent type theory.  PhD thesis, Chalmers University of Technology, 2007.
  * [12] Chris Okasaki.  Purely functional data structures.  1999\.
  * [13] Christine Paulin-Mohring.  Définitions inductives en théorie des types d’ordre supérieur.  PhD thesis, Université Claude Bernard-Lyon I, 1996.
  * [14] The Coq development team.  The Coq Proof Assistant.
  * [15] The Univalent Foundations Program.  Homotopy Type Theory: Univalent Foundations of Mathematics.


[affiliation=1,2]JunzuoZhou [affiliation=1, *]JiangyanYi
[affiliation=1]TaoWang [affiliation=3]JianhuaTao [affiliation=1]YeBai
[affiliation=1,2]Chu YuanZhang [affiliation=1,2]YongRen
[affiliation=1]ZhengqiWen

# TraceableSpeech: Towards Proactively Traceable Text-to-Speech with
Watermarking

###### Abstract

Various threats posed by the progress in text-to-speech (TTS) have prompted
the need to reliably trace synthesized speech. However, contemporary
approaches to this task involve adding watermarks to the audio separately
after generation, a process that hurts both speech quality and watermark
imperceptibility. In addition, these approaches are limited in robustness and
flexibility. To address these problems, we propose TraceableSpeech, a novel
TTS model that directly generates watermarked speech, improving watermark
imperceptibility and speech quality. Furthermore, We design the frame-wise
imprinting and extraction of watermarks, achieving higher robustness against
resplicing attacks and temporal flexibility in operation. Experimental results
show that TraceableSpeech outperforms the strong baseline where VALL-E or
HiFicodec individually uses WavMark in watermark imperceptibility, speech
quality and resilience against resplicing attacks. It also can apply to speech
of various durations.

###### keywords:

proactive traceability, speech watermarking, language model, text-to-speech

##  1 Introduction

Recently, language model technology has achieved excellent performance in the
text-to-speech (TTS) tasks such as VALL-E [1], SPEAR-TTS [2], and SoundStorm
[3]. These methods usually use neural codec [4, 5] to extract discrete
representation from waveform and put them into language models for training.
Synthetic speech becomes increasingly realistic and natural, raising social
issues regarding security and privacy, such as deepfake audio scams and
copyright protection. Therefore, it is vital for regulatory agencies supervise
synthetic speech through traceability methods [6, 7]. Passive forensics is one
of the most common options for traceability [8, 9, 10]. However, the artifact
based detection are difficult to generalize well to unknown scenarios, making
it susceptible to failure as the advancement of increasingly lifelike speech
forgery techniques.

Based on the analysis above, proactive traceability in TTS systems is
imperative. Responding to this necessity, several attempts of embedding
watermarking signals as source information in the generated speech, aim to
alleviate this problem. By utilizing specific algorithms to extract watermarks
imperceptible to the ear, it is feasible to identify the source of the speech.

Audio watermarking methods are divided into two categories: traditional and
deep learning based. Traditional methods mainly include echo hiding [11],
patchwork [12], spread spectrum [13], etc. These methods have fragility and
limited adaptability because they rely on expert knowledge and empirical
rules. Meanwhile, increasingly powerful deep learning based frameworks can
automatically model more robust watermark encoding via neural networks in a
data-driven manner. This advantage simplifies the watermarking design while
keeping superior extractability against real-life speech manipulations or
attacks. Several works have been proposed based on the DNN network [14, 15].
Recently, Chen et al. [16] proposed the WavMark, an audio watermarking
framework based on reversible networks, which surpasses previous work in each
aspect.

However, embedding watermarks into generated speech through the above
frameworks to achieve proactive traceability in TTS still has some
limitations. Firstly, watermark insertion is constrained to post-generation
phases, which triggers error accumulation, reducing the watermark
imperceptibility and the speech quality; Secondly, some advanced approaches
(e.g. WavMark) exhibit issues of low temporal flexibility in implementation
and suboptimal robustness against resplicing attacks. Specifically, during
inference, WavMark is restricted to embedding watermarks in speech segments
that equate to the training snippets in duration, making it unsuitable for TTS
tasks with unpredictable speech durations. In addition, WavMark repeatedly
embeds uniform watermarks on segments at fixed intervals to resist temporal
edits. However, it is still susceptible to high-intensity resplicing attacks,
particularly in shorter utterances.

To address these issues, we propose a proactively traceable TTS model named
TraceableSpeech. Firstly, for imperceptibility, TraceableSpeech integrates
watermarking technology with language model based TTS via end-to-end training
of codec and watermarking mechanism. It directly generates watermarked speech
as information is embedded in the synthesis phase, optimizing watermark
imperceptibility and speech quality; Secondly, for robustness and flexibility,
we design a method for the frame-wise imprinting and extraction of watermarks.
This method broadcasts watermark embedding and merges it with speech
intermediate features of codec at frame-level and restore watermark from an
r-vector extracted by ResNet [17], which maintains exceptional resilience
under resplicing attacks and ensures availability across speech of various
durations. We conducted experiments on the LibriTTS [18]. The contributions of
this paper are as follows:

  * •

We propose a proactively traceable TTS model jointly optimized for
watermarking. This work generate watermarked speech directly, enhancing
watermark imperceptibility to human listeners and speech quality as shown in
better score on PESQ [19], ViSQOL [20], and subjective metrics, etc.

  * •

We design a watermark embedding and extraction method tailored to TTS tasks,
ensuring the watermark’s robustness as shown in the better extraction accuracy
after resplicing attacks, while offering temporal flexibility in operation.
Even after embedding 4-digit base-64 watermarks in 0.3-second utterances, the
extraction accuracy still remains above 95%.

(a) Overall architecture.

(b) Watermark Extractor module.

Figure 1: The first stage: Watermarking mechanism integrate into neural codec.

Figure 2: The second stage: Watermarking mechanism integrate into language
model of VALL-E.

##  2 Proposed Method

###  2.1 The overall Framework of TraceableSpeech

The speech synthesis in TraceableSpeech is structured into two sequential
stages: the neural codec and the language model. Figures 1 and 2 respectively
illustrate the integration of the watermarking mechanism into these two
stages. Both stages realize the closed-loop process of information embedding
to retrieval via modules such as watermark encoder, imprint, and watermark
extractor.

As shown in Figure 1, the neural codec utilizes speech encoder and speech
decoder both derived from HifiCodec’s design [5]. The speech waveform of
duration $d$ is represent as $x\in\mathbb{R}^{T}$ with a sampling rate of
$f_{sr}$, where $T=f_{sr}\times d$. In training, the speech waveform undergoes
encoder downsampling, quantization, and quantized restoration, thereby
transforming into a high-dimensional latent representation
$z\in\mathbb{R}^{t\times 512}$, where $t$ is the count of frames after
240$\times$ down-sampling. The watermark information is embedded in $z$
through the imprint module. Then, the speech decoder generates watermarked
speech from $z$. Ultimately, the joint end-to-end training of watermarking and
codec is realized utilizing the watermark decoder and discriminators.

As shown in Figure 2, the discrete representation obtained by the speech
encoder is put into the language model with the same structure as VALL-E.
During inference, the imprint module embeds the watermark information into the
discrete representation predicted from the language model. Then, the
watermarked speech is synthesized by the speech decoder.

###  2.2 Frame-wise Imprinting

Previous methods directly extend watermark vector through linear layers to
match the waveform's length [16], sacrificing temporal flexibility and raising
non-uniform distribution of watermark information along the temporal axis. In
this work, watermark information is embedded into frame-level speech features
and control it by broadcasting in time-domain, thereby supporting speech of
various duration. Furthermore, the embedded information is uniform and
comprehensive across all parts of this speech, which avoids damage from
resplicing attacks.

As shown in Figure 1(a), we utilize $m$-digit base-$b$ numerical information
as a watermark. The watermark encoder first maps the number of each digit to
embedding using a $b\times 16$ weight matrix. Then, two linear layers convert
a long vector concatenated by $m$ embedding into latent representation
$w_{o}\in\mathbb{R}^{1\times 512}$. In the imprint module, $w_{o}$ is
broadcast along the time axis. Therefore, by controlling the position and
number of frames that are broadcast, the positions and duration of the
watermarked segments can be precisely controlled in the synthesized speech.

In practice, to ensure full-time region protection. All frames are broadcast
to obtain $w\in\mathbb{R}^{t\times 256}$ that is the high-dimensional feature
for merging with the speech latent representation $z$. So that, even if some
frames are truncated, the remaining frames can still be successfully
extracted. Since the watermark is embedded at the frame level, the broadcast
imprint module can embed the information into the entire speech of any
duration, thereby achieving broad temporal flexibility.

###  2.3 Watermark extractor and training mechanism

####  2.3.1 Watermark extractor

As shown in Figure 1(b), the input of the watermark extractor is the Mel-
spectrogram of the synthesized speech from the speech decoder. An r-vector
extracted through the ResNet [21] is individually connected with $m$ groups of
two-layer linear layers to calculate the probability distribution of each
digit and obtain the predicted number by softmax.

####  2.3.2 Training mechanism

Attack simulation: We incorporate attack simulation in training to be
resilient against common watermark attack. In this module, the synthesized
speech undergoes one of the following seven processes [15, 16]: Normal
extraction, no attack (Normal); Resample with 90% of original sampling rate
and recovery (RS-90); White noise with an SNR of 35db was added (Noise-W35);
Randomly dropout 0.1% of the sample points (SD-01); Reduce the amplitude to
90% of its original value (AR-90); Attenuate the resulting speech by a factor
of 0.3, delay the volume by 15%, then overlay the original speech (EA-0315);
Low-pass filter with a cutoff frequency of 5k Hz. Since high-pass filtering
would destroy the essential information for synthesized speech, only the more
practical low-pass filtering is considered (LP-5000).

The assigned weight values of the aforementioned processes are empirically set
at 0.45, 0.04, 0.25, 0.04, 0.04, 0.14, and 0.04, respectively, due to the
TraceableSpeech's higher sensitivity to Noise and Echo.

Optimizing strategy: To integrate with the above network, we design the
following optimization strategy. The training process is divided into two
stages: neural codec and language model. Compared with HiFiCodec [5], the loss
function of the neural codec adds the cross-entropy watermark loss in the
generator:

$\displaystyle\mathcal{L}_{c}=\frac{1}{m}\sum_{i=1}^{m}\sum_{j=1}^{b}l_{ij}\log\left(p_{ij}\right)$
(1)

where $l_{ij}$ and $p_{ij}$ are the one-hot encoding and the predicted
probability of the $i$-th digit watermark for number $j$, respectively. In
addition, the generator loss also include the reconstruction loss of frequency
domain $\mathcal{L}_{f}$, the quantization loss $\mathcal{L}_{qz}$, the
feature matching loss $\mathcal{L}_{feat}$, and the adversarial loss of the
generator $\mathcal{L}_{g}$, all of which are the same as HiFiCodec. The total
loss function of the generator is:

$\begin{split}\mathcal{L}&=\lambda_{f}\mathcal{L}_{f}+\lambda_{g}\mathcal{L}_{g}+\lambda_{feat}\mathcal{L}_{feat}+\lambda_{qz}\mathcal{L}_{qz}+\lambda_{c}\mathcal{L}_{c}\end{split}$
(2)

$\lambda_{f}$, $\lambda_{g}$, $\lambda_{feat}$, $\lambda_{qz}$ and
$\lambda_{c}$ are hyper-parameters to balance each term of the final loss.
Their values are 1, 1, 1, 10, and 5, respectively, thus reflecting a bias
towards the watermark network and quantizer.

The training of the language model is the same as VALL-E.

##  3 Experiments

###  3.1 Dateset

We use the LibriTTS dataset to train the neural
codec111https://github.com/yangdongchao/AcademiCodec and the
VALL-E222https://github.com/lifeiteng/vall-e language model from scratch. The
LibriTTS corpus [18] consists of 585 hours of English speech data from 2456
speakers at 24kHz. Our training set consists of train-clean-100, train-
clean-360, and train-other-500. Our test set is also from the subsets of
LibriTTS.

###  3.2 Experiment Setup

Baseline: We compare TraceableSpeech with the state-of-the-art deep audio
watermarking framework333https://github.com/wavmark/wavmark [16]. This
framework is trained on the 1-second audio snippet. Hence, watermarking can
only be applied to 1-second audio segments during inference. It utilizes an
“utterance mode” for audio exceeding this length by repeatedly adding the same
1-second watermark content at fixed intervals. While WavMark embeds 32-bit
binary watermarks in this mode, the initial 16 bits are allocated as pattern
bits to ascertain the validity and completeness of this segment's watermark.
This method notably reduces the usable capacity to 16 bits in binary. This
watermark is deemed unextractable if the pattern bits in all added segments
are identified as failures. In speech reconstruction and zero-shot speech
synthesis, we utilize WavMark to embed watermarks into the speech waveforms
generated by HiFicodec and VALL-E, respectively. These watermarked speech are
used for comparison.

Training setup: In the experiments detailed in section 3.3 and 3.4, we train a
4-digit base-16 model $4@16$, which has the same watermark capacity as the
baseline, and a 4-digit base-10 model $4@10$. We use ResNet34 in the watermark
extractor. The dimension of the extractive embedding is 256. For the neural
codec, the quantizer utilizes 1 group with 8 codebooks and the batch size is
32. We truncate the training data to 0.5 seconds, all models are trained for
150k steps. For the language model, the maximum duration per batch is 100. The
AR and NAR stages are trained for 20 and 40 epochs, respectively.

Resplicing attacks setup: During inference, a resplicing attack means that the
watermarked speech is randomly cut out $1/4$ to $1/3$ of the watermarked
speech is cut out from the middle of the original waveform, with the rest
concatenated.

Table 1: Watermark Imperceptibility Metrics in Speech Reconstruction

Model | PESQ $\uparrow$ | STOI $\uparrow$ | ViSQOL $\uparrow$
---|---|---|---
HiFicodec + WavMark(16bit) | 3.197 | 0.947 | 3.880
TraceableSpeech(4@10) | 3.641 | 0.950 | 4.060
TraceableSpeech(4@16) | 3.569 | 0.948 | 3.985

  * 1

$@$ denotes the watermarking capacity. For example, $4@16$ indicates 4-digit
base-16, equivalent to the 16-bit capacity of WavMark used in the baseline.
This annotation is applicable to other tables as well.

Table 2: Speech Quality in Zero-Shot Speech Synthesis

Model | WER$(\%)$ $\downarrow$ | MOS $\uparrow$
---|---|---
VALL-E + WavMark(16bit) | 10.80 | 3.554 $\pm$ 0.19
TraceableSpeech(4@10) | 9.61 |  3.959 $\pm$ 0.18
TraceableSpeech(4@16) | 10.47 | 3.905 $\pm$ 0.17

###  3.3 Performance of Speech Reconstruction

Comparing the watermarked speech with its unwatermarked counterpart can help
evaluate the watermark imperceptibility, achieved by calculating PESQ [19],
STOI [22], ViSQOL V3 [20] metrics. Since the speech generated in speech
synthesis experiment is still diverse even using the same text, it is
necessary to set up a codec speech reconstruction experiment. 200 test speech
samples of various durations are from the test-clean of the LibriTTS corpus
Each metric is calculated by comparing the reconstructed speech with the
ground truth. Table 1 demonstrates that TraceableSpeech outperforms baselines
in all metrics. Additionally, The comparison of 4@10 and 4@16 indicates that
the watermark imperceptibility diminishes as its capacity increases.

Table 3: Watermark extraction accuracy (%) under various attacks

Model Attack | Resplicing | Normal | RSP-90 | Noise-W35 | SD-01 | AR-90 | EA-0315 | LP5000
---|---|---|---|---|---|---|---|---
VALL-E + WavMark(16bit) | No | 100.00 | 99.76 | 91.41 | 100.00 | 100.00 | 94.53 | 100.00
TraceableSpeech(4@10) | No | 100.00 | 100.00 | 100.00 | 100.00 | 100.00 | 100.00 | 100.00
TraceableSpeech(4@16) | No | 98.97 | 98.82 | 98.95 | 99.12 | 99.46 | 97.71 | 98.84
VALL-E + WavMark(16bit) | Once | 91.10 | 91.46 | 63.53 | 95.95 | 93.61 | 88.58 | 89.66
TraceableSpeech(4@10) | Once | 100.00 | 100.00 | 100.00 | 99.90 | 100.00 | 100.00 | 100.00
TraceableSpeech(4@16) | Once | 100.00 | 99.82 | 99.83 | 98.78 | 99.50 | 99.57 | 99.62
VALL-E + WavMark(16bit) | Twice | 76.65 | 77.74 | 49.14 | 79.47 | 85.46 | 68.19 | 75.32
TraceableSpeech(4@10) | Twice | 100.00 | 100.00 | 100.00 | 100.00 | 100.00 | 100.00 | 100.00
TraceableSpeech(4@16) | Twice | 99.58 | 99.20 | 99.58 | 99.56 | 99.00 | 99.65 | 98.83

  * 1

The resplicing column mean the times of resplicing attack

Table 4: Watermark extraction accuracy (%) of larger capacity models under
various speech durations (s)

Model Duration | 1.0 | 0.8 | 0.5 | 0.3 | 0.2 | 0.175 | 0.15 | 0.125 | 0.1
---|---|---|---|---|---|---|---|---|---
TraceableSpeech(4@32) | 100.00 | 100.00 | 99.74 | 99.23 | 94.13 | 86.22 | 77.29 | 57.14 | 50.51
TraceableSpeech(4@64) | 100.00 | 100.00 | 99.86 | 95.57 | 80.59 | 66.79 | 53.90 | 27.47 | 17.01

###  3.4 Performance of Zero-Shot Speech Synthesis

We use 200 text prompts from the test-clean of the LibriTTS corpus. Each
sample is subjected to 20 tests of watermark embedding and extraction. The
duration of the synthesized speech is restricted between 1.125 seconds and 10
seconds to reflect the temporal diversity. Considering the limit of the
baseline, we also exclude test samples that are shorter than the
aforementioned lower bound after resplicing attacks.

The quality of the synthesized watermarked speech can be evaluated using
subjective and objective metrics. We utilized HuBERT-large-
ls960-ft4555https://huggingface.co/facebook/hubert-large-ls960-ft [23] to
transcribe speech and compute WER to evaluate content accuracy. In addition,
We invited seven participants to mark speech quality with MOS results. Table 2
shows the results of speech quality, with our work surpasses baselines. And
the speech quality also exhibits an inverse relationship with the watermark
capacity.

If the watermark in the baseline cannot be extracted, it is considered that
all bits are incorrect. As shown in Table 3, the robustness results indicate
that our work maintains a higher extraction accuracy when facing resplicing
attacks than the baseline. Furthermore, our advantage becomes increasingly
apparent as the attacks intensify.

###  3.5 Quantitative analysis of Capacity and Duration

The analysis explores the impact of increased watermark capacity and reduced
speech duration on extraction accuracy. Because the robustness, capacity, and
imperceptibility of watermarks are impossible to achieve simultaneously, the
models trained in this analysis, including 4-digit base-32 (4@32) and 4-digit
base-64 (4@64), are not subjected to simulated attacks. Considering the
increased capacity, we use ResNet101 [17] in the watermark extractor, and the
dimension of the extractive embedding is 512. This analysis is conducted
through speech reconstruction to precisely control the duration of the speech
for evaluation. The test set is composed of speech slices ranging from 0.1 to
1 second. As shown in Table 4, even after embedding 4-digit base-64 watermarks
in 0.3-second speech segments, the extraction accuracy of our method still
remains above 95%.

##  4 Conclusion

This work proposes TraceableSpeech, a novel TTS model that jointly optimizes
the watermarking mechanism and speech synthesis, thereby directly generating
watermarked speech. This approach enhances the watermark imperceptibility and
speech quality. This work also proposes frame-wise imprinting and extraction
networks of watermarks, designed specifically for the characteristics of the
TTS task to enhance robustness against resplicing attacks and improve temporal
flexibility for speech of various durations. Experimental results demonstrate
that TraceableTTS performs superiorly in various metrics, including PESQ, WER,
and extraction accuracy after resplicing attacks. In the future, We aim to
bolster the robustness against increasingly varied and more potent watermark
attacks.

##  5 Acknowledgements

This work is supported by the Strategic Priority Research Program of Chinese
Academy of Sciences, Grant No. XDB0500103, the National Natural Science
Foundation of China (NSFC) (No. 62322120, No.U21B2010, No. 62306316, No.
62206278).

## References

  * [1] C. Wang, S. Chen, Y. Wu, Z. Zhang, L. Zhou, S. Liu, Z. Chen, Y. Liu, H. Wang, J. Li _et al._ , ``Neural codec language models are zero-shot text to speech synthesizers,'' _arXiv preprint arXiv:2301.02111_ , 2023.
  * [2] E. Kharitonov, D. Vincent, Z. Borsos, R. Marinier, S. Girgin, O. Pietquin, M. Sharifi, M. Tagliasacchi, and N. Zeghidour, ``Speak, read and prompt: High-fidelity text-to-speech with minimal supervision,'' _arXiv preprint arXiv:2302.03540_ , 2023.
  * [3] Z. Borsos, M. Sharifi, D. Vincent, E. Kharitonov, N. Zeghidour, and M. Tagliasacchi, ``Soundstorm: Efficient parallel audio generation,'' _arXiv preprint arXiv:2305.09636_ , 2023.
  * [4] A. Défossez, J. Copet, G. Synnaeve, and Y. Adi, ``High fidelity neural audio compression,'' _arXiv preprint arXiv:2210.13438_ , 2022.
  * [5] D. Yang, S. Liu, R. Huang, J. Tian, C. Weng, and Y. Zou, ``Hifi-codec: Group-residual vector quantization for high fidelity audio codec,'' _arXiv preprint arXiv:2305.02765_ , 2023.
  * [6] K. H. Diane Bartz, ``Openai, google, others pledge to watermark ai content for safety, white house says,'' 2023. [Online]. Available: https://www.reuters.com/technology/openai-google-others-pledge-watermark-ai-content-safety-white-house-2023-07-21/
  * [7] M. Sheehan, ``China’s ai regulations and how they get made,'' 2023. [Online]. Available: https://carnegieendowment.org/2023/07/10/china-s-ai-regulations-and-how-they-get-made-pub-90117
  * [8] X. Yan, J. Yi, J. Tao, C. Wang, H. Ma, T. Wang, S. Wang, and R. Fu, ``An initial investigation for detecting vocoder fingerprints of fake audio,'' in _Proceedings of the 1st International Workshop on Deepfake Detection for Audio Multimedia_ , 2022, pp. 61–68.
  * [9] J. Lu, Y. Zhang, Z. Li, Z. Shang, W. Wang, and P. Zhang, ``Detecting unknown speech spoofing algorithms with nearest neighbors,'' in _Proceedings of IJCAI 2023 Workshop on Deepfake Audio Detection and Analysis_ , 2023.
  * [10] Y. Xie, H. Cheng, Y. Wang, and L. Ye, ``Domain generalization via aggregation and separation for audio deepfake detection,'' _IEEE Transactions on Information Forensics and Security_ , 2023.
  * [11] R. Anderson, ``Information hiding: First international workshop cambridge, uk, may 30–june 1, 1996 proceedings,'' in _International Workshop on Information Hiding 1_. Springer, 1996.
  * [12] I.-K. Yeo and H. J. Kim, ``Modified patchwork algorithm: A novel audio watermarking scheme,'' _IEEE Transactions on speech and audio processing_ , vol. 11, no. 4, pp. 381–386, 2003.
  * [13] I. J. Cox, J. Kilian, F. T. Leighton, and T. Shamoon, ``Secure spread spectrum watermarking for multimedia,'' _IEEE transactions on image processing_ , vol. 6, no. 12, pp. 1673–1687, 1997.
  * [14] K. Pavlović, S. Kovačević, I. Djurović, and A. Wojciechowski, ``Robust speech watermarking by a jointly trained embedder and detector using a dnn,'' _Digital Signal Processing_ , vol. 122, p. 103381, 2022.
  * [15] C. Liu, J. Zhang, H. Fang, Z. Ma, W. Zhang, and N. Yu, ``Dear: A deep-learning-based audio re-recording resilient watermarking,'' in _Proceedings of the AAAI Conference on Artificial Intelligence_ , vol. 37, no. 11, 2023, pp. 13 201–13 209.
  * [16] G. Chen, Y. Wu, S. Liu, T. Liu, X. Du, and F. Wei, ``Wavmark: Watermarking for audio generation,'' _arXiv preprint arXiv:2308.12770_ , 2023.
  * [17] H. Zeinali, S. Wang, A. Silnova, P. Matějka, and O. Plchot, ``But system description to voxceleb speaker recognition challenge 2019,'' _arXiv preprint arXiv:1910.12592_ , 2019.
  * [18] H. Zen, V. Dang, R. Clark, Y. Zhang, R. J. Weiss, Y. Jia, Z. Chen, and Y. Wu, ``Libritts: A corpus derived from librispeech for text-to-speech,'' _arXiv preprint arXiv:1904.02882_ , 2019.
  * [19] A. W. Rix, J. G. Beerends, M. P. Hollier, and A. P. Hekstra, ``Perceptual evaluation of speech quality (pesq)-a new method for speech quality assessment of telephone networks and codecs,'' in _2001 IEEE international conference on acoustics, speech, and signal processing. Proceedings (Cat. No. 01CH37221)_ , vol. 2. IEEE, 2001, pp. 749–752.
  * [20] M. Chinen, F. S. Lim, J. Skoglund, N. Gureev, F. O'Gorman, and A. Hines, ``Visqol v3: An open source production ready objective speech and audio metric,'' in _2020 twelfth international conference on quality of multimedia experience (QoMEX)_. IEEE, 2020, pp. 1–6.
  * [21] H. Wang, C. Liang, S. Wang, Z. Chen, B. Zhang, X. Xiang, Y. Deng, and Y. Qian, ``Wespeaker: A research and production oriented speaker embedding learning toolkit,'' in _ICASSP 2023-2023 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP)_. IEEE, 2023, pp. 1–5.
  * [22] C. H. Taal, R. C. Hendriks, R. Heusdens, and J. Jensen, ``A short-time objective intelligibility measure for time-frequency weighted noisy speech,'' in _2010 IEEE international conference on acoustics, speech and signal processing_. IEEE, 2010, pp. 4214–4217.
  * [23] W.-N. Hsu, B. Bolte, Y.-H. H. Tsai, K. Lakhotia, R. Salakhutdinov, and A. Mohamed, ``Hubert: Self-supervised speech representation learning by masked prediction of hidden units,'' _IEEE/ACM Transactions on Audio, Speech, and Language Processing_ , vol. 29, pp. 3451–3460, 2021.