Utilize este identificador para referenciar este registo: http://hdl.handle.net/10400.2/3310
Título: Polimorfismo atómico e o teorema da normalização forte
Autor: Inácio, Maria do Rosário Dinis
Orientador: Edmundo, Mário Jorge
Ferreira, Gilda Dias
Palavras-chave: Matemática
Computação
Lógica matemática
λ-Cálculo
Polimorfismo atómico
Cálculo proposicional intuicionista
Normalização forte
Dedução natural
Isomorfismo de Curry-Howard
Transbordo de instanciação
Atomic polyphormism
Intuitionistic propositional calculus
Strong normalization
Natural deduction
Curry-Howard isomorphidm
Instantion overflow
λ-Calculus
Data de Defesa: 2014
Citação: Inácio, Maria do Rosário Dinis - Polimorfismo atómico e o teorema da normalização forte [Em linha]. [Lisboa] : [s.n.], 2014. 61 p.
Resumo: Nesta dissertação provamos, através do sistema Fat (restrição predicativa do sistema polimórfico F de Jean-Yves Girard), que o cálculo proposicional intuicionista é fortemente normalizável considerando β-conversões. Embora o resultado em si seja bem conhecido, a estratégia (via Fat) seguida nesta dissertação é muito recente, tendo sido apresentada em 2013 no artigo Atomic Polymorphism Esta dissertação pretende ser um estudo autocontido e detalhado dos resultados desse artigo. O sistema Fat começa por ser apresentado em λ-cálculo e através do Isomorfismo de Curry-Howard apresentamos também a sua formulação no cálculo de dedução natural. O sistema contém apenas dois geradores de tipos (fórmulas): implicação e quantificação universal de segunda-ordem restrita a instanciações atómicas, daí a designação de polimorfismo atómico (Fat). Dois resultados centrais em Fat são demonstrados: i. o cálculo proposicional intuicionista pode ser imerso em Fat (via definição de conectivos de Prawitz e transbordo de instanciação); ii. o sistema Fat é fortemente normalizável considerando βη-conversões (adaptação simples da técnica de redutibilidade de Tait). Por último, e com o objetivo de mostrar que a normalização forte de Fat implica a normalização forte do cálculo proposicional intuicionista, provamos que as β-conversões deste último cálculo se traduzem num número finito de βη-conversões em Fat. Tal como nos resultados anteriores também nesta demonstração apresentamos todos os casos, incluindo aqueles que no artigo, por uma questão de limitação de espaço estavam omissos. Um limite ao número máximo de βη-conversões que surgem aquando da tradução das β-conversões é também apresentado.
In this dissertation we prove through the system Fat (predicative restriction of Jean-Yves Girard's system F) that the intuitionistic propositional calculus is strongly normalizable, considering β-conversions. Altough the result is well-known, the strategy (via Fat) followed in this dissertation is quite recent. It was presented in 2013 in the paper Atomic Polymorphism . The present dissertation intends to be a self-contained and detailed study of the results in the paper. System Fat is firstly presented in λ-calculus, and via Curry-Howard's isomorphism we also present its formulation in the natural deduction calculus. The system contains only two generators of types (formulas): implication and second-order universal quantification, restricted to atomic instantiations - which explains the designation of atomic polymorphism Fat. Two central results in Fat are proved: i. the intuitionistic propositional calculus can be embedded into Fat (via Prawitz's definition of connectives and instantiation overflow);\ ii. the system Fat is strongly normalizable, considering βη-convertions (simple adaptation of the Tait's reducibility technique). Finally, aiming at demonstrating that the strong normalization of Fat implies the strong normalization of intuitionistic propositional calculus, we prove that the β-conversions of this latter calculus can be translated into a finite number of βη-conversions of Fat. As in the previous results, we present all the cases, including those which were left aside in the article, due to space limitations. An upper-bound on the number of βη-conversions that appear during the translation of the β-conversions is also presented.
Descrição: Dissertação de Mestrado em Estatística, Matemática e Computação apresentada à Universidade Aberta
URI: http://hdl.handle.net/10400.2/3310
Aparece nas colecções:Mestrado em Estatística, Matemática e Computação / Master's Degree in Statistics, Mathematics and Computation - TMEMC

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
PATNF_Maria_Inácio.pdf419,33 kBAdobe PDFVer/Abrir


FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpace
Formato BibTex MendeleyEndnote Degois 

Todos os registos no repositório estão protegidos por leis de copyright, com todos os direitos reservados.