Closed nominal rewriting and efficiently computable nominal algebra equality

TL;DR

This paper explores the connection between nominal algebra and rewriting, introducing a concise framework for equational reasoning and identifying a subclass where rewriting fully captures algebraic equality, including lambda calculus and logic.

Contribution

It presents a new presentation of nominal equational deduction and characterizes a subclass where rewriting is complete for algebraic equality.

Findings

A new concise presentation of nominal equational deduction.

Characterization of a subclass where rewriting is complete.

Includes lambda-calculus and first-order logic specifications.

Abstract

We analyse the relationship between nominal algebra and nominal rewriting, giving a new and concise presentation of equational deduction in nominal theories. With some new results, we characterise a subclass of equational theories for which nominal rewriting provides a complete procedure to check nominal algebra equality. This subclass includes specifications of the lambda-calculus and first-order logic.