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!

09:16:51 <Taneb> Actually, I care about (x/2)/(2^x) but I think if one converges then so will the other

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: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: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: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).

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:35:02 <mroman> which would mean that the existence of a Q does not mean that no such H can exist.

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: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:43:13 <alercah> and comparing representation works, but there are infinitely many possible representations of equivalent programs

15:44:06 <mroman> if two LC terms are semantically the same they'd evaluate to the same final form eventually

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: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:47:08 <alercah> in order for your argument to be valid, you need a proof that Q *is* unique under reduction

15:53:54 <oerjan> it's not actually a big difference if you disallow I/O there, it can be hardcoded.

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.

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:58 <alercah> (it's not too hard to show how to do this, though I can explain it more if you need)

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: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:37 <ais523> hmm, maybe I should write a better BuzzFizz interp so that I can look into whether it can write a quine

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:11:53 <alercah> equivalent in computational power, but I guess the equivalent for a real computer

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: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:32 <ais523> oh, you're talking about "not all programs are quines" rather than "some programs are quines"

16:15:08 <alercah> I mean, I guess if you define the output of a computation to be normal form, then yes

16:15:45 <alercah> the original definition of turing machine has no output other than ACCEPT/REJECT though

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: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: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:18:46 <mroman> similarily if you had two programs A and B that can each answer correctly for a subset of programs

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:41 <mroman> which evaluates A and B in parallel and since either A or B eventually terminates C terminates

16:22:33 <mroman> so we know that no finite amount of programs combined can answer correctly for every P

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: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: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:55 <mroman> H(x) is a program, suppose H(x) had the property that it answers correctly for all P

16:34:40 <mroman> and H is the property of a program to answer the correctly whether some other program halts.

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: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: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:58:36 <alercah> because the logical step of picking a and b in the proof of sqrt(2) is no different

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.

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:03:22 <mroman> we assumed that we can find a pair a,b with no common factors such that a/b = sqrt(2)

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:12:03 <mroman> so we know that if a/b = sqrt(2) then both a and b can endlessly be divided by two.

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: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:32 <Taneb> Help my scrollback is full of proof and I do not know what is going on (I missed the beginning)

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: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:29:08 <oerjan> now you have the exact same structure as for the point you disagree with in the halting problem.

17:31:36 <oerjan> zzo38: i don't think you can find the squarefree core of a number without prime factorization

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: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:37:27 <oerjan> mroman: grmble. ok let's reformulate the original instead, i think it can be done.

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: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: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: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:50:13 <mroman> \exists X \in S => \exists Y \in S => \not \exists X \in S <- I don't accept this.

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: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: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:25 <int-e> mroman: yes, so you've constructed an *even* square root of 9, which is something that doesn't really exist.

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: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: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: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: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.

19:10:15 <mroman> the other question is whether the halting problem is only undecidable for programs that invoke H.

19:11:52 <Taneb> I think "invokes H" is either ill-defined or itself undecidable (by Rice's theorem)

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: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:15:54 <mroman> the actual question would be whether a program can detect that the termination of another program is dependent on 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: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: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:27:21 <oerjan> for one thing, rice theorem says that it's undecidable whether a program is equivalent to H.

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: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: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: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 <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: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: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:39:40 <int-e> shachaf: so apparently, the recursion achievement is unlocked by unlocking the recursion achievement. that's good to know.

20:50:37 <mroman> if <some thing> were true then there would exist <another thing> showing !<some thing>

20:51:21 <mroman> if <some thing> exists then there would exist <yet another thing> showing <some thing> does not exist.

20:53:00 <APic> But in any Case, whether anything would exist or not, there still would be the pointed Brackets

20:54:01 <mroman> and it's hard to convince your brain about hypothetical physical things that do not exist

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?