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

Abstract

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.