(updated - more formal, removed some parts and improved general clarity)

Over years, I come again and again back to Halting Problem and it's unsolvability ..now I have created a system, which is theoretically able to find halting problems in far larger class of systems than just FSM's.

It's based on what I call topological identicalness of abstractions and abstraction of programs - it could, basically, prove somewhat different programs identical if they follow the same logic. It is not meant to be runnable on normal computer - it takes a lot of memory. It's, right now, a pure theory. When it's ready as theory, it could be optimized into something practical - but that would be rather special cases.

The main things here are:

• To define what it is for program to hang.
• To find a general prover, which could check any program against this definition.

There are 4 class of programs:

1. Finish their job - they can be run and nothing more is needed to eventually know that.
2. Go into infinite repeating cycle - those are FSM's and could be detected by normal static analysis.
3. Go into growing cycle - those are infinite state machines and this text targets those.
4. Fall into halting paradox - those are possible in case something claims to be a solver; this here tries to address that, but I'm not yet perfectly sure in that.

To get 3rd class of programs detected, there are two things needed:

1. A method to prove in each case formally that they do not halt.
2. A method to make those formal cases enumerable so that they could all be reached.

If both are addressed, we would have general solver for halting problem.

Topological identicalness of computer programs

We can order the possible states of any program into finite or infinite (on Turing machine) set. With combinatorics, we can create supersets, which contain all possible sets of these states so that no two sets contain the same element.

This means:

The following is about mathematical set symbols I am going to use. I repeat more important definitions in slightly different wordings so that one can check them against each other for understanding better or chose most convenient one; I know it could be fuzzy otherwise.

Let's call the set of all program states S(p), where p is a program or abstraction. S(p) contains all possible states of this program as a state machine; for infinitely growing programs on Turing machine it contains all distinct (different) states on that program's entire lifetime. Thus it could contain infinite number of states.

Let's create a function U(S(p)), where U contains all state groups of S(p). I call any member of U(S(p) G(S(p)) or simply G, when talking abstractly about common properties of such sets. G(S(p)) is a set of sets of states of S(p), which I call state groups. Each state group, member of G, is set of possible states of state machine p. G does not contain empty set nor two groups, which have a shared member. It might contain one state group containing all elements of S(p).

State groups of S(p) are sets of possible states of S(p). G(S(p)) contains a set of distinct state groups having no overlapping members. U(S(p)) contains all such G(S(p))'s we can form. G is a shortcut for any such set of distinct state groups.

For example, if p has three possible states: A, B, C, then G(S(p)) is any of the following: {(A), (B), (C)}, {(A, B, C)}, {(A, B), (C)}, {(A), (B, C)}, {(A, C), (B)}. In such case, U(S(p)) = { G; G = any of G(S(p)) }, which means that U(S(p)) is set of all G's for p.

I call Z(p) a set of all possible sets of states in S(p).

This repeating was meant to allow to check that it's clear as it's needed for what follows. When I speak about G, I mean any allowed set of state groups, any member of U. One of G-s will also contain state groups with one element in each (unless in some cases of infinite state machine) - this G contains each element of S as state group.

So, terms currently introduced:

• U is an universe of all possible state groups; U(S(p)) is clearly defined, but actually U in general will contain more of them.
• G is a set of all possible state groups for a program, which are distinct to each other. In actuality, I will use G for any states into which this state machine can perform a transition into. I will add elements to G in progress of this text. G(S(p)) is mostly needed to explain the process of abstraction.
• S is a set of all allowed states of a state machine or abstraction. S(p) is a set of all possible states of a program - this is a very straightforward set, which contains, for finite state machines, only the actual states of that machine; S(a) of an abstraction might also contain combined states of that abstraction, but inside an abstraction, they are always straightforward.
• Z is a set of all possible combinations of allowed states. Z(p) does contain all elements contained in any G(S(p)).

Now, for each state in set S there is a state, which will follow it when program is running. I will call this X=>Y, when this notation does not clearly be an implication, where X and Y are members of S and X will directly cause Y when program is running. If X=>Y, then state X at time moment t means that there is state Y at cycle t+1.

I also speak about transformation rules of members of Z, state groups. I say that state group X directly causes state group Y if X=>Y such that X and Y belong to Z and for every member x of X there is x=>y in effect such that y is some member of Y. This means that if X=>Y, each state in group X must cause some state in group Y for next cycle.

