Archive for the 'Nominal algebra' Category

Closed nominal rewriting and efficiently computable nominal algebra equality

By Maribel Fernandez and Murdoch J. Gabbay, from LFMTP 2010, available from Murdoch J. Gabbay’s website:

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 lambda-calculus and first-order logic.

Universal algebra over lambda-terms and nominal terms: the connection in logic between nominal techniques and higher-order variables

By Murdoch J. Gabbay and Dominic P. Mulligan, from LFMTP 2009, available from Murdoch J. Gabbay’s website:

This paper develops the correspondence between equality reasoning with axioms using λ-terms syntax, and reasoning using nominal terms syntax. Both syntaxes involve name-abstraction: λ-terms represent functional abstraction; nominal terms represent atomsabstraction in nominal sets.

It is not evident how to relate the two syntaxes because their intended denotations are so different. We use universal algebra, the logic of equational reasoning, a logical foundation based on an equality judgement form which is spartan but which is sufficiently expressive to encode mathematics in theory and practice.

We investigate how syntax, algebraic theories, and derivability relate across λ-theories (algebra over λ-terms) and nominal algebra theories.