Semántica dinámica de cálculos de sustituciones explicitas a distancia

Mostrar todas las versiones(3)

Los cálculos de sustituciones explícitas son variantes del cálculo-λ en los que la operación de sustitución no se define a nivel del metalenguaje, sino con reglas de reescritura que la implementan. Nuestro principal objeto de estudio es un cálculo de sustituciones explícitas particular, el Linear Su...

Descripción completa

Detalles Bibliográficos
Autor principal: Barenbaum, Pablo
Formato: Tesis Doctoral
Lenguaje:Español
Publicado: 2020
Materias:
SEMANTICA DE LENGUAJES DE PROGRAMACION
CALCULO-λ
SUSTITUCIONES EXPLICITAS
ESTRATEGIAS DE EVALUACION
EVALUACION LAZY
MAQUINAS ABSTRACTAS
SISTEMA DE TIPOS
TEORIA DE RESIDUOS
PROGRAMMING LANGUAGE SEMANTICS
λ-CALCULUS
EXPLICIT SUBSTITUTIONS
EVALUATION STRATEGIES
LAZY EVALUATION
ABSTRACT MACHINES
TYPE SYSTEMS
RESIDUAL THEORY
Acceso en línea:https://hdl.handle.net/20.500.12110/tesis_n6991_Barenbaum
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:tesis_n6991_Barenbaum
record_format dspace
spelling todo:tesis_n6991_Barenbaum2023-10-03T13:15:09Z Semántica dinámica de cálculos de sustituciones explicitas a distancia Dynamic semantics of calculi with explicit substitutions at a distance Barenbaum, Pablo SEMANTICA DE LENGUAJES DE PROGRAMACION CALCULO-λ SUSTITUCIONES EXPLICITAS ESTRATEGIAS DE EVALUACION EVALUACION LAZY MAQUINAS ABSTRACTAS SISTEMA DE TIPOS TEORIA DE RESIDUOS PROGRAMMING LANGUAGE SEMANTICS λ-CALCULUS EXPLICIT SUBSTITUTIONS EVALUATION STRATEGIES LAZY EVALUATION ABSTRACT MACHINES TYPE SYSTEMS RESIDUAL THEORY Los cálculos de sustituciones explícitas son variantes del cálculo-λ en los que la operación de sustitución no se define a nivel del metalenguaje, sino con reglas de reescritura que la implementan. Nuestro principal objeto de estudio es un cálculo de sustituciones explícitas particular, el Linear Substitution Calculus (LSC), definido por Accaoli y Kesner en 2010. Se caracteriza por el hecho de que las reglas de reescritura operan no localmente (a distancia). En esta tesis, en primer lugar, definimos máquinas abstractas que implementan estrategias de evaluacion en el LSC: call-by-name para evaluación débil y fuerte, call-by-value y call-by- need. Demostramos que dichas máquinas son correctas y preservan la complejidad temporal. En segundo lugar, denimos una extension de la estrategia de evaluación call-by-need en el LSC para evaluacion fuerte. Demostramos que la estrategia es completa con respecto a call-by- name, usando un sistema de tipos intersección no idempotente, y mostramos cómo extenderla para lidiar con pattern matching y recursión. Por último, estudiamos la teoría de residuos y familias de radicales en el LSC. Para ello denimos una variante del LSC con etiquetas de Levy, lo que nos permite demostrar que cumple con la propiedad de Finite Family Developments. Aplicamos esta propiedad para obtener resultados de optimalidad, estandarización y normalización de estrategias en el LSC, y generalizamos algunos de estos resultados al marco axiomático de Deterministic Family Structures. Explicit substitution calculi are variants of the λ-calculus in which the operation of substitution is not defined at the metalanguage level, but rather implemented by means of rewriting rules. Our main object of study is a particular explicit substitution calculus, the Linear Substitution Calculus (LSC), introduced by Accaoli and Kesner in 2010. Its distinguishing feature is that rewriting rules operate non-locally (at a distance). In this thesis, first, we define abstract machines to implement evaluation strategies in the LSC: call-by-name for weak and strong evaluation, call-by-value, and call-by-need. We prove that these machines are correct and that they preserve computational time complexity. Second, we define an extension of the call-by- need evaluation strategy in the LSC for strong reduction. We show that the strong call-by-need strategy is complete with respect to call-by-name, using a non-idempotent intersection type system, and we show how to extend the strategy to deal with pattern matching and recursion. Finally, we study the theory of residuals and redex families in the LSC. To this aim, we define a variant of the LSC endowed with Lévy labels, which allows us to prove that it enjoys the Finite Family Developments property. We apply this property to obtain results on optimality, standardization, and normalization for the LSC, and we generalize some of this results to the axiomatic framework of Deterministic Family Structures. Fil: Barenbaum, Pablo. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2020 Tesis Doctoral PDF Español info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar https://hdl.handle.net/20.500.12110/tesis_n6991_Barenbaum
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
language Español
orig_language_str_mv Español
topic SEMANTICA DE LENGUAJES DE PROGRAMACION
CALCULO-λ
SUSTITUCIONES EXPLICITAS
ESTRATEGIAS DE EVALUACION
EVALUACION LAZY
MAQUINAS ABSTRACTAS
SISTEMA DE TIPOS
TEORIA DE RESIDUOS
PROGRAMMING LANGUAGE SEMANTICS
λ-CALCULUS
EXPLICIT SUBSTITUTIONS
EVALUATION STRATEGIES
LAZY EVALUATION
ABSTRACT MACHINES
TYPE SYSTEMS
RESIDUAL THEORY
spellingShingle SEMANTICA DE LENGUAJES DE PROGRAMACION
CALCULO-λ
SUSTITUCIONES EXPLICITAS
ESTRATEGIAS DE EVALUACION
EVALUACION LAZY
MAQUINAS ABSTRACTAS
SISTEMA DE TIPOS
TEORIA DE RESIDUOS
PROGRAMMING LANGUAGE SEMANTICS
λ-CALCULUS
EXPLICIT SUBSTITUTIONS
EVALUATION STRATEGIES
LAZY EVALUATION
ABSTRACT MACHINES
TYPE SYSTEMS
RESIDUAL THEORY
Barenbaum, Pablo
Semántica dinámica de cálculos de sustituciones explicitas a distancia
topic_facet SEMANTICA DE LENGUAJES DE PROGRAMACION
CALCULO-λ
SUSTITUCIONES EXPLICITAS
ESTRATEGIAS DE EVALUACION
EVALUACION LAZY
MAQUINAS ABSTRACTAS
SISTEMA DE TIPOS
TEORIA DE RESIDUOS
PROGRAMMING LANGUAGE SEMANTICS
λ-CALCULUS
EXPLICIT SUBSTITUTIONS
EVALUATION STRATEGIES
LAZY EVALUATION
ABSTRACT MACHINES
TYPE SYSTEMS
RESIDUAL THEORY
description Los cálculos de sustituciones explícitas son variantes del cálculo-λ en los que la operación de sustitución no se define a nivel del metalenguaje, sino con reglas de reescritura que la implementan. Nuestro principal objeto de estudio es un cálculo de sustituciones explícitas particular, el Linear Substitution Calculus (LSC), definido por Accaoli y Kesner en 2010. Se caracteriza por el hecho de que las reglas de reescritura operan no localmente (a distancia). En esta tesis, en primer lugar, definimos máquinas abstractas que implementan estrategias de evaluacion en el LSC: call-by-name para evaluación débil y fuerte, call-by-value y call-by- need. Demostramos que dichas máquinas son correctas y preservan la complejidad temporal. En segundo lugar, denimos una extension de la estrategia de evaluación call-by-need en el LSC para evaluacion fuerte. Demostramos que la estrategia es completa con respecto a call-by- name, usando un sistema de tipos intersección no idempotente, y mostramos cómo extenderla para lidiar con pattern matching y recursión. Por último, estudiamos la teoría de residuos y familias de radicales en el LSC. Para ello denimos una variante del LSC con etiquetas de Levy, lo que nos permite demostrar que cumple con la propiedad de Finite Family Developments. Aplicamos esta propiedad para obtener resultados de optimalidad, estandarización y normalización de estrategias en el LSC, y generalizamos algunos de estos resultados al marco axiomático de Deterministic Family Structures.
format Tesis Doctoral
author Barenbaum, Pablo
author_facet Barenbaum, Pablo
author_sort Barenbaum, Pablo
title Semántica dinámica de cálculos de sustituciones explicitas a distancia
title_short Semántica dinámica de cálculos de sustituciones explicitas a distancia
title_full Semántica dinámica de cálculos de sustituciones explicitas a distancia
title_fullStr Semántica dinámica de cálculos de sustituciones explicitas a distancia
title_full_unstemmed Semántica dinámica de cálculos de sustituciones explicitas a distancia
title_sort semántica dinámica de cálculos de sustituciones explicitas a distancia
publishDate 2020
url https://hdl.handle.net/20.500.12110/tesis_n6991_Barenbaum
work_keys_str_mv AT barenbaumpablo semanticadinamicadecalculosdesustitucionesexplicitasadistancia
AT barenbaumpablo dynamicsemanticsofcalculiwithexplicitsubstitutionsatadistance
_version_ 1807315622928842752

Ejemplares similares