Let's call G an abstraction of a state machine - it is one aspect of it.

I bring an example:

There is a state machine such that:
States: A, B, C belong to S(m1).
Rules: A=>C, B=>C, C=>A.

Then there is another state machine such that:
States: D, E belong to S(m2).
Rules: D=>E, E=>D.

Now, if we make such abstraction of first state machine:
State groups: (A, B), (C) belong to Z(m1) and form some G(S(m1)).
Then we get the following rules:
Rules: (A, B)=>(C), (C)=>(A, B)
C does not produce B, but it produces a state group of (A, B) as it produces any member of it.

So, we can say that there is such abstraction of first state machine, which is topologically identical to second state machine, because both contain two state groups with identical rules between them. We could group abstractions formed by using some G(S(x)) first-order abstractions. In actual reality we would often use Z(y) in place of G(S(x)), where y is some abstract machine - this way, we can draw all possible implications about a state machine's activity on given cycle.

Now, we have a formal rules to do abstractions of state machines. As there are abstractions, there also come the communication channels - we can abstract a state machine into two state machines, which communicate with each other.

We can, for example, have two operations in iteration adding numbers one by one and when they reach 3, they will start from zero again; this iteration is part of a function, which can be called with different starting points. This state machine has 9 states in total. Abstractions of those states will divide this state machine effectively into two state machines, which do not interact with each other - one abstraction would divide them into 3 groups, which contain members each of which imply another. This means - U(S(f)) of that state machine f contains two abstractions, which both count numbers and are topologically identical. There are two such G's for which that applies. This also means that when looking to Z(f), we can find two sets of state groups for which x=>y=>z=>x.

Z(p), where p is infinitely growing machine - infinite state machine - will contain infinite number of state groups, which all are countable. For each cycle of program's work, which does not repeat some historical situation, we can add new state x to S(p) and all sets containing x and zero or more other members of S(p) into Z(p). Thus, Z(p) is enumerable for any state machine.

By abstracting infinite state machines, we will get finite state machines, which we can fully analyze.

State series

Topological identicalness discussed for now could be called "strict identicalness" of abstractions.

We can now form another set of states, which will contain several states following each other.

For example, if A=>B and B=>C, then we could form an arrangement ABC.

Now, if we have such state machine:
Rules: A=>B, B=>C, C=>D, D=>A

Then we see it also implies such state machine:
Rules: ABC=>D, D=>A

By allowing such arrangements in our state sets, we will get a new layer of abstractions. Elements of such sets must have their length as second element.

I will call this set T(Z(p)) or T - by this I mean that we have added time. All possible arrangements we can form from Z(p) are combined in T(Z(p)). G(T) would be shortcut for G containing sets of arrangements of Z(p). Elements of such G do not have to be of same length, thus we also need len(x), where x is a member of T, S or Z and contains the number of cycles such state will remain unchanged. When we have built an abstract machine of such arrangements and arrange them again, length of such arrangement of arrangements is sum of their lengths.

Now, the last and most important of them all - R. R is the combination of all groups of all elements of S and all arrangements we can form from them. R, for any finite S, is finite and for any enumerable S, enumerable. G(R(p)) or - in context - G(R), contains all possible abstractions we can make from a program (abstractions are subsets of possible G-s). R itself is a total sum of abstractions - implication rules of elements of R cover all implication rules of a program as it's elements cover all elements of a program.

State machine abstractions combined

When we abstract a state machine, we will get several state machines, which might interact with each other in several ways.

This means - for any abstraction G of R, there is one such G of R in combination with which the whole program logic could be fully reproduced. I call this a context of G or ~G. Sometimes, this does not matter to G, what happens with ~G - whatever possible states ~G happens to go into, G continues it's determined execution path. In such case G is independent. Context might also be independent from G. G might be independent as long as it stays in some specific state group. Until now, we have looked abstractions - G's - in such way that they have nothing to do with the rest of R. Anyway, R might contain a lot of implication rules (as they are there with states) and additional state arrangement groups, which directly affect some G they directly don't belong to - they can be used to draw conclusions about G. Those implication rules form some smallest G, which is independent itself (anyway, it could be a program itself) - this I call a neighborhood of G.

