Use este identificador para citar ou linkar para este item: http://ridi.ibict.br/handle/123456789/1012
Registro completo de metadados
Campo DCValorIdioma
dc.creatorde Carvalho-Segundo, Washington L. R.-
dc.date.accessioned2019-05-06T16:04:02Z-
dc.date.available2019-03-19-
dc.date.available2019-05-06T16:04:02Z-
dc.date.issued2019-02-20-
dc.identifier.urihttp://ridi.ibict.br/handle/123456789/1012-
dc.description.abstractThe 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.pt_BR
dc.description.provenanceSubmitted by Washington Segundo (washingtonsegundo@ibict.br) on 2019-05-06T16:02:20Z No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) thesis20190319.pdf: 2460573 bytes, checksum: a110e47747c4883105433dc23db4d6b6 (MD5)en
dc.description.provenanceApproved for entry into archive by Washington Segundo (washingtonsegundo@ibict.br) on 2019-05-06T16:04:02Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) thesis20190319.pdf: 2460573 bytes, checksum: a110e47747c4883105433dc23db4d6b6 (MD5)en
dc.description.provenanceMade available in DSpace on 2019-05-06T16:04:02Z (GMT). No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) thesis20190319.pdf: 2460573 bytes, checksum: a110e47747c4883105433dc23db4d6b6 (MD5) Previous issue date: 2019-02-20en
dc.description.sponsorshipCoordenação de Aperfeiçoamento de Pessoal de Nível Superiorpt_BR
dc.languageengpt_BR
dc.publisherUniversidade de Brasíliapt_BR
dc.relationhttp://dx.doi.org/10.5281/zenodo.2582109pt_BR
dc.rightsAcesso Abertopt_BR
dc.subjectLógica nominalpt_BR
dc.subjectAlpha-equivalênciapt_BR
dc.subjectUnificação de primeira-ordempt_BR
dc.subjectUnificação nominalpt_BR
dc.subjectUnificação módulo teorias equacionaispt_BR
dc.subjectEquações de ponto fixopt_BR
dc.subjectNominal logicpt_BR
dc.subjectAlpha-equivalencept_BR
dc.subjectFirst-order unificationpt_BR
dc.subjectNominal unificationpt_BR
dc.subjectUnification modulo equational theoriespt_BR
dc.subjectFixed point equationspt_BR
dc.titleNominal Equational Problems Modulo Associativity, Commutativity and Associativity-Commutativitypt_BR
dc.typeTesept_BR
dc.creator.Latteshttp://lattes.cnpq.br/9453481318889500pt_BR
dc.contributor.advisor1Ayala-Rincón, Mauricio-
dc.contributor.advisor1Latteshttp://lattes.cnpq.br/8466420403941522pt_BR
dc.contributor.advisor-co1Fernández, Maribel-
dc.contributor.referee1Nalon, Cláudia-
dc.contributor.referee1Latteshttp://lattes.cnpq.br/7793795625581127pt_BR
dc.contributor.referee2Díaz-Caro, Alejandro-
dc.contributor.referee3Kutsia, Temur-
dc.contributor.referee4Ventura, Daniel L.-
dc.contributor.referee4Latteshttp://lattes.cnpq.br/4443822193261575pt_BR
dc.description.resumoA 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.pt_BR
dc.publisher.countryBrasilpt_BR
dc.publisher.departmentCiência da Computaçãopt_BR
dc.publisher.programPrograma de Pós-Graduação em Informática - UnBpt_BR
dc.publisher.initialsUnBpt_BR
dc.subject.cnpqCNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::TEORIA DA COMPUTACAO::COMPUTABILIDADE E MODELOS DE COMPUTACAOpt_BR
dc.subject.cnpqCNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::TEORIA DA COMPUTACAO::ANALISE DE ALGORITMOS E COMPLEXIDADE DE COMPUTACAOpt_BR
dc.subject.cnpqCNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::MATEMATICA DA COMPUTACAOpt_BR
dc.relation.references[1] T. Aoto and K. Kikuchi. Nominal Confluence Tool. In Proc. of the 8th Int. Joint Conf.: Automated Reasoning (IJCAR), volume 9706 of LNCS, pages 173–182. Springer, 2016. 4 [2] A. B. Avelar, A. L. Galdino, F. L. C. de Moura, and M. Ayala-Rincón. First-order unification in the PVS proof assistant. Logic Journal of the IGPL, 22(5):758–789, 2014. 5 [3] M. Ayala-Rincón, W. Carvalho-Segundo, M. Fernández, and D. Nantes-Sobrinho. Nominal C-Unification. In Proc. of the 27th Int. Symp. Logic-Based Program Synthesis and Transformation (LOPSTR), volume 10855 of LNCS, pages 235–251. Springer, 2017. 5, 7, 72, 107 [4] M. Ayala-Rincón, W. Carvalho-Segundo, M. Fernández, and D. Nantes-Sobrinho. On Solving Nominal Fixpoint Equations. In Proc. of the 11th Int. Symp. on Frontiers of Combining Systems (FroCoS), volume 10483 of LNCS, pages 209–226. Springer, 2017. 7, 107 [5] M. Ayala-Rincón, W. de Carvalho Segundo, M. Fernández, and D. Nantes-Sobrinho. A formalisation of nominal -equivalence with A and AC function symbols. ENTCS, 332:21–38, 2017. 6, 44 [6] M. Ayala-Rincón, W. de Carvalho Segundo, M. Fernández, and D. Nantes-Sobrinho. A Formalisation of Nominal -equivalence with A, C, and AC Function Symbols. TCS, 2019. Accepted manuscript in Theoretical Computer Science. 6, 44 [7] M. Ayala-Rincón, M. Fernández, W. Carvalho-Segundo, and D. Nantes-Sobrinho. A Formalisation of Nominal C-Matching through Unification with Protected Variables. In Pre-proc. of Logical and Semantic Frameworks with Applications (LSFA), to appear in ENTCS, pages 29–41. Elseviser, 2018. 7, 72 [8] M. Ayala-Rincón, M. Fernández, M. J. Gabbay, and A. C. Rocha Oliveira. Checking Overlaps of Nominal Rewriting Rules. ENTCS, 323:39–56, 2016. 4 [9] M. Ayala-Rincón, M. Fernández, and D. Nantes-Sobrinho. Nominal Narrowing. In Proc. of the 1st Int. Conf. on Formal Structures for Computation and Deduction (FSCD), volume 52 of LIPIcs, pages 11:1–11:17. SDLZI, 2016. 6 [10] M. Ayala-Rincón, M. Fernández, and D. Nantes-Sobrinho. Fixed-Point Constraints for Nominal Equational Unification. In Proc. of the 3rd Int. Conf. on Formal Structuresfor Computation and Deduction (FSCD), volume 108 of LIPIcs, pages 7:1–7:16. SDLZI, 2018. 7, 148 [11] M. Ayala-Rincón, M. Fernández, and A. C. Rocha-oliveira. Completeness in PVS of a Nominal Unification Algorithm. ENTCS, 323:57–74, 2016. 5, 32 [12] M. Ayala-Rincón, M. Fernández, A. C. Rocha-Oliveira, and D. L. Ventura. Nominal essential intersection types. Theoretical Computuper Science, 737:62–80, 2018. 5 [13] B. Aydemir, A. Bohannon, and S. Weirich. Nominal Reasoning Techniques in Coq. ENTCS, 174(5):69–77, 2007. 6 [14] F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge UP, 1998. 19 [15] F. Baader and W. Snyder. Unification Theory. In Handbook of Automated Reasoning (in 2 volumes), pages 445–532. Elsevier and MIT Press, 2001. 3 [16] A. Baumgartner, T. Kutsia, J. Levy, and M. Villaret. Nominal Anti-Unification. In Rewriting Techniques and Applications, (RTA), pages 57–73. SDLZI, 2015. 4 [17] D. Benanav, D. Kapur, and P. Narendran. Complexity of Matching Problems. J. of Sym. Computation, 3(1/2):203–216, 1987. 3, 22, 62, 71 [18] A. Boudet and E. Contejean. AC-Unification of Higher-Order Patterns. In Proc. of Principles and Practice of Constraint Programming, volume 1330 of LNCS, pages 267–281. Springer, 1997. 148 [19] A. Boudet, E. Contejean, and H. Devie. A New AC Unification Algorithm with an Algorithm for Solving Systems of Diophantine Equations. Logic in Computer Science, pages 289–299, 1990. 3 [20] T. Braibant and D. Pous. Tactics for Reasoning Modulo AC in Coq. In In Proc. of the 1st. Int. Conf. on Certified Programs and Proofs (CPP), volume 7086 of LNCS, pages 167–182. Springer, 2011. 6 [21] K. F. Brandt, A. Schlichtkrull, and J. Villadsen. Formalization of First-Order Syntactic Unification. In Pre-proc. of the 32nd Int. Workshop on Unification (UNIF), 2018. 5 [22] W. E. Byrd and D. P. Friedman. Kanren: A Fresh Name in Nominal Logic Programming. In Proc. of the Workshop on Scheme and Functional Programming, pages 79–90, 2007. 4 [23] C. F. Calvès. Complexity and implementation of nominal algorithms. PhD Thesis, King’s College London, 2010. 4 [24] C. F. Calvès and M. Fernández. Matching and Alpha-Equivalence Check for Nominal Terms. J. of Computer and System Sciences, 76(5):283–301, 2010. 4, 64, 69, 70 [25] C. F. Calvès and M. Fernández. The First-order Nominal Link. In Proc. of the 20th Int. Symp. Logic-based Program Synthesis and Transformation (LOPSTR), volume 6564 of LNCS, pages 234–248. Springer, 2011. 4, 31[26] J. Cheney. Prolog User’s Guide & Language Reference Version 0.3 DRAFT, 2003. 4 [27] J. Cheney. Relating nominal and higher-order pattern unification. Proceedings of the 19th international workshop on Unification (UNIF 2005), 2005. 4 [28] J. Cheney. Equivariant unification. J. of Autom. Reasoning, 45(3):267–300, 2010. 4 [29] M. Clausen and A. Fortenbacher. Efficient Solution of Linear Diophantine Equations. J. of Sym. Computation, 8(1-2):201–216, 1989. 3 [30] E. Contejean. A Certified AC Matching Algorithm. In Proc. of the 15th Int. Conf. on Rewriting Techniques and Applications (RTA), volume 3091 of LNCS, pages 70–84. Springer, 2004. 6, 133 [31] E. Copello, E. Tasistro, N. Szasz, A. Bove, and M. Fernández. Principles of Alpha- Induction and Recursion for the Lambda Calculus in Constructive Type Theory. ENTCS, 323:109–124, 2016. 6 [32] CoqTeam. The Coq Proof Assistant Reference Manual, 2019. 32 [33] T. H. Cormen, C. E. Leiserson, R. Rivest, and C. Stein. Introduction to Algorithms. The MIT Press, 2009. 71 [34] R. Di Cosmo. Second Order Isomorphic Types: A Proof Theoretic Study on Second Order lambda-Calculus with Surjective Paring and Terminal Object. Inf. Comput., 119(2):176–201, 1995. 149 [35] F. Durán, S. Eker, S. Escobar, N. Martí-Oliet, J. Meseguer, and C. L. Talcott. Associative unification and symbolic reasoning modulo associativity in maude. In Proc. of Rewriting Logic and Its Applications (WLRA), volume 11152 of LNCS, pages 98–114. Springer, 2018. 6 [36] S. M. Eker. Associative-Commutative Matching Via Bipartite Graph Matching. The Computer J., 38:381–399, 1995. 3 [37] S. M. Eker. Associtative-Commutative Rewriting on Large Terms. In Rewriting Techniques and Applications, (RTA), volume 2706 of LNCS, pages 14–29, 2003. 3 [38] François Fages. Associative-Commutative Unification. J. of Sym. Computation, 3:257–275, 1987. 3, 22 [39] E. Fairweather, M. Fernández, N. Szasz, and A. Tasistro. Dependent Types for Nominal Terms with Atom Substitutions. In Int. Conf. on Typed Lambda Calculi and Applications, (TLCA), pages 180–195. SDLZI, 2015. 5 [40] M. Fernández and M. Gabbay. Curry-Style Types for Nominal Terms. In Int. Work. on Types for Proofs and Programs (TYPES), volume 4502 of LNCS, pages 125–139. Springer, 2006. 5 [41] M. Fernández and M. J. Gabbay. Nominal Rewriting. Information and Computation, 205(6):917–965, 2007. 4, 5[42] M. J. Gabbay and A. M. Pitts. A New Approach to Abstract Syntax with Variable Binding. Formal Aspects of Computing, 13(3-5):341–363, 2002. 3 [43] D. Kapur and P. Narendran. NP-Completeness of the Set Unification and Matching Problems. In 8th International Conference on Automated Deduction (CADE), volume 230 of LNCS, pages 489–495. Springer, 1986. 3, 22 [44] D. Kapur and P. Narendran. Matching, Unification and Complexity. SIGSAM Bulletin, 21(4):6–9, 1987. 3, 22 [45] D. Kapur and P. Narendran. Complexity of Unification Problems with Associative- Commutative Operators. J. of Autom. Reasoning, 9(2):261–288, 1992. 3, 22 [46] R. Kumar and M. Norrish. (Nominal) Unification by Recursive Descent with Triangular Substitutions. In Proc. of the 1st Int. Conf. of Interactive Theorem Proving (ITP), volume 6172 of LNCS, pages 51–66. Springer, 2010. 5 [47] D. Larchey-Wendling and J.-F. Monin. Simulating Induction-Recursion for Partial Algorithms. Accepted to TYPES. Available at https://members.loria.fr/DLarchey/ files/papers/TYPES_2018_paper_19.pdf, 2018. 61 [48] J. Levy and M. Villaret. An Efficient Nominal Unification Algorithm. In Proc. of the 21st Int. Conf. on Rewriting Techniques and Applications (RTA), volume 6 of LIPIcs, pages 209–226. SDLZI, 2010. 4, 31 [49] J. Levy and M. Villaret. Nominal unification from a higher-order perspective. ACM Trans. Comput. Log., 13(2):10:1–10:31, 2012. 4 [50] G. S. Makanin. The Problem of Solvability of Equations in a Free Semigroup. Math. USSR Sbornik, 32(2):129–198, 1977. 17, 22, 149 [51] A Martelli and U. Montanari. Unification in linear time and space: A structured presentation. Technical report, Ist. di Elaborazione delle Informazione, Consiglio Nazionale delle Ricerche, Pisa, Italy, 1976. Internal Rep. B76-16. 3, 16, 22 [52] A. Martelli and U. Montanari. An Efficient Unification Algorithm. ACM Transactions on Programming Languages and Systems, 4(2):258–282, 1982. 16 [53] D. Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. J. Log. Comput., 1(4):497–536, 1991. 4 [54] T. Nipkow. Equational Reasoning in Isabelle. Science of Computer Programming, 12(2):123–149, 1989. 6 [55] T. Nipkow. Functional unification of higher-order patterns. In Proc. of the Eighth Annual Symp. on Logic in Computer Science (LICS), pages 64–74. IEEE, 1993. 4 [56] M. S. Paterson and M. N. Wegman. Linear Unification. J. of Computer and System Sciences, 16(2):158–167, 1978. 3, 4, 16, 22 [57] A. M. Pitts. Nominal Logic, a First Order Theory of Names and Binding. Information and Computation, 186(2):165–193, 2003. 3, 22[58] A. M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge UP, 2013. 3 [59] Z. Qian and K. Wang. Modular AC unification of higher-order patterns. In Proc. of the First Int. Conf. Constraints in Computational Logics, volume 845 of LNCS, pages 105–120. Springer, 1994. 148 [60] J. A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. J. of the ACM, 12(1):23–41, 1965. 3, 13, 22 [61] A. C. Rocha-Oliveira. Unificação, confluência e tipos com interseção para sistemas de reescrita nominal. PhD thesis, Universidade de Brasília (UnB), 2016. 5, 32 [62] Sagan, B. E. The Symmetric Group: Representations, Combinatorial Algorithms, and Symmetric Functions. Springer, 2nd edition, 2001. 107 [63] M. Schmidt-Schauß, T. Kutsia, J. Levy, and M. Villaret. Nominal Unification of Higher Order Expressions with Recursive Let. In Post-proc. of the 26th Int. Sym. on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), volume 10184 of LNCS, pages 328–344. Springer, 2017. 7 [64] J. H. Siekmann. Unification of Commutative Terms. In Proc. of the Int. Symposium on Symbolic and Algebraic Manipulation, volume 72 of LNCS, pages 22–29. Springer, 1979. 3, 18 [65] M. Sozeau. Subset Coercions in Coq. In Proc. of the Int. Work. on Types for Proofs and Programs (TYPES), volume 4502 of LNCS, pages 237–252. Springer, 2006. 61 [66] M. Sozeau. Equations: A Dependent Pattern-Matching Compiler. In Proc. of the 1st Int. Conf. of Interactive Theorem Proving (ITP), volume 6172 of LNCS, pages 419–434. Springer, 2010. 58 [67] M. E. Stickel. A Unification Algorithm for Associative-Commutative Functions. J. of the Association for Computing Machinery, 28(3):423–434, 1981. 3, 19, 22 [68] E. Tiden and S. Arnborg. Unification Problems with One-Sided Distributivity. J. of Sym. Computation, 3:183–202, 1987. 22 [69] C. Urban. Nominal Techniques in Isabelle/HOL. J. of Autom. Reasoning, 40(4):327– 356, 2008. 5 [70] C. Urban. Nominal Unification Revisited. In Proc. of the 24th Int. Work. on Unification (UNIF), volume 42 of EPTCS, pages 1–11, 2010. 5, 32 [71] C. Urban and C. Kaliszyk. General Bindings an Alpha-Equivalence in Nominal Isabelle. Logical Methods in Computer Science, 8:1–35, 2012. 6 [72] C. Urban, A. M. Pitts, and M. J. Gabbay. Nominal Unification. Theoretical Computer Science, 323(1-3):473–497, 2004. 3, 4, 5, 26, 31, 32 [73] Z. Qian. Linear Unification of Higher-Order Patterns. Theory and Practice of Software Development, pages 391–405, 1993. 4pt_BR
Aparece nas coleções:Teses de Doutorado

Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
thesis20190319.pdf2,4 MBAdobe PDFVisualizar/Abrir


Este arquivo é protegido por direitos autorais

Ver licença
Mostrar registro simples do item Recomendar este item Visualizar estatísticas