From: Thomas Walker Lynch Date: Wed, 17 Jun 2026 14:20:21 +0000 (+0000) Subject: doc checkpoint X-Git-Url: https://git.reasoningtechnology.com/%27%20%20%20resolved_path%20%20%20%27?a=commitdiff_plain;h=refs%2Fheads%2Fcore-developer_branch;p=TM-2026 doc checkpoint --- diff --git a/document/TM-2026.html b/document/TM-2026.html index b1f8adc..dfc6d2a 100644 --- a/document/TM-2026.html +++ b/document/TM-2026.html @@ -21,23 +21,23 @@ This is the first volume of the book Tom's Turing Complete Computer Architecture, 'TTCA' book. The initial chapters set down the theory of the TM, Tape Machine. Following the theory chapters is a description of a software library for using the TM as a general iterator and container. The TM software library was released with the first edition of this volume in 2022, written in Common Lisp, and placed on MELPA. Since then, ad hoc versions were developed in C, Java, and Python. The TM-2026 GitHub project has as its purpose unifying the various language versions with a revised command language. The larger objective of these volumes is to morph the Turing Machine into a modern architecture, thus bridging computation theory to computing. The TM software library is a useful fallout of this work.

-

Introduction

+

Introduction

- In 1893 Gottlob Frege published an axiomatic construction of mathematics from set theory. Frege's grand objective was somethign he called Logicism, the philosophical thesis that all of mathematics can be derived entirely from pure logic. To achieve this, his specific machinery relied upon unrestricted set comprehension, formalized as Basic Law V . + In 1893 Gottlob Frege published an axiomatic construction of mathematics from set theory. Frege's grand objective was something he called Logicism, the philosophical thesis that all of mathematics can be derived entirely from pure logic. To achieve this, his specific machinery relied upon unrestricted set comprehension, formalized as Basic Law V .

- At a conference in Paris in 1900 David Hilbert presented a list of pressing unsolved problems in mathematics. - Second on his list was "The Compatibility of the Arithmetical Axioms," Hilbert challenged mathematicians to find a means to demonstrate that "a finite number of logical steps based upon them [axioms] can never lead to contradictory results" . + At a conference in Paris in 1900, David Hilbert presented a list of pressing unsolved problems in mathematics. + Second on his list was "The Compatibility of the Arithmetical Axioms." Hilbert challenged mathematicians to find a means to demonstrate that "a finite number of logical steps based upon them [axioms] can never lead to contradictory results" .

- In 1901 Bertrand Russell discovered a paradox in Frege's machinery. The paradox Russell pointed out was the well-formed formula that defined the set of all sets that do not contain themselves, and the question of whether such a set contained itself . Russel communicated this to Frege in a letter dated 1902-06-16, shortly before his second volume was going to print . Frege hurriedly author an appendix (the Nachwort) admitting his system was compromised. . + In 1901 Bertrand Russell discovered a paradox in Frege's machinery. The paradox Russell pointed out was the well-formed formula that defined the set of all sets that do not contain themselves, and the question of whether such a set contained itself . Russell communicated this to Frege in a letter dated 1902-06-16, shortly before his second volume was going to print . Frege hurriedly authored an appendix (the Nachwort) admitting his system was compromised .

- In 1903 Russell proposed a modification to set theory based on a hierarchy of types to repair this foundational vulnerability. At the base were sets of individuals, then sets based on individuals or sets of individuals, etc. This looks a lot like how types work in modern software . In this manner it is not possible to write a paradoxical set definition. Russell and Alfred North Whitehead then engineered an entirely new, massive architectural scaffolding utilizing this type system to pursue Frege's original objective of deriving mathematics from logic, publishing their results in three volumes between 1910 and 1913 . + In 1903 Russell proposed a modification to set theory based on a hierarchy of types to repair this foundational vulnerability. At the base were sets of individuals, then sets based on individuals or sets of individuals, etc. This looks a lot like how types work in modern software . In this manner, it is not possible to write a paradoxical set definition. Russell and Alfred North Whitehead then engineered an entirely new, massive architectural scaffolding utilizing this type system to pursue Frege's original objective of deriving mathematics from logic, publishing their results in three volumes between 1910 and 1913 .

@@ -45,7 +45,7 @@

