"nondeterminism as abstraction" is, imo, the best example of an "FM export".
Usually you think of nondeterminism as adding complexity to a system -- concurrency, randomness, etc.
So it's kind of surprising to notice that translating a deterministic system into a non-deterministic system is often the first step people take when proving things about complicated algorithms.
Planning, optimization and reinforcement learning are the canonical examples where the reason for this step is easiest to see. These are usually very complex algorithms. You could prove things about an actual implementation, line of code by line of code, but that would be a toooon of work.
If instead you can find over-approximation `inv : State x Action -> List[State]`, and if you know that this invariant is strong enough to imply whatever other properties you want, then you just need to make sure that `inv` over-approximates the actual behavior of the underlying system (either by interrogation or by construction).
It's a very simple observation, motivated by the pragmatics of engineering proofs about complicated systems, which can have a direct impact on how you think about designing those same systems. Now that huge inscrutable models are all the rage, it's a fun little FM trick I used almost every day even though I rarely work on systems that I'd bother to formally model or verify.
Reminds me a lot of thermodynamics. Microstates and transition probabilities are a more “fundamental” description, but when you hit the metal, temperature and pressure are more useful in practice to human engineers
Interesting point. It's almost a form of "design by verifiability" – prioritizing architectures that lend themselves to easier reasoning, even if other architectures might offer marginal performance gains.
The cool thing is that you can sometimes "retcon" an existing system using this approach
So in that case you're not even making any performance concessions; the actual running code isn't changing. You're just imposing an abstraction on top of it for the purpose of analysis. The actual running code doesn't have to change for that analysis to bear fruit (e.g., quashing a bug or just increasing understanding/confidence). That's what it sounds like Hillel did with the A,B,C example in the blog post.
Another sort of funny point is that this basic trick is most often used when performance isn't acceptable, as a way of providing a modicum of stability/debugging to an ostensibly uber-optimized system which, once deployed, turns out to be kinda fragile.
I expected this to be about different meanings of the word "nondeterminism" rather than different causes of a single meaning. Back in college, I remember someone once pointing out to me that the word was used for fairly different concepts in different classes; in our theory classes, "nondeterministic" was used for stuff like finite automata and Turing machine models of computation (like the "N" in "NP" compared to just "P"), whereas in some other classes it might get used the way it's used in this article (e.g. for an AI algorithm that wouldn't always produce the same results). Maybe someone more educated than me might be able to connect why the same word is used for both of those, but as far as I'm able to tell, they seem entirely unrelated.
A deterministic program follows a single path of execution, always producing the same result.
A nondeterministic_1 program follows a single path of execution, but at certain points, it randomly chooses how to proceed, therefore producing different results for different runs.
A nondeterministic_2 program follows multiple paths of execution, at certain points _splitting_ its execution to follow two (or more) paths instead of one, producing a set of results at the end.
A nondeterministic_1 program follows a randomly sampled path from a nondeterministic_2 program, and produces a randomly sampled result from a nondeterministic_2 program.
> A deterministic program follows a single path of execution, always producing the same result.
Looking at a whole program as D/ND isn't too useful for me since it's too big to analyse and constantly being patched by multiple contributors.
Does this definition of deterministic work for smaller things, like a method?
You can transform a function `f: (Rng, args...) -> A` into a function `f: (args...) -> Set<A>` with very little machinery. Some programming languages allow writing functions that are _generic_ over whether they're random or nondeterministic, such as in this Haskell package: https://hackage.haskell.org/package/nondeterminism-1.5/docs/...
They are related and the reason is the last point of the OP article: Abstraction. Things can be "physically" deterministic, but can be abstracted as non-deterministic. This seems strange at first but it actually makes a lot of sense, as long as you're not modelling physics itself, it's irrelevant that there is a theory in which your non-model is deterministic. Machine learning algorithms like ChatGPT can be good examples, given the exact same input+random seed, of course, they'll return the same exact output, but the situation is so computationally complex that modeling that system as deterministic is less useful than modelling it as if it's non-deterministic. This is the same way your computer RAM is not "infinite"--it's like trillions of bits-- but in CS we model it as if it's infinite because the practical difference is not the focus of the discussion. If the discussion really was "can we fit a pigeon in every bit of my computer" or "can we manufacture every bit of this RAM in finite amount of time" then yes, it would be relevant to argue that RAM isn't actually infinite. But given that we're interested in models of computation that get exponentially larger and larger as memory grows, even 10 bits can be an intractibly large space (cf. Busy Beaver numbers) so you might as well solve the problem as if it's infinite.
I couldn't tell you the historical connections, but they "feel" related to me. This comment got me speculating about how to explain this connection; disclaimer I'm writing completely this off the cuff.
First off, NFAs and Nondet Turing Machines (NTM) would be "deterministic" with the OP definition I gave, since they always give the same decision for the same input. Their nondeterminism is a capability they have, an aspect of their process that helps reach a decision. If we need to distinguish "deterministic result" and "deterministic process", I've seen the term Observationally Deterministic used to exclusively mean the former.
A critical theorem in automata theory is that NFAs and NTMs are no more powerful than DFAs or TMs: the former cannot recognize any languages the latter cannot. This is why nondeterministic algorithms (ie, algorithms with a deterministic capability) cannot "solve more problems" than deterministic algorithms, just (probably) solve them faster (NP vs P).
(Interestingly, nondeterministic pushdown automata ARE more powerful than regular PDAs. Only NPDAs can recognize all context-free languages.)
So what does it mean for "nondeterminism" to be a capability of the process? I see the "automata/computation" and the "formal methods" as being the same idea, except with opposite outcomes. When deciding to see if a problem is in NP, we allow the algorithm to make nondeterministic choices, and accept the construction if any choice leads to valid outcome. When deciding to see if a system is satisfies required properties, we allow the model to make nondeterministic choices, and reject if any lead to an invalid outcome.
(Even more handwavy part: I've heard the terms "angelic" and "demonic" choice to distinguish the two. I think from the perspective of complexity, FM's demonic nondeterminism kinda looks like angelic choice in the co-complexity class. From the perspective of FM, complexity's angelic nondeterminism kinda looks like checking a reachability property, as opposed to a safety or liveness property.)
In either case, both are essentially abstractions over concrete implementation details. Just as I cannot physically implement "nondeterministically enter state A, B, or C", I cannot implement "nondeterministically match the regex `A|B|C`". I have to instead find a deterministic implementation, like "try to match A, and if that fails, backtrack and match B, etc."
Determinism is relative. "Non-deterministic" means that an observer, to the best of their ability, cannot predict the result even with full knowledge of all inputs.
This can be used as an abstraction for a theoretically deterministic system that is too complex to handle.
But even if you take "ability" and "knowledge" (of all inputs and the inner workings of the system) serious, there is always the possibility that there are factors you simply don't know. Maybe your model is incomplete. Maybe there are as-yet-unknown physics that make even radioactive decay predictable. So really, it's always an abstraction.
I wonder if it was an intentional joke that immediately under the heading "3. User Input", there is a text box to enter your email to subscribe to the newsletter.
There are two main kinds of nondeterminism.
1. One single future is chosen at every turn and we go down that rabbit hole and never turn back. The author's determinisms all land into here.
2. Explicitly modeled nondeterminism, whereby we execute all the future possibilities (e.g. nondeterministic finite automaton NFA, Mac Carthy's "amb" operator.)
I can't give you a star sticker if you don't mention these, sorry.
Maybe I'm missing something here, but the last type matches 2 pretty well. For example,
> None of that mattered at the scope we were modeling, so we abstracted it all away: "on receiving message, nondeterministically enter state A, B, or C."
That sounds like the author is describing an NFA.
> whereby we execute all the future possibilities... e.g. "amb" operator
Isn't "execute all possibilities" closer to the dual of amb than it is to amb? At least in terms of how the denotation of amb is operationalized.
But it is a good point that sometimes you want to give an actual operational meaning to a literal non-determinism operator.
And then then the different kinds of the latter: angelic (locally or globally) and demonic.
Lately I've been working on a testing system for a DAG identity system I'm working on. The system tries thousands of permutations of DAG setups, all driven from a random seed. In other words, it's entirely repeatable and deterministic each time. If something breaks, I can pinpoint the exact run and re-run it with the exact same parameters.
It took a long time to get there. One of the main things I had root out, time after time, was the use of HashMap/HashSet (this is in rust) which I converted to BTreeMap/BTreeSet because the former are not deterministic when iterating over them, causing all kinds of random permutations for a given seed. I knew this going in, but kind of surprised myself how often I almost absentmindedly reached for a non-deterministic data type when determinism was important.
The non-determinism of Rust's HashMap/HashSet is because the default hasher seeds itself using the operating system's RNG facilities. You can use the with_hasher() function to replace the default hasher with a PRNG that is deterministically seeded.
Your first example is not non-deterministic, it's probabilistic. Drawing a sample from a truly random distribution doesn't make the program non-deterministic.
Non-determinism comes from transitions which have no known distribution and might cause your program to take alternate execution paths without any predefined rule. That's clearly not true in your example.
I think you're splitting hairs here. Not sure what definition or context of determinism you are using, but in most scientific fields not only is probability the de-facto example of non-determinism, but in fact the words are often used interchangeably.
By definition, if your outcome is a random draw from a probability distribution (known or unknown), you cannot guarantee the outcome in a deterministic manner; you can only guarantee that in the limit, a large number of random draws will follow that distribution (known or unknown). But that's not what one would typically call determinism.
Ideally everyone who visits the page would get the entries in a different order.
I'm sure this is a really great article, but I was really excited that this was going to be scientific, philosophical take on different conceptions of possible mechanics that might underly our observations of quantum behaviour and the implications on ideas of free will. I'll have to ask Claude to write that article for me so I can read it.
I’m struggling to wrap my head around abstraction as non-determinism here. Yes, an implementation could change, but then you’ve loaded other code?
It is deterministic, but if it's absurdly hard to prove, you just say it isn't deterministic.
Imagine a program that uses JSON and depends on the order of keys in an object. If you input the same object, but with different key order, you'll get different results.
The program is deterministic, but it looks non-deterministic to a naïve observer.
That's just a very simple example, in a more complex system there could be all kinds of uncommon behaviours that are less simple to trace. So when modeling the system, they just box it as "there be dragons" and move on.
The example is really bad for this because it doesn't say the result is non-deterministic, just complex and treated as a black box which only makes the result hard to reason about when abstracted rather than truly non-deterministic.
A common example from my domain is making floating point math deterministic. This is fairly straightforward for a single operating system/piece of hardware combination but as soon as you need cross-platform determinism is full of gotchas. In particular because the abstraction in this case is often the programming language, the specific compiler used (sometimes even version) and standard library. This also gets as subtle as not being able to use certain instructions like fused multiply-add and SIMD intrinsics where the implementation can differ between pieces of hardware.
The article wasn't bad, but the examples felt a bit thin; almost like the author was reaching a bit to hit that magic number of 5.
And you're definitely not wrong on the abstract subsection. I mean, essentially all he says is that "there's a mechanism in our system which is so complicated/convoluted that we decided not to model it with TLA, so instead we chose to simply call it non-deterministic, and therefore it is now abstract non-determinism." Hmm. If we're truly being abstract, that's not really all that different from the PRNG and user input examples, except, you know, it's actually still completely deterministic code.
Also, I have to say- 5 different types of non-determinism, and not one mention of quantum systems?
I took issue with #4 too. If your code consumes API endpoints that are non-deterministic, that strikes me as something you should take up with your vendor. An error condition on a network call is not non-determinism. It's just reality from time to time.
The author is writing on the context of formal verification. From that point of view, modelling an error condition on a network call as non-deterministic and just lumping potential bugs in the remote API into that as well since you don't control it (i.e. it is not part of the system you are trying to verify) just makes sense so you can go forward with verifying that your code will do the right thing no matter what happens.
Understood. It was hard to tell if he was only writing it from the standpoint of FM or if he was speaking more generally.
randomness is an illusion
randomness is epistemology. determinism is ontology
"nondeterminism as abstraction" is, imo, the best example of an "FM export".
Usually you think of nondeterminism as adding complexity to a system -- concurrency, randomness, etc.
So it's kind of surprising to notice that translating a deterministic system into a non-deterministic system is often the first step people take when proving things about complicated algorithms.
Planning, optimization and reinforcement learning are the canonical examples where the reason for this step is easiest to see. These are usually very complex algorithms. You could prove things about an actual implementation, line of code by line of code, but that would be a toooon of work.
If instead you can find over-approximation `inv : State x Action -> List[State]`, and if you know that this invariant is strong enough to imply whatever other properties you want, then you just need to make sure that `inv` over-approximates the actual behavior of the underlying system (either by interrogation or by construction).
It's a very simple observation, motivated by the pragmatics of engineering proofs about complicated systems, which can have a direct impact on how you think about designing those same systems. Now that huge inscrutable models are all the rage, it's a fun little FM trick I used almost every day even though I rarely work on systems that I'd bother to formally model or verify.
Reminds me a lot of thermodynamics. Microstates and transition probabilities are a more “fundamental” description, but when you hit the metal, temperature and pressure are more useful in practice to human engineers
Interesting point. It's almost a form of "design by verifiability" – prioritizing architectures that lend themselves to easier reasoning, even if other architectures might offer marginal performance gains.
The cool thing is that you can sometimes "retcon" an existing system using this approach
So in that case you're not even making any performance concessions; the actual running code isn't changing. You're just imposing an abstraction on top of it for the purpose of analysis. The actual running code doesn't have to change for that analysis to bear fruit (e.g., quashing a bug or just increasing understanding/confidence). That's what it sounds like Hillel did with the A,B,C example in the blog post.
Another sort of funny point is that this basic trick is most often used when performance isn't acceptable, as a way of providing a modicum of stability/debugging to an ostensibly uber-optimized system which, once deployed, turns out to be kinda fragile.
I expected this to be about different meanings of the word "nondeterminism" rather than different causes of a single meaning. Back in college, I remember someone once pointing out to me that the word was used for fairly different concepts in different classes; in our theory classes, "nondeterministic" was used for stuff like finite automata and Turing machine models of computation (like the "N" in "NP" compared to just "P"), whereas in some other classes it might get used the way it's used in this article (e.g. for an AI algorithm that wouldn't always produce the same results). Maybe someone more educated than me might be able to connect why the same word is used for both of those, but as far as I'm able to tell, they seem entirely unrelated.
A deterministic program follows a single path of execution, always producing the same result.
A nondeterministic_1 program follows a single path of execution, but at certain points, it randomly chooses how to proceed, therefore producing different results for different runs.
A nondeterministic_2 program follows multiple paths of execution, at certain points _splitting_ its execution to follow two (or more) paths instead of one, producing a set of results at the end.
A nondeterministic_1 program follows a randomly sampled path from a nondeterministic_2 program, and produces a randomly sampled result from a nondeterministic_2 program.
> A deterministic program follows a single path of execution, always producing the same result.
Looking at a whole program as D/ND isn't too useful for me since it's too big to analyse and constantly being patched by multiple contributors.
Does this definition of deterministic work for smaller things, like a method?
You can transform a function `f: (Rng, args...) -> A` into a function `f: (args...) -> Set<A>` with very little machinery. Some programming languages allow writing functions that are _generic_ over whether they're random or nondeterministic, such as in this Haskell package: https://hackage.haskell.org/package/nondeterminism-1.5/docs/...
They are related and the reason is the last point of the OP article: Abstraction. Things can be "physically" deterministic, but can be abstracted as non-deterministic. This seems strange at first but it actually makes a lot of sense, as long as you're not modelling physics itself, it's irrelevant that there is a theory in which your non-model is deterministic. Machine learning algorithms like ChatGPT can be good examples, given the exact same input+random seed, of course, they'll return the same exact output, but the situation is so computationally complex that modeling that system as deterministic is less useful than modelling it as if it's non-deterministic. This is the same way your computer RAM is not "infinite"--it's like trillions of bits-- but in CS we model it as if it's infinite because the practical difference is not the focus of the discussion. If the discussion really was "can we fit a pigeon in every bit of my computer" or "can we manufacture every bit of this RAM in finite amount of time" then yes, it would be relevant to argue that RAM isn't actually infinite. But given that we're interested in models of computation that get exponentially larger and larger as memory grows, even 10 bits can be an intractibly large space (cf. Busy Beaver numbers) so you might as well solve the problem as if it's infinite.
I couldn't tell you the historical connections, but they "feel" related to me. This comment got me speculating about how to explain this connection; disclaimer I'm writing completely this off the cuff.
First off, NFAs and Nondet Turing Machines (NTM) would be "deterministic" with the OP definition I gave, since they always give the same decision for the same input. Their nondeterminism is a capability they have, an aspect of their process that helps reach a decision. If we need to distinguish "deterministic result" and "deterministic process", I've seen the term Observationally Deterministic used to exclusively mean the former.
A critical theorem in automata theory is that NFAs and NTMs are no more powerful than DFAs or TMs: the former cannot recognize any languages the latter cannot. This is why nondeterministic algorithms (ie, algorithms with a deterministic capability) cannot "solve more problems" than deterministic algorithms, just (probably) solve them faster (NP vs P).
(Interestingly, nondeterministic pushdown automata ARE more powerful than regular PDAs. Only NPDAs can recognize all context-free languages.)
So what does it mean for "nondeterminism" to be a capability of the process? I see the "automata/computation" and the "formal methods" as being the same idea, except with opposite outcomes. When deciding to see if a problem is in NP, we allow the algorithm to make nondeterministic choices, and accept the construction if any choice leads to valid outcome. When deciding to see if a system is satisfies required properties, we allow the model to make nondeterministic choices, and reject if any lead to an invalid outcome.
(Even more handwavy part: I've heard the terms "angelic" and "demonic" choice to distinguish the two. I think from the perspective of complexity, FM's demonic nondeterminism kinda looks like angelic choice in the co-complexity class. From the perspective of FM, complexity's angelic nondeterminism kinda looks like checking a reachability property, as opposed to a safety or liveness property.)
In either case, both are essentially abstractions over concrete implementation details. Just as I cannot physically implement "nondeterministically enter state A, B, or C", I cannot implement "nondeterministically match the regex `A|B|C`". I have to instead find a deterministic implementation, like "try to match A, and if that fails, backtrack and match B, etc."
https://cstheory.stackexchange.com/questions/632/what-is-the...
Determinism is relative. "Non-deterministic" means that an observer, to the best of their ability, cannot predict the result even with full knowledge of all inputs.
This can be used as an abstraction for a theoretically deterministic system that is too complex to handle.
But even if you take "ability" and "knowledge" (of all inputs and the inner workings of the system) serious, there is always the possibility that there are factors you simply don't know. Maybe your model is incomplete. Maybe there are as-yet-unknown physics that make even radioactive decay predictable. So really, it's always an abstraction.
I wonder if it was an intentional joke that immediately under the heading "3. User Input", there is a text box to enter your email to subscribe to the newsletter.
There are two main kinds of nondeterminism.
1. One single future is chosen at every turn and we go down that rabbit hole and never turn back. The author's determinisms all land into here.
2. Explicitly modeled nondeterminism, whereby we execute all the future possibilities (e.g. nondeterministic finite automaton NFA, Mac Carthy's "amb" operator.)
I can't give you a star sticker if you don't mention these, sorry.
Maybe I'm missing something here, but the last type matches 2 pretty well. For example,
> None of that mattered at the scope we were modeling, so we abstracted it all away: "on receiving message, nondeterministically enter state A, B, or C."
That sounds like the author is describing an NFA.
> whereby we execute all the future possibilities... e.g. "amb" operator
Isn't "execute all possibilities" closer to the dual of amb than it is to amb? At least in terms of how the denotation of amb is operationalized.
But it is a good point that sometimes you want to give an actual operational meaning to a literal non-determinism operator.
And then then the different kinds of the latter: angelic (locally or globally) and demonic.
Lately I've been working on a testing system for a DAG identity system I'm working on. The system tries thousands of permutations of DAG setups, all driven from a random seed. In other words, it's entirely repeatable and deterministic each time. If something breaks, I can pinpoint the exact run and re-run it with the exact same parameters.
It took a long time to get there. One of the main things I had root out, time after time, was the use of HashMap/HashSet (this is in rust) which I converted to BTreeMap/BTreeSet because the former are not deterministic when iterating over them, causing all kinds of random permutations for a given seed. I knew this going in, but kind of surprised myself how often I almost absentmindedly reached for a non-deterministic data type when determinism was important.
The non-determinism of Rust's HashMap/HashSet is because the default hasher seeds itself using the operating system's RNG facilities. You can use the with_hasher() function to replace the default hasher with a PRNG that is deterministically seeded.
Your first example is not non-deterministic, it's probabilistic. Drawing a sample from a truly random distribution doesn't make the program non-deterministic.
Non-determinism comes from transitions which have no known distribution and might cause your program to take alternate execution paths without any predefined rule. That's clearly not true in your example.
I think you're splitting hairs here. Not sure what definition or context of determinism you are using, but in most scientific fields not only is probability the de-facto example of non-determinism, but in fact the words are often used interchangeably.
By definition, if your outcome is a random draw from a probability distribution (known or unknown), you cannot guarantee the outcome in a deterministic manner; you can only guarantee that in the limit, a large number of random draws will follow that distribution (known or unknown). But that's not what one would typically call determinism.
In formal methods, a subfield of computer science, we'd typically use the definition of non-determinism that is widely used within our own field. For example, see: https://cstheory.stackexchange.com/questions/632/what-is-the...
Ideally everyone who visits the page would get the entries in a different order.
I'm sure this is a really great article, but I was really excited that this was going to be scientific, philosophical take on different conceptions of possible mechanics that might underly our observations of quantum behaviour and the implications on ideas of free will. I'll have to ask Claude to write that article for me so I can read it.
I’m struggling to wrap my head around abstraction as non-determinism here. Yes, an implementation could change, but then you’ve loaded other code?
It is deterministic, but if it's absurdly hard to prove, you just say it isn't deterministic.
Imagine a program that uses JSON and depends on the order of keys in an object. If you input the same object, but with different key order, you'll get different results.
The program is deterministic, but it looks non-deterministic to a naïve observer.
That's just a very simple example, in a more complex system there could be all kinds of uncommon behaviours that are less simple to trace. So when modeling the system, they just box it as "there be dragons" and move on.
The example is really bad for this because it doesn't say the result is non-deterministic, just complex and treated as a black box which only makes the result hard to reason about when abstracted rather than truly non-deterministic.
A common example from my domain is making floating point math deterministic. This is fairly straightforward for a single operating system/piece of hardware combination but as soon as you need cross-platform determinism is full of gotchas. In particular because the abstraction in this case is often the programming language, the specific compiler used (sometimes even version) and standard library. This also gets as subtle as not being able to use certain instructions like fused multiply-add and SIMD intrinsics where the implementation can differ between pieces of hardware.
The article wasn't bad, but the examples felt a bit thin; almost like the author was reaching a bit to hit that magic number of 5.
And you're definitely not wrong on the abstract subsection. I mean, essentially all he says is that "there's a mechanism in our system which is so complicated/convoluted that we decided not to model it with TLA, so instead we chose to simply call it non-deterministic, and therefore it is now abstract non-determinism." Hmm. If we're truly being abstract, that's not really all that different from the PRNG and user input examples, except, you know, it's actually still completely deterministic code.
Also, I have to say- 5 different types of non-determinism, and not one mention of quantum systems?
I took issue with #4 too. If your code consumes API endpoints that are non-deterministic, that strikes me as something you should take up with your vendor. An error condition on a network call is not non-determinism. It's just reality from time to time.
The author is writing on the context of formal verification. From that point of view, modelling an error condition on a network call as non-deterministic and just lumping potential bugs in the remote API into that as well since you don't control it (i.e. it is not part of the system you are trying to verify) just makes sense so you can go forward with verifying that your code will do the right thing no matter what happens.
Understood. It was hard to tell if he was only writing it from the standpoint of FM or if he was speaking more generally.
randomness is an illusion
randomness is epistemology. determinism is ontology