Director string

From Wikipedia, the free encyclopedia

This article may not meet the general notability guideline or one of the following specific guidelines for inclusion on Wikipedia: Biographies, Books, Companies, Fiction, Music, Neologisms, Numbers, Web content, or several proposals for new guidelines. If you are familiar with the subject matter, please expand or rewrite the article to establish its notability. The best way to address this concern is to reference published, third-party sources about the subject. If notability cannot be established, the article is more likely to be considered for redirection, merge or ultimately deletion, per Wikipedia:Guide to deletion.
This article has been tagged since June 2008.

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 Sinot, Fernández and Mackie ^[1] as a mechanism for understanding and controlling the computational complexity cost of beta reduction.

1 Motivation
2 Definition
3 General case
4 See also
5 References

[edit] Motivation

In beta reduction, one defines the value of the expression on the left to be that on the right:

$(\lambda x.E)y \equiv E[x:= 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, where-ever it may occur in the expression, but this can clearly become very costly in terms of storage; furthermore, it provides a 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.

[edit] 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

$t ::= f(t_1,t_2,\dots,t_n)$

where f is a function, of arity n, with no free variables, and the $t i$ 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

$\sigma_t: V\to P(\lbrace 1,2,\dots,n\rbrace)$

from the free variables to the power set $P (X)$ of the set $X=\lbrace 1,2,\dots,n\rbrace$ . The values taken by $σ t$ are simply a list of the indices of the $t i$ in which a given free variable occurs. Thus, for example, if a free variable $x\in V$ occurs in $t 3$ and $t 5$ but in no other terms, then one has $σ t (x) = {3,5}$ .

Thus, for every term $t\in T$ in the set of all terms T, one maintains a function $σ t$ , and instead of working only with terms t, one works with pairs $(t,σ t)$ . 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.

[edit] 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.

[edit] See also

Term rewrite system
Explicit substitution
Combinatory reduction system

[edit] References

^ F.-R. Sinot, M. Fernández and I. Mackie. Efficient Reductions with Director Strings. In Proc. Rewriting Techniques and Applications. Springer LNCS vol 2706, 2003