Tese (doutorado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2016. / Submitted by Fernanda Percia França (fernandafranca@bce.unb.br) on 2017-02-01T15:08:06Z
No. of bitstreams: 1
2016_AnaCristinaRochaOliveiraValverde.pdf: 879616 bytes, checksum: b64378498855c30cf60d6faa9518461c (MD5) / Approved for entry into archive by Raquel Viana(raquelviana@bce.unb.br) on 2017-02-01T19:13:19Z (GMT) No. of bitstreams: 1
2016_AnaCristinaRochaOliveiraValverde.pdf: 879616 bytes, checksum: b64378498855c30cf60d6faa9518461c (MD5) / Made available in DSpace on 2017-02-01T19:13:19Z (GMT). No. of bitstreams: 1
2016_AnaCristinaRochaOliveiraValverde.pdf: 879616 bytes, checksum: b64378498855c30cf60d6faa9518461c (MD5) / 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. / 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.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.unb.br:10482/22387 |
| Date | 15 September 2016 |
| Creators | Valverde, Ana Cristina Rocha Oliveira |
| Contributors | Fernández, Maribel, Ayala-Rincón, Mauricio |
| Source Sets | IBICT Brazilian ETDs |
| Language | Inglês |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis |
| Source | reponame:Repositório Institucional da UnB, instname:Universidade de Brasília, instacron:UNB |
| Rights | 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., info:eu-repo/semantics/openAccess |
Page generated in 0.0018 seconds