Michael Suleymanov

M A Zubkov
email: zubkov@itep.ru

Wigner -Weyl formalism and the propagator of Wilson fermions in the presence of varying external electromagnetic field

Keywords:

We develop Wigner -Weyl formalism for the lattice models. For the definiteness we consider Wilson fermions in the presence of U (1) gauge field. The given technique reduces calculation of the two point fermionic Green function to solution of the Groenewold equation. It relates Wigner transformation of the Green function with the Weyl symbol QW of Wilson Dirac operator. We derive the simple expression for QW in the presence of varying external U (1) gauge field. Next, we solve the Groenewold equation to all orders in powers of the derivatives of QW . Thus the given technique allows to calculate the fermion propagator in the lattice model with Wilson fermions in the presence of arbitrary background electromagnetic field. The generalization of this method to the other lattice models is straightforward.

I. INTRODUCTION

The Wigner -Weyl formalism was originally proposed for the reformulation of ordinary quantum mechanics. Later it was also adopted in some form both for the quantum field theory and for the condensed matter physics theory. This formalism in its original form has been developed by H. Groenewold [START_REF] Groenewold | On the Principles of elementary quantum mechanics[END_REF] and J. Moyal [START_REF]Quantum mechanics as a statistical theory[END_REF]. It is based on the notions of the Weyl symbol of operator and the Wigner distribution function. The authors of [START_REF] Groenewold | On the Principles of elementary quantum mechanics[END_REF][START_REF]Quantum mechanics as a statistical theory[END_REF] used the ideas developed earlier by H. Weyl [START_REF] Weyl | Quantenmechanik und Gruppentheorie[END_REF] and E. Wigner [START_REF] Wigner | On the quantum correction for thermodynamic equilibrium[END_REF]. The Wigner -Weyl formalism in quantum mechanics is often referred to as the phase space formulation. It is defined in phase space that is composed of both coordinates and momenta. At the same time the conventional formulation uses either coordinate space or momentum space representations. In the phase space formulation the quantum state is described by the Wigner distribution (instead of a wave function), while the operator product is replaced by the Moyal product of functions defined in phase space.

The phase space formulation of quantum mechanics reduces the operator formulation in coordinate or momentum space to the formulation that deals with the ordinary functions of coordinates and momenta [START_REF] Ali | Quantization Methods: A Guide for Physicists and Analysts[END_REF]6]. There are a lot of various applications of the phase space formulation of quantum mechanics (for the review see, for example, [START_REF] Curtright | Quantum Mechanics in Phase Space[END_REF][START_REF] Zachos | Quantum Mechanics in Phase Space[END_REF]). At the present moment there exist the alternative versions of this formulation, in which the main notionthe distribution function -is defined differently [START_REF] Cohen | Generalized Phase-Space Distribution Functions[END_REF][START_REF] Agarwal | Calculus for Functions of Noncommuting Operators and General Phase-Space Methods in Quantum Mechanics. II. Quantum Mechanics in Phase Space[END_REF]. The most popular version mentioned above operates with the Wigner distribution function W (x, p) [START_REF] Wigner | On the quantum correction for thermodynamic equilibrium[END_REF]. Among the alternative versions we mention those discussed in [START_REF] Sudarshan | Equivalence of Semiclassical and Quantum Mechanical Descriptions of Statistical Light Beams[END_REF][START_REF] Glauber | Coherent and Incoherent States of the Radiation Field[END_REF][START_REF] Husimi | Some Formal Properties of the Density Matrix[END_REF][START_REF] Agarwal | Calculus for Functions of Noncommuting Operators and General Phase-Space Methods in Quantum Mechanics. I. Mapping Theorems and Ordering of Functions of Noncommuting Operators[END_REF][START_REF] Cahill | Ordered Expansions in Boson Amplitude Operators[END_REF].

In the one -dimensional case the quantum mechanical Wigner distribution function W (x, p) depends on the coordinate x and on momentum p. Distribution W (x, p) determines the probability that the coordinate x belongs to the interval [a, b]:

P [a ≤ x ≤ b] = 1 2π ∫ b a ∫ ∞ -∞ W (x, p) dp dx
In ordinary quantum mechanics each observable is represented by operator. Weyl symbol A W (x, p) of operator  is the function in phase space such that the expectation value of the observable with respect to the given distribution W (x, p) is [START_REF]Quantum mechanics as a statistical theory[END_REF][START_REF] Lax | Quantum Noise. XI. Multitime Correspondence between Quantum and Classical Stochastic Processes[END_REF]]

⟨ Â⟩ = 1 2π ∫ A W (x, p)W (x, p) dp dx.
The Wigner function may be expressed through the ordinary wave function ψ(x) as follows W (x, p) = ∫ dy e -ipy ψ * (x + y/2)ψ(x -y/2) Time evolution of the Wigner function is governed by the following equation i∂ t W (x, p, t) = H(x, p) ⋆ W (x, p, t) -W (x, p, t) ⋆ H(x, p)

Here the star (or Moyal) product of the two functions f and g is defined as

f ⋆ g = f exp ( i 2 ( ← - ∂ x -→ ∂ p - ← - ∂ p - → ∂ x )
) g

The left arrow above the derivative means that it acts on f while the right arrow means that it acts on g. By H(x, p) the Weyl symbol of the Hamiltonian is denoted. In general case the definition of the Weyl symbol of operator  is:

A W (x, p) =
∫ dy e -ipy ⟨x + y/2| Â|x -y/2⟩

As it was mentioned above, the Wigner -Weyl formalism has also been extended, at least partially, to the quantum field theory. Namely, one may consider the analogue of the Wigner distribution function

W Γ (x, p) = ∫ dy e -ipy ⟨ ψ(x + y/2)Γψ(x -y/2)⟩
Here ψ is a certain fermionic operator while Γ is an appropriate matrix in spinor and flavor spaces. (Obviously, the similar construction may be introduced also for bosons.) In particular, in this way the analogue of the Wigner distribution function has been defined in QCD (see, for example, [START_REF] Lorce | Quark Wigner Distributions and Orbital Angular Momentum[END_REF][START_REF] Elze | Transport Equations for the QCD Quark Wigner Operator[END_REF] and references therein). Besides, the similar notion of the Wigner distribution has been implemented in the framework of the quantum kinetic theory based on the field theory [START_REF] Hebenstreit | Schwinger pair production in space and time-dependent electric fields: Relating the Wigner formalism to quantum kinetic theory[END_REF][START_REF] Calzetta | Quantum Kinetic Field Theory in Curved Space-time: Covariant Wigner Function and Liouville-vlasov Equation[END_REF]. It was also used in certain noncommutative field theories [START_REF] Bastos | Weyl-Wigner Formulation of Noncommutative Quantum Mechanics[END_REF][START_REF] Dayi | Wigner functions for the Landau problem in noncommutative spaces[END_REF]. Applications of the Wigner function formalism to cosmology were discussed in [START_REF] Habib | Wigner function and decoherence in quantum cosmology[END_REF]. Another applications of this formalism may be found, for example, in [START_REF] Chapman | HBT correlators: Current formalism versus Wigner function formulation[END_REF], see also [START_REF] Berry | Semi-Classical Mechanics in Phase Space: A Study of Wigner's Function[END_REF].

Recently the Wigner -Weyl formalism has been adopted to the investigation of anomalous transport in the quantum field theory [START_REF] Zubkov | Topology of the momentum space, Wigner transformations, and a chiral anomaly in lattice models[END_REF][START_REF] Chernodub | Scale Magnetic Effect in Quantum Electrodynamics and the Wigner-Weyl Formalism[END_REF][START_REF] Khaidukov | Chiral Separation Effect in lattice regularization[END_REF][START_REF] Zubkov | Momentum space topology of QCD[END_REF][START_REF] Zubkov | Absence of equilibrium chiral magnetic effect[END_REF][START_REF] Zubkov | Wigner transformation, momentum space topology, and anomalous transport[END_REF]. The main advantage of this latter approach is that the response of the nondissipative components of both vector and axial currents to the external field strength are expressed through the topological invariants in momentum space. These quantities are not changed if we deform the system smoothly. Thus we are able to calculate the corresponding conductivities within the simple noninteracting systems connected continuously with the more complicated interacting ones. And this gives the values of the conductivities for the given complicated systems. In particular, in this way the absence of the equilibrium chiral magnetic effect [START_REF] Kharzeev | The Chiral Magnetic Effect and Anomaly-Induced Transport[END_REF] in the field theory has been proved [START_REF] Zubkov | Absence of equilibrium chiral magnetic effect[END_REF] while the anomalous quantum Hall effect has been described rigorously both for the Weyl semimetals and for certain 2D and 3D topological insulators [START_REF] Zubkov | Wigner transformation, momentum space topology, and anomalous transport[END_REF]. Besides, the chiral separation effect (proposed in [START_REF] Metlitski | Anomalous Axion Interactions and Topological Currents in Dense Matter[END_REF]) was rigorously re -derived [START_REF] Khaidukov | Chiral Separation Effect in lattice regularization[END_REF] and the alternative derivation of chiral anomaly in lattice regularized quantum field theory has been given [START_REF] Zubkov | Topology of the momentum space, Wigner transformations, and a chiral anomaly in lattice models[END_REF]. The fermion zero modes on vortices in the color superconductor phase of QCD have been considered using this technique in [START_REF] Zubkov | Momentum space topology of QCD[END_REF]. In addition, the scale magnetic effect proposed in [START_REF] Chernodub | Anomalous Transport Due to the Conformal Anomaly[END_REF] has been considered in the framework of this formalism [START_REF] Chernodub | Scale Magnetic Effect in Quantum Electrodynamics and the Wigner-Weyl Formalism[END_REF].

It is worth mentioning that previously the momentum space topological invariants expressed in terms of the Green functions were used mainly in the condensed matter physics theory (for the review see [START_REF] Hasan | Topological Insulators[END_REF][START_REF] Qi | Topological insulators and superconductors[END_REF][START_REF] Volovik | Topology of quantum vacuum, draft for Chapter in proceedings of the Como Summer School on analogue gravity[END_REF][START_REF] Volovik | Quantum phase transitions from topology in momentum space[END_REF][START_REF] Volovik | Topological invariants for Standard Model: from semi-metal to topological insulator[END_REF]). The momentum space topological invariants protect gapless fermions on the boundaries of topological insulators [START_REF] Gurarie | Single-particle Green-s functions and interacting topological insulators[END_REF][START_REF] Essin | Bulk-boundary correspondence of topological insulators from their Green's functions[END_REF] and protect the bulk gapless fermions in Dirac and Weyl semi -metals [START_REF] Volovik | Topological invariants for Standard Model: from semi-metal to topological insulator[END_REF][START_REF] Volovik | The Universe in a Helium Droplet[END_REF]. The gapless fermions associated with topological defects and textures existing in the fermionic superfluids are also described by momentum space topology [START_REF] Volovik | Topological Superfluids[END_REF]. In the context of relativistic quantum field theory momentum space topology has been discussed, for example, in [START_REF] Volovik | The Universe in a Helium Droplet[END_REF][START_REF] Nielsen | Absence of neutrinos on a lattice. I -Proof by homotopy theory[END_REF][START_REF] So | Induced topological invariants by lattice fermions in odd dimensions[END_REF][START_REF] Ishikawa | Magnetic field induced multi component QED in three-dimensions and quantum Hall effect[END_REF][START_REF] Kaplan | Method for simulating chiral fermions on the lattice[END_REF][START_REF] Golterman | Chern-Simons currents and chiral fermions on the lattice[END_REF][START_REF] Hořava | Stability of Fermi surfaces and K-theory[END_REF][START_REF] Creutz | Four-dimensional graphene and chiral fermions[END_REF][START_REF] Kaplan | Spacetime as a topological insulator[END_REF]. In [START_REF] Zubkov | Momentum space topological invariants for the 4D relativistic vacua with mass gap[END_REF] the lattice regularization of QFT with Wilson fermions was discussed from the point of view of the momentum space topology. Appearance of the massless fermions at the intermediate values of bare mass parameter is related to the jump of the introduced momentum space topological invariant.

