Table of Contents
Fetching ...

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

Eilene Tomkins-Flanagan, Connor Hanley, Mary A. Kelly

TL;DR

Doug is a vector-symbolic Lisp representation of the Light Linear Functional Programming Language (LLFPL) designed to ensure that all typed programs halt in polynomial time. By encoding LLFPL types via HDM's slot-value memory within a VSA, and by treating type surface as differentiable in a neural embedding, the approach aims to make type structure learnable and to guide program synthesis toward tractable searches. Doug leverages residue-number encodings and resonator networks to support arithmetic and accurate decoding of numeric components, while preserving structural similarity so nearby embeddings encode related types. The work argues that such learnable, constrained types can model human-like skill acquisition and substantially improve the efficiency and plausibility of intelligent systems performing program synthesis under cognitive constraints.

Abstract

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 (Schimanski2009, ch. 7). The types of Doug are encoded using a slot-value encoding scheme based on holographic declarative memory (HDM; Kelly, 2020). The terms of Doug are encoded using a variant of the Lisp VSA defined by (Flanagan, 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, 1983), and (Newell, 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, 2000), exceeding the efficiency of all currently existing approaches (Kaplan, 2020; 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.

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

TL;DR

Doug is a vector-symbolic Lisp representation of the Light Linear Functional Programming Language (LLFPL) designed to ensure that all typed programs halt in polynomial time. By encoding LLFPL types via HDM's slot-value memory within a VSA, and by treating type surface as differentiable in a neural embedding, the approach aims to make type structure learnable and to guide program synthesis toward tractable searches. Doug leverages residue-number encodings and resonator networks to support arithmetic and accurate decoding of numeric components, while preserving structural similarity so nearby embeddings encode related types. The work argues that such learnable, constrained types can model human-like skill acquisition and substantially improve the efficiency and plausibility of intelligent systems performing program synthesis under cognitive constraints.

Abstract

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 (Schimanski2009, ch. 7). The types of Doug are encoded using a slot-value encoding scheme based on holographic declarative memory (HDM; Kelly, 2020). The terms of Doug are encoded using a variant of the Lisp VSA defined by (Flanagan, 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, 1983), and (Newell, 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, 2000), exceeding the efficiency of all currently existing approaches (Kaplan, 2020; 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.
Paper Structure (12 sections, 9 equations)

This paper contains 12 sections, 9 equations.

Theorems & Definitions (6)

  • Definition 1: Types of LLFPL; Levels of types
  • Definition 2: The constants of LLFPL
  • Definition 3: Terms of LLFPL
  • Definition 4: Doug Types
  • Definition 5: Doug Constants
  • Definition 6: Doug Terms