Clément Aubert

Marc Bagnol

Paolo Pistone

Thomas Seiller

Logic Programming and Logarithmic Space

Keywords: Implicit Complexity, Unification, Logic Programming, Logarithmic Space, Proof Theory, Pointer Machines, Geometry of Interaction, Automata

ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Proof Theory and Implicit Computational Complexity. Very generally, the aim of implicit computational complexity (ICC) is to describe complexity classes with no explicit reference to cost bounds: through a type system or a weakened recursion scheme for instance. The last two decades have seen numerous works relating proof theory (more specifically linear logic [START_REF] Girard | Linear logic[END_REF]) and ICC, the basic idea being to look for restricted substructural logics [START_REF] Girard | Light linear logic[END_REF] with an expressiveness that corresponds exactly to some complexity class.

This has been achieved by various syntactic restrictions, which entail a less complex 3 cut-elimination procedure: control over the modalities [START_REF] Schöpp | Stratified bounded affine logic for logarithmic space[END_REF][START_REF] Dal Lago | Bounded linear logic, revisited[END_REF], type assignments [START_REF] Gaboardi | An implicit characterization of pspace[END_REF] or stratification properties [START_REF] Baillot | Linear logic by levels and bounded time complexity[END_REF], to name a few.

Geometry of Interaction.

In recent years, the cut-elimination procedure and its mathematical modeling has become a central topic in proof theory. The aim of the geometry of interaction research program [START_REF] Girard | Geometry of interaction 1: Interpretation of system F[END_REF] is to provide the tools for such a modeling [START_REF] Asperti | Paths in the lambda-calculus[END_REF][START_REF] Laurent | A token machine for full geometry of interaction (extended abstract)[END_REF][START_REF] Seiller | Interaction graphs: Multiplicatives[END_REF].

As for complexity theory, these models allow for a more synthetic and abstract study of the resources needed to compute the normal form of a program, leading to some complexity characterization results [START_REF] Baillot | Elementary complexity and geometry of interaction[END_REF][START_REF] Girard | Normativity in logic[END_REF][START_REF] Aubert | Unification and logarithmic space[END_REF].

Unification. Unification is one of the key-concepts of theoretical computer science: it is a classical subject of study for complexity theory and a tool with a wide range of applications, including logic programming and type inference algorithms.

Unification has also been used to build syntactic models of geometry of interaction [START_REF] Girard | Geometry of interaction III: accommodating the additives[END_REF][START_REF] Baillot | Elementary complexity and geometry of interaction[END_REF][START_REF] Girard | Three lightings of logic[END_REF] where first-order terms with variables allow for a manipulation of infinite sets through a finite language.

Logic Programming. After the work of Robinson [START_REF] Robinson | A machine-oriented logic based on the resolution principle[END_REF] on the resolution procedure, logic programming has emerged as a new computation paradigm with concrete realizations such as the languages Prolog and Datalog.

On the theoretical side, constant efforts have been provided to clarify expressiveness and complexity issues [START_REF] Dantsin | Complexity and expressive power of logic programming[END_REF]: most problems arising from logic programming are undecidable in their most general form and some restrictions must be introduced in order to make them tractable. For instance, the notion of finitely ground program [START_REF] Calimeri | Computable functions in ASP: Theory and implementation[END_REF] is related to our approach.

Pointer Machines. Multi-head finite automata provide an elegant characterization of logarithmic space computation, in terms of the (qualitative) type of memory used rather than the (quantitative) amount of tape consumed. Since they can scan but not modify the input, they are usually called "pointer machines", even if this nomenclature can be misleading [START_REF] Ben-Amram | What is a "pointer machine[END_REF].

This model was already at the heart of previous works relating geometry of interaction and complexity theory [START_REF] Girard | Normativity in logic[END_REF][START_REF] Aubert | Characterizing co-nl by a group action[END_REF][START_REF] Aubert | Unification and logarithmic space[END_REF]. Contribution and Outline. We begin by exposing the idea of relating geometry of interaction and logic programming, already evoked [START_REF] Girard | Geometry of interaction III: accommodating the additives[END_REF] but never really developed, and by recalling the basic notions on unification theory needed for this article and some related complexity results.

We present in Sect. 2 the algebraic tools used later on to define the encoding of words and pointer machines. Section 2.2 and Sect. 2.3 introduce the syntactical restriction and associated tools that allow us to characterize logarithmic space computation. Note that, compared to earlier work [START_REF] Aubert | Unification and logarithmic space[END_REF], we consider a much wider class of programs while preserving bounded space evaluation: we switch from representation of permutations to a class defined by a syntactical restriction on height of variables, which contains permutations as a strict subset.

The encoding of words enabling our results, which comes from the classical (Church) encoding of lists in proof theory, is given in Sect. 3. It allows to define the counterpart of programs, and a notion of acceptance of a word by a program. Finally, Sect. 4 makes use of the tools introduced earlier to state and prove our complexity results. While the expressiveness part is quite similar to earlier presentations [START_REF] Aubert | Characterizing co-nl by a group action[END_REF][START_REF] Aubert | Unification and logarithmic space[END_REF], the proof that acceptance can be decided within logarithmic space has been made more modular by reducing this problem to the standard problem of cycle search in a graph.

