$\Gamma~{}{\color[rgb]{0.0600000000000001,0.46,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.0600000000000001,0.46,1}\pgfsys@color@cmyk@stroke{0.94}{0.54}{0}{0}\pgfsys@color<EMAIL_ADDRESS>we can get two normal forms
$t_{nf}=\operatorname{{\color[rgb]{0.0600000000000001,0.46,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.0600000000000001,0.46,1}\pgfsys@color@cmyk@stroke{0.94}{0.54}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and
$u_{nf}=\operatorname{{\color[rgb]{0.0600000000000001,0.46,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.0600000000000001,0.46,1}\pgfsys@color@cmyk@stroke{0.94}{0.54}{0}{0}\pgfsys@color<EMAIL_ADDRESS>and test them for equality up-to $\alpha$-conversion (which is a simple
syntactic check in our nameless representation in Agda).

If $t_{nf}=u_{nf}$ then the soundness result allows us to conclude that $t$
and $u$ are convertible terms.

If $t_{nf}\neq u_{nf}$ then $t$ and $u$ are not convertible. Indeed, if they
were then the completeness result guarantees us that $t_{nf}$ and $u_{nf}$
would be equal which leads to a contradiction.

######  Example 5.20.

of terms which are identified thanks to the internalization of the
$\nu$-rules.

  1. 1.

In a context with two functions $f$ and $g$ of type
$\sigma~{}{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`}\rightarrow}~{}{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color<EMAIL_ADDRESS>$\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`}\lambda}}xs.\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`map}}}(f,xs)$
and
$\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`}\lambda}}xs.\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`map}}}(g,xs)$
both normalize to
$\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`}\lambda}}xs.\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`map}}}(\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`}\lambda}}\\_.\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`\langle\rangle}}},xs)\operatorname{~{}{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`++}}~{}}\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color<EMAIL_ADDRESS>and are therefore declared equal.

  2. 2.

