Encodings of Turing machines in linear logic

DOI10.1017/S0960129520000109MaRDI QIDQ5139286zbMATH OpenOpenAlexFDO

Authors James Clift, Daniel Murfet

Publication date 8 December 2020

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1805.10770

zbMATH Keywords

differential linear logiclinear logicTuring machines

Mathematics Subject Classification ID

Turing machines and related notions (03D10) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Categorical aspects of linear logic (18M45) Classical models of computation (Turing machines, etc.) (68Q04)

Abstract: We give several different encodings of the step function of a Turing machine in intuitionistic linear logic, and calculate the denotations of these encodings in the Sweedler semantics.

Recommendations

• Cofree coalgebras and differential linear logic
• Mackey-complete spaces and power series -- a topological model of differential linear logic
• An introduction to differential linear logic: proof-nets, models and antiderivatives
• Linear Läuchli semantics
• Functional interpretations of intuitionistic linear logic

Cites work

• An introduction to differential linear logic: proof-nets, models and antiderivatives
• Categorical semantics of linear logic
• Computational Complexity
• Computing Khovanov-Rozansky homology and defect fusion
• Glueing and orthogonality for models of linear logic
• scientific article; zbMATH DE number 5595162 (Why is no real title available?)
• scientific article; zbMATH DE number 512773 (Why is no real title available?)
• scientific article; zbMATH DE number 1544074 (Why is no real title available?)
• scientific article; zbMATH DE number 1424054 (Why is no real title available?)
• scientific article; zbMATH DE number 3309240 (Why is no real title available?)
• Light linear logic
• Linear logic
• On Computable Numbers, with an Application to the Entscheidungsproblem
• On Sweedler's cofree cocommutative coalgebra.
• On the computational complexity of cut-elimination in linear logic.
• Polynomial identity rings.
• Small universal Turing machines
• The differential lambda-calculus

Cited in

(5)

• A coding theorem for enumerable output machines
• scientific article; zbMATH DE number 786490 (Why is no real title available?)
• scientific article; zbMATH DE number 7167584 (Why is no real title available?)
• HOLL: program synthesis for higher order logic locking
• Linear logic and the Hilbert scheme

This page was built for publication: Encodings of Turing machines in linear logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5139286)