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

Abstract

Um sistema abstrato de redução (ARS) é um par ordenado (A, R) onde A é um conjunto e R é uma relação de redução sobre esse conjunto [1]. A confluência de um ARS, que expressa o determinismo computacional do sistema, é a propriedade que esse sistema tem se, dado um elemento qualquer que possa ser reduzido a partir do fecho transitivo reflexivo da relação do ARS para dois elementos distintos, então esses dois elementos distintos podem ser reduzidos para algum elemento comum a partir do mesmo fecho transitivo reflexivo. Em outras palavras, um ARS é confluente se qualquer divergência pode ser juntada. Existem diversas técnicas distintas para se provar a confluência de um ARS [2], e a que utilizaremos aqui se baseia no fato de que ela pode ser obtida a partir da existência de algum mapeamento que satisfaça a propriedade Z nesse sistema [1, 3]. O cálculo λ é um sistema formal de computação criado por Alonzo Church que é equivalente às máquinas de Turing e que constitui o fundamento teórico do paradigma de programação funcional [4, 5]. Podemos ver o cálculo λ como um sistema abstrato de redução, onde as suas expressões são os elementos de A, e R é o conjunto contendo as reduções do cálculo. Uma das variações do cálculo λ que também pode ser vista como um ARS é o cálculo λx, que é um cálculo com substituição explicita, i.e., uma extensão do cálculo λ cujo operador de substituição é um dos construtores da gramática de termos [6, 7]. Esse trabalho tem como objetivo explicar o processo de formalização via o assistente de provas Coq, que é um provador de teorema altamente utilizado tanto no meio acadêmico quanto na, na indústria confluência do cálculo λx, conforme [6], no contexto nominal.