AuDaLa is Turing Complete
Tom T. P. Franken, Thomas Neele
TL;DR
This work addresses the expressiveness of the data-autonomous language AuDaLa by showing it can simulate a Turing machine, thereby proving Turing completeness. It introduces a concrete AuDaLa encoding of a TM using TapeCell and Control structures and guides the verification through a semantic mapping between AuDaLa implementation configurations and TM configurations, supported by auxiliary lemmas. The main contribution is establishing a formal bridge between AuDaLa's data-centric execution model and classical computability theory, enabling verification of AuDaLa programs. Future work aims to generalize the approach to a full system and to accommodate weak memory semantics.
Abstract
AuDaLa is a recently introduced programming language that follows the new data autonomous paradigm. In this paradigm, small pieces of data execute functions autonomously. Considering the paradigm and the design choices of AuDaLa, it is interesting to determine the expressiveness of the language and to create verification methods for it. In this paper, we take our first steps to such a verification method by implementing Turing machines in AuDaLa and proving that implementation correct. This also proves that AuDaLa is Turing complete.