$\displaystyle+C_{d}\int\int\frac{|{\mathcal{F}}b(k-l,a)|^{2}}{(1+|l|^{2})^{\frac{d}{2}+1}}dldk\left(\int\frac{|F_{l}({\mathcal{S}}_{0}(\mu))-F_{l}({\mathcal{S}}_{0}(\tilde{\mu}))|^{10+d}}{(1+|l|^{2})^{\lambda}}dl\right)^{\frac{1}{10+d}}.$

Given the bound
$|F_{l}({\mathcal{S}}_{0}(\mu))-F_{l}({\mathcal{S}}_{0}(\tilde{\mu}))|<2$, we
have that

$\displaystyle||d_{3}(\cdot,a)||^{2}_{\lambda}$ $\displaystyle\leq
C\left(||b(\cdot,a)||^{2}_{\lambda}\rho_{F}^{2}(\mu,\tilde{\mu})+C_{d}||b(\cdot,a)||^{2}_{2}\rho_{F}^{\frac{2}{10+d}}(\mu,\tilde{\mu})\right).$

Given our assumption on $b$, this implies

$\displaystyle\sup_{a\in A}||d_{3}(\cdot,a)||_{\lambda}$ $\displaystyle\leq
C\rho_{F}^{\frac{1}{10+d}}\sqrt{1+\rho_{F}^{\frac{18+2d}{10+d}}(\mu,\tilde{\mu})}$

and

$I_{2}\leq
C\rho_{F}^{\frac{1}{10+d}}\sqrt{1+\rho_{F}^{\frac{18+2d}{10+d}}(\mu,\tilde{\mu})}+\frac{C(1+|m(\mu)|)\rho_{F}^{2}(\mu,\tilde{\mu})}{\epsilon}.$

To estimate $I_{3}$ we proceed similarly to the estimation of $I_{2}$.
However, in this case, the term $d_{4}$ is

$-\int\frac{Re(ikk^{\top}f_{k}(x)(F_{k}({\mathcal{S}}_{0}(\mu))-F_{k}({\mathcal{S}}_{0}(\tilde{\mu})))^{*})}{(1+|k|^{2})^{\lambda}}dk.$

Thus, in the estimate of $||d_{3}(\cdot,a)||^{2}_{\lambda}$, we have

$|{\mathcal{F}}d_{4}(l)|=\frac{|l|^{2}|F_{l}({\mathcal{S}}_{0}(\mu))-F_{l}({\mathcal{S}}_{0}(\tilde{\mu}))|}{(1+|l|^{2})^{\lambda}}$

instead of

$\frac{|l||F_{l}({\mathcal{S}}_{0}(\mu))-F_{l}({\mathcal{S}}_{0}(\tilde{\mu}))|}{(1+|l|^{2})^{\lambda}}$

and $C_{d}$ in (8.7) has to be defined with an exponent

$\left(\frac{\lambda}{2}-\frac{1}{2}-\frac{d}{4}-1-\frac{\lambda}{10+d}\right)\frac{20+2d}{8+d}.$

This exponent is still strictly larger than $\frac{d}{2}$, $C_{d}<\infty$, and

$I_{3}\leq
C\rho_{F}^{\frac{1}{10+d}}\sqrt{1+\rho_{F}^{\frac{18+2d}{10+d}}(\mu,\tilde{\mu})}+\frac{C(1+|m(\mu)|)\rho_{F}^{2}(\mu,\tilde{\mu})}{\epsilon}$

which is (3.7).

∎

## References

  * [1] G. Auricchio, A. Codegoni, S. Gualandi, G. Toscani, and M. Veneroni, The equivalence of fourier-based and wasserstein metrics on imaging problems, Rendiconti Lincei, 31 (2020), pp. 627–649.
  * [2] A. Bain and D. Crisan, Fundamentals of stochastic filtering, vol. 60 of Stochastic Modelling and Applied Probability, Springer, New York, 2009\.
  * [3] E. Bandini, A. Cosso, M. Fuhrman, and H. Pham, Randomized filtering and bellman equation in wasserstein space for partial observation control problem, Stochastic Processes and their Applications, 129 (2019), pp. 674–711.
  * [4] E. Bayraktar, A. Cecchin, and P. Chakraborty, Mean field control and finite agent approximation for regime-switching jump diffusions, Appl. Math. Optim., 88 (2023), pp. Paper No. 36, 35.
  * [5] E. Bayraktar, A. Cosso, and H. Pham, Randomized dynamic programming principle and Feynman-Kac representation for optimal control of McKean-Vlasov dynamics, Trans. Amer. Math. Soc., 370 (2018), pp. 2115–2160.
  * [6] E. Bayraktar, I. Ekren, and X. Zhang, Finite-time 4-expert prediction problem, Comm. Partial Differential Equations, 45 (2020), pp. 714–757.
  * [7] , Prediction against a limited adversary, J. Mach. Learn. Res., 22 (2021), pp. Paper No. 72, 33.
  * [8] E. Bayraktar, I. Ekren, and X. Zhang, A PDE approach for regret bounds under partial monitoring, arXiv e-prints, (2022), p. arXiv:2209.01256.
  * [9] E. Bayraktar, I. Ekren, and X. Zhang, A smooth variational principle on Wasserstein space, Proc. Amer. Math. Soc., 151 (2023), pp. 4089–4098.
  * [10] E. Bayraktar, I. Ekren, and Y. Zhang, On the asymptotic optimality of the comb strategy for prediction with expert advice, Ann. Appl. Probab., 30 (2020), pp. 2517–2546.
  * [11] E. Bayraktar, H. V. Poor, and X. Zhang, Malicious experts versus the multiplicative weights algorithm in online prediction, IEEE Trans. Inform. Theory, 67 (2021), pp. 559–565.
  * [12] C. Bertucci, Stochastic optimal transport and Hamilton-Jacobi-Bellman equations on the set of probability measures, arXiv e-prints, (2023), p. arXiv:2306.04283.
  * [13] J. M. Borwein and Q. J. Zhu, Techniques of variational analysis, vol. 20 of CMS Books in Mathematics, Springer-Verlag, New York, 2005.
  * [14] H. Brezis, Functional analysis, Sobolev spaces and partial differential equations, Universitext, Springer, New York, 2011.
  * [15] M. Burzoni, V. Ignazio, A. M. Reppen, and H. M. Soner, Viscosity solutions for controlled mckean–vlasov jump-diffusions, SIAM Journal on Control and Optimization, 58 (2020), pp. 1676–1699.
  * [16] J. Calder and N. Drenska, Asymptotically optimal strategies for online prediction with history-dependent experts, To appear in Journal of Fourier Analysis and Applications Special Issue on Harmonic Analysis on Graphs, (2020).
  * [17] P. Cardaliaguet, F. Delarue, J.-M. Lasry, and P.-L. Lions, The Master Equation and the Convergence Problem in Mean Field Games:(AMS-201), vol. 201, Princeton University Press, 2019.
  * [18] R. Carmona and F. Delarue, Probabilistic theory of mean field games with applications. I, vol. 83 of Probability Theory and Stochastic Modelling, Springer, Cham, 2018.  Mean field FBSDEs, control, and games.
  * [19] , Probabilistic theory of mean field games with applications. II, vol. 84 of Probability Theory and Stochastic Modelling, Springer, Cham, 2018.  Mean field games with common noise and master equations.
  * [20] J. A. Carrillo, G. Toscani, et al., Contractive probability metrics and asymptotic behavior of dissipative kinetic equations, Riv. Mat. Univ. Parma, 6 (2007), pp. 75–198.
  * [21] Y. T. Chow and W. Gangbo, A partial laplacian as an infinitesimal generator on the wasserstein space, Journal of Differential Equations, 267 (2019), pp. 6065–6117.
  * [22] A. Cosso, F. Gozzi, I. Kharroubi, H. Pham, and M. Rosestolato, Master bellman equation in the wasserstein space: Uniqueness of viscosity solutions, to appear in the Transactios of AMS, arXiv:2107.10535, (2023+).
  * [23] A. Cosso and M. Martini, On smooth approximations in the Wasserstein space, arXiv e-prints, (2023), p. arXiv:2303.15160.
  * [24] A. M. Cox, S. Källblad, M. Larsson, and S. Svaluto-Ferro, Controlled measure-valued martingales: a viscosity solution approach, to appear in the Annals of Applied Probability, (2023+).
  * [25] M. G. Crandall, H. Ishii, and P.-L. Lions, User’s guide to viscosity solutions of second order partial differential equations, Bull. Amer. Math. Soc. (N.S.), 27 (1992), pp. 1–67.
  * [26] S. Daudin and B. Seeger, A comparison principle for semilinear Hamilton-Jacobi-Bellman equations in the Wasserstein space, arXiv e-prints, (2023), p. arXiv:2308.15174.
  * [27] N. Drenska and R. V. Kohn, A PDE Approach to the Prediction of a Binary Sequence with Advice from Two History-Dependent Experts, arXiv:2007.12732, (2020).
  * [28] N. Drenska and R. V. Kohn, Prediction with expert advice: a PDE perspective, J. Nonlinear Sci., 30 (2020), pp. 137–173.
  * [29] I. Ekren, C. Keller, N. Touzi, and J. Zhang, On viscosity solutions of path dependent pdes, The Annals of Probability, (2014), pp. 204–236.
  * [30] I. Ekren, N. Touzi, and J. Zhang, Viscosity solutions of fully nonlinear parabolic path dependent pdes: Part i, The Annals of Probability, (2016), pp. 1212–1253.
  * [31] G. Fabbri, F. Gozzi, A. Swikech, M. Fuhrman, and G. Tessitore, Stochastic Optimal Control in Infinite Dimension: Dynamic Programming and HJB Equations, Probability Theory and Stochastic Modelling, Springer International Publishing, 2017.
  * [32] W. Gangbo, S. Mayorga, and A. Swiech, Finite dimensional approximations of hamilton–jacobi–bellman equations in spaces of probability measures, SIAM Journal on Mathematical Analysis, 53 (2021), pp. 1320–1356.
  * [33] W. Gangbo, A. R. Mészáros, C. Mou, and J. Zhang, Mean field games master equations with nonseparable Hamiltonians and displacement monotonicity, Ann. Probab., 50 (2022), pp. 2178–2217.
  * [34] F. Gozzi and A. Świech, Hamilton–jacobi–bellman equations for the optimal control of the duncan–mortensen–zakai equation, Journal of Functional Analysis, 172 (2000), pp. 466–510.
  * [35] H. Ishii and P.-L. Lions, Viscosity solutions of fully nonlinear second-order elliptic partial differential equations, Journal of Differential equations, 83 (1990), pp. 26–78.
  * [36] O. Kallenberg, Foundations of modern probability, vol. 99 of Probability Theory and Stochastic Modelling, Springer, Cham, third ed., [2021] ©2021.
  * [37] H. Kunita, Stochastic flows and stochastic differential equations, vol. 24 of Cambridge Studies in Advanced Mathematics, Cambridge University Press, Cambridge, 1997.  Reprint of the 1990 original.
  * [38] J.-M. Lasry and P.-L. Lions, A remark on regularization in hilbert spaces, Israel Journal of Mathematics, 55 (1986), pp. 257–266.
  * [39] P. Lions, Viscosity solutions of fully nonlinear second-order equations and optimal stochastic control in infinite dimensions. part i: The case of bounded stochastic evolutions, Acta mathematica, 161 (1988), pp. 243–278.
  * [40] P.-L. Lions, Viscosity solutions of fully nonlinear second-order equations and optimal stochastic control in infinite dimensions. iii. uniqueness of viscosity solutions for general second-order equations, Journal of Functional Analysis, 86 (1989), pp. 1–18.
  * [41] , Viscosity solutions of fully nonlinear second order equations and optimal stochastic control in infinite dimensions. part ii: optimal control of zakai’s equation, in Stochastic partial differential equations and applications II, Springer, 1989, pp. 147–170.
  * [42] J. Lott, Some geometric calculations on Wasserstein space, Comm. Math. Phys., 277 (2008), pp. 423–437.
  * [43] M. Martini, Kolmogorov equations on spaces of measures associated to nonlinear filtering processes, Stochastic Processes and their Applications, 161 (2023), pp. 385–423.
  * [44] H. Mete Soner and Q. Yan, Viscosity Solutions of the Eikonal Equation on the Wasserstein Space, arXiv e-prints, (2023), p. arXiv:2308.04097.
  * [45] D. Ocone and E. Pardoux, A generalized Itô-Ventzell formula. Application to a class of anticipating stochastic differential equations, Ann. Inst. H. Poincaré Probab. Statist., 25 (1989), pp. 39–71.
  * [46] D. Possamaï and M. Talbi, Mean-field games of optimal stopping: master equation and weak equilibria, arXiv e-prints, (2023), p. arXiv:2307.09278.
  * [47] H. M. Soner and Q. Yan, Viscosity solutions for mckean-vlasov control on a torus, arXiv preprint arXiv:2212.11053, (2022).
  * [48] M. Talbi, N. Touzi, and J. Zhang, Dynamic programming equation for the mean field optimal stopping problem, SIAM J. Control Optim., 61 (2023), pp. 2140–2164.
  * [49] , Viscosity solutions for obstacle problems on Wasserstein space, SIAM J. Control Optim., 61 (2023), pp. 1712–1736.
  * [50] G. Toscani and C. Villani, Probability metrics and uniqueness of the solution to the boltzmann equation for a maxwell gas, Journal of statistical physics, 94 (1999), pp. 619–637.
  * [51] C. Villani et al., Optimal transport: old and new, vol. 338, Springer, 2009.


Pushdown Normal-Form Bisimulation: A Nominal Context-Free Approach to Program Equivalence
This publication has emanated from research supported in part by a grant from Science Foundation Ireland under Grant number 13/RC/2094_2; and the Cisco University Research Program Fund, a corporate advised fund of Silicon Valley Community Foundation.

Pushdown Normal-Form Bisimulation

Vasileios Koutavas1 Yu-Yang Lin1 Nikos Tzevelekos2
Trinity College Dublin Queen Mary University of London

