Formalização em Coq da prova de confluência do cálculo λx no contexto nominal

Abstract

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].