> Here's an example when the function fails to terminate:
I figured this seemed too good to be true. In fact, isn't there a simple reduction to the halting problem? Make a "sequence"
i -> M halts in i steps
for an arbitrary Turing Machine `M`. You can implement the "bit lookups" by simulating `M`. The author says their Swift code can run `anySatisfy` on this "sequence" in finite time, right?
EDIT: quoted at the top, but afaict not mentioned later, the article says,
>> It is well known that it is impossible to define equality between arbitrary functions. However, there is a large class of functions for which we can determine equality
It would have been nice if the author had been explicit about the class of functions for which their program terminates.
It works for any decidable/recursive predicate on bit sequences, i.e. one that is guaranteed to halt for any input.
`and` on an infinite bit sequence is not guaranteed to halt because it is co-recursively enumerable, i.e. it will reject bit sequences that contain `False`, but it will not halt on bit sequences that contain only `True`, since to verify that a bit sequence only contains `True`, you have to check all elements of the sequence.
In ghci,
> and $ repeat True
<doesn't terminate>
> and $ (replicate 10000 True) ++ (False: repeat True)
False
I noticed my post missed the point a bit... I was thinking about functions that check properties of bit sequences, not functions that check properties of predicates on bit sequences.
I get how it works now, thanks. Wish I could edit/delete my old post :-/.
Just to check my understanding: a terminating program that decides bit sequences will have
- a maximum number of bit checks it will make regardless of input, and
- a maximum bit index it will access regardless of input, and even
I figured this seemed too good to be true. In fact, isn't there a simple reduction to the halting problem? Make a "sequence"
for an arbitrary Turing Machine `M`. You can implement the "bit lookups" by simulating `M`. The author says their Swift code can run `anySatisfy` on this "sequence" in finite time, right?EDIT: quoted at the top, but afaict not mentioned later, the article says,
>> It is well known that it is impossible to define equality between arbitrary functions. However, there is a large class of functions for which we can determine equality
It would have been nice if the author had been explicit about the class of functions for which their program terminates.