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 oerjä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