00:29:28 -!- sleffy has joined. 00:47:03 -!- augur has quit (Remote host closed the connection). 01:04:33 -!- moony has joined. 01:12:48 -!- moonythedwarf has joined. 01:15:15 -!- moony has quit (Ping timeout: 256 seconds). 01:23:59 -!- hppavilion[1] has joined. 01:27:48 -!- trout has changed nick to function. 01:50:27 -!- oerjan has quit (Quit: Nite). 01:55:33 -!- sleffy has quit (Ping timeout: 264 seconds). 02:18:42 -!- jaboja has joined. 02:36:11 -!- function has quit (Quit: Found 1 in /dev/zero). 02:55:59 -!- jaboja has quit (Ping timeout: 248 seconds). 03:50:25 -!- hppavilion[1] has quit (Ping timeout: 248 seconds). 04:04:45 -!- variable has joined. 04:47:57 GURPS has "alternative abilities" where you can switch between them, because there are different modes of one thing. I saw once also mention of "alternating abilities", where they must be used in order, and then after the last one is used, the first one becomes available again. Someone said it is silly, but I think it can be interesting if the costs, time to use, and other requirements are significant! 04:48:01 What is your opinion of this? 04:57:27 -!- heroux has quit (Ping timeout: 240 seconds). 05:00:05 -!- heroux has joined. 05:03:13 -!- sleffy has joined. 05:23:21 -!- variable has quit (Quit: /dev/null is full). 05:58:07 -!- variable has joined. 06:58:23 -!- doesthiswork has quit (Quit: Leaving.). 07:10:57 -!- sdfgsdfg has joined. 07:14:13 -!- sdfgsdfg has quit (Remote host closed the connection). 07:14:31 -!- sdfgsdfg has joined. 07:59:21 -!- variable has quit (Quit: /dev/null is full). 08:00:46 -!- variable has joined. 08:00:54 -!- variable has quit (Client Quit). 08:01:24 -!- variable has joined. 08:01:40 -!- variable has quit (Client Quit). 08:14:26 -!- sleffy has quit (Ping timeout: 252 seconds). 08:20:59 -!- sleffy has joined. 08:45:46 -!- ais523 has joined. 08:48:31 -!- moonythedwarf has quit (Ping timeout: 248 seconds). 09:02:27 -!- sleffy has quit (Ping timeout: 240 seconds). 09:09:39 Does the infinite sum of x/(2^x) converge? 09:16:51 Actually, I care about (x/2)/(2^x) but I think if one converges then so will the other 09:18:22 I think they converge at 1 and 0.5 respectively but don't know how to prove it 09:18:51 2 and 1, not 1 and 0.5 09:51:59 -!- erkin has joined. 10:22:16 Taneb: x/(2^x) obviously converges because past a certain point, each element of the sequence is smaller than 1/(1.5^x) (exponential beats linear) 10:22:28 although that sort of argument doesn't tell you what number it converges at 10:40:44 -!- ais523 has quit (Ping timeout: 252 seconds). 10:45:48 -!- danieljabailey has quit (Ping timeout: 272 seconds). 10:46:37 Taneb: for the former, you can show that sum[i=0 to n] i/2^i = 2 - (n+2)/2^n 10:48:16 -!- danieljabailey has joined. 10:51:03 there's also the cute idea of rewriting sum[i=0 to inf] i/2^i = sum[i=0 to inf] sum[j=1 to i] 1/2^i as sum[j=1 to inf] sum[i=j to inf] 1/2^i = sum[j=1 to inf] 2/2^j = 2. 10:52:21 int-e, that's pretty neat 10:52:27 Thank you 10:53:54 And then there's generating functions: x/(1-x)^2 = x(1/(1-x))' = x(1+x+x^2+...+x^i+...)' = x(1 + 2x + 3x^2 + ... + ix^(i-1)) = x + 2x^2 + ... + ix^i + ..., and x/(1-x)^2 =2 for x = 1/2. 10:54:23 (I should probably reverse those equations...) 10:56:19 And I should perhaps note that I'm building on top of the knowledge that the series is (absolutely) convergent, which justifies reordering terms, and replacing 1+x+x^2+... by 1/(1-x). 11:00:21 -!- danieljabailey has quit (Ping timeout: 264 seconds). 11:03:33 -!- danieljabailey has joined. 11:48:36 -!- xkapastel has quit (Quit: Connection closed for inactivity). 12:01:02 -!- danieljabailey has quit (Ping timeout: 252 seconds). 12:03:31 -!- danieljabailey has joined. 12:12:40 -!- sprocklem has joined. 12:21:24 -!- sdfgsdf has joined. 12:22:00 -!- sdfgsdfg has quit (Read error: Connection reset by peer). 12:26:26 -!- sdfgsdf has quit (Ping timeout: 260 seconds). 12:39:29 -!- sdfgsdfg has joined. 12:43:54 -!- erkin has quit (Read error: Connection reset by peer). 12:44:45 -!- sdfgsdfg has quit (Ping timeout: 264 seconds). 12:45:23 -!- erkin has joined. 12:51:31 -!- ais523 has joined. 12:59:05 -!- FreeFull has quit. 13:42:43 -!- jaboja has joined. 14:00:29 -!- doesthiswork has joined. 14:29:04 -!- oerjan has joined. 14:38:09 -!- sprocklem has quit (Ping timeout: 264 seconds). 14:48:35 -!- moony has joined. 15:18:40 -!- boily has joined. 15:19:15 afternoily 15:23:51 BØN MATIRJAN! 15:24:18 * boily is older today! ^^ 15:24:34 -!- mroman has joined. 15:24:51 Suppose there's a program H1 that can answer whether a program P stops. 15:25:09 Then suppose there exists a program Q = IF H1(Q) THEN loop(); ELSE stop(); 15:25:19 Thus H1 would get the answer wrong for Q 15:26:00 Thus we know that H1 gets the answer incorrect for Q 15:26:32 Assume that H1 will answer with "YES" for Q 15:26:51 This allows us to construt an H2(P) = IF P = Q THEN "NO" ELSE H1(P) 15:26:59 which would get the answer correct for Q 15:28:07 or similar if H1 answers with "NO" 15:29:40 in the "NO" case we could even tell this because then Q actually stops in a finite amount of time 15:30:55 if Q exists we can create an H2 that will detect Q and answer correspondingly or else invoke H1 15:31:38 you could construct a Q2 = IF H2(Q) THEN loop(); ELSE STOP(); 15:31:50 at which point you can create an H3 that detects this case as well 15:31:51 and so on. 15:32:20 but you can do this more generically 15:32:45 for any Hx it can detect whether it is invoked during execution of the program 15:33:06 thus you don't need H1, H2, H3, H4... but only an Hx for the generic case. 15:33:14 boily: happy birthday! 15:33:42 thus this Hx should get the answer correct for all Qx 15:33:55 -!- laerling has joined. 15:35:02 which would mean that the existence of a Q does not mean that no such H can exist. 15:35:31 which makes me even more convinced that the halting problem does not exist. 15:36:11 -!- erkin has quit (Quit: Ouch! Got SIGABRT, dying...). 15:36:23 besides what I've already mentioned that proving H can't exist also proves Q can't exist which means that neither H can exist nor can a program exist that would break H 15:36:55 two problems there 15:37:06 first, how do you compare programs for equality? 15:37:13 second, and more importantly, programs are finite 15:37:24 your hypothetical Hx is infinite; you can't just take the limit and say it exists 15:37:29 mroman: the source code of Q is a function of the source code of H. didn't you get this explained the other day? 15:39:17 the point is, there is indeed no Q that works to disprove all Hs, but for every H there is a Q that disproves it. 15:40:06 -!- jaboja has quit (Ping timeout: 260 seconds). 15:41:59 compare programs? Reduce them to some normal form I guess. 15:42:22 which we can do if the program stops in a finite amount of time 15:42:55 or compare source codes 15:42:57 that's not even true 15:43:00 or whatever representation you have for programs 15:43:13 and comparing representation works, but there are infinitely many possible representations of equivalent programs 15:43:29 I guess that doesn't make things any worse 15:43:35 because your Hx still needs to be infinite anyway 15:44:06 if two LC terms are semantically the same they'd evaluate to the same final form eventually 15:44:18 otherwise you'd have a non-deterministic eval 15:44:21 mroman: not if neither halts 15:44:32 yes 15:44:32 and we definitely can't assume that they halt here 15:44:41 but H would halt. 15:44:44 any H would halt 15:44:53 but we're talking about Q 15:44:59 you're comparing programs to Q, which may not halt 15:46:09 also even in LC, you can have two programs which halt on all inputs and give the same results on all inputs 15:46:13 but don't reduce to the same normal form 15:46:16 well then you'd have to proof first that there's a program R that is semantically identical to Q but which can't be reduced to Q in a finite amount of time. 15:46:20 because you need the input in order to reduce them 15:46:41 you can't compare programs by semantics 15:46:44 as in proof that Q is not unique under reduction 15:46:48 no 15:46:51 or whatever that is called in CS terms. 15:46:59 you have it backward 15:47:08 in order for your argument to be valid, you need a proof that Q *is* unique under reduction 15:47:16 which you won't find 15:47:47 there might be a R = IF H(P) == !true THEN ... 15:47:49 or whatever 15:47:57 but that R would be reducable to Q in a finite amount of time 15:48:13 actually wait consider this 15:48:45 R(P) = if (some condition on P) then Q(P) else Q(P) 15:48:47 this doesn't reduce to Q 15:48:50 until you provide an input P 15:49:03 inputs are cheating. 15:49:06 not at all 15:49:10 all these programs have inputs 15:49:21 they don't have meaning without inputs 15:49:40 try formalizing it 15:51:16 I mean ultimately 15:51:34 the input is known before H is invoked 15:51:40 since H only takes a program 15:51:44 not a program PLUS input 15:51:49 -!- garit has joined. 15:51:49 -!- garit has quit (Changing host). 15:51:49 -!- garit has joined. 15:51:54 that's not how it's usually specified 15:52:03 I know. 15:52:05 the halting problem is to determine if a given program halts *on a given input* 15:52:08 but I don't care about the I/O case. 15:52:26 I want the non I/O case :) 15:52:35 passing parameters counts as I/O 15:52:44 you're thinking at too high a level here 15:53:13 H can only somehow measure if P stops or not. 15:53:20 I mean 15:53:29 without communicating with P in any other way 15:53:32 you can look at the input as a program+input combination 15:53:35 H doesn't even get the output of P 15:53:40 and then you "don't have I/O" 15:53:46 turing machines don't have output 15:53:49 besides ACCEPT/REJECT 15:53:54 it's not actually a big difference if you disallow I/O there, it can be hardcoded. 15:53:57 again, you're thinking at too high a level 15:54:06 I/O is not a concept in turing machines 15:54:21 there are modified Turing Machine definitions that do have I/O 15:54:23 normally using a separate tape 15:54:29 yeah 15:54:30 but the original definition doesn't 15:54:41 I accept the halting problem in the I/O case. 15:54:44 That makes sense. 15:54:49 mroman: there is no "I/O case" though 15:54:52 ultimately 15:55:29 Q = IF H(P) ... is inherently an I/O bound action. 15:55:42 because it calls a foreign program that is not within Q 15:55:45 no 15:55:50 that's not how turing machines work 15:55:55 H is embedded in Q 15:56:03 it's not "foreign" 15:56:04 there is no I/O 15:56:12 it's like a subroutine 15:56:35 mroman: i told you, the source code of Q contains the source code of H. 15:56:48 it _is_ within. 15:57:48 but then Q = IF H(Q) doesn't work 15:57:59 because you're only passing Q 15:58:00 not H. 15:58:04 of course it does, you use a quining technique. 15:58:07 ^ 15:58:18 which isn't mentioned in the proof anywhere 15:58:23 because 15:58:35 H is a machine which takes an encoded representation of a Turing machine, right? 15:58:42 like, the input to H is source code 15:58:44 mroman: you may have read a bad version of the proof. 15:58:50 you just assume that you can embed H like that. 15:59:06 mroman: the fact that you can embed H like that is well established 15:59:13 turing machines are universal 15:59:18 of course, i cannot say clearly that i've read it, i just consider it obvious since i _do_ know how to write a quine. 15:59:29 I know how to write a quine too. 15:59:48 (\x.xx)(\x.xx) being the most obvious one 15:59:53 mroman: so the way it works from a technical point of view is 16:00:29 H is a turing machine whose input is a description of turing machine 16:00:32 (that is not a quine) 16:00:46 the description doesn't need to be specified specifically, because we're trying to prove H doesn't exist 16:01:07 so we can assume that there is some way to go from (Turing Machines) -> (input format for H) 16:01:43 Q embeds H as a subroutine 16:01:58 (it's not too hard to show how to do this, though I can explain it more if you need) 16:02:25 so now we apply our mapping to Q, and we get Q in the input format to H 16:02:28 then we feed this to Q 16:02:34 which in turn passes it on to H 16:03:41 -!- laerling has quit (Quit: Leaving). 16:05:46 I mean you could have a turing machine with a Quine operator right? 16:05:54 that shouldn't violate the laws of turing machines. 16:06:09 presumably. but they can already do quines so why bothere 16:06:13 *-e 16:06:24 so you could write a program IF H(myself) THEN loop(); else halt(); 16:06:39 where myself is a builtin that is replaced with the source code of the program itself. 16:07:24 then to be more specific... the program would look like `H(p) := ....; Main := IF H(myself) THEN loop(); ELSE halt();` 16:08:02 hm 16:08:18 it's officially christmas in norway, time to open the first nutella ball... 16:08:19 Not quite, a program can't quine itself 16:08:29 because it doesn't have a copy of its source code 16:08:40 ... 16:08:41 at least not in the general case 16:08:54 quines operate at a meta level 16:08:57 oerjan: what day is it celebrated? and what time does it start? I assume if it's officially Christmas now, it has been for several hours 16:09:07 today is Christmas Eve in the UK and insanely busy in all the shops as a consequences 16:09:10 *consequence 16:09:37 hmm, maybe I should write a better BuzzFizz interp so that I can look into whether it can write a quine 16:09:44 I'd be surprised if it couldn't, but it seems really painful 16:10:03 ais523: 17 on Dec 24 is when the church bells start ringing 16:10:32 that is an oddly specific Christmas tradition 16:10:48 here it starts at midnight between 24 and 25 in theory, or mid-September in practice :-P 16:10:50 well you could have some a regular computer with infinite memory where the program sits in memory itself so it can surely access itself 16:10:58 although the TM would technically be that computer than 16:11:00 but anyway 16:11:00 mroman: sure, but that's not a turing machine 16:11:21 but it's equivalent to turing machines? 16:11:49 or it's at least as good as a turing machine 16:11:53 equivalent in computational power, but I guess the equivalent for a real computer 16:12:04 would be like trying to have the processor output a copy of its own circuitry 16:12:22 most processors can do that just fine, especially as they don't need to output the data defining that circuitry too 16:12:32 but theoretically a turing machine could produce a representation of itself somehow? 16:12:36 ais523: how would they do that without access to a copy of the schematic? 16:13:00 mroman: Any such machine would either have to be specifically designed to do so, or take enough information to do so in the input, or some mix of the two 16:13:08 I'm assuming they have memory, even if it's just cache 16:13:10 like, a machine which just adds two numbers together couldn't 16:13:14 for a more direct example, see https://codegolf.stackexchange.com/a/100114 16:13:16 because it just adds numbers together 16:13:24 -!- laerling has joined. 16:13:32 oh, you're talking about "not all programs are quines" rather than "some programs are quines" 16:14:25 all normal forms are basically quines. 16:14:38 no 16:14:45 you're confusing two things there 16:15:08 I mean, I guess if you define the output of a computation to be normal form, then yes 16:15:15 \x.y evaluates to \x.y 16:15:45 the original definition of turing machine has no output other than ACCEPT/REJECT though 16:15:48 don't remember what it was caled 16:15:49 so quines are impossible under that definition 16:15:50 beta normal form? 16:16:00 alercah: it could leave a description of itself on the tape 16:16:05 ais523: true 16:16:17 ais523: there's a radio program playing sounds from church bells all over the country at this time (and also church choirs) 16:16:23 but that does require a slightly different definition 16:16:33 and the shops close a couple hours earlier at least. 16:16:34 incidentally, I'm upset that nobody else took up the challenge to create a circuit that output a specification of itself, it was a really interesting idea 16:16:38 but either way 16:16:52 oerjan: over here most shops close at 9pm on Christmas Eve 16:17:03 apparently, even if it's a Sunday (which means that they end up opening /longer/ than they normally would…) 16:17:28 The one liner proof is if H exists with said properties then a Q = IF H(Q) THEN loop(); else halt(); exists thus no H can exist with such properties. 16:17:45 and this one is really easy to understand. 16:18:16 -!- boily has quit (Quit: EXPLODING CHICKEN). 16:18:39 a normal form program is basically a literal-only program 16:18:45 those normally aren't considered quines 16:18:46 similarily if you had two programs A and B that can each answer correctly for a subset of programs 16:18:47 > 16:18:49 err 16:18:49 : error: not an expression: ‘’ 16:18:50 > ` 16:18:52 > 1 16:18:52 :1:1: error: parse error on input ‘`’ 16:18:54 1 16:18:56 there we go 16:18:58 you could combine A and B into a new program 16:19:06 "1" is not normally considered a quine in ghci 16:19:11 probably 16:19:14 because it's just a literal that's printed literally 16:19:16 mroman: you can do that, yeah 16:19:18 but it meets some definitions 16:19:28 mroman: there are definitely subsets of programs for which it can be answered 16:20:14 but you'd have to make some assumption 16:20:30 such as saying that if A can't decide it loops forever and if B can't decide then B loops forever 16:21:15 thus you can create a C(P) = PAR { A(P) ; B(P); } 16:21:38 yeah 16:21:41 which evaluates A and B in parallel and since either A or B eventually terminates C terminates 16:21:52 or if neither can decide, then C doesn't terminate 16:21:53 but then you could create D = IF C(P) THEN loop() ELSE halt() 16:22:15 and C(D) would be wrong 16:22:21 or nonterminating 16:22:33 so we know that no finite amount of programs combined can answer correctly for every P 16:22:37 right 16:22:40 (in a finite amount of time) 16:22:47 you mean bounded, not finite 16:22:55 err wait 16:22:57 no I'm wrong 16:23:02 got it backwards because I'm tired 16:23:05 ignore me >_> 16:23:06 I don't know what you mean by bounded vs finite 16:23:15 ok good pretend I didn't say the stupid thing and move on then 16:23:44 oh. bounded is used for quantities 16:23:45 I see. 16:24:23 in this context bounded usually means there's a single upper bound, so like "there is a number X such that the problem can always be decided in less than X time" 16:24:38 vs "the problem is always decided in finite time, but may take arbitrarily long" 16:24:47 but that still leaves one unanswered question 16:24:53 since neither C nor D can exist 16:24:58 what do we do with that? 16:25:01 philosophically 16:25:20 -!- jaboja has joined. 16:25:41 you think that's bad, how about the algorithms that we know exist but that we can't prove them correct 16:27:13 suppose A exists but if A exists a B must exist but the existence of B means A can't exist thus A does not exist but since A does not exist neither does B exist so neither A nor B actually exist. 16:27:43 ais523: in norway sundays in december can have longer opening hours by law, but not today. 16:27:45 which for the halting problem would mean that there doesn't exist a program where H would answer incorrectly. 16:27:59 because the existence of that program is bound to the existence of H. 16:28:03 and we know H doesn't exist. 16:28:51 which sounds more like the halting problem is undecidable 16:28:55 I mean, notwithstanding that you're not quite right about A and B 16:28:55 rather than saying it exists. 16:29:01 that's just how proof by contradiction works 16:29:13 you take one impossibility, and build on it 16:29:16 not really 16:29:24 many of the intermediate constructions you make will be equally impossible 16:29:32 because they rely on the first impossibility 16:29:32 like the proof for the irationality of sqrt(2) is a proof by contradiction right? 16:29:42 that's one approach 16:29:47 but sqrt(2) actually exists. 16:29:50 that's totally different. 16:30:05 ok, fine, proofs of non-existence by contradiction 16:30:13 which is not what the proof about sqrt(2) is 16:30:31 it'd be like saying H exists 16:30:32 try, say, the proof that there are no functions continuous at all rational points but discontinuous at all irrational ones 16:30:38 but it doesn't have a property you say it have 16:30:39 like 16:30:55 H(x) is a program, suppose H(x) had the property that it answers correctly for all P 16:31:06 you could then proof that H can't have that property 16:31:10 yeah 16:31:16 that's another, equally valid way 16:31:19 because Q = IF H(Q) THEN ... would break that property 16:31:27 for sqrt(2) 16:31:28 but this means that H actually exists. 16:31:41 you could prove that there is no number x for which x is rational and x^2 = 2 16:33:08 which would leave the question what property that H has then. 16:33:13 -!- jaboja has quit (Remote host closed the connection). 16:34:28 you could say P is the set of all programs 16:34:40 and H is the property of a program to answer the correctly whether some other program halts. 16:34:48 -!- propumpkin has joined. 16:35:03 well.. P is the set of all programs that take another program as input and answer with a yes or no 16:35:41 you could then show that no program in that set has the property H. 16:36:55 but they all exist. 16:37:02 they just don't have the property H 16:37:16 -!- contrapumpkin has quit (Ping timeout: 260 seconds). 16:37:20 it's just a question of how you define existence 16:37:21 I'd accept that as a valid proof. 16:37:39 because it avoids the circular argument. 16:37:56 you can't embed a program that doesn't exist 16:38:05 but you're assuming it does 16:38:13 yes but still 16:38:20 I'm assuming H(P) exists 16:38:36 a consequence of that assumption is that you can construct Q 16:38:38 which allows me to define Q=IF H(Q) THEN loop(); else halt(); 16:38:43 right 16:38:49 but I can only construct Q if H exists. 16:38:54 because if H doesn't exist 16:38:55 but you assumed thta it does 16:38:55 then Q doesn't. 16:39:01 if H doesn't exist, you don't need Q 16:39:05 because you're already done the proof 16:39:05 so the chain of proof is 16:39:29 if H exists then Q exists and the existence OF Q proofs that H doesn't exist. 16:39:35 but this invalidates my assumption that Q exists 16:39:39 no 16:39:41 and if Q doesn't exist 16:39:42 Q existing is not an assumption 16:39:45 I can't proof that H doesn't exist. 16:40:02 because to prove that H doesn't exist I need that Q to exist. 16:40:13 Q existing is a consequence of H existing 16:40:17 If Q exists 16:40:20 then H must exist. 16:40:21 you have made only one assumption 16:40:23 which is that H exists 16:40:50 The existence of Q proves that H exists. 16:41:05 yes, but that's only valid in the logical context 16:41:09 which is of an assumption that H exists 16:41:42 there's no need for Q to exist if H doesn't exist 16:41:51 meh :D 16:41:59 I can't accept such kind of proofs. 16:42:02 they're illogical. 16:42:14 no, they're quite logical 16:42:26 exists H => exists Q => not exists H. 16:42:43 since I now know H does not exist. 16:42:52 you never proved Q exists 16:42:57 you proved that "if H exists, Q exists" 16:43:01 I have false => exists Q => not exists H. 16:43:14 and false => X is not a valid proof. 16:43:28 no 16:43:30 that step doesn't hold 16:43:57 (A => B) is true if either A is false OR B is true 16:44:23 so (H exists => Q exists) is true even if H doesn't exist 16:44:37 well formally 16:44:52 but we know Q can't exist because Q embeds H. 16:44:57 so either awy 16:44:58 that's fine 16:45:11 we don't need Q to exist on its own 16:45:15 but yes 16:45:20 we only need it to exist if H exists 16:45:24 wrong => true statement is technically true 16:45:32 but a true statement can't follow from a wrong statement. 16:45:44 yeah 16:45:51 so if we were trying to prove Q exists that would be a problem 16:45:57 fortunately we're trying to prove it doesn't exist 16:46:10 no, you're trying to prove H doesn't exist 16:46:20 well yes 16:46:31 and your proof only works if Q exists. 16:46:39 because you're using Q as a counter example 16:46:39 no 16:46:43 that's not true 16:47:38 you mentioned the proof that sqrt(2) is irrational, right? 16:47:43 yes 16:47:55 the first line is "suppose sqrt(2) is rational, then there exist a and b in lowest terms such that a/b = sqrt(2)" 16:48:01 those a and b don't exist 16:48:04 they cannot 16:48:23 well 16:48:31 the combination of a/b = sqrt(2) doesn't exist 16:49:02 you assume that a are natural numbers 16:49:07 *that a and b 16:49:20 I'm asserting that some numbers with some properties exist 16:49:27 saying they exist without those properties is meaningless 16:49:38 and just pointless philosophizing over the definition of "exist" 16:49:57 natural numbers exist 16:50:11 you just can't find a combination of two natural numbers a and b such that a/b = sqrt(2) 16:50:17 sure, but the pair (a, b) such that a/b is in lowest terms and equal to sqrt(2) does not exist 16:50:33 you're just trying to draw some arbitrary definition of mathematical objects that do exist, and ones that don't 16:50:35 any pair of two natural numbers exist 16:50:43 as oerjan said, you could also look at Q as a function 16:50:48 Q(H) = ... 16:50:52 they just don't have the property that a/b = sqrt(2) 16:50:55 or, well, Q(H)(P) 16:50:58 in that case, Q absolutely exists 16:51:43 or in other terms 16:51:51 sqrt(2) is not member of the set N 16:52:04 eh 16:52:04 set Q 16:52:16 like I said, this is pointless philosophizing with no logical meaning 16:52:27 that's not pointless 16:52:31 if H exists 16:52:35 the logical steps are perfectly well defined 16:52:36 and correct 16:52:48 H can't be a member of the sets of all turing machine-ish programs 16:52:54 you're trying to lift Q's existence outside the hypothetical "H exists" 16:53:01 which is logically invalid, and correctly so 16:53:09 but you're complaining that this means it can't exist in the hypothetical 16:53:10 which isn't true 16:53:36 let's call the set of all turing machines T 16:53:44 then H is not member of that set. 16:54:05 that follows from the halting problem proof. 16:54:11 right 16:54:25 but Q is member of that set. 16:54:30 no 16:54:49 it isn't 16:55:01 so Q itself isn't a set of T 16:55:09 do you mean member? 16:55:10 so you can't use the existence of Q to proof anything 16:55:13 because it's not even within T 16:55:21 but the question is whether H can answer it correctly for members of T 16:55:24 but if Q isn't member of T 16:55:29 but 16:55:30 then Q isn't a counter example. 16:55:34 if we suppose H exists 16:55:37 i.e. 16:55:38 H \in T 16:55:41 then Q can be defined 16:55:43 and Q \in T 16:56:00 but Q can only be in T if H is in T 16:56:05 but we assume H is in T 16:56:09 that follows from the definition of H. 16:56:10 so it's a logically valid step 16:56:10 eh. 16:56:12 definition of Q 16:58:26 I think you're getting hung up on "existence" here 16:58:36 because the logical step of picking a and b in the proof of sqrt(2) is no different 16:58:43 it's a step which is only logically valid if the statement is false 16:58:47 that's how proof by contradiction works 16:58:57 I don't think it's the existence per se but the fact that a proof should be valid if up update it with new information. 16:59:05 *you update 16:59:10 but then the sqrt(2) proof is equally invalid 16:59:16 why? 16:59:21 because once we prove that sqrt(2) is irrational 16:59:26 suppose sqrt(2) is a member of Q 16:59:27 we know that the step of picking a and b was invalid 16:59:44 by your argumen 16:59:48 then there would exist an a,b both member of N such that sqrt(2) = a/b. 16:59:53 right 16:59:55 well 17:00:02 if we include the fact that sqrt(2) is positive 17:00:06 otherwise they could be negative 17:00:09 but generally yeah 17:00:33 more specifically, you cand find a pair of a,b with the property of a/b = sqrt(2) 17:00:41 a^2/b^2 = 2 17:00:50 right 17:01:14 yada yada so we know for that to be true both a and b would have to be even numbers. 17:01:30 yeah you can leave out hte details 17:02:43 I skipped one assumption tho 17:02:49 that a and b don't have common factors 17:03:05 yeah, that's fine, I'm familiar with the proof 17:03:22 we assumed that we can find a pair a,b with no common factors such that a/b = sqrt(2) 17:03:29 no 17:03:33 but this is wrong. 17:03:33 we assumed that sqrt(2) \in Q 17:03:48 since both a and b have to be even if a/b = sqrt(2) 17:05:23 -!- xkapastel has joined. 17:05:24 so this is a contradiction 17:05:32 right 17:05:47 thus we know there's no such pair of a,b as we assumed 17:06:46 hm i see 17:06:50 now we know that a and b must have at least a common factor of 2 17:07:05 now we go back 17:08:27 mroman: hm i think i have a hunch where you're getting hung up, and the sqrt(2) proof is just simple enough to avoid it. but what about the proof of the infinitude of primes? 17:09:55 maybe we can find a,b with common factors such that a/b = sqrt(2) 17:09:58 it seems to have the same H => P => no such H thing 17:10:05 *structure 17:10:32 (well, perhaps i should wait to see if you _are_ hung up on sqrt(2) first) 17:11:04 so we divide by two repeat 17:11:11 but you'll always end up with the same thing. 17:11:44 * oerjan had some washing to do 17:12:03 so we know that if a/b = sqrt(2) then both a and b can endlessly be divided by two. 17:13:43 -!- laerling has quit (Ping timeout: 265 seconds). 17:13:53 so sqtr(2) = x*2^infinity 17:17:31 which is nonsense 17:17:52 because you can't do that within Q 17:18:26 you mean there's no largest prime? 17:19:17 Is there a quick algorithm to figure out both the squarefree core of a number as well as the square root of the rest, at the same time? 17:19:59 Assume there's a number with the property of being prime such that you can not find a number larger than that also having the property of being prime. 17:20:49 assume p = p1*p2*p3*p4*p5*...*pn has this property 17:21:38 +1 17:21:54 (otherwise it wouldn't be prime) 17:22:36 then q = p1*p2*p3*p4*p5*...*pn*p+1 would also be prime 17:22:42 thus p doesn't have the property 17:23:12 which now we go back as well 17:23:27 we know that p doesn't have the property 17:23:31 but we know that p is prime 17:24:18 p doesn't need to have the property for the proof to work 17:24:18 p doesn't need to have the property for the proof to work 17:25:26 -!- h0rsep0wer has joined. 17:25:52 so the fact that p doesn't have the property doesn't invalidate the fact that q is a larger prime than p 17:26:13 so q disproves that p has the property. 17:26:21 which is logically consistent. 17:26:32 Help my scrollback is full of proof and I do not know what is going on (I missed the beginning) 17:27:19 mroman: i wanted to explain it in a different way, to highlight the similarity. 17:27:30 Taneb: I reject the halting problem proof on the grounds that you assume and H exists and then create a counter example Q = IF H(Q) THEN loop(); ELSE halt(); to prove that H does not exist. 17:27:36 assume there are finitely many primes, let H be the list of all of them. 17:27:51 but if you come back with this new knowledge of H not existing you'll find that Q (your counter example) can't exist as well 17:27:58 thus your counter example doesn't exist 17:27:59 thus your proof sucks :D 17:28:21 now if H exists, then let Q be the product of all the numbers in H. 17:28:40 continue as you did. from the existence of Q we deduce that H cannot exist. 17:28:57 -!- augur has joined. 17:29:08 now you have the exact same structure as for the point you disagree with in the halting problem. 17:29:16 mroman, so... proof by contradiction? 17:31:36 zzo38: i don't think you can find the squarefree core of a number without prime factorization 17:31:56 Taneb: I'm fine with proofs by contradiction. 17:33:47 -!- augur has quit (Ping timeout: 268 seconds). 17:34:27 Taneb: he's having trouble with proofs of the form H exists => Q exists, Q exists => H doesn't exist, ergo H doesn't exist 17:34:54 oerjan, I see 17:34:54 so i'm trying to show a different one, but i think i chose a bad time. 17:34:59 I think I'll sit this one out 17:36:06 Taneb: The reason is because your proof gives you new knowledge and if you update your proof with this new knowledge you'll find that Q can't exist and thus you don't have a counter example anymore. 17:36:20 The counter example you used to proof the non-existence of H does itself not exist to begin with. 17:36:38 counter examples inherently need to exist 17:36:45 an argument based on a non-existing counter example is 17:36:47 well 17:36:47 mroman, what about a counterexample scheme 17:36:50 I consider it non-sense 17:37:02 A function from example to counter-example 17:37:27 mroman: grmble. ok let's reformulate the original instead, i think it can be done. 17:37:38 but you can reformulate the proof 17:37:52 to show that no program in the sets of all programs can have the property of answering stuff correctly 17:38:36 let H be a program deciding _something_ about other programs. let Q = if H(Q) then loop(); else halt() 17:39:02 as in. Let M be the set of all programs taking a program as input and answer yes or no then we can certainly show that no program in this set answers correctly for all programs. 17:40:04 Meaning that no such program exists in the set of all programs. 17:40:11 ... 17:40:19 (no program that answer correctly for all programs) 17:40:21 whatever. 17:41:06 but the program itself exists 17:41:13 it just doesn't have the property you assumed it does 17:42:21 -!- variable has joined. 17:42:23 There isn't a fundamental difference between the two arguments here to me 17:42:28 int-e: I was going to tell you that SSR is 75% off but I forgot you already played it. 17:43:14 Right. I'm stuck. The Witless is also available at a reasonable price. 17:43:43 Taneb: not in the outcome. 17:43:44 Let M be the set of all programs of the form A(B) = true/false For every program P in M we can construct a program Q = IF P(Q) THEN loop(); ELSE halt(); which would imply that P does not answer correctly for Q. 17:43:55 but there's a slight difference here 17:44:00 namely the fact that P exists 17:44:05 which means Q exists 17:44:11 which means we can use Q as a counter example 17:44:16 because Q exists 17:44:24 mroman, I think we have a difference in mathematical philosphy here 17:44:26 thus making the proof logical. 17:44:32 Taneb: It appears so. 17:45:52 but this proof makes sense to me. 17:45:54 the other doesn't. 17:45:59 int-e: Any other good jams? 17:46:24 but if my reformulation of the proof is correct 17:46:30 then I can accept the halting problem to be true 17:47:05 otherwise I have to continue looking :D 17:47:45 mroman, so... the form you don't like is (\exists x \in S => ¬ \exists x \in S) => ¬ \exists x \in S 17:48:01 -!- Taneb has left ("Leaving"). 17:48:06 -!- Taneb has joined. 17:48:32 But the form you do like is \forall x \in T => (P(x) => ¬P(x)) => ¬P(x) 17:48:38 Is this right? 17:50:13 \exists X \in S => \exists Y \in S => \not \exists X \in S <- I don't accept this. 17:50:41 because the existence of Y \in S is tied to the existence of X \in S 17:50:46 which you later proof to be wrong. 17:50:57 like 17:51:04 I am not sure where that Y is coming from here, the counter example for the halting problem is not in the set of halting oracles 17:51:07 travelling in time shouldn't invalidet proofs. 17:51:12 *invalidate 17:51:20 shachaf: I don't know. I finished The Night of the Rabbit today (which I started last year... I took a break which saved me using a walkthrough) which I liked quite a lot. 17:51:39 well Q is a counter-example to H. 17:51:45 But of course it's a point&click adventure, so completely different genre. 17:51:55 It's a witness that the existence of H is inconsistent 17:52:04 but Q contains H 17:52:16 Q = IF H <- see. H is contained within Q. 17:52:45 All proofs by contradiction do something like that, though 17:52:56 not really. 17:53:10 yes, really. 17:53:36 Assume 9 is even. If 9 were even then sqrt(9) had to be even since 9 is a perfect square. sqrt(9) = 3 which is odd thus our assumption that 9 was even must be wrong thus 9 must be odd. 17:54:07 int-e: Did you jam Recursed? 17:54:18 You make a proof that 3 is even using a proof that 9 is even 17:54:25 mroman: yes, so you've constructed an *even* square root of 9, which is something that doesn't really exist. 17:54:34 -!- propumpkin has changed nick to contrapumpkin. 17:54:35 But then use this to prove that 9 is odd, so the proof that 3 is even cannot exist 17:54:52 well 3 isn't even. 17:54:55 I don't see the problem there. 17:55:26 The only objection I have is that a proof of contradiction is not necessary in this case... never mind involving square roots. 17:55:27 I can't see why you're happy with that and unhappy with expressing Q in terms of H 17:55:55 Taneb: because it's still consistent. 17:56:46 my assumption that 9 is even turned to be wrong 17:56:51 so now I know that 9 is odd. 17:57:06 but no statement is invalidated in this proof by 9 being odd. 17:57:18 nothing in that proof depends on 9 being odd. 17:57:19 The Q constructed in the halting problem proof does exist for any given H as well; it just fails to halt if and only if it doesn't halt, because that property relies on the assumption on H. 17:57:25 I don't understand your argument here 17:57:37 it's like uhm 17:57:38 I'm going to wander off 17:58:25 This is quite analogous to the square root of 9. It exists, it equals 3, it just happens not to be even after all. 18:01:08 Assue 9 is even. If 9 is even then 9+0 is even. Since 9+0 is even then .\ 18:01:28 now you somehow end up showing that 9 is not even. 18:01:41 then isn't valid anymore. 18:02:29 or if would show that 9 is odd. 18:02:33 that just doesn't work logically. 18:02:51 Anyway, I'm with Taneb here, I don't understand what your problem is. 18:04:02 whatever you conclude from 9+0 is even 18:04:06 is only valid if 9+0 is even 18:05:10 :( 18:05:25 shachaf: nay on recursed 18:05:46 mroman: this is just basic logic 18:06:20 int-e: It's a cute game and also on sale 18:06:34 Starts off a bit slowly but there are some fun levels. 18:10:08 int-e: yeah... but it's a big difference whether you say it doesn't exist or whether you say it doesn't have a certain property. 18:10:39 you can certainly say that H doesn't have the property of answering correctly for all programs 18:10:43 as it inevitably fails on Q. 18:11:16 and that's valid. 18:11:47 because if H exists then Q can exist and if Q can exist then Q shows that H doesn't have the right properties. 18:12:17 thus your proof remains valid. 18:14:12 because you can call/embed programs that exist. 18:20:21 whatever :D 18:20:33 I'm just not accepting spooky exists proofs. 18:24:58 shachaf: hmm, might be fun 18:32:17 -!- FreeFull has joined. 18:49:57 -!- jaboja has joined. 19:10:15 the other question is whether the halting problem is only undecidable for programs that invoke H. 19:10:27 and very decidable for programs that do not invoke H. 19:11:00 if it were only undecidable for for programs invoking H 19:11:13 mroman, how do you determine if a program invokes H? 19:11:26 No idea. 19:11:27 but indirectly 19:11:36 if you can't tell if the program halts or not it would contain H. 19:11:52 I think "invokes H" is either ill-defined or itself undecidable (by Rice's theorem) 19:12:02 if the assumption is correct that all undecidable programs invoke H. 19:12:40 so far we just know that programs of the form IF H(myself) THEN ... are undecidable. 19:13:00 so it might be that we can write an a program that answers _correctly_ with yes/no/undecidable 19:13:21 is there a proof that shows that you can't do that either? 19:13:41 -!- sleffy has joined. 19:13:52 trivially as mentioned you can write an H2 that detects a specific Q and respond with undecidable 19:14:08 so a program can surely for some instances tell whether the program halts, doesn't or whether it's undecidable. 19:14:23 so in specific cases it's decidable whether it's undecidable :D 19:14:41 the bigger question is whether it's decidable in the generic case. 19:15:30 specifically... 19:15:54 the actual question would be whether a program can detect that the termination of another program is dependent on itself. 19:16:18 because if H can conclude that the termination of P depends on the output of H 19:16:26 then it can answer with undecidable and would do so correctly. 19:17:07 which means the sets of programs that halt and don't halt would be well defined 19:17:17 and there would be a subset of programs that are undecidable 19:17:21 knowingly undecidable 19:17:29 because the outcome depends on H itself. 19:18:40 trivially for IF H(myself) THEN loop(); ELSE halt(); you can conclude perfectly fine that the outcome depends on H 19:19:09 mroman, not if you don't have the program in that form 19:19:14 If H is inlined you're lost 19:19:30 is there a proof that shows that you can't do that either? <-- yes, because any undecidable program doesn't halt, so you could trivially turn that program into one that decides halting itself. 19:19:55 hu? 19:20:00 why do undecidable programs not halt? 19:20:22 if it did it would be decidable 19:20:30 simply run it until it halts, there's your proof it halts 19:20:46 I mean undecidable as in it's decidable that it depends on H 19:20:54 as in 19:20:56 like 19:20:58 uhm. 19:21:01 "This sentence is false". 19:21:17 I _know_ that this sentence is neither true nor false within this boolean logic. 19:22:08 -!- jaboja has quit (Ping timeout: 252 seconds). 19:22:11 so I know that for IF H(Q) then loop(); else halt(); the outcome is depends on H 19:22:44 so H could detect that the outcome depends on the answer it gave the first time 19:22:46 hypothetically 19:22:54 I mean 19:23:00 I assume turing machines are as smart as humans 19:23:01 kinda 19:23:12 humans can tell that this program is a "paradox" 19:23:22 (at least as smart) 19:24:12 what if H runs the program Q 19:24:22 deliberatily answering with a specific "yes" or "no" 19:24:26 to cause it to either terminate or not 19:24:33 then revising it's answer for the actual output of H. 19:24:38 *its 19:24:58 mroman: ok i didn't interpret undecidable the same way you do. but like others i'm not sure whether your version is well-defined (although it might be an interesting concept if it is.) 19:26:00 oerjan: I mean it as in could an H detect that the halting state of a program depends on H and then answer with a third answer. 19:26:32 the problem is that there's almost surely a way to hide H in a program such that H cannot detect it. 19:26:36 which I guess boils down to H being able to detect itself in the program it's given? 19:26:46 *its 19:27:21 for one thing, rice theorem says that it's undecidable whether a program is equivalent to H. 19:27:26 *rice's 19:28:39 -!- h0rsep0wer has quit (Quit: Leaving). 19:29:37 it's like the halting theorem on steroids: you cannot decide _anything_ about a program that is preserved under equivalence. 19:30:49 you could do statistical tests though. 19:31:06 but that's uninteresting. 19:31:41 -!- moony has quit (Remote host closed the connection). 19:31:42 so 19:31:49 if we assume there's H1 and H2 19:31:58 which are semantically identical 19:32:14 they both answer yes/no/dependent 19:32:21 (let's call it dependent instead of undecidable) 19:32:46 then what happens if we feed Q = IF H2(Q) THEN loop(); ELSE halt(); to H1. 19:33:41 H1 can detect it's own presence. 19:33:43 so 19:33:54 inevatibly IF H2(Q) THEN loop(); ELSE halt(); gets fed through H2 19:33:58 and H2 can detect it's own presence 19:34:04 so H2 would detect itself in there? 19:34:36 so if H1 would just eval this 19:34:44 H2 would say dependent 19:35:07 well actually we need switch-case now :D 19:35:24 since a simple if is just true/false 19:36:01 Q = CASE H2(Q) OF TRUE -> loop(); FALSE -> halt(); DEPENDENT -> .... END 19:36:28 even if we feed hat to H2 19:36:36 H2 is going to answer DEPENDENT 19:36:47 so if we put DEPENDENT -> stops(); in there 19:36:54 then DEPENDENT would be wrong. 19:36:59 because it stops. 19:37:20 thus H2 would get that wrong. 19:37:21 meh. 19:37:24 game over :D 19:38:17 H2 doesn't exist. 19:39:35 I'd say you're overthinking this. You seem to be constantly amazed by the fact that *under a false assumption*, you can prove both a statement and its negation, but in fact this is true for any statement at all. 19:40:42 but you could loosen it 19:40:52 and say H2 just answers whether it's dependent on itself. 19:40:53 nothing else. 19:41:08 so the program might terminate but H2 will answer dependent 19:41:28 so dependent would just mean "dependent on myself". 19:42:58 int-e: not in all forms of logic 19:43:17 some people in my department have put a lot of effort into logics where (x and not x) does not imply y 19:47:18 ais523: please let's not go there 19:48:04 int-e: my thesis was heavily based round forms of logic where (x and not x) is a syntax error 19:48:34 -!- sebbu has quit (Ping timeout: 272 seconds). 19:48:34 I know that there's work on paraconsistent logics and for the time being I'm pretty happy to keep my knowledge of such logics on that level. 19:48:37 so I have some experience with weird logics generally 19:58:26 `? paraconsistent 19:58:28 paraconsistent? ¯\(°​_o)/¯ 19:59:09 `le/rn paraconsistent//There has been a lot of work on paraconsistent logics, although there hasn't been a lot of work on them. 19:59:11 Learned 'paraconsistent': There has been a lot of work on paraconsistent logics, although there hasn't been a lot of work on them. 20:08:31 -!- sleffy has quit (Ping timeout: 248 seconds). 20:19:52 -!- sleffy has joined. 20:20:05 nothing follows from a contradiction. 20:20:48 (x => y) y might be true if it's independent from x 20:20:50 as in 20:21:12 9 is even => there are an infinite number of primes 20:21:35 it's true that there are an infinite number of primes 20:21:52 but it's wrong to follow that from the assumption that 9 is even. 20:23:07 9 is even => 7 is even 20:25:00 if X exists then Y exists. 20:25:09 If X doesn't exist you've just proven that Y doesn't exist. 20:25:22 That's an acceptable conclusion. 20:25:35 if X exists then Y exists. If Y exists then Z exists. 20:25:49 If X doesn't exist then Z doesn't exist. 20:25:54 That's an invalid conclusion. 20:26:06 Z might exist independently 20:26:22 if X exists then Y exists. If Y exists then Z exists. If Z exists then X doesn't exist. 20:27:13 Z only exists if and only if Y exists and Y only exists if and only if X exist. They might exist independently of course, but you'd have to prove that independently. 20:27:54 Since X doesn't exist if Z exists but Z exists if X exists 20:28:39 That just can't possibly work. 20:29:24 it can work if it follows directly 20:30:22 that's like uhm 20:31:03 if a > b then c > d if c > d then a < b 20:31:48 but if a < b then you don't know whether c > d thus you can't know whether a < b 20:32:27 you can only show that a < b if you know for certain that c > d 20:32:28 but you don't 20:32:39 because c > d is only valid if a > b 20:33:06 in essence 20:33:13 you know nothing about whether a > b or a < b 20:34:06 -!- jix has quit (Quit: leaving). 20:34:25 -!- jix has joined. 20:39:40 shachaf: so apparently, the recursion achievement is unlocked by unlocking the recursion achievement. that's good to know. 20:44:34 int-e: sounds obvious in hindsight 20:46:46 yeah this sounds wrong. 20:46:50 i need a better example. 20:47:31 the argument doesn't work there. 20:47:45 it certainly allows you to conclude that a > b can't be true. 20:50:37 if were true then there would exist showing ! 20:50:40 Not the corecursion achievement? 20:50:43 thus isn't true. 20:51:21 if exists then there would exist showing does not exist. 20:51:57 hm. 20:52:01 you guys were right. 20:52:04 this is the same thing. 20:53:00 But in any Case, whether anything would exist or not, there still would be the pointed Brackets 20:53:06 Metadata > Data 20:53:43 it just sounds weird 20:53:51 because the word exists makes my brain jump to physical things 20:54:01 and it's hard to convince your brain about hypothetical physical things that do not exist 20:54:19 Brains are physical, but Spirit is not necessarily 20:54:39 Also, You have an infinite Number of Heads 20:55:33 the existence of H would prove its own inexistence. 20:55:49 This is proven in Robert Anton Wilson's „Quantum Psychology“ 20:56:13 But i got two different Instances of the Book, and both disappeared 20:56:33 Then last Year i tried to order one additional Copy as a Gift for my Sister 20:56:39 It did not arrive 20:56:52 So maybe we actually all have zero Heads ☺ 20:57:55 https://xkcd.com/1782/ 21:01:22 -!- erkin has joined. 21:09:30 well 21:09:34 it's still better than slack. 21:10:14 you can't be in multiple teams in the same tab in slack 21:10:15 that's weak 21:10:43 -!- mroman has quit (Quit: well good night anyway). 21:13:10 -!- ais523 has quit (Quit: quit). 21:16:28 But i got two different Instances of the Book, and both disappeared <-- that sounds like a non-unitary evolution to me, are you sure it's quantum? 21:22:34 oerjan: it was a way of telling shachaf that I've obtained a copy of "Recursed". 21:25:00 -!- FreeFull has quit (Read error: Connection reset by peer). 21:44:00 . o O ( curses, foiled again ) 21:52:39 -!- ais523 has joined. 21:53:07 -!- FreeFull has joined. 22:01:04 -!- sebbu has joined. 22:05:09 -!- erkin has quit (Quit: Ouch! Got SIGABRT, dying...). 22:20:31 -!- jaboja has joined. 22:29:43 -!- h0rsep0wer has joined. 22:32:13 int-e: Did you get the achievement? 22:32:49 well, yes. 22:52:46 -!- variable has quit (Quit: Found 1 in /dev/zero). 23:23:54 -!- ais523 has quit (Ping timeout: 272 seconds). 23:32:34 -!- h0rsep0wer has quit (Remote host closed the connection). 23:42:12 -!- h0rsep0wer has joined. 23:43:04 -!- h0rsep0wer has quit (Remote host closed the connection). 23:49:04 -!- h0rsep0wer has joined. 23:49:56 -!- h0rsep0wer has quit (Client Quit). 23:50:25 -!- sleffy has quit (Ping timeout: 248 seconds). 23:53:11 -!- h0rsep0wer has joined. 23:54:42 -!- h0rsep0wer has quit (Remote host closed the connection). 23:55:06 -!- h0rsep0wer has joined. 23:56:12 -!- h0rsep0wer has quit (Remote host closed the connection). 23:56:35 -!- h0rsep0wer has joined. 23:57:42 -!- h0rsep0wer has quit (Remote host closed the connection).