Polimorfismo atómico e o teorema da normalização forte

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.

Author dc:creator

• Inácio, Maria do Rosário Dinis

Advisors dc:contributor.advisor

• Edmundo, Mário Jorge
• Ferreira, Gilda

• 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

Language dc:language.iso

por

Identifier URI

urn:tid:201139057

OAI identifier oai:identifier

oai:repositorioaberto.uab.pt:10400.2/3310