Solution (source code)

= Solution

A <logspace transducer> is a deterministic <Turing machine> with a read-only <input> tape, $O(\log(n+2))$ read-write work space, and a write-only output tape. It emits symbols successively and cannot reread the output; that output is not charged as working memory. For a total function it must halt on every <input>. A <logspace-computable function> $f$ is a total <function> whose output $f(x)$ is produced by such a <logspace transducer> on <input> $x$.

A <logspace many-one reduction> $A\leq_m^{\log}B$ is a <logspace-computable function> $f$ such that
$$
\boxed{x\in A\quad\Longleftrightarrow\quad f(x)\in B}
$$
for every <string> $x$. The <logarithmic space> bound permits a <polynomial>-length output, even when that output does not fit in work space. Indeed, a halting <logspace transducer> cannot repeat its state, <input>-head position and work-tape contents and head positions: the unreadable output cannot affect its subsequent behaviour. There are only a <polynomial> number of such internal <Turing machine configurations>, hence a <polynomial> bound on the number of steps and output symbols.

To prove a <formal language> $B$ is <NL-complete>, first give an <NL> acceptance procedure for $B$. Then show every $A\in\mathrm{NL}$ has a <logspace many-one reduction> to $B$. Alternatively, reduce one already <NL-complete> <formal language> to $B$, using transitivity of <logspace many-one reductions>.

Transitivity requires <logspace composition by recomputation>, rather than storing the intermediate output. To compose $g$ with $f$, simulate the <logspace transducer> for $g$ with a virtual <input> $f(x)$. Retain its virtual <input>-head position in $O(\log n)$ <bits>. Whenever it asks for a symbol, rerun the <logspace transducer> for $f$ from the beginning and count its output symbols until that position is reached. Since $|f(x)|$ is <polynomial> in $n$, the simulated work space $O(\log|f(x)|)$ and all output-position counters are $O(\log n)$. Repeated runs reuse their storage. This proves closure under composition and explains why the hardness argument works.