Views provided by UsageCounts
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.
:CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::TEORIA DA COMPUTACAO::ANALISE DE ALGORITMOS E COMPLEXIDADE DE COMPUTACAO [CNPQ], Unification modulo equational theories, CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::MATEMATICA DA COMPUTACAO, Alpha-equivalência, First-order unification, Unificação módulo teorias equacionais, 004, :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::MATEMATICA DA COMPUTACAO [CNPQ], CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::TEORIA DA COMPUTACAO::COMPUTABILIDADE E MODELOS DE COMPUTACAO, Alpha-equivalence, Unificação nominal, Unificação de primeira-ordem, CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::TEORIA DA COMPUTACAO::ANALISE DE ALGORITMOS E COMPLEXIDADE DE COMPUTACAO, Equações de ponto fixo, Nominal logic, Fixed point equations, Lógica nominal, Nominal unification
:CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::TEORIA DA COMPUTACAO::ANALISE DE ALGORITMOS E COMPLEXIDADE DE COMPUTACAO [CNPQ], Unification modulo equational theories, CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::MATEMATICA DA COMPUTACAO, Alpha-equivalência, First-order unification, Unificação módulo teorias equacionais, 004, :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::MATEMATICA DA COMPUTACAO [CNPQ], CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::TEORIA DA COMPUTACAO::COMPUTABILIDADE E MODELOS DE COMPUTACAO, Alpha-equivalence, Unificação nominal, Unificação de primeira-ordem, CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::TEORIA DA COMPUTACAO::ANALISE DE ALGORITMOS E COMPLEXIDADE DE COMPUTACAO, Equações de ponto fixo, Nominal logic, Fixed point equations, Lógica nominal, Nominal unification
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
| views | 1 |

Views provided by UsageCounts