Director string
Encyclopedia
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
. Director strings were introduced by Kennaway and Sleep in 1982 and further developed by Sinot, Fernández and Mackie as a mechanism for understanding and controlling the computational complexity
cost of beta reduction.
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.
, 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.
, 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
.
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
, in the area of lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
and computation
Computation
Computation is defined as any type of calculation. Also defined as use of computer technology in Information processing.Computation is a process following a well-defined model understood and expressed in an algorithm, protocol, network topology, etc...
, directors or director strings are a mechanism for keeping track of the free variables in a term
Expression (mathematics)
In mathematics, an expression is a finite combination of symbols that is well-formed according to rules that depend on the context. Symbols can designate numbers , variables, operations, functions, and other mathematical symbols, as well as punctuation, symbols of grouping, and other syntactic...
. Director strings were introduced by Kennaway and Sleep in 1982 and further developed by Sinot, Fernández and Mackie as a mechanism for understanding and controlling the computational complexity
Computational Complexity
Computational Complexity may refer to:*Computational complexity theory*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:While this is a conceptually simple operation, the computational complexity
Computational Complexity
Computational Complexity may refer to:*Computational complexity theory*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 algebraTerm algebra
In universal algebra and mathematical logic, a term algebra is a freely generated algebraic structure over a given signature. For example, in a signature consisting of a single binary operation, the term algebra over a set X of variables is exactly the free magma generated by X...
, 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
Function (mathematics)
In mathematics, a function associates one quantity, the argument of the function, also known as the input, with another quantity, the value of the function, also known as the output. A function assigns exactly one output to each input. The argument and the value may be real numbers, but they can...
, of arity
Arity
In logic, mathematics, and computer science, the arity of a function or operation is the number of arguments or operands that the function takes. The arity of a relation is the dimension of the domain in the corresponding Cartesian product...
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 mapfrom 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 algebraTerm algebra
In universal algebra and mathematical logic, a term algebra is a freely generated algebraic structure over a given signature. For example, in a signature consisting of a single binary operation, the term algebra over a set X of variables is exactly the free magma generated by X...
, the general concept applies more generally, and can be defined both for combinatory algebras and for lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
proper, specifically, within the framework of explicit substitution
Explicit substitution
In computer science, lambda calculi are said to have explicit substitutions if they pay special attention to the formalization of the process of substitution. This is in contrast to the standard lambda calculus where substitutions are performed by beta reductions in an implicit manner which is not...
.
See also
- Term rewrite system
- Explicit substitutionExplicit substitutionIn computer science, lambda calculi are said to have explicit substitutions if they pay special attention to the formalization of the process of substitution. This is in contrast to the standard lambda calculus where substitutions are performed by beta reductions in an implicit manner which is not...
- Combinatory reduction system
- MemoizationMemoizationIn computing, memoization is an optimization technique used primarily to speed up computer programs by having function calls avoid repeating the calculation of results for previously processed inputs...