At type
$\Gamma~{}{\color[rgb]{0.0600000000000001,0.46,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.0600000000000001,0.46,1}\pgfsys@color@cmyk@stroke{0.94}{0.54}{0}{0}\pgfsys@color@cmyk@fill{0.94}{0.54}{0}{0}\vdash}~{}{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`list}}~{}({\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`\alpha}_{k}}~{}{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`}\times}~{}{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`\alpha}_{l}}})~{}{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`}\rightarrow}~{}{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`list}}~{}({\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`\alpha}_{k}}~{}{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`}\times}~{}{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`\alpha}_{l}}})}$,
the terms
$\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color<EMAIL_ADDRESS>and
$\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`}\lambda}}xs.\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`map}}}(swap,\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`map}}}(swap,xs))$
where $swap$ is the function
$\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`}\lambda}}p.(\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`\operatorname{\pi_{2}}}}}p\operatorname{~{}{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`,}}~{}}\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`\operatorname{\pi_{1}}}}}p)$
swapping the order of a pair’s elements are convertible with normal form
$\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`}\lambda}}xs.\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`map}}}(\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`}\lambda}}p.(\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`\operatorname{\pi_{1}}}}}p\operatorname{~{}{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`,}}~{}}\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`\operatorname{\pi_{2}}}}}p),xs)\operatorname{~{}{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`++}}~{}}\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color<EMAIL_ADDRESS>
##  6 Scaling up to Type Theory

Now that we know for sure that the judgmental equality can be safely extended
with some $\nu$-rules, we are ready to tackle more complex type theories. We
have already experimented with extending our simply-typed setting to a
universe of polynomial datatypes with map and fold. We have to identify which
parts of the setting are key to the success of this technique and how to
enforce that the generalized version still has good properties.

#### Types

Arrow types will be replaced by $\Pi$-types and product types by
$\Sigma$-types but the basic machinery of evaluation and type-directed
$\eta$-expansion work in much the same way.

In Type Theory, it is not quite enough to be able to decide the judgmental
equality. Pollack’s PhD thesis (Pollack [1994], Section 5.3.1), taught us how
to turn the typing relation with a conversion rule into a syntax-directed
typechecking algorithm by relying on ordinary evaluation (cf. the application
typing rule in Figure 9). It is therefore quite crucial for ensuring the
reusability of previous typechecking algorithms to be able to guarantee that
ordinary evaluation is complete for uncovering constructor-headed terms i.e.
$\Gamma\vdash t\equiv C~{}\vec{t_{i}}\colon T$ should imply that
$t\leadsto^{\star}C~{}\vec{t_{i}}^{\prime}$. This can be enforced by making
sure that candidates for $\nu$-rules are only reorganizing spines of stuck
eliminators and are absolutely never emitting new constructors.

$\displaystyle\displaystyle{\hbox{\hskip
135.91005pt\vbox{\hbox{\hskip-135.91003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
f\colon F\qquad F\leadsto^{\star}(x:S)\rightarrow T$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash s\colon
S^{\prime}$}\hskip
20.00003pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash S\equiv
S^{\prime}\colon\mathtt{Set}$}}}}}\vbox{}}}\over\hbox{\hskip
34.77243pt\vbox{\vbox{}\hbox{\hskip-34.77243pt\hbox{\hbox{$\displaystyle\displaystyle\Gamma\vdash
fs\colon T[s/x]$}}}}}}$ Figure 9: Syntax-directed typing rule for application,
Pollack Pollack [1994]

####  $\eta$-rules

A Type Theory does not need to have judgmental $\eta$-rules for the
$\nu$-rules to make sense. However this partially defeats the purpose of this
extension: without $\eta$-rules for products we fail to identify the silly
identity on lists of products map swap . map swap with the more traditional
one $\lambda x.x$ because
$f_{1}=\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color<EMAIL_ADDRESS>is different from
$f_{2}=\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`}\lambda}}x.(\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`\operatorname{\pi_{1}}}}}x\operatorname{~{}{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`,}}~{}}\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`\operatorname{\pi_{2}}}}}x)$
when both terms would reduce respectively to
$\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`}\lambda}}x.\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`map}}}{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\langle}f_{1}{~{}\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12},~{}}x{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\rangle\operatorname{~{}{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`++}}~{}}}\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color<EMAIL_ADDRESS>and
$\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`}\lambda}}x.\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`map}}}{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\langle}f_{2}{~{}\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12},~{}}x{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\rangle\operatorname{~{}{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`++}}~{}}}\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color<EMAIL_ADDRESS>So close yet so far away!

#### Defined symbols

In this presentation, a handful of functions are built-in rather than user-
defined. This will probably be one of the biggest changes when moving to a
usable Type Theory. We can enforce that functions defined by pattern-matching
have a fixed arity and are always fully applied at that arity. Such a function
is stuck if it is strict in a neutral argument. Some type theories reduce
pattern matching to the primitive elimination operator for each datatype. To
apply $\nu$-rules, we need to detect which stuck eliminators correspond to
which stuck pattern matches. This is the same problem as producing readable
output from normalizing open terms, and it has already been solved by the
‘labelled type’ translation used in Epigram, which effectively inserts
documentation of stuck pattern matches into spines of stuck eliminators
McBride and McKinna [2004].

#### Criteria for $\nu$-rules

Working in a setting where the datatypes are given by a universe Chapman et
al. [2010], we should at least expect that built-in generic operators, e.g.
map, have associated $\nu$-rules. However, it is clearly desirable to allow
the programmer to propose $\nu$-rules for programs of her own construction.
How will the machine check that proposed $\nu$-rules keep evaluation canonical
and judgmental equality consistent and decidable? We have already seen that
$\nu$-rules must avoid to emit new constructors; this can be summed up by the
mantra: “A $\nu$-rule may restart computation _within_ its contractum but
_never_ in its enclosing context”.

The candidates for $\nu$-rules should hold trivially by a Boyer-Moore style
induction; in other words, the $\beta\delta\iota-\nu$ critical pairs should be
convergent. This tells us that these rules are consistent and can be delayed
until after evaluation.

Obviously, the $\nu-\nu$ critical pairs should also be convergent. These three
criteria are all easy to check provided that $\nu$-reductions give rise to a
terminating term rewrite system.

This termination requirement is the last criterion. As a first instance, a
rather conservative approach could be to ask the user for a linear order on
defined symbols which we would lift to expressions by using the lexicographic
ordering of the encountered defined symbols starting from the “nut” and going
outwards. If this ordering is compatible with a left to right orientation of
the $\nu$-rules she wants to hold, then it is terminating. In the set of
$\nu$-rules used as an example in this paper, the simple ordering
$\operatorname{~{}{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`++}}~{}}>\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color@cmyk@fill{0.91}{0}{0.88}{0.12}\mathtt{`map}}}>\operatorname{{\color[rgb]{0,0.88,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0.88,0}\pgfsys@color@cmyk@stroke{0.91}{0}{0.88}{0.12}\pgfsys@color<EMAIL_ADDRESS>is compatible with the rules.

##  7 Further Opportunities for $\nu$-Rules

We were motivated to develop a proof technique for extending definitional
equality with $\nu$-rules because there are many opportunities where we might
profit by doing so. Let us set out a prospectus.

#### Reflexive coercion for type-based equality.

Altenkirch, McBride and W. Swierstra developed a propositional equality for
intensional type theory Altenkirch et al. [2007] which differs from the usual
inductive definition ($\mathtt{refl~{}a~{}:~{}a~{}=~{}a}$) in that its main
eliminator

$\displaystyle\displaystyle{\hbox{\hskip
60.25812pt\vbox{\hbox{\hskip-60.2581pt\hbox{\hbox{$\displaystyle\displaystyle
S,T:\mathtt{Set}\quad Q:S=T\quad s:S$}}}\vbox{}}}\over\hbox{\hskip
33.82764pt\vbox{\vbox{}\hbox{\hskip-33.82764pt\hbox{\hbox{$\displaystyle\displaystyle
s[Q:S=T\rangle:T$}}}}}}$

computes by structural recursion first on the _types_ $S$ and $T$, and then
(where appropriate) on $s$, rather than by pattern matching on the proof $Q$.
Equality is still reflexive, so evaluation can leave us with terms
$n[\mathtt{refl}\>n:N=N\rangle:N$ where $n$ is a neutral term in a neutral
type $N$. It is clearly a nuisance that this term does not compute to $n$, as
would happen if the eliminator matched on the proof. The fix is to add a
$\nu$-rule which discards coercions whenever it is type-safe to do so:

$\framebox{{\raisebox{0.0pt}[5.78172pt][1.4457pt]{\framebox{{\raisebox{0.0pt}[4.33601pt][0.0pt]{$s$}}}$[Q:S=T\rangle$}}}=\framebox{{\raisebox{0.0pt}[4.33601pt][0.0pt]{$s$}}}\qquad\mbox{if}\;S\equiv
T:\mathtt{Set}$

It is easy to check that adding this rule for neutral terms makes it
admissible for all terms, and hence that we need add it not to evaluation, but
only to the reification process which follows, just as with the $\nu$-rules in
this paper. There, as here, this spares the evaluation process from decisions
which involve $\eta$-expansion and thus require a name supply. The $\nu$-rule
thus gives us a non-disruptive means to respect the full computational
behaviour of inductive equality in the observational setting.

#### Functor laws.

Barral and Soloviev give a treatment of functor laws for parametrized
inductive datatypes by modifying the $\iota$-rules of their underlying type
theory Barral and Soloviev [2006]. We should very much hope to achieve the
same result, as we did here in the special case of lists, just by adding
$\nu$-rules. Our preliminary experiments McBride [2010] suggest that we can
implement functor laws once and for all in a type theory whose datatypes are
given once and for all by a syntactic encoding of strictly positive functors,
as Dagand and colleagues propose Chapman et al. [2010]; Dagand and McBride
[2012]. Moreover, Luo and Adams have shown Luo and Adams [2008] that
structural subtyping for inductive types can be reified by a coherent system
of implicit coercions if functor laws hold definitionally.

#### Monad laws.

Watkins et al. give a definitional treatment of monad laws in order to achieve
an adequate representation of concurrent processes encapsulated monadically in
a logical framework Watkins et al. [2003]. For straightforward free monads, an
experimental extension of Epigram (by Norell, as it happens) McBride [2010]
suggests that we may readily allow $\nu$-rules:

$\framebox{{\raisebox{0.0pt}[5.78172pt][1.4457pt]{$\framebox{{\raisebox{0.0pt}[4.33601pt][0.0pt]{$t$}}}>\\!\\!>\\!\\!=\mathtt{return}$}}}=\framebox{{\raisebox{0.0pt}[4.33601pt][0.0pt]{$t$}}}\qquad\framebox{{\raisebox{0.0pt}[7.22743pt][2.8903pt]{$\framebox{{\raisebox{0.0pt}[5.78172pt][1.4457pt]{$(\framebox{{\raisebox{0.0pt}[4.33601pt][0.0pt]{$t$}}}>\\!\\!>\\!\\!=\sigma)$}}}>\\!\\!>\\!\\!=\rho$}}}=\framebox{{\raisebox{0.0pt}[5.78172pt][1.4457pt]{$\framebox{{\raisebox{0.0pt}[4.33601pt][0.0pt]{$t$}}}>\\!\\!>\\!\\!=((>\\!\\!>\\!\\!=\sigma)\cdot\rho)$}}}$

Atkey’s Foveran system uses a similar normalization method for free monad laws
Atkey [2011], again for an encoded universe of underlying functors.

#### Decomposing functors.

Dagand and colleagues further note that their syntax of descriptions for
indexed functors is, by virtue of being a syntax, itself presentable as the
free monad of a functor. The description decoder

$\mathtt{Decode}:\mathtt{IDesc}\>I\to(I\to\mathtt{Set})\to\mathtt{Set}$

is structurally recursive in the description and lifts pointwise to an
interpretation of substitutions in the $\mathtt{IDesc}$ monad

$\begin{array}[]{l}\llbracket\\_\rrbracket:(O\to\mathtt{IDesc}\>I)\;\;\to\;\;(I\to\mathtt{Set})\to(O\to\mathtt{Set})\\\
\llbracket\sigma\rrbracket\>X\>o=\mathtt{Decode}\>(\sigma\>o)\>X\end{array}$

as indexed functors with a ‘map’ operation satisfying functor laws. However,
not only does this interpretation _deliver_ functors, it is _itself_ a
contravariant functor: the identity substitution yields the identity functor
just by $\beta\delta\iota$, but we may also interpret Kleisli composition as
reverse functor composition

$\llbracket(>\\!\\!>\\!\\!=\sigma)\cdot\rho\rrbracket=\llbracket\rho\rrbracket\cdot\llbracket\sigma\rrbracket$

by means of a $\nu$-rule

$\framebox{{\raisebox{0.0pt}[7.22743pt][2.8903pt]{Decode~{}\framebox{{\raisebox{0.0pt}[5.78172pt][1.4457pt]{$(\framebox{{\raisebox{0.0pt}[4.33601pt][0.0pt]{$D$}}}>\\!\\!>\\!\\!=\sigma)$}}}~{}$X$}}}=\framebox{{\raisebox{0.0pt}[5.78172pt][1.4457pt]{Decode~{}\framebox{{\raisebox{0.0pt}[4.33601pt][0.0pt]{$D$}}}~{}$(\llbracket\sigma\rrbracket\>X)$}}}$

taking each $D$ to be some $\rho\>o$. If we want to do a ‘scrap your
boilerplate’ style traversal of some described container-like structure, we
need merely exhibit the decomposition of the description as some
$(>\\!\\!>\\!\\!=\sigma)\cdot\rho$, where $\rho$ describes the invariant
superstructures and $\sigma$ the modified substructures, then invoke the
functoriality of $\llbracket\rho\rrbracket$. This $\nu$-rule thus lets us
expose functoriality over substructures not anticipated by explicit
parametrization in datatype declarations. We thus recover the kind of ad-hoc
data traversal popularized by Lämmel and Peyton Jones Lämmel and Jones [2003]
by static structural means.

#### Universe embeddings.

A type theory with inductive-recursive definitions is powerful enough to
encode universes of dependent types by giving a datatype of codes _in tandem_
with their interpretations Dybjer and Setzer [1999], the paradigmatic example
being

$\begin{array}[]{@{}l@{\;}|@{\;}l@{}}\mathtt{U}_{1}:\mathtt{Set}&\mathtt{El}_{1}:\mathtt{U}_{1}\to\mathtt{Set}\\\
\mathtt{`Pi}_{1}:(S:\mathtt{U}_{1})\to&\mathtt{El}_{1}\>(\mathtt{`Pi}_{1}\>S\>T)=\\\
\qquad\qquad(\mathtt{El}_{1}\>S\to\mathtt{U}_{1})\to\mathtt{U}_{1}&\;\;(s:\mathtt{El}_{1}\>S)\to\mathtt{El}_{1}\>(T\>s)\\\
\vdots&\vdots\end{array}$

Palmgren Palmgren [1998] suggests that one way to model a cumulative hierarchy
of such universes is to give each a code in the next, so

$\begin{array}[]{@{}l@{\;}|@{\;}l@{}}\mathtt{U}_{2}:\mathtt{Set}&\mathtt{El}_{2}:\mathtt{U}_{2}\to\mathtt{Set}\\\
\mathtt{`U}_{1}:\mathtt{U}_{2}&\mathtt{El}_{2}\>\mathtt{`U}_{1}=\mathtt{U}_{1}\\\
\mathtt{`Pi}_{2}:(S:\mathtt{U}_{2})\to&\mathtt{El}_{2}\>(\mathtt{`Pi}_{2}\>S\>T)=\\\
\qquad\qquad(\mathtt{El}_{2}\>S\to\mathtt{U}_{2})\to\mathtt{U}_{2}&\;\;(s:\mathtt{El}_{2}\>S)\to\mathtt{El}_{2}\>(T\>s)\\\
\vdots&\vdots\end{array}$

and then define an embedding recursively

$\begin{array}[]{l}\uparrow:\mathtt{U}_{1}\to\mathtt{U}_{2}\\\
\uparrow(\mathtt{`Pi}_{1}\>S\>T)=\mathtt{`Pi}_{2}\>(\uparrow S)\>(\lambda
s.\>\uparrow(T\>s))\end{array}$

but a small frustration with this proposal is that $s$ is abstracted at type
$\mathtt{El}_{2}\>(\uparrow S))$, but used at type $\mathtt{El}_{1}\>S$, and
these two types are not definitionally equal for an abstract $S$. One
workaround is to make $\uparrow$ a constructor of $\mathtt{U}_{2}$, at the
cost of some redundancy of representation, but now we might also consider
fixing the discrepancy with a $\nu$-rule

$\framebox{{\raisebox{0.0pt}[7.22743pt][2.8903pt]{$\mathtt{El}_{2}\>\framebox{{\raisebox{0.0pt}[5.78172pt][1.4457pt]{$(\uparrow\framebox{{\raisebox{0.0pt}[4.33601pt][0.0pt]{$S$}}})$}}})$}}}=\framebox{{\raisebox{0.0pt}[5.78172pt][1.4457pt]{$\mathtt{El}_{1}\>\framebox{{\raisebox{0.0pt}[4.33601pt][0.0pt]{$S$}}}$}}}$

This is peculiar for our examples thus far, in that the $\nu$-rule is needed
even to typecheck the $\delta\iota$-rules for $\uparrow$, reflecting the fact
that $\uparrow$ should not be any old function from $\mathtt{U}_{1}$ to
$\mathtt{U}_{2}$, but rather one which preserves the meanings given by
$\mathtt{El}_{1}$ and $\mathtt{El}_{2}$. In effect, the $\nu$-rule is
expressing the coherence property of a richer notion of morphism. It is
inviting to wonder what other notions of coherence we might enable and enforce
by checking that $\nu$-rules hold of the operations we implement.

#### Non-examples.

A key characteristic of a $\nu$-rule is that it is a nut-preserving
rearrangement of neutral term layers. Whilst this is good for associativity
and sometimes for distributivity, it is perfectly useless for commutativity.
Suppose $+$ for natural numbers is recursive on its first argument, and
observe that rewriting $x+y$ to $y+x$ when $x$ is neutral will not result in a
neutral term unless $y$ is also neutral. Less ambitious rules such as
$x+\mathtt{suc}\>y=\mathtt{suc}\>(x+y)$ and $x*0=0$ similarly make neutral
terms come unstuck, and so cannot be postponed until reification if we want to
be sure that evaluation suffices to show whether any expression in a datatype
can be put into constructor-headed form. Walukiewicz-Chrzaszcz has proposed a
more invasive adoption of rewriting for Coq, necessitating a modified
evaluator, but incorporating rules which can expose constructors Walukiewicz-
Chrzaszcz [2003]. Her untyped rewriting approach sits awkwardly with
$\eta$-laws, but we can find a more carefully structured compromise.

##  8 Discussion

We fully expect to scale this technology up to type theory. Abel and Dybjer
(with Aehlig Abel et al. [2007a] and T. Coquand Abel et al. [2007b]) have
already given normalization by evaluation algorithms which we plan to adapt.

Finding good criteria for checking that candidate $\nu$-rules can safely be
added is of the utmost importance. We want to let the programmer negotiate the
new $\nu$-rules she wants, as long as the machine can check that they yield a
notion of standard form and lift from neutral terms to all terms by the prior
equational theory.

It is also interesting to try to integrate $\nu$-rules with more practical
presentations of normalization. For instance Grégoire and Leroy’s conversion
by compilation to a bytecode machine derived from Ocaml’s ZAM Grégoire and
Leroy [2002] decides $\eta$ by expansion only when provoked by a $\lambda$:
such laziness is desirable when possible but causes trouble with $\eta$-rules
for unit types and may conceal the potential to apply $\nu$-rules. Hereditary
substitution Watkins et al. [2003], formalized by Abel Abel [2009] and by
Keller and Altenkirch Keller and Altenkirch [2010], may be easier to adapt.

## Acknowledgements

We would like to thank the anonymous reviewers for their helpful comments and
suggestions as well as Stevan Andjelkovic for carefully reading our draft.

## References

  * Abel [2009] A. Abel.  Implementing a normalizer using sized heterogeneous types.  _Journal of Functional Programming_ , 19(3-4):287–310, 2009.
  * Abel et al. [2007a] A. Abel, K. Aehlig, and P. Dybjer.  Normalization by evaluation for Martin-Löf type theory with one universe.  _Electr. Notes Theor. Comput. Sci_ , 173:17–39, 2007a.
  * Abel et al. [2007b] A. Abel, T. Coquand, and P. Dybjer.  Normalization by evaluation for Martin-Löf type theory with typed equality judgements.  In _LICS_ , pages 3–12. IEEE Computer Society, 2007b.
  * Ahman [2012] D. Ahman.  Computational effects, algebraic theories and normalization by evaluation.  Master’s thesis, University of Cambridge, June 2012.
  * Ahman and Sam [2013] D. Ahman and S. Sam.  Normalization by evaluation and algebraic effects.  In _29th Conference on Mathematical Foundations of Programming Semantics, MFPS XXIX, New Orleans, LA, June 2013_ , 2013.
  * Allais [2012] G. Allais.  Forge crowbars, Acquire normal forms.  Technical report, University of Strathclyde, 2012.  URL http://gallais.org/pdf/report2012.pdf.
  * Allais [2013] G. Allais.  Glueing terms to models - variations on nbe.  Slides, May 2013.  URL http://gallais.org/pdf/awayday13.pdf.
  * Altenkirch and Reus [1999] T. Altenkirch and B. Reus.  Monadic presentations of lambda terms using generalized inductive types.  In _CSL_ , pages 453–468, 1999.
  * Altenkirch et al. [2007] T. Altenkirch, C. McBride, and W. Swierstra.  Observational equality, now!  In A. Stump and H. Xi, editors, _PLPV_ , pages 57–68. ACM, 2007.
  * Atkey [2011] R. Atkey.  A type checker that knows its monad from its elbow.  Blog post, December 2011.  URL http://bentnib.org/posts/2011-12-14-type-checker.html.
  * Barral and Soloviev [2006] F. Barral and S. Soloviev.  Inductive type schemas as functors.  In D. Grigoriev, J. Harrison, and E. A. Hirsch, editors, _CSR_ , volume 3967 of _Lecture Notes in Computer Science_ , pages 35–45. Springer, 2006.
  * Berger and Schwichtenberg [1991] U. Berger and H. Schwichtenberg.  An inverse of the evaluation functional for typed lambda-calculus.  In _LICS: IEEE Symposium on Logic in Computer Science_ , 1991.
  * Boutillier [2009] P. Boutillier.  Equality for lambda-terms with list primitives.  Internship report, University of Strathclyde, ENS Lyon, July 2009.
  * Boyer and Moore [1975] R. S. Boyer and J. S. Moore.  Proving theorems about LISP functions.  _J. ACM_ , 22(1):129–144, Jan. 1975.
  * Chapman et al. [2005] J. Chapman, T. Altenkirch, and C. McBride.  Epigram reloaded: a standalone typechecker for ETT.  In M. C. J. D. van Eekelen, editor, _Trends in Functional Programming_ , volume 6 of _Trends in Functional Programming_ , pages 79–94. Intellect, 2005.
  * Chapman et al. [2010] J. Chapman, P.-E. Dagand, C. McBride, and P. Morris.  The gentle art of levitation.  _SIGPLAN Not._ , 45(9):3–14, Sept. 2010.
  * Chapman [2009] J. M. Chapman.  _Type checking and normalisation_.  PhD thesis, University of Nottingham, 2009.
  * Coquand [2002] C. Coquand.  A formalised proof of the soundness and completeness of a simply typed lambda-calculus with explicit substitutions.  _Higher-Order and Symbolic Computation_ , 15(1):57–90, 2002.
  * Coquand and Dybjer [1997] T. Coquand and P. Dybjer.  Intuitionistic model constructions and normalization proofs.  _Mathematical. Structures in Comp. Sci._ , 7:75–94, Feb. 1997.  ISSN 0960-1295.
  * Dagand and McBride [2012] P.-E. Dagand and C. McBride.  Elaborating Inductive Definitions.  _ArXiv e-prints_ , Oct. 2012.
  * Danielsson [2007] N. A. Danielsson.  A formalisation of a dependently typed language as an Inductive-Recursive family.  In T. Altenkirch and C. McBride, editors, _Types for Proofs and Programs_ , volume 4502 of _Lecture Notes in Computer Science_ , pages 93–109. Springer Berlin Heidelberg, 2007.
  * Danvy [1999] O. Danvy.  Type-directed partial evaluation.  In J. Hatcliff, T. Mogensen, and P. Thiemann, editors, _Partial Evaluation_ , volume 1706 of _Lecture Notes in Computer Science_ , chapter 16, pages 367–411. Springer Berlin / Heidelberg, Berlin, Heidelberg, 1999\.
  * de Bruijn [1972] N. G. de Bruijn.  Lambda Calculus notation with nameless dummies: a tool for automatic formula manipulation.  _Indagationes Mathematicæ_ , 34:381–392, 1972.
  * Dybjer and Setzer [1999] P. Dybjer and A. Setzer.  A finite axiomatization of inductive-recursive definitions.  In J.-Y. Girard, editor, _TLCA_ , volume 1581 of _Lecture Notes in Computer Science_ , pages 129–146. Springer, 1999.
  * Filinski [2001] A. Filinski.  Normalization by evaluation for the computational Lambda-Calculus.  In S. Abramsky, editor, _Typed Lambda Calculi and Applications_ , volume 2044 of _Lecture Notes in Computer Science_ , chapter 15, pages 151–165. Springer Berlin / Heidelberg, Berlin, Heidelberg, Apr. 2001.
  * Girard [2006] J. Girard.  _Le Point Aveugle: Cours de logique: Tome 1, Vers la perfection_.  Hermann, 2006.
  * Grégoire and Leroy [2002] B. Grégoire and X. Leroy.  A compiled implementation of strong reduction.  _SIGPLAN Not._ , 37(9):235–246, 2002.
  * [28] INRIA.  The Coq proof assistant.
  * Keller and Altenkirch [2010] C. Keller and T. Altenkirch.  Hereditary substitutions for simple types, formalized.  In _Proceedings of the third ACM SIGPLAN workshop on Mathematically structured functional programming_ , MSFP ’10, pages 3–10, New York, NY, USA, 2010. ACM.
  * Lämmel and Jones [2003] R. Lämmel and S. L. P. Jones.  Scrap your boilerplate: a practical design pattern for generic programming.  In Z. Shao and P. Lee, editors, _TLDI_ , pages 26–37. ACM, 2003.  ISBN 1-58113-649-8.
  * Luo and Adams [2008] Z. Luo and R. Adams.  Structural subtyping for inductive types with functorial equality rules.  _Mathematical Structures in Computer Science_ , 18(5):931–972, 2008.
  * McBride [2010] C. McBride.  Outrageous but meaningful coincidences: dependent type-safe syntax and evaluation.  In _Proceedings of the 6th ACM SIGPLAN workshop on Generic programming_ , WGP ’10, New York, NY, USA, 2010. ACM.
  * McBride [2010] C. McBride.  EE-PigWeek 4-9 Jan 2010.  Blog post, January 2010.  URL http://www.e-pig.org/epilogue/?p=306.
  * McBride and McKinna [2004] C. McBride and J. McKinna.  The view from the left.  _J. Funct. Program._ , 14(1):69–111, Jan. 2004\.
  * Norell [2008] U. Norell.  Dependently typed programming in Agda.  In P. W. M. Koopman, R. Plasmeijer, and S. D. Swierstra, editors, _Advanced Functional Programming_ , volume 5832 of _Lecture Notes in Computer Science_ , pages 230–266. Springer, 2008.
  * Palmgren [1998] E. Palmgren.  On Universes in Type Theory.  In G. Sambin and J. Smith, editors, _Twenty Five Years of Constructive Type Theory_. Oxford Univ. Press, 1998.
  * Pollack [1994] R. Pollack.  _The theory of LEGO – a proof checker for the extendend calculus of constructions_.  PhD thesis, University of Edinburgh, 1994.
  * Walukiewicz-Chrzaszcz [2003] D. Walukiewicz-Chrzaszcz.  Termination of rewriting in the calculus of constructions.  _J. Funct. Program._ , 13(2):339–414, 2003.
  * Watkins et al. [2003] K. Watkins, I. Cervesato, F. Pfenning, and D. Walker.  A concurrent logical framework: The propositional fragment.  In S. Berardi, M. Coppo, and F. Damiani, editors, _TYPES_ , volume 3085 of _Lecture Notes in Computer Science_ , pages 355–377. Springer, 2003.


# Deep Learning-Based Signal Detection for Dual-Mode Index Modulation 3D-OFDM

Dang-Y Hoang, Tien-Hoa Nguyen, Vu-Duc Ngo, Trung Tan Nguyen, Nguyen Cong
Luong, and Thien Van Luong Dang-Y Hoang, Tien-Hoa Nguyen, and Vu-Duc Ngo are
with the School of Electrical and Electronics Engineering, Hanoi University of
Science and Technology, Hanoi, Vietnam (e-mail<EMAIL_ADDRESS>{hoa.nguyentien,duc.ngovu }@hust.edu.vn.)Trung Tan Nguyen is with the Faculty
of Radio-Electronics, Le Quy Don Technical University, Ha Noi 11355, Vietnam
(e-mail: trungtannguyen@mta.edu.vn).Thien Van Luong and Nguyen Cong Luong are
with the Faculty of Computer Science, Phenikaa University, Hanoi 12116,
Vietnam (e-mail: {thien.luongvan, luong.nguyencong}@phenikaa-uni.edu.vn).

###### Abstract

In this paper, we propose a deep learning-based signal detector called
DuaIM-3DNet for dual-mode index modulation-based three-dimensional (3D)
orthogonal frequency division multiplexing (DM-IM-3D-OFDM). Herein, DM-
IM-3D-OFDM is a subcarrier index modulation scheme which conveys data bits via
both dual-mode 3D constellation symbols and indices of active subcarriers.
Thus, this scheme obtains better error performance than the existing IM
schemes when using the conventional maximum likelihood (ML) detector, which,
however, suffers from high computational complexity, especially when the
system parameters increase. In order to address this fundamental issue, we
propose the usage of a deep neural network (DNN) at the receiver to jointly
and reliably detect both symbols and index bits of DM-IM-3D-OFDM under
Rayleigh fading channels in a data-driven manner. Simulation results
demonstrate that our proposed DNN detector achieves near-optimal performance
at significantly lower runtime complexity compared to the ML detector.

###### Index Terms:

DuaIM-3DNet, deep learning, bit error rate, DNN, dual mode, index modulation,
DM-IM-3D-OFDM.

##  I Introduction

Orthogonal frequency division multiplexing (OFDM) with index modulation OFDM-
IM [1, 2] has recently materialized as a promising multicarrier modulation
candidate to substitute the traditional OFDM. In contrast to OFDM, only a
portion of subcarriers are activated in OFDM-IM, where additional information
bits are virtually carried using the indices of activated sub-carriers, while
other information bits are physically conveyed on the classical $M$-ary
symbols modulated over these activated sub-carriers. As a result, OFDM-IM
outperforms the conventional OFDM in terms of reliability and energy
efficiency, particularly a promising trade-off between reliability and
spectral efficiency performance through adjusting the number of activated sub-
carriers.

A variety of cutting-edge IM-based systems have been developed over the years.
For instance, a tight bound on the bit error rate (BER) of the low-complexity
greedy detector was derived in [3], while study in [2] examined its symbol
error probability (SEP) when using different detection types such as the
maximum likelihood (ML) and GD detectors. The outage probability of OFDM-IM
using the GD detector was first analyzed in [4]. The combination of OFDM-IM
with multiple antennas was introduced in [5]. The BER performance of OFDM-IM
in presence of maximal-ratio combiner (MRC) for enhancing diversity was
investigated in [6]. Since then, a range of techniques has been applied to
either increase the spectral efficiency (SE) or reduce the BER of the OFDM-IM
system. In particular, in order to improve SE, the IM concept is applied to
both in-phase and quadrature (I/Q) parts for doubling the number of index
bits. A low-complexity ML detector and the performance analysis for this
system were also reported. Additionally, the dual mode OFDM (DM-OFDM), which
employs several constellations to transmit data bits using inactive
subcarriers of OFDM-IM, was proposed in [7]. It was demonstrated that at the
penalty of degraded error performance, DM-OFDM can attain higher SE than OFDM-
IM. In [8], a generalized variant of DM-OFDM that vastly improves the SE over
the original version was proposed. Other methods for increasing diversity of
OFDM-IM were reported in [9, 10, 11], which considerably improve BER
performance, especially in high signal-to-noise ratio (SNR) regions.

Aiming at improving the error performance of the classical OFDM, three-
dimensional (3D) constellation and OFDM were combined to form 3D-OFDM in [12].
With 3D-OFDM, data bits are mapped into a 3D constellation and the 3D signals
are divided into sub-carriers, which are modulated using the 2D inverse fast
Fourier transform (IFFT). In comparison with OFDM with the 2D mapper, the 3D
mapper considerably increases the minimum Euclidean distance (MED) between the
various constellations, leading to improved error performance. In [13] and
[14], the theoretical SEP analysis and the peak-to-average power ratio (PAPR)
reduction method of the 3D-OFDM were respectively presented. However, when the
constellation order, SE of 3D-OFDM is only one-third that of traditional OFDM
[15]. Inspired by dual-mode OFDM [7], a novel IM-based scheme called dual-mode
index modulation assisted 3D-OFDM (DM-IM-3D-OFDM) was proposed in [16] to
improve SE of 3D-OFDM. In this scheme, subcarriers are separated into several
sub-blocks and subcarriers in each sub-block are partitioned into two groups,
then modulated by designed dual-mode 3-D constellations based on the floor of
the Poincare sphere [17]. Compared to 3D-OFDM, DM-IM-3D-OFDM provides better
BER performance at high SNRs under fading channels when the optimal ML
detector is employed. However, this conventional detector suffers from high
computational complexity, especially when the system parameters increase. This
paper appears to address this fundamental issue.

In particular, we propose a deep learning-based detector called DuaIM-3DNet
for DM-IM-3D-OFDM. More particularly, we design a novel deep neural network
(DNN) structure for DuaIM-3DNet which consists of two sub-networks called
IndexNet and SymbolNet for detecting active sub-carrier indices and 3D
constellation symbols. The outputs of these two sub-networks are then
concatenated to be fed into a final DNN transmitted bits using Sigmoid
function as the activation of the output layer. Note that before entering the
DNN architecture of our proposed DuaIM-3DNet, the received signal and channel
state information (CSI) are pre-processed based on the domain knowledge such
as zero-forcing (ZF) channel equalizer and energy detection [18]. DuaIM-3DNet
is trained offline using simulated dataset to minimize BER. Then, the trained
model can be deployed as an online detector for promptly detecting transmitted
data bits. Finally, our simulation results demonstrate that our DuaIM-3DNet
detector can provide a near-optimal error performance at much lower runtime
complexity in comparison with the ML detector.

Note that deep learning [19] in conjunction with DNNs has been widely adopted
to wireless communication systems, particularly in physical layer issues. For
example, deep learning was applied for detecting signals of OFDM-IM in [18].
Then, a range of studies, which apply deep learning to either improve the
error performance or reduce the complexity of OFDM-based multicarrier schemes
[20, 21, 22, 23]. Some other applications of deep learning to channel coding
as well as successive interference cancellation receivers of non-orthogonal
downlink can be found in [24] and [25], respectively.

The remaining parts of this paper are structured as follows. The DM-IM-3D-OFDM
system model is discussed in Section II, while Section III introduces the
proposed DuaIM-3DNet detector. Section IV provides simulation results and
discussion. Finally, Section V concludes our paper.

##  II DM-IM-3D-OFDM system model

First, we briefly describe a DM-IM-3D-OFDM system [16]. In DM-IM-3D-OFDM, the
information bits are mapped into two different types of 3-D constellations and
sub-carrier indices. Assume that $m$ information bits are divided into $u$
sub-blocks. Each sub-block contains $n$ sub-carriers and $p$ bits, i.e.
$u=m/p=N/n$, where $N$ is the total number of subcarriers. Then, $p$ bits will
be divided into two components. The first one consisting of $p_{1}$ bits is to
map the sub-carrier indices. The second component with $p_{2}$ bits is mapped
by two different constellations of type A and type B, denoted by
$\mathcal{C}_{A}$ and $\mathcal{C}_{B}$, respectively,
$\mathcal{C}_{A}\cap\mathcal{C}_{B}=\varnothing$. The number of signal points
of $\mathcal{C}_{A}$ and $\mathcal{C}_{B}$ are presented by $c_{A}$ and
$c_{B}$, respectively. We also assume that $k$ stands for the number of sub-
carriers mapped to $\mathcal{C}_{A}$, so the number of sub-carriers mapped to
$\mathcal{C}_{B}$ will be $n-k$. Then, $p_{1}$ and $p_{2}$ are calculated as
follows

$p_{1}=\lfloor\log_{2}C_{n}^{k}\rfloor,$ (1)
$p_{2}=\log_{2}((c_{A})^{k})+\log_{2}((c_{B})^{n-k}),$ (2)

where $C_{n}^{k}$ is the binomial coefficient and $\lfloor.\rfloor$ denotes
the integer floor operator. The number of information-carrying bits in each
sub-block is $p=p_{1}+p_{2}$. An example of the index mapping process is
illustrated in Table I.

TABLE I: Look-up table for index modulation with $n=4,p_{1}=2$ and $k=2$ Index Bits | Indices for $\mathcal{C}_{A}$ | Sub-block
---|---|---
$[0,0]$ | $[1,2]$ | $[A^{(1)},A^{(2)},B^{(1)},B^{(2)}]$
$[0,1]$ | $[2,3]$ | $[B^{(1)},A^{(1)},A^{(2)},B^{(2)}]$
$[1,0]$ | $[3,4]$ | $[B^{(1)},B^{(2)},A^{(1)},A^{(2)}]$
$[1,1]$ | $[1,4]$ | $[A^{(1)},B^{(1)},B^{(2)},A^{(2)}]$

Fig. 1 depicts the design for a basic DM-IM-3D-OFDM system with a block of
sub-carriers. The symbols transmitted in a block are expressed as the matrix
$\mathbf{X}\in\mathbb{C}^{3\times n}$, which is represented in the frequency
domain as $\mathbf{X}=[\mathbf{X}(1),\mathbf{X}(2),...\mathbf{X}(n)]$, where
$\mathbf{X}(\varphi)\in\left\\{\mathcal{C}_{A},\mathcal{C}_{B}\right\\}$,
$1\leq\varphi\leq n$. Note that the design of 3-D constellations for
constructing the symbol matrix $\mathbf{X}$ is detailed in [16]. The look-up
table in Table I may be used to create an $\mathbf{X}$ block. For each sub-
block, the channel impulse response (CIR) matrix of the Rayleigh fading
channel is shown in the frequency domain as follows

$\displaystyle\mathbf{H}=\begin{pmatrix}H_{11}&H_{12}&\ldots&H_{1n}\\\
H_{21}&H_{22}&\ldots&H_{2n}\\\
H_{31}&H_{32}&\ldots&H_{3n}\end{pmatrix}=\begin{pmatrix}\mathbf{H}_{1}\\\
\mathbf{H}_{2}\\\ \mathbf{H}_{3}\end{pmatrix},$ (3)

where
$\mathbf{H}=[\mathbf{H}_{1};\mathbf{H}_{2};\mathbf{H}_{3}]^{T}\in\mathbb{C}^{3\times
n}$ is matrix of size $3\times n$. and the components
$\mathbf{H}_{i}\in\mathbb{C}^{1\times n}$, $1\leq i\leq 3$, have the identical
and independent distribution with zero mean and unit variance.

Figure 1: Diagram of simple DM-IM-3D-OFDM.

The received signal matrix $\mathbf{Y}\in\mathbb{C}^{3\times n}$ is performed
as follows

$\mathbf{Y}=\mathbf{H}\mathbf{X}+\mathbf{Z},$ (4)

where $\mathbf{Z}$ denotes the additive white Gaussian noise (AWGN),
$\mathbf{Z}\in\mathbb{C}^{3\times n}$,
$\mathbf{Z}=[\mathbf{Z}_{1},\mathbf{Z}_{2},\mathbf{Z}_{3}]^{T}$ and the
components $\mathbf{Z}_{j}\in\mathbb{C}^{1\times n}$, $1\leq j\leq 3$, have
the identical and independent distribution with zero-mean and variance of
$N_{0}$.

##  III Proposed DuaIM-3DNet

This section describes the training process and online deployment of the
proposed DuaIM-3DNet detector and the neural network structure for our
detector is also presented.

###  III-A Structure of DuaIM-3DNet

The proposed DuaIM-3DNet structure is illustrated in Fig. 2 which consists of
two identical parallel sub-nets, namely IndexNet and SymbolNet. First, we use
a zero-forcing (ZF) channel equalizer to obtain the equalized received signal
as $\bar{\mathbf{Y}}=\mathbf{Y}\mathbf{H}^{-1}$. The channel matrix
$\mathbf{H}$ and the received signal matrix $\mathbf{Y}$ are known at the
receiver. The IndexNet is responsible for extracting index state
characteristics of carriers whose input is a vector, by flattening the
received signal’s energy matrix represented as $\mathbf{Y}_{E}$. The SymbolNet
is used for demapping the symbol modulation, whose input is the real imaginary
part vector by flattening the equalized signal matrix $\bar{\mathbf{Y}}$,
$\bar{\mathbf{Y}}_{R}$ and $\bar{\mathbf{Y}}_{I}$, respectively. In the second
step, outputs of the two sub-nets are concatenated and flattened into a new
one-dimensional feature, and then the two FC layers are used to recover the
transmitted message $\mathbf{b}$.

Figure 2: Structure of the proposed DuaIM-3DNet. |
---|---
Figure 3: Structure of IndexNet (a) and SymbolNet (b).

Each sub-net, i.e., IndexNet and SymbolNet, in DuaIM-3DNet consists of two
hidden layers. The number of nodes in the output layer is equal to the number
of predicted bits in each sub-block, i.e., $n_{\text{out}}=p$. Details of
IndexNet and SymbolNet parameters are shown in the Table II. In the hidden
layer, the Tanh function is used as the activation function
$f_{\text{Tanh}}(x)=\frac{e^{x}-e^{-x}}{e^{x}+e^{-x}}$. The sigmoid function
$f_{\text{Sig}}(x)=\frac{1}{1+e^{-x}}$ is used to map outputs in the interval
$(0,1)$. The IndexNet contains two FC layers that use the Tanh function, as
illustrated in Fig. 3(a). The numbers of nodes of two hidden layers are
$n_{\text{I1}}$ and $n_{\text{I2}}$, where $n_{\text{I2}}$ is the number of
output nodes of the network and the output of the network is performed by
$\mathbf{z}_{\text{index}}$. Similarly, the SymbolNet contains two FC layers
whose activation function is Tanh, as depicted in Fig. 3(b). It can be seen
from the figure that $n_{\text{S1}}$ and $n_{\text{S2}}$ are the numbers of
nodes of the FC layers. In particular, $n_{\text{S2}}$ is the number of output
nodes of the network, given that the output of the network is performed as
$\mathbf{z}_{\text{sym}}$. The output of IndexNet and SymbolNet will be used
as input of OutNet block.

TABLE II: Parameters of IndexNet, SymbolNet and OutNet with $\left(n,k,c_{A},c_{B}\right)=\left(4,2,2,2\right)$ Parameter | IndexNet | SymbolNet | OutNet
---|---|---|---
Input size | $n_{\text{I0}}=3n=12$ | $n_{\text{S0}}=6n=24$ | $n_{\text{I2}}+n_{\text{S2}}$
Output size | $n_{\text{I2}}$ | $n_{\text{S2}}$ | $p$
FC layer | 2 | 2 | 2
Hidden Nodes | $n_{\text{I1}},n_{\text{I2}}$ | $n_{\text{S1}},n_{\text{S2}}$ | $n_{Con},p$
Output activation | Tanh | Tanh | Sigmoid

Therefore, the final output can be performed as follows

$\mathbf{\hat{b}}=f_{\text{Sig}}(\mathbf{W}_{\text{out}}[f_{\text{Tanh}}(\mathbf{W}_{1}[\mathbf{z}_{\text{index}},\mathbf{z}_{\text{sym}}]+\mathbf{b}_{1})]+\mathbf{b}_{\text{out}}),$
(5)

where $\mathbf{W}_{1}$, $\mathbf{W}_{\text{out}}$, $\mathbf{b}_{1}$,
$\mathbf{b}_{\text{out}}$ denote the weights and biases of the two output FC
layers.

###  III-B Model Training

Training the DuaIM-3DNet network is implemented by Tensorflow which requires a
large amount of training data. Before using the proposed DuaIM-3DNet detector,
it is necessary to offline train the DuaIM-3DNet model using the simulation
data. To get a corresponding set of transmitted matrix
$\mathbf{X}=f_{\text{DM-IM-3D-OFDM}}(\mathbf{b})$, multiple sequences of $p$
bits denoted by $\mathbf{b}$ are randomly generated. Then, under the influence
of the Rayleigh fading channel and AWGN, these matrices are transmitted to the
receiver. In accordance with their established statistical models, the channel
matrix and noise matrix are also randomly created and changed from one bit
sequence to another. A block of $\mathbf{Y}$ received signal values is
referred to as a data sample. The SymbolNet and IndexNet are learned
simultaneously from any data sample. The inputs of the IndexNet and SymbolNet
are $(n_{\text{sample}},3n)$ and $(n_{\text{sample}},6n)$, respectively, where
$n_{\text{sample}}$ is the sample size.

The DuaIM-3DNet model is trained to reduce the BER, through reducing the
discrepancy between sequence $\mathbf{b}$ and its predicted sequence
$\mathbf{\hat{b}}$. We use a loss function that is often employed in
regression models, namely, mean-squared error (MSE), as follows:

$\chi\left(\mathbf{b},\hat{\mathbf{b}};\mathbf{\alpha}\right)=\frac{1}{p}\left\|\mathbf{b}-\hat{\mathbf{b}}\right\|^{2},$
(6)

where
$\alpha=\left\\{[\mathbf{W}_{1},\mathbf{W}_{\text{out}}],[\mathbf{b}_{1},\mathbf{b}_{\text{out}}]\right\\}$
are the weights and biases of model, respectively. We use Adam optimizer [26]
and the learning rate is represented by $\eta$. In order to train DuaIM-3DNet
efficiently, the training SNR level (referred to as $\beta_{\text{train}}$)
used for training must be chosen properly, since the performance of the
trained model is very sensitive to the training SNR. Note that it is crucial
to choose the best $\beta_{\text{train}}$ so that the model trained by this
training SNR performs well for any other testing SNR of interest. For
instance, the noise impact will not be included in the training if
$\beta_{\text{train}}$ is too large, which will result in a poor performance
of the DNN model in the testing phase. We will demonstrate the justification
for choosing a suitable training SNR based on experiments in Section IV -
Simulation Results.

###  III-C Online Deployment

After offline training, the DuaIM-3DNet model with optimized parameter
$\alpha$ is used for online delivery of detection of DM-IM-3D-OFDM signals
with SNRs and channels of interest. The proposed method, in particular, may be
used in real-time to estimate data bits over a variety of channel fading
situations without the need for extra training for $\alpha$. By feeding the
received DuaIM-3DNet signal and the corresponding channel information, our
detector quickly and autonomously outputs the predicted bits.

##  IV Simulation results

In this section, we provide simulation results in terms of BER and detection
runtime. The ML detector is used as the baseline. For training, we use a
training data size of $5\times 10^{4}$ for each epoch with a batch size of 100
and the number of epochs is set to 500. During training, data samples are
randomly generated with each batch. Therefore, we have a total of $25\times
10^{6}$ different data samples. The learning rate $\eta$ is set to 0.001.
Meanwhile, other parameters of DuaIM-3DNet and parameters of DM-IM-3D-OFDM are
detailed in Table III. Although the proposed model considers only Rayleigh
fading channels in the experiments, the DuaIM-3DNet detector still performs
well under other channel models.

###  IV-A BER Performance

In Fig. 4, we demonstrate the BER performance obtained by the DuaIM-3DNet
scheme at different training SNRs, where simulation parameters are provided in
Table III. It can be seen that the BER performance of our proposed detector
significantly varies when changing the training SNR. More specifically, when
training with low training SNRs such as 7 dB, our DuaIM-3DNet detector
achieves the best BER performance at low SNR regions, while using higher
training SNRs such as 15 dB, our proposed DuaIM-3DNet tends to achieve better
performance at high SNRs. Moreover, if the training SNR is too large, such as
$\beta_{\text{train}}=20\,\text{dB}$, the BER performance of the proposed
DuaIM-3DNet significantly degrades. Based on this observation, in order to
achieve the best performance in a wide range of testing SNRs, we propose to
train our DNN detector using two training SNRs, namely 7 dB and 15 dB, as
shown in the following.

Figure 4: BER performance of the proposed DuaIM-3DNet detector when trained
with different training SNRs. The system and DNN model parameters for this
figure are illustrated in Table III.

Based on the results observed from Fig. 4, we found that in order to
effectively train the DNN model, we can train our detector with two training
SNRs at the same time, denoted as $\beta_{\text{train}}^{(1)}$ and
$\beta_{\text{train}}^{(2)}$. More specifically, for each epoch, which is
determined by $\text{epoch}\equiv 0\mod 2$, is trained with
$\beta_{\text{train}}^{(1)}$, and the remaining epochs are trained with
$\beta_{\text{train}}^{(2)}$. Each training SNR will be trained with the same
number of samples, which are different from each other. We train the model
with two training SNRs, namely, $\beta_{\text{train}}^{(1)}=7$ dB and
$\beta_{\text{train}}^{(2)}=$15 dB. Using such the proposed training strategy,
we compare the BER performance between the proposed DuaIM-3DNet and the ML
detector in Fig. 5, where the system parameters of DM-IM-3D-OFDM and the DNN
parameters of DuaIM-3DNet are highlighted in Table III. It is shown from Fig.
5 that the proposed DuaIM-3DNet achieves the BER performance very close to
that of the ML. More specifically, the performance gap between our detector
and the baseline is less than 1 dB across all SNRs.

TABLE III: A summary of simulation parameters Parameter | Value
---|---
Parameters of DM-IM-3D-OFDM $n$, $k$, $c_{A}$, $c_{B}$ | 4,2,2,2
Number nodes of layers in IndexNet $n_{\text{I0}},n_{\text{I1}},n_{\text{I2}}$ | $12,512,256$
Number nodes of layers in SymbolNet $n_{\text{S0}},n_{\text{S1}},n_{\text{S2}}$ | $24,512,256$
Input size of OutNet $n_{\text{Con}}$ | 512
Number nodes of Tanh activation of OutNet $n_{\text{Tanh}}$ | 256
Output size of OutNet $n_{\text{out}}=p$ | 6
Activation of hidden layers of IndexNet, SymbolNet | Tanh
Activation of two hidden layers of OutNet | Tanh-Sigmoid
Training SNR $\beta_{\text{train}}$ | 7,9,12,15,20 dB
Learning rate $\eta$ | 0.001
Batch size | 100
Number of training epochs | 500
Training data size | $25\times 10^{6}$
Testing data size | $10^{6}$
Optimizer | Adam [26]
Figure 5: BER performance comparison between our proposed DuaIM-3DNet and the
ML detector, where our detector is trained with two training SNRs, namely,
$\beta_{\text{train}}^{(1)}=7$ dB and $\beta_{\text{train}}^{(2)}=$15 dB. The
other system and DNN model parameters for this figure are illustrated in Table
III.

###  IV-B Runtime Complexity

We transform the DuaIM-3DNet model developed in the Tensorflow environment to
the MATLAB environment and compute its runtime to assess the complexity of
DuaIM3D-Net. Since the ML detector is also run by the MATLAB using the same
computer in order to guarantee a fair comparison. The runtime is measured in
seconds for both our DuaIM-3DNet and the ML benchmark. The system parameters
and DNN model parameters are illustrated in Table III. The runtime complexity
of both detectors is compared in Table IV. It is shown via this table that the
runtime of the ML is $0.001$ seconds, which is significantly higher than that
of the proposed DuaIM-3DNet, which consumes only $0.0003$ seconds. This
confirms the benefit of our proposed DNN detector in terms of runtime
complexity compared the traditional ML detector.

TABLE IV: Runtime of proposed DuaIM-3DNet and ML detector in seconds $(n,k,c_{A},c_{B})$ | ML | DuaIM-3DNet
---|---|---
(4,2,2,2) | 0.001 | 0.0003

##  V Conclusions

In this paper, we proposed the DuaIM-3DNet detector for the DM-IM-3D-OFDM
system. In particular, we designed a novel DNN structure for DuaIM-3DNet. Our
proposed consists of three sub-neural networks, namely IndexNet for estimating
active indices, SymbolNet for estimating 3D-constellation symbols, both
relying on the pre-processed data of the received signal and CSI, and then the
final DNN called OutNet that combines both IndexNet and SymbolNet for
recovering data bits. Once trained with simulated dataset, the proposed
detector can be deployed for detecting data bits in an online manner with very
low runtime. Our simulation results showed that the proposed DuaIM-3DNet
detector can achieve near-optimal BER performance at remarkably lower runtime
complexity compared to the conventional ML detector.

## References

  * [1] E. Basar, U. Aygolu, E. Panayirci, and H. V. Poor, “Orthogonal frequency division multiplexing with index modulation,” _IEEE Trans. Signal Process._ , vol. 61, no. 22, pp. 5536–5549, 2013.
  * [2] T. V. Luong and Y. Ko, “Impact of CSI uncertainty on MCIK-OFDM: tight, closed-form symbol error probability analysis,” _IEEE Trans. Veh. Technol._ , vol. 67, no. 2, pp. 1272 – 1279, Feb 2018.
  * [3] T. Van Luong and Y. Ko, “A tight bound on BER of MCIK-OFDM with greedy detection and imperfect CSI,” _IEEE Commun. Lett._ , vol. 21, no. 12, pp. 2594–2597, 2017.
  * [4] T. V. Luong and Y. Ko, “Symbol error outage performance analysis of MCIK-OFDM over complex TWDP fading,” in _Proc. Eur. Wireless_ , May 2017, pp. 1–5.
  * [5] E. Basar, “On multiple-input multiple-output OFDM with index modulation for next generation wireless networks,” _IEEE Trans. Signal Process._ , vol. 64, no. 15, pp. 3868–3878, 2016.
  * [6] T. V. Luong and Y. Ko, “The BER analysis of MRC-aided greedy detection for OFDM-IM in presence of uncertain CSI,” _IEEE Wireless Commun. Lett._ , vol. 7, no. 4, pp. 566–569, Aug. 2018.
  * [7] T. Mao, Z. Wang, Q. Wang, S. Chen, and L. Hanzo, “Dual-mode index modulation aided OFDM,” _IEEE Access_ , vol. 5, pp. 50–60, 2017.
  * [8] M. Wen, E. Basar, Q. Li, B. Zheng, and M. Zhang, “Multiple-mode orthogonal frequency division multiplexing with index modulation,” _IEEE Trans. Commun._ , vol. 65, no. 9, pp. 3892–3906, 2017.
  * [9] T. V. Luong, Y. Ko, and J. Choi, “Repeated MCIK-OFDM with enhanced transmit diversity under CSI uncertainty,” _IEEE Trans. Wireless Commun._ , vol. 17, no. 6, pp. 4079–4088, June 2018.
  * [10] M. Wen, B. Ye, E. Basar, Q. Li, and F. Ji, “Enhanced orthogonal frequency division multiplexing with index modulation,” _IEEE Trans. Wireless Commun._ , vol. 16, no. 7, pp. 4786–4801, 2017.
  * [11] T. V. Luong and Y. Ko, “Spread OFDM-IM with precoding matrix and low-complexity detection designs,” _IEEE Trans. Veh. Technol._ , vol. 67, no. 12, pp. 11 619–11 626, Dec. 2018.
  * [12] S. G. Kang, “An OFDM with 3-D signal mapper and 2-D IDFT modulator,” _IEEE Commun. Lett._ , vol. 12, no. 12, pp. 871–873, 2008.
  * [13] Z. Chen, E. C. Choi, and S. G. Kang, “Closed-form expressions for the symbol error probability of 3-D OFDM,” _IEEE Commun. Lett._ , vol. 14, no. 2, pp. 112–114, 2010.
  * [14] H. Huang and L. Zhang, “3-D constellation extension-aided PAPR suppressing for OFDM systems,” in _Proc 10th WCSP_ , 2018, pp. 1–6.
  * [15] Z. Xiang-li, W. Yong, W. Dia-nhong, and C. Zhenx-ing, “Improvement of four-dimensional signal constellations and corresponding OFDM system model design,” _ACTA ELECTONICA SINICA_ , vol. 48, no. 8, pp. 1486–1492, 2020\.
  * [16] M. Wang, Z. Chen, and Z. Chen, “Dual-mode index modulation aided 3D-OFDM,” _IEEE Commun. Lett._ , vol. 26, no. 3, pp. 612–616, 2022.
  * [17] Z. Chen and S. G. Kang, “Three-dimensional modulation formats with constant power for optical communications,” _Opt. Express_ , vol. 19, no. 23, pp. 22 358–22 363, Nov 2011.
  * [18] T. V. Luong, Y. Ko, N. A. Vien, D. H. N. Nguyen, and M. Matthaiou, “Deep learning-based detector for OFDM-IM,” _IEEE Wireless Commun. Lett._ , vol. 8, no. 4, pp. 1159–1162, 2019.
  * [19] J. Schmidhuber, “Deep learning in neural networks: An overview,” _Neural Networks_ , vol. 61, pp. 85–117, 2015.
  * [20] T. Van Luong, Y. Ko, N. A. Vien, M. Matthaiou, and H. Q. Ngo, “Deep energy autoencoder for noncoherent multicarrier MU-SIMO systems,” _IEEE Trans. Wireless Commun._ , vol. 19, no. 6, pp. 3952–3962, 2020.
  * [21] C. Xu, T. Van Luong, L. Xiang, S. Sugiura, R. G. Maunder, L.-L. Yang, and L. Hanzo, “Turbo detection aided autoencoder for multi-carrier wireless systems: Integrating deep learning into channel coded systems,” _IEEE Trans. Cogn. Commun. Netw._ , vol. 8, no. 2, pp. 600–614, 2022.
  * [22] T. V. Luong, Y. Ko, M. Matthaiou, N. A. Vien, M. T. Le, and V. D. Ngo, “Deep learning-aided multicarrier systems,” _IEEE Trans. Wireless Commun._ , vol. 20, no. 3, pp. 2109–2119, 2021.
  * [23] T. Van Luong, X. Zhang, L. Xiang, T. M. Hoang, C. Xu, P. Petropoulos, and L. Hanzo, “Deep learning-aided optical IM/DD OFDM approaches the throughput of RF-OFDM,” _IEEE J. Sel. Areas Commun._ , vol. 40, no. 1, pp. 212–226, 2022.
  * [24] L. Xiang, C. Xu, X. Zhang, T. Van Luong, R. G. Maunder, L.-L. Yang, and L. Hanzo, “Unity-rate coding improves the iterative detection convergence of autoencoder-aided communication systems,” _IEEE Trans. Veh. Technol._ , vol. 71, no. 5, pp. 5037–5047, 2022.
  * [25] T. V. Luong, N. Shlezinger, C. Xu, T. M. Hoang, Y. C. Eldar, and L. Hanzo, “Deep learning based successive interference cancellation for the non-orthogonal downlink,” _IEEE Trans. Veh. Technol._ , pp. 1–13, 2022.
  * [26] D. P. Kingma and J. Ba, “Adam: A method for stochastic optimization,” _arXiv preprint arXiv:1412.6980_ , 2014.


# Meta-AF Echo Cancellation for Improved Keyword Spotting

###### Abstract

Adaptive filters (AFs) are vital for enhancing the performance of downstream
tasks, such as speech recognition, sound event detection, and keyword
spotting. However, traditional AF design prioritizes isolated signal-level
objectives, often overlooking downstream task performance. This can lead to
suboptimal performance. Recent research has leveraged meta-learning to
automatically learn AF update rules from data, alleviating the need for manual
tuning when using simple signal-level objectives. This paper improves the
Meta-AF [1] framework by expanding it to support end-to-end training for
arbitrary downstream tasks. We focus on classification tasks, where we
introduce a novel training methodology that harnesses self-supervision and
classifier feedback. We evaluate our approach on the combined task of acoustic
echo cancellation and keyword spotting. Our findings demonstrate consistent
performance improvements with both pre-trained and joint-trained keyword
spotting models across synthetic and real playback. Notably, these
improvements come without requiring additional tuning, increased inference-
time complexity, or reliance on oracle signal-level training data.

Index Terms—  adaptive filtering, keyword spotting, learning to learn, meta-
learning, acoustic echo cancellation

##  1 Introduction

Adaptive filters (AFs) are essential for many smart systems, including
automatic speech recognition, sound event detection, and keyword spotting [2].
In these applications, AFs serve as key preprocessing steps and are designed
to enhance the performance of their downstream components by removing noise,
reverberation, and other distortions from their input signals. Traditionally,
AFs have been hand-tuned for optimizing signal-level objectives, such as
minimizing mean-squared error, using techniques like recursive least squares
[3, 4, 5]. However, recent advancements in deep learning have introduced
methods for controlling pre-built AF update rules [6, 7, 8], or for learning
entirely new update rules from scratch [9, 1]. Existing techniques often do
not take into account the downstream task and may not lead to the best
performance in practice.

Several pioneering works demonstrated that incorporating downstream task
knowledge into AF control, through manual unification schemes, could enhance
performance [10, 11, 12]. Such improvements necessitate a complex, task/model-
dependent derivation process, as well as feedback from the downstream model to
the AF at test time. This line of work inspired many DNN-based approaches.
These DNN approaches can be broadly grouped into two categories. The first
explicitly decouples preprocessing and downstream operations, treating them as
sequential components within a larger DNN pipeline [13, 14, 2, 15]. This is
highly modular but typically requires more complex training schemes and
engineering overhead [16]. The second takes an end-to-end strategy, trading
modularity for simpler design and training schemes [17, 18, 19, 20].

Fig. 1: The echo canceller $h_{\bm{\theta}[\tau]}$, controlled by optimizer
$g_{\bm{\phi}}$, cancels own-playback and passes its output to keyword
classifier $m_{\bm{\varphi}}$. The optimizer is trained end-to-end with the
classifier, improving performance without the need for additional tuning.

In this paper, we propose a novel framework that bridges these two DNN-based
approaches, allowing for the incorporation of downstream classification task
knowledge into AFs without task-dependent design or test-time feedback. We
propose a modified training scheme for the Meta-AF framework [1], which we
call classification-trained Meta-AF (CT-Meta-AF). CT-Meta-AF is unique in that
it does not require oracle signal-level supervision such as impulse responses
or clean speech. Instead, it leverages a combination of signal-level self-
supervision and automatic classifier feedback. This eliminates the need for
manual task/model dependent tuning and is directly compatible with both off-
the-shelf and end-to-end trained downstream models.

To evaluate our framework, we apply it to two fundamental tasks for smart
devices: acoustic echo cancellation (AEC) and keyword spotting (KWS). AEC is a
critical component of nearly all devices with own-playback, and KWS is
essential for enabling hands-free operation of smart devices. We construct a
challenging joint AEC and KWS dataset by combining two existing datasets [21,
22], and benchmark CT-Meta-AFs against Meta-AF [23] and a Kalman Filter [24],
two state-of-the-art approaches for signal-level objectives. Results show that
CT-Meta-AF achieves consistent performance gains across both synthetic and
real playback scenarios, multiple playback lengths, various task/model
configurations, and both pre-trained and joint-trained keyword spotting
models.

The contributions of this work are: 1) A versatile framework for seamlessly
integrating downstream task knowledge into AF update rules, applicable to
various AFs and tasks, 2) Task-specific insights for AEC and KWS, yielding
models that surpass previous approaches, 3) A comprehensive empirical
exploration of incorporating downstream task knowledge across different
classifier models, employing various training schemes, and evaluating on both
real-world and synthetic data. We also release all code and weights1.

##  2 Meta-AF Background

###  2.1 Adaptive Filters

In this work, an AF is a time-varying filtering procedure with parameters that
are controlled by an online optimization rule in order to solve some objective
function. We denote the filter as $h_{\bm{\theta}[\tau]}$, parameterized by
$\bm{\theta}[\tau]$, and updated using an additive rule,

$\bm{\theta}[\tau+1]=\bm{\theta}[\tau]+\bm{\Delta}[\tau].$ (1)

Time-varying updates $\bm{\Delta}[\tau]$ govern filter adaptation, and are
produced by an update rule $g_{\bm{\phi}}$. Conventional AFs are designed to
produce updates which solve a tractable AF loss $\mathcal{L}(\cdot)$, which is
typically a function of the AF output and some readily available mixture.

To perform our chosen AF task of AEC, we fit a filter to to remove echo caused
by own-playback. The time-domain signal model is
$\underline{\mathbf{d}}[{\mathrm{t}}]=\underline{\mathbf{u}}[{\mathrm{t}}]\ast\underline{\mathbf{w}}+\underline{\mathbf{n}}[{\mathrm{t}}]+\underline{\mathbf{s}}[{\mathrm{t}}]$,
where $\underline{\mathbf{n}}$ is noise, $\underline{\mathbf{s}}$ is a
keyword, and $\underline{\mathbf{w}}$ is the transfer function applied to own
playback $\underline{\mathbf{u}}$. The AF attempts to mimic
$\underline{\mathbf{w}}$ via a multi-frame frequency-domain filter applied
using overlap-save [25]. We denote this as $h_{\bm{\theta}[\tau]}$ with
frequency coefficients
$\bm{\theta}[\tau]=\hat{\mathbf{w}}[\tau]\in\mathbb{C}^{K\times B}$ where $K$
is frequencies, $B$ is the number of blocks, and blocks advance by $K/2$
samples. The output is echo reduced signal
$\underline{\mathbf{e}}[\tau]=h_{\bm{\theta}[\tau]}(\underline{\mathbf{d}}[\tau],\underline{\mathbf{u}}[\tau])$.

###  2.2 Meta-Adaptive Filters

The Meta-AF [1] approach showed that AF control rules could be entirely
learned with a learning-to-learn strategy [26]. Instead of solving the AF loss
$\mathcal{L}(\cdot)$ directly, the procedure solves a meta-loss,

$\hat{\bm{\phi}}=\arg\min_{\bm{\phi}}E_{\mathcal{D}}[\;\mathcal{L}_{M}(\;g_{\bm{\phi}},\mathcal{L}(h_{\bm{\theta}},\cdots)\;)\;],$
(2)

where $\mathcal{L}_{M}(\;g_{\bm{\phi}},\mathcal{L}(h_{\bm{\theta}},\cdots)\;)$
is the meta-loss that is a function of the AF $h_{\bm{\theta}[\tau]}$,
optimizer neural network $g_{\bm{\phi}}$, and $E_{\mathcal{D}}$ represents
expectation over dataset $\mathcal{D}$. The standard setup solves this via an
additive update $\bm{\theta}[\tau+1]=\bm{\theta}[\tau]+g_{\bm{\phi}}(\cdot)$,
where $g_{\bm{\phi}}$ is a complex valued DNN parameterized by $\bm{\phi}$,
applied per frequency $\mathrm{k}$. Typically, $g_{\bm{\phi}}$ has per-
frequency state and inputs,

$\displaystyle(\bm{\Delta}_{\mathrm{k}}[\tau],\bm{\psi}_{\mathrm{k}}[\tau+1])$
$\displaystyle=$ $\displaystyle
g_{\bm{\phi}}(\bm{\xi}_{\mathrm{k}}[\tau],\bm{\psi}_{\mathrm{k}}[\tau])$ (3)
$\displaystyle\bm{\theta}_{\mathrm{k}}[\tau+1]$ $\displaystyle=$
$\displaystyle\bm{\theta}_{\mathrm{k}}[\tau]+\bm{\Delta}_{\mathrm{k}}[\tau],$
(4)

where we index across $K$ frequencies using subscript $\mathrm{k}$. The input
is a stack of the frequency-domain filter gradient, input, target, error, and
output respectively:
$\bm{\xi}_{\mathrm{k}}[\tau]=[\nabla_{\mathrm{k}}[\tau],\mathbf{u}_{\mathrm{k}}[\tau],\mathbf{d}_{\mathrm{k}}[\tau],\mathbf{e}_{\mathrm{k}}[\tau],\mathbf{y}_{\mathrm{k}}[\tau]]$.
The outputs are AF update $\bm{\Delta}_{\mathrm{k}}[\tau]$ and a new internal
state $\bm{\psi}_{\mathrm{k}}[\tau]$. To learn parameters $\bm{\phi}$, we use
backpropagation-through-time and a meta-optimizer (e.g. Adam) over $L$
optimization steps. We set our meta-loss to the self-supervised log-mse meta-
loss,

$\displaystyle\mathcal{L}_{M}(\underline{\bar{\mathbf{e}}})$ $\displaystyle=$
$\displaystyle\ln E[\|\underline{\bar{\mathbf{e}}}[\tau]\|^{2}],$ (5)

where
$\underline{\bar{\mathbf{e}}}[\tau]=\mathrm{cat}(\underline{\mathbf{e}}[\tau],\cdots,\underline{\mathbf{e}}[\tau+L-1])\in\mathbb{R}^{RL}$,
and $\mathrm{cat}$ is the concatenation operator. Intuitively, this loss
encourages an optimizer to maximally reduce the energy of the AF output
without needing oracle echo
($\underline{\mathbf{u}}\ast\underline{\mathbf{w}}$) or oracle speech
($\underline{\mathbf{s}}$) information.

##  3 Classification-Trained Meta-AF

In this work, we propose CT-Meta-AF, an extension to the Meta-AF framework
[1]. CT-Meta-AF learns an AF optimizer for downstream classification tasks in
a data-driven manner, without task/model dependent engineering or the need for
oracle signals like clean speech. Specifically, we use an adaptive filter,
such as an echo canceller, whose time-varying parameters $\bm{\theta}[\tau]$
are updated by a meta-learned update rule $g_{\bm{\phi}}$. The goal is to use
the processed signals from the adaptive filter for a downstream classification
task, such as keyword spotting, performed by a model $m_{\bm{\varphi}}$. To
this end, we employ an end-to-end training setup that enables joint
optimization of the adaptive filter, optimizer, and the classification model.
Our approach uses feedback from the classifier during training to learn a
custom optimizer, resulting in enhanced performance without requiring explicit
coupling or the need for test-time feedback. This approach is also suitable
for training on real mixtures.

###  3.1 Overview

To address the downstream objective, we introduce a modification to the
original meta-loss from (5) that incorporates classification feedback, which
we call $\mathcal{L}_{CM}$. Specifically, $\mathcal{L}_{CM}$ consists of two
components: the classification loss, denoted by $\mathcal{L}_{C}(c,\hat{c})$,
where $c$ is the true class and $\hat{c}=m_{\bm{\varphi}}(\cdot)$ is the
predicted class, and the self-supervised loss, denoted by $\mathcal{L}_{M}$,
as defined in (5). The joint loss,

$\mathcal{L}_{CM}(\bar{\mathbf{e}},c,\hat{c})=\lambda\cdot\mathcal{L}_{C}(c,\hat{c})+(1-\lambda)\cdot\mathcal{L}_{M}(\bar{\mathbf{e}}),$
(6)

uses $\lambda\in[0,1]$ to control the weighting between classification and
self-supervised losses. This approach implicitly couples the representations
learned by $g_{\bm{\phi}}$ and $m_{\bm{\varphi}}$ without explicitly sharing
their parameters, using the idea of “task-splitting” [19, 20].

###  3.2 Pretrained Classifier

When dealing with complex classification tasks, it is common to use off-the-
shelf or pretrained models due to data, compute, or engineering constraints.
In this setting, we assume that the classifier, $m_{\bm{\varphi}}$, is frozen
and not trainable. This leads to a modified (2),

$\hat{\bm{\phi}}=\arg\min_{\bm{\phi}}E_{\mathcal{D}}[\;\mathcal{L}_{CM}(\;m_{\bm{\varphi}},g_{\bm{\phi}},\mathcal{L}(h_{\bm{\theta}},\cdots)\;)\;].$
(7)

This equation incorporates $m_{\bm{\varphi}}$ without modifying it by using
$m_{\bm{\varphi}}$ as an additional loss term. This method allows custom
training of the optimizer for the classifier without the classifier needing to
be aware of the custom preprocessing. It customizes the optimizer to the
classifier, automatically performing the model unification proposed by Seltzer
et al. [10] in a model and task independent fashion.

###  3.3 Jointly Trained Classifier

When ample data and compute resources are available, joint or end-to-end
training is a powerful approach. This involves training both the optimizer
$g_{\bm{\phi}}$ and classifier $m_{\bm{\varphi}}$ simultaneously using the
modified meta-loss function $\mathcal{L}_{CM}$. The parameters of the
optimizer and classifier, $\bm{\phi}$ and $\bm{\varphi}$, are jointly
optimized via

$\hat{\bm{\phi}},\hat{\bm{\varphi}}=\arg\min_{\bm{\phi},\bm{\varphi}}E_{\mathcal{D}}[\;\mathcal{L}_{CM}(\;m_{\bm{\varphi}},g_{\bm{\phi}},\mathcal{L}(h_{\bm{\theta}},\cdots)\;)\;].$
(8)

During joint training, classification feedback is used to adjust the
parameters of the optimizer, improving its ability to generate outputs that
aid in classification. At the same time, the classifier learns to operate on
AF outputs. This builds upon the pretrained classifier setup by producing a
custom-trained classifier that can better leverage the AF. To speed up
training, we can initialize $\bm{\phi}$ and $\bm{\varphi}$ with pretrained
weights. It is also possible to improve performance by allowing
$m_{\bm{\varphi}}$ to use information beyond the outputs of $h_{\bm{\theta}}$.

##  4 Experimental Design

The goal of our setup is to demonstrate that CT-Meta-AF strikes the right
balance between flexibility and structure, enabling high-performance while
still being a direct replacement for existing approaches. We evaluate the
performance of CT-Meta-AF on KWS with device playback. The AEC removes own-
playback from recordings by learning the echo path, as shown in Fig. 1. For
model details, see Fig. 2. We evaluate three scenarios: one with a pretrained
KWS, one with test-time swapped KWS, and one with a jointly trained KWS, all
implemented using Meta-AF [1]. All CT-Meta-AFs use the classifier for
training. The jointly trained KWS is optimized end-to-end and trained
simultaneously with the AEC.

###  4.1 AEC Configurations

To perform AEC, we fit an AF to cancel echo. At inference time, we only assume
access to the playback, $\underline{\mathbf{u}}$ and echoic mixture,
$\underline{\mathbf{d}}$. The AF uses frequency-domain overlap save with a
window of $K=1024$, a hop of $R=512$, and $B=4$ blocks. Each block is denoted
by $\mathbb{C}\text{Filter}$ in Fig. 2. Each AEC filters the farend
$\mathbf{u}[\tau]$ with estimated filter $\hat{\mathbf{w}}[\tau]$ and
subtracts the result from $\mathbf{d}[\tau]$. For a review of AEC see Benesty
et al. [27]. We compare our approach to four baselines: regular Meta-AF [1], a
Kalman filter AEC (Diag. KF) [24], No-Echo, and No-AEC. We grid-search-tune
Diag. KF using KWS accuracy. No-Echo simulates running the KWS model in a
playback-free environment, while No-AEC performs no echo cancellation and
simulates deploying a KWS without AEC.

CT-Meta-AF and Meta-AF use the same higher-order architecture [23] and
training scheme, with the only difference being the loss. For CT-Meta-AF, we
use $\lambda=0.5$ in (6), and for regular Meta-AF, we use $0$. We set the
group size, group hop, and hidden size to $5$, $2$, and $48$, respectively
(see Fig. 2 for details). We use Adam with a batch size of $16$, a learning
rate of $2\cdot 10^{-4}$, momentum $\beta_{1}=0.99$, and we randomize the
truncation length $L$. Additionally, we apply gradient clipping and reduce the
learning rate by half if the validation performance does not improve for $10$
epochs, and we stop training after $30$ epochs with no improvement. For
pretrained KWS experiments, we train $\bm{\phi}$ from scratch, and for joint
training, we initialize with the best pretrained $\bm{\phi}$. When joint
training with Diag. KF or Meta-AF we do not update the pretrained $\bm{\phi}$
and just train the KWS. Each model has $32\,$K complex parameters and trains
on one GPU.

###  4.2 KWS Configurations

We set up KWS as a multi-class classification task, where the keyword
$\underline{\mathbf{s}}$ belongs to a single class $c$. We base our KWS on the
model proposed by Cornell et al. [20]. Our version uses $40$ log-mel-filter-
bank inputs and short-time Fourier transform with a $256$ point hop and a
$512$ point window. The KWS has $3$ residual blocks, each with a $1\times 1$
convolution, layer norm, ReLU, a dilated convolution with kernel size $5$,
layer norm, ReLU, and a final $1\times 1$ convolution. The last residual block
is averaged across time and fed to a dense layer with softmax to predict the
class distribution. See Fig. 2. We use a binary cross-entropy loss and train
the KWS for $50$ epochs with a batch size of $128$, a learning rate of
$10^{-3}$, and use the best checkpoint based on validation performance. We
pretrain on a dataset without playback. For joint training, due to limited GPU
capacity, we use a batchsize of $16$, learning rate of $10^{-4}$,
$\beta_{1}=.9$, reduce the learning rate by half after $10$ epochs with no
improvement, and stop training after $50$ epochs with no improvement. All KWS
models have $\approx 300$K parameters and use $\approx 20$MFLOPs per second.

Fig. 2: Detailed view of the AEC, Optimizer, and KWS. The AEC preprocesses the
KWS inputs and the optimizer controls the AEC parameters. At test time, only
the AEC parameters change

###  4.3 Dataset & Metrics

We use synthetic playback during training and evaluate our models using both
synthetic and real playback data from the Microsoft AEC Challenge [22] and
keywords from the Google Speech Commands V2 dataset [21], sampled at
$16\,$KHz. During training, we trim playback to $3$ seconds, randomly mix
playback with keywords, zero-pad keywords as needed, apply a random shift, and
set the signal-to-echo ratio (SER) uniformly at random between $-25\,$dB and
$0\,$dB. Each keyword is used once. To test, we use playback trimmed to either
$4$ or $12$ seconds. We evaluate three datasets: a $35$-class dataset and two
smaller datasets with $10$ and $2$ classes, respectively. The smaller datasets
contain approximately one-third and one-tenth of the full dataset. We always
use the same folds and never mix across folds.

To evaluate performance, we use macro and micro averaged F1, where higher is
better. The goal is to reflect the class imbalance in the KWS Dataset. We
display results as macro F1 (micro F1).

##  5 Results & Discussion

Here, we investigate the effect of classification training for Meta-AF on AEC
with a downstream KWS. This task simulates a device attempting to classify a
spoken keyword while emitting playback. We show results for zero playback (No-
Echo), no cancellation (No-AEC), Diag. KF, Meta-AF based AEC without
classification training (Meta-AEC), and Meta-AF based AEC with classification
training (CT-Meta-AEC). The Diag. KF and Meta-AEC baselines are state-of-the-
art traditional and data-driven approaches. All models are trained on
synthetic playback with challenging SERs distributed uniformly at random
between $-25\,$dB and $0\,$dB, and real playback is only used for evaluation.
We use an off-the-shelf KWS that is not customized for AEC in sections 5.1 and
5.2 but do experiment with retraining the KWS in section 5.3. We evaluate
longer playback and compute statistical significance for select models. Across
experiments, CT-Meta-AF proved highly stable and required no additional
tuning, making it a drop-in replacement for prior approaches.

###  5.1 Pretrained KWS

First, we test the effectiveness of classification training as described in
3.2. In Table 1, all AEC models share a frozen KWS model pretrained on
keywords without playback. This setup mimics using an off-the-shelf KWS
without retraining but with access to your own dataset, a common real-world
setup. For CT-Meta-AEC training, we use $\lambda=0.5$ when computing
$\mathcal{L}_{CM}$. The F1 degradation from No-Echo to No-AEC shows the
importance of AEC.

In Table 1, CT-Meta-AEC significantly outperforms its signal-level Diag. KF
and Meta-AEC counterparts, as indicated by better F1 scores. In synthetic
playback (left column), CT-Meta-AEC improves over Meta-AEC by some .165 F1.
This gap persists in real playback, where CT-Meta-AEC is the top performing
model by .091 F1. Interestingly, CT-Meta-AEC achieves a 5.80 dB reduction in
echo, while regular Meta-AF attains a 9.57 dB reduction. This observation
underscores the limitations of signal-level metrics as effective descriptors
of downstream performance, especially in the context of nonlinear processing
methods such as DNN-based KWS. Classification-based training effectively
addresses this discrepancy and optimizes downstream performance. In a
secondary evaluation with 12-second signals, CT-Meta-AEC outperforms Meta-AEC
by 0.279 F1 in synthetic playback and 0.119 F1 in real playback.

###  5.2 Specialization and Sensitivity

Next, we study the specialization capabilities of CT-Meta-AEC in different KWS
setups. We use the approach from 3.2 to train three CT-Meta-AEC models: CT-
Meta-AEC-35, CT-Meta-AEC-10, and CT-Meta-AEC-2, corresponding to datasets with
35, 10, and 2 keyword classes, respectively. We assess the performance of each
CT-Meta-AEC model on all three datasets, but always use a downstream KWS model
specifically trained on a matching keyword setup. Table 2 presents the results
of our experiments on synthetic playback scenarios, where each row corresponds
to a distinct AEC model and each column represents a unique test-time KWS
configuration. The first row displays our Meta-AEC baseline. Table entries on
the diagonal show matched train/test setups.

In all columns of Table 2, CT-Meta-AEC with a matching KWS performs best. This
demonstrates that CT-Meta-AEC is learning a specialized optimizer (the
diagonal) which outperforms both generalist optimizer (top row) and optimizers
trained on different models (off diagonal). Notably, results above the
diagonal show that specialization can yield superior results even in the
presence of limited training data. Specifically, Meta-AEC and CT-Meta-AEC-35,
which are trained with three times more data than CT-Meta-AEC-10, are
surpassed by the latter on 10 class KWS. This suggests that classification
training is a data-efficient approach for improving performance on downstream
tasks. The results from mismatched train/test setups show that CT-Meta-AECs
are good at related tasks, and usually still outperform Meta-AEC.

###  5.3 Jointly Trained KWS

We investigate joint training of the AEC and KWS to simulate having sufficient
data for training a complete system, without oracle signal-level supervision.
Both the AEC and KWS models undergo joint training, following the approach in
3.3.The KWS models undergo a pre-training phase on scenes devoid of playback,
followed by fine-tuning using the output of their corresponding AEC models.
This represents a significant departure from the approach outlined in 3.2,
where KWS models were trained without consideration for echo presence. We call
this approach JCT-Meta-AEC. For statistical robustness, we ran three separate
trials of the Meta models.

In Table 3, we find that the training scheme from 3.3 improves performance.
JCT-Meta-AEC outperforms Meta-AEC by $.008$ F1 (p-value $.01$) in real
playback scenarios, underscoring the efficacy of classification training for
real-world performance. While JCT-Meta-AEC outperforms Meta-AEC on synthetic
data, the improvement is not significant. However, on the longer $12$-second
test-set, JCT-Meta-AEC beats Meta-AEC by a margin of 0.057 (p-value $.0005$).
Of note, we did not encounter any training stability issues.

Model |  | Synthetic Playback |  | Real Playback
---|---|---|---|---
No-Echo |  | .928 (.935) |  | .931 (.936)
No-AEC |  | .087 (.098) |  | .102 (.117)
Diag. KF |  | .196 (.208) |  | .165 (.180)
Meta-AEC |  | .335 (.340) |  | .226 (.236)
CT-Meta-AEC |  |  .500 (.508) |  |  .317 (.326)
Table 1: F1 Macro (F1 Micro) with a pretrained KWS and SER $\in[-25,0]\,$dB. No-AEC and No-Echo are lower/upper bounds. Model | 35 Class | 10 Class | 2 Class
---|---|---|---
Meta-AEC | .335 (.340) | .476 (.465) | .751 (.754)
CT-Meta-AEC-35 |  .500 (.508) | .513 (.483) | .786 (.788)
CT-Meta-AEC-10 | .344 (.348) |  .533 (.529) | .781 (.781)
CT-Meta-AEC-2 | .274 (.281) | .413 (.400) |  .802 (.802)
Table 2: Specialization of classification-trained Meta-AEC with performance shown as F1 Macro (F1 Micro). A different model with different keywords is swapped in at test time. SER $\in[-25,0]\,$ dB. Model |  | Synthetic Playback |  | Real Playback
---|---|---|---|---
No-Echo |  | .922 (.928) |  | .931 (.936)
No-AEC |  | .609 (.619) |  | .583 (.593)
Diag. KF |  | .778 (.781) |  | .690 (.698)
Meta-AEC* |  | .870 (.876) |  | .746 (.754)
JCT-Meta-AEC* |  |  .871 (.877) |  |  .754 (.762)
Table 3: F1 Macro (F1 Micro) with a jointly trained KWS and SER
$\in[-25,0]\,$dB. No-AEC and No-Echo are lower/upper bounds. An asterix
denotes that we averaged three trials.

##  6 Conclusion

We proposed a simple yet effective approach for improving the performance of
downstream classification tasks by incorporating classifier feedback into
learned adaptive filter update rules. Our approach, classification-trained
meta-adaptive filtering (CT-Meta-AF) enables end-to-end training without
oracle single-level supervision. We evaluated CT-Meta-AF on echo cancellation
and keyword spotting and observed consistent performance gains across
synthetic and real playback, multiple keyword configurations, and both pre and
jointly trained keyword models. CT-Meta-AF yields performance improvements
without additional inference costs or manual tuning. We believe our approach
has the potential to improve many adaptive filter pipelines, thanks to it’s
plug-and-play design and promising real-world performance.

## References

  * [1] Jonah Casebeer, Nicholas J. Bryan, and Paris Smaragdis,  “Meta-AF: Meta-Learning for Adaptive Filters,”  IEEE Transactions on Audio, Speech, and Language Processing (TASLP), 2022.
  * [2] Reinhold Haeb-Umbach, Shinji Watanabe, Tomohiro Nakatani, Michiel Bacchiani, Bjorn Hoffmeister, Michael L Seltzer, Heiga Zen, and Mehrez Souden,  “Speech Processing for Digital Home Assistants: Combining Signal Processing With Deep-Learning Techniques,”  IEEE Signal Processing Magazine (SPM), 2019.
  * [3] Bernard Widrow and Samuel D. Stearns,  Adaptive Signal Processing,  Prentice-Hall, 1985.
  * [4] V. John Mathews,  “Adaptive Polynomial Filters,”  IEEE Signal Processing Magazine (SPM), 1991.
  * [5] Simon S. Haykin,  Adaptive Filter Theory,  Pearson, 2008.
  * [6] Jonah Casebeer, Jacob Donley, Daniel Wong, Buye Xu, and Anurag Kumar,  “NICE-Beam: Neural Integrated Covariance Estimators for Time-Varying Beamformers,”  arXiv:2112.04613, 2021.
  * [7] Amir Ivry, Israel Cohen, and Baruch Berdugo,  “Deep Adaptation Control for Acoustic Echo Cancellation,”  in IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP). IEEE, 2022.
  * [8] Thomas Haubner, Andreas Brendel, and Walter Kellermann,  “End-To-End Deep Learning-Based Adaptation Control for Frequency-Domain Adaptive System Identification,”  in IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP). IEEE, 2022.
  * [9] Jonah Casebeer, Nicholas J Bryan, and Paris Smaragdis,  “Auto-DSP: Learning to Optimize Acoustic Echo Cancellers,”  in IEEE Workshop on Applications of Signal Processing to Audio and Acoustics (WASPAA), 2021.
  * [10] Michael L Seltzer, Bhiksha Raj, and Richard M Stern,  “Likelihood-Maximizing Beamforming for Robust Hands-Free Speech Recognition,”  IEEE Transactions on Speech and Audio Processing (TSAP), 2004.
  * [11] Guangji Shi, Parham Aarabi, and Hui Jiang,  “Phase-Based Dual-Microphone Speech Enhancement Using a Prior Speech Model,”  IEEE Transactions on Audio, Speech, and Language Processing (TASLP), 2006.
  * [12] Xianyu Zhao and Zhijian Ou,  “Closely Coupled Array Processing and Model-Based Compensation for Microphone Array Speech Recognition,”  IEEE Transactions on Audio, Speech, and Language Processing (TASLP), 2007.
  * [13] Jahn Heymann, Lukas Drude, Christoph Boeddeker, Patrick Hanebrink, and Reinhold Haeb-Umbach,  “Beamnet: End-To-End Training of a Beamformer-Supported Multi-Channel Asr System,”  in IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP). IEEE, 2017.
  * [14] Tsubasa Ochiai, Shinji Watanabe, Takaaki Hori, John R Hershey, and Xiong Xiao,  “Unified Architecture for Multichannel End-To-End Speech Recognition With Neural Beamforming,”  IEEE Journal of Selected Topics in Signal Processing (JSTSP), 2017\.
  * [15] Wangyou Zhang, Xuankai Chang, Christoph Boeddeker, Tomohiro Nakatani, Shinji Watanabe, and Yanmin Qian,  “End-To-End Dereverberation, Beamforming, and Speech Recognition in a Cocktail Party,”  IEEE Transactions on Audio, Speech, and Language Processing (TASLP), 2022.
  * [16] Wangyou Zhang, Christoph Boeddeker, Shinji Watanabe, Tomohiro Nakatani, Marc Delcroix, Keisuke Kinoshita, Tsubasa Ochiai, Naoyuki Kamo, Reinhold Haeb-Umbach, and Yanmin Qian,  “End-To-End Dereverberation, Beamforming, and Speech Recognition With Improved Numerical Stability and Advanced Frontend,”  in IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP). IEEE, 2021.
  * [17] Sri Harish Mallidi, Roland Maas, Kyle Goehner, Ariya Rastrow, Spyros Matsoukas, and Björn Hoffmeister,  “Device-directed Utterance Detection,”  Interspeech, 2018.
  * [18] Nathan Howard, Alex Park, Turaj Zakizadeh Shabestary, Alexander Gruenstein, and Rohit Prabhavalkar,  “A Neural Acoustic Echo Canceller Optimized Using an Automatic Speech Recognizer and Large Scale Synthetic Data,”  in IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP). IEEE, 2021.
  * [19] Sebastian Braun and Maria Luis Valero,  “Task Splitting for Dnn-Based Acoustic Echo and Noise Removal,”  in IEEE Workshop on Applications of Signal Processing to Audio and Acoustics (WASPAA). IEEE, 2022.
  * [20] Samuele Cornell, Thomas Balestri, and Thibaud Sénéchal,  “Implicit Acoustic Echo Cancellation for Keyword Spotting and Device-Directed Speech Detection,”  in Workshop on Spoken Language Technology (SLT). IEEE, 2023.
  * [21] Pete Warden,  “Speech Commands: A Dataset for Limited-Vocabulary Speech Recognition,”  arXiv:1804.03209, 2018.
  * [22] Ross Cutler, Ando Saabas, Tanel Parnamaa, Marju Purin, Hannes Gamper, Sebastian Braun, Karsten Sorensen, and Robert Aichner,  “ICASSP 2022 Acoustic Echo Cancellation Challenge,”  in IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), 2022.
  * [23] Junkai Wu, Jonah Casebeer, Nicholas J. Bryan, and Paris Smaragdis,  “Meta-Learning for Adaptive Filters with Higher-Order Frequency Dependencies,”  in IEEE International Workshop on Acoustic Signal Enhancement (IWAENC), 2022.
  * [24] Fabian Kuech, Edwin Mabande, and Gerald Enzner,  “State-Space Architecture of the Partitioned-Block-Based Acoustic Echo Controller,”  in IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), 2014.
  * [25] J-S Soo and Khee K Pang,  “Multidelay Block Frequency Domain Adaptive Filter,”  IEEE Transactions on Acoustics, Speech, and Signal Processing (TASSP), 1990.
  * [26] Marcin Andrychowicz, Misha Denil, Sergio Gómez Colmenarejo, Matthew W Hoffman, David Pfau, Tom Schaul, Brendan Shillingford, and Nando de Freitas,  “Learning to Learn by Gradient Descent by Gradient Descent,”  in NeurIPS, 2016.
  * [27] Jacob Benesty, Tomas Gänsler, Dennis R Morgan, Steven L. Gay, and M. Mohan Sondhi,  Advances in Network and Acoustic Echo Cancellation,  Springer, 2001.