- In 1928 David Hilbert and Wilhelm Ackermann published a textbook on mathematical logic, Grundzüge der theoretischen Logik . A feature of this book is its attention on procedures to follow for mechanically determining truth of statements. They called the problem solved by such a procedure the Entscheidungsproblem. In the first chapter they review the procedure for solving the Entscheidungsproblem in the propositional logic. For the first order predicate calculus they define the problem as, "Universal validity concerns the following question: How can one determine, for any given logical expression that contains no individual signs [constants], whether the expression represents a true assertion for arbitrary substitutions for the occurring variables, or not?" . They review some special cases with solutions, including one published earlier by Ackermann, but then throw down the gauntlet by saying, + In 1928 David Hilbert and Wilhelm Ackermann published a textbook on mathematical logic, Grundzüge der theoretischen Logik . A feature of this book is its attention to procedures to follow for mechanically determining truth of statements. They called the problem solved by such a procedure the Entscheidungsproblem. In the first chapter they review the procedure for solving the Entscheidungsproblem in the propositional logic. For the first order predicate calculus they define the problem as, "Universal validity concerns the following question: How can one determine, for any given logical expression that contains no individual signs [constants], whether the expression represents a true assertion for arbitrary substitutions for the occurring variables, or not?" . They review some special cases with solutions, including one published earlier by Ackermann, but then throw down the gauntlet by saying, "A general solution to the Entscheidungsproblem, regardless of whether a person considers the first or the second formulation, is not yet available." .

@@ -54,7 +54,7 @@

- In April 1936, Alonzo Church leveraged Gödel's foundational papers to directly answer the Entscheidungsproblem . Working independently, Alan Turing had arrived at his own mechanical solution and upon seeing Church's April publication, Turing rushed to submit his manuscript on 28 May 1936, appending a proof that his mechanical architecture was mathematically equivalent to Church's lambda calculus . As Hilbert and Ackermann concede in the 1938 second edition of their textbook, Church's results demonstrated that "the quest for a general solution of the decision problem must be regarded as hopeless" . By giving the "somewhat vague intuitive concept of recursion a certain precise formalization," Church proved the "non-existence of such a recursive procedure" that could mechanically yield a value of truth or falsehood for every individual formula . With this proof, Church established the absolute logical boundary of formal mathematics. + In April 1936, Alonzo Church leveraged Gödel's foundational papers to directly answer the Entscheidungsproblem . Working independently, Alan Turing had arrived at his own mechanical solution, and upon seeing Church's April publication, Turing rushed to submit his manuscript on 28 May 1936, appending a proof that his mechanical architecture was mathematically equivalent to Church's lambda calculus . As Hilbert and Ackermann concede in the 1938 second edition of their textbook, Church's results demonstrated that "the quest for a general solution of the decision problem must be regarded as hopeless" . By giving the "somewhat vague intuitive concept of recursion a certain precise formalization," Church proved the "non-existence of such a recursive procedure" that could mechanically yield a value of truth or falsehood for every individual formula . With this proof, Church established the absolute logical boundary of formal mathematics.

@@ -62,7 +62,7 @@

- While Gödel, Church, and Turing established the primary boundaries of computation, they did not work in a vacuum. During this period the broader academic community worked to synthesize the definitive mechanics of effective calculability. Jacques Herbrand and Gödel formalized general recursive functions between 1931 and 1934 . Emil Post independently defined "Finite Combinatory Processes" in 1936, outlining a theoretical architecture functionally identical to Turing's model . Stephen Kleene subsequently unified these disparate threads, proving the strict mathematical equivalence of Church's lambda calculus, Herbrand-Gödel recursive functions, and Turing's mechanical architectures . + While Gödel, Church, and Turing established the primary boundaries of computation, they did not work in a vacuum. During this period, the broader academic community worked to synthesize the definitive mechanics of effective calculability. Jacques Herbrand and Gödel formalized general recursive functions between 1931 and 1934 . Emil Post independently defined "Finite Combinatory Processes" in 1936, outlining a theoretical architecture functionally identical to Turing's model . Stephen Kleene subsequently unified these disparate threads, proving the strict mathematical equivalence of Church's lambda calculus, Herbrand-Gödel recursive functions, and Turing's mechanical architectures .

@@ -74,20 +74,20 @@

- For Turing's purposes working on the Entscheidungsproblem, establishing functional equivalence between algorithms and Turing Machine programs was sufficient. However, when the Turing Machine serves as a foundational model for computation theory, we are lead to ask another question, if the Turing Machine is representative of modern architectures. And to the extent it is different, how would this effect the applicability of compu-theoretic results. + For Turing's purposes working on the Entscheidungsproblem, establishing functional equivalence between algorithms and Turing Machine programs was sufficient. However, when the Turing Machine serves as a foundational model for computation theory, we are led to ask another question: whether the Turing Machine is representative of modern architectures, and to the extent it differs, how this would affect the applicability of computation-theoretic results.

