Cálculos de substituições explícitas à la de Bruijn com sistemas de tipos com interseção

Abstract

O calculus é um modelo teórico de computação tão antigo quanto a própria noção de função computável. Devido a definição da substituição como uma metaoperação. existem várias formas de tornar esta substituição explícita no sistema, dando surgimento a uma grande variedade de sistemas baseados no calculus. Estudamos dois cálculos de substituições explícitas, o e o se, com sistemas de tipos com interseção. Estes cálculos utilizam uma notação à la de Bruijn, onde variáveis são representadas por índices ao invés de nomes. Sistemas de atribuição de tipos permitem uma análise sintática (estática) de propriedades semânticas (dinâmicas) de programas, dispensando qualquer declaração de tipos dentro destes. Os tipos com interseção apresentam uma maneira de integrar polimorfismo ao sistema, que tem se mostrado conveniente computacionalmente com propriedades como a tipagem principal, que permite, e.g a compilação separada e a recompilação inteligente para o sistema de tipos computacionais. Para a adição de tipos com interseção aos cálculos estudados, fazemos um estudo do calculus à la de Bruijn com dois sistemas de tipos diferentes. Uma caracterização sintática de tipagens principais, para termos irredutíveis, em um dos sistemas é apresentada. Baseado neste sistema, introduzimos sistemas de tipos com interseção para e o se. A propriedade básica de redução de sujeito, que garante a preservação dos tipos em qualquer computação possível para termos tipáveis, é analisada nas variações dos sistemas propostos. Outra propriedade analisada é a relevância do sistema, garantindo que apenas a informação de tipos necessária para inferência é utilizada, impossibilitando a admissibilidade de uma lei de redundância para o sistema de tipos. ______________________________________________________________________________________ ABSTRACT

The ג-calculus is a well known theoretical computation model as old as the concept of computable functions. Due to the substitution definition as a meta-operator there exists a great quantity of variations of this computational system in which the operation of substitution is treated explicitly. In this work we investigate intersection type systems for two explicit substitution calculi, the גσ and the גse, both with de Bruijn indices. Type assignment systems allow one to have a static code analysis through implicit typing inference, where no type declaration is required. Intersection types present a machine friendly way to add polymorphism to type systems with features such as the principal typing property, allowing e.g. a separate compilation and the smartest recompilation. We study the ג–calculus with de Bruijn indices with two diferente type systems, in a preliminary step for adding intersection types for both explicit substitution calculi. A characterisation for principal typíngs of irreducibe terms is a given in on of the systems, wich the intersection type systems for each גσ and גse are basead on. We analyse the subject reduction property, which guarantees that all terms of the system preserve their types during any possible computation, in some variations for the proposed type systems. Another analysed property is the relevance, in which only necessary suppositions are allowed in a typing inference, turning a weakening rule inadmissible in the type system.