c^{\prime}(t),\dots,c_{n}\circ c^{\prime}(t))$. Therefore the $x_{i}$ must be
instantiated by the terms $c_{i}\circ c^{\prime}(t)$. Hence there are
$u_{i,j}\in{\mathcal{L}}$ such that $c_{i}\circ
c^{\prime}(t)\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{i,j}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}u_{i,j}$
for $i\in I,~{}1\leq j\leq m_{i}$. As well, $c_{j}\circ
c^{\prime}(t)\centernot{\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{j,k}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}}$
for $j\in J,~{}1\leq k\leq n_{j}$. Lastly, writing $u=c_{0}(\widetilde{c}\circ
c^{\prime}(t),\widetilde{u})$ and $c\circ
c^{\prime}(t)\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}c_{0}(\widetilde{c}\circ
c^{\prime}(t),\widetilde{u})$.

By induction hypothesis, each of the $c_{i}$’s preserves autonomy under
composition on $\mathcal{O}$, hence $c_{i}\circ c^{\prime}$ is autonomous for
all $i$. Hence there are autonomous transitions $c_{i}\circ
c^{\prime}\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{i,j}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}d_{i,j}$,
where $d_{i,j}$ are contexts such that $u_{i,j}=d_{i,j}(t)$.

Furthermore, for any $t^{\prime}\in{\mathcal{L}}$, $c_{j}\circ
c^{\prime}(t^{\prime})\centernot{\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{j,k}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}}$:
if there was such a $t^{\prime}$, by autonomy of $c_{j}\circ c^{\prime}$, we
would have $c_{j}\circ
c^{\prime}(t)\mathrel{\stackrel{{\scriptstyle{\;\;\mu_{j,k}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}$.

Therefore, for any $t^{\prime}\in{\mathcal{L}}$, the premises of the above
GSOS rule hold; hence we can deduce $c\circ
c^{\prime}(t^{\prime})\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}c_{0}(\widetilde{c}\circ
c^{\prime}(t^{\prime}),\widetilde{d}(t))$. Thus there is an autonomous
transition $c\circ
c^{\prime}\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}c_{0}(\widetilde{c}\circ
c^{\prime},\widetilde{d})$, and $u=(c_{0}(\widetilde{c}\circ
c^{\prime},\widetilde{d}))(t)$. The transition $c\circ
c^{\prime}(t)\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}u$
is indeed autonomous. This concludes the proof. ∎

######  Proposition .

Consider the set of unary contexts of a language defined within the GSOS
formats, and suppose that bisimilarity is preserved by these contexts. This
set constitutes a set of operators.

###### Proof.

This is a direct consequence of Lemma 4.3: for any language, the empty context
acts as the identity function over the set of terms, and by construction
contexts can be composed; by hypothesis, we consider contexts that respect
bisimilarity. All is left to check is clause 3 of Definition 4.1, i.e., that
composition preserves autonomy over $\mathcal{O}$: this is give by Lemma 4.3.
∎

Some GSOS rule formats guarantee congruence for weak bisimilarity [vG05,
FvG16], which gives clause 4 of Definition 4.1. This condition could actually
be relaxed, by imposing congruence only for certain forms of contexts,
according to how variables occur in the equations. For instance, if certain
syntactical constructs are not used, we do not need congruence to hold for
these constructs. This can be useful, for instance, to allow non-guarded sums
in CCS: in sums, we require variable occurrences to be under prefixes (and the
sum itself need not between prefixed processes).

######  Remark .

Proposition 4.3 makes it possible to apply Theorems 4.1 and 4.1 to any GSOS
language that additionally preserves bisimilarity. However the formulation of
the ‘syntactic solution of an equation’ and of ‘innocuous divergence’ in
Section 4.1 is not as easy to grasp as in CCS.

An alternative would be to assume that the language has constants for
recursively defined processes, which would allow us to remain closer to the
setting of CCS, as exposed in Section 3.

We now state the abstract version of Theorem 3.2. For this, we rely on the
definition of divergence and innocuous divergence from Section 4.1, and use
contexts of a GSOS language to stand for operators.

######  Theorem .

Consider a language whose constructs have SOS rules in the GSOS format and
preserve $\approx$. Consider an equation of the form $X=E$, where $E$ is a
function corresponding to a context of the language (seen as an equation
expression), that is autonomous and has only innocuous divergences,

Then either the equation has no solution or it has a unique solution for
$\approx$.

###### Proof.

This is a direct consequence of Theorem 4.1 and Proposition 4.3. Consider the
context $C$ such that $C[X]$ and $E$ are syntactically equal. Then
$C\in\mathcal{O}$, where $\mathcal{O}$ is the set of unary contexts of the
language; by Proposition 4.3, it is a set of operators. Using Theorem 4.1 we
deduce that the equation has a unique solution. ∎

Checking the autonomy property is often straightforward; for instance, it
holds if, in the body of an equation, all variables are underneath an axiom
construct, that is, a construct that (like prefix in CCS) is defined by means
of SOS rules in which the set of premises is empty. Definitions of guardedness
for SOS specifications from [Vaa92] can also be applied here.

#### tyft/tyxt formats.

We briefly discuss other widely studied formats, the tyft/tyxt formats [GV92].
In those formats, lookaheads are possible. Lookahead allows one to write rules
that ‘look into the future’ (a transition is allowed if certain sequences of
actions are possible); this breaks autonomy (condition 3 of Definition 4.1),
hence Theorem 4.1 does not hold in a tyft/tyxt language. We provide a counter-
example, in a language with three constructions: first, a prefix constructor,
like the prefix of CCS, and with the same rule (it is indeed a tyft rule). We
assume that we can use the prefix construction with at least two distinct
labels, $a$ and $b$. Second, a constant $\mathbf{0}$, that has no rule (as in
CCS). Third, a constructor $\mathtt{forward}$ with the following tyft rule:

$\displaystyle{x\mathrel{\stackrel{{\scriptstyle{\;\;\mu^{\prime}\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}y~{}~{}~{}~{}y\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}z\over{\mathtt{forward}(x)\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}z}}$

Then, the equation $X=a.\mathtt{forward}(X)$ is autonomous or (strongly)
guarded, but does not enjoy unique solution for $\approx$: both $a.\mathbf{0}$
and $a.b.\mathbf{0}$ are solution for $\approx$.

##  5\. Name Passing: the $\pi$-calculus

###  5.1. Unique solution in the asynchronous $\pi$-calculus

In this section, we port our results onto the asynchronous $\pi$-calculus,
$A\pi$ [SW01] (addressing the full $\pi$-calculus would also be possible, but
somewhat more involved). The theory of $A\pi$ is simpler than that of the
synchronous $\pi$-calculus. Notably, bisimulation does not require closure
under name instantiation.

#### Equation expressions, processes and systems of equations.

For the $\pi$-calculus, we inherit the notations from CCS.
$a,b,\ldots,x,y,\ldots$ range over the infinite set of names, and $X,Y,\ldots$
range over equation variables.

In the $\pi$-calculus, the solutions of equations are _process abstractions_ ,
i.e., processes which are made parametric over their free names. This allows
us to work with closed agents, which makes the treatment of equations easier
(in particular w.r.t. name capture).

In order to define the syntactical entities involved in the reasoning about
the $\pi$-calculus, it is useful to start by introducing equation expressions,
ranged over using $E,E^{\prime},\ldots$, as follows:

$\displaystyle F$ $\displaystyle~{}:=~{}K\;\;\mbox{\Large{$\mid$}}\;\;X$
(abstraction identifiers) $\displaystyle E$
$\displaystyle~{}:=~{}{\boldsymbol{0}}\;\;\mbox{\Large{$\mid$}}\;\;a({\widetilde{b}}).E\;\;\mbox{\Large{$\mid$}}\;\;\overline{a}\langle{{\widetilde{b}}}\rangle\;\;\mbox{\Large{$\mid$}}\;\;E_{1}|E_{2}\;\;\mbox{\Large{$\mid$}}\;\;{\boldsymbol{\nu}}a\>E\;\;\mbox{\Large{$\mid$}}\;\;!a({\widetilde{b}}).E\;\;\mbox{\Large{$\mid$}}\;\;F\langle{\widetilde{a}}\rangle$
(equation expressions)

Inputs of the form $c({\widetilde{a}}).E$ and $!c({\widetilde{a}}).E$, and
restrictions ${\boldsymbol{\nu}}a\>E$ are binders for the names
${\widetilde{a}}$ and $a$, with scope $E$.

Replication could be avoided in the syntax since it can be encoded with
recursion. However replication is a useful construct for examples and it is
therefore convenient to have it as a primitive in the syntax because some of
the conditions for our unique-solution theorems will then be easier to check
(we only allow replicated inputs, which are guarded).

The grammar for equation expressions includes the application construct
$F\langle{\widetilde{a}}\rangle$, used to instantiate the formal parameters of
the abstraction identifier $F$ with the actual parameters ${\widetilde{a}}$.
Indeed, since the operational semantics of the $\pi$-calculus makes use of
name substitution, the body of recursive definitions and of equations is
parametrised over a set of names (as will be apparent below).

_Processes_ , ranged over using $P,Q,\ldots$, are defined as equation
expressions in which no occurrence of equation variables is allowed (therefore
the grammar for processes, $P$, is like the grammar for $E$ above, except that
$K$ replaces $F$).

_Process abstractions_ are of the form $({\widetilde{a}})\,P$, where
${\widetilde{a}}$ is a non-empty tuple of distinct names. In
$({\widetilde{a}})\,P$, names ${\widetilde{a}}$ are bound in $P$, giving rise
to the usual notion of bound and free names. A process abstraction is _closed_
if it has no free name.

_Agents._ Processes, process abstractions, and constant identifiers form the
set of _agents_ :

$A\quad:=\quad
P\;\;\mbox{\Large{$\mid$}}\;\;({\widetilde{a}})\,P\;\;\mbox{\Large{$\mid$}}\;\;K\hskip
56.9055pt$

An agent is _closed_ if it does not have free names.

_Recursive definitions._ $K$ is used to stand for recursively defined
abstractions. Each $K$ should have a defining equation of the form
$K\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}({\widetilde{a}})\,P$,
with the additional constraint that $({\widetilde{a}})\,P$ is closed (i.e., it
has no free name).

