M Mahjoub

A Rouabhi

M Tijani

S Granet

A damage model for transversely isotropic materials

In a nuclear disposal project, the damage of the hosting rock is a capital issue that should be studied and understood. This problem is even more complex when the studied rock is anisotropic. In the present paper, a damage model that takes into account both initial and induced anisotropy is introduced using equivalence relations between the real material and a fictitious isotropic one on which we can take all the advantages of the well established isotropic theory. Numerical simulations using a Finite Element Method (FEM) code shows an agreement between the theoretical predictions and the experimental data of Brazilian tests with different orientation angles.

Introduction

In rock engineering, anisotropy is an important aspect that has to be taken into account. This material feature has been a long-standing issue in geomechanics. Multiple studies are interested in this problem since the early developmental stages of rock mechanics [START_REF] Boehler | Anisotropie et comportement rhéologique des matériaux. Anisotropy and rheological behavior of materials[END_REF][START_REF] Amadei | Importance of anisotropy when estimating and measuring in situ stress in rock[END_REF][START_REF] Hobbs | The tensile strength of rocks[END_REF][START_REF] Hobbs | An assessment of a technique for determining the tensile strength of rock[END_REF][START_REF] Hobbs | Rock tensile strength and its relationship to a number of alternative measures of rock strength[END_REF][START_REF] Barla | Indirect tensile testing of anisotropic rocks[END_REF][START_REF] Barron | Brittle fracture initiation in and ultimate failure of rocks, part III: anisotropic rocks: experimental results[END_REF][START_REF] Hudson | Tensile strength and the ring test[END_REF][START_REF] Fine | L'anisotropie des roches, son influence sur l'essai brésilien[END_REF][START_REF] Nova | An investigation into the tensile behaviour of a schistose rock[END_REF]. Recently, new applications such as nuclear waste disposal in argillaceous formations and shale gas exploitation increased the interest to characterize these materials [START_REF] Fjaer | Strength anisotropy of Mancos shale[END_REF][START_REF] Crawford | Shear strength anisotropy in fine-grained rocks[END_REF][START_REF] Rouabhi | Triaxial behaviour of transversely isotropic materials: Application to sedimentary rocks[END_REF][START_REF] Ambrose | Failure of shale under triaxial compressive stress[END_REF][START_REF] Ming | A failure criterion for transversely isotropic rocks[END_REF][START_REF] Cho | Deformation and strength anisotropy of Asan gneiss, Boryeong shale, and Yeoncheon schist[END_REF][START_REF] Rejeb | Projet Tournemire, programme mécanique, caractérisation du comportement mécanique au laboratoire[END_REF][START_REF] Vervoort | Failure of transversely isotropic rock under Brazilian test conditions[END_REF][START_REF] Claesson | Brazilian test: stress field and tensile strength of anisotropic rocks using an analytical solution[END_REF][START_REF] Chen | Determination of deformability and tensile strength of anisotropic rock using brazilian tests[END_REF][START_REF] Exadaktylos | Application of an explicit solution for transversely isotropic circular disc compressed diametrically[END_REF][START_REF] Chen | Measurement of indirect tensile strength of anisotropic rocks by the ring test[END_REF][START_REF] Quoc | Numerical simulations and interpretations of Brazilian tensile tests on transversely isotropic rocks[END_REF][START_REF] Tavallali | Effect of layer orientation on the failure of layered sandstone under Brazilian test conditions[END_REF][START_REF] Tavallali | Behaviour of layered sandstone under Brazilian test conditions: Layer orientation and shape effects[END_REF][START_REF] Quoc | Brazilian Test on Anisotropic Rocks -Laboratory Experiment, Numerical Simulation and Interpretation[END_REF][START_REF] Quoc | Brazilian tensile strength tests on some anisotropic rocks[END_REF]. Rocks anisotropy may be caused by mineral foliation, stratification or discontinuities. For the sake of simplification, it is generally admitted that the elastic behavior of sedimentary rocks like shales and schists can be reasonably described by transverse isotropy characterized by five independent parameters. It has been proven that the assumption of complete symmetry (isotropy) for this kind of materials may induce large errors in the measured in situ stress field [START_REF] Amadei | Importance of anisotropy when estimating and measuring in situ stress in rock[END_REF].

Numerous studies attempted to model the mechanical behavior of transversely isotropic materials. Multiple failure criteria were developed and compared to experimental results of triaxial compression tests [START_REF] Fjaer | Strength anisotropy of Mancos shale[END_REF][START_REF] Crawford | Shear strength anisotropy in fine-grained rocks[END_REF][START_REF] Rouabhi | Triaxial behaviour of transversely isotropic materials: Application to sedimentary rocks[END_REF][START_REF] Ambrose | Failure of shale under triaxial compressive stress[END_REF][START_REF] Ming | A failure criterion for transversely isotropic rocks[END_REF]. Rouabhi et al. [START_REF] Rouabhi | Triaxial behaviour of transversely isotropic materials: Application to sedimentary rocks[END_REF] proposed a viscoplastic constitutive model in order to characterize triaxial creep tests. On the other hand, a crack propagation method was employed to define anisotropic damage behavior laws for transversely isotropic materials (cf. [28, chapter 4 and 5] and [29, chapter 5 and 6]). However, a general methodology to introduce such a model is not yet available.

In order to define a general procedure to produce mechanical behavior models for transversely isotropic materials, the present work proposes an approach to adapt existing isotropic models. This method consists in a three steps process. First, we introduce a fictive equivalent isotropic material. Second, an isotropic model is chosen to characterize the new material. Finally, equivalence relations are used to adapt this model to the real material. A transformation between the behavior of the real anisotropic material and that of an isotropic fictitious one is introduced. This idea is proposed by [START_REF] Car | A large strain plasticity model for anisotropic materials -composite material application[END_REF] to simulate the non-linear constitutive behavior of composite materials and used in [START_REF] Rouabhi | Triaxial behaviour of transversely isotropic materials: Application to sedimentary rocks[END_REF] to define a viscoplastic behavior law and two failure criteria. The respect of the material symmetry is insured by the application of the representation theorem (cf. Truesdell and Noll [31, part B]).

As an application of this approach, a damage constitutive model taking into account both initial and induced anisotropy is introduced. This model is based on the works [START_REF] Rouabhi | Continuum modelling of dynamic behaviour and fragmentation of quasi-brittle materials: application to rock fragmentation by blasting[END_REF][START_REF] Carol | On the formulation of anisotropic elastic degradation. I. Theory on a pseudo-logarithmic damage tensor rate[END_REF][START_REF] Carol | On the formulation of anisotropic elastic degradation. II. Generalized peudo-Rankine model for tensile damage[END_REF] and [35, chapter 2] where a damage second order tensor is considered. The definition and evolution of the damage is established for the fictive isotropic material and afterward transferred to the real material. Numerical simulations of the Brazilian test for two rocks using this behavior law are presented and compared to experimental data from [START_REF] Cho | Deformation and strength anisotropy of Asan gneiss, Boryeong shale, and Yeoncheon schist[END_REF].

The constitutive law proposed in this paper is the cornerstone of a more complete model coupling the mechanical damage with the fluids flow and the heat transfer in the material. Nevertheless, for the sake of clarity, in this paper, the effective stress in the poromechanics sens and the mechanical strain tensors will be simply called stress and strain tensors. Moreover, the transformation from the real material to the fictitious isotropic one concerns only the mechanical behavior and not the other material properties such as the permeability K and the coefficient of thermal expansion α... This paper is organized as follows. Section 2 presents the approach of equivalent isotropic material and the necessary relations. In section 3, this procedure is applied to define an anisotropic damage behavior law for transversely isotropic materials. The model parameters are fitted using measures of the tensile strength.

Afterward, the behavior law is used to simulate 3D Brazilian tests with different orientation angles and the results are compared to experimental data.

Notations. Throughout this paper, a first order tensor (vector) is designed by an arrow over an undercase letter ( a), a second order one is denoted by two lines under a letter a and a fourth order tensor is designed by a tilda beneath a capital letter

Equivalent fictive isotropic material approach

Given a transversely isotropic material where the stress field σ and strain field ε are linked by the transversely isotropic Hooke tensor ∼ H(E, E ′ , ν, ν ′ , G), we define a fictive isotropic material where the stress σ and strain ε are linked by an isotropic tensor ∼ H associated to the fictive elastic parameters ( Ē, ν). The real and the fictitious stress are related by a second order tensorial transformation function ℓ:

σ = ℓ(σ) (1)
This function must respect material symmetry. In this work and in order to go further and allow analytical developments, ℓ is assumed to be linear. Therefore, this transformation may be represented by a fourth order transversely isotropic tensor

∼ L: σ = ∼ L : σ (2)
In order to relate the real and fictive strain, we use the restrictive relation σ : ε = σ : ε which leads to:

ε = ∼ L : ε (3)
Combining equation 2 and 3 with the fact that σ = ∼ H : ε, we deduce that:

∼ H = ∼ L ∼ H ∼ L (4)
In order to drive the expression of

∼ B 1 2 ∼ A ∼ B 1 2 = ∼ B 1 2 ∼ L ∼ B ∼ L ∼ B 1 2
. By writing

∼ B = ∼ B 1 2 ∼ B 1 2 , we obtain ∼ B 1 2 ∼ L ∼ B 1 2 2 = ∼ B 1 2 ∼ A ∼ B 1 2
. Finally, we find:

∼ L = ∼ B -1 2 ∼ B 1 2 ∼ A ∼ B 1 2 1 2 ∼ B -1 2 (5)
Writing the equation 4 in the form

∼ H -1 = ∼ L ∼ H -1 ∼ L, replacing ∼
A by the transversely isotropic tensor ∼ H -1 and ∼ B by the isotropic tensor ∼ H -1 and using the basis (I, J 1 , J 2 , J 3 , J 4 , J 5 ), we obtain:

[L] = [ H 1 2 ] [ H-1 2 ][H -1 ][ H-1 2 ] 1 2 [ H 1 2 ], l4 = ĥ4 / ĥ4 , l5 = ĥ5 / ĥ5 (6)
We finally get the following expressions of li as function of (E, E ′ , ν, ν ′ , G) and ( Ē, ν):

l1 = Ē. ĥ1 + ( b/ā)γ ∆ , l2 = Ē. ĥ2 ∆ , l3 = Ē. ĥ3 + (ā/ b)γ ∆ , l4 = Ē. ĥ4 b , l5 = Ē. ĥ5 b (7)
where

ā = 1 -2ν, b = 1 + ν, γ = ĥ1 ĥ3 -ĥ2 2 , ∆ = āĥ 1 + bĥ 3 + 2 āb γ and ĥ1 = 1 3 [2(1 -ν)/E + (1 -4ν ′ )/E ′ ] , ĥ2 = √ 2 3 [(1 -ν)/E -(1 -ν ′ )/E ′ ] , ĥ3 = 1 3 [(1 -ν)/E + 2(1 + 2ν ′ )/E ′ ] , ĥ4 = (1 + ν)/E ĥ5 = 1/2G (8)
ĥ1 = (1 -2ν)/ Ē, ĥ2 = 0, ĥ3 = ĥ4 = ĥ5 = (1 + ν)/ Ē (9) For a given elastic tensor ∼ H, we construct an infinity of isotropic equivalent materials each one is defined by the couple ( Ē, ν). These parameters may be fixed for instance in such a way that a chosen distance between ∼ H and ∼ H be minimized but we prefer to keep free ( Ē, ν) to take into account, as best as possible, the observed independence between the elastic behavior and damage for instance.

3 Anisotropic damage behavior law for transversely isotropic materials J. Lemaitre [36, chapter 1] defined the mechanical damage as the creation and growth of discontinuities, microvoids and microcracks, in a medium considered as continuous at a large scale. In engineering, the damage is represented by continuous variables in the space. In fact, the mechanics of continuous media introduces a Representative Volume Element (RVE) on which all properties are represented by homogenized variables. Mathematically, the damage variable may be represented either by a scalar, a higher order tensor or a combination of two or more scalar and tensorial variables if several mechanisms of damage occur. In order to take into account the directional bias introduced by the formation of cracks, an anisotropic damage model is to be considered i.e. the damage is represented by a higher order tensor variable. In this case, the largest generality for a damage variable is a representation by a fourth order tensor. However, such a representation is too difficult to use. Therefore, second order symmetric tensors are commonly employed since they are mathematically simpler and yet can describe most essential features of anisotropic damage [START_REF] Rouabhi | Continuum modelling of dynamic behaviour and fragmentation of quasi-brittle materials: application to rock fragmentation by blasting[END_REF][START_REF] Carol | On the formulation of anisotropic elastic degradation. I. Theory on a pseudo-logarithmic damage tensor rate[END_REF][START_REF] Carol | On the formulation of anisotropic elastic degradation. II. Generalized peudo-Rankine model for tensile damage[END_REF][START_REF] Rouabhi | Comportement et fragmentation dynamiques des matériaux quasi-fragiles[END_REF][START_REF] Lemaitre | Engineering damage mechanics: ductile, creep, fatigue and brittle failures[END_REF][START_REF] Lemaitre | Anisotropic damage law of evolution[END_REF][START_REF] Murakami | Constitutive and damage evolution equations of elastic-brittle materials based on irreversible thermodynamics[END_REF]. In general numerical codes, what is called "damage-model" consists principally on a linear relationship between stress and strain with an elastic tensor ∼ H which varies as a function of a damage variable. One can notice that this formalism is commonly used to describe the damage of initially isotropic solids. To the best of our knowledge, an anisotropic damage model for transversely isotropic materials using the mechanics of continuous media is not available.

In order to define an anisotropic damage behavior law for the transversely isotropic material, we will use the equivalent isotropic material approach defined in the previous section. Further, we assume that the relationship between the real and fictive materials ∼

H = ∼ L ∼ H ∼
L remains valid at every stage of the damage but with a fixed ∼ L. This assumption means that we consider the following relationship between the real and the fictive materials:

∼ H -1 (ω) = ∼ L ∼ H -1 (ω) ∼ L ( 10
)
where ω is the damage second order tensor. This may be interpreted as a separation between the effect of natural anisotropy represented by the tensor ∼ L and the induced anisotropy represented by the damage tensor ω.

It remains now to define a damage behavior law for the fictitious isotropic material ∼ H(ω) . An established constitutive model for isotropic materials may be employed. We select here the damage behavior law introduced by Rouabhi et al. [START_REF] Rouabhi | Continuum modelling of dynamic behaviour and fragmentation of quasi-brittle materials: application to rock fragmentation by blasting[END_REF][START_REF] Rouabhi | Comportement et fragmentation dynamiques des matériaux quasi-fragiles[END_REF]. The developed model is based on the so called, in damage mechanics, effective stress σ = ω 1 2 σ ω 1 2 and strain ε = ω -1 2 ε ω -1 2 tensors where σ and ε denote the stress and strain tensors in the damaged isotropic material. The compliance tensor of the fictitious damaged material is given by the following expression:

∼ H -1 (ω) = -ν Ē ω ⊗ ω + 1 + ν Ē ω ⊗ ω (11)
The rate-dependent evolution law of the damage variable ω is given by:

Λ = 2ω -1 2 ω ω -1 2 = 3 k=1 λ(a k ) ˜ n k ⊗ ˜ n k , λ(x) = v d 1 -exp - x R d -1 n d ( 12
)
where a k and ˜ n k are respectively the eigenvalues and the eigenvectors of the tensor a = 1 2 σ ε , v d , R d and n d are material parameters and x denotes the positive part of the tensor x. It's the unique tensor having the same eigenvectors as x and whose eigenvalues are deduced by the operator

x i = (x i + |x i |)/2.
Finally, in order to distinguish the different response in tension and compression, an active damage tensor was introduced as follows:

ω ac = 1 + P (ω -1)P , P = 3 k=1 H(ε k ) n k ⊗ n k ( 13
)
where εk and n k are the eigenvalues and eigenvectors of ε respectively and H is the Heaviside function.

Simulation of Brazilian tests

Indirect tensile tests such as Brazilian tests are very useful in rock mechanics since it is too difficult to carry out direct tensile tests. It is generally used to find the tensile strength for isotropic materials since its value could be directly estimated knowing the ultimate applied load (P ) and the sample dimensions (diameter D and thickness t): Unfortunately, this result is not valid in the case of transversely isotropic materials and that is why some authors have attempted to develop more complicated solutions which take into account not only the applied load and the sample dimensions but also the elastic parameters and the orientation angle [START_REF] Chen | Determination of deformability and tensile strength of anisotropic rock using brazilian tests[END_REF][START_REF] Exadaktylos | Application of an explicit solution for transversely isotropic circular disc compressed diametrically[END_REF][START_REF] Chen | Measurement of indirect tensile strength of anisotropic rocks by the ring test[END_REF][START_REF] Quoc | Brazilian Test on Anisotropic Rocks -Laboratory Experiment, Numerical Simulation and Interpretation[END_REF]. J. Claesson [START_REF] Claesson | Brazilian test: stress field and tensile strength of anisotropic rocks using an analytical solution[END_REF] gave the following approximate formula:

R t = 2P πDt (14)
R t = 2P πDt   E E ′ cos(2Θ) 4 - cos(2Θ) 4 (b -1)   , b = √ EE ′ 2 ( 1 G - 2ν ′ E ′ ) (15)
In order to show the capabilities of the developed oriented damage model for transversely isotropic materials, in what follows, we will simulate numerically the Brazilian test in 3D configuration (t = D/2 = 30 mm) for different orientation angles and for two rocks [START_REF] Cho | Deformation and strength anisotropy of Asan gneiss, Boryeong shale, and Yeoncheon schist[END_REF] using the parameters in table 1 (the parameter Ē is not involved in this case). In these numerical simulations, the rock sample is supposed to be totally adhering the platens of the press therefore we have a totally 3D problem. Figure 1 shows the whole simulation plot (the applied load versus the axial displacement). The peak of these curves is recorded and used in the expression 15 in order to estimate the tensile strength of the rock for the corresponding orientation angle. Figure 2 shows the obtained tensile strength values compared to experimental data. In order to visualize the sample's damage state at the end of the test, the horizontal damage for the two rocks for orientations 0, 45 and 90 is presented in figure 3. It is visible that the damage develops mainly along the centerline of the sample. As can be seen, the proposed model furnishes satisfactory results. However, the obtained compression strength anisotropy is of same range as the Young moduli anisotropy and can not reach the observed values for rocks where a big difference between the two anisotropy values is measured. A further study on the used yield function has to be done in order to overcome this problem. Moreover, some authors such as [START_REF] Hobbs | The tensile strength of rocks[END_REF][START_REF] Hobbs | An assessment of a technique for determining the tensile strength of rock[END_REF][START_REF] Barla | Indirect tensile testing of anisotropic rocks[END_REF][START_REF] Hudson | Tensile strength and the ring test[END_REF][START_REF] Chen | Measurement of indirect tensile strength of anisotropic rocks by the ring test[END_REF] proved that the Brazilian test is not very convenient to determine the tensile strength especially for laminated materials. In fact, in the most of cases, the crack does not happen within the loading plane but within an inclined one which means that the failure is of a shear nature and not tensile one. This observation could be explained by the fact that the compression stress next to the platens of the press reaches the shear limit before that the tensile stress in the sample's center reaches the tensile strength. For that reason, an other test was proposed and consists on making a hole in the sample's center (This test is called the ring test). This way the tensile stress next to the hole is increased and will probably reach the stress strength before that the compression stress reaches the shear strength. As a future work, it would be of a great interest to simulate the ring test and compare the results to experimental data. In this paper, an approach to describe the behavior of transversely isotropic materials is introduced. The method consists in introducing a fictive isotropic equivalent material, choosing an established isotropic model and transferring it to the real material. The elastic moduli of the fictitious material are the only two supplementary parameters introduced by this procedure. This method is used here to define an anisotropic damage behavior law in tensile regime. The model parameters are adjusted to experimental results and used in an FEM code (VIPLEF 3D and Code-Aster) to simulate 3D Brazilian tests for two rocks with different orientation angles. Compared to experimental data, the furnished results are rather satisfactory. However, the obtained tensile strength anisotropy is of the same range as the Young moduli anisotropy and can not reach the observed values for rocks where a big difference between the two anisotropy values is measured. A further work must be done to overcome this issue. Moreover, since the failure in a Brazilian test might be of a shear nature and not only a pure tensile nature, other simulations of the ring test for instance have to be compared to experimental data.

