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