_Systems of equations._ In order to write equations, we need to work with
_equation abstractions_ , written $({\widetilde{a}})\,E$, where
${\widetilde{a}}$ is a non-empty tuple of distinct names. Again, in
$({\widetilde{a}})\,E$, names ${\widetilde{a}}$ are bound in $E$, giving rise
to the usual notion of bound and free names. We say that
$({\widetilde{a}})\,E$ is _closed_ if it has no free name.

An equation is of the form $X=({\widetilde{a}})\,E$, where the body
$({\widetilde{a}})\,E$ of the equation is closed, and can contain the equation
variable $X$. A solution of such an equation is given by a _closed_ process
abstraction of the form $({\widetilde{b}})\,P$ (or, in the case where
${\widetilde{a}}$ is empty, by a closed process). Imposing this condition
allows us to ignore difficulties related to name capture (if, for instance, we
substitute (non closed) $P=a(x).Q$ for $X$ in the equation expression
$E={\boldsymbol{\nu}}a\>\,X$, name $a$ gets captured by the restriction).

Equation variables occurring in equation expressions can be instantiated with
process abstractions. When doing so, we instantiate names in the process
abstractions according to the usages of the equation variable in the equation
expression; this operation is done implicitly, and does not correspond to a
computation step. We illustrate this on an example:

######  Example .

Consider the equation expression
$E=\overline{c}\langle{d}\rangle|X\langle{\widetilde{a}}\rangle$, having $X$
as only equation variable. Then $E[({\widetilde{b}})\,P]$ stands for
$\overline{c}\langle{d}\rangle|P\\{{\widetilde{a}}/{\widetilde{b}}\\}$. Note
that the equation associated to equation expression $E$ is of the form
$X=(c,d,{\widetilde{a}})\,E$.

We can also instantiate equation variables with equation abstractions: if
$E_{1}$ is an equation expression and $({\widetilde{a}})\,E_{2}$ is an
equation abstraction, then $E_{1}[E_{2}]$ stands for the equation expression
obtained by instantiating the variable in $E_{1}$ with
$({\widetilde{a}})\,E_{2}$.

The definitions above for equations are extended to systems of equations; in
particular, the solution of a system of equations is given by a tuple of
process abstractions.

As in CCS, we can turn equations into recursive definitions; this yields the
_syntactic solution_ of the equations.

_Sorting._ Since the calculus is polyadic, we assume a _sorting system_
[Mil99] to avoid disagreements in the arities of the tuples of names carried
by a given name. The sorting is extended to agents in the expected manner.
Similarly, when considering equation variables, it is intended that each
variable has a sort so that we know the number and the sorts of their
parameters. An equation expression is also sorted, and, accordingly,
composition of equation expressions is supposed to be well-sorted.

We will not present the sorting system because it is well-studied (cf. [Mil99,
SW01]), and adapting it to our setting raises no particular difficulty. The
reader should take for granted that all agents described obey a sorting.

#### Transitions.