Geometry of Interaction and Logic Programming

The geometry of interaction program (GoI), started in 1989 [START_REF] Girard | Towards a geometry of interaction[END_REF], aims at describing the dynamics of computation by developing a fully mathematical model of cut-elimination. The original motivations of GoI must be traced back, firstly, to the Curry-Howard correspondence between sequent calculus derivations and typed functional programs: it is on the basis of this correspondence that cut-elimination had been proposed by proof-theorists as a paradigm of computation; secondly, to the finer analysis of cut-elimination coming from linear logic [START_REF] Girard | Linear logic[END_REF] and the replacement of sequent calculus derivations with simpler geometrical structures (proof-nets), more akin to a purely mathematical description.

In the first formulation of GoI [START_REF] Girard | Geometry of interaction 1: Interpretation of system F[END_REF], derivations in second order intuitionistic logic LJ 2 (which can be considered, by Curry-Howard, as programs in System F) are interpreted as pairs (U, σ) of elements (called wirings) of a C * -algebra, U corresponding to the axioms of the derivation and σ to the cuts.

The main property of this interpretation is nilpotency, i.e. if there exists an integer n such that (σU ) n = 0. The cut-elimination (equivalently, the normalization) procedure is then interpreted by the application of an execution operator

EX(U, σ) = k (σU ) k
From the viewpoint of proof theory and computation, nilpotency corresponds to the strong normalization property: the termination of the normalization procedure with any strategy.

Several alternative formulations of geometry of interaction have been proposed since 1989 (see for instance [START_REF] Asperti | Paths in the lambda-calculus[END_REF][START_REF] Laurent | A token machine for full geometry of interaction (extended abstract)[END_REF][START_REF] Seiller | Interaction graphs: Multiplicatives[END_REF]); in particular, wirings can be described as logic programs [START_REF] Girard | Geometry of interaction III: accommodating the additives[END_REF][START_REF] Baillot | Elementary complexity and geometry of interaction[END_REF][START_REF] Girard | Three lightings of logic[END_REF] made of particular clauses called flows, which will be defined in Sect. 2.1.

In this setting the resolution rule induces a notion of product of wirings (Definition 8) and in turn a structure of semiring: the unification semiring U, which can replace the C * -algebras of the first formulations of GoI. 4The EX(.) operator of wirings can be understood as a way to compute the fixed point semantics of logic programs. The nilpotency property of wirings means then that the fixed point given by EX(.) is finite, which is close to the notion of boundedness5 [START_REF] Dantsin | Complexity and expressive power of logic programming[END_REF] of logic programs.

In definitive, from the strong normalization property for intuitionistic second order logic (or any other system which enjoys a GoI interpretation), one obtains through the GoI interpretation a family of bounded (nilpotent) logic programs computing the recursive functions typable in System F. This is quite striking in view of the fact that to decide whenever a program is bounded is -even with drastic constraints -an undecidable problem [START_REF] Hillebrand | Undecidable boundedness problems for datalog programs[END_REF], and that in general boundedness is a property that is difficult to ensure.

Unification and Complexity

We recall in the following some notations and some of the numerous links between complexity and unification, and by extension logic programming.

Notation. We consider a set of first-order terms T, assuming an infinite number of variables x, y, z, . . . ∈ V, a binary function symbol • (written in infix notation), infinitely many constant symbols a, b, c, . . . including the (multipurpose) dummy symbol and, for any n ∈ N * , at least one n-ary function symbol A n .

Note that the binary function symbol • is not associative. However, we will write it by convention as right associating to lighten notations:

t • u • v := t•(u • v).
For any t ∈ T, we write Var(t) the set of variables occurring in t (a term is closed when Var(t) = ∅) and h(t) the height of t: the maximal distance from the root to any leaf in the tree structure of t.

The height of a variable occurrence in a term t is its distance from the root in the tree structure of the term. A substitution θ is a mapping from variables to terms such that xθ = x for all but finitely many x ∈ V. A renaming is a substitution α mapping variables to variables and that is bijective. A term t is a renaming of t if t = tα for some renaming α. A fundamental result [START_REF] Robinson | A machine-oriented logic based on the resolution principle[END_REF] of the theory of unification is that two unifiable terms indeed have a MGU and that it can be computed.

More specifically, the problem of deciding whether two terms are unifiable is Ptime-complete [12, Theorem 1], which implies that parallel algorithms for this problem do not improve much on serial ones. Finding classes of terms where the MGU research can be efficiently parallelized is a real challenge.

It has been proven that this problem remains Ptime-complete even if the arity of the function symbols or the height of the terms is bounded [27, Theorems 4.2.1 and 4.3.1], if both terms are linear or if they do not share variables [START_REF] Dwork | On the sequential nature of unification[END_REF][START_REF] Dwork | Parallel algorithms for term matching[END_REF].

More recently [START_REF] Bellia | N-axioms parallel unification[END_REF], an innovative constraint on variables helped to discover an upper bound of the unification classes that are proven to be in NC.

Regarding space complexity, the result stating that the matching problem is in DLogspace [START_REF] Dwork | On the sequential nature of unification[END_REF] (recalled as Theorem 36) will be used in Sect. 4.2.

The Unification Semiring

