Hispanopedia Wiki
Articulo de referencia

Estrategia de reducción

En la 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ó...

Hispanopedia WikiContenido en espanolLectura gratuita

En la 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(A,→){\displaystyle (A,\to )}una estrategia de reducción→S{\displaystyle \to _{S}}es una relación binaria enA{\displaystyle A}con→S⊆→+{\displaystyle \to _{S}\subsetequ {\overset {+}{\to }}}, dónde→+{\displaystyle {\overset {+}{\to }}}es el cierre transitivo de→{\displaystyle \to }(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 todoa{\displaystyle a}, existe unb{\displaystyle b}cona→b{\displaystyle a\to b}si y solo si∃b′.a→Sb′{\displaystyle \exists b'.a\to _{S}b'}. [ 4 ]

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

Una estrategia determinista es aquella en la que→S{\displaystyle \to _{S}}es una función parcial , es decir, para cadaa∈A{\displaystyle a\in A}como máximo unob{\displaystyle b}de tal manera quea→Sb{\displaystyle a\to _{S}b}. De lo contrario, es una estrategia no determinista . [ 5 ]

Reescritura de términos

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

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

  • leftmost-innermost: en cada paso se contrae el redex más a la izquierda de los redex más internos, donde un redex más interno es un redex que no contiene ningún redex [ 6 ].
  • leftmost-outermost: en cada paso se contrae el redex más a la izquierda de los redex más externos, donde un redex externo es un redex que no está contenido en ningún redex [ 6 ].
  • más a la derecha-más interno, más a la derecha-más externo: de manera similar

Las estrategias de varios pasos incluyen: [ 5 ]

  • parallel-innermost: reduce simultáneamente todos los redexes internos. Esto está bien definido porque los redexes son disjuntos por pares.
  • paralelo-exterior: de manera similar
  • Reducción de Gross-Knuth, [ 7 ] también llamada sustitución completa o reducción de Kleene: [ 5 ] todos los redex en el término se reducen simultáneamente

La reducción paralela 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 realicen (un número finito de) reducciones arbitrarias entre aplicaciones sucesivas de la estrategia. [ 8 ]

Stratego es un lenguaje específico de dominio 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 y más 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 de normal. Esto se conoce como el teorema de estandarización. [ 11 ] [ 12 ]

La reducción más a la izquierda se usa 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 y más 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 usando un recorrido en orden las nociones son distintas. Por ejemplo, en el término(λincógnita.incógnitaΩ)(λy.I){\displaystyle (\lambda xx\Omega)(\lambda yI)}conΩ,I{\displaystyle \Omega ,I}definido aquí , el redex más a la izquierda del recorrido en orden esΩ{\displaystyle \Omega }mientras que el redex más a la izquierda y más externo es la expresión completa. [ 15 ]

La reducción de orden aplicativo se refiere a la reducción de izquierda a derecha. [ 10 ] A diferencia del orden normal, la reducción de orden aplicativo puede no terminar, incluso cuando el término tiene una forma normal. [ 10 ] Por ejemplo, utilizando la reducción de orden aplicativo, es posible la siguiente secuencia de reducciones: (λincógnita.z)((λw.www)(λw.www))→(λincógnita.z)((λw.www)(λw.www)(λw.www))→(λincógnita.z)((λw.www)(λw.www)(λw.www)(λw.www))→(λincógnita.z)((λw.www)(λw.www)(λw.www)(λw.www)(λw.www))…{\displaystyle {\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)(\lambda w.www))\\\rightarrow &(\lambda xz)((\lambda w.www)(\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: (λincógnita.z)((λw.www)(λw.www)){\displaystyle (\mathbf {\lambda } xz)((\lambda w.www)(\lambda w.www))}→z{\displaystyle \rightarrow z}

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

Reducción débil

La reducción de orden normal y la aplicativa son fuertes porque permiten la reducción bajo abstracciones lambda. Por el contrario, la reducción débil no reduce bajo una abstracción lambda. [ 17 ] La reducción por nombre es la estrategia de reducción débil que reduce la redex más a la izquierda y más externa que no está dentro de una abstracción lambda, mientras que la reducción por valor es la estrategia de reducción débil que reduce la redex más a la izquierda y más interna que no está dentro de una abstracción lambda. Estas estrategias se idearon para reflejar las estrategias de evaluación por nombre y 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 por valor que se encuentra en Algol 60 y en los lenguajes de programación modernos. Cuando se combina con la idea de reducción débil, la reducción 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 permitiendo una forma restringida de reducción bajo una abstracción, en particular cuando el redex no involucra la variable ligada 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 aún puede reducirse 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 para los que no existe una secuencia de reducciones que los reduzca sin duplicar el trabajo. Por ejemplo, consideremos

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

Está compuesto por tres términos anidados, a=((λg. ... ) (λh.b)) , b=((λf. ...) c) , y c=(λw. ...) . Solo hay dos posibles β-reducciones que se pueden realizar aquí, sobre a y sobre b. Reducir primero el término externo a da como resultado que el término interno b se duplique, y cada copia tendrá que reducirse, pero reducir primero el término interno b duplicará su argumento c, lo que hará que se duplique el trabajo cuando se conozcan 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 redex 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 debe compartirse. [ 21 ] : 113–114

Las etiquetas consisten en un conjunto infinito numerable de etiquetas atómicas y concatenaciones.ab{\displaystyle ab}, líneas superpuestasa¯{\displaystyle {\overline {a}}}y subrayadosa_{\displaystyle {\underline {a}}}de etiquetas. Un término etiquetado es un término del cálculo lambda donde cada subtérmino tiene una etiqueta. El etiquetado inicial estándar de un término lambda da a cada subtérmino una etiqueta atómica única. [ 21 ] : 132 La β-reducción etiquetada viene dada por: [ 22 ]((λincógnita.METRO)αnorte)β→βα¯⋅METRO[incógnita↦α_⋅norte]{\displaystyle ((\lambda xM)^{\alpha }N)^{\beta }\to \beta {\overline {\alpha }}\cdot M[x\mapsto {\underline {\alpha }}\cdot N]}

dónde⋅{\displaystyle \cdot }concatena etiquetas,β⋅Tα=Tβα{\displaystyle \beta \cdot T^{\alpha }=T^{\beta \alpha }}y sustituciónMETRO[incógnita↦norte]{\displaystyle M[x\mapsto N]}se define de la siguiente manera (utilizando la convención de Barendregt ): [ 22 ]incógnitaα[incógnita↦norte]=α⋅norte(λy.METRO)α[incógnita↦norte]=(λy.METRO[incógnita↦norte])αyα[incógnita↦norte]=yα(METROnorte)α[incógnita↦PAG]=(METRO[incógnita↦PAG]norte[incógnita↦PAG])α{\displaystyle {\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}}} Se puede demostrar que el sistema es confluente. La reducción óptima se define entonces como la reducción de orden normal o de izquierda a derecha mediante la 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 ]

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 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 ]