In reading Alan Turing's 1936 paper, it is striking how modern the text feels, specifically because he discusses algorithms, stored programs, and the mechanical limits of computation. - While his contemporaries largely built purely mathematical and logical frameworks, Turing uniquely tied computation theory directly to the abstraction of machines executing stored programs. Because physical hardware capable of executing stored memory programs had not yet been invented, this explicit architectural grounding makes Turing's work remarkably prescient. Still, Turing could not formally connect the Turing Machine to modern architectures, simply because those architectures did not yet exist. Here, by modern, I refer to architectures utilizing random-access system memory, dedicated instruction fetch streams with dynamic branching, and discrete processing units. Though Charles Babbage's 1842 Analytical Engine touched on these concepts, they would wait until the 1940s to re-emerge. The practical engineering context of 1936 was limited to calculating machines programmed via patch panels. Hence, for example, there is no explanation in his paper as to why a von Neumann architecture machine (1945) running a program would exhibit the computation theoretic results derived from a computation theory based on the Turing Machine (1936). + While his contemporaries largely built purely mathematical and logical frameworks, Turing uniquely tied computation theory directly to the abstraction of machines executing stored programs. Because physical hardware capable of executing stored memory programs had not yet been invented, this explicit architectural grounding makes Turing's work remarkably prescient. Still, Turing could not formally connect the Turing Machine to modern architectures, simply because those architectures did not yet exist. Here, by modern, I refer to architectures utilizing random-access system memory, dedicated instruction fetch streams with dynamic branching, and discrete processing units. Though Charles Babbage's 1842 Analytical Engine touched on these concepts, they would wait until the 1940s to reemerge. The practical engineering context of 1936 was limited to calculating machines programmed via patch panels. Hence, for example, there is no explanation in his paper as to why a von Neumann architecture machine (1945) running a program would exhibit the computation-theoretic results derived from a computation theory based on the Turing Machine (1936).

- To establish the missing connection to modern architecture, the volumes of the TTCA, starting in the following chapters, transform the Turing Machine into a modern architecture in a stepwise fashion, while ensuring that at each step the modifications are inconsequential to computational theoretic existence proofs and complexity class results. We do run into some problems, so the architecture we derive will be a little different than those that we are currently building. + To establish the missing connection to modern architecture, the volumes of the TTCA, starting in the following chapters, transform the Turing Machine into a modern architecture in a stepwise fashion, while ensuring that at each step the modifications are inconsequential to computation-theoretic existence proofs and complexity class results. We do run into some problems, so the architecture we derive will be a little different from those we currently build.

- The infinite tape is not as large of a hurdle as it might seem at first. For computational problems the Turing Machine halts in a finite number of steps. Because the Turing Machine is limited to stepping the read/write head over one cell per machine execution step, in a finite number of steps, only a finite amount of tape is ever used. But for a given computation, how much tape is that? Resolving this by assuming more tape is simply attached when needed is analogous to cheating in a 'guess the bigger number' game by declaring, "My number is always one bigger than the given number, so I will tell you my guess after you state your number." Some mathematicians suggest that what is meant by infinity is precisely a rule of this sort. For engineers building physical hardware, however, to state that a resource starts finite and expands incrementally over time is a very different proposition than being asked to install infinite memory on a machine in the first place. + The infinite tape is not as large of a hurdle as it might seem at first. For computational problems, the Turing Machine halts in a finite number of steps. Because the Turing Machine is limited to stepping the read/write head over one cell per machine execution step, in a finite number of steps, only a finite amount of tape is ever used. But for a given computation, how much tape is that? Resolving this by assuming more tape is simply attached when needed is analogous to cheating in a 'guess the bigger number' game by declaring, "My number is always one bigger than the given number, so I will tell you my guess after you state your number." Some mathematicians suggest that what is meant by infinity is precisely a rule of this sort. For engineers building physical hardware, however, to state that a resource starts finite and expands incrementally over time is a very different proposition than being asked to install infinite memory on a machine in the first place.

@@ -104,8 +104,7 @@ - -

The computer design abstraction stack

+

The computer design abstraction stack

The six levels