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 cannot 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 |
Follow