# Turing Completeness + Dataflow Unification = Arbitrarily invertible (pure, nonrecursive) functions?

Assume we are working in a Turing-complete, referentially-transparent, higher-order language that supports arbitrary dataflow unification. Shouldn't it then be possible to construct the following function (using Haskell-like syntax, because that's what I'm most familiar with)?

-- Takes an arbitrary pure function and constructs its inverse.
-- If the passed-in function is recursive, the result is not guaranteed to terminate
invert :: (a -> b) -> b -> a
invert f r = declare a in let r =|= f a in a


(if =|= is the dataflow unification operator).

Is this indeed possible in such a language? If so, why haven't people leapt at this before? If not, where did my reasoning go wrong?

• Could you make the question a little more self-contained? Can you provide a link or definition of dataflow unification? Also, the title mentions delimited continuations, but no definition is provided, nor is it clear to the uninitiated where these are used. – Dave Clarke Mar 23 '12 at 7:01
• @Dave Clarke Sorry, my thoughts were a bit unclear when I made the title, and I forgot to change it before I submitted. It has been corrected now. – Ptharien's Flame Mar 23 '12 at 23:25
• What about a link for dataflow unification? – Dave Clarke Mar 24 '12 at 3:48
• @Dave Clarke As defined in "Concepts, Techniques and Models of Computer Programming" by Peter Van Roy and Seif Haridi, under the name "incremental tell". I was surprisingly not able to find any online references. :( – Ptharien's Flame Mar 24 '12 at 4:44
• The point I'm trying to make is that your question would be much better if it were more self-contained, and had a link to such a definition of the definition included in the question. – Dave Clarke Mar 24 '12 at 7:56

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.

• Awesome! And, just so I'm clear on this, how does this play against the general unsolvability of the Halting Problem? – Ptharien's Flame Mar 23 '12 at 23:21
• The halting problem can be encoded in the following way: define a function halts_in_n_steps(n). This function simulates a chosen Turing machine for n steps, and then returns whether it halted yet or not. The halting problem is computing inverse(halts_in_n_steps, true). The invert function will be able to invert that function if there is an n such that halts_in_n_steps(n) is true, but otherwise it will loop indefinitely. Unfortunately, invert is not magic ;) – Jules Mar 23 '12 at 23:39

Dataflow unification behaves as you expect on first-order data (numbers, booleans, lists, trees, etc.) but can fail for higher-order data such as functions. In general, unifying functions requires using full higher-order unification, which has terrible performance, up to and including frequent failure to terminate (as it must, since otherwise it would solve the halting problem).

Higher-order logic languages such as $\lambda$-Prolog and Curry typically use restricted forms of higher-order unification, to get better efficiency at the price of completeness.