This section presents the technical setting of this work, the unification semiring: an algebraic structure with a composition law based on unification, that can be seen as an algebraic presentation of a fragment of logic programming.

Flows and Wirings

Flows can be thought of as very specific Horn clauses: safe (the variables of the head must occur in the body) clauses with exactly one atom in the body.

As it is not relevant to this work, we make no technical difference between predicate symbols and function symbols, for it makes the presentation easier. Anyway, to retrieve the connection with logic programming, simply assume a class of function symbols called "predicate symbols" (written in boldface) that can only occur at the root of a term.

Definition 2 (flows).

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

An example of flow that indeed is a clause of logic programming would be for instance colored(x) blue(x) which states that if x is blue, then it is colored. Facts, which are usually defined as ground (using only closed terms) clauses with an empty body, can still be represented as a special kind of flows.

Definition 3 (facts).

A fact is a flow of the form t .

Remark 4. Note that this implies that t is closed. Following on the example above, blue(c) would be the fact stating that the object c is blue.

The main interest of the restriction to flows is that it yields an algebraic structure: a semigroup with a partially defined product.

Definition 5 (product of flows). Let u v and t w be two flows. Suppose we have representatives of the renaming classes such that

Var(v) ∩ Var(w) = ∅. The product of u v and t w is defined if v, t are unifiable with MGU θ as (u v)(t w) := uθ wθ.
Remark 6. The condition on variables ensures that facts form a "left ideal" of the set of flows: if u is a fact and f a flow, then f u is a fact when it is defined.

Example 7. (f(x) x)(f(x) g(x)) = f(f(x)) g(x) (x • d (y • y)•x)((c• c)• x y • x) = x • d y • x (f(x • c) x• d)(d• d ) = f(d•c) (x g(h(x)))(g(y) y) = x h(x)
The product of flows corresponds to the resolution rule in the following sense: given two flows f = u v and g = t w and a M GU θ of v and t, then the resolution rule applied to f and g would yield f g.

To finish with our logic programming example, the product of the flows colored(x) blue(x) and blue(c) would yield colored(c) . Wirings then correspond to logic programs (sets of clauses) and the nilpotency condition can be seen as an algebraic variant of the notion of boundedness of these programs.

Definition 8 (wirings). Wirings are finite sets of flows. The product of wirings is defined as

F G := { f g | f ∈ F, g ∈ G, f g defined }.
We write U for the set of wirings and refer to it as the unification semiring.

The set of wirings U has the structure of a semiring. We use an additive notation for sets of flows to stress this point:

• The symbol + will be used in place of ∪.

• We write sets as the sum of their elements:

{ f 1 , . . . , f n } := f 1 + • • • + f n .
• We write 0 for the empty set.

• The unit is I := x

x.

We will call semiring any subset A of U such that

• 0 ∈ A, • if F ∈ A and G ∈ A then F G ∈ A. • if F, G ∈ A, then F + G ∈ A,
A subset satisfying only the first two conditions will be called a semigroup.

Definition 9 (nilpotency). A wiring

F is nilpotent if F n = 0 for some n ∈ N.
We may use the notation Nil(F ) to express the fact that F is nilpotent.

As mentioned in Sect. 1.1, nilpotency is related with the notion of boundedness [START_REF] Dantsin | Complexity and expressive power of logic programming[END_REF] of a logic program. Indeed, if we have a wiring F and a finite set of facts U, let us consider the set of facts that can be obtained through F , { u | u ∈ F n U for some n } which can also be written as

(I + F + F 2 + • • • )U or EX(F )U (
where EX(.) is the execution operator of Sect. 1.1). If F is nilpotent, one needs to compute the sum only up to a finite rank that does not depend on U, which implies the boundedness property.

Among wirings, those that can produce at most one fact from any fact will be of interest when considering deterministic vs. non-deterministic computation.

Definition 10 (deterministic wirings).

A wiring F is deterministic if given any fact u, card(F u) ≤ 1. We will write U d the set of deterministic wirings.

It is clear from the definition that U d forms a semigroup. The lemma below gives us a class of wirings that are deterministic and easy to recognize, due to its more syntactic definition.

Lemma 11. Let F = i u i t i . If the t i are pairwise disjoint (Definition 1), then F is deterministic.
Proof. Given a closed term t there is at most one of the t i that matches t, therefore F (t ) is either a single fact or 0.

The Balanced Semiring

In this section, we study a constraint on variable height of flows which we call balance. This syntactic constraint can be compared with similar ones proposed in order to get logic programs that are finitely ground [START_REF] Calimeri | Computable functions in ASP: Theory and implementation[END_REF]: balanced wirings are a special case of argument-restricted programs in the sense of [START_REF] Lierler | One more decidable class of finitely ground programs[END_REF].

We will be able to decide the nilpotency of balanced wirings in a space-efficient way, thanks to the results of Sect. 2.3.

Definition 12 (balance). A flow f = t

u is balanced if for any variable x ∈ Var(t) ∪ Var(u), all occurrences of x in either t or u have the same height (recall notations p. 5) which we write h f (x), the height of x in f . A wiring F is balanced if it is a sum of balanced flows.

We write U b for the set of balanced wirings and refer to it as the balanced semiring.

