Please use this identifier to cite or link to this item: http://ridi.ibict.br/handle/123456789/1012
metadata.dc.type: Tese
Title: Nominal Equational Problems Modulo Associativity, Commutativity and Associativity-Commutativity
metadata.dc.creator: de Carvalho-Segundo, Washington L. R.
metadata.dc.contributor.advisor1: Ayala-Rincón, Mauricio
metadata.dc.contributor.advisor-co1: Fernández, Maribel
metadata.dc.contributor.referee1: Nalon, Cláudia
metadata.dc.contributor.referee2: Díaz-Caro, Alejandro
metadata.dc.contributor.referee3: Kutsia, Temur
metadata.dc.contributor.referee4: Ventura, Daniel L.
metadata.dc.description.resumo: 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.
Abstract: The nominal syntax has been used in many application contexts for almost two decades. It is a powerful tool for dealing with variable binding in a concrete manner that can be applied to any specification in which parameters are used to abstract variables, such as in predicates and functions. In the nominal syntax, syntactically different objects can have the same semantics modulo alpha-conversion, as happens in the lambda calculus. Dealing with equality, and in special with alpha-equivalence, is essential in formal languages and implementations. This work investigates the nominal alpha-equivalence with associative (A), commutative (C) and associative-comutative (AC) function symbols. Equalitychecking, matching and unification modulo A, C and AC are investigated. Regarding equality-checking, nominal alpha-equivalence modulo A, C and AC are specified in Coq and proved sound. An algorithm implemented in OCaml for equality-checking modulo A, C and AC is automatically extracted from the specification and experiments are performed using also an improved algorithm. Upper bounds for solving nominal equality-checking problems are given. A rule-based nominal unification modulo C algorithm is specified in Coq and proved sound and complete. By using protected variables, this unification algorithm solves nominal matching problems modulo C, which is formalised to be sound and complete. The rule-based nominal unification algorithm outputs a finite family of sets of fixed point nominal equations. Each of which might have an infinite set of independent solutions. Therefore, nominal unification modulo C or AC are proved to potentially generate infinite independent solutions. This contrasts with syntactic unification modulo C or AC that are known to be in the finitary class. An OCaml implementation of the nominal unification algorithm is provided and used to build examples.
Keywords: 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
metadata.dc.subject.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
metadata.dc.language: eng
metadata.dc.publisher.country: Brasil
Publisher: Universidade de Brasília
metadata.dc.publisher.initials: UnB
metadata.dc.publisher.department: Ciência da Computação
metadata.dc.publisher.program: Programa de Pós-Graduação em Informática
metadata.dc.rights: Acesso Aberto
URI: http://ridi.ibict.br/handle/123456789/1012
Issue Date: 20-Feb-2019
Appears in Collections:Teses de Doutorado

Files in This Item:
File Description SizeFormat 
thesis20190319.pdf2.4 MBAdobe PDFView/Open


This item is protected by original copyright



This item is licensed under a Creative Commons License Creative Commons