00:03:19 -!- boily has joined. 00:03:34 bohily 00:03:58 -!- MoALTz has quit (Ping timeout: 272 seconds). 00:04:24 oerjan: i always imagine you yodeling that hth 00:04:29 -!- hppavilion[2] has quit (Ping timeout: 250 seconds). 00:05:51 hallørjen. 00:06:06 hellochaftiddlywhoo 00:06:44 -!- hppavilion[2] has joined. 00:07:14 hppavellon[2]. 00:07:50 -!- yorick_ has changed nick to yorick. 00:08:15 alas, poor underline 00:13:34 helloily 00:13:42 Vim programs F1 as help and other functions keys do nothing [...] <-- F1 opens help in gvim on windows, at least 00:14:01 (that's the only one i checked) 00:14:23 oh, works in my linux terminal too 00:14:38 oh wait 00:14:44 sorry, misparsed your sentence 00:15:35 quinthellopia 00:19:19 -!- boily has quit (Quit: CLOCKWISE CHICKEN). 00:24:51 -!- hppavilion[2] has quit (Ping timeout: 246 seconds). 00:27:39 -!- hppavilion[2] has joined. 00:50:35 why does socketpair need to be a syscall? 00:57:21 because 00:57:37 -!- hppavilion[2] has quit (Read error: Connection reset by peer). 00:58:34 -!- hppavilion[1] has joined. 01:00:43 oh 01:19:47 -!- Etaoin has joined. 01:20:05 hellaoin 01:25:31 -!- hppavilion[1] has quit (Ping timeout: 240 seconds). 01:55:13 -!- Etaoin has quit (Quit: BOOSH). 02:00:17 -!- hppavilion[1] has joined. 02:00:24 -!- adu has joined. 02:03:57 -!- bender has joined. 02:05:33 -!- hppavilion[1] has quit (Ping timeout: 240 seconds). 02:09:08 -!- bender has quit (Quit: Leaving). 02:15:38 <\oren\> I recently switched to using ctrl-ins, shift-ins for copy and paste. this has the advantage of working on windows, linux and mac the same way 02:16:21 I don't have an Ins key. 02:16:53 <\oren\> o_O; wha? 02:17:13 <\oren\> what computer doesn't have insert? 02:18:49 My work computer, a MacBook Pro. 02:19:22 Somehow it still has a caps lock key, though. 02:19:42 Apple got rid of the floppy drive and of the optical drive. But they didn't get rid of caps lock. Absurd. 02:20:43 -!- hppavilion[1] has joined. 02:20:49 <\oren\> shachaf: I use a macbook at work, but I have an external keyboard 02:21:40 <\oren\> the macbook's keyboard is also missing a numpad, which i consider essential 02:21:54 I consider it inessential. 02:22:06 I learned hjklyubn so now I can play NetHack without a number pad. 02:22:32 <\oren\> I use the numpad to type numbers quickly 02:22:43 I use the numrow to type numbers quickly. 02:23:44 i have given up having a numpad as well 02:23:58 I never wanted it in the first place. 02:24:14 not only are numpadless keyboards more compact, they are less expensive! 02:24:16 Typing numbers is for the birds. 02:24:38 i have yet to adopt a bird to type numbers for me, I regret to admit 02:24:57 The Bird is Cruel! 02:25:03 (Or so `hoag informs me.) 02:25:28 (i have purchased keyboards with numpads before, but it was only coincidence--it was never a factor in my decision) 02:27:07 <\oren\> only thing I don't like about this keyboard (on my Thinkpad) is the lack of a print screen key 02:28:32 I'm OK with a pixel screen. Printers are outdated. 02:28:39 <\oren\> print screen is essential for pics or it didn't happen 02:29:59 On my work computer, a MacBook Pro, I can press Cmd-Shift-3 to make a picture of the screen, or Cmd-Shift-4 to make a picture of a window or rectangle. 02:30:22 Very convenient. 02:30:32 I think my laptop has all the same keys that a full keyboard has, except for two. 02:30:41 Plus it has one key that a full keyboard doesn't have. 02:30:44 On my personal computer, I have a Print Screen key. But I usually run a command line program. 02:30:53 Those keys are insert and scroll lock. 02:31:36 And "fn" is the extra one. 02:32:23 * oerjan has all those, and a numpad 02:32:47 oerjan: do you have a laptop that does have insert and scroll lock keys? 02:33:16 well there's a marking for scr lk on the num lk key 02:33:31 and there's insert on the numpad 02:33:42 So no, it doesn't have a scroll lock key. 02:34:04 my previous laptop didn't have a separate numpad, although it had a setting to put a numpad in the middle of the ordinary keys 02:34:10 OKAY 02:34:23 oerjan: tswett sure showed you 02:34:32 I'm talking about dedicated keys. Mine has decidated keys for all but two of the standard keys. 02:34:33 and the insert key is shared with 0 02:34:52 oerjan: so far, it sounds like you have the same laptop keyboard that I have. 02:35:01 is it an asus 02:35:08 Yes. 02:35:18 which one 02:35:48 Do the media buttons on your F keys go sleep, airplane, keyboard dim, keyboard bright, screen dim, screen bright, screen off, projector, touchpad disable, mute, quiet, loud? 02:37:11 i don't have keyboard lights, but otherwise yes 02:37:21 (i think) 02:38:04 not sure about airplane, it's some kind of radiating antenna symbol 02:38:49 Probably the same thing. 02:38:54 Does your F2 key have a little light in it? 02:38:56 Fn + F3 seems to open up some email program. 02:39:25 oh it's airplane indeed. no light though. 02:39:32 `wisdom 02:39:37 I really oughta get my media keys working. 02:39:52 F3 and F4 have no media symbols 02:39:53 I'm tired of only being able to change my backlight brightness by using the xbacklight command. 02:40:03 døsthiswork//no 02:40:22 clever 02:40:31 `cwlprits døsthiswork 02:40:43 int-e ais523 oerjan elliott olsner Bike FreeFull shachaf 02:40:48 whoa whoa whoa 02:40:58 `hog wisdom/døsthiswork 02:41:06 ​ revert \ cp wisdom/doesthiswork wisdom/d\xc3\xb8sthiswork \ revert \ for x in wisdom/*; do rev "$x" > "$x"a; mv "$x"a "$x"; done \ echo yes > wisdom/d\xc3\xb8sthiswork 02:41:37 `wisdom 02:41:39 pico//pico is the useless twin of nano. 02:43:04 Maybe I should upgrade to 16.4. 02:43:35 pico isn't cool. You know what's cool? nano. 02:44:27 when my laptop was in for repairs, i got a replacement with keyboard lights. i found it irritating, especially since it wouldn't remember that i wanted them off. 02:45:13 (well, when i turned the laptop on.) 02:45:41 is there an atto 02:45:57 Just paint over all the letters with black paint. 02:46:11 Use one of those tiny brushes. 02:46:24 AAAAAAAA 02:46:44 What's the codename for 16.4, anyway? 02:46:58 tswett: the lights came through the borders of the keys, not the letters, iirc. 02:47:17 Just install rubber seals around all the keys. 02:47:23 i may misremember whether the letters also shined 02:47:48 anyway, that laptop is long since back in the shop. 02:48:28 It'd be kind of difficult to use a backlit keyboard where the letters don't shine. 02:48:35 . o O ( Atrocious Allosaurus ) 02:48:58 MAYBE 02:48:58 Isn't this one X? 02:49:02 Also, what was the animal for U? 02:49:12 tswett: i'm just joking 02:49:20 Nobody can name an animal starting with U. 02:49:42 huh 02:49:52 Undulating Utahraptor 02:50:24 Oh wow, my Ubuntu distro has been EOL since February. 02:50:26 Why wasn't I notified? 02:50:40 the notifications were also EOLed hth 02:50:54 -!- hppavilion[2] has joined. 02:51:07 os 02:51:50 hm it is indeed hard to think of a modern animal starting with U. 02:52:15 <\oren\> Usagi 02:52:22 in english, \oren\ 02:52:37 although i also thought of that one 02:52:45 <\oren\> Uman 02:53:15 -!- hppavilion[1] has quit (Ping timeout: 246 seconds). 02:53:25 Ulv 02:53:49 -!- lambda-11235 has quit (Quit: Bye). 02:53:54 <\oren\> hppavilion[2]: you've been incremented! 02:53:58 there's got to be some obscure antelope 02:54:48 <\oren\> Uakari 02:54:55 Yeah, maybe they've got one on the coat of arms of some country starting with U. 02:55:07 <\oren\> it's a kind of monkey 02:55:09 Like, maybe it's an animal where the name of the animal just begins with the name of that country. 02:55:49 <\oren\> Ukrainian swamp tiger 02:56:06 That doesn't sound like an obscure antelope. 02:56:33 stupid wikipedia's mammal list goes by genus in latin 02:57:04 oerjan: "genus" in latin is "genus" hth 02:57:25 * oerjan lightly swats shachaf -----### 02:57:42 No, "genus" in Latin is "genus_(taxinomia)" hth. 02:57:47 Proof: https://la.wikipedia.org/wiki/Genus_%28taxinomia%29 02:57:49 -!- hppavilion[2] has quit (Ping timeout: 260 seconds). 02:57:58 Sorry, it's "genus_%28taxinomia%29". 02:59:33 -!- jaboja has quit (Ping timeout: 240 seconds). 03:00:32 Man, I really miss the days when Ubuntu's theme color was brown instead of purple. 03:01:42 -!- hppavilion[2] has joined. 03:04:56 Oh right, I was gonna ponder this funny little language of mine. 03:10:51 -!- hppavilion[2] has quit (Ping timeout: 240 seconds). 03:11:33 `unicode U+01b9 03:11:37 ​ƹ 03:12:09 `unidecode ƹ 03:12:14 ​[U+01B9 LATIN SMALL LETTER EZH REVERSED] 03:13:08 This is the language that's tentatively named Tokiber. 03:13:21 Not to be confused with the language that's tentatively named Quendle. 03:14:02 -!- hppavilion[2] has joined. 03:14:45 <\oren\> tswett: they switched to purple? 03:15:27 \oren\: yeah, like nearly ten years ago. 03:17:32 <\oren\> their website is still orange 03:19:03 <\oren\> hmm from screenshots of 16.04 I can see there's a lot more purple now, but still some orang 03:19:24 -!- hppavilion[2] has quit (Ping timeout: 260 seconds). 03:19:58 Things I have defined in Tokiber: categories; categories with a terminal object; finite product categories; finite limit categories; monoids; the forgetful functor from monoids to categories; groups; abelian groups; rings with identity; "natural number algebras". 03:20:51 <\oren\> what about strings? 03:21:24 <\oren\> oh, wait, every string is a natural number, never mind 03:21:34 Strings aren't natural numbers. 03:21:57 <\oren\> they could be represented by them? 03:22:14 Of course. 03:22:20 <\oren\> the string "\00" is 2. the string 03:22:31 <\oren\> "\0\0" is 2 03:22:40 <\oren\> h... 03:23:09 A natural number algebra consists of a sort N, a point "zero" in N, and a function "succ" from N to N. 03:23:17 <\oren\> screw it, take the bitstream, add a 1 at the end and call that a number 03:24:27 <\oren\> tswett: a sort like quicksort or mergesort? 03:24:32 Nah, use bijective base 1112064. 03:24:41 "A sort" means "a set or whatever". 03:24:41 What's a point? An arrow from a terminal object? 03:25:16 You should do the CDOs in http://chu.stanford.edu/PrattSRMK2016.pdf 03:25:23 <\oren\> oh, bijective base. that is way better. 03:25:23 You have points and copoints. It's TG. 03:25:33 An arrow from a terminal object, yes. 03:26:04 And adjunctions are just a special case of associativity. 03:26:16 So yeah, really "a sort" means "an object in the ambient category-with-a-terminal-object". 03:26:37 an object in the ambivalent category 03:27:58 "Function", of course, means "arrow". 03:28:15 I want to define the squaring function on the integers. 03:28:32 <\oren\> man, I'm still entirely ignorant of the difference between a category and a set. 03:29:17 There isn't much similarity. 03:29:40 A category is a directed graph equipped with a composition operator which is associative and has identities. 03:29:50 A set isn't. 03:30:23 <\oren\> ok but what does it mean for something to be "in the category C" 03:30:28 Pft. A category is a generalized monoid. 03:30:52 <\oren\> does that mean it's one of the points on the graph? 03:31:00 Do you actually want an answer for what a category is? 03:31:26 \oren\: well, that depends on what the thing is. The vertices of a category are called objects, so that tells you what an "object in the category C" is. 03:32:06 The edges are called arrows or morphisms (the two words are exact synonyms). 03:33:10 <\oren\> ok that makes a lot more sense than the wikipedia article 03:33:26 The "usual case" is for the objects to be algebraic structures and for the arrows to be homomorphisms between them. 03:33:35 That's what the "category of groups" is, for example. 03:34:18 I think thinking of a category as a graph is a bit misleading if you want good intuition. 03:34:45 <\oren\> can I think of it as a set of sets and functions between sets? 03:35:09 <\oren\> that's how i was thinking of it 03:35:09 The important part of a category is the arrows. 03:35:11 You can certainly think of it as being *like* a set of sets and functions between sets. 03:35:14 The objects are almost irrelevant. 03:35:28 The arrows aren't functions (except in some special cases). 03:35:32 In most cases, the objects are "kind of like sets" and the arrows are "kind of like functions". 03:38:02 <\oren\> shachaf: in what ways can they fail to be functions? 03:38:29 Are the elements of a group functions? 03:39:30 Well, that's maybe a bad question because of Cayley's theorem. 03:40:37 -!- lambda-11235 has joined. 03:42:44 <\oren\> shachaf: I was thinking more of what they do to the elements of the objects 03:43:37 \oren\: categories that are "sets and functions between sets" are an important special case, known as _concrete_ categories. 03:44:20 \oren\: I'd give you an example, but maybe first you should have the definition of a category. 03:44:56 <\oren\> seems like first I need the definition of an object? 03:45:14 there isn't one 03:45:22 an object can be literally _anything_ 03:45:30 dependent on the category 03:45:56 First you need the definition of an arrow. 03:46:06 Which can also be literally anything. 03:46:17 OK, well, do you know what a monoid is? 03:46:31 <\oren\> something from Haskell? 03:46:47 <\oren\> no wait that's "monad" 03:47:05 Do you know what a group is? 03:47:11 <\oren\> yes 03:47:23 A monoid is like a group, except elements don't necessarily have inverses. 03:47:54 <\oren\> ok. 03:47:59 So you have multiplication, and you have an identity element 1, such that a(bc) = (ab)c, a1 = a, 1a = a 03:48:33 Sounds good? 03:48:44 <\oren\> yup. with you so far. 03:49:08 A good example of a monoid is strings over some alphabet. Multiplication is concatenation, and 1 is the empty string. 03:49:53 Another example of a monoid is NxN matrices, with the identity matrix and matrix multiplication. 03:50:35 But what you'd want to do is talk about the monoid of all matrices, not just NxN matrices. 03:50:48 Multiplication is still associative, and you still have identity matrices. Right? 03:51:00 <\oren\> yeah. 03:51:13 The trouble is that you can't multiply two arbitrary matrices. The sizes have to match. 03:51:36 In particular, you can multiply and IxJ matrix with a JxK matrix, to get an IxK matrix. 03:52:01 And you don't just have one identity, you have one for each size. So you have a 5x5 identity matrix and so on. 03:52:10 <\oren\> right 03:52:45 The laws are still the same. a(bc) = (ab)c, id_N . a = a, a . id_M = a 03:52:51 If a is an NxM matrix. 03:53:18 (Where . is multiplication.) 03:53:59 So if you generalize that, that's what a category is. 03:54:23 <\oren\> where the matrices are the arrows? 03:54:26 Yes. 03:54:28 A category has a bunch of things, called arrows, that you can multiply together. 03:54:37 But you can't multiply any two things together. 03:54:59 <\oren\> only if one points to the vertex where another begins. 03:55:14 So you have a bunch of things, called objects. Each arrow has a "domain" object and a "codomain" object (these correspond to the dimensions of the matrix). 03:55:48 You generally write f : A -> B to mean that f is an arrow with domain A and codomain B. 03:57:14 You have an operation ., called composition or multiplication, where f . g is defined the codomain of g is equal to the domain of f. 03:57:42 . is associative 03:58:14 And for every object A, you have a special arrow 1_A : A -> A, such that for any f : A -> B, f . 1_A = f, and for any g : C -> A, 1_A . g = g 04:00:21 Does that make sense? 04:00:26 <\oren\> yes 04:00:50 OK. It's pretty simple. 04:01:06 Now you can talk about other categories. A popular one is one where the arrows are functions. 04:01:35 The objects are sets. You can see that it all works out. 04:06:18 <\oren\> that helps a lot, to have an example other than the category(s) of functions and sets 04:06:47 There are lots of other examples. 04:07:59 You can pretty easily see that a monoid is a category with one object. Yes? 04:08:09 (Or can be represented that way, at least.) 04:08:19 <\oren\> yes 04:08:45 And it doesn't matter what the object is. For example, it could be a cup of tea. 04:09:32 You can represent a set as a category, where each object represents an element, and there are only identity arrows. 04:09:37 (That's called a "discrete category".) 04:11:19 You can also represent a preorder as a category. You do that by saying that, for any pair of objects (A,B), there's at most one arrow : A -> B, iff A <= B. 04:12:03 Identity arrows correspond to reflexivity, and arrow composition corresponds to transitivity. 04:12:26 <\oren\> i see, the composition of arrows would only lead to true <= statements... 04:12:39 Right. 04:12:50 These are kind of boring categories because they're extreme. 04:13:40 -!- Etaoin has joined. 04:13:43 <\oren\> they should be on the wiki page so that people can figure out that a category isn't just what i thought it was. 04:13:58 A very popular sort of category is one where the arrows are homomorphisms of some structure. 04:14:11 For example, group homomorphisms, or continuous functions, or linear maps. 04:14:35 The objects would be groups, or topological spaces, or vector spaces, respectively. 04:14:57 (The category of finite-dimensional vector spaces and linear maps is very similar to the one with matrices that we started with.) 04:15:36 Sounds good? 04:15:58 <\oren\> yeah all of those sound like they should work 04:16:26 People almost always define homomorphisms such that they're associative and have identities. 04:16:33 The next question is why would you care about categories? 04:17:04 And in a way this whole conversation is backwards, because that question is the right place to start. 04:19:04 Probably the right approach is to start with naturality, like what's-his-name did. 04:45:38 -!- hppavilion[2] has joined. 04:55:55 What're some of the best spacey simulations? 04:56:23 -!- hppavilion[2] has set topic: The intradisciplinary hub of solidarity matrices, esoteric programming language design, multichannel bot abuse (always safe, sane and consensual), and font forging (dangerous and potentially illegal) | http://esolangs.org/ | logs: http://codu.org/logs/_esoteric/ http://tunes.org/~nef/logs/esoteric/?C=M;O=D | https://dl.dropboxusercontent.com/u/2023808/wisdom.pdf. 05:00:37 <\oren\> hppavilion[2]: KSP is my favorite, but there's also space engine 05:00:52 -!- Etaoin has quit (Quit: Page closed). 05:00:53 \oren\: I mean videos xD 05:01:08 \oren\: Simulations of weird things happening in space 05:08:03 -!- Kaynato has quit (Ping timeout: 240 seconds). 05:13:30 -!- spockers has quit (Quit: bye http://i.imgur.com/nkzOWAv.jpg). 05:16:31 -!- augur has quit (Ping timeout: 240 seconds). 05:16:48 -!- augur has joined. 05:21:19 -!- hppavilion[2] has quit (Ping timeout: 260 seconds). 05:23:06 -!- spockers has joined. 05:33:52 -!- adu has quit (Quit: adu). 05:50:28 Uhhh, right. I wanted to define the squaring function on the integers. 05:50:52 Which probably means I should define the integers. 05:52:39 So far, I don't have a way to do that. 06:01:39 -!- spockers_ has joined. 06:02:09 Like, I have a way to define finite algebras. 06:03:22 -!- spockers has quit (Killed (wilhelm.freenode.net (Nickname regained by services))). 06:03:22 -!- spockers_ has changed nick to spockers. 06:03:34 -!- shikhin_ has joined. 06:04:49 -!- dingbat has quit (*.net *.split). 06:04:49 -!- Melvar has quit (*.net *.split). 06:04:49 -!- Deewiant has quit (*.net *.split). 06:04:49 -!- clog has quit (*.net *.split). 06:04:49 -!- incomprehensibly has quit (*.net *.split). 06:04:49 -!- shikhin has quit (*.net *.split). 06:05:30 -!- shikhin_ has changed nick to shikhin. 06:09:58 So I've defined sets, and I've defined rings with identity. 06:10:08 Here's what the definition of a set currently looks like: 06:10:15 theory Set : CATEGORY { sort Element; } 06:10:38 Paraphrased in English: 06:10:41 "A set consists of a set." 06:11:38 You can define the empty set, too. It looks something like this: 06:11:53 algebra EmptySet : Set { Element := 0; } 06:12:40 The definition of a ring with identity starts out like this: 06:12:55 theory RingWithIdent extends Set : FPRODCAT { 06:13:50 The "extends" keyword automatically defines a forgetful functor RingWithIdent -> Set. 06:16:45 So theoretically, you ought to just be able to grab the left adjoint to that functor, giving you the free functor Set -> RingWithIdent. 06:17:06 And then apply that to EmptySet, and boom, you get the free ring-with-identity on the empty set—in other words, the integers. 06:17:57 That's all well and good. In fact, let me simply declare that that is now a feature of the language. 06:18:03 How are we gonna define functions on the integers, now? 06:20:42 Come to think of it, I haven't defined any way of defining homomorphisms at all. 06:39:36 All right, I suppose theoretically I ought to just be able to say this: 06:40:53 homomorphism square : forget Integer as Set -> forget Integer as Set { all x := mult x x } 06:41:43 Good ol' "forget Integer as Set". One of my favorite algebras. 06:43:56 Whoops, I forgot the semicolon. 06:45:18 And I guess logically, I ought to be able to define the integers like this: 06:45:34 define algebra Integer : RingWithIdent := free EmptySet as RingWithIdent; 06:46:06 Likewise, I ought to be able to define the natural numbers (in one of their incarnations) like this: 06:46:21 define algebra PeanoNatural : NatNumAlg := free EmptySet as NatNumAlg; 06:47:02 Now ideally, one might like to be able to define the "inclusion" function from PeanoNatural to Integer. 06:47:15 Rather, from "forget PeanoNatural as Set" to "forget Integer as Set". 07:03:16 -!- Melvar has joined. 07:03:56 -!- idris-bot has quit (Ping timeout: 250 seconds). 07:06:50 -!- clog has joined. 07:08:13 -!- spockers has quit (Remote host closed the connection). 07:14:33 -!- spockers has joined. 07:28:48 -!- lambda-11235 has quit (Quit: Bye). 07:29:09 -!- spockers has quit (Quit: bye http://i.imgur.com/nkzOWAv.jpg). 07:33:41 -!- spockers has joined. 08:01:28 -!- spockers has quit (Quit: bye http://i.imgur.com/nkzOWAv.jpg). 08:25:53 -!- augur has quit (Remote host closed the connection). 08:36:23 -!- MoALTz has joined. 08:49:22 http://int-e.eu/~bf3/tmp/cube8.html ... that was tricky to reassemble :) 08:52:35 -!- augur has joined. 08:55:04 -!- newsham has joined. 09:16:03 <\oren\> corrolary to the sapir-whorf hypothesis: learning a new language increases the range of thoughts you can think. 09:17:19 Or perhaps decreases it. 09:17:56 tswett: 2 is sometimes called I, the interval category 09:18:09 In some ways it behaves like the closed interval [0,1] 09:18:23 In this perspective a natural transformation is like a homotopy of functors. 09:18:40 Yup. 09:19:46 You can define the interval category in Tokiber easily enough... 09:20:07 theory Interval : CATEGORY { sort Domain; sort Codomain; arrow : Domain -> Codomain; } 09:20:34 Can you define hTop? 09:21:29 The category whose objects are topological spaces and whose arrows are homotopy classes of continuous maps? 09:21:52 Not as a theory, no. 09:22:06 You can't define a theory that has uncountably many objects. 09:22:10 What! 09:22:32 Not even uncountably many? 09:22:35 I mean, you "could" do that, but only by writing an uncountable amount of code. 09:23:15 For the doctrine CATEGORY, you can't even define a theory that has infinitely many objects. 09:25:09 A theory is a finite presentation of a category (or a category-with-a-terminal-object or a finite product category or a finite limit category). And every finitely presented category-with-a-cherry-on-top has only countably many objects. 09:28:15 But what about infinitary theories? 09:28:22 `? frame 09:28:53 A frame is just a complete Heyting algebra. Frame homomorphisms don't preserve implication, if you know what I mean. 09:29:50 -!- bb010g has quit (Quit: Connection closed for inactivity). 09:30:24 Every definition represents a finite mathematical object. 09:30:27 «For infinitary theories, such as that of frames, there is a hitch. Step 2 of Theorem 4.3.6 tells us to form the set of all possible expressions using the generators and the operators, and at this stage the general theory doesn't use the algebraic laws to make any identifications between expressions (this comes in Step 4). This is fine for the finitary algebraic theories. However, for frames, we can mak 09:30:33 e new expressions by forming joins of ... 09:30:35 ... arbitrary sets of older expressions, and this can't be done in set theory. Technically, the "set" of all possible expressions would be a proper class: it is too big to be a valid set. This is a genuine problem. There are infinitary theories (such as that of complete Boolean algebras - see Johnstone [82]) where this is insuperable and presentations simply don't present algebras. For frames, fortunatel 09:30:41 y, presentations do present, but we ... 09:30:44 ... have to argue slightly carefully to show this.» 09:30:46 I don't even remember any of this 09:30:48 Look 09:30:57 You can define a finite ring. You can't define an infinite ring, but you can define a finite presentation of a ring. 09:32:15 And that's a lot like being able to define any finitely presented ring. 09:36:52 -!- oerjan has quit (Quit: Nite). 09:50:02 -!- spockers has joined. 10:19:20 does anyone know why all my compilers on linux create elf files where EI_OSABI is always 0 (which is sysv) instead of 3 (which is linux)? 10:27:18 -!- augur has quit (Remote host closed the connection). 10:27:56 -!- augur has joined. 10:32:22 -!- augur has quit (Ping timeout: 250 seconds). 10:34:21 `` cp /bin/ls .; file ls 10:34:37 ls: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked (uses shared libs), for GNU/Linux 2.6.26, BuildID[sha1]=0x55f1e005df252708d4c456dcc2c7dccea1006553, stripped 10:34:43 `` dd bs=1 seek=7 conv=notrunc count=1 of=ls status=none <<< $'\3'; file ls 10:34:45 dd: invalid status flag: `none' \ Try `dd --help' for more information. \ ls: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked (uses shared libs), for GNU/Linux 2.6.26, BuildID[sha1]=0x55f1e005df252708d4c456dcc2c7dccea1006553, stripped 10:34:54 `` dd bs=1 seek=7 conv=notrunc count=1 of=ls 2>/dev/null <<< $'\3'; file ls 10:34:58 ls: ELF 64-bit LSB executable, x86-64, version 1 (GNU/Linux), dynamically linked (uses shared libs), for GNU/Linux 2.6.26, BuildID[sha1]=0x55f1e005df252708d4c456dcc2c7dccea1006553, stripped 10:35:13 `` ./ls -l ls 10:35:15 ​-rwxr-xr-x 1 5000 0 114032 Jul 2 09:34 ls 10:36:52 all the elf files in my system are (SYSV) instead of (GNU/Linux) 10:52:44 Haha. http://lists.gnu.org/archive/html/bug-glibc/2001-05/msg00169.html ... anyway, "If the object file does not use any extensions, it is recommended that this byte be set to 0." 10:53:00 (the latter quote is from https://refspecs.linuxfoundation.org/elf/gabi4+/ch4.eheader.html ) 11:12:41 -!- hppavilion[2] has joined. 11:22:17 -!- spockers has quit (Quit: bye http://i.imgur.com/nkzOWAv.jpg). 12:17:22 The John Byrne modern-age Superman has canon regarding his facial hair 12:17:35 It grows normally, and he has to heat vision a reflective surface to zap it off 12:41:07 -!- jaboja has joined. 12:44:47 thanks for the link int-e 12:50:52 -!- hppavilion[2] has quit (Ping timeout: 252 seconds). 12:54:34 -!- Melvar has quit (Quit: WeeChat 1.4). 12:54:49 -!- Melvar has joined. 13:04:05 -!- bender has joined. 13:12:35 -!- hppavilion[2] has joined. 13:14:11 The Imperinatus! (Starring Harrison Fnord) 13:30:37 -!- variable has joined. 13:32:51 -!- jaboja has quit (Ping timeout: 264 seconds). 13:35:25 -!- hppavilion[2] has quit (Ping timeout: 252 seconds). 13:35:29 -!- spockers has joined. 13:58:11 -!- bender has quit (Ping timeout: 250 seconds). 14:01:51 -!- idris-bot has joined. 14:02:34 -!- variable has quit (Quit: 1 found in /dev/zero). 14:18:34 -!- hppavilion[2] has joined. 14:48:27 -!- moon_ has quit (Ping timeout: 264 seconds). 14:56:22 -!- Kaynato has joined. 15:07:30 -!- bender has joined. 15:07:52 -!- bender has quit (Client Quit). 15:12:14 -!- moon_ has joined. 15:35:32 -!- spockers has quit (Remote host closed the connection). 16:14:15 -!- bauen1 has quit (Ping timeout: 264 seconds). 16:14:58 -!- Eatonion has joined. 16:15:14 hello 16:15:41 -!- Eatonion has changed nick to Etaoin. 16:17:38 -!- bauen1 has joined. 16:20:00 -!- Kaynato has quit (Ping timeout: 246 seconds). 16:36:49 -!- Etaoin has quit (Quit: Page closed). 16:39:59 -!- FreeFull has quit (Quit: BBL). 16:56:26 -!- spockers has joined. 17:14:49 The Y Chromosome: The human condition's expansion pack 17:16:26 -!- AnotherTest has joined. 17:49:00 Trump 0 AA! 17:49:06 (AA = After Apocalypse) 18:04:55 -!- hppavilion[2] has quit (Ping timeout: 252 seconds). 18:07:33 -!- copumpkin has quit (Quit: My MacBook Pro has gone to sleep. ZZZzzz…). 18:09:29 -!- APic has quit (Quit: leaving). 18:10:10 -!- APic has joined. 18:27:02 is nobody going to talk about lwan? https://lwan.ws/ 18:27:28 people are talking about it right now literally in every other channel on freenode 18:31:26 so it's like nginx as a library? 18:32:13 none of the channels I'm in are talking about it 18:32:21 dito 18:32:43 also, i would recommend to stay as far away from web development as possible 18:32:49 ^ 18:32:53 nothing good can come of it 18:32:59 try googling lolphp 18:33:12 i did php 18:33:57 is there a channel mode we can set to quarantine you? 18:34:14 /set mode -php 18:39:31 any server solution beyond 10,000 RPS is only useful when you are dealing with more than 10,000,000 RPS 18:39:40 not worth trying otherwise 18:40:09 (generally they come with severe trade-offs) 18:56:04 Let's talk about toonemes! 18:56:34 In cartooning, a tooneme is a component of a drawing which comprises the smallest cartonically meaningful unit. 18:57:08 Usually, one single line. 18:59:26 One eyebrow, one eyelid, one contour mark of whatever kind. 19:00:34 http://www.egscomics.com/index.php?id=1209 – look at all those toonemes! 19:02:19 There are some interesting toonemes in between the eyebrows in panel 6. Three of them. 19:03:45 "Angry forehead wrinkles", I suppose. 19:08:41 -!- ybden has quit (Quit: Fing). 19:11:08 -!- ybden has joined. 19:25:25 -!- augur has joined. 19:42:04 -!- jaboja has joined. 19:43:42 -!- FireFly has quit (Ping timeout: 260 seconds). 19:44:21 -!- FireFly has joined. 19:49:31 -!- FreeFull has joined. 20:06:51 -!- augur has quit (Remote host closed the connection). 20:07:35 -!- augur has joined. 20:12:09 -!- augur has quit (Ping timeout: 250 seconds). 20:34:47 Moo 20:47:46 <\oren\> baaa 20:58:38 -!- ais523 has joined. 20:59:17 -!- ais523 has quit (Client Quit). 21:03:51 -!- ais523 has joined. 21:16:40 -!- ais523 has quit (Remote host closed the connection). 21:16:41 -!- J_Arcane has joined. 21:16:49 -!- ais523 has joined. 21:19:54 -!- Frooxius has quit (Quit: *bubbles away*). 21:26:21 hey 21:26:28 hi 21:28:59 what do you do these days 21:30:03 research compiler development, for about a month 21:30:16 but I'm looking for a new job, this one's a fixed-term contract that expires soon 21:31:12 -!- MoALTz has quit (Ping timeout: 276 seconds). 21:32:06 find me one while you're at it ;P 21:39:45 -!- Reece` has joined. 21:41:04 -!- Frooxius has joined. 22:04:23 -!- Frooxius has quit (Ping timeout: 250 seconds). 22:04:25 -!- Reece` has quit (Read error: Connection reset by peer). 22:15:06 -!- hppavilion[1] has joined. 22:18:04 In this Dungeons&Dragons game story is one ogre is always cheating at dice (the dice are loaded so one always comes up 5 and the other one always comes up 2). We hear some ogre talking about one of them cheating at dice and one of them doubts it. To reverse the cheating, rub out the four corner dots of the five. Now they are certain to always lose at dice. 23:01:48 -!- Alcest has joined. 23:06:34 -!- augur has joined. 23:07:19 -!- Frooxius has joined. 23:09:59 -!- augur_ has joined. 23:11:36 -!- augur has quit (Ping timeout: 272 seconds). 23:20:27 -!- AnotherTest has quit (Quit: ZNC - http://znc.in). 23:20:51 -!- hppavilion[1] has quit (Ping timeout: 240 seconds).