The version of the Wigner -Weyl formalism of [START_REF] Zubkov | Topology of the momentum space, Wigner transformations, and a chiral anomaly in lattice models[END_REF][START_REF] Khaidukov | Chiral Separation Effect in lattice regularization[END_REF][START_REF] Zubkov | Absence of equilibrium chiral magnetic effect[END_REF][START_REF] Zubkov | Wigner transformation, momentum space topology, and anomalous transport[END_REF] deals with the lattice regularized quantum field theory. Here the two -point fermion Green function G(p, q) in momentum space M (p, q ∈ M) has been considered. It obeys equation

Q(p -A(i∂ p )))G(p, q) = δ(p -q)
where Q(p) is the lattice Dirac operator written in momentum space while A(x) is external electromagnetic field. Its appearance in momentum representation is given by the pseudo -differential operator A(i∂ p ) realizing the so -called Peierls substitution. Notice, that in this formalism the imaginary time of the Euclidian formulation of the quantum field theory gives one of the components of the (discrete) coordinate space while the corresponding momentum is the fourth component of momentum vector that belongs to M.

Wigner transformation of the two point Green function plays the role similar to the Wigner distribution in quantum mechanical formulation of [START_REF] Groenewold | On the Principles of elementary quantum mechanics[END_REF] and [START_REF]Quantum mechanics as a statistical theory[END_REF]. It may be defined in continuous momentum space for the lattice model in the way similar to the Wigner transformation of continuous coordinate space:

G W (x, p) ≡ ∫ dqe ixq G(p + q/2, p -q/2) (1)
It obeys the Groenewold equation

G W (x, p) ⋆ Q W (x, p) = 1 (2)
with the same star operation as above extended to the D -dimensional vectors of coordinates x and momentum p, while Q W is the Weyl symbol of operator Q(p -A(i∂ p )). (Compare Eq. (2) with Eq. (4.38) of [START_REF] Groenewold | On the Principles of elementary quantum mechanics[END_REF] and Eq. (7.10) of [START_REF]Quantum mechanics as a statistical theory[END_REF], where the Weyl symbol of the commutator of two operators is represented.)

In the present paper we proceed with the development of the approach of [START_REF] Zubkov | Topology of the momentum space, Wigner transformations, and a chiral anomaly in lattice models[END_REF][START_REF] Khaidukov | Chiral Separation Effect in lattice regularization[END_REF][START_REF] Zubkov | Absence of equilibrium chiral magnetic effect[END_REF][START_REF] Zubkov | Wigner transformation, momentum space topology, and anomalous transport[END_REF]. For the definiteness we restrict ourselves with the lattice model with Wilson fermions in the presence of arbitrary external electromagnetic field. The obtained results may easily be extended to the other lattice models as well as to various tight -binding models of solid state physics. First of all we derive the precise expression for the Weyl symbol of the Wilson Dirac operator. Next, we present the complete iterative solution of the Groenewold equation Eq. ( 2), which allows to calculate the fermion propagator in the background of arbitrary external electromagnetic field.

The paper is organized as follows. We start in Sect. II from the pedagogical introduction to the conventional notions of Wigner transformation, Weyl symbols of operators and Moyal product. In Sect. III we proceed with the summary of the momentum space formulation of [START_REF] Zubkov | Topology of the momentum space, Wigner transformations, and a chiral anomaly in lattice models[END_REF][START_REF] Khaidukov | Chiral Separation Effect in lattice regularization[END_REF][START_REF] Zubkov | Absence of equilibrium chiral magnetic effect[END_REF][START_REF] Zubkov | Wigner transformation, momentum space topology, and anomalous transport[END_REF]. In Sect. IV we derive the Peierls substitution, that allows to calculate easily the Wilson Dirac operator in momentum space in the presence of arbitrary electromagnetic field. In Sect. V we present our results on the Weyl symbol of Wilson Dirac operator. In Sect. VI we propose the procedure of the iterative solution of the Groenewold equation, which allows to calculate completely the propagator of Wilson fermions in the presence of external electromagnetic field. In Sect VII we end with the conclusions.

II. WIGNER TRANSFORMATION IN CONTINUOUS COORDINATE SPACE AND CONTINUOUS MOMENTUM SPACE

In this section we briefly review the technique of Wigner transformation applied to quantum mechanics defined in infinite continuous coordinate space.

A. Weyl symbol of operator

We start from the definition of the average of operator  with respect to quantum state Ψ

⟨Ψ| Â |Ψ⟩ = ∫ dxdy ⟨Ψ|x⟩ ⟨x| Â |y⟩ ⟨y|Ψ⟩ (3)
Here by x, y we denote the continuous coordinates. For simplicity we consider the case of one -dimensional space R 1 . The generalization of our expressions to the case of D -dimensional space R D is straightforward. Let us change the coordinates:

x = u + v/2 y = u -v/2 (4)
Then

dxdy = ∂(x, y) ∂(u, v) dudv = ∂x ∂u ∂y ∂u ∂x ∂v ∂y ∂v dudv = -dudv (5)
This gives

⟨Ψ| Â |Ψ⟩ = - ∫ dxdy ⟨x + y/2| Â |x -y/2⟩ ⟨Ψ|x + y/2⟩ ⟨x -y/2|Ψ⟩ = - ∫ dxdydz ⟨x + y/2| Â |x -y/2⟩ δ(z -y) ⟨Ψ|x + z/2⟩ ⟨x -z/2|Ψ⟩ = - ∫ dxdydzdp ⟨x + y/2| Â |x -y/2⟩ e -ip(z-y) 2π ⟨x -z/2|Ψ⟩ ⟨Ψ|x + z/2⟩ = ∫ dxdp 2π dye ipy ⟨x + y/2| Â |x -y/2⟩ dze ipz ⟨x + z/2|Ψ⟩ ⟨Ψ|x -z/2⟩ (6)
The Weyl symbol of operator  is defined as follows

A W (x, p) ≡ ∫ dye -ipy ⟨x + y/2| Â |x -y/2⟩ (7)
or, in terms of the matrix elements in momentum space:

A W (x, p) ≡ ∫ dqe iqx ⟨p + q/2| Â |p -q/2⟩ (8)
Here

⟨x |p⟩ = 1 √ 2π e ipx
Wigner function for the state Ψ is defined as the Weyl symbol of the corresponding density operator:

W (x, p) = ρ W (x, p) = ∫ dye -ipy ⟨x + y/2|Ψ⟩ ⟨Ψ|x -y/2⟩ (9)
In momentum space we have:

W (x, p) = ρ W (x, p) = ∫ dqe iqx ⟨p + q/2|Ψ⟩ ⟨Ψ|p -q/2⟩ (10)
Hence,

⟨Ψ| Â |Ψ⟩ = ∫ dxdp 2π A W (x, p)W (x, p) (11)
Wigner function for the mixed state with the density matrix ρ =

∑ i |Ψ i ⟩ ρ i ⟨Ψ i |
may be defined as

W (x, p) = ρ W (x, p) = ∫ dqe iqx ∑ i ⟨p + q/2|Ψ i ⟩ ρ i ⟨Ψ i |p -q/2⟩ (12)
The vacuum average of operator  with respect to this mixed state may be written in the similar way

⟨ Â⟩ = ∫ dxdp 2π A W (x, p)W (x, p) (13)

B. Moyal product

The Weyl symbol of the product of two operators is given by

(AB) W (x, p) = ∫ dye -ipy ⟨x + y/2| Â B |x -y/2⟩ = ∫ dydze -ipy ⟨x + y/2| Â |z⟩ ⟨z| B |x -y/2⟩ ( 14
)
The transformation of variables

y = u + v z = x -u/2 + v/2 (15)
gives

dydz = ∂(y, z) ∂(u, v) dudv = ∂y ∂u ∂z ∂u ∂y ∂v ∂z ∂v dudv = dudv (16) and (AB) W (x, p) = ∫ dudve -ip(u+v) ⟨ x + u 2 + v 2 Â x - u 2 + v 2 ⟩ ⟨ x - u 2 + v 2 B x - u 2 - v 2 ⟩ = [∫ due -ipu ⟨ x + u 2 Â x - u 2 ⟩ ] e v 2 ← - ∂x-u 2 -→ ∂x [∫ dve -ipv ⟨ x + v 2 B x - v 2 ⟩ ] = [∫ due -ipu ⟨ x + u 2 Â x - u 2 ⟩ ] e i 2 ( ← - ∂x -→ ∂p- ← - ∂p -→ ∂x ) [∫ dve -ipv ⟨ x + v 2 B x - v 2 ⟩ ] (17)
The Moyal product of the Weyl symbols of the two operators  and B is defined as follows

A W (x, p) ⋆ B W (x, p) ≡ (AB) W (x, p) = A W (x, p)e i 2 ( ← - ∂x -→ ∂p- ← - ∂p -→ ∂x ) B W (x, p) (18)

III. WIGNER TRANSFORMATION IN DISCRETE COORDINATE SPACE AND COMPACT MOMENTUM SPACE

In this section we discuss the generalization of the above mentioned constructions to the case, when coordinate space is discrete and infinite, and, therefore, momentum space is continuous but compact.

A. Weyl symbol of operator

Average of an operator with respect to state Ψ is defined as

⟨Ψ| Â |Ψ⟩ = ∫ dpdq ⟨Ψ|p⟩ ⟨p| Â |q⟩ ⟨q|Ψ⟩ (19)
Here the integral is over the compact momentum space. The integration measure is defined in such a way, that ∫ dp = 2π while

⟨x n |p⟩ = 1 √ 2π e ipxn
for any lattice point x n . Again, we restrict ourselves by the one dimensional case. The generalization to the multidimensional systems is straightforward. Then

⟨Ψ| Â |Ψ⟩ = - ∫ dpdq ⟨p + q/2| Â |p -q/2⟩ ⟨Ψ|p + q/2⟩ ⟨p -q/2|Ψ⟩ = - ∫ dpdqdk ⟨p + q/2| Â |p -q/2⟩ δ(k -q) ⟨Ψ|p + k/2⟩ ⟨p -k/2|Ψ⟩ = - ∑ xn ∫ dpdqdk ⟨p + q/2| Â |p -q/2⟩ e -ixn(k-q) 2π ⟨p -k/2|Ψ⟩ ⟨Ψ|p + k/2⟩ = ∑ xn ∫ dp 2π dqe ixnq ⟨p + q/2| Â |p -q/2⟩ dke ixnk ⟨p + k/2|Ψ⟩ ⟨Ψ|p -k/2⟩ (20)
The Weyl symbol of operator  is then defined as follows

A W (x n , p) ≡ ∫ dqe ixnq ⟨p + q/2| Â |p -q/2⟩ (21)
And the Wigner function, which is the Weyl symbol of density operator, is

W (x n , p) = ∫ dqe ixnq ⟨p + q/2|Ψ⟩ ⟨Ψ|p -q/2⟩ (22)
hence

⟨Ψ| Â |Ψ⟩ = ∑ xn ∫ dp 2π A W (x n , p)W (x n , p) (23)

B. Moyal product

Let us consider the Weyl symbol of the product of two operators  and B:

