Título: | Formalização em Coq da prova de confluência do cálculo λx no contexto nominal |
Autor(es): | Soares, José Roberto |
Orientador(es): | Moura, Flávio Leonardo Cavalcanti de |
Assunto: | Linguagem de programação (Computadores) Cálculo lambda |
Data de apresentação: | 14-Out-2024 |
Data de publicação: | 18-Dez-2024 |
Referência: | SOARES, José R.. Formalização em Coq da prova de confluência do cálculo λx no contexto nominal. 2024. 39 f. Trabalho de Conclusão de Curso (Bacharelado em Engenharia da Computação) — Universidade de Brasília, Brasília, 2024. |
Resumo: | O cálculo λ é amplamente reconhecido no meio acadêmico como um modelo fundamen tal da computação, servindo como base para o paradigma funcional, que é a essência
de linguagens de programação como Haskell, Lisp e OCaml. Além dessas, diversas out ras linguagens, como Python, JavaScript e C++, incorporam conceitos do paradigma
funcional de maneira indireta, permitindo a combinação de estilos de programação fun cionais e imperativos. A propriedade de confluência assegura ao cálculo o determinismo
e confiabilidade no sistema, afirmando que, a partir de qualquer divergência realizada no
cálculo (através das operações de redução), o resultado final irá convergir para o mesmo
ponto em comum. Existem várias formas de formalização da propriedade de confluên cia, e a escolhida neste trabalho foi através da propriedade propriedade Z composicional,
detalhada em [1]. Neste trabalho, estudaremos esta propriedade em uma extensão do
cálculo λ chamada de cálculo λx, que conta com um construtor de substituição explícita,
desta forma, se aproximando mais das linguagens de alto nível puramente funcionais. A
formalização foi feita utilizando o assistente de provas Coq, uma poderosa ferramenta
para verificação formal de teoremas, permitindo uma descrição rigorosa e garantindo a
correção dos resultados obtidos.
Este trabalho tem como objetivo expandir o framework para o estudo de propriedades
de cálculos com substituições explícitas no contexto nominal. Como aplicação, utilizamos
o cálculo λx através do assistente de provas Coq. O código pode ser encontrado no
repositório [2]. |
Abstract: | The lambda calculus is widely recognized in academia as a fundamental model of com putation, serving as the foundation for the functional paradigm, which is the essence of
programming languages such as Haskell, Lisp, and OCaml. In addition to these, several
other languages, such as Python, JavaScript, and C++, incorporate functional paradigm
concepts indirectly, allowing for the combination of functional and imperative program ming styles. The confluence property ensures determinism and reliability in the system,
asserting that from any divergence that occurs in the calculus (through reduction opera tions), the final result will converge to the same common point. There are several ways
to formalize the confluence property, and the one chosen in this work was through the
compositional property Z, detailed in [1]. In this work, we will study this property in
an extension of the lambda calculus called λx calculus, which includes an explicit substi tution constructor, thereby getting closer to purely functional high-level languages. The
formalization was done using the Coq proof assistant, a powerful tool for formal theorem
verification, allowing for rigorous description and ensuring the correctness of the results
obtained.
This work aims to expand the framework for studying properties of calculi with explicit
substitutions in the nominal context. As an application, we prove the confluency property
of the λx calculus with the use of the Coq proof assistant. The code can be found in the
repository [2]. |
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, 2024. |
Licença: | A concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor que autoriza a Biblioteca Digital da Produção Intelectual Discente da Universidade de Brasília (BDM) a disponibilizar o trabalho de conclusão de curso por meio do sítio bdm.unb.br, com as seguintes condições: disponível sob Licença Creative Commons 4.0 International, que permite copiar, distribuir e transmitir o trabalho, desde que seja citado o autor e licenciante. Não permite o uso para fins comerciais nem a adaptação desta. |
Aparece na Coleção: | Engenharia da Computação
|
Todos os itens na BDM estão protegidos por copyright. Todos os direitos reservados.