∼A

  . Superscript ' t ' indicates the transpose operation, while 'tr' is the trace operator. Symbol ':' denotes the product with double contraction, e.g. a : b = a ij b ji , where the index denotes cartesian components and repeated subscript imply summation unless otherwise indicated. The product a b denotes a single contraction, i.e. a b ij = a ik b kj . In the same way, we have ∼ A ∼ B ijkl = A ijmn B nmkl . The dyadic or the tensor product is so a ⊗ b ijkl = a ij b kl and ( a ⊗ b) ij = a i b j , whereas ' ⊗ ' denotes the symmetrized dyadic product defined as a ⊗ b ijkl = 1 2 (a ik b jl + a il b jk ). The second-order 1 and the fourth-order ∼ 1 are identity tensors.

∼L 1 2

 1 as a function of ∼ H and ∼ H, let's start by solving the general problem ∼ on the left and on the right, one gets

Figure 1 :

 1 Figure 1: Brazilian test simulation for different orientation angles

Figure 2 :

 2 Figure 2: Tensile strength with simulation

Figure 3 :

 3 Figure 3: Horizontal damage state at the end of the Brazilian test

Table 1 :

 1 Elastic and model parameters for the studied rocks

	Rock	E(GP a) E ′ (GP a)	ν	ν ′	G(GP a)	ν	R d
	Boryeon shale	39.3	19.0	0.18 0.20	8.7	0.1242 4.4325
	Yeoncheon schist	72.1	21.2	0.25 0.16	13.7	0.2586 2.2383


Clément Aubert

Marc Bagnol

Thomas Seiller

Memoization for Unary Logic Programming: Characterizing Ptime

Keywords: Implicit Complexity, Resolution, Logic Programming, Polynomial Time, Proof Theory, Pushdown Automata, Geometry of Interaction Complexité implicite, Résolution, Programmation logique, Temps polynomial, Théorie de la démonstration, Automates à piles, Géométrie de l'intéraction

We give a characterization of deterministic polynomial time computation based on an algebraic structure called the resolution semiring, whose elements can be understood as logic programs or sets of rewriting rules over first-order terms. More precisely, we study the restriction of this framework to terms (and logic programs, rewriting rules) using only unary symbols. We prove it is complete for polynomial time computation, using an encoding of pushdown automata. We then introduce an algebraic counterpart of the memoization technique in order to show its Ptime soundness. We finally relate our approach and complexity results to complexity of logic programming. As an application of our techniques, we show a Ptime-completeness result for a class of logic programming queries which use only unary function symbols.

Introduction

Complexity theory focuses on questions related to resource usage of computer programs, such as the amount of time or memory a given program will need to solve a problem.

Complexity classes are defined as sets of problems that can be solved by algorithms whose executions need comparable amounts of resources. For instance, the class Ptime is the set of predicates over binary words that can be decided by a Turing machine implementing an algorithm whose execution time is bounded by a polynomial in the size of its input.

However, these definitions depend on the notion of machine and cost-model considered, for the efficiency of an algorithm is sensible to these. The "invariance thesis" [START_REF] Van | Machine Models and Simulation[END_REF] is a way to bypass this limitation by defining what "a reasonable model" is: all the "reasonable" models (endowed with cost models) can simulate each other with a "reasonable" overhead. The bootstrap for this notion to apply largely was to remark that polynomial bounds on execution time are robust, as the class of problems captured by different models where this bound coincide. The definition is still machine-dependent, but not dependent of a particular model of computation.

One of the main motivations for an implicit computational complexity (ICC) theory is to find completely machine-independent characterizations of complexity classes. The aim is to characterize classes not "by constraining the amount of resources a machine is allowed to use, but rather by imposing linguistic constraints on the way algorithms are formulated." [15, p. 90] This has been already achieved via different approaches, one of which is based on considering restricted programming languages or computational principles [START_REF] Bellantoni | A New Recursion-Theoretic Characterization of the Polytime Functions[END_REF][START_REF] Leivant | Stratified Functional Programs and Computational Complexity[END_REF][START_REF] Møller | A Functional Language for Logarithmic Space[END_REF].

A number of results also arose from proof theory through the study of subsystems of linear logic [START_REF] Girard | Linear logic[END_REF]. More precisely, the Curry-Howard -or proofs as programs -correspondence expresses a deep relation between formal proofs and typed programs. For instance, one can define a formula Nat which corresponds to the type of binary integers, in the sense that a given (cut-free, i.e. normal, already evaluated) proof of this type represents a given natural number. A proof of the formula Nat ⇒ Nat then corresponds to an algorithm computing a function from integers to integers, where the computation itself amounts to a rewriting on proofs: the cut-elimination procedure.

By restricting the rules of the logical system, one obtains a subsystem where less proofs of type Nat ⇒ Nat can be written, hence less algorithms can be represented. In a number of such restricted systems the class of accepted proofs, i.e. of programs, corresponds 1 to some complexity class: elementary complexity [START_REF] Girard | Light Linear Logic[END_REF][START_REF] Danos | Linear Logic & Elementary Time[END_REF], polynomial time [START_REF] Lafont | Soft linear logic and polynomial time[END_REF][START_REF] Baillot | Light Types for Polynomial Time Computation in Lambda-Calculus[END_REF], logarithmic [START_REF] Dal | Functional Programming in Sublinear Space[END_REF] and polynomial [START_REF] Gaboardi | An Implicit Characterization of PSPACE[END_REF] space.

More recently, new methods for obtaining implicit characterizations of complexity classes based on the geometry of interaction (GoI) research program [START_REF] Girard | Towards a geometry of interaction[END_REF] have been developed. The GoI approach offers a more abstract and algebraic point of view on the cut-elimination procedure of linear logic. One works with a set of untyped programs represented as some geometric objects, e.g. graphs [START_REF] Danos | La Logique Linéaire appliquée à l'étude de divers processus de normalisation (principalement du λ -calcul)[END_REF][START_REF] Seiller | Logique dans le facteur hyperfini : géometrie de l'interaction et complexité[END_REF] or generalizations of graphs [START_REF] Seiller | Interaction Graphs: Graphings[END_REF], bounded linear maps between Hilbert spaces (operators) [START_REF] Girard | Geometry of interaction 1: Interpretation of System F[END_REF][START_REF] Girard | Geometry of Interaction V: logic in the hyperfinite factor[END_REF][START_REF] Seiller | A Correspondence between Maximal Abelian Sub-Algebras and Linear Logic Fragments[END_REF], clauses (or "flows") [START_REF] Girard | Geometry of interaction III: accommodating the additives[END_REF][START_REF] Bagnol | On the Resolution Semiring[END_REF]. This set of objects is then considered together with an abstract notion of execution, seen as an interactive process: a function does not process a static input, but rather communicate with it, asking for values, reading its answers, asking for another value, etc.

Types can then be defined as sets of program representations sharing comparable behaviors. For instance the type Nat ⇒ Nat is the set of untyped programs which, given an integer as input, produce an integer as output.

This approach based on the GoI differs from previous ICC works using linear logic in that they do not rely on a restriction of some type system, but rather on a restriction on the set of program representations considered. Still, they benefit from previous works in type theory: for instance the representation of integers used here comes from their representation in linear logic, translated in the GoI setting, whose interactive point of view on computation has proven crucial in characterizing logarithmic space computation [START_REF] Dal | Functional Programming in Sublinear Space[END_REF].

The first results that used those innovative considerations were based on operator algebras [START_REF] Girard | Normativity in Logic[END_REF][START_REF] Aubert | Characterizing co-NL by a group action[END_REF][START_REF] Aubert | Logarithmic Space and Permutations[END_REF]. Here we consider a more syntactic flavor of the GoI where untyped programs are represented in the so-called resolution semiring [START_REF] Bagnol | On the Resolution Semiring[END_REF], a semiring based on the resolution rule [START_REF] Alan | A Machine-Oriented Logic Based on the Resolution Principle[END_REF] and a specific class of logic programs. This setting presents some advantages: it avoids the involvement of operator algebras theory, it eases the discussions in terms of complexity (we manipulate first-order terms, which have natural notions of size, height, etc.) and it offers a straightforward connection with complexity of logic programming [START_REF] Dantsin | Complexity and expressive power of logic programming[END_REF].

Previous works in this direction led to characterizations of logarithmic space predicates Logspace and co-NLogspace [START_REF] Aubert | Unification and Logarithmic Space[END_REF][START_REF] Aubert | Logic Programming and Logarithmic Space[END_REF], by considering for instance restrictions on the height of variables.

Our main contribution here is a characterization of the class Ptime by studying a natural restriction, namely that one is allowed to use exclusively unary function symbols. Pushdown automata2 are easily related to this simple restriction, for they can be represented as logical programs satisfying this "unarity" restriction. This will imply the completeness of the model under consideration for polynomial time predicates.