In Example 7, only the second line shows the product of balanced flows. The basic idea behind the notion of balance is that it forbids variations of height which may be used to store information "above" a variable. Typically, the flow f(x)

x is not balanced.

Definition 13 (height). The

height h(f ) of a flow f = t u is max{h(t), h(u)}. The height h(F ) of a wiring F is the maximal height of flows in it.
The following lemma summarizes the properties that are preserved by the product of balanced flows. It implies in particular that U b is indeed a semiring. Lemma 14. When it is defined, the product f g of two balanced flows f and g is still balanced and its height is at most max{h(f ), h(g)}.

Proof (sketch). By showing that the variable height condition and the global height are both preserved by the basic steps of the unification procedure.

The Computation Graph

The main tool for a space-efficient treatment of balanced wirings is an associated notion of graph. This section focuses on the algebraic aspects of this notion, proving various technical lemmas, and leaves the complexity issues to Sect. 4.2.

A separating space can be thought of as a finite subset of the Herbrand universe associated with a logic program, containing enough information to decide the problem at hand.

Definition 15 (separating space).

A separating space for a wiring F is a set of facts S such that

• For all u ∈ S, F u ⊆ S. • F n u = 0 for all u ∈ S implies F n = 0.
We can define such a space for balanced wirings with Lemma 14 in mind: balanced wirings behave well with respect to height of terms.

Definition 16 (computation space).

Given a balanced wiring F , we define its computation space Comp(F ) as the set of facts of height at most h(F ), built using only the symbols appearing in F and the constant symbol .

Lemma 17 (separation). If

F is balanced, then Comp(F ) is separating for F . Proof. By Lemma 14, F (u
) is of height at most max{h(F ), h(u)} ≤ h(F ) and it contains only symbols occurring in F and u, therefore if u ∈ Comp(F ) we have F u ⊆ Comp(F ).

By Lemma 14 again, F n is still of height at most h(F ). If (F n )u = 0 for all u ∈ Comp(F ), it means the flows of F n do not match any closed term of height at most h(F ) built with the symbols occurring in F (and eventually ). This is only possible if F n contains no flow, ie. F n = 0.

As F is a finite set, thus built with finitely many symbols, Comp(F ) is also a finite set. We can be a little more precise and give a bound to its cardinality.

Proposition 18 (cardinality). Let F be a balanced wiring, A the maximal arity of function symbols occurring in F and S the set of symbols occurring in

F , then card(Comp(F )) ≤ (card(S) + 1) P h(F ) (A) , where P k (X) = 1 + X + • • • + X k .
Proof. The number of terms of height h(F ) built over the set of symbols S ∪ { } of arity bounded by A is at most as large as the number of complete trees of degree A and height h(F ) (that is, trees where nodes of height less than h(F ) have exactly A childs), with nodes labeled by elements of S ∪ { }.

Then, we can encode in a directed graph 6 the action of the wiring on its computation space.

Definition 19 (computation graph). If F is a balanced wiring, we define its computation graph G(F ) as the directed graph:

• The vertices of G(F ) are the elements of Comp(F ).

• There is an edge from

u to v in G(F ) if v ∈ F u.
We state finally that the computation graph of a wiring contains enough information on the latter to determine its nilpotency. This is a key ingredient in the proof of Theorem 35, as the research of paths and cycles in graphs are problems that are well-known [START_REF] Jones | Space-bounded reducibility among combinatorial problems[END_REF] to be solvable within logarithmic space.

Lemma 20. A balanced wiring F is nilpotent (Definition 9) iff G(F ) is acyclic.
Proof. Suppose there is a cycle of length n in G(F ), and let u be the label of a vertex which is part of this cycle. By definition of G(F ), u ∈ (F n ) k u for all k, which means that (F n ) k = 0 for all k and therefore F cannot be nilpotent.

Conversely, suppose there is no cycle in G(F ). As it is a finite graph, this entails a maximal length N of paths in G(F ). By definition of G(F ), this means that F N +1 u = 0 for all u ∈ Comp(F ) and with Lemma 17 we get F N +1 = 0.

Moreover, the computation graph of a deterministic (Definition 10) wiring has a specific shape, which in turn induces a deterministic procedure in this case.

Lemma 21. If F is a balanced and deterministic wiring, G(F ) has an out-degree (the maximal number of edges a vertex can be the source of) bounded by 1.

Proof. It is a direct consequence of the definitions of G(F ) and determinism.

Tensor product and other semirings

Finally, we list a few other semirings that will be used in the next section, where we define the notions of representation of a word and observation.

The binary function symbol • can be used to define an operation that is similar to the algebraic notion of tensor product.

Definition 22 (tensor product). 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 their tensor product as

