00:01:00 <tswett> 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 <tswett> 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 <tswett> In other words, arrows T -> U produce functors Mod(U) -> Mod(T).
00:20:03 <tswett> So lemme consider an example!
00:20:35 <tswett> Let G be the theory of groups, and let PG be the theory of pointed groups (groups with a distinguished element).
00:21:01 <tswett> There's an arrow G -> PG (everything that can be done within a group can be done within a pointed group).
00:21:17 <tswett> And the resulting functor Mod(PG) -> Mod(G) (every pointed group is a group).
00:21:49 <tswett> 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 <tswett> The trivial pointed group is also a group, of course.
00:22:02 <tswett> 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 <tswett> 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 <tswett> Not all theory extensions have that property.
00:29:50 <tswett> 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 <tswett> But that's not a coslice category, because the trivial abelian group is the trivial group.
00:31:17 <tswett> A pointed group is just a group equipped with a homomorphism out of the trivial pointed group.
00:31:33 <tswett> 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:27 <tswett> I get why certain axioms are allowed in a presentation, and certain ones are not.
00:35:06 <tswett> 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 <tswett> Only the first axiom is preserved by homomorphisms.
00:50:14 -!- oerjan has joined.
00:50:22 <alercah> I suspect because the latter doesn't provide a real quotient group
00:52:33 <tswett> What do you mean, doesn't provide a real quotient group?
00:53:36 <alercah> A presentation defines a group by quotient on the free group in however many generators
00:54:16 <alercah> 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:41 <tswett> 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 <alercah> but what subgroup is that even defining?
00:55:29 <tswett> Is it the... subgroup of all commutators?
00:55:57 <tswett> 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:30 <HackEgo> According to Wikipedia, ATWP means nothing.
00:56:47 <tswett> `le/rn atwp/According to Wikipedia, ATWP means "Air Transport White Paper".
00:56:48 <HackEgo> Usage: `le/[/]rn <key>//<wisdom>
00:56:56 <tswett> `le/rn atwp//According to Wikipedia, ATWP means "Air Transport White Paper".
00:56:58 <HackEgo> Relearned 'atwp': According to Wikipedia, ATWP means "Air Transport White Paper".
00:57:42 <alercah> tswett: huh so I checked, ab = ba is allowed
00:57:58 <alercah> on two generators it generates Z \times Z
00:58:14 <alercah> that makes sense, ab = ba ~ a^-1b^-1ab
00:58:29 <alercah> so not quite sure why I let you trick me into thinking it wasn't
00:58:40 <alercah> oh wait, "for all elements"
00:58:55 <alercah> uh let me think if I can come up with a good explanation
01:00:12 <alercah> I can't think of a trivial one, but if you look up the definition, it doesn't make sense
01:00:23 <tswett> The definition of "presentation of a group"?
01:01:19 <alercah> you can have an infinite set of equations
01:01:27 <alercah> so you can just include every equation of the form xy = yx
01:02:03 <tswett> But the definition of a group presentation doesn't allow you to do anything with universal quantifiers.
01:05:43 <tswett> Now here's the next big thing I'm wondering.
01:05:59 <tswett> Consider the concept of a category.
01:06:18 <tswett> 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 <tswett> If you add a terminal object, now you have the equivalent of a "true" proposition.
01:06:44 <tswett> Add products, now you've got conjunction, too.
01:07:09 <tswett> Add an initial object and coproducts, that's "false" and disjunction.
01:07:36 <tswett> Make it cartesian closed, and now you've got implication.
01:07:46 <alercah> it allows an infinite set of words though
01:07:59 <alercah> so you can just use quantifiers to build the set
01:08:24 <tswett> 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:11:36 <tswett> A cartesian closed category with finite sums is enough for propositional logic.
01:12:17 <tswett> What if I want predicate logic?
01:12:58 <tswett> If you want to do propositional logic in a category, you're probably seeing the objects as propositions.
01:13:45 <tswett> For predicate logic, now you need to look at objects as propositions *and* as domains that can be quantified over.
01:14:18 <tswett> And then a predicate is a morphism from a "domain" to a "proposition".
01:17:10 <tswett> A predicate is a morphism *into* a domain.
01:18:03 <tswett> Now, in predicate logic, you can do conjunction, disjunction, and implication between predicates, not just propositions.
01:19:47 <tswett> This means the category needs to have sums, products, and exponentials for morphisms, not just objects.
01:23:45 <tswett> For the initial object and coproducts, this is automatic.
01:24:32 <tswett> 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 <tswett> To have a cat satisfying a trivial property is not trivial; you must actually have a cat.
01:25:17 <tswett> 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 <tswett> Anyway, this ends up meaning that for predicate, you need a *locally* cartesian closed category with finite sums.
01:28:32 <tswett> And, um, does quantification automatically end up working?
01:34:33 <oerjan> is this the curry-howard-lambek correspondence of system F
01:35:32 <tswett> I'm referencing this: https://ncatlab.org/nlab/show/relation+between+type+theory+and+category+theory
01:40:39 <tswett> 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:12 <tswett> So the predicate "the integer x is even" is encoded as...
01:41:36 <tswett> 1. a proposition considered equivalent to "exists x, x is even"--in other words, the set of even integers
01:41:42 <tswett> 2. the domain, which is the set of integers
01:41:53 <tswett> 3. the inclusion function from the set of even integers to the set of integers
01:41:57 <boily> hellørjan! sidling toward me? :D
01:42:15 <tswett> Don't mind me, I'm just using this channel as my personal notepad.
01:42:31 <tswett> It's great because my notepad automatically contains funny things other people say.
01:44:23 <oerjan> boheily! anywhere nowhere near a category vortex twh
01:44:53 <boily> categories are nice. I don't understand them, but they make nice graphs ^^
01:44:56 <tswett> 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:45:09 <tswett> "(exists x, P(x)) or (exists x, Q(x))".
01:45:18 <tswett> Likewise, "exists x, false" is just "false".
01:46:08 <tswett> "exists x, P(x) and Q(x)" is the pullback of "exists x, P(x)" and "exists x, Q(x)".
01:46:17 <boily> tswellott. probably some manipulations involving sums-of-products or products-of-sums.
01:46:43 <oerjan> tswett: i really don't think you want "exists x," in there
01:47:00 <tswett> Note that I'm using "exists" to mean "dependent sum"...
01:47:24 <shachaf> tswelliott would be an odd individual
01:47:43 <tswett> 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:13 <tswett> You seem upset about this.
01:49:47 <tswett> "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 <oerjan> shachaf: that's about as much category theory as i understand.
01:51:13 <tswett> 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 <tswett> I'm going to skip that one.
01:52:35 <tswett> Let's just go straight to the fun part.
01:52:43 <HackEgo> [wiki] [[Ly]] https://esolangs.org/w/index.php?diff=52475&oldid=52465 * LyricLy * (+2521)
01:52:43 <tswett> What's "exists x, forall y, P(x,y)"?
01:52:43 <shachaf> Well, start with what is exists x. not(P(x)) in terms of exists x. P(x)
01:52:44 <HackEgo> fun fact 0 = 1 | fact n = n * fact (n - 1)
01:54:32 <shachaf> Of course exists x. not(P(x)) is not(forall x. P(x))
01:54:38 <oerjan> 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 <oerjan> unfortunately, the obvious response did not appear to me until after i'd made a worse one.
01:55:22 <shachaf> What's the obvious response?
01:55:30 <oerjan> "Where's the fun in that?"
01:56:02 <shachaf> But now you get your revenge.
01:56:22 <HackEgo> diagram chasing? ¯\(°_o)/¯
01:56:23 <oerjan> well i don't think they're on this channel.
01:57:08 <shachaf> `le/rn diagram chasing//Diagram chasing is a technique used to prove integer lemmas. Taneb invented it.
01:57:10 <HackEgo> Learned 'diagram chasing': Diagram chasing is a technique used to prove integer lemmas. Taneb invented it.
01:58:24 <HackEgo> diagram chasing:Diagram chasing is a technique used to prove integer lemmas. Taneb invented it.
01:58:34 <HackEgo> 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:<Phantom_Hoover> 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:50 <HackEgo> 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.
02:00:22 -!- MDude has joined.
02:00:25 <HackEgo> 8060:2016-05-14 <oerjän> ` mv wisdom/wumpu{,s}
02:00:41 <HackEgo> 8060:2016-05-14 <oerjän> ` mv wisdom/wumpu{,s} \ 8059:2016-05-14 <int-̈e> 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 <shachaf> Apparently the two four lemmas put together make the five lemma. And these people call themselves mathematicians.
02:00:56 <tswett> I'm pretty sure that a locally cartesian closed category with finite sums is enough for predicate logic.
02:01:13 <shachaf> `slwd wumpus//s,labyrinth,diagram,
02:01:15 <HackEgo> 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 <tswett> Well, yeah. Four plus four plus paths from three of the four to three of the other four equals five.
02:01:45 <oerjan> i guess that's a categorical improvement.
02:13:54 <lambdabot> 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:59 <HackEgo> [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:45 <HackEgo> 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:08 <HackEgo> /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: dow: not found
02:58:20 <HackEgo> 8775:2016-07-10 <oerjän> learn Cafreine is the favorite drug of category theorists.
02:58:28 <HackEgo> 8061:2016-05-15 <xfïx> ` echo 4 8 15 16 23 42 > "wisdom/6 random numbers"
03:05:58 <ais523> how could we make the wisdom database Turing-complete?
03:19:45 <shachaf> I've often wondered about using some sort of language for wisdom entries, rather than just plaintext.
03:19:58 <shachaf> For example to allow referencing/including other wisdom entries, and other things.
03:20:12 <shachaf> (Maybe it can allow running arbitrary commands, to implement `? ngevd)
03:23:07 <shachaf> That's kind of boring, though.
03:23:30 <shachaf> fizzie: Can you patch up HackEgo to get access to the nick of the user running the command?
03:24:06 -!- Warriga_l has joined.
03:36:14 <quintopia> i would play wumpus the hunted. it sounds fire
03:45:32 <Warriga_l> That sentence reminded me that I heard a song once that seemed to contain the words "they went fire".
03:45:42 <Warriga_l> So I did a Google search for "they went fire" and was surprised to actually find the song.
03:45:54 <Warriga_l> https://www.youtube.com/watch?v=CSPker14VVY - "Clash", Caravan Palace.
03:53:31 -!- hppavilion[1] has joined.
03:57:43 <Warriga_l> Dang, I feel like there was something I wanted to do.
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 <Vorpal> 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 <Vorpal> I wonder if you construct any useful programs where you jump into the middle of another instruction to execute different code
09:08:25 <Vorpal> possibly the suffix of one instruction and part or all of the next instruction could form a valid instruction as well
09:12:35 <shachaf> What do you count as a useful program?
09:12:57 <shachaf> This sort of thing is often used to write various exploits.
09:13:13 <Vorpal> so it can be used for non-trivial purposes then
09:13:15 <shachaf> I think I've also seen it in other contexts but I can't remember where.
09:13:52 <shachaf> Apparently it's also used for obfuscation. I don't consider that useful.
09:13:54 <Vorpal> 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 <shachaf> There are probably some golfing situations where it's useful, but I doubt there are that many?
09:14:50 <shachaf> I bet it can come up a lot when looking for ROP gadgets.
09:15:01 <shachaf> And https://en.wikipedia.org/wiki/JIT_spraying
09:16:00 <shachaf> 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 <shachaf> Then again ARM has multiple different encodings.
09:17:14 <Vorpal> I was just about to comment on that
09:17:46 <Vorpal> iirc on arm, if LSB is set in the target address of a jump, then it switches to thumb mode
09:17:53 <Vorpal> so maybe that is what they mean?
09:20:21 <shachaf> https://blogs.msdn.microsoft.com/oldnewthing/20090128-00/?p=19353/ talks about using this for golf
09:24:32 <shachaf> Man, this generated password is annoying. It's perfectly interleaved between characters that need shift pressed and characters that don't.
09:24:58 <Vorpal> shachaf: I use a password manager with auto-typing for such passwords
09:25:20 <shachaf> C++11 has auto-typing too.
09:25:30 <Vorpal> not that sort of auto-typing
09:25:47 <Vorpal> also the C++11 one is rudimentary compared to something like haskell for example
09:26:11 <shachaf> I know, I learned Haskell before I learned C++11.
09:27:01 <Vorpal> shachaf: though I guess guessing template parameters may be closer
09:29:43 <shachaf> Anyway, it's silly to generate a password of a fixed length for typing and not consider shift a keypress.
09:29:59 <shachaf> Really I should generate all my passwords to be of the for /[a-z]{n}/
09:30:43 <shachaf> Permitting uppercase letters adds only one bit of entropy per character, and is much harder to remember.
09:31:36 <shachaf> So you could permit uppercase letters, or you could add 3-4 more lowercase letters.
09:33:11 <shachaf> > map (logBase 2) [64^15, 26^19]
10:10:57 <Jafet> unfortunately it's not up to you whether to use uppercase letters, but up to the login provider
10:11:36 <shachaf> I can always add an uppercase letter, a digit, and a "special character" to satisfy the login provider.
10:11:45 <shachaf> What are special characters?
10:11:58 <HackEgo> [U+3235 PARENTHESIZED IDEOGRAPH SPECIAL]
10:12:04 <HackEgo> [U+3295 CIRCLED IDEOGRAPH SPECIAL]
10:12:08 <shachaf> I guess I should use more of those.
10:21:11 <Jafet> 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 <Jafet> “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 <shachaf> That is a clever vandalism.
10:48:45 <HackEgo> 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 <fizzie> 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 <fizzie> I don't know if you could use that for instruction reads.
10:51:15 <fizzie> 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:23:13 <shachaf> 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 <boily> Arachne, Asterion, Jorgrun, a misplaced balrog, a bunch o' spiders and a few electric eels for decoration.
11:56:19 <boily> what the fungot is going on...
11:56:19 <fungot> 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 <boily> fungot: no, you're Sir Fungellot.
11:56:29 <fungot> boily: i never believed it i thought once you were tried for like murder and you couldn't be tried again
12:11:29 <int-e> 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 <fungot> 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 <int-e> what does n.to_s.to_i(8) do with 119? Does it result in 11o = 9?
14:44:28 <HackEgo> /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: irb: not found
14:47:27 -!- Slereah has quit (Ping timeout: 240 seconds).
14:48:15 <int-e> 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 <int-e> (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 <Jafet> note that ⁹ is equivalent to ܋ᾗᾚᾗῃᾗᾗ
15:37:02 <Jafet> 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 <int-e> . 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 <int-e> say: 6 (from 16) 8 (from 8) 7 (less than 8) 5 (String) 2 (Zeichen) 1 (change by 1) 9 (9)
15:41:30 <int-e> ("Zeichen" means "character" in German :P)
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 <int-e> Apparently getting 14063 using H and n, starting from 10, is fairly hard.
16:06:53 <int-e> (10 is the result of 9T, the first number where H has a useful effect)
16:10:37 <Jafet> TnnHHHnHHHnHHHnHHHnTHnT seems no harder than other numbers of the same size
16:11:24 <int-e> (after reaching 10 first one)
16:14:14 <int-e> 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 <int-e> 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 <Jafet> well, the question of whether 9TH*n is enough is probably a hard number theory problem
16:58:36 <tswett> 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 <tswett> 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 <Jafet> 2-player peanos? https://www.youtube.com/watch?v=MzxZ8qtdun0
17:06:58 <int-e> Jafet: I'm doing 9T[Hn]* ... H* is likely to be terribly slow
17:07:21 <HackEgo> olist 1084: shachaf oerjan Sgeo FireFly boily nortti b_jonas
17:09:14 <int-e> (and yay, I made my laptop unusable, had to reboot)
17:11:57 <Jafet> > 10^length "14063" * 10 `div` length "89"
17:12:58 <tswett> I guess you could have a "board game" where the players take turns assigning specific numbers to all the quantifiers.
17:13:12 <Jafet> > let n = 500000 in n * (log n + 0.57)
17:15:42 <Jafet> (it should really be length "33357", which is the precursor to 14063)
17:16:09 <Jafet> tswett: does that work for all quantifiers? (namely, forall quantifiers?)
17:17:03 <tswett> 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 <int-e> Jafet: what does your [HTn]* program say for 36105?
17:21:08 <int-e> (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 <int-e> (37587 is the next one)
17:24:59 -!- tswett has quit (Quit: Leaving).
17:25:22 <int-e> hate the hater ... not the hate
17:27:03 <Jafet> therefore do not hate
17:27:26 <HackEgo> hth ([ʰtʰh̩]) is help received from a hairy toe. It is not at all hambiguitous.
17:27:46 <int-e> hassle the hassler
17:28:06 <Jafet> I can't seem to get past 6995 for [Hn]*, probably because this program is limited to 64-bit numbers
17:32:24 <int-e> http://lpaste.net/5694671569826086912 is what I've produced... throwaway code quality :P
17:34:38 <int-e> and it's gobbling up tons of memory too
17:34:57 <Jafet> 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 <Jafet> well, the 9T[Hn]* search finished without even getting to 6995
18:14:57 <Jafet> it found 3287481 numbers reachable without overflow, and then spun on an empty queue for half an hour
18:18:34 <Jafet> > 2^64 `div 3287481
18:18:36 <lambdabot> <hint>:1:11: error: parse error on input ‘3287481’
18:18:40 <Jafet> > 2^64 `div` 3287481
18:26:38 -!- sebbu has quit (Read error: Connection reset by peer).
18:28:07 <imode> what'cha doin', Jafet.
18:30:58 <Jafet> wasting time on the language given by https://paste.ee/p/hupOT
18:31:19 <imode> "written by trial and error". hah.
18:31:24 <Jafet> I'm not sure why this is worth the time. it's not even on the esowiki
18:31:47 <imode> why not spend the time?
18:32:16 <imode> if it's fun, why not? :P
18:33:10 <Jafet> 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 <Jafet> 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 <HackEgo> [wiki] [[Special:Log/newusers]] create * Totallyhuman * New user account
20:11:12 <HackEgo> [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 <wob_jonas> Hi guys. Can I ask stupid off-topic questions?
20:19:18 -!- LKoen has quit (Remote host closed the connection).
20:20:29 <wob_jonas> 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 <wob_jonas> 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 <wob_jonas> (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 <shachaf> 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 <wob_jonas> shachaf: hmm, that might be under this X mark on the back
20:24:08 <wob_jonas> 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 <shachaf> "When the unit has come to the end of its life, dispose of it inaccordance with local regulations."
20:26:20 <wob_jonas> 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:34 <shachaf> Maybe the local regulations tell you how to turn it off.
20:28:09 <shachaf> https://www.youtube.com/watch?v=ED31RlJASZE outlines one method.
20:28:40 <wob_jonas> shachaf: isn't that a different brand?
20:28:52 <shachaf> It's a different model but I suspet it can be adapted pretty easily.
20:38:19 -!- Stevoisiak has joined.
20:40:21 <Stevoisiak> 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 <wob_jonas> 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 <Stevoisiak> wob_jonas: I created it using my primary username and email, Stevoisiak
20:42:31 <Stevoisiak> I'd like to keep that username if possible
20:45:20 <wob_jonas> 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 <wob_jonas> I don't recall the details of which one works
20:46:35 <wob_jonas> 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 <Stevoisiak> @wob_jonas: I'm still waiting on my initial confirmation email
20:47:38 <Stevoisiak> wob_jonas: I'm still waiting on my initial confrimation email
20:48:15 <Stevoisiak> 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 <wob_jonas> Stevoisiak: fizzie will probably be able to help
20:50:19 <wob_jonas> or oerjan, I'm not sure which one of them
20:56:48 <fizzie> I probably can, if I can figure out how.
20:57:13 <wob_jonas> fizzie: does the automatic email-based password recovery work?
20:57:26 <wob_jonas> if so, then Stevo just has to request that and wait for the email
20:57:35 <fizzie> 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 <fizzie> (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:45 <wob_jonas> 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 <fizzie> 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 <fizzie> And then mail it to the associated email address.
21:00:47 -!- sebbu has joined.
21:01:20 <Stevoisiak> Editing the page for http://esolangs.org/wiki/HQ9%2B
21:04:55 <HackEgo> [wiki] [[Esolang:Introduce yourself]] https://esolangs.org/w/index.php?diff=52476&oldid=52470 * Stevoisiak * (+288) /* Introductions */
21:05:13 <HackEgo> [wiki] [[HQ9+]] M https://esolangs.org/w/index.php?diff=52477&oldid=52067 * Stevoisiak * (+8) Add creation year
21:07:59 <fizzie> Resolved. Though I should really try to get the emails to work.
21:12:10 <Stevoisiak> On an unrelated note: The Befunge CAPTCHA had me so confused
21:12:59 <Stevoisiak> I ended up turning the CAPTCHA into a StackOverflow question.
21:13:18 <wob_jonas> haha, the base 9 to base 10 conversion. gets everyone.
21:13:31 <Stevoisiak> https://stackoverflow.com/questions/45223117/why-does-the-befunge-code-9332682811-9-output-52256370
21:14:32 <wob_jonas> I think it turns base 9 to base 10, but I'm not quite sure
21:16:05 <wob_jonas> it's not quite that, but something close\
21:17:06 <Stevoisiak> 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 <int-e> 118286233 in base 9 is 52256370
21:23:35 <fizzie> It's base 9 and reversed, and the 9 is a terminator.
21:23:46 <fizzie> Oh, int-e said it already.
21:24:02 <int-e> yeah but without understanding the code :P
21:24:37 <wob_jonas> oh, the 9- acts on a duplicate to test for the terminator, it's not used in adding to the number?
21:24:39 <int-e> (well, I have bits and pieces. in particular the multiplication by 9 suggests a conversion *from* base 9)
21:25:02 <fizzie> FWIW, "stick it into an online Befunge interpreter" *is* the intended way of passing it.
21:27:19 <fizzie> 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 <Stevoisiak> fizzie: Honestly, I didn't think of using an interpreter for a good 30 minutes
21:29:48 <fizzie> If you want to work through it, it may be helpful to de-onelinerify it into http://sprunge.us/cMVA
21:30:38 <fizzie> (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 <fizzie> ...sorry, I dropped a \ when converting it...
21:33:44 <fizzie> http://sprunge.us/bEJj should be more like it.
21:34:29 <fizzie> 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:37:58 -!- nulquen has quit.
21:39:07 <Stevoisiak> fizzie: The Captcha help page should mention that an interpreter is the intended solution http://esolangs.org/wiki/Special:Captcha/help
21:44:23 <fizzie> 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:56 <HackEgo> 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 <HackEgo> /home/hackbot/hackbot.hg/multibot_cmds/lib/limits: line 5: exec: : not found
23:05:19 <HackEgo> 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:19:48 <quintopia> did you see there is a free game on humble store today
23:19:58 <quintopia> i've not heard of it before but i can't argue with the price
23:21:04 -!- wob_jonas has quit (Quit: http://www.kiwiirc.com/ - A hand crafted IRC client).
23:22:24 <boily> of course we aren't. Sunday is happening on Sunday, tsé.
23:22:51 <quintopia> just like a bjonas to object and flee
23:25:57 <HackEgo> b_jonas egy nagyon titokzatos személy. Hollétéről egyelőre nem ismertek.
23:26:08 <HackEgo> wob_jonas is b_jonas in disguise, so that he can do magic tricks.
23:38:40 * boily throws a fungot at wob_jonas' scent. “go! let's find him!”
23:38:40 <fungot> boily: it's the same principle or whatever yeah
23:44:26 <HackEgo> 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 <boily> fresh salt and pepper pepper pepper.
23:45:51 <quintopia> unpack those acronyms twh would help
23:46:21 <shachaf> The videos at the YouTube channel named "You Suck At Cooking" are too good.
23:48:19 <shachaf> https://www.youtube.com/channel/UCekQr9znsk2vWxBo3YiLq2w/videos
23:55:02 -!- deltab has joined.