Estrategia de reducción

En reescritura , una estrategia de reducción o estrategia de reescritura es una relación que especifica una reescritura para cada objeto o término, compatible con una relación de reducción dada. ^[1] Algunos autores usan el término para referirse a una estrategia de evaluación . ^[2]^[3]

Definiciones

Formalmente, para un sistema de reescritura abstracto , una estrategia de reducción es una relación binaria en con , donde es el cierre transitivo de (pero no el cierre reflexivo). ^[1] Además, las formas normales de la estrategia deben ser las mismas que las formas normales del sistema de reescritura original, es decir, para todo , existe un con si y solo si . ^[4] $(A,\to )$ $\to_{S}$ ${\estilo de visualización A}$ $\to _{S}\subseteq {\overset {+}{\to }}$ ${\overset {+}{\to }}$ $\to$ ${\estilo de visualización a}$ ${\estilo de visualización b}$ $a\to b$ $\existe b'.a\to _{S}b'$

Una estrategia de reducción de un paso es aquella en la que . De lo contrario, es una estrategia de muchos pasos . ^[5] $\to _{S}\subseteq \to$

Una estrategia determinista es aquella donde es una función parcial , es decir, para cada hay como máximo uno tal que . De lo contrario, es una estrategia no determinista . ^[5] $\to_{S}$ $a\en A$ ${\estilo de visualización b}$ $a\to_{S}b$

Reescritura de términos

En un sistema de reescritura de términos, una estrategia de reescritura especifica, de todos los subtérminos reducibles ( redexes ), cuál debe reducirse ( contraerse ) dentro de un término.

Las estrategias de un solo paso para la reescritura de términos incluyen: ^[5]

más a la izquierda-más interno: en cada paso se contrae el más a la izquierda de los redexes más internos, donde un redex más interno es un redex que no contiene ningún redexe ^[6]
más a la izquierda-más externo: en cada paso se contrae el más a la izquierda de los redexes más externos, donde un redex más externo es un redex que no está contenido en ningún redexe ^[6]
más a la derecha-más interior, más a la derecha-más exterior: de manera similar

Las estrategias de varios pasos incluyen: ^[5]

Paralelo-más interno: reduce todos los redexes más internos simultáneamente. Esto está bien definido porque los redexes son disjuntos por pares.
Paralelo-externo: de manera similar
Reducción de Gross-Knuth, ^[7] también llamada sustitución completa o reducción de Kleene: ^[5] todos los redexes en el término se reducen simultáneamente

La reducción paralela más externa y la reducción de Gross-Knuth son hipernormalizadoras para todos los sistemas de reescritura de términos casi ortogonales, lo que significa que estas estrategias eventualmente alcanzarán una forma normal si existe, incluso cuando se realizan (un número finito) de reducciones arbitrarias entre aplicaciones sucesivas de la estrategia. ^[8]

Stratego es un lenguaje de dominio específico diseñado específicamente para programar estrategias de reescritura de términos. ^[9]

Cálculo lambda

En el contexto del cálculo lambda , la reducción de orden normal se refiere a la reducción más a la izquierda-más a la externa en el sentido dado anteriormente. ^[10] La reducción de orden normal es normalizadora, en el sentido de que si un término tiene una forma normal, entonces la reducción de orden normal eventualmente lo alcanzará, de ahí el nombre normal. Esto se conoce como el teorema de estandarización. ^[11]^[12]

La reducción más a la izquierda se utiliza a veces para referirse a la reducción de orden normal, ya que con un recorrido en preorden las nociones coinciden, y de manera similar, el redex más a la izquierda-externo es el redex con el carácter inicial más a la izquierda cuando el término lambda se considera como una cadena de caracteres. ^[13]^[14] Cuando "más a la izquierda" se define utilizando un recorrido en orden, las nociones son distintas. Por ejemplo, en el término con definido aquí , el redex más a la izquierda del recorrido en orden es mientras que el redex más a la izquierda-externo es la expresión completa. ^[15] $(\lambda xx\Omega )(\lambda yI)$ $\Omega,I$ ${\estilo de visualización \Omega}$

