English

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

Logic in Computer Science 2023-01-31 v1 Programming Languages

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.

Cite

@article{arxiv.2301.12556,
  title  = {A Log-Sensitive Encoding of Turing Machines in the $\lambda$-Calculus},
  author = {Beniamino Accattoli and Ugo Dal Lago and Gabriele Vanoni},
  journal= {arXiv preprint arXiv:2301.12556},
  year   = {2023}
}

Comments

arXiv admin note: substantial text overlap with arXiv:2203.00362

R2 v1 2026-06-28T08:25:40.890Z