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

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

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 e…