Cadena de directores

En matemáticas , en el área del cálculo lambda y la computación , los directores o cadenas de directores son un mecanismo para mantener el seguimiento de las variables libres en un término . En términos generales, pueden entenderse como una especie de memorización para variables libres; es decir, como una técnica de optimización para localizar rápidamente las variables libres en un álgebra de términos o en una expresión lambda. Las cadenas de directores fueron introducidas por Kennaway y Sleep en 1982 y desarrolladas posteriormente por Sinot, Fernández y Mackie ^{[ 1 ]} como un mecanismo para comprender y controlar el costo de complejidad computacional de la reducción beta .

En la reducción beta, se define el valor de la expresión de la izquierda como el de la derecha:

${\displaystyle (\lambda xE)y\equiv E[x:=y]\,}$o${\displaystyle (\lambda xE)y\equiv E[y/x]}$ (Reemplazar todas las x en E (cuerpo) por y )

Aunque conceptualmente se trata de una operación sencilla, la complejidad computacional del paso puede ser considerable: un algoritmo ingenuo buscaría en la expresión E todas las ocurrencias de la variable libre x . Dicho algoritmo tiene una complejidad de O ( n ) respecto a la longitud de la expresión E. Por lo tanto, resulta necesario rastrear de alguna manera las ocurrencias de las variables libres en la expresión. Se podría intentar rastrear la posición de cada variable libre, independientemente de dónde aparezca en la expresión, pero esto puede resultar muy costoso en términos de almacenamiento; además, proporciona un nivel de detalle innecesario. Las cadenas de directores sugieren que el modelo correcto consiste en rastrear las variables libres de forma jerárquica, registrando su uso en términos de componentes.

Consideremos, para simplificar, un álgebra de términos , es decir, una colección de variables libres, constantes y operadores que pueden combinarse libremente. Supongamos que un término t toma la forma

${\displaystyle t::=f(t_{1},t_{2},\dots ,t_{n})}$

donde f es una función de aridad n , sin variables libres , y la${\displaystyle t_{i}}$son términos que pueden o no contener variables libres. Sea V el conjunto de todas las variables libres que pueden aparecer en el conjunto de todos los términos. El director es entonces el mapa

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

desde las variables libres hasta el conjunto potencia${\displaystyle P(X)}$del conjunto${\displaystyle X=\lbrace 1,2,\dots ,n\rbrace }$. Los valores tomados por${\displaystyle \sigma _{t}}$son simplemente una lista de los índices de los${\displaystyle t_{i}}$en la que aparece una variable libre determinada. Por lo tanto, por ejemplo, si una variable libre${\displaystyle x\in V}$ocurre en${\displaystyle t_{3}}$y${\displaystyle t_{5}}$pero en ningún otro término, entonces uno tiene${\displaystyle \sigma _{t}(x)=\lbrace 3,5\rbrace }$.

Por lo tanto, para cada término${\displaystyle t\in T}$En el conjunto de todos los términos T , se mantiene una función${\displaystyle \sigma _{t}}$y en lugar de trabajar solo con términos t , se trabaja con pares${\displaystyle (t,\sigma _{t})}$De este modo, la complejidad temporal de encontrar las variables libres en t se intercambia por la complejidad espacial de mantener una lista de los términos en los que aparece una variable.

Aunque la definición anterior está formulada en términos de un álgebra de términos , el concepto general se aplica de manera más general y puede definirse tanto para álgebras combinatorias como para el cálculo lambda propiamente dicho, específicamente, dentro del marco de la sustitución explícita .

• Sistema de reescritura de términos
• Sustitución explícita
• Memorización

• 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), páginas 201-218, 2005.