Portal de Periódicos da CAPES

Capítulo de livro Acesso aberto Produção Nacional Revisado por pares

BIBTEX RIS

On Solving Nominal Fixpoint Equations

2017; Springer Science+Business Media; Linguagem: Inglês

10.1007/978-3-319-66167-4_12

1611-3349

Maurício Ayala-Rincón, Washington Luís Ribeiro de Carvalho Segundo, Maribel Fernández, Daniele Nantes-Sobrinho,

Formal Methods in Verification

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 , 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.