We then complete the characterization by showing that any such unary logic program can be decided in polynomial time. This part of the proof consists in an adaptation of S. Cook's memoization technique [START_REF] Arthur | Linear Time Simulation of Deterministic Two-Way Pushdown Automata[END_REF] to the context of logic programs.

The last part of the paper presents consequences of these results in terms of complexity of logic programming, namely that the corresponding class of queries are Ptime-complete, when considering combined complexity [20, p. 380].

Compared to other ICC characterizations of Ptime, and in particular those coming from proof theory, our results have a simple formulation and provide an original point of view on complexity classes.

A byproduct of this work is to provide a method to test membership in Ptime: if one can rephrase a problem with clauses H B using only unary function symbols, then our result ensures that the problem lies in Ptime. Conversely if a problem cannot be rephrased that way, it lies outside of Ptime.

Outline of the paper

We begin by giving in Sect. 2.1 the formal definition of the resolution semiring; then briefly explain how words can be represented in this structure (Sect. 2.2) and recall the characterization of logarithmic space obtained in earlier work (Sect. 2.3). In Sect. 2.4 we introduce the restricted semiring that will be under study in this paper: the Stack semiring.

The next two sections are respectively devoted to the completeness and soundness results for Ptime. For completeness, we first review the fact that multi-head finite automata with pushdown stack characterize Ptime and review the memoization technique in this case (Sect. 3.1), and then show how to represent them as elements built from the Stack semiring (Sect. 3.2). The soundness result is then obtained by adapting memoization to the Stack semiring. This adaptation, which we call the saturation technique, is introduced in Sect. 4.1.

In the last section, we formulate our results in terms of complexity of logic programming. In particular, we explain how elements of the Stack semiring can be seen as a particular kind of unary logic programs to which the saturation technique can be applied. This allows us to show that the combined complexity problem for unary logic program is Ptime-complete.

As an illustration, we show in Sect. 5.2 that the circuit value problem can be solved with this method.

The Resolution Semiring

Flows and Wirings

Let us begin with some reminders and notations on first-order terms and unification theory. Notation 2.1 (terms). We consider first-order terms, written t, u, v, . . ., built from variables and function symbols with assigned finite arity. Symbols of arity 0 will be called constants.

Sets of variables and of function symbols of any arity are supposed infinite. Variables will be noted in italics font (e.g. x, y ) and function symbols in typewriter font (e.g. c, f(•), g(•, •)).

We distinguish a binary function symbol • (in infix notation) and a constant symbol . We will omit the parentheses for • and write t

• u • v for t • (u • v).
We write var(t) the set of variables occurring in the term t and say that t is closed if var(t) = ∅. The height h(t) of a term t is the maximal distance between its root and leaves; a variable occurrence's height in t is its distance to the root.

We will write θt the result of applying the substitution θ to the term t and will call renaming a substitution α that bijectively maps variables to variables.

We will be concerned with formal solving of equations of the form t = u where t and u are terms. Let us introduce a precise formulation of this problem and some associated vocabulary. Definition 2.2 (unification, matching and disjointness). Two terms t, u are:

• unifiable if there exists a substitution θ -a unifier of t and u -such that θt = θu . If any other unifier of t and u is an instance of θ , we say θ is the most general unifier (MGU) of t and u ; • matchable if t , u are unifiable, where t , u are renamings of t, u such that var(t )∩var(u ) = ∅; • disjoint if they are not matchable.

A fundamental result of unification theory is that when two terms are unifiable, a MGU exists and is computable. More specifically, the problem of deciding whether two terms are unifiable is Ptime -complete [21, Theorem 1].

The notion of MGU allows to formulate the resolution rule, a key concept of logic programming that defines the composition of Horn clauses (expressions of the form H B 1 , . . . , B n ):

V T 1 , . . . , T n H B 1 , . . . , B m , U var(U ) ∩ var(V ) = ∅ θ is a MGU of U and V
Res θH θB 1 , . . . , θB m , θT 1 , . . . , θT n Note that the condition on variables implies that we are matching U and V rather than unifying them. In other words, the resolution rule deals with variables as if they were bounded.

From this perspective, "flows" -defined below -are a specific type of Horn clauses H B , with exactly one formula B on the right of and all the variables of H already appearing in B . The product of flows will be defined as the resolution rule restricted to this specific type of clauses.

Definition 2.3 (flow).

A flow is an ordered pair f of terms f := t u , with var(t) ⊆ var(u). Flows are considered up to renaming: for any renaming α , t u = αt αu .

A flow t u can also be understood as a rewriting rule over the set of first-order terms. For instance, the flow g(x)

f(x) corresponds to the following rewriting rule: terms of the form f(v) where v is a term are rewritten as g(v) and all other terms are left unchanged.

We will soon define the product of flows which provides a way of composing them; from the term-rewriting perspective, this operation corresponds to composing two rules -when possible, i.e. when the result of the first rewriting rule allows the application of the second -into a single one.

For instance, one can compose the flows f 1 := h(x) g(x) and f 2 := g(x) f(x) to produce the flow

f 1 f 2 = h(x) f(x).
Notice by the way that this (partial) product is not commutative as composing these rules the other way around is impossible, i.e. f 2 f 1 is not defined. Definition 2.4 (product of flows). Let t u and v w be two flows. Suppose we picked representatives of the renaming classes such that var(u) ∩ var(v) = ∅.

The product of t u and v w is defined when u and v are unifiable, with MGU θ , as (t u)(v w) := θt θw .

We now define wirings, which are simply finite sets of flows and therefore correspond to logic programs. From the term-rewriting perspective they are just sets of rewriting rules. The definition of product of flows is naturally lifted to wirings.

Definition 2.5 (wiring).

A wiring is a finite set of flows. Their product is defined as

F G := { f g | f ∈ F, g ∈ G, f g defined } .
The resolution semiring R is the set of all wirings.

The set of wirings R indeed enjoys a structure of semiring. 3 We will use an additive notation for sets of flows to highlight this situation:

• The symbol + will be used in place of ∪, and we write sets as sums of their elements:

{ f 1 , . . . , f n } := f 1 + • • • + f n .
• We denote by 0 the empty set, i.e. the unit of +.

• We have a unit for the product, the wiring I := x x.

As we will always be working within R, the term "semiring" will be used instead of "subsemiring of R".

Finally, let us recall the notion of nilpotency in a semiring and extend the notion of height (of terms) to flows and wirings. Definition 2.6 (height). The height h(f ) of a flow f = t u is defined as max{h(t), h(u)} . A wiring's height is defined as h

(F ) = max{ h(f ) | f ∈ F } . By convention h(0) = 0 .

Definition 2.7 (nilpotency).

A wiring F is nilpotent -written Nil(F ) -if and only if F n = 0 for some n .

The above classical notion from abstract algebra has a specific reading in our case of study. In terms of logic programming, it means that all chains obtained by applying the resolution rule to the set of clauses we consider cannot be longer than a certain bound. From the point of view of rewriting, it means that the set of rewriting rules we consider is terminating with a uniform bound on the length of rewriting chains -note however that we consider rewriting that occur only at the root of terms, while the usual notion from term rewriting systems [START_REF] Baader | Term rewriting and all that[END_REF] allows in-context rewriting.

Representation of Words and Programs

This section explains and motivates the representation of words as flows. By studying their interactions with wirings from a specific semiring, notions of program and language are defined.

First, let us see how the binary function symbol • used to construct terms can be extended to build flows and then semirings. Definition 2.8. Let u v and t w be two flows. Suppose we have chosen representatives of their renaming classes that have disjoint sets of variables.

We define

(u v) • (t w) := u • t v • w .
The operation is extended to wirings by

( i f i ) • ( j g j ) := i,j f i • g j .
Then, given two semirings A and B , we define the semiring

A • B := { i F i • G i | F i ∈ A , G i ∈ B } .
The operation indeed defines a semiring because for any wirings F, F , G, G we have

(F • G)(F • G) = F F • GG .

Moreover, we carry on the convention of writing

A • B • C for A • (B • C) .
Notation 2.9. We write t u the sum t u + u t.

Definition 2.10 (word representations). From now on, we suppose fixed an infinite set of constant symbols P (the position constants) and a finite alphabet Σ disjoint from P with ∈ Σ (we write Σ * the set of words over Σ).

Let W = c 1 • • • c n ∈ Σ * and p = p 0 , p 1 , .
. . , p n be pairwise distinct elements of P . Writing p n+1 = p 0 and c n+1 = c 0 = , we define the representation of W associated with p 0 , p 1 , . . . , p n as the following wiring:

Wp = n i=0 c i • r • x • y • head(p i ) c i+1 • l • x • y • head(p i+1 )
In this definition, the position constants represent memory cells storing the symbols , c 1 , c 2 , . . . . The representation of words is dynamic, i.e. we may think intuitively of movement instructions from a symbol to the next or the previous (hence the choice of symbols l and r for "left/previous" and "right/next") for some kind of automaton reading the input. More details on this will be given in the proof of Theorem 3.3.

Hence, for a given position constant p i , we use terms c i • r and c i • l which will be linked (by flows of the representation) to elements c i+1 • l at position p i+1 and c i-1 • r at position p i-1 respectively.

Note moreover that the representation of the input is circular (this is a consequence of using the Church encoding of words), as we take c n+1 = c 0 = . Flows representing the word c 1 • • • c n can be pictured as follows:

p 0 • r • l p 1 c 1 • r c 1 • l p 2 c 2 • r c 2 • l . . . p n c n • r c n • l
On the other hand, the notion of observation will be the counterpart of a program in our construction. We first give a general definition, that will be instantiated later to classes of observations that characterize specific complexity classes. The important point here is that we forbid an observation to use any position constant, in order to have it interact the same way with all the representations Wp of a word W . Definition 2.11 (observation semiring). We define the semirings P ⊥ of flows that do not use the symbols in P; and Σ lr the semiring generated by flows of the form c

