[Swift-devel] Problem with iterate

[Mihael Hategan]

On Fri, 2010-02-19 at 11:13 +0000, Ben Clifford wrote:
> > Right. So termination is undecidable by virtue of it being a turing
> > complete language. What I'm unsure is whether deadlocks follow as a
> > consequence of that. They are a different beast.
> 
> Turing complete languages don't deadlock in general.
> 
> (yes, concurrent programs do, but regard swift as a serial programming 
> language, not as a concurrent one; and regard concurrent execution as 
> 'merely' an execution optimisation)

Swift semantics can be executed by a single thread without the
involvement of any concurrency as you point out. It would still lead to
non-termination due to loops in the dependency graph.

> 
> So I don't think deadlocks are a consequence of that.
> 

I wasn't asking whether deadlocks are a strict consequence of it being
turing complete. We can clearly have deadlocks with much simpler classes
of programs (a = f(b), b = f(a)).

What I was wondering is whether turing completeness implies
undecidability for deadlocks in the swift semantics.

> But I do think that probably finding deadlocks given the language features 
> of SwiftScript is undecideable (not as a consequence of turing 
> completeness, but because of our choice of language features); and on a 
> more practical note, requires knowledge of the output of app blocks.
> 

Swift is turing complete, so any algorithm that can be written in java
can be written in swift.

Say the deadlock finding function is D(program) returning true if
program deadlocks, false otherwise.

P(program) {
  if (D(program)) {
    return;
  }
  else {
    a = b + 1;
    b = a + 1;
  }
}

P(P):
D(P) = false -> P deadlocks
D(P) = true -> P returns

It's the textbook proof and does not involve apps or arrays.