(AB) W (x n , p) = ∫ dqdke ixn(q+k) ⟨ p + q 2 + k 2 Â p - q 2 + k 2 ⟩ ⟨ p - q 2 + k 2 B p - q 2 - k 2 ⟩ = [∫ dqe ixnq ⟨ p + q 2 Â p - q 2 ⟩ ] e k 2 ← - ∂p-q 2 -→ ∂p [∫ dke ixnk ⟨ p + k 2 B p - k 2 ⟩] = [∫ dqe ixnq ⟨ p + q 2 Â p - q 2 ⟩ ] e i 2 ( - ← - ∂p - → ∂ xn + ← - ∂ xn -→ ∂p ) [∫ dke ixnk ⟨ p + k 2 B p - k 2 ⟩] (24)
Hence, the Moyal product may be defined as in the case of continuous space

(AB) W (x n , p) = A W (x n , p)e i 2 ( ← - ∂ xn -→ ∂p- ← - ∂p - → ∂ xn ) B W (x n , p) (25)
Notice, that Eqs. ( 21) and ( 22) define the Weyl symbol of operator  and the Wigner function as the functions of the continuous variable x n although the original coordinate space is discrete. This formal definition allows to use Eq. ( 25) with the derivative with respect to x n .

As it was mentioned above, all considered expressions may be easily extended to the case of the D -dimensional system with the compact momentum space of arbitrary form. Then we assume that the integration measure over momentum space is normalized in such a way, that

∫ dp = (2π) D
while the states |x n ⟩ are defined in such a way that ⟨x n | x m ⟩ = δ nm . With this normalization the definitions of the Weyl symbol of operator and the Wigner function as well as the definition of Moyal product remain the same. At the same time for the average of operator  with respect to the given quantum state we have

⟨Ψ| Â |Ψ⟩ = ∑ xn ∫ dp (2π) D A W (x n , p)W (x n , p) (26)
For the mixed states given by the density matrix ρ = ∑ i |Ψ i ⟩ ρ i ⟨Ψ i | we have the Wigner function of the form

W (x, p) = ρ W (x, p) = ∫ dqe iqx ∑ i ⟨p + q/2|Ψ i ⟩ ρ i ⟨Ψ i |p -q/2⟩ (27)
Again, the vacuum average of operator  with respect to this mixed state may be written as

⟨ Â⟩ = ∫ dxdp (2π) D A W (x, p)W (x, p) (28)

IV. WILSON FERMIONS AND PEIERLS SUBSTITUTION

A. Free Wilson fermions

Let us consider the partition function for the lattice model with Wilson fermions written in the discrete coordinate space:

Z = ∫ D ΨDΨexp ( - ∑ rn,rm Ψ(r m ) (-iD rn,rm ) Ψ(r n ) ) (29)
Here

D x,y = - 1 2 ∑ i [ (1 + γ i )δ x+e i ,y + (1 -γ i )δ x-e i ,y ] U x,y + (m (0) + 4)δ x,y (30)
γ k are the Dirac gamma matrices, m (0) is the parameter that has the meaning of mass.

Wilson fermions in momentum space correspond to the propagator of the form

G(p) = Q-1 (p)
Here the operator Q has the form

Q(p) = ∑ k=1,2,3,4 γ k g k (p) -im(p) (31)
where

g k (p) = sin(p k ) m(p) = m (0) + 4 ∑ ν=1 (1 -cos(p ν )) (32)
The same system represents the cubic tight -binding model of certain solid state systems if momentum component p 4 is rescaled accordingly in order to represent the discretization of the imaginary time. The model may be extended in several ways to reproduce the tight -binding models for various real materials. Below we will show that coupling of this system to the electromagnetic field A(x) results in the so -called Peierls substitution p → p -A(i∂ p ). In momentum space the electromagnetic field appears as the pseudo -differential operator, in which the dependence of A on coordinate is substituted by the dependence on the operator i∂ p .

B. Wilson fermions in the presence of external Abelian gauge field

Let us consider the partition function for the lattice model with Wilson fermions in the presence of the gauge field written in discrete coordinate space:

Z = ∫ D ΨDΨexp ( - ∑ rn,rm Ψ(r m ) (-iD rn,rm ) Ψ(r n ) ) (33)
Here

D x,y = - 1 2 ∑ i [ (1 + γ i )δ x+e i ,y + (1 -γ i )δ x-e i ,y ] U x,y + (m (0) + 4)δ x,y (34)
γ k are the Dirac gamma matrices, m (0) is the parameter that has the meaning of mass, while U x,y = P e i ∫ y x dξ ξ ξA(ξ ξ ξ) [START_REF] Chernodub | Anomalous Transport Due to the Conformal Anomaly[END_REF] We restrict ourselves by the case of the U (1) gauge field A and then this parallel transporter is given by

U x,y = e i ∫ y x dξ ξ ξA(ξ ξ ξ) (36)

C. Peierls substitution

Let us denote

D rn,rm = - 1 2 ∑ i [ (1 + γ i )δ rn+ei,rm + (1 -γ i )δ rn-ei,rm ] U rn,rm + (m (0) + 4)δ x,y (37)
and

I 1 = ∑ rn,rm Ψ(r m ) (-iD rn,rm ) Ψ(r n ) (38)
Also we define

Ψ(r) = ∫ M d D p |M| e irp Ψ(p) (39)
where |M| = (2π) D is the volume of momentum space. The above expression for I 1 contains the terms proportional to ∑ rn,rm

Ψ(r m )δ rn±ei,rm e i ∫ rm rn dξ ξ ξA(ξ ξ ξ) Ψ(r n ) = ∑ rn Ψ(r n ± e i )e i ∫ rn±e i rn dξ ξ ξA(ξ ξ ξ) Ψ(r n ) = ∑ rn [∫ M d D p |M| e -i(rn±ei)p Ψ(p) ] e i ∫ rn ±e i rn dξ ξ ξA(ξ ξ ξ) [∫ M d D q |M| e irnq Ψ(q) ] = ∑ rn ∫ M d D p |M| ∫ M d D q |M| Ψ(p)e irnq e i ∫ rn ±e i rn dξ ξ ξA(ξ ξ ξ) e -i(rn±ei)p Ψ(q) = ∑ rn ∫ M d D p |M| ∫ M d D q |M| Ψ(p)e irnq exp [ -i ∫ ∓ei 0 dξe i e iξeip A(i∂ p )e -iξeip ] e -i(rn±ei)p Ψ(q) = ∫ M d D p |M| Ψ(p) exp [ -i ∫ ∓1 0 dξe iξpi A i (i∂ p )e -iξpi ] e ∓ieip Ψ(p) (40)
Here we used Eq. ( 116) from Appendix II with x = r n ± e i . Now let us apply Eq. ( 112) from the same Appendix. This gives ∑ rn,rm

Ψ(r m )δ rn±ei,rm e i ∫ rm rn dξ ξ ξA(ξ ξ ξ) Ψ(r n ) = ∫ M d D p |M| Ψ(p)e ∓iei(p-Ai(i∂p)) Ψ(p) (41)
We come to the partition function of the form

Z = ∫ D ΨDΨexp ( - ∫ d D p |M| Ψ(p)Q(p -A(i∂ p ))Ψ(p) ) ( 42
)
where Q is given by Eq. [START_REF] Zubkov | Absence of equilibrium chiral magnetic effect[END_REF]. One can see, that in momentum space the application of the external Abelian gauge field results in the Peierls substitution p → p -A(i∂ p )

V. WEYL SYMBOL FOR THE WILSON FERMIONS

A. Weyl symbols of the simplest operators

Below we will be interested in the Weyl symbols of the operators of the form of Q(p -A(i∂ p )), where A is given by Eq. [START_REF] Zubkov | Absence of equilibrium chiral magnetic effect[END_REF]. Let us start our consideration from the Weyl symbol for a general function of p

(f (p)) W (x, p) = ∫ dqe iqx ⟨p + q/2| f (p) |p -q/2⟩ = ∫ dqe iqx f (p -q/2) ⟨p + q/2|p -q/2⟩ = ∫ dqe iqx f (p -q/2)δ(q) = f (p) (43)
Weyl symbol for a general function of i∂ p is (g(i∂ p )) W (x, p) = ∫ dqe iqx ⟨p + q/2| g(i∂ p ) |p -q/2⟩ = ∫ dqe iqx ⟨p + q/2| g(i∂ p ) |y⟩ ⟨y|p -q/2⟩ dy = ∫ dqe iqx ⟨p + q/2| g(i∂ p ) |y⟩ e i(p-q/2)y (2π) 3/2 dy = ∫ dqe iqx g(y) ⟨p + q/2|y⟩ e i(p-q/2)y (2π) 3/2 dy = ∫ dqe iqx g(y) e -i(p+q/2)y (2π) 3/2 e i(p-q/2)y (2π) 3/2 dy = ∫ dq e iq(x+y) (2π) 3 g(y)dy = g(x)

(44)

Here we used the fact that i ∂ ∂p |y⟩ = y |y⟩. In these expressions for the definiteness we restricted ourselves by the case of the three -dimensional momentum space.

B. Weyl symbol of exp

( i(p k -A k e -ω ω ω∂p ) )
Operator Q for the Wilson fermions is composed of the functions of a single momentum component. Moreover, those functions are sin and cos that are given by the sum of exponents. Therefore, in order to find the Weyl symbol of Q it is enough to calculate the Weyl symbol of the exponent of the combination p k -A(p 1 , ..., p D ). We start our calculation from the consideration of

F (p, i∂ p ) = exp ( i(p k -A k e -ω ω ω∂p ) )
Let us calculate the commutator [p k , A k e -ω ω ω∂p ]:

iA k e -ω ω ω∂p ip k = i(p k -ω k )iA k e -ω ω ω∂p (45)
Therefore,

[ip k , iA k e -ω ω ω∂p ] = iω k iAe -ω ω ω∂p ( 46
)
Using the special case of BCH formula where [X, Y ] = αY , we obtain:

e X e Y = e X+ α 1-e -α Y ( 47
)
This expression is given, for example, in Eq. (1.5) of [START_REF] Suzuki | Decomposition formulas of exponential operators and Lie exponentials with some applications to quantum mechanics and statistical physics[END_REF]. The rather sophisticated derivation of this formula may be found, for example, in [START_REF] Wilcox | Exponential Operators and Parameter Differentiation in Quantum Physics[END_REF]. We present our derivation of this formula in Appendix III. Changing variables to

Y ′ ≡ α 1-e -α Y = β -1 Y , where β -1 ≡ α 1-e -α
, and [X, Y ′ ] = αY ′ , we obtain:

e X+Y ′ = e X e βY ′ ( 48
)
In case of exp

( i(p k -A k e -ω ω ω∂p ) ) with α = iω k we come to exp ( i(p k -A k e -ω ω ω∂p ) ) = e i pk exp(-iβA k e -ω ω ω∂p ) (49)
This decomposition allows to calculate the Weyl symbol of F (p, i∂ p ):

[ exp ( i(p k -A k e -ω ω ω∂p ) ) ] W = [ e i pk exp(-iβA k e -ω ω ω∂p ) ] W = ∫ dqe iqx ⟨p + q/2| e i pk exp(-iβA k e -ω ω ω∂p ) |p -q/2⟩ (50)
Next, we use that i∂ p |y⟩ = y |y⟩ and

i∂ p |p -q/2⟩ = ∫ dyi∂ p |y⟩ ⟨y|p -q/2⟩ = 1 (2π) 3/2 ∫ dyy |y⟩ e iy(p-q/2) = 1 (2π) 3/2 ∫ dy |y⟩ (-i∂ p )e iy(p-q/2)
Therefore,

e i pk exp(-iβA k e -ω ω ω∂p ) |p -q/2⟩ = e i pk ∞ ∑ n=0 (-iβA k ) n n! e -nω ω ω∂p |p -q/2⟩ = e i pk ∞ ∑ n=0 (-iβA k ) n n! |p -q/2 + nω ω ω⟩ = ∞ ∑ n=0 e i(p k -q k /2+nω k ) (-iβA k ) n n! |p -q/2 + nω ω ω⟩ ( 51
)
and come to

