Director string
In mathematics, in the area of lambda calculus and computation, directors or director strings are a mechanism for keeping track of the free variables in a term. Loosely speaking, they can be understood as a kind of memoization for free variables; that is, as an optimization technique for rapidly locating the free variables in a term algebra or in a lambda expression. Director strings were introduced by Kennaway and Sleep in 1982 and further developed by Sinot, Fernández and Mackie[1] as a mechanism for understanding and controlling the computational complexity cost of beta reduction.
Motivation
In beta reduction, one defines the value of the expression on the left to be that on the right:
- or (Replace all x in E(body) by y)
While this is a conceptually simple operation, the computational complexity of the step can be non-trivial: a naive algorithm would scan the expression E for all occurrences of the free variable x. Such an algorithm is clearly O(n) in the length of the expression E. Thus, one is motivated to somehow track the occurrences of the free variables in the expression. One may attempt to track the position of every free variable, wherever it may occur in the expression, but this can clearly become very costly in terms of storage; furthermore, it provides a level of detail that is not really needed. Director strings suggest that the correct model is to track free variables in a hierarchical fashion, by tracking their use in component terms.
Definition
Consider, for simplicity, a term algebra, that is, a collection of free variables, constants, and operators which may be freely combined. Assume that a term t takes the form
where f is a function, of arity n, with no free variables, and the are terms that may or may not contain free variables. Let V denote the set of all free variables that may occur in the set of all terms. The director is then the map
from the free variables to the power set of the set . The values taken by are simply a list of the indices of the in which a given free variable occurs. Thus, for example, if a free variable occurs in and but in no other terms, then one has .
Thus, for every term in the set of all terms T, one maintains a function , and instead of working only with terms t, one works with pairs . Thus, the time complexity of finding the free variables in t is traded for the space complexity of maintaining a list of the terms in which a variable occurs.
General case
Although the above definition is formulated in terms of a term algebra, the general concept applies more generally, and can be defined both for combinatory algebras and for lambda calculus proper, specifically, within the framework of explicit substitution.
See also
References
- ^ Sinot, François-Régis; Fernández, Maribel; Mackie, Ian (2003), "Efficient reductions with director strings", in Nieuwenhuis, Robert (ed.), Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Valencia, Spain, June 9–11, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2706, Springer, pp. 46–60, doi:10.1007/3-540-44881-0_5
- F.-R. Sinot. "Director Strings Revisited: A Generic Approach to the Efficient Representation of Free Variables in Higher-order Rewriting." Journal of Logic and Computation 15(2), pages 201-218, 2005.
Content Disclaimer
Informasi ini disarikan dari Wikipedia dan disajikan kembali untuk tujuan edukasi. Konten tersedia di bawah lisensi CC BY-SA 3.0. Kami tidak bertanggung jawab atas ketidakakuratan data yang bersumber dari kontribusi publik tersebut.
- The information displayed on this website is sourced in part or in whole from Wikipedia and has been adapted for the purpose of restating it. We strive to provide accurate and relevant information, however:
- There is no guarantee of absolute accuracy. Wikipedia is an open, collaborative project that can be edited by anyone, so information is subject to change.
- It is not intended to constitute professional advice. The content displayed is for informational and educational purposes only. For important decisions (e.g., medical, legal, or financial), please consult a professional.
- Content copyright. Wikipedia is licensed under the Creative Commons Attribution-ShareAlike License (CC BY-SA). This means that content may be reused with appropriate attribution and shared under a similar license.
- Responsible use. Any risk arising from the use of information from this website is entirely the responsibility of the user.