Journal article

Encodings of Turing machines in linear logic

James Clift, Daniel Murfet

Mathematical Structures in Computer Science | CAMBRIDGE UNIV PRESS | Published : 2020


The Sweedler semantics of intuitionistic differential linear logic takes values in the category of vector spaces, using the cofree cocommutative coalgebra to interpret the exponential and primitive elements to interpret the differential structure. In this paper, we explicitly compute the denotations under this semantics of an interesting class of proofs in linear logic, introduced by Girard: the encodings of step functions of Turing machines. Along the way we prove some useful technical results about linear independence of denotations of Church numerals and binary integers.

University of Melbourne Researchers