We propose Pushdown Normal Form (PDNF) Bisimulation to verify contextual equivalence in higher-order functional programming languages with local state.
Similar to previous work on Normal Form (NF) bisimulation, PDNF Bisimulation is sound and complete with respect to contextual equivalence.
However, unlike traditional NF Bisimulation, PDNF Bisimulation is also decidable for a class of program terms that reach bounded configurations but can potentially have unbounded call stacks and input an unbounded number of unknown functions from their context.
Our approach relies on the principle that, in model-checking for reachability, pushdown systems can be simulated by finite-state automata designed to accept their initial/final stack content.
We embody this in a stackless Labelled Transition System (LTS), together with an on-the-fly saturation procedure for call stacks, upon which bisimulation is defined.
To enhance the effectiveness of our bisimulation, we develop up-to techniques and confirm their soundness for PDNF Bisimulation.
We develop a prototype implementation of our technique which is able to verify equivalence in examples from practice and the literature that
were out of reach for previous work.

§ INTRODUCTION

§ LANGUAGE AND SEMANTICS

§ STACKED LTS AND NF BISIMULATION

§ STACKLESS LTS AND PUSHDOWN NF BISIMULATION

§ UP-TO TECHNIQUES

§ IMPLEMENTATION AND EVALUATION

§ RELATED AND FUTURE WORK

[For the purpose of Open Access, the author/s has/have applied a CC BY public copyright licence to any Author Accepted Manuscript version arising from this submission.]

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

titleCountdown Timer | Android Developers.
Accessed: 2023-10-10.

titleDOM Standard.
Accessed: 2023-10-10.

titleEvents | jQuery API Documentation.
Accessed: 2023-10-10.

titleEventTarget - Web APIs | MDN Web Docs.
Accessed: 2023-10-10.

titleInput events overview | Android Developers.
Accessed: 2023-10-10.

