There is an even simpler definition of invert that works for all countable domains a, no exotic execution models needed:
invert(f,y) =
for each x in a:
if f(x) == y: return x
For example if the domain a consists of all binary trees, you have to have a method for enumerating binary trees. Functional logic languages are basically an optimization of the above method. They use lazy backtracking search over a instead of naive brute force search. Unfortunately, the preceding is not strictly true. The execution engines of some functional logic languages can get stuck in an infinite portion of the search space, which means that their invert will not terminate for all inputs.
Contrary to popular belief, the preceding algorithm works even for higher order data. On first sight, this would seem to be impossible, because a function domain is not countable. For example the domain int -> int. However, terminating programs can only invoke a function finitely many times. In other words, the continuation of g = invert(f,y) can only invoke g finitely many times. So if there is a function that would be a valid choice for g, there also is a finite function that is a valid choice for g, namely the function that only works on the values that the rest of the program actually calls it on. So in fact we only have to search over all finite functions, and this is a countable domain! Just represent a function as a finite list of (input,output) pairs, and when calling such a function with an input that's not in the list, backtrack back into the loop and continue with the next finite function (this jumping back into the loop can be done with continuations).
Rephrased so that it may be easier to understand: if there is no finite function that does it, then there is also no infinite function that does it, because the only way to observe the difference between a finite and an infinite function is to call it infinitely many times, which would mean that the program didn't terminate in the first place.
Note that, as a special case, we can also invert functions on infinite lazy data structures. And as a special case of this, we have Seemingly impossible functional programs. As you can see, in some sense, it is easier to invert a function on a domain containing infinitely large values than on a domain containing finite values! For instance we can compute an inverse on the domain (int -> bool) -> bool or detect that such an inverse does not exist in finite time, whereas we cannot detect for an arbitrary function of int -> int that it is not invertible at, say, y = 3. So in some sense, the space of all integers is harder to search than the space of all functions int -> bool! Not despite, but because the latter contains infinitely large objects.
