En las matemáticas , en el área de cálculo lambda y computación , directores o cadenas director son un mecanismo para el seguimiento de las variables libres en un plazo . En términos generales, pueden entenderse como una especie de memorización de variables libres; es decir, como una técnica de optimización para localizar rápidamente las variables libres en un término álgebra o en una expresión lambda. Las cadenas de director fueron introducidas por Kennaway y Sleep en 1982 y desarrolladas por Sinot, Fernández y Mackie [1] como un mecanismo para comprender y controlar lacosto de complejidad computacional de la reducción beta .
Motivación
En la reducción beta, se define el valor de la expresión de la izquierda como el de la derecha:
- o (Reemplazar todas las x en E (cuerpo) por y )
Si bien esta es una operación conceptualmente simple, la complejidad computacional del paso puede no ser trivial: un algoritmo ingenuo escanearía la expresión E para todas las apariciones de la variable libre x . Dicho algoritmo es claramente O ( n ) en la longitud de la expresión E . Por lo tanto, uno está motivado para rastrear de alguna manera las ocurrencias de las variables libres en la expresión. Se puede intentar rastrear la posición de cada variable libre, dondequiera que ocurra 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 de director sugieren que el modelo correcto es rastrear las variables libres de manera jerárquica, rastreando su uso en términos de componentes.
Definición
Considere, por simplicidad, un término álgebra , es decir, una colección de variables libres, constantes y operadores que pueden combinarse libremente. Suponga que un término t toma la forma
donde f es una función , de aridad n , sin variables libres , y elson 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
de las variables libres al conjunto de potencia del set . Los valores tomados por son simplemente una lista de los índices del en el que se produce una determinada variable libre. Así, por ejemplo, si una variable libre ocurre en y pero en ningún otro término, entonces uno tiene .
Por lo tanto, 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 intercambia por la complejidad espacial de mantener una lista de los términos en los que ocurre una variable.
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
Referencias
- ^ F.-R. Sinot, M. Fernández e I. Mackie. Reducciones eficientes con cadenas de director . En Proc. Técnicas y aplicaciones de reescritura . Springer LNCS vol 2706, 2003
- F.-R. Sinot. " Director Strings Revisited: Un enfoque genérico para la representación eficiente de variables libres en la reescritura de orden superior " . Journal of Logic and Computation 15 (2), páginas 201-218, 2005.