La reducción de orden aplicativa se refiere a la reducción más a la izquierda-más al interior. ^[10] A diferencia del orden normal, la reducción de orden aplicativa puede no terminar, incluso cuando el término tiene una forma normal. ^[10] Por ejemplo, utilizando la reducción de orden aplicativa, es posible la siguiente secuencia de reducciones: ${\begin{aligned}&(\mathbf {\lambda } xz)((\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda xz)((\lambda w.www)(\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda xz)((\lambda w.www)(\lambda w.www)(\lambda w.www))\\\rightarrow &(\lambda xz)((\lambda w.www)(\lambda w.www)(\lambda w.www)(\lambda w.www))\\&\ldots \end{aligned}}$

Pero utilizando la reducción de orden normal, el mismo punto de partida se reduce rápidamente a la forma normal: $(\mathbf {\lambda } xz)((\lambda w.www)(\lambda w.www))$ $\flecha derecha z$

La β-reducción completa se refiere a la estrategia no determinista de un solo paso que permite reducir cualquier redex en cada paso. ^[3]La β-reducción paralela de Takahashi es la estrategia que reduce todos los redexes en el término simultáneamente. ^[16]

Reducción débil

La reducción de orden normal y aplicativa son fuertes en el sentido de que permiten la reducción bajo abstracciones lambda. En contraste, la reducción débil no reduce bajo una abstracción lambda. ^[17] La reducción de llamada por nombre es la estrategia de reducción débil que reduce el redex más externo a la izquierda que no está dentro de una abstracción lambda, mientras que la reducción de llamada por valor es la estrategia de reducción débil que reduce el redex más interno a la izquierda que no está dentro de una abstracción lambda. Estas estrategias se idearon para reflejar las estrategias de evaluación de llamada por nombre y llamada por valor . ^[18] De hecho, la reducción de orden aplicativa también se introdujo originalmente para modelar la técnica de paso de parámetros de llamada por valor que se encuentra en Algol 60 y los lenguajes de programación modernos. Cuando se combina con la idea de reducción débil, la reducción de llamada por valor resultante es de hecho una aproximación fiel. ^[19]

Desafortunadamente, la reducción débil no es confluente, ^[17] y las ecuaciones de reducción tradicionales del cálculo lambda son inútiles, porque sugieren relaciones que violan el régimen de evaluación débil. ^[19] Sin embargo, es posible extender el sistema para que sea confluente al permitir una forma restringida de reducción bajo una abstracción, en particular cuando el redex no involucra la variable limitada por la abstracción. ^[17] Por ejemplo, λ x .(λ y . x ) z está en forma normal para una estrategia de reducción débil porque el redex (λ y . x ) z está contenido en una abstracción lambda. Pero el término λ x .(λ y . y ) z todavía se puede reducir bajo la estrategia de reducción débil extendida, porque el redex (λ y . y ) z no se refiere a x . ^[20]

Reducción óptima

La reducción óptima está motivada por la existencia de términos lambda donde no existe una secuencia de reducciones que los reduzca sin duplicar el trabajo. Por ejemplo, considere

((λg.(g(g(λx.x)))) (λh.((λf.(f(f(λz.z)))) (λw.(h(w(λy.y)))))))

Está compuesta por tres términos anidados, x=((λg. ... ) (λh.y)) , y=((λf. ...) (λw.z) ) y z=λw.(h(w(λy.y))) . Aquí sólo hay dos posibles β-reducciones que se pueden hacer, en x y en y. Reducir primero el término x externo da como resultado que el término y interno se duplique, y cada copia tendrá que ser reducida, pero reducir primero el término y interno duplicará su argumento z, lo que hará que el trabajo se duplique cuando se den a conocer los valores de h y w. ^[a]

La reducción óptima no es una estrategia de reducción para el cálculo lambda en sentido estricto, ya que al realizar la β-reducción se pierde la información sobre los redexes sustituidos que se comparten. En cambio, se define para el cálculo lambda etiquetado , un cálculo lambda anotado que captura una noción precisa del trabajo que se debe compartir. ^[21]^{: 113–114}

Las etiquetas consisten en un conjunto infinito numerable de etiquetas atómicas y concatenaciones , líneas superiores e inferiores de etiquetas. Un término etiquetado es un término de cálculo lambda donde cada subtérmino tiene una etiqueta. El etiquetado inicial estándar de un término lambda le da a cada subtérmino una etiqueta atómica única. ^[21]^{: 132} La β-reducción etiquetada viene dada por: ^[22] ${\estilo de visualización ab}$ ${\overline {a}}$ ${\underline {a}}$ $((\lambda xM)^{\alpha }N)^{\beta }\to \beta {\overline {\alpha }}\cdot M[x\mapsto {\underline {\alpha }}\cdot N]$

donde concatena etiquetas, , y la sustitución se define de la siguiente manera (usando la convención de Barendregt ): ^[22] Se puede demostrar que el sistema es confluente. La reducción óptima se define entonces como orden normal o reducción más a la izquierda-más externa usando reducción por familias, es decir, la reducción paralela de todos los redexes con la misma etiqueta de parte de función. ^[23] La estrategia es óptima en el sentido de que realiza el número óptimo (mínimo) de pasos de reducción de familia. ^[24] ${\estilo de visualización \cdot}$ $\beta \cdot T^{\alpha }=T^{\beta \alpha }$ $M[x\mapsto N]$ ${\begin{aligned}x^{\alpha }[x\mapsto N]&=\alpha \cdot N&\quad (\lambda yM)^{\alpha }[x\mapsto N]&=(\lambda yM[x\mapsto N])^{\alpha }\\y^{\alpha }[x\mapsto N]&=y^{\alpha }&\quad (MN)^{\alpha }[x\mapsto P]&=(M[x\mapsto P]N[x\mapsto P])^{\alpha }\end{aligned}}$

Un algoritmo práctico para la reducción óptima se describió por primera vez en 1989, ^[25] más de una década después de que la reducción óptima se definiera por primera vez en 1974. ^[26] La máquina óptima de orden superior de Bolonia (BOHM) es una implementación prototipo de una extensión de la técnica a las redes de interacción . ^[21]^{: 362}^[27] Lambdascope es una implementación más reciente de reducción óptima, que también utiliza redes de interacción. ^[28]^[b]

Llamada por reducción de necesidad

La reducción por llamada por necesidad se puede definir de manera similar a la reducción óptima como una reducción débil de extremo izquierdo a extremo utilizando una reducción paralela de redexes con la misma etiqueta, para un cálculo lambda etiquetado ligeramente diferente. ^[17] Una definición alternativa cambia la regla beta a una operación que encuentra el siguiente cálculo "necesario", lo evalúa y sustituye el resultado en todas las ubicaciones. Esto requiere extender la regla beta para permitir la reducción de términos que no son sintácticamente adyacentes. ^[29] Al igual que con la llamada por nombre y la llamada por valor, la reducción por llamada por necesidad se ideó para imitar el comportamiento de la estrategia de evaluación conocida como "llamada por necesidad" o evaluación perezosa .

Véase también

Notas

^ Por cierto, el término anterior se reduce a la función identidad (λy.y) , y se construye creando envoltorios que hacen que la función identidad esté disponible para los enlazadores g=λh... , f=λw... , h = λx.x (al principio) y w=λz.z (al principio), todos los cuales se aplican al término más interno λy.y.
^ Un resumen de investigaciones recientes sobre reducción óptima se puede encontrar en el breve artículo Acerca de la reducción eficiente de términos lambda.

Referencias

^ ab Kirchner, Hélène (26 de agosto de 2015). "Reescritura de estrategias y programas de reescritura estratégica". En Martí-Oliet, Narciso; Ölveczky, Peter Csaba; Talcott, Carolyn (eds.). Lógica, reescritura y concurrencia: ensayos dedicados a José Meseguer con motivo de su 65.º cumpleaños. Springer. ISBN 978-3-319-23165-5. Recuperado el 14 de agosto de 2021 .
^ Selinger, Peter; Valiron, Benoît (2009). "Cálculo lambda cuántico" (PDF) . Técnicas semánticas en computación cuántica : 23. doi :10.1017/CBO9781139193313.005. ISBN 9780521513746. Recuperado el 21 de agosto de 2021 .
^ ab Pierce, Benjamin C. (2002). Tipos y lenguajes de programación. MIT Press . p. 56. ISBN 0-262-16209-1.
^ Klop, Jan Willem; van Oostrom, Vicente; van Raamsdonk, Femke (2007). «Estrategias de reducción y aciclicidad» (PDF) . Reescritura, Computación y Prueba . Apuntes de conferencias sobre informática. vol. 4600, págs. 89-112. CiteSeerX 10.1.1.104.9139 . doi :10.1007/978-3-540-73147-4_5. ISBN 978-3-540-73146-7.
^ abcde Klop, JW "Term Rewriting Systems" (PDF) . Documentos de Nachum Dershowitz y estudiantes . Universidad de Tel Aviv. p. 77 . Consultado el 14 de agosto de 2021 .
^ ab Horwitz, Susan B. "Cálculo Lambda". Notas de CS704 . Universidad de Wisconsin Madison . Consultado el 19 de agosto de 2021 .
^ Barendregt, HP; Eekelen, MCJD; Glauert, JRW; Kennaway, JR; Plasmeijer, MJ; Dormir, MR (1987). Reescritura de gráficos de términos . Arquitecturas y lenguajes paralelos Europa. vol. 259, págs. 141-158. doi :10.1007/3-540-17945-3_8.
^ Antoy, Sergio; Middeldorp, Aart (septiembre de 1996). "Una estrategia de reducción secuencial" (PDF) . Theoretical Computer Science . 165 (1): 75–95. doi :10.1016/0304-3975(96)00041-2 . Consultado el 8 de septiembre de 2021 .
^ Kieburtz, Richard B. (noviembre de 2001). "Una lógica para reescribir estrategias". Notas electrónicas en informática teórica . 58 (2): 138–154. doi : 10.1016/S1571-0661(04)00283-X .
^ abc Mazzola, Guerino; Milmeister, Gérard; Weissmann, Jody (21 de octubre de 2004). Matemáticas integrales para científicos informáticos 2. Springer Science & Business Media. pág. 323. ISBN 978-3-540-20861-7.
^ Curry, Haskell B. ; Feys, Robert (1958). Combinatory Logic . Vol. I. Ámsterdam: Holanda Septentrional. págs. 139-142. ISBN 0-7204-2208-6.
^ Kashima, Ryo. "Una prueba del teorema de estandarización en el cálculo λ" (PDF) . Instituto Tecnológico de Tokio . Consultado el 19 de agosto de 2021 .
^ Vial, Pierre (7 de diciembre de 2017). Operadores de tipificación no idempotentes, más allá del cálculo λ (PDF) (PhD). Sorbonne Paris Cité. p. 62.
^ Partain, William D. (diciembre de 1989). Graph Reduction Without Pointers (PDF) (PhD). Universidad de Carolina del Norte en Chapel Hill . Consultado el 10 de enero de 2022 .
^ Van Oostrom, Vincent; Toyama, Yoshihito (2016). Normalización por descenso aleatorio (PDF) . 1.ª Conferencia internacional sobre estructuras formales para computación y deducción. pág. 32:3. doi : 10.4230/LIPIcs.FSCD.2016.32 .
^ Takahashi, M. (abril de 1995). "Reducciones paralelas en cálculo λ". Información y computación . 118 (1): 120–127. doi : 10.1006/inco.1995.1057 .
^ abcd Blanc, Tomasz; Lévy, Jean-Jacques; Maranget, Luc (2005). "Compartir en el cálculo lambda débil". Procesos, términos y ciclos: pasos en el camino hacia el infinito: ensayos dedicados a Jan Willem Klop con motivo de su 60.º cumpleaños . Springer. pp. 70–87. CiteSeerX 10.1.1.129.147 . doi :10.1007/11601548_7. ISBN . 978-3-540-32425-6.
^ Sestoft, Peter (2002). "Demostración de la reducción del cálculo lambda" (PDF) . En Mogensen, T; Schmidt, D; Sudborough, IH (eds.). La esencia de la computación: complejidad, análisis, transformación. Ensayos dedicados a Neil D. Jones . Apuntes de clase en informática. Vol. 2566. Springer-Verlag. págs. 420–435. ISBN. 3-540-00326-6.
^ ab Felleisen, Matthias (2009). Ingeniería semántica con PLT Redex . Cambridge, Massachusetts: MIT Press. pag. 42.ISBN 978-0262062756.
^ Sestini, Filippo (2019). Normalización por evaluación para reducción lambda débil tipificada (PDF) . 24.ª Conferencia internacional sobre tipos para pruebas y programas (TYPES 2018). doi : 10.4230/LIPIcs.TYPES.2018.6 .
^ abc Asperti, Andrea; Guerrini, Stefano (1998). La implementación óptima de lenguajes de programación funcional . Cambridge, Reino Unido: Cambridge University Press. ISBN 0521621127.
^ ab Fernández, Maribel; Siafakas, Nikolaos (30 de marzo de 2010). "Cálculos lambda etiquetados con copia y borrado explícitos". Actas electrónicas en informática teórica . 22 : 49–64. arXiv : 1003.5515v1 . doi :10.4204/EPTCS.22.5. S2CID 15500633.
^ Lévy, Jean-Jacques (9-11 de noviembre de 1987). Participación en la evaluación de expresiones lambda (PDF) . Segundo simposio franco-japonés sobre programación de computadoras de la futura generación. Cannes, Francia. p. 187. ISBN 0444705260.
^ Terese (2003). Sistemas de reescritura de términos . Cambridge, Reino Unido: Cambridge University Press. p. 518. ISBN. 978-0-521-39115-3.
^ Lamping, John (1990). Un algoritmo para la reducción óptima del cálculo lambda (PDF) . 17.º simposio ACM SIGPLAN-SIGACT sobre principios de lenguajes de programación - POPL '90. págs. 16-30. doi :10.1145/96709.96711.
^ Lévy, Jean-Jacques (junio de 1974). Réductions sures dans le lambda-calcul (PDF) (Doctor) (en francés). Universidad París VII. págs. 81-109. OCLC 476040273 . Consultado el 17 de agosto de 2021 .
^ Asperti, Andrea. "Máquina de orden superior óptima de Bolonia, versión 1.1". GitHub .
^ van Oostrom, Vicente; van de Looij, Kees-Jan; Zwitserlood, Marijn (2004). ] (Lambdascope): Otra implementación óptima del cálculo lambda (PDF) . Taller de Álgebra y Lógica en Sistemas de Programación (ALPS).
^ Chang, Stephen; Felleisen, Matthias (2012). "El cálculo lambda de llamada por necesidad, revisitado" (PDF) . Lenguajes y sistemas de programación . Apuntes de clase en informática. Vol. 7211. págs. 128–147. doi :10.1007/978-3-642-28869-2_7. ISBN 978-3-642-28868-5.S2CID6350826 .

Enlaces externos

Banco de trabajo de reducción de cálculo lambda