Undecidability of program behavioural properties

Conversation started Dec 17, 2017 at 16:09.

user21820

Dec 17, 2017 16:09

@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

@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

Dec 17, 2017 16:24

@user21820 <− Starts here.

Leaky Nun

@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

so my program isn't sound for it

user21820

Dec 17, 2017 16:26

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

Leaky Nun

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

Dec 17, 2017 16:29

( 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

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

Dec 17, 2017 16:30

@user21820 Weekend Trip?

@user21820 Then tell me something to read!

user21820

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

Dec 17, 2017 16:38

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

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

Conversation ended Dec 17, 2017 at 16:43.

all rooms