<<   >>

40. Halting Problem

The halting problem is the problem of determining, from a description of a program and an input, whether the program will finish running or continue to run forever. It was proved in the negative by Alonzo Church and Alan Turing in 1936, and can be rendered in Dyalog APL as follows:

Suppose there is an operator H such that f H ⍵ is 1 or 0 according to whether f ⍵ halts. Consider:

In Dfns

   f←{∇ H ⍵:∇ ⍵ ⋄ ⍬}

For f 0 , if ∇ H 0 is 1 , then ∇ 0 is invoked, leading to an infinite recursion, therefore ∇ H 0 should have been 0 . On the other hand, if ∇ H 0 is 0 , then the ⍬ part is invoked and is the result of f 0 , therefore ∇ H 0 should have been 1 .

Presented as a table: For f 0

suppose ∇ H 0 is invokes consequence ∇ H 0 should be
1 ∇ 0 infinite recursion 0
0 ⍬ f 0 results in ⍬ 1

Therefore, there can not be such an operator H.

In Tradfns

   ⎕fx 'f x' '→f H x'

For f 0

suppose f H 0 is invokes consequence f H 0 should be
1 →1     infinite loop    0
0 →0 f 0 exits 1


Appeared in [110].