00:00:03 http://logic.pdmi.ras.ru/~yumat/H10Pbook/ 00:00:47 http://logic.pdmi.ras.ru/~yumat/H10Pbook/bookcont.htm 00:01:49 ok 00:03:12 anyway for OR the solution isn't something you'll just look at and go "oh lol why couldn't i see that" 00:03:31 although anyone should be able to prove it 00:03:39 I don't think I give up yet 00:04:27 tell me if you do, and we can start talking about fixed-points of morphisms 00:04:48 why does that require knowledge of OR? 00:05:01 it doesn't, i just wanted to segway into it in an awkward way 00:05:06 :D 00:05:19 why 'of morphisms' isn't the theory just the same 00:05:55 well we use morphisms to get all sorts of avoidability results, because infinite words defined as fixed-points of morphisms have the fun property that we can do induction on them. 00:06:30 if the pattern XYX occurs in h^n(a), then it must occur in h^(n-1)(a) 00:06:30 o_o 00:06:44 this is still thue/monoid theory? 00:06:54 yep 00:07:10 topic is combinatorics on/of words, subtopic avoidability 00:07:33 thue is beautiful 00:07:39 possibly the simplest tc language ever 00:07:39 morphisms, by which i mean homomorphisms, are just a convenient way to get there 00:07:48 :P 00:07:49 it doesn't even have variables... or anything 00:08:03 you're a homo (morphism) 00:08:18 alise: it's the same thue at least 00:08:41 -!- AnMaster_ has joined. 00:08:44 oh and well i guess both are word stuff 00:08:53 oh not the language 00:08:57 boring :P 00:09:05 yeah 00:09:16 how do you write logical OR in Thue? 00:09:29 hm 00:09:30 it's easy 00:09:44 i forget the syntax but 00:09:49 0|0 -> 0 00:09:51 0|1 -> 1 00:09:58 1|0 -> 1 00:09:58 1|1 -> 1 00:10:22 it's hard to believe that such ... uncomputational rules can still have things like storage and plugging that storage into other things 00:11:30 I would say Thue is simpler than BCT 00:11:30 ignoring the IO fluff 00:11:45 it's basically [(string,string)] -> string -> string 00:12:38 and really all you do is... pick something from the array, find it in the program, replace by the second element, repeat 00:14:22 -!- AnMaster has quit (*.net *.split). 00:14:40 "i've been using ASP for years, but this is my first shot at something big in PHP, so i didn't even know there was a strip_tags function! wow ASP needs something like that lol" -- this was written in 2010 00:16:29 lol 00:16:47 -!- oerjan has joined. 00:19:36 Maybe I'll go to Norway, they have the Euro :P 00:19:37 er, no 00:19:59 was this sarcasm... 00:20:06 I thought they did? 00:20:16 certainly not 00:20:18 At least I remember reading they did. 00:20:57 we're not an EU member. not that that has stopped other countries from using the Euro. 00:21:26 the Scandinavians love their currencies 00:21:47 They are at least in Schengen. 00:21:50 huh; norway isn't an eu member? 00:21:58 my illusions are being shattered 00:22:08 does denmark at least have the euro 00:22:11 no 00:22:22 alise: you're an eu citizen and you don't know which countries are eu members? O_O 00:22:23 wtffffffffffff :| 00:22:25 of the Scandinavian countries, only Finland does 00:22:34 Norway has the coins with holes in them 00:22:41 oerjan: oh come on britain is barely an eu member :D 00:22:44 neither denmark, sweden or norway have the euro, although with different excuses 00:23:10 norway isn't an eu member, denmark has an exception and sweden pretends they have one ;D 00:23:20 *excemption 00:23:26 *exemption 00:23:43 * coppro has a sudden craving for donus 00:23:45 *donuts 00:23:59 good thing I live in Canada 00:24:00 and the rest of eu seem to pretend sweden does too, so it's de facto 00:24:17 coppro: whereabouts in canada do you live? 00:24:24 alise: Calgary 00:24:35 oerjan: Sweden is exploiting a loophole to avoid having to switch 00:24:37 expect me there roughly tomorrow 00:24:47 :P 00:24:52 have you guys sorted out your shitty government yet? 00:24:55 no :( 00:24:59 ETA? 00:25:14 2900 00:25:35 coppro: yeah but only sweden has a "permanent" permission to use that loophole iiuc 00:25:37 maybe i won't move to canada :P 00:26:01 other eastern members won't get to use it, although with the financial crisis the point is currently moot i think 00:26:26 (since they have a perfectly reasonable reason not to be able to reach the criteria) 00:26:30 (yet) 00:26:31 nooo, the recession is over - the banks are giving out bonuses again! 00:26:40 (paraphrased from reddit) 00:26:49 alise: now _that_ must be sarcasm 00:26:58 since they did that the whole time 00:27:15 yesterday a point of privilege was raised against a Minister in the House of Commons; if the Speaker allows it, the House will probably find him in contempt 00:27:31 coppro: ooh, scary 00:27:35 * oerjan snickers 00:27:38 oerjan: of course. 00:28:01 It is indeed amusing 00:28:01 coppro: in your government 00:28:11 do people shout at each other all the time 00:28:14 oh yes 00:28:20 iirc some tiny countries outside the EU also use the euro; andorra, monaco and san marino i think. 00:28:26 we took our system from you, remember? 00:28:34 and do you have a game where everyone in the party that's talking goes "ooooh" all the time 00:28:39 montenegro did at one time, not sure now 00:28:41 right 00:28:41 just checking 00:28:41 not canada then 00:29:32 and there's some west african franc or something that is linked to the euro iirc (used to be linked to the franc) 00:29:57 (a multinational african currency) 00:30:27 of course wikipedia has all this, probably where i read most of it 00:30:43 anyone want to fight with ggz to play reversi? 00:30:51 ask ais523 if you want to know how horrific it is 00:31:08 no, don't ask, just guess from my horrified reaction 00:31:10 -!- Oranjer has joined. 00:31:32 oerjan: Also the Vatican. 00:32:10 -!- Asztal has joined. 00:32:20 pikhq: darn i thought about it but forgot to write it :D 00:33:44 so guys remember when we were talking about the impossibility of having legal sex in the vatican 00:33:58 oh almost forgot, i got the summer job i mentioned. so i'll be proving properties of CA all summer \o/ 00:33:58 what if you had a friend who was a high-ranking catholic, and he let you have sex in his vatican residence 00:34:36 oklokok o_o 00:34:43 this is a JOB?? 00:34:44 ah also kosovo (unofficial) 00:35:53 oklokok is proving properties of california and, unofficially, kosovo 00:37:27 yes, job at uni 00:37:38 alise: Heheh. 00:37:55 "In addition, the convenient new function Total can now be used to efficiently add lists of numbers. " --Mathematica 5 00:37:59 EFFICIENTLY! 00:38:20 lol what 00:38:24 alise: all of Mathematica is inefficient unless special-cased 00:39:24 ais523: Seriously? 00:39:30 yes 00:39:41 but there's a lot of special-casing 00:39:47 and the special cases tend to be fast 00:39:50 it's one of the things I hate about it 00:39:53 most of mathematica is special cases yeah 00:39:56 really good benchmarks, but practically useless 00:40:05 pikhq: consider - the entire language is just tree rewriting 00:40:21 alise: ... And they implement it naively? 00:40:22 *shudder* 00:40:27 rewriting f[x_1,x_2,...,x_n] into another tree 00:40:43 So they special-case a ton of stuff so that it isn't horribly slow if you do what they want. 00:41:18 why thank you, i too think i'm the luckiest person in the whole fucking universe :) 00:41:45 oklokok: god i hate you 00:41:53 ah that's better 00:41:53 just die so that i can take your place :< 00:42:31 die... just die 00:42:42 <3 00:43:44 also... 00:43:53 the stuff they make me do will probably be like "write this trivial program to do X so we know if we're on the right track" 00:43:54 die :| 00:44:13 oklokok: assure me they will be formal proofs 00:46:12 i think it's faster to just write a python hack. 00:47:18 Sure it's faster. But less proofy! 00:47:37 oh well that's rather true 00:48:27 -!- MigoMipo has quit (Remote host closed the connection). 00:49:55 -!- BeholdMyGlory has quit (Remote host closed the connection). 00:58:42 a python-based proof system would be amusingorrible 00:59:39 card(NN)==aleph(0) 00:59:54 what's NN? 01:00:32 naturals 01:00:42 N is a bit too ambiguous by itself, and blackboard = double-striking 01:00:44 so NN is as good a name as any 01:00:46 double the naturality 01:01:19 heh 01:01:21 except NN looks like it could be NxN. or perhaps more likely, {mn | m,n \in N} 01:01:22 NN that's clever 01:01:48 in any of the three cases the statement is true 01:02:06 Sigma(QQp >> QQ, lambda f: ForAll(QQp, QQp, lambda e1, e2: abs(f(e1) - f(e2)) <= e1 + e2)) 01:02:15 the last notation is used for other things too 01:02:31 oklokok: well yeah, since NN=N for the last case 01:03:05 ugh alise you're making me ill :P 01:03:12 python doesn't even have a type system 01:03:40 that's why you give it one! 01:03:57 ooh I was talking to someone aboutthis 01:04:20 something about adding a type system to lisp 01:04:38 Qi 01:04:59 * fax doesnt likei Qi :[ 01:05:07 its like somem weird frankenstien 01:05:08 me neither 01:05:14 dunno why they made it 01:05:23 well I have nothing against them making it to be honest 01:05:32 just don't get why anyone other than the author gives a toss :P 01:05:50 >>> coerce(refl(), Eq(NN, 2+2, 1+3)) 01:05:55 http://vimeo.com/10297756 01:05:59 refl() :: Eq(NN, 4, 4) 01:06:08 i am so tempted to actually make this now 01:06:09 it would be so popular 01:06:36 -!- ais523 has quit (Remote host closed the connection). 01:06:55 -!- nooga has joined. 01:06:57 why do i always make too much food and eat all of it 01:06:58 tip for english speakers: when spelling german words, switch ei and ie around from what your flawed intuition tells you. hth. 01:07:14 EYEgenvalue 01:07:23 * fax still hs trouble with this 01:07:29 eeigenvalue 01:07:39 eiegenvalue 01:07:45 ~ egen - igen, egen - igen, lets call the whole thing off ~ 01:07:53 aaaaaaaaaaaaaaaigenvalue 01:08:08 oklokok: THERE ARE STARVING PEOPLE IN AFRICA YOU KNOW 01:08:29 card(NN)==card(QQ) 01:08:42 so... does that mean i should eat a lot or that i should not eat a lot? 01:09:01 oklokok: I think it means you should clear your plate. I don't know by what logic it means this. 01:09:42 i think i've seen the proof in preschool 01:10:14 oklokok: you should eat your food so you'll grow up to be a good missionary in africa, clearly 01:10:23 !Exists(NNp, NNp, NNp, NNp, lambda a, b, c, n: (a**n) + (b**n) == (c**n)) 01:10:26 preschool?? 01:10:29 You did set theory in preschool? :P 01:10:30 oerjan: Your interpretation is awesomesauce. 01:10:31 what the nell 01:10:45 fax: You didn't? 01:10:50 no 01:10:54 set theory in preschool would be awesome 01:10:57 I did this stuff at home 01:11:31 Gregor: also possibly realistic 01:11:49 My preschool was basically like this: Get there, finger paint, nap, ring theory, lunch, nap, recess, quantum mechanics, nap, dress-up, go home. 01:12:01 lol 01:12:29 Apparently there was a lot of napping. 01:12:35 A ridiculous amount, frankly. 01:12:35 i mean in my fantasy, the kind of people who tell their children there are starving people in africa to make them eat, are the same kind that would want their children to be missionaries 01:12:36 in? : {A:Set} -> (x:A) -> (B:Set) -> Decision (A === B) 01:12:49 fax: i was talking about the starving kids actually 01:13:04 when i was in preschool i think i was just as retarded as everyone else 01:13:06 ohh 01:13:32 well actually i was one of the two who could read and the other guy was a few years older 01:13:34 oklokok: hey python guy, is it possible to make "3" yield something other than an int 01:13:45 i don't know. 01:13:51 probably. 01:14:17 oklokok: well there seems to be a school of thought that says that when you don't like something you should think about how some other people have it worse. i've never understood how this is supposed to make me feel better. 01:14:20 i know very little about python's internals, which is a bit stupid because those are the whole point 01:14:35 ugh, what a waste 01:14:41 no Timbits left, and the library was closed 01:15:03 oerjan: schadenfreude best freude right 01:15:33 http://vimeo.com/10298933 01:15:37 part 2 ^ 01:16:29 -!- Sgeo has joined. 01:19:00 Anyone here? 01:19:05 yes 01:19:42 why would i eat like 800g of food when i'm full after like 400g 01:20:01 that video fucking rules 01:20:32 what's it about, my connection isn't fast enough to want to look without knowing 01:21:11 wooden 'cells' that can connect up on some conditions and separate on others 01:21:19 oklokok: Need an extra kg. 01:21:21 so basically the game of life 01:21:26 :P:P 01:21:27 (such is the American way) 01:21:29 so conglomerations of them can self replicate in some sense 01:22:20 i wish i lived in america, the land of dreams 01:23:05 Actually, it's the land of too much food. 01:23:51 -!- FireFly has quit (Quit: Leaving). 01:23:58 It is feasible to have a pound (approx. 2kg) of food in a meal here. 01:24:02 goddamn venti 01:24:05 Rather common, even. 01:24:06 goddamn qemu 01:24:07 pound = 500g 01:24:13 Erm. 01:24:21 THINKO SUCKS HARD 01:24:31 I don't get why people think that if some food is tasty more of that food is even tastier. :) 01:24:31 500g is a small breakfast 01:24:34 :D 01:24:45 AND I DIDNT MEAN 1 LBS. 01:24:52 WE OVEREAT MUCH MORE THAN THAT. 01:25:17 i believe that 01:25:29 i like breakfast 01:25:35 it's a very worthwhile kind of meal 01:25:49 it is 01:25:55 I wish I was better at it 01:26:15 coppro, breakfast isn't very difficult 01:26:28 difficult in what sense 01:26:29 you just need to get the basics down 01:26:31 quite :D 01:26:36 you get some things and then you put them in your mouth, and digest them 01:26:37 the trickiest part is having enough time 01:26:51 stop caring about obligations 01:26:53 :D 01:26:54 1 lbs. of meat, though, is quite feasible. Then another 1 lbs. of fries. And a half-gallon of soda. 01:27:06 alise: but the schoolteachers get angry! 01:27:09 ah 01:27:12 that sounds better 01:27:20 coppro: BIG WHOOP 01:27:28 and then my parents get angry 01:27:41 pikhq: American meals are more portions of barely-food lumped together than meals 01:27:41 coppro: BIG WHOOP 01:27:46 lol 01:27:53 alise: Yes. 01:27:57 coppro: just write an amazing mathematical work 01:28:00 Any plans for those machines? 01:28:02 sorted 01:28:12 alise: that sounds like effort 01:28:19 alise 01:28:31 coppro: but it's fun! 01:28:37 Alise: Terry Tao is becoming a finitist http://terrytao.wordpress.com/2010/03/19/a-computational-perspective-on-set-theory/ 01:28:46 * coppro is going to go do more calculus homework :/ 01:28:59 fax: does that make five? 01:29:07 I don't believe in five 01:29:07 so he can't be a finitist 01:29:11 I'm just kidding of course 01:29:26 there's just a little bit of finitism in there though 01:29:33 alise, 5 is trivial 01:29:47 no it is too big 01:29:55 I suppose you have some cubic explanation of the nonexistence of 5? 01:30:13 well my universe is finite right so every set gets a certain ration 01:30:20 and since some sets are just so much bigger than the naturals 01:30:24 and there are so many of them 01:30:30 the naturals only have the space for four elements 01:30:37 lol WHAT 01:30:40 does not follow 01:30:56 i don't believe in not following 01:31:00 i'm also a trivialist 01:31:20 * coppro wonders which unit is next... probably curve sketching. yay 01:31:49 curve sketching calculus homework? 01:31:56 coppro: curve sketching is boring as fuck but it's actually really useful if you just get good enough at it to not really have to think too hard to do it 01:32:23 alise, http://www.paulkabay.com/#trivialism seen this? 01:32:40 fax: yeah but i didn't have the attention span to read all the huge papers 01:32:49 how acn you be a true trivialist :P 01:32:54 i have like this limited obvious-parody attention span thing. 01:32:55 you are not working hard enough 01:33:14 actually i'm a mualist, no questions have "true" answers 01:33:33 fax: Yeah... 01:36:02 I am not sure it's a parody 01:36:13 I can see where you are coming from though 01:36:28 It is. 01:36:28 but not how fast he is going 01:36:33 lol 01:36:48 he says it's a parody right on that page 01:36:53 hmm 01:37:02 I don't wanna do my Agora duties :( 01:37:09 "I do not accept trivialism � I reject it! (Who wouldn�t reject it?) Reading this material may convince you that I am lying and that I really do believe this stuff � but that is because you have no sense of irony." 01:37:10 -!- nooga has quit (Ping timeout: 258 seconds). 01:37:13 coppro: So resign. 01:37:18 alise: that seems bad 01:37:24 I like them generally 01:37:36 it's just that with the lists down, that means extra effort to redirect them to a backup list 01:37:38 alise, I've seen that -- you're just taking it at face value 01:37:44 make a contract whereby someone else does them in return for some material reward by you 01:37:49 -!- nooga has joined. 01:37:52 *reward from you 01:38:00 fax: he uses it to debunk diaelethismsdfjksijf 01:38:02 however you spell it 01:38:46 oh, wonderful 01:39:06 the first question of this assignment (on curve sketching) is "Find the domain of y = sqrt(3x-5)." FUN 01:39:19 alise: He uses it to debunk gwandocu. 01:41:14 coppro: If complex numbers are "acceptable", then that's just [-inf, inf] :P 01:41:28 Gregor: heh, I wish 01:41:33 coppro: what's the domain of that function? the domain is that domain 01:41:37 it's not a tough question, it's just that I thought I was done with this stuff 01:42:24 Gregor: also, inclusive bounds on an infinity? 01:42:41 Idonno, maybe :P 01:42:44 coppro, Don't listne to Gregor, he's an infinitist! 01:42:58 Don't listen to fax, he's infantile! 01:43:01 that's a really bad question 01:43:15 oklopol geez what are you doing here 01:43:21 ...i don't know :< 01:43:26 Gregor: if complex numbers are acceptable, then the domain's C, clearly :) 01:43:36 i actually ate until now, although i guess i also did other things... 01:44:23 `addquote oklopol geez what are you doing here ...i don't know :< i actually ate until now, although i guess i also did other things... 01:44:26 no, the domain is obviously two rounds around C so you get the whole C as the range 01:44:33 oh wait 3x-5 01:44:35 well anyway 01:44:43 140| oklopol geez what are you doing here ...i don't know :< i actually ate until now, although i guess i also did other things... 01:44:43 * alise punches HackEgo 01:44:48 Gregor: fixit 01:44:48 thanks 01:44:55 oklokok: around 5/3, then 01:44:56 hmm, why was that quoteworthy? 01:45:04 it's amusing :P 01:45:04 yeah something like that 01:45:15 anyway- 01:45:16 what's the thing called when you go around multiple times? 01:45:18 riemann something 01:45:19 um what was i going to say 01:45:20 alise: Doesn't seem broken ... 01:45:34 oklokok: double reacharound 01:45:37 00:44 * alise punches HackEgo 01:45:37 Gregor: it lagged right until i told you to fix it :P 01:45:40 this made me laugh quite manically 01:45:43 * oerjan swats alise -----### 01:46:00 the reimann rock 01:46:03 oklopop 01:46:06 *riemann 01:46:27 "reimann" would be pronounced "ruymon" 01:46:29 http://en.wikipedia.org/wiki/Riemann_surface 01:46:34 as in buy 01:46:36 reimann, riemann... lets call the whole thing off 01:46:47 fax: have you been listening to that song a lot or something 01:46:56 oklokok: we already discussed that above 01:46:58 it happens in my head everytime 01:47:07 oerjan: yes, that's why i corrected it. 01:47:22 because people should learn things they're told. not that i do. 01:47:32 lets, let's, let(')s call the whole thing off 01:47:42 lol 01:52:56 so my laptop can rotate the screen 01:53:02 if i can get it in a nice holding position i can read papers like a real man 01:53:30 I wish the iPad was less DRM bullshit and more.. open source 01:53:37 alise: You mean with your eyes burning? 01:53:38 then I'd totally buy one and just lay in bed all day reading 01:53:44 fax: HAHAHAHAHAHAHAHAHAHAHAHAHAhasiudhdif 01:53:45 fax: You mean with your eyes burning? 01:53:53 Gregor: XD 01:53:58 by eyes burning?? 01:54:13 alise what's so funny? The only bad thing about the iPad is that it's closed 01:54:15 Gregor: Anyway, look, I haven't bought that monochrome laser printer yet 01:54:17 YET 01:54:19 Never read anything substantial on a backlit screen then? It's quite horrible. 01:54:29 Gregor I read all the time off the computer :S 01:54:30 fax: well apart from being totally useless for anything creative instead of consuming... 01:54:42 besides, apple, open source? 01:54:45 Gregor... although.. I do have the brigtness down at minimum 01:54:51 you must be kidding; only their internal software is open source 01:55:03 alise, yeah I know it's shit.. I'm saying if it was slightly different it would be good :| 01:55:13 basically: 01:55:21 Big touchscreen that can connect to the internet 01:55:31 yeah but it would require a whole change in apple's philosophy so the end result would be way different 01:55:39 fax: hellooooo crunchpad 01:55:42 :p 01:56:49 alise that was sad :( 01:56:56 http://techcrunch.com/2009/11/30/crunchpad-end/ 01:57:23