Declarative catamorphism with meta-language escapes which can be used e.g. to solve for variable bindings in the codomain.

cata.pl

unescape(\X, X). % Subterms, and in particular logic variables, can be marked as pre-evaluated.

cata(Alg) --> unescape *-> {} ; mapargs(cata(Alg)), call(Alg).

% Example:

alg( 0 +  0,  0).
alg( 0 +  1,  1).
alg( 1 +  0,  1).
alg( 1 + 12, 13).
alg( 2 +  2,  4).
alg( 2 +  3,  5).
alg( 3 + 10, 13).
alg( 0 *  1,  0).
alg( 1 *  0,  0).
alg( 2 *  5, 10).
alg( 3 *  4, 12).

unify_images(Term1, Term2) :-
    cata(alg, Term1, Image),
    cata(alg, Term2, Image).

% ?- unify_images(alg, \X + \Y * (\Z + \Z), \Y + \Z * (\Z + \Y)).
% X = Y, Y = 1,
% Z = 0 ;
% X = 1,
% Y = 3,
% Z = 2 ;
% false.

unescape/2 is "semidet" (succeeding at most once), so the *-> (soft-cut) is equivalent to ->, but *-> makes the purity more obvious.