You are right, a decoding function is needed. The decoding for my given encoding function is not computable because you need to look at all elements of the sequence to see if the rest are the padded zeros or part of the number (because there is a '1' somewhere). But here is a computable, surjective decoding function:
1. The first bit tells you whether the integer should be positive or negative.
2. Then we parse blocks of ten bits. The first bit tells you whether this block is part of the number ('1') or if we reached the end ('0'). If it is part of the number, then the next nine bits are part of the binary encoding of the integer.
This will not terminate for some sequences (for example the all '1' sequence), but it terminates for all sequences that denote integers. Wouldn't this encoding be valid?
(I don't know too much about the halting problem so I might well be wrong here).
> This is not at all what the `equal` function does.
Could you explain what it does do? The way I see it the `find` function constructs a counter-example lazily. The `p` predicate is then applied to this counter-example in `forsome`: `forsome p = p(find(\a -> p a))`. Only if the `p` predicate can determine if the counter-example is valid by looking at a finite amount of digits will the function terminate.
This will not terminate for some sequences (for example the all '1' sequence), but it terminates for all sequences that denote integers. Wouldn't this encoding be valid? (I don't know too much about the halting problem so I might well be wrong here).
> This is not at all what the `equal` function does.
Could you explain what it does do? The way I see it the `find` function constructs a counter-example lazily. The `p` predicate is then applied to this counter-example in `forsome`: `forsome p = p(find(\a -> p a))`. Only if the `p` predicate can determine if the counter-example is valid by looking at a finite amount of digits will the function terminate.