Semántica denotacional para un cálculo-λ relacional

Mostrar todas las versiones(3)

En esta tesis trabajamos con el cálculo-λU, una extensión del cálculo-λ que incorpora las características fundamentales de la programación relacional: alternativa no determinística, secuenciación explícita, unificación de primer orden e introducción de variables frescas. Proponemos un sistema de tip...

Descripción completa

Detalles Bibliográficos
Autor principal: Milicich, Mariana
Otros Autores: Barenbaum, Pablo
Formato: Tesis de grado publishedVersion
Lenguaje:Español
Publicado: Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2022
Materias:
SEMANTICA DENOTACIONAL
CALCULO-λ
UNIFICACION
PROGRAMACION FUNCIONAL
PROGRAMACION LOGICA
PROGRAMACION RELACIONAL
DENOTATIONAL SEMANTICS
λ-CALCULUS
UNIFICATION
FUNCTIONAL PROGRAMMING
LOGIC PROGRAMMING
RALATIONAL PROGRAMMING
Acceso en línea:https://hdl.handle.net/20.500.12110/seminario_nCOM000492_Milicich
https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000492_Milicich_oai
Aporte de:
Repositorio Digital de la Universidad de Buenos Aires (UBA) de Universidad de Buenos Aires
id I28-R145-seminario_nCOM000492_Milicich_oai
record_format dspace
spelling I28-R145-seminario_nCOM000492_Milicich_oai2024-12-17 Barenbaum, Pablo Milicich, Mariana 2022-08-10 En esta tesis trabajamos con el cálculo-λU, una extensión del cálculo-λ que incorpora las características fundamentales de la programación relacional: alternativa no determinística, secuenciación explícita, unificación de primer orden e introducción de variables frescas. Proponemos un sistema de tipos y formulamos una semántica denotacional para su fragmento tipado. Por semántica denotacional entendemos a una función [−]] que dado un programa devuelve su significado o denotación, es decir, un elemento de algún dominio de interpretación apropiado. El objetivo es demostrar que la semántica cumple con propiedades esperables: por un lado, probar la correctitud de la semántica operacional con respecto a la denotacional, que asegura que dos programas equivalentes de acuerdo con una teoría sintáctica de igualdad deben tener la misma denotación; por otra parte, la propiedad de completitud de la semántica operacional con respecto a la denotacional, que asegura que dos programas con la misma denotación se pueden probar equivalentes en una teoría sintáctica de igualdad. En este trabajo logramos formular una semántica denotacional para la cual la semántica operacional verifica una forma débil de correctitud. Queda como trabajo futuro proponer una semántica denotacional para que la operacional sea correcta y completa. In this thesis we work with the λU-calculus, an extension of the λ-calculus that incorporates the fundamental characteristics of relational programming: non-deterministic alternative, explicit secuenciation, first-order unification and introduction of free variables. We propose a type system and formulate a denotational semantics for its typed fragment. By denotational semantics we mean a function [[−]] which, given a program, returns its meaning or denotation, that is, an element of some appropiate interpretacion domain. The goal of this work is to prove that the semantics meets the expected properties: on the one hand, show the soundness of the operational semantics with respect to the denotationali semantics, which ensures that two equivalent programs in accordance with a syntactic theory of equality must have the same denotation; and on the other hand, the property of completeness of the operational semantics with respect to the denotational semantics, which assures that two programs with the same denotation can be shown equivalents in a syntactic theory of equivalence. In this work we managed to formulate a denotational semantics for which the operational semantics verifies a weak form of soundness. It remains as future work to propose a denotational semantics for which the operational semantics is both sound and complete. Fil: Milicich, Mariana. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. application/pdf https://hdl.handle.net/20.500.12110/seminario_nCOM000492_Milicich spa Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar SEMANTICA DENOTACIONAL CALCULO-λ UNIFICACION PROGRAMACION FUNCIONAL PROGRAMACION LOGICA PROGRAMACION RELACIONAL DENOTATIONAL SEMANTICS λ-CALCULUS UNIFICATION FUNCTIONAL PROGRAMMING LOGIC PROGRAMMING RALATIONAL PROGRAMMING Semántica denotacional para un cálculo-λ relacional info:eu-repo/semantics/bachelorThesis info:ar-repo/semantics/tesis de grado info:eu-repo/semantics/publishedVersion https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000492_Milicich_oai
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-145
collection Repositorio Digital de la Universidad de Buenos Aires (UBA)
language Español
orig_language_str_mv spa
topic SEMANTICA DENOTACIONAL
CALCULO-λ
UNIFICACION
PROGRAMACION FUNCIONAL
PROGRAMACION LOGICA
PROGRAMACION RELACIONAL
DENOTATIONAL SEMANTICS
λ-CALCULUS
UNIFICATION
FUNCTIONAL PROGRAMMING
LOGIC PROGRAMMING
RALATIONAL PROGRAMMING
spellingShingle SEMANTICA DENOTACIONAL
CALCULO-λ
UNIFICACION
PROGRAMACION FUNCIONAL
PROGRAMACION LOGICA
PROGRAMACION RELACIONAL
DENOTATIONAL SEMANTICS
λ-CALCULUS
UNIFICATION
FUNCTIONAL PROGRAMMING
LOGIC PROGRAMMING
RALATIONAL PROGRAMMING
Milicich, Mariana
Semántica denotacional para un cálculo-λ relacional
topic_facet SEMANTICA DENOTACIONAL
CALCULO-λ
UNIFICACION
PROGRAMACION FUNCIONAL
PROGRAMACION LOGICA
PROGRAMACION RELACIONAL
DENOTATIONAL SEMANTICS
λ-CALCULUS
UNIFICATION
FUNCTIONAL PROGRAMMING
LOGIC PROGRAMMING
RALATIONAL PROGRAMMING
description En esta tesis trabajamos con el cálculo-λU, una extensión del cálculo-λ que incorpora las características fundamentales de la programación relacional: alternativa no determinística, secuenciación explícita, unificación de primer orden e introducción de variables frescas. Proponemos un sistema de tipos y formulamos una semántica denotacional para su fragmento tipado. Por semántica denotacional entendemos a una función [−]] que dado un programa devuelve su significado o denotación, es decir, un elemento de algún dominio de interpretación apropiado. El objetivo es demostrar que la semántica cumple con propiedades esperables: por un lado, probar la correctitud de la semántica operacional con respecto a la denotacional, que asegura que dos programas equivalentes de acuerdo con una teoría sintáctica de igualdad deben tener la misma denotación; por otra parte, la propiedad de completitud de la semántica operacional con respecto a la denotacional, que asegura que dos programas con la misma denotación se pueden probar equivalentes en una teoría sintáctica de igualdad. En este trabajo logramos formular una semántica denotacional para la cual la semántica operacional verifica una forma débil de correctitud. Queda como trabajo futuro proponer una semántica denotacional para que la operacional sea correcta y completa.
author2 Barenbaum, Pablo
author_facet Barenbaum, Pablo
Milicich, Mariana
format Tesis de grado
Tesis de grado
publishedVersion
author Milicich, Mariana
author_sort Milicich, Mariana
title Semántica denotacional para un cálculo-λ relacional
title_short Semántica denotacional para un cálculo-λ relacional
title_full Semántica denotacional para un cálculo-λ relacional
title_fullStr Semántica denotacional para un cálculo-λ relacional
title_full_unstemmed Semántica denotacional para un cálculo-λ relacional
title_sort semántica denotacional para un cálculo-λ relacional
publisher Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate 2022
url https://hdl.handle.net/20.500.12110/seminario_nCOM000492_Milicich
https://repositoriouba.sisbi.uba.ar/gsdl/cgi-bin/library.cgi?a=d&c=aextesisg&d=seminario_nCOM000492_Milicich_oai
work_keys_str_mv AT milicichmariana semanticadenotacionalparauncalculolrelacional
_version_ 1824952626321555456

Ejemplares similares