Derivatives of Turing machines in Linear Logic

Abstract

We calculate denotations under the Sweedler semantics of the Ehrhard-Regnier derivatives of various encodings of Turing machines into linear logic. We show that these derivatives calculate the rate of change of probabilities naturally arising in the Sweedler semantics of linear logic proofs. The resulting theory is applied to the problem of synthesising Turing machines by gradient descent.

62 pages, moved the section on naive Bayesian observers earlier (Section 6.2) with slight changes to notation, references added in the introduction to Section 7 and related work in Remark 7.16