cadena de director

En matemáticas , en el área del cálculo y la computación lambda , los directores o cadenas directoras son un mecanismo para realizar un seguimiento de las variables libres en un término . En términos generales, pueden entenderse como una especie de memorización de variables libres; es decir, como 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 directoras fueron introducidas por Kennaway y Sleep en 1982 y desarrolladas aún más por Sinot, Fernández y Mackie ^[1] como un mecanismo para comprender y controlar el costo de complejidad computacional de la reducción beta .

Motivación

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

${\displaystyle (\lambda x.E)y\equiv E[x:=y]\,}$o (Reemplace todo x en E (cuerpo) por y ) ${\displaystyle (\lambda x.E)y\equiv E[y/x]}$

Si bien se trata de una operación conceptualmente simple, la complejidad computacional del paso puede no ser trivial: un algoritmo ingenuo escanearía la expresión E en busca de todas las apariciones de la variable libre x . Tal algoritmo es claramente O ( n ) en la longitud de la expresión E. Por lo tanto, uno está motivado a rastrear de alguna manera las apariciones de las variables libres en la expresión. Se puede intentar rastrear la posición de cada variable libre, dondequiera que aparezca en la expresión, pero esto claramente puede resultar muy costoso en términos de almacenamiento; además, proporciona un nivel de detalle que realmente no es necesario. Las cadenas directoras sugieren que el modelo correcto es rastrear las variables libres de forma jerárquica, rastreando su uso en términos de componentes.

Definición

Consideremos, por simplicidad, un término álgebra , es decir, una colección de variables, constantes y operadores libres 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 son términos que pueden contener o no 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 t_{i}}$

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

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

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

Caso general

Aunque la definición anterior está formulada en términos de un término álgebra , 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 .

Ver también

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

Referencias

1. F.-R. Sinot, M. Fernández y I. Mackie. Reducciones eficientes con Director Strings. En Proc. Técnicas y aplicaciones de reescritura . Springer LNCS vol 2706, 2003

• F.-R. Sinot. "Director Strings revisitado: un enfoque genérico para la representación eficiente de variables libres en la reescritura de orden superior". Revista de Lógica y Computación 15 (2), páginas 201-218, 2005.