| Título: | Em direção à formalização das propriedades de normalização do sistema λex |
| Autor(es): | Amaral, Lucas de Moura |
| Orientador(es): | Moura, Flávio Leonardo Cavalcanti de |
| Assunto: | Cálculo lambda
Sistemas de computação |
| Data de apresentação: | 9-Dez-2016 |
| Data de publicação: | 11-Ago-2017 |
| Referência: | AMARAL, Lucas de Moura. Em direção à formalização das propriedades de normalização do sistema λex. 2016. vii, 42 f. Trabalho de Conclusão de Curso (Bacharelado em Ciência da Computação)—Universidade de Brasília, Brasília, 2016. |
| Resumo: | O cálculo /\ é um sistema formal, capaz de expressar o processo computacional. Pela sua simplicidade e expressividade, este cálculo é usado como modelo teórico para o paradigma de programação funcional. Em consequência disto, uma grande quantidade de extensões do cálculo foi proposta, com o objetivo de obter um sistema formal intermediário entre o cálculo /\ e suas implementações. O objeto de estudo deste trabalho é uma destas variantes, chamada /\ex, um cálculo com substituições explicitas proposto por Delia Kesner. Este cálculo é um dos primeiros a possuir a preservação da normalização forte enquanto permite composição completa de substituições explícitas. Continuamos o trabalho de formalização deste cálculo, no assistente de prova Coq, iniciado em 2014, e que tem por objetivo fornecer uma prova mecância e construtiva da propriedade de normalização forte para o cálculo /\ex. Mais especificamente, iniciamos a prova da propriedade IE, chave para a prova da preservação da normalização forte do cálculo /\ex. Isto foi feito seguindo a estratégia de prova no artigo da Kesner: estendemos a formalização para marcar alguns termos que não inserem problemas de normalização e definimos regras de redução para lidar com tais termos. Por fim, provamos a equivalência dessas novas regras com a regra original do sistema. |
| Abstract: | /\-calculus is a formal system, capable of expressing the computational process. Because of its simplicity and expressiveness, this calculus is used as a theorical model for the paradigm of functional programming. Consequently, a great variety of extensions were proposed, with the goal of obtaining an intermediate formal system between the /\-calculus and its implementations. The object of study of this work is one of these variants, called /\ex, a calculus with explicit subsititutions, proposed by Delia Kesner. This calculus is one of the first to preserve strong normalization of terms while permitting full composition of explicit substitutions. We continued the work in the formalization of this calculus, in the Coq proof assistant, initiated in 2014, with the goal of providing a mechanical and constructive proof of the strong normalization property for the /\ ex calculus. More specifically, we began the proof of the IE property, key to the demonstration of the preservation of strong normalization of the _ex-calculus. This was done following the strategy on Kesner’s paper: we extended the formalization to mark some terms that do not insert normalization issues and define reduction rules to deal with such terms. Finally, we prove the equivalence of these new rules with the original reduction rule of the system. |
| Informações adicionais: | Trabalho de Conclusão de Curso (graduação)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2016. |
| Aparece na Coleção: | Ciência da Computação
|
