Основные понятия
The AuDaLa programming language, which follows the data autonomous paradigm, is proven to be Turing complete by implementing a Turing machine in AuDaLa.
Аннотация
The paper presents the implementation of a Turing machine in the AuDaLa programming language and proves that this implementation is correct, thereby establishing that AuDaLa is Turing complete.
Key highlights:
- AuDaLa is a recently introduced programming language that follows the data autonomous paradigm, where small pieces of data execute functions autonomously.
- The authors implement a Turing machine in AuDaLa and provide a detailed proof of the correctness of this implementation.
- The proof involves establishing an equivalence between the configurations of a Turing machine and the configurations that can be extracted from the semantics of the corresponding AuDaLa program.
- The authors leverage the deterministic nature of AuDaLa steps and the absence of read-write data races to prove the correctness of the Turing machine implementation.
- The proof lays the foundation for proving the correctness of AuDaLa programs in general, by providing detailed reasoning about the semantics and inference rules of the language.
- The authors conclude that AuDaLa is Turing complete, which indicates the expressiveness of the data-autonomous paradigm.
Статистика
The Turing machine is defined as a 7-tuple T = (Q, q0, F, Γ, Σ, B, δ), where:
Q is the finite set of control states
q0 is the initial state
F is the set of accepting states
Γ is the set of tape symbols
Σ is the finite set of input symbols
B is the blank symbol
δ is the partial transition function
Цитаты
"AuDaLa is a recently introduced programming language that follows the new data autonomous paradigm. In this paradigm, small pieces of data execute functions autonomously."
"To prove AuDaLa's expressiveness, we prove AuDaLa Turing complete. We do this by implementing a Turing machine in AuDaLa (Section 2.2)."
"Constructing this implementation to exhibit correct behaviour is intricate due to AuDaLa's view on the behaviour of data elements and proofs (specifically those in Appendix A) involve detailed reasoning about the semantics and the inference rules defined in it and lay the foundation for proving AuDaLa programs correct."