[ exp ( i(p k -A k e -ω ω ω∂p ) ) ] W = ∫ dqe iqx ∞ ∑ n=0 e i(p k -q k /2+nω k ) (-iβA k ) n n! ⟨p + q/2|p -q/2 + nω ω ω⟩ = ∞ ∑ n=0 e inω ω ωx e i(p k +nω k /2) (-iβA k ) n n! = e ip k ∞ ∑ n=0 e ni(ω ω ωx+ω k /2) (-iβA k ) n n! = exp [ i(p k -βA k e i(ω ω ωx+ω k /2) ) ] = exp [ i ( p k - (1 -e -iω k )e iω k /2 iω k A k e iω ω ωx ) ] =exp [ i ( p k - sin(ω k /2) ω k /2 A k e iω ω ωx ) ] (52)
C. Weyl symbol of F = exp ( i(pµ - ∑ N J=1 AJµe k J i∂p )
)

The next step is the consideration of the function

F = exp ( i(p µ - ∑ N J=1 A Jµ e k J i∂p )
)

, which appears in the series expansion for arbitrary function (Fourier or Laplace series). As above, we will be using the following relation:

iA
∑ J BJµ ) , i BIµ ] = k Iµ i BIµ (59)
As above we are able to use the special case of the BCH formula [START_REF] Suzuki | Decomposition formulas of exponential operators and Lie exponentials with some applications to quantum mechanics and statistical physics[END_REF] for [X, Y ] = αY , β = 1-e -α α e X+Y = e X e βY (60)

We come to the following representation: exp

( ip µ -i N ∑ J=1 BJµ ) = exp ( ip µ -i N -1 ∑ J=1 BJµ -i BNµ ) = exp ( ip µ -i N -1 ∑ J=1 BJµ ) exp ( -iβ N µ BNµ ) = e i pµ exp ( -i N ∑ J=1 β Jµ BJµ ) = e i pµ N ∏ J=1 e -iβJµ BJµ (61)
where

β Jµ = 1 -e -kJµ k Jµ (62) Hence, exp ( i(p µ - N ∑ J=1 A Jµ e kJ i∂p ) ) = e i pµ N ∏ J=1 exp ( -iβ Jµ A Jµ e kJ i∂p ) = e i pµ N ∏ J=1 ∞ ∑ nJ =0 (-iβ Jµ A Jµ ) nJ n J ! e nJ kJ i∂p = e i pµ ∞ ∑ n1=0 (-iβ 1µ A 1µ ) n1 n 1 ! ... ∞ ∑ n N =0 (-iβ N µ A N µ ) nN n N ! e (n1k1+...+nN kN )i∂p (63)
For imaginary values of k we obtain

⟨p ′′ | exp ( i(p µ - N ∑ J=1 A Jµ e kJ i∂p ) ) |p ′ ⟩ = ⟨p ′′ | e i pµ ∞ ∑ n1=0 (-iβ 1µ A 1µ ) n1 n 1 ! ... ∞ ∑ nN =0 (-iβ N µ A N µ ) nN n N ! e (n1k1+...+nN kN )i∂p |p ′ ⟩ = ⟨p ′′ | e i pµ ∞ ∑ n1=0 (-iβ 1µ A 1µ ) n1 n 1 ! ... ∞ ∑ nN =0 (-iβ N µ A N µ ) nN n N ! |p ′ -i(n 1 k 1 + ... + n N k N )⟩ = ⟨p ′′ | ∞ ∑ n1=0 (-iβ 1µ A 1µ ) n1 n 1 ! ... ∞ ∑ nN =0 (-iβ N µ A N µ ) nN n N ! e ip ′ µ +(n1k1µ+...+nN kNµ) |p ′ -i(n 1 k 1 + ... + n N k N )⟩ = ∞ ∑ n1=0 (-iβ 1µ A 1µ ) n1 n 1 ! ... ∞ ∑ nN =0 (-iβ N µ A N µ ) nN n N ! e ip ′ µ +(n1k1µ+...+nN kNµ) δ [ (p ′′ -p ′ ) + i(n 1 k 1 + ... + n N k N ) ] (64)
The last expression allows to calculate the Weyl symbol of F :

[ exp ( i(p µ - N ∑ J=1 A Jµ e kJ i∂p ) ) ] W = ∫ dqe iqx ⟨p + q/2| exp ( i(p µ - N ∑ J=1 A Jµ e kJ i∂p ) ) |p -q/2⟩ = ∫ dqe iqx ∞ ∑ n1=0 (-iβ 1µ A 1µ ) n1 n 1 ! ... ∞ ∑ nN =0 (-iβ N µ A N µ ) nN n N ! e i(pµ-qµ/2)+(n1k1µ+...+nN kNµ) δ [ q + i(n 1 k 1 + ... + n N k N ) ] = ∞ ∑ n1=0 (-iβ 1µ A 1µ ) n1 n 1 ! ... ∞ ∑ nN =0 (-iβ N µ A N µ ) nN n N ! e (n1k1+...+nN kN )x e ipµ+ 1 2 (n1k1µ+...+nN kNµ) = exp [ i ( p µ - N ∑ J=1 β Jµ e k Jµ /2 A Jµ e k J x ) ] (65)
defining

a(k Jµ ) ≡ β Jµ e kJµ/2 = 1 -e -kJµ k Jµ e kJµ/2 = sinh(k Jµ /2) k Jµ /2 (66)
we come to

[ exp ( i(p µ - N ∑ J=1 A Jµ e kJ i∂p ) ) ] W = exp [ i ( p µ - N ∑ J=1 a(k Jµ )A Jµ e kJ x ) ] (67)
This representation has been derived for the imaginary values of k. However, it may be extended to any complex values of k by analytical continuation.

D. Weyl symbol of F = exp [ i(pµ -Aµ(i∂p)) ]

For the case of arbitrary function A µ (i∂ p ) the Weyl symbol of

F = exp [ i(p µ -A µ (i∂ p ))
] may be calculated using the above obtained expressions. We should represent A in the form of the Laplace transformation:

A µ (x) = ∫ ( õ (k)e kx + c.c. ) dk (68) that is A µ (i∂ p ) = ∫ ( õ (k)e ki∂p + c.c. ) dk (69)
In turn, this integral may be discretized and represented in the form of the series. As a result the Weyl symbol is given by [ exp

( ip µ -i ∫ [ õ (k)e ki∂p + c.c. ] dk
)] W = exp ( ip µ -iA µ (x) ) (70)
where

A µ (x) = ∫ [ a µ (k) õ (k)e kx + c.c. ] dk and a µ (k) = 1 -e -kµ k µ e kµ/2 = sinh(k µ /2) k µ /2 (71) E. Weyl symbol of Wilson Dirac operator Q(p -A(i∂p))
Now we are in the position to calculate the Weyl symbol of operator Q for the Wilson fermions in the presence of arbitrary electromagnetic field A(x). For the operator

Q(p) = ∑ k=1,2,3,4 γ k g k (p) -im(p) (72) with g k (p) = sin(p k ) m(p) = m (0) + 4 ∑ ν=1 (1 -cos(p ν )) ( 73
)
we obtain

[ Q(p -A(i∂ p )) ] W = ∑ k=1,2,3,4 γ k sin(p k -A k (x)) -i(m (0) + 4 ∑ ν=1 (1 -cos(p ν -A ν (x)))) ( 74
)
where A is the following transformation of electromagnetic field:

A µ (x) = ∫ [ sin(k µ /2) k µ /2 õ (k)e ikx + c.c. ] dk ( 75
)
while the original electromagnetic field had the form:

A µ (x) = ∫ [ õ (k)e ikx + c.c. ] dk

VI. PROPAGATOR OF FERMIONIC QUASIPARTICLES IN THE PRESENCE OF EXTERNAL ELECTROMAGNETIC FIELD

A. Wigner transformation of the two point Green function

Let us consider the cubic tight -binding model of Wilson fermions. The two point Green function G(p 1 , p 2 ) obeys equation

Q(p -A(i∂ p )))G(p, q) = δ(p -q)
The Wigner transformation of G is defined as

G W (x n , p) ≡ ∫ dqe ixnq G(p + q/2, p -q/2) (76)
It obeys the Groenewold equation

G W (x n , p) ⋆ Q W (x n , p) = 1 (77)

B. Iterative solution of the Groenewold equation

The Gronewold equation has the explicit form

1 = G W (x n , p) ⋆ Q W (x n , p) = G W (x n , p)e i 2 ( ← - ∂ xn -→ ∂p- ← - ∂p - → ∂ xn ) Q W (x n , p) (78)
Let us introduce the following notation

← → ∆ = i 2 ( ← - ∂ xn -→ ∂ p - ← - ∂ p -→ ∂ xn )
Notice, that the action of this symbol on

Q W (x n , p) = Q(p -A(x n )) is given by Q -1 (p -A(x n )) ← → ∆ Q(p -A(x n )) = -Q -1 (p -A(x n )) i 2 ← - ∂ pj F jk (x n ) -→ ∂ p k Q(p -A(x n ))
where F ij is composed of the transformed gauge potential A of Eq. ( 75) in the way similar to the field strength:

F ij = ∂ i A j -∂ j A i
Let us represent G W (x n , p) as the series

G W (x n , p) = G (0) W (x n , p) + G (1) W (x n , p) + G (2)
W (x n , p) + ... where the term G (i) W (x n , p) has the order i in powers of the derivatives of A with respect to x n . We come to the following series of equations

1 =G (0) W (x n , p)Q W (x n , p) 1 =G (0) W (x n , p)Q W (x n , p) + G (0) W (x n , p) ← → ∆ Q W (x n , p) + G (1) W (x n , p)Q W (x n , p) 1 =G (0) W (x n , p)Q W (x n , p) + G (0) W (x n , p) ← → ∆ Q W (x n , p) + 1 2 G (0) W (x n , p) ← → ∆ 2 Q W (x n , p) + G (1) W (x n , p)Q W (x n , p) + G (1) W (x n , p) ← → ∆ Q W (x n , p) + G (2) W (x n , p)Q W (x n , p) ... 1 = ∑ i,k=0...n; i+k≤n 1 k! G (i) W (x n , p) ← → ∆ k Q W (x n , p) (79)
From this sequence we obtain

G (0) W (x n , p) =Q -1 W (x n , p) G (1) W (x n , p) = - [ Q -1 W (x n , p)) ← → ∆ Q W (x n , p) ] Q -1 W (x n , p) G (2) W (x n , p) = - [ 1 2 G (0) W (x n , p) ← → ∆ 2 Q W (x n , p) + G (1) W (x n , p) ← → ∆ Q W (x n , p) ] Q -1 W (x n , p) ... G (n) W (x n , p) = - ∑ k=0...n-1 1 (n -k)! [ G (k) W (x n , p) ← → ∆ k Q W (x n , p) ] Q -1 W (x n , p) (80)
In the other words

G (0) W (x n , p) =Q -1 W (x n , p) G (1) W (x n , p) = - [ Q -1 W (x n , p)) ← → ∆ Q W (x n , p) ] Q -1 W (x n , p) G (2) W (x n , p) = - [ 1 2 Q -1 W (x n , p) ← → ∆ 2 Q W (x n , p) - [ Q -1 W (x n , p)) ← → ∆ Q W (x n , p) ] Q -1 W (x n , p) ← → ∆ Q W (x n , p) ] Q -1 W (x n , p) ... G (n) W (x n , p) = - ∑ k=0...n-1 1 (n -k)! [ G (k) W (x n , p) ← → ∆ n-k Q W (x n , p) ] Q -1 W (x n , p) (81)

C. The final form of the iterative solution

We represent the results of this iterative solution as follows:

G W (x n , p) = ∑ k G (k) W (x n , p) G (n) W (x n , p) = ∑ ∑ i=1...M ki=n C n k1k2...k M [ ... [ Q -1 W ← → ∆ k1 Q W ] Q -1 W ← → ∆ k2 Q W ] Q -1 W ... ← → ∆ kM Q W ] Q -1 W (82)
Let us substitute this expression to Eq. (81):

