A machine-checked proof of the Standardization Theorem in Lambda Calculus using multiple substitution

Simple item page
dc.contributor.advisorTasistro Souto, Álvaro Danieles
dc.contributor.advisorSzasz Cerutti, Nora Adrianaes
dc.contributor.tribunalBetarte Guidi, Gustavo Romuloes
dc.contributor.tribunalPagano, Migueles
dc.creatorCopes Sabaj, Martín
dc.date.accessioned2018-04-17T08:01:15Z
dc.date.available2018-04-17T08:01:15Z
dc.date.issued2018es
dc.descriptionIncluye bibliografía y anexos.es
dc.descriptionIncluye archivos complementarios.es
dc.description.abstractEn el siguiente trabajo se presenta la formalización en Agda del Teorema de Estandarización para el Cálculo Lambda. Se presenta un corolario del Teorema de Estandarización junto con la demostración del teorema de reducción más izquierdista (leftmost reduction). Si bien existen formalizaciones de estos resultados, lo innovador que se desarrolla en la presente tesis, consiste en el apego de la formalización del Cálculo Lambda a su presentación usual (variables con nombres). El Cálculo Lambda constituye el fundamento teórico de lenguajes de programación funcionales. En la primera parte de este trabajo se reseña la formalización del Cálculo Lambda que se utiliza como base para el desarrollo de los capítulos siguientes e introduce ciertas definiciones propias. En el tercer capítulo se presenta lo más sustancial de la tesis: las definiciones de diferentes nociones de reducción que permiten probar el Teorema de Estandarización que será en términos de una secuencia de reducción estándar. Primero se presentan las nociones de contracción del redex más izquierdista y luego la noción de reducción del redex en la cabecera (de una aplicación). Se demuestra una definición inductiva equivalente a secuencias de reducción estándar. En este capítulo se van desplegando los lemas necesarios para obtener el teorema de estandarización. En el cuarto capítulo de la tesis se aprovecha el Teorema de Estandarización para probar que si un término tiene forma normal, esta es alcanzable por la estrategia de reducción leftmost-outermost. Concluye con la comparación de este desarrollo con otras formalizaciones del mismo resultado y propone algunas líneas para continuarlo.es
dc.format.extent78 p.es
dc.identifier.citationCopes Sabaj, M. (2018). A machine-checked proof of the Standardization Theorem in Lambda Calculus using multiple substitution (Desarrollo de Tesis). Universidad ORT Uruguay, Facultad de Ingeniería. Recuperado de https://rad.ort.edu.uy/handle/20.500.11968/3725es
dc.identifier.urihttp://hdl.handle.net/20.500.11968/3725
dc.languageIngléses
dc.publisherUniversidad ORT Uruguayes
dc.relation.otherhttps://bibliotecas.ort.edu.uy/bibid/86852es
dc.subjectPROYECTOS-MIes
dc.subjectTEOREMA DE ESTANDARIZACIÓNes
dc.subjectLAMBDAes
dc.subjectTEORÍA DE TIPOSes
dc.titleA machine-checked proof of the Standardization Theorem in Lambda Calculus using multiple substitutiones
dc.typeTrabajo final de carreraes
ort.thesis.careerFI - Master en Ingeniería - MIes
ort.thesis.degreegrantorFacultad de Ingenieríaes
ort.thesis.degreelevelMasteres
ort.thesis.degreenameMaster en Ingenieríaes
ort.thesis.degreetypeDesarrollo de Tesises
ort.thesis.noteDesarrollo de Tesis (Master). Universidad ORT Uruguay, Facultad de Ingenieríaes
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Material completo.pdf
Size:
592.15 KB
Format:
Adobe Portable Document Format
Description:
description
Download
Collections
Trabajos finales de carrera de postgrado