(************** Content-type: application/mathematica ************** CreatedBy='Mathematica 5.2' Mathematica-Compatible Notebook This notebook can be used with any Mathematica-compatible application, such as Mathematica, MathReader or Publicon. The data for the notebook starts with the line containing stars above. To get the notebook into a Mathematica-compatible application, do one of the following: * Save the data starting with the line of stars above into a file with a name ending in .nb, then open the file inside the application; * Copy the data starting with the line of stars above to the clipboard, then use the Paste menu command inside the application. Data for notebooks contains only printable 7-bit ASCII and can be sent directly in email or through ftp in text mode. Newlines can be CR, LF or CRLF (Unix, Macintosh or MS-DOS style). NOTE: If you modify the data for this notebook not in a Mathematica- compatible application, you must delete the line below containing the word CacheID, otherwise Mathematica-compatible applications may try to use invalid cache data. For more information on notebooks and Mathematica-compatible applications, contact Wolfram Research: web: http://www.wolfram.com email: info@wolfram.com phone: +1-217-398-0700 (U.S.) Notebook reader applications are available free of charge from Wolfram Research. *******************************************************************) (*CacheID: 232*) (*NotebookFileLineBreakTest NotebookFileLineBreakTest*) (*NotebookOptionsPosition[ 69686, 2112]*) (*NotebookOutlinePosition[ 70690, 2145]*) (* CellTagsIndexPosition[ 70646, 2141]*) (*WindowFrame->Normal*) Notebook[{ Cell[CellGroupData[{ Cell["Computing the Uncomputable Rado Sigma Function", "Title"], Cell["\<\ An Automated,Symbolic Induction Prover for non-halting Turing \ Machines\ \>", "Subtitle"], Cell["Joachim Hertel", "Author"], Cell["\<\ 50 Main St, STE 1000 White Plains, NY,10606 jhertel@h-star.com\ \>", "TextAboutAuthor"], Cell[TextData[{ "It is a classic result of computability theory that there exist \ uncomputable functions.\nA prime example is Tibor Rado's [1] function \ \[Sum][n] (a.k.a. the Busy Beaver function) that measures the productivity of \ n-state, binary Turing Machines. Despite being uncomputable, one knows [6] \ exact values of \[Sum][n] for n=1,2,3,4 and a high lower bound for \ n=5:\[Sum][5]\[GreaterEqual] 4098 [7].\nTo compute the exact value of \ \[Sum][n] one has to decide the halting question for ", Cell[BoxData[ \(TraditionalForm\`\((4 n + 1)\)\^\(2 n\)\)]], " n-state binary Turing Machines. Fortunately, this huge number can be \ reduced by applying well-known techniques like Tree Normalization, Back \ Tracking and Simple Loop Detection [6].\nIn this talk we report about a new \ tool that is successfully used in an ongoing project to compute \[Sum][5]: an \ automated Symbolic Induction Prover (SIP). The SIP tool is written in ", StyleBox["Mathematica", FontSlant->"Italic"], " and provides a unified way to prove that large groups of Turing Machines \ are non-halters. In a way, SIP enable certain Turing Machines to provide \ their own proof of being a non-halter.\nWith few undecided TMs, we now have \ strong evidence that indeed \[Sum][5]=4098. Final results will be reported in \ a forthcoming report [8]." }], "Abstract"], Cell[CellGroupData[{ Cell["Introduction", "SectionFirst"], Cell[CellGroupData[{ Cell["About Rado's Uncomputable Sigma Function", "Subsection"], Cell[TextData[{ " There are too many functions from positive integers to positive \ integers for them all to be (Turing) computable. A Cantor diagonalization \ argument [2] shows, that the set of all such functions is nonenumerable, \ whereas the set of all Turing machines is denumerable [2]. Hence, there must \ exist functions that are uncomputable.\n In 1962, Tibor Rado [1] presented \ the uncomputable function \[CapitalSigma] (aka the Busy Beaver function). \ Roughly speaking, \[CapitalSigma](n) is the largest number of 1's left on the \ tape by a halting binary n-state Turing machine when started on an initially \ all 0-tape. The \[CapitalSigma] function is uncomputable, because otherwise \ it would solve the Halting problem [2], which is known to be undecidable [2]. \ Even more, Rado [1] proved, that \[CapitalSigma] grows faster than any \ computable function for large enough values of n, i.e. for any computable \ function f:\[DoubleStruckCapitalN]\[RightArrow]\[DoubleStruckCapitalN], it \ holds that \[Exists]", Cell[BoxData[ \(TraditionalForm\`\(\(k\_\(\(0\)\(\ \)\)\)\(\ \)\)\)]], "\[ForAll]k\[GreaterEqual]", Cell[BoxData[ \(TraditionalForm\`\(\(k\_\(\(0\)\(\ \)\)\)\(\ \)\)\)]], "f(k)<\[CapitalSigma](k). \n In 1964, Green [11] established general \ lower bounds for the \[CapitalSigma] function for larger values of n by \ explicitly constructing so-called Class M Turing machines, that generate long \ blocks of 1's. Julstrom [12] showed, that Green's Class M Turing machines are \ related to the Ackermann function [2], a function that is computable but not \ primitive recursive.\n Various computational-based approaches to making \ progress on the \[CapitalSigma] function have been taken: brute force \ searches,genetic algorithms,heuristic behavior analysis and many more [13] \ and the \[CapitalSigma] function has become a classic topic in the theory of \ computing [13]. See [16] for a comprehensive list of references on Rado's \ Sigma function.\n However, so far, exact values of \[CapitalSigma][n] have \ only been computed for n=1,2,3,4 (see [6,13]) : \[CapitalSigma][1]=1, \ \[CapitalSigma][2]=4, \[CapitalSigma][3]=6, \[CapitalSigma][4]=13. These \ values are the first elements of the A028444 sequence of integers in the \ On-Line Encyclopedia of Integers [14].\n In 1990, Marxen & Buntrock [7] \ established the lower bound \[CapitalSigma][5]\[GreaterEqual]4098, by \ publishing a record holding binary 5-state Turing machine, that halts after \ 47,176,870 steps and leaves 4098 1's on the tape.\n Michel [5], shows a \ connection of most of the known low n record holding Turing machines and the \ Collatz 3x+1 Problem.\n There are three other related uncomputable functions \ associated with binary n-state Turing Machines:\n Shift[n]:\tThe maximum \ number of moves of a halting binary n-state Turing Machine started on an all \ 0-tape.\n Num[n]:\tThe largest unary number that can be created by a \ halting binary n-state Turing Machine started on an \t\t all 0-tape.\n \ Space[n]:\tThe largest number of different tape cells scanned by a halting \ binary n-state Turing Machine started on \t\tan all 0-tape.\n \n \ Ben-Amram et al., [15] prove that Num[n] \[LessEqual] \[CapitalSigma][n] \ \[LessEqual] Space[n] \[LessEqual] Shift[n], \[ForAll]n. \t " }], "Text"] }, Open ]], Cell[CellGroupData[{ Cell["Why Compute Values of Sigma", "Subsection"], Cell["\<\ Chaitin [3] argues, that the \[CapitalSigma] function is of \ considerable metamathematical interest. According to Chaitin [3], let P be a \ computable predicate of a positive integer n, so that for any specific n it \ is possible to compute if P(n) is true or false. The Goldbach Conjecture is \ an example for P. The \[CapitalSigma] function provides a crucial upper \ bound, for if P has algorithmic information content [3] p ,it suffices to \ examine the first \[CapitalSigma](p) natural numbers to decide whether P is \ True or False for all natural numbers. Hence, the \[CapitalSigma] function \ enables one to convert a large but finite amount of calculations into a \ mathematical proof. Calculating \[CapitalSigma](n) for specific values of n \ thus amounts to a systematic effort to settle all finitely refutable \ mathematical conjectures, that is, to determine all constructive mathematical \ truth [3].\ \>", "Text"] }, Open ]], Cell[CellGroupData[{ Cell["Minds, Machines and Sigma", "Subsection"], Cell[TextData[{ StyleBox["There is an ongoing philosophical discussion whether the human \ mind can surpass the Turing Limit, or can be understood as a Turing Machine. \ The famous logician Kurt G\[ODoubleDot]del discusses his point of view that \ the Mind can indeed surpass the Turing Limit in conjunction with his well \ known Incompleteness Theorem, see [9]. G\[ODoubleDot]del states [9], that \ \[OpenCurlyDoubleQuote]", FontFamily->"Times New Roman"], StyleBox["although at each stage the number and precision of the abstract \ terms at our disposal may be finite, both may converge toward infinity in the \ course of the application of the procedure.", FontFamily->"Times New Roman", FontSlant->"Italic"], StyleBox["\[CloseCurlyDoubleQuote] Computing values of ", FontFamily->"Times New Roman"], "\[CapitalSigma][", StyleBox["n] for increasing n serves as a quantitative example for the \ situation G\[ODoubleDot]del is referring to in [9]. Indeed, Bringsjord et al. \ [4], present a ", FontFamily->"Times New Roman"], StyleBox["New G\[ODoubleDot]delian Argument for Hypercomputing Minds ", FontFamily->"Times New Roman", FontSlant->"Italic"], StyleBox["that is based on the ", FontFamily->"Times New Roman"], "\[CapitalSigma]", StyleBox[" function. In their argument the ", FontFamily->"Times New Roman"], "\[CapitalSigma]", StyleBox[" function provides a discrete way to measure the achievement of \ the human mind surpassing the Turing Limit and establishing new constructive \ mathematical truth. In [4] the core assumption is that if the human mind can \ compute ", FontFamily->"Times New Roman"], "\[CapitalSigma][", StyleBox["n] it also can compute ", FontFamily->"Times New Roman"], "\[CapitalSigma][", StyleBox["n+1], (although that advancement might take quite a long time). \n\ Experience from our ongoing project of computing ", FontFamily->"Times New Roman"], "\[CapitalSigma]", StyleBox[" for 5-state binary Turing Machines shows, that the halting \ question of large subsets of Turing Machines can be decided in a unified way \ using data mining to identify patterns and by the subsequent use of a ", FontFamily->"Times New Roman"], StyleBox["Symbolic Induction Prover ", FontFamily->"Times New Roman", FontSlant->"Italic"], StyleBox["(see next chapter)", FontFamily->"Times New Roman"], StyleBox[" ", FontFamily->"Times New Roman", FontSlant->"Italic"], StyleBox["to prove that these machines are infact non halters once they \ reach a certain pattern when started on an all 0-tape. If we succeed to \ identify an induction base (i.e., some pattern) we then can use the ", FontFamily->"Times New Roman"], StyleBox["Symbolic Induction Prover", FontFamily->"Times New Roman", FontSlant->"Italic"], StyleBox[" to operate as a kind of Meta-Turing Machine, enabling the \ underlying Turing Machine to create its own proof of being a non-halter. \ Nothing in that process is restricted to 5-state Turing Machines. Hence we \ can imagine to climb beyond n = 5. The main challenge becomes the data mining \ part of identifying suitable induction base steps for increasingly complex \ and \[OpenCurlyDoubleQuote]erratic\[CloseCurlyDoubleQuote] behavior of Turing \ Machines. \n\nWe now turn in more detail to the computation of ", FontFamily->"Times New Roman"], "\[CapitalSigma][", StyleBox["5] and to our main computational tool for that task, the ", FontFamily->"Times New Roman"], StyleBox["Symbolic Induction Prover", FontFamily->"Times New Roman", FontSlant->"Italic"], StyleBox[" for non-halting Turing Machines. ", FontFamily->"Times New Roman"], StyleBox["\n", FontSize->12] }], "Text"] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell["The Computation of Sigma for 5-State, Binary Turing Machines", "Section"], Cell[CellGroupData[{ Cell["Notations and Definitions ", "Subsection"], Cell[TextData[{ "Binary n-state Turing Machines conform to these conditions:\n\nThe tape is \ infinite in both directions\nThe tape alphabet is \[Sum]={0,1}\nThe all \ 0-tape is called the blank tape \[CapitalOmega]\nThe Turing Machine has n \ states, labeled 1,\[Ellipsis],n and a HALT state, labeled 0 \nAt each step \ the machine reads,writes the cell scanned by the Turing head and moves the \ Turing head one cell to the left/right\n\n\nHere, we focus on 5-state binary \ Turing Machines: \n\n", StyleBox["Definition", FontWeight->"Bold"], ": The instruction table of a 5-state binary Turing machine M is a 5-by-2 \ table such that M[s,h]: = {ws,mv,ns}, with s\[Element]{1,2,3,4,5}, \ h\[Element]{0,1},ws\[Element]{0,1}, mv\[Element]{L,R}, \ ns\[Element]{0,1,2,3,4,5}\n\n We call ", StyleBox["s", FontWeight->"Bold"], " the current state of M and ", StyleBox["h", FontWeight->"Bold"], " the read symbol in the tape cell positioned under the Turing head H. The \ triple {ws,mv,ns} is called a Turing instruction with ", StyleBox["ws", FontWeight->"Bold"], " the write symbol being written into the tape cell positioned under the \ Turing head H, ", StyleBox["mv", FontWeight->"Bold"], " the move direction of the Turing head H and ", StyleBox["ns", FontWeight->"Bold"], " the next state of M. If ns = 0, M stops, otherwise it continues executing \ instructions.\n Without loss of generality we assume the HALT instruction \ to be {1,R,0}. \n\n That leaves us with", Cell[BoxData[ \(TraditionalForm\`\(\(\ \)\(\((2*2*5 + 1)\)\^\(2*5\)\ = \ 21\^10\)\)\)]], " possible binary 5-state Turing machines. We call this finite set ", Cell[BoxData[ \(TraditionalForm\`\[ScriptCapitalT]\[ScriptCapitalM]\_5\)]], "." }], "Text"], Cell[BoxData[ RowBox[{\(Let\ M\), "\[Element]", RowBox[{ RowBox[{ FormBox[\(\(\ \)\(\[ScriptCapitalT]\[ScriptCapitalM]\_5\)\), "TraditionalForm"], ".", " ", \(M[\[CapitalOmega]]\)}], " ", "means", " ", "Turing", " ", "machine", " ", "M", " ", "is", " ", "started", " ", "on", " ", "tape", " ", \(\[CapitalOmega] . \ \[IndentingNewLine]\(\(Define\)\(:\)\)\)}]}]], "Text", PageBreakAbove->True, TextAlignment->Left, FontFamily->"Times New Roman"], Cell[BoxData[ StyleBox[ RowBox[{ FrameBox[ RowBox[{" ", RowBox[{\(\(\[Sigma] \((M)\)\)\(:\)\), " ", "=", " ", Cell[ BoxData[ FormBox[ TagBox[ RowBox[{"{", StyleBox[GridBox[{ {\(k\ \ \ \ \ \ \ M\ [\[CapitalOmega]]\ halts\ \ and\ leaves\ k\ 1' s\ on\ tape\)}, {\(\ 0\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ o\ therwise\)} }], ShowAutoStyles->True]}], (#&)], TraditionalForm]], "DisplayFormula"]}]}], BoxMargins->{{0.2, 0.2}, {0.4, 0.4}}], "\n"}], "DisplayFormula"]], "DisplayFormula", TextAlignment->Center], Cell[BoxData[ RowBox[{ RowBox[{ StyleBox["Example", FontWeight->"Bold"], ":", " ", \(M\_MB\)}], "=", StyleBox[ TagBox[ RowBox[{"(", "\[NoBreak]", GridBox[{ {\({1, R, 2}\), \({1, L, 3}\)}, {\({1, R, 3}\), \({1, R, 2}\)}, {\({1, R, 4}\), \({0, L, 5}\)}, {\({1, L, 1}\), \({1, L, 4}\)}, {\({1, R, 0}\), \({0, L, 1}\)} }, RowSpacings->1, ColumnSpacings->1, ColumnAlignments->{Left}], "\[NoBreak]", ")"}], Function[ BoxForm`e$, MatrixForm[ BoxForm`e$]]], "DisplayFormula"]}]], "DisplayFormula", TextAlignment->Left], Cell[BoxData[ RowBox[{"\[IndentingNewLine]", RowBox[{ RowBox[{ RowBox[{ StyleBox[\(M\_MB\ \ is\ a\ 5\), FontFamily->"Times New Roman"], StyleBox["-", FontFamily->"Times New Roman"], RowBox[{ StyleBox["stateTuring", FontFamily->"Times New Roman"], StyleBox[" ", FontFamily->"Times New Roman"], StyleBox["Machine", FontFamily->"Times New Roman"], StyleBox[" ", FontFamily->"Times New Roman"], StyleBox["first", FontFamily->"Times New Roman"], StyleBox[" ", FontFamily->"Times New Roman"], StyleBox["published", FontFamily->"Times New Roman"], StyleBox[" ", FontFamily->"Times New Roman"], StyleBox["by", FontFamily->"Times New Roman"], StyleBox[" ", FontFamily->"Times New Roman"], StyleBox["Marxen", FontFamily->"Times New Roman"], StyleBox[" ", FontFamily->"Times New Roman"], StyleBox["and", FontFamily->"Times New Roman"], StyleBox[" ", FontFamily->"Times New Roman"], RowBox[{ StyleBox[\(Buntrock\ [7]\), FontFamily->"Times New Roman"], StyleBox[" ", FontFamily->"Times New Roman"], StyleBox[".", FontFamily->"Times New Roman"], StyleBox["\[IndentingNewLine]", FontFamily->"Times New Roman"], StyleBox[" ", "Input", FontFamily->"Times New Roman"], StyleBox["\[IndentingNewLine]", FontFamily->"Times New Roman"], StyleBox[\(M\_MB[\[CapitalOmega]]\), FontFamily->"Times New Roman"]}], " ", StyleBox["halts", FontFamily->"Times New Roman"], StyleBox[" ", FontFamily->"Times New Roman"], StyleBox["after", FontFamily->"Times New Roman"], StyleBox[" ", FontFamily->"Times New Roman"], StyleBox["47", FontFamily->"Times New Roman"]}]}], StyleBox[",", FontFamily->"Times New Roman"], StyleBox["176", FontFamily->"Times New Roman"], StyleBox[",", FontFamily->"Times New Roman"], StyleBox[\(870 steps\ and\ leaves\ 4098\ 1 - symbols\ on\ the\ tape\), FontFamily->"Times New Roman"], StyleBox[",", FontFamily->"Times New Roman"], StyleBox[\(i . e . \), FontFamily->"Times New Roman"], StyleBox[",", FontFamily->"Times New Roman"], StyleBox[" ", FontFamily->"Times New Roman"], StyleBox[\(\[Sigma][M\_MB] = 4098. \), FontFamily->"Times New Roman"]}], StyleBox["\[IndentingNewLine]", FontFamily->"Times New Roman"]}]}]], "Text", PageWidth->WindowWidth, TextJustification->0, FontFamily->"Times New Roman"], Cell[BoxData[ FrameBox[ StyleBox[\(\(\[CapitalSigma][ 5]\)\(:=\)\(Max[{\[Sigma][M], M \[Element] \[ScriptCapitalJ]\[ScriptCapitalM]\_5}]\)\(\ \)\), FontWeight->"Bold"], BoxMargins->{{0.2, 0.2}, {0.4, 0.4}}]], "Text", TextAlignment->Center, FontFamily->"Times New Roman"], Cell[TextData[{ "Hence ", StyleBox["\[CapitalSigma][5]\[GreaterEqual]4098", FontWeight->"Bold"], ".\nOne has to solve the halting question for a finite,but large number of \ Turing machines to compute the value of \[CapitalSigma](5)." }], "Text", FontFamily->"Times New Roman"], Cell[CellGroupData[{ Cell["Configurations", "Subsubsection", TextAlignment->Left, FontFamily->"Times New Roman"], Cell[BoxData[{ StyleBox[\(\(Let\ denote\ \(\(\[Sum]\^*\)\ the\ set\ of\ finite\ words\ from\ alphabet\ \(\[Sum]\(\(.\)\(\ \[IndentingNewLine]\)\(\[IndentingNewLine]\)\(\ \)\(A\)\)\ machine\ \ configuration\ c\ \ is\ an\ expression\)\)\)\(\ \)\(\[IndentingNewLine]\) \), "Text"], "\[IndentingNewLine]", RowBox[{ RowBox[{ RowBox[{ StyleBox["c", "Text"], StyleBox["=", "Text"], RowBox[{ StyleBox["{", "Text"], RowBox[{ StyleBox["s", "Text", FontWeight->"Bold"], StyleBox[",", "Text"], RowBox[{ StyleBox["{", "Text"], RowBox[{ StyleBox["\[Omega]", "Text"], StyleBox[",", "Text"], StyleBox[\({{x}, 1}\), "Text"], StyleBox[",", "Text"], StyleBox["h", "Text", FontWeight->"Bold"], StyleBox[",", "Text"], StyleBox[\({{y}, 1}\), "Text"], StyleBox[",", "Text"], StyleBox["\[Omega]", "Text"]}], StyleBox["}", "Text"]}]}], StyleBox["}", "Text"]}]}], StyleBox[",", "Text"], RowBox[{ StyleBox["s", FontWeight->"Bold"], " ", "\[Epsilon]", " ", \({0, 1, 2, 3, 4, 5}\)}], ",", RowBox[{ StyleBox["h", FontWeight->"Bold"], " ", "\[Epsilon]", "\[Sum]"}], " ", ",", " ", "x", ",", \(y\ \[Epsilon] \(\(\[Sum]\^*\)\[IndentingNewLine]\ \[IndentingNewLine]\(Note : \ \[Omega]\ \ denotes\ the\ left/ right\ infinite\ blank\ portion\ of\ the\ tape\)\)\)}], "\[IndentingNewLine]"}], "\[IndentingNewLine]", RowBox[{ RowBox[{\(In\ this\ notation\ \ \[CapitalOmega]\), " ", "=", " ", RowBox[{ RowBox[{ RowBox[{ RowBox[{ StyleBox["{", "Text"], RowBox[{ StyleBox["\[Omega]", "Text"], StyleBox[",", "Text"], StyleBox["0", "Text", FontWeight->"Bold"], StyleBox[",", "Text"], StyleBox["\[Omega]", "Text"]}], StyleBox["}", "Text"]}], StyleBox[".", "Text"], StyleBox[" ", "Text"], StyleBox["\[IndentingNewLine]", "Text"], StyleBox["\[IndentingNewLine]", "Text"], StyleBox["We", "Text"]}], StyleBox[" ", "Text"], StyleBox["use", "Text"], StyleBox[" ", "Text"], StyleBox[\({{x}, n}\), "Text"]}], StyleBox[":=", "Text"], StyleBox[" ", "Text"], StyleBox[\({{\(x, \[Ellipsis], x\)\+\(n - times\)}, 1}\ for\ all\ x\[Epsilon] \(\(\[Sum]\^*\)\ to\ define\ symbolic\ configurations\ with\ multipliers\ \ n\) \[GreaterEqual] 1. \), "Text"]}]}], "\[IndentingNewLine]"}], "\[IndentingNewLine]", RowBox[{ RowBox[{ StyleBox["Example", "Text", FontWeight->"Bold"], StyleBox[":", "Text"], StyleBox[" ", "Text"], StyleBox["c", "Text"]}], StyleBox["=", "Text"], RowBox[{ StyleBox["{", "Text"], RowBox[{ StyleBox["s", "Text", FontWeight->"Bold"], StyleBox[",", "Text"], RowBox[{ StyleBox["{", "Text"], RowBox[{ StyleBox["\[Omega]", "Text"], StyleBox[",", "Text"], StyleBox[\({{x}, n}\), "Text"], StyleBox[",", "Text"], StyleBox["h", "Text", FontWeight->"Bold"], StyleBox[",", "Text"], StyleBox[\({{y}, m}\), "Text"], StyleBox[",", "Text"], StyleBox["\[Omega]", "Text"]}], StyleBox["}", "Text"]}]}], StyleBox["}", "Text"]}]}], "\[IndentingNewLine]", RowBox[{ RowBox[{ StyleBox["Example", FontWeight->"Bold"], ":", "c"}], "=", RowBox[{"{", RowBox[{ StyleBox["3", FontWeight->"Bold"], ",", RowBox[{"{", RowBox[{"\[Omega]", ",", StyleBox["0", FontWeight->"Bold"], ",", \({{1, 0, 1}, k}\), ",", "\[Omega]"}], "}"}]}], "}"}]}], "\n", RowBox[{ RowBox[{\(i . e . M\), " ", "is", " ", "in", " ", "state", " ", StyleBox["3", FontWeight->"Bold"]}], ",", \(the\ Turing\ head\ scans\ a\ 0 - cell\), ",", \(and\ the\ sub - tape\ {1, 0, 1}\ is\ occurring\ k - \(\(times\)\(.\)\)\)}]}], "Text", FontFamily->"Times New Roman"] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell["General Approach: Discover and Prove", "Subsection", PageBreakAbove->True], Cell["\<\ By using well-known techniques [6], such as Tree Normalization, \ Backtracking, Simple Loop Detection etc., one can decide the Halting question \ for many of the 5-state binary Turing Machines:\ \>", "Text"], Cell[TextData[{ Cell[BoxData[ \(TraditionalForm\`21\^10\)]], " possible 5-state binary Turing Machines ", Cell[BoxData[ FormBox[GridBox[{ {"\[DoubleLongRightArrow]"}, {\(apply\ known\ techniques\)} }], TraditionalForm]]], " \[TildeTilde] 1,000,000 undecided machines (\"Holdouts\")\n\nFor each \ of the remaining undecided Turing Machines do:\n\nIterate the holdout machine \ a \"number of times\", starting on the blank tape \[CapitalOmega]\nSave the \ configuration after each step\nTry to discover recurring patterns and store \ them as machine configurations\n\n", StyleBox["Examples", FontWeight->"Bold"], ":\n\n\t", Cell[BoxData[ \(TraditionalForm\`\(c\_L\)(n)\)]], " : ={", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{{(x},a*n+b},\[Omega]}},\tn\[GreaterEqual]0\n\t", Cell[BoxData[ \(TraditionalForm\`\(c\_R\)(n)\)]], " : ={", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],{{x},a*n+b},", StyleBox["h", FontWeight->"Bold"], ",\[Omega]}},\tn\[GreaterEqual]0\n\n\t", Cell[BoxData[ \(TraditionalForm\`\(c\_L\)(n)\)]], " : ={", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{{x},1},{{y},", Cell[BoxData[ \(TraditionalForm\`p\_n\)]], "},\[Omega]}},\tn\[GreaterEqual]0\n\t", Cell[BoxData[ \(TraditionalForm\`\(c\_R\)(n)\)]], " : ={", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],{{x},1},{{y},", Cell[BoxData[ \(TraditionalForm\`p\_n\)]], "},", StyleBox["h", FontWeight->"Bold"], ",\[Omega]}}, \tn\[GreaterEqual]0\n\nwith x,y \[Epsilon] ", Cell[BoxData[ \(TraditionalForm\`\(\(\[Sum]\^*\)\(\ \)\)\)]], "and the multiplier ", Cell[BoxData[ \(TraditionalForm\`p\_n\)]], " satisfying a recurrence relation ", Cell[BoxData[ \(TraditionalForm\`p\_\(n + 1\)\)]], " = a*", Cell[BoxData[ \(TraditionalForm\`p\_n\)]], " +b \n\nHere are some actual examples of configurations:\n\nA simple \ linear configuration: c(n) = {", StyleBox["2", FontWeight->"Bold"], ",{\[Omega],", StyleBox["0", FontWeight->"Bold"], ",{{1},4n}},\[Omega]}\n\nA simple exponential configuration: c(n) =", Cell[BoxData[ RowBox[{ StyleBox["{", FontFamily->"Times New Roman"], RowBox[{ StyleBox["1", FontFamily->"Times New Roman", FontWeight->"Bold"], StyleBox[",", FontFamily->"Times New Roman"], RowBox[{ StyleBox["{", FontFamily->"Times New Roman"], RowBox[{ StyleBox["\[Omega]", FontFamily->"Times New Roman"], StyleBox[",", FontFamily->"Times New Roman"], StyleBox["1", FontFamily->"Times New Roman", FontWeight->"Bold"], StyleBox[",", FontFamily->"Times New Roman"], StyleBox[\({{0}, 3\^\(\(\ \)\(n\)\)}\), FontFamily->"Times New Roman"], StyleBox[",", FontFamily->"Times New Roman"], StyleBox[\({{1}, 3}\), FontFamily->"Times New Roman"], StyleBox[",", FontFamily->"Times New Roman"], StyleBox["\[Omega]", FontFamily->"Times New Roman"]}], StyleBox["}", FontFamily->"Times New Roman"]}]}], StyleBox["}", FontFamily->"Times New Roman"]}]]], "\n\nA more complicated configuration:\nc(n) =", Cell[BoxData[ RowBox[{ StyleBox["{", FontFamily->"Times New Roman"], RowBox[{ StyleBox["1", FontFamily->"Times New Roman", FontWeight->"Bold"], StyleBox[",", FontFamily->"Times New Roman"], RowBox[{ StyleBox["{", FontFamily->"Times New Roman"], RowBox[{ StyleBox["\[Omega]", FontFamily->"Times New Roman"], StyleBox[",", FontFamily->"Times New Roman"], StyleBox["0", FontFamily->"Times New Roman", FontWeight->"Bold"], StyleBox[",", FontFamily->"Times New Roman"], StyleBox[\({{0, 0, 1}, 2\^\(2\ n + 1\)}\), FontFamily->"Times New Roman"], StyleBox[",", FontFamily->"Times New Roman"], StyleBox[\({{0, 1}, 3}\), FontFamily->"Times New Roman"], StyleBox[",", FontFamily->"Times New Roman"], StyleBox[\({{0, 0, 1}, 2\^\(2\ n - 1\)}\), FontFamily->"Times New Roman"], StyleBox[",", FontFamily->"Times New Roman"], StyleBox[\({{0, 1}, 3}\), FontFamily->"Times New Roman"], StyleBox[",", FontFamily->"Times New Roman"], "\[Ellipsis]", ",", StyleBox[\({{0, 0, 1}, 2\^3}\), FontFamily->"Times New Roman"], StyleBox[",", FontFamily->"Times New Roman"], StyleBox[\({{0, 1}, 3}\), FontFamily->"Times New Roman"], StyleBox[",", FontFamily->"Times New Roman"], StyleBox[\({{0, 0, 1}, 2\^1}\), FontFamily->"Times New Roman"], StyleBox[",", FontFamily->"Times New Roman"], StyleBox[\({{0, 1}, 3}\), FontFamily->"Times New Roman"], StyleBox[",", FontFamily->"Times New Roman"], StyleBox["\[Omega]", FontFamily->"Times New Roman"]}], StyleBox["}", FontFamily->"Times New Roman"]}]}], StyleBox["}", FontFamily->"Times New Roman"]}]]], "\n\nOnce we have identified a reliable hypothesis for a recurring \ configuration c(n) of a Turing Machine M we want to create an induction proof \ showing that M does indeed NOT halt.\nThe general scheme is as follows:\n\n", StyleBox["Step 1", FontWeight->"Bold"], ": Establish the Induction Proposition: M:\[CapitalOmega]\ \[DoubleLongRightArrow]c(n), \[ForAll]n\[GreaterEqual]0\n\t(i.e. M transforms \ the blank tape into c(n) in a countable number of steps)\n", StyleBox["Step 2", FontWeight->"Bold"], ": Verify the Base Case , i.e. check that M:\[CapitalOmega]\ \[DoubleLongRightArrow]c(n), n = 0 (or any finite number of n)\n", StyleBox["Step 3", FontWeight->"Bold"], ": Formulate the Induction Hypothesis, i.e. assume that M:\[CapitalOmega]\ \[DoubleLongRightArrow]c(k), \[ForAll] 0\[LessEqual]k\[LessEqual]n\n", StyleBox["Step 4", FontWeight->"Bold"], ": Prove the Induction Step, i.e. \ M:\[CapitalOmega]\[DoubleLongRightArrow]c(n+1), or equivalently M:c(n)\ \[DoubleLongRightArrow]c(n+1) \n\n", StyleBox["Note", FontWeight->"Bold"], ": It is the Induction Step (Step 4) that involves the handling of symbolic \ configurations because we have to show M:c(n)\[DoubleLongRightArrow]c(n+1). \ This cannot be done by using the Turing Machine's instruction table as it is, \ because the Turing instructions are defined for numeric tape configurations \ only, not for symbolic configurations. For this we need the Symbolic \ Induction Prover (SIP) , a kind of meta interpreter, that enables the Turing \ Machine to produce it's own induction proof of being a non-halter. \n\n", StyleBox["Note", FontWeight->"Bold"], ": If the induction proof is successful we know that the Turing Machine M \ does not halt and hence \[Sigma](M) = 0.\n\n", StyleBox["Note", FontWeight->"Bold"], ": the induction proof might fail because:\nThe hypothesis is wrong (it's \ just based on a finite amount of tape data)\nThe proof does not terminate \ within the pre-specified amount of CPU time (i.e. it might go through if we \ allow more CPU time)\nA situation is encountered beyond the implemented \ induction logic (we need to enhance the prover)\nA generalized Collatz (3x+1) \ problem is encountered (see below) \n\nWe now turn to a more detailed \ discussion of the Symbolic Induction Prover (SIP). " }], "Text"] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell["The Symbolic Induction Prover", "Section", PageBreakAbove->True], Cell[CellGroupData[{ Cell["Meta-Instructions", "Subsection", FontSize->14], Cell[TextData[{ StyleBox["The underlying idea is a unified and simple principle: analyse \ the Turing Machine's instruction table and extract rules which describe \ meta-transactions on maximal invariant sub-tapes.\n\nExample: Let M = ", FontFamily->"Times New Roman"], Cell[BoxData[GridBox[{ { StyleBox[\(s/h\), FontWeight->"Bold"], StyleBox["0", FontWeight->"Bold"], StyleBox["1", FontWeight->"Bold"]}, { StyleBox["1", FontWeight->"Bold"], "*", "*"}, { StyleBox["2", FontWeight->"Bold"], \((0, R, 5)\), "*"}, { StyleBox["3", FontWeight->"Bold"], \((1, L, 3)\), "*"}, { StyleBox["4", FontWeight->"Bold"], "*", "*"}, { StyleBox["5", FontWeight->"Bold"], "*", \((0, R, 2)\)} }, GridFrame->True, RowLines->True, ColumnLines->True]], FontFamily->"Times New Roman"], StyleBox[" ", FontFamily->"Times New Roman"] }], "Text"], Cell[BoxData[{ RowBox[{"Example", ":", " ", RowBox[{ RowBox[{\(1\^st\), StyleBox[ RowBox[{"o", StyleBox["rder", "DisplayFormula"]}]], StyleBox[" ", "DisplayFormula"], StyleBox["Meta", "DisplayFormula"]}], StyleBox["-", "DisplayFormula"], StyleBox["Instruction", "DisplayFormula"]}]}], "\[IndentingNewLine]", RowBox[{ StyleBox[" ", "DisplayFormula"], StyleBox[ RowBox[{Cell[BoxData[ FormBox[ FrameBox[ RowBox[{ RowBox[{"{", RowBox[{ StyleBox["3", FontWeight->"Bold"], ",", RowBox[{"{", RowBox[{"gl", ",", \({{0}, n}\), ",", StyleBox["0", FontWeight->"Bold"], ",", "gr"}], "}"}]}], "}"}], "\[Rule]", RowBox[{"{", RowBox[{ StyleBox["3", FontWeight->"Bold"], ",", RowBox[{"{", RowBox[{"gl", ",", StyleBox["0", FontWeight->"Bold"], ",", \({{1}, n}\), ",", "gr"}], "}"}]}], "}"}]}], BoxMargins->{{0.2, 0.2}, {0.4, 0.4}}], TraditionalForm]], "DisplayFormula", TextAlignment->Center], " ", \(\[ForAll] \ \(\(n\)\(\[GreaterEqual]\)\(1\)\(\ \)\)\)}], "DisplayFormula"]}]}], "DisplayFormula", TextAlignment->Center], Cell[TextData[{ StyleBox["Here:\n gl ", FontWeight->"Bold"], "symbol for ", StyleBox["g", FontWeight->"Bold"], "eneral ", StyleBox["l", FontWeight->"Bold"], "eft tape\n ", StyleBox["gr ", FontWeight->"Bold"], "symbol for ", StyleBox["g", FontWeight->"Bold"], "eneral ", StyleBox["r", FontWeight->"Bold"], "ight tape\n\nIf at time t , M has configuration\n\n", StyleBox[" ", "DisplayFormula"], Cell[BoxData[ \(TraditionalForm\`\(c\_t\)(n)\)]], StyleBox[" = {", "DisplayFormula"], StyleBox["3", "DisplayFormula", FontWeight->"Bold"], StyleBox[",{\[Omega],{{x},1},{{0},n},", "DisplayFormula"], StyleBox["0", "DisplayFormula", FontWeight->"Bold"], StyleBox[",{{y},1},\[Omega]}} for some words x,y \[Epsilon] ", "DisplayFormula"], StyleBox[Cell[BoxData[ \(TraditionalForm\`\(\[Sum]\^*\)\)], "DisplayFormula"], "DisplayFormula"], StyleBox[",", "DisplayFormula"], "\n\n we can apply the meta-instruction to get\n\n ", Cell[BoxData[ \(TraditionalForm\`\(c\_\(t + 1\)\)(n)\)]], StyleBox[" = {", "DisplayFormula"], StyleBox["3", "DisplayFormula", FontWeight->"Bold"], StyleBox[",{\[Omega],{{x},1},", "DisplayFormula"], StyleBox["0", "DisplayFormula", FontWeight->"Bold"], StyleBox[",{{1},n},{{y},1},\[Omega]}}", "DisplayFormula"] }], "Text", TextAlignment->Left], Cell[BoxData[{ RowBox[{"Example", ":", " ", RowBox[{ RowBox[{\(2\^nd\), " ", StyleBox[ RowBox[{"o", StyleBox["rder", "DisplayFormula"]}]], StyleBox[" ", "DisplayFormula"], StyleBox["Meta", "DisplayFormula"]}], StyleBox["-", "DisplayFormula"], StyleBox["Instruction", "DisplayFormula"]}]}], "\[IndentingNewLine]", StyleBox[ RowBox[{" ", RowBox[{Cell[BoxData[ FormBox[ FrameBox[ RowBox[{ RowBox[{"{", RowBox[{ StyleBox["2", FontWeight->"Bold"], ",", RowBox[{"{", RowBox[{"gl", ",", StyleBox["0", FontWeight->"Bold"], ",", \({{1, 0}, n}\), ",", "gr"}], "}"}]}], "}"}], "\[Rule]", RowBox[{"{", RowBox[{ StyleBox["2", FontWeight->"Bold"], ",", RowBox[{"{", RowBox[{"gl", ",", \({{0}, 2 n}\), ",", StyleBox["0", FontWeight->"Bold"], ",", "gr"}], "}"}]}], "}"}]}], BoxMargins->{{0.2, 0.2}, {0.4, 0.4}}], TraditionalForm]], "DisplayFormula", TextAlignment->Center], " ", \(\[ForAll] \ \(\(n\)\(\[GreaterEqual]\)\(1\)\(\ \)\)\)}]}], "DisplayFormula"]}], "DisplayFormula", TextAlignment->Center], Cell[TextData[{ StyleBox["\nNote", FontWeight->"Bold"], ": A meta-instruction modifies an arbitrarily large countable portion of \ the tape." }], "Text", TextAlignment->Left], Cell[CellGroupData[{ Cell["Induction Schemes", "Subsubsection", TextAlignment->Left, FontSize->14], Cell[TextData[{ "SIP has a build-in library to support several induction proof schemes.\n\ Induction schemes are used in conjunction with meta-instructions to produce \ an induction proof for a non-halting Turing Machine.\nIf necessary, the \ library can be enhanced with new induction schemes.\nWe discuss some of the \ implemented schemes.\n\n", StyleBox["Scheme: Commutation Relations at the Tape Boundary", FontSize->18], "\n\nAssume Turing Machine M exhibits the symbolic machine configuration\n\ c(k) = {", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k},{q,1},\[Omega]}} for some x, q \[Epsilon]", Cell[BoxData[ \(TraditionalForm\`\(\[Sum]\^*\)\)]], " \n", StyleBox["Verify", FontWeight->"Bold"], " M:\[CapitalOmega]\[DoubleLongRightArrow]c(k) for k=0.\n", StyleBox["Assume", FontWeight->"Bold"], ": M: c(k-1)\[DoubleLongRightArrow] c(k).\n", StyleBox["Prove by Induction:", FontWeight->"Bold"], " M: c(k)\[DoubleLongRightArrow] c(k+1)\nIf true, M does not HALT and hence \ \[Sigma][M]=0.\n\n", StyleBox["Induction Proof", FontWeight->"Bold"], "\nLet M be in configuration\nc(k) = {", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k},{q,1},\[Omega]}}\n\nSIP searches for maximal invariant boundary \ conditions and commutation relations: \n", StyleBox["Check if", FontWeight->"Bold"], " \nM: {", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,0},{", Cell[BoxData[ \(TraditionalForm\`q\&~\)]], ",1},gr}}\[DoubleLongRightArrow]{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,1},{", Cell[BoxData[ \(TraditionalForm\`q\&~\)]], ",1},gr}}, for some ", Cell[BoxData[ \(TraditionalForm\`q\&~\)]], "\[Epsilon]", Cell[BoxData[ \(TraditionalForm\`\(\[Sum]\^*\)\)]], ", such that ", Cell[BoxData[ \(TraditionalForm\`q\&~\)]], " = Take[q,Length[", Cell[BoxData[ \(TraditionalForm\`q\&~\)]], "]]\nIf True, check further if x\[VerticalSeparator]\[VerticalSeparator]", Cell[BoxData[ \(TraditionalForm\`q\&~\)]], " = ", Cell[BoxData[ \(TraditionalForm\`q\&~\)]], "\[VerticalSeparator]\[VerticalSeparator]", Cell[BoxData[ \(TraditionalForm\`x\&~\)]], " for some ", Cell[BoxData[ \(TraditionalForm\`x\&~\)]], " \[Epsilon]", Cell[BoxData[ \(TraditionalForm\`\(\[Sum]\^*\)\)]], "\nIf True, modify the Induction Assumption to read:\n\n", StyleBox["Extended Induction Hypothesis", FontWeight->"Bold"], "\nM:{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k-1},{", Cell[BoxData[ \(TraditionalForm\`q\&~\)]], ",1},gr}}\[DoubleLongRightArrow]{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k},{", Cell[BoxData[ \(TraditionalForm\`q\&~\)]], ",1},gr}}\n\nSIP proves this extended induction assumptions as follows:\n\ {", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k},{", Cell[BoxData[ \(TraditionalForm\`q\&~\)]], ",1},gr}}\n\[DownArrow]\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k-1},{x,1}, {", Cell[BoxData[ \(TraditionalForm\`q\&~\)]], ",1},gr}}\n\[DownArrow]\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k-1},{", Cell[BoxData[ \(TraditionalForm\`q\&~\)]], ",1},{", Cell[BoxData[ \(TraditionalForm\`x\&~\)]], ",1},gr}}\t\t (using the commutation relation)\n\[DownArrow]\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k},{", Cell[BoxData[ \(TraditionalForm\`q\&~\)]], ",1},{", Cell[BoxData[ \(TraditionalForm\`x\&~\)]], ",1},gr}} \t\t(using the extended induction hyp for (k-1) \[RightTeeArrow] \ (k) on any gr \n\[DownArrow]\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k},{x,1}, {", Cell[BoxData[ \(TraditionalForm\`q\&~\)]], ",1},gr}}\t\t (using commutation relation)\n\[DownArrow]\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k+1},{", Cell[BoxData[ \(TraditionalForm\`q\&~\)]], ",1},gr}} \[FilledSquare]\nHence M: c(k)\[DoubleLongRightArrow] c(k+1),\ \[ForAll]k\[GreaterEqual]0 and M does NOT halt, hence \[Sigma][M]=0." }], "Text", TextAlignment->Left], Cell[TextData[{ "\n", StyleBox["Scheme: Cyclic Conditions at the Tape Boundary", FontSize->18], "\n\nAssume Turing Machine M exhibits the symbolic machine configuration\n \ c(k) = {", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k},{q,1},\[Omega]}}, for some x, q \[Epsilon]", Cell[BoxData[ \(TraditionalForm\`\(\[Sum]\^*\)\)]], " \n\n", StyleBox["Induction Base", FontWeight->"Bold"], ":\nVerify M:{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,1},gr}}\[DoubleLongRightArrow] M:{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],{y,1},", StyleBox["h", FontWeight->"Bold"], ",gr}} \n\n", StyleBox["Induction Assumption", FontWeight->"Bold"], "\nM:{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,j},gr}}\[DoubleLongRightArrow] M:{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],{y,j},", StyleBox["h", FontWeight->"Bold"], ",gr}},\[ForAll]1\[LessEqual]j\[LessEqual]k-1\n\nAssume further, that the \ instruction table of M results in meta-instructions: \n\nM1:{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],{y,n},", StyleBox["h", FontWeight->"Bold"], ",{", Cell[BoxData[ \(TraditionalForm\`c\_i\)]], ",1},gr}}\[LongRightArrow]{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,n},{", Cell[BoxData[ \(TraditionalForm\`c\_\(i + 1\)\)]], ",1},gr}}, y,", Cell[BoxData[ \(TraditionalForm\`\(\(c\_0\)\(,\)\)\)]], "\[Ellipsis],", Cell[BoxData[ \(TraditionalForm\`c\_m\)]], " \[Epsilon]", Cell[BoxData[ \(TraditionalForm\`\(\[Sum]\^*\)\)]], " ,\[ForAll]n\[GreaterEqual]0,0\[LessEqual]i\[Precedes]m\n\nM2:{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],{y,n},", StyleBox["h", FontWeight->"Bold"], ",{", Cell[BoxData[ \(TraditionalForm\`c\_m\)]], ",1},gr}}\[LongRightArrow]{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],{y,n+1},", StyleBox["h", FontWeight->"Bold"], ",gr}}\n\n", StyleBox["Note", FontWeight->"Bold"], ": ", Cell[BoxData[ \(TraditionalForm\`c\_0\)]], ",\[Ellipsis], ", Cell[BoxData[ \(TraditionalForm\`c\_m\)]], " are the cyclic boundary conditions, with ", Cell[BoxData[ \(TraditionalForm\`c\_0\)]], "={} \n\n", StyleBox["Induction proof", FontWeight->"Bold"], ":\n\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k},{q,1},w}}\n{", StyleBox["s", FontWeight->"Bold"], ",{{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k-1},{x,1},{q,1},w}}\n{", StyleBox["s", FontWeight->"Bold"], ",{{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k-1},gr}}\t\t\t\t(replacing {{x,1},{q,1},w} by ", StyleBox["gr", FontWeight->"Bold"], ")\n\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],{y,k-1},", StyleBox["h", FontWeight->"Bold"], ",gr}}\t\t \t\t(", Cell[BoxData[ \(TraditionalForm\`1\^st\)]], " use of induction hyp)\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k-1},{", Cell[BoxData[ \(TraditionalForm\`c\_1\)]], ",1},gr}}\t\t\t (using meta-instruction M1)\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],{y,k-1},", StyleBox["h", FontWeight->"Bold"], ",{", Cell[BoxData[ \(TraditionalForm\`c\_1\)]], ",1},gr}}\t\t\t ( ", Cell[BoxData[ \(TraditionalForm\`2\^nd\)]], " use of induction hyp)\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k-1},{", Cell[BoxData[ \(TraditionalForm\`c\_2\)]], ",1},gr}}\t\t\t (using meta-instruction M1)\n\[VerticalEllipsis]\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],{y,k-1},", StyleBox["h", FontWeight->"Bold"], ",{", Cell[BoxData[ \(TraditionalForm\`c\_\(m - 1\)\)]], ",1},gr}} \t\t(", Cell[BoxData[ \(TraditionalForm\`\((m - 1)\)\^th\)]], " use of induction hyp)\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k-1},{", Cell[BoxData[ \(TraditionalForm\`c\_m\)]], ",1},gr}}\t\t\t(using meta-instruction M1)\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],{y,k},", StyleBox["h", FontWeight->"Bold"], ",gr}}\t\t \t\t( use of induction hyp and use of M2)\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k},{", Cell[BoxData[ \(TraditionalForm\`c\_1\)]], ",1},gr}}\t \t\t(using meta-instruction)\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k},{", Cell[BoxData[ \(TraditionalForm\`c\_1\)]], ",1}{{x,1},{q,1},w}} \t(plugging back-in the explicit right tape portion)\n\ \[DownArrow]\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k+1},{p,1}{q,1},w}}\t\t(this step might vary in other cases)\n\ \[DownArrow]\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k+1},{q,1}{0,p},w}}\t\t for some p>0\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,k+1},{q,1},w}} \t\t\t(subsuming the finite 0's into \[Omega])\ \[FilledSquare]\n" }], "Text", TextAlignment->Left], Cell[TextData[{ StyleBox["Scheme: Decreasing Cell Sequence at the Tape Boundary", FontSize->18], "\n\nAssume Turing Machine M exhibits:\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{{A},n},{{B},1},{{R},k},gr}}\tk\[GreaterEqual]0 Integer\n\ \[VerticalEllipsis] \n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{{A},n},{{B},2},{{R},k-1},gr}}\n\[VerticalEllipsis]\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{{A},n},{{B},j},{{R},k-j},gr}}\n\n", StyleBox["Induction Base", FontWeight->"Bold"], ":\n\nVerify, that for some function f:\nM:{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{{A},n},{{B},1},{{R},1},gr}}\[LongRightArrow]{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{{A},n + f(1)},{{B},2},gr}} \n\nVerify the Swap Meta Instruction\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{{A},n},{{B},k},{{R},1},gr}}\[LongRightArrow]{s,{w,h,{{A},n+", Cell[BoxData[ \(TraditionalForm\`k\_0\)]], "},{{B},1},{{R},k-1},{{B},1},gr}}\n\n", StyleBox["Induction Assumption", FontWeight->"Bold"], ":\nM:{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{{A},n},{{B},k-1},{{R},1},gr}}\[LongRightArrow]{s,{w,h,{{A},n + \ f[k-1]},{{B},k},gr}}, for some function f \n\n", StyleBox["Induction Proof:", FontWeight->"Bold"], "\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{{A},n},{{B},k},{{R},1},gr}}\n\t\t\[DownArrow]\t\t\t\t\t\t\t(apply Swap \ Meta Instruction)\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{{A},n+", Cell[BoxData[ \(TraditionalForm\`k\_0\)]], "},{{B},1},{{R},k-1},{{B},1},gr}}\n\t\t\[DownArrow]\t\t\t\t\t\t\t(apply \ (k-1)-times Induction Assumption)\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{{A},n+", Cell[BoxData[ \(TraditionalForm\`k\_0\)]], "+", Cell[BoxData[ \(TraditionalForm\`\[Sum]\+\(i = 1\)\%\(k - 1\)f[i]\)]], "},{{B},k},{{R},0},{{B},1},gr}}\n\t\t\[DownArrow]\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{{A},n+", Cell[BoxData[ \(TraditionalForm\`k\_0\)]], "+", Cell[BoxData[ \(TraditionalForm\`\[Sum]\+\(i = 1\)\%\(k - 1\)f[i]\)]], "},{{B},k+1},gr}}\n\nNow, require that \n\n", Cell[BoxData[ \(TraditionalForm\`k\_0\)]], "+", Cell[BoxData[ \(TraditionalForm\`\[Sum]\+\(i = 1\)\%\(k - 1\)f[i]\)]], " = f[k] and hence f[k]=", Cell[BoxData[ \(TraditionalForm\`k\_0\)]], " ", Cell[BoxData[ \(TraditionalForm\`2\^k\)]], "\n\nSimilar schema are also supported:\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],{{A},n},{{B},k},", StyleBox["h", FontWeight->"Bold"], ",{{R},1},gr}}\n\t\t\[DownArrow]\t\t\t\t\t\t(apply Swap Meta Instruction)\n\ {", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],{{A},n+", Cell[BoxData[ \(TraditionalForm\`k\_0\)]], "},{{B},1},", StyleBox["h", FontWeight->"Bold"], ",{{R},k-1},{{X},1},gr}}\n\nand \n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],{{A},n},", StyleBox["h", FontWeight->"Bold"], ",{{B},k},{{R},1},gr}}\n\t\t\[DownArrow]\t\t\t\t\t\t(apply Swap Meta \ Instruction)\n{", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],{{A},n+", Cell[BoxData[ \(TraditionalForm\`k\_0\)]], "},", StyleBox["h", FontWeight->"Bold"], ",{{B},1},{{R},k-1},{{X},1},gr}}\n " }], "Text", TextAlignment->Left] }, Open ]], Cell[CellGroupData[{ Cell["Modulo Arithmetic", "Subsubsection", TextAlignment->Left, FontSize->14], Cell[TextData[{ "Often, meta-instructions are subject to some modulo condition, see e.g., \ the annotated sample proof\n\n", StyleBox["Example", FontWeight->"Bold"], ":\nM:{", StyleBox["s", FontWeight->"Bold"], ",{gl,{1,n},", StyleBox["h", FontWeight->"Bold"], ",gr}}\[LongRightArrow] {", StyleBox["s", FontWeight->"Bold"], ",{gl,{{1},Mod[n,3]},", StyleBox["h", FontWeight->"Bold"], ",{{0,1,0},3 * Floor[", Cell[BoxData[ \(TraditionalForm\`n\/3\)]], "]},gr}} \n\nIf possible, SIP calculates Mod[n,p] explicitly by using \ structural information of n.\n\n", StyleBox["Example", FontWeight->"Bold"], ":\nIf the variable is of the form 2n+1 and p = 2 we know that Mod[2n+1,2] \ = 1.\nIn general SIP uses modulo arithmetic in the finite ring ", Cell[BoxData[ FormBox[ SubscriptBox["\[DoubleStruckCapitalZ]", StyleBox["n", "TI"]], TraditionalForm]], "InlineFormula"], ", including \n\n", StyleBox["Fermat's Little Theorem", FontWeight->"Bold"], ": ", StyleBox["Mod[", FontWeight->"Bold"], Cell[BoxData[ \(TraditionalForm\`a\^p\)], FontWeight->"Bold"], StyleBox[",p] = a", FontWeight->"Bold"], ", \[ForAll] a \[Epsilon] Integers, \[ForAll] p \[Epsilon] Primes\n\nand \ ", StyleBox["Euler's generalization", FontWeight->"Bold"], " ", StyleBox["Mod[", FontWeight->"Bold"], Cell[BoxData[ \(TraditionalForm\`a\^\(\[CurlyPhi](n)\)\)], FontWeight->"Bold"], StyleBox[",n] = 1", FontWeight->"Bold"], ", \[ForAll] a,n \[Epsilon] Integers\n\n (Euler's Phi function \ \[CurlyPhi][n] gives the number of positive integers less than or equal to ", Cell[BoxData[ FormBox[ StyleBox["n", "TI"], TraditionalForm]], "InlineFormula"], " which are relatively prime to ", Cell[BoxData[ FormBox[ StyleBox["n", "TI"], TraditionalForm]], "InlineFormula"], ").\n\nIf nothing specific can be computed, SIP picks a value Mod[n,p] = v \ \[CurlyEpsilon] {0,\[Ellipsis],p-1}and generates p sub-proofs, one for each \ possible v value at each decision point in the general induction proof.\n" }], "Text", TextAlignment->Left] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell["The SIP Package", "Subsection", PageBreakAbove->True, TextAlignment->Left, FontSize->14], Cell["\<\ SIP includes these major functional packages to support meta \ instructions and symbolic induction proofs for Turing Machine configurations: \ \>", "Text", PageBreakAbove->Automatic, TextAlignment->Left], Cell[CellGroupData[{ Cell["Create and Execute Meta Instructions", "Subsubsection", PageBreakAbove->Automatic, TextAlignment->Left, FontSize->14], Cell[TextData[{ StyleBox["metaservices\t", FontWeight->"Bold"], "\[DoubleLongRightArrow] creates rules that represent Meta Instructions\t\n\ ", StyleBox["swapservices\t", FontWeight->"Bold"], "\[DoubleLongRightArrow] handles all orders of meta instructions\n", StyleBox["shiftservices\t", FontWeight->"Bold"], "\[DoubleLongRightArrow] shifts configurations into Normal Form to make \ them comparable" }], "Text", PageBreakAbove->Automatic, TextAlignment->Left] }, Open ]], Cell[CellGroupData[{ Cell["Handling of Induction Proofs ", "Subsubsection", PageBreakAbove->Automatic, TextAlignment->Left, FontSize->14], Cell[TextData[{ StyleBox["inductionservices\t", FontWeight->"Bold"], "\[DoubleLongRightArrow] the main package for induction proof schemes\n", StyleBox["tracebufferservices\t", FontWeight->"Bold"], "\[DoubleLongRightArrow] detects emerging schemes by tracing the steps of \ an induction proof, producing induction assumptions, invokes SIP recursively \ for proof \n" }], "Text", PageBreakAbove->Automatic, TextAlignment->Left] }, Open ]], Cell[CellGroupData[{ Cell["Modulo Arithmetic for Symbolic Variables ", "Subsubsection", PageBreakAbove->Automatic, TextAlignment->Left, FontSize->14], Cell[TextData[{ StyleBox["getgaugedvarservice\t", FontWeight->"Bold"], "\[DoubleLongRightArrow] handles modulo arithmetic for symbolic variables" }], "Text", PageBreakAbove->Automatic, TextAlignment->Left] }, Open ]], Cell[CellGroupData[{ Cell["Handling Boundary Conditions", "Subsubsection", PageBreakAbove->Automatic, TextAlignment->Left, FontSize->14], Cell[TextData[{ StyleBox["extremepointservices\t", FontWeight->"Bold"], "\[DoubleLongRightArrow] handles logic associated with maximal invariant \ tape boundaries" }], "Text", PageBreakAbove->Automatic, TextAlignment->Left] }, Open ]], Cell[CellGroupData[{ Cell["Technical Services", "Subsubsection", PageBreakAbove->Automatic, TextAlignment->Left, FontSize->14], Cell[TextData[{ StyleBox["semaphoresupport\t", FontWeight->"Bold"], "\[DoubleLongRightArrow] provides services to serialize induction schemes \ to prevent \"vicious circles\" \n", StyleBox["environmentservices\t", FontWeight->"Bold"], "\[DoubleLongRightArrow] specifies the Proof Environment (global parameters \ etc) " }], "Text", PageBreakAbove->Automatic, TextAlignment->Left] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell["Annotated Sample Proof", "Subsection", PageBreakAbove->Automatic, TextAlignment->Left], Cell[TextData[{ "Consider this Turing Machine\n\nM= ", Cell[BoxData[ RowBox[{"(", "\[NoBreak]", GridBox[{ {\({1, R, 2}\), \({0, L, 1}\)}, {\({1, R, 3}\), \({1, L, 2}\)}, {\({1, R, 4}\), \({1, L, 1}\)}, {\({1, L, 5}\), \({0, R, 5}\)}, {\({1, R, 0}\), \({0, L, 2}\)} }, RowSpacings->1, ColumnSpacings->1, ColumnAlignments->{Left}], "\[NoBreak]", ")"}]]], "\n\n", StyleBox["Assumed configuration:", FontWeight->"Bold"], "\n\nc(n) = {4,{w,{{1},5+2 n},0,{{1},1+n},w}}\n\n", StyleBox["Base Case", FontWeight->"Bold"], ": M:\[CapitalOmega]\[DoubleLongRightArrow]c(n) verified for n=0,2,4,...\n\n\ ", StyleBox["Induction Step", FontWeight->"Bold"], "\nM:c[n]\[LongRightArrow]c[n+2]\n", Cell[BoxData[ \(\(\(NotebookOpen["\"]; \)\( (*\ CD\ drive\ *) \)\)\)], "InlineInput", TextAlignment->Left, ButtonBoxOptions->{Active->True, ButtonStyle->"MainBookLink", ButtonFrame->"DialogBox"}] }], "Text", PageBreakAbove->Automatic, TextAlignment->Left] }, Open ]], Cell[CellGroupData[{ Cell["Results", "Subsection", TextAlignment->Left, FontSize->14], Cell[TextData[{ "Start with ", Cell[BoxData[ \(TraditionalForm\`\[ScriptCapitalT]\[ScriptCapitalM]\_5\)]], ", card(", Cell[BoxData[ \(TraditionalForm\`\[ScriptCapitalT]\[ScriptCapitalM]\_5\)]], ") = ", Cell[BoxData[ \(TraditionalForm\`21\^10\)]], "\nApplying well-known [6] and fast techniques (such as Tree Normal Form, \ BackTrack,Simple Loop Detection etc) leaves about 1,000,000 Turing Machines \ undecided.\n\[ShortRightArrow]\t", StyleBox["850,000", FontWeight->"Bold"], " Turing Machines of a linear type, e.g. {", StyleBox["s", FontWeight->"Bold"], ",{\[Omega],", StyleBox["h", FontWeight->"Bold"], ",{x,a*n + b},\[Omega]}} for some x \[Epsilon] ", Cell[BoxData[ \(TraditionalForm\`\(\[Sum]\^*\)\)]], ", or slightly more complex, ", StyleBox["proved by SIP to not HALT", FontWeight->"Bold"], " \n\[ShortRightArrow]\t", StyleBox["143,000", FontWeight->"Bold"], " Turing Machines of polynomial or exponential configurations,", StyleBox[" proved by SIP to not HALT", FontWeight->"Bold"], "\n\[ShortRightArrow]\t1,000 Turing Machines currently too complex for the \ Symbolic Prover\n\[ShortRightArrow]\t\[Rule]\t", StyleBox["900", FontWeight->"Bold"], " of those are ", StyleBox["manually proven to not HALT", FontWeight->"Bold"], "\n\[ShortRightArrow]\t\[ShortRightArrow]\t", StyleBox["100", FontWeight->"Bold"], " cases are still ", StyleBox["HOLDOUT", FontWeight->"Bold"], "s and are currently under consideration, but there is ", StyleBox["strong evidence that they do not halt", FontWeight->"Bold"], "\n\[ShortRightArrow]\t", StyleBox["6,000", FontWeight->"Bold"], "\tTuring Machines ", StyleBox["HALT within 50 Mio Steps", FontWeight->"Bold"], "\nGiven that, we find that for the number of 1-Symbols (\[CapitalSigma]) \ left on the tape, the number of cells scanned (Space) and the number of \ moves (Shift) the Marxen-Buntrock [7] machine is the champion \n\n", Cell[BoxData[ RowBox[{" ", RowBox[{\(M\_MB\), "=", StyleBox[ TagBox[ RowBox[{"(", "\[NoBreak]", GridBox[{ {\({1, R, 2}\), \({1, L, 3}\)}, {\({1, R, 3}\), \({1, R, 2}\)}, {\({1, R, 4}\), \({0, L, 5}\)}, {\({1, L, 1}\), \({1, L, 4}\)}, {\({1, R, 0}\), \({0, L, 1}\)} }, RowSpacings->1, ColumnSpacings->1, ColumnAlignments->{Left}], "\[NoBreak]", ")"}], Function[ BoxForm`e$, MatrixForm[ BoxForm`e$]]], "DisplayFormula"]}]}]], "DisplayFormula", TextAlignment->Left], "\n\nwith: \n", StyleBox["\[Sum][5]\t\t= 4098\nShift[5]\t= 47,176,870\nSpace[5]\t= 12,289", FontWeight->"Bold"], "\n\nThe largest ", StyleBox["unary", FontWeight->"Bold"], " number (i.e. empty tape with a single block of consecutive 1's) produced \ by any halting binary 5-state Turing Machine is \n\n", StyleBox["Num[5]\t= 165", FontWeight->"Bold"], "\n\nThe NUM-Champion is: \n\n", Cell[BoxData[ RowBox[{\(M\_\(NUM - Champ\)\), "=", TagBox[ RowBox[{"(", "\[NoBreak]", GridBox[{ {\({1, R, 2}\), \({1, L, 1}\)}, {\({1, R, 3}\), \({1, L, 5}\)}, {\({1, R, 4}\), \({1, R, 5}\)}, {\({0, L, 1}\), \({1, R, 3}\)}, {\({1, R, 0}\), \({0, L, 2}\)} }, RowSpacings->1, ColumnSpacings->1, ColumnAlignments->{Left}], "\[NoBreak]", ")"}], Function[ BoxForm`e$, MatrixForm[ BoxForm`e$]]], "\[NoBreak]"}]], TextAlignment->Left], "\n\n", StyleBox["Note", FontWeight->"Bold"], ": There exists the possibility that the halting question for one or more \ of the remaining holdouts is linked to the Collatz 3x+1 problem (see also \ [5]).\nThis is currently under investigation and the final results will be \ reported in a forthcoming paper [8]." }], "Text", TextAlignment->Left] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell[TextData[StyleBox["References", FontWeight->"Bold"]], "Section", PageBreakAbove->True], Cell[TextData[{ "\n", StyleBox["[1]\tT.Rado, Bell System Technical Journal, ", FontFamily->"Times New Roman", FontSize->9], StyleBox["41", FontFamily->"Times New Roman", FontSize->9, FontWeight->"Bold"], StyleBox[", 1962, 877-884\n[2]\tG.S.Boolos, R.C.Jeffrey Computability and \ Logic, Cambridge, 1989\n[3]\tG.J.Chaitin, Computing the Busy Beaver Function", FontFamily->"Times New Roman", FontSize->9], StyleBox["\n", FontFamily->"Times New Roman", FontSize->9, FontSlant->"Italic"], StyleBox[" \t in: T.M. Cover, B. Gopinath, Open Problems in \ Communication and Computation, Springer, 1987\n[4]\tS.Bringsjord et al., A \ New G\[ODoubleDot]delian Argument for Hypercomputing Minds Based on the Busy \ Beaver Problem\n \tTo be published in: Applied Mathematics and Computation \ \n[5]\tP.Michel, Arch. Math. Logic, ", FontFamily->"Times New Roman", FontSize->9], StyleBox["32", FontFamily->"Times New Roman", FontSize->9, FontWeight->"Bold"], StyleBox[", 1993, 351-367\n[6]\tR.Machlin, Q.Strout, Physica D, ", FontFamily->"Times New Roman", FontSize->9], StyleBox["42", FontFamily->"Times New Roman", FontSize->9, FontWeight->"Bold"], StyleBox[", 1990, 85-98, and references therein\n[7]\tH.Marxen, J.Buntrock, \ Bull. EATACS, ", FontFamily->"Times New Roman", FontSize->9], StyleBox["40", FontFamily->"Times New Roman", FontSize->9, FontWeight->"Bold"], StyleBox[", 1990, 247-251\n[8]\tJ.Hertel, The Computation of the Value of \ Rado's Non-Computable \[CapitalOAcute] Function for 5-State Turing\n \t\ Machines, work in progress\n[9]\tK.G\[ODoubleDot]del, Some Remarks on the \ Undecidability Results, in [10, pp 305-306], 1972\n[10]\tS.Fefferman et al. \ (eds.), Kurt G\[ODoubleDot]del Collected Works Vol. II, Oxford, 1990 \n[11]\t\ M.W.Green: ", FontFamily->"Times New Roman", FontSize->9], StyleBox["Proceedings of the 5th IEEE Annual Symposium on Switching Circuit \ Theory and Logical Design, \t\t1964, 91-94", FontFamily->"Times New Roman", FontSize->9, FontVariations->{"CompatibilityType"->0}], StyleBox["\n[12]\tB.A.Julstrom, ACM SIGACT, ", FontFamily->"Times New Roman", FontSize->9], StyleBox["23", FontFamily->"Times New Roman", FontSize->9, FontWeight->"Bold"], StyleBox[", 1992, 100-106\n[13]\tE. W. Weisstein, Busy Beaver.From \ MathWorld--A Wolfram Web Resource.\n \t\ http://mathworld.wolfram.com/BusyBeaver.html\n[14]\tOn-Line Encyclopedia of \ Integer Sequences, Sequence Id=A028444\n\t\ http://www.research.att.com/~njas/sequences/index.html\n[15]\tA.M.Ben-Amrein, \ B.A.Julstrom, K.Zwick, Math. Systems Theory, ", FontFamily->"Times New Roman", FontSize->9], StyleBox["29", FontFamily->"Times New Roman", FontSize->9, FontWeight->"Bold"], StyleBox[", 1996, 375-386\n[16]\tH.J.M.Wijers, Bibliography on the Busy \ Beaver Problem, 2004\n\thttp://www.win.tue.nl/~wijers/bbbibl.pdf", FontFamily->"Times New Roman", FontSize->9] }], "Reference"] }, Open ]] }, Open ]] }, FrontEndVersion->"5.2 for X", ScreenRectangle->{{0, 1920}, {0, 1200}}, ScreenStyleEnvironment->"Working", WindowToolbars->{}, Evaluator->"K2", WindowSize->{1592, 1083}, WindowMargins->{{116, Automatic}, {Automatic, 25}}, PrintingCopies->1, PrintingPageRange->{Automatic, Automatic}, PageHeaders->{{ Inherited, Inherited, Cell[ "Joachim Herte", "Header"]}, { Cell[ "Computing the Uncomputable Rado Sigma Function", "Header"], Inherited, Inherited}}, Magnification->1, StyleDefinitions -> "IMS2006styles.nb" ] (******************************************************************* Cached data follows. If you edit this Notebook file directly, not using Mathematica, you must remove the line containing CacheID at the top of the file. The cache data will then be recreated when you save this file from within Mathematica. *******************************************************************) (*CellTagsOutline CellTagsIndex->{} *) (*CellTagsIndex CellTagsIndex->{} *) (*NotebookFileOutline Notebook[{ Cell[CellGroupData[{ Cell[1776, 53, 63, 0, 78, "Title"], Cell[1842, 55, 100, 3, 40, "Subtitle"], Cell[1945, 60, 32, 0, 22, "Author"], Cell[1980, 62, 97, 4, 61, "TextAboutAuthor"], Cell[2080, 68, 1369, 22, 181, "Abstract"], Cell[CellGroupData[{ Cell[3474, 94, 36, 0, 62, "SectionFirst"], Cell[CellGroupData[{ Cell[3535, 98, 62, 0, 54, "Subsection"], Cell[3600, 100, 3376, 48, 314, "Text"] }, Open ]], Cell[CellGroupData[{ Cell[7013, 153, 49, 0, 54, "Subsection"], Cell[7065, 155, 939, 14, 62, "Text"] }, Open ]], Cell[CellGroupData[{ Cell[8041, 174, 47, 0, 54, "Subsection"], Cell[8091, 176, 3776, 79, 216, "Text"] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell[11916, 261, 79, 0, 62, "Section"], Cell[CellGroupData[{ Cell[12020, 265, 48, 0, 54, "Subsection"], Cell[12071, 267, 1809, 40, 332, "Text"], Cell[13883, 309, 518, 12, 44, "Text", PageBreakAbove->True], Cell[14404, 323, 893, 22, 70, "DisplayFormula"], Cell[15300, 347, 734, 20, 95, "DisplayFormula"], Cell[16037, 369, 3417, 88, 101, "Text"], Cell[19457, 459, 325, 8, 31, "Text"], Cell[19785, 469, 289, 7, 47, "Text"], Cell[CellGroupData[{ Cell[20099, 480, 95, 2, 43, "Subsubsection"], Cell[20197, 484, 5715, 182, 313, "Text"] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell[25961, 672, 82, 1, 54, "Subsection", PageBreakAbove->True], Cell[26046, 675, 217, 4, 26, "Text"], Cell[26266, 681, 8416, 220, 885, "Text"] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell[34731, 907, 72, 1, 62, "Section", PageBreakAbove->True], Cell[CellGroupData[{ Cell[34828, 912, 55, 1, 54, "Subsection"], Cell[34886, 915, 1142, 35, 161, "Text"], Cell[36031, 952, 1768, 47, 48, "DisplayFormula"], Cell[37802, 1001, 1378, 45, 206, "Text"], Cell[39183, 1048, 1734, 45, 49, "DisplayFormula"], Cell[40920, 1095, 184, 6, 44, "Text"], Cell[CellGroupData[{ Cell[41129, 1105, 81, 2, 44, "Subsubsection"], Cell[41213, 1109, 4781, 172, 733, "Text"], Cell[45997, 1283, 5661, 230, 769, "Text"], Cell[51661, 1515, 3934, 146, 787, "Text"] }, Open ]], Cell[CellGroupData[{ Cell[55632, 1666, 81, 2, 44, "Subsubsection"], Cell[55716, 1670, 2219, 69, 353, "Text"] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell[57984, 1745, 100, 3, 54, "Subsection", PageBreakAbove->True], Cell[58087, 1750, 217, 6, 44, "Text", PageBreakAbove->Automatic], Cell[CellGroupData[{ Cell[58329, 1760, 129, 3, 44, "Subsubsection", PageBreakAbove->Automatic], Cell[58461, 1765, 488, 14, 62, "Text", PageBreakAbove->Automatic] }, Open ]], Cell[CellGroupData[{ Cell[58986, 1784, 122, 3, 44, "Subsubsection", PageBreakAbove->Automatic], Cell[59111, 1789, 448, 11, 62, "Text", PageBreakAbove->Automatic] }, Open ]], Cell[CellGroupData[{ Cell[59596, 1805, 134, 3, 44, "Subsubsection", PageBreakAbove->Automatic], Cell[59733, 1810, 217, 6, 26, "Text", PageBreakAbove->Automatic] }, Open ]], Cell[CellGroupData[{ Cell[59987, 1821, 121, 3, 44, "Subsubsection", PageBreakAbove->Automatic], Cell[60111, 1826, 235, 7, 26, "Text", PageBreakAbove->Automatic] }, Open ]], Cell[CellGroupData[{ Cell[60383, 1838, 111, 3, 44, "Subsubsection", PageBreakAbove->Automatic], Cell[60497, 1843, 399, 11, 44, "Text", PageBreakAbove->Automatic] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell[60945, 1860, 96, 2, 54, "Subsection", PageBreakAbove->Automatic], Cell[61044, 1864, 1117, 33, 304, "Text", PageBreakAbove->Automatic] }, Open ]], Cell[CellGroupData[{ Cell[62198, 1902, 68, 2, 54, "Subsection"], Cell[62269, 1906, 4159, 112, 628, "Text"] }, Open ]] }, Open ]], Cell[CellGroupData[{ Cell[66477, 2024, 95, 2, 62, "Section", PageBreakAbove->True], Cell[66575, 2028, 3083, 80, 286, "Reference"] }, Open ]] }, Open ]] } ] *) (******************************************************************* End of Mathematica Notebook file. *******************************************************************)