00:00:08 <fax> I can compute it for 2x2 and 3x3 :P
00:00:12 <fax> and I know some of the rules
00:00:16 <fax> but that's all
00:00:16 <oerjan> in other dimensions that doesn't work unless you use (n-1) vectors to cross
00:00:54 <AnMaster> fax, I can compute it for arbitrarily large matrixes
00:01:07 <AnMaster> but I hate anything larger than 3x3
00:01:15 <AnMaster> due to the huge amount of work in it
00:01:29 <AnMaster> finding sub-determinants and so on (if that is the English term for it)
00:02:22 <AnMaster> oerjan, but with n-1, how could that even work?
00:02:34 <AnMaster> oerjan, you can only take det() on a square matrix right?
00:02:59 <AnMaster> oerjan, which means that n-1 for 5 wouldn't really work out as far as I can see
00:04:56 -!- tombom has quit (Quit: Leaving).
00:05:25 <oerjan> AnMaster: you let the product of v_1, ..., v_(n-1) be the unique vector x such that det (v_1,v_2,...,v_(n-1),y = x.y for all y
00:05:50 * AnMaster mentally converts that to math notation
00:06:02 <AnMaster> oerjan, I find it *extremely* hard to read ASCIIed math notation
00:06:12 <fizzie> But did you know that the coefficients of the characteristic polynomial of H, where H is the Hessenberg matrix from Arnoldi iteration of matrix A and vector b, turn up (with negative sign) as the last column of pinv(K)*A*K, where K is the Krylov matrix for A, b and pinv() is the "usual" pseudoinverse?
00:06:13 <oerjan> mind you i'm not sure if my definition has the right handedness
00:06:38 <oerjan> if not just switch things around a bit
00:07:01 <fizzie> I just said, the usual (Moore-Penrose?) pseudoinverse.
00:07:02 <alise> ascii math notation is easy you're just a whiner :)
00:07:14 <AnMaster> oerjan, how do you define handedness for more than 3 dimensions?
00:07:18 <fizzie> (This was a homework bit for yesterday's Matrix Computations thing.)
00:08:15 <oerjan> AnMaster: such that the product of e_1, e_2, ..., e_(n-1) is e_n, i presume
00:08:43 <oerjan> (e_i being the unit vector of the i'th axis)
00:09:29 <oerjan> which means my handedness above was right for 3, i think
00:11:59 <oerjan> AnMaster: btw one intuition for determinant (which ignores the sign though) is that if you take the hypercube spanned by e_1,...,e_n (i.e. the cube with all coordinates in [0,1]) and apply a matrix M to it, then the _volume_ of the resulting hyperparallelogram is abs(det M).
00:12:17 -!- augur has joined.
00:12:53 <AnMaster> oerjan, anything involving the word "hypercube" definitely doesn't feel like related to my "intuition"
00:13:12 <oerjan> or equivalently, the hypercube spanned by vectors v_1,...,v_n has volume abs(det(v_1,...,v_n)).
00:13:23 <oerjan> AnMaster: well you can use it or 2 and 3 dimensions too
00:13:41 <AnMaster> well that is a trivial case I gues
00:14:11 <AnMaster> oerjan, so for 2x2 mat, that would be ad-bc
00:14:19 <oerjan> s/hypercube/hyperparallelogram/, last one
00:15:12 <fizzie> Isn't it pretty: http://www.cis.hut.fi/htkallas/hw7.pdf (Usually my homework answers are horrible handwaving, but this one is pretty explicit. Though that does steal a pretty complicated Theorem 9.7 out of the lecturer.)
00:15:34 <oerjan> btw hyperparallelogram is probably not the right term, although it _is_ a parallelogram in 2 dims
00:15:47 * Sgeo wants to take math courses
00:16:25 <AnMaster> fizzie, what language is that code?
00:16:33 <oerjan> AnMaster: one corner of the parallelogram is the origin. two of the others are (a,b) and (c,d), the last one is their sum
00:17:09 <AnMaster> after you said "hyperparallelogram"
00:17:18 <fizzie> AnMaster: Matlab, and the >> is just the prompt.
00:17:55 <fizzie> AnMaster: Or Octave, in this case, but with a Matlab prompt to make the recipient feel more at home.
00:18:14 -!- augur has quit (Ping timeout: 256 seconds).
00:18:37 <oerjan> AnMaster: ah, 3 dims is parallelepiped
00:19:13 <oerjan> somehow i hadn't quite made that a household name, though i've certainly seen it :D
00:19:21 <AnMaster> oerjan, I admit however I was fuzzy on the spelling
00:19:28 <AnMaster> oerjan, but I had a math teacher mention it a lot
00:20:25 <oerjan> "Coxeter called the generalization of a parallelepiped in higher dimensions a parallelotope."
00:20:31 <fizzie> I've got the phrase "rhombus, the neglected parallelogram!" stuck in my head, but I can't remember where I read it from.
00:20:37 <oerjan> _that_ i'm not sure i've heard
00:21:06 <AnMaster> oerjan, he also loves making a huge distinction between "geometrical vectors" and "algebraic vectors"
00:21:12 -!- MigoMipo has quit (Remote host closed the connection).
00:21:20 <AnMaster> (not sure of translations here)
00:21:48 <AnMaster> wikipedia seems to call the former http://en.wikipedia.org/wiki/Euclidean_vector
00:22:35 <Sgeo> fizzie, no chance it's Triangle and Robert, is it?
00:22:44 <fizzie> oerjan: Couldn't you just call it "paral".("le"x($dim-1))."piped"? Then you'd always have the dimension explicitly in the name.
00:23:09 <oerjan> well you _could_, but that would be evil.
00:23:26 <AnMaster> Sgeo, oh that, one of the worst strips I ever started reading and then gave up after 120 or so strips
00:23:52 <AnMaster> fizzie, how do you pronounce it?
00:24:06 <AnMaster> fizzie, and what programming language?
00:24:22 <fizzie> That was the Perl notation.
00:24:26 <oerjan> fizzie: that x should be ^ in my view
00:25:17 <oerjan> also you would have to allow for $dim being a variable, and/or transfinite
00:25:20 <fizzie> Yes, but I was worried you'd think I'd just want the number there, and not actual repetitititition of lelele.
00:25:42 <AnMaster> oerjan, in math it is $*d*i*m isn't it? ;P
00:25:53 <oerjan> fizzie: not a chance to avoid that once it's generalized
00:26:08 * oerjan swats AnMaster -----###
00:26:28 -!- BeholdMyGlory has quit (Read error: Connection reset by peer).
00:26:31 <alise> AnMaster: triangle and robert is great! not that i've read much
00:26:51 <AnMaster> alise, we have different tastes clearly
00:27:02 <AnMaster> "well drawn" is not in your list :P
00:27:07 <fizzie> A Pythonist would (well, could) say "paral"+"le"*(dim-1)+"piped", I believe.
00:27:18 <AnMaster> well, not so much in mine either
00:27:36 <Sgeo> AnMaster, I loved it
00:27:37 <AnMaster> fizzie, is thyat string duplication with *?
00:28:12 <fizzie> Yes, it does string multiplication if you give a string and a number.
00:28:32 <fizzie> >>> "paral"+"le"*4+"piped"
00:28:52 <Sgeo> alise and I have the same tastes? o.O
00:29:19 <fizzie> I don't *think* it was Triangle and Robert, though; I have a feeling it was a human(oid) character in some bit of fiction.
00:29:50 <fizzie> Right, it was just an old Nukees strip: http://www.nukees.com/comics/19980318a.gif
00:30:09 <fizzie> But at least that's not well drawn either.
00:31:55 <Deewiant> On rhombuses: http://www.penny-arcade.com/comic/2009/1/9/locked-brutal-combat/
00:32:15 -!- FireFly has quit (Quit: Leaving).
00:32:35 <fizzie> Deewiant: You mean "rhombi", don't you?
00:32:53 <fizzie> "Pl. rhombuses (7-8 -us's); 8 rhombi." I guess they both do, yes.
00:33:09 <fizzie> But it sounds better as "rhombi", though also a bit vacuum-roboty.
00:33:18 <Deewiant> I had just typed "rhombus" already and it's less keypresses to add "es" than to backspace twice and add "i".
00:33:33 <fizzie> Rhoomba, the rhombus-shaped Roomba.
00:33:34 <oerjan> use rhomboi for the original greek (i think)
00:34:15 <fizzie> fungot: Have you read that particular Penny-Arcade comic, by the way?
00:34:15 <fungot> fizzie: so i says to her, though.
00:34:27 <fizzie> fungot: What does that even mean?
00:34:27 <fungot> fizzie: this is fantastic. maybe after this we can subjugate some indigenous peoples. or, the devil. you are a woman raised as a man.
00:34:42 <fizzie> Subjugating the devil sounds dangerous business.
00:35:05 <AnMaster> don't make me laugh out loud atm
00:35:37 <oklopol> haha you're better off using your grandma as a math forum than #math
00:35:48 <oklopol> "hey wanna hear about this interesting thing i came up with?" "go fuck yourself"
00:38:13 <alise> fizzie: dammit i'm laughing because of fungot but I'm trying to look all serious
00:38:13 <fungot> alise: my guess? the bullshit. there's no shame in that. well, he hasn't been playing very well. and, i was pushing them, and then i saw something. something big.
00:38:16 <alise> daaaamn youuuuuuuuu
00:38:18 <fungot> Available: agora alice c64 ct darwin discworld europarl ff7 fisher ic irc jargon lovecraft nethack pa* speeches ss wp youtube
00:38:21 <fungot> alise: annarchy's mother: anne claire, eat your dinner. you know, potty issues. there. he's got these friends back at the flag named earthquake and demise, right? i bet it's something bad in there.
00:39:15 <fungot> Selected style: pa (around 1200 transcribed Penny Arcade comics)
00:39:27 <fungot> Selected style: darwin (Books by Charles Darwin -- you know, that evilution guy)
00:39:33 <fungot> AnMaster: he shows " page 111) that when naturalists confine their attention to agriculture, were fnord when a species has once disappeared it never reappeared.), and no doubt every female flower which i examined appeared more like a dandy than a warrior, but he has seen/ carcasses :) dead seals. wherever these slaty feldspathic rocks abound, greenstone seems common; at/ c. persica et turcica, mr. f. fnord six feet, in proporti
00:40:00 <fungot> Selected style: europarl (European Parliament speeches during approx. 1996-2006)
00:40:32 <AnMaster> fungot, this should prevent alise from laughing if he wan'ts to avoid it
00:40:34 <fungot> AnMaster: mr president, ladies and gentlemen, and by the governments of both old and new member states have long since been prepared and sent to parliament.
00:40:52 <fungot> AnMaster: i am happy to say that any such principle needs to be stressed that the guidelines in leader+ now need to be repeated. i have to say that i have already criticised the method used for each individual, which remains and will always be positive and enriching factor for europe.
00:41:38 <oklopol> i was invited in this math high school thing, but i didn't go because i had a gf
00:42:03 <oklopol> cuz true love is more important than math
00:42:15 <oklopol> we broke up when i started high school
00:42:27 <alise> "and no doubt every female flower which i examined appeared more like a dandy than a warrior, but he has seen/ carcasses :) dead seals." --Darwin
00:49:38 <alise> the mathematics that can be proved is not the true mathematics.
00:49:44 <alise> i.e., only the negations of proved things are true.
00:51:33 <fax> -1 * -1 = -1
00:52:04 <fax> I wish I understood cubic truth :(
00:53:39 <alise> -m * -n = -(m*n) clearly
00:53:46 <Gregor> TIME CUBE IS BETTER THAN YOUR QUEER GOD
00:53:46 <alise> therefore -1 * 1 = 1
00:54:00 <Sgeo> http://i.imgur.com/SQHYl.jpg . Clicking a piece toggles the piece, and pieces orthogonally adjacent. THe goal is to get all pieces to be cylinders, or all pieces to be cones. This configuration should be solvable in 3 moves. How easy/hard are those moves to figure out? I know how to solve it given a live board, but it always takes me a while
00:55:14 <Sgeo> Also, are there any unsolvable configurations? If not, I can simplify my reset algorithm a bit. Currently, it just blanks the board and simulates 3 clicks
00:57:13 <fax> Sgeo what is this made in??
00:57:25 <fax> "Clicking a piece toggles the piece, and pieces orthogonally adjacent" -- lights out!! this game is OLD
00:57:32 <alise> some virtual world.
00:57:37 <alise> you can tell because it's sgeo and it has health meters
00:57:38 <Sgeo> It's in Active Worlds. The code for the puzzle itself is in C#
00:57:46 <fax> it's idk equations in Z2
00:57:47 <Sgeo> I did not add the health meters
00:58:05 <fax> you can solve every solvable puzzle in a maximum of 9 clicks :D
00:58:08 * fax proves the trivial
00:58:09 <Sgeo> Clicking a piece doesn't toggle all pieces in a row or column
00:58:38 <Sgeo> I originally programmed it that way, since I misremembered the original game we're um, recreating
00:59:34 <oklopol> why is http://mathoverflow.net/questions/18696/how-to-write-if-else-as-mathematic-equation stupid?
00:59:51 * Sgeo feels vindicated by oklopol's question.
01:01:19 <fax> it's stupide because programs are alredy formal language
01:01:28 <fax> you don't have to turn everything into 'math'
01:01:31 <fax> it already IS
01:01:37 <alise> and because he clearly has no idea how booleans work
01:01:51 <alise> he seems to think everything as to be arithmetic
01:02:39 <oklopol> "fax: oerjan, another thing I really want to do is make a 4D (or more D..) world that you can immerse yourself in :(" <<< been wanting to do this since like forever
01:03:13 * Sgeo takes interest
01:03:26 <fax> http://eusebeia.dyndns.org/4d/vis/vis.html
01:03:31 * fax has been searching for answers
01:03:34 <pikhq> oklopol: The question is like asking "how do you write if-else in a program".
01:04:20 <pikhq> Sorry, change that.
01:04:27 <pikhq> "How do you write if-else in programming"
01:05:18 <alise> How do you shot if-else
01:06:18 <oklopol> fax: you don't know the definition of a determinant?
01:07:06 <fax> anyway definitions are overrated
01:07:19 <oerjan> Sgeo: if you can prove for each piece that there is a sequence of moves to toggle _just_ that piece, then all configurations are solvable, otherwise not.
01:07:22 <pikhq> One could, for instance, define yourself sufficiently formal psuedocode and just write "if foo then bar else baz". Or you could do that in lambda calculus. Or you could just write it as a piecewise function. Or you could do some rather clever arithmetic to get it down to a single arithmetic statement (though I doubt that's feasible with the example there)
01:07:27 <fax> if you have two equivalent characterizations of something, which one is the 'definition'?
01:08:11 <alise> pikhq: there is an easy way to switch on 0/1 arithmetically
01:08:11 <Oranjer> the one that places the term in a category of differentiated terms
01:08:11 <oerjan> because any others can be solved by combining those sequences
01:08:13 <alise> with an else clause
01:08:18 <alise> I forget the exact definition though
01:08:27 <Sgeo> I've figured out how to toggle just the middle piece
01:08:38 <fax> by the way I saw a really gorgeous proof using iverson notation
01:08:49 <fax> in Concrete Maths
01:08:50 <Sgeo> No, I don't think I have
01:09:05 <fax> lol oklopol has completely lost respect for me
01:09:17 <oerjan> Sgeo: oh wait you said just 3 moves? then what i said is not true. in fact it cannot be.
01:09:41 <fax> Sgeo I would think of the inverse problem
01:09:50 <fax> starting from the solution, what moves take you to a given state
01:09:52 <Sgeo> Well, if I can show that it's always solvable in X moves, that's enough
01:10:02 <oerjan> if it should always be <= 3 moves i mean
01:10:33 <Sgeo> It's just that due to the way I scramble the board, there's a solution in 3 moves for any state achievable by this scrambler
01:10:51 <oerjan> Sgeo: as fax said, 9 moves is enough for everything that can be solved
01:11:10 <lament> 9 moves should be enough for anybody
01:13:48 <Sgeo> Wait, how is that trivial?
01:14:03 <fax> Sgeo, it doesn't prove that everything has a solution
01:14:04 <oklopol> oh the question was about how you'd express if-then in math? i just read "what natural set of mathematical operations on reals can be used to compile if-thens to math?"
01:14:44 <Sgeo> But I still don't see how 9 moves is enough to solve all solvable cases
01:14:59 <fax> because if you press twice on the same place that = doing nothing
01:15:01 <oerjan> Sgeo: because you never need to click a piece twice (just cancels out), and the order you click them doesn't matter
01:15:15 <alise> fax: you just abused =
01:15:23 <fax> no I didn't
01:15:33 <alise> no more than i did
01:15:35 <oklopol> "fax: if you have two equivalent characterizations of something, which one is the 'definition'?" <<< depends on author, in this case i'd be asking for *a* definition
01:16:06 <fax> 2^9 different sets of moves you can do
01:16:10 <fax> 2^9 different boards....
01:16:22 <fax> I wonder if they are equal sets though
01:17:13 <Sgeo> If two different move sets can take you to the same board, then the answer is no, right?
01:17:24 <oklopol> "fax: lol oklopol has completely lost respect for me" <<< i was just reading logs, i only lose respect for myself for not remembering definitions, from other people i just expect the capability to learn the matters at hand at a given time
01:17:42 <fax> I just don't really care about having a definition
01:17:49 <fax> because I know the important properties of it
01:18:00 <alise> fax: CONSTRUCTIVISM BITCH
01:19:10 <oerjan> !haskell (9*8*7)/6 + (9*8)/2 + 9
01:19:20 <oklopol> "alise: fax: you just abused =" <<< why is it abusing the definitions, it's the relation a^2 = 1 in the abelian group of move sequences
01:19:46 <oklopol> my brain isn't really here, also wow i finished the log
01:19:53 <alise> oklopol: fax always whines about me abusing =
01:19:55 <oerjan> Sgeo: btw your problem can be solved with determinants
01:20:06 <oklopol> oh well i don't know much about constructivism
01:20:17 * Sgeo has worse problems than this
01:20:23 <oklopol> this issue is way more subtle than me
01:20:26 <Sgeo> I can get away with not understanding this in depth
01:20:33 <Sgeo> There's another puzzle that I can't get away with it
01:21:33 <Sgeo> Also, I don't really know what determinants are? I think something to do with matrixes and solving multiple multivariable equations?
01:21:34 <oerjan> hey i have a Determinant.hs file. let's see...
01:23:01 <oklopol> fax: if you know even a few of its basic properties, you'll probably know a definition for the determinant :P
01:24:32 <alise> oklopol: constructivism: you must actually show a value that obeys certain constraints, if you want to prove such a value exists
01:24:33 <oerjan> Sgeo: yes. if the determinant is nonzero then every equation with that matrix is solvable. it turns out your problem can be expressed as a matrix equation.
01:24:38 <alise> you do this by removing ~~p -> p. you probably know that
01:24:49 <alise> ~~p is pretty damn strong evidence for p though :P
01:25:07 <Sgeo> How can it be expressed as a matrix equation? o.O
01:26:12 <oklopol> alise: i know that much, how does that make fax's statement incorrect?
01:26:19 <oerjan> Sgeo: a 9*9 matrix. item M_i,j is 1 if pushing piece i toggles piece j, 0 otherwise.
01:27:16 <Sgeo> How can we be sure that that maps to something that determinants are sensible for?
01:27:56 <oklopol> because they are used when solving matrix equations
01:28:36 <oerjan> be patient. now make a vector v of length 9 with 0's and 1's. then M v is a vector whose i'th coordinate is odd iff pushing the pieces that are 1 in v will toggle that piece.
01:28:53 <alise> oklopol: oh i was just talking about his I don't need a definition for determinants I have the properties
01:29:16 <alise> of course a constructivist - he's one, being a dependent folken - would demand a definition before even talking about properties
01:29:23 <alise> (folken: singular of folk)
01:29:27 <oerjan> (this is really a question about the field Z_2, but we can talk about odd and even instead)
01:29:34 <alise> it stands towards reason
01:29:41 <alise> ooh, geometric logic proofs!
01:30:03 <Sgeo> Where can I read tutorials about this sort of math?
01:30:25 <oerjan> Sgeo: now it happens to be that you can achieve _all_ vectors as M v in this way, iff det M is odd.
01:30:40 <oerjan> in other words all configurations are solvable iff det M is odd.
01:31:55 <oerjan> on the other if it isn't, then you can do some matrix operations to get a summary of exactly what configurations you can solve.
01:32:01 <Sgeo> What does each vector represent, exactly?
01:32:14 <oklopol> v is what buttons you push
01:32:30 <oerjan> Sgeo: the original vector v represents button pushing. 0 no, 1 yes.
01:32:51 <alise> i should do a tri-valued logic that doesn't just have 3 = unknown it's boring
01:32:52 <oerjan> M v represents buttons toggled. odd yes, even no.
01:33:00 <Sgeo> M is basically a function that takes a vector and returns a vector?
01:33:42 <oklopol> then we have to solve M v = y for v, where M is the rules of the game, and y is the desired outcome (which things are circles on the board), and if det M is odd, then we can divide by M to get M v = y <==> v = M^-1 y, and now "M^-1 y" is just an ordinary vector, which is a solution for the game
01:33:53 * Sgeo is not used to struggling with math
01:34:29 <oerjan> Sgeo: incidentally if det M is odd, then we can _invert_ the matrix to get all solutions.
01:34:38 <oerjan> (inversion mod 2 here)
01:34:46 * oklopol is trying his best to ruin oerjan's explanation by shortcutting it
01:34:58 <oklopol> well more like being faster i guess
01:35:05 <Sgeo> If M v's exist enough such that there's an M v for each configuration, all configurations are solvable
01:35:09 <oerjan> speed is always my problem
01:36:12 <Sgeo> How do you learn what an odd and even determinant means
01:36:26 <oklopol> it's not about odd/even usually, it's about nonzer/zero
01:37:03 <oklopol> it's just we're working in Z_2 here (the space with just two objects, odd and even), so zero = even, and the only nonzero object is "odd"
01:37:21 * Sgeo wishes he asked about a more pressing problem
01:37:28 <alise> Z_2 is also known as booleans
01:37:47 <oklopol> i would say booleans are the boolean algebra formed by those two, not the field
01:38:07 <alise> hmm i guess i see the algebra as built upon the type
01:38:08 <oklopol> or perhaps type inference will take care of that
01:38:09 <oerjan> Sgeo: determinants work in any _field_. we are really working in the field Z_2 (mod 2 arithmetic) here
01:38:18 <alise> so boolean is true | false, the algebra is all the operations
01:38:28 * oerjan swats oklopol, then himself -----###
01:38:36 <Sgeo> Wait, M is just a matrix?
01:38:50 <oklopol> normal matrix, but the field is Z_2 and not real numbers like usually
01:38:51 <Sgeo> I need a tutorial on this stuff
01:39:00 <Sgeo> Thought it was a function
01:39:06 <alise> 15:37:12 <pikhq> However, ((int)NULL) does not necessarily equal 0.
01:39:06 <alise> oh, so that means (int)(void*)0 doesn't have to be 0, heh
01:39:14 <Sgeo> I was like "You're dividing by a function?"
01:39:25 <oerjan> Sgeo: there is a one-one correspondence between matrices and linear functions between vectors
01:39:26 <oklopol> well it is, see matrices are in fact a representation for "linear functions", which are these simple kind of functions
01:39:58 <oklopol> clearly only one of us is needed here
01:40:04 <Sgeo> How do you learn all this? Better yet, how can I learn all this?
01:40:14 <alise> well f*g is clearly function composition by symbol analogy
01:40:15 <oklopol> well university does wonders
01:40:21 <alise> so f/g is the reverse of function composition
01:40:31 <alise> clearly 1/f gives (g,h) where f is the composition of the two
01:40:39 <alise> work out the rest yourself
01:40:40 <Sgeo> No online stuff?
01:41:06 <oerjan> Sgeo: linear algebra for the matrices in general, then number theory/higher algebra for the Z_2 part
01:41:09 -!- augur has joined.
01:41:29 <oerjan> (ring/field theory from the higher algebra)
01:41:47 <oklopol> there probably is online stuff, but online tutorials for math stuff are usually only found for trivial things
01:41:52 <oklopol> this might belong in that category
01:42:42 <oklopol> well of course you can find books online but i mean these sort of quick tutorials to X you can't really find on galois cohomologies
01:42:57 <oklopol> (i have no idea what those are)
01:43:53 <oklopol> Sgeo: also read what alise said about composition, that's exactly what matrix division is, inverting the linear function represented by the matrix.
01:44:24 <oerjan> i know a bit of galois theory, and a bit of cohomology, but i have no idea how they combine...
01:44:28 <oklopol> turns out linear functions are invertible (they have normal function inverses) iff their determinant is nonzero
01:44:43 * Sgeo doesn't even recognize what "galois" is supposed to mean
01:45:02 <Sgeo> oklopol, that makes a lot of sense somehow
01:45:25 <oklopol> Sgeo: yes, especially if you remember the volume definition of the determinant
01:45:37 * Sgeo still doesn't quite know what a determinant is
01:45:55 <oklopol> well it's just a function from matrices over a field to the field itself
01:46:01 <oklopol> which has a few nice properties
01:46:15 <oerjan> Sgeo: that volume thing i explained to AnMaster earlier today
01:46:20 <oklopol> in special cases like reals you have, as oerjan mentioned, interesting geometric properties too
01:46:50 * Sgeo has no clue how to even get started learning this stuff
01:47:16 <oklopol> i'd get a book on linear algebra and do exercises like crazy
01:47:16 <fax> what stuff??
01:47:29 <fax> yeah linear algebra is the best thign
01:47:33 <fax> but determinants arean't.....
01:47:49 <oklopol> nothing wrong with determinants
01:48:17 <oklopol> where you don't have any of their less useful properties, just invertibility
01:48:35 <oklopol> i mean most of the time we just need to know whether the determinant is nonzero
01:48:44 <Sgeo> I suppose none of this is related to Computer Science? Maybe I should stick with this college and Minor in math
01:48:49 <oklopol> in fact so often it would even make sense to have a separate name for such a function
01:48:59 <oklopol> or maybe that's not true, just my impression
01:49:38 <oklopol> all you need to know is learning things is related to knowing things is related to computer science
01:50:13 <oklopol> i really have to go to sleep ->
01:50:56 * Sgeo is going to forget about everything and play a game
01:52:29 <oerjan> Sgeo: i calculate the determinant to be -7, thus odd, thus everything is solvable
01:57:31 -!- coppro has quit (Ping timeout: 246 seconds).
02:04:03 <pineapple> does anyone know of implementations of (P)RNGs in brainfuck?
02:04:57 <pineapple> or would i be better off plugging /dev/random into stdin?
02:05:37 <alise> there's a langtons ant based thing but it gives the same result every run
02:05:42 <alise> there's no source of entropy in bf
02:05:52 <alise> but you can use e.g. user input to seed it multiple times
02:07:31 <fax> Sgeo I'm trying to prove this lights out thing by brute force
02:07:37 <fax> I don't really know how long it will take
02:08:51 <pikhq> There is a PRNG on the esolang wiki's algorithms page.
02:09:20 <pikhq> But obviously you're going to find a decent source of entropy to make it even vaguely useful.
02:09:38 <pikhq> (I suggest "Please pound on the keyboard")
02:10:43 <pineapple> bah... all my decent ideas for entropy kill the use of stdin
02:11:46 <pikhq> Well, yeah. There aren't any other sources of input at all.
02:11:49 <fax> random numbers in brainfuck shouldn't be hard
02:11:53 <oerjan> pineapple: cat your entropy source and input together?
02:11:57 <fax> oh it's been done
02:12:10 <pikhq> fax: Brainfuck has only one non-deterministic feature. ","
02:12:22 <fax> pikhq of course I meant pseudorandom :(
02:12:43 <fax> wow I'm already through 341 of 512 cases!
02:13:10 <oerjan> fax: wth you're not just doing the 9 pieces?
02:13:16 <fax> oerjan just 9
02:13:32 <fax> my algorithm doesnt take into account any symmetries
02:13:45 <fax> I'm doing a formal proof by brute force
02:14:07 <oerjan> fax: i mean, you're not just checking if you can get each single piece toggled?
02:15:12 <fax> iim trying to prove
02:15:12 <fax> Theorem complete : forall a b c d e f g h i, moves (a::b::c::d::e::f::g::h::i::nil) win.
02:15:20 <fax> which says that for every starting board you can solve it
02:15:28 <fax> by using a finite number of moves
02:15:46 <fax> so I could play each board and that would prove it, but I wrote a thingy that plays it for me instead
02:15:51 <fax> it's really really stupid ;D
02:16:04 <oerjan> now prove it for an m*n board ;D
02:16:06 <fax> I didn't even have to show that moves are comutative or doubled up cancel out
02:16:07 <fax> or symmetries
02:18:52 <fax> I just axiomatized what moves are valid (all 9 of them)
02:19:01 <pineapple> assuming that a move flips 5 cells in a + pattern, doesn't wrap around
02:19:04 <fax> as a data type
02:19:12 <fax> it's taken over 10 mins :D
02:19:37 * fax is on case 210/512
02:19:46 <fax> if I took ONE symmetry into account it would be done now
02:19:56 <fax> and there'sa lot more than one
02:20:18 <fax> if I proved it using a clever method that doesn't involve search..... I wonder if I would still be doing it :P
02:21:11 <pineapple> enumerate all 3 and 4 cell positions, invert for 5-8
02:21:52 <fax> I should make redo this tommorw, and record it
02:22:03 <pineapple> (my 7 for 2 lights are: 12 13 15 16 19 25 26)
02:22:07 <fax> then I can time the porgramming time vs the pproof checking timem for all these different approaches
02:22:45 <pineapple> what language are you using to check them in?
02:24:17 <oerjan> fax: 4*4 _isn't_ all solvable
02:24:30 <oerjan> (says my determinant check)
02:24:30 <fax> im glad I'm not doing 4x4 :P
02:24:43 <fax> wait you use determinant for this lights out thing?
02:24:48 <oerjan> pineapple: determinant of the matrix is 0
02:25:09 <Sgeo> oerjan, thought someone said it was -7?
02:25:09 <oerjan> fax: you didn't see all the discussion above?
02:25:19 <oerjan> Sgeo: that was me, and for 3*3
02:25:40 <Sgeo> Oh, the 0 was for 4*4
02:25:45 <oerjan> 3*4 is -9, so also all solvable, but 4*4 is 0, so not
02:26:11 <Sgeo> I suppose it's better to randomize than to Simulate random clicks
02:26:29 <oerjan> Sgeo: that would depend on how hard you want to make it...
02:26:37 <fax> by the way
02:28:21 <fax> wow I don't understand that idea with the matrix at all
02:28:22 <pineapple> oerjan: ok. yeah... googling seems to confirm what you're saying...
02:28:35 <fax> what's M? (the rules of the game, but encoded how?)
02:28:44 <pineapple> random unsolvable 4x4 board: .XXX/...X/.XXX/....
02:28:55 <oerjan> [[1,1,0,1,0,0,0,0,0],[1,1,1,0,1,0,0,0,0],[0,1,1,0,0,1,0,0,0],[1,0,0,1,1,0,1,0,0],[0,1,0,1,1,1,0,1,0],[0,0,1,0,1,1,0,0,1],[0,0,0,1,0,0,1,1,0],[0,0,0,0,1,0,1,1,1],[0,0,0,0,0,1,0,1,1]] :: [[Integer]]
02:29:21 <oerjan> fax: that's the matrix for 3*3
02:29:41 <pineapple> oerjan: 2x3 should give you 0 as well
02:30:15 <oerjan> pineapple: yeah it does. interesting that those determinants are _exactly_ 0, and not just even.
02:30:23 <fax> oerjan, oh I have a data type like this but it's not a matrix
02:30:35 <fax> oh! I see what you do, that's really neat!
02:30:43 <fax> I should program this too
02:30:44 <pineapple> oerjan: do you get the significance of the number if it's non-zero?
02:30:44 <oerjan> fax: this is just a haskell list of lists, actually.
02:30:53 <fax> oerjan well I am thinking of it as a matrix
02:31:00 <oerjan> i had a determinant program from way before which used lists of lists
02:31:18 <fax> my computer is really REALLY struggling with a particular lights out configuration
02:31:18 <pineapple> also: if you can work out the determinant of a 3x3 in your head, i have the perfect game for you
02:31:47 * Sgeo has another puzzle that needs math analysis
02:31:49 <oerjan> pineapple: this is actually a 9*9 _matrix_ for the 3*3 game, so no :D
02:31:50 <Sgeo> Not today though
02:32:03 <pineapple> oerjan: a 3x3 matrix, not a 3x3 board
02:32:22 <oerjan> pineapple: ouch. well _maybe_ i could do it.
02:32:32 <oerjan> doesn't mean i feel like it...
02:32:47 <oerjan> i guess i'd want to use minors
02:32:53 <pineapple> http://www.boardgamegeek.com/thread/402843/rules-non-degenerate-or-not-quite-kramers-rule
02:33:29 <oerjan> minors of 3*3 are just cross products anyhow (also discussed above)
02:34:22 <Sgeo> Actually, instead of asking for math help, there's probably enough analysis stuff posted somewhere. I just need to know the name
02:34:33 <oerjan> minors of matrices, a tool for evaluating the determinant
02:34:47 <oerjan> although not very useful for big ones iirc
02:35:18 <Sgeo> There are two containers of water, a larger one [A], and a smaller one [B]. You can fill a container completely with water, transfer water from one to the other [the transfer stops when the repicient is full or the sender is empty], and drain a container
02:35:22 <pineapple> oerjan: if i get what you're saying... then yes, probably only useful for 3x3
02:35:32 <Sgeo> There's a red line on container A. the goal is to get the water level of A to match the line
02:36:28 <oerjan> pineapple: the determinant being even but non-zero doesn't have any significance for lights out, but you could maybe create a similar game based on addition with a different modulus than 2, where it would be.
02:36:31 <Sgeo> The practical problem I have is this: If I'm given the size of A and B, can I move the line and be able to make a puzzle such that a solution exists?
02:37:51 <pineapple> oerjan: did you click the link i gave?
02:38:22 <pineapple> oerjan: reason i asked about the significance of it is that... i think that 7 presses the is the max needed for 3x3 and 9 for 3x4
02:38:46 <pineapple> which (and i might be very wrong here) i think means that 5x5 will give -23
02:40:27 * Sgeo appends an "and if so, how"
02:40:59 <oerjan> Sgeo: well obviously you can put the red line in the place corresponding to the volume of B
02:41:08 <pineapple> Sgeo: assuming that the water supply is infinite, that A > B, that A > target, and that everything is integers?
02:41:44 * fax 52 cases left!!
02:42:34 <oerjan> pineapple: um no 3*3 can require 9 presses
02:42:57 <pineapple> (but don't bother with the latter half if A % B == 0)
02:43:52 <oerjan> pineapple: because all configurations can be solved, _every_ push subset of the 9 must be different. so if you push all 9, there is no way to get it back without pushing them all again.
02:44:17 <Sgeo> I'm still not sure whether everything is integers
02:44:31 <pineapple> Sgeo: if you assume it, it's a lot easier
02:44:34 <Sgeo> Actually, I don't think it's a safe assumption
02:44:36 <oerjan> Sgeo: golden ratio might be interesting :D
02:44:52 <Sgeo> Let me show you a picture
02:45:44 <Sgeo> http://i.imgur.com/3CenQ.jpg The only thing I can easily change is the red line
02:45:45 <pineapple> oerjan: ok... doesn't all 9 invert all 9?
02:45:50 <oerjan> pineapple: determinant for 5*5 is 0, actually. (so not all solvable)
02:46:24 <oerjan> it toggles a diagonal cross
02:47:06 <Sgeo> pineapple, it's supposed to be confidential, but I don't care. I'm under no contract.
02:47:30 <pineapple> Sgeo: if you're under NDA, be careful...
02:47:36 <oerjan> Sgeo: are the containers empty at the start?
02:47:59 <pineapple> hmm... i doubt that it's properly floats... might be large intergers, though
02:48:31 * Sgeo isn't even sure how to measure them precisely
02:48:49 <pineapple> Sgeo: are you willing to be unsceientific?
02:49:05 <Sgeo> If you mean with measuring, I think I have to be
02:49:11 <alise> pineapple: it's not NDA Sgeo just likes to spend time in projects where kids pretend they're professional
02:49:25 <alise> and "fire" people and make "design plans" and really they're just making some random stuff in virtual reality without pay
02:49:32 <pineapple> hold a ruler up to the screen, etc
02:50:07 <Sgeo> I think the only kid in this project is the other programmer
02:51:17 <fax> yay proof complete!!!
02:51:31 <fax> so yeah you really can get every configureation
02:52:43 <fax> http://pastie.org/878074
02:52:45 -!- jcp has joined.
02:52:49 <fax> most stupid way I could think of at the time
02:53:20 <Sgeo> So, I move the line to A-B?
02:54:24 <pineapple> if all numbers are integers, there's no guarantee that it's solvable for all line positions
02:55:14 <pineapple> if A and B aren't coprime, then the target has to be a multiple of hcf(A,B)
02:56:08 * Sgeo really needs a way to repay pineapple, oklopol, and oerjan. Thank you SO MUCH
02:56:35 <Sgeo> I feel like I'm taking and not giving
02:57:05 <Sgeo> fax, what language is that?
02:57:50 <fax> I just did this because it's ridiculous to do this
02:58:02 <fax> and I wanted to do a huge proof by computation
02:58:22 <fax> even though it was a contrived one
02:59:05 <Gregor> [In case anybody's interested, some game music I'm writing per request: http://codu.org/tmp/gm1wipp3.ogg ]
02:59:36 -!- augur has quit (Ping timeout: 265 seconds).
02:59:51 <oerjan> Sgeo: (0,0)(A,0)(0,B)(A-B,B)(A,B)(B,0)(A-B,0)(B,B) are the only configurations i can get without knowing more about the relative size of A and B
03:00:11 <Sgeo> What's the second number supposed to be?
03:00:24 -!- augur has joined.
03:00:25 <oerjan> (contents of A, contents of B)
03:00:44 <oerjan> with A and B being their max volume
03:02:29 <oerjan> the last two are the only ones that might give more options by doing a transfer
03:03:19 <oerjan> but what they give depend on whether they fill up or empty first
03:04:07 <oerjan> (0,A-B) or (A-2B,B) vs. (2B,0) or (A,2B-A)
03:04:45 <Sgeo> oerjan, I'm interested in the configuration of the ring. I think at win, the water level of B is irrelevant
03:05:02 <pineapple> Sgeo: tap to A; while(A isn't empty) {A to B; if (B is full) B to floor; else tap to A;}
03:05:32 <pineapple> will, if A and B are co-prime, eventually pass through all amounts possible in A
03:05:39 <oerjan> Sgeo: i need both to know what i can get _from_ there though
03:06:09 <pineapple> in fact, that will cycle through all possible values of B as well
03:06:16 <Sgeo> I don't have an easy way of measuring both atm
03:06:28 <Sgeo> Hold on, actually
03:06:34 <oerjan> pineapple: co-prime is irrelevant
03:06:55 <Sgeo> pineapple, when the puzzle is set up, I know how [inefficiently] to solve it
03:07:02 <oerjan> that's just factoring out the common factor
03:07:08 <pineapple> oerjan: only slightly... if they aren't, then there's less possible levels that can be hit
03:07:33 <pineapple> Sgeo: that;s also probably the most efficient way...
03:07:47 <oklopol> yeah but we can probably assume the sizes are reals or rationals
03:07:55 <oklopol> i have no idea what you're talking about
03:07:57 <pineapple> either that or backwards, which is filling B and pouring as much into A each time
03:07:58 <oerjan> pineapple: i suppose by "all amounts possible" you mean "all integer amounts between 0 and A"?
03:08:10 <Sgeo> When the original game was around, I just kept in mind to "preserve information"
03:08:46 <oklopol> what does it mean that a gameboard is divided into 11 segments
03:08:55 <Sgeo> I think A = (3/2) B
03:09:00 <pineapple> oerjan: yes... although if they're not integers, then eventually you will either hit all possible things or never end...
03:09:05 <oklopol> well i guess just that, and i should read the rest of the rules to find out moer
03:09:18 -!- augur_ has joined.
03:09:31 <pineapple> <oklopol> what does it mean that a gameboard is divided into 11 segments - ?
03:09:47 <Sgeo> Actually, I just thought of an exact way to measure it *facepalm*
03:09:48 <oerjan> pineapple: oh wait i think i see a clue there - you always tap _into_ A but _out of_ B
03:10:11 <pineapple> oerjan: essentially: yes... or the other way around
03:10:15 -!- augur has quit (Ping timeout: 265 seconds).
03:10:44 -!- augur_ has changed nick to augur.
03:10:52 <oerjan> the total amount is always between 0 and A+B
03:11:18 <Sgeo> I'm going to go collect the exact numbers
03:13:04 <oklopol> and who can't calculate a 3x3 matrix determinant, you have to be able to remember like 5 numbers
03:13:22 <oklopol> i mean i'm not saying i can do it fast enough to play the game
03:13:30 <oklopol> yeah that was a completely random number
03:13:49 <pineapple> once you have it for the opening position: you only need to look at the (broken) diagonals of the target cell
03:13:55 <oklopol> i'm too tired to even want to think about trying to find the correct number
03:14:55 <oerjan> so what it really does is x=A; while (x) {if (x>=b) x-=b; else x+=a;}
03:15:34 <pineapple> Sgeo: you pulled those numbers from the code?
03:16:06 <Sgeo> pineapple, I moved an object to the bottom and top of each cylinder, and measured its location
03:16:22 <pineapple> suggest you do an svn blame (or equivalent), then yell at whoever chose those numbers
03:16:39 <Sgeo> 6/4 = 3/2, right?
03:16:42 <Sgeo> And is 3/2 bad?
03:17:09 <pineapple> but they've tried to implement something that they don't fully understand
03:17:41 <pineapple> by making a puzzle that has high marmite factor between trivial and frustrating
03:17:42 <Sgeo> I didn't understand it enough to be able to give instructions
03:18:50 <oerjan> `define marmite factor
03:19:07 <Sgeo> I take it it's difficult to solve?
03:19:17 <oerjan> i don't watch tv, _and_ i'm norwegian
03:19:21 <pineapple> "marmite - you either love it or you hate it" - there's nothing in between
03:20:07 <oerjan> i do have a vague understanding of what marmite is, though
03:20:15 <Sgeo> So to some it's difficult, some it's annoyingly easy?
03:20:24 <pineapple> Sgeo: i mean that it's either very trivial or very frustrating... and if the player can't work out that they should aim for A-B to make it trivial, then they will be very frustrated by it
03:20:49 <Sgeo> Why don't I program it and see if it frustrates me
03:21:49 <Sgeo> Getting the person who created this to change it is probably ah.. somewhat difficult
03:22:11 -!- alise has quit.
03:22:34 <pineapple> Sgeo: then ask them a direct question: "what are you trying to acheive by including this puzzle? what is the point that you're trying to make?"
03:22:36 * oerjan now understands why that algorithm cycles through all possible amounts
03:22:55 -!- Oranjer has left (?).
03:23:05 <Sgeo> pineapple, the puzzle is there because it was in the original game, but getting the numbers from the original is nigh-impossible now
03:23:22 <Sgeo> THe numbers are what they are because no one had a clear understanding of what they should be
03:23:45 <Sgeo> http://wiki.activeworlds.com/index.php?title=Mutation
03:25:01 <pineapple> have you tried googling for spoilers, then calculating the numbers from that?
03:25:11 <Sgeo> Original equiv puzzle: http://wiki.activeworlds.com/index.php?title=Image:Blue_crystal.PNG
03:26:06 <Sgeo> Let me implement this, and if it really is that bad, I can convince someone to change the numbers
03:26:24 <pineapple> Sgeo: i take it that no-one else have even considered to measure them?
03:26:47 <Sgeo> We wouldn't know how, I thinkl
03:27:13 <Sgeo> I mean, besides measuring pixels in a screenshot
03:27:28 <oerjan> Sgeo: you could use pineapple's algorithm
03:27:53 <oerjan> basically see how long it takes until you cycle to all 0
03:27:58 <Sgeo> I thought pineapple was giving a solution for the puzzle, not how to generate.. OH
03:28:30 <oerjan> i am pretty sure you can deduce the ratio of A to B from the progression
03:28:48 <Sgeo> The original isn't playable anymore
03:28:50 <Sgeo> Although we can visit
03:28:51 <pineapple> the other way is measure with pixels and see what numbers you get
03:28:53 <oerjan> assuming you manage to avoid hitting the red line
03:29:30 <Sgeo> Where did pineapple put his algorithm
03:30:01 <oerjan> <pineapple> Sgeo: tap to A; while(A isn't empty) {A to B; if (B is full) B to floor; else tap to A;}
03:30:32 <oerjan> that causes the total amount to be changed by -B (mod A) at each step
03:30:34 <Sgeo> What does tap mean? go to top?
03:30:49 <pineapple> tap to A means fill A from the tap
03:31:02 * Sgeo does this by hand
03:31:53 <oerjan> you count how many times you fill A, and how many times you empty B, until you cycle. then the ratio of times = ratio of volumes
03:32:22 <Sgeo> I think I just hit an infini.. um
03:32:31 <Sgeo> So this isn't how to determine how easy it is?
03:32:43 <Sgeo> I think I hit the solution a bit too soon
03:32:50 <oerjan> it's how to determine all relevant information
03:33:07 <pineapple> (relevent for getting the if statement handled correctly)
03:33:10 <Sgeo> For 6:4, tapping A, A->B is done
03:33:51 <Sgeo> The only positions A reaches are 0, 2, and 6
03:34:03 <Sgeo> Unless I'm doing something wrong
03:34:10 <oerjan> Sgeo: if you _know_ it's 6:4 you don't need to measure do you
03:34:34 <Sgeo> oerjan, those are the measurements for the NEW stuff. I still don't know what the original was, but I think it was tougher than this
03:34:56 <pineapple> Sgeo: i'm almost certain it is, based on the screenshot
03:35:19 <Sgeo> A can never reach anything other than 0, 2, and 6?
03:35:24 <oerjan> Sgeo: pineapple's algorithm shows that you can choose _any_ integer volumes you want
03:35:42 <oerjan> Sgeo: it should be able to reach 4
03:36:09 <Sgeo> Um, that's even easier
03:36:59 <oerjan> Sgeo: the spots you can hit are the multiples of the greatest common factor of 6 and 4 (i.e. 2)
03:37:18 -!- fax has quit (Quit: Lost terminal).
03:37:24 <pineapple> Sgeo: nearest (smallest) interger solution for the original image, based om measurements: A=25, B=13, t=4
03:37:57 <Sgeo> Hm, remember, the camera was kind of at an angle
03:39:36 <oerjan> if it were A=24, B=12 then things would be a bit awkward :D
03:39:40 -!- songhead95 has joined.
03:40:17 <Sgeo> Maybe a more straight-on picture would be appreciated?
03:40:41 <pineapple> in the original... did the red line move? i'm assuming not
03:41:04 <Sgeo> As far as I remember
03:41:12 <songhead95> is there a Brainfuck interpreter that just takes input from stdin, and can be used as a shell interpreter eg.
03:41:59 <Sgeo> Should I try to make it so that the bottom edge of each cylinder is head-on?
03:42:03 <oerjan> songhead95: almost any interpreter should be able to do that, since all those #! characters are comment characters in BF
03:42:07 <pikhq> songhead95: Several.
03:42:28 <pikhq> Might I suggest Egobfi?
03:44:31 <Sgeo> http://i.imgur.com/Sn4ZE.png
03:46:15 <pikhq> Sgeo: AW looks positively... 90s.
03:47:16 <pineapple> B 157, A 283, t 93-96 (likely somewhere in the middle)
03:48:39 <Sgeo> Probably better to use 9/5 than the exact original measurements
03:49:15 <Sgeo> So what? Will it be playable?
03:49:59 <oerjan> Sgeo: all integers are playable, in principle ;D
03:50:07 <Sgeo> Will it not be too trivial?
03:50:55 <Sgeo> As long as it's not as trivial as 3/2 was
03:51:43 <pineapple> when B is emptued for the 3rd time, A has 3 in it
03:52:07 <pineapple> that's not trivial... and probably not that frustrating
03:52:20 <Sgeo> pineapple, how can I repay you?
04:09:49 -!- Asztal has quit (Ping timeout: 264 seconds).
04:26:06 -!- jcp has quit (Quit: I will do anything (almost) for a new router.).
05:15:10 -!- augur has quit (Ping timeout: 256 seconds).
05:49:08 -!- augur has joined.
05:56:56 <Sgeo> So much for hoping that my code would be perfect first time
06:27:08 -!- deschutron has left (?).
06:30:58 -!- coppro has joined.
07:21:30 -!- oerjan has quit (Quit: leaving).
07:58:18 -!- Sgeo has quit (Ping timeout: 265 seconds).
07:59:59 -!- clog has quit (ended).
08:00:00 -!- clog has joined.
08:29:56 -!- coppro has quit (Quit: upgrade time).
08:53:53 -!- coppro has joined.
09:00:18 -!- coppro has quit (Quit: I am leaving. You are about to explode.).
09:33:04 -!- kar8nga has joined.
09:33:45 -!- kev_ has joined.
09:34:14 -!- kev_ has quit (Client Quit).
09:36:11 -!- pikhq has quit (Read error: Connection reset by peer).
09:37:30 -!- FireFly has joined.
09:42:48 -!- pikhq has joined.
10:06:24 -!- tombom has joined.
10:24:23 -!- nooga has joined.
10:37:05 <nooga> i just caused panic
10:42:13 -!- BeholdMyGlory has joined.
11:11:13 -!- nooga has quit (Ping timeout: 240 seconds).
11:15:40 -!- MigoMipo has joined.
11:25:05 -!- kar8nga has quit (Read error: Connection reset by peer).
11:36:29 -!- nooga has joined.
11:45:10 -!- alise has joined.
11:45:20 <alise> Maximal antipotential.
11:45:37 <alise> 07:18:59 <ais523> wow, the Poincaré conjecture has been proved
11:46:12 <alise> the guy who solved it is awesome he denied a prize for it because he didn't think the board were qualified to assess his work
11:46:41 <alise> "According to a 2006 interview, Perelman is currently jobless, living with his mother in Saint Petersburg."
11:46:47 <alise> guess he really doesn't like money
11:49:55 <alise> ais523: to be less obtuse, the Poincare conjecture was proved 2002-2003
11:50:54 <fizzie> Yes, but the actual millennium prize about it seems to have been awarded to him two days ago, making this a bit topical. One has to wonder whether they bothered to ask him if he wants it, though.
11:52:17 <alise> On 18 March, 2010, Perelman was awarded a Millennium Prize for solving the problem.[14] He had previously stated that "I'm not going to decide whether to accept the prize until it is offered."[3]
11:52:21 <alise> So: I think he did accept.
11:53:04 <alise> http://www.claymath.org/poincare/index.html
11:53:12 <alise> they misromanised his name :)))
11:53:51 <fizzie> I don't know; New Scientists says "A million-dollar prize for solving one of toughest problems in mathematics has been awarded to a Russian mathematician, but the real puzzle is whether he'll accept it."
11:54:04 <fizzie> "The president of CMI, James Carlson, is waiting to see if Perelman will do the same for the Millennium prize. "It may be a while before he makes his decision," he says."
11:54:29 <Deewiant> alise: There are different romanizations, and that, AFAIK, is valid.
11:54:29 <alise> I imagine he will probably decline; why Millennium but not Fields?
11:54:43 <alise> Deewiant: Yeah, I know :P
11:54:54 <alise> Grigori is a nicer romanisation though
11:55:01 <fizzie> Though, billions and billions of dollars!
11:55:14 <fizzie> Maybe his mother goes all "you'll take that money or I'll kick you out".
11:55:17 <Deewiant> I guess the -iy is closer to the actual pronunciation
11:55:40 <Deewiant> Although I guess nobody English will pronounce it any differently whether it's -i, -y, or -iy
11:55:59 <alise> Billions and billions: 1 million
11:56:30 <fizzie> Well, those were small billions.
11:56:38 <alise> I'm pretty sure anyone who declines the Fields medal is one fucking morally certain man
11:57:05 <alise> Heh, the Fields medal only awards $15,000USD as of 2006
11:58:13 <alise> 19:46:15 <pikhq> Sgeo: AW looks positively... 90s.
11:58:13 <alise> that's why he likes it
11:58:31 <alise> WIND OF FURY! POWER OF BLOOD! HEALING! LIGHT! BY YOUR POWERS COMBINED, I AM---
11:58:34 <alise> (http://i.imgur.com/Sn4ZE.png)
11:58:39 <alise> ooh, I forgot MAGIC SHIELD!
12:00:16 <fizzie> The one that ends up with -i sounds a bit non-information-preserving; I don't know how that domanization would differentiate between Григорий and Григори; google seems to suggest that some people use the latter as a name too.
12:00:36 <oklopol> even if i had no use for a million, i'd take it just so others don't get it
12:01:04 <alise> I might decline some prestigous prize because I'll be more famous if I do that :)
12:01:11 <oklopol> but i would totally have a use for a million, i've always wanted to give some homeless guy 100000
12:01:34 <fizzie> oklopol: Then he'll spend it all on booze and die, you man-slaughtererer.
12:01:55 <alise> Quite frankly I would enjoy money.
12:02:12 <oklopol> i would probably choose one whose brain isn't completely melted yet
12:02:29 <oklopol> oh well i would probably buy a house too
12:03:08 <oklopol> and probably give half of the rest to people i know and half in a bank of smth
12:03:10 <fizzie> My wife asked me what I'd do with 50 million euros (she'd buy some 14-million manor somewhere, I forget just where); the first thing I could think of was "hmm, maybe I'll buy dessert with lunch at work". (That costs 0.95 eur extra.)
12:04:46 <alise> i'd prolly just hire a buncha expensive people to manage it for me and turn it into more money (they can have some so they don't run away)
12:04:53 <alise> and then I could gain money without bound, and thus I could completely ignore money as it is, over time, infinite
12:05:03 <alise> take that, capitalism
12:05:41 <fizzie> Everything's so expensive nowadays since I no longer get any student discounts; apparently graduate students aren't quite as good as real students. So the lunch is now 5.40 eur as opposed to 2.55 or so.
12:06:47 <alise> i'd also get loads of people to build my perfect house, buying one is so boring
12:06:48 <oklopol> you don't work at uni? i mean if you get a salary, 5,40 is nothing
12:07:08 <alise> i want like... i don't know, cool technology. in my walls
12:07:51 <fizzie> oklopol: It's the principle of it! Besides, the change in lunch price pretty much ate the wage-raise I got by graduating. (It bumps the "difficulty level" pay-scale column index by one automatically.)
12:08:11 <fizzie> (And the change in bus ticket price did the rest.)
12:14:54 <alise> even though I dislike geometric proofs
12:14:58 <alise> Elements is so beautiful
12:15:02 <alise> the first constructivist work, I wonder?
12:15:30 <alise> also using geometry as the foundation of all mathematics amuses me...
12:17:17 <alise> i mean his geometry basically embeds the real numbers...
12:19:06 <nooga> i'm going to scotland!
12:21:39 <oklopol> can't you do geometry on rationals?
12:23:24 <oklopol> i haven't actually seen an axiomatization of geometry, but i hear there were some really simple things that hadn't been realized to not be derivable from the axioms but were used as if they were, as late as late 1900's
12:23:40 <oklopol> because it's such a hard thing to axiomatize, given we have such strong intuitions about it
12:23:52 <oklopol> something like points exist between two points
12:25:35 <oklopol> we have a geometry course at uni, but apparently it skips some of the boring details
12:27:07 <oklopol> probably have to be pretty boring, because the lecturer said they were, and he was all hyper over cyclic modules "and we get this particularly fascinating fellow" he loves to personify things "if we just have one generator"
12:28:47 <fizzie> The Matrix Computations lecturer refers to matrices and vectors as people too, usually with the word "guy"; "and this guy here ... and we get this guy ..." and so on.
12:30:58 <fizzie> He also keeps laughing all the time, without any explicit jokes.
12:31:09 <oklopol> if there's a sum where i goes from 1 to n, the same lecturer often says "ja i kipittää 1:stä n:ään"
12:31:13 <oklopol> which i always find hilarious
12:31:44 <oklopol> where the funny thing is kipittää is a funny word
12:31:58 <fizzie> Some of my friends collected the best sayings of maths lecturers in notebooks; unfortunately I don't have any handy.
12:32:44 <fizzie> "These matrices can be... really big *ehehe*." It's very amusing to listen, though.
12:34:59 <fizzie> The course seems to currently be in a transition to the interesting part; the part where we no longer have a matrix A as a pile of numbers, but instead just a linear operator A that you can apply to a vector, because the matrix itself would be too large to store in memory. Now it's going to be all Krylov subspaces and whatnot.
12:35:35 <oklopol> please define them in guy terms
12:35:57 <oklopol> how many courses are you on usually?
12:36:21 <fizzie> K_r(A, b) = span(b, Ab, A^2b, ..., A^(r-1)b), nothing more complicated than that.
12:36:51 <fizzie> I seem to have around 4-5 now. It's only something like 60 course credits for the licensiate/doctoral degree, after all.
12:37:18 <oklopol> so this A dude here makes all sortsa copies of itself and then all those copies have buttsex with b at the same time and a vector space is spanned
12:37:47 <fizzie> Yes. Except you have to worry about the numerical stability of the buttsex.
12:40:03 <oklopol> 4-5 is considered a lot among turkuans
12:40:28 <oklopol> maybe we are a crappier uni
12:41:03 <fizzie> I don't think it's considered "a lot" here, but it's not an especially tiny amount either, I Guess.
12:41:19 -!- tombom has quit (Quit: Leaving).
12:41:25 <oklopol> actually one of the professors told me people in turku are better at math usually, which he'd probably be regretting if he knew i was gonna tell it to everyone
12:41:58 <fizzie> Back at the beginning of the course, when he was trying to motivate the course by talking about big matrices, he was all about "the Google matrix", which is a NxN matrix where N is the size of the Internet.
12:42:23 <fizzie> I guess this is somehow related to the fact that you get PageRank values as eigenvalues of some sort of adjacency matrix of the Internet.
12:42:40 <oklopol> or the universe matrix containing for each point the points at most one meter from it?!?
12:43:06 <fizzie> There might've been actually some physics problem, though maybe not quite like that.
12:43:16 <oklopol> unless you can give out search results by multiplying with the matrix, then it would be slightly more interesting
12:43:51 <fizzie> Same here, actually; boo-ya.
12:50:13 -!- oklopol has quit (Ping timeout: 276 seconds).
12:52:05 <AnMaster> <oklopol> turns out linear functions are invertible (they have normal function inverses) iff their determinant is nonzero <-- makes perfect sense considering that is true for matrices.
12:53:00 <AnMaster> <Sgeo> I suppose none of this is related to Computer Science? Maybe I should stick with this college and Minor in math <-- well, matrices at least are used a lot in programming. Especially 3D iirc.
12:54:22 <AnMaster> alise, however programming is a part of CS
12:55:23 <alise> programming isn't even applied CS
12:55:44 <alise> programming, aka software engineering, is an enirely separate field that happens to use some ideas from CS
12:55:50 <alise> just like physics uses mathematics...
12:57:01 <AnMaster> alise, however, I'm pretty sure (basic) programming is taught as part of CS courses. At least for all universities I checked.
12:57:15 <AnMaster> alise, which is what I was talking about
12:58:00 <alise> If a CS course involves Java, C, Python - it's probably crap.
12:58:14 <alise> Well, Python can go okay, but only if it's used in an abstract way.
12:58:16 <AnMaster> alise, I think C and lisp were the most common ones
12:58:34 <alise> (Almost all (mathematical term!) CS courses suck.)
12:58:52 <alise> In fact I'm not sure I'd call any existing CS curriculum good.
12:58:59 <alise> MIT sorta ruined theirs by abandoning SICP and doing robots in Python instead.
12:59:47 <alise> The xkcd effect, may I call it.
13:00:09 <alise> "Default search engine has been changed to Yahoo!" --Ubuntu.com
13:00:37 <alise> AnMaster: xkcd glorifies "fun hacking!" and "zomg cool robots!" and "python is SO EASY!"
13:00:48 <alise> "This beta sports full removal of HAL from the boot process, making Ubuntu faster to boot and faster to resume from suspend."
13:00:48 <alise> Well, that's good.
13:00:53 <AnMaster> alise, well sure, python *is* easy
13:00:58 <alise> "We now feature built-in integration with Twitter, identi.ca, Facebook, and other social networks with the MeMenu in the panel, which is built upon the Gwibber project, which has a completely new, more reliable backend built on top of desktopcouch. Gwibber now also supports a multi-column view for monitoring multiple feeds simultaneously."
13:01:12 <alise> "Millions of songs are available for purchase from your Ubuntu desktop, integrated with the Rhythmbox Music Player and using Ubuntu One cloud storage for backup and easy sync. Watch http://one.ubuntu.com/blog for the public beta launch."
13:01:22 <alise> Otherwise a humdrum improvement release.
13:01:37 <alise> But seriously: Yahoo, social crap by default, integrated music purchasing?
13:01:42 <AnMaster> alise, I think jaunty might have been the last "good" release
13:01:53 <alise> I didn't mind 9.10.
13:02:07 <alise> Karmic's the latest release. :P
13:02:16 <AnMaster> alise, well this new one sounds horrible
13:02:29 <alise> I only quoted the horrid bits. Obviously.
13:02:32 <alise> "Paul also noted that the most controversial aspect of the new design amongst users has been the placement of the window control buttons on the left instead of the right side of the windows"
13:02:36 <alise> Copying OS X, are we?
13:02:59 <AnMaster> I don't use standard theme anyway
13:03:16 <alise> Y'know what? I think I'll just stick with Windows 7 for now.
13:04:08 <AnMaster> alise, arch linux isn't too bad
13:04:59 <AnMaster> alise, on the plus sides it doesn't integrate music stores, nor social crap by default, and default search engine is whatever <your browser> uses as upstream default
13:05:20 <alise> yeah but on a laptop?
13:05:48 <alise> clearly I should just instantly code ehirdOS
13:06:05 <AnMaster> alise, ACPI is horrible I'm told
13:06:12 <AnMaster> and you really need that for laptops :(
13:06:38 * alise decides to name his first proof system something along the lines of provenance
13:07:07 <alise> it'll have two components, the proof checker (basically a typechecker for some dependently-typed total lambda calculus) and the proof compiler (from a form you'd actually want to write; with niceties such as definitions)
13:07:13 <alise> so they need names
13:07:31 <alise> and also perhaps a third component, that extracts computational (non-proof) content from a proof and compiles that to some functional language
13:07:48 <alise> I guess the proof checker should be prove, and the compiler nance, if I'm going by provenance
13:07:51 <alise> AnMaster: That's way boring.
13:08:12 <alise> Maybe I should have:
13:08:32 <alise> volit -- program extractor
13:08:40 <alise> The system as a whole being Provenance and Volition.
13:08:54 <alise> Because computation is like some sort of volition.
13:09:00 <alise> You're going forwards to do some sort of goal. Of such.
13:09:11 <alise> The problem is that prove is a bit of a vague name for a proof checker.
13:09:22 <AnMaster> google result is Volition® as the third
13:09:54 <alise> It's a bloody English word
13:09:58 <alise> You can't trademark it
13:10:05 <AnMaster> alise, well it seems to have been done :/
13:10:05 <alise> Only in some very specific field
13:10:13 <alise> You fail at trademark law :P
13:10:46 <alise> I should clearly write PROVE first.
13:10:50 <alise> In, eh, let's say Haskell.
13:11:06 <alise> What calculus? Perhaps the calculus of inductive constructions.
13:11:25 <AnMaster> alise, why not in coq or agda?
13:12:22 <alise> Because I don't really know enough of Coq or Agda to do those. If I was doing it so I could prove the checker correct, then Agda would be the wrong choice; it's a very experimental, exporatory language and false has been proven in it many many times.
13:12:22 <alise> Coq I know even less than Agda.
13:12:40 <alise> Besides, volit will probably spew out (horrific) Haskell.
13:12:57 <alise> It annoys me that prove has to know about sets, and not just propositions.
13:13:36 <AnMaster> alise, what exactly will volit do?
13:14:41 <alise> Well, nance is in many ways like a programming language. You have data types, in Type, and you have a subset of Type named Prop which contains propositional statements.
13:14:55 <alise> You prove a Prop by writing (terminating) code that constructs a value of the given Prop.
13:15:12 <alise> The values of Props are irrelevant - they are indistinguishable; for any x,y:P where P:Prop, x=y
13:15:17 <alise> but the values of Sets are not
13:15:25 <AnMaster> alise, sounds like you are an constructivist ;O
13:15:46 <alise> Through the Curry-Howard lens, we can eliminate proofs (Prop values), as they carry exactly 0 bits of information.
13:16:04 <alise> We have lambdas, as ways of proving implication and also defining functions on sets.
13:16:08 <alise> So... we have a total programming language.
13:16:30 <alise> Sprinkle on some mechanism for IO, and you have both a programming language with dependent types and consequently proving, and a proof assistant.
13:17:02 <alise> If you're doing proofs, you use nance and it feeds its result to prove for you; if you're programming, you use nance and it feeds its result to volit (and then, presumably, to ghc) for you.
13:17:15 <alise> Often the files you do both to will be the same.
13:17:31 <AnMaster> why not allow non-constructive proofs btw?
13:17:31 <alise> AnMaster: Well, the typechecker just says "Yes" or "No" in so many words.
13:17:46 <alise> Well, because I don't believe that forall p, p \/ ~p, for one.
13:17:53 <alise> Two, you can have that
13:18:02 <alise> classicalOr p q = ~(~p & ~q)
13:18:20 <alise> Or you can even just take as a parameter the law of the excluded middle, thus having LEM -> whatever.
13:18:24 <alise> Constructivism contains classical logic
13:19:08 <alise> But it's simple as that I'm a constructivist, and I also believe in the computationalness of proofs and the like - total Curry-Howard disciple - so, begone LEM.
13:19:16 <AnMaster> why don't you believe forall p, p \/ ~p ?
13:19:30 <alise> That's law of the excluded middle.
13:19:42 <alise> AnMaster: Consider axioms like the Continuum Hypothesis (in the context of ZFC).
13:20:01 <alise> You can add the axiom CH to ZFC, and yield an (almost certainly) consistent system (if ZFC is consistent that is).
13:20:05 <alise> You don't need to.
13:20:07 <alise> It's just an example.
13:20:08 <alise> You can also add the axiom ~CH to ZFC.
13:20:18 <alise> So in plain ZFC without any frills: is CH true or false?
13:20:23 <alise> The answer is that it's neither.
13:20:34 <alise> AnMaster: also true for large ordinal axioms
13:20:44 <alise> AnMaster: Not undecidable.
13:20:57 <alise> Consider Godel's theorem.
13:21:05 <alise> It's not quite the same.
13:21:28 <AnMaster> hm okay, I think I see what you mean
13:21:48 <AnMaster> though I'm the first to admit that this is way out of my expertise.
13:22:14 <alise> AnMaster: It's simple enough: There are statements for which our formalisms do not have the mechanisms that we can apply to derive either a proof of p, or a proof of not-p.
13:22:25 <alise> Given that, where does the law of the excluded middle stand?
13:22:43 <alise> Either p or not p -- but it cannot be shown to be either. My opinion - shared with other constructivists - is that it is neither.
13:22:51 <AnMaster> alise, but non-constructive proofs are sexy :P
13:23:13 <alise> I think proofs of ~~p are not very interesting. :P
13:23:24 <alise> AnMaster: Mind you, I do believe that ~~p is very strong evidence for p.
13:23:35 <alise> I just don't believe it entails it.
13:23:44 <AnMaster> in a two-valued boolean logic at least
13:23:56 <alise> Yeah, well, propositions aren't booleans.
13:24:18 <alise> Whoever first made (x = y), (x > y) etc. booleans was a vile person.
13:24:20 <AnMaster> computers however *work* on boolean logic basically.
13:24:30 <alise> No, they work on electricity.
13:24:41 <AnMaster> alise, well sure, but at one level they do what I said mostly
13:25:24 <AnMaster> for the digital logic parts of them, which makes up a rather large and crucial portion of how they work
13:26:10 <alise> Coming up with a model for inductive types is Hard.
13:26:10 <AnMaster> of course there are analogue computers, but from what I understood they are kind of rare
13:26:22 <alise> Incidentally, nance will be where the type inferrence is.
13:26:37 <alise> prove will literally require an annotation for every single parameter and result.
13:26:41 <AnMaster> alise, I suspect the output it generates then might be rather large.
13:26:49 <alise> And no variable names or anything: It takes in lambda calculus with De Bruijn indexes.
13:26:53 <alise> (Plus type annotations).
13:27:28 <alise> I mean, GHC basically stops one step short of lambda-calculus.
13:27:34 <AnMaster> well, I can't really predict how much it will grow compared to input
13:27:56 <alise> Not that much, really. You can't infer anything dependent anyway.
13:28:00 <alise> Well, almost anything.
13:28:09 <alise> So only trivial things will have their types inferred.
13:28:32 <AnMaster> and well, I presume you somehow at the end can get out reasonable machine code, reasonable for an OS that is (which was your goal wasn't it?)
13:28:59 <alise> Oh, this is just my first foray into actually making one of these.
13:29:08 <alise> Nowhere near OS stage yet.
13:29:24 <AnMaster> alise, out of interest: how will you handle the low level interaction with the architecture in your OS? Some parts must be OS specific, be it configuring memory mappings or whatever.
13:29:36 <AnMaster> s/OS specific/hardware specific/
13:29:41 <alise> The machine code generated will probably not be pretty; after all, 42 will be represented by 42 nested constructors and then a unit value.
13:30:04 <AnMaster> alise, pipe it into llvm or something and hope for the best?
13:30:13 <alise> GHC produces alright code anyway.
13:31:13 <AnMaster> alise, still, I find the problem of proving the bits that deal with poking hardware correct quite interesting. Such as setting up memory mappings for processes and dealing with DMA or whatever.
13:31:19 <alise> AnMaster: Also, they don't need to be proved.
13:31:26 <alise> After all, the correctness of the code depends on the hardware being correct in the first place.
13:31:40 <AnMaster> I was just about to say that that might be an issue as well
13:31:55 <alise> Well, I don't think FDIV ever happened again.
13:32:00 <alise> They formally verify chips nowadays.
13:32:10 <AnMaster> iirc intel and amd both use correctness checkers for their CPUs nowdays, at least for the FPU. No one wants to see another FDIV bug
13:32:20 <AnMaster> alise, damn you beat me to it :P
13:32:27 <alise> I love how induction <=> recursion.
13:32:56 <AnMaster> alise, I knew they were related, but are they actually equivalent?
13:33:32 <AnMaster> I can't see how to get from one to the other exactly, but yeah they are pretty similar when you think about it
13:33:34 <alise> nat-induct : forall (P : Nat -> Prop), P 0 -> (forall (n:Nat), P n -> P (succ n)) -> forall (n:Nat), P n
13:33:43 <alise> now ignore Prop being propositions so irrelevant values just imagine it's any type
13:33:50 <alise> then consider P x = Integer
13:33:55 <alise> AnMaster: forall naturals n
13:34:22 <alise> integer -> (forall (n:Nat), integer -> integer) -> forall (n:Nat), integer
13:34:24 <alise> forall is the same as a function arrow
13:34:38 <alise> integer -> (Nat -> integer -> intgeer) -> (Nat -> integer)
13:34:39 <alise> so the first argument is the base case
13:34:51 <alise> the second gets the current value to consider, and also the rest of the computation (lazily)
13:34:55 <alise> and it combines the two with recursion
13:35:17 <alise> in fact you can derive a function like this for /any/ inductive data type, mechanically
13:35:44 <AnMaster> alise, btw do you reject proofs of existence by contradiction (that is, proving something must exist, because otherwise it would result in a contradiction, without giving any way to construct said thing)
13:35:44 <alise> epigram 2 does this
13:35:45 -!- kar8nga has joined.
13:36:24 <alise> AnMaster: Something must exist, otherwise contradiction = Not something must exist, implies contradiction = Not not something must exist = Not not P = ~~P
13:36:27 <alise> So that's using ~~P to prove P. No. I do not accept that.
13:37:00 <nooga> building plan9port
13:37:13 <AnMaster> alise, I think that means you end up rejecting some major parts of modern mathematics.
13:37:30 <AnMaster> but I'm pretty sure I read about that somewhere
13:37:41 <alise> you reject uncomputable real numbers, but nobody cares about them
13:37:50 <alise> AnMaster: consider that the four-colour theorem was proved with Coq
13:37:53 <alise> a constructivist system
13:37:59 <alise> it's very much practical
13:38:15 <AnMaster> http://en.wikipedia.org/wiki/Existence_theorem mentions "Such pure existence results are in any case ubiquitous in contemporary mathematics. For example, for a linear problem the set of solutions will be a vector space, and some a priori calculation of its dimension may be possible. In any case where the dimension is probably at least 1, an existence assertion has been made (that a non-zero solution
13:38:15 <AnMaster> exists.)". I don't have any clue what that means though really
13:38:39 <alise> Incidentally, interesting thing:
13:38:45 <alise> This is Pierce's law.
13:39:00 <alise> It is the type of call-with-current-continuation.
13:39:20 <alise> The continuation is (P->Q), i.e. gimme something and I'll give you anything (it's just a dummy value computationally so you can put it anywhere)
13:39:35 <alise> and you result in a P (because whatever you pass to the continuation must be able to stand for what would normally result, typewise)
13:39:36 <alise> and it gives you a P, by constructing a continuation
13:39:47 <alise> This doesn't hold in intuitionistic logic (and other similar constructivist ones)
13:39:52 <AnMaster> call/cc is always somewhat mind bending.
13:39:52 <alise> because it implies the law of the excluded middle
13:39:58 <alise> first, know that _|_ is the type with no elements, i.e. falsity
13:40:00 <AnMaster> alise, so no call/cc in your language?
13:40:03 <alise> and that ~p is p -> _|_
13:41:02 <alise> "In particular, when Q is taken to be a false formula, the law says that if P must be true whenever it implies the false, then P is true. In this way Peirce's law implies the law of excluded middle."
13:41:11 <alise> we can prove anything
13:41:15 <alise> so if P is true whenever it implies the false
13:41:27 <alise> that means that P is true
13:41:29 <alise> because P implies false
13:41:32 <alise> and from false we can derive P
13:41:46 <alise> ergo, law of the excluded middle
13:41:58 <alise> so call/cc -> law of the excluded middle :D
13:42:06 <alise> AnMaster: no call/cc outside of something like a continuation monad
13:42:09 <alise> no biggie - haskell doesn't have it either
13:42:49 <alise> AnMaster: you know the y combinator? as in a fixed point combinator doesn't matter which one
13:42:51 <alise> fix : (a -> a) -> a
13:42:56 <alise> so fix (1:) = [1,1,1,1,1,1,...]
13:43:03 <alise> i.e. fix f = f (fix f)
13:43:46 <alise> AnMaster: oh please tell me you know that
13:44:20 <AnMaster> it is familiar, but never really used lambda calculus.
13:44:25 <alise> it's in haskell too
13:44:26 <alise> fix (1:) = 1 : fix (1:) = 1 : 1 : fix (1:) = ...
13:44:46 <alise> fact = fix (\me n -> if n == 0 then 1 else me (n-1))
13:45:05 <alise> fact = (\me n -> if n == 0 then 1 else me (n-1)) (fix (\me n -> if n == 0 then 1 else me (n-1)))
13:45:05 <AnMaster> ah a quick check on wikipedia reminded me of what it was
13:45:14 <alise> fact = (\me n -> if n == 0 then 1 else me (n-1)) ((\me n -> if n == 0 then 1 else me (n-1)) (fix (\me n -> if n == 0 then 1 else me (n-1))))
13:45:18 <alise> thus allowing recursion
13:45:25 <alise> fix : forall a, (a -> a) -> a
13:45:27 <alise> consider it logically
13:45:31 <alise> (a -> a) is a tautology
13:45:45 <alise> and indeed using fix we can derive ANYTHING
13:45:47 <AnMaster> alise, (a implies a) implies a? for all a?
13:45:51 <alise> fix id : forall a, a
13:46:02 <alise> so for all p, p is true, not p is true, ...
13:46:07 <alise> fix is inconsistency in a bag!
13:46:16 <alise> ...and this, kids, is why you don't allow general recursion
13:46:33 <AnMaster> id : a -> a <-- that seems sane to me though. id is a no-operation after all
13:46:53 <alise> a implies a for all a
13:47:03 <alise> but (a -> a) -> a is not true
13:47:07 <alise> obviously a implies itself
13:47:13 <alise> if 2 is prime, then 2 is prime
13:47:18 <alise> if 2 is not prime, then 2 is not prime
13:47:32 <alise> so in fix : (a -> a) -> a
13:47:36 <AnMaster> alise, but considering the truth table for -> something seems wrong if id: a->a
13:47:37 <alise> we can ignore (a -> a) as it's already proved
13:47:40 <alise> so fix : forall a, a
13:47:51 <alise> -> doesn't have a truth table
13:47:57 <alise> but even classically A -> A holds...
13:48:04 <AnMaster> alise, not the classical logic ->?
13:48:19 <alise> classical -> has a truth table
13:48:24 <alise> but A -> A is still always true
13:48:30 <alise> it reduces to !(A&!A)
13:48:37 <alise> which is the law of non-contradiction
13:48:42 <AnMaster> but a -> b, says basically nothing about b if a is false
13:48:47 <alise> foo : somethingtrue -> a
13:48:55 <alise> proof: foo theproofofsomethingtrue
13:48:58 <alise> fix is equivalent to
13:49:12 <alise> and you get a proof of false
13:49:53 <alise> plug in reimann-hypothesis for a, and you get a proof of that too
13:49:59 <alise> plug in ~reimann-hypothesis, and its negation appears!
13:50:07 <alise> so many THINGS we can achieve with trivialism!
13:51:39 <alise> file extension .na is free. not any more!
13:52:02 <alise> actually .ne looks nicer to me, so
13:53:25 <AnMaster> hm, while I do like some of the points of total fp, I still quite like non-constructive proofs. what a dilemma this is :/
13:54:17 <AnMaster> alise, do you reject or accept proof by induction btw?
13:54:25 <alise> Induction is obviously true.
13:54:37 <alise> Proof: Structural recursion.
13:55:35 <alise> Why haven't you asked me about the Axiom of Choice yet?
13:56:54 <AnMaster> you can't prove it, that is why it is called axiom. But why are you so eager to be asked about it?
13:57:11 <AnMaster> (at least you can't prove it from some sets of axioms)
13:58:16 <AnMaster> alise, also since you accept transfinite induction, doesn't that mean you must accept AoC?
14:01:35 <alise> you are mixing it up
14:01:35 <alise> Anyway, I only accept some of the Axiom of Choice: the part that is provable.
14:01:46 <alise> http://r6.ca/blog/20050604T143800Z.html
14:01:54 <alise> The intensional axiom of choice. But you know what?
14:01:57 <alise> It doesn't imply well-ordering.
14:02:08 <alise> It's Axiom of Choice without the weird shit.
14:02:11 <alise> And it's provable in type theory.
14:02:33 <alise> putString : (Sigma (w : World m c). pre c) -> (World (m+1) (modify c) -> Sigma (w' : World n c'). (n > (m+1) ? post c'))
14:02:33 <alise> where pre c = stdout is open in conditions
14:02:33 <alise> modify c = c (I don't think writing to stdout should ever change conditions...)
14:02:33 <alise> post c = nothing, we require no postconditions here
14:02:43 <alise> oh wait, forgot the result
14:03:26 <alise> putString : (Sigma (w : World m c). pre c) -> (World (m+1) (modify c) -> Sigma (w' : World n c'). (n > (m+1) ? post c')) -> Sigma (w' : World n c'). (n > (m+1) ? post c')
14:03:28 <alise> oh, I forgot the actual string :D
14:04:40 <AnMaster> I can't read that, and you know that
14:05:49 <alise> putString : String -> WorldSatisfying m c stdoutOpen -> (World (m+1) c -> WorldGreater n c' (m+1)) -> World n c
14:05:56 <alise> AnMaster: I'm just musing to myself
14:06:33 <alise> AnMaster: actual usage of this will look something like
14:06:36 <alise> main = putString "Hello, world!"
14:06:56 <alise> AnMaster: it's just condition magic so that it's actually impossible for the program to, e.g. write to a closed handle
14:07:09 <alise> because the writing functions require the conditions of the world you give it to have that file handle to be open
14:07:26 <alise> and the close function transforms the conditions in the new world the continuation gets so that the handle is closed there
14:08:07 <AnMaster> alise, it shouldn't be too hard to make it impossible to write to a closed handle in a "normal" language. (Yeah "normal" isn't really the right word, but...)
14:08:18 <alise> I'm talking at typechecking time here.
14:08:27 <AnMaster> right, that is somewhat harder
14:08:32 <alise> (AnMaster slowly creeps away, defeated.)
14:08:42 <alise> AnMaster: Slight misuse of the term somewhat there
14:08:43 <AnMaster> for runtime, something like ref counting should work
14:09:58 <AnMaster> alise, well, perhaps. but if you in a "normal" language would require proof that a file handle could not escape a given scope, and then could prove how it is used in said scope it would be possible before runtime there too. no?
14:10:22 <AnMaster> of course, that doesn't cover all possible situations
14:12:37 <alise> how can you require a proof in a normal language
14:12:58 <alise> "Recursion must be easier than recursion. Otherwise recursive programs would never terminate."
14:16:40 <alise> type IO r = (Sigma (w : World m c). pre c) -> (World (m+n) (change c) -> r -> Sigma (w : World m' c'). (m' > (m+n) /\ post c')) -> World m' c'
14:17:34 <alise> type IO pre change post r = (Sigma (w : World m c). pre c) -> (World (m+n) (change c) -> r -> Sigma (w : World m' c'). (m' > (m+n) /\ post c')) -> World m' c'
14:17:41 <alise> main : IO stdoutOpen id (const ?) Unit
14:17:41 <alise> main = putString "Hello, world!"
14:17:45 <alise> That's const T there
14:17:49 <alise> main : IO stdoutOpen id (const T) Unit
14:17:49 <alise> main = putString "Hello, world!"
14:18:27 -!- fax has joined.
14:18:51 <alise> IO pre change post r -- the type of an IO interaction on a world satisfying pre, which does change to the world's conditions, and results in an r, as long as the world at the end of the hullabaloo satisfies post
14:18:53 <alise> type IO pre change post r = (Sigma (w : World m c). pre c) -> (World (m+n) (change c) -> r -> Sigma (w : World m' c'). (m' > (m+n) /\ post c')) -> World m' c'
14:19:01 <alise> oh, I need to paramaterise over n... grr
14:19:05 <alise> I'd rather not though
14:19:16 <alise> fax: simplify my io system :p
14:20:42 <fax> zoom in on his pocket, what's in that letter?
14:22:29 <fax> I like data IO :: * -> * where Return :: a -> IO a ; (:>>=:) :: IO a -> (a -> IO b) -> IO b ; PutChar :: ...
14:22:46 <fax> you can just do something like that, except with stronger specifications in the types
14:23:22 <alise> but that breaks things when you add new IO actions
14:23:25 <alise> IMO, you should be able to write
14:23:29 <alise> postulate foo : ... some IO action ...
14:23:33 <alise> and have everything still work
14:24:59 <alise> type IO pre change post r = (Sigma (w : World m c). pre c) -> ((Sigma (w' : World m' (change c)). m' > m) -> r -> Sigma (w'' : World m'' c'). (m'' > m' /\ post c')) -> World m' c'
14:25:11 <alise> I guess I don't need to paramaterise on pre/change/post, that can just be part of the types of the actions
14:26:35 <alise> type IO r = ((Sigma (w : World m c). m > SOMETHING) -> r -> Sigma (w' : World m' c'). (m' > m /\ SOMETHING)) -> World m' c'
14:27:10 <fax> I never understood the 'realworld' stuff
14:27:17 <fax> just seemed inelegant to me
14:27:39 <alise> well here World is a very abstract thing
14:28:03 <alise> World m c is a (thing) of sequence number m (we use this to ensure you can't use the same world twice, as you have to do it increasingly), with conditions c
14:28:05 <alise> conditions are things you can do like
14:28:15 <alise> as in, in the conditions c, is the file handle stdout open?
14:28:22 <alise> and also transform
14:28:24 <alise> withClosed stdout c
14:28:41 <alise> apart from that, it's completely opaque
14:28:55 <fax> c++ help super primes @_@
14:28:56 <fax> immediate need asap : c++ help super primes @_@
14:30:06 <alise> hmm, I guess I need postulate data structures
14:30:22 <alise> postulate IOStruct : Sigma (IO : Set). isIO IO
14:30:39 <alise> and I need to posulate World instead
14:30:59 <alise> postulate WorldStruct : Sigma (World : Nat -> Conditions -> Set). isWorld World
14:31:51 <alise> fax: i mean your IO data structure just doesn't handle things like FFIs and the like
14:31:55 <alise> or even added IO operations
14:32:12 <fax> yeah it does
14:32:13 <alise> fax: besides you need SOME sort of world-like structure, because you need to be able to do pre and post conditions
14:32:15 <fax> that's what the ... bit was for
14:32:32 <fax> it's put pre & post conditions in bind
14:33:00 <alise> so what is bind's type?
14:33:48 <fax> forget about IO for a moment
14:33:53 <fax> this works for any monad
14:35:30 <fax> nevermind, it was wrong
14:36:08 <alise> type IO r = ((Sigma (w : World m c). m > SOMETHING) -> r -> Sigma (w' : World m' c'). (m' > m /\ SOMETHING)) -> World m' c'
14:36:11 <alise> is that I can't say SOMETHING
14:41:36 <alise> fax: http://pastie.org/878467.txt?key=babbgfpdokohtn3kjvzdnq
14:41:50 <alise> this is obviously wrong in some major way because I can't figure out how it isn't wrong
14:42:32 <alise> but I /think/ it's a totally pure, general, abstract constraint-based IO system
14:43:15 -!- pikhq has quit (Read error: Connection reset by peer).
14:43:28 <alise> this project - write hello in nance - turns out to be much harder than I ever imagined
14:44:32 <alise> fax: so how would /you/ do it :)
14:44:44 <fax> I don't do IO
14:45:21 <fax> just do pure programming in a monad then write a 10 line C/Haskell thing to drive it
14:46:31 <alise> nah the whole point of volit is to extract the program from the ... program
14:46:36 <alise> safe io is very important
14:46:49 <alise> and i think being able to prove things about IOing programs is awesome
14:52:51 <alise> fax: what was that method you suggested for doing inductive data types?
14:56:12 <alise> fax: you said it yesterday
14:56:21 <alise> you axiomatise induction or something and then that gives you inductive types
14:59:05 <alise> I wish ais523 was here so I could ask him something.
15:00:02 <alise> fax: can you define coinductive data types with inductive ones?
15:00:58 <fax> I don't know
15:05:22 <alise> nance foo.ne -o foo.prove && prove foo.prove && volit foo.ne -o foo.hs && ghc -O2 --make foo.hs -o foo
15:05:33 <alise> Hmm, I guess nance and volit have to share a library so they can process Nance code.
15:05:40 <alise> Although I could also have /another/ intermediate form:
15:06:44 <alise> nance foo.ne -o foo.ncr && ncr2prove foo.ncr && prove foo.ncr && volit foo.ncr -o foo.hs && ghc -O2 --make foo.hs -o foo
15:07:11 <alise> nance foo.ne -o foo.ncr && ncr2prove foo.ncr -o foo.prv && prove foo.prv && volit foo.ncr -o foo.hs && ghc -O2 --make foo.hs -o foo
15:07:18 <alise> So ncr has enough information to distinguish things like Prop and Set easily, while prv is completely core.
15:11:21 <alise> So then to trust a Nance proof foo.ne, you have to trust that nance compiles it correctly to foo.ncr, then that ncr2prove compiles foo.ncr correctly to foo.prv, then prove checks it correctly.
15:11:38 <alise> As opposed to: to trust a Nance proof foo.ne, you have to trust that nance compiles it correctly to foo.prv, then that prove checks it correctly.
15:11:45 <alise> Prove checking it correctly is basically certain, so:
15:11:52 <alise> Trust nance & ncr2prv vs trust nance.
15:14:49 -!- pikhq has joined.
15:52:52 -!- atrapado has quit (Quit: Ex-Chat).
16:27:07 <alise> woo, I can use unetbootin to boot the ubuntu iso from an ntfs partition i think
16:46:28 -!- ais523 has joined.
16:50:10 <alise> Have you tried the 10.04 beta?
16:50:26 <alise> http://1.2.3.9/bmi/news.softpedia.com/images/extra/LINUX/large/ubuntu10artwork-large_009.jpg ;; the theme is a bit pretty.
16:50:30 <alise> But it uses Yahoo! by default (?!)
16:50:39 <alise> and includes some social networking bullshit by default; sigh
16:50:42 <ais523> alise: yahoo paid them more than google
16:50:47 <ais523> but you can change it back easily enough
16:51:02 <alise> yes, but it exposes canonical a bit for the money-grabbing bastards they are :))
16:51:23 <alise> I'm downloading 9.10 now just because I'd like some stability. 10.04? Maybe later.
16:51:28 <alise> When I have more bandwidth, perhaps.
16:52:46 <alise> Now if only they'd fix the subpixel rendering...
16:55:37 -!- alise_ has joined.
16:56:00 <alise_> My 3G connection dropped. Disconnected, reconnected - chrome portrays the ISO as downloaded - no resuming - fuck!
16:57:16 -!- alise has quit (Ping timeout: 256 seconds).
16:58:11 <alise_> ais523: Punch me so I feel better
16:58:57 <alise_> http://nctritech.files.wordpress.com/2008/11/tcpip_punch1.jpg
16:59:36 * alise_ ponders whether to redownload 9.10 or go for 10.04
16:59:40 <ais523> alise_: I take it it didn't manage to download before the connection dropped?
16:59:49 <alise_> ais523: not unless I suddenly got a 100 mbit connection
17:00:07 <Deewiant> This is why you should use something that can resume when you're on an uncertain connection
17:00:16 <alise_> Deewiant: I thought Chrome would be such a thing.
17:01:01 -!- songhead95 has quit (Quit: songhead95).
17:01:13 <ais523> it seems a bizzare feature for Chrome not to have
17:03:06 <alise_> Deewiant: Then you will be tanasin?
17:03:46 <Deewiant> What does tanasinn have to do with anything :-P
17:04:11 <alise_> 10.04: Unstable lots of updates so network access and stuff... but nice themes and stuff, and, uh, ...
17:04:25 <alise_> Deewiant: "Don't think, feel. Then you will be tanasinn."
17:04:49 <alise_> Constructivist tanasinn.
17:06:08 <ais523> alise_: isn't 10.04 the version which puts the minimize/close/maximise buttons on the top-left of the window, in defiance of both fitts' law and common sense?
17:08:12 <alise_> ais523: It doesn't defy Fitts', and OS X does it too
17:08:19 <alise_> the close position sucks though
17:08:25 <alise_> it's unfittsy there, I agree
17:08:27 <ais523> alise_: the close position isn't in the corner, like it is on OS X
17:08:38 <alise_> http://www.design-by-izo.com/2010/03/13/ubuntu-lucid-and-that-button-layout/
17:08:41 <ais523> also, it's very close to the menus, which has the effect of meaning you have to be more careful
17:08:55 <alise_> http://www.design-by-izo.com/wp-content/uploads/2010/03/button-layout-kde.png seems like the best solution
17:09:01 <alise_> it's the most fittsy of them all
17:09:52 <ais523> alise_: oh, my close button's red already
17:09:55 <ais523> I use the New Wave theme
17:10:00 <ais523> at least, it turns red when you hover over it
17:10:06 -!- songhead95 has joined.
17:10:07 <alise_> I wasn't talking about redness :P
17:10:12 <ais523> and although it doesn't look like it stretches to the corner, it fdoes
17:10:14 <ais523> alise_: no, but he was
17:10:40 <alise_> http://www.design-by-izo.com/wp-content/uploads/2010/03/button-layout-kde.png <-- this is a pretty kde theme, I wonder what it is
17:10:56 * alise_ just installs 9.10, I'm too lazy to do anything fancy
17:11:09 <alise_> what's good for resumable windows downloads?
17:11:25 <ais523> I think firefox does them, but it's a bit bloated
17:11:34 <ais523> you could grab a Windows copy of wget, that would probably be ideal
17:11:51 <alise_> http://1.2.3.11/bmi/www.jensroesner.de/wgetgui/wgetgui_simple.png
17:11:58 <alise_> http://www.jensroesner.de/wgetgui/wgetgui_simple.png
17:12:03 <alise_> I regret googling "Windows wget ui"
17:12:39 <ais523> oh, I'd say go for a command-line tool
17:12:59 <ais523> also, http://1.2.3.11/ what?
17:13:07 <alise_> stupid 3g broadband stick mangles all images :)
17:13:07 <ais523> 1.2.3.0/24 is reserved
17:13:22 <alise_> (to add javascript so you can do shift-r/a to improve the quality of images)
17:13:26 <ais523> haha, it's contributing to 1.2.3.0/24 pollution
17:13:34 <alise_> you can send a certain header to stop it -- but I don't think Chrome can do that :)#
17:14:19 <ais523> why doesn't it just use an IP in 10 or 192.168?
17:14:26 <ais523> those would both be obvious choices, considering what it's doing
17:15:13 <fizzie> ais523: The "obvious" reason for not using a private-area IP is to avoid conflicts for people who use those in their local networks, but I don't quite see how it'd apply for a 3G stick necessarily.
17:15:38 <ais523> also, avoiding conflicts by using you're using an address that's specifically reserved for a different purpose, and hoping nobody else will use it either?
17:16:01 <fizzie> Deewiant: You could make some "172.16/12 - never forget!" T-shirts.
17:16:36 <ais523> Deewiant: I was aware there was a /12 floating around somewhere for that purpose, but not its number
17:18:10 <fizzie> They have one block in each of the class A, B and C ranges, even though everything's so CIDRy nowadays.
17:19:29 <alise_> Wow, there is not one shitty Windows download manager.
17:19:33 <alise_> Guess I'll just use command-line wget.
17:20:36 <Deewiant> alise_: http://www.oldversion.com/GetRight.html
17:21:39 <alise_> Which is the least shitty version? :-)
17:22:03 <Deewiant> I can't remember, to be honest
17:22:19 <Deewiant> Presumably any of the ones that are there are non-shitty
17:23:10 <fizzie> Their official description is funny: "GetRight® is a download manager that simply improves and optimizes the files you download from the Internet."
17:23:14 <alise_> Apparently 6.3 is the latest, and it has 6, so probably not
17:23:19 <fizzie> Not only does it download well, it even makes the content better.
17:24:02 <alise_> Wise Installation Wizard. 2002. A /bit/ too old.
17:25:32 <ais523> hey, that even predates XP, somehow
17:25:42 <ais523> still, I remember wise
17:25:49 <ais523> more for the uninstall program, which was called unwise
17:25:55 -!- olsner_ has joined.
17:26:03 <alise_> Really old is good; new is sometimes good.
17:26:08 <alise_> In-between is shitty. Usually. For Windows.
17:26:16 <alise_> ---------------------------
17:26:16 <alise_> Unsupported 16-Bit Application
17:26:16 <alise_> ---------------------------
17:26:16 <alise_> The program or feature "\??\C:\Users\Elliott\Documents\Downloads\getright13.exe" cannot start or run due to incompatibity with 64-bit versions of Windows. Please contact the software vendor to ask if a 64-bit Windows compatible version is available.
17:26:16 <alise_> ---------------------------
17:26:17 <alise_> ---------------------------
17:26:32 <ais523> alise_: it was common back then, 32-bit programs were relatively unreliable on XP
17:26:44 <ais523> I know, I always wrote 16-bit for XP because it had trouble getting 32-bit programs working correctly
17:26:55 <ais523> well, XP (before SP) and 98
17:27:00 <Deewiant> alise_: 2002 is too old? I had probably stopped using getright by 2000
17:27:00 <alise_> almost all XP programs are 32-bit. And this is really old, not XP era.
17:27:04 <ais523> the issue being that half the APIs didn't work
17:27:12 <alise_> Deewiant: Yeah, but Wise gives me AIDS.
17:27:16 <ais523> so you had to keep trying them more or less at random until you found one that did
17:27:22 <alise_> (Yes, it gives me AIDS every single time I use it.)
17:27:34 <Deewiant> alise_: I use a reliable Internet connection ;-)
17:27:44 <alise_> Yeah, well, slight issues with that
17:28:18 <Deewiant> alise_: Opera probably has this stuff built in, FWIW. It tends to.
17:28:18 <fizzie> Let's party like it's.
17:28:22 <ais523> isn't that before Windows really understood networking?
17:28:31 -!- songhead95 has quit (Quit: songhead95).
17:29:12 <AnMaster> <ais523> alise_: it was common back then, 32-bit programs were relatively unreliable on XP
17:29:27 <ais523> AnMaster: early versions, at least
17:29:32 <alise_> ais523 is in a fantasy world of crazy
17:29:36 <AnMaster> ais523, that's rather hard to believe
17:29:39 <ais523> hmm, either that, or it's just that my 32-bit compiler was rather unreliable
17:29:44 <ais523> thinking about it, that seems a lot more plausible
17:29:47 <AnMaster> I mean sure, for windows 95 or windows NT 4.0
17:29:48 <fizzie> That's probably a matter of definition; compared to 3.x, all the 9x releases have been pretty internet-savvy. I don't even think you needed a separate TCP/IP stack any more. (Or was it so that IE in 95 still had one?)
17:29:54 <AnMaster> yes probably there it could happen
17:30:13 <Deewiant> fizzie: Certainly not in 98. Not sure about 95.
17:30:45 <AnMaster> I mean, I never saw the point of them
17:30:55 <AnMaster> what can they do that normal tools to download can't?
17:30:55 <fizzie> Deewiant: Does it do the impolite "open multiple connections to same server" thing by default?-)
17:30:57 <alise_> resuming on failed connection
17:31:07 <alise_> man this program is so uh... 1999
17:31:10 <Deewiant> fizzie: I'm not sure. It might.
17:31:21 <Deewiant> fizzie: I think the early versions didn't, at least.
17:31:28 <AnMaster> alise_, is there no wget for windows? I'm pretty sure there was a non-cygwin port of wget
17:31:52 -!- nooga has quit (Ping timeout: 240 seconds).
17:32:03 <alise_> AnMaster: There is, but meh.
17:32:08 <alise_> I'd prefer it automatically doing so when my connection breaks.
17:32:16 <alise_> I should write a good download manager, except I won't be using Windows for much longer.
17:32:23 <AnMaster> alise_, I'd prefer it to do when I regain connection instead ;P
17:32:29 <Deewiant> AnMaster: Back in the day there might not have been; plus it's CLI, so a bit annoying for normal people, and thus it only handles one file at once.
17:33:08 <alise_> The interface for my download manager would be a list with filenames, progress meters, downladed/total, speed, estimated time and a cancel button to remove it from the list. Downloading would be dragging a URL to the window.
17:33:09 <AnMaster> Deewiant, back in the day it would have been too slow to download more than one file at once
17:33:31 <ais523> well, is there a good GUI download manager even for Linux that isn't attached to a browser?
17:33:36 <alise_> with zmodem you could chat /and/ download
17:33:37 <AnMaster> alise_, like the firefox download list basically?
17:33:41 <ais523> wget's an excellent /command-line/ download manager, but it isn't GUI
17:33:42 <alise_> ais523: but why? linux browsers do it just fine :P
17:33:49 <AnMaster> I think firefox does do resuming
17:33:53 <alise_> ais523: ooh, this links into an excellent idea I had for a GNOME UI feature
17:33:57 -!- nooga has joined.
17:33:57 <AnMaster> ais523, pretty sure I saw a KDE one once
17:34:12 <alise_> ais523: now you ask what it is
17:34:14 <AnMaster> oh wait, it was ais523 who asked it in fact
17:34:17 -!- wIRC9 has joined.
17:34:17 <Deewiant> AnMaster: Yes, which is exactly why you want a manager, so that you can queue dozens.
17:34:34 -!- wIRC9 has quit (Client Quit).
17:34:38 <AnMaster> alise_, ais523: you have nicks starting on same char and of the same length
17:34:41 -!- songhead95 has joined.
17:34:46 <alise_> ais523: ASK WHAT IT IS
17:34:51 <ais523> AnMaster: your nick also starts with the same char
17:34:56 <ais523> alise_: oh, what is it/
17:34:58 <fizzie> Deewiant: I think it went so that plain 95 didn't include a TCP/IP stack, but they made one and distributed it with IE 2-or-so and the later 95 versions; and I think the IE dialler and stack also worked in 3.11 later on. There was also a version of Trumpet Winsock for 95.
17:34:58 <alise_> and is of the same length if you pad it out!
17:35:06 <alise_> ais523: I'll tell you in /msg, it's floody
17:35:07 <ais523> I thought you wanted me to ask AnMaster what his KDE download manager was
17:35:10 <AnMaster> ais523, it is of different case and nick of different length
17:35:22 <ais523> AnMaster: IRC is case-insensitive
17:35:23 <AnMaster> I just noticed that one existed
17:35:40 <ais523> AnMaster: hey, I didn't ask, it was alise_ who didn't ask me to ask you!
17:35:43 <AnMaster> ais523, well sure, but that isn't relevant to visually reading the nicks
17:35:49 <fizzie> Deewiant: I do remember that for a 3.11 user, the IE dialler was considerably more modern-looking than the (maybe not most current) version of Trumpet I had.
17:36:03 <ais523> AnMaster: they're different colours in this client...
17:36:44 <AnMaster> ais523, I never liked that, most of the time it is even more confusing
17:36:49 <fizzie> AnMaster: Trumpet Winsock.
17:37:16 <fizzie> AnMaster: Yes, I think it could do PPP too; also SLIP.
17:38:15 <fizzie> Also, I don't think you can chat and download simultaneously with (unmodified) ZMODEM, because I think the main "killer feature" of SMODEM was the chat thing. (And there was some competitors too.)
17:38:45 -!- alise_ has quit (Read error: Connection reset by peer).
17:38:57 <AnMaster> wasn't smodem something used for BBS or such
17:39:02 <fizzie> SMODEM also does bidirectional transfers.
17:39:17 -!- alise_ has joined.
17:39:24 <alise_> I'm not entirely sure this resume worked
17:39:33 <fizzie> http://en.wikipedia.org/wiki/File:SModem.png -- look, isn't it awesome!
17:39:39 <alise_> oh fuck this shit, someone mail me an ubuntu cd
17:39:57 <AnMaster> alise_, you could get them for free before iirc
17:41:17 <alise_> yeah but it takes time
17:41:29 <AnMaster> so does it for everyone else here too
17:41:29 -!- alise_ has quit (Read error: Connection reset by peer).
17:41:46 -!- alise_ has joined.
17:43:17 <fizzie> Switch to the QNX Demo Disk, it's modern as anything, with a web browser and all, and yet you'd have to download just two floppies.
17:43:22 <fizzie> http://toastytech.com/guis/qnxdemo.html
17:43:30 <fizzie> You might have some problems with the 3G stick in it, though.
17:43:45 <fizzie> But there's the "QNX Is Cool!" demo!
17:43:50 -!- alise_ has quit (Read error: Connection reset by peer).
17:44:06 -!- alise has joined.
17:46:01 -!- alise has quit (Read error: Connection reset by peer).
17:46:37 -!- alise_ has joined.
17:47:17 <fizzie> That is one unreliable network.
17:48:28 -!- alise_ has quit (Read error: Connection reset by peer).
17:49:46 -!- alise_ has joined.
17:50:08 <fax> afphhpfhffhpfphhnjgeul
17:53:00 -!- oerjan has joined.
17:53:24 -!- kar8nga has quit (Remote host closed the connection).
17:53:24 -!- alise_ has quit (Read error: Connection reset by peer).
17:53:42 -!- alise has joined.
17:54:59 -!- nooga has quit (Ping timeout: 260 seconds).
17:55:34 -!- alise has quit (Read error: Connection reset by peer).
17:55:51 -!- alise has joined.
17:57:49 -!- alise has quit (Read error: Connection reset by peer).
17:58:07 -!- alise has joined.
18:02:52 -!- alise has quit (Ping timeout: 276 seconds).
18:03:26 -!- songhead95 has quit (Quit: songhead95).
18:04:27 -!- alise has joined.
18:04:28 <alise> Anyone remember optbot? :)
18:04:40 <ais523> although I can't remember what it did
18:04:56 <alise> repeated random lines from history
18:05:06 <oerjan> i remember it was named for me
18:05:17 <alise> well, also AnMaster
18:05:23 <alise> AnMaster said otpbot for the erlang thing
18:05:34 <alise> Oerjan's Puns Terrible or something
18:05:41 <alise> no it was Oerjan's Terrible Puns
18:05:45 <alise> but I kept typoing opt
18:06:29 <fizzie> fungot can also repeat random lines from history, it just gets a bit confused sometimes.
18:06:32 <fungot> fizzie: the question of rendered fat, the commission will clearly seek every available means to escape the current legal framework, mr president, and what we are intending to use its relationships with european partners, the non-governmental organizations which, in the coming months, the forwarding of appropriations to implement the legislation and practice. however, we must support all initiatives that aim at strengthening our
18:06:45 <fizzie> Oh, someone's been doing politics again.
18:07:19 <alise> 16:24:03 <AnMaster> ehird, caller() { local myvar; callee "myvar" "other arguments"; } callee() { printf -v "$1" "%s" "$2"; }
18:07:29 <fizzie> Bot-tweet: "About NetHack: hacking: the chamber was of a retreating nymph. 'saruman!' he cried, and treasure it as though it were a piece of v-shaped..."
18:07:34 <alise> AnMaster: can you eval in the caller's scope?
18:08:17 <oerjan> local is dynamically scoped, not static, if that's perl
18:08:32 <oerjan> (proper static is "my" iirc)
18:08:44 <fizzie> That doesn't look like perl; there's no sub, and no sigil for the var.
18:09:23 <fizzie> But you can eval code in the caller's scope in MATLAB, too: evalin('caller', 'x = 42'); is a rather impolite thing to do.
18:09:44 <oerjan> <oklopol> can't you do geometry on rationals?
18:09:52 <oerjan> no, you need square roots
18:10:11 <fizzie> Or even evalin('base', 'x = 42'); if you want it to be evaluated directly in the workspace of the user's session.
18:10:25 <ais523> in Perl, you can't exactly eval in the caller's scope
18:10:27 <oerjan> the constructible numbers it's the smallest field closed under square roots
18:10:38 <ais523> but you can take the caller's local/lexical variables from the symbol table and modify them that way
18:10:58 <oerjan> (well, field of reals)
18:11:19 <Deewiant> fizzie: Why would one ever want to use this? :-P
18:11:47 <fizzie> Deewiant: You can use it to forcibly return values, even if the caller doesn't want you to. :p
18:12:08 <Deewiant> Well yes, you can use it to be obnoxious
18:12:09 <fizzie> Deewiant: There's also a curious restriction: "evalin cannot be used recursively to evaluate an expression. For example, a sequence of the form evalin('caller', 'evalin(''caller'', ''x'')') doesn't work."
18:12:10 <alise> it's bash not perl
18:12:14 <alise> eqaw4235s6etf987yg-p09uh-o]=p
18:12:39 <AnMaster> <alise> AnMaster: can you eval in the caller's scope? <-- that is bash, but well I think I described it at the time I mentioned it
18:12:40 <alise> [#324qw56e7ri8ulp9jo[0j['0oi;pj0l98hyngtfrxeadwq4rs6hu8,ghp0oi[;0,l98gu7y6tfry5d6t4esrw3aqe4st6p0o'l[0ogy6utfd65eswra432qstdey6p[0o'0j98sw5y6gtik09y6tr4eswgr4sw6tr4efwas4uy60pytfresar6y6tr4fesw646ir4fe3r4y6eaw87tr4ef
18:12:41 <fizzie> Deewiant: There's also assignin() if you want to stick a value into the caller's workspace without having to turn it into a string like that.
18:13:11 <Deewiant> fizzie: Awfully handy, I suppose
18:13:49 <fizzie> Deewiant: The examples do look a bit contrived.
18:13:51 <AnMaster> alise, anyway, why aieeee? You saw it before
18:14:15 <fizzie> Deewiant: "The assignin function is particularly useful for these tasks: Exporting data from a function to the MATLAB workspace. Within a function, changing the value of a variable that is defined in the workspace of the caller function (such as a variable in the function argument list)."
18:14:25 <ais523> in INTERCAL, you can assign variables in the caller's scope by temporarily ending scope for that variable, then resuming it again
18:14:33 <ais523> scopes in INTERCAL don't actually have to be well-nested
18:14:34 <fizzie> Deewiant: I guess the latter part makes it a sort of a pass-by-reference mechanism.
18:15:06 <fizzie> Deewiant: You can do value = evalin('caller', varname) to "dereference" the "pointer", and then assignin('caller', varname, value) to set it.
18:15:51 <ais523> I think I prefer the INTERCAL method
18:16:07 <fizzie> Deewiant: Well, MATLAB's completely pass-by-value, as far as I remember, so if you want to do that sort of stuff...
18:16:45 <fizzie> (There's a copy-on-write thing if you pass in a large matrix.)
18:16:51 <AnMaster> alise, as for eval in caller's scope, define what that actually would mean in terms of bash scoping please
18:17:04 <alise> pass-by-singular-reference
18:17:09 <AnMaster> I can't figure out how the question makes sense in bash's model
18:17:12 <alise> all equal values have the same reference; passing a value passes this reference
18:17:18 <alise> mutating it mutates it in all places
18:17:53 <alise> f(x) = {x += 1}; y = 2+1; f(3); print(y) --> 4
18:18:15 <AnMaster> alise, everything will be resolved to the first scope that has it
18:19:06 <AnMaster> the only thing for which eval in local scope would differ from eval in own scope would be: a) making new local variables in caller b) in case of your own local variables shadowing the caller's
18:19:18 <AnMaster> I think the answer to those is: "no you can't do that"
18:20:04 <alise> anyone remember my language where you could goto /anywhere/? :)
18:20:16 <ais523> it was, but rather too similar to INTERCAL
18:20:23 <alise> Deewiant: no, it was structured that's the beauty
18:20:25 <ais523> Deewiant: no, you could goto, say, the inside of an expression
18:20:31 <alise> returns were jumping to the right place in your caller
18:20:36 <alise> you could jump into the middle of a loop and it'd work fine
18:20:38 <ais523> actually, you can do that in Overload too
18:20:43 <alise> ais523: I wasn't sure about expressions
18:20:44 <ais523> only Overload is a mess that I've abandoned
18:20:45 -!- myndzi has quit (Read error: Connection reset by peer).
18:20:46 <alise> but any statement, certainly
18:20:52 <ais523> executing a pointer took you to wherever the pointer was pointing
18:21:03 <ais523> fixing the callstack after that was your responsibility
18:21:10 <ais523> (so there wasn't really a callstack)
18:21:13 <AnMaster> <ais523> aww, why not? <-- I can't think of a way to do theose
18:21:17 -!- myndzi has joined.
18:21:23 <AnMaster> if someone else know a way, please tell
18:21:24 <ais523> hey, I invented CPS without realising it
18:21:37 <ais523> /just now/ I have realised that Overload is CPS
18:21:43 <ais523> and it's been like that for years
18:23:11 <AnMaster> anyway I just realised that <alise> 16:24:03 <AnMaster> ehird, caller() { local myvar; callee "myvar" "other arguments"; } callee() { printf -v "$1" "%s" "$2"; }
18:23:23 <AnMaster> if the callee had it's own local variable "myvar" defined
18:23:55 <AnMaster> so to ensure a roubust program, local variables should be prefixed with some sort of namespacy thingy
18:24:14 <AnMaster> lcl_<function name>_<variable name>
18:24:35 <fizzie> Deewiant: Hey, the only usage example for evalin is "This example extracts the value of the variable var in the MATLAB base workspace and captures the value in the local variable v: v = evalin('base', 'var');" It doesn't really help in understanding why you'd want to use it.
18:25:49 -!- songhead95 has joined.
18:26:28 <AnMaster> fizzie, the reason for using this sort of thing in bash
18:26:36 <AnMaster> is that you can only return an unsigned byte
18:27:08 <AnMaster> which means you *have* to do this way to return anything more complex
18:27:18 <fizzie> It's silly that way. Matlab lets you return an arbitrary number of return values, and in any case those return values can be arbitrary data structures.
18:27:23 <AnMaster> or use some global "return_value" variable
18:27:31 <AnMaster> but that seems even more error prone
18:28:00 <AnMaster> fizzie, also for bash this is just a side effect of the scoping rules
18:28:05 <AnMaster> printf -v is just "print to variable name"
18:28:14 <AnMaster> because indirect assignment requires that or eval
18:28:34 <AnMaster> you can't do foo=quux; $foo=bar and get bar into quux
18:29:10 <AnMaster> for the other way around, reading a variable from the variable name you get passed as a variable there is special syntax
18:29:14 <fizzie> I guess in MATLAB you'd be most likely to use this as a some sort of a debugging aid; sticking an "assignin('base', 'temp', confusing_expression);" somewhere means that after executing it, you'll have the value inspectable in the session.
18:29:49 <AnMaster> foo=bar; myvariable=foo; echo ${!myvariable} would echo bar I think
18:29:58 <AnMaster> might have been something else than ! there
18:30:20 <AnMaster> fizzie, does matlab have a debugger though?
18:31:04 <AnMaster> bash 4 has associative arrays, but I "emulated" that before in bash 3.x
18:32:49 <alise> STUPID FUCKING PIECE OF
18:33:06 <AnMaster> fizzie, hm does C++ have anything to mess up the scoping?
18:33:35 <AnMaster> if not, that might one of the very few sane parts of C++... (C has quite sane scoping IMO)
18:33:41 <ais523> AnMaster: probably, C++ can mess up /anything/
18:34:28 <AnMaster> well, C99 does something strange for inline without static iirc
18:34:42 <AnMaster> in particular extern inline, which might be a GNU extension
18:35:42 <olsner> istr there was a gnu extension, and then C99 invented something with the same syntax but a different meaning
18:36:16 <AnMaster> olsner, and yes that sounds familiar
18:36:36 <alise> afdnkjsdfn\jkfkjsdaghsdkfghjsdkjfghskjdfghdafsgdfg
18:36:39 <alise> this fucking 3g stick piece of crap
18:36:53 <AnMaster> alise, calm down, it won't become better because you are angry at it
18:37:09 <AnMaster> alternatively: channel your rage, and insert a really bad star wars joke
18:37:37 <alise> i've been trying to download this file for .... like three hours
18:37:42 <alise> first time almost done cut off
18:37:50 <alise> then my connection broke while trying to find ONE download manager that works
18:37:55 <alise> now it's just cutting off randomly after 30 seconds or so
18:38:00 <alise> AnMaster: BUT NONE OF THIS SHIT IS WORKING YOU IDIOT >_<
18:38:09 <AnMaster> alise, well on the original file
18:38:20 <fizzie> There is some sort of "he has no patience" starwars joke to be made here.
18:38:34 <alise> Deewiant: 600 megabytes or therewithin
18:38:36 <songhead95> i had to go with the "Credits will do fine"
18:38:41 <alise> d you have to use -c the first time to use -c later?
18:38:47 <alise> not that it matters
18:38:52 <alise> 6 kb/sec, wonderful
18:38:54 <AnMaster> fizzie, that too, but I was going for the "try to convert to dark side"
18:39:05 <fizzie> 6 kb/sec is a rather respectable modem speed.
18:39:16 <alise> ais523: ok, this will be quicker: I'm coming to Birmingham; have an Ubuntu 9.10 USB stick ready when I arrive
18:39:19 <fizzie> I seem to recall some sort of "a megabyte per hour" rule of thumb.
18:39:32 <ais523> alise: USB stick's ready already
18:39:38 <ais523> and are you /serious/?
18:39:44 <Deewiant> alise: 600 megabytes would take you several days with a modem connection; I wouldn't worry about a few hours
18:39:55 <alise> ais523: hmm... let me ask google maps
18:40:20 -!- songhead95 has quit (Quit: songhead95).
18:41:00 <alise> ais523: hmm... on public transport it'd take me anywhere between 7 and 10 hours
18:41:10 <alise> by car, only 3.5 hours
18:41:21 <alise> quick, use quantum mechanics to transfer a car here
18:41:42 <alise> do you need -c to resume later?
18:41:45 <alise> or does it work anyway
18:41:47 <alise> say it works anyway
18:42:02 <fizzie> You don't need -c at the first invocation, if that's what you mean.
18:42:07 <fizzie> Only later when you're trying to resume.
18:42:12 <alise> good because it just broke
18:42:15 <alise> now what's the thing again to resume
18:42:40 <alise> foo is url or filename
18:43:05 <alise> now let's hope it actually resumes
18:43:05 <AnMaster> without -c wget will start downloading to <filename>.1
18:43:23 <AnMaster> alise, and lets hope there is no data corruption
18:43:33 <alise> no it will not resume
18:43:45 <AnMaster> alise, I remember downloading an iso (arch or ubuntu iirc) and the data was corrupted near the start
18:43:52 <AnMaster> since then I use bittorrent for linux iso downloads
18:44:39 <fizzie> alise: I don't remember where you live, but walking from Hexham (which I think was at least nearby at some point) to where I live would take you just 5 days, 13 hours. (It involves some 371 steps; you take the Newcastle-Ijmuiden-Amsterdam ferry to Netherlands, then the Hoek van Holland-Harwich ferry back to UK, then the Harwich-Esbjerg ferry to Denmark; then you just walk across Denmark (a hundred miles or so), take another ferry to Rostock, and from there to H
18:44:40 <AnMaster> alise, does the server support not starting at the start?
18:45:00 <AnMaster> "would take you just 5 days, 13 hours. (It involves some 371 steps;"
18:45:01 <alise> I assume you mean footsteps.
18:45:15 <fizzie> Yes, with large enough boots.
18:45:35 <alise> ...Also, why on earth would you go back to the UK? :D
18:45:49 <fizzie> alise: Because Google Maps says so!
18:46:38 <fizzie> AnMaster: You forgot Germany there. (Rostock's in Germany.)
18:47:02 <AnMaster> fizzie, not over Sweden? He is missing out on stuff then
18:47:31 <fizzie> AnMaster: Presumably it's because walking is so slow; it's good to find routes where you don't have much walking between ferry stops.
18:49:26 <fizzie> AnMaster: http://zem.fi/~fis/alise_walkabout.png
18:49:51 <Deewiant> That's a funny-looking loop near the Netherlands.
18:50:39 <fizzie> Deewiant: I asked it for walking directions from Copenhagen to Amsterdam (our summer trip goes thereby); it gave me this really silly denmark-norway-denmark-norway-UK-holland thing.
18:50:42 <AnMaster> fizzie, if it takes ferries, why not also take trains?
18:51:16 <fizzie> AnMaster: Walking directions are in beta, you see.
18:51:42 <Deewiant> fizzie: Walking directions might not be the best idea :-P
18:51:48 <oerjan> i suppose it includes ferries because sometimes you cannot avoid them, while you could always walk along the train tracks...
18:52:02 <alise> yay bittorrent download is going fast
18:52:02 <AnMaster> Deewiant, try walking directions from new york to somewhere in Europe
18:52:17 <fizzie> AnMaster: They removed the "swim over atlantic ocean" thing, I think.
18:52:36 <AnMaster> fizzie, did that actually happen in it once?!
18:53:04 <alise> We could not calculate directions between new york and helsinki.
18:53:21 <fizzie> AnMaster: See e.g. http://www.ghacks.net/2007/04/11/google-maps-swim-across-the-atlantic-ocean/
18:53:48 <alise> doesn't do helsinki to moscow anyway :(
18:53:53 <Deewiant> The car-directions hexham->helsinki make more sense
18:54:06 <alise> Walking directions to Helsinki, Finland
18:54:07 <fizzie> AnMaster: It still has "Kayak across the Pacific Ocean" as a possibility.
18:54:07 <alise> 1.Head east toward Simonkatu
18:54:18 <fizzie> AnMaster: If you ask for "new york to sydney", for example.
18:54:36 <AnMaster> fizzie, is that an easteregg then?
18:54:47 <AnMaster> I mean, it seems unlikely to be due to an oversight
18:55:14 <fizzie> AnMaster: Most likely. It's given for the "by car" directions, anyway, and I'm not sure how you're meant to take the car with you in the kayak.
18:55:26 <fizzie> That's one pretty big kayak.
18:56:34 <fizzie> 57. Take the 1st left onto Kalakaua Ave 1.9 mi
18:56:34 <fizzie> 58. Kayak across the Pacific Ocean
18:56:34 <fizzie> Entering Japan 3,879 mi
18:56:34 <fizzie> 59. Turn right toward 県道263号線 0.3 mi
18:56:35 <oerjan> clearly what you want is a large kon-tiki style raft big enough for a car
18:56:37 <AnMaster> fizzie, I get it for walking between New York and Hawaii
18:56:40 <AnMaster> 753.Kayak across the Pacific Ocean
18:56:41 <alise> .At the roundabout, take the 1st exit onto W Denton Way
18:56:41 <alise> Go through 1 roundabout
18:56:44 <alise> These are for the walking directions
18:57:05 <fizzie> alise: It should have a "Dodge the car's like it's Frogger!" written-in-red comment there. :p
18:57:33 <AnMaster> alise, could it be that there are sidewalks?
18:57:58 <alise> "Go THROUGH 1 roundabout"
18:58:32 <pikhq> Clearly Google has a psychotic AI running that.
18:59:01 <fizzie> Deewiant: Anyway, I asked for walking directions because the only other alternative was "by car", and we're not going to have/rent one; it doesn't do trains. (Was there some sort of limited-region public transportation thing already?)
18:59:25 <alise> http://maps.google.com/maps?f=d&source=s_d&saddr=hexham&daddr=helsinki+to:brussels&hl=en&geocode=&mra=ls&dirflg=w&sll=-5.52475,179.448463&sspn=74.498813,114.433594&ie=UTF8&ll=48.806863,8.481445&spn=13.289494,28.608398&z=5
18:59:33 <alise> Hexham, Helsinki, Brussels.
18:59:41 <Deewiant> fizzie: You can always hitchhike.
18:59:48 <alise> It does public transport now, yes.
18:59:52 <alise> fizzie: You should have visited me.
18:59:55 <AnMaster> to go from stockholm to london by walking
19:00:01 <AnMaster> it tells me to visit riga on the way
19:00:24 <AnMaster> the route is even crazier for Stockholm to Manchester
19:00:31 <fizzie> Deewiant: In retrospect, the "by car" instructions worked better for my "I just want some sort of time estimate for the train routes" use anyway.
19:00:51 <AnMaster> also it seems to be non-deterministic
19:01:00 <AnMaster> I get different results when I retry the same search
19:01:16 <pineapple> fizzie: where are you trying to get to?
19:01:26 -!- oerjan has quit (Quit: Later).
19:01:39 <fizzie> pineapple: Nowhere at the moment, we have the routes all planned up already. I was just wondering back then.
19:02:50 <fizzie> Deewiant: It's a bit sad that I could find no sensible train routing system that'd export me a .gpx file. I toyed a bit with OpenStreetMap editors, but it seemed non-trivial to extract long-distance train route geodata from that either, since the tracks aren't very comprehensively grouped into sets, just partially-somewhere-a-bit.
19:03:35 <fizzie> Deewiant: In the end I just took a generic .gpx editor thing that could display openstreetmap layers, and added some manual polylines over the railway lines that we're going to take. (I wanted a map of our route to show to relatives.)
19:03:38 <Deewiant> I might be able to sympathize if I knew what a .gpx was, but I guess it's some standard format for that.
19:04:00 <fizzie> Deewiant: It's a bit like Google's KML; a XML format for tracks, waypoints and such.
19:04:01 <AnMaster> Stockholm-Rostock by walking takes you through first Tallinn then Helsinki
19:05:33 <fizzie> AnMaster: I'm not sure how comprehensive their ferry schedules are. They might not include those cruise-line corporations, even though those have those "route trip" style tickets in addition to the cruises.
19:05:52 <fizzie> AnMaster: Certainly you can get directly from Stockholm to Helsinki, at the very least; most likely from Stockholm to Rostock too.
19:06:03 <AnMaster> fizzie, probably going by Åland
19:08:14 <alise> You are not able to access this service because Content Control is in place.
19:08:15 <alise> If you're 18 years or over, you can remove Content Control by contacting your mobile service provider's customer support
19:08:15 <alise> fucking piece of shit
19:08:46 <AnMaster> alise, no, I mean the blocked one
19:08:49 <alise> tmobile do the same but i unlocked it on that one but that one is all flutty right nw so i'm using this one
19:08:53 <alise> as is all other image hosts
19:09:01 <alise> this stick is PAID FOR
19:09:09 <alise> you have no right to fuck with the data I'M paying for, nanny
19:09:22 <fizzie> AnMaster: On the other hand, I 'm not sure you people need those ferries very much; you can just take one of those fancy-schmancy X2000 trains from Stockholm to Copenhagen, then another train from there to anywhere in Germany you'd like; that's what we're going to do, anyway.
19:09:42 <AnMaster> fizzie, mhm. X2000 aren't really fancy
19:09:52 <AnMaster> relatively slow compared to TGV and so on
19:09:53 <fizzie> AnMaster: With that sort of name, it almost has to be.
19:10:03 <Deewiant> alise: If not, you can use that
19:10:04 <AnMaster> fizzie, you never went on X2000 before?
19:10:20 <alise> http://upurs.us/image/11623.jpeg
19:10:22 <fizzie> AnMaster: I haven't been going round Sweden much.
19:10:22 <alise> A jpeg but who cares
19:10:25 <AnMaster> fizzie, they are tilting trains though, might feel a bit strange when taking curves thus
19:10:35 <alise> You can almost ignore the bloat behind the screen.
19:10:51 <AnMaster> alise, that is able to resume downloads easily enough
19:10:51 <fizzie> AnMaster: Yes, I think they're not much different from the local Pendolino ones.
19:11:12 <alise> Of course, I like BitTorrent.
19:11:17 <alise> But uTorrent is normally a lot less simple than that.
19:11:19 <fizzie> AnMaster: (Except that ours break down all the time.)
19:11:38 <AnMaster> fizzie, like last autumn or such
19:11:47 <alise> AnMaster: Example: http://blog.consultmirror.com/wp-content/uploads/2008/10/utorrent-general-view.png
19:11:50 <AnMaster> they had to take almost all out of service to replace the wheels
19:11:55 <AnMaster> due to some construction issue
19:11:57 <fizzie> "The Finnish Pendolinos have received a lot of bad publicity in Finland for their serious reliability issues, mostly caused by technical problems with their tilting system and couplers. The train did not manage to cope with the severe winter conditions."
19:13:06 <alise> It is fluff with no purpose; statistics pon for people with no IRC to waste time on.
19:14:32 <alise> ehirdOS would be fine here because it would be less than 690 megabytes.
19:14:51 <fizzie> alise: Did you miss my QNX demo disk suggestion?-)
19:15:07 <pikhq> Eh, just use debug.com.
19:15:23 <fizzie> alise: The "QNX is Cool!" demo! How could you resist!
19:15:33 <alise> AnMaster: Lateral thinking puzzle: You have no optical drive, no USB sticks, no floppies, no storage media whatsoever. You have a hard drive, Windows and the interwebs. How do you boot the Ubuntu LiveCD to install it to the spare partition you have?
19:15:42 <alise> I worked it out. :P
19:16:40 <alise> Wubi installs to a file in an NTFS partition, and does not boot the LiveCD.
19:16:50 <alise> (Yes, it literally /puts a Linux partition in a file on an NTFS partition/.)
19:17:05 <AnMaster> alise, well do that but to the installer instead
19:17:16 <AnMaster> then load the whole thing into ram (hope it fits!)
19:17:27 <alise> No, what you said makes no sense.
19:17:41 <AnMaster> alise, well, repartition and put the thing there
19:18:03 <alise> How? You only have NTDLR.
19:18:14 <alise> It doesn't get Linux.
19:18:15 <AnMaster> alise, well you can chainload with ntdlr
19:18:15 <alise> It can't boot Linux.
19:18:28 <alise> You only have Windows.
19:18:32 <alise> No LiveCD or anything to set this up.
19:18:38 <alise> You're on completely the wrong track.
19:18:40 <pikhq> Hmmm... Install a boot disk image that can read ISOs off of NTFS filesystems, chainload it from NTLDR, and have that boot into the LiveCD.
19:18:41 <AnMaster> alise, topology linux works kind of like wubi does
19:19:01 <AnMaster> I tried it many many years ago
19:19:18 <alise> I'll just tell you.
19:19:24 <fizzie> I have done the "Linux in ntldr boot menu" thing too; it involves just extracting a 512-byte boot sector into file, and adding one line to boot.ini; or at least that's the way it worked with win2k.
19:19:35 <AnMaster> fizzie, something like that yes
19:19:42 <fizzie> I was thinking you'd just run the installer in a VM, with the spare partition direct-mounted, but that doesn't solve the booting thing really, I guess.
19:19:42 <alise> Use http://unetbootin.sourceforge.net/. It fucks with NTDLR to boot Linux from an NTFS partition (part of one that is not a whole one) prepared from the .iso you want.
19:19:51 <alise> You then use this to install Ubuntu, then reboot Windows; it will undo the changes.
19:20:17 <alise> Also, I've never heard of topology linux.
19:20:21 <alise> Google shows nothing.
19:20:54 <AnMaster> alise, I guess topology linux is dead then
19:20:56 <pikhq> It was a Slackware-based distro that installed onto an NTFS partition, could boot either onto the straight system or via coLinux.
19:21:04 <AnMaster> pikhq, ah yes you heard of it then
19:21:06 <pikhq> Been ages since I've seen it, though.
19:21:34 <fizzie> I seem to recall there was a Slackware installation method which puts the linux system in a FAT filesystem, not in a single file; all files are different FAT files, and there's one huge hidden metadata file to keep ownership and inode and real-filename information in.
19:21:45 <fizzie> And of course loadlin; I used to use loadlin to boot my first Slackware.
19:21:55 <fizzie> (With an entry in a dos 6.22 boot menu to directly invoke loadlin.)
19:22:03 <fizzie> I suppose loadlin's no-go in modern Windowses.
19:22:14 <pikhq> fizzie: Yeah, DragonLinux IIRC...
19:22:16 <AnMaster> alise, anyway I think it is likely your way will fuck up the system so you can't recover from it
19:22:27 <pikhq> UMSDOS is no longer maintained, so that doesn't work. ;)
19:22:42 <fizzie> Ah, yes, "umsdos" was the name.
19:22:42 <alise> AnMaster: why, because you say so? It is a supported method of install
19:22:52 <fizzie> I was just googling for "udos", so that was pretty close.
19:22:58 <AnMaster> alise, what happens if the install fails when the disk is partly overwritten
19:23:30 <alise> AnMaster: Uh... you install onto a different partition.
19:23:38 <AnMaster> alise, how do you make the partition then?
19:23:53 <AnMaster> normal windows system is one huge partition
19:24:03 <alise> Yes, but this is already partitioned into two, conveniently.
19:24:12 <AnMaster> alise, ah that helps a lot indeed
19:24:19 <fizzie> AnMaster: The original problem statement did involve "the spare partition you have".
19:25:39 <Deewiant> You can use partitionmagic to repartition anyway, if you're feeling lucky
19:25:49 <AnMaster> Deewiant, when running from the same system!?
19:26:09 <Deewiant> Yes, I think it can install something to do it at boot
19:26:30 <AnMaster> would be replacing autochk entry I presume, like those "defrag on boot" tools do
19:26:31 <alise> It isn't from the same system
19:26:32 <alise> It reboots the system
19:26:41 <alise> and uses the tinkered bootloader to run the on-NTFS Linux
19:26:45 <AnMaster> alise, we were talking about repartitioning
19:27:01 <fizzie> PartitionMagic does (or did, anyway) that, yes; you queue the actions, it asks you to reboot, at boot-time it does the magic.
19:27:16 <alise> AnMaster: so do it from inside the ubuntu livecd
19:27:45 <AnMaster> alise, I wouldn't like that, if the file for the livecd image had to be moved
19:27:56 <fizzie> AnMaster: What would be scary would be to use some sort of alpha-quality parted NTFS resize patch. (I'm not sure if there is one yet, but I'm sure there will be at some point.)
19:28:18 <AnMaster> fizzie, you can use gparted to resize ntfs
19:28:33 <AnMaster> but I wouldn't want parted running from the partition (or even disk) being resized
19:28:36 <fizzie> Oh? http://www.gnu.org/software/parted/features.shtml was lying to me, then.
19:28:46 <AnMaster> fizzie, gparted invokes ntfsresize then parted
19:29:06 <AnMaster> fizzie, so it doesn't let parted do the whole work
19:29:23 <AnMaster> fizzie, gparted is in fact more than just a GUI frontend to parted
19:29:50 <alise> AnMaster: just dont run anything new
19:29:54 <alise> and it won't need to touch the disk
19:30:08 <AnMaster> alise, well, unlikely, any data moving will push things out of disk cache
19:30:18 <AnMaster> due to the large amounts of data being moved
19:30:26 <alise> maybe unetbootin copies everything to ram anyway
19:30:29 <AnMaster> alise, so if I did it, I would do it from a ram disk indeed
19:30:30 <alise> for overwriting windows
19:30:58 <AnMaster> alise, and what if the install failed if you *are* overwriting linux. Yeah you are into deep problems, that's my point
19:31:45 <alise> *overwriting windows
19:32:21 <AnMaster> it is easy to end up with an unbootable system and no usb drive or cd to recover it from
19:32:26 <alise> Windows 7 isn't too bad.
19:32:31 <alise> Ubuntu is nicer though.
19:35:01 <AnMaster> alise, are you going to dual boot?
19:36:55 <alise> Yes, just in case.
19:37:03 <alise> And for lessriskiness of installation.
19:53:31 <AnMaster> pikhq, even so, 690 mb. would be extreme
19:53:53 <alise> you didn't mean the iso
19:54:04 <alise> no 2gb for netbooks
19:54:35 <AnMaster> alise, so how large is your harddrive/SSD
19:54:36 <alise> it's just the minimum you see
19:54:43 <alise> e.g. the dell mini 9 comes with that by default, iirc
19:54:43 <alise> it's a 250gb hd divided in two partitions, anyway
19:54:47 <alise> WINDOWS and Data, which has hard drive recovery stuff by default
19:54:51 <alise> it's a hard drive not an ssd
19:54:59 <alise> it cost 497, not 1,500 :-)
19:55:29 -!- Gracenotes has quit (Ping timeout: 246 seconds).
19:59:39 <pikhq> alise: Could you put that in real money?
20:01:05 <alise> 9547252537776.06 ZW$
20:01:16 <alise> Hmm, that may be the pre-reset Zimbabwean dollar.
20:01:30 <pikhq> That's a few orders of magnitude too small.
20:01:43 <alise> Then it's the post-reset one.
20:01:50 <alise> (Where $1 became old $1bn)
20:02:11 <alise> the use of the dollar as an official currency was effectively abandoned on 12 April 2009 as a result of the Reserve Bank of Zimbabwe legalising the use of foreign currencies for transactions in January 2009
20:02:13 -!- cheater2 has quit (Read error: Connection reset by peer).
20:02:26 <pikhq> The USD isn't real currency. I was just mocking your country's lack of Euroness.
20:03:17 <alise> Wait, it was $10bn.
20:03:25 <alise> Yeah; Sweden needs to get on the Euro bandwagon.
20:03:29 <alise> What, you meant USD?!?!?!?!
20:03:50 <alise> What, you meant UK?!?!?!?!
20:04:33 <alise> Maybe I'll go to Norway, they have the Euro :P
20:04:59 -!- cheater2 has joined.
20:05:28 <alise> But they also have... shudder.. Lutefisk.
20:09:09 <pikhq> Yes, they have caustic food.
20:11:15 * alise notes that there don't seem to be any pirate copies of mathematica for linux on the tubes
20:11:29 <alise> Well, none of 7 anyway.
20:11:34 -!- cheater2 has quit (Ping timeout: 264 seconds).
20:16:43 <alise> Admittedly I don't have access to any actually decent torrent trackers.
20:16:53 <alise> Mathematica 5 2 Win Linux Mac software other operating systems applications windows
20:17:47 <alise> >200kb download speed!
20:18:19 <alise> And back down again :P
20:19:15 <Deewiant> alise: Are you Google-deficient? "mathematica 7 linux torrent", top link.
20:20:38 <alise> I've never before had success using Google to find torrents.
20:21:03 <alise> Incidentally, Mathematica on OS X expands to a 4GB .app :x
20:22:07 <AnMaster> I just got back and read the line: "<alise> Mathematica porn!"
20:23:02 <AnMaster> alise, tpb has mathematica 7 for linux iirc
20:23:21 <AnMaster> by pure coincidence, so have I
20:23:30 <AnMaster> *completely* unrelated of course
20:24:23 -!- cheater2 has joined.
20:26:11 <alise> Does it have any Linux-related shittiness?
20:26:19 <fax> alise why the fuck would you steal mathematica
20:26:33 <alise> Oh no, not an idiotic copyright defender.
20:26:40 <fax> you're the idiot
20:26:53 <alise> Firstly, copyright infringement is - apart from being an uncrime invented by idiots - not theft even if you support it.
20:27:00 <alise> Economically, nonsense. Morally, nonsense.
20:27:07 <fax> firsly: shut up, you're an idiot
20:27:20 <Deewiant> I like how you both called each other idiots without even knowing what you were actually going to say
20:27:20 <alise> If you continue calling me an idiot without basis I will simply put you on /ignore.
20:27:40 <fax> good then you might stop telling me I suck
20:27:53 <alise> Deewiant: Well, I know he's a Wolfram fanboy and calling copyright infringement stealing along with the brash wording of "why the fuck would you steal mathematica" gave me a pretty good predictor
20:28:03 <alise> fax: I haven't done that but if you want to distort something I've said that way I won't stop you
20:28:19 <fax> alise, you're such an idiot you can't even remember something that happened this morning
20:29:43 <alise> just grepped the logs, I never said you sucked
20:30:07 <fax> okay well you could also learn to spell
20:30:32 <fax> 07:00:58 <fax> I don't know
20:30:32 <fax> 07:01:17 <alise> :|
20:30:32 <fax> 07:01:20 <alise> u suk
20:31:01 <fax> and it's rude to be all impatient like "I'm waiting" while someones trying to think
20:31:23 <alise> wow you're pissed off because I wasn't being totally serious all the time?
20:31:30 <alise> it's not like I didn't gratuitously adorn things with emoticons either
20:31:32 -!- Slereah has quit (Ping timeout: 246 seconds).
20:31:37 <alise> you're way too hypersensitive
20:32:27 <fax> alise: redunant
20:36:12 -!- Slereah has joined.
20:38:00 -!- olsner_ has quit (Quit: olsner_).
20:40:22 <AnMaster> <alise> Does it have any Linux-related shittiness? <-- some
20:40:30 <AnMaster> alise, if you by that means "buggy"
20:40:40 <AnMaster> you need to disable the java stuff or it bogs down the whole system
20:40:45 <AnMaster> and you need to get some replacement files
20:40:54 <AnMaster> to fix other causes of bogging down the whole system
20:41:01 <AnMaster> the java stuff is needed for the built in help stuff
20:42:07 <fax> alise be nice to me :/
20:42:13 <Deewiant> I haven't run into any system-bogging, and the help has worked too :-P
20:42:32 <AnMaster> Deewiant, check number of wakeups with powertop while mathematica is running
20:42:38 <AnMaster> it is caused around 5000 per seconds
20:42:54 <Deewiant> That's not what I'd call "bogging down the whole system"
20:42:57 <AnMaster> Deewiant, on a laptop that just doesn't work
20:43:08 <AnMaster> Deewiant, well true, that is what the other replacement files fix
20:43:09 <Deewiant> It's using excessive amounts of power, but that's it
20:43:27 <Deewiant> Yeah, see, the 100% CPU usage I haven't run into :-P
20:43:29 -!- sebbu2 has joined.
20:43:52 <alise> fax: so be nice to me
20:44:10 <alise> fax: see, this is /not/ the way you ask me to be nice to you
20:44:15 <AnMaster> fax, why do you think alise is an idiot for pirating mathematica
20:44:26 <alise> AnMaster: because he's a wolfram fanboy and calls copyright infringement "stealing"
20:44:27 <fax> AnMaster, I just called him an idiot because he said that to me
20:44:30 <AnMaster> because this is ridiculous from both of you
20:44:33 <fax> alise you don't know anything
20:44:35 <alise> <3 Wolfram + Piracy is evil = you monster
20:44:42 <fax> seriouly just stop guessing
20:44:43 <AnMaster> <fax> alise why the fuck would you steal mathematica
20:44:43 <AnMaster> <alise> Oh no, not an idiotic copyright defender.
20:44:43 -!- sebbu has quit (Ping timeout: 276 seconds).
20:44:43 -!- sebbu2 has changed nick to sebbu.
20:44:53 <Deewiant> Yeah, that's what I commented on earlier
20:44:56 <AnMaster> fax, please explain what you meant with your first line there
20:44:57 <fax> AnMaster: yeah I just explained it
20:45:19 <AnMaster> fax, you didn't explain "alise why the fuck would you steal mathematica"
20:45:26 <fax> what's to explain
20:45:42 <AnMaster> I can think of lots of reason to pirate mathematica
20:45:49 <AnMaster> so what is your reasons not to
20:46:32 <AnMaster> oh and wolfram is somwhat insane. He needs to get medical help before his ego kills him
20:48:45 <fax> http://upload.wikimedia.org/wikipedia/commons/0/06/Pentatope_of_70_spheres_animation_original.gif
20:54:00 -!- jcp has joined.
20:54:08 <alise> I'm going to boot into Ubuntu now.
20:54:12 -!- alise has quit.
21:00:26 <augur> i'd boot your ubu- oh. :|
21:03:02 -!- songhead95 has joined.
21:03:36 -!- songhead95 has quit (Remote host closed the connection).
21:04:18 -!- songhead95 has joined.
21:06:44 -!- MigoMipo has quit (Remote host closed the connection).
21:12:14 <fizzie> Deewiant: I don't suppose you happen to be on T-76.5753, incidentally?
21:13:59 <fizzie> Admittedly I had no reason to suspect you were, except that it would've been a Fancy Coincidence.
21:15:13 <fizzie> There's the © and ® characters in the "special characters" key-list on the N900, but no ™ :/ .. maybe because the first two are in latin-1 and that one is not, but that's not a good reason.
21:33:02 -!- MigoMipo has joined.
21:40:49 <ais523> hmm, worrying that alise hasn't come back
21:52:31 <fizzie> ais523: It's the Ubuntu, it's razzling-dazzling multimedia interface has locked him into a trance.
21:53:02 <fizzie> When you gaze into GNOME, the gnome also gazes at you.
21:53:12 <Deewiant> fizzie: Your apostrophes are extraneous again
21:53:26 <fizzie> Deewiant: I am being very bad with them today for some reason.
21:53:49 <fizzie> Deewiant: I shall try to avoid all contractions, maybe that will help.
21:54:20 <Deewiant> If you avoid possessives as well you should be fine.
22:18:26 -!- alise has joined.
22:20:30 <alise> Who knew that you needed to do a forced lazy unmount of the partition the system is running on to install Ubuntu?
22:23:36 <fizzie> It must be part of the built-in intelligence test, to see if you are Worthy of Ubuntu.
22:25:21 <ais523> I was wondering why you took so long to come back
22:25:27 <alise> ais523: umount -f -l (a mount from the partition the system is running on)
22:25:37 <ais523> hmm, I didn't need to do that to install
22:25:53 <ais523> I don't think I used the command line at all, come to think of it
22:26:02 <ais523> except afterwards, to compile the wifi card driver
22:26:25 <alise> Well, I was running the LiveCD from an NTFS partition.
22:26:30 <alise> And /cdrom was C:\ whilst / was a subset of C:\.
22:26:43 <alise> I had to force-unmount /cdrom (it refused to do so because the device was being used) and then remount it again before it got to GRUB.
22:27:30 <alise> because the Toshiba Satellite, as you know, has no optical drive; and I didn't have any USB sticks handy
22:27:45 <ais523> didn't realise the lack of a USB stick
22:28:05 <fizzie> Yes, don't you get USB sticks with breakfast cereal nowadays?
22:28:27 * alise installs ttf-droid to change the UI font
22:28:32 <alise> I'm a bit bored of DejaVu Sans.
22:28:45 <fizzie> Deewiant: What sort of breakfast cereal do you buy?
22:28:48 <alise> By "I'm a bit bored of", I mean "I think that a really boring font is".
22:28:59 <ais523> I was going to say "what's wrong with DejaVu Sans", but boringness is a fine reason
22:29:01 <fizzie> Is ttf-droid the Android font?
22:29:02 <Deewiant> fizzie: I don't. Maybe that's the problem.
22:29:17 <ais523> I eat oats for breakfast, but persuade someone else to buy them
22:29:25 <alise> DejaVu Sans is a bit too wide especially.
22:29:36 <alise> It's, if nothing else, not boring.
22:29:44 <alise> ais523: what; raw oats?
22:30:09 <alise> lactose intolerant?
22:30:12 <ais523> I'm not vegan, although my breakfast is by chance
22:30:16 <ais523> it's lactose intolerance
22:30:21 <fizzie> I have the Android monospaced font on the N900 in use in the terminal; it's a lot nicer to the Nokia font. Can't really say whether I prefer it over DejaVu Sans Mono, but then again, I'm pretty boring too.
22:30:37 <ais523> also, I can have a bit of lactose per week, but not too much
22:30:39 <alise> 3% [1 ttf-droid 94119/2,771kB 3%] // and it freezes...
22:30:46 <ais523> besides, I've been drinking soya milk for decades, now
22:31:11 <ais523> and due to the way acquired tastes work, I now can't stand to drink any other sort of milk
22:33:42 <alise> "We have commissioned a new font to be developed both for the logos of Ubuntu and Canonical, and for use in the interface. The font will be called Ubuntu, and will be a modern humanist font that is optimised for screen legibility."
22:33:45 <alise> Let's hope that's nice, then.
22:36:36 <pineapple> alise: is this your first time using linux?
22:36:45 <alise> Not by a long shot.
22:36:58 <alise> First time installing it on this /machine/, yes...
22:37:06 <alise> First time installing it without an optical drive or USB stick... yeah.
22:38:04 <alise> I've used Debian, Arch, almost Slackware (its installer hates me; or more probably my systems), even tried getting Mastodon to work... I'd say I've tried stali, but it isn't even out yet.
22:38:14 <alise> I also tried Mandriva when I was young and naive.
22:38:22 <alise> I've also used FreeBSD.
22:38:39 * alise uses Oxford University as his Ubuntu mirror
22:38:48 <alise> At least it works.
22:38:57 <alise> Albeit rather terribly slowly.
22:39:02 <fizzie> Slackware (or was that Debian) had a nice, standard "install without any boot media" officially-supported installation strategy, which (I think) involved dd'ing the ISO image on the partition you were going to use for swap, then booting the installer off that (kernel with loadlin, I think; this was for from-DOS installs), and activating swap only after the installation was done.
22:39:19 <alise> pineapple: Oh, I've also used Plan 9 and researched its architecture rather extensively.
22:39:28 <pikhq> That is still supported in Slackware.
22:39:38 <pikhq> And I think the Debian install manual describes how to do the same.
22:39:47 <fizzie> pikhq: Can you still install Slackware from a huge pile of floppies?-)
22:40:00 <pikhq> fizzie: No, they stopped that a couple releases ago.
22:40:10 <alise> Stop using freaky smilies man
22:40:44 <fizzie> Admittedly floppy distributions were getting a bit ridiculous when the number of floppies goes >20 or so.
22:41:41 <pikhq> I think they had a release of that.
22:42:26 <fizzie> Win95 OSR 2.1 was a 23-floppy release, it seems. (I have forgotten the exact count.)
22:42:57 <pikhq> I actually installed it from floppy once.
22:43:07 <alise> "I know. I was THERE."
22:43:14 <alise> I wonder why it is that none of my installations ever go smoothly?
22:45:16 <alise> ais523: what's the best ubuntu mirror :x
22:45:24 <alise> i need one insanely fast because my connection sucks.
22:45:33 <ais523> I use the one in Sweden when there's heavy load
22:45:58 <ais523> atm, though, I think I'm on the default UK one
22:46:01 <ais523> which should be on the menus
22:46:54 * alise tries the swedish kernel.org
22:52:25 <pineapple> mirrorservice.org is usually reliable for me
22:54:06 -!- Gracenotes has joined.
22:55:35 -!- alise has quit (Quit: Leaving).
22:56:42 -!- alise has joined.
22:56:58 -!- alise has quit (Client Quit).
23:01:44 -!- alise_ has joined.
23:03:42 <augur> What's the fanclub for Black Adder called?
23:03:44 <Ilari> Soya "milk". Milk comes from mammals. Soya isn't one. :->
23:04:23 <ais523> Ilari: well, soya milk's the usual name
23:04:26 <alise_> Ilari: Milk snobbery? That is a new one.
23:05:52 <fax> milk comes from coconuts
23:08:18 <Ilari> There are lots of other products that are called by incorrect names. Like various "Creams" (that are really mostly water, soft fat and additives).
23:08:34 <pikhq> 豆乳 comes from beans!
23:09:37 <alise_> Ilari: I'd say something about prescriptivism, but -
23:10:16 <Ilari> Then there are downright oxymorons like "Fat-free mayonnaise".
23:12:18 -!- oklopol has joined.
23:12:59 <oklopol> i was watching a priest dance an erotic dance
23:16:19 <fax> oklopol -- do you know chevally warning
23:16:46 <fax> it's a good theorm :D
23:16:49 <fax> number theory
23:17:02 <fax> oklopol I cannot solve this OR thing :/
23:17:29 <oklopol> well there are a few concepts you don't know that it depends on
23:18:08 <oklopol> i mean really basic concepts, just that you might not realize they're important
23:18:30 <Ilari> Oh, and then there is some misleading names like "milk drink". That's not Milk (something has been done to it so it can't be sold as milk). Oh and don't search for "soya milk" either, its "soya drink".
23:21:03 <Ilari> Oh, and those various "Creams" fortunately can't be sold as creams. :-)
23:23:53 <Ilari> Wonder what milk of Bosavi woolly rat would taste like... :-)
23:24:46 <oklopol> the idea was you do U=V OR U=W by either making U match with V or W, for this you'll need to have ...U... = ...V...W..., and then do some magic to make U only hit exactly one of those two. for this you'll need to at least be able to build primitive words out of U's, V's and W's
23:26:16 <oklopol> ofc i can give more concrete hints as well, or just show you the whole proof; there's a lot more interesting stuff to prove where this came from.... :P
23:27:55 <oklopol> (if anyone else is interested, the context is to represent the OR of two equations on words as one)
23:30:03 -!- coppro has joined.
23:30:28 -!- oklokok has joined.
23:31:10 <fax> oklopol, that doesn't make sense :|
23:31:19 <fax> if U only hits one of them what happens to the rest
23:31:39 -!- alise has joined.
23:31:58 <alise> Good mrr'nng America.
23:32:12 <oklokok> who cares? we know it can't hit anything but either of them, if it can hit one of them, the OR is true, if it can't hit either, then it can't hit anything, and the OR is false
23:32:24 -!- alise_ has quit (Ping timeout: 252 seconds).
23:32:57 <fax> for ...U... = ...V...W...
23:33:12 <fax> the both sides have to be the same length
23:33:25 <fax> so how can we have ... = ...V... OR ... = ...W...
23:33:26 <oklokok> you have to find such values for ... that U can only be on top of either V or W, then it can be on one of them iff either of the equations is solvable, we just have to make sure it can't be on top of anything else
23:33:54 <oklokok> err you can just have some new variables in ... that fill the rest
23:34:00 <alise> coppro: The major changes are in the GNOME version though.
23:34:03 -!- oklopol has quit (Ping timeout: 252 seconds).
23:34:25 <coppro> I don't care, I'm happy the upgrade was smooth
23:34:43 <oklokok> like zUz' = ...V...W..., not that i'm saying the left side can actually be that simple
23:35:24 <oklokok> U can be anything, so there's no way to guarantee U can't be on top of say just the left half of V
23:36:06 <oklokok> oh well those should be Z and Z'
23:36:19 <oklokok> i can't learn this convention it seems
23:38:01 <oklokok> anyway i find this trivial because i've seen the solution, but it may have been an open problem at some point, don't really know
23:39:41 <alise> ais523: Isn't it interesting that one of the best programming /environments/, Mathematica, is paired with one of the worst programming /languages/?
23:40:01 <ais523> alise: the environment is tained by the language, I think
23:40:07 <ais523> also, I hate the way it does line breaks
23:40:22 <ais523> as in, mathematica the IDE suffers from being written in mathematica the lang
23:40:57 <oklokok> the length of the RHS of the solution i have is 38. so you're not going to find it by any sort of brute force
23:41:04 <alise> mm... but if you don't run into the shittiness of the language, it's very nice
23:41:13 <fax> oklokok haha I'm not going to find it at all
23:41:40 <alise> ais523: also I think automatic formatting is obviously good but mathematica messes it up
23:41:46 <fax> oklokok I couldn't even find the diophantine representation of complement of powers of 2
23:41:54 <fax> that one is SO EASY but I didn't get it :|
23:41:58 <ais523> alise: ok, I'm happy with that opinion
23:43:06 <oklokok> like an equation where the solutions, restricted to X, are exactly N - {2^n | n \in N}
23:43:43 <fax> here's the set {a} of composites: a = xy
23:43:52 <fax> well that's wrong actually
23:43:54 <fax> let me correct it
23:43:59 <fax> here's the set {a} of composites: a = (x+2)(y+2)
23:44:06 <fax> since it's in natural numbers
23:44:25 <oklokok> right so solutions restricted to a are exactly composites
23:44:44 <fax> all positive values of a are composites
23:44:59 <fax> the general idea is D(a,x1,x2,...,xn) = 0
23:45:10 <fax> where D is some polynomial iwht integer coefficents
23:45:20 <oklokok> yeah, i just needed the definition of "diophantine representation"
23:46:24 <oklokok> so umm is it "x = (y + 3)(z + 1)"?
23:46:32 <oklokok> you need to have some factor that's more than 2
23:46:37 <oklokok> and then some other factors
23:47:21 <augur> so who's watched Earth: Final Conflict?
23:52:26 <fax> oklopol, the answer is (2y + 3)(z + 1)
23:53:04 <oklokok> was just about to get paper
23:53:09 <fax> anyway the complement of this set (powers of two) is diophantine as well
23:53:17 <fax> but that's a hard theorem (takes a whole chapter)
23:53:48 <fax> the method is great.. he encodes a sequence (fibonacci sequence) and since that has roughly exponential growth, that proves that exponentitation can be defined too :D
23:54:04 <fax> the sequence they actually use (to make the proof more direct) isn't fibs though
23:54:32 <fax> should have said asymptotic rather than roughly
23:54:35 <oklokok> for "has odd factor" you just write x = odd*any, the other direction doesn't have a simple explanation with existential quantification
23:55:09 <fax> (complement isn't always diophantine, compare with the analogue of recursive languages...:))
23:55:22 <fax> but in the case of exponentiation it is
23:55:41 <fax> and proving that exponentiation was diophantine was the last piece needed to complete the proof (of hilberts 10th)
23:55:49 <oklokok> hmm well not sure about of course
23:57:18 <oklokok> right i've actually seen that
23:57:37 <fax> seen what/?
23:59:00 <oklokok> exponentiation, but i just realized i haven't
23:59:39 <fax> it's a pretty tough chapter, I haven't really worked through it yet just understood the general idea