A formalization of the nominal theory in Coq
| Autor: | Paranhos, Fabrício Sanches |
|---|---|
| Přispěvatelé: | Ventura, Daniel Lima, Vieira, Bruno Lopes, Nantes Sobrinho, Daniele |
| Jazyk: | portugalština |
| Rok vydání: | 2022 |
| Předmět: | |
| Zdroj: | Biblioteca Digital de Teses e Dissertações da UFG Universidade Federal de Goiás (UFG) instacron:UFG |
| Popis: | Nas implementações e análises de linguagens de programação é recorrente a necessidade de manipulação, ou demonstração, de termos contendo ligantes. Entretanto, na prática, esta não é uma tarefa trivial. Dentre os principais problemas pode-se citar a captura de variável livre, a identificação de termos α-equivalentes e em demonstrações indutivas sobre termos contendo variáveis ligadas, nos quais são necessários diversos lemas de renomeação de variável. No contexto informal, diversos dispositivos foram elaborados a fim de mitigar os problemas relacionados a variáveis ligadas, como, por exemplo, a convenção de variável de Barendregt. Enquanto no contexto de verificação de provas formalizadas num assistente, ainda é um problema em aberto, com diversas soluções e propostas de representação de variáveis ligadas. Dentre elas, as técnicas nominais têm sido elogiadas por sua capacidade formalizar gramáticas com estruturas ligantes mais próximas de seus desenvolvimentos informais, através de uma metateoria uniforme baseada em permutação de nomes. Devido à falta de uma biblioteca nominal para assistentes de provas construtivos, apresentamos nesta dissertação uma formalização em progresso da teoria nominal em Coq, salientando as principais decisões de design e projeto. Implementamos e comparamos dois métodos, um pragmático, apoiado nos pilares básicos da teoria nominal, e uma formalização construtiva dos principais elementos da teoria nominal: conjuntos nominais, suporte, frescor, funções suportadas, α-equivalência nominal e abstração de nomes. Apresentamos uma hierarquia de classes para definição de conjuntos nominais, que aliado ao mecanismo de reescrita generalizada, alcançamos definições e provas concisas, em simultâneo evitando o conhecido cenário “setoid hell”. In the implementations and analysis of programming languages, the need for manipulation, or demonstration, of terms containing variable binding structures is recurrent. However, in practice, this is not a trivial task. The main problems are the capture of free variables, the identification of α-equivalent terms and inductive demonstrations about terms containing bound variables, in which several variable renaming lemmas are needed. In the informal context, several devices were developed to mitigate problems related to bound variables, such as, for example, the Barendregt Variable Convention. While in the context of proofs verification, formalized in a proof assistant, it is still an open problem with several solutions and proposals for the representation of bound variables. Among them, nominal techniques have been praised for their ability to formalize grammars with binding structures closer to their informal developments, through a uniform metatheory based on name permutation. Due to the lack of a nominal library for constructive proof assistants, we present in this dissertation an ongoing formalization of the nominal theory in Coq, where we highlight the main design and project decisions. We implemented and compared two methods, a pragmatic one, supported by the basic pillars of nominal theory, and a constructive formalization of the main elements of nominal theory: nominal sets, support, freshness, supported functions, nominal α-equivalence and name abstraction. Our main contribution was to present a class hierarchy for the definition of nominal sets, which combined with the generalized rewriting mechanism, achieve concise definitions and proofs, while avoiding the well-known “setoid hell” scenario. Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|