00:01:00 Since we're only considering finite limit theories, every theory also has a "free model", which is the initial object of Mod(T). 00:07:42 Now, given any arrow T -> U, we're essentially saying every axiom in T can also be found in U, which means that every model of U will also work as a model of T... 00:08:14 In other words, arrows T -> U produce functors Mod(U) -> Mod(T). 00:20:03 So lemme consider an example! 00:20:35 Let G be the theory of groups, and let PG be the theory of pointed groups (groups with a distinguished element). 00:21:01 There's an arrow G -> PG (everything that can be done within a group can be done within a pointed group). 00:21:17 And the resulting functor Mod(PG) -> Mod(G) (every pointed group is a group). 00:21:49 All these model categories have "initial objects" or "trivial models". There is a trivial group, and there is a trivial pointed group. 00:21:55 The trivial pointed group is also a group, of course. 00:22:02 But it's not the trivial group; it's the infinite cyclic group. 00:24:39 -!- Phantom_Hoover has quit (Read error: Connection reset by peer). 00:28:45 Now, I (essentially) said earlier that not only is there a functor Mod(PG) -> Mod(G), but Mod(PG) is actually a coslice category of Mod(G). 00:29:17 Not all theory extensions have that property. 00:29:50 For example, if AbG is the theory of abelian groups, then we have the inclusion arrow G -> AbG, which generates the "forgetful" functor Mod(AbG) -> Mod(G). 00:30:19 But that's not a coslice category, because the trivial abelian group is the trivial group. 00:30:28 So... 00:31:17 A pointed group is just a group equipped with a homomorphism out of the trivial pointed group. 00:31:33 It is *not* the case that an abelian group is just a group equipped with a homomorphism out of the trivial abelian group. 00:34:18 Oooooooh. I get it. 00:34:27 I get why certain axioms are allowed in a presentation, and certain ones are not. 00:35:06 How come a group presentation is allowed to contain the axiom "there exists an element a with a^2 = e", but it is not allowed to contain the axiom "for all elements a and b, ab = ba"? 00:35:23 Only the first axiom is preserved by homomorphisms. 00:50:14 -!- oerjan has joined. 00:50:22 I suspect because the latter doesn't provide a real quotient group 00:52:33 What do you mean, doesn't provide a real quotient group? 00:53:36 A presentation defines a group by quotient on the free group in however many generators 00:53:52 Right. 00:54:16 so in order for an equation to be allowed, you have to be able to meaningfully turn it into a normal subgroup to quotient by 00:54:29 Yup. 00:54:41 The thing about the axiom "for all elements a and b, ab = ba" is that it's sensitive to what the elements are. 00:54:54 but what subgroup is that even defining? 00:55:07 Umm, good question. 00:55:29 Is it the... subgroup of all commutators? 00:55:57 ATWP: "The commutator subgroup is important because it is the smallest normal subgroup such that the quotient group of the original group by this subgroup is abelian." 00:56:29 ? atwp 00:56:30 According to Wikipedia, ATWP means nothing. 00:56:47 le/rn atwp/According to Wikipedia, ATWP means "Air Transport White Paper". 00:56:48 Usage: le/[/]rn // 00:56:56 le/rn atwp//According to Wikipedia, ATWP means "Air Transport White Paper". 00:56:58 Relearned 'atwp': According to Wikipedia, ATWP means "Air Transport White Paper". 00:57:42 tswett: huh so I checked, ab = ba is allowed 00:57:58 on two generators it generates Z \times Z 00:58:14 that makes sense, ab = ba ~ a^-1b^-1ab 00:58:18 * = 1 00:58:29 so not quite sure why I let you trick me into thinking it wasn't 00:58:40 oh wait, "for all elements" 00:58:55 uh let me think if I can come up with a good explanation 01:00:12 I can't think of a trivial one, but if you look up the definition, it doesn't make sense 01:00:23 The definition of "presentation of a group"? 01:01:07 yeah 01:01:19 you can have an infinite set of equations 01:01:27 Right. 01:01:27 so you can just include every equation of the form xy = yx 01:01:39 Yup. 01:02:03 But the definition of a group presentation doesn't allow you to do anything with universal quantifiers. 01:05:43 Now here's the next big thing I'm wondering. 01:05:59 Consider the concept of a category. 01:06:18 What would you have to add to it, piece by piece, in order to bring it up to being equivalent to second-order logic? 01:06:35 If you add a terminal object, now you have the equivalent of a "true" proposition. 01:06:44 Add products, now you've got conjunction, too. 01:07:09 Add an initial object and coproducts, that's "false" and disjunction. 01:07:36 Make it cartesian closed, and now you've got implication. 01:07:46 it allows an infinite set of words though 01:07:59 so you can just use quantifiers to build the set 01:08:10 Right. 01:08:24 Or, if you want to just write a presentation of some specific abelian group, it suffices to just say all the generators commute with each other. 01:09:23 yeah 01:10:46 So lemme seeeeeee. 01:11:36 A cartesian closed category with finite sums is enough for propositional logic. 01:12:17 What if I want predicate logic? 01:12:58 If you want to do propositional logic in a category, you're probably seeing the objects as propositions. 01:13:45 For predicate logic, now you need to look at objects as propositions *and* as domains that can be quantified over. 01:14:18 And then a predicate is a morphism from a "domain" to a "proposition". 01:17:05 No, that's not right. 01:17:10 A predicate is a morphism *into* a domain. 01:18:03 Now, in predicate logic, you can do conjunction, disjunction, and implication between predicates, not just propositions. 01:19:47 This means the category needs to have sums, products, and exponentials for morphisms, not just objects. 01:23:45 For the initial object and coproducts, this is automatic. 01:24:32 To have a cat satisfying an impossible property is impossible. To have a blue-or-green cat is to either have a blue cat or have a green cat. 01:24:58 To have a cat satisfying a trivial property is not trivial; you must actually have a cat. 01:25:17 And to have a blue-and-green cat is not to both have a blue cat and have a green cat; they must be the same cat. 01:27:24 Anyway, this ends up meaning that for predicate, you need a *locally* cartesian closed category with finite sums. 01:28:32 And, um, does quantification automatically end up working? 01:34:33 is this the curry-howard-lambek correspondence of system F 01:35:26 Ummmmm, might be? 01:35:32 I'm referencing this: https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory 01:40:39 So lemme see. There's this idea where a predicate is "encoded" as three things: its "total space" (a proposition which is considered equivalent to "exists x, P(x)"), its domain, and the proof of the implication from the former to the latter. 01:41:07 * oerjan sidles away carefully 01:41:12 So the predicate "the integer x is even" is encoded as... 01:41:36 1. a proposition considered equivalent to "exists x, x is even"--in other words, the set of even integers 01:41:42 2. the domain, which is the set of integers 01:41:53 3. the inclusion function from the set of even integers to the set of integers 01:41:57 hellørjan! sidling toward me? :D 01:42:07 Yeeeeeeeeeeah. 01:42:15 Don't mind me, I'm just using this channel as my personal notepad. 01:42:31 It's great because my notepad automatically contains funny things other people say. 01:44:23 boheily! anywhere nowhere near a category vortex twh 01:44:53 categories are nice. I don't understand them, but they make nice graphs ^^ 01:44:56 So, sums are easy. How do you write "exists x, P(x) or Q(x)" in terms of "exists x, P(x)" and "exists x, Q(x)"? 01:44:58 It's just... 01:45:09 "(exists x, P(x)) or (exists x, Q(x))". 01:45:18 Likewise, "exists x, false" is just "false". 01:46:08 "exists x, P(x) and Q(x)" is the pullback of "exists x, P(x)" and "exists x, Q(x)". 01:46:17 tswellott. probably some manipulations involving sums-of-products or products-of-sums. 01:46:43 tswett: i really don't think you want "exists x," in there 01:47:00 Note that I'm using "exists" to mean "dependent sum"... 01:47:24 tswelliott would be an odd individual 01:47:28 O KAY 01:47:43 So "there exists a 0-tuple" isn't equivalent to "there exists an integer", since the latter has infinitely many proofs and the former only has one. 01:48:01 AAAAAAA 01:48:13 You seem upset about this. 01:48:13 * oerjan cuddles a five lemma 01:48:15 AAAAAAA? 01:49:33 five lemma?! 01:49:47 "The five lemma can be thought of as a combination of two other theorems, the four lemmas, which are dual to each other." 01:49:57 shachaf: that's about as much category theory as i understand. 01:50:04 without glazing over. 01:50:20 at least i used to. 01:51:13 So what the heck is "exists x, P(x) -> Q(x)" in terms of "exists x, P(x)" and "exists x, Q(x)"... 01:51:44 I'm going to skip that one. 01:52:35 Let's just go straight to the fun part. 01:52:43 [wiki] [[Ly]] https://esolangs.org/w/index.php?diff=52475&oldid=52465 * LyricLy * (+2521) 01:52:43 What's "exists x, forall y, P(x,y)"? 01:52:43 Well, start with what is exists x. not(P(x)) in terms of exists x. P(x) 01:52:43 ? fun fact 01:52:44 fun fact 0 = 1 | fact n = n * fact (n - 1) 01:53:00 I love the fun fact. 01:54:32 Of course exists x. not(P(x)) is not(forall x. P(x)) 01:54:38 i had a near-pun experience after posting that on agora and someone responded they preferred fact x = foldl (*) 1 [1..x] 01:55:14 unfortunately, the obvious response did not appear to me until after i'd made a worse one. 01:55:19 *occur 01:55:22 What's the obvious response? 01:55:30 "Where's the fun in that?" 01:56:02 But now you get your revenge. 01:56:21 ? diagram chasing 01:56:22 diagram chasing? ¯°​_o)/¯ 01:56:23 well i don't think they're on this channel. 01:57:08 le/rn diagram chasing//Diagram chasing is a technique used to prove integer lemmas. Taneb invented it. 01:57:10 Learned 'diagram chasing': Diagram chasing is a technique used to prove integer lemmas. Taneb invented it. 01:58:23 grWp chasing 01:58:24 diagram chasing:Diagram chasing is a technique used to prove integer lemmas. Taneb invented it. 01:58:33 grWp chase 01:58:34 abstract nonsense:We would have an explanation of abstract nonsense here, but it fled into a diagram and we haven't been able to chase it. We will try again once we find an abstract machete. \ scotland: it's that place where they all wear kilts and chase haggises around whilst warding off the loch ness monster with bagpipes \ wumpus 01:58:49 2 grWp chase 01:58:50 2/2:mpus:Wumpus the Hunted is an early 70s action game in which the Wumpus is trapped in a dodecahedral labyrinth where it's chased by bats. It has to avoid traps and evade magical arrows that are guided by a nefarious AI. 01:59:06 cwlprits wumpus 01:59:12 oerjän 02:00:18 dowg wumpus 02:00:22 -!- MDude has joined. 02:00:25 8060:2016-05-14  mv wisdom/wumpu{,s} 02:00:28 I'm just gonna say... 02:00:29 Ah, right. 02:00:29 thought so 02:00:33 dowg wumpu 02:00:41 8060:2016-05-14  mv wisdom/wumpu{,s} \ 8059:2016-05-14 learn Wumpus the Hunted is an early 70s action game in which the Wumpus is trapped in a dodecahedral labyrinth where it\'s chased by bats. It has to avoid traps and evade magical arrows that are guided by a nefarious AI. 02:00:52 Apparently the two four lemmas put together make the five lemma. And these people call themselves mathematicians. 02:00:56 I'm pretty sure that a locally cartesian closed category with finite sums is enough for predicate logic. 02:01:13 slwd wumpus//s,labyrinth,diagram, 02:01:15 wumpus//Wumpus the Hunted is an early 70s action game in which the Wumpus is trapped in a dodecahedral diagram where it's chased by bats. It has to avoid traps and evade magical arrows that are guided by a nefarious AI. 02:01:32 Well, yeah. Four plus four plus paths from three of the four to three of the other four equals five. 02:01:45 i guess that's a categorical improvement. 02:13:54 @metar ENVA 02:13:54 ENVA 200050Z 13007KT CAVOK 07/06 Q1018 RMK WIND 670FT 12008KT 02:18:47 -!- ais523 has joined. 02:22:46 -!- ais523 has quit (Remote host closed the connection). 02:22:55 -!- ais523 has joined. 02:22:58 unidecode éêè 02:22:59 ​[U+00E9 LATIN SMALL LETTER E WITH ACUTE] [U+00EA LATIN SMALL LETTER E WITH CIRCUMFLEX] [U+00E8 LATIN SMALL LETTER E WITH GRAVE] 02:54:44 -!- boily has quit (Quit: FUNK CHICKEN). 02:57:41 5 w 02:57:45 1/1:dynamic-unwind//dynamic-unwind is just like dynamic-wind except that it's a different sort of weather. \ ⊥//⊥ is a bottom tack, useful for annoying teachers. \ cafreine//Cafreine is the favorite drug of category theorists. \ yeeesh//See yeesh. \ 6 random numbers//4 8 15 16 23 42 02:58:07 dow cafreine 02:58:08 ​/home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: dow: not found 02:58:13 dowg cafreine 02:58:20 8775:2016-07-10 learn Cafreine is the favorite drug of category theorists. 02:58:22 dowg 6 random numbers 02:58:28 8061:2016-05-15  echo 4 8 15 16 23 42 > "wisdom/6 random numbers" 03:05:58 how could we make the wisdom database Turing-complete? 03:19:45 I've often wondered about using some sort of language for wisdom entries, rather than just plaintext. 03:19:58 For example to allow referencing/including other wisdom entries, and other things. 03:20:12 (Maybe it can allow running arbitrary commands, to implement ? ngevd) 03:23:07 That's kind of boring, though. 03:23:30 fizzie: Can you patch up HackEgo to get access to the nick of the user running the command? 03:23:36 That would twh. 03:24:06 -!- Warriga_l has joined. 03:36:14 i would play wumpus the hunted. it sounds fire 03:45:32 That sentence reminded me that I heard a song once that seemed to contain the words "they went fire". 03:45:42 So I did a Google search for "they went fire" and was surprised to actually find the song. 03:45:54 https://www.youtube.com/watch?v=CSPker14VVY - "Clash", Caravan Palace. 03:53:31 -!- hppavilion[1] has joined. 03:57:43 Dang, I feel like there was something I wanted to do. 03:57:57 Something about math. 03:58:02 -!- Warriga_l has changed nick to tswet_t. 03:58:41 -!- hppavilion[1] has quit (Ping timeout: 248 seconds). 04:42:55 -!- oerjan has quit (Quit: Nite). 05:18:17 -!- tswett has quit (Read error: Connection reset by peer). 05:18:42 -!- tswett has joined. 05:19:36 -!- doesthiswork has joined. 05:48:33 -!- idris-bot has quit (Quit: Terminated). 05:50:18 -!- Melvar has quit (Quit: thunderstorm). 06:08:41 -!- doesthiswork has quit (Quit: Leaving.). 06:20:32 -!- erkin has joined. 06:24:34 -!- Melvar has joined. 06:50:31 -!- augur has quit (Remote host closed the connection). 06:51:23 -!- augur has joined. 06:55:48 -!- augur has quit (Ping timeout: 260 seconds). 07:01:18 -!- FreeFull has quit. 07:15:46 -!- hppavilion[1] has joined. 07:16:51 -!- augur has joined. 07:21:05 -!- augur has quit (Ping timeout: 240 seconds). 07:24:11 -!- ais523 has quit. 07:52:20 -!- erkin has quit (Quit: Ouch! Got SIGABRT, dying...). 08:02:41 -!- imode has quit (Ping timeout: 255 seconds). 08:22:47 -!- tswett has quit (Read error: Connection reset by peer). 08:23:12 -!- tswett has joined. 08:53:08 -!- AnotherTest has joined. 08:57:37 -!- erkin has joined. 09:07:36 Hm x86 and x86-64 has variable length instructions. This presumably means that the suffix of one instruction could be another valid instruction. 09:08:01 I wonder if you construct any useful programs where you jump into the middle of another instruction to execute different code 09:08:25 possibly the suffix of one instruction and part or all of the next instruction could form a valid instruction as well 09:12:35 What do you count as a useful program? 09:12:57 This sort of thing is often used to write various exploits. 09:13:04 Oh, interesting 09:13:13 so it can be used for non-trivial purposes then 09:13:15 I think I've also seen it in other contexts but I can't remember where. 09:13:52 Apparently it's also used for obfuscation. I don't consider that useful. 09:13:54 I imagine it might have been useful back in the day when the computers had much more limited memory, say 286 or older 09:14:40 There are probably some golfing situations where it's useful, but I doubt there are that many? 09:14:50 I bet it can come up a lot when looking for ROP gadgets. 09:15:01 And https://en.wikipedia.org/wiki/JIT_spraying 09:16:00 That page says you can jump into the middle of an instruction on ARM. That's interesting because I thought ARM had a fixed-length encoding. Do they not require instructions to be aligned? 09:16:11 Then again ARM has multiple different encodings. 09:17:14 I was just about to comment on that 09:17:46 iirc on arm, if LSB is set in the target address of a jump, then it switches to thumb mode 09:17:53 so maybe that is what they mean? 09:19:38 ROP is too good 09:20:21 https://blogs.msdn.microsoft.com/oldnewthing/20090128-00/?p=19353/ talks about using this for golf 09:23:09 interesting 09:24:32 Man, this generated password is annoying. It's perfectly interleaved between characters that need shift pressed and characters that don't. 09:24:58 shachaf: I use a password manager with auto-typing for such passwords 09:25:20 C++11 has auto-typing too. 09:25:30 not that sort of auto-typing 09:25:47 also the C++11 one is rudimentary compared to something like haskell for example 09:26:11 I know, I learned Haskell before I learned C++11. 09:26:23 heh 09:27:01 shachaf: though I guess guessing template parameters may be closer 09:29:43 Anyway, it's silly to generate a password of a fixed length for typing and not consider shift a keypress. 09:29:59 Really I should generate all my passwords to be of the for /[a-z]{n}/ 09:30:02 form 09:30:43 Permitting uppercase letters adds only one bit of entropy per character, and is much harder to remember. 09:30:52 > logBase 2 (26^15) 09:30:54 70.50659577211638 09:30:58 > logBase 2 (52^15) 09:31:01 85.50659577211638 09:31:03 no surprise 09:31:19 > logBase 2 (26^18) 09:31:21 84.60791492653966 09:31:36 So you could permit uppercase letters, or you could add 3-4 more lowercase letters. 09:33:11 > map (logBase 2) [64^15, 26^19] 09:33:13 [90.0,89.30835464468075] 10:10:57 unfortunately it's not up to you whether to use uppercase letters, but up to the login provider 10:11:36 I can always add an uppercase letter, a digit, and a "special character" to satisfy the login provider. 10:11:45 What are special characters? 10:11:57 unidecode ㈵ 10:11:58 ​[U+3235 PARENTHESIZED IDEOGRAPH SPECIAL] 10:12:03 unidecode ㊕ 10:12:04 ​[U+3295 CIRCLED IDEOGRAPH SPECIAL] 10:12:08 I guess I should use more of those. 10:21:11 apparently on cortex-m chips, the only available encoding is a mix of 16-bit and 32-bit instructions 10:23:08 -!- hppavilion[1] has quit (Ping timeout: 260 seconds). 10:24:14 “According to the Japanese, the index finger is connected to the urinary bladder and the kidney. However, in other cultures the index finger is thought to be connected to the hand.” 10:25:21 That is a clever vandalism. 10:48:40 unicode 特 10:48:45 U+7279 CJK UNIFIED IDEOGRAPH-7279 \ UTF-8: e7 89 b9 UTF-16BE: 7279 Decimal: 特 \ 特 (特) \ Uppercase: U+7279 \ Category: Lo (Letter, Other) \ Bidi: L (Left-to-Right) 10:50:31 shachaf: There are some ARMs (around the ARMv4, ARMv5 generations) where an unaligned word read actually returns the word rotated, i.e., if the memory contents are |00 01 02 03|04 05 06 07| and you read a word at offset 2, you get back the bytes 02 03 00 01. (Approximately so, anyway.) 10:50:36 I don't know if you could use that for instruction reads. 10:51:15 shachaf: I think you mentioned the nick thing before, and I was going to do it, but then forgot. Will try to remember at some point. 11:00:01 whoa whoa whoa 11:23:13 oerjan: do you understand goodwillie functor calculus twh 11:36:31 -!- boily has joined. 11:43:06 -!- Slereah has joined. 11:43:16 -!- Slereah__ has quit (Ping timeout: 255 seconds). 11:44:25 -!- joast has quit (Ping timeout: 246 seconds). 11:50:02 -!- Slereah__ has joined. 11:51:40 -!- Slereah has quit (Ping timeout: 260 seconds). 11:56:13 Arachne, Asterion, Jorgrun, a misplaced balrog, a bunch o' spiders and a few electric eels for decoration. 11:56:19 what the fungot is going on... 11:56:19 boily: hey my name is christie)) disabled or handicapped so i started collecting things with angels um yeah that's probably it)) 11:56:29 fungot: no, you're Sir Fungellot. 11:56:29 boily: i never believed it i thought once you were tried for like murder and you couldn't be tried again 12:11:29 fungot: but have you ever been tried for murder? also I rather suspect that you could be tried for a different murder in any case, as long as you're still alive. 12:11:29 int-e: the idea i think that they 12:12:45 -!- erkin has quit (Read error: Connection reset by peer). 12:30:42 -!- boily has quit (Quit: NEARBY CHICKEN). 12:35:52 -!- AnotherTest has quit (Ping timeout: 246 seconds). 12:41:04 -!- AnotherTest has joined. 12:58:59 -!- Slereah has joined. 13:00:35 -!- Slereah__ has quit (Ping timeout: 240 seconds). 13:03:25 -!- deltab_ has joined. 13:04:27 -!- deltab_ has quit (Client Quit). 13:12:11 -!- erkin has joined. 13:12:14 -!- idris-bot has joined. 13:15:53 -!- Cale has quit (Quit: Leaving). 13:16:10 -!- Cale has joined. 14:00:30 -!- doesthiswork has joined. 14:28:56 <\a\a\a> https://ghostbin.com/paste/azx76 is it theoretically possible to prove a program using this can end with n being any (positive, real) number 14:43:36 what does n.to_s.to_i(8) do with 119? Does it result in 11o = 9? 14:44:27 irb 14:44:28 ​/home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: irb: not found 14:45:56 (yes it does) 14:47:27 -!- Slereah has quit (Ping timeout: 240 seconds). 14:48:15 So I expect you can get all natural numbers without too much trouble, using just the reinterpretations as hex and octal. But I have no proof nor time to attempt one. (Intuitively, iterating the reinterpretation as hex will produce a pseudo-random string of initial digits, so to produce n, just wait until the number starts with n in octal, followed by 8 or 9) 14:49:20 -!- Slereah has joined. 14:51:58 (and getting big numbers this way may turn out to be highly impractical) 14:53:37 <\a\a\a> yeah, i just intended for it to be hard to actually work with numbers but still possible to do 14:56:18 -!- ^_^v has joined. 15:05:42 -!- doesthiswork has quit (Quit: Leaving.). 15:35:12 -!- Slereah has quit (Ping timeout: 260 seconds). 15:35:55 -!- Slereah has joined. 15:36:15 note that ⁹ is equivalent to ܋ᾗᾚᾗῃᾗᾗ 15:37:02 also note that this paste site doesn't actually support copying code 15:37:22 <\a\a\a> yeah this took a while to put together so i slowly realized things i could do over the course of writing it 15:38:22 <\a\a\a> that's why you have both ⁹܋ᾚᾚᾚᾚᾚᾗ܋ and ⁹ᾗ܋ 15:38:33 . o O ( can we have an ASCII version of this? ) 15:39:14 <\a\a\a> i like having it be unrelated, weird unicode characters. it makes the code look interesting 15:39:26 <\a\a\a> but it also does confuse geany so uh, hold on 15:41:05 say: 6 (from 16) 8 (from 8) 7 (less than 8) 5 (String) 2 (Zeichen) 1 (change by 1) 9 (9) 15:41:30 ("Zeichen" means "character" in German :P) 15:41:39 also "sign" 15:43:24 <\a\a\a> here's an ascii version https://paste.ee/p/hupOT 15:46:01 -!- erkin has quit (Quit: Ouch! Got SIGABRT, dying...). 16:06:24 Apparently getting 14063 using H and n, starting from 10, is fairly hard. 16:06:53 (10 is the result of 9T, the first number where H has a useful effect) 16:10:37 TnnHHHnHHHnHHHnHHHnTHnT seems no harder than other numbers of the same size 16:11:06 I'm not using T 16:11:24 (after reaching 10 first one) 16:14:14 I'm also not actually searching for 14063 specifically; I'm enumerating numbers, and 14063 is the smallest one missing at this time. 16:24:14 and indeed adding T helps it get past this point easily. 16:29:26 -!- Slereah__ has joined. 16:30:09 -!- Slereah has quit (Ping timeout: 248 seconds). 16:34:38 -!- augur has joined. 16:37:23 -!- contrapumpkin has joined. 16:40:26 well, the question of whether 9TH*n is enough is probably a hard number theory problem 16:57:12 Hey yo. 16:58:36 Is there a 2-player board game with reasonably simple rules, such that one player always has a winning strategy, and such that any statement about the integers can be transformed into a board position, such that the first player has a winning strategy if and only if the statement is true? 16:59:54 Inb4 "yeah, there's no board, no pieces, and no moves; the win condition is to be the first player if and only if the statement is true." 17:03:18 2-player peanos? https://www.youtube.com/watch?v=MzxZ8qtdun0 17:06:58 Jafet: I'm doing 9T[Hn]* ... H* is likely to be terribly slow 17:07:01 > 8^6 17:07:04 262144 17:07:15 > 8^5 17:07:18 32768 17:07:21 olist 1084 17:07:21 olist 1084: shachaf oerjan Sgeo FireFly boily nortti b_jonas 17:07:40 err, H*n 17:09:14 (and yay, I made my laptop unusable, had to reboot) 17:11:57 > 10^length "14063" * 10 div length "89" 17:12:00 500000 17:12:58 I guess you could have a "board game" where the players take turns assigning specific numbers to all the quantifiers. 17:13:12 > let n = 500000 in n * (log n + 0.57) 17:13:14 6846181.688702164 17:15:42 (it should really be length "33357", which is the precursor to 14063) 17:16:09 tswett: does that work for all quantifiers? (namely, forall quantifiers?) 17:17:03 If all the quantifiers are at the very front of the statement, then player 1 picks the values for the existential quantifiers and player 2 picks the values for the universal quantifiers. 17:18:19 -!- AnotherTest has quit (Ping timeout: 246 seconds). 17:18:55 Jafet: what does your [HTn]* program say for 36105? 17:21:08 (hah, 8m30s into the enumeration it found a solution for that one... well, it doesn't actually record the solutions) 17:22:10 -!- FreeFull has joined. 17:22:10 (37587 is the next one) 17:24:55 See y'all later. Hth. 17:24:59 -!- tswett has quit (Quit: Leaving). 17:25:22 hate the hater ... not the hate 17:27:03 therefore do not hate 17:27:25 ? hth 17:27:26 hth ([ʰtʰh̩]) is help received from a hairy toe. It is not at all hambiguitous. 17:27:38 hug the hater 17:27:46 hassle the hassler 17:28:06 I can't seem to get past 6995 for [Hn]*, probably because this program is limited to 64-bit numbers 17:32:24 http://lpaste.net/5694671569826086912 is what I've produced... throwaway code quality :P 17:34:38 and it's gobbling up tons of memory too 17:34:57 hm, prenex normal form (all quantifiers at the front) in fact exists for first-order arithmetic 18:02:59 -!- imode has joined. 18:04:52 -!- augur has quit (Remote host closed the connection). 18:13:00 well, the 9T[Hn]* search finished without even getting to 6995 18:14:57 it found 3287481 numbers reachable without overflow, and then spun on an empty queue for half an hour 18:18:34 > 2^64 div 3287481 18:18:36 :1:11: error: parse error on input ‘3287481’ 18:18:40 > 2^64 div 3287481 18:18:43 5611209334353 18:26:38 -!- sebbu has quit (Read error: Connection reset by peer). 18:28:07 what'cha doin', Jafet. 18:30:58 wasting time on the language given by https://paste.ee/p/hupOT 18:31:19 "written by trial and error". hah. 18:31:24 I'm not sure why this is worth the time. it's not even on the esowiki 18:31:47 why not spend the time? 18:32:16 if it's fun, why not? :P 18:33:10 well, it's almost certain that every number is reachable by those operations and it is equally almost certain that trying to prove this will be futile 18:34:13 it's mildly surprising that so few numbers are reachable with a 64-bit state, though 18:47:13 -!- augur has joined. 18:53:19 -!- LKoen has joined. 18:57:40 -!- sebbu has joined. 19:09:37 -!- sebbu2 has joined. 19:10:07 -!- sebbu has quit (Ping timeout: 255 seconds). 19:21:29 -!- sebbu has joined. 19:22:18 -!- sebbu2 has quit (Ping timeout: 255 seconds). 19:28:32 -!- sleffy has joined. 19:44:47 -!- sebbu2 has joined. 19:46:21 -!- sebbu3 has joined. 19:46:43 -!- sebbu has quit (Ping timeout: 246 seconds). 19:49:16 -!- sebbu2 has quit (Ping timeout: 255 seconds). 19:50:59 -!- sebbu3 has quit (Ping timeout: 255 seconds). 19:58:06 -!- sebbu has joined. 20:03:44 [wiki] [[Special:Log/newusers]] create * Totallyhuman * New user account 20:11:12 [wiki] [[Special:Log/newusers]] create * Stevoisiak * New user account 20:17:47 -!- wob_jonas has joined. 20:17:50 <\oren\> http://www.tmz.com/2017/07/20/linkin-park-singer-chester-bennington-dead-commits-suicide/ 20:18:02 Hi guys. Can I ask stupid off-topic questions? 20:19:18 -!- LKoen has quit (Remote host closed the connection). 20:20:29 I just installed a new carbon-monoxide alarm. The old alarm is of type Honeywell SF-450-EN, and is at its end of lifetime. How do I turn off (shut down) the old alarm before I dispose of it as used electrics? 20:20:54 If someone happens to know the proper way, that would make my life simpler. If not, I'll call their customer service number tomorrow and ask them. 20:21:18 <\oren\> take batteries out I assume? 20:21:29 (The new alarm is of a different model, and I know how to turn that one of, but that knowledge is of no use to me.) 20:21:58 I have some sort of batteryless alarm that has a thing in the back you can poke to permanently turn it off. 20:22:56 shachaf: hmm, that might be under this X mark on the back 20:24:08 I don't understand why the manual for that device doesn't tell how this works. I've downloaded an English language manual, and it doesn't say anything. 20:25:33 "When the unit has come to the end of its life, dispose of it inaccordance with local regulations." 20:26:20 shachaf: right. that tells me I have to dispose it as electric waste, not together with household waste. I know how to do that. 20:26:26 But that's after I turn if off. 20:26:34 Maybe the local regulations tell you how to turn it off. 20:27:04 Hmm. 20:28:09 https://www.youtube.com/watch?v=ED31RlJASZE outlines one method. 20:28:40 shachaf: isn't that a different brand? 20:28:52 It's a different model but I suspet it can be adapted pretty easily. 20:38:19 -!- Stevoisiak has joined. 20:40:21 Hello. I just created an account on Esolangs and have already managed to lock myself out. Is there a way to reset my password? 20:41:56 Stevoisiak: someone in here might be able to help, but if you only created the account now, it might be simpler to create another account 20:42:21 wob_jonas: I created it using my primary username and email, Stevoisiak 20:42:31 I'd like to keep that username if possible 20:44:49 fizzie: who can help in that? 20:45:20 Stevoisiak: one thing you might want to try is to remove cookies then login only on the http interface or only on the https interface, sometimes one of those don't work 20:45:42 I don't recall the details of which one works 20:46:35 Stevoisiak: also try the automatic password reset form which sends you an email http://esolangs.org/wiki/Special:PasswordReset , I'm not sure if that works for this wiki but it's worth a try 20:47:03 @wob_jonas: I'm still waiting on my initial confirmation email 20:47:03 Unknown command, try @list 20:47:38 wob_jonas: I'm still waiting on my initial confrimation email 20:48:15 Also, I'm currently logged into the account. I just don't know what the password is. (LastPass didn't save my password for some reason) 20:48:20 Stevoisiak: fizzie will probably be able to help 20:50:19 or oerjan, I'm not sure which one of them 20:56:48 I probably can, if I can figure out how. 20:57:13 fizzie: does the automatic email-based password recovery work? 20:57:26 if so, then Stevo just has to request that and wait for the email 20:57:35 In theory yes, but there's a bit of an issue with the email setup on the wiki, which may result in emails never getting there. 20:57:54 (The server doesn't have a valid reverse DNS entry, thanks to Cloud at Cost, and many mail servers don't like that at all.) 20:58:08 ok 20:58:45 well, if Stevo is still logged in, he can prove that by editing, and then at worst you can rename his account and he can create a new one with this name 21:00:07 Looks like there's an administration script that can set the password of any user, I can just reset it manually. 21:00:21 -!- sebbu has quit (Read error: Connection reset by peer). 21:00:36 And then mail it to the associated email address. 21:00:44 Sure. I'll make an edit nw 21:00:47 -!- sebbu has joined. 21:01:20 Editing the page for http://esolangs.org/wiki/HQ9%2B 21:02:05 Oh wait, I have to do an intro first 21:04:55 [wiki] [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=52476&oldid=52470 * Stevoisiak * (+288) /* Introductions */ 21:05:05 There we go 21:05:13 [wiki] [[HQ9+]] M https://esolangs.org/w/index.php?diff=52477&oldid=52067 * Stevoisiak * (+8) Add creation year 21:07:59 Resolved. Though I should really try to get the emails to work. 21:12:10 On an unrelated note: The Befunge CAPTCHA had me so confused 21:12:59 I ended up turning the CAPTCHA into a StackOverflow question. 21:13:18 haha, the base 9 to base 10 conversion. gets everyone. 21:13:29 Wait, that's the reason? 21:13:31 https://stackoverflow.com/questions/45223117/why-does-the-befunge-code-9332682811-9-output-52256370 21:14:32 I think it turns base 9 to base 10, but I'm not quite sure 21:16:05 it's not quite that, but something close\ 21:16:10 I don't know the exact rule 21:16:12 I forgot 21:17:06 Doesn't seem to be base 9. 9332682811 in base 9 is 26072072027 21:21:03 -!- nulquen has joined. 21:21:09 -!- AnotherTest has joined. 21:23:04 118286233 in base 9 is 52256370 21:23:35 It's base 9 and reversed, and the 9 is a terminator. 21:23:46 Oh, int-e said it already. 21:24:02 yeah but without understanding the code :P 21:24:37 oh, the 9- acts on a duplicate to test for the terminator, it's not used in adding to the number? 21:24:39 (well, I have bits and pieces. in particular the multiplication by 9 suggests a conversion *from* base 9) 21:25:02 FWIW, "stick it into an online Befunge interpreter" *is* the intended way of passing it. 21:27:19 It's not so much an in-joke but a response to some rather nasty bouts of spammers. So's the introduction requirement. 21:29:11 fizzie: Honestly, I didn't think of using an interpreter for a good 30 minutes 21:29:48 If you want to work through it, it may be helpful to de-onelinerify it into http://sprunge.us/cMVA 21:30:38 (In the original the 9 is used for two slightly different things when going in different directions, which I think was a nice touch.) 21:31:53 -!- deltab has quit (Quit: Lost terminal). 21:33:07 ...sorry, I dropped a \ when converting it... 21:33:44 http://sprunge.us/bEJj should be more like it. 21:34:29 At the start of the loop (the >) the top of stack is basically an accumulator, so it pulls the next number under it (, tests if it is the terminating 9 (:9- and _), and if not, multiplies the accumulator by 9 and adds the new number to it (\9*+). 21:35:32 Hi. 21:37:58 -!- nulquen has quit. 21:39:07 fizzie: The Captcha help page should mention that an interpreter is the intended solution http://esolangs.org/wiki/Special:Captcha/help 21:44:23 Yeah, probably. I'm guessing that's a stock help text we've never customized. 21:49:07 -!- Phantom_Hoover has joined. 22:00:43 -!- Stevoisiak has quit (Quit: Page closed). 22:26:43 -!- Cale has quit (Ping timeout: 276 seconds). 22:27:45 -!- LKoen has joined. 22:33:33 -!- imode has quit (Ping timeout: 255 seconds). 22:37:54 -!- Cale has joined. 22:47:19 -!- ^_^v has quit (Quit: This computer has gone to sleep). 22:58:39 -!- LKoen has quit (Quit: “It’s only logical. First you learn to talk, then you learn to think. Too bad it’s not the other way round.”). 23:00:35 -!- joast has joined. 23:04:39 -!- boily has joined. 23:04:52 5 w 23:04:56 1/2:gaspatsjo//gaspatsjo is a norwegian soup, which died out due to a lack of hot summer days \ supermarioperator//supermarioperator is one of many confusing operators as defined in Control.Plumbers.Monad. Your sanity is in another castle. \ brain//Brains are just receptacles for bricks. \ rules of wisdom//unless essential for the entry‘s humor, 23:05:16  23:05:16 ​/home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: : not found 23:05:19 n 23:05:19 2/2:should: be understandable without the lookup key, be single spaced and end in a newline with no space before that, and use proper capitalization and punctuation jander//Jander was murdered, or deactivated permanently, depending on which side you ask. 23:07:40 -!- AnotherTest has quit (Ping timeout: 276 seconds). 23:10:31 -!- AnotherTest has joined. 23:18:40 -!- tswett has joined. 23:18:55 helloily 23:19:33 QUINTHELLOPIA! 23:19:38 Sunday. 23:19:48 did you see there is a free game on humble store today 23:19:58 i've not heard of it before but i can't argue with the price 23:20:08 huh? 23:20:27 shadow warrior 23:20:52 boily: huh what? it's not sunday 23:21:04 -!- wob_jonas has quit (Quit: http://www.kiwiirc.com/ - A hand crafted IRC client). 23:21:17 lel 23:22:24 of course we aren't. Sunday is happening on Sunday, tsé. 23:22:51 just like a bjonas to object and flee 23:25:50 ? bjonas 23:25:51 bjonas? ¯\(°​_o)/¯ 23:25:56 ? b_jonas 23:25:57 b_jonas egy nagyon titokzatos személy. Hollétéről egyelőre nem ismertek. 23:26:08 ? wob_jonas 23:26:08 wob_jonas is b_jonas in disguise, so that he can do magic tricks. 23:34:17 such as suddenly disappearing 23:38:40 * boily throws a fungot at wob_jonas' scent. “go! let's find him!” 23:38:40 boily: it's the same principle or whatever yeah 23:44:25 `? shachaf 23:44:26 Queen Shachaf of the Dawn sprø som selleri and cosplays Nepeta Leijon on weekends. He hates bell peppers with a passion. He doesn't know when to stop asking questions. 23:45:09 fresh salt and pepper pepper pepper. 23:45:22 boily: whoa whoa whoa 23:45:24 YSAC is TG 23:45:48 :D 23:45:51 unpack those acronyms twh would help 23:46:21 The videos at the YouTube channel named "You Suck At Cooking" are too good. 23:47:36 thachaf tdh did help 23:48:19 https://www.youtube.com/channel/UCekQr9znsk2vWxBo3YiLq2w/videos 23:55:02 -!- deltab has joined.