Don't Implement Unification by Recursion

I find the prevailing use of “recursion”, i.e. β-reduction all the way to ground terms, to be an impoverished sense of the term.

By all means, you should be familiar with the evaluation semantics of your runtime environment. If you don’t know the search depth of your input or can’t otherwise constrain stack height beforehand beware the specter of symbolic recursion, but recursion is so much more.

Functional reactive programs do not suffer from stack-overflow on recursion (implementation details notwithstanding). By Church-Turing every sombolic-recursive function can be translated to a looped iteration over some memoization of intermeduate results. The stack is just a special case of such memoization. Popular functional programming patterns provide other bottled up memoization strategies: Fold/Reduce, map/zip/join, either/amb/cond the list goes on (heh). Your iterating loop is still traversing the solution space in a recursive manner, provided you dot your ‘i’s and carry your remainders correctly.

Heck, any feedback circuit is essentially recursive and I have never seen an IIR-filter blow the stack (by itself, mind you).

> It is somewhat surprising that unification is cleaner and easier to implement in an loopy imperative mutational style than in a recursive functional pure style.

I came to a similar conclusion, my implementation uses recursion but also leans on shared mutable variables, which is something I usually avoid especially for more "mathy" code. https://jasonhpriestley.com/short-simple-unification

I want to disagree, but honestly the recursive method I tend to use is almost isomorphic to a loop + stack/deque. Eager elimination of `x=t` pairs, or eager normalization of substitutions sounds potentially inefficient, imho it's better to check that on the fly upon selecting a pair.

When you study the old AI programming you eventually realize that non-determinism rules and recursion drools. Recursion is great for certain things that would be hard otherwise (drawing fractals) but it shouldn’t be the first tool you reach for. It’s known to be dangerous in embedded systems because it can blow out the stack. Turns very simple O(N) problems into O(N^2) but unfortunately a generation of computer science pedagogues taught people that recursion > iteration because BASIC was the teaching language of the 1970s and first half of the 1980s and they couldn’t get over that Lisp, Forth, UCSD Pascal and other contenders didn’t make it to the finish.

Unification, etc, is one of the good use cases of the so-called Tardis monad.

> Unification has too much spooky action at a distance, a threaded state

Isn’t this why we have the State monad, or even just fold-like functions? There are multiple ways to tame this problem without resorting to mutable state and side-effects. We know how that deal with the devil usually turns out.

(And I have no idea what "spooky action at a distance" means in this context. If anything, functional programming eliminates such shenanigans by expressing behavior clearly in the type system.)

I get that some mediocre programmers don't understand recursion. But telling other programmers to work with inferior methods, which are harder to understand and maintain is a sin. He is wrong of course. Do implement unification with recursion.

>It is somewhat surprising that unification is cleaner and easier to implement in an loopy imperative mutational style than in a recursive functional pure style. Typically theorem proving / mathematical algorithms are much cleaner in the second style in my subjective opinion.

This is the Curry–Howard correspondence.

While it seems everyone wants to force individuals into one of the formal vs constructivist, it is best to have both in your toolbox.

Contex and personal preference and ability apply here, but in general it is easier for us mortals to use the constructivist approach when programming.

This is because, by simply choosing to not admit PEM a priori, programs become far more like constructive proofs.

If you look at the similarities between how Church approached the Entscheidungsproblem, the equivalence of TM and lambda calculus, the implications of Post's theorm and an assumption of PEM, it will be clear that the formalist approach demands much more of the programmer.

Functional programming grew out of those proofs-as-programs concepts, so if you prefer functional styles, the proofs are the program you write.

Obviously the above has an absurd amount of oversimplification, but I am curious what would have been different if one had started with more intuitional forms of Unification.

For me, I would have probably just moved to the formalist model to be honest like the author.

I just wanted to point out there is a real reason many people find writing algorithms in a functional/constructivist path.

I live by "don't recurse, iterate". Don't get me wrong, recursion seems really clever, if you live in a universe with an infinite stack.