> Are there any drawbacks to the larger context window?
Yes. When you say something stupid, ChatGPT won't forget it as easily...
596 karma · joined June 27, 2023
Yes. When you say something stupid, ChatGPT won't forget it as easily...
You could only prove it if you add something else, e.g. a precondition saying that X = 30.
I think you meant in the opposite order, i.e.: "If X is greater than 20, then X is greater than 10" :)
But otherwise your point is valid.
This is used in theorem provers, for example, so that you don't have to verify proofs of theorems over and over again (which can be very slow).
Instead, you verify them once, save the state of the heap to disk (as a binary ELF, for instance) and then you can run the binary to continue exactly where you left off (i.e. with all the interesting theorems already in memory, in a proved state).
This is what the HOL4 theorem prover's main `hol` script does, i.e. it runs HOL4 by loading such a memory state from disk, with the core theories and theorems already loaded.
Presumably, to make this reproducible you'd need to make sure that all the memory objects are saved to disk in a deterministic order somehow (e.g. not in memory address order, as it can change from run to run, especially when using multiple threads).
Edit: Presumably you'd also need to make sure that you persist the heap when all threads are idle and in a known state (e.g. with all timers stopped), to avoid random stack states and extraneous temporary allocations from being persisted, which would also affect the resulting binary.
Except that the Linux kernel falsely taints itself with the "proprietary" bit when a module with a non-proprietary, non-GPL compatible license is loaded.
But of course, not being GPL compatible does not necessarily imply that it's proprietary, e.g. the CDDL (as used by ZFS) is a non-GPL compatible, free software license (according to the FSF).
And furthermore, this is documented and intentional.
It is, but that's not the observation I was making. You only mentioned one way of solving the problem, but that's not the only way.
> That is, it turns out that the only way to verify whether an arbitrary finite-state Turing machine will halt on a specific input is to check all possible states
What do you mean by all possible states? If you mean literally all possible states, that's not true. I mean, yes, you could iterate over all possible states to solve that problem, but that's probably the least efficient way to solve it.
There are already-known algorithms which always solve the Halting problem for machines with finite state, and they don't need to iterate over all possible states. They do, however, need to iterate over all state transitions that the machine actually goes through (multiple times, even). However, these algorithms that I'm mentioning (i.e. cycle detection algorithms) are also quite dumb. They don't exploit any knowledge about the state transitions in order to analyze whether the machines halt or not, they just simulate the machine step by step (this is due to the definition of the cycle detection problem itself, which does not allow inspecting the program).
In principle, and even in practice, it's possible to make those algorithms significantly more efficient, at least for many of the machines (i.e. programs) that we care about.
I suspect it is not possible to make such a (fully automatic) algorithm significantly more efficient for all possible programs (even the nonsensical ones), although I don't think such a proof exists (if it does, I would like to see it). The closest I've been pointed to is a paper possibly implying that such an algorithm would have to be EXPTIME-complete, although even the person that pointed me to that paper had some difficulty interpreting it -- and even if that were true, that says nothing about its real-world efficiency.
> That is, it turns out that the only way to verify whether an arbitrary finite-state Turing machine will halt on a specific input is to check all possible states
Can you point me to a source that proves this claim? Not only I'm doubting it, but even if you are right, I'd be really interested in reading such a proof.
> For an example, an arbitrary program for a computer with as much memory as the infamous "640KB is enough for anyone" quote would require at least 640,000^255 (~10^1480) computational steps to check if it halts.
Again, I'm wondering why you are claiming that the only possible algorithms which can check whether arbitrary finite-state programs halt have to iterate over all possible states (or even all the actual state transitions).
If you take that description at face value and consider a model of computation with finite state (like real-world computers have), then it is decidable.
If you take the usual formal description of the halting problem, which like you said, is specifically defined over Turing machines (i.e. a theoretical model which assumes you can have a machine with literally infinite state, which is impossible to construct in our universe), then yes, you'd need hyper-computation to solve that.
BTW, it's not only hyper-computation that can solve the halting problem.
The halting problem is decidable in models of computation that have finite state (although the decider machine does need more state than the machine being analyzed).
Tangential question, but is this going to annoy dogs?
It can also be a self-reinforcing behavior, as giving credit can also in turn benefit you later.
Again, just because everything is predetermined doesn't mean there aren't complex dynamics in motion, ones which greatly influence behavior and the chances of making a decision. Understanding these dynamics can also influence how you behave in the future.
Edit:
It seems that I am saying "if you kick a raccoon, it will run away". And you are saying "whether I kick the raccoon or not has already been determined".
In this case, my analysis is helpful/useful while yours isn't. My analysis can influence your future behavior (e.g. if you run into a menacing raccoon in the future, it will increase the chances that you will be able to defend yourself properly), especially if you didn't know this before, while your analysis probably doesn't affect behavior (except to promote apathy perhaps, which is likely even detrimental).
[ Disclaimer: I know nothing about raccoons, it was just an example ]
It doesn't mean you are wrong, it's just that saying "everything is predetermined" is not a useful way of looking at the world. It's like saying "white paint is white", which is not very surprising.
Strictly speaking, it's not even quite correct: quantum mechanics tells us that, even though the universe has (deterministic) physical laws, it also behaves randomly at a fundamental level. However, that does not change the fact that we don't have free will (since we have zero control over the randomness).
But it's conceivable that some of our decisions might be affected by quantum randomness (this is even obvious in some contrived, but realistic Schrödinger's-cat-like scenarios).
Just because you don't have free will doesn't mean your behavior is not affected by your environment.
But there is. It's `zpool clear <poolname>`.
That said, you probably need to have created or imported the pool using stable device names (e.g. `zpool import -d /dev/disk/by-id` or `by-part-uuid`, for example). Otherwise, when reattaching the USB device it might get assigned a different device name (e.g. `/dev/sdb` instead of `/dev/sda`) and ZFS might think the device is still unavailable.
Are you absolutely sure they weren't engineered by some alien mad scientist? Or even a sane one, just for giggles?
However, whether that translates to a loss in momentum is a bit more fuzzy and I really can't tell whether it does or doesn't. Although I'm far from being a physicist, so hopefully someone more knowledgeable chimes in to enlighten us...
But I'm curious: what is your reasoning for asking whether photons have a mechanism to lose momentum as a consequence of them affecting the curvature of spacetime? It's not at all obvious to me the relationship between these two concepts.
Spoiler warning:
"Are cats liquid? I saw this question asked on the Internet. It was based on the common definition that a liquid is a material that can adapt its shape to its container. <Cue photos of cats fitting inside a jar, a basket, a wine glass, etc>. It seems to be the case."
This moment at 35m25s was also priceless:
"We have two past winners who have been kind enough to join us tonight.
First, the 2008 Ig Nobel Chemistry Prize was awarded jointly to one team who showed that Coca-Cola is an effective spermicide. And that prize was jointly awarded to another team who showed that it's not."
On a more serious note, I'm not sure if I will ever understand why many of the Ig Nobel prize winners got funding for their research...
As I mentioned, no "wasting" is happening. The "wasting" is all in your head. I can assure you that every watt is being used to its capacity (up to the unavoidable physical and other loss limits, like any electricity use).
> is the free-market equivalent
No, it isn't. That's not what "free-market" means. A carbon tax would have to be enforced by a government or government-regulated authority, it wouldn't be done in a free market. Free markets do not price externalities such as carbon emissions.
It's one of the jobs of governments to regulate markets, so that they work as efficiently as possible. In fact, that's one of their most legitimate and useful jobs. Furthermore, governments are the ones who have a monopoly on regulation. So if they are not regulating correctly, you know exactly who to blame. There's no one else responsible for doing that job.
> The truth or falsehood of the statement is irrelevant, it's politically ludicrous.
Well, I don't think that's true, but even if it were, if you keep blaming Bitcoin and similarly singling out other uses of energy as the culprits of carbon emissions, it would keep being politically ludicrous, because there are always people and businesses who would be affected by the demonization of such uses and would feel personally (or corporately) attacked by being singled out.
Which means that the only real, efficient and fair way of reducing carbon emissions is to tax them all equally. Whatever businesses (or other energy uses) stop being lucrative and go bankrupt, are exactly the businesses that should go bankrupt, because they are not sustainable (as long as the carbon emissions are taxed at an environmentally sustainable level and not more).
If you're going to reduce emissions, and practically all developed countries are working to do it AFAIK, then it should be done this way and I don't see why right-wingers or anyone else should object to such a plan, rather than what is really ludicrous, which is to arbitrarily demonize uses of energy, one by one, until you reach a critical mass of users who eventually are going to say "enough is enough".
Now, if your argument is that right-wing governments are in principle opposed to reducing carbon emissions, that's a completely different argument and again, it has nothing to do with Bitcoin. It's a political issue alone and the blame-shifting is not going to solve it.
> that means that avoiding spending excessive electrical energy on inefficient vanity projects is a matter of personal responsibility.
See, here are the problems with that argument:
1. There's no "excessive" electrical energy being used.
2. The project is not "inefficient".
3. It's not a "vanity" project.
4. It's not a matter of personal responsibility either. Once again, that's blame shifting.
Personal responsibility in the way you are imagining it is not going to solve this problem.
It'd be way, way, way, way easier to actually influence a right-wing government to solve it, once and for all, in the most efficient way possible, for the entire population than to change the behavior of hundreds of millions of people individually (especially by writing unconvincing arguments on the Internet).
Fossil fuels have nothing to do with Bitcoin, but rather how countries manage their electricity production. Bitcoin works just as well with electricity produced by renewable energy. And all other uses of electricity (of which Bitcoin is an insignificant percentage), or even worse, uses of energy in general, are also backed by fossil fuels (even more than electricity alone).
So if you're not happy with how your government manages electricity production (or how they're not taxing emissions enough), go ahead and complain to your elected politicians instead of shifting the blame to those who legitimately want to use electricity for their own purposes, which they have a right to, like anybody else who uses electricity.
The reason cats are being sterilized is, supposedly, "to avoid indiscriminate reproduction and possible abandonment" of the cats themselves.
The law is called "Animal welfare law" and it's only about pets and their owners. It has nothing to do with endangered or invasive species or even any other type of environmental concern.
In Spanish (behind a paywall): https://elpais.com/clima-y-medio-ambiente/2023-09-28/llega-l...
The new law introduces quite a few other rules as well: you can't leave your dog alone on the street (e.g. tied to a street lamp while you enter a shop), you can't leave your dog alone on a balcony or in a car, you can't leave your dog alone for 24 hours anywhere, mandatory pet owner course if you have a dog -- although the Spanish article says it's for all pet owners, even birds -- that said, currently the course is postponed because they couldn't prepare it on time; mandatory insurance for your dog, steep fines for breaking these rules, etc.
Working dogs are exempt from these rules. Not only are they being discriminated, but they also don't have a right to minimum wage despite having a job.
Why they are sterilizing the cats and not the mosquitoes and the cockroaches is beyond me. Cats can't even fly!
But really, in general, anything that would require pressing the same key a variable number of times in a row might benefit from a knob control, especially if it makes sense to do the same thing in some "opposite" direction. And especially if you do that multiple times per day. So it kind of depends on how you use your computer.
See this URL and search for "Programmable Knob":
https://www.keychron.com/products/keychron-q6-qmk-custom-mec...
If you go down a bit, you'll see you can program a knob rotation (in one direction or the other) to perform a macro, including key combinations. I'm pretty sure there are also key designations for mouse movements.
That said, you might not be able to adjust the granularity of the mouse movement very well (not sure, really).
I think all of them have hot-swappable keys and many of them even have hot-swappable mechanical switches, I think. In most of their keyboards, all the keys (and key combinations) are fully configurable at the hardware level as well.
I can vouch for the quality of the ones I have (Q3), but mine don't have Bluetooth so I don't know how well that works.
Anyway, thanks for the info! Unfortunately the GMMK PRO doesn't seem to have the layouts I prefer, but I'll keep an eye on future products!
After using this keyboard, I can't imagine ever buying another keyboard without a knob. It's really great to control your audio volume with an appropriate hardware control rather than pressing the same key 15 times in a row like an idiot or fiddling around with the mouse.
You can configure the knob (or any key) to do different things with different key combinations, at the hardware level even (with the Via tool), so you don't have to configure multiple OSes one-by-one to do the same thing. I've configured Alt+Knob rotation to control my screen brightness, which I adjust multiple times per day. You can also configure it to control the zoom, or move the mouse, etc.
The knob also functions as an additional key if you press it downwards. I think by default it is configured to mute (which makes sense, since by default a knob rotation without any other key combination controls the audio volume).
When you go look for keyboards with a knob you won't find many, and the Keychron keyboards (Q-series and Q Pro-series, the latter being both wired and wireless), are really the best there is AFAIK (unless you create your own, perhaps).