(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 . Given two semirings A, B, we define A ⊗ B := { i F i ⊗ G i | F i ∈ A , G i ∈ B }.
The tensor product of two semirings is easily shown to be a semiring.

Example 23. (f(x) • y y • x) ⊗ (x g(x)) = (f(x)• y)•z (y • x)•g(z)
Notation. As the symbol • , the ⊗ operation is not associative. We carry on the convention for • and write it as right associating:

A ⊗ B ⊗ C := A ⊗ (B ⊗ C).
Semirings can also naturally be associated to any set of closed terms or to the restriction to a certain set of symbols.

Definition 24. Given a set of closed terms E, we define the following semiring

E := { i t i u i | t i , u i ∈ E }.
If S is a set of symbols and A a semiring, we write A \S the semiring of wirings of A , that do not use the symbols in S.

This operation yields semirings because composition of flows made of closed terms involves no actual unification: it is just equality of terms and therefore one never steps out of E .

Finally, the unit I = x x of U yields a semiring.

Definition 25 (unit semiring).

The unit semiring is defined as I := { 0 , I }.

Words and Observations

We define in this section the global framework that will be used later on to obtain the characterization of logarithmic space computation. In order to discuss the contents of this section, let us first define two specific semirings.

Definition 26 (word and observation semirings).

We fix two (disjoint) infinite sets of constant symbols P and S, and a unary function symbol M. We denote by M(P) the set of terms M(p) with p ∈ P. We define the following two semirings that are included in U b :

• The word semiring is the semiring W := I ⊗ I ⊗ M(P) .

• The observation semiring is the semiring O := S ⊗ U b \P .

Remark 27. The expression I ⊗ I ⊗ M(P) may seem odd at first sight, as the intuition from algebra is that I ⊗ I I. But remember that we are here in a syntactical context and therefore we need to be careful with things that can usually be treated "up to isomorphism", as it may cause some unifications to fail where they should not.

These two semirings will be used as parameters of a construction M Σ (.) over an alphabet Σ (we suppose ∈ Σ), that will define the representation of words and a notion of abstract machine, that we shall call observations. Definition 28. We fix the set of constant symbols LR := {L, R}.

Given a set of constant symbols Σ and a semiring A we define the semiring

M Σ (A) := (Σ ∪ { }) ⊗ LR ⊗ A.
In the following of this section, we will show how to represent lists of elements of Σ by wirings in the semiring M Σ (W). Then, we will explain how the semiring M Σ (O) captures a notion of abstract machine. In the last section of the paper we will explain further how observations and words interact, and prove that this interaction captures logarithmic space computation.

Representation of Words

We now show how one can represent words by wirings in M Σ (W). We recall this semiring is defined as (Σ ∪ { }) ⊗ LR ⊗ I ⊗ I ⊗ M(P) . The part (Σ ∪ { }) ⊗ LR deals with, and is dependent on, the alphabet Σ considered; this is where the input and the observation will interact. The two instances of the unit semiring I correspond to the fact that the word cannot affect parts of the observation that correspond to internal configurations. The last part, namely the semiring M(P) , will contain the position constants of the representation of words.

Notation. We write t u for t u + u t.

Definition 29 (word representations).

Let W = c 1 , . . . , c n be a word over an alphabet Σ and p = p 0 , p 1 , . . . , p n be pairwise distinct constant symbols. Writing p n+1 = p 0 and c 0 = c n+1 = , 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 • M(p i ) c i+1 • L•x • y • M(p i+1 ) (1)
We will write R(W ) the set of representations of a given word W .

To better understand this representation, consider that each symbol in the alphabet Σ comes in two "flavors", left and right. Then, one can easily construct the "context" W =

n i=0 c i • R• x • y • M([ ] i ) c i+1 • L• x• y • M([ ] i+1
) from the list as the sums of the arrows in the following picture (where x and y are omitted):

• R • L M([ ]0) c 1 • R • L (M[ ]1) c 2 • R • L M([ ]2) . . . c n • R • L M([ ]n)
Then, choosing a set p = p 0 , . . . , p n of position constants, intuitively representing physical memory addresses, the representation Wp of a word associated with p is obtained by filling, for all i = 0, . . . , n, the hole [ ] i by the constant p i . This abstract representation of words is not an arbitrary choice. It is inspired by the interpretation of lists in geometry of interaction.

Indeed, in System F, the type of binary lists corresponds to the formula ∀X (X ⇒ X) ⇒ (X ⇒ X) ⇒ (X ⇒ X). Any lambda-term in normal form of this type can be written as

λf 0 f 1 x. f c1 f c2 • • • f c k x, where c 1 • • • c k is a word over {0, 1}.
The GoI representation of such a lambda-term yields the abstract representation just defined. 7 Notice that the additional symbol used to represent words corresponds to the variable x in the preceding lambda-term. Note also the fact that the representation of integer is cyclic, and that the symbol serves as a reference for the starting/ending point of the word.

Let us finally stress that the words are represented as deterministic wirings. This implies that the restriction to deterministic observations will correspond to restricting ourselves to deterministic pointer machines. The framework, however, allows for a number of generalization and variants. For instance, one can define a representation of trees by adapting Definition 29 in such a way that every vertex is related to its descendants; doing so would however yield non-deterministic wirings. In the same spirit, a notion of "one-way representations of words", defined by replacing the symbol by the symbol in Equation 1of Definition 29, could be used to characterize one-way multi-head automata.

Observations

We now define observations. We will then explain how these can be thought of as a kind of abstract machines. An observation is an element of the semiring

M Σ (O) = (Σ ∪ { }) ⊗ LR ⊗ (S ⊗ U b \P )
Once again, the part of the semiring (Σ ∪ { }) ⊗ LR is dependent on the alphabet Σ considered and represents the point of interaction between the words and the machine. The semiring S intuitively corresponds to the states of the observation, while the part U b \P forbids the machine to act non-trivially on the position constants of the representation of words. The fact that the machine cannot perform any operation on the memory addresses -the position constantsof the word representation explains why observations are naturally thought of as a kind of pointer machines.

Definition 30 (observation). An observation is any element O of M Σ (O).

We can define the language associated to an observation. The condition of acceptance will be represented as the nilpotency of the product O Wp where Wp ∈ R(W ) represents a word W and O is an observation.

Definition 31 (language of an observation).

Let O be an observation on the alphabet Σ. We define the language accepted by O as

L(O) := W ∈ Σ * ∀p, Nil(O Wp )
One important point is that the semirings M Σ (W) and M Σ (O) are not completely disjoint, and therefore allow for non-trivial interaction of observations and words. However, they are sufficiently disjoint so that this computation does not depend on the choice of the representative of a given word.

Lemma 32. Let W be a word, and Wp , Wq ∈ R(W ). For every observation O ∈ M Σ (O), Nil(O Wp ) if and only if Nil(O Wq ).

Proof. As we pointed out, the observation cannot act on the position constants of the representations Wp and Wq . This implies that for all integer k the wirings (O Wp ) k and (O Wq ) k are two instances of the same context, i.e. they are equal up to the interchange of the positions constants p 0 , . . . , p n and q 0 , . . . , q n . This implies that (O Wp ) k = 0 if and only if (O Wq ) k = 0.

Corollary 33. Let O be an observation on the alphabet Σ. The set L(O) can be equivalently defined as the set

L(O) = W ∈ Σ * ∃p, Nil(O Wp )
This result implies that the notion of acceptance has the intended sense and is finitely verifiable: whether a word W is accepted by an observation O can be checked without considering all representations of W .

This kind of situation where two semirings W and O are disjoint enough to obtain Corollary 33 can be formalized through the notion of normative pair considered in earlier works [START_REF] Girard | Normativity in logic[END_REF][START_REF] Aubert | Characterizing co-nl by a group action[END_REF][START_REF] Aubert | Unification and logarithmic space[END_REF].

Logarithmic Space

This section starts by explaining the computation one can perform with the observations, and prove that it corresponds to logarithmic space computation by showing how pointer machines can be simulated. Then, we will prove how the language of an observation can be decided within logarithmic space.

This section uses the complexity classes DLogspace and coNLogspace, as well as notions of completeness of a problem and reduction between problems. We use in Sect. 4.2 the classical theorem of coNLogspace-completeness of the acyclicity problem in directed graphs, and in Sect. 4.1 a convenient model of computation, two-ways multi-head finite automata [START_REF] Holzer | Multi-head finite automata: Characterizations, concepts and open problems[END_REF], a generalization of automata also called "pointer machine". Note that the non-deterministic part of our results concerns coNLogspace, or equivalently NLogspace by the famous Immerman-Szelepcsényi theorem.

Completeness: Observations as Pointer Machines

Let h 0 , x, y ∈ V, p 0 , p 1 , A 0 constants and Σ = {0, 1}, the excerpt of a dialogue in Figure 1 We just depicted two transitions corresponding to an automata that reads the first bit of the word, and if this bit is a 1, goes back to the starting position, in state b. We remark that the answer of w 1 differs from the one of w 2 : there is no need to clarify the position (the variable argument of M), since h 0 was already replaced by p 1 . Such an information is needed only in the first step of the computation: after that, the updates of the position of the pointer take place on the word side. We remark that neither the state nor the constant A 0 is an object of dialogue.

Note also that this excerpt corresponds to a deterministic computation. In general, several elements of the observation could get unified with the current configuration, yielding non-deterministic transitions.

• R • init • A0 • M(h0) • L • init • A0 • M(h0) (o1) 1 • L • x • y • M(p1) • R • x • y • M(p0) (w1) 1 • L • b • A0 • M(h0) 1 • L • init • A0 • M(h0) (o2) • R • x • y • M(p0) 1 • L • x • y • M(p1) (w2)
By unification,

1 • L • init • A0 • M(p1) • L • init • A0 • M(p0) (w1o1) 1 • L • b • A0 • M(p1) • L • init • A0 • M(p0) (o2w1o1) • R • b • A0 • M(p0) • L • init • A0 • M(p0) (w2o2w1o1)
This can be understood as the small following dialogue:

Multiple Pointers and Swapping

We now add some computational power to our observations by adding the possibility to handle several pointers. The observations will now use a k-ary function A k that allows to "store" k additional positions in the variables h 1 , . . . , h k . This part of the observation is not affected by the word, which means that only one head (the main pointer) can move. The observation can exchange the position of the main pointer and the position stored in A k : we therefore refer to the arguments of A k as auxiliary pointers that can become the main pointer at some point of the computation. This is of course strictly equivalent to having several heads with the ability to move. Consider the following flow, that encodes the transition "if the observation reads 1 • R in state s, it stores the position of the main pointer (the variable h 0 ) at the i-th position in A k and start reading the input with a new pointer":

• R • s • A k (h 1 , . . . , h 0 , . . . , h k ) • M(h i ) 1•R • s•A k (h 1 , . . . , h i , . . . , h k )• M(h 0 )
Suppose that later on, when reading 0 • L in state r, we want to give back to that pointer the role of main pointer. That means to swap again the position of the variables h 0 and h i , in order to store the position that was currently read and to restore the position that was "frozen" in A k .

_ • L•r • A k (h 1 , . . . , h i , . . . , h k ) • M(h 0 ) 0• L•r • A k (h 1 , . . . , h 0 , . . . , h k )• M(h i )
The occurrence of L in the head of the previous flow reflects that we want to read the input from left to right, but the "_" slot cannot be a free variable, for that would break the safety of our clauses, the fact that all the variable of the head (the left-member) appears in the body (the right-member). So this slot should be occupied by the last value read by the pointer represented by the variable h 0 , an information that should be encoded in the state r. 8Acceptance and Rejection Remember (Corollary 33) that the language of an observation is the set of words such that the wiring composed of the observation applied to a representation of the word is nilpotent. So one could add a flow with the body corresponding to the desired situation leading to acceptance, and the head being some constant accept that appears in the body of no other flow, thus ending computation when it is reached. But in fact, it is sufficient not to add any flow: doing nothing is accepting! The real challenge is to reject a word: it means to loop. We cannot simply add the unit (I := x x) to our observation, since that would make our observation loop for any input. So we have to be more clever than that, and to encode rejection as a re-initialization of the observation: we want the observation to put all the pointers on and to go back to an init state. So, a rejection is in fact a "perform for ever the same computation".

Suppose the main pointer was reading from right to left, that we are in state b and that we want to re-initialize the computation. Then, for every c ∈ Σ, it is enough to add the transitions (go-back-c) and (re-init) to the observation,

c• L•b • A(h 1 , . . . , h k )•M(h 0 ) c • R• b•A(h 1 , . . . , h k ) • M(h 0 ) (go-back-c) • R• init•A(h 0 , . . . , h 0 )•M(h 0 ) • R• b•A(h 1 , . . . , h k ) • M(h 0 ) (re-init)
Once the main pointer is back on , (re-init) re-initializes all the positions of the auxiliary pointers to the position of and changes the state for init.

There is another justification for this design: as the observation and the representation of the word are sums, and as the computation is the application, any transition that can be applied will be applied, i.e. if the body of a flow of our observation and the head of a flow of the word can be unified, the computation will start in a possibly "wrong" initialization. That some of these incorrect runs accept for incorrect reason is no trouble, since only rejection is "meaningful" due to the nilpotency criterion. But, with this framework, an incorrect run will be re-initialized to the "right" initialization, and perform the correct computation: in that case, it will loop if and only if the input is rejected.

Two-Ways Multi-Heads Finite Automata and Completeness

The model we just developed has clearly the same expressivity as two-ways multi-head finite automata, a model of particular interest to us for it is well studied, tolerant to a lot of enhancements or restrictions 9 and gives an elegant characterization of DLogspace and NLogspace [START_REF] Holzer | Multi-head finite automata: Characterizations, concepts and open problems[END_REF][START_REF] Pighizzini | Two-way finite automata: Old and recent results[END_REF].

Then, by a plain and uniform encoding of two-ways multi-head finite automata, we get Theorem 34. That acceptance and rejection in the non-deterministic case are "reversed" (i.e. all path have to accept for the computation to accept) makes us characterize coNLogspace instead of NLogspace.

Note that encoding a deterministic automaton yields a wiring of the form of Lemma 11, which would be therefore a deterministic wiring.

Theorem 34. If L ∈ coNLogspace, then there is an observation O such that L(O) = L. If moreover L ∈ DLogspace, then O can be chosen deterministic.

Soundness of Observations

We now use the results of Sect. 2.3 and Sect. 3.2 to design a procedure that decides whether a word belongs to the language of an observation within logarithmic space. This procedure will reduce this problem to the problem of testing the acyclicity of a graph, that is well-known to be tractable with logarithmic space resources.

First, we show how the computation graph of the product of the observation and the word representation can be constructed deterministically using only logarithmic space; then, we prove that testing the acyclicity of such a graph can be done within the same bounds. Here, depending on the shape of the graph (which is dependent in itself of determinism of the wiring, recall Lemma 21), the procedure will be deterministic or non-deterministic.

Finally, using the fact that logarithmic space algorithms can be composed [30, Fig. 8.10], Lemma 20 and Corollary 33, we will obtain the expected result: A Foreword on Word and Size Given a word W over Σ, to build a representation Wp as in Definition 29 is clearly in DLogspace: it is a plain matter of encoding. By Lemma 32, it is sufficient to consider a single representation. So for the rest of this procedure, we consider given Wp ∈ R(W ) and write F := O Wp . The size of Σ is a constant, and it is clear that the maximal arity and the height of the balanced wiring F remain fixed when W varies. The only point that fluctuates is the cardinality of the set of symbols that occurs in F , and it is linearly growing with the length of W , corresponding to the number of position constants. In the following, any mention to a logarithmic amount of space is to be completed by "relatively to the length of W ".

Building the Computation Graph

We need two main ingredients to build the computation graph (Definition 19) of F : to enumerate the computation space Comp(F ) (recall Definition 16), and to determine whether there is an edge between two vertices. By Proposition 18, card(Comp(F )) is polynomial in the size of W . Hence, given a balanced wiring F , a logarithmic amount of memory is enough to enumerate the members of Comp(F ), that is the vertices of G(F ). Now the second part of the construction of G(F ) is to determine if there is an edge between two vertices. Remember that there is an edge from Actually, this result relies on a subtle manipulation of the representation of the terms as simple directed acyclic graphs [START_REF] Baader | Unification theory[END_REF], where the variables are "shared". Translations between this representation of terms and the usual one can be performed in logarithmic space [12, p. 38].

u = u to v = v in G(F ) if v ∈ F u.

Deciding if G(F ) is Acyclic

We know thanks to Lemma 20 that answering this question is equivalent to deciding if F is nilpotent. We may notice that G(F ) is a directed, potentially unconnected graph of size card(Comp(F )).

It is well-know that testing for acyclicity of a directed graph is a coNLogspace [24, p. 83] problem. Moreover, if F is deterministic (which is the case when O is), then G(F ) has out-degree bounded by 1 (Lemma 21) and one can test its acyclicity without being non-deterministic: it is enough to list the vertices of Comp(F ), and for each of them to follow card(Comp(F )) edges and to test for equality with the vertex picked at the beginning. If a loop is found, the algorithm rejects, otherwise it accepts after testing the last vertex. Only the starting vertex and the current vertex need to be stored, which fits within logarithmic space, and there is no need to do any non-deterministic transitions.

Conclusion

We presented the unification semiring, a construction that can be used both as an algebraic model of logic programming and as a setting for a dynamic model of logic. Within this semiring, we were able to identify a class of wirings that have the exact expressive power of logarithmic space computation.

If we try to step back a little, we can notice that the main tool in the soundness proof (Sect. 4.2) is the computation graph, defined in Sect. 2.3. More precisely, the properties of this graph, notably its cardinality (that turns out to be polynomial in the size of the input), allow to define a decision procedure that needs only logarithmic space. The technique is modular, hence not limited to logarithmic space: identifying other conditions on wirings that ensure size bounds on the computation graph would be a first step towards the characterization of other space complexity classes.

Concerning completeness, the choice of encoding pointer machines (Sect. 4.1) rather than log-space bounded Turing machines was quite natural. Balanced wirings correspond to the idea of computing with pointers: manipulation of data without writing abilities, and thus with no capacity to store any information other than a fixed number of positions on the input.

By considering other classes of wirings or by modifying the encoding it might be possible to capture other notions of machines characterizing some complexity classes: we already mentioned at the end of Sect. 3.1 a modification of the representation of the word that would model one-way finite automata.

The relation with proof theory needs to be explored further: the approach of this paper seems indeed to suggest a sort of "Curry-Howard" correspondence for logic programming.

As Sect. 1.1 highlighted, there are many notions that might be transferable from one field to the other, thanks to a common setting provided by geometry of interaction and the unification semiring. Most notably, the notion of nilpotency (on the proof-theoretic side: strong normalization) corresponds to a variant of boundedness of logic programs, a property that is usually hard to ensure.

Another direction could be to look for a proof-system counterpart of this work: a corresponding "balanced" logic of logarithmic space.

  between an observation O = o 1 + o 2 + • • • and the representation of a word Wp = w 1 + w 2 + • • • should help the reader to grasp the mechanism.

Fig. 1 .

 1 Fig. 1. The beginning of a dialogue between an observation and the representation of a word

Theorem 35 .

 35 If O is an observation, then L(O) ∈ coNLogspace. If moreover O is deterministic, then L(O) ∈ DLogspace.

Definition 1 (unification, matching and disjointness). Two terms t, u are • unifiable if there exists a substitution θ, called a unifier of t and u, such that tθ = uθ. A unifier θ such that any other unifier of t and u is an instance of θ is called a 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.

Theorem 36 (matching is in DLogspace [12, p. 49]).

  So one has to scan the members of F = O To list the members of F is in DLogspace, but unification in general is a difficult problem (see Sect. 1.2). The special case of matching can be tested with a logarithmic amount of space: Given two terms t and u such that either t or u is closed, deciding if they are matchable is in DLogspace.

						Wp : if
	there exists (t 1	t 2 )(t 1	t 2 ) ∈ F such that (t 1	t 2 )(t 1	t 2 )(u	) = v	,
	then there is an edge from u to v.

By adding complex scalar coefficients, one can actually extend U into a C *algebra[START_REF] Girard | Geometry of interaction III: accommodating the additives[END_REF].

[START_REF] Baillot | Linear logic by levels and bounded time complexity[END_REF] A program is bounded if there is an integer k such that the fixed point computation of the program is stable after k iterations, independently of the facts input.

Here by directed graph we mean a set of vertices V together with a set of edges E ⊆ V × V . We say that there is an edge from e ∈ V to f ∈ V when (e, f ) ∈ E.

That is, we should have states r , r0 and r1, and flows accordingly.

In fact, most of the variations (the automata can be one-way, sweeping, rotating, oblivious, etc.) are studied in terms of number of states and additional heads needed to simulate a variation with another, but most of the time they keep characterizing the same complexity classes.

Acknowledgments

The authors would like to thank the anonymous referees for helpful suggestions and comments.

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