Sobre a confluência do cálculo λx na representação nominal

Abstract

O cálculo lambda é um modelo teórico do início da década de 1930 e é a base do paradigma de programação funcional utilizado por linguagens como Ocaml, Haskell e Lisp. Com o desenvolvimento de software assistentes de prova ao longo dos anos, diversas formas de representação do cálculo lambda em ambiente formal foram propostas, dentre elas a que mais se assemelha à representação em papel e lápis é a representação nominal. A principal operação do cálculo lambda, o conceito da β-redução, que associa uma aplicação de uma abstração a uma operação de substituição, pode ser entendida como um passo de computação. Com a necessidade de um formalismo que trouxesse a operação de substituição ao nível da linguagem objeto foram criados os cálculos com substituições explícitas, dentre eles o abordado por esse trabalho, o cálculo λx. A confluência é uma propriedade que afirma que qualquer divergência converge. No cálculo λx essas reduções são representadas pela regra B e pelo conjunto de regras x. Uma forma de provar que o cálculo lambda é confluente é através da propriedade Z composicional. Nesse trabalho introduzimos o cálculo lambda e algumas das suas representações em assistentes de prova, depois introduzimos o software usado nesse trabalho, o Coq, e depois passamos pelas contribuições desse trabalho para a infraestrutura da prova da confluência de λx.