We can work out rules about the ways they interact with each other. Most interesting interaction rules are restrictions to interactions, which can only be found by looking several machines in combination. For example, one abstract machine G can be proven to not intervene into memory requests of another or to not send any signal before it has got a specific signal. As those interactions involve some time - one machine can, for example, wait for signals only each second tick and leave unnoticed any signals at other times or do different things with signals dependent on timing.

For analyzing any abstract machine, we must make the set of rules of interactions. For interesting abstractions, we usually find such state group that as long as our abstract machine does not leave it, it will also not be interrupted. If it will get signals so systematically that they could be as well included in it's own state groups, we might have chosen a wrong abstraction.

This is normal that in a program run, abstract machines will be created and destroyed. We can find rules covering some specific machines, which is often created, to specify the logic of our whole system.

Indefinite growth of computer programs as topologically equivalent subsequent state machines

We can now formulate:

In case some G_x produces such G_y that G_x==G_y - they are topologically identical -, we can call this a child of that G_x. In case this is a direct result of G_x - any G_x produces such G_y that it's identical to G_x we will call this cycle - in this case, infinite cycle. As we develop the internal rules of state machines, we also look them as a whole - we do implications about their relations. For a child of G_x we will have some slots connecting it to it's parent. We can specify those slots as we do more implications, but basically - getting a child will mean abstract relations, pointers. Child of G_x might have direct connections with other abstraction systems with which G_x has connections; it might have connections with children of those abstractions, G's, connected with G_x and it might have connections with G_x itself - which is a very common case. In latter case, it might have some connection to G_x in such way that it's children would also have connection with G_x, but it might have such that for it's children, the same implication rules produce connection with itself. There is finite number of classes of such connections - those can be expressed as paths in network of relatives. Some paths are absolute (as the topmost G is connected to all G's) and some paths are relative - they are implied from rules of abstraction itself about itself. You see that each context has a local R.

Now we see, what should be happening inside a solver:

• It grows a network of logic of each G.
• It finds all topologically identical G's.
• It understands, which G's are guaranteed to produce which G's and which will be their connections - parent could connect a child with it's own relatives and child could produce it's own.
• Some parts of it's activities are based on studying G's - abstractions and their direct implications - and others are based on studying the whole - drawing logical connections between abstractions based on what is known. When studying abstractions, it will look their growth in time and convert that into implication rules - it will also know, which rules are necessary and enough to produce which rules; there might be several sets of such relative axioms for any rule. When studying the whole, it will make deductions based on rules it has found, thus removing many states from different G's - showing that based on what is known, they will never be reached; it will also find any kind of cycles.

About cycles, there is such knowledge, which we can find:

• If some abstraction has a possibility to produce a child (by the way, the parent-child word use is just for convenience, most probably the same child is looked as being child of several abstractions at once etc., the logic between abstractions will largely overlap), then which states will produce it - partially, this is a local analysis of an abstraction.
• If some abstraction is in such relation to others, then local analysis of abstractions will be connected - if one abstraction has rule that it will not send signal x to another in case that other will not signal y and vice versa, another has the same rule, then the possibility to get signal x will be removed from both, which could simplify the world; same kind of global analysis are needed to make the cycles exact - if child is told to not go into state x unless parent goes into state x, state x will be removed.
• There could be any kind of complex state logic. It can be analyzed that some state will be definitely reached or definitely reached in case some other state of connected abstraction will be reached; etc..

An abstract machine will born whenever some abstraction can be applied to some local R. It is destroyed when it can not anymore. It has signals and timing of destroyment. Each abstraction is finite state machine and can be fully analyzed in relation to it's connections to outer world - it's basically a random bunch of states applicable to R at any given moment. It's highly probable that most abstractions live for only one cycle at any given birth. Anyway, we will analyze all abstractions thoroughly, then analyze fully the results of this analysis, apply the results to currently active state system and then find new abstractions to analyze. New states come from the fact that our program grows in process of analysis - most notably, in 1D Cellular Automata context, we will analyze some number of cells with given length; as a result of this analysis process, we will produce some transitions, which will change the state of neighbor cell - ask for some new memory. Through this we will have a bunch of new state groups to analyze - we have added a number of elements to global R and now start analyzing the next iteration of it.

