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)]
