Many formal languages include binders as well as operators that satisfy equational axioms, such as commutativity. Here we consider the nominal language, a general formal framework which provides support for the representation of binders, freshness conditions and \(\alpha \) -renaming. Rather than relying on the usual freshness constraints, we introduce a nominal algebra which employs permutation fixed-point constraints in \(\alpha \) -equivalence judgements, seamlessly integrating commutativity into the reasoning process. We establish its proof-theoretical properties and provide a sound and complete semantics in the setting of nominal sets. Additionally, we propose a novel algorithm for nominal unification modulo commutativity, which we prove terminating and correct. By leveraging fixed-point constraints, our approach ensures a finitary unification theory, unlike standard methods relying on freshness constraints. This framework offers a robust foundation for structural induction and recursion over syntax with binders and commutative operators, enabling reasoning in settings such as first-order logic and the \(\pi \) -calculus.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Equational Reasoning Modulo Commutativity in Languages with Binders

  • Ali K. Caires-Santos,
  • Maribel Fernández,
  • Daniele Nantes-Sobrinho

摘要

Many formal languages include binders as well as operators that satisfy equational axioms, such as commutativity. Here we consider the nominal language, a general formal framework which provides support for the representation of binders, freshness conditions and \(\alpha \) -renaming. Rather than relying on the usual freshness constraints, we introduce a nominal algebra which employs permutation fixed-point constraints in \(\alpha \) -equivalence judgements, seamlessly integrating commutativity into the reasoning process. We establish its proof-theoretical properties and provide a sound and complete semantics in the setting of nominal sets. Additionally, we propose a novel algorithm for nominal unification modulo commutativity, which we prove terminating and correct. By leveraging fixed-point constraints, our approach ensures a finitary unification theory, unlike standard methods relying on freshness constraints. This framework offers a robust foundation for structural induction and recursion over syntax with binders and commutative operators, enabling reasoning in settings such as first-order logic and the \(\pi \) -calculus.