[discarded1023]

I can't speak to the point of doing this, but (IIRC/IIUC) you're talking paths and they're talking the entire computation tree, i.e., a term in their calculus represents all solutions, and computing normal forms makes them easy to read off (?). Perhaps there's some meat in how they handle the equivalent of `bagof/3`/`setof/3`.