A machine-checked proof of the Standardization Theorem in Lambda Calculus using multiple substitution
Loading...
Date
2018
Authors
Publisher
Universidad ORT Uruguay
DOI
ISSN
ISBN
Abstract
En 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.
En
Thesis note
Desarrollo de Tesis (Master). Universidad ORT Uruguay, Facultad de Ingeniería
Thesis degree name
Master en Ingeniería
78 p.
Notes
Incluye bibliografía y anexos.
Incluye archivos complementarios.
Incluye archivos complementarios.
Subject
PROYECTOS-MI, TEOREMA DE ESTANDARIZACIÓN, LAMBDA, TEORÍA DE TIPOS
Type
Trabajo final de carrera
Access the full text
Citation
Copes 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/3725