一句话：借助基于合一的代数与线性逻辑/交互几何，给出 Logspace 与 Nlogspace 的代数刻画，并联系指针机。
本文从证明论出发，尤其是线性逻辑与交互几何（geometry of interaction），提出一种以合一（unification）为复合运算的代数，用以刻画复杂度类 Logspace 与 Nlogspace。作者在该合一代数中构造计算模型，并通过在代数内对有限置换的语法表示，证明一个观察（即程序在代数中的对应物）是否接受某输入词可在对数空间内判定。最后说明该构造自然对应于指针机（pointer machine），为理解对数空间计算提供了直观而统一的代数视角。
We present an algebraic characterization of the complexity classes Logspace and Nlogspace, using an algebra with a composition law based on unification. This new bridge between unification and complexity classes is rooted in proof theory and more specifically linear logic and geometry of interaction. We show how to build a model of computation in the unification algebra and then, by means of a syntactic representation of finite permutations in the algebra, we prove that whether an observation (the algebraic counterpart of a program) accepts a word can be decided within logarithmic space. Finally, we show that the construction naturally corresponds to pointer machines, a convenient way of understanding logarithmic space computation.Comment: arXiv admin note: text overlap with arXiv:1402.4327