|
|
|
|
|
by Krssst
16 days ago
|
|
Fully agree with the article (as my comment history would attest). I wonder why people worry so much more about "determinism" over conformance to a spec. (a compiler can be nondeterministic and correct which is not particularly good but definitely not worse than being incorrect) Maybe most devs don't care so much about the language specification and just expect the code to do vaguely what it looks it should do intuitively? This is not very clear to me, at least for libraries I guess a lot of people don't read API docs and just call the API hoping it does what the name says (preconditions be damned) in which case nondeterminisc observable behavior would be more problematic than nonconformance to a spec (API doc) they don't read. |
|
Try writing the grammar of natural language in EBNF if you want a fast but unsatisfying answer.
The univalence axiom and HoTT is another path.
Or just trying to find out why two programs in lambda calculus that are beta convertible and thus recursively inseparable is another path.
Finite model theory and how gödels completeness theorem doesn’t hold while it does for infinite models is another path.
Finite VC dimensionality being required for PAC learnability is a path from the other side.
There are many forms of indeterminacy, and some allow for a concept of equality that disallows apartness, like computing, but the relationship with choice/omniscience/set shattering is complicated.
Perhaps non HoTT type theory being a map between type Families may provide some useful intuition.
Under lambda calculus, which is equivalent to intuitionistic logic, the principle of explosion (ex falso quodlibet) states that any statement can be proven from a contradiction.
Intuitionists accept this rule because, under their constructive interpretation, an absurdity means a problem is demonstrably impossible to solve.
PAC learning, through set shattering makes any logic Classic, introducing PEM/AC or various forms of it.
It isn’t just the presence of indeterminacy that matters, the form it takes matters.