Director Strings Revisited: A Generic Approach to the Efficient Representation of Free Variables in Higher-order Rewriting

摘要

The representation of free variables is crucial for the efficiency of the implementation of various kinds of rewrite systems. We give an innovative, although very natural, representation of variables abstract enough to fit in many different frameworks and more satisfactory from an operational perspective than usual representations. This work also provides a generalization of director strings for the λ-calculus.