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