Nominal (universal) algebra: equational logic with names and binding

By Murdoch J. Gabbay and Aad Mathijssen, in the Journal of Logic and Computation, available from Murdoch J. Gabbay’s website:

In informal mathematical discourse (such as the text of a paper on theoretical computer science) we often reason about equalities involving binding of object-variables. We find ourselves writing assertions involving meta-variables and capture-avoidance constraints on where object-variables can and cannot occur free. Formalising such assertions is problematic because the standard logical frameworks cannot express capture-avoidance constraints directly.
In this paper we make the case for extending the logic of equality with meta-variables and capture-avoidance constraints, to obtain ‘nominal algebra’. We use nominal techniques that allow for a direct formalisation of meta-level assertions, while remaining close to informal practice. We investigate proof-theoretical properties, we provide a sound and complete semantics in nominal sets, and we compare and contrast our design decisions with other possibilities leading to similar systems.

0 Responses to “Nominal (universal) algebra: equational logic with names and binding”

  1. Leave a Comment

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: