A Log-Sensitive Encoding of Turing Machines in the $\lambda$-Calculus

TL;DR

This paper adapts the lambda-calculus encoding of Turing machines to efficiently model logarithmic space by introducing a two-tape system and a modified input tape encoding, improving space management for complexity analysis.

Contribution

It presents a modified encoding of Turing machines in the lambda-calculus optimized for logarithmic space, with a two-tape model and a new input tape encoding.

Findings

Encoding supports logarithmic space analysis

Two-tape model reduces space overhead

Enhanced encoding improves complexity classification

Abstract

This note modifies the reference encoding of Turing machines in the $\lambda$-calculus by Dal Lago and Accattoli, which is tuned for time efficiency, as to accommodate logarithmic space. There are two main changes: Turing machines now have *two* tapes, an input tape and a work tape, and the input tape is encoded differently, because the reference encoding comes with a linear space overhead for managing tapes, which is excessive for studying logarithmic space.