G (n) W (x n , p) = - ∑ m=0...n-1 1 (n -m)! ∑ ∑ i=1...M ki=m C m k1k2...kM [ ... [ Q -1 W ← → ∆ k1 Q W ] Q -1 W ← → ∆ k2 Q W ] Q -1 W ... ← → ∆ kM Q W ] Q -1 W ← → ∆ n-m Q W ] Q -1 W (83)
Constants C n k1k2...kM satisfy the following equations, that determine them iteratively:

C 0 0 = 1 C k1+...+k M +k M +1 k1k2...kM kM+1 = - 1 k M +1 ! C k1+...+k M k1k2...kM (84)
We obtain:

C 0 0 = 1 C 1 1 = -1 C 2 2 = - 1 2 , C 2 1,1 = 1 C 3 3 = - 1 3! , C 3 12 = 1 2 , C 3 2,1 = 1 2 , C 3 1,1,1 = -1 C 4 4 = - 1 4! , C 4 13 = 1 3! , C 4 2,2 = 1 4 , C 4 1,1,2 = -1/2, C 4 3,1 = 1 3! , C 4 1,2,1 = - 1 2 , C 4 2,1,1 = - 1 2 , C 4 1,1,1,1 = 1 C 5 5 = - 1 5! , C 5 1,4 = - 1 4! ( - 1 1! ) , C 5 2,3 = - 1 3! ( - 1 2! ) , C 5 1,1,3 = - 1 3! ( - 1 1! )( - 1 1! ) , C 5 3,2 = - 1 2! ( - 1 3! ) , C 5 1,2,2 = - 1 2! ( - 1 2! ) , C 3 2,1,2 = - 1 2! ( - 1 1! )( - 1 2! ) , C 3 1,1,1,2 = - 1 2! ( - 1 1! )( - 1 1! )( - 1 1! ) , C 5 4,1 = ( - 1 1! )( - 1 4!
) , C

) , C

) , C

) ,

C 5 3,1,1 = ( - 1 1! )( - 1 1! )( - 1 3! ) , C 5 1,2,1,1 = ( - 1 1! )( - 1 1! )( - 1 2! )( - 1 1! ) , C 5 2,1,1,1 = ( - 1 1! )( - 1 1! )( - 1 1! )( - 1 2! ) , C 5 1,1,1,1,1 = ( - 1 1! )( - 1 1! )( - 1 1! )( - 1 1! )( - 1 1! ) ... C k1+...+kM k1k2...k M = (-1) M k 1 !k 2 !...k M ! ...
(85) We obtain the final form of the solution:

G W (x n , p) =Q -1 W + ∑ n=1...∞ ∑ M = 1...n k 1 + ... + k M = n k i ̸ = 0 (-1) M k 1 !k 2 !...k M ! [ ... [ Q -1 W ← → ∆ k1 Q W ] Q -1 W ← → ∆ k2 Q W ] Q -1 W ... ← → ∆ kM Q W ] Q -1 W = ∑ M =0...∞ [ ... [ Q -1 W (1 -e ← → ∆ )Q W ] Q -1 W (1 -e ← → ∆ )Q W ] ...(1 -e ← → ∆ )Q W ] Q -1 W M brackets = ∑ M =0...∞ [ ... [ Q -1 W (1 -⋆)Q W ] Q -1 W (1 -⋆)Q W ] Q -1 W ...(1 -⋆)Q W ] Q -1 W M brackets (86)
In the first row the sum may be extended to the values M = n = 0, then the first term will be equal to Q -1 W . Let us introduce the product operator •, which works as follows being combined with the star product introduced above:

A • B ⋆ C = (AB) ⋆ C, A ⋆ B • C = (A ⋆ B) • C
In the first equation ⋆ acts both on AB and on C while in the second equation it acts only on A and B. These rules allow to write the above equation in the compact way:

G W (x n , p) = ∑ M =0...∞ Q -1 W (1 -⋆)Q W • Q -1 W (1 -⋆)Q W • Q -1 W ...(1 -⋆)Q W • Q -1 W M • -products = ∑ M =0...∞ ( Q -1 W (1 -⋆)Q W • ) M Q -1 W (87)
We may write symbolically:

G W (x n , p) = ( 1 -Q -1 W (1 -⋆)Q W • ) -1 Q -1 W = ( Q -1 W ⋆ Q W • ) -1 Q -1 W ( 88
)
The last expression serves also as the alternative proof of Eq. ( 86) because we started from G W ⋆ Q W = 1. We substitute Eq. ( 89) to the star product G W ⋆ Q W and obtain

G W ⋆ Q W = ∑ M =0...∞ ( Q -1 W (1 -⋆)Q W • ) M Q -1 W ⋆ Q W = - ∑ M =0...∞ ( Q -1 W (1 -⋆)Q W • ) M Q -1 W (1 -⋆)Q W + ∑ M =0...∞ ( Q -1 W (1 -⋆)Q W • ) M = - ∑ M =1...∞ ( Q -1 W (1 -⋆)Q W • ) M + ∑ M =0...∞ ( Q -1 W (1 -⋆)Q W • ) M = ( Q -1 W (1 -⋆)Q W • ) 0 = 1 (89)

VII. SUMMARY OF OBTAINED RESULTS AND CONCLUSIONS

In this paper we develop the Wigner Weyl formalism for the model of lattice Wilson fermions. First of all we derive the expression for the Weyl symbol of the lattice Wilson Dirac operator in the presence of arbitrary electromagnetic field. It appears to be surprisingly simple:

[ Q(p -A(i∂ p )) ] W = ∑ k=1,2,3,4 γ k sin(p k -A k (x)) -i(m (0) + 4 ∑ ν=1 (1 -cos(p ν -A ν (x)))) (90)
where by A we denote the following transformation of the original electromagnetic field:

A µ (x) = ∫ [ sin(k µ /2) k µ /2 õ (k)e ikx + c.c. ] dk (91)
(The original electromagnetic field itself has the form: 90) is further used to calculate the Wilson fermion propagator in the presence of arbitrary electronagnetic field. Namely, we consider first the Wigner transformation G W of the propagator, and solve iteratively the Groenewold equation. This solution has the form:

A µ (x) = ∫ [ õ (k)e ikx + c.c. ] dk.) Eq. (
G W (x n , p) =Q -1 W + ∑ n=1...∞ ∑ M = 1...n k 1 + ... + k M = n k i ̸ = 0 (-1) M k 1 !k 2 !...k M ! [ ... [ Q -1 W ← → ∆ k1 Q W ] Q -1 W ← → ∆ k2 Q W ] Q -1 W ... ← → ∆ kM Q W ] Q -1 W = ∑ M =0...∞ [ ... [ Q -1 W (1 -e ← → ∆ )Q W ] Q -1 W (1 -e ← → ∆ )Q W ] ...(1 -e ← → ∆ )Q W ] Q -1 W M brackets (92) where ← → ∆ = i 2 ( ← - ∂ xn -→ ∂ p - ← - ∂ p - → ∂ xn
)

. The obtained solution for the Wigner transformation of the two point Green function allows to reconstruct the Green function itself. In momentum space we have:

G(p + q/2, p -q/2) = 1 (2π) D ∑ n e -ixnq G W (x n , p) (93)
while in coordinate space the propagator is given by

G(z n , y n ) = ∫ dpe i(zn-yn)p G W ( z n + y n 2 , p ) (94)
The presented scheme allows to calculate, in principle, the propagator of Wilson fermions on the background of any external electromagnetic field. It would be interesting to apply it, for example, to the calculation of the propagator in the presence of varying external magnetic field of the particular form or in the presence of the particular electromagnetic wave. But this study is out of the scope of the present paper and will be reported elsewhere.

Another interesting continuation of the presented research is the extension of the Wigner -Weyl formalism to the more complicated lattice models defined on the rectangular lattices to be used for the regularization of the continuum quantum field theory. It would be interesting, in particular, to extend the proposed formalism to the model with overlap fermions that are most suitable for the investigation of QCD in the chiral limit. We foresee certain difficulties in such an extension related to the calculation of the Weyl symbol of the overlap Dirac operator caused by the structure of the latter essentially different from that of the Wilson fermions.

The presented results also may be extended to the lattice models with the non -rectangular lattice, that will allow to calculate analytically the fermionic quasiparticle propagator in various tight -binding models of the solid state physics. Unlike the case of the overlap fermions, in this extension in many cases the general structure of operator Q remains similar to that of Eq. ( 31) with certain new basis matrices γ k instead of the Dirac matrices and with the arguments of g and m that depend on the projection of momenta to vectors of reciprocal lattice.

To conclude, in the present paper we propose the extension of the Wigner -Weyl formalism to the lattice quantum field theory with Wilson fermions. The proposed formalism gives the efficient algorithm for the calculation of the Wilson fermions propagator in the presence of arbitrary external electromagnetic field. This technique may be extended in the straightforward way to the wide range of the non -hypercubic lattice models relevant for the description of the solid state physics. Thus we expect that the proposed technique may have applications both to the quantum field theory in lattice regularization and to the solid state physics. Using the lattice Wilson fermion propagator in the presence of arbitrary external electromagnetic field this will be possible to investigate via numerical simulations, for example, various effects in quark matter in the presence of in -homogeneous external electromagnetic field. On the solid state physics side the direct applications will become possible when the similar formalism will be developed for the crystal lattice of more complicated and more realistic form. Then our formalism will allow to investigate various phenomena typical for the interaction of electronic quasiparticles with photons.

In [START_REF] Zubkov | Topology of the momentum space, Wigner transformations, and a chiral anomaly in lattice models[END_REF][START_REF] Chernodub | Scale Magnetic Effect in Quantum Electrodynamics and the Wigner-Weyl Formalism[END_REF][START_REF] Khaidukov | Chiral Separation Effect in lattice regularization[END_REF][START_REF] Zubkov | Momentum space topology of QCD[END_REF][START_REF] Zubkov | Absence of equilibrium chiral magnetic effect[END_REF][START_REF] Zubkov | Wigner transformation, momentum space topology, and anomalous transport[END_REF] the two first terms (in the expansion in powers of the derivatives) of the present solution of the Groenewold equation were calculated, which give the linear response of vector/axial currents to the external field strength. It appears that in many cases the corresponding coefficients are the topological invariants in momentum space, i.e. they are not changed when the system is changed smoothly. This gives the efficient description of certain anomalous transport phenomena (chiral magnetic effect, chiral separation effect, anomalous quantum Hall effect, scale magnetic effect, etc). Our present study generalizes the approach of [START_REF] Zubkov | Topology of the momentum space, Wigner transformations, and a chiral anomaly in lattice models[END_REF][START_REF] Chernodub | Scale Magnetic Effect in Quantum Electrodynamics and the Wigner-Weyl Formalism[END_REF][START_REF] Khaidukov | Chiral Separation Effect in lattice regularization[END_REF][START_REF] Zubkov | Momentum space topology of QCD[END_REF][START_REF] Zubkov | Absence of equilibrium chiral magnetic effect[END_REF][START_REF] Zubkov | Wigner transformation, momentum space topology, and anomalous transport[END_REF] essentially and gives the more powerful method of calculations. In the present paper we represent the complete iterative solution of the Groenewold equation (to all orders of the derivative expansion) in the presence of arbitrarily varying external electromagnetic field. It would be interesting to use this approach for the investigation of the anomalous transport in case of varying external field strength. We foresee, that the intimate relation between topology and the non -dissipative transport will survive here as well, but its description may be governed by the more complicated topological invariants.

Both authors kindly acknowledge useful discussions with Z.V.Khaidukov.

A. Continuous coordinates -continuous momenta

