Hey Pentti, We Did It Again!: Differentiable vector-symbolic types that prove polynomial termination

We present a typed computer language, Doug, in which all typed programs may be proved to halt in polynomial time, encoded in a vector-symbolic architecture (VSA). Doug is just an encoding of the light linear functional programming language (LLFPL) described by Schimanski (2009, ch. 7). The types of Doug are encoded using the slot-value encoding scheme of holographic declarative memory (HDM; Kelly, Arora, West, & Reitter, 2020). The terms of Doug are encoded using a variant of the Lisp VSA defined by Tomkins-Flanagan and Kelly (2024). Doug allows for some points on the embedding space of a neural network to be interpreted as types, where the types of nearby points are similar both in structure and content. Types in Doug are therefore learnable by a neural network. Following Chollet (2019), Card, Moran, and Newell (1983), and Newell and Rosenbloom (1981), we view skill as the application of a procedure, or program of action, that causes a goal to be satisfied. Skill acquisition may therefore be expressed as program synthesis. Using Doug, we hope to describe a form of learning of skilled behaviour that follows a human-like pace of skill acquisition (i.e., substantially faster than brute force; Heathcote, Brown, & Mewhort, 2000), exceeding the efficiency of all currently existing approaches (Kaplan et al., 2020; A. L. Jones, 2021; Chollet, 2024). Our approach brings us one step closer to modeling human mental representations, as they must actually exist in the brain, and those representations’ acquisition, as they are actually learned.