1: \documentclass{amsart}

2: \usepackage{amsmath, amssymb, amsthm, amscd, graphicx}

3: \usepackage{epstopdf}

4: 

5: % for 100% printing

6: \hoffset-1.2cm

7: \voffset+0.5cm

8: 

9: \setlength{\unitlength}{1mm}

10: 

11: \theoremstyle{plain}

12: \newtheorem{prop}{Proposition}[section]

13: \newtheorem{coro}[prop]{Corollary}

14: \newtheorem{fact}[prop]{Fact}

15: \newtheorem{conj}[prop]{Conjecture}

16: \newtheorem{lemm}[prop]{Lemma}

17: \newtheorem{ques}[prop]{Question}

18: 

19: \theoremstyle{definition}

20: \newtheorem{defi}[prop]{Definition}

21: \newtheorem{nota}[prop]{Notation}

22: \newtheorem{exam}[prop]{Example}

23: \newtheorem{rema}[prop]{Remark}

24: 

25: \numberwithin{equation}{section}

26: 

27: % bibliography

28: 

29: \def\Reff#1; #2; #3; #4; #5; #6; #7\par{%

30: \bibitem{#1} #2, {\it #3}, #4 {\bf #5} (#6) #7}

31: 

32: \def\Ref#1; #2; #3; #4\par{%

33: \bibitem{#1} #2, {\it #3}, #4}

34: 

35: \let\a=\alpha

36: \renewcommand{\aa}[1]{a_{#1}}

37: \renewcommand{\AA}[1]{A_{#1}}

38: \newcommand{\AAm}[1]{A_{#1}^{\scriptscriptstyle-}}

39: \newcommand{\AAp}[1]{A_{#1}^{\scriptscriptstyle+}}

40: \newcommand{\act}{\cdot}

41: \newcommand{\ALD}{\mathtt{ALD}}

42: \newcommand{\ALDi}{\mathtt{ALD}_1}

43: \newcommand{\ALDii}{\mathtt{ALD}_2}

44: \newcommand{\Ass}{\mathtt{A}}

45: 

46: \let\b=\beta

47: \newcommand{\BB}{\mathtt{B}}

48: \newcommand{\blue}[1]{\widehat{#1}}

49: \newcommand{\Bp}{B_{\scriptscriptstyle\bullet}}

50: 

51: \newcommand{\CC}{\mathbb{C}}

52: \newcommand{\cf}{{\it cf.}\ }

53: \newcommand{\ccl}{c\ell}

54: \newcommand{\cl}{\mathtt{cl}}

55: \newcommand{\cg}{\leftrightarrow}

56: \newcommand{\comp}{\mathbin{\scriptstyle\bullet}}

57: 

58: \let\d=\delta

59: \newcommand{\D}{\Delta}

60: \newcommand{\dd}[2]{d_{#1,#2}}

61: \newcommand{\ddd}[3]{d_{#1,#2,#3}}

62: \newcommand{\Dd}[2]{\delta_{#1,#2}}

63: \newcommand{\Ddt}[2]{\widetilde\delta_{#1,#2}}

64: \newcommand{\DD}[2]{\D_{#1}^{#2}}

65: 

66: \newcommand{\e}{\varepsilon}

67: \newcommand{\ea}{{\scriptstyle\varnothing}} % empty address

68: \newcommand{\eb}{b}

69: \newcommand{\ee}{e} % orientation 

70: \newcommand{\EE}[1]{\sim_{#1}}

71: \newcommand{\EEq}[1]{\mathrel{\widetilde\equiv_{#1}}}

72: \newcommand{\eg}{{\it e.g.}}

73: \newcommand{\eq}[1]{\equiv_{#1}}

74: \newcommand{\Eq}[1]{\mathrel{\widehat\equiv_{#1}}}

75: \newcommand{\EQ}[1]{\mathrel{\leftrightarrow_{{#1}}}}

76: \newcommand{\etc}{{\it etc.}}

77: \newcommand{\ev}{\mathtt{eval}}

78: \newcommand{\eev}{\mathit{eval}}

79: 

80: \newcommand{\ff}{f} % a function

81: \newcommand{\ffm}{f_{\!\scriptscriptstyle-}}

82: \newcommand{\ffp}{f_{\!\scriptscriptstyle+}}

83: 

84: \let\g=\gamma

85: \let\ge=\geqslant

86: \newcommand{\GA}{\Geo{\mathtt{A}}}

87: \newcommand{\GALD}{\Geo\ALD}

88: \newcommand{\GALDp}{\Geo\ALD^{\scriptscriptstyle+}}

89: \renewcommand{\gg}{g} % a function

90: \renewcommand{\ggg}{g'} % an element of a group

91: \newcommand{\Geo}[1]{\mathtt{Geom}_{#1}}

92: \newcommand{\GGeo}[1]{\mathcal{G}eom_{#1}}

93: \newcommand{\GGA}{\GGeo{\mathtt{A}}}

94: \newcommand{\GGAp}{\GGeo{\mathtt{A}}^{\scriptscriptstyle+}}

95: \newcommand{\GGALD}{\GGeo{\mathtt{ALD}}}

96: \newcommand{\GGALDp}{\GGeo{\mathtt{ALD}}^{\scriptscriptstyle+}}

97: \newcommand{\GGLD}{\GGeo{\LD}}

98: \newcommand{\GGLDp}{\GGeo{\LD}^{\scriptscriptstyle+}}

99: \newcommand{\GGLL}{\GGeo{\LLL}}

100: \newcommand{\GGLLp}{\GGeo{\LLL}^{\scriptscriptstyle+}}

101: \newcommand{\ggm}{g_{\!\scriptscriptstyle-}}

102: \newcommand{\ggp}{g_{\!\scriptscriptstyle+}}

103: \newcommand{\GLD}{\Geo{\LD}}

104: \newcommand{\GLDp}{\Geo{\LD}^{\scriptscriptstyle+}}

105: \newcommand{\GLL}{\Geo{\LLL}}

106: \newcommand{\GLLp}{\Geo{\LLL}^{\scriptscriptstyle+}}

107: 

108: \newcommand{\id}{id}

109: \newcommand{\ie}{{\it i.e.}}

110: \let\ince=\subseteq

111: \newcommand{\IInt}{\mathcal{C}c}

112: \renewcommand{\Im}{\mathrm{Im}}

113: \newcommand{\Int}{\mathtt{Cc}}

114: \newcommand{\inv}{^{-1}}

115: \newcommand{\Inv}{{}^{-1}}

116: \newcommand{\INV}[1]{(#1)^{-1}}

117: 

118: \newcommand{\LD}{\mathtt{LD}}

119: \let\le=\leqslant

120: \newcommand{\LL}{L}% algebraic law

121: \newcommand{\LLbis}{L'}% another algebraic law

122: \newcommand{\LLL}{\mathcal{L}}% family of algebraic laws

123: \newcommand{\LLp}{{L'}}% algebraic law

124: 

125: \renewcommand{\o}{\omega}

126: \newcommand{\onto}{\mathrel{\to\hspace{-0.7em}\to}}

127: \newcommand{\OO}[1]{L_{#1}}%Operateur

128: \newcommand{\OOp}[1]{L_{#1}^{\scriptscriptstyle+}}%Operateur

129: \newcommand{\OObis}[1]{{L'}_{#1}}%Operateur

130: \newcommand{\OObisp}[1]{{L'}_{#1}^{\scriptscriptstyle+}}%Operateur

131: \newcommand{\OOO}[2]{{#1}_{#2}}%Operateur

132: \newcommand{\OOOm}[2]{{#1}_{#2}^{\scriptscriptstyle-}}%Operateur

133: \newcommand{\OOOp}[2]{{#1}_{#2}^{\scriptscriptstyle+}}%Operateur

134: \newcommand{\op}{*}

135: \newcommand{\Op}{\mathbin{\scriptstyle\square}}

136: \newcommand{\OP}{\circ}

137: 

138: \newcommand{\proj}{\mathtt{pr}}

139: 

140: \newcommand{\rel}{\diamond}

141: \newcommand{\resp}{{\it resp.{~}}}

142: \newcommand{\RLD}{R_{\LD}}

143: \newcommand{\RLDp}{R_{\LD}^{\scriptscriptstyle+}}

144: \newcommand{\RLL}{R_{\LLL}}

145: \newcommand{\RLLp}{R_{\LLL}^{\scriptscriptstyle+}}

146: \newcommand{\RR}{\mathbb{R}}

147: 

148: \let\s=\sigma

149: \newcommand{\Set}{S}

150: \newcommand{\sh}[1]{\mathtt{sh}_{#1}}

151: \newcommand{\ssh}[1]{\mathit{sh}_{#1}}

152: \newcommand{\Sign}{\mathcal{F}} % signature

153: \renewcommand{\ss}[1]{\sigma_{#1}}

154: \renewcommand{\SS}[1]{\Sigma_{#1}}

155: \newcommand{\SSm}[1]{\Sigma_{#1}^{\scriptscriptstyle-}}

156: \newcommand{\SSp}[1]{\Sigma_{#1}^{\scriptscriptstyle+}}

157: \newcommand{\sub}[2]{\mathtt{sub}(#1,#2)} % subterm

158: \newcommand{\subst}{\sigma} % substitution

159: \newcommand{\substt}{\tau} % substitution

160: 

161: \newcommand{\Term}[1]{\mathtt{Term}_{#1}} % terms

162: \newcommand{\TTerm}[2]{\mathtt{Term}_{#1,#2}} % terms

163: \newcommand{\tm}{l}

164: \newcommand{\toLDp}{\to_{\LD}^{\scriptscriptstyle+}}

165: \newcommand{\toLLp}{\to_{\LLL}^{\scriptscriptstyle+}}

166: \newcommand{\To}{\Term{\op}}

167: \newcommand{\Tox}{\Term{\op,\OP,\xx}}

168: \newcommand{\tp}{r}

169: \renewcommand{\tt}{t} % a term

170: \newcommand{\tti}{t_1} % a subterm

171: \newcommand{\ttii}{t_2} % a subterm

172: \newcommand{\ttiii}{t_3} % a subterm

173: \newcommand{\ttz}{t_0} % a subterm

174: \newcommand{\ttt}{t'} % another term

175: \newcommand{\ttti}{t'_1} % a subterm

176: \newcommand{\tttii}{t'_2} % a subterm

177: \newcommand{\tttiii}{t'_3} % a subterm

178: \newcommand{\tttt}{t''} % another term

179: \newcommand{\ttttt}{t'''} % another term

180: \newcommand{\tttz}{t'_0} % another subterm

181: \newcommand{\TS}{\Term\Sign} % terms

182: \newcommand{\TSV}{\TTerm\Sign\Var} % terms

183: \newcommand{\TSx}{\TTerm\Sign\xx}

184: 

185: \newcommand{\Var}{\mathcal{X}} % variables

186: 

187: \newcommand{\ww}{w}

188: \newcommand{\WW}[1]{\mathcal{W}_{#1}}

189: \newcommand{\WALD}{\mathcal{W}_{\ALD}}

190: \newcommand{\WLL}{\mathcal{W}_{\LLL}}

191: 

192: \newcommand{\xx}{x}

193: \newcommand{\XX}[1]{L_{#1}}

194: \newcommand{\XXp}[1]{L_{#1}^{\scriptscriptstyle+}}

195: 

196: \newcommand{\yy}{y}

197: \newcommand{\YY}[1]{L'_{#1}}

198: \newcommand{\YYp}[1]{{L'}_{#1}^{\scriptscriptstyle+}}

199: 

200: \newcommand{\zz}{z}

201: 

202: \hyphenation{mon-oid mon-oids Lem-ma}

203: 

204: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

205: \begin{document}

206: 

207: \author{Patrick DEHORNOY}

208: \address{Laboratoire de Math\'ematiques Nicolas

209: Oresme UMR 6139\\ Universit\'e de Caen,

210: 14032~Caen, France}

211: \email{dehornoy@math.unicaen.fr}

212: \urladdr{//www.math.unicaen.fr/\!\hbox{$\sim$}dehornoy}

213: 

214: \title{Using groups for investigating rewrite systems}

215: 

216: \keywords{algebraic law, term rewrite system, word problem, confluence}

217: 

218: \subjclass{68Q01, 68Q42, 20N02}

219: 

220: \begin{abstract}

221: We describe several technical tools that prove to be efficient for investigating the rewrite systems associated with a family of algebraic laws, and might be useful for more general rewrite systems. These tools consist in introducing a monoid of partial operators, listing the monoid relations expressing the possible local confluence of the rewrite system, then introducing the group presented by these relations, and finally replacing the initial rewrite system with a internal process entirely sitting in the latter group. When the approach can be completed, one typically obtains a practical method for constructing algebras satisfying prescribed laws and for solving the associated word problem.

222: \end{abstract}

223: 

224: \maketitle

225: 

226: \section*{Introduction}

227: 

228: Let~$\LLL$ be a family of algebraic laws, typically associativity, commutativity, distributivity, \etc, involving a certain signature~$\Sign$, and let~$\Var$ be an infinite set of variables. By associating with every law $\tm = \tp$ of~$\LLL$ the two rules $\tm \to \tp$ and $\tp \to \tm$, we obtain a rewrite system~$R_{\LLL}$ on the family of all $\Sign$-terms constructed on~$\Var$. The aim of this paper is to present a general method for investigating the rewrite systems of the form~$R_{\LLL}$ by introducing an associated monoid or group. This approach proved to be useful for various systems~$R_{\LLL}$, and it might be relevant for more general rewrite systems, typically those arising in a context of algebra~\cite{Coh, DeJ}.

229: 

230: The approach comprises three steps.

231: The first one consists in associating with the rewrite system~$R_{\LLL}$ a certain inverse monoid ~$\GGeo{\LLL}$ of partial operators by taking into account where and in which direction the rules are applied; this monoid is called the {\it geometry monoid} for~$\LLL$ as it captures several specific geometrical phenomena specific to~$\LLL$.

232: 

233: The second step consists in replacing the inverse monoid~$\GGeo{\LLL}$ with a group $\Geo{\LLL}$ that resembles it: when the laws of~$\LLL$ are simple enough, typically when no variable is repeated more than once in each side of the laws, the group~$\Geo{\LLL}$ can be defined to simply be the universal group of~$\GGeo{\LLL}$; in more complicated cases, a convenient group can be obtained by investigating the local confluence relations holding in~$\GGeo{\LLL}$ and defining~$\Geo{\LLL}$ to be the group presented by these relations. 

234: 

235: The third---and technically main---step is an internalization process that replaces the external action of~$\GGeo{\LLL}$ on terms by an internal multiplication in~$\Geo{\LLL}$. 

236: 

237: When all three steps can be completed, various questions about the laws~$\LLL$ can be successfully addressed, typically constructing algebras that satisfy these laws, or solving the word problem of~$\LLL$, \ie, designing an algorithm that decides whether two terms are equivalent under the congruence generated by~$R_{\LLL}$.

238: 

239: In this paper, we shall present the approach in a general setting and mention some of the existing examples. However, in order to make this paper more than a survey, we shall put the emphasis on a new example for which the method had not been considered before, namely the case of  the augmented left self-distributivity laws, or $\ALD$-laws, defined to be the following three laws

240: \begin{equation}

241: \label{E:ALD}

242: \tag{$\ALD$}

243: \begin{cases}

244: \ x \op (y \op z) = (x \op y) \op (x \op z),\\

245: \ x \op (y \OP z) = (x \op y) \OP (x \op z),\\

246: \ x \op (y \op z) = (x \OP y) \op z.

247: \end{cases}

248: \end{equation}

249: These laws and the algebras that satisfy them, called {\it $\ALD$-algebras} in this paper, appeared recently in several frameworks \cite{Dhb, Dhe, Dhj}, and they had never been addressed from the point of view of the geometry monoid. We shall see that a number of technical questions remain open in this seemingly difficult case. Nevertheless, the method is sufficient to naturally lead to the construction of a (highly non-trivial) example of such an $\ALD$-algebra. Technically, the main step is the construction of what is called a blueprint for the $\ALD$-laws.

250: 

251: The leading principle underlying the approach is to use the geometry monoid to {\it guess} some formulas, and then to check the latter by a direct verification. Typically, concentrating on the possible confluence relations that hold in the geometry monoid~$\GGLL$ and using these relations for introducing a group~$\GLL$ relies on a heuristic approach rather than on any uniform proved argument. Now the point is that this approach, which might seem loose, actually works in some definitely non-trivial cases: thus what legitimates the scheme is not some general a priori argument, but rather its a posteriori success.

252: 

253: The paper is organized as follows. The geometry monoid~$\GGLL$ is introduced in Section~\ref{S:Monoid}. The process for going from the monoid~$\GGLL$ to a group~$\GLL$ is described in Section~\ref{S:Group}. The principle of internalizing terms in the geometry monoid/group is explained in Section~\ref{S:Blue}. Next, we show in Section~\ref{S:Using} how the general study developed in Sections~\ref{S:Group} and~\ref{S:Blue} can be used, in good cases, to investigate a family of algebraic laws, with a special emphasis on the example of~$\ALD$. Finally, in Section~\ref{S:Conf}, we briefly address the question of recognizing whether~$\GLL$ is a group of fractions, which amounts to investigating whether a locally confluent system is actually confluent: we insist on some methods for doing that even in a non-noetherian framework, \ie, when the standard methods fail.

254: 

255: \section{The geometry monoid~$\GGLL$}

256: \label{S:Monoid}

257: 

258: The first step in our study consists in analysing a rewrite system by means of a monoid of partial operators. The general idea is as follows. If $R$ is a rewrite system on some set~$T$, then, in the most general situation, several rules may be applied to a given element~$\tt$ of~$T$, and, on the other hand, not every rule need to apply to~$\tt$, so the action of~$R$ on~$T$ cannot be described by functional operators in a natural way. However, by fixing the value of enough parameters, we can always discard the lack of uniqueness and describe~$R$ in terms of partial functional operators. 

259: 

260: Here we shall apply this scheme in the case when $T$ is a set of terms and $R$ consists of rules that can be applied to various subterms, more precisely when $R$ is the rewrite system associated with a family of algebraic laws. In this case, we shall obtain uniqueness, hence functionality, whenever the rule and the position are fixed.

261: 

262: \subsection{Applying an algebraic law}

263: 

264: For $\Sign$ a signature consisting of operation symbols exclusively, and $\Var$ a nonempty set of variables, we denote by $\TSV$ the family of all terms built using operation symbols from~$\Sign$ and variables from~$\Var$. Practically, we shall assume that some infinite list of variables has been fixed, and drop the reference to~$\Var$, thus writing~$\Term\Sign{}$ for~$\TSV$. An algebraic law is a pair of terms $\{\tm, \tp\}$---usually denoted as $\tm = \tp$. We shall speak of an {\it ordered} algebraic law to insist that the pair~$(\tm, \tp)$ is ordered, \ie, a distinguished orientation is chosen. For instance, there are two oriented versions for the standard associativity law $\xx \cdot (\yy \cdot \zz) = (\xx \cdot \yy) \cdot \zz$, namely the pair $(\xx \cdot (\yy \cdot \zz), (\xx \cdot \yy) \cdot \zz)$, and the symmetric pair. Note that, as the commutativity law is $\xx \cdot \yy = \yy \cdot \xx$ is involutive, there is, up to a substitution of variables, only one oriented version.

265: 

266: In this context, the fundamental operation of {\it applying} an algebraic law to a term corresponds to a rewrite system: applying $\tm=\tp$---\ie, $\{\tm, \tp\}$---to some term~$\tt$ means replacing some subterm~$\ttz$ of~$\tt$ which happens to be a substitute of~$\tm$ with the corresponding substitute~$\tttz$ of~$\tp$, or {\it vice versa}. This means that there exists a position~$\a$ and a substitution~$\subst$, \ie, a mapping from~$\Var$ into~$\TS$, such that the $\a$th subterm of~$\tt$ is $\tm\subst$ and $\ttt$ is obtained from~$\tt$ by replacing the $\a$th subterm with~$\tp\subst$---or {\it vice versa} exchanging the roles of~$\tm$ and~$\tp$ (Figure~\ref{F:Apply}). In other words, we apply one of the two rules $\tm \to \tp$, $\tp \to \tm$.

267: 

268: \begin{figure} [htb]

269: \begin{picture}(70,42)

270: \put(17,39){$\tt$}

271: \put(58,39){$\ttt$}

272: \put(0,7){\includegraphics{Apply.eps}}

273: \put(16,18){$\tm$}

274: \put(13.5,25){$\a$}

275: \put(54,25){$\a$}

276: \put(10,9){$\underbrace{\hbox to 14mm{\hfill}}$}

277: \put(12,3){$\ttz=\tm\subst$}

278: \put(56.5,17){$\tp$}

279: \put(51,6){$\underbrace{\hbox to 16mm{\hfill}}$}

280: \put(54,0){$\tttz=\tp\subst$}

281: \end{picture}

282: \caption{\smaller Applying the law $\tm=\tp$ to a term~$\tt$, here viewed as a rooted tree: one replaces some subterm~$\ttz$ of~$\tt$ that is a substitute of~$\tm$ with the corresponding substitute of~$\tp$---or vice versa.}

283: \label{F:Apply}

284: \end{figure}

285: 

286: \begin{defi}

287: For each family of algebraic laws~$\LLL$ involving the signature~$\Sign$, we denote by~$R_{\LLL}$ the rewrite system on~$\Term\Sign{}$ consisting of all rules $\tm \to \tp$ and $\tp \to \tm$ for $\tm = \tp$ a law of~$\LLL$.

288: \end{defi}

289: 

290: Thus, by very definition, we have

291: 

292: \begin{prop}

293: \label{P:Equiv}

294: Let $\LLL$ be a family of algebraic laws involving the signature~$\Sign$. Then two terms~$\tt, \ttt$ in~$\TS$ are $\LLL$-equivalent if and only if one has $\tt \EQ\LLL \ttt$, where $\EQ\LLL$ is the equivalence relation generated by~$R_{\LLL}$.

295: \end{prop}

296: 

297: \subsection{Geometry monoid: the principle}

298: 

299: The rewrite systems~$R_{\LLL}$ are not functional: there may be many ways to apply one of its rules to a given term. However, these systems can be viewed as the union of a family of partial functions, each of which corresponds to choosing a law, an orientation, and a position.

300: 

301: For the sequel, it is convenient to fix an addressing system for the subterms of a term, \ie, for the positions in a term. As is usual, we shall see terms as rooted trees (\cf~Figure~\ref{F:Apply}), where the inner nodes are labeled using operation symbols, and the leaves are labeled using variables. Then a subterm of a term~$\tt$ is naturally specified by the node where its root lies, which is itself determined by the path that connects the root of the tree to that node. If all operation symbols are binary---which will be the case in the examples considered below---we can for instance use finite sequences of~$0$'s and~$1$'s to describe such a path, using $0$ for ``forking to the left'' and $1$ for ``forking to the right''. We use $\ea$ for the empty address, \ie, the address of the root. If $\tt$ is a term, and $\a$ is an address, we denote by $\sub\tt\a$ the $\a$-th subterm of~$\tt$, \ie, the subterm of~$\tt$ whose position is specified by~$\a$. Note that $\sub\tt\a$ exists only for~$\a$ short enough: $\sub\tt\ea$ always exists and equals~$\tt$, but, for instance, $\sub\tt0$ and~$\sub\tt1$, which are the left and the right subterms of~$\tt$ respectively, exist only if $\tt$ is not a variable.

302: 

303: \begin{defi}\label{D:Oper}

304: $(i)$ Assume that $\LL$ is an oriented algebraic law. For each address~$\a$ and each orientation~$\ee$ (namely $+$ or $-$), we denote by $\OOO\LL\a^\ee$ the (partial) operator on terms corresponding to applying~$\LL$ at

305: position~$\a$ in direction~$\ee$. 

306: 

307: $(ii)$ For~$\LLL$ a family of oriented laws, we define the {\it geometry monoid of~$\LLL$}, denoted~$\GGLL$, to be the monoid generated, using composition, by all operators~$\OOO\LL\a^\ee$ when $\LL$ ranges over~$\LLL$, $\a$ ranges over all addresses, and $\ee$ ranges over~$\{+,-\}$.

308: \end{defi}

309: 

310: We shall always think of the operators~$\OOO\LL\a^\ee$ as acting on the right, thus writing $\tt \act \ff$ rather than $\ff(\tt)$ for the image of the term~$\tt$ under the operator~$\ff$. To be coherent, we use the reversed composition, denoted~$\comp$, in the geometry monoid. Thus, $\ff \comp \gg$ means ``$\ff$ then $\gg$''.

311: 

312: \begin{rema}

313: When a term~$\ttz$ is a substitute of the term~$\tm$, the substitution~$\subst$ such that $\ttz = \tm\subst$ is not unique, as the value of~$\xx\subst$ is uniquely determined only for those variables~$\xx$ that occur in~$\tm$. Hence, for $\LL = (\tm, \tp)$, the operator~$\OOOp\LL\a$ is functional only if the same variables occur in~$\tm$ and~$\tp$. The laws that satisfy this condition will be called {\it balanced}. Although this is not necessary, we shall always restrict to balanced laws in the sequel. Thus we discard laws like $\xx = \xx \op \yy$; note that the algebras obeying such laws are trivial.

314: \end{rema}

315: 

316: By construction, every element in a geometry monoid~$\GGLL$ is a finite product of operators~$\OOO\LL\a^e$ with~$\LL$ in~$\LLL$. It will be convenient in the sequel to fix the following notation:

317: 

318: \begin{nota}

319: For~$\LLL$ a family of (oriented, balanced) laws, we denote by~$\WLL$ the free monoid generated by all letters~$\OOO\LL\a^e$ with~$\LL \in \LLL$, $\a \in \{0,1\}^*$, and $e \in \{+,-\}$; we denote by $\eev$ the canonical evaluation morphism 

320: $$\eev : \WLL \to \GGLL.$$

321: \end{nota} 

322: 

323: Thus $\WLL$ consists of all abstract products of letters~$\OOO\LL\a^e$, while $\GGLL$ consists of actual operators on terms. We shall see soon that, in general (and as can be expected), the evaluation mapping is far from injective, \ie, the geometry monoid~$\GGLL$ is far from free.

324: 

325: \subsection{Geometry monoid: the example of~$\ALD$}

326: \label{S:ALD}

327: 

328: To illustrate our approach, we consider the family~$(\ALD)$ consisting of the following three algebraic laws:

329: \begin{gather}

330: \tag{$\LD$}\label{E:LD}

331: \xx \op (\yy \op \zz) = (\xx \op \zz) \op (\xx \op \zz),\\

332: \tag{$\ALDi$}\label{E:ALD1}

333: \xx \op (\yy \OP \zz) = (\xx \op \zz) \OP (\xx \op \zz),\\

334: \tag{$\ALDii$}\label{E:ALD2}

335: \xx \op (\yy \op \zz) = (\xx \OP \yy) \op \zz.

336: \end{gather}

337: The specific interest of this choice is that, contrary to~$(\LD)$ alone, the above mixed laws, collectively denoted~$(\ALD)$---``Augmented Left self-Distributivity''---in the sequel, have never been investigated from the viewpoint of the geometry monoid and, so, the results we shall obtain below are new.

338: 

339: Here the signature consists of two binary operation symbols~$\op, \OP$. The law~\eqref{E:LD} is the left self-distributivity law, which was extensively studied in~\cite{Dgd}. The additional laws~\eqref{E:ALD1} and~\eqref{E:ALD2} express that $\op$ is left distributive with respect to~$\OP$ and that $\OP$ behaves like a sort of composition relative to~$\op$. Many examples of $\LD$-algebras, \ie, of structures satisfying~\eqref{E:LD}, happen to be equipped with a second operation that satisfies the mixed laws~$(\ALDi)$ and~$(\ALDii)$. This is in particular the case for every group equipped with the $\LD$-operation $\xx \op \yy := \xx \yy\xx\inv$: in this case, defining the second operation to be the multiplication $\xx \OP \yy := \xx \yy$ yields an $\ALD$-algebra---and more, actually, namely an $\LD$-monoid in the sense of~\cite{Dgd}, Chapter~XI.

340: 

341: By definition, the geometry monoid~$\GGALD$ is generated by three families of operators, corresponding to the three laws. In the specific case, we observe that the actions of the operators $\OOOp\LD\a$ and $(\ALDi)\OOOp{}\a$ are parallel, as both consist in distributing the left subterm to the two halves of the right subterm. However, their domains are disjoint, as $\OOOp\LD\a$ applies only when the symbol at~$\a1$ is~$\op$, while $(\ALDi)\OOOp{}\a$ applies only when the symbol at~$\a1$ is~$\OP$. Hence, instead of considering two operators separately, we shall introduce their union, which is still functional, and denote it by~$\SSp\a$. In particular, we have

342: \begin{equation}

343: \SSp\ea : \tti \op (\ttii \Op \ttiii) \to (\tti \op \ttii)

344: \Op (\tti \op \ttiii), 

345: \end{equation}

346: \ie, $\SSp\ea$, which will be also simply denoted $\SSp{}$, is the operator that maps every term of the form $\tti \op (\ttii \Op \ttiii)$ to the corresponding term $(\tti \op \ttii) \Op (\tti \op \ttiii)$, where $\Op$ stands for either~$\op$ or~$\OP$. Similarly, we have

347: \begin{equation}

348: \AAp\ea: \tti \op (\ttii \op \ttiii) \to (\tti \OP \ttii) \op \ttiii,

349: \end{equation}

350: \ie, $\AAp\ea$, also denoted~$\AAp{}$, maps every term of the form $\tti \op (\ttii \op \ttiii)$ to $(\tti \OP \ttii) \op \ttiii$. By definition, the geometry monoid~$\GGeo\ALD$ is the monoid generated by all partial operators~$\SSp\a$, $\SSm\a$, $\AAp\a$, and~$\AAm\a$ with~$\a$ ranging over~$\{0,1\}^*$.

351: 

352: As displayed in Figure~\ref{F:Exam}, a given term may belong to the domain and the range of several operators~$\SS\a^{\pm}$ and~$\AA\a^{\pm}$.

353: 

354: \begin{figure} [htb]

355: \begin{picture}(105,58)

356: \put(0,0){\includegraphics{Exam.eps}}

357: \put(5,40){$\op$}

358: \put(9,32){$\op$}

359: \put(1,32){$\xx_1$}

360: \put(13,24){$\op$}

361: \put(5,24){$\xx_2$}

362: \put(9,16){$\xx_3$}

363: \put(17,16){$\xx_4$}

364: \put(45,40){$\op$}

365: \put(49,32){$\op$}

366: \put(41,32){$\xx_1$}

367: \put(53,24){$\xx_4$}

368: \put(45,24){$\OP$}

369: \put(49,16){$\xx_3$}

370: \put(41,16){$\xx_2$}

371: \put(90,53){$\op$}

372: \put(84,45){$\op$}

373: \put(96,45){$\op$}

374: \put(80,37){$\xx_1$}

375: \put(88,37){$\OP$}

376: \put(92,37){$\xx_1$}

377: \put(100,37){$\xx_4$}

378: \put(84,29){$\xx_2$}

379: \put(92,29){$\xx_3$}

380: \put(90,25){$\op$}

381: \put(86,17){$\OP$}

382: \put(93,17){$\xx_4$}

383: \put(82,9){$\xx_1$}

384: \put(89.5,9){$\OP$}

385: \put(86,1){$\xx_2$}

386: \put(93,1){$\xx_3$}

387: \put(25,30){$\AA1^-$}

388: \put(67,16){$\AA\ea^+$}

389: \put(67,37){$\SS\ea^+$}

390: \end{picture}

391: \caption{\smaller Case of~$\ALD$: Two positive operators apply to the term $\xx_1 \op ((\xx_2 \OP \xx_3) \op \xx_4)$, namely~$\SSp\ea$ and~$\AAp\ea$, while one negative operator applies to it, namely~$\AAm1$, \ie, the copy of~$\AAm\ea$ acting at position~$1$.}

392: \label{F:Exam}

393: \end{figure}

394: 

395: \begin{rema}

396: \label{R:Position}

397: For a signature~$\Sign$ comprising more than one operation symbol, as is the case with~$\ALD$, only taking into account the address where a law is applied does not exhaust all information. Indeed, when an operator~$\OO\a^e$ is applied to a term~$\tt$, the complete list of the operation symbols that occur in~$\tt$ above~$\a$ may be important, typically in terms of the relations possibly connecting various operators.

398: In order to include such data, we can use positions instead of addresses to index the operators of the geometry monoid, a {\it position} being defined to be a finite sequence of even length consisting of alternating operation symbols and forking directions: for instance, $(\op, 1)$ and $(\op, 1, \OP, 0)$ are positions that refine the addresses~$1$ and~$10$ respectively. In this framework, the operator~$\AA1^-$ mentioned in Figure~\ref{F:Exam} would become $\AA{(\op,1)}^-$, \ie, $\AA1^-$ applied to a term with~$\op$ at the root. Observe that an operator~$\OO\a^e$ as defined in Definition~\ref{D:Oper} is, as a set of pairs of terms, just the disjoint union of all operators~$\OO{p}^e$ with~$p$ a position that projects on the address~$\a$ when the operation symbols are forgotten. Although these refinements may be necessary in some cases, they are not in the examples considered in this paper, in particular~$\ALD$, and there will be no need to split the operators~$\OO\a^e$ into more elementary components.

399: \end{rema}

400: 

401: \subsection{Connection between $\GGLL$ and $\LLL$-equivalence}

402: 

403: We saw in Proposition~\ref{P:Equiv} that $\LLL$-equivalence is directly connected with the equivalence relation~$\EQ\LLL$ associated with the rewrite system~$R_{\LLL}$. As a consequence, it is also connected with the geometry monoid~$\GGLL$: 

404: 

405: \begin{prop}

406: \label{P:Basic}

407: Let $\LLL$ be any family of algebraic laws involving the signature~$\Sign$. Then two terms~$\tt, \ttt$ in~$\TS$ are $\LLL$-equivalent if and only if some element of the geometry monoid~$\GGLL$ maps~$\tt$ to~$\ttt$.

408: \end{prop}

409: 

410: \begin{proof}

411: Let us write $\tt \equiv \ttt$ if some operator of~$\GGLL$ maps~$\tt$ to~$\ttt$. First $\tt \equiv\ttt$ implies $\tt \EQ\LLL \ttt$. Indeed, by construction, $\ttt = \tt \act \OOO\LL\a^\ee$ implies $\tt \EQ\LLL \ttt$. As $\EQ\LLL$ is transitive, the same is true when several operators~$\OOO\LL\a^\ee$ are composed.

412: 

413: Conversely, $\EQ\LLL$ is the congruence generated by the instances of the laws of~$\LLL$, so, in order to prove that $\tt \EQ\LLL \ttt$ implies $\tt \equiv \ttt$, it is enough to prove that $\equiv$ is a congruence on terms, and that it contains all instances of the laws of~$\LLL$. Now, $\equiv$ is an equivalence relation because $\GGLL$ is closed under composition and contains the identity mapping, and it is a congruence, \ie, it is compatible with all operations of~$\Sign$. Indeed, assume that $\OOOp\LL\a$ maps~$\tt$ to~$\ttt$. Let $\ttz$ be any term and $\Op$ be any operation in~$\Sign$. Then---assuming that all operations of~$\Sign$ are binary and $0,1$~addresses are used---the operator $\OOOp\LL{0\a}$ maps~$\ttz\Op\tt$ to~$\ttz\Op\ttt$, while $\OOOp\LL{1\a}$ maps~$\tt\Op\ttz$ to~$\ttt\Op\ttz$. Finally, assume that $(\tt, \ttt)$ is an instance of some law~$\LL$ of~$\LLL$. This means that there exists a substitution~$\subst$ such that, assuming that $\LL$ is $\tm = \tp$, one has $\tt = \tm\subst$ and $\ttt = \tp\subst$. Now, by definition, $\OOOp\LL\ea$ maps~$\tt$ to~$\ttt$, so $\tt \equiv \ttt$ holds.

414: \end{proof}

415: 

416: Our aim in this paper is not to develop a general theory of the geometry monoid. However, we mention two results, namely one about the structure of~$\GGLL$ and one about its dependence on~$\LLL$.

417: 

418: First, we observe that, by construction, each operator in the geometry monoid~$\GGLL$ is close to admitting an inverse. Indeed, the operator~$\OOOm\LL\a$ is, as a set of pairs, the inverse of the operator~$\OOOp\LL\a$, \ie,  $\OOOp\LL\a$ maps~$\tt$ to~$\ttt$ if and only if $\OOOm\LL\a$ maps~$\ttt$ to~$\tt$. This is not enough to make~$\GGLL$ into a group, as the composition $\OOOp\LL\a \comp \OOOm\LL\a$ is the identity operator of its domain only, and {\it not} the identity operator of~$\TS$ in general, but we have:

419: 

420: \begin{prop}

421: Assume that $\LLL$ is a family of balanced algebraic laws. Then $\GGLL$ is an inverse monoid.

422: \end{prop}

423: 

424: \begin{proof}

425: Assume that $\ff$ is a nonempty operator in~$\GLL$. Then, by construction, there exists a word~$\ww$ in~$\WLL$ such that $\ff$ equals $\eev(\ww)$. Let $\ww\inv$ be the formal inverse of~$\ww$, \ie, the word obtained from~$\ww$ by exchanging~$\OOOp\LL\a$ and~$\OOOm\LL\a$ everywhere in~$\ww$ and reversing the order of the letters, and let $\gg := \eev(\ww\inv)$. An immediate induction shows that a pair of terms~$(\tt,\ttt)$ belongs to~$\ff$ if and only if the pair~$(\ttt,\tt)$ belongs to~$\gg$, and we deduce

426: $$\ff \comp \gg \comp \ff  = \ff

427: \mbox{\quad and \quad}

428: \gg \comp \ff \comp \gg = \gg,$$

429: so every element in~$\GLL$ possesses an inverse as required for an inverse monoid---this applies in particular to $\ff=\gg=\emptyset$.

430: \end{proof}

431: 

432: As for the second result, the {\it equational variety} associated with a family~$\LLL$ of algebraic laws involving the signature~$\Sign$ is, by definition, the collection of all $\Sign$-structures that satisfy the laws of~$\LLL$. Different families of laws may give rise to the same variety: for instance, when appended to the commutativity law $xy = yx$, the associativity law $x(yz) = (xy)z$ and the law $x(yz) = z(yx)$ define the same variety. 

433: 

434: \begin{prop}

435: \cite{Dew}

436: Up to isomorphism, the monoid~$\GGLL$ only depends on the equational variety defined by~$\LLL$: if $\LLL$ and $\LLL'$ define the same variety, then the monoids $\GGLL$ and $\GGeo{\LLL'}$ are isomorphic.

437: \end{prop}

438: 

439: \begin{proof} [Sketch of proof]

440: It suffices to show that, when we add to a family~$\LLL$ a new law~$\LL$ that is a consequence of the laws of~$\LLL$, then the geometry monoid is not changed. Assume $\LL = (\tm, \tp)$. By Proposition~\ref{P:Basic}, the hypothesis that $\LL$ is a consequence of~$\LLL$ implies that some operator~$\ff$ in~$\GGLL$ maps~$\tm$ to~$\tp$. The geometry monoid~$\GGeo{\LLL \cup \{\LL\}}$ is obtained from~$\GGLL$ by adding a new generator that is a product of the canonical generators of~$\GGLL$, and, therefore, it is isomorphic to~$\GGLL$.

441: \end{proof}

442: 

443: \section{Replacing the geometry monoid with a group}

444:  \label{S:Group}

445: 

446: The first specific step that proves to be often useful in investigating the geometry monoids consists in replacing the monoid~$\GGLL$ with a {\it group}~$\GLL$ that resembles it. The benefit of the replacement is the possibility of freely computing with inverses and avoiding the problems possibly connected with the empty operator. However, there is no universal recipe for going from~$\GGLL$ to a (non-trivial) group, and we shall complete the approach in specific cases only, by guessing confluence relations in~$\GGLL$ and introducing the abstract group defined by these relations.

447: 

448: \subsection{The linear case}

449: \label{SS:Linear}

450: 

451: For each inverse monoid~$M$, there exists a biggest quotient of~$M$ that is a group, namely the {\it universal group~$U(M)$} of~$M$ obtained by collapsing all idempotents to~$1$~\cite{Pat}. When the geometry monoid~$\GGLL$ does not contain the empty operator, the idempotent elements are those operators that are identity on their domain, and the associated group keeps enough information to be non-trivial. We shall first briefly mention one case when this favourable situation occurs, namely the case of {\it linear} laws.

452: 

453: \begin{defi}

454: A term~$\tt$ is said to be {\it injective} if no variable occurs twice in~$\tt$. An algebraic law $\tm = \tp$ is said to be {\it linear} if it is balanced and, in addition, the terms~$\tm$ and~$\tp$ are injective.

455: \end{defi}

456: 

457: For instance, associativity and commutativity are linear laws, while self-distributi\-vity is not, as the variable~$\xx$ is repeated twice in the right hand term of $\xx(\yy\zz) = (\xx\yy)(\xx\zz)$.

458: 

459: In order to describe the case of linear laws, we start with a general result about the elements of a geometry monoid.

460: 

461: \begin{defi}

462: Assume that $\ff$ is an operator on~$\TS$. We say that a pair of terms~$(\tm, \tp)$ is a {\it seed} for~$\ff$ if $\ff$, as a set of pairs, consists of all instances of~$(\tm, \tp)$, \ie, consists of all pairs~$(\tm \subst, \tp \subst)$ with~$\subst$ a $\TS$-valued substitution.

463: \end{defi}

464: 

465: If $\LL$ is the law $\tm = \tp$, then $\OOOp\LL\ea$ consists of all instances of~$(\tm, \tp)$, so $(\tm, \tp)$ is a seed for~$\OOOp\LL\ea$. More generally we have:

466: 

467: \begin{lemm} \cite{Dgd}

468: \label{L:Seed}

469: Assume that $\LLL$ is a family of balanced algebraic laws involving a single binary operation symbol. Then each nonempty operator~$\ff$ in~$\GGLL$ admits a seed.

470: \end{lemm}

471: 

472: \begin{proof} [Sketch of proof]

473: First, every operator~$\OOOp\LL\a$ admits a seed, because, if $(\tm,\tp)$ is a seed for~$\OOOp\LL\ea$ and $\xx$ is a variable not occurring in~$\tm$ and~$\tp$, then, assuming that $\op$ is the operation symbol, $(\xx \op\tm,\xx\op\tp)$ is a seed for~$\OOOp\LL1$, $(\tm\op\xx,\tp\op\xx)$ is a seed for~$\OOOp\LL0$, and an easy induction gives the result for every~$\OOOp\LL\a$.

474: 

475: Then, by construction, every operator in~$\GGLL$ is a finite composition of operators~$\OOO\LL\a^\ee$ with~$\LL$ in~$\LLL$, and, by definition, the latter admit seeds. Hence, the point is to show that the composition of two operators admitting a seed still admits a seed provided it is nonempty. So, assume that $\ff$ and~$\gg$ consist of all instances of~$(\tm_1, \tp_1)$ and~$(\tm_2, \tp_2)$, respectively. Two cases may occur. Either there exists no term that is a substitute both of~$\tp_1$ and~$\tm_2$, and in this case $\ff \comp \gg$ is empty. Or there exists such a term. Then, as is well known \cite{Rob}, there exists a most general unifier (MGU) of the terms~$\tp_1$ and~$\tm_2$, \ie, there exist two substitutions~$\subst, \substt$ satisfying $\tp_1 \subst = \tm_2 \substt$ and such that every common substitute of~$\tp_1$ and~$\tm_2$ is a substitute of~$\tp_1 \subst$. In this case, it is easy to check that $(\tm_1 \subst, \tp_2 \substt)$ is a seed for~$\ff \comp \gg$.

476: \end{proof}

477: 

478: \begin{rema}

479: The restriction on the signature in Lemma~\ref{L:Seed} can be dropped at the expense of splitting the operators~$\OOOp\LL\a$ according to positions as explained in Remark~\ref{R:Position}, or, alternatively, of considering a more general notion of terms and instances in which substitution is possible not only for variables but also for some specific operation symbols considered as variables of a new type. Once again, there is no need to go into details here, as we shall not use such notions. 

480: \end{rema}

481: 

482: \begin{lemm}

483: Assume that $\LLL$ is a family of linear laws involving a single binary operation symbol. Then the seed of every operator in~$\GGLL$ is a pair of injective terms. Moreover, $\GGLL$ does not contain the empty operator.

484: \end{lemm}

485: 

486: \begin{proof}

487: The MGU of two injective terms always exists and it is an injective term: indeed, the only reason that may cause an unifier not to exist is a variable clash, and this cannot happen with injective terms. So the result about the seed follows from an induction. As for the empty operator, it cannot appear as the needed unifier always exists.

488: \end{proof}

489: 

490: \begin{defi}

491: \label{D:Sim}

492: Assume that $\ff, \gg$ are partial mappings on some set~$S$. We say that $\ff \sim \gg$ (\resp $\ff\approx\gg$) holds if there exists at least one

493: element~$\xx$ in~$S$ such that $\ff(\xx) = \gg(\xx)$ holds (\resp\ if $\ff(\xx) = \gg(\xx)$ holds for every~$\xx$ in the intersection of the domains of~$\ff$ and~$\gg$).

494: \end{defi}

495: 

496: When the geometry monoid~$\GGLL$ contains the empty operator, the relations~$\sim$ and~$\approx$ need not be transitive. This however cannot happen in the linear case:

497: 

498: \begin{prop} \cite{Dhb} \label{P:Group}

499: \label{P:Geom}

500: Assume that $\LLL$ is a family of linear laws. Then the relations~$\sim$ and~$\approx$ coincide, and they are congruences on the monoid~$\GGLL$. Furthermore, the quotient-monoid~$\GGLL/\!\approx$ is a group, and it is the universal group of~$\GGLL$.

501: \end{prop}

502: 

503: Under the previous hypotheses, we shall denote by~$\GLL$ the

504: group~$\GGLL/\!\approx$. So, in this case, we have a scheme of the form

505: \begin{equation}

506: \label{E:Quotient}

507: \begin{CD}

508: \WLL

509: @>{\mathrm{onto}}>>

510: \GGLL

511: @>{\mathrm{onto}}>>

512: \GLL.

513: \end{CD}

514: \end{equation}

515: Moreover, the partial action of~$\GGLL$ on terms induces a well-defined action of~$\GLL$ as, by definition, all operators in a $\approx$-class agree on the terms that lie in their domain. Furthermore, no information is lost when we replace~$\GGLL$ with~$\GLL$ in the precise sense that the counterpart of Proposition~\ref{P:Basic} is true: two terms~$\tt, \ttt$ are $\LLL$-equivalent if and only if we have $\ttt = \tt \act \gg$ for some~$\gg$ in~$\GLL$. So, in this case, one can replace the monoid~$\GGLL$ with the group~$\GLL$ in all further uses, and it is then natural to call the latter the {\it geometry group} of~$\LLL$.

516: 

517: \begin{exam}

518: Let $\Ass$ denote the associativity law $x(yz) = (xy)z$. Then the corresponding group~$\GA$ is a well known group, namely R.\,Thompson's group~$F$ \cite{Tho}. In the case of associativity together with commutativity, the corresponding group is R.\,Thompson's group~$V$---\cf~\cite{Dhb}. 

519: \end{exam}

520: 

521: \begin{rema}

522: Even in the smooth case of linear laws, the action of the group~$\GLL$ on terms is a partial action: for $\tt \act \gg$ to be defined, it is necessary that $\tt$ be large enough. However, we can obtain an everywhere defined action by considering infinite trees; equivalently, this amounts to defining an action on the boundary of the family of finite terms, which is a Cantor set in the case of terms involving one binary operation symbol and one variable.

523: \end{rema}

524: 

525: \subsection{Confluence relations: the principle}

526: 

527: Whenever the empty operator occurs in the geometry monoid, the previous approach badly fails:

528: 

529: \begin{lemm}

530: \label{L:Empty}

531: Assume that $\GGLL$ contains the empty operator. Then the universal group $U(\GGLL)$ is trivial, \ie, it reduces to $\{1\}$.

532: \end{lemm}

533: 

534: \begin{proof}

535: Assume that $\pi$ is a homomorphism of~$\GGLL$ to a group. Then, for each~$\ff$ in~$\GGLL$, we have $\emptyset \comp \ff = \emptyset$, hence $\pi(\ff) \pi(\emptyset) = \pi(\emptyset)$, whence $\pi(\ff) = 1$.

536: \end{proof}

537: 

538: \begin{exam}

539: \label{X:Empty}

540: The case when there is no unifier frequently occurs. For instance, in the case of the self-distributivity law~$(\LD)$, every term~$\tt$ belonging to the range of~$\SSp\ea$ satisfies $\sub\tt{00} = \sub\tt{10}$; it follows that every term~$\tt$ in the range of~$\SSp\ea \comp \SSp1$ satisfies $\sub\tt{00} = \sub\tt{100}$, and therefore $\sub\tt{00} \not= \sub\tt{10}$. Hence no term in the image of $\SSp\ea \comp \SSp1$ mays belong to the domain of~$\SSm\ea$: in other words, the composition of the operators $\SSp\ea$, $\SSp1$, and $\SSm\ea$ is empty, \ie, the operator $\SSp{} \comp \SSp1 \comp \SSm{}$, as a set of ordered pairs, is the empty set, and, in particular, its domain of definition is empty. In other words, we have in~$\GGeo\LD$---as well as in~$\GGeo\ALD$---the relation

541: $$\eev(\SSp\eaÊ\SSp1 \SSm\ea) = \emptyset.$$

542: This implies that {any} word~$\ww$ in~$\WW\LD$ containing $\SSp\ea \SSp1 \SSm\ea$ as a factor evaluates in~$\GGeo\LD$ into the empty operator. This is in particular the case for the symmetrized word $\SSp\ea  \SSp1 \SSm\ea \SSp\ea \SSm1 \SSm\ea$, although the latter appears as freely reducing to the empty word and one might therefore expect the associated operator to be close to the identity.

543: \end{exam}

544: 

545: 

546: The above situation almost always occurs when non-linear laws are involved. As the example of $(xy)(xz) = (xz)(xy)$ shows, it is not readily true that the presence of at least one non-linear law in~$\LLL$ forces the empty operator to belong to~$\GGLL$, but, for instance, it is sufficient for implementing the argument used in Example~\ref{X:Empty} that $\LLL$ contains a law $\tm = \tp$ such that, for some variable~$\xx$, the sets $\{\a_1, ..., \a_p\}$ and $\{\b_1, ..., \b_q\}$ where~$\xx$ respectively occurs in~$\tm$ and~$\tp$ are distinct and at least one of them is not a singleton.

547: 

548: In such cases, the universal group~$U(\GGLL)$ is of no use, and we have to look for another method. A misleading attempt would be to try to modify the construction of the geometry monoid so as to artificially discard the empty operator. We doubt that anything interesting can occur by doing so---see \cite{Dgd} for a more thorough discussion. Instead, we shall now develop a completely different method for associating with~$\GGLL$ a group that keeps the meaningful information of~$\GGLL$, namely finding a presentation of~$\GGLL$ and introducing the group that admits this presentation---whatever its connection with~$\GGLL$ is.

549: 

550: Actually, finding a presentation of~$\GGLL$ is in general out of reach, at least by a direct approach. So, once again, we use an indirect approach consisting in isolating {\it some} relations satisfied in~$\GGLL$ using a uniform scheme, but not trying to prove that these relations make a presentation: the latter will possibly come at the very end when further constructions have been performed.

551: 

552: So, at this point, the problem is to find relations connecting the various operators~$\OOO\LL\a^\ee$ of~$\GGLL$. In the sequel, we shall concentrate  on {\it positive} relations, \ie, on relations that involve the operators~$\OOp\a$ but not their inverses.

553: 

554: \begin{defi}

555: For~$\LLL$ a family of oriented algebraic laws, we denote by~$\RLLp$ the rewrite system comprising the rules $\tm \to \tp$ for $(\tm, \tp)$ in~$\LLL$; the {\it positive geometry monoid}~$\GGLLp$ of~$\LLL$ is defined to be the submonoid of~$\GGLL$ generated by all operators~$\OOOp\LL\a$ with~$\LL$ in~$\LLL$ and~$\a$ in~$\{0,1\}^*$.

556: \end{defi}

557: 

558: The connection between the rewrite system~$\RLLp$ and the positive geometry monoid~$\GGLLp$ is similar to the connection between the rewrite system~$\RLL$ and the geometry monoid~$\GGLL$. We shall be looking for relations in~$\GGLLp$, \ie, for relations connecting the operators~$\OOp\a$ in~$\GGLLp$. The principle will be to investigate the relations that possibly arise when two operators are applied to one and the same term~$\tt$, which amounts to inverstigating the local confluence of the rewrite system~$\RLLp$. This means that, for all laws~$\LL, \LLbis$ in~$\LLL$ and all addresses~$\a, \b$, we look for relations of the generic form

559: \begin{equation}

560: \label{E:Conf}

561: \OOp\a \comp ... = \OObisp\b \comp ...

562: \end{equation}

563: In other words, we look for common right multiples in~$\GGLLp$.

564: 

565: \begin{defi}

566: For $\ff$ a (partial) mapping on~$\TS$ and $\a$ an address, we denote by~$\ssh\a(\ff)$ the {\it $\a$-shift} of~$\ff$, defined to be the partial operator on~$\TS$ that consists in applying~$\ff$ to the $\a$th subterm of its argument: $\tt \act \ssh\a(\ff)$ is defined if and only if $\sub\tt\a$ exists and $\sub\tt\a \act \ff$ is defined, and, in this case, $\tt \act \ssh\a(\ff)$ is obtained from~$\tt$ bt replacing the $\a$th subterm by its image under~$\ff$.

567: \end{defi}

568: 

569: So, for instance, we have $\OOOp\LL\a = \ssh\a(\OOOp\LL\ea)$ for each law~$\LL$ and each address~$\a$, and, more generally, $\OOOp\LL{\a\b} = \ssh\a(\OOOp\LL\b)$ for all~$\a, \b$.

570: 

571: As for confluence relations in the monoid~$\GGLLp$, two general schemes will be involved. The first one relies on the following general principle: 

572: 

573: \begin{lemm}

574: Assume that $\a$ and $\b$ are incomparable addresses, \ie, there exists

575: $\g$ such that $\g0$ is a prefix of~$\a$ and $\g1$ is a prefix of~$\b$,

576: or vice versa. Then, for all partial operators~$\ff, \gg$, we have

577: \begin{equation}

578: \label{E:Comm0}

579: \ssh\a(\ff) \comp \ssh\b(\gg) = \ssh\b(\gg) \comp \ssh\a(\ff).

580: \end{equation}

581: \end{lemm}

582: 

583: \begin{proof}

584: (Figure~\ref{F:Ortho}) 

585: The operators~$\ssh\a(\ff)$ and~$\ssh\b(\gg)$ act on disjoint

586: subtrees, and therefore they commute. 

587: \end{proof}

588: 

589: \begin{figure} [htb]

590: \begin{picture}(40,40)

591: \put(0,0){\includegraphics{Ortho.eps}}

592: \put(10,12){$\a$}

593: \put(24,14){$\b$}

594: \put(17,27){$\g$}

595: \put(13.5,23.5){$\g0$}

596: \put(23.5,23.5){$\g1$}

597: \end{picture}

598: \caption{\smaller Incomparable addresses: The $\a$th and $\b$th subterms are disjoint, and therefore operators acting on them commute.}

599: \label{F:Ortho}

600: \end{figure}

601: 

602: In particular, we deduce:

603: 

604: \begin{prop}

605: Assume that $\a$ and $\b$ are incomparable addresses, \ie, there exists

606: $\g$ such that $\g0$ is a prefix of~$\a$ and $\g1$ is a prefix of~$\b$,

607: or conversely. Then we have

608: \begin{equation}

609: \label{E:Comm}

610: \OOp\a \comp \OObisp\b = \OObisp\b \comp \OOp\a.

611: \end{equation}

612: \end{prop}

613: 

614: The second general scheme appears in connection with what can be called

615: a {\it geometric inheritance} phenomenon.

616: 

617: \begin{lemm}

618: \label{L:Conf}

619: Assume that $\LL$ is the oriented law $(\tm, \tp)$ and that some variable~$\xx$ occurs at addresses $\b_1, ..., \b_p$ in~$\tm$ and at $\g_1, ..., \g_q$ in~$\tp$. Then, for each (partial) operator~$\ff$ acting on terms, we have

620: \begin{equation}

621: \label{E:Heir0}

622: \ssh{\b_1}(\ff) \comp ... \comp \ssh{\b_p}(\ff) \comp

623: \OOp\ea =

624: \OOp\ea \comp \ssh{\g_1}(\ff) \comp ... \comp

625: \ssh{\g_q}(\ff).

626: \end{equation}

627: More generally, for each address~$\a$, we have

628: \begin{equation}

629: \label{E:Heir1}

630: \ssh{\a\b_1}(\ff) \comp ... \comp \ssh{\a\b_p}(\ff) \comp

631: \OOp\a =

632: \OOp\a \comp \ssh{\a\g_1}(\ff) \comp ... \comp

633: \ssh{\a\g_q}(\ff).

634: \end{equation}

635: \end{lemm}

636: 

637: \begin{proof}

638: (Figure~\ref{F:Heir})

639: Assume that $\OOp\ea$ maps~$\tt$ to~$\ttt$. This means that there exists a substitution~$\subst$ such that $\tt$ is~$\tm \subst$ and $\ttt$ is~$\tp \subst$. Let~$\subst_1$ be the substitution defined by $\yy\subst_1 = \yy \subst$ for $\yy \not= \xx$, and $\xx \subst_1 = \xx \subst \ff$. Let $\tt_1 := \tm \subst_1$ and $\ttt_1:= \tp \subst_1$. Then, by construction, $\OOp{}$ maps~$\tt_1$ to~$\ttt_1$. Now, $\tt_1$ is obtained from~$\tt$ by replacing the subterms at addresses $\b_1$, ..., $\b_p$ with their image under~$\ff$, so we have

640: $$\tt_1 = \tt \act (\ssh{\b_1}(\ff) \comp ... \comp \ssh{\b_p}(\ff)).$$

641: Similarly, $\ttt_1$ is obtained from~$\ttt$ by replacing the subterms at addresses $\g_1$, ..., $\g_q$ with their image under~$\ff$, so we have

642: $$\ttt_1 = \ttt \act (\ssh{\g_1}(\ff) \comp ... \comp \ssh{\g_q}(\ff)),$$

643: and \eqref{E:Heir0} follows.

644: 

645: Relation~\eqref{E:Heir1} is deduced by applying~$\ssh\a$ to both terms of~\eqref{E:Heir0}.

646: \end{proof}

647: 

648: \begin{figure} [htb]

649: \begin{picture}(62,42)(0,-3)

650: \put(0,0){\includegraphics{Heir.eps}}

651: \put(0,0){\includegraphics{Heir.eps}}

652: \put(7,27){$\xx$}

653: \put(7,32){$\b_1$}

654: \put(17.5,32){$\b_p$}

655: \put(36.5,34){$\g_1$}

656: \put(57.5,30){$\g_q$}

657: \put(17,27){$\xx$}

658: \put(37,29){$\xx$}

659: \put(52,26){$\xx$}

660: \put(57,25){$\xx$}

661: \put(12,40){$\tm$}

662: \put(50,40){$\tp$}

663: \put(27,34){$\to$}

664: \put(27,15){$\to$}

665: \put(12,20){$\tm \subst$}

666: \put(50,20){$\tp \subst$}

667: \put(6,-0.5){$\xx \subst$}

668: \put(16,-0.5){$\xx \subst$}

669: \put(36,1.5){$\xx \subst$}

670: \put(51,-1.5){$\xx \subst$}

671: \put(56,-2.5){$\xx \subst$}

672: \put(7,12){$\b_1$}

673: \put(17.5,12){$\b_p$}

674: \put(36.5,14){$\g_1$}

675: \put(57.5,10){$\g_q$}

676: \end{picture}

677: \caption{\smaller Inheritance phenomenon: If the variable~$\xx$ occurs at~$\b_1, ..., \b_p$ in~$\tm$ and at $\g_1, ..., \g_q$ in~$\tp$ and nowhere else, then, for each term~$\tm\subst$, the subterm~$\xx\subst$ occurs at $\b_1, ..., \b_p$ in~$\tm\subst$, and t $\g_1, ..., \g_q$ in~$\tp\subst$, and applying~$\ff$ in each $\xx\subst$ before or after applying $\tm \to \tp$ leads to the same result.}

678: \label{F:Heir}

679: \end{figure}

680: 

681: By applying Lemma~\ref{L:Conf} to the case when the operator~$\ff$ has the form~$\OObisp\d$, we obtain:

682: 

683: \begin{prop}

684: Assume that $\LL$ is the oriented law $(\tm, \tp)$ and that some variable~$\xx$ occurs at addresses $\b_1, ...\b_p$ in~$\tm$ and at $\g_1, ..., \g_q$ in~$\tp$. Then, for all addresses~$\a, \d$ and each law~$\LLbis$, we have

685: \begin{equation}

686: \label{E:Heir}

687: \OOp\a \comp \OObisp{\a\g_1\d} \comp ... \comp

688: \OObisp{\a\g_q\d} =

689: \OObisp{\a\b_1\d} \comp ... \comp \OObisp{\a\b_p\d} \comp

690: \OOp\a.

691: \end{equation}

692: \end{prop}

693: 

694: In general, the previous two general schemes do not exhaust all possible confluence relations in~$\GGLL$. Typically, no relation is obtained for pairs of the form $(\a, \a\b)$ where $\b$ is so short that it falls inside the terms~$\tm$ or~$\tp$ associated with the considered law. In this case, no general scheme is known, and one has to look at the specific terms in order to find possible confluence relations.

695: 

696: \subsection{Confluence relations: the example of $\ALD$}

697: \label{SS:ConfALD}

698: 

699: We illustrate the previous scheme on the case of~$\ALD$. The first family of confluence relations comprises the trivial commutation relations, here all relations

700: \begin{equation}

701: \label{E:ALDComm}

702: \XX\a \comp \YY\b = \YY\b \comp \XX\a

703: \mbox{\quad for $\XX{}, \YY{} = \SS{}, \AA{}$ and $\a, \b$ incomparable}.

704: \end{equation}

705: The second family of confluence relations comprises the geometric inheritance relations. As for the laws~$\LD$ and~$\ALDi$, \ie, for the operator~$\SS{}$, three variables are involved in the rule 

706: \begin{equation}

707: \label{E:Sigma}

708: x \op (y \Op z) \to (x \op y) \Op (x \op z).

709: \end{equation}

710: The variable~$x$ occurs at address~$0$ on the LHS of~\eqref{E:Sigma}, while it occurs at~$00$ and~$10$ on the RHS. So Relation~\eqref{E:Heir} is here

711: \begin{equation}

712: \label{E:ALDHeir1}

713: \SSp\a \comp \XXp{\a0\d} = \XXp{\a00\d} \comp \XXp{\a10\d} \comp \SSp\a

714: \end{equation}

715: for $\XX{} = \SS{}, \AA{}$. Similarly, the variable~$y$ occurs at~$10$ on the LHS of~\eqref{E:Sigma}, and at~$01$ on the RHS, while the variable~$z$ occurs at~$11$ on both sides. Thus  Relations~\eqref{E:Heir} become

716: \begin{gather}

717: \label{E:ALDHeir2}

718: \SSp\a \comp \XXp{\a10\d} = \XXp{\a01\d} \comp \SSp\a, \\

719: \label{E:ALDHeir3}

720: \SSp\a \comp \XXp{\a11\d} = \XXp{\a11\d} \comp \SSp\a

721: \mbox{\quad for $\XX{} = \SS\ea, \AA\ea$}.

722: \end{gather}

723: The treatment is analogous for the law~$\ALDii$, \ie, for the operator~$\AA{}$. Three

724: variables occur in the rule

725: \begin{equation}

726: \label{E:A}

727: x \op (y \op z) \to (x \OP y) \op z.

728: \end{equation}

729: The variable~$x$ occurs at~$0$ on the LHS of~\eqref{E:A}, and at~$00$ on the RHS; $y$ occurs at~$10$ and at~$01$ respectively; finally, $z$ occurs at~$11$ and at~$1$. The corresponding Relations~\eqref{E:Heir} are

730: \begin{gather}

731: \label{E:ALDHeir4}

732: \AAp\a \comp \XXp{\a0\d} = \XXp{\a00\d} \comp \AAp\a, \\

733: \label{E:ALDHeir5}

734: \AAp\a \comp \XXp{\a10\d} = \XXp{\a01\d} \comp \AAp\a, \\

735: \label{E:ALDHeir6}

736: \AAp\a \comp \XXp{\a11\d} = \XXp{\a1\d} \comp \AAp\a,

737: \end{gather}

738: again for $\XX{} = \SS{}, \AA{}$. 

739: 

740: With the previous approach, we succeeded in finding one relation of type~\eqref{E:Conf} for all pairs~$\a, \b$, with the exception of the pairs $\{\AAp\a, \SSp\a\}$, as well as all pairs $\{\XXp\a, \YYp{\a1}\}$. So the question is whether we can find in~$\GGALDp$ relations of the form

741: \begin{equation*}

742: \XX\a \comp ... = \YY{\a} \comp ... 

743: \mbox{\quad and\quad}

744: \XX\a \comp ... = \YY{\a1} \comp ... 

745: \end{equation*}

746: when $(\XX{}, \YY{})$ ranges over the various combinations of~$\SS{}$ and~$\AA{}$. As shown in Figure~\ref{F:Crit}, there exist such relations, namely

747: \begin{gather}

748: \label{E:ALDCrit1}

749: \SSp\a \comp \SSp{\a1} \comp \SSp\a = 

750: \SSp{\a1} \comp \SSp\a \comp \SSp{\a1} \comp \SSp{\a0}, \\

751: \label{E:ALDCrit2}

752: \SSp\a \comp \SSp{\a1} \comp \AAp\a 

753: = \AAp{\a1} \comp \SSp\a \comp

754: \SS{\a0},\\

755: \label{E:ALDCrit3}

756: \AAp{\a} \comp \SSp{\a} = \SSp{\a1} \comp \SSp{\a} \comp \AAp{\a1} \comp \AAp{\a0}.

757: \end{gather}

758: 

759: \begin{figure} [htb]

760: \begin{picture}(74,48)

761: \put(0,0){\includegraphics[scale=0.6]{Crit1.eps}}

762: \put(7,23){$\SSp1$}

763: \put(67,23){$\SSp\ea$}

764: \put(19,43){$\SSp\ea$}

765: \put(48,43){$\SSp1$}

766: \put(19,13){$\SSp\ea$}

767: \put(45,13){$\SSp1\SSp0$}

768: \end{picture}

769: 

770: \begin{picture}(74,50)

771: \put(0,0){\includegraphics[scale=0.6]{Crit2.eps}}

772: \put(7,23){$\AAp1$}

773: \put(67,23){$\AAp\ea$}

774: \put(19,43){$\SSp\ea$}

775: \put(48,43){$\SSp1$}

776: \put(19,13){$\SSp\ea$}

777: \put(48,13){$\SSp0$}

778: \end{picture}

779: 

780: \begin{picture}(74,50)

781: \put(0,0){\includegraphics[scale=0.6]{Crit3.eps}}

782: \put(7,23){$\SSp1$}

783: \put(67,23){$\SSp\ea$}

784: \put(34,43){$\AAp\ea$}

785: \put(19,13){$\SSp\ea$}

786: \put(45,13){$\AAp1\AAp0$}

787: \end{picture}

788: \caption{\smaller Three more types of confluence relations in $\GGALD$: here $\Op$ stands for both~$\op$ or~$\OP$, the numbers stand for the indices of the variables.}

789: \label{F:Crit}

790: \end{figure}

791: 

792: Notice that all cases are not covered: there is {\it no} relation  $\AAp{\a} ... = \SSp{\a} ...$, 

793: or $\AAp{\a} ... = \AAp{\a1} ...$ in the list above.

794: 

795: \subsection{The geometry group}

796: 

797: According to the principle considered above, we introduce the abstract group for which the confluence relations of~$\GGLL$ make a presentation.

798: 

799: \begin{defi}

800: \label{D:GLL}

801: For~$\LLL$ a family of oriented algebraic laws, we define the {\it geometry group}~$\GLL$ of~$\LLL$ to be the group generated by formal copies of the operators~$\OOp\a$ for~$\LL$ in~$\LLL$, subject to all confluence relations connecting these operators in the monoid~$\GGLLp$. We denote by~$\ev$ the canonical evaluation morphism of~$\WLL$ onto~$\GLL$.

802: \end{defi}

803: 

804: \begin{exam}

805: In the case of the $\ALD$-laws, the group $\GALD$ is, by definition, a group generated by two infinite series of generators $\SS\a$ and $\AA\a$ indexed by finite sequences of~$0$'s and~$1$'s, subject to the relations~\eqref{E:ALDComm}, \eqref{E:ALDHeir1}, \eqref{E:ALDHeir2}, \eqref{E:ALDHeir3}, \eqref{E:ALDCrit1}, \eqref{E:ALDCrit2}, and \eqref{E:ALDCrit3}.

806: \end{exam}

807: 

808: \begin{exam}

809: Let us come back to the (linear) associativity law~$\Ass$. One easily checks that, for each pair of addresses $\a, \b$, there exists a natural confluence relation of the form $\AAp\a \comp ... = \AAp\b \comp ...$ in the positive monoid~$\GGAp$. Indeed, besides the quasi-commutativity inheritance relations

810: $$\AAp\a \comp \AAp{\a0\d} = \AAp{\a00\d} \comp \AAp\a, \quad

811: \AAp\a \comp \AAp{\a10\d} = \AAp{\a01\d} \comp \AAp\a, \quad

812: \AAp\a \comp \AAp{\a11\d} = \AAp{\a1\d} \comp \AAp\a,$$

813: the only missing pairs are the pairs $\a, \a1$, and the famous MacLane--Stasheff pentagon equality~\ref{Mac}

814: $$\AAp\a \comp \AAp\a = \AAp{\a1} \comp \AAp\a \comp \AAp{\a1}$$

815: completes the picture. Then the group~$\GA$ presented by the above relations coincides with the group $\GGA/\!\!\approx$ of Proposition~\ref{P:Geom}, \ie, with R.\,Thompson's group~$F$ \cite{Dfg}: so, in this case, the method based on presentation by confluence relations subsumes that of Section~\ref{SS:Linear}.

816: \end{exam}

817: 

818: When confluence relations are used to introduce the group~$\GLL$, the connection between the monoid~$\GGLL$ and the group~$\GLL$ is not obvious. Indeed, instead of the sequence of~\eqref{E:Quotient}, the scheme is now

819: \begin{equation}

820: \label{E:QuotientBis}

821: \begin{CD}

822: \WLL

823: @>{\mathrm{onto}}>{\eev}>

824: \GGLL\\

825: @V{\mathrm{onto}}V{\ev}V\\

826: \GLL

827: \end{CD}

828: \end{equation}

829: and it is not clear whether any factorization connects~$\GGLL$ and~$\GLL$. In order to prove that there exists a morphism from~$\GGLL$ to~$\GLL$, we ought to know that the selected confluence relations exhaust all relations holding in~$\GGLL$---which cannot be the case if the empty operator occurs. And, in order to prove that there exists a morphism from~$\GLL$ to~$\GGLL$, we ought to be able to control the pairs $\OOOp\LL\a \comp \OOOm\LL\a$ in~$\GGLL$. Precisely, assume that $\ww, \ww'$ are words in~$\WLL$ that satisfy $\ev(\ww) = \ev(\ww')$, \ie, that represent the same element of~$\GLL$. This means that there exists a finite sequence of words~$\ww = \ww_0, \ww_1, ..., \ww_n = \ww'$ such that each~$\ww_i$ is obtained from the previous one either by applying one of the confluence relation, or by deleting some subfactor $\OOO\LL\a \OOO\LL\a\inv$ or $\OOO\LL\a\inv \OOO\LL\a$, or by inserting such a subfactor. In the first two cases, the associated operators are equal, but, in the third case, the associated operators need not be equal, and, in particular, the empty operator may appear. So we cannot deduce from the fact that $\ww, \ww'$ represent the same element in~$\GLL$ the fact that they represent the same element in~$\GGLL$. However, and this is an important point, even if we cannot directly compare~$\GGLL$ and~$\GLL$, we can use 

830: the properties of~$\GGLL$ as a sort of oracle for guessing properties of~$\GLL$, and then try to find a direct proof for the results so conjectured.

831: 

832: \section{Internalization of terms}

833: \label{S:Blue}

834: 

835: At this point, we have have associated a monoid~$\GGLL$, and in some cases a group~$\GLL$, with each family of algebraic laws~$\LLL$. By construction, there is a partial action of the monoid~$\GGLL$ on terms, and similarly, at least in the case of linear laws, a partial action of the group~$\GLL$ on terms. The next step consists in trying to carry terms inside the monoid~$\GGLL$ and/or the group~$\GLL$, so as to replace the external action of the monoid or the group on terms by an internal operation, typically a multiplication in good cases. Once again, we have no general solution, but we explain how to complete the construction in good cases, and specifically in the case of the $\ALD$-laws.

836: 

837: \subsection{Blueprint of a term: the principle}

838: \label{SS:Blue1}

839: 

840: A priori, terms and operators of the geometry monoid live in disjoint worlds: the only connection is that operators act on terms. The principle we shall apply in the sequel---and which turns out to be efficient in good cases---consists in building inside the geometry monoid~$\GGLL$, and simultaneously inside the geometry group~$\GLL$ that mimicks its algebraic properties, a copy of each term, so that the action of operators on terms translates into a simple operation inside~$\GGLL$ and~$\GLL$, typically a multiplication. This copy of a term~$\tt$ in~$\GLL$ will be called the {\it blueprint} of~$\tt$.

841: 

842: We recall that, for~$\Sign$ a list of operation symbols, $\TS$ denotes the family of all terms constructed using the operations of~$\Sign$ and variables from an infinite list~$\Var$. In the sequel, we assume that $\xx$ is a fixed element of~$\Var$, and use $\TSx$ for the family of all terms constructined using the operations of~$\Sign$ and the single variable~$\xx$.

843: 

844: The general principle is as follows. Assume that $\LLL$ is a family of algebraic laws involving the signature~$\Sign$, and we have an injective map (``carbon copy'')

845: \begin{equation}

846: \IInt: \TSx \to \GGLL,

847: \end{equation}

848: \ie, a representation of terms inside the geometry monoid~$\GGLL$. If $\tt, \ttt$ are $\LLL$-equivalent terms, \ie, by Proposition~\ref{P:Basic}, if some element~$\ff$ of~$\GGLL$ maps~$\tt$ to~$\ttt$, there must exist some relation between the copies~$\IInt(\tt)$ and~$\IInt(\ttt)$. We shall be interested in the case when this relation takes the form

849: \begin{equation}

850: \label{E:Blue1}

851: \IInt(\tt \act \ff) \sim \IInt(\tt) \comp \varphi(\ff)

852: \end{equation}

853: where $\varphi$ is some endomorphism of~$\GGLL$, \ie, when the action of~$\GGLL$ on terms becomes a right multiplication twisted by endomorphism at the level of the copies---optimally, we might hope for an equality in~\eqref{E:Blue1}, but the problem of the empty operator makes a true equality impossible in most cases: this is precisely why we shall subsequently resort to the group~$\GLL$. We recall that $\WLL$ denotes the family of all abstract words in the letters~$\OOO\LL\a^{\pm1}$ for~$\LL$ in~$\LLL$ and~$\a$ an address. By construction, every operator in~$\GGLL$ is a finite product of elementary operators~$\OOO\LL\a^{\pm}$, so it can be expressed as $\eev(\ww)$ where $\ww$ is a word in~$\WLL$, and \eqref{E:Blue1} can be restated as

854: \begin{equation}

855: \label{E:Blue2}

856: \IInt(\tt \act \eev(\ww)) \sim \IInt(\tt) \comp \varphi(\eev(\ww))),

857: \end{equation}

858: for~$\tt$ in~$\TSx$ and $\ww$ in~$\WLL$ such that $\tt \act \eev(\ww)$ is defined.

859: 

860: Now, according to the general principle of Section~\ref{S:Group}, we wish to replace the monoid~$\GGLL$ with the group~$\GLL$. If the construction of the mapping~$\IInt$ is explicit enough, we can mimick it in the group~$\GLL$, thus defining a similar (hopefully injective) mapping

861: \begin{equation}

862: \Int: \TSx \to \GLL

863: \end{equation}

864: and use $\Int(\tt)$ as a copy of~$\tt$ inside~$\GLL$. If $\GLL$ resembles~$\GGLL$ enough, we may hope that the counterpart of~\eqref{E:Blue2} holds in~$\GLL$, so that we can carry the action of~$\GGLL$ on terms inside the group~$\GLL$. We are thus led to the following notion:

865: 

866: \begin{defi}

867: \label{D:Blue}

868: Assume that $\LLL$ is a family of oriented algebraic laws involving the signature~$\Sign$, and that $\phi$ is an endomorphism of~$\GLL$. A mapping $\Int: \TSx \to \GLL$ is said to be a {\it $\phi$-blueprint} if the relation

869: \begin{equation}

870: \label{E:Constr}

871: \Int(\tt \act \eev(\ww)) = \Int(\tt) \cdot \phi(\ev(\ww))

872: \end{equation}

873: holds in~$\GLL$ for every term~$\tt$ and every word~$\ww$ in~$\WLL$ such that $\tt \act \eev(\ww)$ is defined. 

874: \end{defi}

875: 

876: Thus, a $\phi$-blueprint transforms the operation of applying the laws of~$\LLL$ into a multiplication twisted by~$\phi$ in the group~$\GLL$. The interest of a $\phi$-blueprint will be discussed in Section~\ref{S:Using} below. The general idea is that it allows for carrying the problems about $\LLL$-equivalence inside the presented group~$\GLL$, and therefore may lead to solutions when the latter is under control. Typically, carrying the relation~$\EQ\LLL$ to~$\GLL$ using the map~$\Int$ supposed to be injective yields a new equivalence relation inside~$\GLL$ that may be more easily controlled than~$\EQ\LLL$ itself. 

877: 

878: \begin{rema}

879: A constant mapping provides a blueprint, certainly a trivial and uninteresting one. In the sequel, we are mainly interested in blueprints that are injective or close to, but we shall see that, in certain cases like that of~$\ALD$, even a blueprint that is not proved to be injective may be useful. That is why we do not require injectivity in Definition~\ref{D:Blue}.

880: \end{rema}

881: 

882: \subsection{Blueprint of a term: the example of~$\ALD$}

883: 

884: In order to realize the approach sketched above, \ie, to construct a blueprint, in the case of the~$\ALD$-laws, the first step consists in representing terms in~$\GGLL$, \ie, in selecting for each term~$\tt$ a certain operator~$\IInt(\tt)$ in the geometry monoid~$\GGLL$ that in some sense characterizes~$\tt$. A general idea is to choose an operator that {\it constructs}~$\tt$ starting from some fixed absolute startpoint. This procedure heavily depends on the specific algebraic laws we are investigating, here~$\ALD$. We use $\Tox$ for the family of all well-formed terms involving two binary operators~$\op, \OP$ and the single variable~$\xx$.

885: 

886: The solution we develop relies on some specific property of the $\ALD$-laws, namely the existence of an {\it absorption} phenomenon. To decribe this phenomenon, let us define {\it right vines} to be those terms of~$\Tox$ inductively specificed by

887: \begin{equation} \label{E:Vine}

888: \xx^{[n]} := \begin{cases}

889: \xx&\mbox{for $n = 1$}, \\

890: \xx \op \xx^{[n-1]}

891: &\mbox{for $n \ge 2$}.

892: \end{cases}

893: \end{equation}

894: The associated trees are ``all to the right'' trees. The following result expresses that, in presence of the laws of~$\ALD$, every term~$\tt$ of~$\Tox$ is absorbed by all sufficiently large right vines.

895: 

896: \begin{lemm} [absorption lemma]

897: \label{L:Absorption}

898: For each term~$\tt$ in~$\Tox$, there exists a positive integer~$p$ such that 

899: \begin{equation} \label{E:Absorption}

900: \xx^{[n]} \EQ\ALD \tt \op \xx^{[n-p]}

901: \mbox{\qquad holds for $n$ large enough}.

902: \end{equation}

903: \end{lemm}

904: 

905: \begin{proof}

906: The property is true with $p = 1$ for~$\tt = \xx$ and $n \ge 2$ (in which case the equivalence is an equality), so, in order to establish it for every term in~$\Tox$, it

907: is enough to show that, if

908: \eqref{E:Absorption} holds for~$\tti$

909: and~$\ttii$, then it holds for

910: $\tti \op \ttii$ and for $\tti \OP \ttii$ as

911: well. So assume $\xx^{[n]} \EQ\ALD \tti \op

912: \xx^{[n-p_1]}$ for $n \ge m_1$ and

913: $\xx^{[n]} \EQ\ALD \ttii

914: \op \xx^{[n-p_2]}$ for $n \ge m_2$. We

915: obtain for $n \ge

916: \max(m_1+p_2, m_2+p_1)$

917: \begin{align*}

918: \xx^{[n]}

919: &\EQ\ALD \tti \op \xx^{[n-p_1]} 

920: &\mbox{by hypothesis,}\\

921: &\EQ\ALD \tti \op (\ttii \op \xx^{[n-p_1 -p_2]}) 

922: &\mbox{by hypothesis,}\\

923: &\EQ\ALD (\tti \op \ttii) \op (\tti \op \xx^{[n-p_1 -p_2]}) 

924: &\mbox{by $\LD$,}\\

925: &\EQ\ALD (\tti \op \ttii) \op \xx^{[n-p_2]} 

926: &\mbox{by hypothesis.}

927: \end{align*}

928: Similarly, we have for $n \ge \max(m_1,

929: m_2+p_1)$

930: \begin{align*}

931: \xx^{[n]}

932: &\EQ\ALD \tti \op \xx^{[n-p_1]} 

933: &\mbox{by hypothesis,}\\

934: &\EQ\ALD \tti \op (\ttii \op \xx^{[n-p_1 -p_2]}) 

935: &\mbox{by hypothesis,}\\

936: &\EQ\ALD (\tti \OP \ttii) \op \xx^{[n-p_1 -p_2]}

937: &\mbox{by $\ALDii$,}

938: \end{align*}

939: so the induction is completed.

940: \end{proof}

941: 

942: By Proposition~\ref{P:Basic}, the equivalence of~\eqref{E:Absorption} must be witnessed for by some operator of the geometry monoid~$\GGALD$: for each term~$\tt$ in~$\Tox$ and every integer~$n$, there must exist an operator~$\IInt(\tt)$ in~$\GGALD$, hence a composition of operators~$\SS\a^\pm$ and~$\AA\a^\pm$, that maps~$\xx^{[n]}$ to $\tt \op \xx^{[n-p]}$. Actually, the inductive proof of Lemma~\ref{L:Absorption} gives not only the existence of such a witness, but only an inductive construction for such a witness.

943: 

944: \begin{lemm} \label{L:Translation}

945: For~$\tt$ in~$\Tox$, inductively define $\IInt(\tt)$ in~$\GGALD$ by

946: \begin{equation}

947: \IInt(\tt) = 

948: \begin{cases}

949: \id 

950: & \mbox{for $\tt = \xx$,}\\

951: \IInt(\tti) \comp \ssh1(\IInt(\ttii)) \comp \SSp\ea \comp \ssh1(\IInt(\tti))\inv 

952: &\mbox{for $\tt = \tti \op \ttii$,}\\

953: \IInt(\tti) \comp \ssh1(\IInt(\ttii)) \comp \AAp\ea  

954: &\mbox{for $\tt = \tti \OP \ttii$}.

955: \end{cases}

956: \end{equation}

957: Then, for every term~$\tt$ in~$\Tox$, there exists~$p$ such that, for every~$n$ large enough, we have

958: \begin{equation}

959: \label{E:Blue}

960: \IInt(\tt) : \xx^{[n]} \mapsto \tt \op \xx^{[n-p]}.

961: \end{equation}

962: \end{lemm}

963: 

964: \begin{proof}

965: The formulas of~\eqref{E:NNewop} are a mere translation of the successive equivalence steps in the proof of Lemma~\ref{L:Absorption}, and the result is then a straightforward verification.

966: \end{proof}

967: 

968: Note that \eqref{E:Blue} guarantees that the mapping~$\IInt$ is injective, since the term~$\tt$ can be recovered from the operator~$\IInt(\tt)$. So it is coherent to use the operator~$\IInt(\tt)$ as a counterpart of the term~$\tt$ inside the geometry monoid~$\GGALD$. According to the general scheme of Section~\ref{SS:Blue1}, we shall now analyse the counterpart of the action of~$\GGLL$ on terms. 

969: 

970: \begin{lemm}

971: \label{L:Action}

972: For each term~$\tt$ in~$\Tox$ and each operator~$\ff$ in~$\GGALD$ such that $\tt \act \ff$ is defined, we have

973: \begin{equation}

974: \label{E:AAction}

975: \IInt(\tt \act \ff) \sim \IInt(\tt) \comp \ssh0(\ff).

976: \end{equation}

977: \end{lemm}

978: 

979: \begin{proof}

980: Let $\ttt = \tt \act \ff$. Then, for each term~$\tti$, the operator~$\sh0(\ff)$ maps the term~$\tt \op \tti$ to~$\ttt \op \tti$---and, similarly, $\tt \OP \tti$ to $(\tt \act \ff) \OP \tti$. So, in particular, $\sh0(\ff)$ maps~$\tt \op \xx^{[n]}$ to~$\ttt \op \xx^{[n]}$ for each~$n$. Now, by Lemma~\ref{L:Translation} (and for~$n$ large enough), the operator~$\IInt(\tt)$ maps~$\xx^{[n]}$ to~$\tt \op \xx^{[n-p]}$, while $\IInt(\ttt)$ maps~$\xx^{[n]}$ to~$\ttt \op \xx^{[n - p']}$ for some~$p'$. This means that both $\IInt(\tt) \comp \sh0(\ff)$ and $\IInt(\ttt)$ map~$\xx^{[n]}$ to~$\ttt \op \xx^{[n-p']}$. Hence, in the monoid~$\GGALD$, the two operators $\IInt(\tt) \comp \sh0(\ff)$ and $\IInt(\ttt)$ agree on at least one term, namely~$\tt$, which, by definition, means that \eqref{E:AAction} holds.

981: \end{proof}

982: 

983: We thus obtained in the case of~$\ALD$ a relation of the form~\eqref{E:Blue1}, the involved endormorphism of~$\GGALD$ being~$\ssh0$. Expressed on the shape of~\eqref{E:Blue2}, the relation reads

984: \begin{equation}

985: \label{E:AActionBis}

986: \IInt(\tt \act \eev(\ww)) \sim \IInt(\tt) \comp \ssh0(\eev(\ww))

987: \end{equation}

988: for $\tt$ a term in~$\Tox$ and $\ww$ a word in~$\WALD$ such that $\tt \act \eev(\ww)$ is defined. 

989: 

990: Following the general scheme of Section~\ref{SS:Blue1} again, we now mimick the construction of~$\IInt$ inside the group~$\GALD$.  Using $\sh\a$ to denote the endomorphism of~$\GALD$ that maps $\SS\a$ to~$\SS{1\a}$ and $\AA\a$ to~$\AA{1\a}$ for each address~$\a$, this amounts to setting:

991: 

992: \begin{defi}

993: We inductively associate with every term~$\tt$ in~$\Tox$ an element~$\Int(\tt)$ of~$\GALD$, also denoted~$\blue\tt$, by

994: \begin{equation}

995: \Int(\tt) = 

996: \begin{cases}

997: 1 

998: &\mbox{for $\tt = \xx$,}\\

999: \Int(\tti) \cdot \sh1(\Int(\ttii)) \cdot \SS\ea \cdot \sh1(\Int(\tti))\inv 

1000: &\mbox{for $\tt = \tti \op \ttii$,}\\

1001: \Int(\tti) \cdot \sh1(\Int(\ttii)) \cdot \AA\ea  

1002: &\mbox{for $\tt = \tti \OP \ttii$.}

1003: \end{cases}

1004: \end{equation}

1005: \end{defi}

1006: 

1007: \begin{exam}

1008: Let $\tt$ be $\xx \op ((\xx \OP \xx) \op \xx)$. Starting from $\Int(\xx) = 1$, we first find 

1009: $$\Int(\xx \OP \xx) = 1 \cdot \sh1(1) \cdot \AA\ea = \AA\ea,$$ 

1010: then

1011: $$\Int((\xx \OP \xx) \op \xx) = \AA\ea \cdot \sh1(1) \cdot \SS\ea \cdot \sh1(\AA\ea)\inv = \AA\ea \SS\ea \AA1\inv,$$ 

1012: and, finally,

1013: $$\Int(\tt) = 1 \cdot \sh1(\AA\ea \SS\ea \AA1\inv) \cdot \SS\ea \cdot \sh1(1)\inv = \AA1 \SS1 \AA{11}\inv \SS\ea.$$ 

1014: \end{exam}

1015: 

1016: If our intuition is correct, \ie, if the confluence relations defining the group~$\GALD$ capture enough of the geometry of the laws~$\ALD$, Relation~\eqref{E:AActionBis} should follow from the lattice relations in~$\GGALD$, and, therefore, it should induce an equality in the group~$\GALD$, \ie, we {\it should} have the relation

1017: \begin{equation}

1018: \label{E:ActionBis}

1019: \Int(\tt \act \eev(\ww)) = \Int(\tt) \cdot \sh0(\ev(\ww)),

1020: \end{equation}

1021: \ie, with our former definition, the mapping~$\Int$ should be an $\sh0$-blueprint . This is indeed the case---and this is the key point for our current analysis of the ALD-laws. The nice feature is that, if the result is true---and it is---its proof must be a simple verification.

1022: 

1023: \begin{lemm}

1024: \label{L:Main}

1025: The mapping~$\Int$ is a $\sh0$-blueprint for the $\ALD$-laws.

1026: \end{lemm}

1027: 

1028: \begin{proof}

1029: For an induction on the length of the word~$\ww$, it is enough to prove the result when $\ww$ consists of a single letter, \ie, it is one of $\AA\a^{\pm 1}$, $\SS\a^{\pm1}$. Moreover, the cases of $\AA\a\inv$ and $\SS\a\inv$ immediately follow from the cases of~$\AA\a$ and~$\SS\a$, respectively. So, the point is to establish the equalities

1030: \begin{equation}

1031: \label{E:ActionLocal}

1032: \Int(\tt \act \AA\a) = \Int(\tt) \cdot \AA{0\a} ,\quad

1033: \Int(\tt \act \SS\a) = \Int(\tt) \cdot \SS{0\a},

1034: \end{equation}

1035: whenever the involved terms are defined. 

1036: 

1037: We prove~\eqref{E:ActionLocal} using induction on the length of the address~$\a$. Let us begin with $\a = \ea$ and the case of~$\AA\a$, \ie, of~$\AA\ea$. Saying that $\tt \act \AA\ea$ (\ie, $\tt \act \AA\ea$) is defined, means that $\tt$ can be decomposed as $\tt = \tti \op (\ttii \op \ttiii)$, and, then, we have $\ttt = (\tti \OP \ttii) \op \ttiii$. Using the commutation and quasi-commutation relations of~$\GALD$, we find

1038: \begin{align*}

1039: \blue\ttt 

1040: &= \blue\tti \cdot \sh1(\blue\ttii) \cdot \AA\ea \cdot \sh1(\blue\ttiii) \cdot \SS\ea \cdot \AA1\inv \cdot \sh{11}(\blue\ttii)\inv \cdot \sh1(\blue\tti)\inv ,\\

1041: &= \blue\tti \cdot \sh1(\blue\ttii) \cdot \sh{11}(\blue\ttiii) \cdot \AA\ea \cdot \SS\ea \cdot \AA1\inv \cdot \sh{11}(\blue\ttii)\inv \cdot \sh1(\blue\tti)\inv ,\\

1042: \blue\tt \cdot \AA{0\a} 

1043: &= \blue\tti \cdot \sh1(\blue\ttii) \cdot \sh{11}(\blue\ttiii) \cdot \SS1 \cdot \sh{11}(\blue\ttii)\inv \cdot \SS\ea \cdot \sh1(\blue\tti)\inv \cdot \AA0,\\

1044: &= \blue\tti \cdot \sh1(\blue\ttii) \cdot \sh{11}(\blue\ttiii) \cdot \SS1 \cdot \SS\ea \cdot \AA0 \cdot \sh{11}(\blue\ttii)\inv \cdot \sh1(\blue\tti)\inv,

1045: \end{align*}

1046: and the equality follows from~\eqref{E:ALDCrit3}, which gives 

1047: $\AA\ea \cdot \SS\ea \cdot \AA1\inv = \SS1 \cdot \SS\ea \cdot \AA0$.

1048: 

1049: We consider now the case of~$\SS\ea$. The hypothesis that $\tt \act \SS\ea$ is defined means that $\tt$ can be decomposed as $\tti \op (\ttii \Op \ttiii)$, and, then, $\ttt$ is $(\tti \op \ttii) \Op (\tti \op \ttiii)$. Assume first $\Op = \op$ (this is the most complicated case). Using the commutation and quasi-commutation relations of~$\GALD$, we find

1050: \begin{align*}

1051: \blue\ttt 

1052: &= \blue\tti \cdot \sh1(\blue\ttii) \cdot \SS\ea \cdot \sh1(\blue\tti)\inv \cdot \sh1(\blue\tti) \cdot \sh{11}(\blue\ttiii) \cdot \SS1 \cdot \sh{11}(\blue\tti)\inv \\

1053: &\hspace{40mm}

1054: \cdot \SS\ea \cdot \sh{11}(\blue\tti) \cdot \SS1\inv \cdot \sh{11}(\blue\ttii)\inv \cdot \sh1(\blue\tti)\inv\\

1055: &= \blue\tti \cdot \sh1(\blue\ttii)  \cdot \sh{11}(\blue\ttiii) \cdot \SS\ea \cdot \SS1 

1056: \cdot \SS\ea \cdot \SS1\inv \cdot \sh{11}(\blue\ttii)\inv \cdot \sh1(\blue\tti)\inv,\\

1057: \blue\tt \cdot \SS{0\a} 

1058: &= \blue\tti \cdot \sh1(\blue\ttii) \cdot \sh{11}(\blue\ttiii) \cdot \SS1 \cdot \sh{11}(\blue\ttii)\inv \cdot \SS\ea \cdot \sh1(\blue\tti)\inv \cdot \SS0\\

1059: &= \blue\tti \cdot \sh1(\blue\ttii) \cdot \sh{11}(\blue\ttiii) \cdot \SS1 \cdot \SS\ea \cdot \SS0 \cdot \sh{11}(\blue\ttii)\inv \cdot \sh1(\blue\tti)\inv,

1060: \end{align*}

1061: and the equality follows from the~\eqref{E:ALDCrit1} relation $\SS1 \cdot \SS\ea \cdot \SS1 \cdot \SS0 = \SS\ea \cdot \SS1 \cdot \SS\ea$. Assume now $\Op = \OP$. One finds

1062: \begin{align*}

1063: \blue\ttt 

1064: &= \blue\tti \cdot \sh1(\blue\ttii) \cdot \SS\ea \cdot \sh1(\blue\tti)\inv \cdot \sh1(\blue\tti) \cdot \sh{11}(\blue\ttiii) \cdot \SS1 \cdot \sh{11}(\blue\tti)\inv \cdot \AA\ea \\

1065: &= \blue\tti \cdot \sh1(\blue\ttii) \cdot \sh{11}(\blue\ttiii) \cdot \SS\ea \cdot \SS1 \cdot \AA\ea\cdot \sh1(\blue\tti)\inv ,\\

1066: \blue\tt \cdot \SS{0\a} 

1067: &= \blue\tti \cdot \sh1(\blue\ttii) \cdot \sh{11}(\blue\ttiii) \cdot \AA1 \cdot \SS\ea \cdot \sh1(\blue\tti)\inv \cdot \SS0\\

1068: &= \blue\tti \cdot \sh1(\blue\ttii) \cdot \sh{11}(\blue\ttiii) \cdot \AA1 \cdot \SS\ea  \cdot \SS0\cdot \sh1(\blue\tti)\inv,

1069: \end{align*}

1070: and the equality follows from the~\eqref{E:ALDCrit2} relation $\AA1 \cdot \SS\ea \cdot \SS0 = \SS\ea \cdot \SS1 \cdot \AA\ea$. 

1071: 

1072: The case $\a = \ea$ is completed. 

1073: From now on, we shall treat the cases of~$\AA\a$ and~$\SS\a$ simultaneously, using~$\XX\a$ as a common notation. Assume first that the address~$\a$ is $0\b$ for some~$\b$. The hypothesis that $\tt \act \XX\a$ is defined implies that $\tt$ can be decomposed as $\tti \Op \ttii$, and, then, $\ttt$ is $\ttti \Op \ttii$, with $\ttti = \tti \act \XX\b$. Assume first $\Op = \op$. The induction hypothesis implies $\blue\ttti = \blue\tti \cdot \XX{0\b}$. We find

1074: \begin{align*}

1075: \blue\ttt 

1076: &= \blue\tti \cdot \XX{0\b} \cdot \sh1(\blue\ttii) \cdot \SS\ea \cdot \XX{10\b}\inv \cdot \sh1(\blue\tti)\inv ,\\

1077: &= \blue\tti \cdot \sh1(\blue\ttii) \cdot \XX{0\b} \cdot \SS\ea \cdot \XX{10\b}\inv \cdot \sh1(\blue\tti)\inv,\\

1078: \blue\tt \cdot \XX{0\a} 

1079: &= \blue\tti \cdot \sh1(\blue\ttii) \cdot \SS\ea \cdot \sh1(\blue\tti)\inv \cdot \XX{00\b},\\

1080: &= \blue\tti \cdot \sh1(\blue\ttii) \cdot \SS\ea \cdot \XX{00\b} \cdot \sh1(\blue\tti)\inv,

1081: \end{align*}

1082: and the equality follows from the~\eqref{E:ALDHeir1} relation $\XX{0\b} \cdot \SS\ea = \SS\ea \cdot \XX{00\b} \cdot \XX{10\b}$. Similarly, for $\Op = \OP$, we find

1083: \begin{align*}

1084: \blue\ttt 

1085: &= \blue\tti \cdot \XX{0\b} \cdot \sh1(\blue\ttii) \cdot \AA\ea 

1086: = \blue\tti \cdot \sh1(\blue\ttii) \cdot \XX{0\b} \cdot \AA\ea ,\\

1087: \blue\tt \cdot \XX{0\a} 

1088: &= \blue\tti \cdot \sh1(\blue\ttii) \cdot \AA\ea \cdot \XX{00\b},

1089: \end{align*}

1090: and the equality follows from the~\eqref{E:ALDHeir4} relation $\XX{0\b} \cdot \AA\ea = \AA\ea \cdot \XX{00\b}$. 

1091: 

1092: The argument is similar when  the address~$\a$ is $1\b$ for some~$\b$. The hypothesis that $\tt \act \XX\a$ is defined implies that $\tt$ can de decomposed as $\tti \Op \ttii$, and, then, $\ttt$ is $\tti \Op \tttii$, with $\tttii = \ttii \act \XX\b$. Assume first $\Op = \op$. The induction hypothesis implies $\blue\ttti = \blue\tti \cdot \XX{0\b}$. We find now

1093: \begin{align*}

1094: \blue\tt \cdot \XX{0\a} 

1095: &= \blue\tti \cdot \sh1(\blue\ttii) \cdot \SS\ea \cdot \sh1(\blue\tti)\inv \cdot \XX{01\b}

1096: = \blue\tti \cdot \sh1(\blue\ttii) \cdot \SS\ea \cdot \XX{01\b} \cdot \sh1(\blue\tti)\inv,\\

1097: \blue\ttt 

1098: &= \blue\tti \cdot \sh1(\blue\ttii) \cdot \XX{10\b} \cdot \SS\ea \cdot \sh1(\blue\tti)\inv ,

1099: \end{align*}

1100: and the equality follows from the~\eqref{E:ALDHeir2} relation $\XX{10\b} \cdot \SS\ea = \SS\ea \cdot \XX{01\b}$. Finally, for $\Op = \OP$, we have

1101: \begin{align*}

1102: \blue\tt \cdot \XX{0\a} 

1103: &= \blue\tti \cdot \sh1(\blue\ttii) \cdot \AA\ea \cdot \XX{01\b},\\

1104: \blue\ttt 

1105: &= \blue\tti \cdot \sh1(\blue\ttii) \cdot \XX{01\b} \cdot \AA\ea,

1106: \end{align*}

1107: and the equality follows from the~\eqref{E:ALDHeir5} relation $\XX{10\b} \cdot \AA\ea = \AA\ea \cdot \XX{01\b}$. The induction is complete. 

1108: \end{proof}

1109: 

1110: We thus completed the construction of a blueprint for the $\ALD$-laws. It may be observed that this construction induces the construction of a similar $\sh0$-blueprint for the $\LD$-law considered alone: indeed, in the case of terms not containing the operator~$\OP$, the blueprint does not involve any generator~$\AA\a$, and it can be checked that the only relations needed to check the blueprint condition are present in the group~$\GLD$.

1111: 

1112: \begin{rema}

1113: Here the blueprints have been defined for terms in one variable only. Developing a similar approach for terms involving several variables is possible, at the expense of extending the geometry monoid~$\GGLL$ by introducing additional operators whose action is to shift the indices of the variables so as to still generate all terms starting from right vines. We refer to~\cite{Dgd} for details in the specific case of the $\LD$-law.

1114: \end{rema}

1115: 

1116: \section{Using~$\GLL$ to study~$\LLL$}

1117: \label{S:Using}

1118: 

1119: We claim that the geometry group~$\GLL$ is an interesting object that provides useful information about the laws of~$\LLL$. The way this vague statement can be made precise depends on the specific algebraic laws one considers. If the latter are simple, typically associativity and/or commutativity, constructing an $\LLL$-algebra or solving the word problem of~$\LLL$ is not a challenge, and in particular appealing to~$\GLL$ is not necessary. However the group~$\GLL$ may be of interest in itself, as the enormous literature devoted to R.Thompson's groups~$F$ and~$V$ shows~\cite{Tho, McT, CFP}. In the case of complicated laws, typically self-distributivity or variants, constructing $\LLL$-algebras and solving the word problem of~$\LLL$ may be difficult (and often even open) questions, and then the geometry group may be useful. The basic scheme consists in exploiting the blueprint construction---when it exists---to define an algebraic system satisfying the laws of~$\LLL$ on some quotient of the group~$\GLL$.

1120: 

1121: \subsection{Construction of algebraic systems: principle}

1122: 

1123: The first, and more direct, application of the previous approach is the construction of an algebra that obeys some prescribed laws. The general principle is as follows:

1124: 

1125: \begin{prop}

1126: \label{P:Eval}

1127: Assume that $\LLL$ is a family of balanced algebraic laws involving the signature~$\Sign$, that $\Int$ is a $\phi$-blueprint for the laws~$\LLL$, and that $H$ is a subgroup of~$\GLL$ that includes the image of~$\phi$. For~$\tt$ a term in~$\TSx$, let $\cl(\tt)$ be the left coset of~$\Int(\tt)$ modulo~$H$. Then the map~$\cl$ is constant on each $\EQ\LL$-class, \ie, $\LLL$-equivalent terms have the same image.

1128: \end{prop}

1129: 

1130: \begin{proof}

1131: Assume that $\tt$ and $\ttt$ are $\LLL$-equivalent terms in~$\Tox$. By Proposition~\ref{P:Basic}, there must exist an operator in~$\GGLL$ that maps~$\tt$ to~$\ttt$, and, therefore, there must exist a word~$\ww$ in~$\WLL$ such that $\tt \act \eev(\ww)$ is defined and equal to~$\ttt$. Then, by~\eqref{E:Constr}, we have $\Int(\ttt) = \Int(\tt) \cdot \phi(\ev(\ww))$ in~$\GLL$, so the hypothesis gives

1132: $$(\Int(\tt))\inv \cdot (\Int(\ttt)) \in H,$$

1133: \ie, $\Int(\tt)$ and $\Int(\ttt)$ lie in the same $H$-coset.

1134: \end{proof}

1135: 

1136: \begin{coro}

1137: \label{C:Eval}

1138: Under the same hypothesis, let $M$ be the image of the mapping~$\cl$. For each operation symbol~$\Op$ in~$\Sign$, define an operation in~$M$ by 

1139: $$\Int(\tt) H \Op \Int(\ttt) H := \Int(\tt \Op \ttt)H.$$

1140: Then $M$ equipped with these operations is an $\LLL$-algebra, \ie, an $\Sign$-structure satisfying all laws of~$\LLL$. 

1141: \end{coro}

1142: 

1143: Note that, in general, nothing guarantees that the system so obtained is non-trivial: it might happen that the quotient-structure $H\backslash\GLL$ collapses to a point. This does not happen in the cases we shall consider: on the contrary, the obtained algebraic systems will turn out to be free, \ie, as far from trivial as possible.

1144: 

1145: \subsection{Construction of algebraic systems: the example of~$\ALD$}

1146: 

1147: We return to our leading example, namely the $\ALD$-laws. In Section~\ref{S:Blue} we constructed a $\sh0$-blueprint~$\Int$ for~$\ALD$, so Proposition~\ref{P:Eval} and Corollary~\ref{C:Eval} directly apply for each subgroup~$H$ of~$\GALD$ including the image of~$\sh0$, typically $H := \sh0(\GALD)$. We thus obtain an $\ALD$-algebra whose domain is some subset of the coset set $\sh0(\GALD)\backslash\GALD$. 

1148: 

1149: Actually, we can adapt the results to make them more simple and handy. Indeed, instead of restricting to the image of the mapping~$\cl$, we can extend the construction to the whole group~$\GALD$. To do that, the idea is obvious: we look at the inductive definition of the blueprint, and define $\op$ and $\OP$ to be the operations used to construct $\Int(\tt \op \ttt)$ and $\Int(\tt \OP \ttt)$ from $\Int(\tt)$ and $\Int(\ttt)$, \ie, we choose the operations on~$\GALD$ that make $\Int$ a morphism from the free algebra~$(\Tox, \op, \OP)$ to~$\GALD$.

1150: 

1151: \begin{lemm}

1152: \label{L:Obst}

1153: On the group~$\GALD$ define two new binary operations $\op, \OP$ by

1154: \begin{equation} 

1155: \label{E:Newop}

1156: \xx \op \yy := \xx \cdot \sh1(\yy) \cdot

1157: \SS\ea \cdot \sh1(\xx)\inv, \qquad

1158: \xx \OP \yy := \xx \cdot \sh1(\yy) \cdot

1159: \AA\ea.

1160: \end{equation}

1161: Then, for all $\xx, \yy, \zz$ in~$\GALD$ and $\Op$ in $\{\op, \OP\}$, we have

1162: \begin{gather}

1163: \label{E:Obst1}

1164: (\xx \op \yy) \Op (\xx \op \zz) = x \op (\yy \Op \zz) \cdot \SS0,\\

1165: \label{E:Obst2}

1166: (\xx \OP \yy) \op \zz = \xx \op (\yy \op \zz) \cdot \AA0,\\

1167: \label{E:Quot1}

1168: (\xx \cdot \sh0(\zz) \Op \yy = \xx \Op \yy \cdot \sh{00}(\zz),\\

1169: \label{E:Quot2}

1170: \xx \Op (\yy \cdot \sh0(\zz)) = x \Op \yy \cdot \sh{01}(\zz).

1171: \end{gather}

1172: \end{lemm}

1173: 

1174: \begin{proof}

1175: The verifications are those already made in the proof of Lemma~\ref{L:Main}. The only difference is that, in Section~\ref{S:Blue}, we only consider elements of~$\GALD$ 

1176: that are blueprints of terms, while, now, we consider arbitrary elements of~$\GALD$. Now inspecting the proof of Section~\ref{S:Blue} shows that the specific form of the elements is never used, and, therefore, the whole computation remains valid.

1177: \end{proof}

1178: 

1179: Relations~\eqref{E:Obst1} and~\eqref{E:Obst2} control the obstruction for $(\GALD, \op, \OP)$ to be an $\ALD$-algebra, and show that the latter belongs to the subgroup~$\sh0(\GALD)$. Relations~\eqref{E:Quot1} and~\eqref{E:Quot2} show that the operations on~$\GALD$ induce well-defined operations on the coset set $\sh0(\GALD) \backslash \GALD$. Thus we may state:

1180: 

1181: \begin{prop}

1182: Let $M$ be the coset set~$\sh0(\GALD) \backslash \GALD$. Then $M$ equipped with the operations induced by those of Lemma~\ref{L:Obst} is an $\ALD$-algebra.

1183: \end{prop}

1184: 

1185: The subgroup~$\sh0(\GALD)$ is not normal, and, therefore, the associated coset set is not a group. When we replace $\sh0(\GALD)$ with a larger subgroup~$H$ of~$\GALD$, typically the normal subgroup generated by $\sh0(\GALD)$, we can still apply Proposition~\ref{P:Eval}, but it is not a priori sure that the operations~$\op$ and~$\OP$ induce well-defined operations on the whole of $H \backslash \GALD$. This however happens in good cases, as here with~$\ALD$.

1186: 

1187: \begin{lemm}

1188: Every normal subgroup of~$\GALD$ that includes the image of~$\sh0$ contains all generators~$\SS\a$ and~$\AA\a$ such that $\a$ contains at least one~$0$.

1189: \end{lemm}

1190: 

1191: \begin{proof}

1192: For $\XX{} = \SS{}$ or~$\AA{}$, the commutation relation~\eqref{E:ALDHeir5} gives $\XX{10} = \AA\eaÊ\cdot \XX{01} \cdot \AA\ea\inv$, hence, inductively

1193: $$\XX{1^i0\a} = \AA{1^{i-1}} \cdot \ldots \cdot \AA1 \cdot \AA\ea \cdot \XX{01^i\a} \cdot \AA\ea\inv \cdot \AA1\inv \cdot \ldots \cdot \AA{1^{i-1}}\inv,$$

1194: which shows that ant normal subgroup containing all~$\XX{0\g}$ must contain all~$\XX\a$ such that $\a$ contains at least one~$0$.

1195: \end{proof}

1196: 

1197: Thus, collapsing all generators~$\SS\a$ and~$\AA\a$ such that $\a$ begins with~$0$ in~$\GALD$ requires to collapse all generators~$\XX\a$ such that $\a$ contains at least one~$0$, in which case the quotient-group is generated by the images of the remaining generators, namely the generators~$\SS{1^{i-1}}$ and~$\AA{1^{i-1}}$ with $i \ge 1$. Considering what remains from the defining relations of~$\GALD$, and using~$\ss i$ and~$\aa i$ as simplified notation for~$\SS{1^{i-1}}$ and~$\AA{1^{i-1}}$, we are led to the following group:

1198: 

1199: \begin{defi}

1200: \label{D:Braids}

1201: We let $\Bp$ be the group generated two infinite sequences $\ss1, \ss2, ...$ and $\aa1, \aa2, ...$ of generators subject to the relations

1202: \begin{equation} 

1203: \label{E:Relations}

1204: \begin{cases}

1205: \ \ss i \ss j  = \ss j \ss i,

1206: \quad \ss i \aa j  = \aa j \ss i,

1207: \quad \aa i \aa{j-1} = \aa j \aa i,

1208: \quad \aa i \ss{j-1} = \ss j \aa i,\\

1209: \ \ss i \ss{i+1} \ss i 

1210: = \ss{i+1} \ss i \ss{i+1},

1211: \quad

1212: \ss{i+1} \ss i \aa{i+1}

1213: = \aa i \ss i,

1214: \quad

1215: \ss i \ss{i+1} \aa i 

1216: = \aa{i+1} \ss i

1217: \end{cases}

1218: \end{equation}

1219: for $i \ge 1$ and $j \ge i+2$.

1220: \end{defi}

1221: 

1222: (We do not claim that $\Bp$ is the quotient of~$\GALD$ by the normal subgroup generated by~$\sh0(\GALD)$.) By construction, mapping $\SS{1^{i-1}}$ to~$\ss i$ and $\AA{1^{i-1}}$ to~$\aa i$ defines a surjective homomorphism~$\pi$ of~$\GALD$ onto~$\Bp$ whose kernel includes~$\sh0(\GALD)$, and therefore the normal subgroup~$N$ it generates. However, it might be that $\pi$ collapses more than~$N$, and proving that this does not happen would require a more complete algebraic study of the group~$\GALD$, which is not our current aim. Here, the only thing we wish to observe that, by mimicking once again the construction of the blueprint, we can construct an $\ALD$-structure on the group~$\Bp$:

1223: 

1224: \begin{prop}

1225: \cite{Dhe, Dhj}

1226: Let $\sh{}$ denote the endomorphism of the group~$\Bp$ that maps~$\ss i$ to~$\ss{i+1}$ and~$\aa i$ to~$\aa{i+1}$ for every positive integer~$i$. Define binary operations~$\op, \OP$ on~$\Bp$ by

1227: \begin{equation}

1228: \label{E:NNewop}

1229: \xx \op \yy := \xx \cdot \sh{}(\yy) \cdot

1230: \ss1 \cdot \sh1(\xx)\inv, \qquad

1231: \xx \OP \yy := \xx \cdot \sh{}(\yy) \cdot \aa1.

1232: \end{equation}

1233: Then $(\Bp, \op, \OP)$ is an $\ALD$-algebra. Moreover, this $\ALD$-algebra is torsion-free, \ie, every element of~$\Bp$ generates a free $\ALD$-subsystem.

1234: \end{prop}

1235:  

1236: The group~$\Bp$ was introduced by M.\,Brin in~\cite{Bri1, Bri2} and the author in~\cite{Dhb} independently, and its elements have been interpreted in~\cite{Dhe} as parenthesized braids, an refinement of standard Artin braids in which one takes into account the distances between the strands. The above results show that, in the context of the $\ALD$-laws, the connection between~$\GALD$ and~$\Bp$ is similar to the connection between the geometry group of self-distributivity and the braid group~$B_\infty$, as investigated in~\cite{Dgd}. The benefit of the geometry monoid approach is to make the operations~\eqref{E:NNewop} natural and explain why they had to appear in this form and in this group.

1237: 

1238: \subsection{Presentation of $\GGLL$}

1239: 

1240: A different use of a blueprint is to allow for a closer comparison between the monoid~$\GGLL$ and the group~$\GLL$ in the non-linear case. We observed that $\GLL$ is constructed by means of a list of confluence relations holding in~$\GGLL$, but, in general, there is no reason why this list should be complete, \ie, provide a presentation of~$\GGLL$. Actually, when the empty operator belongs to~$\GGLL$, it cannot be the case that the confluence relations exhaust all relations of~$\GGLL$ as no such relation involves~$\emptyset$. However, the true question is to control the relations of~$\GGLL$ that do not involve the empty operator, which amounts to describing the relation~$\sim$ of Definition~\ref{D:Sim} on~$\GGLL$. Then, we have the following solution: 

1241: 

1242: \begin{prop}

1243: \label{P:Pres}

1244: Assume that $\phi$ is injective and $\Int$ is a $\phi$-blueprint for the laws~$\LLL$. Then the confluence relations used in the definition of~$\GLL$ generate all non-trivial relations in~$\GGLL$ in the following sense: for all word~$\ww, \ww'$ in~$\WLL$, the relation $\eev(\ww) \sim \eev(\ww')$ holds only if $\ww$ and $\ww'$ represent the same element of the group~$\GLL$.

1245: \end{prop}

1246: 

1247: \begin{proof}

1248: Assume that $\ww, \ww'$ are words in~$\WLL$ such that the associated operators~$\eev(\ww)$ and~$\eev(\ww')$ in~$\GGLL$ are connected by~$\sim$, \ie, there exists at least one term~$\tt$ on which they agree. Let~$\ttt$ be the common image of~$\tt$ under these operators. The hypothesis that $\Int$ is a $\phi$-blueprint gives

1249: $$\Int(\tt) \cdot \phi(\ev(\ww)) = \Int(\ttt) = \Int(\tt) \cdot \phi(\ev(\ww'))$$

1250: in~$\GLL$, whence $\phi(\ev(\ww)) = \phi(\ev(\ww'))$. If $\phi$ is injective, we deduce $\ev(\ww) = \ev(\ww')$, \ie, the words~$\ww$ and~$\ww'$ represent the same element of the group~$\GLL$.

1251: \end{proof}

1252: 

1253: \begin{exam}

1254: \label{X:Rel}

1255: We conjecture that the endomorphism~$\sh0$ is injective on the group~$\GALD$, which would imply that the confluence relations listed in Section~\ref{SS:ConfALD} generate, in the sense described above, all relations holding in the geometry monoid~$\GGALD$. 

1256: 

1257: When we restrict from~$\ALD$ to~$\LD$ alone, then the argument is similar, and, in that case, the injectivity of~$\sh0$ on~$\GLD$ is known. What makes the case of~$\ALD$ more difficult is that, in the latter case, some confluence relations are missing, and the group~$\GALD$ is not a group of fractions for the positive monoid~$\GALDp$, while $\GLD$ is a group of fractions for~$\GLDp$. In both cases, proving the injectivity of~$\sh0$ on the positive monoid is easy, but extending the result to the group is not obvious hen the latter is not a group of fractions.

1258: \end{exam}

1259:  

1260: \subsection{Solving the word problem}

1261: 

1262: Still another possibility is to use the blueprint for solving the word problem of~$\LLL$, \ie, to construct an algorithm that decides whether two terms~$\tt, \ttt$ are equivalent modulo the laws of~$\LLL$.

1263: 

1264: \begin{prop}

1265: \label{P:WP}

1266: Assume that $\Int$ is a Turing computable $\phi$-blueprint for the laws~$\LLL$, that $P, Q$ are disjoint recursively enumerable subsets of~$\GLL$ such that $P$ includes the image of~$\phi$, and there is a binary relation~$\rel$ on~$\TSx$ such that, for all terms~$\tt, \ttt$, at least one of~$\tt \EQ\LLL \ttt$, $\tt \rel \ttt$ holds and $\tt \rel \ttt$ implies $\Int(\tt)\inv \Int(\ttt) \in Q$. Then the word problem of the laws~$\LLL$ is solvable.

1267: \end{prop}

1268: 

1269: \begin{proof}

1270: Let $\widehat P, \widehat Q$ be disjoint recursive sets that include~$P$ and~$Q$ respectively. First assume that $\tt \EQ\LLL \ttt$ holds. Under the hypotheses, this implies 

1271: $$\Int(\tt)\inv \Int(\ttt) \in \Im(\phi) \subseteq P \subseteq \widehat P.$$

1272: Conversely, assume that $\tt \EQ\LLL \ttt$ fails. Then necessarily $\tt \rel \ttt$ holds, 

1273: which implies

1274: $$\Int(\tt)\inv \Int(\ttt) \in Q \subseteq \widehat Q,$$

1275: so $\tt \EQ\LLL \ttt$ is equivalent to $\Int(\tt)\inv \Int(\ttt) \in \widehat P$. As the function~$\Int$ is assumed to be Turing computable and the set~$P$ is assumed to be Turing decidable, the latter condition is Turing decidable.

1276: \end{proof}

1277: 

1278: \begin{exam}

1279: Let us consider the case of the $\LD$-law. We know that there exists an $\sh0$-blueprint~$\Int$ for~$\LD$. Let $\tt \rel \ttt$ be the symmetric closure of the relation ``$\tt$ is $\LD$-equivalent to some iterated left subterm of some term $\LD$-equivalent to~$\ttt$''. Let $P$ be the subset of~$\GLD$ consisting of those elements that can be expressed using none of~$\SS\ea, \SS\ea\inv$, and let~$Q$ be the subset of~$\GLD$ consisting of those elements that can be expressed using exactly one of~$\SS\ea, \SS\ea\inv$. It is easy to show that every element of~$\GLD$ in the image of~$\sh0$ belongs to~$P$, while $\tt \rel \ttt$ implies $\Int(\tt)\inv \Int(\ttt) \in Q$. Moreover, one can show that $P$ and $Q$ are disjoint and recursive, so Proposition~\ref{P:WP} implies that the word problem of~$\LD$ is solvable \cite{Dgd}. This was the first solution for a long standing open question---other solutions are known now.

1280: 

1281: A similar scheme was used in~\cite{Dgj} to solve the word problem for the central duplication law $x(yz) = (xy)(yz)$---and, in this case, no alternative solution is known so far.

1282: 

1283: As for the word problem of the~$\ALD$-laws---for which a direct solution involving the group~$\Bp$ of Definition~\ref{D:Braids} is known---the scheme might work as well, but, as in Example~\ref{X:Rel}, some pieces are missing as the group~$\GALD$ fails to be a group of fractions for the positive monoid~$\GALDp$, making the verification of certain technical conditions problematic, typically the fact the expected sets~$P, Q$ are disjoint.

1284: \end{exam}

1285: 

1286: \section{Proving global confluence}

1287: \label{S:Conf}

1288: 

1289: Let $\LLL$ be a family of oriented algebraic laws. Then we have introduced both the geometry monoid~$\GGLL$, which corresponds to the rewrite system~$\RLL$ and to using the laws of~$\LLL$ with either orientation, and the positive geometry monoid~$\GGLLp$, which corresponds to the rewrite system~$\RLLp$ and to using the laws of~$\LLL$ in the distinguished direction only. An important case is when the system~$\RLLp$ turns out to be confluent, and it is a technically significant issue to prove this confluence result when possible.

1290: 

1291: The standard way for proving a confluence result consists in checking local confluence and then using some noetherianity condition to conclude using the classical Newman lemma---see for instance~\cite{Boo, Hue}. However, it turns out that, in the current framework, the rules one considers are often ill-oriented, so that no noetherianity can be expected. The aim of this short section is to present an alternative method that can be used instead.

1292: 

1293: \subsection{Least common expansion}

1294: 

1295: Let us start with the example of the $\LD$-law $x \op (y \op z) = (x\op y)\op (x\op z)$. If we orient it in the contracting direction $(x\op y)\op (x\op z) \to x\op (y\op z)$, then the rule diminishes the size and is therefore neotherian, but it is easily checked that confluence fails. When one chooses the expanding orientation, namely $x\op (y\op z) \to (x\op y)\op (x\op z)$, then, as seen in Section~\ref{SS:ConfALD}, we obtain a locally confluent system as, for each pair of addresses~$\a, \b$, there exists one (and exactly one) confluence relation $\SSp\a \comp ... = \SSp\b \comp ...$, where $\SSp\a$ denotes ``applying $\LD$ at position~$\a$ in the expanding direction''. Now, the rule increases the size of the terms, and it is not noetherian as, for instance, starting with the term $x \op (x \op x)$, we can apply~$\SSp\ea$ any number of times. So the general question is: 

1296: \begin{quote}

1297: How to prove that the locally confluent system~$\RLLp$ is possibly globally confluent (without assuming any noetherianity condition)?

1298: \end{quote} 

1299: Let us say that a term~$\ttt$ is a {\it degree~$d$} $\LLL$-expansion of a term~$\tt$ is $\ttt$ is the image of~$\tt$ under an element of~$\GGLLp$ that can be expressed as the product of at most~$d$ elementary operators~$\OOOp\LL\a$. The method developed in~\cite{Dgd} uses the following criterion:

1300: 

1301: \begin{prop}

1302: Assume that there exists a mapping~$\partial: \TS \to \TS$ such that, for each term~$\tt$, the term~$\partial\tt$ is an $\LLL$-expansion of all degree~$1$ $\LLL$-expansions of~$\tt$ and, moreover, the mapping~$\partial$ is increasing w.r.t.~$\toLLp$, \ie, $\tt \toLLp \ttt$ implies $\partial\tt \toLLp \partial\ttt$. Then $\RLLp$ is confluent.

1303: \end{prop}

1304: 

1305: \begin{proof}

1306: It is enough to prove that, for each~$d$, the term $\partial^d\tt$ is a common $\LLL$-expansion of~$\tt$ of all degree~$d$ $\LLL$-expansions of~$\tt$. We use induction on~$d$. The result is trivial for $d = 0$, and it is true for $d = 1$ by hypothesis. Assume $d \ge 2$, and let $\ttt$ be a degree~$d$ $\LLL$-expansion of~$\tt$. By hypothesis, there exists~$\tti$ such that $\tti$ is a degree~$d-1$ expansion of~$\tt$, and $\ttt$ is a degree~$1$ expansion of~$\tti$. On the one hand, $\ttt$ is a degree~$1$ expansion of~$\tti$, hence $\partial \tti$ is an expansion of~$\ttt$. On the other hand, by induction hypothesis, $\partial^{d-1}\tt$ is an expansion of~$\tti$, hence $\partial^d\tt$ is an expansion of~$\partial\tti$. Being an expansion is transitive, hence $\partial^d\tt$ is an expansion of~$\ttt$, as expected. 

1307: \end{proof}

1308: 

1309: The criterion was first designed for the case of self-distributivity \cite{Dgd}, but it was subsequently also applied in the case of central duplication \cite{Dgj}, and in the case of idempotency with or without self-distributivity \cite{Lrb}. In each case, the construction of the operator~$\partial$ heavily relies on the considered laws.

1310: 

1311: \subsection{Group of fractions}

1312: 

1313: An alternative solution for proving the possible confluence of the positive rewrite system~$\RLLp$ consists in working in the geometry monoid~$\GGLL$, or, rather, in its positive submonoid~$\GGLLp$. Then we have the following criterion:

1314: 

1315: \begin{prop}

1316: \label{P:Mult}

1317: Assume that the monoid~$\GGLLp$ admits common right multiples in the following strong sense: for all~$\ff, \gg$ in~$\GGLLp$, there exist $\ff', \gg'$ satisfying $\ff \comp \gg' = \gg \comp \ff'$ and, in addition, the domain of~$\ff \comp \gg'$ is the intersection of the domains of~$\ff$ and~$\gg$. Then the rewrite system~$\RLLp$ is confluent.

1318: \end{prop}

1319: 

1320: \begin{proof}

1321: Write $\tt \toLLp \ttt$ if $\tt$ rewrites to~$\ttt$ with respect to~$\RLLp$. Now assume $\tt \toLLp \ttt$ and $\tt \toLLp \tttt$. By Proposition~\ref{P:Basic}, there exist~$\ff, \gg$ in~$\GGLLp$ satisfying $\ttt = \tt \act \ff$ and $\tttt = \tt \act \gg$. By Proposition~\ref{P:Mult}, there exist~$\ff', \gg'$ in~$\GGLLp$ satisfying $\ff \comp \gg' = \gg \comp \ff'$ and such that the domain of $\ff \comp \gg'$ is the intersection of the domains of~$\ff$ and~$\gg$, hence contains~$\tt$. Then we have

1322: $$\ttt \act \gg' = \tt \act (\ff \comp \gg') = \tt \act (\gg \comp \ff') = \tttt \act \ff',$$

1323: \ie, letting $\ttttt = \tt \act (\ff \comp \gg')$, we have $\ttt \toLDp \ttttt$ and $\tttt \toLDp \ttttt$.

1324: \end{proof}

1325: 

1326: In good cases, Proposition~\ref{P:Mult} can be proved using the group~$\GLL$, or rather the positive monoid~$\GLLp$, and its presentation: here we denote by~$\GLLp$ the monoid generated by  generators~$\OOO\LL\a$ for~$\LL$ in~$\LLL$ and~$\a$ an address, subject to all confluence relations connecting the operators~$\OOOp\LL\a$ in~$\GGLL$, \ie, the monoid that admits, as a monoid, the same presentation as the group~$\GLL$. Optimally, we could expect that the possible existence of common right multiples in~$\GLLp$ implies the existence of common right multiples in~$\GGLLp$, in the strong form required in Proposition~\ref{P:Mult}. Always because of the empty operator, this need not be the case in general. Nevertheless, we have

1327: 

1328: \begin{prop}

1329: Assume that $\LLL$ consists of semi-linear laws, \ie, laws $\tm \to \tp$ with $\tm$ an injective term (no variable repeated), and $\GLLp$ admits common right multiples. Then $\GGLLp$ admits common right multiples and Proposition~\ref{P:Mult} applies.

1330: \end{prop}

1331: 

1332: \begin{proof}[Sketch of proof]

1333: Under the hypotheses, the empty operator does not appear in~$\GGLLp$, and it follows that $\GGLLp$ is a homomorphic image of~$\GLLp$. Thus every relation in~$\GLLp$ projects into a relation in~$\GGLLp$, and, in particular, common multiples in~$\GLLp$ induce common multiples in~$\GGLLp$.

1334: \end{proof}

1335: 

1336: So the question remains of proving the existence of common right multiples in the monoid~$\GLLp$. By hypothesis, we start with a presented monoid where the relations

1337: are of the form $\OOO\LL\a \cdot ... = \OOO\LLbis\b \cdot ...$, \ie, they assert the existence of some common right multiples, and what we need is to extend the result so as to show that any two elements of the monoid admit a common right multiple. This is easy if all relations in the presentation turns out to have length at most~$2$ for, in that case, an easy induction gives a common multiple of length at most~$p+q$ for any two elements that can be expressed by words of length~$p$ and~$q$. In more complicated cases---typically in the case of the $\LD$-law, where we have seen some confluence relations involve words of length~$3$ or~$4$, like $\SS\ea \SS1 \SS\ea = \SS1 \SS\ea \SS1 \SS0$---the method consists in finding a family of words~$X$ that includes all generators~$\OOO\LL\a$ and is closed under complement in the sense that, for all words~$u, v$ in~$X$, there exists $u', v'$ in~$X$ such that both $uv'$ and~$vu'$ represent a common right multiple of the elements of~$\GLLp$ represented by~$u$ and~$v$. For instance, this approach works for~$\LD$, but it is rather delicate and leads to an upper bound which, instead of~$p+q$ as above, is a tower of exponentials of height~$2^{p+q}$~\cite{Dgd}.

1338: 

1339: When one can prove that common (right) multiples exist in the monoid~$\GLLp$, and, that, in addition, the latter admits cancellation, then standard results \cite{CPr} guarantee that the group~$\GLL$ is a group of fractions for~$\GLLp$, and this turns out to be crucial in the study of~$\GLL$. Again, proving that $\GLLp$ is cancellative requires specific tools connected with the so-called word reversing method~\cite{Dgp}. In many good cases (self-distributivity, associativity, central duplication), one can show that the divisibility relation gives~$\GLLp$ the structure of a lattice---but this is beyond the scope of this paper.

1340: 

1341: \section{Summary}

1342: \label{S:Summary}

1343: 

1344: We thus showed how introducing by means of confluence relations an abstract group that is supposed to mimick the properties of the geometry monoid---hence of the initial rewrite system---and then internalizing terms in that group so as to transform the initial external action into an internal multiplication may allow to solve nontrivial questions about a given family of algebraic laws. 

1345: 

1346: In the case of non linear algebraic laws, \ie, when some variable is repeated at least twice, due to the problem of the empty operator, the geometry monoid is an intrinsically inconvenient object, and our approach for replacing it with a group is the only known one. Of course, one might consider other relations than the confluence relations. The latter proved to be suitable for the examples considered here, but different schemes might prove relevant for other identities: for instance, when commutativity is involved, the operators are involutive, and the associated relations $\OOO\LL\a^2 = 1$ are not confluence relations. In some cases, one can keep the principle of introducing the structure~$\GLL$ presented by the confluence relations in~$\GGLL$, but taking~$\GLL$ to be a monoid rather than a group: typically, this has to be done in the case of the {\it idempotency law} $x = xx$, as, in this case, confluence relations of the type

1347: $\OOOp\LL\ea \comp \OOOp\LL\ea = \OOOp\LL\ea \comp \OOOp\LL0 \comp \OOOp\LL1$ are satisfied, preventing $\GGLL$ from admitting left cancellation---see~\cite{Jed}. So we see that the methods described here require some flexibility in their application.

1348: 

1349: However, it should be possible to adapt all three main steps, namely introducing a monoid of partial operators, replacing it with a group using a presentation, and internalizing the rewrite system by representing the objects on which the initial action is defined by copies inside the group, to more general frameworks. An example is given in~\cite{Dhb} where algebraic laws are replaced with a more complicated action on terms (``twisted commutativity''); we think that more rewrite systems, possibly of a completely different type, could be investigated using similar tools.

1350:  

1351: \begin{thebibliography}{99}

1352: 

1353: \Reff Boo; R.\,Book; Thue systems as rewriting systems; J. Symb. Comput.; 3; 1987; 39--68.

1354: 

1355: \Ref Bri1; M.\,Brin; The algebra of strand splitting. I. A braided version of Thompson's

1356: group~$V$; arXiv math.GR/040642.

1357: 

1358: \Reff Bri2; M.\,Brin; The algebra of strand splitting. II. A presentation for the braid group

1359: on one strand; Intern. J. of Algebra and Computation; 16; 2006; 203--219.

1360: 

1361: \Reff CFP; J.W.\,Cannon, W.J.\,Floyd, \& W.R.\,Parry; Introductory notes on Richard Thompson's groups; Ens. Math.; 42; 1996; 215--257.

1362: 

1363: \Ref CPr; A.H.\,Clifford \& G.B. Preston; The Algebraic Theory of Semigroups, vol.~1; AMS Surveys {\bf 7}, (1961).

1364: 

1365: \Reff Coh; D.E.\,Cohen; String rewriting, a survey for group theorists. {\rm in G.A. Niblo, M.A.Roller eds., Geometric Group  Theory, vol.~1}; London Math. Soc. Lect. Note Ser.; 181; 1993; 37--47.

1366: 

1367: \Reff Dew; P.\,Dehornoy; Structural monoids associated to equational varieties; Proc. Amer. Math. Soc.; 117-2; 1993; 293--304.

1368: 

1369: \Reff Dfg; P.\,Dehornoy; The structure group for the associativity identity; J. Pure Appl. Algebra; 111; 1996; 59--82.

1370: 

1371: \Ref Dgd; P.\,Dehornoy; Braids and Self-Distributivity; Progress in Math. vol. 192, Birkh\"auser (2000).

1372: 

1373: \Reff Dgj; P.\,Dehornoy; Study of an identity; Alg. Universalis; 48; 2002; 223--248.

1374: 

1375: \Reff Dgp; P.\,Dehornoy; Complete positive group presentations; J. of Algebra; 268; 2003; 156--197.

1376: 

1377: \Reff Dhb; P. Dehornoy; Geometric presentations of Thompson's groups; J. Pure Appl. Algebra; 203; 2005; 1--44.

1378: 

1379: \Reff Dhe; P.\,Dehornoy; The group of parenthesized braids; Advances in Math.; 205; 2006; 354--409.

1380: 

1381: \Ref Dhj; P.\,Dehornoy; Free augmented LD-systems; arXiv: math.GR/0507196; J. Algebra \& Appl., in press.

1382: 

1383: \Ref DeJ; N.\,Dershowitz \& J.P.\,Jouannaud; Rewrite

1384: Systems; {\it in} Handbook of Theor. Comp. Sc. vol.~B, J.~van

1385: Leeuwen {\it ed.}, Elsevier (1994).

1386: 

1387: \Reff Hue; G.\,Huet; Confluent reductions: Abstract

1388: properties and applications to term rewriting systems;

1389: Journal of the ACM; 27; 1980; 797--821.

1390: 

1391: \Ref Jed; P.\,Jedlicka; Geometry monoid of left distributivity and left idempotency; J. Algebra and Discrete Math., in press.

1392: 

1393: \Ref Lrb; D.\,Larue; Left-distributive and left-distributive idempotent algebras; PhD Thesis, University of Colorado, Boulder (1994).

1394: 

1395: \Reff Mac; S.\,Mac Lane; Natural associativity and

1396: commutativity; Rice Univ. Studies; 49; 1963; 28--46

1397: 

1398: \Ref McT; R.\,McKenzie \& R.J.\,Thompson; An elementary

1399: construction of unsolvable word problems in group

1400: theory; {\it in } Word Problems, Boone \& {\it al.} eds., North

1401: Holland, Studies in Logic vol. 71 (1973).

1402: 

1403: \Ref Pat; A.\,Paterson; Groupoids, inverse semigroups, and

1404: their operator algebras; Progress in Math. vol.~170,

1405: Birkh\"auser (1998).

1406: 

1407: \Reff Rob; J.\,Robinson; A machine-oriented logic based on the resolution principle; J. of the ACM; 10; 1963; 163--174.

1408: 

1409: \Ref Tho; R.J.\,Thompson; Embeddings into finitely

1410: generated simple groups which preserve the word

1411: problem; in {\it Word problems II: The Oxford book}, S.I.

1412: Adjan \& {\it al.} eds., Studies in Logic vol.

1413: 95, North Holland (1980) 401--440.

1414: 

1415: \end{thebibliography}

1416: 

1417: \end{document}