Fourier transform:

f (x) = 1 √ 2π ∫ ∞ -∞ dke ikx f (k) f (k) = 1 √ 2π ∫ ∞ -∞ dxe -ikx f (x) (95)
The integral representation for the delta functions

f (x) = 1 2π ∫ ∞ -∞ dke ikx ∫ ∞ -∞ dx ′ e -ikx ′ f (x ′ ) = ∫ ∞ -∞ dx ′ f (x ′ ) 1 2π ∫ ∞ -∞ dke ik(x-x ′ ) (96) hence δ(x -x ′ ) = 1 2π ∫ ∞ -∞ e ik(x-x ′ ) dk (97) and f (k) = ∫ ∞ -∞ dxe -ikx 1 2π ∫ ∞ -∞ dk ′ e ik ′ x f (k ′ ) = ∫ ∞ -∞ dk ′ f (k ′ ) 1 2π ∫ ∞ -∞ dxe -ix(k-k ′ ) (98) hence δ(k -k ′ ) = 1 2π ∫ ∞ -∞ e -ix(k-k ′ ) dx (99) B. Compact coordinates, x ∈ [0, L] -discrete momenta
Fourier series:

f (x) = ∞ ∑ n=0 e ik0nx f (k n ) k n = k 0 n k 0 = 2π L f (k n ) = 1 L ∫ L 0 dxe -iknx f (x) (100)
The representation of the delta functions through the integrals/series:

f (x) = ∞ ∑ n=0 e ik0nx 1 L ∫ L 0 dx ′ e -ik0nx ′ f (x ′ ) = ∫ L 0 dx ′ f (x ′ ) 1 L ∞ ∑ n=0 e ik0n(x-x ′ ) (101) hence δ(x -x ′ ) = 1 L ∞ ∑ n=0 e ik0n(x-x ′ ) (102)
and

f (k n ) = 1 L ∫ L 0 dxe -ik0nx ∞ ∑ m=0 e ik0mx f (k m ) = ∞ ∑ m=0 f (k m ) 1 L ∫ L 0 dxe -ik0x(n-m) (103) hence δ(k n -k m ) = 1 L ∫ L 0 dxe -ik0x(n-m) (104) C. Discrete coordinates -the compact region of momenta, k ∈ [0, 2π L ]
Fourier series:

f (k) = ∞ ∑ n=0 e -ikxn f (x n ) x n = nL f (x n ) = 1 2π/L ∫ 2π/L 0 dke ikxn f (k) (105)
The representation of the delta functions as the integrals/series:

f (k) = ∞ ∑ n=0 e -iknL L 2π ∫ 2π/L 0 dk ′ e ik ′ nL f (k ′ ) = ∫ 2π/L 0 dk ′ f (k ′ ) L 2π ∞ ∑ n=0 e -inL(k-k ′ ) (106) hence δ(k -k ′ ) = L 2π ∞ ∑ n=0 e -inL(k-k ′ ) (107)
and ) ( e ip∆ e i∆A(i∂p)

f (x n ) = L 2π ∫ 2π/L 0 dke iknL ∞ ∑ m=0 e -ikmL f (x m ) = ∞ ∑ m=0 f (x m ) L 2π
) N e -ip(x+(u2-u1)) = lim ∆→0 ( e i∆A (i∂p) ) ( e ip∆ e i∆A(i∂p)

) N -1 e ip∆ e i∆A(x+(u2-u1)) e -ip(x+(u2-u1)) = lim ∆→0 ( e i∆A (i∂p) ) ( e ip∆ e i∆A(i∂p)

) N -1 e -ip(x+(u2-u1)-∆) e i∆A(x+(u2-u1)) = lim ∆→0 ( e i∆A (i∂p) ) ( e ip∆ e i∆A(i∂p)

) N -2 e -ip(x+(u2-u1)-2∆) e i∆(A(x+(u2-u1)-∆))+A(x+(u2-u1)) = lim The Lemma will be proved if we will show, that A(t) and B(t) obey the same first order differential equation, while A(0) = B(0). The latter requirement is obvious. Let us calculate the derivatives:

∂ t A(t) = ∂ t exp(X + tY ) = ∂ t exp ( X + tY N ) N = N -1 ∑ k=0 exp ( X + tY N ) k [ ∂ t exp ( X + tY N )] exp ( X + tY N ) N -k-1 (121)
taking the limit N → ∞, one gets

∂ t exp ( X + tY N ) = Y N (122)
and the sum in this case becomes an integral

∂ t A(t) =