An actual logic of hanging is that some abstraction will produce independent child identical to it. Independent means that this child does not go into any state, which would result in state of parent program, which would destroy it. By analyzing an abstraction, we will find the behavior of abstraction; by analyzing the whole, we will find parent-child relations and also parent's relations to it's context. We will also make notice about which implication rulesets are needed to produce such child and if they are guaranteed to be met in child just because they are met in parent - if this is so and the program logic is waiting behind a child, we have detected a normal hanging condition.

What about halting problem unsolvability proof of Turing?

This needs proof that it detects halting problem; it also needs counterexamples about programs, which would be mistakenly detected or a proof that there are none.

Turing's proof has, as one of it's assumptions, an idea that a program, which does halt, could not be considered as not halting. If we could show, formally, that ideed, there is a way to define programs, which are all wrong even if they halt - then it's way to go. This means - we will not disprove the proof of Turing by that, but we might find an exact definition about when this happens. I think that my formulation applies and is detectable with methods described here.

If we can prove that parent produces topologically identical child because of reasons, which are there for a child to produce the next iteration; and we can prove that parent waits for child and it's actions depend on child's decision - I think that no sane program will do that. And we have the logic covered to reach such deduction.

Which Turing-complete machine can be fully described in such way?

My favorite is 1D Cellular Automata. It has been shown that one can fully model Turing machine on 1D CA - such Cellular Automata is Turing-complete.

Cellular Automata is very simple thing. 1D CA in principially infinite array of cells. Each cell has a position, which can addressed as integer on that CA (I think we can make it bounded at beginning so that it would be a natural number as non-bounded 1D CA can also modeled as topologically equivalent bounded-at-beginning CA). Each cell is finite state machine, which is connected to it's local neighbors - cells directly before and after it. For any program with finite code, it would be started with some finite number of cells having non-zero value. Programs can take more space in their activities.

We can make all possible abstractions from first condition and then start running them cycle-by-cycle. In process, new cells might go into non-zero value - thus, an initial automata is connected with one "infinity cell", which has properties of infinity. It can change it's state and this activity can be easily described as simple state change - basically, first cell of infinity is included in this first abstraction set with it's state group.

How to represent those abstractions and their relations?

As careful reading has shown, we do implications about abstractions using data about their context. This means that each abstraction, in reality, will produce restricted abstractions - such abstractions, which already contain some relevant logic of their context. Context can be infinitely growing, thus is often leaves some things open. This is critical to have good model of how this context is expressed.

For an abstract machine, as it's groups combine several groups, it is known, which groups have transitions into which groups - for example, A=>B is clear rule, but sometimes there is no such direct group that if A=>B and C=>D and groups are (A, C), (B), (D), then (A, C) has some clear transition rule into some other group. If we look at Z of this abstract machine, it also contains (B, D) - so we could say that (A, C)=>(B, D). For keeping our abstract machines simple we say that (A, C) has implication rule into two groups - for that, we need potential implication rule. Let's name it ≃> so that (A, C)≃(B) and (A, C)≃(D) and thus, (A, C)!≃(E), for example. A group can have a rule (A, C)≃(A, C) in case one of them have transition rule into member of the same group. We also need a "destroyed" state here, which is the situation after which the world of that state machine goes into some state, which does not belong into it's allowed states. Right now, anyway, we have defined our G in such way that this is not visible, how that could happen - any G has group of any allowed state of system. Anyway, things get more complex when we are allowed to detect cycles - child of a cycle carries some set of implication rules together from parent, but not all of them. Thus, if we see that child has an abstraction, which is topologically identical to abstraction of parent, we create an abstract machine, which only contains those implication rules, which are carried through indefinitely. Such abstract machine has a "destroyed" state group. Let's call this machine M as in meta. Such machines will be found by global analysis of contexts and in their context, new R will be formed - new world, which allows another set of abstractions. States of M are often partially undetermined, but even as such, all known transitions can be fully analyzed. Here we have defined cycles (C was not available) and partial abstractions; cycle is partial abstraction and partial abstractions can have exit state (this state can be reduced out by global analysis).

As global analysis reduces out some states, which are not going to happen - for example, it becomes clear that some cycle will exit only if it gets signal from parent, but it never sends signal to child nor does context send that signal, thus an exit state will be deleted. This produces also reduced abstract machines - each reduced abstract machine is normal abstract machine, each reduced partial abstract machine is normal partial abstract machine.

