Advice I received from a logic programming researcher concerning my own attempts to make a C++ logic programming library: "I think that a good model [...] is r

Advice I received from a logic programming researcher concerning my own attempts to make a C++ logic programming library: "I think that a good model [...] is rewriting not lambda calculus." Yet I still struggle to find a good way to integrate that as a DSL. The problem is that it is natural to use functions and lambdas of the host language to package usage of the DSL expressions, but that is a leaky abstraction: you need variables of the logic DSL to act nonlocally, yet you would like to be able to reason locally about branches of the full expression tree. These are mutually exclusive. For functional programming we want to treat the terms as values, but for non-local connections (same variable in two different subexpressions) we need variables to have semantics of pointers. And what of memory management...