Director de cadena

En matemáticas , en el área del cálculo y computación lambda , los directores o cadenas de directores 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 para las 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 coste de complejidad computacional de la reducción beta .

Motivación

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

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

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 en busca de todas las ocurrencias 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 ocurrencias de las variables libres en la expresión. Uno puede intentar rastrear la posición de cada variable libre, donde sea que pueda ocurrir en la expresión, pero esto puede volverse claramente 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

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 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 la función ${\displaystyle t_{i}}$

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

de las variables libres al conjunto potencia del conjunto . Los valores tomados por son simplemente una lista de los índices de en los que aparece una variable libre dada. Así, por ejemplo, si una variable libre aparece en y pero en ningún otro término, 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 }$

De este modo, para cada término del conjunto de todos los términos T , se mantiene una función , y en lugar de trabajar sólo con términos t , se trabaja con pares . 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. ${\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 á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 .

Véase también

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

Referencias

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

• F.-R. Sinot. "Director Strings Revisited: A Generic Approach to the Efficient Representation of Free Variables in Higher-Orden Rewriting" ( Revista de lógica y computación, 15 (2), páginas 201-218, 2005).