+ For example, the problem of separating $\lambda$-terms popped up inevitably while working with Claudio Sacerdoti Coen and Beniamino Accattoli on the observational equality of the \textit{fireball calculus} \fire{} \cite{DBLP:conf/lics/AccattoliC15}. Our goal here is to provide a suitable notion of \textit{bisimulation} in order to characterize syntactically the equivalence of programs (i.e. contextual equivalence).\r
+\r
+ \subsubsection*{The Fireball Calculus}\r
+\r
+ \fire{} is an \textit{open} call-by-value \lc{}. Recall that \textit{call-by-value} is an evaluation strategy for the \lc{} in which - intuitively - functions' arguments are evaluated before the function call. \fire{} is similar to Plotkin's call-by-value \lc{}, which is at the foundation of programming languages (OCaml) and proof assistants (Coq), but \fire{} (as a \textit{weak calculus}, when reductions occur only outside abstractions) is particularly elegant because:\r
+ \begin{itemize}\r
+ \item it is \textit{strongly confluent};\r
+ \item normal forms have a clean syntactic description as \textit{fireballs}: a fireball is either an abstractions (like values in Plotkin), or a variable possibly applied to other fireballs.\r
+ \end{itemize}\r
+\r
+Strong evaluation may be obtained as usual by iterating the weak one under abstractions. But, mainly because fireballs are not closed under substitutions, the strong calculus has some issues:\r
+\begin{itemize}\r
+ \item it is \textit{not} confluent;\r
+ \item contextual equivalence is not closed under reduction.\r
+ % a term and its strong normal form may not be contextual equivalent (in the usual sense).\r
+ For example: \[(\lambda y.\,z) \, (x\, x) \to_{\beta} z ,\] but in a context replacing the free variable $x$ with $\lambda x.\, x\, x$, the term on the left diverges, and the one on the right converges.\r
+\r
+\end{itemize}\r