Nominal Equational Problems Modulo Associativity, Commutativity and Associativity-Commutativity

• Ano de defesa: 2019
• Autor(a) principal: de Carvalho-Segundo, Washington L. R.
• Orientador(a): Ayala-Rincón, Mauricio
• Banca de defesa: Nalon, Cláudia , Díaz-Caro, Alejandro , Kutsia, Temur, Ventura, Daniel L.
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: eng
• Instituição de defesa: Universidade de Brasília
• Programa de Pós-Graduação: Programa de Pós-Graduação em Informática - UnB
• Departamento: Ciência da Computação
• País: Brasil
• Palavras-chave em Português: Lógica nominal; Alpha-equivalência; Unificação de primeira-ordem; Unificação nominal; Unificação módulo teorias equacionais; Equações de ponto fixo; Nominal logic; Alpha-equivalence; First-order unification; Nominal unification; Unification modulo equational theories; Fixed point equations
• Área do conhecimento CNPq: CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::TEORIA DA COMPUTACAO::COMPUTABILIDADE E MODELOS DE COMPUTACAO; CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::TEORIA DA COMPUTACAO::ANALISE DE ALGORITMOS E COMPLEXIDADE DE COMPUTACAO; CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::MATEMATICA DA COMPUTACAO
• Link de acesso: http://ridi.ibict.br/handle/123456789/1012

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.