titleIntroduction to Event Listeners (The Java™
Accessed: 2023-10-10.

authorpersonSamson Abramsky.
The Lazy Lambda Calculus.
In booktitleResearch Topics in Functional
Programming. publisherAddison-Wesley Longman Publishing Co.,
Inc., addressUSA, pages65–116.

[Abramsky et al(1998)]
authorpersonSamson Abramsky, personKohei
Honda, and personGuy McCusker.
A Fully Abstract Game Semantics for General
References. In booktitleThirteenth Annual IEEE Symposium
on Logic in Computer Science, Indianapolis, Indiana, USA, June 21-24, 1998.
publisherIEEE Computer Society, pages334–344.

[Abramsky et al(2000)]
authorpersonSamson Abramsky, personRadha
Jagadeesan, and personPasquale Malacaria.
Full Abstraction for PCF.
journalInf. Comput. volume163,
number2, pages409–470.

[Ahmed et al(2009)]
authorpersonAmal Ahmed, personDerek Dreyer,
and personAndreas Rossberg. year2009.
State-dependent representation independence. In
booktitleProceedings of the 36th ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA,
USA, January 21-23, 2009, editorpersonZhong Shao
and personBenjamin C. Pierce (Eds.).
publisherACM, pages340–353.

[Biernacki and Lenglet(2012)]
authorpersonDariusz Biernacki and
personSergueï Lenglet. year2012.
Normal Form Bisimulations for Delimited-Control
Operators. In booktitleFunctional and Logic Programming -
11th International Symposium, FLOPS 2012, Kobe, Japan, May 23-25, 2012.
Proceedings (seriesLecture Notes in Computer Science,
Vol. volume7294), editorpersonTom
Schrijvers and personPeter Thiemann (Eds.).
publisherSpringer, pages47–61.

[Biernacki et al(2019)]
authorpersonDariusz Biernacki,
personSergueï Lenglet, and personPiotr
Polesiuk. year2019.
A Complete Normal-Form Bisimilarity for State. In
booktitleFoundations of Software Science and Computation
Structures - 22nd International Conference, FOSSACS 2019, Proceedings
(seriesLecture Notes in Computer Science,
Vol. volume11425), editorpersonMikolaj
Bojanczyk and personAlex Simpson (Eds.).
publisherSpringer, pages98–114.

[Bojanczyk et al(2014)]
authorpersonMikolaj Bojanczyk, personBartek
Klin, and personSlawomir Lasota.
Automata theory in nominal sets.
journalLog. Methods Comput. Sci.
volume10, number3 (year2014).

[Bojanczyk et al(2013)]
authorpersonMikolaj Bojanczyk, personBartek
Klin, personSlawomir Lasota, and personSzymon
Torunczyk. year2013.
Turing Machines with Atoms. In
booktitle28th Annual ACM/IEEE Symposium on Logic in
Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013.
publisherIEEE Computer Society, pages183–192.

[Bouajjani et al(1997)]
authorpersonAhmed Bouajjani, personJavier
Esparza, and personOded Maler.
Reachability Analysis of Pushdown Automata:
Application to Model-Checking. In booktitleCONCUR '97:
Concurrency Theory, 8th International Conference, Warsaw, Poland, July 1-4,
1997, Proceedings (seriesLecture Notes in Computer
Science, Vol. volume1243),
editorpersonAntoni W. Mazurkiewicz and
personJózef Winkowski (Eds.).
publisherSpringer, pages135–150.

[Cheng and Kaminski(1998)]
authorpersonEdward Y. C. Cheng and
personMichael Kaminski. year1998.
Context-Free Languages over Infinite Alphabets.
journalActa Informatica volume35,
number3 (year1998), pages245–267.

authorpersonAleksandar S. Dimovski.
Program verification using symbolic game
journalTheor. Comput. Sci.  volume560
(year2014), pages364–379.

[Dreyer et al(2010)]
authorpersonDerek Dreyer, personGeorg Neis,
and personLars Birkedal. year2010.
The impact of higher-order state and control
effects on local relational reasoning. In
booktitleProceeding of the 15th ACM SIGPLAN
international conference on Functional programming, ICFP 2010, Baltimore,
Maryland, USA, September 27-29, 2010,
editorpersonPaul Hudak and
personStephanie Weirich (Eds.). publisherACM,

[Earl et al(2010)]
authorpersonChristopher Earl, personMatthew
Might, and personDavid Van Horn.
Pushdown Control-Flow Analysis of Higher-Order
journalCoRR  volumeabs/1007.4268

[Esparza et al(2001)]
authorpersonJavier Esparza,
personAntonín Kucera, and personStefan
Schwoon. year2001.
Model-Checking LTL with Regular Valuations for
Pushdown Systems. In booktitleTheoretical Aspects of
Computer Software, 4th International Symposium, TACS 2001, Sendai, Japan,
October 29-31, 2001, Proceedings (seriesLecture Notes in
Computer Science, Vol. volume2215),
editorpersonNaoki Kobayashi and
personBenjamin C. Pierce (Eds.). publisherSpringer,

authorpersonMatthias Felleisen.
titleThe calculi of lambda-nu-cs conversion: a
syntactic theory of control and state in imperative higher-order programming
thesistypePh. D. Dissertation. schoolIndiana

[Felsing et al(2014)]
authorpersonDennis Felsing, personSarah
Grebing, personVladimir Klebanov, personPhilipp
Rümmer, and personMattias Ulbrich.
Automating regression verification. In
booktitleACM/IEEE International Conference on Automated
Software Engineering, ASE '14, Vasteras, Sweden - September 15 - 19,
2014, editorpersonIvica Crnkovic,
personMarsha Chechik, and personPaul
Grünbacher (Eds.). publisherACM,

[Finkel et al(1997)]
authorpersonAlain Finkel, personBernard
Willems, and personPierre Wolper.
A direct symbolic approach to model checking
pushdown systems. In booktitleSecond International Workshop
on Verification of Infinite State Systems, Infinity 1997, Bologna, Italy,
July 11-12, 1997 (seriesElectronic Notes in Theoretical
Computer Science, Vol. volume9),
editorpersonFaron Moller (Ed.).
publisherElsevier, pages27–37.

[Gabbay and Pitts(2002)]
authorpersonMurdoch Gabbay and
personAndrew M. Pitts. year2002.
A New Approach to Abstract Syntax with Variable
journalFormal Aspects Comput.
volume13, number3-5 (year2002),

[Gamma et al(1995)]
authorpersonErich Gamma, personRichard
Helm, personRalph Johnson, and personJohn
Vlissides. year1995.
booktitleDesign patterns: elements of reusable
object-oriented software.
publisherPearson Deutschland GmbH.

[Ghica and McCusker(2003)]
authorpersonDan R. Ghica and personGuy
McCusker. year2003.
The regular-language semantics of second-order
idealized A\({}_{\mbox{LGOL}}\).
journalTheor. Comput. Sci. volume309,
number1-3 (year2003), pages469–502.

[Ghica and Tzevelekos(2012)]
authorpersonDan R. Ghica and personNikos
Tzevelekos. year2012.
A System-Level Game Semantics. In
booktitleProceedings of the 28th Conference on the
Mathematical Foundations of Programming Semantics, MFPS 2012, Bath, UK,
June 6-9, 2012 (seriesElectronic Notes in Theoretical
Computer Science, Vol. volume286),
editorpersonUlrich Berger and
personMichael W. Mislove (Eds.). publisherElsevier,

[Gilray et al(2016)]
authorpersonThomas Gilray, personSteven
Lyde, personMichael D. Adams, personMatthew Might,
and personDavid Van Horn. year2016.
Pushdown control-flow analysis for free. In
booktitleProceedings of the 43rd Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL
2016, St. Petersburg, FL, USA, January 20 - 22, 2016,
editorpersonRastislav Bodík and
personRupak Majumdar (Eds.). publisherACM,

[Godlin and Strichman(2008)]
authorpersonBenny Godlin and personOfer
Strichman. year2008.
Inference rules for proving the equivalence of
recursive procedures.
journalActa Informatica volume45,
number6 (year2008), pages403–439.

[Godlin and Strichman(2009)]
authorpersonBenny Godlin and personOfer
Strichman. year2009.
Regression verification. In
booktitleProceedings of the 46th Design Automation
Conference, DAC 2009, San Francisco, CA, USA, July 26-31, 2009.
publisherACM, pages466–471.

[Gordon et al(1999)]
authorpersonAndrew D. Gordon, personPaul D.
Hankin, and personSøren B. Lassen.
Compilation and equivalence of imperative objects.
journalJournal of Functional Programming
volume9, number4 (year1999),

[Hopkins et al(2012)]
authorpersonDavid Hopkins, personAndrzej S.
Murawski, and personC.-H. Luke Ong.
Hector: An Equivalence Checker for a Higher-Order
Fragment of ML. In booktitleComputer Aided Verification -
24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012
Proceedings (seriesLecture Notes in Computer Science,
Vol. volume7358),
editorpersonP. Madhusudan and
personSanjit A. Seshia (Eds.). publisherSpringer,

[Horn and Might(2010)]
authorpersonDavid Van Horn and
personMatthew Might. year2010.
Abstracting abstract machines. In
booktitleProceeding of the 15th ACM SIGPLAN
international conference on Functional programming, ICFP 2010, Baltimore,
Maryland, USA, September 27-29, 2010,
editorpersonPaul Hudak and
personStephanie Weirich (Eds.). publisherACM,

[Hur et al(2012)]
authorpersonChung-Kil Hur, personDerek
Dreyer, personGeorg Neis, and personViktor
Vafeiadis. year2012.
The marriage of bisimulations and Kripke logical
relations. In booktitleProceedings of the 39th ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL
2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012,
editorpersonJohn Field and personMichael
Hicks (Eds.). publisherACM, pages59–72.

[Hyland and Ong(2000)]
authorpersonJ. M. E. Hyland and
personC.-H. Luke Ong. year2000.
On Full Abstraction for PCF: I, II, and III.
journalInf. Comput. volume163,
number2 (year2000), pages285–408.

authorpersonGuilhem Jaber.
Operational Nominal Game Semantics. In
booktitleFoundations of Software Science and Computation
Structures - 18th International Conference, FoSSaCS 2015, Proceedings
(seriesLecture Notes in Computer Science,
Vol. volume9034), editorpersonAndrew M.
Pitts (Ed.). publisherSpringer, pages264–278.

authorpersonGuilhem Jaber.
SyTeCi: automating contextual equivalence for
higher-order programs with references.
journalProc. ACM Program. Lang.
volume4, numberPOPL (year2020),

[Jaber and Tabareau(2015)]
authorpersonGuilhem Jaber and
personNicolas Tabareau. year2015.
Kripke Open Bisimulation - A Marriage of Game
Semantics and Operational Techniques. In
booktitleProgramming Languages and Systems - 13th Asian
Symposium, APLAS 2015, Pohang, South Korea, November 30 - December 2, 2015,
Proceedings (seriesLecture Notes in Computer Science,
Vol. volume9458), editorpersonXinyu Feng
and personSungwoo Park (Eds.). publisherSpringer,

[Jagadeesan et al(2009)]
authorpersonRadha Jagadeesan, personCorin
Pitcher, and personJames Riely.
Open Bisimulation for Aspects.
journalLNCS Trans. Aspect Oriented Softw. Dev.
volume5, pages72–132.

[Kim et al(2008)]
authorpersonJang-Sub Kim, personErchin
Serpedin, personDong Ryeol Shin, and
personKhalid A. Qaraqe. year2008.
Handoff Triggering and Network Selection Algorithms
for Load-Balancing Handoff in CDMA-WLAN Integrated Networks.
journalEURASIP J. Wirel. Commun. Netw.
volume2008 (year2008).

[Koutavas et al(2022)]
authorpersonVasileios Koutavas,
personYu-Yang Lin, and personNikos Tzevelekos.
From Bounded Checking to Verification of
Equivalence via Symbolic Up-to Techniques. In
booktitleTools and Algorithms for the Construction and
Analysis of Systems - 28th International Conference, TACAS 2022,
Proceedings, Part II (seriesLecture Notes in Computer
Science, Vol. volume13244),
editorpersonDana Fisman and
personGrigore Rosu (Eds.). publisherSpringer,

[Koutavas et al(2023)]
authorpersonVasileios Koutavas,
personYu-Yang Lin, and personNikos Tzevelekos.
Fully Abstract Normal Form Bisimulation for
Call-by-Value PCF. In booktitleLICS.

[Koutavas and Wand(2006)]
authorpersonVasileios Koutavas and
personMitchell Wand. year2006.
Small bisimulations for reasoning about
higher-order imperative programs. In booktitleProceedings
of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13,
2006, editorpersonJ. Gregory Morrisett and
personSimon L. Peyton Jones (Eds.). publisherACM,

[Lahiri et al(2012)]
authorpersonShuvendu K. Lahiri, personChris
Hawblitzel, personMing Kawaguchi, and
personHenrique Rebêlo. year2012.
SYMDIFF: A Language-Agnostic Semantic Diff Tool
for Imperative Programs. In booktitleComputer Aided
Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA,
July 7-13, 2012 Proceedings (seriesLecture Notes in
Computer Science, Vol. volume7358),
editorpersonP. Madhusudan and
personSanjit A. Seshia (Eds.). publisherSpringer,

authorpersonJames Laird.
A Fully Abstract Trace Semantics for General
References. In booktitleAutomata, Languages and
Programming, 34th International Colloquium, ICALP 2007, Wroclaw, Poland,
July 9-13, 2007, Proceedings (seriesLecture Notes in
Computer Science, Vol. volume4596),
editorpersonLars Arge, personChristian
Cachin, personTomasz Jurdzinski, and personAndrzej
Tarlecki (Eds.). publisherSpringer, pages667–679.

authorpersonSøren B. Lassen.
Bisimulation in Untyped Lambda Calculus: Böhm
Trees and Bisimulation up to Context. In booktitleFifteenth
Conference on Mathematical Foundations of Progamming Semantics, MFPS 1999,
Tulane University, New Orleans, LA, USA, April 28 - May 1, 1999
(seriesElectronic Notes in Theoretical Computer Science,
Vol. volume20), editorpersonStephen D.
Brookes, personAchim Jung, personMichael W. Mislove,
and personAndre Scedrov (Eds.). publisherElsevier,

authorpersonSøren B. Lassen.
Eager Normal Form Bisimulation. In
booktitle20th IEEE Symposium on Logic in Computer Science
(LICS 2005), 26-29 June 2005, Chicago, IL, USA, Proceedings.
publisherIEEE Computer Society, pages345–354.

authorpersonSøren B. Lassen.
Normal Form Simulation for McCarthy's Amb. In
booktitleProceedings of the 21st Annual Conference on
Mathematical Foundations of Programming Semantics, MFPS 2005, Birmingham,
UK, May 18-21, 2005 (seriesElectronic Notes in Theoretical
Computer Science, Vol. volume155),
editorpersonMartín Hötzel Escardó,
personAchim Jung, and personMichael W. Mislove
(Eds.). publisherElsevier, pages445–465.

[Lassen and Levy(2007)]
authorpersonSøren B. Lassen and
personPaul Blain Levy. year2007.
Typed Normal Form Bisimulation. In
booktitleComputer Science Logic, 21st International
Workshop, CSL 2007, 16th Annual Conference of the EACSL, Lausanne,
Switzerland, September 11-15, 2007, Proceedings
(seriesLecture Notes in Computer Science,
Vol. volume4646), editorpersonJacques
Duparc and personThomas A. Henzinger (Eds.).
publisherSpringer, pages283–297.

[Lassen and Levy(2008)]
authorpersonSøren B. Lassen and
personPaul Blain Levy. year2008.
Typed Normal Form Bisimulation for Parametric
Polymorphism. In booktitleProceedings of the Twenty-Third
Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June
2008, Pittsburgh, PA, USA. publisherIEEE Computer Society,

[Mason and Talcott(1991)]
authorpersonIan Mason and personCarolyn
Talcott. year1991.
Equivalence in functional languages with effects.
journalJournal of Functional Programming
volume1, number3 (year1991),

authorpersonJ. H. Morris, Jr.
titleLambda Calculus Models of Programming
thesistypePh. D. Dissertation. schoolMIT,
addressCambridge, MA.

[Murawski et al(2015)]
authorpersonAndrzej S. Murawski,
personSteven J. Ramsay, and personNikos
Tzevelekos. year2015.
A Contextual Equivalence Checker for IMJ
\({_\ast}\). In booktitleAutomated Technology for
Verification and Analysis - 13th International Symposium, ATVA 2015,
Shanghai, China, October 12-15, 2015, Proceedings
(seriesLecture Notes in Computer Science,
Vol. volume9364), editorpersonBernd
Finkbeiner, personGeguang Pu, and personLijun
Zhang (Eds.). publisherSpringer, pages234–240.

[Murawski et al(2017)]
authorpersonAndrzej S. Murawski,
personSteven J. Ramsay, and personNikos
Tzevelekos. year2017.
Reachability in pushdown register automata.
journalJ. Comput. Syst. Sci.  volume87
(year2017), pages58–83.

[Murawski and Tzevelekos(2021)]
authorpersonAndrzej S. Murawski and
personNikos Tzevelekos. year2021.
Game Semantics for Interface Middleweight Java.
journalJ. ACM volume68,
number1 (year2021), pages4:1–4:51.

authorpersonHanno Nickau.
Hereditarily Sequential Functionals. In
booktitleLogical Foundations of Computer Science, Third
International Symposium, LFCS'94, St. Petersburg, Russia, July 11-14, 1994,
Proceedings (seriesLecture Notes in Computer Science,
Vol. volume813), editorpersonAnil Nerode
and personYuri V. Matiyasevich (Eds.).
publisherSpringer, pages253–264.

authorpersonDamien Pous.
Coinduction All the Way Up. In
booktitleProceedings of the 31st Annual ACM/IEEE Symposium
on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8,
2016, editorpersonMartin Grohe,
personEric Koskinen, and personNatarajan Shankar
(Eds.). publisherACM, pages307–316.

[Pous and Sangiorgi(2012)]
authorpersonDamien Pous and personDavide
Sangiorgi. year2012.
Enhancements of the bisimulation proof method.
In booktitleAdvanced Topics in Bisimulation and
Coinduction, editorpersonDavide Sangiorgi and
personJan J. M. M. Rutten (Eds.). seriesCambridge
tracts in theoretical computer science, Vol. volume52.
publisherCambridge University Press, pages233–289.

authorpersonDavide Sangiorgi.
The Lazy Lambda Calculus in a Concurrency
journalInf. Comput. volume111,
number1 (year1994), pages120–153.

[Sangiorgi et al(2011)]
authorpersonDavide Sangiorgi, personNaoki
Kobayashi, and personEijiro Sumii.
Environmental bisimulations for higher-order
journalACM Trans. Program. Lang. Syst.
volume33, number1 (year2011),

authorpersonStefan Schwoon.
titleModel checking pushdown systems.
thesistypePh. D. Dissertation.
schoolTechnical University Munich, Germany.

[Støvring and Lassen(2007)]
authorpersonKristian Støvring and
personSøren B. Lassen. year2007.
A complete, co-inductive syntactic theory of
sequential control and state. In booktitleProceedings of
the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages, POPL 2007, Nice, France, January 17-19, 2007,
editorpersonMartin Hofmann and
personMatthias Felleisen (Eds.). publisherACM,

[Sumii and Pierce(2007a)]
authorpersonEijiro Sumii and
personBenjamin C. Pierce. year2007a.
A bisimulation for dynamic sealing.
journalTheor. Comput. Sci. volume375,
number1-3 (year2007), pages169–192.

[Sumii and Pierce(2007b)]
authorpersonEijiro Sumii and
personBenjamin C. Pierce. year2007b.
A bisimulation for type abstraction and recursion.
journalJ. ACM volume54,
number5 (year2007), pages26.

[Vardoulakis and Shivers(2011)]
authorpersonDimitrios Vardoulakis and
personOlin Shivers. year2011.
CFA2: a Context-Free Approach to Control-Flow
journalLog. Methods Comput. Sci.
volume7, number2 (year2011).

This appendix is provided for the benefit of the reviewers, and will not appear in a final version of this paper.

§ THE STACKLESS LTS

\[\begin{array}{@{}ll@{\;\;}l@{}}
\irule![PropCall][propappf]{
(D,\Gamma') \in \ulpatt(v)
%\dom{\Gamma'}\cap \dom{\Gamma} = \emptyset
\pconf{A}{\Gamma}{s}{E[\app {\alpha} v]}
\trans{\lpropapp{\alpha}{D}}
\oconf{A}{\Gamma,\Gamma'}{s}{E}
\\
\irule![PropRet][propretf]{
(D,\Gamma') \in \ulpatt(v)
%\dom{\Gamma'}\cap \dom{\Gamma} = \emptyset
\pconf{A}{\Gamma}{s}{v}
\trans{\lpropret{D}}
\oconf{A}{\Gamma,\Gamma'}{s}{\chi}
\\
\irule![OpCall][opappf]{
\nbox{
\vec\alpha\fresh\Gamma,s,\Ed\land        (D,\vec \alpha) \in \ulpatt(T)
\\{\hspace{-5mm}}\land
\Sigma_s \vdash \Gamma(i) : T \arrow T'
\land
\app {\Gamma(i)} {D\hole[\vec \alpha]} \funred e
\oconf{A}{\Gamma}{s}{\Ed}
\trans{\lopapp{i}{D\hole[\vec \alpha]}}
\pconf{A\uplus\vec\alpha}{\Gamma}{s}{e}
\\
\irule![OpRet][opretf]{
\vec\alpha\fresh\Gamma,s,\Ed\land  (D,\vec \alpha) \in \ulpatt(T)
\oconf{A}{\Gamma}{s}{E\hole_T}
\trans{\lopret{D\hole[\vec\alpha]}}
\pconf{A\uplus\vec\alpha}{\Gamma}{s}{E\hole[D[\vec\alpha]]}
\\
\irule![Tau][tau]{
\redconf{s}{e} \red \redconf{s'}{e'}
\pconf{A}{\Gamma}{s}{e}
\trans{\tau}
\pconf{A}{\Gamma}{s'}{e'}
\\
\irule![Response][dummy]{
\nbox{ \eta \not= \tau
\text{ and }
C \not\wtrans{\eta}
\text{ from other rules}
C \trans{\eta} \botcconf
% \\
% \irule![Term][term]{}{
%   \oconf{A}{\Gamma}{s}{\diamond}
%   \trans{\lterm}
%   \botcconf
% }
\end{array}\]

The Stackless Labelled Transition System. Relation $\funred$ is defined as in <Ref>.

The following is a weak (pushdown) simulation:

\begin{align}
\bisim{R} = \{\ &(C_1,C_2,\Sigma,\beta) \mid\;
\Sigma\text{ sat-connected}\land
(C_1,C_2,\Sigma,\beta)\text{ compatible}\notag\\
%              &\quad{}\land \beta=\diamond\implies\toS{C_1,\noe}\tsR\toS{C_2,\noe}\tag{A$^\diamond$}\label{cond:a0}\\
&{}\land\forall K_i.\ \beta\toSigsD{K_1,K_2}
% \toS{C_i,K_i}\text{ defined}
\implies
\toS{C_1,K_1}\simil\toS{C_2,K_2}\tag{A}\label{cond:a}\\
& {}\land\forall C_i',K_i.\  \betais{C'_1,C'_2}\toSigsD{K_1,K_2}
%\land \toS{C_i',K_i}\text{ defined}
\implies
\toS{C_1',K_1}\simil\toS{C_2',K_2}\tag{A$^*$}\label{cond:a1}\\
& {}\land\beta\neq\diamond\implies\exists C_1',C_2'.\ \beta=\betais{C_1',C_2'}\land
\    \}
\end{align}

Let $C_1\bisim*R_{\Sigma,\beta}C_2$, for $C_1\not=\botcconf$, and pick some $\beta\toSigsD{K_1,K_2}$.

By <ref> we have $\tilde C_1\simil\tilde C_2$.
If $C_1\lterm$ then $C_1.\Ed=\diamond$ and, by compatibility, $\beta=\diamond$. But then $K_1=\noe$ and therefore $\tC_1\lterm$, so $\tC_2\lterm$. Again by compatibility we get $C_2.\Ed=\diamond$ hence $C_2\lterm$.
Suppose now $C_1\realtrans{\eta}C_1'$.

* $\eta=\tau$. Then, $\tC_1\realtrans{\tau}\tC_1'=\toS{C_1',K_1}$ and hence, by $\tau$-closure, $\tC_1'\simil \tC_2$.
It suffices to show that $C_1'\bisim*R_{\Sigma,\beta}C_2$. Condition <ref> holds as $\Sigma$ has not changed, while <ref>
follows from the hypothesis and <Ref>.
Finally, for <ref> we use <ref>.

* $\eta=\lpropapp{\alpha}{D}$. Then, $\tC_1\realtrans{\lpropapp{\alpha}{D}}\tC_1'=\toS{C_1',K_1}$ and hence
$\tC_2\wtrans{\lpropapp{\alpha}{D}}\tC_2'$ with
$\tC_1'\simil\tC_2'$. We obtain $C_2\wtrans{\lpropapp{\alpha}{D}}C_2'$, with $\tC_2'=\toS{C_2',K_2}$, and it suffices to show conditions <ref>.
These are shown as in the previous case above.

* $\eta=\lopret{D[\vec\alpha]}$ with $\vec\alpha\fresh C_2$.
Let $\vec\alpha'\fresh K_1,K_2,\vec\alpha$ be of the same length as $\vec\alpha$.
Then, $\tC_1\realtrans{\lopret{D[\vec\alpha']}}\tC_1'$ and hence
$\tC_2\trans{\lopret{D[\vec\alpha']}}\tC_2'$ with
$\tC_1'\simil\tC_2'$. We obtain $C_2\trans{\lopret{D[\vec\alpha]}}C_2'$,
where $\tC_i'=\toS{\pi\cdot C_i',K_i}$ and $\pi=(\vec \alpha\ \vec\alpha')$ (permute component-wise $\vec \alpha$ with $\vec\alpha'$).
We need to show that $C_1'\bisim*R_{\Sigma,\beta}C_2'$, and in particular
show conditions <ref>. Condition <ref> still holds as $\Sigma$ has not changed. For <ref>, we use <Ref>. For <ref>, assuming $\beta\neq\diamond$, by hypothesis there are $C_1'',C_2''$ such that $\beta=\betais{C_1'',C_2''}$ and $(C_1'',C_2'')\satrans{\varepsilon}(C_1,C_2)$. By <Ref> we have $( C_1, C_2)\satrans{\varepsilon}( C_1', C_2')$, and we then use rule Trans.

* $\eta=\lopapp{i}{D[\vec\alpha]}$ with $\vec\alpha\fresh C_2$.
Let $\vec\alpha'\fresh K_1,K_2,\vec\alpha$ be of the same length as $\vec\alpha$.
Then, setting $\Ed_i=C_i.\Ed$, $\tC_1\realtrans{\lopapp{i}{D[\vec\alpha']}}\tC_1'$ and, hence, $\tC_2\trans{\lopapp{i}{D[\vec\alpha']}}\tC_2'$ with $\tC_1'\simil\tC_2'$.
We obtain $C_2\trans{\lopapp{i}{D[\vec\alpha]}}C_2'$ with
$\tC_i'=\toS{(\vec\alpha\ \vec\alpha')\cdot C_i',(\Ed_i,K_i)}$. We set $\beta'=\betais{C_1',C_2'}$ and $\Sigma'=\Sigma[\beta'\trans{\Ed_1,\Ed_2}\beta]$.
To verify
that $\Sigma'$ is sat-connected, by equivariance of $\Sigma$ (and of the sat-LTS) it suffices to show that the edge $\beta'\trans{\Ed_1,\Ed_2}\beta$ preserves it.
By condition <ref> (on $\Sigma$) we have $\beta=\betais{C_{10},C_{20}}$  and $(C_{10},C_{20})\satrans{\varepsilon}( C_1, C_2)$ and, by <Ref>, $(C_1,C_2)\satrans{(\Ed_1,\Ed_2)}(C_1',C_2')$, so $
(C_{10},C_{20})\satrans{\varepsilon}\cdot\satrans{(\Ed_1,\Ed_2)}( C_1', C_2')

as required.

It remains to show $C_1'\bisim*R_{\Sigma',\beta'}C_2'$, and in particular that conditions <ref> hold.
For <ref>, we have that $\beta'=\betais{C_1',C_2'}$ so
we require that $(C_1',C_2')\satrans{\varepsilon}(C_1',C_2')$, which is trivial.
We also note that <ref> follows from <ref> since $\beta'=\betais{C_1',C_2'}$.

For <ref>, let $\beta'',C_i'',K_i''$ be such that $\beta''=\betais{C_1'',C_2''}\toSigsD[\Sigma']{K_1'',K_2''}$. We show that $\toS{C_1'',K_1''}\simil\toS{C_2'',K_2''}$ using rule induction on
$\beta''\toSigsD[\Sigma']{K_1'',K_2''}$. Since $\beta''\not=\diamond$, we must have:

\[
\irule{
\hat\beta\toSigsD[\Sigma']{\hat K_1,\hat K_2}
\\
\beta''\toSig[\Sigma']{\hat\Ed_1,\hat\Ed_2}\hat\beta
\beta''\toSigsD[\Sigma']{K_1'',K_2''}
\]

for some $\hat\beta,\hat K_i,\hat\Ed_i$ with $K_i''=\hat\Ed_i,\hat K_i$. In the base case, $\hat\beta=\hat\Ed_i=\diamond$ and $\hat K_i=K_i''={\noe}$.
If $\beta''\toSig{\hat\Ed_1,\hat\Ed_2}\hat\beta$ then $\beta''\toSigsD{K_1'',K_2''}$ and the claim follows by <ref> applied on $\Sigma$ (as $C_1\bisim*R_{\Sigma,\beta}C_2$). Otherwise, we must have $\beta''=\pi\cdot\beta'$ (for some $\pi$) and $\beta=\Ed_i=\diamond$, and so the claim follows from $\tC_1'\simil\tC_2'$  and closure under $\pi$ (as $C_i'=C_i''$).
Suppose now $\hat\beta\neq\diamond$. By sat-connectedness, $\hat\beta =\betais{\hat C_1,\hat C_2}$
for some $\hat C_i$ such that
$(\hat C_1,\hat C_2)\satrans{\varepsilon}\cdot\satrans{(\hat\Ed_1,\hat\Ed_2)}( C_1'', C_2'')$.

By induction hypothesis we have $\toS{\hat C_1,\hat K_1}\simil\toS{\hat C_2,\hat K_2}$, so by <ref> we have $\toS{ C_1'', K_1''}\simil\toS{ C_2'', K_2''}$.

* $\eta=\lpropret{D}$ and $\beta\toSig{\Ed_1,\Ed_2}\beta'$.
Note first that, for any $K_i'$ such that $\beta'\toSigsD{K_1',K_2'}$, we get $A\cup\tC_1\trans{\lpropret{D}}\tC_1'$ and hence $A\cup\tC_2\wtrans{\lpropret{D}}\tC_2'$ with $\tC_1'\simil\tC_2'$, where  $\tC_i=\toS{C_i,(\Ed_i,K_i')}$ and
$\tC_1'=A\cup\toS{C_1'\sub{\chi}{\Ed_1},K_1'}$ (by compatibility, these are all defined).
Picking now any such $K_1',K_2'$,
we obtain $C_2\wtrans{\lpropret{D[\vec\alpha]}}C_2'$ for $C_2'$ such that $\tC_2'=A\cup\toS{C_2'\sub{\chi}{\Ed_2},K_2'}$, so it remains to show that $C_1'\sub{\chi}{\Ed_1}\bisim*R_{\Sigma',\beta'} C_2'\sub{\chi}{\Ed_2}$ for $\Sigma'=\Sigma@\beta'$. Condition <ref> still holds as $\Sigma'$ is a subgraph of $\Sigma$; while we saw above that condition <ref> holds ($\tC_1'\simil\tC_2'$ is true for any valid choice of $K_i'$).
For <ref>, if
then $\beta\neq\diamond$. Hence, condition <ref> on $C_1\bisim*R_{\Sigma,\beta}C_2$ implies
for $\beta=\betais{C_{10},C_{20}}$. Since $\Sigma$ is sat-connected,
assuming  $\beta'=\betais{C_1'',C_2''}$, we get

\[
(C_{1}'',C_{2}'')\satrans{\varepsilon}\cdot\satrans{(\Ed_1,\Ed_2)}( C_{10}, C_{20})
\]

and by <Ref>
we obtain $(C_{1}'',C_{2}'')\satrans{\varepsilon}( C_1'\sub\chi{\Ed_1}, C_2'\sub\chi{\Ed_2})$.

§ PAIR (BI-)SIMULATION

In order to define and prove our up to separation technique, we need to extend the stackless LTS to pairs of configurations and  define a notion of bisimulation over it.

We define pair configurations $\bconf{C_1}{C_2}$ for all stackless LTS configurations $C_1$, $C_2$.
To enable symmetric reasoning we define $\co{1} \defeq 2$ and $\co{2}\defeq 1$.
We let $\bC$ range over pair configurations, and write $\bC.i$ to get the $i$'th inner configuration.
We write $\bC\downarrow$ when $\bC.1\downarrow$ and $\bC.2\downarrow$.

We extend the LTS of <ref> to pair configurations as follows:

\begin{align*}
\begin{array}{rlrlll}
\irule!{
C_i \trans{\eta} C_i'
\text{ and }
C_{\co{i}} = C'_{\co{i}}
\text{ an opponent configuration and }
&\bconf{C_1}{C_2} \trans{\eta,i} \bconf{C_1'}{C_2'}
\\
\irule!{
\nbox{
C_1 \trans{\eta} C_1'
\text{ and }
C_2 \trans{\eta} C_2'
\text{ and }
C_1.e = C_2.e \text{ or } C_1.\Ed = C_2.\Ed
\\\hfill\text{ and }
C_1'.e = C_2'.e \text{ or } C_1'.\Ed = C_2'.\Ed
&\bconf{C_1}{C_2} \trans{\eta,0} \bconf{C_1'}{C_2'}
\end{array}
\end{align*}

We also write $\bC \realtrans{\eta,k} \bC'$ when the transition is derived from the above LTS, without using the dummy rule of the stackless LTS in <ref>.

The following definition lifts <ref> to the pair LTS.

\begin{align*}
\mathsf{PEPoint} \ni \ \bbeta &::=\ (\beta_1, \beta_2, k)  \qquad (k\in\{0,1,2\})\\
\mathsf{PCGrph}\ni \ \bSigma &\subseteq_{\rm fin}^{\neq\emptyset} \mathsf{PEPoint}\times\Kont\times\Kont\times\mathsf{PEPoint}
\end{align*}

and each $\bSigma$ must satisfy the conditions:

*  Reachability. For all $\bbeta\in\dom{\bSigma}$ there are evaluation stacks $K_1,K_2$ such that $\bbeta\toSigs[\bSigma]{K_1,K_2}\diamond$

* Top and Divergence. For all $\bbeta'^{k'}\toSig[\bSigma]{\Ed_1,\Ed_2}\bbeta^{k}$ and $j\in\{1,2\}$:

\begin{align*}
&    (\diamond,\diamond,0)\in\dom{\bSigma}\land (\bbeta'=(\diamond,\diamond,0)\implies\bbeta=(\diamond,\diamond,0)) \land
(\bbeta=(\diamond,\diamond,0)\iff\Ed_j=\diamond) \\
&{}\land    (\bbeta'.k.j=\bot\iff \Ed_j=\bot) \land
\Ed_j=\bot)
\end{align*}

where, if $\bbeta = (\beta_1,\beta_2, k)$ and $i \in\{1,2\}$, we write $\bbeta.i.1=\bot$ when $\beta_i=\betais{\botcconf,C}$
and $\bbeta.i.2=\bot$ when $\beta_i=\betais{C,\botcconf}$.

* Nominal closure. For  all $\bbeta'\toSig[\bSigma]{\Ed_1,\Ed_2}\bbeta$ and permutations $\pi$,     $\pi\cdot\bbeta'\toSig[\bSigma]{\pi\cdot\Ed_1,\pi\cdot\Ed_2}\pi\cdot\bbeta$.

Finally, we lift <ref> to pair graphs obtaining continuation graph extension
and restriction $\bSigma@\bbeta$.

We will write $\bbeta.i$ to mean $\beta_i$ ($i\in\{1,2\}$), and $\bbeta^m$ to mean $k=m$, when $\bbeta = (\beta_1,\beta_2,k)$.

We define simulation on compatible pair configurations.

Configurations $\bconf{C_1}{C_2}$ and $\bconf{C_1'}{C_2'}$ are compatible, when $C_j$ and $C_j'$ are compatible according to <ref>, for $j\in\{1,2\}$.

A tuple $(\bconf{C_1}{C_2}, \bconf{C_1'}{C_2'}, \bSigma, (\beta_1,\beta_2,k))$ is compatible if
$\bconf{C_1}{C_2}$ and $\bconf{C_1'}{C_2'}$ compatible, $\bSigma@(\beta_1,\beta_2,k)=\bSigma$ and
for $i,j\in\{1,2\}$:

($\bot$) if $\beta_i.1=\bot$ then $C_i=\botcconf$; if $\beta_i.2=\bot$ then $C_i'=\botcconf$;

($\diamond$) if $\beta_i=\diamond$ then $C_i.\Ed=C_i'.\Ed=\diamond$ or $\an{C_i.e}=\an{C_i'.e}=\emptyset$; and if $C_i.\Ed=\diamond$ then $\beta_i=\diamond$.[And also $C_i'.\Ed=\diamond$ by compatibility of $C_i, C_i'$.]

and moreover:

* if $C_i$ is a proponent and $C_{\co{i}}$ an opponent configuration, then $k=i$;

* if $C_1$ and $C_2$ are proponent configurations, then $k=0$;

* if $k=0$ then $\beta_1.e=\beta_2.e$ and $C_1.e = C_2.e$ or $C_1.\Ed = C_2.\Ed$, and the same for $C_1'$, $C_2'$.

A relation R with elements of the form $(\bC_1,\bC_2,\bSigma,\bbeta)$, and membership thereof denoted $\bC_1 \bbisim*{R}_{\bSigma,\bbeta} \bC_2$, is called
weak pair simulation when
for all $\bC_1 \bbisim*{R}_{\bSigma,\bbeta^k} \bC_2$ we have $(\bC_1,\bC_2,\bSigma,\bbeta^k)$ compatible

if $\bC_1\downarrow$
then $\bC_2\downarrow$

* if $\bC_1 \realtrans{\lopret{D[\vec\alpha]},k} \bC_1'$ with  $\vec\alpha\fresh \bC_2$
then $\bC_2 \wtrans{\lopret{D[\vec\alpha]},k} \bC_2'$ and
$\bC_1' \bbisim*{R}_{\bSigma,\bbeta^k} \bC_2'$

* if $\bC_1 \realtrans{\eta,k} \bC_1'$
then $\bC_2 \wtrans{\eta,k} \bC_2'$ and
$\bC_1' \bbisim*{R}_{\bSigma,\bbeta^k} \bC_2'$, for $\eta\in\{\tau,\lpropapp{\alpha}{D}\}$

* if $\bC_1 \realtrans{\lopapp{i}{D\hole[\vec \alpha]},j}  \bC_1'$ with  $\vec\alpha\fresh \bC_2$
then $\bC_2 \trans{\lopapp{i}{D\hole[\vec \alpha]},j}  \bC_2'$
$\bC_1' \bbisim*{R}_{\bSigma',\bbeta'} \bC_2'$
and $\bSigma' = \bSigma[\bbeta' \mapsto (\Ed_1, \Ed_2, \bbeta^k)]$

\begin{gather*}\begin{array}{lllll}
\bbeta' = (\betais{\bC_1'.1,\bC_2'.1}, \betais{\bC_1'.2,\bC_2'.2}, 0) & \Ed_1 = \bC_1.1.\Ed = \bC_1.2.\Ed, & \Ed_2 = \bC_2.1.\Ed = \bC_2.2.\Ed & \text{ if } j = 0; \text{ or}\\
\bbeta' = (\betais{\bC_1'.1,\bC_2'.1}, \bbeta.2, 1)                   & \Ed_1 = \bC_1.1.\Ed                & \Ed_2 =\bC_2.1.\Ed                & \text{ if } j = 1; \text{ or}\\
\bbeta' = (\bbeta.1, \betais{\bC_1'.2,\bC_2'.2}, 2)                   & \Ed_2 = \bC_1.2.\Ed                & \Ed_2 =\bC_2.2.\Ed                & \text{ if } j = 2\phantom{; \text{ or}}
\end{array}\end{gather*}

* if $\bC_1 \realtrans{\lpropret{D},k} \bC_1'$
then $\bC_2 \wtrans{\lpropret{D},k} \bC_2'$
$\bC_1'\sub{\chi}{\Edb_1} \bbisim*{R}_{\bSigma',\bbeta'} \bC_2'\sub{\chi}{\Edb_2}$ with $\bSigma'=\bSigma@\bbeta'$.

Pair Similarity $(\bsimil)$ is the largest weak simulation.
Relation R is a weak pair bisimulation when R and $\bbisim{R}^{-1}$ are weak pair simulations, where $R^{-1}=\{(\bC_1,\bC_2,\bSigma^{-1},\bbeta^{-1})\mid (\bC_2,\bC_1,\bSigma,\bbeta)\in \bbisim{R}\}$.
Pair bisimilarity $(\bbisimil)$ is the largest weak bisimulation.

Given two continuation graphs $\Sigma_1$, $\Sigma_2$ we construct the product graph:

\begin{gather*}
\irule{
((\diamond,\diamond,0), \diamond, \diamond, (\diamond, \diamond, 0)) \in \Sigma_1 \otimes \Sigma_2
\\
\irule{
(\beta_1,\beta_2,k) \in \dom{\Sigma_1\otimes\Sigma_2}
\\
\forall i \in \{1,2\}.~(\beta_i', \Ed, \Ed', \beta_i) \in \Sigma_i
\\
\forall j \in \{1,2\}.~\beta'_1.j.e=\beta'_2.j.e
((\beta_1',\beta_2',0), \Ed, \Ed', (\beta_1, \beta_2, k)) \in \Sigma_1\otimes\Sigma_2
\\
\irule{
(\beta_1,\beta_2,k) \in \dom{\Sigma_1\otimes\Sigma_2}
\\\\
(\beta_i',\Ed, \Ed', \beta_i) \in \Sigma_i
\\
\beta_{\co{i}} = \beta_{\co{i}}'
\\
((\beta_1',\beta_2',i), \Ed, \Ed', (\beta_1, \beta_2, k)) \in \Sigma_1\otimes\Sigma_2
\end{gather*}

Suppose  $\Sigma_1, \Sigma_2$ well-formed continuation graphs; then $\Sigma_1 \otimes \Sigma_2$ is a well-formed pair continuation graph.

By induction on the construction of $\Sigma_1 \otimes \Sigma_2$, reasoning about each condition separately and using the induction hypothesis for proving reachability and the second part of closure. Because $\Sigma_i$ ($i\in\{1,2\}$) are closed under permutations of their tuples, so is the product graph.

Moreover, given two stackless configuration relations $\bisim{R}_1$,$\bisim{R}_2$, we define the pair relation $\bisim{R}_1\otimes\bisim{R}_2$ by induction:

\begin{gather*}
\irule{
C_1 \bisim*{R}_{1\,\Sigma_1,\beta_1} C_1'
\\
C_2 \bisim*{R}_{2\,\Sigma_2,\beta_2} C_2'
\\\\
C_1.\Phi = C_2.\Phi
\\
C_1'.\Phi = C_2'.\Phi
\\\\
\bbeta = (\beta_1,\beta_2,0) \in \dom{\Sigma_1\otimes\Sigma_2}
\bconf{C_1}{C_2}
\mathrel{(\bisim{R}_1\otimes\bisim{R}_2)_{(\Sigma_1\otimes\Sigma_2)@\bbeta,\;\bbeta}}
\bconf{C_1'}{C_2'}
\\
\irule{
C_1 \bisim*{R}_{1\,\Sigma_1,\beta_1} C_1'
\\
C_2 \bisim*{R}_{2\,\Sigma_2,\beta_2} C_2'
\\\\
\bbeta = (\beta_1,\beta_2,i) \in \dom{\Sigma_1\otimes\Sigma_2}
\\
C_{\co{i}},C_{\co{i}}' \text{ opponent configurations}
\bconf{C_1}{C_2}
\mathrel{(\bisim{R}_1\otimes\bisim{R}_2)_{(\Sigma_1\otimes\Sigma_2)@\bbeta,\;\bbeta}}
\bconf{C_1'}{C_2'}
\end{gather*}

Let $\bisim{R}_1$ and $\bisim{R}_2$ are stackless simulations; then $\bisim{R}_1\otimes\bisim{R}_2$ is a pair simulation.

By showing that $(\eta,i)$ transitions are matched because $\bisim{R}_i$  is a simulation (for $i\in\{1,2\}$), and $\eta,0$ transitions are matched because both $\bisim{R}_1$, $\bisim{R}_2$ are simulations and the constituent configurations can perform the same moves.
In addition we use simple lemmas to show that the extension and reachability operations of the pair continuation graph is captured by the construction of the product relation (cf. <ref>).

§.§ Pair Configuration Lemmas

Suppose $\Sigma_i = \Sigma_i@\beta_i (i\in\{1,2\})$ are valid call graphs.
Then $(\beta_1,\beta_2,k)    \in \dom{\Sigma_1\otimes\Sigma_2}$.

\begin{align*}
\Sigma_i'              & = \Sigma_i[\beta_i' \mapsto (E_a, E_b, \beta_i)] & (i\in\{1,2\}) \\
\Sigma_i               & = \Sigma_i@\beta_i                               & (i\in\{1,2\})
\end{align*}

\begin{align*}
(\beta_1',\beta_2',k')                             & \in \dom{\Sigma_1'\otimes\Sigma_2'} \qquad\text{and}\\
(\Sigma_1'\otimes\Sigma_2')@(\beta_1',\beta_2',k') & =
\end{align*}

\begin{align*}
\Sigma_i                & = \Sigma_i@\beta_i             & (i\in\{1,2\}) \\
(\beta_i',E_{1a},E_{2b},\beta_i) & \in \Sigma_i          & (i\in\{1,2\}) \\
\end{align*}

\begin{align*}
((\Sigma_1\otimes\Sigma_2)@(\beta_1',\beta_2',k'))@(\beta_1,\beta_2,k) =
\end{align*}

Suppose $\bbeta\in\dom\bSigma$; then:

* $\bmerge{\bSigma}@\bmerge{\bbeta} = \bmerge{\bSigma@\bbeta}$

* $\bmerge{\bSigma}[\bmerge{\bbeta'} \mapsto (\Ed_1,\Ed_2,\bmerge{\bbeta})] = \bmerge{\bSigma[\bbeta' \mapsto (\Ed_1,\Ed_2,\bbeta)]}$

§ UP TO SEPARATION

§.§ Soundness of Up to Separation

\begin{gather*}
C_1 \sepconj[I][k] C_2 \utsepconj*{\bisim{R}}_{\Sigma,\bmerge{\bbeta_{12}}} C_1' \sepconj[I][k] C_2'\\
C_1 = \pconf{A_1}{\Gamma_1\sepconj[I,L]\Gamma}{s_1\sepconj[L] s}{e_1} \qquad
C_2 = \oconf{A_2}{\Gamma_2\sepconj[I,L]\Gamma}{s_2\sepconj[L] s}{\Ed_2} \\
C_1' = \pconf{A_1'}{\Gamma_1'\sepconj[I,L']\Gamma}{s_1'\sepconj[L'] s'}{e_1'} \qquad
C_2' = \oconf{A_2'}{\Gamma_2'\sepconj[I,L']\Gamma}{s_2'\sepconj[L'] s'}{\Ed_2'}
\end{gather*}

$C_i \simil_{\Sigma_i,\beta_i} C_i'$ ($i\in\{1,2\}$)
$\bbeta_{12}= (\beta_1,\beta_2,k)$.
We show the case where $k=1$ and the two interesting subcases of $\WP$:

$\bullet$ Case
$C_1 \sepconj[I][1] C_2 \realtrans{\eta} C_{32}$
$(\Edb_3,\Edb_3',\bmerge{\bbeta_{32}}) \in \Sigma(\bmerge{\beta_{12}})$:

We have
$C_1 \realtrans{\eta} C_3$ and

\begin{gather*}
C_3 = \oconf{A_1}{\Gamma_1,\Gamma_3\sepconj[I,L]\Gamma}{s_1\sepconj[L] s}{\chi}
\qquad
C_{32} = C_3\sepconj[I][k] C_2
\\
(\Edb_3,\Edb_3',\beta_3) \in \Sigma_1(\beta_1)
\qquad
\bbeta_{32}=(\beta_3,\beta_2, k_{32})
\end{gather*}

We then have

\begin{gather*}
\bconf{C_1}{C_2} \realtrans{\eta,1} \bconf{C_3}{C_2}
\qquad
(\Edb_3,\Edb_3',\bbeta_{32}) \in (\Sigma_1\oplus\Sigma_2)(\bbeta_{12})
\end{gather*}

By <ref>, and $\bconf{C_1}{C_2} \mathrel{(\simil \otimes \simil)_{(\Sigma_1\otimes\Sigma_2)@\bbeta_{12},~\bbeta_{12}}} \bconf{C_1'}{C_2'}$ :

\begin{gather*}
\bconf{C_1'}{C_2'} \wtrans{\eta,1} \bconf{C_3'}{C_2}
\qquad
C_3' = \oconf{A_1'}{\Gamma_1',\Gamma_3'\sepconj[I,L']\Gamma'}{s_1'\sepconj[L] s'}{\chi}
\\
\bconf{C_3}{C_2}\sub{\chi}{\Edb_3}=
\bconf{C_3\sub{\chi}{\Edb_3}}{C_2}
\mathrel{(\simil \otimes \simil)_{(\Sigma_1\otimes\Sigma_2)@\bbeta_{32},~\bbeta_{32}}}
\bconf{C_3'\sub{\chi}{\Edb_3'}}{C_2}=
\bconf{C_3'}{C_2}\sub{\chi}{\Edb_3'}
\end{gather*}

\begin{gather*}
{C_1'}\sepconj[I][1]{C_2'} \wtrans{\eta} {C_3'}\sepconj[I][1]{C_2'}
\\
C_3\sub{\chi}{\Edb_3} \sepconj[I][k_{32}] C_2
\utsepconj*{\simil}_{\bmerge{(\Sigma_1\otimes\Sigma_2)@\bbeta_{32}},~\bmerge{\bbeta_{32}}}
C_3'\sub{\chi}{\Edb_3} \sepconj[I][k_{32}] C_2'
\end{gather*}

$\bullet$ Case
$C_1 \sepconj[I][1] C_2 \realtrans{\eta} C_{32}$
$\eta=\lopapp{i}{D\hole[\vec \alpha]}$:

If $i\in\dom{\Gamma_1}$, we have
$C_1 \realtrans{\eta} C_3$ and

\begin{gather*}
C_3 = \oconf{A_1}{\Gamma_1\sepconj[I,L]\Gamma}{s_1\sepconj[L] s}{\Ed_3}
\qquad
C_{32} = C_3\sepconj[I][1] C_2
\end{gather*}

We then have
\bconf{C_1}{C_2} \realtrans{\eta,1} \bconf{C_3}{C_2}
By <ref>, $\bconf{C_1}{C_2} \mathrel{(\simil \otimes \simil)_{(\Sigma_1\otimes\Sigma_2)@\bbeta_{12},~\bbeta_{12}}} \bconf{C_1'}{C_2'}$ :

\begin{gather*}
\bconf{C_1'}{C_2} \trans{\eta,1} \bconf{C_3'}{C_2}
\qquad
\beta_e = \betais{C_3, C_3'}
\qquad
\bbeta_{32}=(\beta_3,\beta_2, 1)
\\
\bSigma_{32} = (\Sigma_1\oplus\Sigma_2)[\bbeta_{32} \mapsto (\Edb_3,\Edb_3',\bbeta_{12})]
\qquad
\bconf{C_3}{C_2}
\mathrel{(\simil \otimes \simil)_{\bSigma_{32},~\bbeta_{32}}}
\bconf{C_3'}{C_2}
\end{gather*}

\begin{gather*}
{C_1'}\sepconj[I][1]{C_2'} \trans{\eta} {C_3'}\sepconj[I][1]{C_2'}
\\
C_3 \sepconj[I][1] C_2
\utsepconj*{\simil}_{\bmerge{\bSigma_{32}@\bbeta_{32}},~\bmerge{\bbeta_{32}}}
C_3' \sepconj[I][1] C_2'
\end{gather*}

If $i\in\Gamma$ the proof is similar, with the exception that we consider transition $\eta,0$ from the pair configurations.

§.§ Completeness of Up to Separation

Let $\bisim{R}$ be a simulation and
$C_1 \sepconj[I][0] C_2 \simil_{\Sigma,\beta} C_1' \sepconj[I][0] C_2'$.
We will show that $C_1 \simil_{\Sigma',\beta'} C_1'$, for some $\Sigma',\beta'$ (the proof for $C_2,C_2'$ is symmetric).
We unfold the definition for
$C_1 \sepconj[I][0] C_2$ and
$C_1' \sepconj[I][0] C_2'$, considering cases.
The case where $C_1 \sepconj[I][0] C_2 = C_1=\botconf$ is trivial.
The remaining two cases are similar and we only show one:

\begin{align*}
C_1&=\oconf{A_1}{\Gamma_1\sepconj[I,L]\Gamma}{s_1\sepconj s}{\Ed}
\\
C_2&=\oconf{A_2}{\Gamma_2\sepconj[I,L]\Gamma}{s_2\sepconj[L] s}{\Ed}
\\
C_1 \sepconj[I][0] C_2 &=
\oconf{A_1\cup A_2}{\Gamma_1\sepconj\Gamma_2\sepconj\Gamma}{s_1\sepconj s_2\sepconj s}{\Ed}
\\
C_1 \sepconj[I][0] C_2 &\mathrel{{\weakrelinv}^{(n)}}
\oconf{A_1\cup A_2}{\Gamma_1\sepconj\Gamma}{s_1\sepconj s_2\sepconj s}{\Ed} = C_3
\end{align*}

where ${\weakrelinv}^{(n)} =\; \weakrelinv_{i_1}\ldots\weakrelinv_{i_n}$ and $\{i_1,\ldots,i_n\}=\dom{\Gamma_2}$.

\begin{align*}
C_1'&=\oconf{A_1'}{\Gamma_1'\sepconj[I,L']\Gamma'}{s_1'\sepconj s'}{\Ed'}
\\
C_2'&=\oconf{A_2'}{\Gamma_2'\sepconj[I,L']\Gamma'}{s_2'\sepconj[L'] s'}{\Ed'}
\\
C_1' \sepconj[I][0] C_2' &=
\oconf{A_1'\cup A_2'}{\Gamma_1'\sepconj\Gamma_2'\sepconj\Gamma'}{s_1'\sepconj s_2'\sepconj s'}{\Ed'}
\\
C_1' \sepconj[I][0] C_2' &\mathrel{{\weakrelinv}^{(n)}}
\oconf{A_1'\cup A_2'}{\Gamma_1'\sepconj\Gamma'}{s_1'\sepconj s_2'\sepconj s'}{\Ed'} = C_3'
\end{align*}

By <ref>, we have
$C_3 \simil_{\Sigma_3,\beta_3} C_3'$, for some $\Sigma_3,\beta_3$. Moreover,

\begin{align*}
C_3 & \gcrelinv_{A_2,\dom{s_2}} \oconf{A_1}{\Gamma_1\sepconj\Gamma}{s_1\sepconj s}{\Ed} = C_1
\\
C_3' & \gcrelinv_{A_2',\dom{s_2'}} \oconf{A_1'}{\Gamma_1'\sepconj\Gamma'}{s_1'\sepconj s'}{\Ed'} = C_1'
\end{align*}

By <ref>, we have
$C_1 \simil_{\Sigma_4,\beta_4} C_1'$, for some $\Sigma_4,\beta_4$.


# Giant density-of-states van Hove singularities in the face-centered cubic
lattice

P.A. Igoshev  V.Yu. Irkhin  M. N. Mikheev Institute of Metal Physics, 620108
Ekaterinburg, Russia

###### Abstract

All van Hove singularities in the density of states (DOS) of face-centered
cubic lattice in the nearest and next-nearest neighbour approximation,
focusing on higher-order ones, are found and classified. At special values of
the ratio $\tau$ of nearest ($t$) and next-nearest neighbour hopping integral
$t^{\prime}$ giant DOS singularities, caused by van Hove lines or surfaces,
are formed. An exact formula for DOS which provides efficient numerical
implementation is proposed. The standard tetrahedron method is demonstrated to
be inapplicable due to its poor convergence in the vicinity of kinks caused by
van Hove singularities. A comparison with the case of large space
dimensionality (infinite coordination number) including next-nearest
neighbours is performed.

###### keywords:

Density of states, Electronic properties , van Hove singularities

††journal: Journal of LaTeX Templates

##  1 Introduction

Zero-velocity $\mathbf{k}$ points in the Brillouin zone are inevitably present
in the one-particle excitation spectrum of a periodic system, as follows from
the Morse theorem in differential topology (see [1]). A peculiar role of such
points is manifested by the fact that each such $\mathbf{k}$-point generally
produces a divergence in the derivative of the corresponding density of states
(DOS) at the energy for this $\mathbf{k}$. We refer to such a DOS feature as
the van Hove singularity (vHS) [1]. This singularity can be enhanced by some
factors (e. g. merging of several singularities, effective-mass divergence,
etc.), which results in the DOS divergence at the corresponding energy,
leading to significant effects in physical properties.

The vHS’s play an important role in the solid state physics leading to
important consequences for electronic, magnetic and structural properties.
Formation of strong van Hove singularities results in the localization of the
electron states and in an increase in the role of correlation effects [2].
Therefore these singularities, especially electronic DOS peaks near the Fermi
level, are crucial for ferromagnetic ordering [3, 4] and favor other Fermi-
liquid instabilities, including superconductivity (see, e.g., [5]). A
geometrical origin of DOS peaks in a general context, as well as its
implementation for concrete compound electronic spectrum obtained within the
density functional theory (DFT) were investigated in detail in Ref. [6]. In
particular, in fcc phase of Sr, weakly dispersive one-dimension manifolds
(their prototype is a van Hove line) are positioned at the face of the
Brillouin zone near the Fermi level. They correspond to X–U, U–L, L–K, K–U,
and K–W directions.

Recently, so-called higher-order van Hove singularities connected with
divergence of some effective masses have attracted a lot of attention, in
particular as a possible cause of unconventional insulating state and
superconductivity in twisted bilayer graphene at a magic angle [7, 8, 9]. A
giant vHS was found within DFT calculations [10] in Mg3Bi2 compound with high
thermoelectric power. Non-trivial consequences of electron spectrum features
were found in nodal-line semimetals: three-dimensional ZrSiSe [11] and bilayer
ZrSiS [12] possessing a whole vHS line. We state that peculiarities of
spectrum may have various and valuable impact onto physical properties and its
isoenergetic surface topology should be investigated carefully within
numerical and analytical aspects.

Van Hove singularities are also extensively discussed now in the context of
the so-called Hund’s metals where they can result (together with asymmetry of
DOS with respect to the Fermi level) in a considerable enhancement of
quasiparticle damping (up to destroying Landau quasiparticle behaviour) as a
consequence of the Hund coupling [13]. Compounds with particular narrow bands
can serve as examples of such systems: $\alpha$\- and $\gamma$-Fe, and Ni were
considered as candidates to the Hund’s metal group [13]. The Hund-metal
features are similar to the orbital-selective Mott transitions, introduced to
explain unusual properties of Ca2-xSrxRuO4 [14], which are to a large extent
determined by vHS. Strong and non-monotonous temperature behaviour of magnetic
susceptibility in LaFeAsO is caused by a closeness of the DOS peak, possibly
produced by van Hove singularity near the Fermi level [15]. Therefore it is
instructive and useful for concrete calculations to have explicit DOS
expressions.

Early investigation [16] presented a numerical interpolation of DOS for cubic
lattices, but only the case of nearest-neighbor hopping approximation
(integral $t$) was considered. At the same time, for modeling real compounds
the next-nearest-neighbor hopping $t^{\prime}$ plays often an important role.
For the square lattice, this point was widely discussed in the context of
superconducting cuprates within the non-degenerate Hubbard model. Here, simple
Néel antiferromagnetic order, being present in the nearest-neighbour
approximation at half-filling for arbitrarily small Hubbard’s $U$, can be
replaced by incommensurate magnetic ordering [17, 18], $d$-wave susceptibility
[19], ferromagnetic ordering [17, 18, 19, 20], provided that considerable
next-nearest-neighbour hopping is introduced.

The van Hove singularity owing to L point in the fcc lattice Brillouin zone
produces weak ferromagnetic ordering in ZrZn2 and plays important role in
unusual physical properties: metamagnetic transition in a weak magnetic field,
Lifshitz transitions, non-Fermi-liquid behaviour [21, 22, 23, 24]. Magnetic
ordering in Ni is mainly caused by the vicinity of L point to the Fermi
surface (so-called “van Hove magnet”) [25], which dramatically distinguishes
this from systems with well-formed local moments like $\alpha$-Fe and rare-
earth systems.

From this point of view, the case of three-dimensional bipartite lattices
(simple cubic and body-centered cubic) was investigated in Refs. [26, 27],
closed analytical expressions for DOS as a function of energy and
$\tau=t^{\prime}/t$ in terms of elliptic integrals being obtained.

For a non-bipartite fcc lattice, an analytical investigation of the Van Hove
energy levels and numerical analysis of the DOS within the nearest and the
next-nearest neighbour hopping approximation were performed to a great extent
only in a limited interval $0<\tau<+1$ [28], which did not allow to find van
Hove singularity lines. At the special value $\tau=-1/2$, a giant Van Hove
line occurs at the band edge producing a DOS singularity of the inverse
square-root type (for the case of infinite-dimension lattice it was discussed
in Ref. [29]). Here we provide an analysis of stability of this singularity
and of its influence on the DOS picture in the whole $\tau$ interval.

##  2 Electron spectrum and giant van Hove singularities at $\tau=-1/2,0,1$

We write down electron spectrum as

$t_{\rm
fcc}\left(\mathbf{k};\tau\right)=-4t\left(\cos{k_{x}}\cos{k_{y}}+\cos{k_{x}}\cos{k_{z}}+\cos{k_{y}}\cos{k_{z}}\right)\\\
+2t\tau\left(\cos 2{k_{x}}+\cos 2{k_{y}}+\cos 2{k_{z}}\right),$ (1)

where we assume nearest-neighbour hopping integral $t>0$ and parametrize the
next-nearest-neighbour hopping integral $t^{\prime}=\tau t$ (lattice parameter
is chosen as $a=2$). Below we take $t=1$ for brevity. The definition of
nearest-neighbor hopping integral is the same as in Ref. [16]. Density of
states is defined by the following integral over Brillouin zone

$\rho_{\rm fcc}(\epsilon,\tau=0)=\int\frac{d^{3}\mathbf{k}}{V_{\rm
BZ}}\delta(\epsilon-t_{\rm fcc}\left(\mathbf{k};\tau\right)).$ (2)

In Table 1 we present an analysis of van Hove $\mathbf{k}$ points in the
vicinity of van Hove $\mathbf{k}$ point) depending on $\tau$. We write down
their energy and signature, i.e. the difference of positive and negative
indices of inertia of the second order $t_{\rm
fcc}\left(\mathbf{k};\tau\right)$ Taylor-expansion terms. For further
convenience, an excerpt from this in a demonstrative manner is given in Fig.
1.

An analogous Table I is presented in Ref. [28], being restricted to $\tau<1$
($\gamma=-\tau$ in that consideration). To compare, $0$ point of [28]
corresponds to $\Gamma$ being a global minimum at $\tau<1$ and a local maximum
at $\tau>1$; A point of [28] corresponds to L and actually changes its type at
$\tau=+1$ to global minimum at $\tau>1$; B point of [28] corresponds to W and
does not change its vHS type at $\tau=-1$, as is claimed in Ref. [28]; C point
of [28] corresponds to X; D point of Ref. [28] corresponds to
$\varDelta^{\ast}$ and is realized at $|\tau|>1$ with /+1/ at $\tau<-1$ and
/-1/ at $\tau>+1$, which is not taken into account in [28] (also the
expression for the energy contains a typo); E point of [28] corresponds to
$\varSigma^{\ast}$. Thus the Table I of Ref. [28] contains some errors and
typos.

Table 1: Non-equivalent $\mathbf{k}$ points of van Hove singularities for FCC lattice, see. Fig. 1. Arrow denotes a change of signature of mass tensor of van Hove $\mathbf{k}$ point as $\tau$ increases above the reference $\tau_{\ast}$ value. $k_{\varSigma^{\ast}}=\arccos(2\tau-1)^{-1},k_{\varDelta^{\ast}}=\arccos\tau^{-1}$. $a^{(1)}_{\rm\varDelta^{\ast}}=4(\tau^{-1}-1)(1+2\tau)$, $a^{(2)}_{\rm\varDelta^{\ast}}=8\tau^{-1}(\tau^{2}-1)$, $a^{(1)}_{\rm\varSigma^{\ast}}=8(\tau-1)(1+2\tau)/(1-2\tau)$, $a^{(2)}_{\rm\varSigma^{\ast}}=16\tau(\tau-1)(1+2\tau)(1-2\tau)^{-2}$, $a^{(3)}_{\rm\varSigma^{\ast}}=16\tau(\tau-1)(2\tau-1)^{-1}$. We distinguish four types of van Hove points: minimum (“min”), maximum(“max”), $/\pm 1/$ corresponds to signature of the Hessian matrix of $t(\mathbf{k};\tau^{\prime})$ at the saddle van Hove point $\mathbf{k}=\mathbf{k}_{\rm vH}$. $\varSigma^{\ast}(\varDelta^{\ast})$ denotes van Hove point located at high-symmetry Brillouin zone direction $\varSigma(\varDelta)$.  $\mathbf{k}$ | $w=t(\mathbf{k})$ | inverse masses | signature
---|---|---|---
$\Gamma(0,0,0)$ | $-12+6\tau$ | $8(1-\tau),8(1-\tau),8(1-\tau)$ | min$\stackrel{{\scriptstyle\tau=1}}{{\rightarrow}}$max
X$(0,0,\pi)$ | $+4+6\tau$ | $-8\tau,-8\tau,-8(1+\tau)$ | min$\stackrel{{\scriptstyle\tau=-1}}{{\rightarrow}}/+1/\stackrel{{\scriptstyle\tau=0}}{{\rightarrow}}{\rm max}$
W$(0,\pi/2,\pi)$ | $+4+2\tau$ | $-4(1+2\tau),8\tau,8\tau$ | $/+1/\stackrel{{\scriptstyle\tau=-1/2}}{{\rightarrow}}{\rm max}\stackrel{{\scriptstyle\tau=0}}{{\rightarrow}}/-1/$
L$(\pi/2,\pi/2,\pi/2)$ | $-6\tau$ | $4(1+2\tau),4(1+2\tau),8(\tau-1)$ | ${\rm max}\stackrel{{\scriptstyle\tau=-1/2}}{{\rightarrow}}/+1/\stackrel{{\scriptstyle\tau=+1}}{{\rightarrow}}{\rm min}$
${\varDelta^{\ast}}\left(0,0,k_{\varDelta^{\ast}}\right)$ | $-2\tau^{-1}(2+2\tau-\tau^{2})$ | $a^{(1)}_{\rm\varDelta^{\ast}},a^{(1)}_{\rm\varDelta^{\ast}},a^{(2)}_{\rm\varDelta^{\ast}}$ |  $/-1/,\tau>+1$; $/+1/,\tau<-1$
${\varSigma^{\ast}}\left(0,k_{\varSigma^{\ast}},k_{\varSigma^{\ast}}\right)$ | $4(1-2\tau)^{-1}-2\tau$ | $a^{(1)}_{\rm\varSigma^{\ast}},a^{(2)}_{\rm\varSigma^{\ast}},a^{(3)}_{\rm\varSigma^{\ast}}$ |  $/+1/,\tau>+1$; $/-1/,\tau<0$

Figure 1: (a) $\tau$ dependence of the energy $w$ of van Hove $\mathbf{k}$
points for fcc lattice, see definitions in Table 1. Solid line denotes a local
maximum point, dashed line a local minimum point, dotted line line a saddle-
point. (b) Brillouin zone of fcc lattice with notations for high-symmetry
points and directions.

The $\tau$ dependence of van Hove energies presented in Fig. 1 implies that at
special values $\tau=-1,-1/2,0,1/2,1$ isoenergetic surfaces demonstrate
topological transitions (change of van Hove singularity types).

The derivation of DOS formula for fcc lattice is presented in the next
Section, see Eq. (23–22). Below in this Section we present only calculation
results and qualitative analysis. We have three special cases providing van
Hove singularities: $\tau=-1/2$, $\tau=0$ and $\tau=1$. For $\tau=-1/2$ the
whole van Hove surface

$\cos k_{x}+\cos k_{y}+\cos k_{z}=0$ (3)

is formed, which corresponds to merging of energy levels for W, L and
$\varSigma^{\ast}$ points, and results in giant quasi-one-dimensional
behavior. However in this case DOS can be calculated easily, since the
spectrum can be represented as $t_{\rm
fcc}\left(\mathbf{k};-1/2\right)=3-t^{2}_{\rm sc}(\mathbf{k})/2$, where
$t_{\rm sc}(\mathbf{k})=2(\cos k_{x}+\cos k_{y}+\cos k_{z})$ is tight-binding
spectrum for the simple cubic lattice in the nearest-neighbour approximation.
Direct use of this formula implies

$\rho_{\rm fcc}(\epsilon;\tau=-1/2)=\frac{\sqrt{2}\rho_{\rm
sc}(\sqrt{2(3-\epsilon)})}{\sqrt{3-\epsilon}}.$ (4)

with $\rho_{\rm sc}(\epsilon)$ being the corresponding simple cubic lattice
DOS. This implies that van Hove singularity exists at the top of the band
$\epsilon=+3$, and in the vicinity of it we have the following “one-
dimensional” asymptotics $\rho_{\rm fcc}(\epsilon)=\sqrt{2}\rho_{\rm
sc}(0)/\sqrt{3-\epsilon}+\mathcal{O}(\sqrt{3-\epsilon})$. Such a singularity
is analogous to that for the square lattice in the next-nearest-neighbour
hopping approximation at $t^{\prime}=0.5t$ when the flat band in the vicinity
of van Hove lines $k_{x}=0$ and $k_{y}=0$ is formed [30].

Figure 2: DOS of fcc lattice calculated using numerical integration (23) at
$\tau=-1.5,-1,-0.6$, and $-1/2$ within the region in the vicinity of giant van
Hove singularity level $\epsilon=+3$ at $\tau=-1/2$ (shown by dashed vertical
line). DOS plot in full energy range is shown in the inset. Values of $\tau$
are shown in the legend.

From Figs. 2–5, one can trace the influence of small deviations from critical
$\tau$ values on DOS plots. We deal with giant van Hove singularities of three
types: (i) the logarithmic one (for $\tau=0$) at the top of the band; this was
found by R. Jelitto [16]; (ii) the inverse fourth-order-root type which was
found at $\tau=1$ at the bottom of the band; (iii) quasi-one-dimensional one
of inverse-square-root type ($\tau=-1/2$) at the top of the band, which
originates from van Hove surface containing high-order van Hove points. From
Fig. 3 one can see that logarithmic singularity is much weaker than inverse-
square-root type singularity. This relation holds under deviation of $\tau$
from critical values corresponding to topological transitions. At the same
time, the difference of (ii) and (iii) singularities is practically not seen
on the scale shown.

The transition of $\tau$ through each special point $\tau=-1/2,0,1$ causes a
divergence of one or more of electron masses, see Table 1. This means that at
deviation of $\tau$ from the “critical” value the van Hove line or surface
decays into a few points with heavy masses.

At $\tau\lesssim-1/2$, see Fig. 2, two van Hove points W$/+1/$ and
$\varSigma^{\ast}/-1/$ are formed with close energies, $w^{\rm
fcc}_{\varSigma^{\ast}}(\tau)-w^{\rm fcc}_{\rm W}(\tau)\sim-(1+2\tau)$; there
is a narrow plateau between these energy levels. At the same time the
occurrence of a kink at van Hove energy $w_{\varDelta^{\ast}}$ at $\tau<-1$
does not change substantially the DOS form.

For $\tau$ larger than $-1/2$ (up to $\tau=0$), the energy interval between
these two points near the band top corresponds to strong falling of DOS from
the energy of the saddle point ($\varSigma^{\ast}$) to the energy of the
maximum (W) with heavy mass at $\tau$ close to 0 and $-1/2$, see Fig. 3.
According to Table 1, internal van Hove points $\varDelta^{\ast}$ and
$\varSigma^{\ast}$ are absent in the case $|\tau|\leq 1$. The least
interesting case $0<\tau<1$ was investigated in detail in Ref. [28], see Fig.
4. Inside this interval, there are no internal van Hove points, as well as van
Hove lines and surfaces but at the ends of this interval, $\tau=0,1$ giant van
Hove singularities occur.

Figure 3: The same as Fig. 2 for $\tau=-1/2,-0.45,-0.35,-0.2,-0.05$, and $0$
within the region in the vicinity of giant van Hove singularities level
$\epsilon=+4$ (at $\tau=0$) and $\epsilon=+3$ (at $\tau=-1/2$) (shown by
dashed vertical line). DOS plot in full energy range is shown in the inset.

At $\tau\gtrsim+1$, the van Hove line $\varLambda$ present at $\tau=+1$ and
producing giant van Hove singularity decays into three van Hove points:
$\varDelta^{\ast},\varSigma^{\ast},\Gamma$. Besides that, the energies of two
first points form a typical narrow plateau with the width $w^{\rm
fcc}_{\varDelta^{\ast}}(\tau)-w^{\rm
fcc}_{\varSigma^{\ast}}(\tau)\sim(\tau-1)^{2}$ between levels of opposite-
signature saddle points, see Fig 5.

For $\tau=0$, the van Hove line $V=\\{(0,\pi,k_{z}),-\pi/2<k_{z}<\pi/2\\}$
joining W and X points corresponds to merging of energy levels of these
points. Therefore we get for inverse transverse masses
$m^{-1}_{V}(k_{z})=-4(1\pm\cos k_{z})$. In this case, we represent the
spectrum in the vicinity of the $V$ line as

$E_{V}(k_{z},q_{x},q_{y})=t_{\rm
fcc}\left(\mathbf{k}_{V}(q_{x},\pi+q_{y},k_{z});\tau=0\right)=4-2(1-\cos
k_{z})q_{x}^{2}\\\ -2(1+\cos k_{z})q_{y}^{2}+(1-\cos k_{z})q_{x}^{4}/6+(1+\cos
k_{z})q_{y}^{4}/6+q_{x}^{2}q_{y}^{2}.$ (5)

Expanding the spectrum in $k_{z}=q_{z}$ we get up to leading terms

$t_{\rm
fcc}\left(\mathbf{k}_{V}(q_{x},\pi+q_{y},q_{z});\tau=0\right)=4-4q^{2}_{y}-q^{2}_{x}q^{2}_{z}$

which implies that X is a higher-order van Hove point, since only one inverse
mass is non-zero.

Figure 4: DOS plot for $\tau=0,0.05,+0.25,+0.5,+0.75,0.95$, and $1$.  Figure
5: The same as Fig. 2 for $\tau=1,1.05,1.2,1.35,1.5$, and $2$.

We have six non-equivalent $V$ lines, each pair of them being positioned at
the square faces of the Brillouin zone. The contribution of the vicinity of
these lines, see Eq. (2), reads (we take into account that a pair of $V$ lines
crosses at higher-order van Hove X point, so that to avoid doubling the
contribution of X point vicinity we divide this by factor of 2)

$\Delta\rho_{V}(\epsilon,\tau=0)=3\int_{\mathcal{O}(V)}\frac{d^{3}\mathbf{k}}{V_{\rm
BZ}}\delta(\epsilon-t_{\rm fcc}\left(\mathbf{k};\tau=0\right)),$ (6)

where the Brillouin zone volume for fcc lattice reads $V_{\rm BZ}=4\pi^{3}$.
$q_{x}=(1-\cos k_{z})^{-1/2}q_{\perp}\cos\varphi$, $q_{y}=(1+\cos
k_{z})^{-1/2}q_{\perp}\sin\varphi$ and $\mathcal{O}(V)$ is determined by
cutoff conditions. We obtain

$\Delta\rho_{V}(\epsilon,\tau=0)\\\ =\frac{3}{V_{\rm
BZ}}\int\limits_{-\pi/2}^{\pi/2}dk_{z}\int dq_{x}dq_{y}\delta\left(\epsilon-
E_{V}(k_{z},q_{x},q_{y})\right)\\\ =\frac{3}{V_{\rm
BZ}}\int\limits_{-\pi/2}^{\pi/2}\frac{dk_{z}}{|\sin
k_{z}|}\int\limits_{0}^{\bar{q}_{\perp}\left(k_{z}\right)}dq_{\perp}q_{\perp}\int\limits_{0}^{2\pi}d\varphi\delta\left(\epsilon-4+2q^{2}_{\perp}\right.\\\
\left.-\frac{q^{4}_{\perp}}{12}\left(\frac{\cos^{4}\varphi}{\sin^{2}\frac{k_{z}}{2}}+\frac{\sin^{4}\varphi}{\cos^{2}\frac{k_{z}}{2}}+\frac{3\sin^{2}2\varphi}{\sin^{2}k_{z}}\right)\right),$
(7)

where $k_{z}$-dependent cutoff parameter is introduced which is determined
from fourth-order terms in the spectrum expansion. Main contribution to the
integral originates from small $k_{z}$, so that $\sin^{4}\varphi$ term is
irrelevant. Maximal value of the fourth-order term is
${q^{4}_{\perp}}/(3k_{z}^{2})$. From the condition
$2q_{\perp}^{2}={q^{4}_{\perp}}/(3k_{z}^{2})$ we find an estimation of the
scale where fourth-order terms become important,
$\bar{q}_{\perp}\left(k_{z}\right)=\alpha_{V}k_{z}$, $\alpha_{V}\sim\sqrt{6}$.
We get finally the asymptotics valid at small $4-\epsilon$:

$\Delta\rho_{V}(\epsilon,\tau=0)=\frac{3}{8\pi^{2}}\theta\left(4-\epsilon\right)\ln\frac{8\alpha^{2}_{V}}{4-\epsilon}.$
(8)

The line $\varLambda$, joining van Hove points $\Gamma$ and L, becomes van
Hove line at $\tau=1$. We consider this case by expanding spectrum in the
vicinity of van Hove line $\varLambda$: $k_{x}=k_{y}=k_{z}=k_{\varLambda}$,
$0<k_{\lambda}<\pi/2$. We parametrize the line $\Lambda$ as
$\mathbf{k}_{\varLambda}(q_{1},q_{2},k_{\varLambda})=q_{\perp}\cos\varphi\mathbf{e}_{1}+q_{\perp}\sin\varphi\mathbf{e}_{2}+\sqrt{3}k_{\varLambda}\mathbf{e}_{3}$,
where the orthonormal basis $\mathbf{e}_{1}(+1/\sqrt{2},0,-1/\sqrt{2})$,
$\mathbf{e}_{2}(-1/\sqrt{6},+2/\sqrt{6},-1/\sqrt{6})$,
$\mathbf{e}_{2}(+1/\sqrt{3},+1/\sqrt{3},+1/\sqrt{3})$ was used. We have up to
higher order terms $E_{\varLambda}(k_{\varLambda},q_{\perp},\varphi)=t_{\rm
fcc}\left(\mathbf{k}_{\varLambda}(q_{\perp},\varphi,k_{\varLambda});\tau=1\right)=-6+6\sin^{2}k_{\varLambda}q_{\perp}^{2}-\sqrt{6}\sin
k_{\varLambda}\cos
k_{\varLambda}\sin\varphi(3\cos^{2}\varphi-\sin^{2}\varphi)q^{3}_{\perp}-(3-5\cos
2k_{\varLambda})q^{4}_{\perp}/8$. Since in the vicinity of $k_{\varLambda}=0$
the leading non-constant contribution starts from fourth-order terms in
$q_{\perp}$ and $k_{z}$, we see that $\Gamma$ is a van Hove higher-order point
with all the inverse masses being zero. Analogously to the case of $V$ line we
introduce the cutoff for $\bar{q}_{\perp}=\alpha_{\perp}k_{\varLambda}$, where
numerical value $\alpha_{\perp}\sim\sqrt{6}$ and should be determined more
precisely later.

We extract from the definition (2) the contribution from the vicinity eight
$\Lambda$ lines

$\Delta\rho_{\varLambda}(\epsilon,\tau=1)=8\int_{\mathcal{O}(\varLambda)}\frac{d^{3}\mathbf{k}}{V_{\rm
BZ}}\delta(\epsilon-t_{\rm fcc}\left(\mathbf{k};\tau=1\right))\\\
=\frac{8}{4\pi^{3}}\int\limits_{0}^{\pi/2}dk_{\varLambda}\int\limits_{0}^{\bar{q}\left(k_{\varLambda}\right)}dq_{\perp}q_{\perp}\int\limits_{0}^{2\pi}d\varphi\delta\left(\epsilon-
E_{\varLambda}(k_{\varLambda},q_{\perp},\varphi)\right).$ (9)

Due to the use of the cutoff, we can neglect subleading terms in formula (9)
to obtain:

$\Delta\rho_{\varLambda}(\epsilon,\tau=1)=\frac{1}{3\pi^{2}}\left(\frac{6\alpha^{2}_{\perp}}{6+\epsilon}\right)^{1/4}.$
(10)

To get a close agreement for Eq. (10) and numerical calculation (see below) in
the vicinity $\epsilon=-6$ point we choose $\alpha_{\perp}=1.88\sqrt{6}\approx
4.6$. We compare $\rho_{\rm fcc}(\epsilon,\tau=1)$ calculated by direct using
Eq. (23), see below, and asymptotics (10) with a chosen $\alpha_{\perp}=4.6$
in Fig. 6. One case see a good agreement in the vicinity of the vHS point at
$\epsilon=-6$.

Figure 6: $\tau=1$. Density of states $\rho_{\rm fcc}(\epsilon,\tau=1)$ (see
below Eq. (23)) and its analytic ansatz
$\Delta\rho_{\varLambda}(\epsilon,\tau=1)$, see Eq. (10), in the vicinity of
band bottom. In the inset the plots of $1/\rho^{4}_{\rm fcc}(\epsilon,\tau=1)$
and $1/\Delta\rho^{4}_{\varLambda}(\epsilon,\tau=1)$ are shown.

##  3 Fully analytical treatment of the density of states

To derive an analytic expression for the DOS we use the effective one-
dimensional presentation of the spectrum (1):

$t_{\rm
fcc}\left(\mathbf{k};\tau\right)=t_{0}(k_{x},k_{y})-2p(k_{x},k_{y})\cos
k_{z}-2p^{\prime}(1+\cos 2k_{z}),$ (11)

where

$\displaystyle t_{0}(k_{x},k_{y})$ $\displaystyle=$ $\displaystyle-4t\cos
k_{x}\cos k_{y}-2\tau t(1-\cos 2k_{x}-\cos 2k_{y}),$ $\displaystyle
p(k_{x},k_{y})$ $\displaystyle=$ $\displaystyle 2t(\cos k_{x}+\cos k_{y}),$
(12)

and $p^{\prime}=-\tau t$. Below we set for brevity $t=1$. Investigation of the
spectrum (1) [27] yields the following boundaries for it

$\displaystyle E_{\rm min}(\tau)$ $\displaystyle=$ $\displaystyle{\rm
min}[-12+6\tau,-6\tau],$ $\displaystyle E_{\rm max}(\tau)$ $\displaystyle=$
$\displaystyle{\rm max}[4+6\tau,4+2\tau,-6\tau].$ (13)

We directly use the definition of the density of states

$\rho_{\rm
fcc}(\epsilon;\tau)=\iiint\limits_{0<k_{i}<\pi}\frac{dk_{x}}{\pi}\frac{dk_{y}}{\pi}\frac{dk_{z}}{\pi}\delta(\epsilon-
t_{\rm fcc}\left(\mathbf{k};\tau\right)).$ (14)

to obtain

$\rho_{\rm
fcc}(\epsilon)=\iint\limits_{0<k_{i}<\pi}\frac{dk_{x}}{\pi}\frac{dk_{y}}{\pi}\rho_{1D}(\epsilon-
t_{0}(k_{x},k_{y}),t_{1D}(k_{x},k_{y}),t^{\prime}_{1D}),$ (15)

where we have introduced the known DOS

$\rho_{1D}(\epsilon;p,p^{\prime})=\int\limits_{0}^{\pi}\frac{dk}{\pi}\delta(\epsilon-
t_{1D}(p,p^{\prime}))$ (16)

for the 1D spectrum within nearest and next-nearest neighbor hopping
approximation (with effective integrals $p$ and $p^{\prime}$)

$t_{1D}(k;p,p^{\prime})=-2p\cos k-2p^{\prime}(1+\cos 2k).$ (17)

An explicit expression for (16) is

$\rho_{1D}(\epsilon;p,p^{\prime})=\sum_{\sigma=\pm
1}\bar{\rho}_{1D}\left(\epsilon;\sigma|p|,p^{\prime}\right),$ (18)

where

$\bar{\rho}_{1D}\left(\epsilon;p,p^{\prime}\right)=\frac{1}{2\pi}\sqrt{\frac{\theta(p^{2}-4p^{\prime}\epsilon)}{p^{2}-4p^{\prime}\epsilon}}\varphi\left(\frac{\sqrt{p^{2}-4p^{\prime}\epsilon}+p}{4p^{\prime}}\right)$
(19)

and

$\varphi(x)=g(1-x^{2})$ (20)

with $g(x)=\sqrt{\theta(x)/x}$ and $\theta(x)$ being the Heaviside step
function.

Further simplification can be achieved by introducing symmetrized variables:
$s(k_{x},k_{y})=(1/2)(\cos k_{x}+\cos k_{y})$, $\xi(k_{x},k_{y})=(1/2)|\cos
k_{x}-\cos k_{y}|$.

We thereby obtain

$\rho_{\rm
fcc}(\epsilon,\tau)=\frac{1}{\pi^{3}}\int\limits_{-1}^{+1}ds\int\limits_{0}^{1-|s|}\frac{d\xi}{\sqrt{((1-|s|)^{2}-\xi^{2})((1+|s|)^{2}-\xi^{2})}}\\\
\times\varphi\left(\left(1/\mathcal{K}(\epsilon,\tau,s,\xi^{2})+s\right)/\tau\right)\mathcal{K}(\epsilon,\tau,s,\xi^{2}),$
(21)

where

$\mathcal{K}(\epsilon,\tau,s,a)=g\left(1+\tau-2\tau^{2})s^{2}+\tau((\epsilon-6\tau)/4-(1+2\tau)a)\right)$
(22)

is introduced for brevity. We rescale $\xi^{2}=(1-|s|)^{2}\zeta$ to make inner
integration limits constant:

$\rho_{\rm
fcc}(\epsilon,\tau)=\frac{1}{2\pi^{3}}\int\limits_{-1}^{+1}ds\int\limits_{0}^{1}\frac{d\zeta
Q(\epsilon,\tau,s,\zeta)}{\sqrt{(1-\zeta)\zeta}},$ (23)
$Q(\epsilon,\tau,s,\zeta)=\frac{\varphi\left(\left(1/\mathcal{K}(\epsilon,\tau,s,(1-|s|)^{2}\zeta)+s\right)/\tau\right)\mathcal{K}(\epsilon,\tau,s,(1-|s|)^{2}\zeta))}{\sqrt{(1+|s|)^{2}-(1-|s|)^{2}\zeta}}.$
(24)

The formulas (20), (22–24) provide analytical results which are convenient for
numerical calculations.

##  4 Comparison with tetrahedron method

A commonly used tetrahedron method [31] is a popular tool of density-of-states
calculation within density functional theory [32]. A fundamental block of this
approach is linear approximation of the spectrum within an elementary
tetrahedron. However, when one of tetrahedron vertices is a van Hove point,
its contribution, being actually dominating, is crudely averaged with the
contributions of another vertices. This implies very bad accuracy of the
method when the energy is in the vicinity of van Hove points. In Fig. 7, a
comparison of the results of direct calculation using Eq. (23) and tetrahedron
method is shown. For the latter method, we find strong artificial oscillations
in the vicinity of van Hove energies. The convergence of the results in the
limit $N_{\rm mesh}\rightarrow\infty$ is thereby substantially poor. The
origin of this discrepancy is an averaging of vertices of particular
tetrahedron with zero velocity and non-zero on equal foot, which
underestimates the contribution of van Hove singularity point vicinity in
reciprocal space, see also Ref. [33].

Figure 7: Comparison of DOS for fcc lattice with $\tau=-0.6$ in the vicinity
of plateau calculated directly using Eq. (23), tetrahedron method with
tetrahedron number $6\times N_{\rm mesh}\times N_{\rm mesh}\times N_{\rm
mesh}$, for the grid resolution $N_{\rm g}=20,50$ and in the limit $d=\infty$,
see derivation in the Appendix. The inset shows the whole bandwidth energy
range.

##  5 Conclusions

To conclude, we have analyzed in detail the van Hove singularities in the
excitation spectrum of fcc lattice. These singularities can play an important
role in the temperature dependencies of physical properties. e.g., electronic
heat capacity, magnetic susceptibility, thermoelectric power (for bipartite
lattices, these effects were treated in Refs.[26, 27]). In this connection,
examples of fcc Ni and ZrZn2 (the C15 Laves phase crystal structure which is a
superposition of fcc sublattices) can be once more mentioned. The vHS can be
also important for some lattice and magnetic characteristics owing to
anomalies of phonon and magnon spectra. Especial role belongs to van Hove
lines intersection typically forming a higher-order van Hove point, which
leads to more strong effects [10].

We also state that DOS in the vicinity of vHS energies can be poorly captured
by standard approaches within dynamical mean-field theory ($d=\infty$ limit)
and tetrahedron method, which are popular in density-functional calculations.
Our analysis can be useful to supplement computational approaches which deal
with the electron spectrum and properties of actual materials.

The research was carried out within the state assignment of the Ministry of
Science and Higher Education of the Russian Federation (theme “Quantum” No.
122021000038-7) and supported in part by Russian Foundation for Basic Research
(project No. 20-02-00252). The calculations were performed on the Uran
supercomputer at the IMM UB RAS.

## Appendix. $d=\infty$ case

In Ref. [29], the fcc-lattice DOS in the limit of infinite space dimension $d$
was considered in the special case $t^{\prime}=t/2$ (where giant quasi-one-
dimension van Hove singularity is formed owing to van Hove surface). Passing
to such a limit may be useful in the context of dynamical mean-field approach
implementation. Therefore, it is instructive to compare the DOS form in the
limit of infinite dimension with the case $d=3$. To derive an explicit
expression for DOS in this limit we have to set the scaling of hopping
integrals with $d$: $t=t_{1}/\sqrt{d(d-1)}$, $t^{\prime}=t_{2}/\sqrt{2d}$
(this is based on the fact that a site in fcc lattice has $2d(d-1)$ nearest
and $2d$ next-nearest neighbours). The derivation uses “statistical”
independence of the quantities $\xi=\sqrt{2/d}\sum_{i}\cos k_{i}$ and
$\eta=\sqrt{2/d}\sum_{i}\cos 2k_{i}$ in the limit $d\rightarrow\infty$. Since
$\varepsilon_{\bf k}=-t_{1}(\xi^{2}-1)+t_{2}\eta$, we obtain directly

$\rho_{d=\infty}(\varepsilon;t_{1},t_{2})=\frac{\exp\left[-(\varepsilon-
t_{1})^{2}/(2t^{2}_{2})\right]}{2\pi\sqrt{|t_{1}t_{2}|}}f\left(\frac{t^{2}_{2}-2t_{1}(\varepsilon-
t_{1})}{|t_{1}t_{2}|}\right),$ (25)

where

$f(x)=\frac{e^{x^{2}/16}}{2}\sqrt{|x|}\begin{cases}K_{1/4}(x^{2}/16),&x>0,\\\
\frac{\pi}{\sqrt{2}}\left(I_{1/4}(x^{2}/16)+I_{-1/4}(x^{2}/16)\right),&x<0,\end{cases}$
(26)

where $I_{\nu}$ and $K_{\nu}$ are Infeld and McDonald functions, respectively.

The comparison of the results for the cases $d=3$ and $d\rightarrow\infty$ at
$\tau=-0.6$ is shown in Fig. 7. We can see that the $d=3$ DOS possesses
pronounced van Hove plateau, which is destroyed in the limit
$d\rightarrow\infty$. Note also that the case of giant van Hove singularity
$t^{\prime}=t/2$ is not captured by Eq. (25).

## References

  * [1] L. Van Hove, Phys. Rev. 89, 1189 (1953).
  * [2] S. V. Vonsovskii, M. I. Katsnelson, and A. V. Trefilov, Phys. Met. Metallogr. 76, 247 (1993).
  * [3] E. C. Stoner, Proc. Roy. Soc. A 165, 372 (1938).
  * [4] D. M. Edwards and E. P. Wohlfarth, Proc. R. Soc. Lond. A 303, 127 (1968).
  * [5] K. Kim, S. Kim, J. S. Kim, H. Kim, J.-H. Park, and B. I. Min, Phys. Rev. B 97, 165102 (2018).
  * [6] M. I. Katsnel’son, G. V. Peschanskikh, and A. V. Trefilov, Sov. Phys. Solid State 32, 272 (1990).
  * [7] N. F. Q. Yuan, H. Isobe, L. Fu, Nat. Comm. 10, 5769 (2019).
  * [8] H. Isobe, N. F. Q. Yuan, L. Fu, Phys. Rev. X 8, 041041 (2018).
  * [9] V. Kozii, H. Isobe, J. W. F. Venderbos, L. Fu, Phys. Rev. B 99, 144507 (2019).
  * [10] N. T. Hung, J. M. Adhidewata, A. R. T. Nugraha, R. Saito, Phys. Rev. B 105, 115142 (2022).
  * [11] Y. Shao, A. N. Rudenko, J. Hu, Z. Sun, Y. Zhu, S. Moon, A. Millis, S. Y., A. I. Lichtenstein, D. Smirnov, Z. Q. Mao, M. I. Katsnelson, and D. N. Basov, Nat. Phys. 16, 636 (2020).
  * [12] A. N. Rudenko, E. A. Stepanov, A. I. Lichtenstein, and M. I. Katsnelson, Phys. Rev. Lett. 120, 216401 (2018).
  * [13] A. S. Belozerov, A. A. Katanin and V. I. Anisimov, Phys. Rev. B 97, 115141 (2018).
  * [14] V. I. Anisimov, I. A. Nekrasov, D. E. Kondakov, T. M. Rice, and M. Sigrist, Eur. Phys. J. B 25, 191 (2002).
  * [15] S. L. Skornyakov, A. A. Katanin, and V. I. Anisimov, Phys. Rev. Lett. 106, 047007 (2011).
  * [16] R. J. Jelitto, J. Phys. Chem. Solids 30, 609 (1969).
  * [17] P.A. Igoshev, M.A. Timirgazin, A.A. Katanin, A.K. Arzhnikov and V.Yu. Irkhin, Phys. Rev. B 81, 094407 (2010).
  * [18] P.A. Igoshev, M.A. Timirgazin, V.F. Gilmutdinov, A.K. Arzhnikov and V. Yu. Irkhin, J. Phys.: Cond. Matt. 27, 446002 (2015).
  * [19] A. A. Katanin and A. P. Kampf, Phys. Rev. B 68, 195101 (2003).
  * [20] R. Hlubina, S. Sorella, and F. Guinea, Phys. Rev. Lett. 78, 1343 (1997); R. Hlubina, Phys. Rev. B 59, 13960 (1999).
  * [21] S. J. C. Yates, G. Santi, S. M. Hayden, P. J. Meeson, and S. B. Dugdale, Phys. Rev. Lett. 90, 057003 (2003).
  * [22] Zs. Major, S. B. Dugdale, R. J. Watts, G. Santi, M. A. Alam, S. M. Hayden, J. A. Duffy, J.W. Taylor, T. Jarlborg, E. Bruno, D. Benea, and H. Ebert, Phys. Rev. Lett. 92, 107003 (2004).
  * [23] Y. Amaji , T. Misawa, M. Imada, J. Phys. Soc. Jpn 76, 063702 (2007).
  * [24] N. Kabeya, H. Markawa, K. Deguchi, N. Kimura, H. Aoki, N. K. Sato, J. Phys. Soc. Jpn 81, 073706 (2012).
  * [25] A. Hausoel, M. Karolak, E. Sasioglu, et al. Nat. Commun. 8, 16062 (2017).
  * [26] P. A. Igoshev and V. Yu. Irkhin, Phys. Met. Metallogr. 120, 1282 (2019).
  * [27] P. A. Igoshev and V. Yu. Irkhin, JETP Lett. 110, 727 (2019).
  * [28] R. H. Swendsen and H. Callen, Phys. Rev. B 6, 2860 (1972).
  * [29] M. Ulmke, Eur. Phys. J. B 1, 301 (1998).
  * [30] P.A. Igoshev, E.E. Kokorina, I.A. Nekrasov, Physics of Metals and Metallography 118, 207 (2017).
  * [31] P. E. Blöchl, O. Jepsen, O. K. Andersen, Phys. Rev. B 49, 16223 (1994).
  * [32] R.O. Jones, O. Gunnarsson, Rev. Mod. Phys. 61, 689 (1989).
  * [33] A.A. Stepanenko, D.O. Volkova, P.A. Igoshev, A.A. Katanin, J. Exp. Theor. Phys. 125, 879 (2017).