librexpr

((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 you define division by zero.

More generally, in normal math, every theorem that involves division by some value Y which could be zero must have as hypothesis that Y is not equal to zero. All these theorems still work in systems like Lean where division by zero is defined to be zero, so nothing is lost.

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/expansion is that (|n| args...) = n - numargs when n >= numargs. This happens to coincide with False when n = numargs + 1, so it would have been better if I had said "when n > numargs + 1".

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 must be toplevel, not as an argument to another function, because otherwise it is lazy and not executed. The number of args also cannot be infinite, since that would require an infinitely large program.

The expansion into |n|(args...) must happen before we know what n is, because in the lambda calculus we can't know anything about a function without calling it. Since it happens before we know what n is, then the number of args will necessarily be the same for all n. When n > numargs, |n|(args...) ignores all its arguments and halts, and therefore f cannot be a useful test for zero.

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 "painting", even though all of these things are considered "art". The name could be just "AI songwriting", or it could be some fancier name (like "photography" has a fancy name).

Giving it a different name would also imply that you shouldn't submit AI songs to a songwriting competition, much like you wouldn't submit a photograph to a painting competition, but you could have separate competitions for AI songs, and separate competitions that accept anything, and so on.

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 personally I have no problem with considering GPT stuff "art", but I think it should be considered a separate art form and given a different name.

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 stack, especially if the tree has many kinds of objects and many branches.

Unfortunately in most languages this pattern will lead to stack overflow on medium-sized inputs, so you can't often use it unless you're using a language like Racket or Erlang which can't really stack overflow.

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 them without engaging with their arguments. This does not lead to good discussion.

I think that unaligned and sufficiently smart AI could kill everyone because I looked at the arguments for and against and came to a conclusion. Presumably this is the same thing you did. I know my own mind better than you, and I'm telling you that your attempts to explain why I disagree with you are completely off the mark.

> We don’t enact public policy based on predictions of a biblical apocalypse, nor do we ban televisions or computers because groups like the Amish disapprove of them.

The reason we don't do that is because we evaluate their arguments and disagree with them. It has nothing to do with who they are or why they believe what they believe.

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 risks of AI. You can do better than this.

Sorry, you seem to be confusing HTTPS with E2EE. Mastodon already uses HTTPS for all its traffic, including the traffic between servers.