Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2012. / Submitted by Alaíde Gonçalves dos Santos (alaide@unb.br) on 2012-12-20T11:22:37Z
No. of bitstreams: 1
2012_AnaCristinaRochaOliveira.pdf: 577195 bytes, checksum: 05058096982215ccfe447e66ab499abf (MD5) / Approved for entry into archive by Guimaraes Jacqueline(jacqueline.guimaraes@bce.unb.br) on 2012-12-20T14:08:41Z (GMT) No. of bitstreams: 1
2012_AnaCristinaRochaOliveira.pdf: 577195 bytes, checksum: 05058096982215ccfe447e66ab499abf (MD5) / Made available in DSpace on 2012-12-20T14:08:41Z (GMT). No. of bitstreams: 1
2012_AnaCristinaRochaOliveira.pdf: 577195 bytes, checksum: 05058096982215ccfe447e66ab499abf (MD5) / Ortogonalidade é uma característica da programação que consiste, de uma maneira
sintática, em garantir o determinismo de especificações funcionais. Essencialmente, a
ortogonalidade não permite, por um lado, a ambiguidade inerente do não determinismo,
isto é, a existência de diferentes regras que especificam a mesma função e que podem ser aplicadas simultaneamente (não ambiguidade) e, por outro, também proíbe a repetição de variáveis no lado esquerdo dessas regras (linearidade à esquerda). Na teoria dos Sistemas de Reescrita de Termos (TRSs), determinismo é identificado pela renomada propriedade de confluência, que basicamente a rma que sempre que houver possibilidades de simplificações ou computações diferentes de um termo, as respostas computadas ou os termos reduzidos obtidos devem coincidir. Embora a prova seja tecnicamente elaborada, confluência é bem conhecida como uma consequência da ortogonalidade. Dessa forma, ortogonalidade é uma importante característica matemática intrínseca especificação de funções recursivas, sendo naturalmente aplicada em programação e especificações funcionais. A começar pela formalização da teoria de TRSs no assistente de provas PVS, esse trabalho descreve como a confluência de TRSs ortogonais estão sendo formalizada utilizando essa ferramenta. Progressos substanciais foram constatados nessa
pesquisa, obtendo-se até o presente momento formalizações completas para propriedades
similares, por em com restrições, tais como a formalização completa para a propriedade
de confluência de TRS's não ambíguos e lineares (à esquerda e à direita). _______________________________________________________________________________________ ABSTRACT / Orthogonality is a discipline of programming that in a syntactic manner guarantees
determinism of functional specifications. Essentially, orthogonality avoids, on the one
side, the inherent ambiguity of non determinism, prohibiting the existence of different rules that specify the same function and that may apply simultaneously (non-ambiguity), and, on the other side, it eliminates the possibility of occurrence of repetitions of variables in the left-hand side of these rules (left linearity). In the theory of term rewriting systems (TRSs) determinism is captured by the well-known property of confluence, that basically states that whenever different computations or simplifications from a term are possible, the computed answers or the obtained reduced terms should coincide. Although the proof is technically elaborated, confluence is well-known to be a consequence of
orthogonality. Thus, orthogonality is an important mathematical discipline intrinsic to the specification of recursive functions that is naturally applied in functional programming and specification. Starting from a formalization of the theory of TRSs in the proof assistant PVS, this work describes how confluence of orthogonal TRSs is being formalized in this proof assistant. Substantial progress has been done in this research, obtaining until now complete formalizations for some similar, but restricted properties, such as a complete
formalization for the property of confluence of non ambiguous and (left and right) linear TRSs.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.unb.br:10482/11845 |
| Date | 17 August 2012 |
| Creators | Oliveira, Ana Cristina Rocha |
| Contributors | Ayala-Rincón, Mauricio |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UnB, instname:Universidade de Brasília, instacron:UNB |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0063 seconds