< 1270425618 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION sees a bunch of ][ in Lost Kingdom, and decides that removal of extreneous loops isn't a bad idea, even if it misses some extraneous loops < 1270425632 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Topological cream. < 1270425820 0 :mibygl!unknown@unknown.invalid QUIT :Quit: Page closed < 1270425857 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :I wish I had something sufficiently esoteric to present (to sort-of justify that we needed the channel in a usable state), but that Piet compiler I was hoping to advertise here is still a bit too unfinished. < 1270425905 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :(In the "ERROR:main.c:94:main: code should not be reached. Aborted (core dumped)" sense of unfinished.) < 1270425956 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hey ehird < 1270425966 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ever heard of finite fourie transform < 1270425974 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :finite fourier transform < 1270425974 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So I want a language where self-concatenation results in nop. < 1270425986 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So for all code x, xx = nop < 1270425991 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :fax: Yes.... < 1270425997 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::( < 1270426017 0 :BeholdMyGlory!unknown@unknown.invalid QUIT :Remote host closed the connection < 1270426031 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: that's probably easy if you don't also want concatenation to mean execution chaining :D < 1270426032 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Flip bit, *, is a self negating op. < 1270426061 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :otherwise, cpressey already tried that. (burro, was it?) < 1270426067 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: hey, cpressey managed it but hs inverses weren't thr same < 1270426069 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :His < 1270426078 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :They were different code iirc < 1270426105 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :say % moves cell < 1270426131 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :"If M, then move left; else move right. Toggle M.@ < 1270426140 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :*M." < 1270426146 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :%% is nop < 1270426148 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :oh true < 1270426155 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :xyxy wouldn't be nop < 1270426156 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Then suppose ! = toggle M < 1270426162 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :%!%! < 1270426171 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :even if primitive operations had that property < 1270426174 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :That's not nop. < 1270426189 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So let's say % doesn't toggle M. < 1270426200 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Then %!%! is a nop. < 1270426202 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :you would need xyx = y for all x,y, essentially < 1270426213 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :oh right, an _abelian_ group < 1270426222 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: well that's what im doing < 1270426226 0 :dbc!~daniel@130-94-161-238-dsl.hevanet.com JOIN :#esoteric < 1270426245 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :* flip; % if m then leftelse right; ! toggle m < 1270426246 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :you end up just xoring bits of features, that way < 1270426256 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*bit fields < 1270426258 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :this is ok so far, right? < 1270426272 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :%*!%*! < 1270426291 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :.0 0 0 < 1270426297 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :0 .0 0 < 1270426312 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :0 .1 0 (not m) < 1270426326 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :.0 1 0 (not m) < 1270426332 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :.1 1 0 < 1270426335 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :dammit < 1270426371 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: each operation would essentially be a flip of some set of bits < 1270426376 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :eliminate ! Then < 1270426387 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :> if m then right else left < 1270426397 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :< if m then left else right < 1270426402 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :both toggle m < 1270426417 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: new idea < 1270426428 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :p(reverse p) = nop < 1270426452 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :*>*< <*>* < 1270426462 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :1 0 0 0 < 1270426471 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :1 .0 0 0 < 1270426473 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :well that's easy since you only need each primitive operation to have that property < 1270426480 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :1 .1 0 0 < 1270426491 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :1 1 .0 0 < 1270426498 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :1 .1 0 0 < 1270426503 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :yeah that works < 1270426508 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :My optimizer stripped 1781 bytes off of Lost Kingdom < 1270426522 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: is pp = nop feasible < 1270426528 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :as in potentially tc? < 1270426534 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Or at least nontrivial < 1270426538 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i don't think so < 1270426565 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Then reversing it is. < 1270426592 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :since it has to be an abelian group, you could _sort_ the operations and it would be equivalent. obviously the only property remaining is whether each primitive operation is an even or odd number of times < 1270426594 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :symmys, is the name. < 1270426616 0 :calamari!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: nice < 1270426631 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :calamari, how so? < 1270426636 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: ha < 1270426640 0 :calamari!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: closer to 2 mb :P < 1270426677 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: ok what about pp=opposite of p < 1270426689 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: that just means ppp = nop, right? < 1270426689 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :This thing currently doesn't have the brains to run parts of code, see the result, and just put it back in < 1270426708 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: hmm.. yes, I suppose < 1270426748 0 :calamari!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: my bfbasic language produces rather bloated code, so I'm sure you can do better :) < 1270426761 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :that seems trickier to understand. hm. < 1270426771 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :calamari: it is truly hideous code! :) < 1270426781 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :calamari, the only effect my optimizer has is removing loops that occur immediately after loops < 1270426802 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION is curious about the [-][.] structure at the beginning < 1270426864 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Oppoppo would be a nice name for the pp=opposite p Lang. < 1270426881 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: obviously abelian groups made out of Z_3 parts will fulfil that, but i'm wondering if it can be non-abelian < 1270426940 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :hm for finite groups, now what was that theorem... < 1270426987 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1270427011 0 :calamari!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: ??? < 1270427029 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :No what I'll call "flat" code (code made up of +-<>) should need to change direction more than twice < 1270427045 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :calamari, Lost Kingdom begins with [-][.]. < 1270427050 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :erm, not the last . < 1270427056 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :I'm curious as to why < 1270427080 0 :calamari!unknown@unknown.invalid PRIVMSG #esoteric :maybe he added that on, but I don't see that in the actual compiler < 1270427101 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Erm, 3 times, not twice < 1270427107 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :[-][.] seems... dumb < 1270427117 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: It's omittable in its entirety. < 1270427130 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :coppro: I think that's a stripped out set of comment blocks? < 1270427143 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :p^3 = 1 can be non-abelian iirc < 1270427171 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :pikhq, my optimizer currently isn't perfect < 1270427172 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :3x3 upper triangle matrices < 1270427179 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :err no wait < 1270427181 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :It just emits loops after loops at this point < 1270427189 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Hrm. < 1270427214 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :well anyway there was some sort of example i'm too tired to come up with < 1270427226 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Also, it won't attempt to optimize + - < 1270427230 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :And I consider that a feature < 1270427304 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :hm sylow's theorem, but i'm not sure it helps < 1270427307 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*theorems < 1270427339 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: oh fine < 1270427356 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i'm trying to find it but it seems the webpage of our algebra course is down < 1270427370 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :somehow you can do it with matrices < 1270427381 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :1 on the diagonal ofc < 1270427387 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: or how about p^length(p) = nop :) < 1270427394 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :now if it's finite it must have order 3^n, at least < 1270427415 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: aigh < 1270427454 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :hm actually that might give some restrictions < 1270427459 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :It occurs to me that loops nested thus: [++[-]] means that the outer loop doesn't need to be a loo\ < 1270427461 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :loop < 1270427469 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :so < 1270427473 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :** is nop < 1270427478 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :as is ****** < 1270427479 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: um wait then every primitive operation is a nop :D < 1270427481 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1270427489 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :((1 a b) (0 1 c) (0 0 1))^3 = ((1 2a (2b + ab)) (0 1 2c) (0 0 1)) ((1 a b) (0 1 c) (0 0 1)), so okay, the idea is you take a field with char 3 < 1270427493 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*^1 you see < 1270427495 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: er I mean < 1270427503 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :length+1 < 1270427508 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1270427520 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :********* is nop < 1270427532 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Or am I incorrect somehow? < 1270427561 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: how do you get the last one? < 1270427600 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: #*** = 3; ***^4 = ************ < 1270427601 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: the outer loop could still be done 0 or 1 times < 1270427622 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :#** = 2; **^3 = ****** < 1270427624 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Oh, right < 1270427624 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :huh < 1270427638 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: l*(l+1) is always even < 1270427650 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :right... < 1270427655 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :you are simply getting everything (**)^n < 1270427665 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :which is equivalent to having just ** < 1270427680 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :x^#x-1 = nop :D < 1270427693 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :okay checked < 1270427707 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :so nop from ** is ** < 1270427716 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :from ***, ****** < 1270427724 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :****, ************ < 1270427734 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so for p^3 = 1, you can take any field F with char(F) = 3, and the upper triangular matrices with 1 in the diagonal will be a non-abelian group with p^3 = 1 w.r.t. multiplication < 1270427762 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :everything except p^3 is obvious, i couldn't do that with ascii notation < 1270427775 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :would've been much easier to work out in my head < 1270427793 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :p^3 = 1 < 1270427816 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: still all even. and _you_ do realize that concatenating nops gives a nop, right? < 1270427837 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: i'm being silly < 1270427851 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :CAN WE PLEASE TALK ABOUT THESE GROUPS NOW < 1270427880 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: make em eso < 1270427889 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :groups are very eso < 1270427899 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :non-abelian ones < 1270427903 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :at least < 1270427907 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :groups don't exist < 1270427940 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: 3x3 matrices, you said? < 1270427951 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1270427975 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :so just 3 degrees of freedom... < 1270427998 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :p^63 = nop < 1270428003 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :happy? :P < 1270428005 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :what are degrees of freedom? i've heard of them but didn't really gut it < 1270428037 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :dimension of space, mostly? < 1270428058 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oh < 1270428060 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :cool :) < 1270428084 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :in statistics the explanation was really vague < 1270428090 0 :ehirdiphone!unknown@unknown.invalid QUIT :Quit: Get Colloquy for iPhone! http://mobile.colloquy.info < 1270428108 0 :ehirdiphone!~ehirdipho@82.132.139.144 JOIN :#esoteric < 1270428153 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :fizzie: you're still op >:) < 1270428176 0 :fax!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1270428189 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :[1 a b; 0 1 c; 0 0 1] [1 d e; 0 1 f; 0 0 1] = [1 d+a e+af+b; 0 1 f+c; 0 0 1] < 1270428204 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :if i did it correctly < 1270428212 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :iidic < 1270428276 0 :fax!~none@unaffiliated/fax JOIN :#esoteric < 1270428289 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ehird < 1270428338 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Fax < 1270428345 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hi < 1270428349 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :hi < 1270428372 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: looks plausible < 1270428375 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :will you still ignore me if I mention p, q and <-> fax < 1270428444 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :answer: yes < 1270428467 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :so M^2 = [1 2a 2b+ac; 0 1 2c; 0 0 1], M^3 = [1 3a 2b+ac+2ac+b; 0 1 3c; 0 0 1] = 0 if char. 3 < 1270428470 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I PMd you < 1270428477 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric := 1, yes < 1270428478 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :er, = 1 < 1270428497 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :cuz non-abelian < 1270428505 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :...and cuz matrix i guess < 1270428525 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :non-abelian doesn't apply when multiplying a matrix with itself, though < 1270428533 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :yo < 1270428562 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :yeah but you don't use 0 for identity in one place and 1 in another < 1270428573 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so because the group isn't altogether abelian, you'd use 1 < 1270428576 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :it was a typo :D < 1270428591 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :and 1 = identity matrix < 1270428596 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1270428599 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :02:47… oklopol: cuz non-abelian < 1270428600 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :02:47… oklopol: ...and cuz matrix i guess < 1270428606 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i included both reasons < 1270428630 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :WHATEVER < 1270428647 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :using Z_3 as the field, that gives 9 elements < 1270428650 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i mean because the 0 couldn't have been interpreted as the zero matrix < 1270428659 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :it would definitely still have been the identity matrix < 1270428680 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: oh, and it doesn't need to be a field, a commutative ring is sufficient < 1270428694 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so i think the non-abelian thing is a better reason- < 1270428695 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :*. < 1270428707 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :well sure < 1270428848 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :food -> < 1270428856 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :dog -> < 1270429135 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Dog food < 1270429245 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :now the _next_ question is, can we get an infinite group of this type with finitely many generators? < 1270429334 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :and then something whose word problem is unsolvable, to perhaps give us TC? < 1270429358 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :im TC < 1270429360 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :(turning crazy) < 1270429787 0 :Gracenotes!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1270429794 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :if you just have {a, b} and w^3 = 1 for all words, then you have an infinite amount of words and finite amt of generators, i think < 1270429810 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :and it's a group because p^-1 = pp < 1270429832 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ooh < 1270429837 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :"The Burnside problem, posed by William Burnside in 1902 and one of the oldest and most influential questions in group theory, asks whether a finitely generated group in which every element has finite order must necessarily be a finite group" < 1270429851 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :xD < 1270429854 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oh umm < 1270429856 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :DEAD END REACHED < 1270429862 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :yeah okay then there must be something wrong with mine < 1270429867 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone no the answer is no < 1270429878 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1270429882 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :it's not entirely unanswered, mind you < 1270429884 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so no dead end < 1270429891 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :huh, isn't it completely answered? < 1270429897 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :could be < 1270429901 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :what about ppppp = nop < 1270429903 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i'm just reading the article < 1270429909 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i think it was by some russians < 1270429914 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: that falls under burnside too. < 1270429917 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :construction was like 200 pages < 1270429926 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :however, burnside is generally false, it seems < 1270429932 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :p^1001 = nop < 1270429932 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i just said that < 1270429939 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :yeah < 1270429942 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :the answer is no < 1270429960 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :also that's why construction an not proof < 1270429962 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :but that doesn't tell us which particular powers are possible < 1270429963 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :*and < 1270429989 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :ohhhhhhh < 1270429996 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :HA < 1270429997 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :okay i just realized what was wrong with my idea < 1270430005 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :TIME TO SEARCH FUCKERS < 1270430038 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :if you take {a, b}^3 and then take the free monoid with the constraint w^3 = 1, then also uw^3 = 1 for all u, w. so it's not a group, it's just a monoid < 1270430062 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so turns out the burnside problem of monoids can be answered by any fucker in a minute, but for groups it requires russians. < 1270430080 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :err {a, b}^* obviously < 1270430097 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: um any monoid in which everything has w^3 = 1 is a group < 1270430115 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :because you have an explicit inverse w^2 < 1270430125 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :hmm well umm yes < 1270430128 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so what's wrong < 1270430142 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :well you haven't proved it's actually infinite... < 1270430154 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :the thue morse word has no repetition of order more than 2 < 1270430159 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :take subwords < 1270430166 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :ah! < 1270430185 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :they need not be different < 1270430214 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :because you can expand any 1 < 1270430217 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :in the middle < 1270430289 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :"By contrast, very little is known when exponents are small, exponents 2,3,4 and 6 excepted." < 1270430341 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :in other words, it's probably still unsolved for many of them < 1270430357 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :but solved for 3, so probably it's finite then < 1270430441 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :okay what you need to do for semigroups is to add a 0 element and set uxxxv = 0 for all u, x, v < 1270430474 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :then you can find an infinite amount of words in a binary alphabet by taking thue-morse < 1270430530 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :and we have 0*u = 0 = u*0, obviously not a group < 1270430568 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :"B(m,3), B(m,4), and B(m,6) are finite for all m." < 1270430572 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :now for any substring of the thue-morse word, you can do no rewrites, because the 0 element doesn't occur and neither does a repetition of order 3 < 1270430593 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :m is the size of finite basis? < 1270430597 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(and B(m,2) is even simpler, it's what we discussed above) < 1270430600 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :yeah < 1270430601 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :or maybe not basis set of generators < 1270430609 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*yeah < 1270430777 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :"The particular case of B(2, 5) remains open: as of 2005[update], it is not known whether this group is finite. < 1270430794 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :of course it's finite < 1270430822 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :um and you know this how? :D < 1270430953 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I'm just saying random stuff sorry :( < 1270430972 0 :impomatic!unknown@unknown.invalid PRIVMSG #esoteric :There's a CROBOTs tournament at the end of the month if anyone want to take part < 1270431122 0 :fizzie!unknown@unknown.invalid MODE #esoteric :-o fizzie < 1270431134 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :(Oh, I completely forgot about that.) < 1270431650 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :"Moreover, the word and conjugacy problems were shown to be effectively solvable in B(m, n) both for the cases of odd and even exponents n." < 1270431677 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :so uh all exponents n < 1270431687 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :would be another way of saying that. < 1270431688 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :might mean it is hard to make something TC even if B(m, n) is infinite < 1270431730 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: well, it is at the end of a section where every other result _does_ distinguish odd and even < 1270431768 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :even being apparently more complicated in several respects < 1270431800 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :s/section/paragraph/ < 1270431930 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :also, http://en.wikipedia.org/wiki/Tarski_monster_group < 1270431952 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :those have some huge exponents though < 1270431953 0 :impomatic!unknown@unknown.invalid QUIT :Quit: ChatZilla 0.9.86 [Firefox 3.5.9/20100315083431] < 1270432026 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oho < 1270432031 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I lik monster groups < 1270432043 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I want to study moonshine but I have to learn some stuff first..... < 1270432050 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :that's not _the_ monster group though < 1270432054 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :yeah < 1270432060 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I didn't realize there was other ones actually < 1270432065 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :these are actually infinite < 1270432072 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oh :( < 1270432089 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :but have _only_ finite subgroups < 1270432100 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1270432101 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :and only of a particular, prime order < 1270432150 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :tarski & hutch < 1270432264 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone: there are google hits for that < 1270432330 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION somewhat mindboggles at a package that provides isBottom < 1270432449 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: there is a package by conal containing a function f such that < 1270432465 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :f _|_ y = y < 1270432472 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :f x _|_ = x < 1270432476 0 :charlls!charlls@166.237.150.123 JOIN :#esoteric < 1270432485 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :if neither are _|_, it returns either < 1270432508 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(psst: the one that evaluates first) < 1270432511 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :I guess it deals with nontermination by being whichever is .. riht < 1270432607 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Definition isBottom {A} (x : A) : bool := true. < 1270432610 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Erm < 1270432614 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :false < 1270432637 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ehird lol I just wrote that in #haskell a moment ago < 1270432645 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :heh < 1270432656 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :GET TO BED :| < 1270432662 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I want to try to program for a bit first < 1270432667 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :but it probably wont work and I'll go < 1270432691 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :do computable reals < 1270432704 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :prove some thing about them < 1270432795 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :every function on them is continuous, i hear. you could prove that. < 1270432798 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ehird yeah I have been meaning to write in the bit about reals from my book < 1270432807 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oerjan, I'm not sure if that is provable! < 1270432822 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :oh well < 1270432823 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oerjan, I think it's _true_ but may be sort of like the continuum hypothesis or similar < 1270432843 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I'm thinking interally though < 1270432850 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :like inside the type theory < 1270432858 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :yeah I hope I am not making this up < 1270432889 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hmm < 1270432902 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I suppose it's related to the unprovability of trichotomy < 1270432920 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :and trichotomy implies some pretty strong statements but I don't think it quite reaches P \/ ~P < 1270432932 0 :adam_d!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1270432958 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :fax: you can't prove the trichotomy for comp reals? < 1270432961 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I should try to get a better understand of this stuff < 1270432968 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :huh < 1270432972 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :and write a note on it or something < 1270432983 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I wonder if there's q middle ground < 1270432985 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :*a < 1270432988 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :this computable reals and analysis stuff (and meta theory) < 1270433018 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :maybe continued fractions? < 1270433043 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :continued frractions are something I am not very comfortable with... < 1270433051 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Why not? < 1270433058 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I never used them < 1270433072 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :1+1/1+1/... < 1270433079 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :there's the golden ratio < 1270433082 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :DONE < 1270433085 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric ::p < 1270433085 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I know that one :P < 1270433091 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :well i suppose it's about how if you have one real x and another real y then it can be that for every n they are closer than 1/n but you cannot prove it < 1270433100 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(prove forall ...) < 1270433102 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :can you solve every quadratic as a continued fraction? < 1270433105 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I'll play with them tomorrow I guess < 1270433123 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :fax: every real has a continued fraction < 1270433132 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Are there any BF optimizers that optimize back into BF code? < 1270433140 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Well Chaitins constant... < 1270433146 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: Yes < 1270433148 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :but you still must be able to define functions on them, and therefore any functions must also have their value close < 1270433157 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :x=(-b/a)+(-c/a)/x < 1270433157 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Same site as list kingdom < 1270433163 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Jonripley or sth < 1270433175 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :(-b/a)+(-c/a)/((-b/a)+(-c/a)/((-b/a)+(-c/a)/((-b/a)+(-c/a)... < 1270433176 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I guess < 1270433184 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :but that will never give a complex value < 1270433189 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :that can't be right < 1270433197 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :maybe it diverges on those cases < 1270433203 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I'll define continued fractions in coq tomorrow < 1270433213 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone, no unitness tomorrow? < 1270433230 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Not tomorrow. M < 1270433231 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :fax: quadratics have _periodic_ continued fractions iirc < 1270433238 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :and only they < 1270433246 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*roots of < 1270433261 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION doesn't see any optimization stuff on the site < 1270433273 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :well a continued fraction still has to be a function... < 1270433278 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :nat->nat < 1270433283 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :hmm < 1270433295 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :oh, well real ones i guess < 1270433316 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION pokes ehirdiphone  < 1270433336 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Search more < 1270433349 0 :charlls!unknown@unknown.invalid QUIT :Quit: Saliendo < 1270433354 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :hmm < 1270433404 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :wait does 0 have a continued fraction < 1270433423 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :0 = 0 + 0/(0 + 0/(0 + ... < 1270433431 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :0 repeated means that 0 = 0 + 1/0 = 1/0 < 1270433446 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone, are you sure there's something there? < 1270433449 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :but 0(1/0) =/= 1 < 1270433456 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: 80% < 1270433468 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :fax: oh 0/ < 1270433474 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION sees nothing relevant < 1270433483 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :is 0/ allowed in a continued fractin? < 1270433490 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :it must be... < 1270433493 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Just 1/ afaik < 1270433508 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric :0/ would be pretty dumb in a continued fraction < 1270433539 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :f : N -> N; R(f) = f(0) + 1/(f(1) + 1/...) < 1270433625 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiphone, I'm still not seeing it < 1270433630 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION should probably stop whining < 1270433645 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :im curious abuot the convergence of this continued fraction for quadratic < 1270433663 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: it's clearly been optimized away < 1270433690 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :fax: no, 1/ only in ordinary continued fractions < 1270433696 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ahhh < 1270433697 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :okay < 1270433701 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :If he has one, he either didn't realize the pointlessness of ][loop] < 1270433703 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :that makes things harder < 1270433704 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :well < 1270433708 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :1/infinity = 0 < 1270433716 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Or he doesn't run his own code through it < 1270433717 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :so what's the continued fraction for infinitY? < 1270433724 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :fax: 1/0 ? < 1270433725 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :1 + 1/0 I guess < 1270433731 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :so 0 = 0 + 1/infinty < 1270433748 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :so 0 = 0 + 1 /( 1 + 1 /( 0 + 1 /( < 1270433757 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i think 0 and infinity are sort of boundary cases < 1270433770 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :you just let the fraction _end_ there < 1270433779 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :f 0 := 1; f (S _) := 2 // sqrt 2 < 1270433787 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :or any integer for that matter. < 1270433816 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :it seems to orbit around e-4 < 1270433821 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :and not get smaller < 1270433838 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oh it's getting smaller... just takes some time < 1270433904 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I wonder which infinity it is < 1270433913 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :zero is all the same but infinity is all different < 1270433914 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :The tastiest one. < 1270433926 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :one of my favorite infinity is sqrt(2pi) < 1270433941 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :thats' 1 + 2 + 3 + 4 + 5 + ... IIRC < 1270433943 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :>_> < 1270433959 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :no sorry it's 1 * 2 * 3 * 4 * 5 * ... < 1270433970 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :1 + 2 + 3 + 4 + 5 + ... = -1/12 < 1270433981 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :clearly. < 1270434008 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :hey everyone makes mistakes < 1270434008 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::) < 1270434032 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :hey wait a minute. now _you_ are doing math and _i_ am saying random nonsense. < 1270434057 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :fax: also of course all rationals only have finite continued fractions < 1270434069 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :So really it is nat -> maybe nat < 1270434079 0 :sshc!unknown@unknown.invalid QUIT :Quit: leaving < 1270434084 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oerjan, the old 3/5-switch :) < 1270434089 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :(two; irrationals have one infinite one) < 1270434106 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :(fuck yeah I just referenced wiles proof of fermats lol theorem) < 1270434120 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :1 = 1/(0+1/(0+1/(... *whistles innocently* < 1270434136 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ehirdiPHONE can you prove that every rational is finite? < 1270434145 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :finite continued fraction < 1270434152 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I am sure that it is true but I wonder how to actually build it < 1270434156 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :fax: no but wikipedia can < 1270434163 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Euclidean algorithm < 1270434168 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Checkout < 1270434171 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :... < 1270434175 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Checkkit < 1270434180 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :>_> < 1270434187 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :induction on the size of numerator and denominator < 1270434210 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1270434252 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :s/and/+/ if you want a specific measure < 1270434300 0 :sshc!~sshc@unaffiliated/sshc JOIN :#esoteric < 1270434372 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :http://upload.wikimedia.org/math/f/9/7/f9729d86173eced1bc46aeb6087dada9.png <------ nice picture < 1270434417 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :but but... it's not fractal! < 1270434469 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :I like the . < 1270434481 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :The 0 at the end of the recurring 9s < 1270434623 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :New Autotune the news tomorrow! < 1270434711 0 :coppro!unknown@unknown.invalid PRIVMSG #esoteric ::( Autotune < 1270434720 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :obama the musical? < 1270434740 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ACTION googles that < 1270434776 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Autotune the news! < 1270434782 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Autotune the news! < 1270434789 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Everything sounds beeettet < 1270434792 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Beetter < 1270434796 0 :ehirdiphone!unknown@unknown.invalid PRIVMSG #esoteric :Autotuuuuuuned < 1270434847 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :These later ones tend to reference earlier ones < 1270434898 0 :jcp!unknown@unknown.invalid NICK :banbino < 1270434902 0 :banbino!unknown@unknown.invalid NICK :Banbino < 1270435040 0 :sshc!unknown@unknown.invalid QUIT :Quit: leaving < 1270435144 0 :Gracenotes!~person@wikipedia/Gracenotes JOIN :#esoteric < 1270435299 0 :Banbino!unknown@unknown.invalid NICK :jcp < 1270435565 0 :sshc!~sshc@unaffiliated/sshc JOIN :#esoteric < 1270435637 0 :ehirdiphone!unknown@unknown.invalid QUIT :Quit: Get Colloquy for iPhone! http://mobile.colloquy.info < 1270435730 0 :coppro!unknown@unknown.invalid QUIT :Quit: I am leaving. You are about to explode. < 1270435769 0 :coppro!~coppro@unaffiliated/coppro JOIN :#esoteric < 1270436072 0 :jcp!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1270436225 0 :sebbu2!~sebbu@ADijon-152-1-2-182.w83-194.abo.wanadoo.fr JOIN :#esoteric < 1270436273 0 :sebbu!unknown@unknown.invalid QUIT :Ping timeout: 276 seconds < 1270436274 0 :sebbu2!unknown@unknown.invalid NICK :sebbu < 1270436320 0 :EgoBot!unknown@unknown.invalid QUIT :Remote host closed the connection < 1270436321 0 :HackEgo!unknown@unknown.invalid QUIT :Remote host closed the connection < 1270436324 0 :HackEgo!~HackEgo@codu.xen.prgmr.com JOIN :#esoteric < 1270436326 0 :EgoBot!~EgoBot@codu.xen.prgmr.com JOIN :#esoteric < 1270436974 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1270437110 0 :sshc!unknown@unknown.invalid QUIT :Quit: leaving < 1270437274 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklopol < 1270437274 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :? < 1270437947 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :me? < 1270438022 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :ffffffff < 1270438028 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I can't remember what I was going to say to you < 1270438042 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oh yeah have you seen divisibility lattices? < 1270438172 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1270438219 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Lesse ... 1 is bottom ... is there a top? < 1270438231 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :well the top is the number you are factoring < 1270438232 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oh < 1270438235 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :obviously not < 1270438235 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :no I guess it's not < 1270438240 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :if you take all nats < 1270438243 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :what about infinity! < 1270438249 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :1*2*3*4*5*.. < 1270438250 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Who says you can't divide by infinity? < 1270438258 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :that's divisible by everything infinetly many times < 1270438266 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :that's the obvious way to make it bounded i guess < 1270438278 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :you add infinity to make it bounded? :D < 1270438326 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :well... yes :P < 1270438362 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :but now you must add more infinities, like 2*2*2*... >:) < 1270438385 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I wonder which ones have values and which dont < 1270438394 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :what do you mean? < 1270438401 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :apparently harmonic series doesn't have a value < 1270438409 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :but I am not sure about htat.. < 1270438419 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :although 1*2*3*4*5*... is still on top, all primes divide it infinitely often < 1270438453 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :man I just can't understand this chapter < 1270439069 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :fax: don't be your brain's bitch < 1270439115 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :pain's bridge < 1270439159 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :seriously I have been working on this stuff for 3 days now < 1270439168 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :it's very difficult < 1270439170 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I am not Gauss < 1270439186 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :completely degaussed, in fact < 1270439192 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :..................................................... lol < 1270439203 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :okay seems the divisibility lattices are distributive < 1270439234 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :it's just the sum of one N lattice per prime, isn't it < 1270439280 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklopol, how dod you prove it? < 1270439293 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i proved it using the cool characterization i mentioned < 1270439296 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(that's how you can use it to program in fractran) < 1270439298 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :yes I want to see :))) < 1270439300 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :in burris' book on universal algebra < 1270439303 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :did you find two numbers? < 1270439309 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :one for each of those lattices < 1270439314 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oh it's really easy to prove < 1270439325 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :you can just check it yourself if you know the characterization < 1270439333 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :dunno if it's easy from the definition < 1270439360 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :idea was to try both to see how much better the characterization is in action, but i'm not sure i have the energy now < 1270439389 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: how do you define the sum of two lattices? < 1270439401 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :of an infinite number of them, actually... < 1270439411 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :oh wait < 1270439418 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :like (x, y) <= (z, w) iff x <= z, y <= w? < 1270439424 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :yes. < 1270439441 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :although i realized only a finite number can be different from 0 < 1270439441 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :and that extended to infinite products < 1270439455 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :hmm < 1270439474 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :which is analogous to sums of modules/abelian groups < 1270439486 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :vs. products that are unrestricted < 1270439505 0 :fax!unknown@unknown.invalid QUIT :Quit: Lost terminal < 1270439534 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :also one thing i remember about distributive lattice is that they are exactly the sublattices of boolean algebras < 1270439540 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*lattices < 1270439552 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :okay so we can take the sublattice of N^P generated by the individual primes, maybe < 1270439564 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :they are?!? < 1270439569 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :that's an even cooler characterization. < 1270439571 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :yes iirc < 1270439585 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :there's a whole chapter about boolean algebras in the universal algebra book < 1270439596 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :unfortunately not in the exam so i'm probably not going to read it anytime soon < 1270439640 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :one way of showing this is that _both_ classes of algebras have only {0,1} as their subdirectly irreducible members < 1270439661 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(up to isomorphism) < 1270439729 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :there's probably a less heavy-weight method, i just happened to learn about subdirectly irreducible algebras once < 1270439741 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :okay i've actually proved the former < 1270439755 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :proved what? < 1270439768 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :err < 1270439781 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i seem to have expanded both and said former about one of the two < 1270439788 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i've proved that for distributive lattices < 1270439810 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :proved _what_ for distributive lattices? < 1270439816 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :xD < 1270439819 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :err < 1270439839 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :that the class of distributive lattices has only {0,1} as a subdirectly irreducible member < 1270439850 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :Exercise 1.11. Show that a distributive lattice is subdirectly irreducible if and only if it < 1270439850 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :is a 2-element lattice. < 1270439855 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ah. < 1270439869 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :harder than it sounds, that one < 1270439874 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :from this it should be trivial actually < 1270439881 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :you don't need the other one < 1270439882 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :it should, huh. < 1270439914 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :just note that a product of 2-element lattices is also a boolean algebra < 1270439933 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :subdirect irreducability still feels a bit strange to me, don't see how that's useful directly, but i'm all ears < 1270439942 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oh < 1270439949 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :hmm < 1270439975 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :well the thing is every algebra is a subdirect product of irreducible ones < 1270439992 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :yes < 1270439995 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :where a subdirect product is a special kind of subalgebra of a product < 1270439997 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :right < 1270440013 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :yeah i know what it is, and i'm starting to see how the proof would go < 1270440066 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so umm first of all every distributive algebra must be a subdirect product of {0, 1}'s, which are boolean algebras < 1270440074 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :yep < 1270440080 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*lattice < 1270440088 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :err right < 1270440099 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :but why is the subdirect embedding also a boolean algebra? < 1270440107 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :or wait is that obvious < 1270440119 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :it's not, it's a _sublattice_ of one < 1270440135 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oh lol < 1270440142 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :okay so actually it is totally trivial < 1270440166 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :once you get the lemma proved < 1270440180 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :yeah < 1270440246 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :the idea for the lemma is there's a very strong characterization for the smallest congruence relation C(a, b) equating a and b, so if there are three elements, and C(a, c) and C(b, c) both contain (a, b), you can use the characterization to prove a = b < 1270440269 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so you can separate any pair by a nontrivial congruence, which is equivalent to not being subdirectly irreducible < 1270440278 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i'm not sure why i told you that < 1270440285 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :maybe just because i remembered it. < 1270440347 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i actually had this really complicated proof with pictures and shit, the other guy on the course had a short algebraic proof and said "i have no idea what i actually did here, but it seems to be correct" < 1270440399 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i have many more uninteresting stories, if you wanna hear < 1270440400 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ok. when i learned about subdirect products i just played around with defining congruences. iirc a /\ x = a /\ y gives a congruence, and similarly for \/ < 1270440417 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :or rather, i though in terms of quotients < 1270440420 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*thought < 1270440464 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :and these congruences exist both for distributive lattices and for boolean algebras < 1270440502 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :(boolean algebras sort of are distributive lattices, so isn't that obvious) < 1270440507 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :(?) < 1270440524 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :well yes as long as you prove "not" is also preserved < 1270440538 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :hmm right < 1270440630 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :"oerjan: where a subdirect product is a special kind of subalgebra of a product" <<< why leave this open, it means it's surjective w.r.t. any individual index of the product < 1270440653 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :a /\ ~(a /\ x) = a /\ ~a \/ a /\ ~x = a /\ ~x < 1270440660 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i don't like it when people leave things out of definitions, everything starts feeling all blurry and scary < 1270440680 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :that's not a very clear definition < 1270440703 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: so wait what did that prove exactly < 1270440722 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :that ~ is preserved by the congruence. at least i think it implies it. < 1270440750 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: well just after i said that you told you already knew about it < 1270440752 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :let's see if i can even see what it means to be preserved by a congruence... < 1270440776 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :oh < 1270440786 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: yes, i didn't mean "why did you leave this open", i just needed to fill it < 1270440788 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i'm still thinking in terms of quotients, you see < 1270440791 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :**you* < 1270440799 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oh umm hmm right < 1270440851 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :the map x -> a /\ x is a quotient map, if you redefine the operations on the range by applying extra a /\ ... liberally < 1270440869 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :a is just some element you choose? < 1270440873 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :yeah < 1270440882 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :and quotient maps give congruences, of course < 1270440899 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :um i shouldn't even call it quotient < 1270440906 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :homomorphism < 1270440913 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :the kernel is a congruence < 1270440914 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :yeah < 1270440934 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :it's just isomorphic to the quotient of the congruence < 1270440967 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :yes, by the famous whatevermorphism theorem < 1270440995 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :so essentially all you have to prove is that applying a /\ ... liberally on the right side _does_ make it a homomorphism < 1270441027 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :and the above equation does that for ~ < 1270441061 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so you proved h(~(h(x))) = h(~x)? < 1270441068 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :for /\ it's almost trivial, and for \/ you need the distributive law < 1270441069 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :where h is the homom < 1270441085 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :well yeah < 1270441105 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :where h is the map < 1270441133 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :shouldn't you prove ~h(x) = h(~x), that is, ~(a ^ x) = a ^ ~x < 1270441139 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :wait... < 1270441150 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i think i'm a bit lost. < 1270441166 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :nope the thing is that we don't use the same operations on the range (even if it is a subset) < 1270441190 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :we use the operations with the h liberally reapplied at the end < 1270441215 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so like ~y : range = a ^ ~y : domain < 1270441216 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :so we're defining a new algebra which just happens to share some points < 1270441223 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :yeah < 1270441265 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :and this works very well for distributive lattices and boolean algebras < 1270441290 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i also played around with doing it for heyting algebras < 1270441306 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i got kripke models that way < 1270441448 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(heyting algebras are to intuitionistic logic what boolean algebras are to boolean logic) < 1270441463 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :okay i finally get your one-liner up there. < 1270441471 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :the range vs domain issue was a bit confusing < 1270441511 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oh they are now? i just know they have ->. < 1270441532 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :and i remember most of the axioms < 1270441569 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ah yes. i guess the fact i could do this was a kind of an epiphany, made it much simpler to find congruences < 1270441583 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :do you know cylindrical algebras of dimension n and n-valued post algebras? < 1270441591 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :heck no < 1270441627 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :okay those were the two weirder examples of algebras in the book < 1270441690 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :was just wondering because you seem to have an intimate relationship with all the others < 1270441707 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i had never heard of heyting algebras either < 1270441720 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :boolean algebras i had heard of, surprisingly enough < 1270441725 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :iirc i found in an _irreducible_ heyting algebra that a \/ b is true iff either a is true or b is true, where "is true" means is equal to the true element < 1270441774 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :what does true mean? :) < 1270441792 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :x is true iff 1 -> x or something? < 1270441794 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :eh < 1270441797 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :what does that even mean < 1270441804 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :let me rethink < 1270441807 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :well 1 is the true element i guess < 1270441825 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so x is true means x = 1? < 1270441828 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :yeah < 1270441851 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :was that subdirectly irreducible or directly? < 1270441865 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :subdirectly < 1270441879 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i don't know which is more common, prolly subdirect because of the problems direct has < 1270441881 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :that's what i was dabbling with at the time < 1270441890 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :right, right < 1270441934 0 :calamari!unknown@unknown.invalid QUIT :Ping timeout: 276 seconds < 1270441978 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :well, it was about time this channel had an interesting conversation, i thank you for that. i should get back to my stuffs now < 1270441993 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i also _think_ that if x is not 0, then there is a heyting algebra homomorphism sending x to 1 != 0 < 1270442032 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :there's too much axioms for me to wanna try that straight from the definition < 1270442065 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :actually not that many but anyway < 1270442068 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :well it may have been just using a map like x /\ ... and the above trick < 1270442086 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :or possibly x => ... < 1270442089 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :I.. think, now that I understand how to use StateT, the actual implentation of the interpreter just became trivial < 1270442090 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :*-> < 1270442100 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: heh < 1270442122 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Although not quite.. I don't think sequence does quite what I want it to do < 1270442145 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Actually, hm. That "trivial" function doesn't quite ty.. n/m < 1270442150 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :sequence does them one after the other, passing each state to the next, iirc < 1270442168 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(afa state is concerned) < 1270442213 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION was wrongly thinking that the thing for , would be StateT Tape IO Char, but it is StateT Tape IO (), just like everything else < 1270442336 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo_: what did you want sequence for? < 1270442347 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :maybe sequence_ would be better? < 1270442369 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :(you're not interested in any results not in the state, so) < 1270442405 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :oerjan, getting my point about being confused across, I know the difference < 1270442429 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ok < 1270442489 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Besides, if I want to use sequence, I can always use (const () . ) (sequence_ $) < 1270442498 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Um, don't know if that's exactly what I'd use < 1270442508 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Also, no _ obviously < 1270442516 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION is not quite a master of pointfree < 1270442555 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :const () `fmap` < 1270442574 0 :jcp!unknown@unknown.invalid QUIT :Quit: I will do anything (almost) for a new router. < 1270442640 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :however, i think sequence_ sometimes is more tail recursive < 1270442667 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :since it doesn't need to put on the return value remembered < 1270442737 0 :calamari!~calamari@ip70-162-184-104.ph.ph.cox.net JOIN :#esoteric < 1270442895 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Going to go eat now < 1270442907 0 :sshc!~sshc@unaffiliated/sshc JOIN :#esoteric < 1270443317 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Would you say it's complete and utter overkill to use Linux to make a disk image that does the following: run LostKng? < 1270443419 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :s/use.*: // *whistles innocently* < 1270443444 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :oerjan: Hah. < 1270443862 0 :lament!unknown@unknown.invalid QUIT :Ping timeout: 264 seconds < 1270443894 0 :augur!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1270444485 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :legalify = cmdsToBF . parseBF -- Turns any string into legal BF < 1270444505 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Well, not checking for hitting the left edge or negatives or anything < 1270444675 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :any string already is legal BF, unless it has mismatched brackets >:) < 1270444707 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :legalify fixes mismatched brackets < 1270444715 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ok then < 1270444728 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Although fixing might not be what's wanted < 1270444739 0 :lament!~lament@S0106002312fa554a.vc.shawcable.net JOIN :#esoteric < 1270444760 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :(truncating at the first extra ], and adding ] if there were extra [) < 1270444803 0 :augur!~augur@216-164-33-76.c3-0.slvr-ubr1.lnh-slvr.md.cable.rcn.com JOIN :#esoteric < 1270444889 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1270444977 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :oerjan, does sequence_ work well with infinite lists? < 1270445002 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i think so < 1270445040 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :sequence_ = foldr (>>) (return ()) < 1270445044 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :sequence = fold.. was about to ask < 1270445061 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Might have said foldl though :/ < 1270445077 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :well, sequence_, yeah < 1270445115 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :Well, with >>, there's supposed to be no difference, right? < 1270445120 0 :Sgeo_!unknown@unknown.invalid PRIVMSG #esoteric :And foldr works with infinite lists < 1270445139 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :i should think it's intended to be usable < 1270445195 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :as long as the monad used can handle it < 1270445630 0 :lament!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1270445899 0 :Oranjer!unknown@unknown.invalid PART #esoteric :? < 1270446353 0 :pikhq!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1270446584 0 :pikhq!~pikhq@75-106-123-198.cust.wildblue.net JOIN :#esoteric < 1270446771 0 :Sgeo_!unknown@unknown.invalid NICK :Sgeo < 1270447326 0 :lament!~lament@S0106002312fa554a.vc.shawcable.net JOIN :#esoteric < 1270449005 0 :lament!unknown@unknown.invalid QUIT :Remote host closed the connection < 1270449677 0 :adu!~ajr@pool-74-96-89-29.washdc.fios.verizon.net JOIN :#esoteric < 1270449977 0 :oerjan!unknown@unknown.invalid QUIT :Quit: Good night < 1270449986 0 :calamari!unknown@unknown.invalid QUIT :Quit: Leaving < 1270450764 0 :coppro!unknown@unknown.invalid QUIT :Quit: I am leaving. You are about to explode. < 1270451312 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :hey kidos < 1270452375 0 :FireFly!~firefly@unaffiliated/firefly JOIN :#esoteric < 1270453183 0 :adu!unknown@unknown.invalid PRIVMSG #esoteric :hi augur < 1270453191 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :who you < 1270453278 0 :Gracenotes!unknown@unknown.invalid QUIT :Quit: Leaving < 1270453537 0 :adu!unknown@unknown.invalid QUIT :Quit: adu < 1270454399 0 :clog!unknown@unknown.invalid QUIT :ended < 1270454400 0 :clog!unknown@unknown.invalid JOIN :#esoteric < 1270455468 0 :augur!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1270455490 0 :augur!~augur@216-164-33-76.c3-0.slvr-ubr1.lnh-slvr.md.cable.rcn.com JOIN :#esoteric < 1270456914 0 :Gracenotes!~person@wikipedia/Gracenotes JOIN :#esoteric < 1270456955 0 :adu!~ajr@pool-74-96-89-29.washdc.fios.verizon.net JOIN :#esoteric < 1270459743 0 :lament!~lament@S0106002312fa554a.vc.shawcable.net JOIN :#esoteric < 1270461745 0 :lament!unknown@unknown.invalid QUIT :Ping timeout: 248 seconds < 1270461846 0 :jcp!unknown@unknown.invalid QUIT :Quit: I will do anything (almost) for a new router. < 1270461958 0 :tombom!~tombom@wikipedia/Tombomp JOIN :#esoteric < 1270462281 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :The more clear case of yesterday's banned two made a reasonable argument that the other ban was merely collateral damage, and that the subject might behave and contribute constructively. I don't know how true that is -- for all I know, it might be a Clever Ruse and they could be the same person -- but since it's not such a great chore to reapply the ban, and I'll be around reasonably well for the next some hours to monitor what happen < 1270462281 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :s, I think I'm going to unban the other one. < 1270462283 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :If (s?he|it) decides to come back, you might consider explaining that -- while it may not always be apparent -- there's some sort of vaguely defined set of channel-appropriate behaviour; and while disagreeing is one thing, deliberately annoying people, at least for an extended amount of time, is another. < 1270462489 0 :ChanServ!unknown@unknown.invalid MODE #esoteric :+o fizzie < 1270462500 0 :fizzie!unknown@unknown.invalid MODE #esoteric :-b *!*@unaffiliated/quadrescence < 1270462503 0 :fizzie!unknown@unknown.invalid MODE #esoteric :-o fizzie < 1270463004 0 :Alex3012_!~chatzilla@ool-18b989d3.dyn.optonline.net JOIN :#esoteric < 1270463105 0 :Alex3012!unknown@unknown.invalid QUIT :Ping timeout: 276 seconds < 1270463114 0 :Alex3012_!unknown@unknown.invalid NICK :Alex3012 < 1270464944 0 :adam_d!~Adam@client-86-23-116-15.brhm.adsl.virginmedia.com JOIN :#esoteric < 1270467314 0 :BeholdMyGlory!~behold@unaffiliated/beholdmyglory JOIN :#esoteric < 1270467404 0 :Gracenotes!unknown@unknown.invalid QUIT :Quit: Leaving < 1270467926 0 :MizardX!~MizardX@unaffiliated/mizardx JOIN :#esoteric < 1270470632 0 :cheater2!unknown@unknown.invalid QUIT :Ping timeout: 276 seconds < 1270470895 0 :cheater2!~cheater@ip-80-226-20-226.vodafone-net.de JOIN :#esoteric < 1270471962 0 :ais523!~ais523@unaffiliated/ais523 JOIN :#esoteric < 1270472332 0 :adu_!~ajr@pool-173-66-9-50.washdc.fios.verizon.net JOIN :#esoteric < 1270472487 0 :adu!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1270473627 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ACTION wonders how a program on a single core, single cpu system, can have higher cpu time than wall time. < 1270473673 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :According to my watch it has been running for about 1.5 minutes, But cpu time in top of it is 3 minutes and 24 seconds < 1270473766 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, hi btw < 1270473820 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hi < 1270473895 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :any idea about the weird cpu time btw, ais523 ? < 1270473913 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :no < 1270473922 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm... are you overclocking/underclocking the system? < 1270473936 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it's possible that the CPU has a bogus idea of how much time it's taking, I suppose < 1270473947 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, ondemand cpu speed is in use < 1270473951 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :but no overclocking < 1270473984 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :but since this process is baiscally CPU bound it is eating about 99% of the CPU all the time < 1270473988 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm < 1270473991 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :so the system should be at top speed < 1270474004 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :yep, cpufreq-info confirms that system is running at 2 GHz < 1270474018 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :and there the process finished < 1270474025 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :so hard to tell now afterwards < 1270474082 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :(it was optipng running on a few thousand small png files btw) < 1270475647 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ACTION wonders how to write sort(1) in dd/sh < 1270476263 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :btw, is it just me, or has spam decreased drastically during the past 2 days or so < 1270476284 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I only got one spam during that period, normally I get something like 30 / day or so... < 1270476325 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, ^ < 1270476338 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I'm still getting just as much spam as before < 1270476342 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hm < 1270476360 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :pure chance then I guess < 1270476434 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :there should be some list with like "don't spam me, I'm too smart to fall for it". Sadly I guess that wouldn't work... < 1270476525 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :(I imagine it would work in a similar way to those block-telemarketing registers) < 1270476539 0 :adam_d_!~Adam@client-86-23-116-15.brhm.adsl.virginmedia.com JOIN :#esoteric < 1270476663 0 :adam_d!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1270477872 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :"./textures/cargo/explosives.png: Microsoft DirectDraw Surface (DDS), 128 x 128, DXT1" <-- Quite a lot of wtf here... 1) .png for THAT? 2) The game this is from uses OpenGL, not sure if it runs on windows at all... < 1270477924 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: those registers do work < 1270477935 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :at least in the UK, telemarketing companies don't want to be tracked down and fined < 1270477961 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :true < 1270478084 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, what I meant was that it wouldn't work for spam < 1270478093 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :no, it wouldn't < 1270478104 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :although, a spammer was arrested and fined in California recently < 1270478118 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it made the headlines, on the basis that nobody expected they'd actually catch one < 1270478150 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ah < 1270478286 0 :fax!~none@unaffiliated/fax JOIN :#esoteric < 1270478332 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Yeah, but most of them are probably A) unwilling participants in a botnet and/or B) not in a country that gives a shit. < 1270478638 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yep, the spammer in question was a business doing it deliberately, and even turned up in court to defend itself < 1270478650 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :which is also rather bizzare < 1270478868 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: Did I ever link http://codu.org/music/vg/gm1.ogg at you? < 1270478897 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :not sure < 1270478905 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ACTION wgets < 1270478935 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Gregor, piano, some sort of synth? < 1270478962 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :'s more video game music (created per request) < 1270478965 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :and hm... some string instrument < 1270478977 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :and huh, a lot more < 1270478980 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :OK, it's an odd ensemble :P < 1270478986 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Gregor, nice though < 1270478991 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :so far at least < 1270478999 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Gregor, was there a xylophone? < 1270479005 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, I generally like video game music < 1270479019 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: Nothing even similar :P < 1270479035 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ACTION plays it < 1270479051 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Gregor, some percussion thing that sounded somewhat wooden? < 1270479064 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :only for a very short period < 1270479074 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I assume that you're referring amusingly to the Shamisen :P < 1270479082 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Which is a plucked string instrument. < 1270479094 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :huh, never heard of Shamisen before < 1270479099 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :but yes very nice. < 1270479139 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Gregor, but please provide me a list of the instruments < 1270479150 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :also, for which video game was it created? < 1270479170 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Just a class project of a friend of a friend. < 1270479182 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I can do one better, I think ... < 1270479200 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :http://codu.org/music/vg/gm1.mid < 1270479206 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :http://codu.org/music/vg/gm1.rg even < 1270479245 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :aargh wth. That isn't the QT theme in rosegarden < 1270479253 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ACTION wonders why it is mostly black < 1270479261 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1270479263 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :it looks like a cross of blender and QT < 1270479266 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :awful < 1270479277 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :'snot supposed to look like that :P < 1270479290 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Gregor, yeah, let me check other QT apps... < 1270479305 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yay, I use Rosegarden to < 1270479305 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :kate looks normal < 1270479306 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :*too < 1270479314 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hm < 1270479320 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :konsole and Rosegarden are the only Qt apps I use regularly, and konsole is supposed to be mostly black :P < 1270479322 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: why does it go silent from 1:00 onwards? < 1270479338 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i like the theme 0.....0b3.....32e.....edge...... < 1270479342 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, it isn't? < 1270479349 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, maybe your download failed? < 1270479350 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :ais523: "It"? < 1270479353 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :or youy hit mute? < 1270479356 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: your music < 1270479363 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :with chromatic scale fedcba0123 < 1270479366 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :ais523: Yeah, that's a "you" fail, since it does not :P < 1270479375 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :OK, that's strange, I rewound past 1:00 and then it started working < 1270479377 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i guess it's pretty much the only theme < 1270479383 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Gregor, which version of rosegarden do you have? < 1270479396 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: 1.7.3 < 1270479419 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :10.02 here??? < 1270479426 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :what happened there < 1270479436 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :did they jump or something < 1270479442 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Guhhh ...? :P < 1270479461 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :http://www.rosegardenmusic.com/ < 1270479462 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Apparently they did. < 1270479468 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :aaargh it *is* supposed to look like that < 1270479477 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I just use whatever the latest in Debian is X-P < 1270479493 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Gregor, but the gui is supposed to look black, see screenshot on their website < 1270479495 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :how awful < 1270479508 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Oh, they're doing the retarded year = release number thing. < 1270479515 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :it doesn't even fit together < 1270479516 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :was there a matrix mode in rosegarden < 1270479523 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :since it seems to use the GTK style for some stuff < 1270479524 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: Sure < 1270479530 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :(as I set up qtconfig to do) < 1270479537 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :can you get it for win? < 1270479537 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :(because I like clearlooks) < 1270479538 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :But matrix mode is weird and pointless. < 1270479542 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :eh? < 1270479546 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :what do you compose in? < 1270479552 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :NOTATION < 1270479556 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :8| < 1270479559 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :you're insane < 1270479565 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :music notation is the worst thing ever invented < 1270479566 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :same as Gregor said. A lot easier that way < 1270479571 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :And/or actually a half-competent musician :P < 1270479585 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oklopol, also you record it mostly < 1270479600 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Right, yeah, I've got my digital piano plugged into my computer. < 1270479601 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :OK, something is /very/ wrong with Totem ATM < 1270479610 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: heh, I used to use NOTATION when I was on Windows < 1270479613 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :and then use some quantisise or whatever < 1270479617 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :forgot what it was called < 1270479633 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, is this a nodepad joke? < 1270479637 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :no < 1270479638 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :well sure if you like, but music notation is still a really ugly way to look at the result < 1270479648 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it's an actual program < 1270479654 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :it's not very good, but it's good /enough/ < 1270479656 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i mean unless piano music, then it's useful for playing sure < 1270479661 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :I actually do use matrix mode when I just record midi raw (and so, not conforming to any tempo) and want to edit it. Otherwise I record in notation mode because I can actually read and understand it ... < 1270479679 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and has a few brilliant interface fails, such as making it very difficult to figure out how to set one clef to treble clef and a different clef to base clef < 1270479694 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :STOP DISAGREEING WITH MY INSANE OPINIONS < 1270479740 0 :tombom_!~tombom@wikipedia/Tombomp JOIN :#esoteric < 1270479743 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i bet i've composed more music than you! (maybe not as much good music, but that's probably not relevant) < 1270479751 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :heh < 1270479783 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :That may or may not be true, I've thrown away vastly more music than I've kept. < 1270479807 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :But I guess when you make it that fine-grained, it all becomes meaningless :P < 1270479809 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :still the new GUI is completely awful. And it looks like three different people designed each half of it (!) without looking at each other's work. < 1270479810 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :during my whole two years of uni i think i've written like 4 songs or something :< i used to write one every few days at some point < 1270479824 0 :tombom!unknown@unknown.invalid QUIT :Ping timeout: 246 seconds < 1270479865 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ah found where to change it < 1270479865 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :yay < 1270479866 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: i think the best measure is to measure the amount of measures < 1270479875 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :...ever written < 1270479876 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :remove thick in preferences for "use thorn style" < 1270479889 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :which seems to be the codename of this release or something < 1270479897 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :þorn < 1270479927 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :but then does it count that i've written programs that generate random music and i've occasionally just let them generate hundreds of hours for funsies < 1270479942 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :WAIT if that counts then http://codu.org/algorhythms/ < 1270479945 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Gregor, huh, how did you manage to not make it play using the sound card? < 1270479946 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric ::D < 1270479963 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: I have an absurdly complicated system for recording via fluidsynth. < 1270479976 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Gregor, but that is a *.mid, not a *.rg < 1270479988 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, rosegarden doesn't seem to be working with timidity on this computer < 1270479996 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: Oh, from rosegarden; it's all configurable somewhere ... < 1270480003 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :okay something must be wrong on my side < 1270480004 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hm < 1270480006 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: And more specifically, http://codu.org/music/auto/OUT-T5.ogg (IIRC the link) < 1270480055 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ah found it < 1270480059 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :no sound font loaded < 1270480060 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :huh < 1270480070 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :that is supposed to happen in rc.local wonder what went wrong < 1270480084 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :ais523: fluidsynth is (way) better anyway (or at least, it would be if it wasn't hugely buggy) < 1270480102 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :meh, all I really care about is being able to hear the notes < 1270480134 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, any idea (on jaunty) how to run a custom command early on in boot. In fact it must be after the generic wireless stuff is loaded but before the specific driver for my wlan chipset is loaded. < 1270480140 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :so rc.local won't work < 1270480172 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Gregor, sb live 5.1 beats fluidsynth IMO < 1270480175 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: Is it sufficient to just unload the driver, do whatever you need to, then reload the driver? < 1270480198 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: Yes, probably, but producing recordings of it is annoying (well, OK, same for fluidsynth ... ) < 1270480214 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Gregor, yeah but it takes a few seconds for the interface to come down, so I would need to add something like: rmmod iwlagn && sleep 4 && iw reg set SE && modprobe iwlang < 1270480217 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :iwlagn* < 1270480218 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: last time I needed to do that I just added a script to init.d by hand, although I'm not sure that's the best way < 1270480234 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Gregor, it won't work right away < 1270480237 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :for unknown reason < 1270480262 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Well, then you're screwzored. < 1270480263 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ACTION wonders why iw reg set can't take effect on already up interfaces < 1270480275 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :or even down but with driver loaded < 1270480277 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :tried that too < 1270480353 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :strange; Timidity is working on its own, just not from Rosegarden, but Rosegarden says everything's fine with the MIDI < 1270480389 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Gregor, what game was it for? I don't think I asked that above, and if I did I either didn't get an answer or I didn't see the answer or I forgot it < 1270480424 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ah I did ask it, but didn't get an answer as far as I can tell < 1270480425 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: Just a class project of a friend of a friend. < 1270480445 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Sort of a StarCraft ripoff :P < 1270480447 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ah right < 1270480449 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :heh < 1270480470 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Gregor, starcraft is rts right? < 1270480474 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Yes < 1270480477 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: that's completely computer generated? < 1270480485 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i've just heard a few of these < 1270480493 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: OUT-T5 is computer-generated notes, human-generated dynamics < 1270480502 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, hm < 1270480512 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :okay so what does that mean exactly? < 1270480514 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, why timidity? < 1270480519 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :or maybe i should read the page < 1270480527 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: because I have it handy, for playing MIDI files < 1270480544 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: It means that it's more of an exercise in proving how important the human factor in playing music is than an exercise in proving how well a simple algorithm can compose :P < 1270480554 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and Rosegarden's supposed to work out of the box < 1270480560 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :with it < 1270480563 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, hm < 1270480580 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I never got timidity to _not_ crash < 1270480581 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :and did, on my last computer < 1270480587 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so... what does human-generated dynamics mean, you play something on the piano, and random notes are substitute? < 1270480587 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :it is the most unstable thing I ever seen < 1270480588 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :*d < 1270480617 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hmm, and it works fine from Totem < 1270480617 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i need technical details < 1270480642 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: Google for a program called Tapper (maybe "tapper conductor program" or something like that) < 1270480657 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ais523, fluidsynth is very nice to generate music files, but for playing midi directly I found it sometimes lags or such. So there I use the hardware synth on my sound card < 1270480669 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: With it, you take a MIDI file with no dynamics or tempo, and it reads the dynamics and tempo from playing on a digital piano, but uses the notes from the MIDI file. < 1270480701 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Gregor, dynamics include everything except the which note is played? < 1270480703 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: So I, the informed viewer of the notation, play it how I think it should sound, but don't play the actual notes (as they're borderline-impossible). < 1270480728 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :as in, how hard or soft you hit the key, when the note is played, the length of it, and so on? < 1270480738 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Basically. < 1270480745 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Gregor, what about the pedal? < 1270480782 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :(well pedals I guess. But I was thinking of sustain mainly) < 1270480822 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :That too. < 1270480840 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oh dynamics, right, i don't care about dynamics < 1270480846 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :huh < 1270480868 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :you can do that stuff arbitrarily, as long as it's consistent < 1270480874 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :Gregor, and I have to say http://codu.org/music/auto/OUT-T5.ogg wasn't very good < 1270480878 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :no offence meant < 1270480883 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :OUT-T5 has its moments < 1270480898 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :but there's not themes, so it's sort of non-music < 1270480901 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :*no < 1270480904 0 :alise!~alise@host86-138-199-235.range86-138.btcentralplus.com JOIN :#esoteric < 1270480907 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :moments of fits yes. < 1270480908 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :;P < 1270480925 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :the listener needs a clear melody they analyze < 1270480927 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :*can analyze < 1270480937 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oklopol, yes indeed < 1270480960 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :fax: Aye! < 1270481005 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :the usual listening process is as follows, you listen, write it on a matrix display in your head, try to find visual patterns, then hear those patterns in the music. < 1270481023 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :is it? < 1270481028 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :for me < 1270481032 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ah < 1270481034 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :for some reason that's enjoyable < 1270481103 0 :alise_!~alise@91.104.231.174 JOIN :#esoteric < 1270481111 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hi Alex3012 < 1270481113 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :errr < 1270481115 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :hi alise_ < 1270481117 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :I meant < 1270481134 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :ACTION wonders why the tab order was alise -> alex -> alise_ < 1270481136 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :should i wash the dishes and clean the apartment of just laze around the whole day < 1270481141 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oh wait, last spoken < 1270481163 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :what, some irc client is actually non-retarded enough to do that? < 1270481168 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: many :P < 1270481175 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oklopol, cleaning the apartment of just laze around for an entire day? < 1270481177 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :is it that large? < 1270481194 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i've tried irssi, xchat and mirc and then something with a bird none of them did < 1270481202 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oklopol, most clients can be set to do last spoken < 1270481208 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :and various webchats and other things i don't recall < 1270481212 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :xchat can definitely, pretty sure irssi can too < 1270481221 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: pidgin? < 1270481222 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :"can", python can do it too < 1270481222 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :but yeah I don't think it is default in xchat at least < 1270481226 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :xchat can do it yeah < 1270481228 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :it's just a setting < 1270481228 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :who gives a fuck, they *don't do it* < 1270481230 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :one flick to do < 1270481234 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oklopol, as in, there is a simple setting < 1270481239 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :a single checkbox or such < 1270481242 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so why isn't it on < 1270481244 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :prefs -> input box -> last spoken < 1270481250 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: 'cuz sometimes it's annoying < 1270481251 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oklopol, because many people don't want that I guess? < 1270481254 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :like if i'm talking to awesome < 1270481255 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :for hours < 1270481258 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :THOSE PEOPLE ARE WRONG < 1270481258 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :then suddenly asshole butts in < 1270481261 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and i end up talking to asshole < 1270481274 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :o_o < 1270481276 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :well umm SHUT UP < 1270481285 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :you too fax < 1270481288 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :sorry < 1270481289 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :nah jk < 1270481301 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :you don't have to shut up < 1270481310 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :but it helps < 1270481318 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :but you have to agree with me on something, i'm getting tired of being different < 1270481318 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, like: "a, you are an a person." and if "asshat" joins in between those two tab completes... < 1270481328 0 :deschutron!~alex@219-90-213-238.ip.adam.com.au JOIN :#esoteric < 1270481332 0 :alise!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1270481346 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :that's a great real life example < 1270481349 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster, you are an asshat person. < 1270481355 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :alise_ you're an alise_ person < 1270481371 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :alise_, yeah you can get mistakes like that < 1270481380 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :clearly it should be that I'm an awesome person < 1270481384 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :fax is a fax person < 1270481385 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::( < 1270481401 0 :AnMaster!unknown@unknown.invalid PRIVMSG #esoteric :oklopol, I know the example is far fetched! < 1270481404 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :that means frequent teleporter < 1270481469 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so i'm almost done with my bachelor's, and then i find the last algo i was gonna write up is completely wrong in the paper, and a lot of what i've written already uses it. < 1270481478 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :ouch < 1270481505 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :well assuming it's not my mistake, probably the case is that there's a simple way to fix it < 1270481527 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i'm sure it's wrong, but the problem is the author probably didn't have the algo wrong, but just explained it wrong < 1270481554 0 :oerjan!~oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1270481565 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i would explain it but what the algo does is a bit random without context < 1270481605 0 :deschutron!unknown@unknown.invalid PRIVMSG #esoteric :final year research project eh? < 1270481664 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :bachelor's, the first research project, not my own research, i basically just have to find sources and copypaste (in such a way that it shows the material went through my brain). < 1270481672 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :this is my second year < 1270481673 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :loll < 1270481731 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :the problem is i decided to read straight from journals and these papers are full of mistakes i only recently find myself having the skill to correct. which is a bit of a complicated sentence i guess < 1270481739 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :or not < 1270481746 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :also not that many mistakes actually < 1270481748 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :ouch < 1270481871 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :AnMaster: I didn't write it, so I don't care what you think :P < 1270481907 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: i liked the notes but the dynamics sucked ass! < 1270481915 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :*sobblecopter* :P < 1270481922 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :what about rhythm < 1270481925 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :was that yours? < 1270481929 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :No < 1270481934 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :...because that was pretty good too < 1270481938 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric ::P < 1270481966 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :shoppe tiem. < 1270481972 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :~~> < 1270481978 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :or wait maybe not just yet < 1270482034 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :~~~~~~~~~> < 1270482054 0 :deschutron!unknown@unknown.invalid QUIT :Ping timeout: 258 seconds < 1270482385 0 :deschutron!~alex@114-30-116-165.ip.adam.com.au JOIN :#esoteric < 1270482462 0 :deschutron!unknown@unknown.invalid PRIVMSG #esoteric :i see < 1270482547 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :okay now really shoppe tiem < 1270482615 0 :adu_!unknown@unknown.invalid QUIT :Quit: adu_ < 1270482840 0 :adam_d_!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1270482939 0 :adam_d_!~Adam@client-86-23-116-15.brhm.adsl.virginmedia.com JOIN :#esoteric < 1270483217 0 :adam_d_!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1270483459 0 :adam_d!~Adam@client-86-23-116-15.brhm.adsl.virginmedia.com JOIN :#esoteric < 1270484029 0 :adam_d!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1270484039 0 :adam_d!~Adam@client-86-23-116-15.brhm.adsl.virginmedia.com JOIN :#esoteric < 1270484174 0 :charlls!~charlls@201.226.222.130 JOIN :#esoteric < 1270484389 0 :oerjan!unknown@unknown.invalid QUIT :Quit: leaving < 1270484730 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :15:23 < benmachine> besides which there are languages which are deliberately obnoxious < 1270484734 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :15:23 < EvanR-work> right < 1270484736 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :15:24 < Jafet> PLEASE DO NAME ONE < 1270484792 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :which channel? I recognise Jafet from #nethack < 1270484804 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Malbolge's probably the best example of a deliberately obnoxious lang, though < 1270484815 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i recognize jafet from people pasting what he's said < 1270484849 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :lol < 1270484870 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :#haskell < 1270484882 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so maybe there too < 1270484959 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :fax: did you reply? < 1270484960 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: then why not also put the undynamic'd versions up? < 1270484976 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :no < 1270484977 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oh wait you do < 1270485000 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :I jost hjojddd < 1270485032 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oh wait maybe you don't < 1270485066 0 :deschutron!unknown@unknown.invalid PART #esoteric :? < 1270485107 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :hi ais523 < 1270485119 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :hi < 1270485166 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION is defining the reals via continued fractions in coq < 1270485337 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :call me 0400243514 and whatever thing finland has, i can't find my cellphone, won't answer < 1270485359 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :should be something like +358 prolly < 1270485436 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: who, me? < 1270485436 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :Callerying. < 1270485443 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :o---:) < 1270485444 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :whoever < 1270485444 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :thanks < 1270485448 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION looks up the dailing code < 1270485451 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :why do you want called < 1270485454 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :too late < 1270485456 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :why do you want called < 1270485460 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :fizzie called < 1270485465 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i told you < 1270485467 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :yeah it's +358 < 1270485473 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: what only one call accepted? < 1270485475 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :why would anyone want to talk on a phone?????? < 1270485479 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :fizzie: also good, now i can harrass you if i come to helsinki < 1270485488 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :I thought since I was in the same country, I'd best call just in case you were lying about the "no answer" thing. < 1270485493 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :fax: no one, cell phones are clocks you can find by calling them. < 1270485502 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oh < 1270485514 0 :adam_d_!~Adam@client-86-23-116-15.brhm.adsl.virginmedia.com JOIN :#esoteric < 1270485525 0 :fizzie!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: The number's on the first google-hit anyway, so no great loss there. < 1270485534 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric ::P < 1270485556 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :alise_: i don't mind if you call me < 1270485572 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :now the fucking shoppe -> < 1270485612 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oh won't answer < 1270485614 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :lame < 1270485617 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oh well < 1270485623 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i've talked to you on skype that is enough for one lifetime < 1270485624 0 :adam_d!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1270485667 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :I love the idea of having trouble finding your phone, and asking someone in another country over IRC to phone it so you can locate it < 1270485728 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :there is something so modern-international about that < 1270486016 0 :lament!~lament@S0106002312fa554a.vc.shawcable.net JOIN :#esoteric < 1270486207 0 :FireFly!unknown@unknown.invalid QUIT :Ping timeout: 268 seconds < 1270486347 0 :FireFly!~firefly@unaffiliated/firefly JOIN :#esoteric < 1270486780 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: They're there. < 1270486806 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: It's Onerously Uptight Toccata < 1270486811 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: Hence "OUT" < 1270486900 0 :adam_d_!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1270486935 0 :coppro!~coppro@unaffiliated/coppro JOIN :#esoteric < 1270486940 0 :coppro!unknown@unknown.invalid QUIT :Client Quit < 1270486981 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :what it was actually played? < 1270487053 0 :coppro!~coppro@unaffiliated/coppro JOIN :#esoteric < 1270487333 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :alise_: Sort of :P < 1270487365 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :link < 1270487572 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :http://codu.org/music/auto/OUT-T5.ogg < 1270487582 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :It was "played" with Tapper, so I played the dynamics and tempo, not the notes. < 1270487661 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :eh? < 1270487689 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I like it < 1270487776 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Tapper is a program that takes a MIDI file and lets you play the dynamics and tempo on a digital piano, replacing the notes you play with those from the original MIDI. < 1270487785 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :So when it's wildly impossible to play, you can still play it :P < 1270487998 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :Gregor: you have a gift for naming autogenerated music < 1270488016 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Random-adverb random-adjective random-type-of-music. < 1270488019 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Yes, quite the gift. < 1270488054 0 :adam_d_!~Adam@client-86-23-116-15.brhm.adsl.virginmedia.com JOIN :#esoteric < 1270488068 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yep < 1270488078 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ais523: the name is autogenerated too though :P < 1270488078 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :just you manage to pick particularly amusing random choices < 1270488093 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :Where by "you", you mean "rand()" :P < 1270488100 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :alise_: heh, then he has a gift for amusing random number generators < 1270488106 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :YES. < 1270488172 0 :charlesq__!~charlls@201.226.222.130 JOIN :#esoteric < 1270488379 0 :charlls!unknown@unknown.invalid QUIT :Ping timeout: 258 seconds < 1270488447 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :ais523: i've done it before, it's always either a finn who calls or no one :< < 1270488462 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :once someone tried to call me who was not in finland, but it didn't work < 1270488494 0 :charlesq__!unknown@unknown.invalid QUIT :Ping timeout: 258 seconds < 1270488497 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: ah < 1270488841 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: i can tryyyy < 1270488842 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :if you'll answer. < 1270488866 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :i will then < 1270488909 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :okayyyyyyyyyyyyy what is the number againyyyyyyyyyyy < 1270488926 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :0400243514 < 1270488945 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :now i need to get skype downloaded < 1270489017 0 :adam_d_!unknown@unknown.invalid QUIT :Ping timeout: 265 seconds < 1270489135 0 :coppro!unknown@unknown.invalid QUIT :Quit: boarding < 1270489213 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :(i seriously hope you don't actually do it... :P) < 1270489405 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :why not < 1270489429 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :because phone calls are scary < 1270489458 0 :lament!unknown@unknown.invalid QUIT :Ping timeout: 276 seconds < 1270491340 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :this will be so cool i could... < 1270491341 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :submarine it < 1270491638 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :ACTION is alarmingly tired < 1270491949 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1270494209 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :hey guyez < 1270494210 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :I wrote a function < 1270494213 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :http://pastie.org/904126.txt?key=dmlvdatdbqpi68fo3gwjg < 1270494263 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :http://pastie.org/904128.txt?key=x8d87tccpvmsig80c46r3w here's the auxiliary proof i used < 1270494271 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :totally by hand i swear < 1270494340 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :that's fucking beautiful man < 1270494449 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise_: Hmm. For a second there I was going "wait, it's Monday... What's he doing here..." XD < 1270494477 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: why's that funny < 1270494501 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: sorry to disappoint you man but this is what i actually wrote http://pastie.org/904133.txt?key=sgwgk3z0vdxdip61onraow < 1270494508 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :conclusion: computers are better at writing progams than humans < 1270494509 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*progams < 1270494512 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*programs < 1270494540 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: that omega is one wild-ass beast, you're in a proof right and it's to do with numbers right < 1270494542 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and you type omega < 1270494545 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :then you press '.' < 1270494552 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and it spits out something like http://pastie.org/904128.txt?key=x8d87tccpvmsig80c46r3w < 1270494556 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and WHAMM totally proved man < 1270494559 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :alise_: that's pretty too, but not nearly as. < 1270494568 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :eventually we'll just have OmegaCoq < 1270494578 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :alise_: Unit-ness. < 1270494580 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Theorem riemannhypothesis : blah blah blah. < 1270494582 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :omega. < 1270494583 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Qed. < 1270494594 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :pikhq: of course i mean why is it funny that you thought that i mean it's an obvious thing to think :P < 1270494594 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::/ < 1270494608 0 :pikhq!unknown@unknown.invalid PRIVMSG #esoteric :Ah. < 1270494613 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION defines rational and irrational : R -> Prop < 1270494647 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oh dear wait i need the continued fraction part to be optional < 1270494708 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION defines sqrt(2) < 1270494795 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Program CoFixpoint twos : CF := step 2 _ twos. < 1270494797 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :2 is not 0? < 1270494799 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :proved beyotch < 1270494807 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Program is beautiful < 1270494827 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Definition sqrt2 : R := real 1 (Some twos). < 1270494829 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :yeah some twos < 1270494831 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :just some of 'em < 1270494836 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :infinity of them to be precise < 1270494864 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :http://pastie.org/904145.txt?key=jynafvfiitwk3wphbwoqfq < 1270494870 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :here's what i need to do to prove that sqrt(2) is irrational < 1270494935 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :okay could we do as follows, you stop talking about coq till i learn it? < 1270494976 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: no :D < 1270494982 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :don't worry, the wildcard' stuff makes no fucking sense to me either < 1270494986 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :it's just coinduction wizardry... < 1270495005 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :seriously you should learn coq though, i'm pretty sure i could prove anything... even that the world is flat < 1270495008 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :that's how awesome it is < 1270495029 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :have you actually proven anything nontrivial? < 1270495043 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :sqrt(2) irrational is like elementary school biology homework < 1270495064 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklopol, he's not even shown that it's sqrt(2) < 1270495162 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: no :P < 1270495166 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i'm only doing this < 1270495169 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :to test my reals < 1270495172 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :via continued fractions < 1270495177 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Program CoFixpoint twos : CF := step 2 _ twos. < 1270495177 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Definition sqrt2 : R := real 1 (Some twos). < 1270495177 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Theorem sqrt2_irrational : irrational sqrt2. < 1270495177 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : intro i. < 1270495177 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : induction i. < 1270495178 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : simpl; auto. < 1270495180 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : assumption. < 1270495184 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :Qed. < 1270495185 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :and yes i didn't even prove it's the square root of two < 1270495188 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i have no... arithmetic, as such < 1270495210 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :fax: okay lulz. i just glance at the codes to assess their prettiness. < 1270495211 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: also, biology? < 1270495225 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :yeah biology, it's so easy it doesn't even need to be *math* homework < 1270495232 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :oklopl im mad at alise for being a dick to me < 1270495251 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :she was a dick to you? < 1270495255 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax thinks i'm a dick because i was talking to him then he demanded that i use his automatic primality prover before i do anything else < 1270495263 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :then he said if i don't do it right now she won't talk to me any more < 1270495265 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :*she < 1270495268 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fucking pronouns and irc < 1270495275 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :then I didn't, then she stopped talking to me < 1270495295 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :you are so short sighted alise that has nothing to do with it < 1270495308 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :alise_: it's not what you said, it's the way you said it < 1270495332 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :yawn < 1270495342 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :IT'S FUNNY TO ME < 1270495351 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :fax: i'm mad at her too now < 1270495367 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :http://fermatslasttheorem.blogspot.com/2006/05/basic-properties-of-cyclotomic.html < 1270495370 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fax: to be quite honest i am completely uninterested in talking to you if that involves continually doing exactly what you tell me to do before doing anything else < 1270495377 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :now let that be the end of it < 1270495435 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :no < 1270495512 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :no howso < 1270496048 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :In case anyone cares, the interpreter part of the interpreter was a bit easier than I thought it would be < 1270496062 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :Still need to make some tweaks though, but it can run Hello world < 1270496260 0 :charlls!~charlls@201.226.222.130 JOIN :#esoteric < 1270497130 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :fff < 1270497134 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :coq needs smarter pattern matching < 1270497250 0 :cheater2!unknown@unknown.invalid QUIT :Ping timeout: 264 seconds < 1270497396 0 :zzo38!~zzo38@h24-207-48-53.dlt.dccnet.com JOIN :#esoteric < 1270497401 0 :zzo38!unknown@unknown.invalid PRIVMSG #esoteric :Really, I ought to fix FlogScript uses all bcmath but I don't know the best way < 1270497440 0 :MigoMipo!~migomipo@84-217-11-143.tn.glocalnet.net JOIN :#esoteric < 1270497540 0 :cheater2!~cheater@ip-80-226-52-189.vodafone-net.de JOIN :#esoteric < 1270497567 0 :zzo38!unknown@unknown.invalid PART #esoteric :? < 1270497640 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :oklopol: more awesome noise: http://pastie.org/904213.txt?key=xwcjbezd3bn5212tsa0xwa < 1270497882 0 :tombom!~tombom@wikipedia/Tombomp JOIN :#esoteric < 1270497984 0 :tombom_!unknown@unknown.invalid QUIT :Ping timeout: 240 seconds < 1270498171 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :i got coq to print out "Anomaly. Please report." < 1270498219 0 :atrapado!~roper@46.188.116.91.dynamic.mundo-r.com JOIN :#esoteric < 1270498494 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :heh < 1270498662 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : H : nat < 1270498662 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : n : nat < 1270498662 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : wildcard' : n <> 0 < 1270498662 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : cf' : CF < 1270498662 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : H0 : rational (real H (Some (step n wildcard' cf'))) < 1270498664 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : ============================ < 1270498665 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : exists n0 : nat, rational (real n0 (Some cf')) < 1270498667 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ouch < 1270498674 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :that was /not/ the issue i was expecting with this function < 1270498696 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : H0 : rational (real H (Some (step n wildcard' cf'))) < 1270498696 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : ============================ < 1270498696 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : rational (real n (Some cf')) < 1270498722 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :basically i'm having to prove that a continued fraction is rational, given that the same fraction plus one extra term is rational < 1270498738 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :the problem arises if we expand what rational is shorthand for: < 1270498741 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : exists i : nat, is_None (a_Sn i (real n (Some cf'))) < 1270498751 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :where a_Sn is a rather complex recursive function. < 1270498798 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : H0 : is_None (a_Sn x (real H (Some (step n wildcard' cf')))) < 1270498799 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : ============================ < 1270498799 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric : is_None (a_Sn (pred x) (real n (Some cf'))) < 1270498800 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :this should be easier < 1270498998 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :ACTION rejiggles is_Some and is_None a bit to make things easier < 1270499573 0 :alise_!unknown@unknown.invalid PRIVMSG #esoteric :bye for a bit < 1270499575 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :jiggles? < 1270499577 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :bye < 1270499589 0 :alise_!unknown@unknown.invalid QUIT :Remote host closed the connection < 1270501231 0 :calamari!~calamari@ip70-162-184-104.ph.ph.cox.net JOIN :#esoteric < 1270501489 0 :charlls!unknown@unknown.invalid QUIT :Ping timeout: 258 seconds < 1270501803 0 :oobe!~hell@insidiousramblings.com JOIN :#esoteric < 1270501952 0 :jcp!unknown@unknown.invalid QUIT :Quit: I will do anything (almost) for a new router. < 1270502045 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :oobe: It's spelled "oboe" < 1270502072 0 :oobe!unknown@unknown.invalid PRIVMSG #esoteric :i think i know how to spell my own name < 1270502204 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :However, you shall now become the new pooppy (coppro) in my head :P. How about ... carlinet. < 1270502328 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :is oobe an actual norwegian name`? < 1270502329 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :*? < 1270502383 0 :oobe!unknown@unknown.invalid PRIVMSG #esoteric :nope < 1270502393 0 :oobe!unknown@unknown.invalid PRIVMSG #esoteric :its just my nick i use < 1270502423 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :oh sorry didn't notice your name is actually ascii pr0n < 1270502439 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric : \o/ < 1270502445 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric ::( < 1270502455 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :you're too short < 1270502465 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :so you don't get a body < 1270502465 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric : \o/ < 1270502469 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric : \o/ < 1270502469 0 :myndzi\!unknown@unknown.invalid PRIVMSG #esoteric :          | < 1270502469 0 :myndzi\!unknown@unknown.invalid PRIVMSG #esoteric :          |\ < 1270502484 0 :augur!unknown@unknown.invalid QUIT :Ping timeout: 276 seconds < 1270503126 0 :uorygl!unknown@unknown.invalid PRIVMSG #esoteric :I'm not sure I see the pr0n interpretation very well. < 1270503154 0 :oklopol!unknown@unknown.invalid PRIVMSG #esoteric :it was a complicated joke. < 1270503780 0 :charlls!~charlls@201.226.222.130 JOIN :#esoteric < 1270504511 0 :charlls!unknown@unknown.invalid QUIT :Quit: Saliendo < 1270504832 0 :tombom_!~tombom@wikipedia/Tombomp JOIN :#esoteric < 1270504934 0 :tombom!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1270505224 0 :tombom__!~tombom@86.25.52.173 JOIN :#esoteric < 1270505257 0 :tombom_!unknown@unknown.invalid QUIT :Ping timeout: 246 seconds < 1270505305 0 :jcp!~jw@bzflag/contributor/javawizard2539 JOIN :#esoteric < 1270505997 0 :MigoMipo!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1270506398 0 :augur!~augur@129-2-175-79.wireless.umd.edu JOIN :#esoteric < 1270506587 0 :augur!unknown@unknown.invalid PRIVMSG #esoteric :george carlinet < 1270506847 0 :alise!~alise___@212.183.140.38 JOIN :#esoteric < 1270506964 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :hi < 1270506971 0 :augur_!~augur@129-2-175-79.wireless.umd.edu JOIN :#esoteric < 1270506972 0 :augur!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1270506982 0 :augur_!unknown@unknown.invalid NICK :augur < 1270507095 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :anyone wanna do my proof for me < 1270507152 0 :fax!unknown@unknown.invalid PRIVMSG #esoteric :alise it's because you don't listen to me < 1270507167 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :k < 1270507396 0 :augur!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1270507418 0 :augur!~augur@129-2-175-79.wireless.umd.edu JOIN :#esoteric < 1270507532 0 :augur!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1270507536 0 :augur_!~augur@129-2-175-79.wireless.umd.edu JOIN :#esoteric < 1270507558 0 :augur_!unknown@unknown.invalid NICK :augur < 1270507569 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :MISSING: One underscore < 1270507571 0 :Gregor!unknown@unknown.invalid PRIVMSG #esoteric :REWARD: $0 < 1270507773 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : H0 : is_None (a_Sn x (real H (Some (step n wildcard' cf')))) < 1270507773 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : H1 : x <> 0 < 1270507774 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : ============================ < 1270507774 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : exists i : nat, is_None (a_Sn i (real n (Some cf'))) < 1270507774 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it's a start < 1270507804 0 :augur!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1270507852 0 :augur!~augur@129-2-175-79.wireless.umd.edu JOIN :#esoteric < 1270508037 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : H0 : is_None (CF_a_Sn x (step n wildcard' cf')) < 1270508038 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : H1 : x <> 0 < 1270508038 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : ============================ < 1270508038 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : is_None (CF_a_Sn (safe_pred x H1) cf') < 1270508041 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :this should honestly be really trivial :P < 1270508125 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it's tricky because it's not entirely clear from the definition of rational that you can traverse the (potentially infinite) list and reach an ending... < 1270508127 0 :olsner_!~salparot@c83-252-161-133.bredband.comhem.se JOIN :#esoteric < 1270508131 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Program Fixpoint Q_of_rational_CF (cf : CF) (H : exists n, rational (real n (Some cf))) : Q := < 1270508131 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : match cf with < 1270508131 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : | final n _ => Q_of_nat n < 1270508131 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : | step n _ cf' => Q_of_nat n + 1 / Q_of_rational_CF cf' _ < 1270508131 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : end % Q. < 1270508133 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :that's the entire function < 1270508141 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :the whole complexity is that tiny _ in the Q_of_rational_CF recursive call < 1270508145 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :because it's a bloody proof < 1270508163 0 :augur!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1270508167 0 :olsner_!unknown@unknown.invalid QUIT :Client Quit < 1270508187 0 :augur!~augur@129-2-175-79.wireless.umd.edu JOIN :#esoteric < 1270508283 0 :augur!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1270508295 0 :augur!~augur@129-2-175-79.wireless.umd.edu JOIN :#esoteric < 1270508402 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :gah, I'm stuck! < 1270508487 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :alise, hm? < 1270508498 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :trying to do this proof < 1270508595 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :http://pastie.org/904537.txt?key=rqxoszxqfg7nkfvbf8jwa < 1270508609 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I think I can think of Yet Another definition for rational/irrational that makes this easier < 1270508627 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :not based on the hugely complicated CF_a_Sn function < 1270508667 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :hmm ... no < 1270508669 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :I need CF_a_Sn to access elements < 1270508729 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :I think I failed to win Agora because I was inactive < 1270508920 0 :Gracenotes!~person@wikipedia/Gracenotes JOIN :#esoteric < 1270509007 0 :Sgeo!unknown@unknown.invalid PRIVMSG #esoteric :ACTION goes to play with some worms < 1270509115 0 :FireFly!unknown@unknown.invalid QUIT :Quit: Leaving < 1270509203 0 :tombom__!unknown@unknown.invalid QUIT :Quit: Leaving < 1270509605 0 :oerjan!~oerjan@hagbart.nvg.ntnu.no JOIN :#esoteric < 1270510087 0 :augur_!~augur@129-2-175-79.wireless.umd.edu JOIN :#esoteric < 1270510093 0 :augur!unknown@unknown.invalid QUIT :Read error: Connection reset by peer < 1270510246 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :Sgeo: i presume the computerised sort < 1270510341 0 :oerjan!unknown@unknown.invalid PRIVMSG #esoteric :"Nobody loves me, everybody hates me. Think I'll go and eat worms!" < 1270510394 0 :augur_!unknown@unknown.invalid QUIT :Ping timeout: 260 seconds < 1270510459 0 :ais523!unknown@unknown.invalid PRIVMSG #esoteric :yep, there was an accident and every active player won Agora < 1270510593 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :here's some wonderful noise: http://pastie.org/904583.txt?key=bg0znn8ou1ynm5vozuag < 1270510594 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :everything after exist (fun m : nat => m <> S n0) n0 < 1270510602 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :is a computer-generated proof that... drumroll... n is not S n < 1270510609 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :it actually gets cut off: < 1270510611 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : (fun .. => .. < 1270510611 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : .. < 1270510612 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : .. < 1270510612 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : .. < 1270510612 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric : end) I 0%Z Omega19 in < 1270510614 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :for being too absurdly long to display < 1270510643 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :can you imagine a proof of that identity even remotely as advanced before COMPUTERS???? < 1270510654 0 :oklopol!unknown@unknown.invalid QUIT :Ping timeout: 252 seconds < 1270510691 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :http://pastie.org/904585.txt?key=5ijpll8mfjaxlpcn9wthq < 1270510695 0 :alise!unknown@unknown.invalid PRIVMSG #esoteric :this definition is also acceptable. < 1270510930 0 :Oranjer!~HP_Admini@adsl-243-221-66.cae.bellsouth.net JOIN :#esoteric < 1270511754 0 :cheater3!~cheater@ip-80-226-15-69.vodafone-net.de JOIN :#esoteric < 1270511861 0 :cheater2!unknown@unknown.invalid QUIT :Ping timeout: 276 seconds