For anyone who finds this sort of discussion interesting, I highly recommend reading Chapter 3 of The Structure and Interpretation of Computer Programs. There is quite a bit of philosophical musing about the connection between time and state. For example:
> The basic phenomenon here is that synchronizing different processes, establishing shared state, or imposing an order on events requires communication among the processes. In essence, any notion of time in concurrency control must be intimately tied to communication. It is intriguing that a similar connection between time and communication also arises in the Theory of Relativity, where the speed of light (the fastest signal that can be used to synchronize events) is a fundamental constant relating time and space. The complexities we encounter in dealing with time and state in our computational models may in fact mirror a fundamental complexity of the physical universe.
Thanks for sharing that. Einstein and Minkowski knew perfectly well that space and time are inseparable over 100 years ago.
>Not sure what religion has to do with it.
>absolute time is not falsifiable…you have to believe in it.
Either time is a necessary condition for experience, or it’s a measurable object of experience. It can’t be both. You can’t have time in time. Which one do you believe in?
Are you saying: Lets say a Theory of Everything is found, it explains Relativity, and Quantum Mechanics, Gravity, . Everything is tied together. And, this theory does not have Time. Time is just a side effect we can measure. But, at that point, you would still need some 'belief'? Because it is so far beyond our ability to perceive it maybe?
Or, another way. Even a Theory of Everything, at it's root is just Math, it isn't 'what the universe actually is'. So we'd still need belief?
Looking at some of these screenshots, this is such a fantastic idea that it is surprising it wasn't done earlier. Magit has the perfect interface, why shouldn't everything be like that? Who wants to read the Info manual anyway? Info, Dired, Calc, obviously. Org mode, of course.
Maybe other people have been working separately on similar ideas? Really it is extremely obvious in retrospect that everything should have a Magit style interface. Ultimately, it would be great if that were the default, generally assumed style throughout Emacs. It would be great if all that effort could be coordinated and merged into the main distribution. Built-in, no external packages.
Well said. The Magit interface is such a pleasure to use, sometimes I will modify and rearrange commits just for fun. A Magit-style interface for Calc seems like a great idea.
> We are selecting for the maximally pathological machines.
This is not quite right. We're selecting for maximally long-running (or mark-producing, etc) programs. Whether those programs turn out to be "pathological" in some sense is an open question, and a question that can only be answered (to a limited extent) by observing and analyzing actual champion machines. Apriori, there's nothing we can say about what a champion program will do or what its code will be like. The Spaghetti Code Conjecture says that these champion programs will tend to be complicated. I have argued in the past that this may not be the case. It's entirely possible that the code of a champion program will be written more or less straightforwardly, and its long-running-ness comes from executing some bizarre and exotic mathematical function.
Actually, I think the more likely outcome is that some champions will be spaghetti and some will be clean. If they were all spaghetti or all clean, then that fact could be exploited to speed up the search process by discarding all programs not matching the property. And that sounds too good to be true, so it probably isn't. Maybe BB(8) champion is clean, BB(9) is spaghetti, etc, and there are no reliable trends.
> past BB(3), there isn't any known size where the champion machines for Σ(n) and S(n) are different.
My feeling is that this trend cannot continue forever, and for infinitely many N they are different. If they are always the same, then you could find the steps champion just by finding the marks champion. This would be convenient, because as you pointed out, steps are more logically important, while marks are more practically important. But this feels too good to be true, and so it probably isn't.
Hmm, around n = 2 or k = 2, there are only 2 added transitions for a machine to do "the next big thing" googologically, so that doesn't leave much slack for many different machines at the same level. But maybe that could happen closer to the n = k line, where each increment adds many new transitions. Or to the contrary, maybe each increment just does several "next big things".
Busy Beaver champion programs are said to run for super-exponentially many steps. But nobody has actually run their simulators for that many steps. Instead, simulators can prove tape fast-forwarding rules. Basically, you look for repeating tape patterns. If you can prove the pattern is correct, then you can apply that transformation again if some tape circumstance shows up again.
For example (using run-length encoding),
1^n 0 1^m
might become
1^(n-1) 0 1^(m+2)
When the rule is applied, the transformation is applied directly to the tape, generally by manipulating some count variables.
Now, how many machine steps does it take to apply this transformation? Well, TBH I'm not really sure. It seems kinda complicated, especially when the rules get more elaborate. If you are trying to run your simulator as fast as possible, you probably don't want to bother calculating it at all anyway, since you can always rerun the analysis at a more leisurely pace later.
So when I say that marks are "more practically important", I mean that marks are central to the operation of advanced simulators, whereas steps are a derived afterthought value.
Logically, the steps are more important, since they give you an easy method for solving the halting problem for the state/color class.
So far, the markiest programs are also the steppiest. My conjecture is that they will turn out to be different in infinitely many classes. If they were always the same, you would be able to get the logical primacy of steps just from working with marks. And that sounds too good to be true.
Congratulations to the team! So the (blank tape) halting problem is solved for 5-state 2-color Turing machine programs. Has anyone tried applying these same techniques to the 2-state 4-color case? That seems like it would probably be tractable, although generally speaking colors are more powerful than states, so there might be some surprises there. (6-state 2-color and 2-state 5-color both seem intractable, perhaps even provably so.)
By the way, there is an extremely stupid but disturbingly widespread idea that humans are able to just intuit solutions to the halting problem, using the mind's eye or quantum mechanics in the brain or whatever. Needless to say, this did not factor into the proof.
> Has anyone tried applying these same techniques to the 2-color 4-state case?
I assume you mean the 4-color case. As I understand it, the deciders currently in use are sufficient to prove all the 2×4 holdouts non-halting. So the current champion gives us Σ(2,4) = 2,050 and S(2,4) = 3,932,964, barring some big errors in the decider design. The result just hasn't been organized in one place.
> (6-state 2-color and 2-state 5-color both seem intractable, perhaps even provably so.)
Yes, 2×5 has the Hydra, and 6×2 has the Antihydra, which compute the same iteration, but with different starting points and halting conditions. The standard conjecture (related to Mahler's 3/2 problem) is that this iteration is uniformly distributed mod 2, and a proof of that conjecture would very likely prove both machines non-halting, by yielding suprema and infima on the cumulative ratio of 0s to 1s. But of course there is no known method of proof.
> By the way, there is an extremely stupid but disturbingly widespread idea that humans are able to just intuit solutions to the halting problem, using the mind's eye or quantum mechanics in the brain or whatever. Needless to say, this did not factor into the proof.
The year is 52,000 CE and humans have solved BB(18) in the sense of exhaustively categorizing halting vs non-halting 19-state no-input programs. They have used a proof generator based on a logical theory called Aleph*, and at that time it had been known for 1.5k years that ZFC is incapable of establishing BB(18).
Compared to the year 2024 CE, considerable millennia before Aleph* came into use, it is clear that no program written at that point in history was capable of even using brute force proof checking to solve BB(18) in theory (like how we can enumerate and check ZFC proofs today to solve BB(??) in theory).
That's what is meant by the "humans intuit solutions to the halting problem" position. AFAIK, there's no known hard, theoretical reason why the above laid out future history cannot take place. And due to BB being incomputable, humans had to develop new theory to be able to construct the programs required. Something has to be accredited for the results, and it can't be computation since the programs did not exist.
> AFAIK, there's no known hard, theoretical reason why the above laid out future history cannot take place.
Probably the biggest issue is that they'd have no method to establish that Aleph* is consistent. To continue this BB chain indefinitely, you must invent further and further first-order theories, each of which might not be consistent, let alone Σ₁-sound. And with an Σ₁-unsound theory, any halting proof might not hold up in the standard model of the integers. You'd effectively have to postulate an indefinite amount of oracular knowledge.
Also, another physical issue: you can show that within any consistent, recursively axiomatizable theory, the length of the shortest proof of "the longest-running n-state machine is M" must grow at an uncomputable rate in terms of n. Ditto for the shortest proof of "machine M halts", where M is factually the longest-running n-state machine. Otherwise, a machine could use a computable bound on the proof length to solve the halting problem. Therefore, the proof should very quickly become too large to fit within our light cone.
In any case, the BB-related evidence for that position rested on BB(5) being determinable by extending the techniques used for BB(4). But in fact, it turns out that similar extensions don't even get you to BB(6). So there isn't anything to support the position, other than the pure speculation that anything is physically achievable given enough time.
How do we know that there would be consistency issues or Σ₁-soundness issues?
Your claim about proof size categorizing n-state machine halting status is new to me. Do you have any links to read more about this?
The argument doesn't make sense to me. Rather it seems like more of a consequence of BB being incomputable in the first place. The proof sizes for each BB(n) aren't expected to be computable at all. There is necessarily a different theory for each n (or intervals of n where each theory applies with limits on each).
> So there isn't anything to support the position, other than the pure speculation that anything is physically achievable given enough time.
Something something burden of proof something. It would be extremely fascinating to have a conclusive argument that large BB numbers cannot be solved.
> How do we know that there would be consistency issues or Σ₁-soundness issues?
From Gödel's second incompleteness theorem, no consistent first-order recursively-axiomatizable theory (i.e., a theory that can have its proofs validated by a Turing machine) can prove its own consistency. Thus, to prove that your current theory (e.g., ZFC) is consistent, you must move to a stronger one (e.g., Aleph*). But then you can't prove the consistency of that without an even stronger theory, and so on. Thus, you end up with an infinite regression, and you can't ultimately prove the consistency of any of these theories.
> Your claim about proof size categorizing n-state machine halting status is new to me. Do you have any links to read more about this?
Not really, other than some of my own ramblings on the bbchallenge Discord server. But it's not that long:
Suppose that the longest-running n-state machine M can always be proven to halt using a proof of under f(n) symbols, where f(n) is some fixed computable function. Then, you could construct a TM that, given n, enumerates every valid proof of length less than f(n) symbols, and checks whether it shows that a particular n-state machine halts. The TM then simulates all of the proven halters to see how long they run. By assumption, the longest-running machine M is included in this list. So this TM can compute BB(n), which is an impossibility. Therefore, the function f(n) cannot exist.
As a corollary, since it's "uncomputably difficult" to prove that the longest-running machine halts at all, it's no less difficult to fully establish the value of BB(n).
> Thus, you end up with an infinite regression, and you can't ultimately prove the consistency of any of these theories.
There is similar issue with even ZFC and PA. It’s not really a dealbreaker imo.
> Suppose that the longest-running n-state machine M can always be proven to halt using a proof of under f(n) symbols, where f(n) is some fixed computable function. Then, you could construct a TM that, given n, enumerates every valid proof of length less than f(n) symbols
The issue with that argument is that the TM which enumerates every valid proof can’t exist in the first place.
If you fix an axiomatic theory, it’s already known that the theory has a limit.[1]
If every theory has a limit, you need countably infinitely many axiomatic theories together to prove BB(n) for all n. So there’s no TM which can even enumerate all the proofs, since a TM must have finite states, and thus can’t enumerate infinitely many proof systems.
(In fact for similar reasons I believe a Halt program, which has infinite states but which works for all TMs with finite states, platonically exists. It’s an emulator and an infinitely long busy beaver number lookup table. The diagonalization argument doesn’t apply, since the infinite Halt doesn’t accept itself as input.
This Halt would have countably many states since each busy beaver number is finitely calculated and there’s only countably many of them.)
So it’s not clear that f(n) is uncomputable. If f(n) is the symbol count and not the binary encoded length of the symbols, it even seems that it’s trivially bounded by some constant for all n. The proof could be one symbol the meaning of which is encoded in the theory.
It is a fascinating question though. I’m sure there is some function of axiomatic theory proof checker TM size and binary encoded proof length which does grow with n. It’s unclear if it would be uncomputable though.
The consequence of it being uncomputable is that the universe doesn’t have the resources to even encode the theory and/or represent it’s proofs.
In fact I suppose even as long as it grows at all, there would be a limit to BB(n) which can be possibly determined. Very fascinating
> There is similar issue with even ZFC and PA. It’s not really a dealbreaker imo.
We obtain PA from our basic intuitions about how the standard integers work, derived from empirical evidence. Everything past that involves increasing levels of intuition. So to continue it indefinitely, you must postulate an infinite amount of correct intuition, in some magical fashion that can never be captured in a computer. You can claim unlimited ingenuity all you want, but there's no a priori reason that it should indefinitely yield the truth, especially when it goes far, far past what our finite empiricism can provide.
We just haven't hit these limits yet, since very weak inductive theories are still sufficient for proving BB(5): we don't even need the full power of PA yet for our non-halting proofs. Thus why it looks like it should be so easy.
> If you fix an axiomatic theory, it’s already known that the theory has a limit.[1]
Not quite. Fix some consistent axiomatic theory T which proves PA. Then there will be infinitely many TMs which do not halt (in the standard model), but T cannot prove that they cannot halt, due to incompleteness. (Therefore T cannot settle the BB(n) question past a certain point, as Aaronson correctly says.)
But for every TM that does halt (in the standard model), T can prove that it halts, and the proof is to list out a trace of the TM's execution. Thus, every halting machine of every length has a halting proof in T.
The only benefit of a more powerful theory T is that it can "compress" this maximal BB(n)-sized proof into something more physically managable. But once we fix a certain T, we find (by my earlier argument) that it can only compress the proof so far, and the compressed size still must be an uncomputable function.
We can also see this by a forward argument, instead of by contradiction. Suppose that we'll accept any halting proof in a theory T. Then we can write a TM that lists through all proofs in T that are smaller than some bound N. (Notice that this is a finite set, since I've put an upper bound on it!) Then, for every proof that is a valid halting proof, the TM runs the corresponding machine. Then, the TM will halt, and its halting time will be greater than the halting time of any machine that can be proven to halt in T within N symbols. Set N to Graham's number (which is easily definable), and now the halting proof of the TM in T will not fit in our light cone.
(Notice how our TM clearly halts if T is Σ₁-sound! But since T cannot prove its own Σ₁-soundness, it doesn't have any way to prove our TM halting other than by the brute-force method.)
> In fact for similar reasons I believe a Halt program, which has infinite states but which works for all TMs with finite states, platonically exists. It’s an emulator and an infinitely long busy beaver number lookup table. The diagonalization argument doesn’t apply, since the infinite Halt doesn’t accept itself as input.
In that case, you just end up with the well-known oracle halting problem, where you equip a TM with access to this "infinite-state" machine. Then the problem is that you have a more powerful model of computation, but still with no way of solving its own halting problem. Much like how a consistent theory can only prove the consistency of weaker theories, not its own consistency.
> So it’s not clear that f(n) is uncomputable. If f(n) is the symbol count and not the binary encoded length of the symbols, it even seems that it’s trivially bounded by some constant for all n. The proof could be one symbol the meaning of which is encoded in the theory.
Of course I'm fixing a particular theory and a particular alphabet of constant size, the alternative would be absurd. The important part is about the ultimate behavior as n varies.
Thanks for typing all that out. It is very fascinating.
I’m just not convinced that fixing a theory and disallowing soundness axioms is any practical impairment for discovering busy beaver numbers.
Of course things get out of hand, but then why not collect evidence for soundness and let proofs avoid including an actual execution of the TM?
We don’t need a printout of grahams number computation to know a TM which computes it halts. why impose that here?
Has anybody done a compilation of such a PA proof generating/checking and simulating TM? It must have an enormous number of states and almost certainly wouldn’t be the BB of its cohort. Not including how it should be a similar thing where to prove it’s step count we shouldn’t need to emulate it.
> We don’t need a printout of grahams number computation to know a TM which computes it halts. why impose that here?
Of course, the TM which "computes Graham's number" can trivially be proven to halt, without running it fully.
But it is much harder to show that the TM (let's call it M) which "computes Graham's number, then plugs it into a big halting-proof generator (in a fixed theory T) as an upper bound on the number of symbols, then executes each proven-halting TM in order" also halts.
The problem is, just because a theory T gives a halting proof for a machine, doesn't necessarily mean that it halts. (That is, T isn't necessarily Σ₁-sound.) And if that doesn't hold, then M might run into a "fake halter" that can be proven halting in T, but doesn't truly halt in the standard model. Thus, the only ways to show that M halts are to either establish that T is Σ₁-sound, which can only be done by appealing to a stronger theory, or to run through each of the Graham's number of proofs, which takes astronomically long.
This is similar to an instance of the Berry paradox: if you could easily prove that M halts, then it would have a relatively short halting proof within T. But then it would find its own halting proof, and simulate itself. But then it would simulate itself simulating itself, etc., etc., and never actually halt. So T wouldn't be Σ₁-sound, since M doesn't halt even though you proved that it halts. The only way out of this trap is if M doesn't simulate itself, i.e., it takes more than Graham's number of symbols in its own halting proof in T.
> They have used a proof generator based on a logical theory...
I don't understand your scenario. If they're using a proof generator, that sounds like the opposite of intuiting or using the human mind. Maybe they used "intuition" to come up with new axioms for a logical theory, but that is not the same as determining of some particular concrete TM program whether or not it halts.
You got it - the creative developments of a stronger theory. This allows the creation of tools which can categorize TMs, tools which wouldn’t exist otherwise.
It’s fascinating that the entire space of finite amounts of random gibberish contains every such stronger theory.
As a thought experiment it does well. Interestingly the Church-Turing thesis seems to exclude ingenuity. That is, it doesn’t try to say there aren’t functions on natural numbers which are uncomputable but can be calculated with ingenuity. Seems that a ton of people conflate those things.
I don’t have the understanding, but apparently there are finitary statements which are independent of ZFC. This has been used to prove that BB(745) is independent of ZFC.
Furthermore, Scott aaronson jokingly conjectured that even BB(20) is independent of ZFC. That’s my reference here where we end up needing Aleph* for BB(18).
> Let me state that without my notes Shade's text simply has no human reality at all, since the human reality of such a poem as his ... has to depend entirely on the reality of its author and his surroundings, attachments and so forth, a reality that only my notes can provide. To this statement my dear poet would probably not have subscribed, but, for better or worse, it is the commentator who has the last word.
Final exam questions:
1. To what extent did Nabokov agree or disagree with this approach to literary criticism?
2. Did Nabokov personally identify more with Shade or with Kinbote?
Oof, I hate these questions. Nabokov would have hated 1 as a question because Pale Fire is a sort of extended essay about this very thing, written in the voice of a narcissistic obsessive weirdo and providing him with a sort of chorus response as a poem.
2 feels simplistic to me as well, when asked about one of the great masters of characterization. If you ask who did he sympathize with more, then I’d say possibly ‘neither’.
The "states" (A, B, C) correspond to goto targets. The "colors" (0, 1, 2, 3) are runtime data. At each state, the current color is read, and an instruction is executed (print some color, move left or right, goto some state) based on which color is there. Transliterated into C it looks like this:
#include "machine.h"
int main(void)
{
A:
switch (SCAN) {
case 0:
WRITE(1); RIGHT; goto B;
case 1:
WRITE(3); LEFT; goto B;
case 2:
WRITE(1); RIGHT; goto H;
case 3:
WRITE(2); RIGHT; goto A;
}
B:
switch (SCAN) {
case 0:
WRITE(2); LEFT; goto C;
case 1:
WRITE(3); RIGHT; goto B;
case 2:
WRITE(1); LEFT; goto C;
case 3:
WRITE(2); RIGHT; goto A;
}
C:
switch (SCAN) {
case 0:
WRITE(3); RIGHT; goto B;
case 1:
WRITE(1); LEFT; goto B;
case 2:
WRITE(3); LEFT; goto C;
case 3:
WRITE(2); RIGHT; goto C;
}
H:
HALT;
}
Question: are there any opportunities to rewrite this logic in a more "structured" style, or to make any other optimizations?
I love these puzzles. GNU C supports a label as value for computed goto. This is useful for direct threaded dispatch. You trade off a branch instruction for an address lookup, but it makes the code more structured.
Sometimes, the fact that one implementation includes it can make it actually more difficult to standardize, if there are some implementation details that are disagreeable (see GNU's nested functions)
It is sometimes thought that extremely long-running Turing machine programs must be deeply complicated, or "spaghetti code". This new reigning champion program is a counterexample. All things considered, it is relatively simple.
There are three states: A, B, C. (States are just like goto targets in C.) State B passes control to A and C, but states A and C don't "know about" each other; they only pass control back to B. This is a sort of modular construction, whereas in true spaghetti code each state would be able to pass to all the others.
This program has some other interesting features. It never prints a blank (that is, whenever it scans a 0, it prints 1, 2, or 3). Additionally, every instruction changes either the state or the color -- there are no "lazy instructions" like B1 -> 1LB that just move position without changing anything else.
There is some debate in the bbchallenge project regarding the current long-running champions: do their properties reflect those of the actual longest-running machine of that size, or are their properties just the easiest to automatically search for and prove things about, as a kind of streetlamp effect? There's no way to know, until the entire search space has been ruled out, either definitely or heuristically. (Every size past BB(5, 2) contains chaotic, pseudorandom machines that are expected to run forever, but can't be proven to do so without big advances in number theory.)
Though I suspect that no long-running machine can be utterly chaotic, at least when you look at the patterns it produces on the tape. To run for a long time, a machine must simulate some sort of higher-level rule: if it were dumping symbols on the tape at random, then it would very soon reach a halting configuration, a cyclical configuration, or some other simplified pattern. Still, one can have long-running machines that do simulate something chaotic on a higher level, spending an inordinate amount of time between each high-level step until it halts.
I agree completely, all of these kinds of conjectures are shaped by what is detectable. If there are any "dark matter" programs out there, they by definition will be difficult to find. That said, I find it entirely plausible that the champions will win by exploiting complex and exotic mathematical facts, while the implementations of the math do not themselves need to be complex or exotic at the code level.
Yeah, thankfully we're still in the range where halting machines are at least estimable in terms of inductive notations like the up-arrow. But as the machines gain more breathing room for working with variable-length data, we can start getting monsters like the TREE sequence.
Handwaving here, but I think longest running machines can't follow a specific structure in general.
Rough sketch of an argument:
Let's construct a number from all intermediate states of the machine concatenated. The number of digits of this number should correspond to the runtime (sketchy). We only care about the halting machines, so it's finite. We know that it must be unique because if a smaller machine computes the same number, we could get a bigger number by simply running the smaller program and doing other nonsense. That means the biggest programs are komolgorov optimal, and the numbers themselves should be k-trivial and thus nearly but not quite computable. Since they're not computable, the programs themselves can't follow a structure to generate them (since that would be computable in turn for larger values).
Of course, there can't be some grand global structure to describe all the champions in one go. But there could be properties that many have in common, e.g., predominantly consisting some number of nested recursions, characterized by some transfinite ordinal. For instance, this particular machine recurses over the first several hyperoperations.
At a high level, wouldn’t you expect Champions to be chaotic in the limit? As in, the halting problem tells us that any increasing sequence of Champions is not computable.
Yes, for a busy beaver properly defined in information theoretic terms, like BBλ2 [1], one can prove that its champions must be incompressible up to some constant. Mikhail Andreev's article "Busy Beavers and Kolmogorov complexity" [2] explores these connections.
The OEIS is a curated selection of integer sequences. It only includes those sequences deemed interesting (usually mathematically, but also recreationally, and occasionally for some other reason). It's easy to generate a new sequence from an old one, say B(n) = A(n) + 11 for some sequence A. But if you submit that it will be rejected because it isn't interesting. (Trying to come up with an OEIS-worthy sequence is difficult and edifying, and a great rainy-day activity.)
But even if the OEIS had no standards and included every imaginable sequence, it still wouldn't include more than a vanishingly small fraction of the total set of all integer sequences. This is because almost all integer sequences are infinitely long and cannot be specified. There just aren't enough words!
At one point a project in a research group I'm part of did automatic parsing of the entire OEIS to find relations between different existing sequences. Using a very simple approach, they found ~300 000 000 relations (e.g. meaning one sequence can be expressed as some combination of other sequences); see section 4 of [1].
However they submitted only three (!) of those back to OEIS.
Even with 130 reviewers on the OEIS side, submitting all of those relations would have basically been a Denial-of-service attack on the review process.
Yes, one useful application of Cantor's theorem is to show that anything claiming to enumerate all integer sequences must fail to do so. That's assuming that the sequences can be infinite; if it were the Online Encyclopedia of Finite Integer Sequences, then it could succeed at enumerating all of them.
(As for the diagonal argument, make sure that the ith value of the counter-sequence DIFFERS from the ith value of the ith sequence. A sequence whose ith value matches the ith value of the ith sequence doesn't produce a contradiction, and could in fact be part of the encyclopedia.)
You don't even have to repeat the diagonal argument. There's a one-to-one correspondence between subsets of the natural numbers and sequences of elements from {0,1}. The i-th element is 1 if i is in the set, otherwise it's zero.
> The basic phenomenon here is that synchronizing different processes, establishing shared state, or imposing an order on events requires communication among the processes. In essence, any notion of time in concurrency control must be intimately tied to communication. It is intriguing that a similar connection between time and communication also arises in the Theory of Relativity, where the speed of light (the fastest signal that can be used to synchronize events) is a fundamental constant relating time and space. The complexities we encounter in dealing with time and state in our computational models may in fact mirror a fundamental complexity of the physical universe.
https://mitp-content-server.mit.edu/books/content/sectbyfn/b...