• d c • d with c, c ∈ Σ ∪ { } and d, d ∈ {l, r} .
We define the semiring of observations as:

O := (Σ lr • R) ∩ P ⊥
and the semiring of observations over the semiring A as

O[ A ] := (Σ lr • A) ∩ P ⊥
The following theorem is a consequence [9, Theorem IV.5] of the fact that observations cannot use position constants. With this theorem, we can safely define how a word can be accepted by an observation: the notion is independent of the specific choice of a representation of position constants.

Definition 2.13 (accepted language). Let O be an observation. We define the language accepted by O as

L(O) := { W ∈ Σ * | ∀p, Nil(O Wp ) }

Balanced Flows and Logarithmic Space

In previous work [START_REF] Aubert | Logic Programming and Logarithmic Space[END_REF], we investigated the semiring of balanced wirings, that are defined as sets of balanced -or "height-preserving" -flows.

Definition 2.14 (balance).

A flow f = t u is balanced if for any variable x ∈ var(t) ∪ var(u) , all occurrences of x in both t and u have the same height (recall notations p. 5). A balanced wiring F is a sum of balanced flows.

We write R b for the set of balanced wirings. It also appears that a natural subclass of balanced wirings characterizes DLogspace, the class of deterministic logarithmic space computable predicates.

The Stack Semiring

This paper deals with another restriction on flows, namely the restriction to unary flows, i.e. flows defined from unary function symbols only. The semiring of wirings composed only of unary flows is called the Stack semiring, and will be shown to characterize polynomial time computation.

Here we briefly give the definitions and results about this semiring that will be needed in this paper. A more complete picture can be found in the second author's Ph.D. thesis [START_REF] Bagnol | On the Resolution Semiring[END_REF].

Definition 2.17 (unary flows). A unary flow is a flow built using only unary function symbols and a variable. The semiring Stack is the set of wirings of the form i t i u i where the t i u i are unary flows.

Example 2.18. The flows f(f(x )) g(x ) and x g(x ) are unary, while x • f(x) g(x) and f(c)

x are not.

Notation 2.19 (stack operations). If τ = g 1 , . . . , g n is a finite sequence of unary function symbols and t is a term, we write τ (t

) := g 1 g 2 (• • • g n (t) • • • .
We will write τ σ the concatenation of the sequences τ and σ . Given two sequences τ and σ we define the flow op τ, σ := τ (x) σ(x) which we call a stack operation.

Note that, by definition, an element of the Stack semiring must be a sum of stack operations.

The notion of cyclic flow is crucial in the proof of the characterization of polynomial time computation. As we will see, it is complementary to the nilpotency property for elements of Stack , i.e. a wiring in Stack will be shown to be either cyclic or nilpotent.

Definition 2.20 (cyclicity). A flow t

u is a cycle if t and u are matchable (Definition 2.2). A wiring F is cyclic if there is a k such that F k contains a cycle.

For s = f 1 , . . . , f n a sequence of stack operations, define:

• its height as h( s) := max i h(f i )

• its cardinality 4 Card( s) := Card{ f i | 1 ≤ i ≤ n } . • its product p( s) as f 1 • • • f n .
We say the sequence s is cyclic if there is a sub-sequence

s i,j = f i , . . . , f j (1 ≤ i ≤ j ≤ n ) such that p( s i,j ) is a cycle. Remark 2.21. A flow f is a cycle iff f 2 = 0.
To carry on the proof evoked above that cyclicity and nilpotency are complementary notions in Stack , we borrow a result from an earlier work about GoI and complexity in the context of an algebra of Horn clauses. Lemma 2.22 (acyclic sequence [10, lemma 5.3]). If s is an acyclic sequence of stack operations, then we have

h p( s) ≤ h( s)(Card( s) + 1)
The following property says that cycles in Stack can be iterated indefinitely, i.e. a stack operation op τ, σ such that (op τ, σ ) 2 = 0 is never nilpotent. Proposition 2.23. If a stack operation f is a cycle, then f n = 0 for all n . Remark 2.24. This does not hold for general flows. For instance,

f = x • c d • x is a cycle because f 2 = c • c d • d = 0 (by Remark 2.21), but f 3 = (x • c d • x )(c • c d • d) = 0 . Theorem 2.25 (nilpotency in Stack ). A wiring F ∈ Stack is nilpotent iff it is acyclic.
Proof Suppose F is not nilpotent, so that there is at least one stack operation in F n for any n , and let S be the number of different function symbols appearing in F . Set k := (S h (F )(Card(F )+1) + S h (F )(Card(F )+1)-1 + • • • + 1) 2 , i.e. the total number of different flows of height at most h (F )(Card(F ) + 1) using the symbols appearing in F .

Let f = 0 be an element of F k+1 . It is the product p ( s) of a sequence s = f 1 , . . . , f k+1 of stack operations that belong to F . We show by contradiction that this sequence must be cyclic, so let us suppose it is not. By Lemma 2.22, we know that for any i > 0 , setting

s i := f 1 , . . . , f i we have h p ( s i ) ≤ h ( s i )(Card( s i ) + 1) ≤ h (F )(Card(F ) + 1)
Therefore, for any i > 0 the flow p ( s i ) is of height at most h (F )(Card(F ) + 1) and uses only symbols appearing in F , i.e. it wanders in a set of cardinal k , so there must be 1 ≤ i < j ≤ k + 1 such that p ( s i ) = p ( s j ) . Now, setting s i+1,j := f i+1 , . . . , f j , we have that p ( s i )p ( s i+1,j ) = p ( s j ) = p ( s i ) hence p ( s i )p ( s i+1,j ) 2 = p ( s i ) = 0 and thus p ( s i+1,j ) 2 = 0 i.e. p ( s i+1,j ) is a cycle. As p ( s i+1,j ) ∈ F j-i we can conclude that F is cyclic.

The converse is an immediate consequence of Proposition 2.23.

Example 2.26. Consider the wiring

F := f 1 (x) f 0 (x) + f 0 (f 1 (x)) f 1 (f 0 (x)) + f 0 (f 0 (f 1 (x))) f 1 (f 1 (f 0 (x))) + f 0 (f 0 (f 0 (x))) f 1 (f 1 (f 1 (x)))
which implements a sort of counter from 0 to 7 in binary notation that resets to 0 when it reaches 8 (we see the sequence f x f y f z as the integer x+2y+4z ). It is clear with this intuition in mind that this wiring is cyclic. Indeed, an easy computation shows that f 0 (f 0 (f 0 (x))) f 0 (f 0 (f 0 (x))) ∈ F 8 . If we lift this example to the case of a counter from 0 to 2 n -1 that resets to 0 when it reaches 2 n , we obtain an example of a wiring F of cardinal n and height n -1 such that F 2 n contains a cycle, but F 2 n -1 does not. This shows that the number of iterations needed to find a cycle may be exponential in the height and the cardinal of F , which rules out a polynomial time decision procedure for the nilpotency problem that would simply compute the iterations of F until it finds a cycle in it. The class of deterministic polynomial time computable predicates Ptime is the most studied complexity class, mainly because it supposedly contains all "tractable" problems.

Extending our approach to this class was a long-standing goal, whose completeness part is attained thanks to the connection with pushdown automata. In this subsection, we recall their definition, the Ptime characterization theorem we will rely on and the memoization technique.

Definition and classical results

Automata form a very basic model of computation that can be extended in different ways. For instance, allowing multiple heads that can move in two directions on the input tape, one gets a model of computation equivalent to read-only Turing machines.

Among possible extensions, our interest will focus on the addition of a "pushdown stack" (together with multiple heads), which we referred to as "pushdown automata" until now. We will see that this leads to a characterization of Ptime.

Let us give below the most general definition, for the non-deterministic case.

Definition 3.1 (2MFA+S ). For k 1, a 2-way k -head finite automaton with pushdown stack ( 2MFA+S(k)) is a tuple M = {S, i, A, B, , , , σ} where:

• S is the finite set of states, with i ∈ S the initial state;

• A is the input alphabet, B the stack alphabet; The automaton rejects the input if it loops, otherwise it accepts. This condition is equivalent to the standard way of defining acceptance and rejection by "reaching a special state" [33, Theorem 2, p. 125]. Modulo another standard transformation, we restrict the transition relation so that at most one head moves at each transition. Without pushdown stacks, 2-way k -head finite automata characterize Logspace and NLogspace , depending on the automata being deterministic or not.

This result, used in our previous work [START_REF] Aubert | Logic Programming and Logarithmic Space[END_REF][START_REF] Aubert | Logarithmic Space and Permutations[END_REF], was first stated informally by Juris Hartmanis [32, pp. 338-339] and is often [13, p. 13], [32, pp. 338-339], attributed to Alan Cobham. However, a detailed proof can be found in a classical handbook [43, pp. 223-225]. The addition of a pushdown stack improves the expressivity of the machine model, as stated in the following theorem. Theorem 3.2. 2MFA+S characterize Ptime.

RR n°8796

Without reproving this classical result of complexity theory, we review the main ideas that support it.

Simulating a polynomial-time Turing machine with a 2MFA+S amounts to designing an equivalent Turing machine whose movements of heads follow a regular pattern. That permits to seamlessly simulate their contents with a pushdown stack. A complete proof [13, pp. 9-11] as well as a precise algorithm [43, pp. 238-240] can be found in the literature.

Simulating a 2MFA+S with a polynomial-time Turing machine cannot amount to simply simulate step-by-step the automaton with the Turing machine. The reason is that for any automaton, one can design an automaton that recognizes the same language but runs exponentially slower [1, p. 197]. That the automaton can accept its input after an exponential computation time is similar with the situation of the counter in Example 2.26.

The technique invented by Alfred V. Aho et al. [START_REF] Aho | Time and Tape Complexity of Pushdown Automaton Languages[END_REF] and made popular by Stephen A. Cook consists in building a "memoization table" that allows the Turing machine to create shortcuts in the simulation of the automaton, decreasing drastically its computation time. In some cases, an automaton with an exponentially long run can even be simulated in linear time [START_REF] Arthur | Linear Time Simulation of Deterministic Two-Way Pushdown Automata[END_REF].

We give more details on this technique in the next subsection, as its adaptation to our context will be a key ingredient in the soundness proof in Sect. 4.

The memoization technique

Although the name comes from machine-learning [START_REF] Michie | Memo" Functions and Machine Learning[END_REF], this technique is usually attributed to S. A. Cook and has provided fundamental as well as practical results. In the specific case of automata with stack, it can be condensed in the following remark: if at a given time you are in state q with b on top of a stack of height h 1 , and if you end up later on in the state q with some symbol b on top of a stack of height h , without having popped a symbol at height inferior to h, and if you are about to pop this symbol, then you can save this progression (q, b) → (q , b ). If later on you find yourself in the same state q, with b on top of your stack and with the heads in the same positions, you can directly skip to the saved progression, as there is no need to perform this part of the computation again. This "partial information", the description of your automaton without the contents of the stack, apart from its top symbol, is sometimes called "surface configuration" or "partial identifier".

The memoization technique consists in building and using the transitive closure of the relation between surface configuration. Differently expressed, memoization is a "clever evaluation strategy, applicable whenever the results of certain computations are needed more than once" [2, p. 348]. One looking for subtle refinements could look for a technique of memoization computed independently from the input, allowing to "compile" a stack program into equivalent online memoizing program [START_REF] Andersen | Generalizing Cook's Transformation to Imperative Stack Programs[END_REF] that runs exponentially faster. A nice explanation in the case of single head automata can be found in a recent and short article by R. Glück [START_REF] Glück | Simulation of Two-Way Pushdown Automata Revisited[END_REF].

We will be adapting this idea to our context in Sect. 4.1, which will amount to a form of exponentiation by squaring.

Encoding 2MFA+S as Observations: Ptime Completeness

The encoding proposed below is similar to the previously developed [START_REF] Aubert | Logic Programming and Logarithmic Space[END_REF]Sect. 4.1] encoding of 2-way k -head finite automata (without pushdown stack) by flows. The only difference is the addition of a "plug-in" that allows for a representation of stacks in observations. Remember that acceptance by observations is phrased in terms of nilpotency of the product O Wp of the observation and the representation of the input (Definition 2.13). Hence the Inria computation in this model is defined as an iteration: one computes by considering the sequence O Wp , (O Wp ) 2 , (O Wp ) 3 , . . . and the computation either ends at some point (i.e. accepts) -that is (O Wp ) n = 0 for some integer n -or loops (i.e. rejects). One can think of this iteration as representing a dialogue, or a game, between the observation and its input.

