dc.contributor | Ayala-Rincón, Mauricio | |
dc.contributor | Fernández, Maribel | |
dc.creator | Carvalho Segundo, Washington Luís Ribeiro de | |
dc.date.accessioned | 2019-09-27T19:03:35Z | |
dc.date.accessioned | 2022-10-04T15:12:54Z | |
dc.date.available | 2019-09-27T19:03:35Z | |
dc.date.available | 2022-10-04T15:12:54Z | |
dc.date.created | 2019-09-27T19:03:35Z | |
dc.date.issued | 2019-09-27 | |
dc.identifier | CARVALHO SEGUNDO, Washington Luís Ribeiro de. Nominal equational problems modulo associativity, commutativity and associativity-commutativity. 2019. xi, 161 f., il. Tese (Doutorado em Informática)—Universidade de Brasília, Brasília, 2019. | |
dc.identifier | http://repositorio.unb.br/handle/10482/35474 | |
dc.identifier.uri | http://repositorioslatinoamericanos.uchile.cl/handle/2250/3858826 | |
dc.description.abstract | A sintaxe nominal tem sido utilizada em vários contextos por quase duas décadas. Ela é
uma ferramenta poderosa para se lidar com ligação de variáveis de uma forma concreta,
que pode ser aplicada a qualquer especificação na qual parâmetros são utilizados para se
abstrair variáveis, tal como em predicados e funções. Na sintaxe nominal, objetos que
são sintaticamente diferentes podem ter a mesma semântica módulo alfa-conversão, tal
como acontece no Cálculo Lambda. O tratamento de igualdades, em especial a alphaequivalêcia,
é algo essencial em linguagens formais e implementações. Este trabalho investiga
a alpha-equivalência nominal com símbolos de função associativos (A), comutativos
(C) e associativos-comutativos (AC). Verificação de equivalência, casamento e unificação
módulo A, C e AC são investigados. Em relação a verificação de igualdade, as alphaequivalências
nominais módulo A, C e AC foram especificadas em Coq e provadas ser
corretas. Um algoritmo implementado em OCaml para verificação de igualdade módulo
A, C e AC é automaticamente extraído da especificação e experimentos são executados
utilizando-se também um algoritmo aperfeiçoado. Limites superiores para o tempo de
execução na solução de problemas nominais de verificação equacional são fornecidos. Um
algoritmo de unificação módulo C baseado em regras de redução é especificado em Coq
e provado ser correto e completo. Por meio do uso de variáveis protegidas, este algoritmo
de unificação resolve problemas de casamento nominal módulo C, o que foi também
formalizado ser correto e completo. O algoritmo de unificação baseado em regras de redução
fornece uma família finita de conjuntos de equações nominais de ponto fixo. Cada
uma destas equações pode ter um conjunto infinito de soluções independentes. Portanto,
demonstra-se que problemas de unificação nominal módulo C e AC podem gerar um conjunto
infinito de soluções independentes. Este fato contrasta com unificação sintática
módulo C ou AC, que são conhecidas por estar na classe finitária de problemas. Uma
implementação em OCaml do algoritmo de unificação nominal é fornecida e utilizado para
se construir exemplos. | |
dc.language | Inglês | |
dc.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. | |
dc.rights | Acesso Aberto | |
dc.title | Nominal equational problems modulo associativity, commutativity and associativity-commutativity | |
dc.type | Tesis | |