Effective Halt-ability - Gödel’s Halting Theorem

During the mid-1990s, while an undergraduate at the University of Nebraska at Omaha, a well-kept secret in the Midwest, a simple high-level language feature that might ameliorate the dilemma of Gödel’s Halting Theorem was struck upon. Its rudiments might have been realized during a first course in programming fundamentals in Pascal at Vanderbilt University circa the Spring of 1989. It was simply this, “the only programmatic structure which would ever produce an infinite iteration found within any code listing is a definite or indefinite repetition. Hence, it seemed reasonable that, if one places a limiting constraint before each instance of these classes of statements found within a program listing, one might guarantee halt-ability; however, one could not ensure the correctness of the program’s final state. When a limit on an iteration was exceeded, a program could gracefully exit and provide an exception report. Such a technique would not guarantee programmatic correctness. Yet, seeing the simplicity of this approach, it might be the case that Gödel’s Halting problem might have been left behind by him as a teaching heuristic, a challenging yet very solvable problem.

A simple, conceptual description of the Halting Problem follows the pattern of its formal mathematically construction; yet, it only uses abstractions.

Also, considering the fact that Gödel and Turing would have been working primarily in the context of machine language, this view of the Halting Problem is understandable. And, in the absence of structured programming or any formal software engineering principles and best practices, these early systems likely were very error prone and commonly entering states of infinite iteration. So, a reasonable first step in ensuring program correctness is guaranteeing halt-ability, the absence of any runaway conditions. Plus, crafting a program which could process any other program listing and detect whether it would eventually terminate or not would be a wise strategy for this first step. Then, the question becomes, “is such possible? Or, is such computable?” Hence, the Theorem of Halt-ability. 

Gödel’s proof is contradictory by construction. Hence, mathematical instinct says that the reasoning is somewhat circular. We start with a contradictory construction and the show that it produces a contradiction. Is such acceptable proof-work? Yet, the assertion of the proof and its claims has stood for decades.

And, if one might somehow show that a program shall eventually halt, the next goal which one must guarantee is that its beginning, intermediate, and final states are all correct. Such might be achievable through the use of formally verifiable programmatic contracts. Such as those developed by Bertrand Meyer.  

Guaranteeing halt-ability in the high-level language layer of a system description would require the use of a global plus numerous local constraints covering all of the iterative structures within the program specification. If none of these upper-bounds on repetition were met, the program would reach its final state and stop. If one of these constraints were violated, the program would raise an exception, print a report on the error stream, and gracefully halt execution. And, a language translation tool, like a compiler or interpreter, which inspected a program listing ensuring that every repetition structure was within the scope of such constraints, would be a counterexample contradicting Gödel’s claim. In other words, it would be the very class of program that he sought.

At the layer of the instruction set architecture, detecting the presence of a processing loop would be necessary. So, an architecture with commands that signal the beginning and ending of a loop are sufficient for its detection. A hardware implementation of such would place a value of high in a field upon entering a loop, a value of medium upon exiting, and a value of low when it is outside of any loop.

While this value is high, a loop counter would be incremented before the first instruction of any iteration. When a loop is exited, the state of any enclosing ones, which includes its counter, would be removed from a register stack maintaining these and made the active loop state. And, if an architecture does not support a loop-begin and loop-end imperatives, they might be simulated by placing values representing these events plus loop state variables within the register file.

It is the case that the “practical” nesting depth of loops has its bounds. It is the said that the goal of efficient programmatic design would use a level of nesting that would produce a quadratic running time or better. So, a hardware implementation that supported a depth of nesting around ten should sufficient. Yet, the placement of the loop frames within the lowest portion of their stack in the main memory file would support a practically unlimited level of nesting. Although, such is impractical from the standpoint of algorithmic efficiency. Seeing that, the development of algorithms with a quadratic time complexity be the goal.

 So, an approximate high-level language solution be this.

#GOEDEL’S HALTING PROBLEM RESOLUTION - EXAMPLE

@[ MAXIMUM-ALLOWABLE-CYCLES := ANY_RESOLVABLE_VALUE ]

WHILE NON-STOP:

                NON-STOP := METHODCALL( PARAMETER_LIST )

So, in modern computing, it might be the case that the question of halt-ability is solve-able. The battle for programmatically enforceable correctness remains. Although, the work of Bertrand Meyer and his programmatic (design) contracts show promise.

It also might be the case that the computing community already holds this insight; yet, it has not been deemed a worthwhile implementation as a hardware circuit or high-level language feature. It is certain that evidence of Gödel’s counterexample exists among current language translation tools. A Python process will gracefully exit and report an exception if a recursive function exceeds an allowable number of self-referential calls. This ensures “halt-ability” for any recursively defined program. Plus, recursion and iteration are processing equivalents, simply different sides of the same algorithmic coin. So, in a sense, Python’s modern hybrid compiler-interpreter is the very type of program that Gödel sought and proved was not computable.

In the case of this problem of halt-ability, it is likely that many students are very-well baffled, befuddled, and brain-bazzizalled by its proof-description, the inherent contradiction built in the proof-work, and the social dynamic involved in questioning a scientific holy-grail put in place by a respected name of Germanic heritage. The Nobel prize-winning physicist at Stanford, Professor William Shockley, helped measure the social weighting of racial cohort labels. His work was based upon what he called “genetic” measures. These were a collection of “carefully chosen” measures. Which he felt accurately and best described the relative strengths of four racial communities. Unfortunately, five primary ones exist on this earth. One of these, those who are descendants of the indigenous inhabitants of the Americas was completely left off the list. Considering the history of the European-led occupation of the Americas, they might simply have been deemed a genocidal afterthought. However, these rankings might shift and adopt an arbitrary ordering depending upon the nature, number, and type of measures chosen for the genetic tuple describing these relative strengths. So, as it oft has been said, “Statistics might lie; and, liars might use statistics.” Yet, Shockley’s work in the social sciences is rarely questioned. This is a function of his social demographic, earnt station in life, and “expert” power.

Most likely, Shockley’s sequential series of populations curves should coincide perfectly with aligned medians. The only difference would be the relative sizes of each normal curve based upon the corresponding population sizes of each group. Yet, that was a brief digression.

Few students in this generation will dare ask an instructor a question for fear of the coming wrath. Which might be dealt out by an insecure professor or peers who are hoping that they keep the average level of performance in the course exceedingly low. This, academic apathy, is the greatest factor limiting the progress made in the modern sciences.

This “insight” has applicability in language design, compiler construction, architecture, or theory. This observation is so incredibly trivial that it does not merit a formal publication. Although, it might potentially invalidate a number of instances of proof-work found in the modern theory of computation as described within Computability, Complexity, and Languages: Fundamentals of Theoretical Computer Science 2nd Edition by Martin Davis, Ron Sigal, and Elaine J. Weyuker. As such, a greater range of problem classes might be computable. Hence, a wider spectrum of problems might be solvable.

Homeboy From Heaven [JOD: Psalm 119:73 – 80 (KJV)]