As in CCS, transitions are of the form
$P\mathrel{\stackrel{{\scriptstyle{\;\;\mu\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P^{\prime}$,
where the grammar for actions is given by

$\mu\quad:=\quad
a({\widetilde{b}})\;\;\mbox{\Large{$\mid$}}\;\;{\boldsymbol{\nu}}\widetilde{d}\>\overline{a}\langle{{\widetilde{b}}}\rangle\;\;\mbox{\Large{$\mid$}}\;\;\tau\enspace.$

${\boldsymbol{\nu}}\emptyset\>\overline{a}\langle{{\widetilde{b}}}\rangle$ is
written simply $\overline{a}\langle{{\widetilde{b}}}\rangle$. Free and bound
names of an action are defined as usual. Figure 5 presents the transition
rules for $A\pi$. We maintain from CCS the notations for transitions, such as
$\mathrel{\stackrel{{\scriptstyle{\;\;\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$,
$\mathrel{\stackrel{{\scriptstyle{\;\;{\hat{\mu}}\;\;}}}{{\mbox{$\mathord{\smash{=}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{=}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\Rightarrow}$}}}}$,
and so on.

a(~b).P $\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$a(~b) P !a(~b).P $\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$a(~b) !a(~b).P | P ¯a⟨~b⟩$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$¯a⟨~b⟩ 0 P$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$ν ~d¯a⟨~b⟩ P’ ν n P$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$ν ({n}∪~d) ¯a⟨~b⟩  P’ n∈~bP$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$μ P’ ν n P$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$μ ν n P’ d∉na(μ) P$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$a(~b) P’Q$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$ν ~d¯a⟨~b’⟩ Q’ P | Q$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$τ ν ~d (P’{$\widetilde{b^{\prime}}$ / ${\widetilde{b}}$} | Q’) P$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$μ P’P | Q$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$μ P’ | Qbn(μ)∩fn(Q)=∅P{~b/~a}$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$μ P’K ⟨~b ⟩$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$μ P’  if K=$\triangle$(~a) P

Figure 5. $A\pi$: Labelled Transition Semantics

In bisimulations or similar coinductive relations for the asynchronous
$\pi$-calculus, no name instantiation is required in the input clause or
elsewhere (provided $\alpha$-convertible processes are identified); i.e., the
_ground_ versions of the relations are congruence relations [SW01]. Similarly,
the extension of bisimilarity to agents only considers fresh names: $A\approx
A^{\prime}$ if $A\langle{\widetilde{a}}\rangle\approx
A^{\prime}\langle{\widetilde{a}}\rangle$ where ${\widetilde{a}}$ is a tuple of
fresh names (as usual, of the appropriate sort).

######  Example .

If $K$ is the syntactic solution of the equation $X=(a)~{}!a(x).X\langle
x\rangle$, then we have $K\langle
b\rangle\mathrel{\stackrel{{\scriptstyle{\;\;b(y)\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}K\langle
y\rangle|K\langle b\rangle$.

Theorems 3.1 and 3.2 for CCS can be adapted to the asynchronous
$\pi$-calculus. The definitions concerning transitions and divergences are
transported to $A\pi$ as expected. In the case of an abstraction, one first
has to instantiate the parameters with fresh names; thus $F$ has a divergence
if the process $F\langle{\widetilde{a}}\rangle$ has a divergence, where
${\widetilde{a}}$ are fresh names.

######  Theorem  (Unique solution in A$\pi$).

A guarded system of equations whose syntactic solutions do not contain
divergences has a unique solution for $\approx$.

###### Proof.

Because we only consider closed abstractions, all names are instantiated when
performing a substitution of a variable by an abstraction. This allows us to
use the same proof as for Theorem 3.2 in CCS. ∎

######  Theorem  (Unique solution with innocuous divergences in A$\pi$).

A guarded system of equations whose syntactic solutions only have innocuous
divergences has a unique solution for $\approx$.

###### Proof.

The proof of Theorem 5.1 has to be modified exactly as in the CCS case, where
the proof of Theorem 3.1 is modified to establish Theorem 3.2. ∎

As in CCS, the guardedness condition can be removed if the rule for the
unfolding of a constant produces a $\tau$-transition.

We now state an analogue of Lemma 3.3 for $A\pi$, giving a sufficient
condition to guarantee that a system of equations only has innocuous
divergences. This condition is decidable, and sufficient for the application
in Section 5.2. We leave the study of finer conditions for future work.

######  Lemma .

Consider a well-sorted system of equations $\widetilde{X}=\widetilde{E}$ in
$A\pi$ (in particular, for each $i$, the sort of $X_{i}$ and of $E_{i}$ are
the same).

Suppose that there is a sort of names such that names of that sort are never
used in subject output position. If for each $i$ there is $n_{i}$ such that in
$(E_{i})^{n_{i}}$, each equation variable occurs underneath an (input) prefix
of that sort, then the system has only innocuous divergences.

In earlier sections about CCS, we pointed out the connection between
techniques based on unique solution of equations and enhancements of the
bisimulation proof method. The same connection is less immediate in name-
passing calculi, where indeed there are noticeable differences. In particular,
‘up to context’ enhancements for the ground bisimilarity of the $\pi$-calculus
require closure under name instantiation, even when ground bisimilarity is
known to be preserved by substitutions (it is an open problem whether the
closure can be lifted). Thus, when comparing two derivatives $C[P]$ and
$C[Q]$, in general it is not sufficient that $P$ and $Q$ alone are in the
candidate relation: one is required to include also all their closures under
name substitutions (or, if the terms in the holes are abstractions,
instantiation of their parameters with arbitrary tuples of names). In
contrast, the two unique solution theorems above are ‘purely ground’:
$F=({\widetilde{x}})P$ is solution of an equation $X=({\widetilde{x}})E$ if
$P$ and $E\\{\raisebox{2.15277pt}{\small$F$}\\!/\\!\mbox{\small$X$}\\}$ are
ground bisimilar – a single ground instance of the equation is evaluated.

#### The full $\pi$-calculus

In the full $\pi$-calculus, including the output prefix
$\overline{a}\langle{{\widetilde{b}}}\rangle.P$, ground bisimilarity is not a
congruence. One has therefore to use other forms of bisimilarity. The most
used is _early bisimilarity_ ; correspondingly one uses an early transition
system, where the parameters of inputs are instantiated with arbitrary (i.e.,
not necessarily fresh) names, as in
$a(\widetilde{x}).P\mathrel{\stackrel{{\scriptstyle{\;\;{a}\langle{{\widetilde{b}}}\rangle\;\;}}}{{\mbox{$\mathord{\smash{-}}\mkern-6.0mu\cleaders\hbox{$\mkern-2.0mu\mathord{\smash{-}}\mkern-2.0mu$}\hfill\mkern-6.0mu\mathord{\rightarrow}$}}}}P\\{\raisebox{2.15277pt}{\small${\widetilde{b}}$}\\!/\\!\mbox{\small$\widetilde{x}$}\\}$.
Modulo the move to the early setting, the theory exposed for the asynchronous
$\pi$-calculus also holds in the full $\pi$-calculus.

However, when considering a different LTS, such as the early LTS, divergences
that did not exist in the ground LTS may arise, and as such, prevent Theorems
5.1 or 5.1 to be used. It is even possible that, by considering a different
LTS, an equation that had a unique solution loses this property. We leave the
study of this question for future work.

###  5.2. An application: encoding of the call-by-name $\lambda$-calculus

To show an extended application of our techniques for the $\pi$-calculus, we
revisit the proof of full abstraction for Milner’s encoding of the call-by-
name (or lazy) $\lambda$-calculus into $A\pi$ [Mil92] with respect to Lévy
Longo Trees (LTs), precisely the completeness part. We use $M,N$ to range over
the set $\Lambda$ of $\lambda$-terms, and $x,y,z$ to range over $\lambda$
variables.

We assume the standard concepts of free and bound variables and substitutions,
and identify $\alpha$-convertible terms. The terms in $\Lambda$ are sometimes
call _open_ to distinguish them from the subset of _closed_ terms – those
without free variables. The rules defining the call-by-name strategy, defined
on open terms, are the following: (λx . M) N→M{N/x} M→M’ M N →M’ N

As usual $\Rightarrow$ is the reflexive and transitive closure of the single-
step reduction $\rightarrow$.

We write $M\Uparrow$ if $M$ diverges. If $M$ is an open $\lambda$-term, then
either $M$ diverges, or $M\Rightarrow\lambda x.M^{\prime}$ (for some $x$ and
$M^{\prime}$), or $M\Rightarrow x~{}M_{1}~{}\dots~{}M_{n}$ (for some $x$,
$M_{1}$, …, $M_{n}$).

The following notion of tree is used to provide a semantics for the call-by-
name $\lambda$-calculus.

######  Definition  (Lévy-Longo Tree).

The _Lévy-Longo Tree_ (LT) of an open $\lambda$-term $M$, written $LT(M)$, is
the (possibly infinite) tree defined coinductively as follows.

  1. (1)

If $M$ diverges, then $LT(M)$ is the tree with a single node labelled $\bot$.

  2. (2)

If $M\Rightarrow\lambda x.M^{\prime}$, then $LT(M)$ is the tree with a root
labelled with "$\lambda x.$", and $LT(M^{\prime})$ as its unique descendant.

  3. (3)

If $M\Rightarrow x~{}M_{1}~{}\dots~{}M_{n}$, then $LT(M)$ is the tree with a
root labelled with "$x$", and $LT(M_{1}),\dots,LT(M_{n})$ (in this order) as
its $n$ descendants.

LT equality (whereby two $\lambda$-terms are identified if their LTs are
equal) can also be presented as a bisimilarity (_open bisimilarity_ ,
$\simeq^{o}$), defined as the largest _open bisimulation_.

######  Definition .

A relation ${\mathcal{R}}$ on $\Lambda$ is an _open bisimulation_ if, whenever
$M\mathrel{\mathcal{R}}N$:

  1. (1)

$M\Rightarrow\lambda x.M^{\prime}$ implies $N\Rightarrow\lambda x.N^{\prime}$
with $M^{\prime}\mathrel{\mathcal{R}}N^{\prime}$;

  2. (2)

$M\Rightarrow x~{}M_{1}~{}\dots~{}M_{n}$ with $n\geq 0$ implies $N\Rightarrow
x~{}N_{1}~{}\dots~{}N_{n}$ and $M_{i}\mathrel{\mathcal{R}}N_{i}$ for all
$1\leq i\leq n$.

  3. (3)

The converse of clauses 1 and 2 on the challenges from $N$.

[[San00, SX18]] Let $M$ and $N$ be two $\lambda$-terms; then $LT(M)=LT(N)$ iff
$M\simeq^{o}N$.

Milner’s encoding of the call-by-name $\lambda$-calculus into $A\pi$ [Mil92] is defined as follows: [ [ λx. M ]  ] =$\triangle$ (p) p (x,q). [ [ M ]  ] ⟨q ⟩ [ [ x ]  ] =$\triangle$ (p) ¯x⟨p⟩ [ [ M N ]  ] =$\triangle$ (p) ν r, x ([ [ M ]  ] ⟨r ⟩ | ¯r⟨x,p⟩|!x(q).[ [ N ]  ] ⟨q ⟩)

Function application is translated into a particular form of parallel
combination of two agents, the function and its argument; $\beta$-reduction is
then modeled as process interaction. Since the syntax of the $\pi$-calculus
only allows for the transmission of names along channels, the communication of
a term is simulated by the communication of a trigger for it. The translation
of a $\lambda$-term is an abstraction that is parametric on a name, the
_location_ of the $\lambda$-term, which is intuitively the name along which
the term, as a function, will receive its argument. Precisely, the encoding of
a term receives two names along its location $p$: the first is a trigger for
its argument and the second is the location to be used for the next
interaction.

The full abstraction theorem for the encoding [San00, SX18] states that two
$\lambda$-terms have the same LT iff their encodings into $A\pi$ are weakly
bisimilar terms. Full abstraction has two components: soundness, which says
that if the encodings are weakly bisimilar then the original terms have the
same LT; and completeness, which is the converse direction. The proof [San00,
SX18] first establishes an operational correspondence between the behaviour
(visible and silent actions) of $\lambda$-terms and of their encodings. Then,
exploiting this correspondence, soundness and completeness are proved using
the bisimulation proof method. For soundness, this amounts to following the
defining clauses of open bisimulation (Definition 5.2). In contrast,
completeness involves enhancements of the bisimulation proof method, notably
‘bisimulation up to context and expansion’. In the latter, _expansion_ is an
auxiliary preorder relation, finer than weak bisimilarity. As a consequence,
the technique requires having developed the basic theory for the expansion
preorder (e.g., precongruence properties and basic algebraic laws), and
requires an operational correspondence fine enough in order to be able to
reason about expansion (expansion appears within the statements of operational
correspondence).

Below we show that, by appealing to unique solution of equations, completeness
can be proved by defining an appropriate system of equations, each equation
having a simple shape, and without the need for auxiliary preorders. For this,
the only results needed are: $(i)$ validity of $\beta$-reduction for the
encoding (Lemma 5.2), whose proof is simple and consists in the application of
a few algebraic laws (including laws for replication); $(ii)$ the property
that if $M$ diverges then $[\\![M]\\!]\langle p\rangle$ may never produce a
visible action (Lemma 5.2); $(iii)$ a Lemma for rearranging parallel
composition and restrictions in the process encoding
$x~{}M_{1}~{}\dots~{}M_{n}$ (Lemma 5.2).

######  Lemma  (Validity of $\beta$-reduction, [San00]).

For $M\in\Lambda$, if $M\rightarrow M^{\prime}$ then
$[\\![M]\\!]\approx[\\![M^{\prime}]\\!]$.

######  Lemma .

If $M$ diverges, then $[\\![M]\\!]\approx(p)\,{\boldsymbol{0}}$.

[[San00]] For any $M_{1},\dots,M_{n}\in\Lambda$, and variable $x$, we have

$\displaystyle[\\![x~{}M_{1}~{}\dots~{}M_{n}]\\!]$
$\displaystyle=(p)\,({\boldsymbol{\nu}}r_{0},\ldots,r_{n}\>)\big{(}\overline{x}\langle{r_{0}}\rangle|\overline{r_{0}}\langle{r_{1},x_{1}}\rangle|\ldots|\overline{r_{n-1}}\langle{r_{n},x_{n}}\rangle|$
$\displaystyle\quad\quad\quad\quad\quad\quad\quad!x_{1}(q_{1}).[\\![M_{1}]\\!]\langle
q_{1}\rangle|\ldots|!x_{n}(q_{n}).[\\![M_{n}]\\!]\langle
q_{n}\rangle\big{)}\enspace.$

######  Theorem  (Completeness, [San00]).

For $M,N\in\Lambda$, $LT(M)=LT(N)$ implies $[\\![M]\\!]\approx[\\![N]\\!]$.

###### Proof.

Suppose $M_{0}$ and $N_{0}$ are two $\lambda$-terms with the same LT. We
define a system of equations, whose solutions are obtained from the encodings
of $M_{0}$ and $N_{0}$. We will then use Theorem 5.1 to deduce
$[\\![M_{0}]\\!]\approx[\\![N_{0}]\\!]$.

Since $M_{0}$ and $N_{0}$ have the same LT, then by Theorem 5.2 there is an
open bisimulation ${\mathcal{R}}$ containing the pair $(M_{0},N_{0})$. The
variables of the equations are of the form $X_{M,N}$ for
$M\mathrel{\mathcal{R}}N$, and there is one equation for each pair in
${\mathcal{R}}$.

We consider a pair $(M,N)$ in $\mathrel{\mathcal{R}}$, and explain how the
corresponding equation is defined. We assume an ordering of the
$\lambda$-calculus variables so to be able to view a finite set of variables
as a tuple. This allows us to write ${\widetilde{x}}$ for the variables
appearing free in $M$ or $N$.

The equations are the translation of the clauses of Definition 5.2, assuming a
generalisation of the encoding to equation variables by adding the clause:
$[\\![X_{M,N}]\\!]\stackrel{{\scriptstyle\mbox{\scriptsize
def}}}{{=}}({\widetilde{x}},p)X_{M,N}\langle{\widetilde{x}},p\rangle$.

Since $M\mathrel{\mathcal{R}}N$, then either both $M$ and $N$ diverge, or they
satisfy one of the two clauses of Definition 5.2.

  * •

If $M,N$ are both divergent, then the equation is
$X_{M,N}=({\widetilde{x}},p)!\tau$. (as $!\tau\approx[\\![\Omega]\\!]$)

  * •

If $M,N$ satisfy clause 1 of Definition 5.2, the equation is

$X_{M,N}=({\widetilde{x}},p)\,[\\![\lambda
x.X_{M^{\prime},N^{\prime}}]\\!]\langle p\rangle\enspace,\quad\mbox{ that is,
}\quad
X_{M,N}=({\widetilde{x}},p)\,p(x,q).X_{M^{\prime},N^{\prime}}\langle\widetilde{y},q\rangle\enspace,$

where $\widetilde{y}$ are the free variables in $M^{\prime},N^{\prime}$.

  * •

If $M,N$ satisfy clause 2 of Definition 5.2, the equation is given by the
translation of $x~{}X_{M_{1},N_{1}}\ldots X_{M_{n},N_{n}}$, which, rearranging
restrictions and parallel compositions (Lemma 5.2), can be written

$X_{M,N}=({\widetilde{x}},p)({\boldsymbol{\nu}}r_{0},\ldots,r_{n}\>)\big{(}\begin{array}[t]{l}\overline{x}\langle{r_{0}}\rangle|\overline{r_{0}}\langle{r_{1},x_{1}}\rangle|\ldots|\overline{r_{n-1}}\langle{r_{n},x_{n}}\rangle|\\\
!x_{1}(q_{1}).X_{M_{1},N_{1}}\langle\widetilde{x_{1}},q_{1}\rangle|\ldots|!x_{n}(q_{n}).X_{M_{n},N_{n}}\langle\widetilde{x_{n}},q_{n}\rangle\,\big{)}\end{array}$

where $\widetilde{x_{i}}$ are the free variables in $M_{i},N_{i}$.

Essentially, each equation above represents the translation of a specific node
of the LT for $M$ and $N$.

We then rely on Lemma 5.1 to show that the equations may only produce
innocuous divergences. It is easy to check that the syntactic condition holds:
a location name may only appear once (in input position); a trigger name
either appears once (as a replicated input), or it only appears in output
position.

Now, for $(M,N)\in{\mathcal{R}}$, define $F_{M,N}$ as the abstraction
$({\widetilde{x}},p)[\\![M]\\!]\langle p\rangle$, and similarly
$G_{M,N}\stackrel{{\scriptstyle\mbox{\scriptsize$\triangle$}}}{{=}}({\widetilde{x}},p)[\\![N]\\!]\langle
p\rangle$. Lemma 5.2 allows us to show that the set of all such abstractions
$F_{M,N}$ yields a solution for the system of equations, and similarly for
$G_{M,N}$.

We reason by cases, following Definition 5.2.

  * •

If clause (1) of Definition 5.2 holds, then $M\Rightarrow
x~{}M_{1}~{}\dots~{}M_{n}$ and we have

$\displaystyle F_{M,N}$ $\displaystyle=(\widetilde{y},p)[\\![M]\\!]\langle
p\rangle$ $\displaystyle\approx(\widetilde{y},p)[\\![xM_{1}\dots
M_{n}]\\!]\langle p\rangle$ (by Lemma 5.2)
$\displaystyle=(\widetilde{y},p)p(x,q).[\\![M^{\prime}]\\!]q$
$\displaystyle=(\widetilde{y},p)\big{(}p(x,q).X_{M^{\prime},N^{\prime}}\langle\widetilde{z}\rangle\big{)}\\{F_{M^{\prime},N^{\prime}}/X_{M^{\prime},N^{\prime}}\\}$

where $\widetilde{z}$ is a subset of $x,\widetilde{y}$, containing the free
variables of $M$ and $N$.

  * •

If clause (2) holds, then $M\Rightarrow\lambda x.M^{\prime}$ and we have

$\displaystyle F_{M,N}$ $\displaystyle=(\widetilde{y},p)[\\![M]\\!]\langle
p\rangle$
$\displaystyle\approx(\widetilde{y},p)({\boldsymbol{\nu}}r_{0},\ldots,r_{n}\>)\big{(}\overline{x}\langle{r_{0}}\rangle|\overline{r_{0}}\langle{r_{1},x_{1}}\rangle|\ldots|\overline{r_{n-1}}\langle{r_{n},x_{n}}\rangle|$
$\displaystyle\quad\quad!x_{1}(q_{1}).[\\![M_{1}]\\!]{q_{1}}|\ldots|!x_{n}(q_{n}).[\\![M_{n}]\\!]{q_{n}}\,\big{)}$
(by Lemmas 5.2 and 5.2)
$\displaystyle\approx(\widetilde{y},p)({\boldsymbol{\nu}}r_{0},\ldots,r_{n}\>)\big{(}\overline{x}\langle{r_{0}}\rangle|\overline{r_{0}}\langle{r_{1},x_{1}}\rangle|\ldots|\overline{r_{n-1}}\langle{r_{n},x_{n}}\rangle|$
$\displaystyle\quad\quad!x_{1}(q_{1}).X_{M_{1},N_{1}}\langle\widetilde{x_{1}},q_{1}\rangle|\ldots|!x_{n}(q_{n}).X_{M_{n},N_{n}}\langle\widetilde{x_{n}},q_{n}\rangle\,\big{)}$
$\displaystyle\quad\quad\\{F_{M_{1},N_{1}}/X_{M_{1},N_{1}},\dots,F_{M_{n},N_{n}}/X_{M_{n},N_{n}}\\}$

  * •

If neither clause (1) or (2) hold, meaning both $M$ and $N$ diverge, then we
have

$\displaystyle F_{M,N}$ $\displaystyle=({\widetilde{x}},p)[\\![M]\\!]\langle
p\rangle$ $\displaystyle\approx({\widetilde{x}},p){\boldsymbol{0}}$ (by Lemma
5.2) $\displaystyle\approx({\widetilde{x}},p)!\tau$

Since $F_{M,N}$ and $G_{M,N}$ are both solutions of the system of equations,
they are bisimilar, which finally allows us to deduce that
$[\\![M_{0}]\\!]\approx[\\![N_{0}]\\!]$ ∎

##  6\. Conclusions & Future Work

We have compared our techniques to one of the most powerful forms of
enhancements of the bisimulation proof method, namely Pous ‘up to transitivity
and context’, showing that, up to a technical condition, our techniques are at
least as powerful. We believe that also the converse holds, though possibly
under different side conditions. We leave a detailed analysis of this
comparison, which seems non-trivial, for future work. In this respect, the
goal of the work on unique solution of equations is to provide a way of better
understanding up-to techniques and to shed light into the conditions for their
soundness. The technique by Pous, in particular, is arguably more complex,
both in its definition and its application, than the unique solution theorems
presented here.

As said above, the comparison with up-to techniques could also help
understanding the need for the closure under substitutions in up to context
techniques for name-passing calculi such as the asynchronous $\pi$-calculus.
Surprisingly, our unique solution techniques, despite the strong similarities
with up-to context techniques, do not require the closure under substitutions.
However, currently it is unclear how to formally relate bisimulation
enhancements and ‘unique solution of equations’ in name-passing calculi.

Up-to techniques have been analysed in an abstract setting using lattice
theory [Pou16] and category theory [BPPR17, RBR13]. It could be interesting to
do the same for the unique-solution techniques, to study their connections
with up-to techniques, and to understand which equivalences can be handled
(possibly using, or refining, the abstract formulation presented in Section
4).

In comparison with the enhancements of the bisimulation proof method, the main
drawback of the techniques exposed in this paper is the presence of a semantic
condition, involving divergence: the unfoldings of the equations should not
produce divergences, or only produce innocuous divergences. A syntactic
condition for this has been proposed (Lemma 3.3). Various techniques for
checking divergence in concurrent calculi exist in the literature, including
type-based techniques [YBH04, DHS10, DS06]. However, in general divergence is
undecidable, and therefore, the check may sometimes be unfeasible.
Nevertheless, the equations that one writes for proofs usually involve forms
of ‘normalised’ processes, and as such they are divergence-free (or at most,
contain only innocuous divergences). More experiments are needed to validate
this claim or to understand how limiting this problem is.

Several studies in functional programming and type theory rely on type-based
methods to insure that coinductive definitions are productive, i.e., do not
give rise to partially defined functions (in order to preserve logical
consistency) [Nak00, AM13]. Understanding whether these approaches can be
adapted to analyse divergences and innocuous divergences in systems of
equations is a topic for future investigations.

##### Acknowledgements.

This work was supported by Labex MILYON/ANR-10-LABX-0070, by the European
Research Council (ERC) under the Horizon 2020 programme (CoVeCe, grant
agreement No 678157), by H2020-MSCA-RISE project ‘Behapi’ (ID 778233), and by
the project ANR-16-CE25-0011 REPAS.

## References

  * [AFV01] Luca Aceto, Wan Fokkink, and Chris Verhoef.  Handbook of Process Algebra (J.A. Bergstra and A. Ponse and S.A. Smolka, editors), chapter Structural operational semantics.  Elsevier Science, 2001.
  * [AM13] Robert Atkey and Conor McBride.  Productive coprogramming with guarded recursion.  In Greg Morrisett and Tarmo Uustalu, editors, ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA - September 25 - 27, 2013, pages 197–208. ACM, 2013.
  * [BBR10] Jos C.M. Baeten, Twan Basten, and Michel A. Reniers.  Process Algebra: Equational Theories of Communicating Processes.  Cambridge University Press, 2010.
  * [BHR84] Stephen D. Brookes, C. A. R. Hoare, and A. W. Roscoe.  A theory of communicating sequential processes.  J. ACM, 31(3):560–599, 1984.
  * [BIM88] Bard Bloom, Sorin Istrail, and Albert R. Meyer.  Bisimulation can’t be traced.  In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 229–239, 1988.
  * [BIM95] Bard Bloom, Sorin Istrail, and Albert R. Meyer.  Bisimulation can’t be traced.  J. ACM, 42(1):232–268, 1995.
  * [BPPR17] Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot.  A general account of coinduction up-to.  Acta Inf., 54(2):127–190, 2017.
  * [BR84] Stephen D. Brookes and A. W. Roscoe.  An improved failures model for communicating processes.  In Seminar on Concurrency, Carnegie-Mellon University, Pittsburg, PA, USA, pages 281–305, 1984.
  * [BW90] J. C. M. Baeten and W. P. Weijland.  Process Algebra.  Cambridge University Press, New York, NY, USA, 1990.
  * [DHS10] Romain Demangeon, Daniel Hirschkoff, and Davide Sangiorgi.  Termination in impure concurrent languages.  In CONCUR 2010 - Concurrency Theory, 21th International Conference, pages 328–342, 2010.
  * [DHS17] Adrien Durier, Daniel Hirschkoff, and Davide Sangiorgi.  Divergence and unique solution of equations.  In Proc. of CONCUR’2017, volume 85 of LIPIcs, pages 11:1–11:16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017.
  * [DHS18] Adrien Durier, Daniel Hirschkoff, and Davide Sangiorgi.  Eager functions as processes.  In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 364–373. ACM, 2018.
  * [DS06] Yuxin Deng and Davide Sangiorgi.  Ensuring termination by typability.  Inf. Comput., 204(7):1045–1082, 2006.
  * [Dur17] Adrien Durier.  Divergence and unique solution of equations in an abstract setting, Coq formal proof.  Available at https://github.com/adurier/uniquesolution/, 2017\.
  * [FvG16] Wan Fokkink and Rob J. van Glabbeek.  Divide and congruence II: delay and weak bisimilarity.  In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, pages 778–787. ACM, 2016.
  * [GM14] Jan Friso Groote and Mohammad Reza Mousavi.  Modeling and Analysis of Communicating Systems.  MIT Press, 2014.
  * [GV92] Jan Friso Groote and Frits W. Vaandrager.  Structured operational semantics and bisimulation as a congruence.  Inf. Comput., 100(2):202–260, 1992.
  * [Hoa85] C. A. R. Hoare.  Communicating Sequential Processes.  Prentice-Hall, 1985.
  * [Mil89] Robin Milner.  Communication and concurrency.  PHI Series in computer science. Prentice Hall, 1989.
  * [Mil92] Robin Milner.  Functions as processes.  Mathematical Structures in Computer Science, 2(2):119–141, 1992\.
  * [Mil99] Robin Milner.  Communicating and mobile systems - the Pi-calculus.  Cambridge University Press, 1999.
  * [MRG07] Mohammad Reza Mousavi, Michel A. Reniers, and Jan Friso Groote.  SOS formats and meta-theory: 20 years after.  Theor. Comput. Sci., 373(3):238–272, 2007.
  * [Nak00] Hiroshi Nakano.  A modality for recursion.  In 15th Annual IEEE Symposium on Logic in Computer Science, Santa Barbara, California, USA, June 26-29, 2000, pages 255–266. IEEE Computer Society, 2000.
  * [Pou08] Damien Pous.  Up to techniques for bisimulations.  PhD thesis, ENS Lyon, February 2008.
  * [Pou16] Damien Pous.  Coinduction all the way up.  In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, pages 307–316, 2016.
  * [PS11] Damien Pous and Davide Sangiorgi.  Advanced Topics in Bisimulation and Coinduction (D. Sangiorgi and J. Rutten editors), chapter Enhancements of the coinductive proof method.  Cambridge University Press, 2011.
  * [RBR13] Jurriaan Rot, Marcello M. Bonsangue, and Jan J. M. M. Rutten.  Coalgebraic bisimulation-up-to.  In SOFSEM 2013: Theory and Practice of Computer Science, 39th International Conference on Current Trends in Theory and Practice of Computer Science, pages 369–381, 2013.
  * [Ros92] A. W. Roscoe.  An alternative order for the failures model.  J. Log. Comput., 2(5):557–577, 1992.
  * [Ros97] A. W. Roscoe.  The Theory and Practice of Concurrency.  Prentice Hall PTR, Upper Saddle River, NJ, USA, 1997.
  * [Ros10] A. W. Roscoe.  Understanding Concurrent Systems.  Springer, 2010.
  * [San00] Davide Sangiorgi.  Lazy functions and mobile processes.  In G. Plotkin, C. Stirling, and M. Tofte, editors, Proof, Language and Interaction: Essays in Honour of Robin Milner. MIT Press, 2000\.
  * [San15] Davide Sangiorgi.  Equations, contractions, and unique solutions.  In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, pages 421–432, 2015.
  * [SW01] Davide Sangiorgi and David Walker.  The Pi-Calculus - a theory of mobile processes.  Cambridge University Press, 2001.
  * [SX18] Davide Sangiorgi and Xian Xu.  Trees from functions as processes.  Logical Methods in Computer Science, 14(3), 2018.
  * [Vaa92] Frits W. Vaandrager.  Expressiveness results for process algebras.  In Sematics: Foundations and Applications, REX Workshop, Beekbergen, The Netherlands, June 1-4, 1992, Proceedings, pages 609–638, 1992\.
  * [vG90] Rob J. van Glabbeek.  The linear time-branching time spectrum (extended abstract).  In CONCUR ’90, Theories of Concurrency: Unification and Extension, Amsterdam, The Netherlands, August 27-30, 1990, Proceedings, pages 278–297, 1990.
  * [vG05] Rob J. van Glabbeek.  On cool congruence formats for weak bisimulations.  In Theoretical Aspects of Computing - ICTAC 2005, Second International Colloquium, pages 318–333, 2005.
  * [YBH04] Nobuko Yoshida, Martin Berger, and Kohei Honda.  Strong Normalisation in the Pi-Calculus.  Information and Computation, 191(2):145–202, 2004.


# Quantum particle under dynamical confinement:
From quantum Fermi acceleration to high harmonic generation

S. Rakhmanova,c, C. Trunkb and D. Matrasulovc aChirchik State Pedagogical
University, 104 Amur Temur Str., Chirchik, 111700,Uzbekistan
b Technische Universität Ilmenau, Postfach 100565, 98684 Ilmenau, Germany
c Turin Polytechnic University in Tashkent, 17 Niyazov Str., 100095, Tashkent,
Uzbekistan

###### Abstract

Quantum dynamics of a particle confined in a box with time-dependent wall is
revisited by considering some unexplored aspects of the problem. In
particular, the case of dynamical confinement in a time-dependent box in the
presence of purely time-varying external potential is treated by obtaining
exact solution. Also, some external potentials approving separation of space
and time variables in the Schrödinger equation with time-dependent boundary
conditions are classified. Time-dependence of the average kinetic energy and
average quantum force are analyzed. A model for optical high harmonic
generation in the presence of dynamical confinement and external linearly
polarized monochromatic field is proposed.

## Acknowledgement

This research is partially supported by European Union’s Horizon 2020 research
and innovation programme under the Marie Sklodowska-Curie grant agreement ID:
873071, project SOMPATY (Spectral Optimization: From Mathematics to Physics
and Advanced Technology).

##  1 Introduction

Dynamical confinement in quantum mechanics attracted much attention during
past few decades. It is described in terms of the Schrödinger equation with
time-dependent boundary conditions.

Early treatments of the problem date back to Doescher, who explored basic
aspects of the problem [1]. Munier et al. considered more detailed treatment
of the problem and computed some physically observable quantities for the
problem of time-dependent box [2]. Later Makowsky [3]-[5] and Razavy [6, 7]
presented a systematic study of the problem, by considering one-dimensional
box with moving walls and classifying time-dependence of the wall approving
exact solution of the Schrödinger equation with time-dependent boundary
conditions. Unitary transformation mapping time-dependent box to that with
fixed walls was found in [6, 7] using an approach developed earlier by Berry
and Klein [8]. Some aspects of the problem of quantum box with moving walls
and its applications to dynamical Casimir effect was studied in a series of
papers by Dodonov et al. [9]-[12]. Berry phase in time-dependent box was
considered in [13, 14, 15]. Seba considered the problem of time-dependent box
in the context of quantum Fermi acceleration [16]. Application of the time-
dependent box to the problem of confined quantum gas was considered in [17,
18], where quantum force operator for dynamical confinement was introduced.

The problem of hydrogen atom confined in time-dependent spherical box was
considered in [19]. Time-dependent harmonic oscillator which is directly
related to time-dependent quantum box was presented in a series of papers by
Lewis [20, 21]. Different aspects of the problem of dynamical confinement was
studied in [22] -[28]. Inverse problem for dynamical confinement, i.e. the
problem of recovering boundary’s time-dependence from existing solution is
considered in [29]. Dynamical confinement in a half-line is studied in [30].
The probem of time-dependent Neumann boundary conditions is treated in [31].
Extension of the dynamical confinement to relativistic case by considering
Dirac equation for time-dependent box was done in [32]. Time-dependent quantum
graphs have been considered in the Refs.[33, 34, 35].

Despite the fact that considerable aspects of the problem of dynamical
confinement have been considered, some issues in the topic are still remaining
as less- or not studied. This concerns such aspects as time-dependent Neumann
boundary conditions, non-adiabatic limit and exactly solvable models. Another
important problem in this context is extension of the model to the case when
time-dependent box interacts with an external potential. In such case, if the
potential is position independent, the problem approves factorization of space
and time variables.

In this paper we address the problem of dynamical confinement in the presence
of a external electromagnetic field. By assuming that time-dependence of the
wall’s position approves separation of space and time-variables, we obtain
general solution of the problem and compute such physically observable
characteristics, as average kinetic energy and average force. Moreover, we
consider the case of dynamical confinement driven by external linearly
polarized monochromatic optical field. For this system, we study high harmonic
generation induced by optical field.

This paper is organized as follows. In the next section we briefly recall the
problem of time-dependent boundary conditions for the Schrodinger equation on
a quantum box. In Section 3 we consider a particle in a time-dependent box in
the presence of external potentials with the focus on exactly solvable cases,
i.e., when the problem allows factorization of the time- and space variables.
Section 4 presents the treatment of the average kinetic energy of the particle
and of the average quantum force acting to the particle by moving wall.
Section 5 presents a quantum optics model for dynamical confinement by
considering high harmonic generation, Fermi acceleration and average quantum
force as a function of time.

##  2 Dynamical confinement in 1D quantum box

Here, following [3, 6], we briefly recall the problem of time-dependent
boundary conditions in quantum mechanics, by considering 1D quantum box with
moving wall. Consider a particle confined between two infinitely high walls.
The position of the left wall is assumed to be fixed at $x=0$, while the right
one moves according to some positively determined function $L(t)$ which is a
smooth function, $L:[0,\infty)\rightarrow(0,\infty)$. Then the particle
dynamics in such a box is described in terms of the following time-dependent
Schrödinger equation ($\hbar=m=1$):

$i\frac{\partial\Psi(x,t)}{\partial t}=H(x,t)\Psi(x,t),\quad
t\in[0,\infty),x\in[0,L(t)]$ (1)

with the Hamiltonian

$H(x,t)=-\frac{1}{2}\frac{\partial^{2}}{\partial x^{2}}+V(x,t).$ (2)

Here, for simplicity, we assume the potential $V$ to be continuous on its
domain $\\{(x,t)\,|\,t\in[0,\infty),x\in[0,L(t)]\\}$. We impose, for Equation
(1), the following Dirichlet boundary conditions given at the interval
$[0,L(t)]$:

$\Psi(x,t)|_{x=0}=\Psi(x,t)|_{x=L(t)}=0.$ (3)

Introducing a new coordinate

$y=\frac{x}{L(t)},$ (4)

Equation (1) can be rewritten as

$i\frac{\partial\Psi(y,t)}{\partial
t}=-\frac{1}{2L^{2}}\frac{\partial^{2}\Psi(y,t)}{\partial
y^{2}}+i\frac{\dot{L}}{L}y\frac{\partial\Psi(y,t)}{\partial
y}+V(yL(t),t)\Psi(y,t),$ (5)

where $\dot{L}=dL/dt$ and new boundary conditions are given by

$\Psi(y,t)|_{y=0}=\Psi(y,t)|_{y=1}=0forallt\in[0,\infty).$ (6)

However, such transformation leads to breaking of the self-adjointness of the
problem, i.e., the Schrödinger operator in the right hand side of (5) is not
self-adjoint. Therefore, one needs to recover self-adjointness using the
transformation

$\Psi(y,t)=\sqrt{2/L}\exp{\Biggl{(}\frac{i}{2}L\dot{L}y^{2}\Biggl{)}}\varphi(y,t),$
(7)

that reduces Equation (5) to the following form [3]

$i\frac{\partial\varphi(y,t)}{\partial
t}=-\frac{1}{2L^{2}}\frac{\partial^{2}\varphi(y,t)}{\partial
y^{2}}+\Biggl{(}\frac{1}{2}L\ddot{L}y^{2}+V\Biggl{)}\varphi(y,t),$ (8)

where $\ddot{L}=d\dot{L}/dt$ and $\varphi(y,t)$ satisfies the boundary
conditions (6). We mention that (8) can also be obtained from Equation (1) via
some unitary transformation, cf. [7].

In this section we consider the case $V=0$. Assume that the expression
$4L^{3}\ddot{L}$ is a non-positive constant for all $t\in[0,\infty)$, i.e.

$0\leq B^{2}=-4L^{3}\ddot{L}=\textnormal{const}$ (9)

for some real $B$. Introduce a new “time variable” $\tau$ via

$\tau(t)=\int_{0}^{t}\frac{ds}{[L(s)]^{2}}.$ (10)

Equation (8) reduces to

$i\frac{\partial\varphi(y,\tau)}{\partial\tau}=-\frac{1}{2}\frac{\partial^{2}\varphi(y,\tau)}{\partial
y^{2}}-\frac{1}{8}B^{2}y^{2}\varphi(y,\tau),$ (11)

see also [3]. The solution of (11) can now be factorized as

$\varphi(y,\tau)=f(\tau)\Phi(y).$ (12)

Using a separation constant $K$, the equation for $\Phi$ reduces to the Kummer
equation

$z\frac{d^{2}U}{dz^{2}}+\Biggl{(}\frac{1}{2}-z\Biggl{)}\frac{dU}{dz}+\frac{1}{4}(\kappa^{2}-1)U=0,$
(13)

where $z=(iB/2)y^{2},\kappa^{2}=4K/iB,U(z)=\exp{(z/2)}\Phi(z)$. Hence (see
13.1.13 from [36]) the Kummer function
$z^{1/2}M\Big{(}\frac{3-\kappa^{2}}{4},\frac{3}{2},z\Big{)}$ is a solution of
Equation (13). Hence, a solution for

$H_{0}\Phi(y)=K\Phi(y)\quad\mbox{with
}H_{0}:=-\frac{1}{2}\frac{d^{2}}{dy^{2}}-\frac{1}{8}B^{2}y^{2}.$ (14)

is of the form

$\Phi(y)=CyM\Biggl{(}\frac{3iB-4K}{4iB},\frac{3}{2},\frac{iB}{2}y^{2}\Biggl{)}e^{-\frac{iB}{4}y^{2}},$
(15)

where $C$ is the normalization constant. Exact solution of Equation (1) can be
written as [3]

$\Psi(x,t)=\frac{Cx}{\sqrt{L^{3}}}e^{\frac{i}{2}x^{2}\left(\frac{\dot{L}}{L}-\frac{B}{2L^{2}}\right)-iK\tau(t)}M\left(\frac{3iB-4K}{4iB},\frac{3}{2},\frac{iB}{2}\frac{x^{2}}{L^{2}}\right).$
(16)

Note that $\Psi(0,t)=0$ for all $t$. However, $\Psi(L,t)=0$ if and if

$M\left(\frac{3iB-4K}{4iB},\frac{3}{2},\frac{iB}{2}\right)=0.$ (17)

Therefore the boundary condition (3) is satisfied if and only if $K$ equals a
zero of the Kummer function in (17). Denote these zeros by $K_{n}$, $n\in N$.
Define the function $\Psi_{n}$ via the right hand side of Equation (16) where
$K$ is replaced by $K_{n}$.

It is important to mention that the time-dependent Dirichlet boundary
conditions imposed for (1) approve norm conservation. Indeed, let $N(t)$ be
the norm at time $t$ as the $L^{2}$-norm of $\Psi$ with respect to the spatial
variable $x$,

$N(t):=||\Psi(x,t)||^{2}=\int^{L(t)}_{0}|\Psi|^{2}dx.$ (18)

Then, for the time-derivative we have

$\frac{dN}{dt}(t)=\int^{L(t)}_{0}\frac{\partial}{\partial
t}|\Psi(x,t)|^{2}dx+\dot{L}(t)|\Psi|^{2}|_{x=L(t)}=\int^{L(t)}_{0}\frac{\partial}{\partial
t}|\Psi(x,t)|^{2}dx$ (19)

Taking into account (1), (3) and

$i\int^{L(t)}_{0}\frac{\partial}{\partial
t}|\Psi|^{2}dx=\frac{1}{2}\left.\left(\Psi\frac{\partial\Psi^{*}}{\partial
x}-\Psi^{*}\frac{\partial\Psi}{\partial x}\right)\right|^{x=L(t)}_{x=0}=0,$
(20)

we have norm conservation $\frac{dN}{dt}(t)=0$.

##  3 Dynamical confinement in the presence of external potential:
Exactly solvable models

The model in Section 2 approves factorization of the variables in the case of
constraint (9). However, when the system interacts with an external position-
independent time-varying field, factorization is also possible. Here we
consider time-dependent quantum box driven by external purely time-dependent
potential $V$. The dynamics of the system is governed by the following time-
dependent Schrödinger equation:

$i\frac{\partial\Psi(x,t)}{\partial
t}=-\frac{1}{2}\frac{\partial^{2}\Psi(x,t)}{\partial x^{2}}+V(t)\Psi(x,t)$
(21)

The boundary conditions for this equation are imposed as in (3). Following the
previous section, we transform the boundary conditions into time-independent
ones by introducing a new coordinate $y$ which is given by (4). Using the
transformation of the wave function given by Equation (7) and under the
assumption that $L(t)$ fulfills the condition in Equation (9), we have with
Equation (8)

$iL^{2}\frac{\partial\varphi(y,t)}{\partial
t}=-\frac{1}{2}\frac{\partial^{2}\varphi(y,t)}{\partial
y^{2}}-\frac{1}{8}B^{2}y^{2}\varphi(y,t)+L^{2}V(t)\varphi(y,t),$ (22)

Let $\Phi_{n}$ satisfy (14) with Dirichlet boundary conditions (17) with
respect to the eigenvalue $K=K_{n}$ and denote its normalization constant by
$C_{n}$. It is well-known that the system $\\{\Phi_{n}\\}_{n}$ forms an
orthonormal basis of $L^{2}(0,1)$. We choose as an Ansatz for the solution of
(22)

$\varphi(y,t)=\sum_{n}C_{n}(t)\Phi_{n}(y)$ (23)

By substituting (23) into Equation (22), we (formally) obtain

$iL^{2}\sum_{n}\dot{C}_{n}(t)\Phi_{n}(y)=\sum_{n}C_{n}(t)H_{0}\Phi_{n}(y)+L^{2}V(t)\sum_{n}C_{n}(t)\Phi_{n}(y).$
(24)

Then, after multiplying both sides of equation to $\Phi_{m}^{*}(y)$,
integrating over $y$ and using the orthonormal condition for a basis,
$\int_{0}^{1}\Phi_{m}^{*}(y)\Phi_{n}(y)dy=\delta_{mn}$, we have

$iL^{2}\dot{C}_{n}(t)=C_{n}(t)K_{n}+L^{2}V(t)C_{n}(t)$ (25)

It’s solution is in the form

$C_{n}(t)=C_{n}(0)e^{-i\int_{0}^{t}\big{(}\frac{K_{n}}{L^{2}}+V(s)\big{)}ds}$
(26)

where $C_{n}(0)$ can be determined from a smooth initial condition which
insures $\sum_{n}|C_{n}(0)|^{2}<\infty$. Finally, one obtains the general
solution for Equation (21)

$\displaystyle\Psi(x,t)=\sum_{n}C_{n}(0)e^{-i\int_{0}^{t}\big{(}\frac{K_{n}}{L^{2}}+V(s)\big{)}ds}C_{n}\sqrt{\frac{2}{L^{3}}}xM\Biggl{(}\frac{3iB-4K_{n}}{4iB},\frac{3}{2},\frac{iB}{2}\frac{x^{2}}{L^{2}}\Biggl{)}$
$\displaystyle\times
e^{-\frac{iB}{4}\frac{x^{2}}{L^{2}}+\frac{i}{2}\frac{\dot{L}}{L}x^{2}}.$ (27)

It is worthful to consider some other potentials approving factorization of
variables in the Schrödinger equation with time-dependent boundary conditions.
One of them is interaction proportional to inverse square of the distance
given as

$V=\frac{\alpha}{x^{2}}$

where $\alpha$ is constant. For this case Equation (8) can be written as

$i\frac{\partial\varphi(y,t)}{\partial
t}=-\frac{1}{2L^{2}}\frac{\partial^{2}\varphi(y,t)}{\partial
y^{2}}+\Biggl{(}\frac{1}{2}L\ddot{L}y^{2}+\frac{\alpha}{L^{2}y^{2}}\Biggl{)}\varphi(y,t),$
(28)

Variables of this equation can be separated, provided $L(t)$ fulfills (9).

Similarly to the above, one can show that potential in the form
$V=x\varepsilon(t)$ also approves of separation time and space variables and
one obtains Schrödinger equation for anharmonic oscillator given as

$i\frac{\partial\varphi(y,t)}{\partial
t}=-\frac{1}{2L^{2}}\frac{\partial^{2}\varphi(y,t)}{\partial
y^{2}}+\Biggl{(}\frac{1}{2}L\ddot{L}y^{2}+Ly\varepsilon(t)\Biggl{)}\varphi(y,t),$
(29)

Variables of this equation can be separated when
$L^{3}\ddot{L}=\textnormal{const}=\beta$ and
$L^{3}\varepsilon(t)=\textnormal{const}=\gamma$ conditions are fulfilled. From
those two conditions one can see $\varepsilon(t)=\frac{\gamma}{\beta}\ddot{L}$
and (29) becomes

$iL^{2}\frac{\partial\varphi(y,t)}{\partial
t}=-\frac{1}{2}\frac{\partial^{2}\varphi(y,t)}{\partial
y^{2}}+\frac{1}{2}\beta y^{2}\varphi(y,t)+\gamma y\varphi(y,t).$ (30)

Finally, for potential given in the form of nonlinearly polarized
monochromatic field given by $V=x^{2}\epsilon\cos\omega t,$ where $\epsilon$,
$\omega$ are strength and frequency of external field, one can also factorize
space and time variables and have

$i\frac{\partial\varphi(y,t)}{\partial
t}=-\frac{1}{2L^{2}}\frac{\partial^{2}\varphi(y,t)}{\partial
y^{2}}+\Biggl{(}\frac{1}{2}L\ddot{L}y^{2}+L^{2}y^{2}\epsilon\cos\omega
t\Biggl{)}\varphi(y,t),$ (31)

Conditions for factorization of variables for this equation given in the form
of constraint $L^{3}\ddot{L}+2\epsilon L^{4}\cos\omega
t=\textnormal{const}=\beta$.

##  4 Average kinetic energy and quantum force induced by dynamical
confinement

Having found the solution of the Schrödinger equation for time-dependent
quantum box, one can compute physically observable variables, such as average
kinetic energy and average (quantum) force. The average kinetic energy is
determined as the expectation value of the kinetic energy operator:

$\hat{H}=-\frac{1}{2}\frac{\partial^{2}}{\partial x^{2}}.$ (32)

The expectation value of energy is given by

$<E(t)>=\langle\Psi|\hat{H}|\Psi\rangle,$ (33)

where $|\Psi\rangle$ is a solution of (21). We have

$<E_{k}(t)>=\int_{0}^{L(t)}\Psi^{*}(x,t)\Biggl{(}-\frac{1}{2}\frac{\partial^{2}}{\partial
x^{2}}\Biggl{)}\Psi(x,t)dx=\frac{1}{2}\int_{0}^{L(t)}\Biggl{|}\frac{\partial\Psi(x,t)}{\partial
x}\Biggl{|}^{2}dx$ (34)

or with (7)

$<E_{k}(t)>=\frac{1}{L^{2}}\int_{0}^{1}\Biggl{|}\frac{\partial\varphi(y,t)}{\partial
y}\Biggl{|}^{2}dy+\frac{2\dot{L}}{L}\textnormal{Im}\Biggl{(}\int_{0}^{1}y\varphi^{*}(y,t)\frac{\partial\varphi(y,t)}{\partial
y}dy\Biggl{)}+$
$\dot{L}^{2}\int_{0}^{1}y^{2}|\varphi(y,t)|^{2}dy=\frac{1}{L^{2}}S_{0}+\frac{2\dot{L}}{L}\textnormal{Im}(S_{1})+\dot{L}^{2}S_{2}.$

Explicit expressions for $S_{0},\;$ $S_{1}\;$ and $S_{2}\;$ are provided in
Appendix A.

Quantum force can be determined as the expectation value of the force operator
as

$\hat{F}=-\frac{\partial\hat{H}}{\partial L(t)}.$ (35)

Then for the expectation value of the force operator one has [17]

$<F(t)>=-\frac{\partial\langle E_{k}(t)\rangle}{\partial
L}=\frac{2}{L^{3}}S_{0}+\frac{2\dot{L}}{L^{2}}\textnormal{Im}(S_{1}).$ (36)

##  5 Quantum Fermi acceleration and high harmonic generation in driven time-
dependent box

An important effect that can be realized in a quantum box with oscillating
walls is the so-called Fermi acceleration in quantum regime, or quantum Fermi
acceleration. It is a quantum analog of the classical Fermi acceleration that
occurs in bouncing balls colliding with oscillating wall. In classical regime,
unbounded growth of the average kinetic energy of a particle can be observed
in such a system. Quantum Fermi acceleration in a time-dependent box was
studied in [7, 16]. Here we extend these studies to the case of interaction
(in addition to the interaction with oscillating wall) with an external time-
periodic potential.

Figure 1: Average kinetic energy and force as a function of time at different
values of amplitude of oscillating wall $a$ for $L_{0}=10$, $\omega_{0}=0.5$,
$\epsilon=0.1$ and $\omega=0.05$ ($L=L_{0}+a\cos\omega_{0}t$ and V=$\epsilon
x\cos\omega t$).

We consider a version of the dynamically confined system which can be
experimentally realized in optics. Namely, we propose a model for time-
dependent box driven by linearly polarized monochromatic field given by

$V(x,t)=\epsilon x\cos\omega t,$ (37)

where $\epsilon$ and $\omega$ are the field strength and the frequency,
respectively.

In the following we consider a quantum particle in a box with oscillating wall
and interacting with the external linearly polarized monochromatic field given
by (37). Wall’s oscillation is assumed to be given as

$L=L_{0}+a\cos\omega_{0}t.$

In this case, Equation (8) cannot be separated and one has to solve it
numerically. Here we will use the following Ansatz for $\varphi(y,t)$:

$\large\varphi(y,t)=\sum_{n}C_{n}(t)\sin\pi ny,$ (38)

where $\phi_{n}(y):=\sin\pi ny$ solves the equation
$-\frac{1}{2}\frac{d^{2}\phi_{n}}{dy^{2}}=\frac{\pi^{2}n^{2}}{2}\phi_{n}$ with
Dirichlet boundary conditions on the interval $[0,1]$.

Figure 2: Average kinetic energy and force as a function of time at different
values of field strength $\epsilon$ for $L_{0}=10$, $a=3$, $\omega_{0}=0.5$
and $\omega=0.05$ ($L=L_{0}+a\cos\omega_{0}t$ and V=$\epsilon x\cos\omega t$).

For the coefficients $C_{n}$ we have the following system of differential
equations

$\large
iL^{2}\dot{C}_{n}(t)=C_{n}(t)\frac{\pi^{2}n^{2}}{2}+\sum_{m}V_{nm}C_{m}(t)$
(39)

where $V_{nm}=L^{3}\ddot{L}I_{1nm}+2\epsilon L^{3}\cos\omega tI_{2nm}$ and

$I_{1nm}=\int_{0}^{1}y^{2}\phi_{n}^{*}\phi_{m}dy=\left\\{\begin{array}[]{l}\quad\qquad\frac{1}{6}+\frac{1}{4n^{2}\pi^{2}},\qquad\qquad\;n=m\\\
\frac{1}{\pi^{2}}\Big{(}\frac{(-1)^{m-n}}{(m-n)^{2}}-\frac{(-1)^{m+n}}{(m+n)^{2}}\Big{)},\qquad
n\neq m\end{array}\right.$

and

$I_{2nm}=\int_{0}^{1}y\phi_{n}^{*}\phi_{m}dy=\left\\{\begin{array}[]{l}\quad\qquad\qquad\frac{1}{4},\qquad\qquad\qquad\quad\;\;n=m\\\
\frac{1}{2\pi^{2}}\Big{(}\frac{(-1)^{m-n}-1}{(m-n)^{2}}-\frac{(-1)^{m+n}-1}{(m+n)^{2}}\Big{)},\qquad
n\neq m\end{array}\right.$

We solve (39) numerically by choosing initial condition as $C_{1}(0)=1$ and
$C_{n}(0)=0$ for $n\neq 1$. Having found $C_{n}(t)$ one constructs $\phi_{n}$
and $\Psi$ via (4) and (7).

In Figure 1 time-dependence of the average kinetic energy of the particle
$<E_{k}>$ and the quantum force $<F>$ acting on the wall are plotted at
different values of the wall’s oscillation amplitude $a$. For smaller values
of $a$ both average kinetic energy and force are periodic, while at higher
values they become quasi periodic and certain growth of the ”peaks” can be
observed. However, suppression of the growth occurs as time elapses.

Figure 3: Average kinetic energy and force as a function of time at different
values of frequency of external field $\omega$ for $L_{0}=10$, $a=3$,
$\omega_{0}=0.5$ and $\epsilon=0.1$ ($L=L_{0}+a\cos\omega_{0}t$ and
V=$\epsilon x\cos\omega t$).

Figure 2 presents the time-dependence of the average kinetic energy and the
force at different values of the external field strength $\epsilon$. The
behavior of $<E_{k}(t)>$ and $<F(t)>$ are similar to that in Figure 1, which
implies similarity of the roles of $\epsilon$ and $a$ in the particle
dynamics. In other words, particle ”feels” both, oscillating wall and external
monochromatic field as a periodic perturbation.

In Figures 3 and 4, $<E_{k}(t)>$ and $<F(t)>$ are plotted at different values
of the external field and oscillating boundary frequency for $L_{0}=10$,
respectively. Qualitatively plots look similar to those in Figures 1 and 2.

Figure 4: Average kinetic energy and force as a function of time at different
values of frequency of oscillating wall $\omega_{0}$ for $L_{0}=10$, $a=3$,
$\epsilon=0.1$ and $\omega=0.05$ ($L=L_{0}+a\cos\omega_{0}t$ and V=$\epsilon
x\cos\omega t$).

An important effect which can be considered in the system time-dependent
quantum box+ external monochromatic field is optical high harmonic generation
(HHG) induced by interaction of the time-dependent box with external optical
field given by (37). Evolution of the whole system, ”dynamical box + optical
field” is governed by (1).

Detailed description of the high harmonic generation in quantum regime can be
found in [38]. Here we will focus on the role of confinement in optical
harmonic generation. The main physical characteristics of such process is the
average dipole moment which is given by [38]

$<d(t)>=-<\Psi(x,t)|x|\Psi(x,t)>.$

The spectrum of high harmonic generation (HHG) is characterized by the
quantity [38]

$I(\nu)=|<d(\nu)>|^{2}=\Biggl{|}\frac{1}{T}\int_{0}^{T}e^{-i\nu
t}<d(t)>dt\Biggl{|}^{2},$ (40)

where $T$ is the total duration of interaction.

Figure 5 shows plots of the spectrum of harmonic generation as a function of
harmonic order at different values of external field strength for $L_{0}=10$,
$a=3$, $\omega_{0}=0.5$, $\omega=1$ and $T=200$. The plot shows that the HHG
intensity strongly depends on the field strength. For higher values of
$\epsilon$, one can observe increasing of intensity. Figure 6 presents plots
of HHG-spectra at different amplitudes of oscillating box. An important
feature of the HHG-spectra presented in Figures 5 and 6 is the existence of a
plateau in the curves, i.e. there is rather side range of frequencies having
the same intensity of generation (emission). Such a feature is of importance
from the viewpoint of applications of the model in attosecond physics, where
wide range of generated high frequencies with high enough intensity is
required.

Figure 5: Spectrum of HHG as a function of harmonic order at different values
of field strength $\epsilon$ for $L_{0}=10$, $a=3$, $\omega_{0}=0.5$,
$\omega=1$ and T=200 ($L=L_{0}+a\cos\omega_{0}t$ and $V=\epsilon x\cos\omega
t$).

##  6 Conclusion

In this paper we considered the problem of dynamical confinement in a time-
dependent 1D quantum box interacting with external potentials. The main focus
is given to find an exact solution of the problem. In particular, an exact
solution of the problem is obtained for the purely time-dependent external
potential. Some other external potentials approving factorization of space and
time variables in the time-dependent Schrödinger equation with moving boundary
conditions are classified.

Average kinetic energy and quantum force for the particle simultaneously
subjected to the influence of dynamical confinement and external time-periodic
field are analyzed as a function of time. A model for high harmonic generation
in time-dependent box that can be experimentally realized in quantum optics,
is proposed. The spectrum of high harmonics generated by such system is
computed.

The proposed model can be directly applied to the problems of tunable quantum
Fermi acceleration and quantum transport in low-dimensional confined systems
arising in optics and condensed matter. An extension of the model to the case
of 2D and 3D systems, where the role of boundaries geometry is very
challenging is a task for forthcoming studies.

Figure 6: Spectrum of HHG as a function of harmonic order at different values
of amplitude of oscillating box $a$ for $L_{0}=10$ $\epsilon=0.1$,
$\omega_{0}=0.5$, $\omega=1$ and $T=100$ ($L=L_{0}+a\cos\omega_{0}t$ and
$V=\epsilon x\cos\omega t$).

## Appendix A

Here we will give explicit forms of the quantities $S_{0},\;$ $S_{1}\;$ and
$S_{2}\;$ Using the solution of Equation (22) one can find $S_{0},\;$
$S_{1}\;$ and $S_{2}\;$ that are defined as

$S_{0}=\sum_{n,m}C_{n}^{*}(t)C_{m}(t)\Biggl{[}I_{1}+\frac{W_{m}}{6}I_{2}+\frac{W_{n}^{*}}{6}I_{2}^{*}+\frac{W_{n}^{*}W_{m}}{36}I_{4}-\frac{iBW_{n}^{*}}{12}I_{5}+\frac{iBW_{m}}{12}I_{5}^{*}+\frac{B^{2}}{4}I_{6}\Big{]}$

$S_{1}=\sum_{n,m}C_{n}^{*}(t)C_{m}(t)\Biggl{[}I_{3}+\frac{W_{m}}{6}I_{5}^{*}-\frac{iB}{2}I_{6}\Big{]}$

$S_{2}=\sum_{n,m}C_{n}^{*}(t)C_{m}(t)I_{6}$

with $W_{n}=3iB-4K_{n}$ and $I_{1},\;$ $I_{2},\;$ $I_{3},\;$ $I_{4},\;$
$I_{5},\;$ $I_{6}\;$ given by

$I_{1}=\int_{0}^{1}M^{*}\Biggl{(}\frac{3iB-4K_{n}}{4iB},\frac{3}{2},\frac{iB}{2}y^{2}\Biggl{)}M\Biggl{(}\frac{3iB-4K_{m}}{4iB},\frac{3}{2},\frac{iB}{2}y^{2}\Biggl{)}dy$

$I_{2}=\int_{0}^{1}y^{2}M^{*}\Biggl{(}\frac{3iB-4K_{n}}{4iB},\frac{3}{2},\frac{iB}{2}y^{2}\Biggl{)}M\Biggl{(}\frac{7iB-4K_{m}}{4iB},\frac{5}{2},\frac{iB}{2}y^{2}\Biggl{)}dy$

$I_{3}=\int_{0}^{1}y^{2}M^{*}\Biggl{(}\frac{3iB-4K_{n}}{4iB},\frac{3}{2},\frac{iB}{2}y^{2}\Biggl{)}M\Biggl{(}\frac{3iB-4K_{m}}{4iB},\frac{3}{2},\frac{iB}{2}y^{2}\Biggl{)}dy$

$I_{4}=\int_{0}^{1}y^{4}M^{*}\Biggl{(}\frac{7iB-4K_{n}}{4iB},\frac{5}{2},\frac{iB}{2}y^{2}\Biggl{)}M\Biggl{(}\frac{7iB-4K_{m}}{4iB},\frac{5}{2},\frac{iB}{2}y^{2}\Biggl{)}dy$

$I_{5}=\int_{0}^{1}y^{4}M^{*}\Biggl{(}\frac{7iB-4K_{n}}{4iB},\frac{5}{2},\frac{iB}{2}y^{2}\Biggl{)}M\Biggl{(}\frac{3iB-4K_{m}}{4iB},\frac{3}{2},\frac{iB}{2}y^{2}\Biggl{)}dy$

$I_{6}=\int_{0}^{1}y^{4}M^{*}\Biggl{(}\frac{3iB-4K_{n}}{4iB},\frac{3}{2},\frac{iB}{2}y^{2}\Biggl{)}M\Biggl{(}\frac{3iB-4K_{m}}{4iB},\frac{3}{2},\frac{iB}{2}y^{2}\Biggl{)}dy$

## References

  * [1] S.W. Doescher, H.H. Rice, Am. J. Phys. 37 1246 (1969).
  * [2] A. Munier, J.R. Burgan, M. Feix, E. Fijalkow, J. Math. Phys. 22 1219 (1981).
  * [3] A.J. Makowski, S.T. Dembinski, Phys. Lett. A 154 217 (1991).
  * [4] A.J. Makowski, P. Peptowski, Phys. Lett. A 163 142 (1992).
  * [5] A.J. Makowski, J. Phys. A: Math. Gen. 25 3419(1992).
  * [6] M. Razavy, Lett. Nuovo Cimento 37, 13, 30 Luglio (1983).
  * [7] M. Razavy, Phys. Rev. A 44 2384 (1991).
  * [8] M.V. Berry, G. Klein, J. Phys. A 17, 1805 (1984).
  * [9] V.V. Dodonov, V.I. Man’ko, D.E. Nikonov, Phys. Lett. A 162 359 (1992).
  * [10] V.V. Dodonov, A.B. Klimov, D.E. Nikonov, J. Math. Phys. 34, 2742 (1993).
  * [11] V.V. Dodonov, A.V. Dodonov, J. Phys. A: Math. Gen.39 6271 (2006).
  * [12] A.V. Dodonov, B. Militello, A. Napoli, A. Messina, Phys. Rev. A 93 052505 (2016).
  * [13] P. Pereshogin, P. Pronin, Phys. Lett. A 156 12 (1991).
  * [14] Ohjong Kwon, Yongduk Kim and Chahn Lee, J. Phys. A . 25 61134121 (1992).
  * [15] A-L. Wang and F-P. Liu, Mod. Phys. Lett. B, 28 1450122 (2014).
  * [16] P. Seba. Phys. Rev. A 41 2306 (1990).
  * [17] K. Nakamura, S.K. Avazbaev, Z.A. Sobirov, D.U. Matrasulov, T. Monnai, Phys. Rev. E 83, 041133, (2011).
  * [18] K. Nakamura, Z.A. Sobirov, D.U. Matrasulov, S.K. Avazbaev, Phys. Rev. E 86 061128 (2012).
  * [19] S. Rakhmanov, D. Matrasulov, V.I. Matveev, Eur, J. Phys. D 72 177 (2018).
  * [20] H.R. Lewis Jr., J. Math. Phys. 9 1976 (1968).
  * [21] H.R. Lewis Jr., W.B. Riesenfeld, J. Math. Phys. 10 1458 (1969).
  * [22] D.N. Pinder, Am. J. Phys.58 54 (1990).
  * [23] C. Scheiniger, M.Kleber, Physica D 50 391 (1991).
  * [24] J.D. Lejarreta, J. Phys. A 32, 4749 (1999).
  * [25] Li. Ling, Li. Bo-Zang, Phys. Lett. A 291, 190 (2001).
  * [26] C. Yuce, Phys. Lett. A 321 291 (2004).
  * [27] T.K. Jana, P. Roy, Phys. Lett. A. 372, 2368 (2008).
  * [28] M.L. Glasser, J. Mateo, J. Negro, L.M. Nieto, Chaos, Solitons and Fractals (In press, 2009).
  * [29] J.N. Flavin, J. Math. Anal. Appl. 371, 552 (2010).
  * [30] D.A. Smith, W.Y. Toh, Euro. Jnl of Applied Mathematics: page 1 of 33 (2021).
  * [31] A. Duca, R. Joly, Ann. Henri Poincare 22, 2029 (2021).
  * [32] Z.A. Sobirov, D. Matrasulov, Sh. Ataev, H. Yusupov, In Complex Phenomena in Nanoscale Systems (2009).
  * [33] D.U. Matrasulov, J.R. Yusupov, K.K. Sabirov, Z.A. Sobirov, Nanosystems: Phys. Chem. Math. 6. 173, (2015).
  * [34] D.S. Nikiforov, I.V. Blinova, I.Y. Popov, Indian J. Phys. 93, 913 (2019).
  * [35] U. Smilansky, G. Sofer, ArXiv:2210.14652v1 (2022).
  * [36] M. Abramowitz, I.A. Stegun, Handbook of Mathematical Functions, National Bureau of Standards, Washington (1964).
  * [37] S. Bernet, R. Abfalterer, C. Keller, M. K. Oberthaler, J. Schmiedmayer, A. Zeilinger, Phys. Rev. A 62 023606 (2000).
  * [38] R.W. Boyd, Nonlinear Optics, 3rd ed., Academic Press (2007).