Logic Programming and Logarithmic Space
Clément Aubert\inst{1
\input{abstract
abstract.tex
We present an algebraic view on logic programming, related to proof theory and more specifically linear logic and geometry of interaction.
Within this construction, a characterization of logspace (deterministic and non-deterministic) computation is given \textit{via} a synctactic restriction, using an encoding of words that derives from proof theory.

We show that the acceptance of a word by an observation (the counterpart of a program in the encoding) can be decided within logarithmic space, by reducing this problem to the acyclicity of a graph.
%deciding if a graph has a cycle.
%it to cycle search in a graph, and 
We show moreover that observations are as expressive as two-ways multi-heads finite automata, a kind of pointer machines that is a standard model of logarithmic space computation.

aplas14.tex
\documentclass[envcountsame]{llncs}
\pdfoutput=1 % for axriv
\input{packages}
\input{thm}
\input{macros}

\begin{document}
	\renewcommand{\labelitemi}{\scalebox{0.8}{$\bullet$}} % symbole pour itemize
	
	%%% linebreak, spacing and hyphenation tweak
	\hyphenpenalty=2000
	\tolerance=600

	\input{SECTIONS} %actual content

\end{document}

balanced.tex
In this section, we study a constraint on variable height of flows which we call \emph{balance}. This syntactic constraint can be compared with similar ones proposed in order to get logic programs that are \emph{finitely ground}~\cite{Calimeri2008}: balanced wirings are a special case of \emph{argument-restricted} programs in the sense of \cite{Lierler2009}.

Balanced wirings will enjoy properties (see \autoref{sec_compgraph}) that will allow to decide their nilpotency efficiently. 

\begin{definition}[balance]%
\label{def-balanced}
	A flow $f=t\flow u$ is \emph{balanced} if for any variable $x\in\var(t)\cup\var(u)$,
	all occurrences of $x$ in either $t$ or $u$ have the same height (recall notations p.~\pageref{def-height})
	which we write $\h_f(x)$, the \emph{height of $x$ in $f$}.
	A wiring $F$ is \emph{balanced} if it is a sum of balanced flows.
	
	We write $\balg$ the set of balanced wirings and refer to it as the \emph{balanced semiring}.
\end{definition}



Note that in \autoref{example_flows}, only the second line shows product of balanced flows.

\begin{definition}[height]\label{def_height}
	The \emph{height} $\h(f)$ of a flow $f=t \flow u$ is $\max\{\h(t),\h(u)\}$.
	The \emph{height} $\h(F)$ of a wiring $F$ is the maximal height of flows in it.
\end{definition}

The following lemma summarizes the properties that are preserved by the product of balanced flows.
It implies in particular that $\balg$ is indeed a semiring.


\begin{lemma}\label{lem_balanced}
	When it is defined, the product $fg$ of two balanced flows $f$ and $g$ is still balanced
	and its height is at most $\max\{\h(f),\h(g)\}$.
\end{lemma}

\begin{proof}[sketch]
	By showing that the variable height condition and the global height are both preserved
	by the basic steps of the unification procedure.
	\qed
\end{proof}

%\begin{corollary}[balanced semiring]
%	$\balg$ is a semiring.
%\end{corollary}

compgraph.tex
The main tool for a space-efficient treatment of balanced wirings
is an associated notion of graph. % that will contain enough information to decide the problem at hand.
This section focuses on the algebraic aspects of this notion, 
proving various technical lemmas, and leaves the complexity issues to \autoref{sec_soundness}.

\smallskip

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.

\begin{definition}[separating space]
	A \emph{separating space} for a wiring $F$ is a set of facts $\BF S$ such that
	\begin{itemize}
		\item For all $\BF u\in \BF S$, $F\BF u\subseteq \BF S$.
		\item $F^n\BF u=0$ for all $\BF u\in\BF S$ implies $F^n=0$.
	\end{itemize}
\end{definition}

We can define such a space for balanced wirings with \autoref{lem_balanced} in mind: balanced wirings behave well with respect to height of terms.

\begin{definition}[computation space]\label{def-comp}
	Given a balanced wiring $\wiring{F}$, we define its \emph{computation space}
	$\comp{\wiring{F}}$ as the set of facts of height at most $\h(\wiring{F})$,
	built using only the symbols appearing in $\wiring{F}$ and the constant symbol $\factsym$.
\end{definition}

\begin{lemma}[separation]\label{lem_sep}
	If $F$ is balanced, then $\comp{\wiring{F}}$ is separating for~$F$.
\end{lemma}

\begin{proof}
	By \autoref{lem_balanced}, $\wiring F(\fact u)$ is of height at most $\max\{\h(\wiring F),\h(u)\}\leq\h(\wiring F)$ and it contains only symbols occurring in $\wiring F$ and $u$,
	therefore if $\BF u\in \comp{\wiring{F}}$ we have $\wiring F\BF u\subseteq \comp{\wiring{F}}$.
	
	By \autoref{lem_balanced} again, $F^n$ is still of height at most $\h(F)$. If $(F^n)\BF u=0$ for all $\BF u\in\comp{\wiring{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 $\factsym$). This is only possible if $F$ contains no flow, \textit{ie.} $F=0$.\qed
\end{proof}

As $F$ is a finite set, thus built with finitely many symbols, $\comp{\wiring{F}}$ is also a finite set.
We can be a little more precise and give a bound to its cardinal.

\begin{proposition}[cardinality]\label{card-comp}
	Let $\wiring{F}$ be a balanced wiring, $A$ the maximal arity of function symbols
	occurring in $\wiring{F}$ and $S$ the set of symbols occurring in $\wiring{F}$,
	then $\card{\comp{\wiring{F}}}\ \leq\ (\card S+1)^{P_{\h(\wiring{F})}(A)}$,
	where $P_k(X)=1+X+\cdots+X^k$.
\end{proposition}

\begin{proof}
	The number of terms of height $\h(F)$ built over the set of symbols $S\cup\{\factsym\}$
	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\cup\{\factsym\}$.\qed
\end{proof}

Then, we can encode in a directed graph\footnote{Here by directed graph we mean a set of \emph{vertices} $V$ together with a set of \emph{edges} $E\subseteq V\times V$.
We say that there is an edge \emph{from $e\in V$ to $f\in V$} when $(e,f)\in E$.} the action of the wiring on its computation space.%, which will be useful in section \autoref{sec_soundness}, as the research of paths and cycles in graphs are problems that are well-know to be solvable within logarithmic space.

\begin{definition}[computation graph]\label{compgraph}
	If $F$ is a balanced wiring, we define its \emph{computation graph} $\G(\wiring{F})$ as the directed graph:
	\begin{itemize}
		\item The vertices of $\G(\wiring{F})$ are the elements of $\comp{\wiring{F}}$.
		\item There is an edge from $\BF u$ to $\BF v$ in $\G(\wiring{F})$ if $\BF v\in \wiring{F} \BF u$.
	\end{itemize}
\end{definition}

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 \autoref{nilp-in-l}, as the research of paths and cycles in graphs are problems that are well-known to be solvable within logarithmic space.

\begin{lemma}\label{nilp-iff-acycl}
	A balanced wiring $\wiring{F}$ is nilpotent (\autoref{def_nilp}) \iff $\G(\wiring{F})$ is acyclic.
\end{lemma}


\begin{proof}
	Suppose there is a cycle of length $n$ in $\G(\wiring{F})$, and let $\BF u$ be the label of a vertex which is part of this cycle. By definition of $\G(\wiring{F})$, $\BF u\in(\wiring{F}^n)^k\BF u$ for all $k$, which means that $(\wiring{F}^n)^k\neq0$ for all $k$ and therefore $F$ cannot be nilpotent.
	
	Conversely, suppose there is no cycle in $\G(\wiring{F})$. As it is a finite graph, this entails a maximal length $N$ of paths in $\G(F)$. By definition of $\G(\wiring{F})$, this means that $F^{N+1}\BF u=0$ for all $\BF u\in\comp{\wiring{F}}$ and with \autoref{lem_sep} we get $F^{N+1}=0$. \qed
\end{proof}


Moreover, the computation graph of a deterministic (\autoref{def_fun}) wiring has a specific shape, which in turn induces a deterministic procedure in this case.

\begin{lemma}\label{det-graph}
	If $F$ is a balanced and deterministic wiring, $\G(\wiring{F})$ has an out-degree (the maximal number of edges a vertex can be the source of) bounded by $1$.
\end{lemma}

\begin{proof}
	It is a direct consequence of the definitions of $\G(\wiring{F})$ and determinism.
	\qed
\end{proof}

completeness.tex
This section describes the kind of computation one can model with observations.
%The mechanism of execution, the iteration, makes it clear that that there will be no possibility to modify the input, since a \enquote{fresh copy} of it is provided at every step.

Let $h_0, x, y$ be variables, $\TT p_0, \TT p_1, \nary 0$ constants and $\Sigma = \{0, 1\}$, the excerpt of a dialogue in \autoref{fig-dial} between an observation $O=o_1 + o_2 + \cdots\,$ and the representation of a word $\bar W_p=w_1 + w_2 + \cdots\,$ should help the reader to grasp the mechanism.

%\medskip
%\noindent\scalebox{0.876}%
%{\noindent
%\begin{tabular}{ll}
%	$(o_1)\ \wordterm{\start}{\L}{\state{init}}{\nary 0}{h_0} \flow \wordterm{\start}{\R}{\state{init}}{\nary 0}{h_0}$ 
%		& \quad and after unification: \\
%	$(w_1)\ \wordterm{\start}{\R}{x}{y}{\TT p_0 } \flow \wordterm{1}{\L}{x}{y}{\TT p_1 }$
%		& $(o_1 w_1)\ \wordterm{\start}{\L}{\state{init}}{\nary 0}{\TT p_0} \flow \wordterm{1}{\L}{\state{init}}{\nary 0}{\TT p_1 }$ \\
%	$(o_2)\ \wordterm{1}{\L}{\state{init}}{\nary 0}{h_0} \flow \wordterm{1}{\L}{\state{b}}{\nary 0}{h_0}$
%		& $(o_1 w_1 o_2)\ \wordterm{\start}{\L}{\state{init}}{\nary 0}{\TT p_0} \flow \wordterm{1}{\L}{\state{b}}{\nary 0}{\TT p_1}$ \\
%	$(w_2)\ \wordterm{1}{\L}{x}{y}{\TT p_1}  \flow \wordterm{\start}{\R}{x}{y}{\TT p_0 }$
%		& $(o_1 w_1 o_2 w_2) \wordterm{\start}{\L}{\state{init}}{\nary 0}{\TT p_0} \flow \wordterm{\start}{\R}{\state{b}}{\nary 0}{\TT p_0}$
%\end{tabular}
%}
%
%\medskip
%{
%	\begin{multicols}{2}
%	\setlength{\parindent}{0pt}\footnotesize
%	$(o_1)\ \wordterm{\start}{\L}{\state{init}}{\nary 0}{h_0} \flow \wordterm{\start}{\R}{\state{init}}{\nary 0}{h_0}$

%	$(w_1)\ \wordterm{\start}{\R}{x}{y}{\TT p_0 } \flow \wordterm{1}{\L}{x}{y}{\TT p_1 }$

%	$(o_2)\ \wordterm{1}{\L}{\state{init}}{\nary 0}{h_0} \flow \wordterm{1}{\L}{\state{b}}{\nary 0}{h_0}$

%	$(w_2)\ \wordterm{1}{\L}{x}{y}{\TT p_1}  \flow \wordterm{\start}{\R}{x}{y}{\TT p_0 }$

%	\smallskip
%	\quad and by unification:

%	$(o_1 w_1)\ \wordterm{\start}{\L}{\state{init}}{\nary 0}{\TT p_0} \flow \wordterm{1}{\L}{\state{init}}{\nary 0}{\TT p_1 }$

%	$(o_1 w_1 o_2)\ \wordterm{\start}{\L}{\state{init}}{\nary 0}{\TT p_0} \flow \wordterm{1}{\L}{\state{b}}{\nary 0}{\TT p_1}$

%	$(o_1 w_1 o_2 w_2)\
%	\quad\wordterm{\start}{\L}{\state{init}}{\nary 0}{\TT p_0} \flow \wordterm{\start}{\R}{\state{b}}{\nary 0}{\TT p_0}$
%	\end{multicols}
%}
\begin{figure}
\begin{align}
\wordterm{\start}{\L}{\state{init}}{\nary 0}{h_0}	& \flow \wordterm{\start}{\R}{\state{init}}{\nary 0}{h_0}	\tag{$o_1$}\\
\wordterm{\start}{\R}{x}{y}{\TT p_0 } & \flow \wordterm{1}{\L}{x}{y}{\TT p_1 } \tag{$w_1$}\\
\wordterm{1}{\L}{\state{init}}{\nary 0}{h_0} & \flow \wordterm{1}{\L}{\state{b}}{\nary 0}{h_0}	\tag{$o_2$}\\
\wordterm{1}{\L}{x}{y}{\TT p_1} &  \flow \wordterm{\start}{\R}{x}{y}{\TT p_0 } \tag{$w_2$}\\
\shortintertext{By unification,}
\wordterm{\start}{\L}{\state{init}}{\nary 0}{\TT p_0} & \flow \wordterm{1}{\L}{\state{init}}{\nary 0}{\TT p_1 }	\tag{$o_1 w_1$}\\
%\wordterm{1}{\L}{\state{init}}{\nary 0}{\TT p_1} & \flow \wordterm{\start}{\R}{\state{b}}{\nary 0}{\TT p_0}	\tag{$o_2 w_2$}\\
\wordterm{\start}{\L}{\state{init}}{\nary 0}{\TT p_0} & \flow \wordterm{1}{\L}{\state{b}}{\nary 0}{\TT p_1}	\tag{$o_1 w_1 o_2$}\\
\wordterm{\start}{\L}{\state{init}}{\nary 0}{\TT p_0} & \flow \wordterm{\start}{\R}{\state{b}}{\nary 0}{\TT p_0}	\tag{$o_1 w_1 o_2 w_2$}
\end{align}
%This result corresponds to the fact that the observation was at the left of $\start$ (on the input side, at the very beginning of the tape if you read it from left to right), that it read a $\TT{1}$ by moving right, and that it is now on the input side of this first bit (at $\TT p_1$).
This can be understood as the small following dialogue:
\begin{dialogue}
	\speak{$o_1$} \direct{Is in state $\state{init}$} \enquote{I read $\start$ from left to right, what do I read now?}
	\speak{$w_1$} \enquote{Your position was $\TT p_0$, you are now in position $\TT p_1$ and read $1$.}
	\speak{$o_2$} \direct{Change state to $\state{b}$} \enquote{I do an about-turn, what do I read now?}
	\speak{$w_2$} \enquote{You are now in position $\TT p_0$ and read $\start$.}
\end{dialogue}
\caption{An example of dialogue between an observation and the representation of a word}
\label{fig-dial}
\end{figure}

%And the word add at the same time \enquote{Your state and the position of the auxiliary pointers are left unchanged}.
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 $\state{b}$.
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 $\TT p_1$.
Such an information is needed only in the first step of computation: after that, the updates of the position of the pointer take place on the word side.
Remark that neither the state nor the constant $\nary 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.%: $o_2$ might not be the only flow to \enquote{answer}, other flows could be unified, and that would corresonds to our definition of non-deterministic wirings.

\subsubsection{Multiple Pointers and Swapping}
We now add some computational power to our observation by adding the possibility to handle several pointers.
The observations will now use a $k$-ary function $\nary k$ that allows to \enquote{store} $k$ positions.
This part of the observation is not affected by the word, which means that only one head (the \emph{main pointer}) can move.
The observation can exchange the position of the main pointer and the position stored in $\nary k$: we therefore refer to the arguments of $\nary k$ as \emph{auxiliary pointers} that can become the main pointer at some point of the computation.
This is of course strictly equivalent to several heads that have the ability to move.

Consider the following flow, that encodes the transition \enquote{if the observation reads $1\p\R$ in state $\state{s}$, it stores the position of the main pointer (the variable $h_0$) at the $i$-th position in $\nary k$ and start reading the input with a new pointer}:

\medskip
\centerline{
\(
\wordterm{1}{\R}{\state{s}}{\nary k (\extlist{h_1}{\extlist{h_i}{h_k}})}{h_0}  \flow \wordterm{\start}{\R}{\state{s'}}{\nary k (\extlist{h_1}{\extlist{h_0}{h_k}})}{h_i}
\)
}

\medskip
Suppose now we want to write an observation that, if it reads $0\p\L$ in state $\state{r}$, then it restores the value that was stored in the $i$-th position of $\nary k$, it stores the position in $\M$ and changes to state $\state{r'}$, how should we proceed?
The point is that the flow above did not \enquote{memorize} the value that was stored at that position.

\medskip
\centerline{
\(
\wordterm{0}{\L}{\state{r}}{\nary k (\extlist{h_1}{\extlist{h_0}{h_k}})}{h_i} \flow \wordterm{x}{\_}{\state{r'}}{\nary k (\extlist{h_1}{\extlist{h_i}{h_k}})}{h_0}
\)
}

\medskip
The variable $x$ should be free and will be unified with the flow of the word that corresponds to the position constant that was substituted to $h_0$.
But there are two such flows in the word, so the direction of the next movement should be indicated in the $\_$ slot.
Such an information could be encoded in the state $\state{r'}$%
\footnote{That is, we could have two states $\state{r'_{\L}}$ and $\state{r'_{\R}}$ and two flows accordingly.}
and in the transition function.

%From the balanced constrain, it seems clear that we will be able to parse the input, but not to stack any information.
%Morally, all we can do is switch positions between several variables.
%In the setting we are going to define, the algebra $\calg{\TT S}$ is going to encode states, and $\ralg{\TT P}{\balg}$ will be the part where the machine interacts with the input.
%What can it do, well, to may have several copy of the position constant, swap them, but no more.
%In $\ralg{\TT P}{\balg}$ : $\M(h_0)$ and $\nary k(\extlist{h_1}{h_k})$ where $h_i \in \vars$ and $k \in \natural$ ($A$ can even be a constant : in that case, only the main pointer.
%We omit the superscript $k$, that should be clear from context.

%Problem: what to put in the $\_$?
%If $h_i$ is still a variable, not a problem: it will read $\start$, all we have to worry is the direction.
%If $h_i$ already moved, $h_1$ has been substituted by a position constant, and we have to handle that.
%Cannot be two variables, since that would break the constrain on variable inclusions (remember \autoref{def_flow}).

%So we have to \enquote{restore} wisely the pointer, to acknowledge what was the last bit it read, and its direction.
%For that, the most convenient way to do it is to store this information in the states.
%In the previous transition, $\state{s_2}$ should be changed as $\state{s_2\_h_0\_was\_reading\_\start\_\R}$.
%So any state has to encode: the state as e mean it as usual, plus the $k$ couples value-direction for each auxiliary pointers.
%This is quite inefficient, but an usual trick of complexity theorist to encode such a bunch of information in the state, and do not raise any problem.

\subsubsection{Acceptance and Rejection}
Remember (\autoref{lang-reloaded}) 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 head corresponding to the desired situation leading to acceptance, and the body being $0$.
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 forever.
We cannot simply add the unit ($\unit := x \flow x$) to our observation, since that would make our observation loop \emph{no matter the word in input}.
So we have to be clever than that, and to encode rejection as a re-initialization of the observation: we want the observation to put all the pointers on $\start$ and to go back to an $\state{init}$ state.
So, a loop is in fact a \enquote{perform for ever the same computation}.

If we reject, suppose the main pointer was reading from right to left, and that we changed to $\state{b}$.
Then, for every $\TT c \in \Sigma$, it is enough to add the transitions \eqref{reject} and \eqref{reinit} to the observation,

\vspace{-6mm}
\begin{align}
\wordterm{\TT c}{\R}{\state{b}}{\A(\extlist{h_1}{h_k})}{h_0}	& \flow \wordterm{\TT c}{\L}{\state{b}}{\A(\extlist{h_1}{h_k})}{h_0} \label{reject} \tag{go-back-$\TT c$}\\
\wordterm{\start}{\R}{\state{b}}{\A(\extlist{h_1}{h_k})}{h_0}	& \flow \wordterm{\start}{\R}{\state{init}}{\A(\extlist{h_0}{h_0})}{h_0} \tag{re-init} \label{reinit}
\end{align}
\vspace{-6mm}

Once the main pointer is back on $\start$, \eqref{reinit} re-initializes all the positions of the auxiliary pointers to the position of $\start$ and changes the state for $\state{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, \ie if the body (the right-member) of a flow of our observation and the head (the left-member) of a flow of the word can be unified, the computation will start in a possibly \enquote{wrong} initialization.
That some of this incorrect runs accept for incorrect reason is no trouble, since only rejection is \enquote{meaningful} due to the nilpotency criterion.
But, with this framework, an incorrect run will be re-initialized to the \enquote{right} initialization, and performs the correct computation: in that case, it will loop if and only if the input is rejected.

\subsubsection{Two-Ways Multi-Heads Finite Automata and Completeness}
The model we just developed has clearly the same expressivity as two-ways multi-heads finite automata, a model of particular interest to us for it is well studied, tolerant to a lot of enhancements or restrictions%
\footnote{In fact, most of the variations (the automata can be one-way, sweeping, rotating, oblivious, etc.) are studied in terms of number of states needed to simulate a variation with another, but most of the time they characterize the same complexity classes.
%So for instance the circularity of our representation of the input is rather an advantage than a drawback, and it clearly does not enhance the expressiveness of automata.
}
and gives an elegant characterization of \logspace and \nlogspace~\cite{Holzer2008,Pighizzini2013}.
%The reader willing to get numerous results and sources about this model can have a look at recent surveys \cite{Holzer2008,Pighizzini2013}.

Then, by a plain and uniform encoding of two-ways multi-heads finite automata, we get \autoref{th_compl}.
That acceptance and rejection in the non-deterministic case are \enquote{reversed} (\ie all path have to accept for the computation to accepts) makes us characterize \conlogspace instead of \nlogspace.

Note that encoding a \emph{deterministic} automaton yields a wiring of the form of \autoref{lem_det}, which would be therefore a deterministic wiring.
\begin{theorem}\label{th_compl}
If $L\in\conlogspace$, then there is an observation $O$ such that $\lang O=L$. Moreover, if $L\in \logspace$, $O$ can be chosen deterministic.
% \subseteq \lang{\C O_d}$, $\conlogspace \subseteq \lang{\C O}$.
\end{theorem}






%%%%
%%%
% Ci-dessous, plus que des commentaires.
%%
%%%

%One can then easily define an uniform translation,that takes as input a Two-ways Multi-Heads Finite Automata and outputs an observation that will have the same language.
%\begin{definition}[$2$-ways Multi-Head Finite Automata]
%A deterministic (resp. non-deterministic) $2$-ways Finite Automata with $k \in \naturalp$ heads (\DFA{k} (resp. \NFA{k})) is the given of an alphabet $\Sigma$, a non-empty set of states $\state{S}$, an initial state $\state{i} \in \state{S}$ and a transition function (resp. relation) %$\delta$ that takes as argument the values read by the $k$ heads, the current state, and returns (resp. a set of) $k$ movements and a new state, i.e. $\delta \subseteq (\Sigma^k \times \state{S}) \times (\{-1, 0, +1\}^k \times \state{S})$.
%The input, a word over $\Sigma$, is presented between two special characters $\vartriangleright$ and $\vartriangleleft$ (the \emph{endmarkers}) and $\delta$ is such that no head can ever go beyond those endmarkers.
%A configuration is a tuple reflecting the current state, the content of the input tape and the position of the $k$ heads.
%If after a finite number of application of $\delta$, the configuration (resp. configurations) reached are not in the domain of $\delta$, we say that the input is accepted%
%\footnote{Please remark that acceptation is reversed in the non-deterministic case: we want \emph{all computation paths} to stop for the input to be accepted.}%
%, elsewhere it is rejected and the automata loops forever.
%We define the language $\lang{M}$ of a \DFA{k} (resp. \NFA{k}) to be the sets of words over $\Sigma$ that $M$ accepts.
%By extension, the family of all languages accepted by a \DFA{k} (resp. \NFA{k}) is denoted  $\lang{\DFA{k}}$ (resp. $\lang{\NFA{k}}$)
%\end{definition}

%\begin{theorem}
%\label{fa-et-l}
%$\cup_{k\geqslant1}\lang{\DFA{k}} = \logspace$, $\cup_{k\geqslant1}\lang{\NFA{k}} = \conlogspace$.
%\end{theorem}

%\subsubsection{Other Features}
%\begin{align*}
%\wordterm{\start}{\L}{\state{t}}{\A (v)}{h_0} & \flow \wordterm{\start}{\L}{\state{t}}{\A (h_i)}{h_0}
%\end{align*}

%We test at the end  that they are at the same position.
%Even this last test is not mandatory (since only one $\start$ can occurs in $\bar{W}$), we kept it for it involves non-linearity in an elegant way: we can test equality of positions seamlessly.

%Remark that in this setting, the word \emph{is} deterministic, but nothing prevent us from inventing non-deterministic words or more complex structures.

%Rather than giving an abstract method of encoding (that can be easily adapted from a previous work \cite[Sect. 4.2]{Aubert2014}\CLEM{À la réflexion c'est un peu gonflé de renvoyer à ce papier, car la preuve est déjà un "sketch".}), we prefer to give in the following a complex example that should convince the reader that this encoding is uniform (it can be applied blindly to any automata) and quite simple.

%%% Poubelle ?
% a precise definition of what we had in mind when speaking of \enquote{pointer machines}, and a precise proof of how such a device could be encoded by (non-balanced) wirings.
% We chose in this work to focus on a complex example that should help the reader to get intuitions and to grasp how the encoding works.
% We nevertheless recall some notations and peculiarities of our device.

% The course of the computation will be very specific, for the input is not a \enquote{passive} data, there is a constant dialogue between the input and the observation.
% It was formally depicted \cite{Aubert2014} as two different transitions in the automata ($\TT{SWAP}$ and $\TT{MOVE}$), but one can also conceive it as a game, where the observation asks a question, test all the possibilities, and the data answer according to the value and the position encoded.
% \emph{It is the input that moves the main pointer} by updating the constant reflecting the positions.
% Then the observation plays with this data, by swapping pointers, changing its state.
% Thanks to non-linearity, it is now possible to test for equality of position between two pointers, and to make a pointer jump to the position of another. 

%\subsubsection{An Example of Translation}
%Consider a \DFA{2} $M$ such that $\lang{M} = \{1^n 0^n  ~|~ n \in \naturalp\}$, with five states, $\state{i}$, $\state{m}$, $\state{b}$, $\state{l}$ and $\state{r}$.

%We begin the computation in state $\state{i}$, and we move the second head (denoted $H_2$) right until it reads the endmarker $\vartriangleleft$.
%Then we enter in state $\state{m}$, where $H_1$ (the first pointer) move right and $H_2$ move left.
%If $H_1$ reads a $1$ and $H_2$ reads a $0$ we go on, and if $H_1$ reads a $0$ and $H_2$ reads a $1$ we enter in state $\state{b}$.
%In that state, we move $H_1$ and $H_2$ from right to left until $H_2$ read $\vartriangleright$.
%When it does, we switch to state $\state{l}$, where $H_1$ is moved one cell left: if $H_1$ reads also the endmarker we accept, elsewhere we enter in state $\state{r}$.
%cell back and test for equality of position: if $H_1$ and $H_2$ are in the same position we accept, elsewhere we start the computation anew, looping forever.
%All the transition that are not depicted simply goes in the same state $\state{r}$, that corresponds to a \enquote{re-initialization} procedure: $H_1$ moves to $\vartriangleright$, $H_2$ to $\vartriangleleft$ and we start again the computation in state $\state{i}$.
%
%six (relevant) states $\state{m_1}$, $\state{m_2}$, $\state{b_1}$, $\state{b_2}$, $\state{l}$ and $\state{t}$.
%At the beginning of the computation, we leave the first head (denoted $H_1$) on $\vartriangleright$, move the second one (denoted $H_2$) to $\vartriangleleft$, and enter in state $\state{m_1}$.
%As long as $H_1$ scans $0$, we stay in state $\state{m_1}$ and move $H_1$ one cell right.
%When it reads a $1$, it switches to state $\state{m_2}$, and $H_2$ begins to move from right to left.
%The automata stays in state $\state{m_2}$ as long as $H_2$ reads $1$.
%When $H_2$ reads a $0$, we enter in state $\state{b}$: $H_1$ and $H_2$ move one cell back, and we compare when they read $\vartriangleright$. If it is after the same transition we accept, elsewhere we start the computation anew, looping forever.
%All the transition that are not despicted 

%As the pointer in an observation cannot move at the same time, we will be forced to decompose the transition involving two movement of pointers in two, but beside that the encoding is rather straightforward.
%The observation will be the sum of the flows \eqref{ce-t_1}--\eqref{ce-t_9} given in \autoref{fig-flow}.

%We give the encoding of an observation $\obs{O}$ such that $\lang{\obs{O}} = \lang{M}$.
%Applying \autoref{lang-obs}, this means that $\isnilp{\obs{O}\bar{W}_{p}}$ if and only if $\exists n \in \naturalp$ such that $W = \star 1^n 0^n$.

%\begin{figure}
%\newcommand{\labelettag}[1]{\tag{\small{$#1$}} \label{ce-#1}}
%\begin{align*}%
%\wordterm{1}{\R}{\state{m_1}}{\A(h_2)}{h_1}		& \flow \wordterm{1}{\L}{\state{m_1}}{\A(h_2)}{h_1} 			\labelettag{t_1}\\
%\wordterm{0}{\R}{\state{m_1}}{\A (h_2)}{h_1}		& \flow \wordterm{0}{\L}{\state{m_2}}{\A(h_1)}{h_2} 			\labelettag{t_2}\\
%\\
%\wordterm{0}{\L}{\state{m_2}}{\A (h_1)}{h_2}		& \flow \wordterm{0}{\R}{\state{m_2}}{\A(h_1)}{h_2} 			\labelettag{t_3}\\
%\wordterm{1}{\L}{\state{m_2}}{\A (h_1)}{h_2}		& \flow \wordterm{0}{\L}{\state{b_1}}{\A(h_1)}{h_2} 			\labelettag{t_4}\\
%\\
%\wordterm{0}{\L}{\state{b_1}}{\A (h_1)}{h_2}		& \flow \wordterm{0}{\R}{\state{b_2}}{\A(h_2)}{h_1} 			\labelettag{t_5}\\
%\wordterm{0}{\L}{\state{b_2}}{\A (h_2)}{h_1}		& \flow \wordterm{0}{\R}{\state{b_1}}{\A(h_1)}{h_2} 			\labelettag{t_6}\\
%\\
%\wordterm{\start}{\L}{\state{b_2}}{\A (h_2)}{h_1}		& \flow \wordterm{\start}{\L}{\state{l}}{\A(h_1)}{h_2} 	\labelettag{t_7}\\
%\wordterm{\start}{\L}{\state{l}}{\A (h_1)}{h_2}		& \flow \wordterm{\start}{\L}{\state{t}}{\A(h_1)}{h_2} 	\labelettag{t_8}\\
%\wordterm{\start}{\L}{\state{t}}{\A (v)}{h_0}			& \flow 0 												\labelettag{t_9}
%\end{align*}
%\caption{Encoding an observation that accepts $\start 1^n 0^n$}
%\label{fig-flow}
%\end{figure}
%
%The first head moves from left to right: as long as it reads $1$, it goes on \eqref{ce-t_1}.
%When it reads a $0$ \eqref{ce-t_2}, it stays in position and become the auxiliary pointer ($h_2$ and $h_1$ exchange their positions).
%Then the second pointer goes back, from right to left, and goes on until it reads a $0$ \eqref{ce-t_3}.
%When it reads a $1$ \eqref{ce-t_4}, it changes its direction and goes back on the last $0$ it read.
%At \eqref{ce-t_5} and \eqref{ce-t_6}, the main and auxiliary pointers switch roles at every transition.
%They go one bit by one bit to the begging of the tape, scanning only $0$'s.
%
%If the input is of the desired form, the first pointer will scan $\start$ before the second pointer.
%Then, we perform one last movement with the second pointer, that should read a $\start$.
%We test at the end \eqref{ce-t_9} that they are at the same position.
%Even this last test is not mandatory (since only one $\start$ can occurs in $\bar{W}$), we kept it for it involves non-linearity in an elegant way: we can test equality of positions seamlessly.

%The fact that no flow has for state $\state{t}$ on its left-hand reflect the fact that this state is terminal: once this state is reached, no transition can take place.

%\CLEM{Les problèmes sont les suivants : 
%* la dernière valeur lue par le pointeur qui passe auxiliare doit etre stockée dans l'état, et les transitions modifiées pour en tenir compte.
%* dire "on ajoute toutes les autres transitions vers l'état $\state{r}$" est trop vague en l'état. À l'opposé, les décrire est pénible.
%* L'observation telle que rédigée teste $1^n0^m$, avec $n$ et $m$ pas forcément égaux. Dans la première phase, $h_1$ et $h_2$ doivent bouger en meme alternativement, ce qui rajoute plein d'alterances un peu chiantes à formuler.
%* Le teste de position \eqref{ce-t_9} est trompeur : si les deux pointeurs ne sont pas à la meme position, on ne peut pas unifier, et … le calcul s'arrete, ce qui corresponds à accepter. On n'a pas de "contre-test", "si les deux pointeurs ne ont pas à la meme position (ce qui nécessite un $x \neq y$ d'une façon ou d'une autre), alors fais cela.}

conclusion.tex
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.

\smallskip

If we try to step back a little, we can notice that the main tool in the soundness proof (\autoref{sec_soundness}) is the computation graph, defined in \autoref{sec_compgraph}.
More precisely, the properties of this graph, notably its cardinal (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.

\smallskip
Concerning completeness, the choice of encoding pointer machines (\autoref{sec_comleteness}) 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 that a modifcation of the representation of the input that would model one-way finite automata.


\smallskip
The relation with proof theory needs to be explored further: the approach of this paper seems indeed to suggest a sort of \enquote{Curry-Howard} correspondance for logic programming.

As \autoref{ssec_goilp} 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 \enquote{balanced} logic of logarithmic space.

%* Résumé de ce qui a été fait



%* Perspectives : 

%** Univers d’Herbrand : contrainte sémantique pour borner les programmes


%** Étendre avec des piles pour caractériser $\ptime$.


%** Contraintes sur le sens de lecture ($1$-way, $2$-ways) de l'entrée vient de la représentation de l’entrée, pas des automates.
%\MARC{Pourquoi en conclusion?}

goiandlp.tex

The geometry of interaction program (\GoI for short), started in 1989~\cite{Girard1989b}, 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 \emph{Curry-Howard correspondence} between sequent calculus derivations and typed functional programs: it is on the basis of this correspondence that \hbox{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~\cite{Girard1987} 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~\cite{Girard1989a}, derivations in second order intuitionistic logic \LJs (which can be considered, by \emph{Curry-Howard}, as programs in \systF) are interpreted as pairs $(U,\sigma)$ of elements (called \emph{wirings}) of a $\mathbb{C}^{*}$-algebra, $U$ corresponding to the axioms of the derivation and $\sigma$ to the cuts.

The main property of this interpretation is \emph{nilpotency}: there exists an integer $n$ such that $(\sigma U)^{n}=0$.
The cut-elimination (equivalently, the normalization) procedure is then interpreted by the application of an \emph{execution operator}

\medskip
\centerline{$EX(U,\sigma)=\sum_{k}(\sigma U)^{k}$}
\medskip
From the viewpoint of proof theory and computation, nilpotency corresponds to the \emph{strong normalization property}: the termination of the normalization procedure with any strategy.

Several alternative formulations of geometry of interaction have been proposed since 1988 (see for instance~\cite{Asperti1994,Laurent2001,Seiller2012a}); in particular, wirings can be described as logic programs~\cite{Girard1995a,Baillot2001,Girard2013} made of particular clauses called \emph{flows}, which will be defined in \autoref{sec_flows}.

% an approach which constitutes the main source of inspiration for this paper: given a set of first-order terms $\terms$ and two terms $t,u\in \terms$ such that $\var(t)\subseteq \var(u)$, one calls an object of the form $t\flow u$ a \emph{flow} (\autoref{def_flow}, read \enquote{clause}) and a finite set of flows a \emph{wiring}  (\autoref{def_wirings}, read \enquote{logic program}).

In this setting the resolution rule induces a notion of product of wirings (\autoref{def_wirings}) and in turn a structure of semiring: the \emph{unification semiring} $\ualg$, which can replace the $\mathbb{C}^{*}$-algebras of the first formulations of \GoI\footnote{By adding complex scalar coefficients, one can actually extend $\ualg$ into a $\mathbb{C}^{*}$-algebra~\cite{Girard1995a}.}.

The $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 \emph{boundedness}~\cite{Dantsin2001} of logic programs.


%That puts in light the novelty and power of the constrain we are going to introduce in \autoref{def-balanced}, that allow to enforce a bound on the space needed to simulate the logic program, and hence a bound on its run-time.
%However, this bound is relative to the size of the input.

\smallskip
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 \systF.

This is quite striking in view of the fact that to decide whenever a program is \emph{bounded}%
\footnote{A program is \emph{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 inputed.}
is --~even with drastic constraints~-- an undecidable problem~\cite{Hillebrand1995}, and that in general boundedness is a property that is difficult to ensure.
 %the boundedness problem (to decide whether or not a logic program is bounded) was shown \cite{Hillebrand1995} to be --~even with drastic constraints~-- undecidable, and that in general boundedness is a property that is difficult to ensure.

intro_log-space.tex
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.
%any language in \conlogspace can be decided by an observation, and that it can be restricted as well to the deterministic case.
Then, we will prove how the language of an observation can be decided within logarithmic space.

This section uses the complexity classes \logspace and \conlogspace, as well as notions of completeness of a problem and reduction between problems.
We use in \autoref{sec_soundness} the classical theorem of \conlogspace-completeness of the acyclicity problem in directed graphs,
%\logspace- (resp. \nlogspace-) completeness of the acyclicity problem in undirected (resp. directed) graphs,
 and in \autoref{sec_comleteness} a convenient model of computation, two-ways multi-heads finite automata, a generalization of automata also called \enquote{pointer machine}.
The reader who would like some reminders may have a look at any classical textbook~\cite{Savage1998}.
Note that the non-deterministic part of our results concerns \conlogspace, or equivalently \nlogspace by the famous Immerman-Szelepcsényi theorem.

intro.tex
\vspace{-3mm}
\subsubsection{Proof Theory and Implicit Complexity Theory}
Very generally, the aim of implicit complexity theory (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 \cite{Girard1987}) and ICC,
the basic idea being to look for restricted substructural logics~\cite{Girard1995} with 
an expressiveness that corresponds exactly to some complexity class.

This has been achieved by various syntactic restrictions, which entail a less complex
(any function provably total in second-order Peano Arithmetic~\cite{Girard1987} can be encoded in second-order linear logic)
cut-elimination procedure: control over the modalities \cite{Schopp2007,Lago2010},
type assignments \cite{Gaboardi2012} or stratification properties \cite{Baillot2010},
to name a few.

\subsubsection{Geometry of Interaction} Over the 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~\cite{Girard1989a} is to provide the tools for such a modeling~\cite{Asperti1994,Laurent2001,Seiller2012a}.

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 \cite{Baillot2001,Girard2012,Aubert2014}.

\subsubsection{Unification} The unification technique 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~\cite{Girard1995a,Baillot2001,Girard2013} where first-order terms with variables allow for a manipulation of infinite sets through a finite language.

\subsubsection{Logic Programming} After the work of Robinson on the resolution procedure, logic programming has emerged as a new computation paradigm with concrete realizations such as the languages \proglang{Prolog} and \proglang{Datalog}.

On the theoretical side, a lot of efforts has been made to clarify expressiveness 
and complexity issues~\cite{Dantsin2001}:
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 \emph{finitely ground program}~\cite{Calimeri2008} is related to our approach.

\subsubsection{Pointer Machines}
Multi-heads finite automata provide an elegant characterization of logspace 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 \enquote{pointer machines}.%, even if this nomenclature may be misleading \cite{Ben-amram1995}.

This model was already at the heart of previous works relating geometry of interaction and complexity theory~\cite{Girard2012,Aubert2012,Aubert2014}.

\medskip

\subsubsection{Contribution and Outline}
We begin by exposing the idea of relating geometry of interaction and logic programming, already evoked~\cite{Girard1995a} 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 \autoref{sec_ualg} the algebraic tools
used later on to define the encoding of words and pointer machines.%
\renewcommand{\subsectionautorefname}{Section} % Au début d’une phrase, on abbrège pas le "Section"
\autoref{sec_balanced}%
\renewcommand{\subsectionautorefname}{Sect.} % On restaure l’abbréviation. 
and \autoref{sec_compgraph} introduce the syntactical
 restriction and associated tools that allow us to characterize logarithmic space computation.
Note that, compared to earlier work~\cite{Aubert2014}, 
we consider a much wider class of programs while preserving bounded space evaluation.

The encoding of words enabling our results,
which comes from the classical (Church) encoding of lists in proof theory,
is given in \autoref{sec_representation}.
It allows to define the counterpart of programs, and a notion of acceptance of a word by a program.

Finally, \autoref{sec_complexity} makes use of the tools introduced earlier
to state and prove our complexity results. While the expressiveness part 
is quite similar to earlier presentations~\cite{Aubert2012,Aubert2014}, the proof that acceptance %LSP
can be decided within logarithmic space has been made more modular
by reducing it to cycle search in a graph.

intro_WaO.tex
%\CLEM{Sauf erreur de ma part, il n’est mentionné nul part que tout ça est balancé. Ça ne serait pas utile de le rappeler ?}
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.

\begin{definition}[word and observation semirings]
	We fix two (disjoint) infinite sets of constant symbols $\TT P$ and $\TT S$, and a unary function symbol $\M$.
	We denote by $\M(\TT P)$ the set of terms $\M(\TT p)$ with $\TT p\in\TT P$.
	We define the following two semirings that are included in $\balg$:
	\begin{itemize}	
	\item The \emph{word semiring} is the semiring $\walg:=\C \unitalg\ptensor\unitalg\ptensor \calg{\TT M(\TT P)}$.
	\item The \emph{observation semiring} is the semiring $\oalg:=\calg{\TT S}\ptensor\ralg{\TT P}{\balg}$.
%	\THOMAS{Je persiste à dire que $\balg$ est une notation trop pauvre; ici c'est $\balg_{\calg{\TT P}}$ qu'on voudrait..}
	\end{itemize}
\end{definition}

These two semirings will be used as parameters of a construction $\matr{\Sigma}{.}$ to define the representation of words and a notion of abstract machine, that we shall call observations, on an alphabet $\Sigma$ (we suppose $\star\not\in\Sigma$). %The semirings $\oalg$ and $\walg$ just defined will be used as parameters in a construction $\matr{\Sigma}{.}$.

\begin{definition}
	We fix the set of constant symbols $\LR:=\{\L,\R\}$.
	
	Given a set of constant symbols $\Sigma$ and a semiring $\C A$ we define the semiring $\matr{\Sigma}{\C A}:=\calg{(\Sigma\cup\{\star\})} \ptensor \calg\LR\ptensor\C A$.
\end{definition}

In the following of this section, we will show how to represent lists of elements of $\Sigma$ by 
wirings in the semiring $\matr{\Sigma}{\walg}$. 
Then, we will explain how the semiring $\matr{\Sigma}{\oalg}$ 
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.

macros.tex
% polices math
\newcommand{\C}[1]{\mathcal{#1}}
\newcommand{\F}[1]{\mathfrak{#1}}
\newcommand{\BB}[1]{\mathbb{#1}}
\newcommand{\BF}[1]{\mathbf{#1}}
\newcommand{\RM}[1]{\mathrm{#1}}
\newcommand{\SF}[1]{\mathsf{#1}}
\newcommand{\IT}[1]{\mathit{#1}}
\newcommand{\TT}[1]{\mathtt{#1}}

% flows
% Je ne vois pas trop l’utilité de ces calages :
%\newcommand{\flow}{\,\scalebox{1.1}{$\leftharpoonup$}\,}			% fleche des flots
%\newcommand{\sflow}{\,\scalebox{1.1}{$\leftrightharpoons$}\,}		% flot symetrique: u<-v + v<-u

\newcommand{\flow}{\ensuremath{\leftharpoonup}}		% flot symetrique: u<-v + v<-u
\newcommand{\pflow}{\downharpoonleft\!}							% projection sur un terme
\newcommand{\sflow}{\ensuremath{\leftrightharpoons}}		% flot symetrique: u<-v + v<-u

\newcommand{\query}[1]{\querysym \flow #1}						% requetes LP
\newcommand{\fact}[1]{#1\flow\factsym}							% facts LP
\newcommand{\wiring}[1]{#1}										% Wiring, ne fait rien pour le moment.
\newcommand{\mgu}[1]{\IT #1}										% Most General Unifier
\newcommand{\obs}[1]{\ensuremath{#1}}							% Observation. Police sans doute à revoir

% algebres
\newcommand{\balg}{{\C U_b}}	%balanced
\newcommand{\dalg}{\C U_d}	%deterministic
\newcommand{\ualg}{\C U}	%unif algebra
\newcommand{\calg}[1]{#1^\leftharpoonup}	%closed
\newcommand{\walg}{\C W}		% words
\newcommand{\salg}{\C S}		% states
\newcommand{\ralg}[2]{#2^{\setminus #1}} % restriction
\newcommand{\oalg}{\C O} % observations
\newcommand{\wordalg}{\C \unitalg\ptensor\unitalg\ptensor \calg{\TT M(\TT P)}}	% word, expanded
\newcommand{\matr}[2]{\C M_{#1}\left(#2\right)}

% produit tensoriel
\newcommand{\tpower}[1]{^{\otimes #1}}		%n-ème puissance tensorielle
\newcommand{\ptensor}{\,\dot{\otimes}\,}		%produit tensoriel de flots

% comp vector, comp graph
\newcommand{\comp}[1]{\BF{Comp}(#1)}
% macros lettre font spécifique
\newcommand{\G}{\BF G}
\newcommand{\h}{\TT h} 
\newcommand{\M}{\TT M}
\newcommand{\A}{\TT A}

% termes, symboles spécifiques
\renewcommand{\L}{\TT{L}}
\newcommand{\R}{\TT{R}} % Je ne comprends pas trop d’où venait ce \scriptsize. S’il est rétabli, le rétablir sur \L et \LR.
\newcommand{\LR}{\TT{LR}}
\newcommand{\start}{\star}
\newcommand{\p}{\scalebox{0.6}{$\,\bullet\,$}}
\newcommand{\querysym}{\star}
\newcommand{\factsym}{\star}
\newcommand{\nary}[1]{\TT A_{#1}}

%rep entiers
\newcommand{\wordterm}[5]{\TT{#1} \p #2 \p #3 \p #4 \p \M(#5)}
% Emploi / ordre des valeurs :
% valeur encodée
% sens, i.e. \R ou \L
% état de la machine
% pointeurs aux.
% Position de la tête de lecture (pointeur principal)
\newcommand{\wordrep}[2]{W[\extlist{\,\TT #1}{\TT #2}]}
\newcommand{\setofrep}[1]{\C{R}(#1)} % Set of representations of a word

% observations
\newcommand{\isnilp}[1]{\BF{Nil}(#1)} % Is nilpotent


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% general math
\newcommand{\extlist}[2]{#1,\,\dots\,,#2}		% liste/suite en extension
\newcommand{\extset}[2]{\left\{\,#1,\,\dots\,,#2\,\right\}}		% ensemble en extension
\newcommand{\set}[2]{\left\{\:#1 \ \middle|\ #2\:\right\}}	% ensemble en comprehension
\newcommand{\seq}{\,\textbf{;}\,}			% composition sequentielle
\newcommand{\iso}{\xrightarrow[]{\,_\sim}}	% fleche isomorphisme
\newcommand{\void}{\varnothing}				% ensemble vide
\newcommand{\unitalg}{\C I}					% algebres engendrée par l'unité
\newcommand{\unit}{I}						% unité
\newcommand{\numberset}[1]{\ensuremath{\mathbb{#1}}}	%Tous les ens. seront ainsi.
\renewcommand{\natural}{\numberset{N}} 					%Entiers naturels
\newcommand{\naturalp}{\numberset{N^*}} 				%Entiers naturels
%\renewcommand{\max}{\texttt{\textit{max}}}				%max Clem : changement de police, pas joli comme ça.
\renewcommand{\max}{\mathop{\mathrm{max}}}


% informatique, termes, automates
\renewcommand{\problem}[1]{\textsc{#1}}		% probleme
\newcommand{\proglang}[1]{\textsc{#1}}		% langage de prog
\newcommand{\dom}{\TT{Dom}}									% domaine
\newcommand{\var}{\TT{Var}}									% variables
\newcommand{\uequ}{\raisebox{-1pt}{$\,\stackrel{\TT ?}\texttt{=}\,$}} % equation d'unification =?
\newcommand{\vars}{\TT{V}}				%variables
\newcommand{\const}{\TT{C}}				%constantes
\newcommand{\terms}{\TT{T}}				%termes
\newcommand{\closed}{\TT{T_{\TT{c}}}}	%termes clos
\newcommand{\langage}[1]{\mathcal{#1}}	%Langage
\newcommand{\lang}[1]{\langage{L}(#1)}	%Langage d'une machine, d'une observation
\newcommand{\state}[1]{\BF{#1}}

% logique, symboles LL
\newcommand{\LP}{\proglang{LP}\xspace}
\newcommand{\GoI}{\proglang{GoI}\xspace}
\newcommand{\systF}{System~\proglang{F}\xspace}
\newcommand{\LJs}{\proglang{LJ$^2$}\xspace}

% Complexité
%\newcommand{\card}[1]{\texttt{\textit{card}}(#1)} 	% Cardinal Clem : la police était vraiment moche.
\newcommand{\card}[1]{\mathop{\mathrm{card}}(#1)}
\newcommand{\bigO}{\ensuremath{\mathcal{O}}} 			% Big O notation
\newcommand{\cc}[1]{\textsc{#1}\xspace}					% Classe de comelexité
\newcommand{\logspace}{\cc{D\-Log\-space}}							% Logspace
\newcommand{\nlogspace}{\cc{N\-Log\-space}}							% N-Logspace
\newcommand{\conlogspace}{\cc{co\nlogspace}}		% co-N-Logspace
\newcommand{\ptime}{\cc{Ptime}}								% Ptime
\newcommand{\nc}{\cc{NC}}								% Nick's Class, NC

% signalisation, commentaires
%\newcommand{\TODO}[1]{{\color{red}\bfseries{#1}}}
%\newcommand{\CLEM}[1]{{\color{blue}\textbf{Clément : #1}}}
%\newcommand{\PAOLO}[1]{{\color{green}\textbf{Paolo : #1}}}
%\newcommand{\MARC}[1]{{\color{magenta}\textbf{Marc : #1}}}
%\newcommand{\THOMAS}[1]{{\color{orange}\textbf{Thomas : #1}}}

% Abbréviations
\newcommand{\ie}{\textit{i.e.}\xspace}
\renewcommand{\iff}{\text{iff}\xspace}
\newcommand{\eg}{e.g.\xspace}
\newcommand{\cf}{cf.\xspace}
\newcommand{\etc}{{\it etc.}\xspace}
\newcommand{\via}{\emph{via}\xspace}
\newcommand{\vs}{\emph{versus}\xspace}
\newcommand{\aka}{\emph{a.k.a.}\xspace}
\newcommand{\re}{{\it r.e.}\xspace}
\newcommand{\vv}{\emph{vice-versa}\xspace}
\newcommand{\wrt}{with respect to\xspace}
\newcommand{\Wlog}{Without loss of generality\xspace}
\newcommand{\wlg}{without loss of generality\xspace}
packages.tex
%%% encodage et langue
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage[english]{babel} % document en anglais

%%% extending tex
\usepackage{etex}
\usepackage{xargs,ifthen}
\usepackage{fixltx2e} 			% \textsubscript, corrige erreurs de Latex.
\usepackage{lmodern}				% Latin Modern = enhanced Computer Modern.
%\usepackage{fnpct}				% Amélioration des notes de bas de page.

%%% writing algorithms
\usepackage{algorithm,algorithmic}

%%% Drawings
\usepackage{tikz}
\usetikzlibrary{automata,positioning}
\usetikzlibrary{arrows,calc}

%%% layout and typography
\usepackage{blindtext}
\usepackage{microtype}
\usepackage{csquotes}
\usepackage{enumitem}
	\setitemize{itemsep=1pt,topsep=3pt,parsep=0pt,partopsep=0pt}
\usepackage{xcolor}
\definecolor{persimmon}{rgb}{0.93, 0.35, 0.0}
\definecolor{cssgreen}{rgb}{0.0, 0.5, 0.0}
\usepackage{hyperref}
	\hypersetup{
		plainpages			=	false,		% Pages anchors are named by the Arabic form
		bookmarksnumbered	=	true,		% put section numbers in bookmarks
		bookmarksopen		=	true,		% Par défaut la barre des favoris est ouverte.
		bookmarksdepth		=	2,			% À profondeur 2.
		colorlinks			=	true, 		% False = encadrés, True = mis en couleur
		breaklinks			=	true,		% Pour les césures
		linkcolor			=	persimmon,	% liens internes
		citecolor			=	cssgreen,	% Pour les citations
		pdfdisplaydoctitle	= 	true,		% display document title instead of file name in title bar,
	}
\usepackage{xspace}
\usepackage{multicol}
\usepackage{wrapfig}
\usepackage{graphicx}

%%% symboles math, theoremes, police
\usepackage{amsmath,amssymb}
\usepackage{mathtools}

%%% réseaux et logique
\usepackage{stmaryrd}
\usepackage{cmll}

% Hack pour les renvois aux sections.
\addto\extrasenglish{%
\renewcommand{\sectionautorefname}{Sect.}
\renewcommand{\subsectionautorefname}{Sect.}
}
% The following should be abbreviated when they appear in running text unless they come at the beginning of a sentence: Chap., Sect., Fig.
\renewcommand{\equationautorefname}{Eq.}
\def\appendixautorefname{Appendix}
\newcommand{\aref}[1]{\hyperref[#1]{Appendix~\ref{#1}}} % Bogue hyperref / autoref avec les appendices


%\usepackage[l2tabu]{nag}
\usepackage{dialogue}

sec_observations.tex
We now define \emph{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
\[\calg{(\Sigma\cup\{\star\})} \ptensor \calg\LR\ptensor(\calg{\TT S}\ptensor\ralg{\TT P}{\balg})\]
Once again, the part of the semiring $\calg{(\Sigma\cup\{\star\})} \ptensor \calg\LR$ is dependent on the alphabet $\Sigma$ considered and represents the point of interaction between the words and the machine. 
The semiring $\calg{\TT S}$ intuitively corresponds to the \emph{states} of the observation, 
while the part $\ralg{\TT P}{\balg}$ forbids the machine to act non-trivially on the \emph{position constant} of the representation of words. 
The fact that the machine cannot perform any operation on the memory addresses --~the position constants~-- of the word representation explains why observations are naturally though of as a kind of \emph{pointer machines}.

\begin{definition}[observation]
	An \emph{observation} is any element $\obs{O}$ of $\matr{\Sigma}{\oalg}$.
\end{definition}

We can define the language associated to an observation.
The condition of acceptance will be represented as the nilpotency of the product $\obs{O}\bar{W}_{p}$ where $\bar{W}_{p}\in\setofrep{W}$ represents a word $W$ and $\obs{O}$ is an observation.

%\THOMAS{Je vous laisse déplacer ça:\\
%We will therefore use the following notation:
%\[\isnilp{A}:=\exists k \geqslant 0, A^{k}=0\]
%\CLEM{J’aime bien cette notation, mais il faut l’introduire dès \autoref{def_nilp} et l’employer.}
%\MARC{A voir selon l'usage: introduire une notation ``Nil(A)'' pour ``A is nilpotent'', le gain de place est minime.}
%\CLEM{Mais ça vite de faire des phrases. Vite vu, on emploie la macro 5 fois, il y a une petite dizaine d’autres endroits où on pourrait l’employer.}}

\begin{definition}[language of an observation]
\label{lang-obs}
Let $\obs{O}$ be an observation on the alphabet $\Sigma$.
We define the \emph{language accepted by $\obs{O}$} as

\smallskip
\centerline{
\(\lang{\obs{O}}:=\set{W\in \Sigma^{\ast}}{\forall p, \,\isnilp{\obs{O}\bar{W}_{p}}}\)
}

%\smallskip
%This definition extends to any set $\C O$ of observations: let $\lang{\C O}=\{\lang{\obs{O}}~|~ \obs{O} \in \C O\}$.
%If this set contains only deterministic observations, we write $\lang{\C O_d}$.
\end{definition}
%\CLEM{Deux points : c’est $\obs{O}\bar{W}_{p}$ (ci-dessus) ou $\bar{W}_{p}\obs{O}$ (ci-dessous)? Je dirai que c’est Obs Entier. + Je trouve la notation $\bar{W}_{p}$ pas trop belle. $\bar{W_{p}}$? }\THOMAS{$\bar{W}_{p}$??}

One important point is that the semirings $\matr{\Sigma}{\walg}$ and $\matr{\Sigma}{\oalg}$ 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. 
%This is stated in the following lemma.

\begin{lemma}
\label{equiv-of-rep}
Let $W$ be a word, and $\bar{W}_{p}, \bar{W}_{q}\in\setofrep{W}$.
For every observation $\obs{O}\in \matr{\Sigma}{\oalg}$, $\isnilp{\obs{O}\bar{W}_{p}}$ if and only if $\isnilp{\obs{O}\bar{W}_{q}}$.
\end{lemma}

\begin{proof}
As we pointed out, the observation cannot act on the position constants of the representations $\bar{W}_{p}$ and $\bar{W}_{q}$.
This implies that for all integer $k$ the wirings $(\obs{O}\bar{W}_{p})^{k}$ and $(\obs{O}\bar{W}_{q})^{k}$ are two instances of the same \emph{context}, \ie they are equal up to the interchange of the positions constants $\extlist{\TT p_{0}}{\TT p_{n}}$ and $\extlist{\TT q_{0}}{\TT q_{n}}$.
This implies that $(\obs{O}\bar{W}_{p})^{k}=0$ if and only if $(\obs{O}\bar{W}_{q})^{k}=0$.
\qed
%, i.e. $\isnilp{\obs{O}\bar{W}_{p}}$ if and only if $\isnilp{\obs{O}\bar{W}_{q}}$ (with equal degrees of nilpotency).
%\THOMAS{Est-ce qu'on fait la preuve ou on se contente de citer?}
%\CLEM{On cite \& donne une idée de preuve assez vague.}
%\MARC{Ce n'est pas la même technique, la preuve est potentiellement plus simple (pas d'occurence des symboles de constantes utilisés par le mot côté observation. On peut faire un sketch ça prendra 2 lignes.}
\end{proof}

%The corollary below is important because it allows to verify
%whether a word $W$ is accepted by an observation $O$ can be done
%without considering all representations of $W$.

\begin{corollary}%
\label{lang-reloaded}
Let $\obs{O}$ be an observation on the alphabet $\Sigma$.
The set $\lang{\obs{O}}$ can be equivalently defined as the set

\smallskip
\centerline{
\(\lang{\obs{O}}=\set{W\in \Sigma^{\ast}}{\exists p,\, \isnilp{\obs{O}\bar{W}_{p}}}\)
}
\end{corollary}

This result implies that the notion of acceptance has the intended sense and is finitely verifyable: whether a word $W$ is accepted by an observation $O$ can be checked
without considering all representations of $W$.

%It is here a consequence of the definitions of the word and observations semirings $\walg$ and $\oalg$. 
%Indeed, the interaction between the representations of words and the observations is restricted to the part $\calg{(\Sigma\cup\{\star\})} \ptensor \calg\LR$ dealing with the alphabet $\Sigma$.

This kind of situation where two semirings $\walg$ and $\oalg$ are disjoint enough to obtain \autoref{lang-reloaded} can be formalized through the notion of \emph{normative pair} considered in earlier works \cite{Girard2012,Aubert2012,Aubert2014}.


%\THOMAS{Un petit mot sur la suite.}
%
%\CLEM{Un mot ici aussi sur déterminisme ? Préciser que l’entier est toujours déterministe, mais pas l’observation ? Renvoi : \autoref{def_fun}}

SECTIONS.tex
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% TITRE
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\title{Logic Programming and Logarithmic Space}
\author{
	Clément Aubert\inst{1} \and Marc Bagnol\inst{1} \and Paolo Pistone\inst{1} \and Thomas Seiller\inst{2}
	\thanks{This work was partly supported by the ANR-10-BLAN-0213 Logoi and the ANR-11-BS02-0010 Récré.}}
\institute{Aix Marseille Université, CNRS, % Centrale Marseille, (on est vraiment obligés? ça pourrit la mise en page et on n'a rien à voir avec centrale...)
			I2M UMR 7373, 13453, Marseille, France
			\and I.H.\'{E}.S., Le Bois-Marie, 35, Route de Chartres, 91440 Bures-sur-Yvette, France}

\hypersetup{
	pdfinfo={
		Author		=	{Clément Aubert, Marc Bagnol, Paolo Pistone, Thomas Seiller},
		Title		=	{Logic Programming and Logarithmic Space},
		Keywords	=	{Implicit Complexity, Unification, Logic Programming, Logarithmic Space, Proof Theory, Pointer Machines, Geometry of Interaction, Automata},
		Creator		=	{PDFLaTeX},
		Producer	=	{PDFLaTeX},
		Lang		=	{en}
	}
}

\maketitle

%%%%%%%%%%%% CHAPTERS and SECTIONS
%\CLEM{Résumé entre 70 et 150 mots} 
\begin{abstract}
	\input{abstract}
\end{abstract}

\keywords{Implicit Complexity, Unification, Logic Programming, Logarithmic Space, Proof Theory, Pointer Machines, Geometry of Interaction, Automata}

\section{Introduction}
	\input{intro}
	\subsection{Geometry of Interaction and Logic Programming}\label{ssec_goilp}
	\input{goiandlp}
	\subsection{Unification and Complexity}\label{ssec_unif}
	\input{unification}

\section{The Unification Semiring}\label{sec_ualg}
	\input{ualgebra}
	\subsection{The Balanced Semiring}\label{sec_balanced}
	\input{balanced}
	\subsection{The Computation Graph}\label{sec_compgraph}
	\input{compgraph}
	\subsection{Tensor product and other semirings}
	\input{tensor}

\section{Words and Observations}\label{sec_representation}
	\input{intro_WaO}
	\subsection{Representation of Words}\label{sec_words}
	\input{sec_words}
	\subsection{Observations}\label{sec_observations}
	\input{sec_observations}
	
\section{Logarithmic Space}\label{sec_complexity}
	\input{intro_log-space}
	\subsection{Completeness: Observations as Pointer Machines}\label{sec_comleteness}
	\input{completeness}
	\subsection{Soundness of Observations}\label{sec_soundness}
	\input{soundness}

\section{Conclusion}
	\input{conclusion}

\bibliographystyle{splncs03}
\bibliography{court,biblio}
\addcontentsline{toc}{section}{References}

sec_words.tex
We now show how one can represent words by wirings in $\matr{\Sigma}{\walg}$. We recall this semiring is defined as 
\(\big(\calg{(\Sigma\cup\{\star\})} \ptensor \calg\LR\big)\ptensor\C \unitalg\ptensor\unitalg\ptensor \calg{\TT M(\TT P)}\).

The part $\calg{(\Sigma\cup\{\star\})} \ptensor \calg\LR$ deals with, and is dependent on, the alphabet $\Sigma$ considered;
this is where the integer and the observation will interact.
The two instances of the unit semiring $\unitalg$ correspond to the fact that the word cannot affect parts of the observation
that correspond to internal configurations.
%an observation can have a non-trivial action on this part of the semiring.
The last part, namely the semiring $\calg{\TT M(\TT P)}$, will contain the \emph{position constants} of the representation of words.

%\CLEM{J’aime bien l’explication mais je me demande si on ne gagnerait pas en lisibilité en faisant
%\[
%\underbrace{\calg{(\Sigma\cup\{\star\})} \ptensor \calg\LR}_{1}
%\ptensor (
%\underbrace{\C \unitalg \ptensor(\unitalg}_{2}
%\ptensor (
%\underbrace{\calg{\TT M(\TT P)}}_{3}
%)))\]
%Et ensuite : "$1$ is the part where the data and the observation will interact. It is …" Ça permets de se dégager du parenthésage qui ne colle pas.
%}

%\THOMAS{Je propose de modifier les représentations et d'utiliser des parenthèses: $(\TT{c_{i}} \p L) \p (x \p y) \p \M(p)$ pour distinguer les parties alphabet/machine/entier. Cela va avec l'écriture des algèbres sous la forme $(\C M_{\Sigma,\LR})\ptensor(\C \unitalg\ptensor\unitalg)\ptensor (\calg{\TT M(\TT P)})$ et $(\C M_{\Sigma,\LR})\ptensor(\calg{\TT S})\ptensor(\ralg{\TT P}{\balg})$. Cela permet des explications plus intuitives.}\CLEM{Je suis pour}
%\MARC{Mais malheureusement ça marche pas comme ça. On en discute sur skype.}

\begin{notation}
	We write $t\sflow u$ for $t\flow u +u\flow t$.
\end{notation}


\begin{definition}[word representations]\label{word-rep}
	Let $W= \TT c_1\dots\TT c_n$ be a word over an alphabet $\Sigma$ and $p=\extlist{\TT p_0,\TT p_1}{\TT p_n}$ be pairwise distinct constant symbols.
	
	Writing $\TT p_{n+1}=\TT p_{0}$ and $\TT{c_{0}} = \TT{c_{n+1}} = \start$, we define the \emph{representation} of $W$ associated with $\extlist{\TT p_0,\TT p_1}{\TT p_n}$ as the following wiring: % which is an element of $\matr{\Sigma,\LR}{\walg}$:
	\begin{equation}\label{rep-entier-sum}
	\bar{W}_{p}= \sum_{i=0}^{n}{\wordterm{c_{i}}{\L}{x}{y}{\TT p_{i}} \sflow {\wordterm{c_{i+1}}{\R}{x}{y}{\TT p_{i+1}}}}
	\end{equation}

	We will write $\setofrep{W}$ the set of representations of a given word $W$.
	%\CLEM{Ou pas plutôt $\setofrep{\bar{W}}$?}\THOMAS{C'est l'ensemble des représentations d'un mot, donc $W$ et non $\bar{W}$.}
\end{definition}

To understand better this representation, consider that each symbol in the alphabet $\Sigma$ comes in 
two \enquote{flavors}, \emph{left} and \emph{right}. %— or \emph{ingoing} and \emph{outgoing}.
Then, one can easily construct the \enquote{context} 
\(\bar{W}=\sum_{i=0}^{n}{\wordterm{\TT c_{i}}{\L}{x}{y}{[~]_{i}} \sflow {\wordterm{\TT c_{i+1}}{\R}{x}{y}{[~]_{i+1}}}}\)
from the list as the sums of the arrows in the following picture (where $x$ and $y$ are omitted): 
\begin{center}
\begin{tikzpicture}[x=1.2cm,y=1.2cm,inner sep=2pt, outer sep=1pt]
	\node[shape=circle,draw] (S) at (0,0) {$\star$};
		\node (SE) at (S.east) {};
		\node (SW) at (S.west) {};
		\node (SN) at (S.north) {};
		\node (So) at (SE.east) {$\bullet$};
		\node (SoL) at (So.north) {\scriptsize{$\R$}};
		\node (Si) at (SW.west) {$\bullet$};
		\node (SiL) at (Si.north) {\scriptsize{$\L$}};
		\node (Sv) at ($(SN.north)+(0,0.05)$) {\scriptsize{$\TT M([~]_{0})$}};
	\node[shape=circle,draw] (A) at (2,0) {$\TT c_{1}$};
		\node (AE) at (A.east) {};
		\node (AW) at (A.west) {};
		\node (AN) at (A.north) {};
		\node (Ao) at (AE.east) {$\bullet$};
		\node (AoL) at (Ao.north) {\scriptsize{$\R$}};
		\node (Ai) at (AW.west) {$\bullet$};
		\node (AiL) at (Ai.north) {\scriptsize{$\L$}};
		\node (Av) at ($(AN.north)+(0,0.05)$) {\scriptsize{$(\TT M[~]_{1})$}};
	\node[shape=circle,draw] (B) at (4,0) {$\TT c_{2}$};
		\node (BE) at (B.east) {};
		\node (BW) at (B.west) {};
		\node (BN) at (B.north) {};
		\node (Bo) at (BE.east) {$\bullet$};
		\node (BoL) at (Bo.north) {\scriptsize{$\R$}};
		\node (Bi) at (BW.west) {$\bullet$};
		\node (BiL) at (Bi.north) {\scriptsize{$\L$}};
		\node (Bv) at ($(BN.north)+(0,0.05)$) {\scriptsize{$\TT M([~]_{2})$}};
	\node[shape=circle] (C) at (6,0) {$\dots$};
		\node (CE) at (C.east) {};
		\node (CW) at (C.west) {};
		\node (Co) at (CE.east) {};
		\node (Ci) at (CW.west) {};
	\node[shape=circle,draw] (D) at (8,0) {$\TT c_{n}$};
		\node (DE) at (D.east) {};
		\node (DW) at (D.west) {};
		\node (DN) at (D.north) {};
		\node (Do) at (DE.east) {$\bullet$};
		\node (DoL) at (Do.north) {\scriptsize{$\R$}};
		\node (Di) at (DW.west) {$\bullet$};
		\node (DiL) at (Di.north) {\scriptsize{$\L$}};
		\node (Dv) at ($(DN.north)+(0,0.05)$) {\scriptsize{$\TT M([~]_{n})$}};
	% Edges S <-> A
	\draw[-left to] ($(So.east)+(0,0.05)$) to ($(Ai.west)+(0,0.05)$) {};
	\draw[-left to] ($(Ai.west)+(0,-0.05)$) to ($(So.east)+(0,-0.05)$) {};
	% Edges A <-> B
	\draw[-left to] ($(Ao.east)+(0,0.05)$) to ($(Bi.west)+(0,0.05)$) {};
	\draw[-left to] ($(Bi.west)+(0,-0.05)$) to ($(Ao.east)+(0,-0.05)$) {};
	% Edges B <-> C
	\draw[-left to] ($(Bo.east)+(0,0.05)$) to ($(Ci.west)+(0,0.05)$) {};
	\draw[-left to] ($(Ci.west)+(0,-0.05)$) to ($(Bo.east)+(0,-0.05)$) {};
	% Edges C <-> D
	\draw[-left to] ($(Co.east)+(0,0.05)$) to ($(Di.west)+(0,0.05)$) {};
	\draw[-left to] ($(Di.west)+(0,-0.05)$) to ($(Co.east)+(0,-0.05)$) {};
	% Edges D <-> S
%	\draw[-left to] ($(Do.south)+(0.08,0)$)  .. controls (8,-1.05) and (0,-1.05) .. ($(Si.south)+(-0.08,0)$) {};
%	\draw[-left to] ($(Si.south)+(0.08,0)$)  .. controls (0,-0.95) and (8,-0.95) .. ($(Do.south)+(-0.08,0)$) {};
	\draw[-left to, rounded corners] ($(Do.south)+(0.05,0)$)  -- ($(Do.south)+(0.05,-0.3)$) -- ($(Si.south)+(-0.05,-0.3)$) -- ($(Si.south)+(-0.05,0)$);
	\draw[-left to, rounded corners] ($(Si.south)+(0.05,0)$)  -- ($(Si.south)+(0.05,-0.2)$) -- ($(Do.south)+(-0.05,-0.2)$) -- ($(Do.south)+(-0.05,0)$);
\end{tikzpicture}
\end{center}
Then, choosing a set $p=\extlist{\TT p_{0}}{\TT p_{n}}$ of position constants, intuitively representing physical memory addresses,
the representation $\bar{W}_{p}$ of a word associated with $p$ is obtained by filling, for all $i=\extlist{0}{n}$, the hole $[~]_{i}$ by the constant $\TT p_{i}$.

\smallskip
This abstract representation of words is not an arbitrary choice.
It comes from the interpretation of lists in geometry of interaction.

Indeed, in \systF, the type of binary lists corresponds to the formula 
$\forall X~(X\Rightarrow X)\Rightarrow (X\Rightarrow X)\Rightarrow (X\Rightarrow X)$.
Any lambda-term in normal form of this type can be written as
$\lambda f_{0}f_{1}x.\,f_{\TT c_{1}}f_{\TT c_{2}}\cdots f_{\TT c_{k}}x$,
where $\TT c_{1}\cdots c_k$ is a word on $\{0,1\}$.
The \GoI representation of such a lambda-term yields the abstract representation just defined\footnote{A thorough explanation can be found in previous work by Aubert and Seiller~\cite{Aubert2012}.}.
Notice that the additional symbol $\star$ used to represent words corresponds to the variable $x$ in the preceding lambda-term.
Note also the fact that the representation of integer is \emph{cyclic}, and that the symbol $\star$ serves as a reference for the starting/ending point of the word.

Let us finally stress that the words are represented as \emph{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 \autoref{word-rep} 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 \enquote{one-way representations of words}, defined by replacing the symbol $\sflow$ by the symbol $\flow$ in \eqref{rep-entier-sum} of \autoref{word-rep}, could be used to characterize one-way multi-heads automata.

%\THOMAS{représentation des mots = wiring déterministe}
%\CLEM{Au début de ces deux déf. (ou alors ailleurs, une fois pour toutes ?), il faut préciser qu'aucune des variables $c_1 \hdots c_n$ n'est $\star$.} \MARC{voire même un petit passage sur les mots cycliques.}
%\THOMAS{Est-ce qu'il faut faire comme ça (dire que les $c_{i}$ sont différents de $\star$) ou bien est-ce qu'on dit simplement dans un deuxième temps que les listes binaires sont représentées avec un $\star$ au début. Si c'est la première option, je serais plutôt d'avis d'exclure $\Sigma$ de l'alphabet car ce n'est pas un symbole comme les autres.}
%\CLEM{Pas d’avis,  il faut juste se mettre d’accord. Pour le moment, définir de but en blanc \autoref{abstract-rep-of-word} qu’un mot c’est $\start c_1 \hdots c_n$, ça me fait un peu bizarre.}

simple_example.tex
We give in \autoref{fig-state-diagram} the (labeled) state diagram of a deterministic automata\footnote{That is, with one head.} that ends on input $W \in \{0, 1\}^*$ if and only if $\exists n \in \natural$ such that $W = \start 0^n$.
Elsewhere, it loops by repeating the computation for ever.
We assume, for the sake of simplicity, that the head starts on the first bit next to $\start$, that the input is cyclic and that $\start$ occurs only once in $W$.
\CLEM{À clarifier dans la façon dont on définit un mot, et dont on le représente.}

\begin{figure}
\begin{minipage}[b]{0.45\textwidth}
\centering%
\begin{tikzpicture}[auto]%[shorten >=1pt,node distance=2cm,on grid,auto] 
   \node[state] (i)   {$\state{i}$}; 
   \node[state, accepting] (y) [below left=of i] {$\state{y}$}; 
   \node[state] (n) [below right=of i] {$\state{n}$}; 
    \path[->] 
    (i)		edge	[loop above]	node	{$0$}	node[pos=0.9,right]{\small{$t_1$}}		()
          	edge  	[bend right] 	node	{$1$} 	node[pos=0.9,left]{\small{$t_2$}}		(n)
           	edge  					node	{$\start$} node[pos=0.9,right]{\small{$t_6$}}	(y)
    (n)		edge	[loop below]	node	{$0$} 		node[pos=0.9,left]{\small{$t_3$}}	()
    		edge	[loop right]	node	{$1$} 		node[pos=0.9,below]{\small{$t_4$}}	()
           	edge  	[bend right]	node [swap]	{$\start$} node[pos=0.9,right]{\small{$t_5$}} (i);
\end{tikzpicture}%
\caption{A labeled state diagram for an automata that accepts $\start 0^n$}\label{fig-state-diagram}
\end{minipage}
\hspace{0.1\textwidth}
\begin{minipage}[b]{0.45\textwidth}
\centering%
\begin{align*}%
\wordterm{0}{\R}{\state{i}}{v}{z} & \rflow \wordterm{0}{\L}{\state{i}}{v}{z'} \tag{\small{$t_1$}} \label{set1}\\
\wordterm{1}{\R}{\state{i}}{v}{z} & \rflow \wordterm{1}{\L}{\state{n}}{v}{z'} \tag{\small{$t_2$}} \label{set2}\\
\wordterm{0}{\R}{\state{n}}{v}{z} & \rflow \wordterm{0}{\L}{\state{n}}{v}{z'} \tag{\small{$t_3$}} \label{set3}\\
\wordterm{1}{\R}{\state{n}}{v}{z} & \rflow \wordterm{1}{\L}{\state{n}}{v}{z'} \tag{\small{$t_4$}} \label{set4}\\
\wordterm{\start}{\R}{\state{n}}{v}{z} & \rflow \wordterm{\start}{\L}{\state{i}}{v}{z'} \tag{\small{$t_5$}} \label{set5}\\
\wordterm{\start}{\R}{\state{i}}{v}{z} & \rflow \wordterm{\start}{\L}{\state{y}}{v}{z'} \tag{\small{$t_6$}} \label{set6}
\end{align*}%
\caption{The corresponding encoding as flows}\label{fig-flow}
\end{minipage}
\end{figure}

We will now encode it as an observation.
Remember from \autoref{word-rep} that the string $W = \start \TT{c_1} \hdots \TT{c_n}$ over $\{\start, 0, 1\}$ with $\start$ occurring only once is represented, once the constant representing the positions $\extlist{\TT p_0}{\TT p_n}$ has been fixed, as 
\[
\begin{array}{llrcl}
	W :=	& & \wordterm{\start}{\L}{x}{y}{\TT{p_0}} & \sflow &  \wordterm{c_1}{\R}{x}{y}{\TT{p_1}} \\
			&+& \wordterm{c_1}{\L}{x}{y}{\TT{p_1}} & \sflow & \wordterm{c_2}{\R}{x}{y}{\TT{p_2}} \\
			& & & \vdots  \\
			&+& \wordterm{c_n}{\L}{x}{y}{\TT{p_n}} & \sflow & \wordterm{\start}{\R}{x}{y}{\TT{p_0}}
	\end{array}
\]

We denote by $a \rflow b$ the flow $b \flow a$: in the case of a transition system as the one we are going to expose, it helps to read it as a functional relation (here, a function) encoding a classical transition function. 

The observation will simply be the sum of the flows \eqref{set1}--\eqref{set6} given in \autoref{fig-flow}.
The variable $v$ stands for \enquote{void}: it will be of no use in this case, where only one head is used.

The fact that no flow has for state $\state{y}$ on its left-hand reflect the fact that this state is terminal: once this state is reached, no transition can take place.
In fact, one could even replace \eqref{set6} with
\begin{align*}%
\wordterm{\start}{\R}{\state{i}}{v}{z} & \rflow 0 \tag{\small{$t'_6$}} \label{set6bis}
\end{align*}%
Here, a loop is in fact a \enquote{perform for ever the same computation}.
There is a reason for this design: as the observation is a sum, any transition that can be applied will be applied, i.e. if the left-member of a flow of our observation and a part of the input can be unified, the computation will start in a possibly \enquote{wrong} initialization.
That some of this incorrect runs accept for incorrect reason is no trouble, since only rejection is meaningful in our framework.
Hence, the state $\state{n}$ acts as a buffer, where the head scans the input looking for the $\start$, and when it found it, it start the computation in the correct position, and in the correct state (that is, $\state{i}$).
Several runs occur in parallel, but we know that if the letter $1$ is ever found, all paths end.
On the contrary, if the letter $1$ is found, at least one path performs the computation forever.

Hence, this observation is nilpotent if and only if when applied to a representation of $W$, $W$ contains only $\start$ and $0$'s.

\CLEM{Faire un petit exemple d’entrée et de jeu programme / entrée ?}
soundness.tex
We now use the results of \autoref{sec_compgraph} and \autoref{sec_observations} to design a procedure that decides whether a word belongs to the language of an observation within logarithmic space.
This procedure will use the classical reduction from a problem to testing the acyclicity of a graph, a problem 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 \autoref{det-graph}), the procedure will be deterministic or non-deterministic.

Finally, using classical composition of logspace algorithms%
\footnote{The reader unused to the mechanism of composition of logspace-algorithms may have a look at a classical textbook \cite[Fig. 8.10]{Savage1998}.}, \autoref{nilp-iff-acycl} and \autoref{lang-reloaded}, we will obtain the result expected, that is:

\begin{theorem}%
\label{nilp-in-l}
If $O$ is an observation, then $\lang O\in \conlogspace$. If moreover $O$ is deterministic, then $\lang O\in\logspace$.
\end{theorem}

\subsubsection{A Foreword on Word and Size}
Given a word $W$ over $\Sigma$, to build a representation $\bar{W}_p$ as in \autoref{word-rep} is clearly in $\logspace$: it is a plain matter of encoding.
By \autoref{equiv-of-rep}, it is sufficient to consider a single representation.
So for the rest of this procedure, we consider given $\bar{W}_{p} \in \setofrep{W}$ and write $\wiring{F}:= \obs{O}\bar{W}_{p}$.
The size of $\Sigma$ is a constant, and it is clear that the maximal arity and the height of the balanced wiring $\wiring{F}$ remain fixed when $W$ varies.
The only point that fluctuates is the cardinality of the set of symbols that occurs in $\wiring{F}$, and it is linearly growing with the length of $W$, corresponding to the number of positions constant.
In the following, any mention to a logarithmic amount of space is to be completed by \enquote{relatively to the length of $W$}.

\subsubsection{Building the Computation Graph}
We need two main ingredients to build the computation graph (\autoref{compgraph}) of $\wiring{F}$: to enumerate the computation space $\comp{\wiring{F}}$ (recall \autoref{def-comp}), and to determine whether there is an edge between two vertices.

By \autoref{card-comp}, $\card{\comp{\wiring{F}}}$ is polynomial in the size of $W$.
Hence, given a balanced wiring $\wiring{F}$, a logarithmic amount of memory is enough to enumerate the members of $\comp{\wiring{F}}$, that is the vertices of $\G(\wiring{F})$.

Now the second part of the construction of $\G(\wiring{F})$ is to determine if there is an edge between two vertices.
Remember that there is an edge from $\BF u = \fact{u}$ to $\BF v = \fact{v}$ in $\G (\wiring{F})$ if $\BF v \in \wiring{F} \BF u$.
So one has to scan the members of $\wiring{F}=\obs{O}\bar{W}_{p}$: if there exists $(t_1 \flow t_2)(t'_1 \flow t'_2) \in \wiring{F}$ such that $(t_1 \flow t_2)(t'_1 \flow t'_2) (\fact{u}) = \fact{v}$, then there is an edge from $\BF u$ to $\BF v$.
To list the members of $\wiring{F}$ is in $\logspace$, but unification in general is a difficult problem (see \autoref{ssec_unif}).
The special case of matching can be tested with a logarithmic amount of space:

\begin{theorem}[Matching is in {\sc \logspace} \protect{\cite[p.~49]{Dwork1984}}]
\label{thm-unif-logspace}
	Given two terms $t$ and $u$ such that either $t$ or $u$ is closed, deciding if they are matchable is in \logspace.
\end{theorem}

Actually, this result relies on a subtle manipulation of the representation of the terms as \emph{simple directed acyclic graphs}\footnote{The reader willing to learn more about this may have a look at a classical chapter~\cite{Baader2001}.}, where the variables are \enquote{shared}.
Translations between this representation of terms and the usual one can be performed in logarithmic space \cite[p.~38]{Dwork1984}.


\subsubsection{Deciding if $\G(\wiring{F})$ is Acyclic}
We know thanks to \autoref{nilp-iff-acycl} that answering this question is equivalent to deciding if $\wiring{F}$ is nilpotent.
We may notice that $\G(\wiring{F})$ is a directed, potentially unconnected graph of size $\card{\comp{\wiring{F}}}$.

It is well-know that testing for acyclicity of a directed
% (resp. undirected)
graph is a \conlogspace \cite[p.~83]{Jones1975} problem.
% (resp. \logspace \cite[Theorem 3.1.(a)]{Cook1980a})
Moreover, if $\wiring{F}$ is deterministic (which is the case when $O$ is), then $\G(\wiring{F})$ has out-degree bounded by $1$ (\autoref{det-graph}) and one can test its acyclicity without being non-deterministic: it is enough to list the vertices of $\comp{\wiring{F}}$, and for each of them to follow $\card{\comp{\wiring{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.

tensor.tex
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.

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

\begin{definition}[tensor product]\label{ptensor}
	Let $\,u\flow v\,$ and $\,t\flow w\,$ be two flows.
	Suppose we have chosen representatives of their renaming classes that have disjoint sets of variables. We define their \emph{tensor product} as
	$(u\flow v) \ptensor (t\flow w):=\: u\p t \flow v\p w$.
	The operation is extended to wirings by $(\sum_i f_i)\ptensor(\sum_j g_j):= \sum_{i,j} f_i\ptensor g_j$.
%	
%	\smallskip
	Given two semirings $\C A,\C B$, we define %their tensor product as
%	\[\C A\ptensor \C B:= \,\set{\sum_i F_i\ptensor G_i}{F_i\in\C A\,,\,G_i\in \C B}\]
%
%	\smallskip
	%\centerline{
	$\C A\ptensor \C B:= \,\set{\sum_i F_i\ptensor G_i}{F_i\in\C A\,,\,G_i\in \C B}$.
	%}
\end{definition}

The tensor product of two semirings is easily shown to be a semiring.

\example{~

$(\TT f(x)\p y\flow y\p x)\ptensor(x\flow \TT g(x))= (\TT f(x)\p y)\p z\flow (y\p x)\p \TT g(z) $}

\begin{notation}
	As the symbol $\p$, the $\ptensor$ operation is not associative. We carry on the convention for $\p$ and write it as \emph{right associating}: $\C A\ptensor\C B\ptensor\C C:=\C A\ptensor(\C B\ptensor\C C)$.
\end{notation}

Semirings can also naturally be associated to any set of closed terms or to the restriction to a certain set of symbols.

\begin{definition}
	Given a set of closed terms $E$, we define the following semiring $\calg E:=\set{\sum_i t_i\flow u_i}{t_i,u_i \in E}$.
	%
	If $\TT S$ is a set of symbols and $\C A$ a semiring, we write $\ralg{\TT S}{\C A}$ the semiring of wirings of $\C A$ , that do not use the symbols in $\TT S$.
\end{definition}

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 $\calg E$.

\smallskip
Finally, the unit $I=x\flow x$ of $\ualg$ yields a semiring.

\begin{definition}[unit semiring]
	We call \emph{unit semiring} the semiring $\unitalg:=\{\,\unit\,\}$.
\end{definition}

thm.tex
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% MACROS without numerotation

%\newcommand{\notations}[1]{\noindent\textbf{Notations.} {\it#1}}
%\newcommand{\notation}[1]{\noindent\textbf{Notation.} {\it#1}}
%\renewcommand{\remark}[1]{\noindent\textbf{Remark.} {\it #1}}
%\renewcommand{\example}[1]{\noindent\textbf{Example.} {\it#1}}
%\newcommand{\examples}[1]{\noindent\textbf{Examples.} {\it #1}}

% Environnement supplémentaire pour les notations
\spnewtheorem*{notation}{Notation}{\itshape}{\rmfamily}
\spnewtheorem*{notations}{Notations}{\itshape}{\rmfamily}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% STYLES

% \newtheoremstyle{general}% name of the style to be used
%  {12pt}% measure of space to leave above the theorem. E.g.: 3pt
%  {12pt}% measure of space to leave below the theorem. E.g.: 3pt
%  {\normalfont}% name of font to use in the body of the theorem
%  {0pt}% measure of space to indent
%  {\bf}% name of head font
%  {}% punctuation between head and body
%  { }% space after theorem head; " " = normal interword space
%  {}% Manually specify head

%\newtheorem{definition}[theorem]{Definition}
%\newtheorem{lemma}[theorem]{Lemma}
%\newtheorem{proposition}[theorem]{Proposition}
%\newtheorem{corollary}[theorem]{Corollary}

\newcommand{\safespace}[1]		% les sauts de ligne semblent éviter le craquage au niveau espace vertical...
{
	
	\vspace{#1}
	
}

\newcommand{\negenvspace}{-0.8mm}		%paramètre global pour tous les env de theorem

%\AtBeginEnvironment{notation}{\safespace\negenvspace}
%
%\AtEndEnvironment{notation}{\safespace\negenvspace}
%
%\AtBeginEnvironment{definition}{\safespace\negenvspace}
%\AtEndEnvironment{definition}{\safespace\negenvspace}
%
%\AtBeginEnvironment{lemma}{\safespace\negenvspace}
%\AtEndEnvironment{lemma}{\safespace\negenvspace}
%
%\AtBeginEnvironment{theorem}{\safespace\negenvspace}
%\AtEndEnvironment{theorem}{\safespace\negenvspace}
%
%\AtBeginEnvironment{proposition}{\safespace\negenvspace}
%\AtEndEnvironment{proposition}{\safespace\negenvspace}
%
%\AtBeginEnvironment{corollary}{\safespace\negenvspace}
%\AtEndEnvironment{corollary}{\safespace\negenvspace}
%
%\AtBeginEnvironment{example}{\safespace\negenvspace}
%\AtEndEnvironment{example}{\safespace\negenvspace}
%
%\AtBeginEnvironment{remark}{\safespace\negenvspace}
%\AtEndEnvironment{remark}{\safespace\negenvspace}
%
%\AtBeginEnvironment{notation}{\safespace\negenvspace}
%\AtEndEnvironment{notation}{\safespace\negenvspace}
%
%\AtBeginEnvironment{proof}{\safespace\negenvspace}
%\AtEndEnvironment{proof}{\safespace\negenvspace}

ualgebra.tex
This section presents the technical setting of this work, the \emph{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.

	\subsection{Flows and Wirings}\label{sec_flows}

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 difference between predicate symbols and function symbols, for it makes the presentation easier.
%Given a unary atomic predicate $A(x)$, a flow $f=t\flow u$ induces the Horn clause $A(f):=A(t)\leftarrow A(u)$.

\begin{definition}[flows]\label{def_flow}
	A \emph{flow} is a pair of terms $t\flow u$
	with $\var(t)\subseteq\var(u)$.
	Flows are considered up to renaming: for any renaming $\alpha$,
	$t \flow u\,=\,t\alpha \flow u\alpha$.
\end{definition}

Facts, that are usually defined as ground (using only closed terms) clauses with an empty body, can still be represented as a special kind of flows.

\begin{definition}[facts]\label{def_fact}
	A \emph{fact} is a flow of the form $\fact t$.
\end{definition}

\remark{Note that this implies that $t$ is closed.}% Again, if $f$ is a fact, then $\TT C(f)$ is a fact in the sense of logic programming.}

\medskip

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

\begin{definition}[product of flows]
	Let $u\flow v$ and $t\flow w$ be two flows.
	Suppose we have representatives of the renaming classes
	such that $\var(v)\cap\var(w)=\varnothing$.
	The \emph{product} of $u\flow v$ and $t\flow w$ is defined
	if $v,t$ are unifiable with MGU $\theta$
	%(the specific choice of a MGU does not matter)
	as
%\smallskip
%	\centerline{
	$(u\flow v)(t\flow w)\,:=\:u\theta \flow w\theta$.
	%}
\end{definition}

\remark{The condition on variables ensures that facts form a \enquote{left ideal} of the set of flows:
if $\BF u$ is a fact and $f$ a flow, then $f\BF u$ is a fact when it is defined.
}

\example{~
\label{example_flows}

$(\TT f(x) \flow x)(\TT f(x)\flow \TT g(x)) = \TT f(\TT f(x)) \flow \TT g(x)$

$(x \p \TT c \flow (y\p y) \p x)(( \TT c \p \TT c) \p x \flow y\p x) = x \p \TT c \flow  \TT c \p \TT x$

$(\TT f(x\p c) \flow x\p\TT d)(\fact{\TT d\p\TT d}) =\fact{\TT f(\TT d\p\TT c)}$
}

\medskip
The product of flows corresponds to the resolution rule in the following sense: given two flows $f=u\flow v$ and $g=t\flow w$ and a $MGU$ $\theta$ of $v$ and $t$, then the resolution rule applied to $f$ and $g$ would yield $fg$.

\smallskip
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.


\begin{definition}[wirings]\label{def_wirings}
	\emph{Wirings} are finite sets of flows.
	The product of wirings is defined as
	$FG:=\set{fg}{f \in F, \, g \in G, \: fg \text{ defined}}$.
	
	We write $\ualg$ the set of wirings and refer to it as the \emph{unification semiring}.
\end{definition}

%If $F$ is a wiring, the set $A(F)=\{ A(f)~|~f\in F\}$ can be seen as a logic program.

\medskip
The set of wirings $\ualg$ has a structure of semiring. We use an \emph{additive notation} for sets of flows to stress this point:
\begin{itemize}
	\item The symbol $+$ will be used in place of $\cup$.
	\item We write sets as the sum of their elements: $\extset{f_1}{f_n}:= f_1 + \cdots + f_n$.
	\item We write $0$ for the empty set.
	\item The unit is $\unit := x \flow x$.
\end{itemize}

We will call \emph{semiring} any subset $\C A$ of $\ualg$ such that
\begin{itemize}
	\item $0\in\C A$,
	\item if $\extlist{F_1}{F_n} \in \C A$, then $F_1 + \, \cdots \,+ F_n \in \C A$,
	\item if $F \in \C A$ and $G\in\C A$ then $FG \in \C A$.
\end{itemize}

\begin{definition}[nilpotency]\label{def_nilp}
	A wiring $\wiring{F}$ is \emph{nilpotent} if $\wiring{F}^n=0$ for some $n \in \natural$.
	We may use the notation $\isnilp F$ to express the fact that $F$ is nilpotent.
\end{definition}

As mentionned in \autoref{ssec_goilp}, nilpotency is related with the notion of \emph{boundedness}~\cite{Dantsin2001} of a logic program.
Indeed, if we have a wiring $F$ and a finite set of facts $\BF U$, let us consider the set of facts that can be obtained through $F$ $\set{\BF u}{\BF u\in F^n\BF U \text{ for some }n}$ which can also be written as
%
%\smallskip
%\centerline{
$(\unit+F+F^2+\cdots)\BF U$ or $EX(F)\BF U$ (where EX(.) is the execution operator of \autoref{ssec_goilp}).
%}

%\smallskip
If $F$ is nilpotent, one needs to compute the sum only up to a finite rank that does not depend on $\BF U$, which implies the  boundedness property.

%\remark{If $F$ is nilpotent wiring, then the execution formula of $GoI$ provides an algebraic variant of the fixed point semantics of \LP (for a quick recall see \cite{Dantsin2001}): let $U_{F}$ be the \emph{Herbrand universe} of $F$, i.e. the set of all facts made of terms in the language of $F$ plus the constant $\star$ ; if by a \emph{Herbrand interpretation}%
%\footnote{Usually, a Herbrand interpretation is rather a set of formulae of the form $A(\extlist{t_{1}}{t_{n}})$ with $\extlist{t_{1}}{t_{n}}$ in the Herbrand universe; indeed, everything can be reformulated by using a unary predicate $A(x)$ and considering $\TT C(f)$ rather than $F$.
%}
% we mean a wiring contained in $U_{F}$, then $F$ itself acts, by left multiplication, as a monotone operator over Herbrand interpretations (monotonicity is an immediate consequence of distributivity).
% Since $F$ is nilpotent (of order $n$), the operator $EX(F)=\sum_{k=0}^{n-1}F^{k}$ computes the least fixed point of $F$.}

%let's recall that the \emph{Herbrand universe} $U_{P}$ of a program $P$ is the set of ground terms in the language of $P$ (possibly augmented with an auxiliary constant) and the \emph{Herbrand base} $B_{P}$ is the set of ground atoms in the language of $P$.
% A \enquote{Herbrand interpretation} is a subset of the Herbrand base, intuitively corresponding to the set of formulas which receive the value $\TT{true}$ under the interpretation; a program induces then a monotone operator over Herbrand interpretation whose least fixed point (which is provided by the Knaster-Tarski Theorem) properly interprets the program. 


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

\begin{definition}[deterministic wirings]\label{def_fun}
	A wiring $F$ is \emph{deterministic} if given any fact $\BF u$, $\card{F\BF u}\leq 1$.
	We will write $\dalg$ the set of deterministic wirings.
\end{definition}

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

\begin{lemma}\label{lem_det}
	Let $F=\sum_i u_i\flow t_i$. If the $t_i$ are pairwise disjoint (\autoref{disjoint}), then $F$ is deterministic.
\end{lemma}

\begin{proof}
	Given a closed term $t$ there is at most one of the $t_i$ that matches $t$, therefore $F(\fact t)$ is either a single fact or $0$.\qed
\end{proof}

unification.tex
Unification is a classical subject of research, at the intersection of practical and theoretical considerations.
We recall in the following some notations and some of the numerous links between complexity and unification, and by extension logic programming.

%\safespace{-1mm}

\begin{notations}
	\label{def_terms}
		We consider a set of first-order terms $\terms$, 
		assuming an infinite number of variables $x, y,z,\:\ldots\in\vars$, 
		a binary function symbol $\p$ (written in \emph{infix notation}),
		infinitely many constant symbols $\TT a,\TT b,\TT c, \ldots$
		including the (multipurpose) dummy symbol $\factsym$ and, for any $n \in \naturalp$, at least one $n$-ary function symbol $\nary n$.
	
	Note that the binary function symbol $\p$ is not associative. However, we will write it
by convention as \emph{right associating} to lighten notations: $t\p u\p v := t \p(u\p v)$.
	
		For any $t \in \terms$, we write $\var(t)$ the set of variables occurring in $t$
		(a term is \emph{closed} when $\var(t)=\varnothing$)
		and $\h(t)$ the \emph{heigth} of $t$: the maximal distance from the root to any other subterm in the tree structure of $t$.
		
		The \emph{height of a variable occurrence} in a term $t$ is its distance from the root in the tree structure of the term.\label{def-height}
	\label{renaming}
		A \emph{substitution} $\mgu{\theta}$ is a mapping form variables to terms such that $x \mgu{\theta} = x$ for all but finitely many $x \in \vars$.
		A \emph{renaming} is a substitution $\mgu{\alpha}$ mapping variables to variables and that is bijective.
		A term $t'$ is a \emph{renaming} of $t$ if $t'=t \mgu{\alpha}$ for some renaming $\mgu{\alpha}$.
\end{notations}

%\safespace{-1mm}

\begin{definition}[unification, matching and disjointness]\label{disjoint}
	Two terms $t, u$ are 
	\begin{itemize}
	\item \emph{unifiable} if there exists a substitution%
	\footnote{Called a \emph{unifier}. Remember that two terms $t,u$ that are unifiable have a \emph{most general unifier} (MGU): a unifier $\theta$ such that any other unifier of $t,u$ is an instance of $\theta$.}
	$\mgu{\theta}$ such that $t \mgu{\theta} = u \mgu{\theta}$,
	\item \emph{matchable} if $t',u'$ are unifiable,  where $t',u'$ are renamings of $t,u$ such that $\var(t') \cap \var(u') = \varnothing$,
	\item \emph{disjoint} if they are not matchable.
	\end{itemize}
\end{definition}

%\safespace{-1mm}

It is well-known that the problem of deciding whether two terms are unifiable is $\ptime$-complete \cite[Theorem 1]{Dwork1984}, 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 \cite[Theorems 4.2.1 and 4.3.1]{Ohkubo1987}, if both terms are linear or if they do not share variables \cite{Dwork1984,Dwork1988}.
More recently \cite{Bellia2003}, 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 \emph{matching problem} is in \logspace~\cite{Dwork1984} (recalled as \autoref{thm-unif-logspace}) will be used in \autoref{sec_soundness}.

%The reader willing to learn more about Logic Programming and complexity may find useful a recent survey \cite{Dantsin2001} dealing with such issues.

%%%% à mettre dans une autre section

%A point we would like to focus on is \emph{boundedness of datalog program} \cite[p.~392]{Dantsin2001}: a datalog program is bounded if the number of iteration steps needed to reach the least fixed point is independent of the input.
%This problem was shown \cite{Hillebrand1995} to be --~even with drastic constrains~-- undecidable.
%That puts in light the novelty and power of the constrain we are going to introduce in \autoref{def-balanced}, that allow to enforce a bound on the space needed to simulate the logic program, and hence a bound on its run-time.
%However, this bound is relative to the size of the input.

aplas14.bbl
\begin{thebibliography}{10}
\providecommand{\url}[1]{\texttt{#1}}
\providecommand{\urlprefix}{URL }

\bibitem{Asperti1994}
Asperti, A., Danos, V., Laneve, C., Regnier, L.: Paths in the lambda-calculus.
  In: LICS. pp. 426--436. IEEE Computer Society (1994)

\bibitem{Aubert2014}
Aubert, C., Bagnol, M.: Unification and logarithmic space. In: Dowek, G. (ed.)
  RTA-TLCA 2014. LNCS, vol. 8650, pp. 77--–92. Springer (2014)

\bibitem{Aubert2012}
Aubert, C., Seiller, T.: Characterizing co-nl by a group action. Arxiv preprint
   abs/1209.3422 (2012)

\bibitem{Baader2001}
Baader, F., Snyder, W.: Unification theory. In: Robinson, J.A., Voronkov, A.
  (eds.) Handbook of Automated Reasoning, pp. 445--532. Elsevier and MIT Press
  (2001)

\bibitem{Baillot2010}
Baillot, P., Mazza, D.: Linear logic by levels and bounded time complexity.
  Theoret. Comput. Sci.  411(2),  470--503 (2010)

\bibitem{Baillot2001}
Baillot, P., Pedicini, M.: Elementary complexity and geometry of interaction.
  Fund. Inform.  45(1--2),  1--31 (2001)

\bibitem{Bellia2003}
Bellia, M., Occhiuto, M.E.: N-axioms parallel unification. Fund. Inform.
  55(2),  115--128 (2003)

\bibitem{Calimeri2008}
Calimeri, F., Cozza, S., Ianni, G., Leone, N.: Computable functions in {ASP}:
  Theory and implementation. In: Garcia de~la Banda, M., Pontelli, E. (eds.)
  ICLP. LNCS, vol. 5366, pp. 407--424. Springer (2008)

\bibitem{Lago2010}
Dal~Lago, U., Hofmann, M.: Bounded linear logic, revisited. Log. Meth. Comput.
  Sci.  6(4) (2010)

\bibitem{Dantsin2001}
Dantsin, E., Eiter, T., Gottlob, G., Voronkov, A.: Complexity and expressive
  power of logic programming. ACM Comput. Surv.  33(3),  374--425 (2001)

\bibitem{Dwork1984}
Dwork, C., Kanellakis, P.C., Mitchell, J.C.: On the sequential nature of
  unification. J. Log. Program.  1(1),  35--50 (1984)

\bibitem{Dwork1988}
Dwork, C., Kanellakis, P.C., Stockmeyer, L.J.: Parallel algorithms for term
  matching. SIAM J. Comput.  17(4),  711--731 (1988)

\bibitem{Gaboardi2012}
Gaboardi, M., Marion, J.Y., Ronchi Della~Rocca, S.: An implicit
  characterization of pspace. ACM Trans. Comput. Log.  13(2),  18:1--18:36
  (2012)

\bibitem{Girard1987}
Girard, J.Y.: Linear logic. Theoret. Comput. Sci.  50(1),  1--101 (1987)

\bibitem{Girard1989a}
Girard, J.Y.: Geometry of interaction 1: Interpretation of system {F}. Studies
  in Logic and the Foundations of Mathematics  127,  221--260 (1989)

\bibitem{Girard1989b}
Girard, J.Y.: Towards a geometry of interaction. In: Gray, J.W.,
  {\v{S}}{\v{c}}edrov, A. (eds.) Proceedings of the AMS-IMS-SIAM Joint Summer
  Research Conference held June 14-20, 1987. Categories in Computer Science and
  Logic, vol.~92, pp. 69--108. AMS (1989)

\bibitem{Girard1995a}
Girard, J.Y.: Geometry of interaction {III}: accommodating the additives. In:
  Girard, J.Y., Lafont, Y., Regnier, L. (eds.) Advances in Linear Logic, pp.
  329--389. No. 222 in London Math. Soc. Lecture Note Ser., CUP (Jun 1995)

\bibitem{Girard1995}
Girard, J.Y.: Light linear logic. In: Leivant, D. (ed.) LCC, LNCS, vol. 960,
  pp. 145--176. Springer (1995)

\bibitem{Girard2012}
Girard, J.Y.: Normativity in logic. In: Dybjer, P., Lindström, S., Palmgren,
  E., Sundholm, G. (eds.) Epistemology versus Ontology, Logic, Epistemology,
  and the Unity of Science, vol.~27, pp. 243--263. Springer (2012)

\bibitem{Girard2013}
Girard, J.Y.: Three lightings of logic. In: Ronchi Della~Rocca, S. (ed.) CSL.
  LIPIcs, vol.~23, pp. 11--23. Schloss Dagstuhl - Leibniz-Zentrum für
  Informatik (2013)

\bibitem{Hillebrand1995}
Hillebrand, G.G., Kanellakis, P.C., Mairson, H.G., Vardi, M.Y.: Undecidable
  boundedness problems for datalog programs. J. Log. Program.  25(2),  163--190
  (1995)

\bibitem{Holzer2008}
Holzer, M., Kutrib, M., Malcher, A.: Multi-head finite automata:
  Characterizations, concepts and open problems. In: Neary, T., Woods, D.,
  Seda, A.K., Murphy, N. (eds.) CSP. EPTCS, vol.~1, pp. 93--107 (2008)

\bibitem{Jones1975}
Jones, N.D.: Space-bounded reducibility among combinatorial problems. J.
  Comput. Syst. Sci.  11(1),  68--85 (1975)

\bibitem{Laurent2001}
Laurent, O.: A token machine for full geometry of interaction (extended
  abstract). In: Abramsky, S. (ed.) TLCA. LNCS, vol. 2044, pp. 283--297.
  Springer (May 2001)

\bibitem{Lierler2009}
Lierler, Y., Lifschitz, V.: One more decidable class of finitely ground
  programs. In: Hill, P.M., Warren, D.S. (eds.) ICLP. LNCS, vol. 5649, pp.
  489--493. Springer (2009)

\bibitem{Ohkubo1987}
Ohkubo, M., Yasuura, H., Yajima, S.: On parallel computation time of
  unification for restricted terms. Tech. rep., Kyoto University (May 1987)

\bibitem{Pighizzini2013}
Pighizzini, G.: Two-way finite automata: Old and recent results. Fund. Inform.
  126(2--3),  225--246 (2013)

\bibitem{Savage1998}
Savage, J.E.: Models of computation - exploring the power of computing.
  Addison-Wesley (1998)

\bibitem{Schopp2007}
Schöpp, U.: Stratified bounded affine logic for logarithmic space. In: LICS.
  pp. 411--420. IEEE Computer Society (2007)

\bibitem{Seiller2012a}
Seiller, T.: Interaction graphs: Multiplicatives. Ann. Pure Appl. Logic  163,
  1808--1837 (Dec 2012)

\end{thebibliography}
