Omslagsbillede

Uma formalização da teoria nominal em Coq

Saved in:
Bibliografiske detaljer
Hovedforfatter: Paranhos, Fabrício Sanches
Publication Date: 2022
Format: Master thesis
Sprog: por
Source: Repositório Institucional da UFG
Download full: http://repositorio.bc.ufg.br/tede/handle/tede/12314
Summary: 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.
Summary: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.

Lignende værker