Skip navigation
Please use this identifier to cite or link to this item: http://repositorio.unb.br/handle/10482/22387
Files in This Item:
File Description SizeFormat 
2016_AnaCristinaRochaOliveiraValverde.pdf859 kBAdobe PDFView/Open
Title: Unificação, confluência e tipos com interseção para sistemas de reescrita nominal
Authors: Valverde, Ana Cristina Rocha Oliveira
Orientador(es):: Ayala-Rincón, Mauricio
Coorientador(es):: Fernández, Maribel
Assunto:: Sistemas nominais
Sistemas de computação
Sintaxe
Issue Date: 1-Feb-2017
Citation: VALVERDE, Ana Cristina Rocha Oliveira. Unificação, confluência e tipos com interseção para sistemas de reescrita nominal. 2016. x, 89 f., il. Tese (Doutorado em Informática)—Universidade de Brasília, Brasília, 2016.
Abstract: Sistemas nominais são uma abordagem alternativa para o tratamento de variáveis em sistemas computacionais, onde a reescrita de primeira ordem é generalizada através do suporte para especificação de ligação de variáveis e de _-equivalência, fazendo uso do conceito de freshness e da troca bijetiva de nomes (swapping). Teoremas bem conhecidos em reescrita de primeira ordem podem ser adaptados a fim de serem adicionalmente válidos em reescrita nominal. Nesta tese, nós analisamos sob que condições a confluência de sistemas de reescrita e o Critério dos Pares Críticos são válidos para a reescrita nominal, assim como para a reescrita nominal fechada (que é uma noção de reescrita mais eficiente nesse contexto). As condições definidas aqui são de fácil checagem através de um algoritmo de unificação nominal. A unificação nominal foi inicialmente estudada por Urban, Pitts e Gabbay e formalizada por Urban no assistente de prova Isabelle/HOL. Neste trabalho, são também apresentadas uma especificação nova de unificação nominal na linguagem do PVS e uma formalização da sua terminação, correção e completude. Em nossa especificação, ao invés de aplicar regras de simplificação a condições restritivas de unificação e freshness, soluções para um problema de unificação são construídas recursivamente através de uma especificação funcional direta, obtendo uma formalização que é mais próxima a implementações algorítmicas. Esta formalização é o passo inicial com vistas a ter mais resultados formalizados sobre reescrita nominal em PVS, onde um forte arcabouço de sistemas de reescrita de termos já é disponibilizado. Ademais, um sistema de tipos com interseção para termos nominais é apresentado. O sistema de tipos presente possui a importante propriedade de redução do sujeito para uma noção especializada de reescrita nominal tipada, o que significa que a tipabilidade no sistema é coerente com execuções computacionais.
Abstract: Nominal systems are an alternative approach for the treatment of variables in computational systems where first-order rewriting is generalised by providing support for the specification of binding operators and α-equivalence using the notions of freshness and name swapping. Famous theorems in the context of first-order rewriting can be adapted for nominal rewriting as well. In this thesis, we analyse the conditions under which confluence of orthogonal rewrite systems and the Critical Pair Criterion hold for nominal rewriting as well as for closed nominal rewriting (an efficient notion of rewriting in this context). The conditions we define are easy to check using a nominal unification algorithm. Nominal unification was initially studied by Urban, Pitts and Gabbay and then first formalised by Urban in the proof assistant Isabelle/HOL. In this work, we also present a new specification of nominal unification in the language of PVS and a formalisation of its termination, soundness and completeness. In our specification, instead of applying simplification rules to unification and freshness constraints, we recursively build solutions for the original problem through a straightforward functional specification, obtaining a formalisation that is closer to algorithmic implementations. This formalisation is a first step in order to have more formalised results about nominal rewriting in PVS, where a huge background for term rewriting system is already available. Additionally, an inter- section type system is presented for nominal terms. The present type system possesses the important property of subject reduction for a specialised notion of typed nominal rewriting, that means the soundness of typability under computational execution.
Description: Tese (doutorado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2016.
Licença:: A concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor com as seguintes condições: Na qualidade de titular dos direitos de autor da publicação, autorizo a Universidade de Brasília e o IBICT a disponibilizar por meio dos sites www.bce.unb.br, www.ibict.br, http://hercules.vtls.com/cgi-bin/ndltd/chameleon?lng=pt&skin=ndltd sem ressarcimento dos direitos autorais, de acordo com a Lei nº 9610/98, o texto integral da obra disponibilizada, conforme permissões assinaladas, para fins de leitura, impressão e/ou download, a título de divulgação da produção científica brasileira, a partir desta data.
Appears in Collections:CIC - Doutorado em Informática (Teses)

Show full item record Recommend this item " class="statisticsLink btn btn-primary" href="/handle/10482/22387/statistics">



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.