eee

  expression for the P ordered exponent.The path-ordering operator is defined as followsP (f (x)g(y)) ≡ θ(x -y)g(y)f (x) + θ(y -x)f (x)g(y) ∆e n∆ B Ĉe -n∆ B   e B (113)that isI = [ e ∆e 0∆ B Ĉe -0∆ B ] [ e ∆e 1∆ B Ĉe -1∆ B ] ... [ e ∆e (1-∆) B Ĉe -(1-∆) B ] [ e ∆e B Ĉe -B ] -1 Ô Â Ô-1 + ... = Ôe  Ô-1, we may rewrite I as followsI = [ e ∆ Ĉ ] [ e ∆ B e ∆ Ĉ e -∆ B ] [ e ∆ 2B e ∆ Ĉ e -∆ 2B ] ... [ e (1-∆) B e ∆ Ĉ e -(1-∆) B ] [ e B e ∆ Ĉ e - B ] e B = e ∆ Ĉ [ e ∆ B e ∆ Ĉ ] ipu A(i∂ p )e -ipu du ] e -ipx = exp   i u2-u1 ∫ 0 A(x + u)du -ipx ipn∆ e i∆A(i∂p) e -ipn∆   e -ipx = [ lim ∆→0 ( e i∆A(i∂p)) ( e ip∆ e i∆A(i∂p) e -ip∆ ) ... ( e ipN ∆ e i∆A(i∂p) e -ipN ∆

e

  X e Y = exp(X + α 1 -e -α Y ) (118) or, alternatively exp(X + Y ) = e X e βY(119)where β = 1-e -α α .ProofLet us defineA(t) = exp(X + tY ), B(t) = e X e βtY(120)

∫ 1 0 1 0e

 11 e u(X+tY ) Y e(1-u)(X+tY ) du(123) where u = k N . In the following we will use the identitye u(X+tY ) Y = Y e u(X+α+tY )(124)that follows from the obvious relation u(X + tY )Y = Y u(X + α + tY ) based on the commutation relation of X and Y . Hence,∂ t A(t) = Y e (X+tY ) ∫ uα du = Y A(t) e α -1 α (125)On the other hand, the derivative of B(t) is given by∂ t B(t) = ∂ t e X e βtY = e X βY e βtY = Y e X e βtY βe α = Y B(t) e α -1 α (126)(Here we used Eq. (124) for u = 1, t = 0.) One can see, that indeed A(t) and B(t) obey the same first order differential equation. There is only one solution of this equation that obeys the initial condition B(0) = A(0), and this proves the Lemma.

  Jµ e kJ i∂p ip µ = i(p µ + ik Jµ )iA Jµ e kJ i∂p

			(53)
	It gives
	[ip (54)
	Let us define the operator
			BJµ ≡ A Jµ e kJ i∂p	(55)
	It obeys the commutation relations
			[ BJµ , BIµ ] = 0	(56)
	and
			[ip µ , i BJµ ] = k Jµ i BJµ	(57)
	Therefore, we have
		[i(p µ -B Jµ ), iB Iµ ] = k Iµ iB Iµ	(58)
	and
	[	(
		i	pµ -

µ , iA Jµ e kJ i∂p ] = k Jµ iA Jµ e kJ i∂p

Appendix I. Fourier transform

In this Appendix we accumulate for the convenience of the reader the well -known expressions for the Fourier transform and Fourier series widely used throughout the text of the paper. For simplicity we consider the onedimensional constructions.

Appendix III. BCH formula for the particular Lie algebra

In this section we derive the particular case of the BCH formula, that corresponds to the Lie algebra of operators composed of the basis elements X, Y with the commutation relation [X, Y ] = αY . We are going to prove the following Lemma


Alexandra Goultiaeva

Yves Lespérance
email: lesperan@cse.yorku.ca

Incremental Plan Recognition in an Agent Programming Framework

Keywords: Reconnaissance de plans, raisonnement sur l'action, langages de programmation d Plan recognition, reasoning about action, agent programming languages

Dans cet article, nous proposons un modèle formel de la reconnaissance de plans en vue de l'inclure dans un formalisme de programmation d'agent. Le modèle est basé sur le calcul des situations et le langage de programmation d'agent ConGolog. Ceci fournit un langage très riche pour la spécification des plans à reconnaitre. Notre modèle supporte aussi la reconnaissance incrémentale, où l'ensemble des hypothèses de plans exécutés est filtré à mesure que les actions sont observées. Le modèle est spécifié en termes d'un système de transitions pour le langage de plans. Le modèle supporte aussi les plans structurés hiérarchiquement et reconnait les relations entre un plan et les sous-plan qu'il contient.

Introduction

The ability to recognize plans of others can be useful in a wide variety of applications, from office assistance (where a program might provide useful reminders, or give hints on how to correct a faulty plan), to monitoring and aiding astronauts, providing assistance to people with cognitive or memory problems to allow them to live independently, etc.

There has been a lot of work in the area of plan recognition; see [START_REF] Carberry | Techniques for plan recognition. User Modeling and User-Adapted Interaction[END_REF] for a recent survey. Some of this work develops symbolic techniques for identifying plans that match the observations. For instance, [START_REF] Avrahami | Fast and complete symbolic plan recognition[END_REF] uses a decision tree to match observations to plan steps and graph traversal to identify branches that represent consistent hypotheses. To deal with uncertainty and identify most likely hypotheses, some work uses probabilistic techniques; for instance [START_REF] Bui | A general model for online probabilistic plan recognition[END_REF], uses an extension of Hidden Markov Models for this. Other work combines symbolic and probabilistic approaches, e.g. [START_REF] Avrahami | Hybrid symbolicprobabilistic plan recognition: Initial stepsd[END_REF]. Many approaches (including the ones just cited) support hierarchical task network-type plans, allowing methods to have several alternative decompositions, as well as looping tasks. However, these approaches do not support concurrently executing plans.

Our approach is based on the ConGolog agent programming language [START_REF] De | ConGolog, a concurrent programming language based on the situation calculus[END_REF], which supports very rich plans, including concurrent processes. We think that developing a unified agent programming framework that supports plan recognition as well as plan synthesis and behavior specification would have a number of benefits, including ease of use, and reuse of domain specifications and reasoning methods. Our work is closely related to the plan recognition framework of [START_REF] Demolombe | What does it mean that an agent is performing a typical procedure? A formal definition in the Situation Calculus[END_REF], where plans are rep-resented as Golog 1 programs, with two additional constructs: σ, which matches any sequence of actions, and α 1 -α 2 , which matches an execution of plan α 1 as long as it does not also match an execution of α 2 . α 1 -α 2 is quite a useful and powerful construct, which allows one to specify plans in terms of what must not happen in addition to what can happen. This cannot be done in most other plan recognition frameworks.

In this paper, we provide an alternative formalization and implementation of the plan recognition framework of [START_REF] Demolombe | What does it mean that an agent is performing a typical procedure? A formal definition in the Situation Calculus[END_REF]. Plans are represented as procedures, which may include calls to other procedures. Because of this, the plan recognition framework provides additional information, such as the call hierarchy, which details the procedures that are in progress or have completed, which procedure called which, and what remains to execute.

Another major difference between our approach and that of [START_REF] Demolombe | What does it mean that an agent is performing a typical procedure? A formal definition in the Situation Calculus[END_REF] is that we support incremental plan recognition. Given a set of hypotheses about what plans may be executing and a new observed action, our formalization defines what the revised set of hypotheses should be. Plan recognition is specified in terms of a structural operational semantics (single-step transitions) in the style of [START_REF] Plotkin | A structural approach to operational semantics[END_REF] for the plan specification language. [START_REF] Demolombe | What does it mean that an agent is performing a typical procedure? A formal definition in the Situation Calculus[END_REF] used a different semantics where programs were mapped into complete executions.

We have implemented a plan recognition system based on this formalization. It can be executed "on-line" and constantly keeps track of what plans may be executing, without having to recalculate them for each new observed action. Focusing on procedures rather than complete plans allows plans to be hierarchical and modular, and the result of the recognition is more informative and meaningful.

In the rest of the paper, we first give an overview of the Situation Calculus and ConGolog, and then present our formal model of plan recognition. Then, we give some examples to illustrate how the framework is used. Following this, we briefly describe our implementation of the model. We conclude the paper with a discussion of the novel features and limitations of our account, and provide suggestions for future work.

The Situation Calculus and ConGolog

The technical machinery that we use to define high-level program execution is based on that of [START_REF] De | ConGolog, a concurrent programming language based on the situation calculus[END_REF]. The starting point in the definition is the situation calculus [START_REF] Mccarthy | Some philosophical problems from the standpoint of artificial intellig ence[END_REF]. We will not go over the language here except to note the following components: there is a special constant S 0 used to denote the initial situation; there is a distinguished binary function symbol do where do(a, s) denotes the successor situation to s resulting from performing the action a; relations whose truth values vary from situation to situation, are called (relational) fluents, and are denoted by predicate symbols taking a situation term as their last argument. There is a special predicate P oss(a, s) used to state that action a is executable in situation s.

Within this language, we can formulate domain theories which describe how the world changes as a result of the available actions. Here, we use action theories of the following form:

• Axioms describing the initial situation, S 0 .

• Action precondition axioms, one for each primitive action a, characterizing P oss(a, s).

• Successor state axioms, one for each fluent F , which characterize the conditions under which F ( x, do(a, s))

holds in terms of what holds in situation s; these axioms may be compiled from effects axioms, but provide a solution to the frame problem [START_REF] Reiter | The frame problem in the situation calculus: A simple solution (sometimes) and a completeness result for goal regression[END_REF].

• Unique names axioms for the primitive actions.

• A set of foundational, domain independent axioms for situations Σ as in [START_REF] Reiter | Knowledge in Action: Logical Foundations for Specifying and Implementing Dynamical Systems[END_REF].

Next we turn to programs. The programs we consider here are based on the Con-Golog language defined in [START_REF] De | ConGolog, a concurrent programming language based on the situation calculus[END_REF] In [START_REF] De | ConGolog, a concurrent programming language based on the situation calculus[END_REF], a single step transition semantics in the style of [START_REF] Plotkin | A structural approach to operational semantics[END_REF]

Formalizing plan recognition

Recognizing a plan means that given a sequence of observed actions, the system must be able to determine which plan(s) the user may be following. The framework described here relies on a plan library, which details the possible plans as procedures in ConGolog. Given the sequence of actions performed, the system should be able to provide the following information: the plan that the user is currently following; the stage in the plan that the user is following -what has already been done and what remains to be done; and which procedures that plan is part ofis the user doing it as part of a larger plan?

The framework is specified in terms of ConGolog, to which a few extensions are made. Note that what is described below could have alternatively been done by modifying the semantics of the language.

The following formalization is designed to build on top of the existing framework as much as possible.

First, we introduce two special primitive actions: startP roc(name(args)) and endP roc(name(args)). These are annotation actions, present only in the plan library, but never actually observed.

The two actions are used to represent procedure invocation and completion. It is assumed that every procedure that we want to distinguish in the plan library starts with the action startP roc(name(args)) and ends with the action endP roc(name(args)), where name is the name of the procedure in which the actions occur, and args are its arguments. This markup can be generated automatically given a plan library.

Our transition system semantics for plans fully supports concurrency. Environments involving multiple agents can also be dealt with if we assume that the agent of each action is specified (say as a distinguished parameter of the action). However, if there is concurrency over different procedures run by the same agent, the annotated situation as currently defined is not generally sufficient to determine which thread/procedure an observed action belongs to. Additional annotations will need to be introduced to specify this. We leave this for future work.

After the inclusion of the annotation actions, for each sequence of actions there are two situations: the real (observed) situation, and the annotated situation, which includes the actions startP roc and endP roc. Given the annotated situation, it is straightforward to obtain the state of the execution stack (which procedures are currently executing), determine what actions were executed by which procedures, and determine the remaining plan. An action startP roc(proc) means that the procedure proc was called, and should be added to the stack. The action endP roc(proc) signals that the last procedure has terminated, and should be removed from the stack. Note that for a given real situation, there may be multiple annotated situations that would match it. Each of those situations would show a different possible execution path in the plan library. For example, if the plan library contained the following procedures:

proc p1 startP roc(p1); a; b; endP roc(p1) endProc proc p2 startP roc(p2); a; c; endP roc(p2) endProc then the real situation do(a, S 0 ) would have two possible annotated situations that would match it:

do(a, do(startP roc(p1), S 0 )) and do(a, do(startP roc(p2), S 0 )).

In this context, the plan recognition problem reduces to the following: given the observed situation and a plan library, find the possible annotated situations.

The first two predicates defined for the new formalism are aT rans and rT rans. The predicate aT rans is a form of T rans that allows only a transition step that cannot be observed: either an annotation action or a test/wait action. The predicate rT rans is a form of T rans which only allows observable actions. The helper predicate Annt is true if and only if the action passed to it is an annotation action:

Annt(a) def = ∃n . a = startP roc(n) ∨ ∃n . a = endP roc(n) aT rans(δ, s, δ , s ) def = T rans(δ, s, δ , s ) ∧ (∃a . (s = do(a, s) ∧ Annt(a)) ∨ s = s) rT rans(δ, s, δ , s ) def = T rans(δ, s, δ , s ) ∧ ∃a . s = do(a, s) ∧ ¬Annt(a)
We also define aT rans * as the reflexive transitive closure of aT rans.

The transition predicate nT rans(δ, s r , s a , δ , s r , s a ) is the main predicate in our plan recognition framework. It holds when δ is the program remaining from δ after performing any number of annotation actions or tests, followed by an observable action. Situation s r is the real situation before performing those steps, and s r is the real situation after. Situation s a is the annotated situation (which reflects the annotations as well as the real actions) before the program steps, and s a is the annotated situation after. Effectively, our definition below amounts to nT rans being equivalent to aT rans * composed with rT rans: nT rans(δ, s r , s a , δ , s r , s a ) def = ∃δ , s a , a.aT rans * (δ, s a , δ , s a ) ∧ rT rans(δ , s r , δ , do(a, s r ))

∧ s r = do(a, s r ) ∧ s a = do(a, s a ).
Just as nT rans is the counterpart to T rans which deals with annotation actions, nF inal is the counterpart to F inal, which allows any number of annotation actions or tests to be performed:

nF inal(δ, s) def = ∃δ , s . aT rans * (δ, s, δ , s ) ∧ F inal(δ , s )
As mentioned in [START_REF] Demolombe | What does it mean that an agent is performing a typical procedure? A formal definition in the Situation Calculus[END_REF], in many cases it would be useful for the procedures to leave some actions unspecified, or to place additional constraints on the plans. So they introduced two new constructs. The first is anyBut(actionList), which allows one to execute an arbitrary primitive action which is not in its argument list. For example, anyBut ([b, d]) would match actions a or c, but not b or d. It is a useful shorthand for writing general plans which might involve unspecified steps. For example, a plan might specify that a certain condition needs to hold for its continuation, but leave unspecified what action(s) was performed to achieve the condition. It is simply an abbreviation, included for convenience. Another shorthand construct, any, can be defined to match any action without exceptions. We can define these as follows:

2 anyBut([a 1 , ..., a n ]) def = πa.(if(a = a 1 ∧ ... ∧ a = a n ) then a else F alse?endIf) any def = anyBut([])
The second construct is minus(δ, δ). This matches any execution that would match δ, as long as it does not match δ. This construct allows the plan to place additional constraints on the sequences of actions that would be recognized within a certain procedure. For example, the procedure that corresponds to a task of cleaning the house could include unspecified parts, and would match many different sequences of actions, but not if they involve brushing teeth. Assuming cleanUp and brushT eeth are procedures in the plan library, then it is possible to specify the above as minus(cleanUp, brushT eeth).

To define this construct, we need to define what a step of execution for this construct is, and the remaining program. Also, note that δ must match all observable actions performed by δ, but might do different annotation and test actions; those differences should be ignored.

An additional axiom is added to specify T rans for the minus construct:

T rans(minus(δ, δ), s, δ , s ) ≡ ∃δ .aT rans(δ, s, δ , s ) ∧ δ = minus(δ , δ) ∨ ∃δ , a.rT rans(δ, s, δ , do(a, s)) ∧ s = do(a, s) ∧ (¬∃ δ s s i .nT rans ( δ, s, s, δ , do(a, s ), Note that whether T rans holds for minus(δ, δ) depends on whether nT rans holds for δ and the latter depends on aT rans * and ultimately T rans, so the definition might not appear to be well founded. We ensure that it is well founded by imposing the restriction that no minus can appear in the second argument δ of a minus. So in the axiom, we use nT rans which is defined just like nT rans, except that it is based on a version of T rans, T rans , that does not support the minus construct and does not include the T rans axiom for the minus construct. So T rans is just the existing T rans from [START_REF] De | ConGolog, a concurrent programming language based on the situation calculus[END_REF], which is well defined, and nT rans is defined in terms of it. Then we can define the new T rans that supports minus in terms of nT rans and we have a well founded definition. The same approach is used to define F inal for minus. The construct minus is considered finished when δ is finished, but δ is not:

s i ) ∧ δ = δ ∨ ∃ δ s s i .nT rans ( δ, s, s, δ , do(a, s ), s i ) ∧ ¬nF inal ( δ , do(a, s )) ∧ δ = minus(δ , δ )).
F inal(minus(δ, δ), s) ≡ F inal(δ, s) ∧ ¬nF inal ( δ, s).
We use C to denote the extended Con-Golog axioms: C together with the above two. Note that recursive procedures can be as in [START_REF] De | ConGolog, a concurrent programming language based on the situation calculus[END_REF].

The above definition relies on a condition imposed on the δ that may appear as second argument in a minus: for any sequence of transitions involving the same actions, δ should have only one possible remaining program. More formally:

T rans * ( δ, s, δ1 , s 1 ) ∧ T rans( δ1 , s 1 , δ , do(a 1 , s 1 )) ∧ T rans * ( δ, s, δ2 , s 2 ) ∧ T rans( δ2 , s 2 , δ , do(a 2 , s 2 )) ∧ do(a 1 , s 1 ) = do(a 2 , s 2 ) ⊃ δ = δ
This restriction seems quite natural because δ is a model of what is not allowed. Based on the above definition, to get the annotated situation from an observable one, we only need to apply nT rans a number of times, until the observable situation is reached. We define nT rans * as the reflexive transitive closure of nT rans. The predicate allT rans(s r , s a , δ rem ) means that s a denotes a possible annotated situation that matches the observed situation s r , and δ rem is the remaining plan: allT rans(s r , s a , δ rem ) def = nT rans * (planLibrary, S 0 , S 0 , δ rem , s r , s a )

where S 0 is the initial situation and planLibrary is a procedure that represents the plan library.

The set of all the remaining programs δ and their corresponding annotated situations S a for a given real situation S can be defined as follows:

allP lans(S) def = {(δ, S a )| D ∪ C | = allT rans(S, S a , δ)}
where D is the action theory for the domain.

As mentioned earlier, our account also allows incremental calculation of the set of plans that the agent may be executing. If (δ , S a ) ∈ allP lans(S) and D ∪ C | = nT rans(δ , S, S a , δ, do(A, S), S a ), then (δ, S a ) ∈ allP lans(do(A, S)). The converse is also true under some conditions that typically hold.

Examples

The main example described here is a simulation of activities in a home. There are four rooms: the bedroom, kitchen, living room, and bathroom. There are also four objects: the toothbrush, book, spoon, and cup. Each object has its own place, where it should be located. The toothbrush should be in the bathroom, the book in the living room, and the spoon and cup in the kitchen.

Initially, all objects are where they are supposed to be, except for two: the book is in the kitchen, and the toothbrush is in the living room. The location of the monitored agent is originally in the bedroom.

There are four possible primitive actions:

• goT o(room): changes the location of the agent to be room;

• pickUp(object): only possible if the agent is in the same room as the object; this causes the object to be held;

• putDown(object): only possible if the agent holds the object; puts the object down;

• use(object): only possible if the agent holds the object.

We use the following fluents:

• loc: the room in which the agent is;

• loc(thing): the room in which the thing is;

• Hold(thing): true if the agent holds the thing, false otherwise.

We also use the following non-fluent predicates:

• Room(r): r is a room;

• Object(t): t is an object;

• InP lace(thing, room): holds if thing is in its place when it is in room.

There are five procedures in the plan library:

• get(thing): go to the room where thing is, and pick it up;

• putAway(thing): go to the room where the thing should be, and put it down;

• cleanUp: while there are objects that are not in their places, get such an object, or put it away;

• brushT eeth: get the toothbrush, use the toothbrush, and either put away the toothbrush, or put it down (where the agent is);

• readBook: get the book, use the book, and either put away the book, or put it down.

The procedures are defined below. We also use the following procedure: Procedures brushT eeth and readBook have options: either the agent might put the thing away in its place, or it might put the thing down wherever it happens to be. In practice, a person might do either, and both executions should be recognized as part of the procedure.

proc getT o(
Perhaps the most complex procedure in this example is cleanUp. The main idea is that when executing this procedure, the agent will, at each iteration, get a thing that is not in its proper place, or put away something it already holds. The main plan library chooses some procedure to execute nondeterministically and repeats this zero or more times: proc planLibrary (cleanUp|brushT eeth| readBook|(πt.get(t))) * . endProc Let's look at an execution trace for the above example. Suppose that the first action was goT o(kitchen). The following possible scenarios are then output by the system: proc get(book) -> goTo(kitchen) proc get(cup) -> goTo(kitchen) proc get(spoon) -> goTo(kitchen) proc readBook -> proc get(book) -> goTo(kitchen) proc cleanUp -> proc get(book) -> goTo(kitchen)

The system is trying to guess what the user is doing by going to the kitchen. It lists the five plans from the library that might have this first action. Note that the possibilities of doing cleanUp by getting a cup or a spoon are not listed. This is because both the spoon and cup are already in their places, so if the agent picked them up, it would not be cleaning up. Now suppose that the next action is pickUp(book). Then, the system can discard some of the above possibilities, namely those which involve taking something else. The new possible scenarios are: The above examples are kept simple to illustrate how the various constructs work. The system was tested on both of the above examples, and more complicated ones. All of the above traces were generated by the implementation.

Implementation and Experimentation

Our plan recognition system was implemented using a Prolog-based version of In-diGolog, an extension of ConGolog introduced in [START_REF] De | An incremental interpreter for high-level programs with sensing[END_REF]. The implementation closely follows the definitions, without any optimization for performance. The implementation assumes that the axioms specifying the initial situation are represented as Prolog clauses and makes the closed world assumption.

The system uses a user-defined domain specification and plan library. All procedures in the library need to satisfy some restrictions. Each procedure P that is to be reflected in the scenario has to start and end with actions startP roc(P ) and endP roc(P ), respectively. The procedures can also use constructs anyBut and minus.

The implementation can be used in interactive mode. Then the user is expected to enter the observed actions one by one. Also, at any point the user can issue one of the following commands: prompt -list all current hypotheses, reset -forget the previous actions and start fresh, and exitfinish execution.

We ran some experiments on the home activities domain discussed above, with a slight modification: the last option in the plan library is now (πt.[get(t), putDown(t)]) instead of (πt.get(t)). This was done ensure that there are arbirarily long executions of the plan library. For each n, where n is the length of an observed action sequence, we randomly selected 200 sequences of n actions that could be generated by the plan library. We then ran the plan recognition system on all of those and averaged the running time. The results appear in Figure 1. We can see that our system can identify matching plans for a sequence of 80 observed actions in less than one second on average in this test domain. As well, for this domain the running time seems to grow linearly with the length of the observed action sequence. In this paper, we have described a framework for plan recognition in the Situation Calculus. The ConGolog programming language is used to specify plans. The system matches the actions of the monitored agent against the plan library and returns some scenarios, representing the execution paths that the agent may have followed.

The main differences between our account of plan recognition and the one described by [START_REF] Demolombe | What does it mean that an agent is performing a typical procedure? A formal definition in the Situation Calculus[END_REF] are that ours is able to model procedure calls within plans and that it is incremental. Because our approach to plan recognition concentrates on procedures, it is able to distinguish sub-procedures from each other as well as from top-level plans. This allows the scenarios to be fairly detailed both as to how and why a certain plan was being executed.

Because our formalism is incremental, it does not need to know the whole sequence of actions to interpret the next step; nor does it need to re-compute matching scenarios from scratch whenever a new action is made. It would be well-suited for real-time applications or continuous monitoring.

The framework described here is easily extended with new annotations to specify, for example, the goals and preconditions of each plan and/or possible reactions to it by the monitoring system. As mentioned earlier, to fully support the recognition of concurrent executions of plans, additional annotations to track which process performed each action should be introduced.

Another possible extension would be to assign probabilities to actions and plans, similarly to what was done in [START_REF] Demolombe | Intention recognition in the Situation Calculus and Probability Theory frameworks[END_REF]. This would make it possible to rank the possible execution hypotheses, select the most probable ones and use this to predict which actions the agent is more likely to execute next. One could also look at qualitative mechanisms for doing this. More experimental evaluation of our system is also needed.

There has already been work on home care applications for a plan recognition system. For example, [START_REF] Lin | IPARS: Intelligent portable activity recognition system via everyday objects, human movements, and activity duration[END_REF] describes a plan recognition system that includes strategies for monitoring and obtaining actions, as well as using learning to modify the plan libraries. Both of those techniques can potentially work with our system.

Figure 1 :

 1 Figure 1: Average runtime (seconds) versus the length of the action sequence

  This says the following: if the next step of the plan δ is not an observable action, then the remaining program is what remains of δ minus δ; if δ performs an observable action, and δ cannot match that action, then the remaining program is what remains of δ; if δ can match the observable action performed by δ but it is not final, then the remaining program is what remains of δ minus what remains of δ.

  checks if the current location is already the destination room r. If not, the action goT o is executed. It is a helper procedure, which was only introduced for convenience, and was not deemed important enough to appear in the annotations. Hence, it does not have startP roc and endP roc actions. So, when the program is executed, the procedure getT o will not appear in the stack.

	r) Room(r)?; if loc = r then goT o(r) endIf endProc getT o The definition of most of the other proce-dures is straightforward: proc get(t) startP roc(get(t)); ¬Hold(t)?; getT o(loc(t)); pickUp(t); endP roc(get(t)) endProc; proc putAway(t) startP roc(putAway(t)); Hold(t)?; π r.InP lace(t, r)?; getT o(r); putDown(t); endP roc(putAway(t)) endProc; proc brushT eeth startP roc(brushT eeth); get(toothbrush); use(toothbrush); (putAway(toothbrush)| putDown(toothbrush)); endP roc(brushT eeth) endProc; proc readBook startP roc(readBook); get(book); use(book); (putAway(book)|putDown(book)); endP roc(readBook) endProc;

  then cleanUp u matches it. However, cleanUp m does not. That is because cleanUp m has the minus construct, and the observed actions matched the exception part of it. The action putDown(toothbrush) can be considered the last action of brushT eeth, which was ruled out by the minus in cleanUp m . So, cleanUp m cannot match this sequence of actions. cleanUp u , which is identical to cleanUp m except for the minus construct, does match the action, and produces the following scenario:

	proc get(book) -> goTo(kitchen); pickUp(book) proc readBook -> get(book) -> goTo(kitchen); pickUp(book) proc cleanUp -> proc get(book) -> goTo(kitchen); pickUp(book) The next action is use(book). The plan get(book) is finished, but there is no plan in the library that could start with the ac-tion use(book). So, this possibility can be discarded. The next action of cleanUp cannot match the observed actions as well. Thus the only remaining possible plan is readBook: proc readBook -> proc get(book) -> goTo(kitchen); pickUp(book); use(book) Now, let us consider a different scenario. In order to demonstrate the use of the minus and anyBut constructs, we can de-fine two variants of cleanUp. In the first one, cleanUp u , an arbitrary action is al-lowed at the end of every iteration of the loop. The second one, cleanUp m , together with the optional arbitrary action, intro-duces a constraint: a sequence of actions will not be matched if it involves the exe-cution of procedure brushT eeth. This is achieved by using the minus construct. proc cleanUp u startP roc(cleanUp u ); while ∃t.Object(t) ∧ ¬InP lace(t, loc(t)) do π t.Object(t) ∧ ¬InP lace(t, loc(t))?; (get(t)|putAway(t)); (any|nil) endProc endP roc(cleanUp u )]) endWhile; Now, if the next step is putDown(toothbrush), proc cleanUp_u -> proc get(toothbrush) -> goTo(livingRoom); pickUp(toothbrush); use(toothbrush); proc putAway(toothbrush) -> goTo(bathroom); putDown(toothbrush) Another example that the system was tested on is that from [8] involving aircraft flying procedures. There is a single pro-cedure called fireOnBoard. It involves three actions, performed sequentially, with possibly other actions interleaved. The three actions are fuelOff, fullT hrottle, and mixtureOff. The only restriction is that while executing this procedure, the ac-tion fuelOn must not occur. In our frame-work, this example can be represented as follows: proc fireOnBoard startP roc(fireOnBoard), minus([fuelOff; any * ; fullT hrottle; any * ; mixtureOff], [(anyBut([fuelOn])) * ; fuelOn]); endP roc(fireOnBoard) endProc	proc cleanUp m startP roc(cleanUp m ); minus( while ∃t.Object(t) ∧ ¬InP lace(t, loc(t)) do π t.Object(t) ∧ ¬InP lace(t, loc(t))?; (get(t)|putAway(t)); (any|nil); endWhile, [brushT eeth]); endP roc(cleanUp m ) endProc Suppose that the sequence of ob-served actions starts with the two actions goT o(livingRoom) and take(toothbrush). All three variants of cleanUp would match those actions, and produce the same scenario: proc cleanUp_k -> proc get(toothbrush) -> goTo(livingRoom); pickUp(toothbrush) where k is either nothing, or u or m, de-pending on the version of the procedure used. Now suppose that the next action is use(toothbrush). The original version of cleanUp does not match the observed ac-tion. The other two variants, cleanUp u and cleanUp m , would still match the situ-ation, because the new action matches the unspecified action at the end of the loop. If the next action is goT o(bathroom), then both remaining procedures match this as well: proc cleanUp_k -> goTo(bathroom) proc putAway(toothbrush) -> use(toothbrush); pickUp(toothbrush); goTo(livingRoom); proc get(toothbrush) ->

where k can only be u or m.

Golog [9] is a precursor of ConGolog that does not support concurrency.

When n = 0, by convention the condition is equivalent to T rue.

We could try to drop this restriction and collect all the remaining δ, but it is not clear that these can always be finitely represented, e.g. πn.(P ositiveInteger(n)?; a; b(n)).