@LeakyNun Tell me whether the program that searches for a Collatz cycle halts or not!

@user21820 can you derive a contradiction?

If you can find a Collatz cycle, you would have disproven the conjecture. If you can establish that there is no cycle, then you would have made major progress.

Alternatively, tell me whether ( the program that searches for a proof over ZFC that ( ZFC is arithmetically unsound ) ) halts or not. =D

@user21820 I'm quite serious

isn't there a procedure to turn a program P into a program Q such that P applied to Q answers wrong on the halting problem for Q ?

@LeakyNun What? We already know no such program H exists.

@user21820 I mean, how to disprove the existence of such program?

@mercio It's called unsolvability of the halting problem, and you may be interested in reading at least the first half of my pinned post on the right about the incompleteness theorems, where I show that it is easy to prove incompleteness by using the fact that the halting problem cannot be solved.

@user21820 how do you know?

@LeakyNun Wait don't you already know, from reading that same post?

@user21820 that only addresses programs that take any input

my program only takes the empty input

Aha.

But sure there is a more general theorem.

We say that P is a behavioural property iff ( for every programs x,y that have the same output behaviour (same output or both do not halt) we have P(x) ⇔ P(y) ).

For example, halting on empty input is a behavioural property.

Take any behavioural property P such that there are programs t,f satisfying P(t) and ¬P(f). Then the undecidability theorem states that there is no program that can decide P.

The proof is quite easy actually. Given any program D that decides P, we can construct the program S = ( x ↦ D( y ↦ x(x)(y) ) ? f : t ).

Where the ( q ? u : v ) is standard C/Java meaning ( if q then u otherwise v ).

@mercio @LeakyNun: Do you get what I have defined S to be?

S takes input x, runs D on the program ( y ↦ x(x)(y) ) which is symbolically constructed, and then returns either f or t based on D's answer.

@user21820 Hi

Hello!

I'm proving the general undecidability theorem for program behaviour.

Now consider S(S). It halts because D always halts, and hence must output either t or f. You can easily see that both cases lead to contradiction.

Is it something I should be able to follow?

If you know programming, you definitely can understand it.

That's all there is to it. Any questions?

ok let me back up and read off the top

@user21820 <− Starts here.

@user21820 but y ↦ x(x)(y) takes input

@LeakyNun All programs take input. This undecidability theorem applies to any behavioural property that may depend on what the program does on various inputs.

my program is only sound for empty input

otherwise it is noise

but your program y ↦ x(x)(y) takes input

Your program takes a program x and decides whether x(0) halts or not.

so my program isn't sound for it

yes

No you're not getting it.

I know I'm not

that's why I asked you

Given your program, we have a decider for ( programs that halt on zero/empty input ).

Which is impossible as the theorem shows.

If you are saying that your program does not always give a yes/no answer then you cannot say "whether" in your definition.

I don't get what y ↦ x(x)(y) means

I mean, I know what it means of course

( y ↦ x(x)(y) ) is a program that takes input y and runs x on x and then the result on y. Such a program can be constructed programmatically from the code of x.

exactly

will pop back in later, ping me whenever you're free @user21820

oh

@LastIronStar I will be going off soon for quite a long while.

you want it to take input even though there won't be any

I see

@user21820 Weekend Trip?

@user21820 Then tell me something to read!

No no just like hours.

Haha..

@LeakyNun Yes the key is just to construct a behavioural property (of programs with input) that can be solved by your decider.

So this undecidability theorem easily proves the unsolvability of the halting problem.

And many many others.

It can be phrased informally as:

> Every non-trivial behavioural property of programs cannot be decided by a program.

ok

tio.run/##rY0xCsMwDADn6BVBYJCgW6cU0k/…

def does_halt(s):
	assert(type(s)==str)
	return len(s)>99

def S(x):
	assert(type(x)==str)
	return not does_halt("%s(%s)(input())"%(x,x))

print(S("""def S(x):
	assert(type(x)==str)
	return not does_halt("%s(%s)(input())"%(x,x))"""))

:P

I know there are some problems, just trying to loosely code it

@user21820

@LeakyNun Why so complicated? Just use Javascript:

@user21820 ...

you win

function S(x) { return ( D( function(y) { return x(x)(y); } ) ? f : t ); }

This S may crash on run-time, but it serves its purpose.

alright

you should have function S(x) { return ( ! D( function(y) { return x(x)(y); } ) ); } instead :P

Okay got it?

Cannot work.

S needs to return a program.

It's to diagonalize using the programs t,f.

oh, so a program is a function now?

wait, t and f are programs?

or better, S = x => D(y => x(x)(y)) ? f : t

I do come from PPCG :P

@LeakyNun Ironic.

@user21820 how?

@LeakyNun (1) Your chat account is literally from there. (2) Your first attempt was a bit long compared to my Javascript.

lol

That's why I love Javascript for explaining computability stuff. It looks exactly like what I said in the mathematics.

Anyway do you get the theorem and the proof fully?

@LeakyNun: You there? I'm not going to be here soon.

I think I do

Okay then. If you (or anyone else) has further questions about it, just ask and I'll respond next time.

@LeakyNun: See you!

see you