We turn now to the proof of Ptime-completeness for the set of balanced observations with stacks.

Proof

The proof relies on encoding a 2MFA+S(k) M that recognizes L -whose existence is ensured by Theorem 3.2 -as an observation of O b+s . Taking A = Σ the input alphabet, k + 1 the number of heads of the automaton, we will encode the transition relation of M as a balanced observation with stack. More precisely, the automaton will be represented as an element

O M of O b+s = O[ Stack • R b ]
which can be written as a sum of flows of the form

c • d • σ(x) • q • aux k (y 1 , . . . , y k ) • head(z ) c • d • s(x) • q • aux k (y 1 , . . . , y k ) • head(z) with • c, c ∈ Σ ∪ { } , • d, d ∈ {l, r},
• σ a finite sequence of unary function symbols,

• s a unary function symbol,

• q, q two constant symbols,

• aux k , head functions symbols of respective arity k and 1.

The intuition behind the encoding is that a configuration of a 2MFA+S(k + 1) processing an input can be seen as a closed term

c • d • τ ( ) • q • aux k (p i1 , . . . , p i k ) • head(p j )
where the p i are position constants representing the positions of the main pointer (head(p j )) and of the auxiliary pointers (aux k (p i1 , . . . , p i k )); the symbol q represents the state the automaton is in; τ ( ) represents the current stack; the symbol d represents the direction of the next move of the main pointer; the symbol c represents the symbol currently read by the main pointer. When a configuration matches the right side of the flow, the transition is followed, leading to an updated configuration.

More precisely, we will be encoding M as an observation O M , and observe the iterations of O M Wp , its product with a word representation. Let us explain how the basic operations of M are encoded: Moving the pointers. Looking back at the definition of the encoding of words (Definition 2.10), we see that we can have a new reading of what the representation of a word does: it moves the main pointer in the required direction. From that perspective, the position holding the symbol in Definition 2.10 allows to simulate the behavior of the endmarkers and . On the other hand, the observation is not able to manipulate the position of pointers directly (remember observations are forbidden to use the position constants) but can change the direction symbol d , rearrange pointers (hence changing which one is the main pointer) and modify its state and the symbol c accordingly. For instance, a flow of the form

• • • • aux k (x, . . . , y k ) • head(y 1 ) • • • • aux k (y 1 , . . . , y k ) • head(x)
encodes the instruction "swap the main pointer and the first auxiliary pointer". Note however that our model has no built-in way to remember the values of the auxiliary pointers -it remembers only their positions as arguments of aux k (• • • ) -, but this can be implemented easily using additional states.

One can see that it is the interaction between the observation O M and the word representation Wp that simulates the behavior of the automaton, and not the observation on its own manipulating some passive data. Handling the stack. Suppose we have a unary function symbol b(•) for each symbol b of the stack alphabet B .

A transition that reads b and pops it is simply written as

• • • • x • • • • • • • • b(x) • • • •
A transition that reads b and pushes a symbol c is written

• • • • c(b(x)) • • • • • • • • b(x) • • • •
Changing the state. We suppose that we have a constant q for each state q of M . Then, updating the state amounts to picking the right q and q in the flow representing the transition. Acceptance and rejection. The encoding of acceptance and rejection is slightly more delicate, as detailed in a previous article [6, p. 6.2.3.]. The basic idea is that acceptance in our model is defined as nilpotency, that is to say: the absence of loops. If no transition in the automaton can be fired, then no flow in our encoding can be unified, and the computation ends.

Conversely, a loop in the automaton will refrain the wiring from being nilpotent. The point we need to be careful about is the encoding of loops: those should be represented as a re-initialization of the computation, as discussed in details in earlier work [START_REF] Aubert | Characterizing co-NL by a group action[END_REF]. The reason for this is that another encoding may interfere with the representation of acceptation as termination: the existence of a loop in the observation O M representing the automaton M , even one that is not used in the computation with the input W , prevents the wiring O M Wp from being nilpotent. Indeed, the "loop" in Definition 3.1 of 2MFA+S is to be read as "perform forever the same computation".

Notice that the encoding of pushdown automata as observations with stacks produces only specific observations, namely those that are sums of flows of a particular form (shown at the beginning of the preceding proof). This is due to the fact that one encodes the transitions directly, so that each flow corresponds to a transition step.

In particular, as the transition relation of automata depends only on the top of the stack, the body (i.e. the right-hand part) of the flows must be of the form

• • • • b(x) • • • • .
However, a general observation with stack is not constrained in this way, and allows a more compact representation of programs where one can read, pop and push several symbols of the stack simultaneously.

Nevertheless, this does not increase the expressive power: the next section is devoted to prove that the language recognized by any observation with stack lies in Ptime. We now introduce the saturation technique, which allows to decide nilpotency of Stack elements in polynomial time. This technique relies on the fact that under certain conditions, the height of flows does not grow when computing their product. It adapts memoization to our setting: we repeatedly extend the wiring by adding pairwise products of flows, allowing for more and more "transitions" at each step. Notation 4.1. Let τ and σ be sequences of unary function symbols.

If h τ (x) ≥ h σ(x) we say that op τ, σ is increasing.

If h τ (x) ≤ h σ(x)
we say that op τ, σ is decreasing.

A wiring in Stack is increasing (resp. decreasing) if it contains only increasing (resp. decreasing) stack operations. Lemma 4.2 (stability of height). Let f = op τ, σ and g = op ρ, χ be stack operations. If f is decreasing and g is increasing, we have h(f g) ≤ max{h(f ), h(g)} .

Proof

If f g = 0 , the property holds because h (0) = 0 . Otherwise, we have either σ = ρµ or σµ = ρ .

Suppose we are in the first case (the second being symmetric). Then we have f g = op τ, χµ and h (σ) = h (ρµ) .

As g is increasing, h (χ) ≤ h (ρ) and therefore we have

h (χµ) ≤ h (ρµ) = h (σ) ≤ h (f ) ≤ max{h (f ), h (g)} .
With this lemma in mind, we can define a shortcut operation that augments an element of Stack by adding new flows while keeping the maximal height unchanged. Iterating this operation, we obtain a saturated version of the initial wiring, containing shortcuts, shortcuts of shortcuts, etc.

We are designing in fact an exponentiation by squaring procedure for elements of Stack , the algebraic reading of memoization.

Definition 4.3 (saturation). If F ∈ Stack we define its increasing F

↑ := {f ∈ F | f is increasing} and decreasing F ↓ := { f ∈ F | f is decreasing } subsets.
We set the shortcut operation short(F ) := F + F ↓ F ↑ and its least fixpoint, which we call the saturation of F :

satur(F ) := n∈N short n (F )
where short n denotes the n th iteration of short. Now, as we are only manipulating flows with a limited height, the iteration of the shortcut operation is bound to stabilize at some point. For any n , we have

