Use este identificador para citar ou linkar para este item: http://repositorio.unb.br/handle/10482/8787
Título: Cálculos de substituições explícitas à la de Bruijn com sistemas de tipos com interseção
Autor(es): Ventura, Daniel Lima
Orientador(es): Ayala-Rincón, Mauricio
Assunto: Computação - matemática
Matemática
Data de publicação: 29-Jun-2011
Data de defesa: 5-Mar-2010
Citação: VENTURA, Daniel Lima. Cálculos de substituições explícitas à la de Bruijn com sistemas de tipos com interseção. 2010. xiii, 187 f., il. Dissertação (Mestrado em Matemática)-Universidade de Brasília, Brasília, 2010.
Resumo: 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.
Descrição: Dissertação (Mestrado em Matemática)-Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, Brasília, 2010.
Aparece nas coleções:MAT - Mestrado em Matemática (Dissertações)

Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
2010_DanielLimaVentura.pdf921,44 kBAdobe PDFVisualizar/Abrir


Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.