Formalização da confluência para sistemas de reescrita ortogonais

Abstract

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.