h short n (F ) = h(F ) . Moreover if n ≥ (S h(F ) + S h(F )-1 + • • • + 1) 2 then short n (F ) = satur(F ) .
The rewriting terminates as step 1 strictly reduces the length of the sequence and step 2 can never be applied twice in a row (it can be applied only when step 1 is impossible and its application makes step 1 possible). Let g 1 , . . . , g n be the resulting sequence, as it cannot be reduced, the g i must be either all increasing or all decreasing. Therefore, by the invariants above g 1 , . . . , g n is either a sequence of elements of satur (F ) ↓ or satur (F ) ↑ such that the product g 1 • • • g n is a cycle.

Finally, we need a way to decide cyclicity of elements of Stack that are either increasing or decreasing.

Lemma 4.9. Given any integer h , there is a procedure Incr h (•) ∈ Ptime that, given an element F ∈ Stack which is either increasing or decreasing and satisfying h(F ) ≤ h as an input, accepts iff F is nilpotent.

Proof

Let S be a set of function symbols and h an integer. We define the truncation wiring associated to S and h T h,S :=

τ =f1, ... ,f h ∈S τ ( ) τ (x)
and set for the rest of the proof T := T h (F ),E where E is the set of function symbols occurring in F . As it contains only flows of the form τ ( ) σ(x), i.e. with only one variable, T F is balanced and can be computed in polynomial time since T is of polynomial size in |F | .

If F is increasing, an easy computation shows that we have (T F ) n = T F n . From this, we deduce that

F is nilpotent iff T F is. If F = i σ i (x) τ i (x) is decreasing, we can consider F † := i τ i (x) σ i (x)
which is increasing and nilpotent iff F is. Then, as we know [5, p. 54], [9, Theorem IV.12] the nilpotency problem for balanced wirings to be in co-NLogspace ⊆Ptime, we are done. Theorem 4.10 (nilpotency is in Ptime). Given any integer h , there is a procedure Nilp h (•) ∈ Ptime that, given a F ∈ Stack such that h(F ) ≤ h as an input, accepts iff F is nilpotent.

Proof

Simply take Nilp h (•) = Incr h (Satur h (•)). By compositionality of Ptime and FPtime algorithms, this procedure is in Ptime . Remark 4.11. All the results we gave in this section are parametrized by a height limit h, but this is only to ease the presentation. Indeed, it is possible to transform any element of Stack with an unspecified height into another element of comparable size but of height at most 2 , preserving its nilpotency.

More precisely: consider a flow l = σ(x) τ (x) , with σ = f 1 , . . . , f m and τ = g 1 , . . . , g n . Let us introduce new function symbols l pop i (•) and l push j (•) for 1 ≤ i ≤ m and 1 ≤ j ≤ n . We can rewrite l as the sum

g 1 (x) l push 1 (x) + l push 1 (g 2 (x)) l push 2 (x) + • • • • • • + l push n (x) l pop 1 (x) + • • • • • • + l pop m-1 (x) l pop m (f m-1 (x)) + l pop m (x) f m (x)
with the idea that instead of popping and pushing several symbols at the same time, we do this step by step: we push/pop only one symbol and then leave a marker (either l pop i (•) or l push j (•)) for the next operation to be performed. Moreover, we see that this flow of size (Definition 4.5) |l| = m + n is transformed in a wiring containing three flows of size 2 (the central and two extremal ones) and (m -1) + (n -1) flows of size 3; hence the sum has size 3|l|.

When dealing with a wiring W , we can do the same by considering one family of l pop i (•) and l push j (•) symbols for each flow l of W . It is not hard to see that the resulting wiring W flat has the same behavior as the original one in terms of nilpotency. It is also clear that the height of W flat is indeed 2 . Finally, if we started with a wiring W of size N , which is the sum of the sizes of the flows in it, we get in the end that |W flat | = 3|W | using the one-flow case above.

This suggests by the way that the bound in Proposition 4.4 is probably too rough, but a way to sharpen it still needs to be found.

Ptime Soundness

We will now use the saturation technique to prove that the language recognized by an observation with stack belongs to the class Ptime. The important point in the proof is that, given an observation O and a representation Wp of a word W , one can produce in polynomial time an element of Stack whose nilpotency is equivalent to the nilpotency of O Wp . One can then decide the nilpotency of this element thanks to the procedure described in the previous section. Proposition 4.12. Let O ∈ O b+s be an observation with stack. There is a procedure Red O (•) ∈ FPtime that, given a word W as an input, outputs a wiring F ∈ Stack with h(F ) ≤ h(O) such that F is nilpotent iff O Wp is for any choice of p.

Proof (sketch [9, proposition IV.21])

The idea is that the product O Wp can be seen as an element of R b • Stack . Then, its balanced part can be replaced in polynomial time by closed terms without altering the nilpotency in a way similar to what is done to treat the nilpotency of elements of R b [START_REF] Aubert | Logic Programming and Logarithmic Space[END_REF].

We are left with a flow

i t i • σ i (x) u i • τ i (x) such that t i u i is balanced and σ i (x)
τ i (x) is a stack operation, and we can associate to each closed t i , u i , unary function symbols t i (•), u i (•) , and rewrite our flow as i t i (σ i (x))

u i (τ i (x)) ∈ Stack .

Unary Logic Programming

In previous sections, we showed how the Stack semiring captures polynomial time computation. As we already mentioned, the elements of this semiring correspond to a specific class of logic programs.

We cover in here the consequences in terms of logic programming of the results and techniques introduced so far. The basic definitions and a list of previously known results -that highlight the novelty of our result -regarding logic programming can be found in an extensive survey [START_REF] Dantsin | Complexity and expressive power of logic programming[END_REF].

As an illustration, we show in Sect. 5.2 how the classical boolean circuit value problem (CVP) [START_REF] Ladner | The circuit value problem is log space complete for P[END_REF] can be encoded as a unary logic program, thus providing an alternative proof of its inclusion in Ptime .

Unary Queries

Definition 5.1 (data, goal, query). A unary query is a triple Q = (D, P, G), where: Inria • that in t u the variables of t does not appear in u ;

• constants in the program part of the query.

A harder question is whether everything scales up to logic programs of the form H B 1 , . . . , B n , with more than one formula on the right of . Indeed we would no longer have obvious notions of increasing or decreasing (Notation 4.1) clause anymore, and these are crucial to the saturation technique. It is already known [20, pp. 386-387] that in the case of propositional (i.e. with no variables) logic programming, allowing more than one B i makes the combined complexity (see Remark 5.8 below) switch from Logspace to Ptime: one can expect by analogy a higher complexity than Ptime in our unary case, but nothing has been proven yet.

Remark 5.8. In terms of complexity of logic programs, we are considering the combined complexity [20, p. 380]: every part of the query Q = (D, P, G) is variable. If for instance we fixed P and G (thus considering data complexity), we would have a problem that is still in Ptime, but it is unclear to us if it would be complete. Indeed, the encoding of Sect. 3.2 relies on a representation of inputs as plain programs, and on the fact that the evaluation process is a matter of interaction between programs rather than mere data processing.

Circuit Value Problem

To illustrate our point in the introduction about rephrasing a problem with unary symbols to tell whether it lies in Ptime, we present an encoding of the classical Ptime-complete circuit value problem (CVP) [START_REF] Dantsin | Complexity and expressive power of logic programming[END_REF] as a unary query. An instance of CVP is a boolean circuit composed of and, or, not, 0 and 1 gates and is accepted if the circuit computes the value 1 at its output gate.

More

:= a(b(x)) c(x) + a(x) c(x) + b(x) c(x) [a, b or c] := a(x) c(x) + b(x) c(x) + a(b(x)) c(x) [a not b] := a(x) b(x) + a(x) b(x) [ 0 a] := x a(x) [ 1 a] := x a(x)
The intuition behind this encoding is that we are handling a stack of needed values, v(•) (resp. v(•)) meaning "we need the value 1 (resp. 0) at v ". The flows associated to gates are then meant to handle this stack, popping and pushing needed values.

Then, to a circuit (G, o) we associate the unary query

o( ) , e vertex of G [e] ,
This query succeeds iff the circuit computes the value 1 at the gate o: the data o( ) initiates a stack with the intuitive meaning "we need the value 1 at o ", the encodings of edges propagate the needed values to the point where they can be "popped" if the correct 0 x or 1 x is available. The query succeeds if we can derive the goal -i.e. the empty stack -with the intuitive meaning "all the needed values have been provided".

Note the parallel nature of this way of solving the problem: when we compute the saturation of (the encoding of) the query, we unify the terms that match at any point of the circuit without having to worry in which order we perform the operations.

For instance, the two elements a Finally, let us say a word about the stabilization time of satur (•) (Definition 4.3) in this case. Given a circuit with S gates, we are dealing with flows of height at most 2 , written with at most S different symbols. In view of Proposition 4.4 we have that the iterations of short (•) will stabilize in at most (S 2 + S + 1) 2 steps. A bound that is rough, due the absence of optimization and fine-grained analysis of the procedure.

Perspectives

This article extends modularly on our previous approaches [START_REF] Aubert | Characterizing co-NL by a group action[END_REF][START_REF] Aubert | Logarithmic Space and Permutations[END_REF][START_REF] Aubert | Unification and Logarithmic Space[END_REF][START_REF] Aubert | Logic Programming and Logarithmic Space[END_REF] to obtain a characterization of Ptime, by adding a sort of "stack plugin" to observations. This enhancement was guided by the intuition of a stack added to an automaton, allowing to move from Logspace to Ptime and providing a decisive proof technique: memoization.

We saw that to a qualitative constraint on the way memory is handled by automata corresponds a syntactical restriction on flows. These flows are evaluated in a setting inspired by the representation of inputs in the interactive approach to the Curry-Howard correspondencegeometry of interaction -, which makes the complexity parametric in the program and the input. However, despite the evaluation being highly parallel and different from the step-by-step evaluation performed by automata, a precise simulation of pushdown automata by unary logic program is given, leading to complexity results.

