arXiv subjects

James Clift

Publications and source records attributed to James Clift.

5 recordsLinked to original sources

arXiv2021

Geometry of Program Synthesis

We re-evaluate universal computation based on the synthesis of Turing machines. This leads to a view of programs as singularities of analytic varieties or, equivalently, as phases of the Bayesian posterior of a synthesis problem. This new point of view reveals unexplored directions of research in program synthesis, of which neural networks are a subset, for example in relation to phase transitions, complexity and generalisation. We also lay the empirical foundations for these new directions by reporting on our implementation in code of some simple experiments.

cs.LG↗

arXiv2019

Logic and the $2$-Simplicial Transformer

We introduce the $2$-simplicial Transformer, an extension of the Transformer which includes a form of higher-dimensional attention generalising the dot-product attention, and uses this attention to update entity representations with tensor products of value vectors. We show that this architecture is a useful inductive bias for logical reasoning in the context of deep reinforcement learning.

cs.LG↗

arXiv2018

Derivatives of Turing machines in Linear Logic

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.

math.LO↗

arXiv2018

Encodings of Turing machines in Linear Logic

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.

math.LO↗

arXiv2017

Cofree coalgebras and differential linear logic

We prove that the semantics of intuitionistic linear logic in vector spaces which uses cofree coalgebras is also a model of differential linear logic, and that the Cartesian closed category of cofree coalgebras is a model of the simply-typed differential lambda calculus.

cs.LO↗