librexpr

5 ms·

1.
by librexpr 10mo ago
> Say I want natural numbers, I need to choose a concrete implementation in set theory e.g. Von Neumann, but there are multiple choices. You don't need to choose a concrete implementation. If you don't want to choose a constru
2.
by librexpr 3y ago
((x / y) * y) = x is not a true statement about real numbers, regardless of if division by zero is defined as an error or as being equal to 0. The true statement is ( y != 0 -> ((x / y) * y) = x ), and this holds no matter how
3.
by librexpr 3y ago
Yudkowsky was not fooled. He made three tweets on this subject in that time frame, which can all be seen using this link: https://nitter.net/ESYudkowsky/search?f=tweets&since=2023-05... First tweet: > ...can we
4.
by librexpr 3y ago
"Carrier" isn't a mathematical term, they're just using that word in place of the word "set" to distinguish it from ZF sets. "Group" refers to a specific kind of mathematical structure[0], but it&#x27
5.
by librexpr 3y ago
You're right, that was imprecise of me. But if F = (\x. \y. (|n| args...)) is equivalent to True or False, then it is also equivalent to (F True False), which brings us back to a toplevel (|n| args...). Another slight correction/e
6.
by librexpr 3y ago
I'm pretty sure it's impossible to write a function that tests for zero for these numerals. Necessarily, any such function f(|n|) would have to expand at some point into a toplevel |n|(args...) with some number of args. This call
7.
by librexpr 3y ago
I explicitly said that I don't mind calling it "art". I meant that things like "AI songwriting" should be given a different name than "songwriting" like "photography" has a different name than &q
8.
by librexpr 3y ago
You'll note that "photography" as an art has its own name and is considered a different art than painting or drawing. And if you took a photo and then said "I drew this", people would say you were lying. So person
9.
by librexpr 3y ago
I mostly agree, but one really nice use case for recursion is when dealing with trees. For example, writing a function parse_object() that recursively calls itself to parse child objects is way more pleasant than manually managing your own
10.
by librexpr 3y ago
None of the comment is apt. You're seeing people you disagree with and assuming that if they disagree with you it must be because they're crazy, and then you use words like "cult" and "LARP" to try to dismiss t
11.
by librexpr 3y ago
Oh my god will you people stop with the bullshit psychoanalysis. People disagree about things all the time, it's normal, you don't need to invoke this pseudo-Freudian nonsense to explain why people disagree with you about the risk
12.
by librexpr 4y ago
I wish people wouldn't spread rumors like this. ActivityPub does have shared inboxes[0] and Mastodon does use them[1], so no duplicate messages will be sent in your example. [0] https://www.w3.org/TR/activitypub&#x
13.
by librexpr 4y ago
I think if we take "description of a number" to mean "ZF formula that uniquely picks out that number", then that cannot be defined, because a formula picks out a number when it is true for that number and false for all o
14.
by librexpr 4y ago
You might want to check out the Gödel–Gentzen negative translation[0], which is an interpretation of classical logic in intuitionistic logic, which can be (somewhat inaccurately) summarized as "if P is provable in classical logic, then
15.
by librexpr 4y ago
Sorry, you seem to be confusing HTTPS with E2EE. Mastodon already uses HTTPS for all its traffic, including the traffic between servers.
16.
by librexpr 4y ago
In addition to this, I'd like to add that intuitionistic logic is consistent if and only if classical logic is. This follows from the Godel-Gentzen negative translation[0], which implies that for any contradiction in classical logic, y
17.
by librexpr 4y ago
Cantor's work on infinity and the diagonal argument was hugely important in mathematics, paving the way for important results like Godel's incompleteness theorems, the halting problem, the creation of modern set theory which allow
18.
by librexpr 4y ago
Maybe it would have been a good idea to have two names for unwrap, one which would mean "I'm certain that this value will always be okay", and another which would mean "I'm taking a shortcut because I'm writing
19.
by librexpr 4y ago
Mathematicians can skip a lot of steps because they have a good intuition of what's possible and what's not, so it's enough when they know that in principle something could be proven. But this can make it hard for a beginner
20.
by librexpr 4y ago
I just want to point out that you don't need to know the precise bounds of such a computational model to prove things about your programs. There already exist Turing-complete programming languages where you can prove non-trivial proper
21.
by librexpr 4y ago
Quoting from Wikipedia about Rice's theorem: > for any non-trivial property of partial functions, no general and effective method can decide whether an algorithm computes a partial function with that property This basically translat
22.
by librexpr 4y ago
Rice's Theorem isn't as strong as you say it is. What it says is that there exist programs that it's impossible to prove whether or not they have specific non-trivial properties. But there still exist many programs where we
23.
by librexpr 5y ago
There's a big difference between publishing the source code of malware while clearly stating that it's malware, vs publishing trojan malware on NPM while knowing that it will be automatically installed by a bunch of package manage
24.
by librexpr 5y ago
Hmm, good try, but it's not quite right. Here's a simpler way to get all the numbers divisible by 2, 3, 5, or 7, in a 100-number range, and which I think is easier to verify that it's correct: numbers_not_divisible_by_2
25.
by librexpr 5y ago
I did propose a solution to all these reputational damages you mentioned: requiring clearly labeling derivative works as derivative works. Someone selling something that looks like your work won't affect your reputation if they have to
26.
by librexpr 5y ago
I've been nerdsniped haha. Just found this quora question which is the same as what you asked: < https://www.quora.com/Assume-n-1-How-can-I-prove-one-can-onl... > But the answers seem wrong? The first one uses only
27.
by librexpr 5y ago
(I meant 20 + 30, not 20 + 50, sorry for the confusion.) I don't think I understand in what ways it can be damaging to reputation. Maybe you mean if I pretended to be the original author? Because in that case I think it's a differ
28.
by librexpr 5y ago
I'm just an amateur, but if you don't mind some brute-forcing, it's enough to prove that for every n between 1 and (2*3*5*7*11*13)/10+1=3004, exclusive of 1 but inclusive of 3004, there are at most 23 numbers between 10n
29.
by librexpr 5y ago
The ability to preserve, study, and build on works is very important to me. Some of my favorite fiction is fanfiction, there are many ROM hacks and mods that improve games I've played, etc. Shorter copyright would enable these things b
30.
by librexpr 5y ago
It didn't mess up the instruction "make every fifth line bold". The blank spaces between each "paragraph" are empty lines, so it counted them too. I think this is perfectly reasonable behavior, it's what I woul

More ›