00:05:50 -!- Phantom_Hoover has quit (Remote host closed the connection). 00:06:18 -!- Phantom_Hoover has joined. 00:06:38 -!- Zarutian has quit (Quit: Zarutian). 00:09:54 -!- DHeadshot has quit (Ping timeout: 265 seconds). 00:15:58 -!- pumpklynn has changed nick to lynn. 00:20:54 -!- Hoolootwo has quit (Excess Flood). 00:21:04 -!- zemhill__ has joined. 00:21:07 -!- Hoolootwo has joined. 00:21:24 -!- wob_jonas has quit (Quit: http://www.kiwiirc.com/ - A hand crafted IRC client). 00:26:16 -!- zemhill_ has quit (Ping timeout: 247 seconds). 00:26:25 -!- hppavilion[1] has quit (Ping timeout: 268 seconds). 00:42:33 -!- oerjan has joined. 00:43:01 -!- moonheart08 has joined. 00:43:07 you thought i died? 00:43:14 nope. i havent even got the disk to boot right >_> 00:44:07 * moonheart08 is messing with the partitions 00:45:01 @messages- 00:45:01 boily said 13h 57m 33s ago: hellørjan. you really did special case sed -i. bleh! flblblblblbl! :Þ 00:45:29 @tell boily would i lie to you? unless it somehow involved a horrible pun, that is. 00:45:29 Consider it noted. 00:48:45 shachaf: wow, I believe the karma/more interaction was lost in March 2012 00:53:24 -!- moonheart08 has quit (Ping timeout: 265 seconds). 00:55:22 int-e: now i'm wondering how much of the geisterdamen language is nonsense and how much the foglios have actually assigned meaning to... in any case, clearly Eotain now considers this Personal. 00:56:53 -!- ais523 has changed nick to callforjudgement. 00:56:55 -!- callforjudgement has changed nick to ais523. 00:57:16 that was, somehow, a consequence of letting an extra finger brush on my touchpad 00:57:20 Konversation is weird 00:57:53 the keys are like right next to each other 00:58:59 <\oren\> I gave each kid about 500 grams of candy 00:59:06 oerjan: believe it or not, I have not gotten around to GG yet 00:59:13 int-e: shocking 00:59:23 I had important game to play ;) 00:59:41 and now I'm looking at this stupid bot 00:59:57 meanwhile, i haven't got any further than GG. somehow after not getting more than 6-7 hours of sleep for several days, today my body wanted 13. 01:01:52 int-e: i considered making it @quit yesterday instead, but i was too curious how long it would take... 01:02:44 3 hours... but apparently it discards messages to channels that it has left 01:03:12 int-e: well it seemed to get through them slowly nevertheless. 01:03:48 int-e: it was sending despite not being in the channel 01:03:56 I did a mode -n for a few seconds to check 01:04:03 oh right it did 01:04:13 oh. 01:04:30 bug upon bug 01:06:18 int-e: otoh the last time i got many @tells at once, i was positively surprised that it _didn't_ drop any (although maybe asking for them in public was a bad move), if that's related it would be nice to keep. 01:06:57 no, that's unrelated 01:07:21 because i remember it used to do so. 01:10:29 oerjan: https://github.com/lambdabot/lambdabot/commit/d695bbf4b2d805d508107f23dbeb4382f07f9b5a ... you've been very quick to notice ;) 01:11:04 anyway I really suspect the karma thing has been broken for several years... but it's hard to be certain. 01:11:34 depends when someone last tried that command... i remember it being used before... 01:11:41 (too many indirections in the code for effective archaeology) 01:11:49 and it would be strange if no one did for 4 years. 01:12:30 int-e: is it possible that it always bypassed @more, but that there used to be a _different_ cutoff mechanism that caught it? 01:13:03 i.e. i think you reorganized that sort of stuff at one point 01:13:32 int-e: No, I linked to some logs that had @more for @karma-all in Dec 2012 01:13:54 http://codu.org/logs/log/_esoteric/2012-12-29#191333oerjan 01:14:11 (that's why i'm asking about the @tells ... if that was the sort of thing that happened, they could have been changed by the same thing.) 01:14:56 but i guess your github link makes that unlikely. 01:15:30 shachaf: 2012 _was_ several years ago hth 01:15:42 has really no one used the command in between? 01:15:51 int-e: see also http://codu.org/logs/log/_esoteric/2013-04-14 01:16:51 int-e: oh, note http://codu.org/logs/log/_esoteric/2012-12-29#191156lambdabot , that eventually timed out too 01:16:55 Hmm, but see #haskell on 2013-07-11 01:16:56 Timeout. 01:17:09 shachaf: LINK 01:17:24 oerjan: tunes.org took down the old logs htdnh 01:17:39 i think they're archived somewhere? 01:17:47 You can download http://tunes.org/~nef/logs/old/haskell-13.zip if you really want to. 01:18:05 Oh, I bet ircbrowse.net has them. 01:18:20 http://ircbrowse.net/browse/haskell?id=16059990×tamp=1373543230#t1373543230 hth 01:19:00 yay 01:19:32 so the command amassed two separate flaws 01:19:57 I kind of want to exploit this bug while it's still around. 01:20:04 But the only way to do it is to annoy people. 01:20:08 So I guess I won't. 01:20:32 indeed. i noticed it also slows down lambdabot at large 01:20:49 so maybe we should have @quit it 01:20:52 slambdabot 01:21:00 int-e: Does lambdabot auto-restart on @quit? 01:21:12 Also you should add me to the admin list. 01:22:18 shachaf: it does unless you do it twice in quick succession 01:23:08 not entirely sure how quick 01:30:15 5 minutes, apparently 01:38:19 -!- jeff-the-killer has quit (Quit: jeffl35 has quit (Quit: jeffl35 has quit (Quit: jeffl35 has quit (Quit: jeffl35 has quit ...). 01:39:03 -!- jeffl35 has joined. 01:39:04 -!- lambdabot has quit (Quit: bad karma). 01:41:20 -!- hppavilion[1] has joined. 01:41:38 Quick, is the syntax for Unefunge the same as for Befunge? 01:42:00 yes 01:43:06 there may be a certain lack of ^ and v 01:43:16 * oerjan doesn't actually know 01:43:44 -!- lambdabot has joined. 01:44:03 @karma-all 01:44:08 blah 31337 01:44:14 egrep 31337 01:44:24 nobody 2000 01:44:30 C/C 1712 01:44:36 [5855 @more lines] 01:44:38 what happened to zgrep 01:45:00 `which zgrep 01:45:07 /bin/zgrep 01:45:13 shachaf: still there hth 01:45:18 good question... some sort of internal timeout? I don't know, and it's really too late to figure that out. 01:45:24 @karma zgrep 01:45:28 zgrep has a karma of 31337 01:45:42 fancy 01:46:19 @karma-all 01:46:20 blah 31337 01:46:20 egrep 31337 01:46:20 zgrep 31337 01:46:20 nobody 2000 01:46:20 C/C 1712 01:46:22 [5855 @more lines] 01:46:30 hmm, no timeout logged though 01:46:37 err, oops 01:46:40 Interesting that it still generated the line, which is why @more cut it off after 4 lines. 01:46:43 there it is: [ERROR] : Main: caught (and ignoring) <> 01:46:46 I was wondering about that. 01:48:16 but anyway... this fix should hold for now 01:48:18 does @tell ignore timeouts too? 01:48:30 because it did take some time i recall 01:48:36 and longer than that 01:48:44 in which case it might have the same problem 01:49:10 er @messages etc, i guess 01:52:36 no, @messages is different, I believe 01:52:49 but I really can't think straight anymore, need sleep, see yoyu 01:52:55 good night 01:52:58 that hello world in seed is pretty fun 02:04:35 -!- godel has joined. 02:11:15 -!- hppavilion[1] has quit (Ping timeout: 268 seconds). 02:11:54 -!- nisstyre has joined. 02:12:07 -!- nisstyre has quit (Changing host). 02:12:08 -!- nisstyre has joined. 02:28:50 -!- hppavilion[1] has joined. 02:31:56 -!- Phantom_Hoover has quit (Remote host closed the connection). 02:38:18 Target player sacrifices a nontoken nonland permanent of your choice. Choose a nonland permanent card from the sacrificed permanent's owner's graveyard and put that card onto the battlefield under the control of the sacrificed permanent's controller. 02:38:57 Do you like this? 02:39:11 Hm, the set of all sets that do not contain themselves is just the set of all sets 02:39:16 Because no sets contain themselves :P 02:39:22 uh 02:39:34 under what axioms? 02:39:37 hppavilion[1]: I think in some theories sets can contain themself 02:39:47 quintopia: Shhhh 02:40:07 quintopia: Various axioms, most importantly the "sets never contain themselves" axiom? 02:40:17 boring 02:40:19 S \union {S} = S, I guess? 02:40:19 is that an attempt at humour 02:40:26 shachaf: Not even an attempt 02:40:31 shachaf: Just sadness 02:41:01 It's an attempt at humor like being bald is a hair color, like abstinence is a sex act, etc. 02:41:16 * hppavilion[1] . o O ( Did he-who-shall-be-named invent abstinence? ) 02:42:27 It has been said that like atheist to be religion is like being bald is hair color. 02:42:54 zzo38: Yes, that's where I got those 02:43:15 It's weird to me that people reject blackboard bold as distinct from bold, and advise that normal bold be used in typeset works 02:43:55 Blackboard bold is more distinct anyways isn't it? 02:43:59 It seems like it'd be better to use BB exclusively, because it's more visually distinct from normal letters than CB (which is just "the same letter, but thicker") 02:44:03 zzo38: Yes, exactly 02:44:45 But it depend what is being written, what kind of format is appropriate for it. 02:45:52 At the very least, BB should be used for |Reals, |Naturals, |Zintegers, and |Qationals because that's what we all recognize 02:46:13 fraktur 4 ever 02:46:14 And maybe also |Complexes and |Primes 02:46:25 In those cases yes you should use the blackboard bold 02:46:30 shachaf: Fraktur is nice too, to indicate separate things 02:46:48 𝕭𝖑𝖆𝖍𝖇𝖔𝖗𝖊𝖉 𝕭𝖔𝖑𝖉 02:47:29 shachaf: Isn't that more like Anciente ſcriptur Boulde? 02:47:43 zzo38: I think of BB as indicating certain "ubersets"- the big, important ones; like reals, naturals, integers, and primes 02:48:00 The standard Computer Modern fonts do not have blackboard bold, but does include calligraphic letters 02:48:14 So they should *definitely* be used for those, and for non-universal things they should be limited to the VERY important sets 02:48:17 So, you can add extra fonts if you want blackboard bold or fraktur fonts 02:48:37 Though, for the set of boolean values I like to write a T+F amalgamation :D 02:48:54 ("set of boolean values") 02:49:31 There should also be a standard symbol for irrational numbers, IMO 02:49:44 subobject classifers are no joke, yo 02:50:10 I've seen J| used, by analogy that Q is 10 from the end of the English alphabet and J is 10 after the beginning, and |Q and J| are disjoint 02:50:44 How are you going to write a T+F amalgamation; you can add it into a font by use of METAFONT if you like to do so, though. 02:51:05 R\Q is fine 02:51:19 fairbairn threshold, yo 02:51:46 shachaf: ?? 02:52:04 @google fairbairn threshold 02:52:05 https://www.haskell.org/pipermail/libraries/2012-February/017548.html 02:52:07 zzo38: Are you asking what a T+F amalgamation looks like or how I plan to put it in a computer? 02:52:23 hppavilion[1]: Both 02:52:23 google.com is one of the ""hidden gems"" of the internet 02:53:01 zzo38: It looks like a T with a shorter tick on the left coming from the middle, like in the letter "F" (but with the other side of the "hat") 02:53:26 But, by use of METAFONT you can make fonts out of whatever shapes you want. 02:53:32 shachaf: I didn't know whether it was a real thing, or even a pun 02:53:33 hppavilion[1]: Ah, OK 02:54:16 what's a good name for a data structure which encodes proofs of correctness? 02:54:23 like a map that does this is a ? map 02:54:51 elaborate twh 02:55:05 alercah: I do not understand. Is it like a... yeah, no idea 02:55:22 I was going to say "Bloom filter", but that's not what you're asking 02:55:37 so like, a normal map provides you with guarantees like "if you insert (k, v), then (k, v) is in the map" 02:55:55 I'm writing an interface for maps that provide proofs of such properties in Idris 02:56:09 alercah: You might like something like "JuryMap" ("jury" because it's proven correct) 02:56:15 hah 02:56:39 "Jury" could be replaced with "Judge" depending on whether this is Japan 02:56:54 (In Japan, cases are decided by the judge; no jury is present. Like fascists.) 02:57:56 alercah: Not a joke though. That's actually pretty good; you'd have to leave a comment to say what it does, obviously, but after that people will immediately make the connection and it will be easy to remember 02:58:47 alercah: "certified" is the usual adjective, I believe 02:58:52 ais523: thank you 02:59:05 i.e. a certified compiler is a compiler that's been proven to implement the language it claims to implement 02:59:21 s/i\.e\./e.g./ 02:59:28 hppavilion[1]: Japan recently added a system of lay judges... 02:59:44 some European nations have judge-alone trials, no? 02:59:46 pikhq: Oh? Haven't heard about that 02:59:48 (need the backslashes, otherwise if the s/// is interpreted as global we'd have a compe.g.) 02:59:54 alercah: They're like fascists too 03:00:13 alercah: the UK does if the stakes are sufficiently low 03:00:16 For severe crimes *now* in Japan, you are tried before 6 members of the lay population and 3 professional judges. 03:00:18 ais523: here too 03:00:27 ais523: but I think the entire system in e.g. Italy is judge-alone 03:00:30 since it's not adversarial 03:00:37 To be found guilty you need to be found guilty by a majority of the judges. 03:00:52 (also, Japan does not have an adversarial court system) 03:01:08 ais523: Ah, yes, of course judge-only is OK for REALLY minor things (e.g. parking tickets) 03:01:11 I think the reason behind adversarial is that it's hard to trust people to present the case in an unbiased way, so you ask two people to present it with opposite biases 03:01:28 That's the idea. 03:01:35 uh 03:01:41 I accidentally opened the clock in tmux 03:01:45 ais523: Yes, but then the moment there's a third way of looking at it... 03:01:49 how do I quit it? 03:01:58 "I'll be judge, I'll be jury," Said cunning old Fury: "I'll try the whole cause, and condemn you to death." 03:02:08 hppavilion[1]: here the right to a jury trial applies only when the maximum punishment is above 2 years 03:02:31 shachaf: is Fury a church? 03:02:40 shachaf: Yes, exactly 03:02:53 alercah: No, he's Samuel L. Jackson hth 03:02:54 alercah: Apparently Fury is a pooch. 03:02:57 I didn't know that. 03:12:15 Is this good: Zeux Agem's Evil Clone {BGR} Legendary Creature - Bat Wizard (1/1) ;; Flying, Protection from legendary, Bands with other legendary creatures ;; {6}, {T}: Destroy target permanent. ;; [["You eat with your left hand!" - Zeux Agem to his evil clone]] 03:12:35 `unidecode λ 03:12:36 [U+03BB GREEK SMALL LETTER LAMDA] 03:12:46 duhn... Duhn... DUHHHHN 03:16:12 ? 03:16:19 zzo38: I'm trying to work it out 03:16:37 my guess is that the lack of haste makes it nonviable in most formats 03:16:47 as it can't do anything the turn you play it, and has no protection against removal 03:17:15 also you need to play it alongside large legendary creatures, or have 6+ mana, to have any real benefit 03:17:25 You are correct about those things at least 03:17:30 that card is mega xuez 03:17:33 that said, the tap ability is very powerful if the game goes long 03:17:49 and it stays in play somehow 03:17:58 I just can't figure out what sort of decks you'd be able to pull that off /against/ 03:18:18 aggro decks will win first, and most other decks will have a bunch of spot removal or counterspells 03:18:34 (combo decks will win first, have spot removal, /and/ have counterspells) 03:18:40 I can change it of course if needed 03:18:46 -!- navet has joined. 03:18:47 (and don't care much about having their permanents destroyed or being attacked by a 1/1) 03:19:32 like, banding doesn't help much against a combo deck because they don't like to block anyway 03:19:35 Zeux Agem has the same converted mana cost (but different colors; should it be the same?), supertype, type, subtype, and converted mana cost as this card. 03:20:55 well, Evil Twin is UB colours 03:21:01 `card-by-name Evil Twin 03:21:02 Evil Twin \ 2UB \ Creature -- Shapeshifter \ 0/0 \ You may have Evil Twin enter the battlefield as a copy of any creature on the battlefield except it gains "{U}{B}, {T}: Destroy target creature with the same name as this creature." \ ISD-R 03:21:42 Ah. OK 03:22:15 I think banding is probably out of colour, it's nearly always white 03:22:27 Yes, that I believe 03:22:43 protection from legendary is blue under what the color pie rules are stated as (however, that rule was never actually used, because Wizards stopped using protection before they ever created such a card) 03:23:00 flying is normally blue but can also be white or black (or on very large creatures, red) 03:23:08 Maybe it should be the same {1WU} as the original I don't know? 03:23:09 destroying a permanent is BG or BW 03:23:32 although it's sometimes seen on colourless cards at a very high cost 03:28:11 Is 6 enough? 03:28:54 yes, but I've only seen that when the card itself is also colourless 03:29:04 not sure if you can do that on a coloured card or not 03:30:16 Are there British MTG cards that spell "color" with a u? 03:30:29 no 03:31:00 I don't really care about that, because I am not WotC. But changes could still be made to what I wrote if it would help to improve it, anyways. 03:31:45 So, your ideas can help anyways. 03:33:20 What is an operation supposed to be called if f(x);f(y) and f(x+y) are going to be the same operation? 03:33:31 What is ;? 03:33:37 flip (.)? 03:33:46 No, that doesn't make sense. 03:33:52 sequential composition, I guess? 03:33:53 No, it is like in C 03:33:56 right 03:34:15 It is an impure operation 03:34:25 zzo38: in this case, the argument to f is a repeat count, I think? I don't think it can be anything else 03:34:38 Well, you can make it pure by adding a state argument. 03:34:48 f(x, f(y, s)) = f(x+y, s) 03:34:53 So f is a monoid action or something. 03:34:54 shachaf: Yes, you can have that 03:34:57 right, because following these defintiions, f(3) = f(1); f(1); f(1) 03:36:16 ais523: But depending on the operation it might not require natural numbers; they may work with any nonnegative real numbers, with any real numbers, or with any complex numbers, even. And they might do more than just to increment a counter. 03:36:53 (For example, if f is a function that is supposed to be called to specify that a given amount of time has passed; the amount of time might not necessarily be an integer.) 03:37:01 Can f be self-modifying? 03:37:12 I guess that doesn't matter, given that it modifies arbitrary state anyway. 03:38:01 . o O ( is there a UB card that makes demons fly out of your nose? ) 03:38:31 Probably not; are you going to make a UB card with demons in your nose? 03:38:50 I like that idea I can add that to uncards.txt 03:40:23 yay 03:42:00 gah did i accidentally press end in the log window - now where was i... 03:42:37 Demons In Your Nose {UB} Instant ;; If there are any Demons in your nose, you may cast them. Each of those spells gains flying. 03:46:02 [wiki] [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=50069&oldid=50066 * Oerjan * (+52) Order, I said! Or was that another page... 03:46:11 apparently i was editing. 03:46:53 it's disappointing seeing so many people failing to follow the instructions 03:47:03 but we have to draw the line between humans and spambots somewhere 03:50:14 I now have a 4-letter word generator 03:50:58 ais523: Sometimes, a human is- for the purposes of the internet- basically a spambot 03:51:37 zzo38: I think the correct template is "Each of those cards gains flying as you cast it" 03:51:59 not 100% sure, though, you might need to say "spells" rather than "cards" 03:53:52 [wiki] [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=50070&oldid=50069 * Oerjan * (+6) This obviously needs bolding too 03:54:13 I have generated a list of every English 4-letter word of the form CVCC, CCVC, CVVC, CVCV, VCVC, or VCCV 03:54:33 someone just failed 5 times in a row at that particular point 03:54:55 Now to choose new curse words 03:55:02 And add some inflection & honorifics 03:56:03 ais523: eventually the whole instruction will be bold, and we can cycle back hth 03:56:26 I was wondering about that 03:56:45 actually I fear for the future of the Internet at the point when bots become better at CAPTCHAs than humans do 03:57:01 ais523: That's already happened, iirc 03:57:34 actually, I had a vision of a company that you can pay money for accounts on, then use those accounts to sign into other services, and it's up to you whether you connect them or not 03:57:55 the payment of money is used in lieu of a captcha, if someone's found to be spamming through an account than it can be cancelled 03:58:06 ais523: I'm pretty sure we have those, and they don't require money- oh, the money, I see 03:58:11 many large websites (e.g. google, yahoo) are using cellphone numbers for the same purpose 03:58:17 hppavilion[1]: it's when they become better than humans at following instructions we've got problems 03:58:24 oerjan: They already are hth 03:58:26 computers are already better than humans at following instructions 03:58:30 (clearly they already beat _some_ humans) 03:58:33 That's what computers do 03:58:35 however, humans are better than computers at /understanding/ instructions 03:58:42 OKAY 03:58:50 following them, however, is the entire purpose of a computer 03:58:56 computers can't /not/ follow instructions, it's what they're for 03:59:06 ais523: Yes, exactly. Computers are the best instruction-followers, humans are the best at figuring out what the instructions *are* (and in some cases, giving them to the computer) 03:59:21 ais523: The cell phones are annoying for me, because I don't have a cell phone 03:59:23 (and the normal way to attack/exclude a computer is to find a loophole in the instructions it was given) 03:59:27 Computers can not follow instructions, for example with hardware errors. 03:59:42 hppavilion[1]: I don't have a cellphone but my router does 03:59:52 shachaf: The difference in english (at least logically) between "can not" and "cannot" has always bugged me 03:59:56 Is there an esoteric language based on hardware errors? 04:00:05 I don't think so 04:00:06 I know about https://www.cs.princeton.edu/~appel/papers/memerr.pdf , which is pretty neat. 04:00:09 you should call it rowhammer 04:00:15 after the exploit 04:00:16 I feel like we should have "cant" as one word, rather than "can't" contracting "cannot" 04:00:32 I think it is a different word 04:00:34 "cant"'s already a word, but it means something else and is pronounced differently 04:00:56 They write a JVM program that gets compiled into code which is very likely to violate the sandbox constraints if a single bit is flipped. 04:01:13 Then they heat up the computer (which is supposed to be a secure computer of some sort) until a bit is flipped. 04:01:21 Or something like that, I don't remembe the details. 04:02:24 shachaf: So any bit, not just one particular bit? 04:03:39 they're aiming for one particular bit, I think 04:06:06 iirc it's one particular bit in an object, but they have _many_ of those objects. 04:06:19 to increase the probability. 04:07:39 making those bits as large a fraction of memory as possible. 04:08:27 also when i read about it it may only have worked at memories without error correction? 04:08:32 *with 04:08:44 *s/at/with/ 04:10:20 oerjan: Ah 04:10:43 -!- jeffl35 has changed nick to jeff-the-killer. 04:11:27 oerjan: But that leads to an issue where, assuming the rest of the object code is more than a bit long, it's much more likely for an important bit to be flipped than that important one, is it not? 04:11:34 oh we do have a halloween topic 04:11:38 I mean, it COULD be an error, especially on something Googly 04:11:42 oerjan: Yes. You're welcome. 04:12:53 hppavilion[1]: it is likely to just crash, indeed. i don't remember how clever they were about reducing that. 04:13:35 it may be that they actually could flip nearly any bit in that object. not sure. 04:13:53 shachaf: This sounds like a much less practical version of Rowhammer. 04:14:00 or wait 04:14:34 oerjan: It's probably that it just only needs to work once, and you run it on a million servers so that loln makes one work and then you win 04:14:58 * oerjan should look at that pdf instead of guessing 04:16:11 hppavilion[1]: hm the intro says the exploit has about 70% chance of working 04:16:31 oerjan: ¡Lies! 04:16:51 i mean the abstract 04:16:55 pikhq: Well, it's older. 04:17:50 Sure, and probably also a bit less hardware-specific. 04:18:24 Something tells me that sort of bit flipping trick more has to do with the properties of DRAM in general. 04:23:25 hppavilion[1]: it's in fact any bit of most of the objects, see page 2. the object fields are nearly all pointers, and as long as the changed pointer is anywhere within nearly any of them, they can exploit it. 04:24:42 Hm... S is a set where |ℕ| < |S| < |ℝ|. Provide either (a) an example of S or (b) a proof that S is impossible 04:24:47 oerjan: Wow. 04:24:58 oerjan: Ooooh, I see why 04:25:29 `unidecode ℕℝ 04:25:30 [U+2115 DOUBLE-STRUCK CAPITAL N] [U+211D DOUBLE-STRUCK CAPITAL R] 04:25:59 oerjan: Naturals and Reals; I couldn't do the standard |N and |R in this context because it wouldn't parse right 04:26:07 (either for a computer OR a human reader) 04:26:19 hppavilion[1]: https://en.wikipedia.org/wiki/Continuum_hypothesis hth 04:26:26 oerjan: Oh, rihgt 04:26:32 you could just write N and R like everyone else instead of trying to show off hth 04:26:45 shachaf: I wasn't trying to show off 04:26:52 am i being too nasty 04:26:54 shachaf: I tried to use Unicode for labels in my CALESYTA language 04:26:55 probably 04:26:59 -!- shachaf has left. 04:27:02 the interp handles it fine, unfortunately the editor doesn't 04:27:23 shachaf: double-struck N and R is nailed into my mind; using normal N and R just looks wrong, like they shouldn't be representing something so important 04:27:44 I think most of us read TeX here. 04:27:57 pikhq: Ah, yes, that works too 04:28:19 oerjan: Huh, I seem to have remembered that being that cardc = Aleph_1, which is COMPLETELY different 04:28:38 (...they're equivalent in some bizarre way, aren't they?) 04:28:54 What. N and similar set symbols aren't in normal TeX. 04:29:06 pikhq: Yeah, because Knuth is a dick 04:29:09 amsfonts fixes it, at least. 04:29:20 $\mathbb{N}$ 04:29:25 pikhq: Yes, but only for N, Z, R, and maybe Q iirc 04:29:26 (gag) 04:29:40 PWNZIQRC. 04:29:51 pikhq: I forget, what's W? 04:29:52 $\left\|\mathbb{N}\right\|$ 04:30:34 pikhq: I usually just type \bb{string} to indicate what it is without actually making a whole system 04:30:35 hppavilion[1]: Uh, $\mathbb{N}_{>0}$ 04:30:58 pikhq: ...really? we use- oh, right, "whole" 04:31:03 hppavilion[1]: aleph-1 = 2 to the power of the number of integers, by definition; it's also very easy to prove it's equal to the number of reals 04:31:18 pikhq: "But N doesn't contain 0 anyway" :P 04:31:40 (err, this is to what extent "=" is defined on infinities) 04:31:47 (it does. I was trying to explain countable vs. uncountable infinity to an 11 year old earlier today, and that came up. Somehow) 04:32:30 Really, I feel like blackboard bold shouldn't be in unicode, it should just be a font (within a typeface) 04:33:06 So I can have a blackboard bold ſ (long s) or ð (eth) or @ (at sign) >:D. 04:34:32 ais523: you recall incorrectly, what you are describing is beth-1. 04:34:50 (or possibly you read from a wrong source, i believe those exist) 04:34:57 oerjan: I thought that beth-1 was the second-smallest infinity 04:35:04 no. the other way around. 04:35:07 it is possible that I was taught backwards 04:35:08 Apparently the rationale was to permit maintaining symbol distinctions in mathematic notation in plain text. 04:35:42 i.e. it was viewed that the symbol variants here were *semantic*, not just style variants. 04:36:01 So we've got the opposite of CJK unification because of the same rules. 04:36:05 ais523: well after that thing i read in the logs it's good to get out of my "don't be stupid, ais523 is always right" vibe ;) 04:37:26 yes, being educated when I'm wrong is helpful 04:38:27 hm although i'm wondering if they're still equivalent with AoC. it might be that there could be no cardinality strictly between |N| and |R|, without the latter being aleph-1 because R isn't well-orderable. 04:38:52 Wikipedia says that many textbooks assume the continuum hypothesis 04:38:55 (aleph-1 is the second-smallest infinite _well-orderable_ cardinal, by definition) 04:39:10 in which case aleph-1 and beth-1 are interchangeable; that'd explain the amount of misinformation going around 04:39:43 some might even assume the generalized CH, in which case all alephs are beths 04:41:17 > cos 208341 04:41:18 hppavilion[1]: anyway, if you have AoC, then every infinite cardinality is an aleph, and alephs are always well ordered so aleph-1 is the next after aleph-0=|N| 04:41:20 -0.9999999999670789 04:41:20 04:41:25 -!- augur has quit (Remote host closed the connection). 04:42:15 and therefore there is nothing between aleph-0 and aleph-1, but something between aleph-0 and anything larger than aleph-1. 04:42:32 pikhq: I've also considered writing |N as NN or \NN, |R as RR or \RR, etc. 04:43:05 Also interesting, apparently 2^|N has the same cardinality as |R, so there's a weird bijection here somewhere that I must find 04:43:16 oerjan: does the axiom of choice imply that infinities are well-ordered? I'm guessing not 04:43:40 hmm, it wouldn't surprise me if there were at least countably infinitely many well-ordered infinities before they started becoming badly odered 04:43:43 *ordered 04:48:06 > cos 208341 <-- * briefly wonders if that's somehow a clue to ais523's hello world program 04:48:16 ais523: If you have too many well-ordered infinities in one place, it starts to smell bad hth 04:48:19 nah, I was reading random PPCG pages again 04:48:44 it was intended for a programming language in which "cos" was implemented as a single byte 04:49:00 the point being that deleting any byte makes the output longer than "-1" 04:49:18 ais523: yes it does imply that. AoC ~ "every set can be well ordered". 04:49:48