Logic - 2017-12-17 (page 2 of 2)

« first day (487 days earlier) ← previous day next day → last day (2624 days later) »

user21820

16:02

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

Leaky Nun

@user21820 can you derive a contradiction?

user21820

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

Leaky Nun

@user21820 I'm quite serious

mercio

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 ?

user21820

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

Leaky Nun

16:07

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

user21820

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

Leaky Nun

@user21820 how do you know?

user21820

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

Leaky Nun

@user21820 that only addresses programs that take any input

my program only takes the empty input

user21820

Aha.

But sure there is a more general theorem.

@mercio: LeakyNun is right that my post does not address his version, so I'll present a short proof of the general undecidability theorem now.

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.

LastIronStar

16:18

@user21820 Hi

user21820

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.

LastIronStar

Is it something I should be able to follow?

user21820

If you know programming, you definitely can understand it.

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

LastIronStar

ok let me back up and read off the top

user21820

@user21820 <− Starts here.

Leaky Nun

16:24

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

user21820

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

Leaky Nun

37 mins ago, by Leaky Nun

@user21820 I have a program H that takes a program and returns whether it halts on an empty input.

my program is only sound for empty input

otherwise it is noise

user21820

14 mins ago, by user21820

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

Leaky Nun

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

user21820

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

Leaky Nun

16:26

so my program isn't sound for it

yes

user21820

No you're not getting it.

Leaky Nun

I know I'm not

that's why I asked you

user21820

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.

Leaky Nun

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

I mean, I know what it means of course

user21820

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

Leaky Nun

16:29

exactly

LastIronStar

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

Leaky Nun

user21820

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

Leaky Nun

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

I see

LastIronStar

@user21820 Weekend Trip?

@user21820 Then tell me something to read!

user21820

16:30

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.

LastIronStar

Leaky Nun

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))"""))

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

@user21820

user21820

@LeakyNun Why so complicated? Just use Javascript:

Leaky Nun

@user21820 ...

you win

user21820

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.

Leaky Nun

16:41

alright

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

user21820

Okay got it?

Cannot work.

S needs to return a program.

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

Leaky Nun

oh, so a program is a function now?

wait, t and f are programs?

user21820

29 mins ago, by user21820

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.

Leaky Nun

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

I do come from PPCG :P

user21820

@LeakyNun Ironic.

Leaky Nun

16:43

@user21820 how?

user21820

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

Leaky Nun

lol

user21820

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.

Leaky Nun

I think I do

user21820

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

@LeakyNun: See you!

Leaky Nun

16:52

see you

« first day (487 days earlier) ← previous day next day → last day (2624 days later) »

all rooms

Transcript for

Dec16

Dec '1717

Dec18

♦ $Mathematics$ Logic

This room is meant for discussion about logic, including found...

formal-systems foundations logic no-trolls

join this room
about this room

00:00

06:00

12:00

18:00

all times are UTC

$Mathematics$

Transcript for

♦ Logic

♦ $Mathematics$ Logic