We were able to adapt the mechanism of pre-computation of transitions, known as memoization, in a setting where logic programs are represented as algebraic objects. This technique -that we called the saturation technique -computes shortcuts in a logic program in order to decide its nilpotency faster. This approach to complexity was earlier based on von Neumann algebras [START_REF] Girard | Normativity in Logic[END_REF][START_REF] Aubert | Characterizing co-NL by a group action[END_REF][START_REF] Aubert | Logarithmic Space and Permutations[END_REF] and now explore unification theory [START_REF] Bagnol | On the Resolution Semiring[END_REF][START_REF] Aubert | Unification and Logarithmic Space[END_REF][START_REF] Aubert | Logic Programming and Logarithmic Space[END_REF]: it is emerging as a meeting point for computer science, logic and mathematics. This raises multiple questions and perspectives.

A number of interrogations come from the relations of this work to proof theory. First, we could consider the Church encoding of other data types -trees for instance -and define "orthogonally" set of programs interacting with them, wondering what is their computational nature. In the distance, one may hope for a connection between our approach and ongoing work on higher order trees and model checking; all alike, one could study the interaction between observations and one-way integers -briefly discussed in earlier work [START_REF] Aubert | Logic Programming and Logarithmic Space[END_REF] -or non-deterministic data. Second, a still unanswered question of interest is to give an account of observations in terms of a proof-system.

One could also investigate possible relations with other models of computation, such as the interaction abstract machine [START_REF] Danos | Reversible, Irreversible and Optimal lambda-Machines[END_REF] that already developed and used -although with a different, much more logical, meaning -the notion of shortcut in the evaluation.

Finally, we also aim at representing functional computation, by considering a more general notion of observation that would allow for expressing the notion of output.

Theorem 2 .

 2 12 (normativity). Let Wp and Wq be two representations of a word W and O an observation. Then Nil(O Wp ) if and only if Nil(O Wq ).

Definition 2 .

 2 15 (balanced observation). A balanced observation is an element of O[ R b • R b ]. This natural restriction was shown to characterize logarithmic space computation [5, Theorems 34-35]. Inria Theorem 2.16 (balance and logarithmic space). If O is a balanced observation, then L(O) ∈ co-NLogspace . If L ∈ co-NLogspace then there exists a balanced observation such that L(O) = L .

Finally, let us

  define a new class of observations, based on the Stack semiring. Definition 2.27. A balanced observation with stack is an element of O b+s := O[ Stack • R b ] . Inria 3 Pushdown Automata and Ptime Completeness 3.1 Characterization of Ptime by Pushdown Automata

•

  andare the left and right endmarkers, , / ∈ A;• is the bottom symbol of the stack, / ∈ B ;• σ is the transition relation, i.e. a subset of the product (S×(A }) k ×B )×(S×{-1, 0, +1} k × {pop, push(b)}) where A (resp. B ) denotes A ∪ { , } (resp. B ∪ { } ). The instruction -1 corresponds to moving the head one cell to the left, 0 corresponds to keeping the head on the current cell and +1 corresponds to moving it one cell to the right. Regarding the pushdown stack, the instruction pop means "erase the top symbol", while, for all b ∈ B , push(b) means "write b on top of the stack".

Theorem 3 . 3 .

 33 If L ∈ Ptime , then there exists a balanced observation with stack O ∈ O b+s such that L = L(O) .

Inria

4

  Nilpotency in Stack and Ptime soundness 4.1 The Saturation Technique

Proposition 4 . 4 (

 44 stability of saturation). Let F ∈ Stack be a wiring and S the number of distinct function symbols appearing in F .

Theorem 4 .

 4 13 (soundness). If O ∈ O b+s is an observation with stack, then L(O) ∈ Ptime .ProofWe have, using the compositionality of Ptime and FPtime again, that Nilp h (O) (Red O (•)) is a decision procedure in Ptime for L(O) .

b or c a not b 0 a 1 a

 1 formally, we can see an instance of CVP as (G, o) with G an acyclic directed hypergraph 5 with a distinguished output vertex o built with edges among a, b and c a, such that any vertex is the target of exactly one edge. First, we associate to each vertex v of the graph a pair v(•), v(•), of unary function symbols. Then to each edge e we associate a flow [e] as follows: [a, b and c]

  (x) o( ) and b(x) o( ) of [a, b or o( )] would be unified with o( ) , providing two flows a(x) and b(x) . Those flows would be, at the next execution step, tested for unification against all (provided we respect the increasing/decreasing discipline at work in Definition 4.3) the other flows and so on, without having to wait to know whether a or b will hold the value 1 . A partial evaluation happens at any point of the graph, independently of the input: [a, b and c] and [c not d] will give after one step of evaluation the flows a(b(x)) d(x), a(x) d(x) and b(x) d(x). The execution does not have to sequentially wait for the propagation of the needed values.

We mean extensional correspondence: they compute the same functions.RR n°8796

More precisely, 2 -way k -head non-deterministic finite automata with pushdown stack. See Sect.

3.1.1. Inria

RR n°8796

A semiring is a set R equipped with two operations + (the sum) and × (the product, whose symbol is usually omitted), and an element 0 ∈ R such that: (R, +, 0) is a commutative monoid; (R, ×) is a semigroup, i.e. a monoid which may not have a neutral element; the product distributes over the sum; the element 0 is absorbent: 0r = r0 = 0 for all r ∈ R . Inria

Note that the cardinality of s is not necessarily equal to the length of s . For instance, ifs = f 1 , f 1 , f 2 with f 1 = f 2 then Card( s) = 2 . RR n°8796

A directed hypergraph is given as a set of vertices V and a set of edges E ⊆ P(V ) × P(V ) . We say that (S, T ) ∈ E is an edge from S to T .We consider labeled edges and write x1, . . . , xn k y1, . . . , ym an edge labeled by k from { x 1 , . . . , xn } to { y 1 , . . . , ym } . Inria

† This work was partly supported by the ANR-11-INSE-0007 REVER, the ANR-10-BLAN-0213 Logoi and the ANR-11-BS02-0010 Récré.

Proof

By Lemma 4.2 we have

Therefore h short (F ) = h (F ) , and we get the first property by induction. For any n , the elements of short n (F ) are stack operations of height at most h (F ) built from the function symbols appearing in F , therefore short n (F ) is a subset of a set of cardinality k := (S h (F ) + S h (F )-1 + • • • + 1) 2 . As G ⊆ short (G) for all G , the iteration of short (•) on F must be stable after at most k steps.

In the following, we let FPtime be the class of functions computable by Turing machine in polynomial time. Here we need to specify how the size of a wiring is measured. By computing the fixpoint of short (•) we have first a FPtime procedure computing the saturation.

Corollary 4.6 (computing the saturation). Given any integer h , there is procedure Satur h (•) ∈ FPtime that, given an element F ∈ Stack such that h(F ) ≤ h as an input, outputs satur(F ) .

Moreover, we can obtain a further reduction of the nilpotency problem in Stack related to saturation.

Lemma 4.7 (rotation). Let f and g be stack operations. Then f g is a cycle iff gf is a cycle.

Proof

If f g is a cycle, then (f g) n = 0 for any n by Proposition 2.23. In particular (f g) 3 = 0 and as we have (f g) 3 = f (gf )(gf )g we get (gf ) 2 = 0, i.e. gf is a cycle.

Proof

The cyclicity of satur (F ) ↑ or satur (F ) ↓ obviously implies that of

Conversely, suppose F is cyclic and let s = f 1 , . . . , f n ∈ F be such that the product p ( s) ∈ F n is a cycle.

We are going to produce from s a sequence of elements of satur (F ) ↑ or satur (F ) ↓ whose product is a cycle. For this we apply to the sequence the following rewriting procedure:

1. If there are f i and f i+1 such that f i is decreasing and f i+1 is increasing, then rewrite s as f 1 , . . . , f i f i+1 , . . . , f n .

2. If step 1 does not apply and s = s 1 s 2 ( s 1 and s 2 both non-empty) with all elements of s 1 increasing and all elements of s 2 decreasing, then rewrite s as s 2 s 1 .

This rewriting procedure preserves the following invariants:

• All elements of the sequence are in satur (F ) : step 2 does not affect the elements of the sequence (only their order) and step 1 replaces the flows f i ∈ satur (F ) ↓ and f i+1 ∈ satur (F ) ↑ by f i f i+1 ∈ satur (F ).

• The product p ( s) of the sequence is a cycle: step 1 does not alter p ( s) and step 2 does not alter the fact that p ( s) is a cycle by Lemma 4.7.

Inria

• D is a set of closed unary terms (a unary data),

• P is a an element of Stack (a unary program),

• G is a closed unary term (a unary goal).

We say that the query Q succeeds if G can be derived combining d for d ∈ D and the elements of P by the resolution rule exposed in Sect. 2.1, otherwise we say the query fails.

The size |Q| of the query is defined as the total number of occurrences of symbols in it.

To apply the saturation technique directly, we need to represent all the elements of the unary query (data, program, goal) as elements of Stack . This requires an encoding.

Definition 5.2 (encoding unary queries). We suppose that for any constant symbol c , we have a unary function symbol c(•) . We also need two unary functions, START(•) and ACCEPT(•) .

To any unary data D we associate an element of Stack :

and to any unary goal G = τ (c) we associate

Remark 5.3. The program part P of the query needs not to be encoded as it is already an element of Stack .

Once a query is encoded, we can tell if it is successful or not using the language of the resolution semiring.

Proof

The lemma above, combined with Corollary 4.6, ensures that the problem lies indeed in the class Ptime, modulo the considerations on the height of Remark 4.11.

The hardness part follows from a variation on the encoding presented in Sect. 3.2 and the reduction derived from Proposition 4.12.

Remark 5.7. We presented the result in a restricted form, to stay in line with the previous sections. However, it should be clear to the reader that this construction would not be impacted if we allowed

• non-closed goals and data; RR n°8796