quchen

18 ms·

151.
by quchen 4y ago
Why does it fail to exist? It’s an axiom that can be added to intuitionistic axiom systems just as well as for classical ones, no? It’s orthogonal to the law of the excluded middle after all. In constructive mathematics with AC, you would j
152.
by quchen 4y ago
> It depends on what you think a number is. Let’s not mix up teminology and semantics. What a number here is is quite clear, we’re all talking about relatively standard math, the standard axiom of choice, and not some opinion on numbers.
153.
by quchen 4y ago
> e and pi arise in axiomatic systems we use to approximate our world. They never appear in nature. It’s like that for all numbers, not just the fancier ones! I have never experienced a 1.
154.
by quchen 4y ago
> You can’t say you can’t chose an item from a set because you can’t describe the item. Or rather: the whole point of the axiom is giving you such a description.
155.
by quchen 4y ago
Had a laugh about that too. It’s sometimes hard to tell what’s »non-technical« when you’ve spent a lot of time on something, and even then what it means to be »technical« depends a lot on the audience. Non-technical here means knows basic m
156.
by quchen 4y ago
The philosophical zombie might be an interesting rabbit hole for you! https://en.m.wikipedia.org/wiki/Philosophical_zombie
157.
by quchen 4y ago
(Derailing this troll-initiated thread a bit with a serious answer) > what’s the formula for quicksort That is expressible! It’s what one would write in a proof assistant or powerful type system such as Coq, Agda, Idris. The formula is t
158.
by quchen 4y ago
This, but unironically. Their formula (11) involves basics (sums and products), the only nontrivial part would be the partial partitions, and for that the first paragraph of chapter 2 explains how to get it from ordinary partitions, which i
159.
by quchen 4y ago
»More than exponential«. The standard formula for determinants of an n×n matrix (equation 1 in the paper) is the sum of n! terms, one term for each permutation of {1..n}. The paper details a method (equation 11) in which the sum is instead
160.
by quchen 4y ago
You just made me realize it’s an adventure game. It’s also an RPG and choose-your-adventure game and so much else, that I filed it as »Disco Elysium« without ever thinking about genres.
161.
by quchen 4y ago
These seem to be more complicated versions of the Yosemite Bowline; do you have any info on that one? It’s been my go-to bowline for all applications (climbing, sailing), yet now I’m wondering whether it has some weakness I don’t know about
162.
by quchen 4y ago
> Rows run, columns climb What a great mnemonic, I’ll start using it even though I typically don’t mix the two up! Thanks a lot.
163.
by quchen 4y ago
Smooth often means that higher derivatives are continuous as well. A straight line changing into an arc has continuous first derivative, but the second is discontinuous.
164.
by quchen 5y ago
It’s >>= but with a font very poorly chosen for a tutorial :-| FWIW C and C++ also have this operator, it does bitwise right shift assignment there.
165.
by quchen 5y ago
Should mean the same thing as means has the same result value here. The operational semantics could be different, as you mention: even without side effects, computing x may be very expensive. This isn’t even special to FP, it’s a basic
166.
by quchen 5y ago
That sounds cool! Is there some preview documentation available somewhere?
167.
by quchen 5y ago
Isn't that exactly how any constructive proof works?
168.
by quchen 5y ago
Monad and Functor were first, if I remember correctly Applicative made its debut when Parsec became popular. For a long time, the hierarchy was »Functor ===> Applicative, Monad is independent«. We made Applicative a superclass of Monad a
169.
by quchen 5y ago
Just enumerate them all, if none is missing it's fairly easy to compress. (And 1b per number is really inefficient) ;-) main = traverse print [1..99999999]
170.
by quchen 5y ago
Yes, u is often used as an approximation to μ. Pronounce it »micro«. The most prominent abbreviation is uc for microcontroller, and uLisp is »Microlisp«.
171.
by quchen 5y ago
This is really cool, I would love to program my fleet of ESP8266s with anything but C. And I’ve been passively interested in using Lisp for many years. Using Lisp for my program as glue for the normal ESP C libraries would be awesome. I’v
172.
by quchen 5y ago
Every day isn’t sustainable, but Psilocin/LSD tolerance builds as fast as it diminishes again, typically gone within a week or at most two. If you want to abuse them, the chemicals certainly won’t stop you. And when you’re in the minds
173.
by quchen 5y ago
I'm open to doing it again, but I have no particular urge to do so. I'm torn between taking it for fun (but unhappy about the lack of depth) or for reflection (which is hard to plan for and exhausting). In the end it's a very
174.
by quchen 5y ago
> excessive and sustained consumption of psychedelics seems to lead people into increasingly weird thoughts We have lots of _clinical_ evidence even that that’s the case for a lot of medication, which is why we don’t usually administer e
175.
by quchen 5y ago
In my experience, »mushrooms rewire you« does not really do them justice: they mostly help you rewire yourself; more like changing habits (internal) rather than surgery (external). Here’s a personal example: a couple of years ago I had a ve
176.
by quchen 5y ago
On the contrary, parties can be very safe environments. Much like there are better and worse places to drink, there are better and worse places for taking other drugs. A lot of factors play into the setting. Music is very often a plus, feel
177.
by quchen 5y ago
Did they mention why? Sounds like FUD to me, since the psilos I know of are mostly water, indigestible chitin, and trace amount of kidney-excreted psilocin/psilocybin.
178.
by quchen 5y ago
Ponzi is also derogatory. You should not dismiss the fact that Bitcoin kicked off blockchain as a technology, got a lot of people into a sort of financial playground, had questionable value and utility initially, and all that. All that cons
179.
by quchen 5y ago
One of my favourite papers of all time. Most of the paper is a good joke, but Slowsort takes it a step further. It is just so inefficient I can’t help but laugh out loud each time I revisit the paper and re-understand the algorithm. It ti
180.
by quchen 6y ago
I think this would be misleading once you dive deeper into particle physics. The strong interaction is really »the interaction mediated by gluons between color-charged things«. • Gluons interact with gluons, without the need for quarks. • M

More ›