The comment didn't say that ZKP had nothing to do with blockchain. The comment said that blockchains are not needed/involved for a zero knowledge proof, just like war is not needed for radar.
5,541 karma · joined November 11, 2012
When I taught my daughter chess at the age of 5, I did not teach her by laying out the rules and in general when I teach people anything, I don't start by emphasizing rules. Rules are often the least interesting part of any subject and I find rules are much easier to learn once a sufficient amount of motivation has been given first, and then we get to a point where we use rules to crystalize our intuition and express rigorously what we've come to learn. The rules are the end result of learning, not the starting point.
With chess, I taught my daughter by simply playing a simple game where I had a queen, and she had one king and two pawns, and her goal was to get one pawn across the board and my goal was to stop her.
The king and pawns are arranged so that with perfect play she is guaranteed a win, and eventually she learned the pattern that allows her to always win. I then switched it up so she gets the queen and I get the king/pawns but I arrange the king/pawns so that I will always lose if she plays perfectly.
After this, I added more pawns for white and a bishop for black. The motivation for adding these pieces is that to play perfectly and always win as white, you need to learn how pawns define the physical structure of the board, making walls and allowing for control over certain parts of the board, but this also comes at the cost of introducing clutter and making it hard for the king to maneuver.
After these principles are learned, then I introduce the knight, because the knight can jump over walls and isn't as burdened by clutter. I don't just put a knight in the game out of nowhere and make her memorize how it moves... by the time the knight is introduced, it feels natural to want a piece that has better maneuverability over the extra pawns.
And so on so forth... each piece is introduced with some kind of motivation for why it exists. It's not just there for the sake of existing because of some rule that you just need to memorize. It exists because it adds some kind of flavor and richness to the game and you end up absorbing the rules rather than just memorizing them.
Now I'm dwelling a bit on chess here... but the principle applies to programming as well. I don't think if you ever just listed the rules you did as a means of teaching someone about monads anyone would ever come to appreciate why these rules matter or why they should waste any time learning them and in fact I am fairly confident that this kind approach to teaching people functional programming is why it's taken so long for mainstream languages to appreciate these features and adopt them.
>I think the more correct statement is that there are different models of ZFC in which BB(748) are different numbers.
You asked how this was possible and that's the specific question that I am addressing. As I mentioned elsewhere, to fully appreciate this answer requires parsing some very subtle and nuanced details that simply can not be glossed over or dismissed, if you genuinely want to know how it's possible that ZFC can be consistent even though different models give different values of BB(748).
If you want to argue something else, about what model is correct or what model is incorrect, that's a perfectly fine argument to have but it's more in the realm of philosophy than it is in the realm of formal mathematics.
>For any X⊆N, if 0 ∈ X, and for every n ∈ X, S(n) ∈ X, then X=N.
You're right that this is a perfectly valid axiom in SOL, but it's not true that it rules out non-standard "shit". What this axiom does is it forces your theory to have a single model, the categorical model. But this axiom does not in anyway pick out the standard model as the categorical model, it doesn't force the categorical model to be the standard model. It's possible that N = {0, 1, 2, ..., Q - 1, Q, Q + 1, ...} in which case the categorical model ends up being nonstandard. This axiom has no way to force N to be intended standard model.
What second order logic does let you do is deal with only one single model, called the categorical model. So instead of having a theory that has a whole bunch of different models including the actual natural numbers along with undesirable models that contain infinitely large values... you can force your theory to have one single model, no more "It's true in this model, but it's false in that other nonstandard model that's getting in the way." So yes in a particular theory of second order logic BB(748) has one single value because there is only one single model.
So problem solved right? Not even close... because that one single categorical model being used to represent the natural numbers may not be the actual natural numbers, the intended natural numbers where every number is actually finite. Having one single categorical model does not imply working with the actual model you intended to work with. Depending on your choice of second order theory you may be operating within a theory where the single categorical model is indeed unbeknownst to you {0, 1, 2, 3, ..., Q - 1, Q, Q + 1, ...} and hence BB(748) is equal to Q and you'll have no way of knowing this before hand since you lack an effective proof system.
In first order logic it's impossible to uniquely define any property that would also uniquely define the natural numbers.
Yes, between you and me we know that BB(n) needs to be a natural number, but we have no way to formally and uniquely define what natural numbers are. The best we can do is come up with a formal definition of natural numbers that includes the actual natural numbers but will also include other number systems that contain mathematical objects that are infinitely big and hence are not actual natural numbers. Hence our formal definition of natural numbers will not uniquely define a single set of numbers {0, 1, 2, 3, ...}, there will be other sets of numbers such as {0, 1, 2, 3, ..., Q - 1, Q, Q + 1, ...} for some infinitely large object Q that satisfy the formal definition of natural numbers. Between you and me, we both know Q isn't an actual natural number, but what we don't know is what formal rule we need to add to our formal definition of natural numbers in order to get rid of Q. In fact, it's worse than that; we know that even if we add a rule that gets rid of Q, there will always be some other number system {0, 1, 2, 3, ..., Q* - 1, Q*, Q* + 1, ...} to take its place. No formal definition can ever uniquely define the natural numbers (unless that formal system is inconsistent).
It's also true that a model where BB(748) = Q is not the actual BB, it's some other function. The problem is that this model satisfies all of the rules of ZFC and all of the properties that ZFC says natural numbers must satisfy and hence it satisfies the formal definition of BB even though it isn't the actual BB. Remember it is impossible for the formal definition of BB to include the property that BB(n) = an actual natural number, because there is no formal definition that uniquely singles out what the actual natural numbers are. Since there exists one such model that satisfies all of the rules about BB but isn't actually the real BB then we can't use ZFC to formally prove what the value of BB(748) actually is.
What we can do is add new rules to ZFC get rid of this model, but that will only push the issue down to BB(749) or BB(750) or maybe if pick a really powerful rule we push the issue down to BB(800)... but the point stands that adding new rules only pushes the problem further down the road, it never eliminates the problem entirely.
From within those models Q satisfies all the properties of being a natural number but it's not actually a natural number. Q is some successor of 0, you can add 1 to Q to get another distinct mathematical object, there is some predecessor to Q called P so that P + 1 = Q, etc etc... Q satisfies all the properties within ZFC of being a natural number but it isn't an actual natural number.
Furthermore if ZFC is consistent then it's impossible for any model of ZFC to have BB(4) = 100. ZFC is sufficiently powerful to prove that BB(4) != 100, it is not sufficiently powerful enough to prove that BB(748) = F for some actual natural number F.
The issue is that there is no way within ZFC to determine which value is the smallest.
Q isn't a natural number because natural numbers must be finite, but Q is infinitely large.
>If you had unlimited time and paper, you could sit down and run the machine by hand, counting each step, until it reaches the halting state. You will have counted Q steps.
What if the machine never stops? How many steps will you run before you decide that the machine never halts?
>There’s no such thing as a machine that stops after a number of steps defined by an infinitely large construct.
There's no such thing as an actual machine that stops after an infinite number of steps, but that's not the issue. The issue is that ZFC has different models with conflicting definitions of what infinite is. In one model there is an object called Q that satisfies all of the properties in ZFC of being a natural number, but is infinitely large. In this model the Turing Machine halts after Q steps. But there is another model, called the standard model, and in this model there is no Q, all elements of this model are actually finite, and in this model the Turing machine never halts.
ZFC doesn't know which of these two models is the "real" model of natural numbers. From within ZFC both of these models satisfy all properties of natural numbers. It's only from outside of ZFC that one of these models is wrong, namely the model that contains Q as an element.
You can add more axioms to ZFC to get rid of the model that has Q as an element, but if the resulting theory containing your new axiom is consistent, then it necessarily follows that there is some other model that will contain some element Q* which is also infinitely large but from within the theory satisfies all of the new/stronger properties of being a natural number.
So in one model a Turing Machine called R never stops. In another model R stops after Q steps. But here's the issue... Q isn't an actual natural number, what it is is some mathematical object that satisfies all of the properties of a natural number in ZFC, but is not an actual natural number. What it actually is is some infinitely large object that satisfies all of the Peano axioms of what a natural number is as well as satisfies the following set of rules:
Q > 0
Q > 1
Q > 2
Q > 3
...
So within this model, the Turing machine R halts after Q steps, and since from within the model Q is finite then from within this model BB(748) is at least equal to Q.
If BB(748) is actually 10,000, then we can add this as an axiom to ZFC to get a new formal theory ZFC + "BB(748) = 10000".
In this new theory the previous structure that contained Q as an element will not satisfy the definition of a natural number, so we don't have to worry about Q anymore... however, there will exist some number T > 748 where BB(T) is independent of our new theory. For BB(T), there will exist some other model that has its own Q* which satisfies all of our axioms including the axiom that BB(748) = 10000, but also that
Q* > 0
Q* > 1
Q* > 2
Q* > 3
...
To use your own terminology, this is clearly and objectively false. The US Supreme Court made no such finding.
What the court concluded was that even if Oracle had a copyright on the API, Google's use of it fell under fair use so that making a ruling on the question of whether the API was protected by copyright was moot.
Now whether what Schmidhuber claims is what actually happened or not I don't know... but that is his claim and it's fundamentally different from what you are describing.
https://www.ghacks.net/2023/02/13/reminder-internet-explorer...
Access 97 depends on some Internet Explorer components and Microsoft has made it all but impossible to install Internet Explorer on the most recent Windows 10 and Window 11.
Apart from that I also tried getting Minesweeper and SkiFree to work on Windows 10 and Windows 10 just straight up refuses to run them with the message "This app can't run on your PC."
Even galaxies themselves don't expand over time.
One question would be what do you hope to gain from a potential analogy. If you want a very down to Earth, practical and somewhat physical understanding, then the simplest and best explanation is that there are systems of objects in our universe, at very very large scales, that have a group velocity that is greater than the escape velocity needed to attract it to any other system of objects, and those systems are observed to be accelerating away from each other. No analogy is needed for this, it's just a fact presented plain and simply.
There is no theory that predicts a cause for this, but the best theory of gravity, general relativity, is a very flexible and open-ended framework that allows one to plug all kinds of different and imagined scenarios into it and see the results, even if those scenarios have no actual physical interpretation. Some people did play around with imagined results like an expanding universe, a contracting universe, an infinitely large universe, a closed but unbounded universe etc etc... General relativity doesn't predict any of these universes but it does let you explore these possibilities.
When Edwin Hubble observed that galaxies are moving away from each other then this observation was made to fit into the existing theory of general relativity. In order to take the raw observation and fit it with general relativity which interprets gravity as a purely geometric phenomenon, it did so by reframing this behavior not exactly as an intrinsic motion belonging to these large scale systems but rather as if these systems are stationary but there is more and more space filling up the universe in-between these large scale objects which gives them their apparent motion.
This is a means of reconciling the geometric view of gravity, ie. space-time, with the actual observed data. The specific technical details of how this reconciliation is performed is as OP mentioned, the FLRW metric which is here but as you said is too technical for most people to appreciate:
https://en.wikipedia.org/wiki/Friedmann%E2%80%93Lema%C3%AEtr...
You might then ask, what does this solution predict happens to atoms, or our solar system? Perhaps it predicts a very small and imperceptible expansion because other forces dominate, but nevertheless it must predict something, right? This is a tempting position, but it's not quite right.
The key reason is that the FLRW metric, which explains Hubble's observation as the literal stretching of space, literally don't make sense and can't be solved for systems like planets, solar systems, or even galaxies because it can only be used if certain requirements/preconditions are fulfilled.
These requirements are present only on the absolute largest scales where the universe looks fairly even/balanced, there is no center of mass, there is no region of the universe that is more special than any other region. In our solar system the sun is a pretty special center of mass and the solar system is not evenly balanced, same thing goes for our galaxy, and hence none of the models currently studied to describe Hubble's observations work for both the extremely large scale universe as well as for other scales.
Both std::function<> and lambdas were introduced in C++11.
Furthermore absolutely no one should use std::bind, it's an absolute abomination.
The idea that you'd dismiss loop unrolling as some kind of non-issue is incredibly baffling, you need only compare the benchmark built without optimizations enabled to the one with optimizations enabled, and you'll see that the unoptimized build is about half as fast!
Speaking of Python the most recent Python release has some significant performance increases in some scenarios because of some additional loop unrolling that has been exploited.
>That's why I said "well-optimized regex." Most regexes, in practice, are not well-optimized!
So then what exactly is the point of your argument? I point out that using regex's are slow, which almost anyone would reasonably assume means that using regex libraries tend to be slow.
Is the entire point of your comment that you can take a regex and then manually implement a special purpose algorithm for it that isn't slow? Was that the point of your comment, because if so you could have made that clear initially and saved both of us a lot of time.
>I think that's perfectly reasonable here, as the given problem is finding the fastest algorithm that decides whether a string is in the language generated by ASCII characters without the vowels.
No it's not reasonable at all because if you take your definition then there is nothing to use. Being a regular language is not something you can "use" or "not use", it's a property of a set of strings, you don't get to use it. The language consisting of all strings that have at least one vowel in them is a regular language, case closed, usage has nothing to do with it. In the sense that you're using it, any algorithm whatsoever that returns true or false for a string that matches some arbitrary regular language can be considered an implementation of a regex, for some fixed regular language. But of course this is a completely trivial argument which is why there's absolutely no point in discussing it.
In the non-trivial sense that everyone else uses it... regex's are libraries that people use that let them write a string representing a pattern and then the library returns an object that can be used to test whether or not a string matches that pattern, or can be used to search for a substring that matches a pattern along with a host of functionality. The claim in my original post is that these libraries, including the one used by the blog post, tend to be slow. They are, as you point out, designed for ergonomics and convenience, not for performance.
It is not at all reasonable to argue that some arbitrary implementation you divined for a particular regular language constitutes some argument that regular expressions are a high performance means of performing string matching, but at least you have clarified your position and shown it to be absolutely trivial and meaningless, and hopefully anyone who has read your post won't be misled into thinking you meant that regex libraries that are commonly used by actual engineers like Python's, or PCRE2, or boost or the standard library are fast... but I have my doubts about that.
But if you use an actual regex the way people actually use them, using either the one provided by their standard library or one that is readily available then regex is pretty slow. Certainly, in principle a regex is neither fast or slow, it's a declarative description of a set of strings. Any claim about its performance rests on particular implementations.
For example you wrote out a benchmark that presumably is a lot faster than a naive search... but notice you didn't use the standard library <regex>, instead you manually implemented an algorithm to perform a search and then just decided that this is what a regex implementation would have done anyways (ignoring that by implementing it directly in source code, the optimizer can then fine tune it).
So now... there is a 10% chance that you genuinely didn't know that C++ has a <regex> library that you could have used, or you did in fact know that C++ has such a library and you chose not to you use it because... you also know it's very slow.
I did the benchmark myself using the standard library regex, boost regex, and PCRE2 regex, and all of them are about 5-15x slower than the simple loop:
https://gist.github.com/kranar/a3187cba00d57ba630b74b84f09b4...
https://en.wikipedia.org/wiki/Product_topology#Axiom_of_choi...
>One of many ways to express the axiom of choice is to say that it is equivalent to the statement that the Cartesian product of a collection of non-empty sets is non-empty.
With that insight it should follow that using another implementation in C should outperform even the regex, and indeed the following simple Python method that this article for whatever reason ignored vastly outperforms everything:
def contains_vowel_find(s):
for c in "aeiouAEIOU":
if s.find(c) != -1:
return True
return False
In my benchmark this approach is 10 times faster than using a regex:
https://gist.github.com/kranar/24323e81ea1c34fb56aff621f6c09...