Sobre a confluência do cálculo λx com locally nameless representation

Abstract

O Calculo Lambda com Substituições Explícitas é uma expansão da gramática do Cálculo Lambda proposto por A. Church na década de 1930. Múltiplas implementações desse cálculo existem, umas delas é denominada λx. Como demonstrado por K. Nakazawa, o sistema λx é confluente. A demonstração ocorre pela construção de uma relação entre este sistema de reduções e a propriedade Z. Este trabalho apresenta uma tentativa da formalização dessa prova via assistente de provas Coq. Ocálculo λx é implementado neste trabalho expandindo o framework locally nameless representation. Este framework foi introduzido por A. Charguéraud e traz uma noção mista entre a representação com nomes e com Índices de De Bruijn. Ao longo do trabalho é exposto que a formalização não pode ser concluída por estes meios pois, a noção de substituição para as substituições explícitas do cálculo λx difere da noção de substituições da meta-substituição proposta pelo framework. Além disso, esta meta-substituição fere o Lema da Substituição em seu caso geral. Trabalhos futuros incluem a reimplementação da meta-substituição e a conclusão da formalização via assistentes de prova.