A notion that some event will produce a specific group of R and this group always produces itself if formal way to say that some states imply that a machine will definitely reach some state group and stay in it infinitely. As there is "destroy" state of abstraction, there are also numerous groups containing it. There is also a group, which contains all states except "destroy" state - if this group is immortal, then that machine will never be destroyed. This shows that static analyzer can have a specific formal knowledge of restricted abstract machines, which leads, for example, to knowledge of hanging.

Reduction of partial abstract machine is achieved in two ways:

• By removing some states or transition possibilities from it - for each finite machine, there is a finite set of such partial machines, because there is finite number of states and rules you can remove. By removing one of two ≃> rules, you will get one => rule as it becomes exact. Thus, such reduction is a good thing - it might make abstract machines behavior more determined. It allows to detect new cycles - for example that some machine will stay in state group x of it's R whenever it reaches some state of this group. By that it would also produce reduced version of itself on place of itself, which also means a reduction into dependent parent etc. This is an example about how state machines could be born - in this case, it would be born at the same abstract space where it's parent is located, without destroying it's parent.
• By adding some state transition rules. We can abstract the potential reactions of context as specific state machine connected to our own. For example, if some state transition of our state machine is related to parent in such way that if it sends signal A to parent (goes into any state of group, which we can call signal A), then parent will send signal B to it (change some shared part of state in such way that it will go into state, which is part of group B). Abstracting parent in such way we could get an abstract machine, which will have four states - waiting for signal (C), getting signal (A), doing inner work (D), sending signal (B). Doing inner work is a state arrangement - it could contain, for example, the state group of all elements in S in arrangement of so many cycles as many cycles it takes for parent to finish it's job. It could hypothetically also contain a cycle M - as cycle has undefined length, it could then take more or less time. For arrangement, things are straightforward - if arrangement length is fixed, then we could just make a deduction of our state machine (I basically use that word to differentiate from reduction as this differentiation is very important). This means - as both abstract machines are FSMs (we always locally work with FSMs), we can do things similar to this: if one state machine of two has 4-cycle length and another has 5-cycle length and they are related, we can make up 20-cycle length (LCM) machine and have combined states in it. This would not change our current state groups if we want to keep them (for example to check for topological overlapping of state logic with other machines, which start up from the same machine), but it would produce four specific cases for each state and a new set of implication rules. Anyway, if cycle length is indefinite, it would produce infinite number of states. Luckily, we can use a different practice with cycles - instead of telling that there is connection with cycle, we will tell a specific instance of cycle. In case our connected neighbor is first element of that cycle and we are first element of our cycle and the transition rules of our child are related to transition rules to it's child, we can combine them. In such combination we can add up different arrangements - for example, if the arrangements we have to wait are G and H for parent cycle in form of GH, but GHH for it's child and GHHH for it's child, we need to have state group J, which contains GH for first element of that cycle and JH for second element. In such way we can always keep the relation correct. Rules of abstract child machine can always only build things from states and arrangements of their parents - this means summing them together or using directly. In case there is some more complex logic, we simply wait until this logic has been analyzed enough to draw important conclusions - we would not allow our checker to try to form cycles with more complex mathematical structure, because all patterns (and we are seeking for patterns, remember) can be implied from them. Anyway, the structure of pointers is important - we always need to keep account of all groups of implication rules, which produce something; for non-cycle, those are the basic rules; for cycle, there are cycle-local rules, which are the rules, which children give to their children precisely because they are given to themselves in the same form. Those form a local ruleset of a child. When making abstract relations to cycles, we will keep the data about those connection structures and have a way to create pointers to how far in this structure we need - in case we are connected to M_x of some cycle because of the rules we inherit to our children unimpact, they will be connected to things in their relation to M_x - this can be that our child is connected to M_y = M_x+1 and thus it's child is connected to M_y+1; but it can be that it is connected to M_y = M_x and it's child is connected to M_y because of that. And if M_x is connected to M_x-1 and this connection has any relevance into how it interacts with us, then there must be a possibility to do global analysis in relation of our child and M_x-1. Only in case neither side is dependent of other is there no need to allow such connection or do some global analysis of them in pair.