Llamar por necesidad reducción

La reducción por necesidad se puede definir de manera similar a la reducción óptima como una reducción débil de izquierda a derecha que utiliza la 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 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

  1. ↑ Por cierto, el término anterior se reduce a la función identidad (λy.y) y se construye haciendo envolturas 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 .
  2. ↑ Un resumen de investigaciones recientes sobre la reducción óptima se puede encontrar en el breve artículo Acerca de la reducción eficiente de términos lambda .

Referencias

  1. 1 2 Kirchner, Hélène (26 de agosto de 2015). «Estrategias de reescritura y programas estratégicos de reescritura» . 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-5Consultado el 14 de agosto de 2021 .
  2. ↑ 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 9780521513746Consultado el 21 de agosto de 2021 .
  3. 1 2 Pierce, Benjamin C. (2002). Tipos y lenguajes de programación . MIT Press . pág. 56. ISBN  0-262-16209-1.
  4. ^ 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.
  5. 1 2 3 4 5 Klop, JW "Sistemas de reescritura de términos" (PDF) . Artículos de Nachum Dershowitz y estudiantes . Universidad de Tel Aviv. pág. 77. Recuperado el 14 de agosto de 2021 . 
  6. 1 2 Horwitz, Susan B. "Cálculo Lambda" . Apuntes de CS704 . Universidad de Wisconsin Madison . Consultado el 19 de agosto de 2021 .
  7. ^ 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 . hdl : 2066/17285 .  
  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 . Recuperado el 8 de septiembre de 2021 .
  9. ↑ Kieburtz, Richard B. (noviembre de 2001). "Una lógica para estrategias de reescritura" . Electronic Notes in Theoretical Computer Science . 58 (2): 138– 154. doi : 10.1016/S1571-0661(04)00283-X .
  10. 1 2 3 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.
  11. ↑ Curry, Haskell B.; Feys , Robert (1958). Lógica combinatoria . Vol. I. Ámsterdam: North Holland. págs. 139–142 . ISBN   0-7204-2208-6.{{cite book}}: Incompatibilidad de ISBN/Fecha ( ayuda )
  12. ↑ Kashima, Ryo. "Una demostración del teorema de estandarización en el cálculo lambda" (PDF) . Instituto Tecnológico de Tokio . Consultado el 19 de agosto de 2021 .
  13. ^ Vial, Pierre (7 de diciembre de 2017). Operadores de tipificación no idempotentes, más allá del cálculo λ (PDF) (Doctor). Sorbona París Cité. pag. 62. 
  14. ↑ Partain, William D. (diciembre de 1989). Reducción de grafos sin punteros (PDF) (PhD). Universidad de Carolina del Norte en Chapel Hill . Recuperado el 10 de enero de 2022 .
  15. ↑ Van Oostrom, Vincent; Toyama, Yoshihito (2016). Normalización por descenso aleatorio (PDF) . 1.ª Conferencia Internacional sobre Estructuras Formales para la Computación y la Deducción. p. 32:3. doi : 10.4230/LIPIcs.FSCD.2016.32 . 
  16. ↑ Takahashi, M. (abril de 1995). "Reducciones paralelas en el cálculo λ" . Information and Computation . 118 (1): 120– 127. doi : 10.1006/inco.1995.1057 .
  17. 1 2 3 4 Blanc, Tomasz; Lévy, Jean-Jacques; Maranget, Luc (2005). «Compartiendo en el cálculo lambda débil». Procesos, términos y ciclos: Pasos en el camino al infinito: Ensayos dedicados a Jan Willem Klop con motivo de su 60 cumpleaños . Springer. págs. 70–87 . CiteSeerX 10.1.1.129.147 . doi : 10.1007/11601548_7 . ISBN   978-3-540-32425-6.
  18. ↑ 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 . Lecture Notes in Computer Science. Vol. 2566. Springer-Verlag. pp. 420–435 . ISBN   3-540-00326-6.
  19. 1 2 Felleisen, Matthias (2009). Ingeniería semántica con PLT Redex . Cambridge, Mass.: MIT Press. pág. 42. ISBN  978-0262062756.
  20. ↑ Sestini, Filippo (2019). Normalización por evaluación para reducción lambda débil tipada (PDF) . 24.ª Conferencia Internacional sobre Tipos para Pruebas y Programas (TYPES 2018). doi : 10.4230/LIPIcs.TYPES.2018.6 .
  21. 1 2 3 Asperti, Andrea; Guerrini, Stefano (1998). La implementación óptima de lenguajes de programación funcional . Cambridge, Reino Unido: Cambridge University Press. ISBN 0521621127.
  22. 1 2 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 . 
  23. ↑ Lévy, Jean-Jacques (9-11 de noviembre de 1987). Compartir en la evaluación de expresiones lambda (PDF) . Segundo Simposio Franco-Japonés sobre Programación de Computadoras de Futura Generación. Cannes, Francia. pág. 187. ISBN  0444705260.
  24. ↑ Terese (2003). Sistemas de reescritura de términos . Cambridge, Reino Unido: Cambridge University Press. pág. 518. ISBN  978-0-521-39115-3.
  25. ↑ 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. pp. 16–30 . doi : 10.1145/96709.96711 . 
  26. ^ 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 a 109. OCLC 476040273 . Consultado el 17 de agosto de 2021 .  
  27. ↑ Asperti, Andrea. "Bologna Optimal Higher-Order Machine, Version 1.1" . GitHub .
  28. ^ 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). Archivado desde el original (PDF) el 6 de julio de 2017 . Consultado el 18 de agosto de 2021 .
  29. ↑ Chang, Stephen; Felleisen, Matthias (2012). "El cálculo lambda por necesidad, una revisión" (PDF) . Lenguajes y sistemas de programación . Notas 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. S2CID 6350826 . 
  • Banco de trabajo para la reducción del cálculo lambda