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. Director strings were introduced by F.-R. Sinot as a mechanism for for understanding and controlling the computational complexity cost of beta reduction.

Specifically, assume that a term takes the form

$f(t_{1},t_{2},\cdots ,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 free variables that may occur in the set of terms. The director is then the map

$\sigma _{t}:V\to P(\lbrace 1,2,\cdots ,n\rbrace )$

from the free variables to the power set $P(X)$ of the set $X=\lbrace 1,2,\cdots ,n\rbrace$. The values taken by $\sigma _{t}$ are simply a list of the indicies of the $t_{i}$ in which a given free variable occurs.