00:00:18 * Sgeo_ 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 00:00:32 Topological cream. 00:03:40 -!- mibygl has quit (Quit: Page closed). 00:04:17 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. 00:05:05 (In the "ERROR:main.c:94:main: code should not be reached. Aborted (core dumped)" sense of unfinished.) 00:05:56 hey ehird 00:06:06 ever heard of finite fourie transform 00:06:14 finite fourier transform 00:06:14 So I want a language where self-concatenation results in nop. 00:06:26 So for all code x, xx = nop 00:06:31 fax: Yes.... 00:06:37 :( 00:06:57 -!- BeholdMyGlory has quit (Remote host closed the connection). 00:07:11 ehirdiphone: that's probably easy if you don't also want concatenation to mean execution chaining :D 00:07:12 Flip bit, *, is a self negating op. 00:07:41 otherwise, cpressey already tried that. (burro, was it?) 00:07:47 oerjan: hey, cpressey managed it but hs inverses weren't thr same 00:07:49 His 00:07:58 They were different code iirc 00:08:25 say % moves cell 00:08:51 "If M, then move left; else move right. Toggle M.@ 00:09:00 *M." 00:09:06 %% is nop 00:09:08 oh true 00:09:15 xyxy wouldn't be nop 00:09:16 Then suppose ! = toggle M 00:09:22 %!%! 00:09:31 even if primitive operations had that property 00:09:34 That's not nop. 00:09:49 So let's say % doesn't toggle M. 00:10:00 Then %!%! is a nop. 00:10:02 you would need xyx = y for all x,y, essentially 00:10:13 oh right, an _abelian_ group 00:10:22 oerjan: well that's what im doing 00:10:26 -!- dbc has joined. 00:10:45 * flip; % if m then leftelse right; ! toggle m 00:10:46 you end up just xoring bits of features, that way 00:10:56 *bit fields 00:10:58 this is ok so far, right? 00:11:12 %*!%*! 00:11:31 .0 0 0 00:11:37 0 .0 0 00:11:52 0 .1 0 (not m) 00:12:06 .0 1 0 (not m) 00:12:12 .1 1 0 00:12:15 dammit 00:12:51 ehirdiphone: each operation would essentially be a flip of some set of bits 00:12:56 eliminate ! Then 00:13:07 > if m then right else left 00:13:17 < if m then left else right 00:13:22 both toggle m 00:13:37 oerjan: new idea 00:13:48 p(reverse p) = nop 00:14:12 *>*< <*>* 00:14:22 1 0 0 0 00:14:31 1 .0 0 0 00:14:33 well that's easy since you only need each primitive operation to have that property 00:14:40 1 .1 0 0 00:14:51 1 1 .0 0 00:14:58 1 .1 0 0 00:15:03 yeah that works 00:15:08 My optimizer stripped 1781 bytes off of Lost Kingdom 00:15:22 oerjan: is pp = nop feasible 00:15:28 as in potentially tc? 00:15:34 Or at least nontrivial 00:15:38 i don't think so 00:16:05 Then reversing it is. 00:16:32 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 00:16:34 symmys, is the name. 00:16:56 Sgeo_: nice 00:17:11 calamari, how so? 00:17:16 oerjan: ha 00:17:20 Sgeo_: closer to 2 mb :P 00:17:57 oerjan: ok what about pp=opposite of p 00:18:09 ehirdiphone: that just means ppp = nop, right? 00:18:09 This thing currently doesn't have the brains to run parts of code, see the result, and just put it back in 00:18:28 oerjan: hmm.. yes, I suppose 00:19:08 Sgeo_: my bfbasic language produces rather bloated code, so I'm sure you can do better :) 00:19:21 that seems trickier to understand. hm. 00:19:31 calamari: it is truly hideous code! :) 00:19:41 calamari, the only effect my optimizer has is removing loops that occur immediately after loops 00:20:02 * Sgeo_ is curious about the [-][.] structure at the beginning 00:21:04 Oppoppo would be a nice name for the pp=opposite p Lang. 00:21:21 ehirdiphone: obviously abelian groups made out of Z_3 parts will fulfil that, but i'm wondering if it can be non-abelian 00:22:20 hm for finite groups, now what was that theorem... 00:23:07 :D 00:23:31 Sgeo_: ??? 00:23:49 No what I'll call "flat" code (code made up of +-<>) should need to change direction more than twice 00:24:05 calamari, Lost Kingdom begins with [-][.]. 00:24:10 erm, not the last . 00:24:16 I'm curious as to why 00:24:40 maybe he added that on, but I don't see that in the actual compiler 00:25:01 Erm, 3 times, not twice 00:25:07 [-][.] seems... dumb 00:25:17 Sgeo_: It's omittable in its entirety. 00:25:30 coppro: I think that's a stripped out set of comment blocks? 00:25:43 p^3 = 1 can be non-abelian iirc 00:26:11 pikhq, my optimizer currently isn't perfect 00:26:12 3x3 upper triangle matrices 00:26:19 err no wait 00:26:21 It just emits loops after loops at this point 00:26:29 Hrm. 00:26:54 well anyway there was some sort of example i'm too tired to come up with 00:27:06 Also, it won't attempt to optimize + - 00:27:10 And I consider that a feature 00:28:24 hm sylow's theorem, but i'm not sure it helps 00:28:27 *theorems 00:28:59 oklopol: oh fine 00:29:16 i'm trying to find it but it seems the webpage of our algebra course is down 00:29:30 somehow you can do it with matrices 00:29:41 1 on the diagonal ofc 00:29:47 oerjan: or how about p^length(p) = nop :) 00:29:54 now if it's finite it must have order 3^n, at least 00:30:15 ehirdiphone: aigh 00:30:54 hm actually that might give some restrictions 00:30:59 It occurs to me that loops nested thus: [++[-]] means that the outer loop doesn't need to be a loo\ 00:31:01 loop 00:31:09 so 00:31:13 ** is nop 00:31:18 as is ****** 00:31:19 ehirdiphone: um wait then every primitive operation is a nop :D 00:31:21 :D 00:31:29 ((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 00:31:33 *^1 you see 00:31:35 oerjan: er I mean 00:31:43 length+1 00:31:48 ok 00:32:00 ********* is nop 00:32:12 Or am I incorrect somehow? 00:32:41 ehirdiphone: how do you get the last one? 00:33:20 oerjan: #*** = 3; ***^4 = ************ 00:33:21 Sgeo_: the outer loop could still be done 0 or 1 times 00:33:42 #** = 2; **^3 = ****** 00:33:44 Oh, right 00:33:44 huh 00:33:58 ehirdiphone: l*(l+1) is always even 00:34:10 right... 00:34:15 you are simply getting everything (**)^n 00:34:25 which is equivalent to having just ** 00:34:40 x^#x-1 = nop :D 00:34:53 okay checked 00:35:07 so nop from ** is ** 00:35:16 from ***, ****** 00:35:24 ****, ************ 00:35:34 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 00:36:02 everything except p^3 is obvious, i couldn't do that with ascii notation 00:36:15 would've been much easier to work out in my head 00:36:33 p^3 = 1 00:36:56 ehirdiphone: still all even. and _you_ do realize that concatenating nops gives a nop, right? 00:37:17 oerjan: i'm being silly 00:37:31 CAN WE PLEASE TALK ABOUT THESE GROUPS NOW 00:38:00 oklopol: make em eso 00:38:09 groups are very eso 00:38:19 non-abelian ones 00:38:23 at least 00:38:27 groups don't exist 00:39:00 oklopol: 3x3 matrices, you said? 00:39:11 yes 00:39:35 so just 3 degrees of freedom... 00:39:58 p^63 = nop 00:40:03 happy? :P 00:40:05 what are degrees of freedom? i've heard of them but didn't really gut it 00:40:37 dimension of space, mostly? 00:40:58 oh 00:41:00 cool :) 00:41:24 in statistics the explanation was really vague 00:41:30 -!- ehirdiphone has quit (Quit: Get Colloquy for iPhone! http://mobile.colloquy.info). 00:41:48 -!- ehirdiphone has joined. 00:42:33 fizzie: you're still op >:) 00:42:56 -!- fax has quit (Ping timeout: 265 seconds). 00:43:09 [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] 00:43:24 if i did it correctly 00:43:32 iidic 00:44:36 -!- fax has joined. 00:44:49 ehird 00:45:38 Fax 00:45:45 hi 00:45:49 hi 00:46:12 oerjan: looks plausible 00:46:15 will you still ignore me if I mention p, q and <-> fax 00:47:24 answer: yes 00:47:47 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 00:47:50 I PMd you 00:47:57 = 1, yes 00:47:58 er, = 1 00:48:17 cuz non-abelian 00:48:25 ...and cuz matrix i guess 00:48:45 non-abelian doesn't apply when multiplying a matrix with itself, though 00:48:53 yo 00:49:22 yeah but you don't use 0 for identity in one place and 1 in another 00:49:33 so because the group isn't altogether abelian, you'd use 1 00:49:36 it was a typo :D 00:49:51 and 1 = identity matrix 00:49:56 -!- jcp has joined. 00:49:59 02:47… oklopol: cuz non-abelian 00:50:00 02:47… oklopol: ...and cuz matrix i guess 00:50:06 i included both reasons 00:50:30 WHATEVER 00:50:47 using Z_3 as the field, that gives 9 elements 00:50:50 i mean because the 0 couldn't have been interpreted as the zero matrix 00:50:59 it would definitely still have been the identity matrix 00:51:20 oklopol: oh, and it doesn't need to be a field, a commutative ring is sufficient 00:51:34 so i think the non-abelian thing is a better reason- 00:51:35 *. 00:51:47 well sure 00:54:08 food -> 00:54:16 dog -> 00:58:55 Dog food 01:00:45 now the _next_ question is, can we get an infinite group of this type with finitely many generators? 01:02:14 and then something whose word problem is unsolvable, to perhaps give us TC? 01:02:38 im TC 01:02:40 (turning crazy) 01:09:47 -!- Gracenotes has quit (Ping timeout: 260 seconds). 01:09:54 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 01:10:10 and it's a group because p^-1 = pp 01:10:32 ooh 01:10:37 "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" 01:10:51 xD 01:10:54 oh umm 01:10:56 DEAD END REACHED 01:11:02 yeah okay then there must be something wrong with mine 01:11:07 ehirdiphone no the answer is no 01:11:18 :D 01:11:22 it's not entirely unanswered, mind you 01:11:24 so no dead end 01:11:31 huh, isn't it completely answered? 01:11:37 could be 01:11:41 what about ppppp = nop 01:11:43 i'm just reading the article 01:11:49 i think it was by some russians 01:11:54 ehirdiphone: that falls under burnside too. 01:11:57 construction was like 200 pages 01:12:06 however, burnside is generally false, it seems 01:12:12 p^1001 = nop 01:12:12 i just said that 01:12:19 yeah 01:12:22 the answer is no 01:12:40 also that's why construction an not proof 01:12:42 but that doesn't tell us which particular powers are possible 01:12:43 *and 01:13:09 ohhhhhhh 01:13:16 HA 01:13:17 okay i just realized what was wrong with my idea 01:13:25 TIME TO SEARCH FUCKERS 01:13:58 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 01:14:22 so turns out the burnside problem of monoids can be answered by any fucker in a minute, but for groups it requires russians. 01:14:40 err {a, b}^* obviously 01:14:57 oklopol: um any monoid in which everything has w^3 = 1 is a group 01:15:15 because you have an explicit inverse w^2 01:15:25 hmm well umm yes 01:15:28 so what's wrong 01:15:42 well you haven't proved it's actually infinite... 01:15:54 the thue morse word has no repetition of order more than 2 01:15:59 take subwords 01:16:06 ah! 01:16:25 they need not be different 01:16:54 because you can expand any 1 01:16:57 in the middle 01:18:09 "By contrast, very little is known when exponents are small, exponents 2,3,4 and 6 excepted." 01:19:01 in other words, it's probably still unsolved for many of them 01:19:17 but solved for 3, so probably it's finite then 01:20:41 okay what you need to do for semigroups is to add a 0 element and set uxxxv = 0 for all u, x, v 01:21:14 then you can find an infinite amount of words in a binary alphabet by taking thue-morse 01:22:10 and we have 0*u = 0 = u*0, obviously not a group 01:22:48 "B(m,3), B(m,4), and B(m,6) are finite for all m." 01:22:52 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 01:23:13 m is the size of finite basis? 01:23:17 (and B(m,2) is even simpler, it's what we discussed above) 01:23:20 yeah 01:23:21 or maybe not basis set of generators 01:23:29 *yeah 01:26:17 "The particular case of B(2, 5) remains open: as of 2005[update], it is not known whether this group is finite. 01:26:34 of course it's finite 01:27:02 um and you know this how? :D 01:29:13 I'm just saying random stuff sorry :( 01:29:32 There's a CROBOTs tournament at the end of the month if anyone want to take part 01:32:02 -!- fizzie has set channel mode: -o fizzie. 01:32:14 (Oh, I completely forgot about that.) 01:40:50 "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." 01:41:17 so uh all exponents n 01:41:27 would be another way of saying that. 01:41:28 might mean it is hard to make something TC even if B(m, n) is infinite 01:42:10 ehirdiphone: well, it is at the end of a section where every other result _does_ distinguish odd and even 01:42:48 even being apparently more complicated in several respects 01:43:20 s/section/paragraph/ 01:45:30 also, http://en.wikipedia.org/wiki/Tarski_monster_group 01:45:52 those have some huge exponents though 01:45:53 -!- impomatic has quit (Quit: ChatZilla 0.9.86 [Firefox 3.5.9/20100315083431]). 01:47:06 oho 01:47:11 I lik monster groups 01:47:23 I want to study moonshine but I have to learn some stuff first..... 01:47:30 that's not _the_ monster group though 01:47:34 yeah 01:47:40 I didn't realize there was other ones actually 01:47:45 these are actually infinite 01:47:52 oh :( 01:48:09 but have _only_ finite subgroups 01:48:20 :D 01:48:21 and only of a particular, prime order 01:49:10 tarski & hutch 01:51:04 ehirdiphone: there are google hits for that 01:52:10 * Sgeo_ somewhat mindboggles at a package that provides isBottom 01:54:09 Sgeo_: there is a package by conal containing a function f such that 01:54:25 f _|_ y = y 01:54:32 f x _|_ = x 01:54:36 -!- charlls has joined. 01:54:45 if neither are _|_, it returns either 01:55:08 (psst: the one that evaluates first) 01:55:11 I guess it deals with nontermination by being whichever is .. riht 01:56:47 Definition isBottom {A} (x : A) : bool := true. 01:56:50 Erm 01:56:54 false 01:57:17 ehird lol I just wrote that in #haskell a moment ago 01:57:25 heh 01:57:36 GET TO BED :| 01:57:42 I want to try to program for a bit first 01:57:47 but it probably wont work and I'll go 01:58:11 do computable reals 01:58:24 prove some thing about them 01:59:55 every function on them is continuous, i hear. you could prove that. 01:59:58 ehird yeah I have been meaning to write in the bit about reals from my book 02:00:07 oerjan, I'm not sure if that is provable! 02:00:22 oh well 02:00:23 oerjan, I think it's _true_ but may be sort of like the continuum hypothesis or similar 02:00:43 I'm thinking interally though 02:00:50 like inside the type theory 02:00:58 yeah I hope I am not making this up 02:01:29 hmm 02:01:42 I suppose it's related to the unprovability of trichotomy 02:02:00 and trichotomy implies some pretty strong statements but I don't think it quite reaches P \/ ~P 02:02:12 -!- adam_d has quit (Ping timeout: 265 seconds). 02:02:38 fax: you can't prove the trichotomy for comp reals? 02:02:41 I should try to get a better understand of this stuff 02:02:48 huh 02:02:52 and write a note on it or something 02:03:03 I wonder if there's q middle ground 02:03:05 *a 02:03:08 this computable reals and analysis stuff (and meta theory) 02:03:38 maybe continued fractions? 02:04:03 continued frractions are something I am not very comfortable with... 02:04:11 Why not? 02:04:18 I never used them 02:04:32 1+1/1+1/... 02:04:39 there's the golden ratio 02:04:42 DONE 02:04:45 :p 02:04:45 I know that one :P 02:04:51 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 02:05:00 (prove forall ...) 02:05:02 can you solve every quadratic as a continued fraction? 02:05:05 I'll play with them tomorrow I guess 02:05:23 fax: every real has a continued fraction 02:05:32 Are there any BF optimizers that optimize back into BF code? 02:05:40 Well Chaitins constant... 02:05:46 Sgeo_: Yes 02:05:48 but you still must be able to define functions on them, and therefore any functions must also have their value close 02:05:57 x=(-b/a)+(-c/a)/x 02:05:57 Same site as list kingdom 02:06:03 Jonripley or sth 02:06:15 (-b/a)+(-c/a)/((-b/a)+(-c/a)/((-b/a)+(-c/a)/((-b/a)+(-c/a)... 02:06:16 I guess 02:06:24 but that will never give a complex value 02:06:29 that can't be right 02:06:37 maybe it diverges on those cases 02:06:43 I'll define continued fractions in coq tomorrow 02:06:53 ehirdiphone, no unitness tomorrow? 02:07:10 Not tomorrow. M 02:07:11 fax: quadratics have _periodic_ continued fractions iirc 02:07:18 and only they 02:07:26 *roots of 02:07:41 * Sgeo_ doesn't see any optimization stuff on the site 02:07:53 well a continued fraction still has to be a function... 02:07:58 nat->nat 02:08:03 hmm 02:08:15 oh, well real ones i guess 02:08:36 * Sgeo_ pokes ehirdiphone 02:08:56 Search more 02:09:09 -!- charlls has quit (Quit: Saliendo). 02:09:14 hmm 02:10:04 wait does 0 have a continued fraction 02:10:23 0 = 0 + 0/(0 + 0/(0 + ... 02:10:31 0 repeated means that 0 = 0 + 1/0 = 1/0 02:10:46 ehirdiphone, are you sure there's something there? 02:10:49 but 0(1/0) =/= 1 02:10:56 Sgeo_: 80% 02:11:08 fax: oh 0/ 02:11:14 * Sgeo_ sees nothing relevant 02:11:23 is 0/ allowed in a continued fractin? 02:11:30 it must be... 02:11:33 Just 1/ afaik 02:11:48 0/ would be pretty dumb in a continued fraction 02:12:19 f : N -> N; R(f) = f(0) + 1/(f(1) + 1/...) 02:13:45 ehirdiphone, I'm still not seeing it 02:13:50 * Sgeo_ should probably stop whining 02:14:05 im curious abuot the convergence of this continued fraction for quadratic 02:14:23 Sgeo_: it's clearly been optimized away 02:14:50 fax: no, 1/ only in ordinary continued fractions 02:14:56 ahhh 02:14:57 okay 02:15:01 If he has one, he either didn't realize the pointlessness of ][loop] 02:15:03 that makes things harder 02:15:04 well 02:15:08 1/infinity = 0 02:15:16 Or he doesn't run his own code through it 02:15:17 so what's the continued fraction for infinitY? 02:15:24 fax: 1/0 ? 02:15:25 1 + 1/0 I guess 02:15:31 so 0 = 0 + 1/infinty 02:15:48 so 0 = 0 + 1 /( 1 + 1 /( 0 + 1 /( 02:15:57 i think 0 and infinity are sort of boundary cases 02:16:10 you just let the fraction _end_ there 02:16:19 f 0 := 1; f (S _) := 2 // sqrt 2 02:16:27 or any integer for that matter. 02:16:56 it seems to orbit around e-4 02:17:01 and not get smaller 02:17:18 oh it's getting smaller... just takes some time 02:18:24 I wonder which infinity it is 02:18:33 zero is all the same but infinity is all different 02:18:34 The tastiest one. 02:18:46 one of my favorite infinity is sqrt(2pi) 02:19:01 thats' 1 + 2 + 3 + 4 + 5 + ... IIRC 02:19:03 >_> 02:19:19 no sorry it's 1 * 2 * 3 * 4 * 5 * ... 02:19:30 1 + 2 + 3 + 4 + 5 + ... = -1/12 02:19:41 clearly. 02:20:08 hey everyone makes mistakes 02:20:08 :) 02:20:32 hey wait a minute. now _you_ are doing math and _i_ am saying random nonsense. 02:20:57 fax: also of course all rationals only have finite continued fractions 02:21:09 So really it is nat -> maybe nat 02:21:19 -!- sshc has quit (Quit: leaving). 02:21:24 oerjan, the old 3/5-switch :) 02:21:29 (two; irrationals have one infinite one) 02:21:46 (fuck yeah I just referenced wiles proof of fermats lol theorem) 02:22:00 1 = 1/(0+1/(0+1/(... *whistles innocently* 02:22:16 ehirdiPHONE can you prove that every rational is finite? 02:22:25 finite continued fraction 02:22:32 I am sure that it is true but I wonder how to actually build it 02:22:36 fax: no but wikipedia can 02:22:43 Euclidean algorithm 02:22:48 Checkout 02:22:51 ... 02:22:55 Checkkit 02:23:00 >_> 02:23:07 induction on the size of numerator and denominator 02:23:30 lol 02:24:12 s/and/+/ if you want a specific measure 02:25:00 -!- sshc has joined. 02:26:12 http://upload.wikimedia.org/math/f/9/7/f9729d86173eced1bc46aeb6087dada9.png <------ nice picture 02:26:57 but but... it's not fractal! 02:27:49 I like the . 02:28:01 The 0 at the end of the recurring 9s 02:30:23 New Autotune the news tomorrow! 02:31:51 :( Autotune 02:32:00 obama the musical? 02:32:20 * oerjan googles that 02:32:56 Autotune the news! 02:33:02 Autotune the news! 02:33:09 Everything sounds beeettet 02:33:12 Beetter 02:33:16 Autotuuuuuuned 02:34:07 These later ones tend to reference earlier ones 02:34:58 -!- jcp has changed nick to banbino. 02:35:02 -!- banbino has changed nick to Banbino. 02:37:20 -!- sshc has quit (Quit: leaving). 02:39:04 -!- Gracenotes has joined. 02:41:39 -!- Banbino has changed nick to jcp. 02:46:05 -!- sshc has joined. 02:47:17 -!- ehirdiphone has quit (Quit: Get Colloquy for iPhone! http://mobile.colloquy.info). 02:48:50 -!- coppro has quit (Quit: I am leaving. You are about to explode.). 02:49:29 -!- coppro has joined. 02:54:32 -!- jcp has quit (Read error: Connection reset by peer). 02:57:05 -!- sebbu2 has joined. 02:57:53 -!- sebbu has quit (Ping timeout: 276 seconds). 02:57:54 -!- sebbu2 has changed nick to sebbu. 02:58:40 -!- EgoBot has quit (Remote host closed the connection). 02:58:41 -!- HackEgo has quit (Remote host closed the connection). 02:58:44 -!- HackEgo has joined. 02:58:46 -!- EgoBot has joined. 03:09:34 -!- jcp has joined. 03:11:50 -!- sshc has quit (Quit: leaving). 03:14:34 oklopol 03:14:34 ? 03:25:47 me? 03:27:02 ffffffff 03:27:08 I can't remember what I was going to say to you 03:27:22 oh yeah have you seen divisibility lattices? 03:29:32 yes 03:30:19 Lesse ... 1 is bottom ... is there a top? 03:30:31 well the top is the number you are factoring 03:30:32 oh 03:30:35 obviously not 03:30:35 no I guess it's not 03:30:40 if you take all nats 03:30:43 what about infinity! 03:30:49 1*2*3*4*5*.. 03:30:50 Who says you can't divide by infinity? 03:30:58 that's divisible by everything infinetly many times 03:31:06 that's the obvious way to make it bounded i guess 03:31:18 you add infinity to make it bounded? :D 03:32:06 well... yes :P 03:32:42 but now you must add more infinities, like 2*2*2*... >:) 03:33:05 I wonder which ones have values and which dont 03:33:14 what do you mean? 03:33:21 apparently harmonic series doesn't have a value 03:33:29 but I am not sure about htat.. 03:33:39 although 1*2*3*4*5*... is still on top, all primes divide it infinitely often 03:34:13 man I just can't understand this chapter 03:44:29 fax: don't be your brain's bitch 03:45:15 pain's bridge 03:45:59 seriously I have been working on this stuff for 3 days now 03:46:08 it's very difficult 03:46:10 I am not Gauss 03:46:26 completely degaussed, in fact 03:46:32 ..................................................... lol 03:46:43 okay seems the divisibility lattices are distributive 03:47:14 it's just the sum of one N lattice per prime, isn't it 03:48:00 oklopol, how dod you prove it? 03:48:13 i proved it using the cool characterization i mentioned 03:48:16 (that's how you can use it to program in fractran) 03:48:18 yes I want to see :))) 03:48:20 in burris' book on universal algebra 03:48:23 did you find two numbers? 03:48:29 one for each of those lattices 03:48:34 oh it's really easy to prove 03:48:45 you can just check it yourself if you know the characterization 03:48:53 dunno if it's easy from the definition 03:49:20 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 03:49:49 oerjan: how do you define the sum of two lattices? 03:50:01 of an infinite number of them, actually... 03:50:11 oh wait 03:50:18 like (x, y) <= (z, w) iff x <= z, y <= w? 03:50:24 yes. 03:50:41 although i realized only a finite number can be different from 0 03:50:41 and that extended to infinite products 03:50:55 hmm 03:51:14 which is analogous to sums of modules/abelian groups 03:51:26 vs. products that are unrestricted 03:51:45 -!- fax has quit (Quit: Lost terminal). 03:52:14 also one thing i remember about distributive lattice is that they are exactly the sublattices of boolean algebras 03:52:20 *lattices 03:52:32 okay so we can take the sublattice of N^P generated by the individual primes, maybe 03:52:44 they are?!? 03:52:49 that's an even cooler characterization. 03:52:51 yes iirc 03:53:05 there's a whole chapter about boolean algebras in the universal algebra book 03:53:16 unfortunately not in the exam so i'm probably not going to read it anytime soon 03:54:00 one way of showing this is that _both_ classes of algebras have only {0,1} as their subdirectly irreducible members 03:54:21 (up to isomorphism) 03:55:29 there's probably a less heavy-weight method, i just happened to learn about subdirectly irreducible algebras once 03:55:41 okay i've actually proved the former 03:55:55 proved what? 03:56:08 err 03:56:21 i seem to have expanded both and said former about one of the two 03:56:28 i've proved that for distributive lattices 03:56:50 proved _what_ for distributive lattices? 03:56:56 xD 03:56:59 err 03:57:19 that the class of distributive lattices has only {0,1} as a subdirectly irreducible member 03:57:30 Exercise 1.11. Show that a distributive lattice is subdirectly irreducible if and only if it 03:57:30 is a 2-element lattice. 03:57:35 ah. 03:57:49 harder than it sounds, that one 03:57:54 from this it should be trivial actually 03:58:01 you don't need the other one 03:58:02 it should, huh. 03:58:34 just note that a product of 2-element lattices is also a boolean algebra 03:58:53 subdirect irreducability still feels a bit strange to me, don't see how that's useful directly, but i'm all ears 03:59:02 oh 03:59:09 hmm 03:59:35 well the thing is every algebra is a subdirect product of irreducible ones 03:59:52 yes 03:59:55 where a subdirect product is a special kind of subalgebra of a product 03:59:57 right 04:00:13 yeah i know what it is, and i'm starting to see how the proof would go 04:01:06 so umm first of all every distributive algebra must be a subdirect product of {0, 1}'s, which are boolean algebras 04:01:14 yep 04:01:20 *lattice 04:01:28 err right 04:01:39 but why is the subdirect embedding also a boolean algebra? 04:01:47 or wait is that obvious 04:01:59 it's not, it's a _sublattice_ of one 04:02:15 oh lol 04:02:22 okay so actually it is totally trivial 04:02:46 once you get the lemma proved 04:03:00 yeah 04:04:06 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 04:04:29 so you can separate any pair by a nontrivial congruence, which is equivalent to not being subdirectly irreducible 04:04:38 i'm not sure why i told you that 04:04:45 maybe just because i remembered it. 04:05:47 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" 04:06:39 i have many more uninteresting stories, if you wanna hear 04:06:40 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 \/ 04:06:57 or rather, i though in terms of quotients 04:07:00 *thought 04:07:44 and these congruences exist both for distributive lattices and for boolean algebras 04:08:22 (boolean algebras sort of are distributive lattices, so isn't that obvious) 04:08:27 (?) 04:08:44 well yes as long as you prove "not" is also preserved 04:08:58 hmm right 04:10:30 "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 04:10:53 a /\ ~(a /\ x) = a /\ ~a \/ a /\ ~x = a /\ ~x 04:11:00 i don't like it when people leave things out of definitions, everything starts feeling all blurry and scary 04:11:20 that's not a very clear definition 04:11:43 oerjan: so wait what did that prove exactly 04:12:02 that ~ is preserved by the congruence. at least i think it implies it. 04:12:30 oklopol: well just after i said that you told you already knew about it 04:12:32 let's see if i can even see what it means to be preserved by a congruence... 04:12:56 oh 04:13:06 oerjan: yes, i didn't mean "why did you leave this open", i just needed to fill it 04:13:08 i'm still thinking in terms of quotients, you see 04:13:11 **you* 04:13:19 oh umm hmm right 04:14:11 the map x -> a /\ x is a quotient map, if you redefine the operations on the range by applying extra a /\ ... liberally 04:14:29 a is just some element you choose? 04:14:33 yeah 04:14:42 and quotient maps give congruences, of course 04:14:59 um i shouldn't even call it quotient 04:15:06 homomorphism 04:15:13 the kernel is a congruence 04:15:14 yeah 04:15:34 it's just isomorphic to the quotient of the congruence 04:16:07 yes, by the famous whatevermorphism theorem 04:16:35 so essentially all you have to prove is that applying a /\ ... liberally on the right side _does_ make it a homomorphism 04:17:07 and the above equation does that for ~ 04:17:41 so you proved h(~(h(x))) = h(~x)? 04:17:48 for /\ it's almost trivial, and for \/ you need the distributive law 04:17:49 where h is the homom 04:18:05 well yeah 04:18:25 where h is the map 04:18:53 shouldn't you prove ~h(x) = h(~x), that is, ~(a ^ x) = a ^ ~x 04:18:59 wait... 04:19:10 i think i'm a bit lost. 04:19:26 nope the thing is that we don't use the same operations on the range (even if it is a subset) 04:19:50 we use the operations with the h liberally reapplied at the end 04:20:15 so like ~y : range = a ^ ~y : domain 04:20:16 so we're defining a new algebra which just happens to share some points 04:20:23 yeah 04:21:05 and this works very well for distributive lattices and boolean algebras 04:21:30 i also played around with doing it for heyting algebras 04:21:46 i got kripke models that way 04:24:08 (heyting algebras are to intuitionistic logic what boolean algebras are to boolean logic) 04:24:23 okay i finally get your one-liner up there. 04:24:31 the range vs domain issue was a bit confusing 04:25:11 oh they are now? i just know they have ->. 04:25:32 and i remember most of the axioms 04:26:09 ah yes. i guess the fact i could do this was a kind of an epiphany, made it much simpler to find congruences 04:26:23 do you know cylindrical algebras of dimension n and n-valued post algebras? 04:26:31 heck no 04:27:07 okay those were the two weirder examples of algebras in the book 04:28:10 was just wondering because you seem to have an intimate relationship with all the others 04:28:27 i had never heard of heyting algebras either 04:28:40 boolean algebras i had heard of, surprisingly enough 04:28:45 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 04:29:34 what does true mean? :) 04:29:52 x is true iff 1 -> x or something? 04:29:54 eh 04:29:57 what does that even mean 04:30:04 let me rethink 04:30:07 well 1 is the true element i guess 04:30:25 so x is true means x = 1? 04:30:28 yeah 04:30:51 was that subdirectly irreducible or directly? 04:31:05 subdirectly 04:31:19 i don't know which is more common, prolly subdirect because of the problems direct has 04:31:21 that's what i was dabbling with at the time 04:31:30 right, right 04:32:14 -!- calamari has quit (Ping timeout: 276 seconds). 04:32:58 well, it was about time this channel had an interesting conversation, i thank you for that. i should get back to my stuffs now 04:33:13 i also _think_ that if x is not 0, then there is a heyting algebra homomorphism sending x to 1 != 0 04:33:52 there's too much axioms for me to wanna try that straight from the definition 04:34:25 actually not that many but anyway 04:34:28 well it may have been just using a map like x /\ ... and the above trick 04:34:46 or possibly x => ... 04:34:49 I.. think, now that I understand how to use StateT, the actual implentation of the interpreter just became trivial 04:34:50 *-> 04:35:00 Sgeo_: heh 04:35:22 Although not quite.. I don't think sequence does quite what I want it to do 04:35:45 Actually, hm. That "trivial" function doesn't quite ty.. n/m 04:35:50 sequence does them one after the other, passing each state to the next, iirc 04:36:08 (afa state is concerned) 04:36:53 * Sgeo_ was wrongly thinking that the thing for , would be StateT Tape IO Char, but it is StateT Tape IO (), just like everything else 04:38:56 Sgeo_: what did you want sequence for? 04:39:07 maybe sequence_ would be better? 04:39:29 (you're not interested in any results not in the state, so) 04:40:05 oerjan, getting my point about being confused across, I know the difference 04:40:29 ok 04:41:29 Besides, if I want to use sequence, I can always use (const () . ) (sequence_ $) 04:41:38 Um, don't know if that's exactly what I'd use 04:41:48 Also, no _ obviously 04:41:56 * Sgeo_ is not quite a master of pointfree 04:42:35 const () `fmap` 04:42:54 -!- jcp has quit (Quit: I will do anything (almost) for a new router.). 04:44:00 however, i think sequence_ sometimes is more tail recursive 04:44:27 since it doesn't need to put on the return value remembered 04:45:37 -!- calamari has joined. 04:48:15 Going to go eat now 04:48:27 -!- sshc has joined. 04:55:17 Would you say it's complete and utter overkill to use Linux to make a disk image that does the following: run LostKng? 04:56:59 s/use.*: // *whistles innocently* 04:57:24 oerjan: Hah. 05:04:22 -!- lament has quit (Ping timeout: 264 seconds). 05:04:54 -!- augur has quit (Ping timeout: 265 seconds). 05:14:45 legalify = cmdsToBF . parseBF -- Turns any string into legal BF 05:15:05 Well, not checking for hitting the left edge or negatives or anything 05:17:55 any string already is legal BF, unless it has mismatched brackets >:) 05:18:27 legalify fixes mismatched brackets 05:18:35 ok then 05:18:48 Although fixing might not be what's wanted 05:18:59 -!- lament has joined. 05:19:20 (truncating at the first extra ], and adding ] if there were extra [) 05:20:03 -!- augur has joined. 05:21:29 -!- jcp has joined. 05:22:57 oerjan, does sequence_ work well with infinite lists? 05:23:22 i think so 05:24:00 sequence_ = foldr (>>) (return ()) 05:24:04 sequence = fold.. was about to ask 05:24:21 Might have said foldl though :/ 05:24:37 well, sequence_, yeah 05:25:15 Well, with >>, there's supposed to be no difference, right? 05:25:20 And foldr works with infinite lists 05:25:39 i should think it's intended to be usable 05:26:35 as long as the monad used can handle it 05:33:50 -!- lament has quit (Ping timeout: 260 seconds). 05:38:19 -!- Oranjer has left (?). 05:45:53 -!- pikhq has quit (Read error: Connection reset by peer). 05:49:44 -!- pikhq has joined. 05:52:51 -!- Sgeo_ has changed nick to Sgeo. 06:02:06 -!- lament has joined. 06:30:05 -!- lament has quit (Remote host closed the connection). 06:41:17 -!- adu has joined. 06:46:17 -!- oerjan has quit (Quit: Good night). 06:46:26 -!- calamari has quit (Quit: Leaving). 06:59:24 -!- coppro has quit (Quit: I am leaving. You are about to explode.). 07:08:32 hey kidos 07:26:15 -!- FireFly has joined. 07:39:43 hi augur 07:39:51 who you 07:41:18 -!- Gracenotes has quit (Quit: Leaving). 07:45:37 -!- adu has quit (Quit: adu). 07:59:59 -!- clog has quit (ended). 08:00:00 -!- clog has joined. 08:17:48 -!- augur has quit (Read error: Connection reset by peer). 08:18:10 -!- augur has joined. 08:41:54 -!- Gracenotes has joined. 08:42:35 -!- adu has joined. 09:29:03 -!- lament has joined. 10:02:25 -!- lament has quit (Ping timeout: 248 seconds). 10:04:06 -!- jcp has quit (Quit: I will do anything (almost) for a new router.). 10:05:58 -!- tombom has joined. 10:11:21 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 10:11:21 s, I think I'm going to unban the other one. 10:11:23 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. 10:14:49 -!- ChanServ has set channel mode: +o fizzie. 10:15:00 -!- fizzie has set channel mode: -b *!*@unaffiliated/quadrescence. 10:15:03 -!- fizzie has set channel mode: -o fizzie. 10:23:24 -!- Alex3012_ has joined. 10:25:05 -!- Alex3012 has quit (Ping timeout: 276 seconds). 10:25:14 -!- Alex3012_ has changed nick to Alex3012. 10:55:44 -!- adam_d has joined. 11:35:14 -!- BeholdMyGlory has joined. 11:36:44 -!- Gracenotes has quit (Quit: Leaving). 11:45:26 -!- MizardX has joined. 12:30:32 -!- cheater2 has quit (Ping timeout: 276 seconds). 12:34:55 -!- cheater2 has joined. 12:52:42 -!- ais523 has joined. 12:58:52 -!- adu_ has joined. 13:01:27 -!- adu has quit (Ping timeout: 265 seconds). 13:20:27 * AnMaster wonders how a program on a single core, single cpu system, can have higher cpu time than wall time. 13:21:13 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 13:22:46 ais523, hi btw 13:23:40 hi 13:24:55 any idea about the weird cpu time btw, ais523 ? 13:25:13 no 13:25:22 hmm... are you overclocking/underclocking the system? 13:25:36 it's possible that the CPU has a bogus idea of how much time it's taking, I suppose 13:25:47 ais523, ondemand cpu speed is in use 13:25:51 but no overclocking 13:26:24 but since this process is baiscally CPU bound it is eating about 99% of the CPU all the time 13:26:28 hmm 13:26:31 so the system should be at top speed 13:26:44 yep, cpufreq-info confirms that system is running at 2 GHz 13:26:58 and there the process finished 13:27:05 so hard to tell now afterwards 13:28:02 (it was optipng running on a few thousand small png files btw) 13:54:07 * AnMaster wonders how to write sort(1) in dd/sh 14:04:23 btw, is it just me, or has spam decreased drastically during the past 2 days or so 14:04:44 I only got one spam during that period, normally I get something like 30 / day or so... 14:05:25 ais523, ^ 14:05:38 I'm still getting just as much spam as before 14:05:42 hm 14:06:00 pure chance then I guess 14:07:14 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... 14:08:45 (I imagine it would work in a similar way to those block-telemarketing registers) 14:08:59 -!- adam_d_ has joined. 14:11:03 -!- adam_d has quit (Ping timeout: 265 seconds). 14:31:12 "./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... 14:32:04 AnMaster: those registers do work 14:32:15 at least in the UK, telemarketing companies don't want to be tracked down and fined 14:32:41 true 14:34:44 ais523, what I meant was that it wouldn't work for spam 14:34:53 no, it wouldn't 14:35:04 although, a spammer was arrested and fined in California recently 14:35:18 it made the headlines, on the basis that nobody expected they'd actually catch one 14:35:50 ah 14:38:06 -!- fax has joined. 14:38:52 Yeah, but most of them are probably A) unwilling participants in a botnet and/or B) not in a country that gives a shit. 14:43:58 yep, the spammer in question was a business doing it deliberately, and even turned up in court to defend itself 14:44:10 which is also rather bizzare 14:47:48 AnMaster: Did I ever link http://codu.org/music/vg/gm1.ogg at you? 14:48:17 not sure 14:48:25 * AnMaster wgets 14:48:55 Gregor, piano, some sort of synth? 14:49:22 's more video game music (created per request) 14:49:25 and hm... some string instrument 14:49:37 and huh, a lot more 14:49:40 OK, it's an odd ensemble :P 14:49:46 Gregor, nice though 14:49:51 so far at least 14:49:59 Gregor, was there a xylophone? 14:50:05 hmm, I generally like video game music 14:50:19 AnMaster: Nothing even similar :P 14:50:35 * ais523 plays it 14:50:51 Gregor, some percussion thing that sounded somewhat wooden? 14:51:04 only for a very short period 14:51:14 I assume that you're referring amusingly to the Shamisen :P 14:51:22 Which is a plucked string instrument. 14:51:34 huh, never heard of Shamisen before 14:51:39 but yes very nice. 14:52:19 Gregor, but please provide me a list of the instruments 14:52:30 also, for which video game was it created? 14:52:50 Just a class project of a friend of a friend. 14:53:02 I can do one better, I think ... 14:53:20 http://codu.org/music/vg/gm1.mid 14:53:26 http://codu.org/music/vg/gm1.rg even 14:54:05 aargh wth. That isn't the QT theme in rosegarden 14:54:13 * AnMaster wonders why it is mostly black 14:54:21 lol 14:54:23 it looks like a cross of blender and QT 14:54:26 awful 14:54:37 'snot supposed to look like that :P 14:54:50 Gregor, yeah, let me check other QT apps... 14:55:05 yay, I use Rosegarden to 14:55:05 kate looks normal 14:55:06 *too 14:55:14 hm 14:55:20 konsole and Rosegarden are the only Qt apps I use regularly, and konsole is supposed to be mostly black :P 14:55:22 Gregor: why does it go silent from 1:00 onwards? 14:55:38 i like the theme 0.....0b3.....32e.....edge...... 14:55:42 ais523, it isn't? 14:55:49 ais523, maybe your download failed? 14:55:50 ais523: "It"? 14:55:53 or youy hit mute? 14:55:56 Gregor: your music 14:56:03 with chromatic scale fedcba0123 14:56:06 ais523: Yeah, that's a "you" fail, since it does not :P 14:56:15 OK, that's strange, I rewound past 1:00 and then it started working 14:56:17 i guess it's pretty much the only theme 14:56:23 Gregor, which version of rosegarden do you have? 14:56:36 AnMaster: 1.7.3 14:56:59 10.02 here??? 14:57:06 what happened there 14:57:16 did they jump or something 14:57:22 Guhhh ...? :P 14:57:41 http://www.rosegardenmusic.com/ 14:57:42 Apparently they did. 14:57:48 aaargh it *is* supposed to look like that 14:57:57 I just use whatever the latest in Debian is X-P 14:58:13 Gregor, but the gui is supposed to look black, see screenshot on their website 14:58:15 how awful 14:58:28 Oh, they're doing the retarded year = release number thing. 14:58:35 it doesn't even fit together 14:58:36 was there a matrix mode in rosegarden 14:58:43 since it seems to use the GTK style for some stuff 14:58:44 oklopol: Sure 14:58:50 (as I set up qtconfig to do) 14:58:57 can you get it for win? 14:58:57 (because I like clearlooks) 14:58:58 But matrix mode is weird and pointless. 14:59:02 eh? 14:59:06 what do you compose in? 14:59:12 NOTATION 14:59:16 8| 14:59:19 you're insane 14:59:25 music notation is the worst thing ever invented 14:59:26 same as Gregor said. A lot easier that way 14:59:31 And/or actually a half-competent musician :P 14:59:45 oklopol, also you record it mostly 15:00:00 Right, yeah, I've got my digital piano plugged into my computer. 15:00:01 OK, something is /very/ wrong with Totem ATM 15:00:10 Gregor: heh, I used to use NOTATION when I was on Windows 15:00:13 and then use some quantisise or whatever 15:00:17 forgot what it was called 15:00:33 ais523, is this a nodepad joke? 15:00:37 no 15:00:38 well sure if you like, but music notation is still a really ugly way to look at the result 15:00:48 it's an actual program 15:00:54 it's not very good, but it's good /enough/ 15:00:56 i mean unless piano music, then it's useful for playing sure 15:01:01 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 ... 15:01:19 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 15:01:34 STOP DISAGREEING WITH MY INSANE OPINIONS 15:02:20 -!- tombom_ has joined. 15:02:23 i bet i've composed more music than you! (maybe not as much good music, but that's probably not relevant) 15:02:31 heh 15:03:03 That may or may not be true, I've thrown away vastly more music than I've kept. 15:03:27 But I guess when you make it that fine-grained, it all becomes meaningless :P 15:03:29 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. 15:03:30 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 15:03:44 -!- tombom has quit (Ping timeout: 246 seconds). 15:04:25 ah found where to change it 15:04:25 yay 15:04:26 Gregor: i think the best measure is to measure the amount of measures 15:04:35 ...ever written 15:04:36 remove thick in preferences for "use thorn style" 15:04:49 which seems to be the codename of this release or something 15:04:57 þorn 15:05:27 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 15:05:42 WAIT if that counts then http://codu.org/algorhythms/ 15:05:45 Gregor, huh, how did you manage to not make it play using the sound card? 15:05:46 :D 15:06:03 AnMaster: I have an absurdly complicated system for recording via fluidsynth. 15:06:16 Gregor, but that is a *.mid, not a *.rg 15:06:28 hmm, rosegarden doesn't seem to be working with timidity on this computer 15:06:36 AnMaster: Oh, from rosegarden; it's all configurable somewhere ... 15:06:43 okay something must be wrong on my side 15:06:44 hm 15:06:46 oklopol: And more specifically, http://codu.org/music/auto/OUT-T5.ogg (IIRC the link) 15:07:35 ah found it 15:07:39 no sound font loaded 15:07:40 huh 15:07:50 that is supposed to happen in rc.local wonder what went wrong 15:08:04 ais523: fluidsynth is (way) better anyway (or at least, it would be if it wasn't hugely buggy) 15:08:22 meh, all I really care about is being able to hear the notes 15:08:54 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. 15:09:00 so rc.local won't work 15:09:32 Gregor, sb live 5.1 beats fluidsynth IMO 15:09:35 AnMaster: Is it sufficient to just unload the driver, do whatever you need to, then reload the driver? 15:09:58 AnMaster: Yes, probably, but producing recordings of it is annoying (well, OK, same for fluidsynth ... ) 15:10:14 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 15:10:17 iwlagn* 15:10:18 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 15:10:34 Gregor, it won't work right away 15:10:37 for unknown reason 15:11:02 Well, then you're screwzored. 15:11:03 * AnMaster wonders why iw reg set can't take effect on already up interfaces 15:11:15 or even down but with driver loaded 15:11:17 tried that too 15:12:33 strange; Timidity is working on its own, just not from Rosegarden, but Rosegarden says everything's fine with the MIDI 15:13:09 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 15:13:44 ah I did ask it, but didn't get an answer as far as I can tell 15:13:45 AnMaster: Just a class project of a friend of a friend. 15:14:05 Sort of a StarCraft ripoff :P 15:14:07 ah right 15:14:09 heh 15:14:30 Gregor, starcraft is rts right? 15:14:34 Yes 15:14:37 Gregor: that's completely computer generated? 15:14:45 i've just heard a few of these 15:14:53 oklopol: OUT-T5 is computer-generated notes, human-generated dynamics 15:15:02 ais523, hm 15:15:12 okay so what does that mean exactly? 15:15:14 ais523, why timidity? 15:15:19 or maybe i should read the page 15:15:27 AnMaster: because I have it handy, for playing MIDI files 15:15:44 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 15:15:54 and Rosegarden's supposed to work out of the box 15:16:00 with it 15:16:03 ais523, hm 15:16:20 I never got timidity to _not_ crash 15:16:21 and did, on my last computer 15:16:27 so... what does human-generated dynamics mean, you play something on the piano, and random notes are substitute? 15:16:27 it is the most unstable thing I ever seen 15:16:28 *d 15:16:57 hmm, and it works fine from Totem 15:16:57 i need technical details 15:17:22 oklopol: Google for a program called Tapper (maybe "tapper conductor program" or something like that) 15:17:37 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 15:17:49 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. 15:18:21 Gregor, dynamics include everything except the which note is played? 15:18:23 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). 15:18:48 as in, how hard or soft you hit the key, when the note is played, the length of it, and so on? 15:18:58 Basically. 15:19:05 Gregor, what about the pedal? 15:19:42 (well pedals I guess. But I was thinking of sustain mainly) 15:20:22 That too. 15:20:40 oh dynamics, right, i don't care about dynamics 15:20:46 huh 15:21:08 you can do that stuff arbitrarily, as long as it's consistent 15:21:14 Gregor, and I have to say http://codu.org/music/auto/OUT-T5.ogg wasn't very good 15:21:18 no offence meant 15:21:23 OUT-T5 has its moments 15:21:38 but there's not themes, so it's sort of non-music 15:21:41 *no 15:21:44 -!- alise has joined. 15:21:47 moments of fits yes. 15:21:48 ;P 15:22:05 the listener needs a clear melody they analyze 15:22:07 *can analyze 15:22:17 oklopol, yes indeed 15:22:40 fax: Aye! 15:23:25 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. 15:23:43 is it? 15:23:48 for me 15:23:52 ah 15:23:54 for some reason that's enjoyable 15:25:03 -!- alise_ has joined. 15:25:11 hi Alex3012 15:25:13 errr 15:25:15 hi alise_ 15:25:17 I meant 15:25:34 * AnMaster wonders why the tab order was alise -> alex -> alise_ 15:25:36 should i wash the dishes and clean the apartment of just laze around the whole day 15:25:41 oh wait, last spoken 15:26:03 what, some irc client is actually non-retarded enough to do that? 15:26:08 oklopol: many :P 15:26:15 oklopol, cleaning the apartment of just laze around for an entire day? 15:26:17 is it that large? 15:26:34 i've tried irssi, xchat and mirc and then something with a bird none of them did 15:26:42 oklopol, most clients can be set to do last spoken 15:26:48 and various webchats and other things i don't recall 15:26:52 xchat can definitely, pretty sure irssi can too 15:27:01 oklopol: pidgin? 15:27:02 "can", python can do it too 15:27:02 but yeah I don't think it is default in xchat at least 15:27:06 xchat can do it yeah 15:27:08 it's just a setting 15:27:08 who gives a fuck, they *don't do it* 15:27:10 one flick to do 15:27:14 oklopol, as in, there is a simple setting 15:27:19 a single checkbox or such 15:27:22 so why isn't it on 15:27:24 prefs -> input box -> last spoken 15:27:30 oklopol: 'cuz sometimes it's annoying 15:27:31 oklopol, because many people don't want that I guess? 15:27:34 like if i'm talking to awesome 15:27:35 for hours 15:27:38 THOSE PEOPLE ARE WRONG 15:27:38 then suddenly asshole butts in 15:27:41 and i end up talking to asshole 15:27:54 o_o 15:27:56 well umm SHUT UP 15:28:05 you too fax 15:28:08 sorry 15:28:09 nah jk 15:28:21 you don't have to shut up 15:28:30 but it helps 15:28:38 but you have to agree with me on something, i'm getting tired of being different 15:28:38 alise_, like: "a, you are an a person." and if "asshat" joins in between those two tab completes... 15:28:48 -!- deschutron has joined. 15:28:52 -!- alise has quit (Ping timeout: 265 seconds). 15:29:06 that's a great real life example 15:29:09 AnMaster, you are an asshat person. 15:29:15 alise_ you're an alise_ person 15:29:31 alise_, yeah you can get mistakes like that 15:29:40 clearly it should be that I'm an awesome person 15:29:44 fax is a fax person 15:29:45 :( 15:30:01 oklopol, I know the example is far fetched! 15:30:04 that means frequent teleporter 15:31:09 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. 15:31:18 ouch 15:31:45 well assuming it's not my mistake, probably the case is that there's a simple way to fix it 15:32:07 i'm sure it's wrong, but the problem is the author probably didn't have the algo wrong, but just explained it wrong 15:32:34 -!- oerjan has joined. 15:32:45 i would explain it but what the algo does is a bit random without context 15:33:25 final year research project eh? 15:34:24 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). 15:34:32 this is my second year 15:34:33 loll 15:35:31 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 15:35:39 or not 15:35:46 also not that many mistakes actually 15:35:48 ouch 15:37:51 AnMaster: I didn't write it, so I don't care what you think :P 15:38:27 Gregor: i liked the notes but the dynamics sucked ass! 15:38:35 *sobblecopter* :P 15:38:42 what about rhythm 15:38:45 was that yours? 15:38:49 No 15:38:54 ...because that was pretty good too 15:38:58 :P 15:39:26 shoppe tiem. 15:39:32 ~~> 15:39:38 or wait maybe not just yet 15:40:34 ~~~~~~~~~> 15:40:54 -!- deschutron has quit (Ping timeout: 258 seconds). 15:46:25 -!- deschutron has joined. 15:47:42 i see 15:49:07 okay now really shoppe tiem 15:50:15 -!- adu_ has quit (Quit: adu_). 15:54:00 -!- adam_d_ has quit (Ping timeout: 265 seconds). 15:55:39 -!- adam_d_ has joined. 16:00:17 -!- adam_d_ has quit (Ping timeout: 265 seconds). 16:04:19 -!- adam_d has joined. 16:13:49 -!- adam_d has quit (Ping timeout: 265 seconds). 16:13:59 -!- adam_d has joined. 16:16:14 -!- charlls has joined. 16:19:49 -!- oerjan has quit (Quit: leaving). 16:25:30 15:23 < benmachine> besides which there are languages which are deliberately obnoxious 16:25:34 15:23 < EvanR-work> right 16:25:36 15:24 < Jafet> PLEASE DO NAME ONE 16:26:32 which channel? I recognise Jafet from #nethack 16:26:44 Malbolge's probably the best example of a deliberately obnoxious lang, though 16:26:55 i recognize jafet from people pasting what he's said 16:27:29 lol 16:27:50 #haskell 16:28:02 so maybe there too 16:29:19 fax: did you reply? 16:29:20 Gregor: then why not also put the undynamic'd versions up? 16:29:36 no 16:29:37 oh wait you do 16:30:00 I jost hjojddd 16:30:32 oh wait maybe you don't 16:31:06 -!- deschutron has left (?). 16:31:47 hi ais523 16:31:59 hi 16:32:46 * alise_ is defining the reals via continued fractions in coq 16:35:37 call me 0400243514 and whatever thing finland has, i can't find my cellphone, won't answer 16:35:59 should be something like +358 prolly 16:37:16 oklopol: who, me? 16:37:16 Callerying. 16:37:23 o---:) 16:37:24 whoever 16:37:24 thanks 16:37:28 * alise_ looks up the dailing code 16:37:31 why do you want called 16:37:34 too late 16:37:36 why do you want called 16:37:40 fizzie called 16:37:45 i told you 16:37:47 yeah it's +358 16:37:53 oklopol: what only one call accepted? 16:37:55 why would anyone want to talk on a phone?????? 16:37:59 fizzie: also good, now i can harrass you if i come to helsinki 16:38:08 I thought since I was in the same country, I'd best call just in case you were lying about the "no answer" thing. 16:38:13 fax: no one, cell phones are clocks you can find by calling them. 16:38:22 oh 16:38:34 -!- adam_d_ has joined. 16:38:45 oklopol: The number's on the first google-hit anyway, so no great loss there. 16:38:54 :P 16:39:16 alise_: i don't mind if you call me 16:39:32 now the fucking shoppe -> 16:40:12 oh won't answer 16:40:14 lame 16:40:17 oh well 16:40:23 i've talked to you on skype that is enough for one lifetime 16:40:24 -!- adam_d has quit (Ping timeout: 265 seconds). 16:41:07 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 16:42:08 there is something so modern-international about that 16:46:56 -!- lament has joined. 16:50:07 -!- FireFly has quit (Ping timeout: 268 seconds). 16:52:27 -!- FireFly has joined. 16:59:40 oklopol: They're there. 17:00:06 oklopol: It's Onerously Uptight Toccata 17:00:11 oklopol: Hence "OUT" 17:01:40 -!- adam_d_ has quit (Ping timeout: 265 seconds). 17:02:15 -!- coppro has joined. 17:02:20 -!- coppro has quit (Client Quit). 17:03:01 what it was actually played? 17:04:13 -!- coppro has joined. 17:08:53 alise_: Sort of :P 17:09:25 link 17:12:52 http://codu.org/music/auto/OUT-T5.ogg 17:13:02 It was "played" with Tapper, so I played the dynamics and tempo, not the notes. 17:14:21 eh? 17:14:49 I like it 17:16:16 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. 17:16:25 So when it's wildly impossible to play, you can still play it :P 17:19:58 Gregor: you have a gift for naming autogenerated music 17:20:16 Random-adverb random-adjective random-type-of-music. 17:20:19 Yes, quite the gift. 17:20:54 -!- adam_d_ has joined. 17:21:08 yep 17:21:18 ais523: the name is autogenerated too though :P 17:21:18 just you manage to pick particularly amusing random choices 17:21:33 Where by "you", you mean "rand()" :P 17:21:40 alise_: heh, then he has a gift for amusing random number generators 17:21:46 YES. 17:22:52 -!- charlesq__ has joined. 17:26:19 -!- charlls has quit (Ping timeout: 258 seconds). 17:27:27 ais523: i've done it before, it's always either a finn who calls or no one :< 17:27:42 once someone tried to call me who was not in finland, but it didn't work 17:28:14 -!- charlesq__ has quit (Ping timeout: 258 seconds). 17:28:17 oklopol: ah 17:34:01 oklopol: i can tryyyy 17:34:02 if you'll answer. 17:34:26 i will then 17:35:09 okayyyyyyyyyyyyy what is the number againyyyyyyyyyyy 17:35:26 0400243514 17:35:45 now i need to get skype downloaded 17:36:57 -!- adam_d_ has quit (Ping timeout: 265 seconds). 17:38:55 -!- coppro has quit (Quit: boarding). 17:40:13 (i seriously hope you don't actually do it... :P) 17:43:25 why not 17:43:49 because phone calls are scary 17:44:18 -!- lament has quit (Ping timeout: 276 seconds). 18:15:40 this will be so cool i could... 18:15:41 submarine it 18:20:38 * Sgeo is alarmingly tired 18:25:49 -!- jcp has joined. 19:03:29 hey guyez 19:03:30 I wrote a function 19:03:33 http://pastie.org/904126.txt?key=dmlvdatdbqpi68fo3gwjg 19:04:23 http://pastie.org/904128.txt?key=x8d87tccpvmsig80c46r3w here's the auxiliary proof i used 19:04:31 totally by hand i swear 19:05:40 that's fucking beautiful man 19:07:29 alise_: Hmm. For a second there I was going "wait, it's Monday... What's he doing here..." XD 19:07:57 pikhq: why's that funny 19:08:21 oklopol: sorry to disappoint you man but this is what i actually wrote http://pastie.org/904133.txt?key=sgwgk3z0vdxdip61onraow 19:08:28 conclusion: computers are better at writing progams than humans 19:08:29 *progams 19:08:32 *programs 19:09:00 oklopol: that omega is one wild-ass beast, you're in a proof right and it's to do with numbers right 19:09:02 and you type omega 19:09:05 then you press '.' 19:09:12 and it spits out something like http://pastie.org/904128.txt?key=x8d87tccpvmsig80c46r3w 19:09:16 and WHAMM totally proved man 19:09:19 alise_: that's pretty too, but not nearly as. 19:09:28 eventually we'll just have OmegaCoq 19:09:38 alise_: Unit-ness. 19:09:40 Theorem riemannhypothesis : blah blah blah. 19:09:42 omega. 19:09:43 Qed. 19:09:54 pikhq: of course i mean why is it funny that you thought that i mean it's an obvious thing to think :P 19:09:54 :/ 19:10:08 Ah. 19:10:13 * alise_ defines rational and irrational : R -> Prop 19:10:47 oh dear wait i need the continued fraction part to be optional 19:11:48 * alise_ defines sqrt(2) 19:13:15 Program CoFixpoint twos : CF := step 2 _ twos. 19:13:17 2 is not 0? 19:13:19 proved beyotch 19:13:27 Program is beautiful 19:13:47 Definition sqrt2 : R := real 1 (Some twos). 19:13:49 yeah some twos 19:13:51 just some of 'em 19:13:56 infinity of them to be precise 19:14:24 http://pastie.org/904145.txt?key=jynafvfiitwk3wphbwoqfq 19:14:30 here's what i need to do to prove that sqrt(2) is irrational 19:15:35 okay could we do as follows, you stop talking about coq till i learn it? 19:16:16 oklopol: no :D 19:16:22 don't worry, the wildcard' stuff makes no fucking sense to me either 19:16:26 it's just coinduction wizardry... 19:16:45 seriously you should learn coq though, i'm pretty sure i could prove anything... even that the world is flat 19:16:48 that's how awesome it is 19:17:09 have you actually proven anything nontrivial? 19:17:23 sqrt(2) irrational is like elementary school biology homework 19:17:44 oklopol, he's not even shown that it's sqrt(2) 19:19:22 oklopol: no :P 19:19:26 i'm only doing this 19:19:29 to test my reals 19:19:32 via continued fractions 19:19:37 Program CoFixpoint twos : CF := step 2 _ twos. 19:19:37 Definition sqrt2 : R := real 1 (Some twos). 19:19:37 Theorem sqrt2_irrational : irrational sqrt2. 19:19:37 intro i. 19:19:37 induction i. 19:19:38 simpl; auto. 19:19:40 assumption. 19:19:44 Qed. 19:19:45 and yes i didn't even prove it's the square root of two 19:19:48 i have no... arithmetic, as such 19:20:10 fax: okay lulz. i just glance at the codes to assess their prettiness. 19:20:11 oklopol: also, biology? 19:20:25 yeah biology, it's so easy it doesn't even need to be *math* homework 19:20:32 oklopl im mad at alise for being a dick to me 19:20:51 she was a dick to you? 19:20:55 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 19:21:03 then he said if i don't do it right now she won't talk to me any more 19:21:05 *she 19:21:08 fucking pronouns and irc 19:21:15 then I didn't, then she stopped talking to me 19:21:35 you are so short sighted alise that has nothing to do with it 19:21:48 alise_: it's not what you said, it's the way you said it 19:22:12 yawn 19:22:22 IT'S FUNNY TO ME 19:22:31 fax: i'm mad at her too now 19:22:47 http://fermatslasttheorem.blogspot.com/2006/05/basic-properties-of-cyclotomic.html 19:22:50 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 19:22:57 now let that be the end of it 19:23:55 no 19:25:12 no howso 19:34:08 In case anyone cares, the interpreter part of the interpreter was a bit easier than I thought it would be 19:34:22 Still need to make some tweaks though, but it can run Hello world 19:37:40 -!- charlls has joined. 19:52:10 fff 19:52:14 coq needs smarter pattern matching 19:54:10 -!- cheater2 has quit (Ping timeout: 264 seconds). 19:56:36 -!- zzo38 has joined. 19:56:41 Really, I ought to fix FlogScript uses all bcmath but I don't know the best way 19:57:20 -!- MigoMipo has joined. 19:59:00 -!- cheater2 has joined. 19:59:27 -!- zzo38 has left (?). 20:00:40 oklopol: more awesome noise: http://pastie.org/904213.txt?key=xwcjbezd3bn5212tsa0xwa 20:04:42 -!- tombom has joined. 20:06:24 -!- tombom_ has quit (Ping timeout: 240 seconds). 20:09:31 i got coq to print out "Anomaly. Please report." 20:10:19 -!- atrapado has joined. 20:14:54 heh 20:17:42 H : nat 20:17:42 n : nat 20:17:42 wildcard' : n <> 0 20:17:42 cf' : CF 20:17:42 H0 : rational (real H (Some (step n wildcard' cf'))) 20:17:44 ============================ 20:17:45 exists n0 : nat, rational (real n0 (Some cf')) 20:17:47 ouch 20:17:54 that was /not/ the issue i was expecting with this function 20:18:16 H0 : rational (real H (Some (step n wildcard' cf'))) 20:18:16 ============================ 20:18:16 rational (real n (Some cf')) 20:18:42 basically i'm having to prove that a continued fraction is rational, given that the same fraction plus one extra term is rational 20:18:58 the problem arises if we expand what rational is shorthand for: 20:19:01 exists i : nat, is_None (a_Sn i (real n (Some cf'))) 20:19:11 where a_Sn is a rather complex recursive function. 20:19:58 H0 : is_None (a_Sn x (real H (Some (step n wildcard' cf')))) 20:19:59 ============================ 20:19:59 is_None (a_Sn (pred x) (real n (Some cf'))) 20:20:00 this should be easier 20:23:18 * alise_ rejiggles is_Some and is_None a bit to make things easier 20:32:53 bye for a bit 20:32:55 jiggles? 20:32:57 bye 20:33:09 -!- alise_ has quit (Remote host closed the connection). 21:00:31 -!- calamari has joined. 21:04:49 -!- charlls has quit (Ping timeout: 258 seconds). 21:10:03 -!- oobe has joined. 21:12:32 -!- jcp has quit (Quit: I will do anything (almost) for a new router.). 21:14:05 oobe: It's spelled "oboe" 21:14:32 i think i know how to spell my own name 21:16:44 However, you shall now become the new pooppy (coppro) in my head :P. How about ... carlinet. 21:18:48 is oobe an actual norwegian name`? 21:18:49 *? 21:19:43 nope 21:19:53 its just my nick i use 21:20:23 oh sorry didn't notice your name is actually ascii pr0n 21:20:39 \o/ 21:20:45 :( 21:20:55 you're too short 21:21:05 so you don't get a body 21:21:05 \o/ 21:21:09 \o/ 21:21:09 | 21:21:09 |\ 21:21:24 -!- augur has quit (Ping timeout: 276 seconds). 21:32:06 I'm not sure I see the pr0n interpretation very well. 21:32:34 it was a complicated joke. 21:43:00 -!- charlls has joined. 21:55:11 -!- charlls has quit (Quit: Saliendo). 22:00:32 -!- tombom_ has joined. 22:02:14 -!- tombom has quit (Ping timeout: 260 seconds). 22:07:04 -!- tombom__ has joined. 22:07:37 -!- tombom_ has quit (Ping timeout: 246 seconds). 22:08:25 -!- jcp has joined. 22:19:57 -!- MigoMipo has quit (Read error: Connection reset by peer). 22:26:38 -!- augur has joined. 22:29:47 george carlinet 22:34:07 -!- alise has joined. 22:36:04 hi 22:36:11 -!- augur_ has joined. 22:36:12 -!- augur has quit (Read error: Connection reset by peer). 22:36:22 -!- augur_ has changed nick to augur. 22:38:15 anyone wanna do my proof for me 22:39:12 alise it's because you don't listen to me 22:39:27 k 22:43:16 -!- augur has quit (Read error: Connection reset by peer). 22:43:38 -!- augur has joined. 22:45:32 -!- augur has quit (Read error: Connection reset by peer). 22:45:36 -!- augur_ has joined. 22:45:58 -!- augur_ has changed nick to augur. 22:46:09 MISSING: One underscore 22:46:11 REWARD: $0 22:49:33 H0 : is_None (a_Sn x (real H (Some (step n wildcard' cf')))) 22:49:33 H1 : x <> 0 22:49:34 ============================ 22:49:34 exists i : nat, is_None (a_Sn i (real n (Some cf'))) 22:49:34 it's a start 22:50:04 -!- augur has quit (Read error: Connection reset by peer). 22:50:52 -!- augur has joined. 22:53:57 H0 : is_None (CF_a_Sn x (step n wildcard' cf')) 22:53:58 H1 : x <> 0 22:53:58 ============================ 22:53:58 is_None (CF_a_Sn (safe_pred x H1) cf') 22:54:01 this should honestly be really trivial :P 22:55:25 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... 22:55:27 -!- olsner_ has joined. 22:55:31 Program Fixpoint Q_of_rational_CF (cf : CF) (H : exists n, rational (real n (Some cf))) : Q := 22:55:31 match cf with 22:55:31 | final n _ => Q_of_nat n 22:55:31 | step n _ cf' => Q_of_nat n + 1 / Q_of_rational_CF cf' _ 22:55:31 end % Q. 22:55:33 that's the entire function 22:55:41 the whole complexity is that tiny _ in the Q_of_rational_CF recursive call 22:55:45 because it's a bloody proof 22:56:03 -!- augur has quit (Read error: Connection reset by peer). 22:56:07 -!- olsner_ has quit (Client Quit). 22:56:27 -!- augur has joined. 22:58:03 -!- augur has quit (Read error: Connection reset by peer). 22:58:15 -!- augur has joined. 23:00:02 gah, I'm stuck! 23:01:27 alise, hm? 23:01:38 trying to do this proof 23:03:15 http://pastie.org/904537.txt?key=rqxoszxqfg7nkfvbf8jwa 23:03:29 I think I can think of Yet Another definition for rational/irrational that makes this easier 23:03:47 not based on the hugely complicated CF_a_Sn function 23:04:27 hmm ... no 23:04:29 I need CF_a_Sn to access elements 23:05:29 I think I failed to win Agora because I was inactive 23:08:40 -!- Gracenotes has joined. 23:10:07 * Sgeo goes to play with some worms 23:11:55 -!- FireFly has quit (Quit: Leaving). 23:13:23 -!- tombom__ has quit (Quit: Leaving). 23:20:05 -!- oerjan has joined. 23:28:07 -!- augur_ has joined. 23:28:13 -!- augur has quit (Read error: Connection reset by peer). 23:30:46 Sgeo: i presume the computerised sort 23:32:21 "Nobody loves me, everybody hates me. Think I'll go and eat worms!" 23:33:14 -!- augur_ has quit (Ping timeout: 260 seconds). 23:34:19 yep, there was an accident and every active player won Agora 23:36:33 here's some wonderful noise: http://pastie.org/904583.txt?key=bg0znn8ou1ynm5vozuag 23:36:34 everything after exist (fun m : nat => m <> S n0) n0 23:36:42 is a computer-generated proof that... drumroll... n is not S n 23:36:49 it actually gets cut off: 23:36:51 (fun .. => .. 23:36:51 .. 23:36:52 .. 23:36:52 .. 23:36:52 end) I 0%Z Omega19 in 23:36:54 for being too absurdly long to display 23:37:23 can you imagine a proof of that identity even remotely as advanced before COMPUTERS???? 23:37:34 -!- oklopol has quit (Ping timeout: 252 seconds). 23:38:11 http://pastie.org/904585.txt?key=5ijpll8mfjaxlpcn9wthq 23:38:15 this definition is also acceptable. 23:42:10 -!- Oranjer has joined. 23:55:54 -!- cheater3 has joined. 23:57:41 -!- cheater2 has quit (Ping timeout: 276 seconds).