Name
Abstract | ||
|---|---|---|
In nominal syntax, variable binding is specified using atom-abstraction constructors, and alpha-equivalence is formalised using freshness constraints and atom swappings, which implement variable renamings. Composition of swappings gives rise to atom permutations. Algorithms to check equivalence, match and unify nominal terms have been extended to deal with terms where some operators are associative and/or commutative. In the case of nominal C-unification, problems are transformed into finite and complete families of fixpoint equations of the form pi.X approximate to(?) X, where pi is a permutation. To generate nominal C-unifiers, a technique to obtain a sound and complete set of solutions for these equations is needed. In this work we show how complete sets of solutions for nominal fixpoint problems are built and discuss efficient techniques to generate solutions based on algebraic properties of permutations. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1007/978-3-319-66167-4_12 | Lecture Notes in Artificial Intelligence |
Field | DocType | Volume |
Discrete mathematics,Associative property,Of the form,Commutative property,Computer science,Permutation,Nominal terms,Equivalence (measure theory),Operator (computer programming),Fixed point | Conference | 10483 |
ISSN | Citations | PageRank |
0302-9743 | 0 | 0.34 |
References | Authors | |
4 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mauricio Ayala-Rincón | 1 | 156 | 31.94 |
| Washington de Carvalho Segundo | 2 | 0 | 1.69 |
| Maribel Fernández | 3 | 315 | 23.44 |
| Daniele Nantes-Sobrinho | 4 | 0 | 0.34 |