Nominal (Universal) Algebra: Equational Logic with Names and Binding
Citations Over TimeTop 1% of 2009 papers
Abstract
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 captureavoidance constraints on where object-variables can and cannot occur free. Formalizing such assertions is problematic because the standard logical frameworks cannot express capture-avoidance constraints directly. In this article, 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 formalization 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.
Related Papers
- → Contrast adaptation may enhance contrast discrimination(2002)48 cited
- → A Note on Maximized Posttest Contrasts(1979)1 cited
- → Contrast in visual selective attention: just another feature?(2010)
- Analysis of the Difference of Chinese and English According to Thinking Models(2004)
- Defining and Classifying "Contrast" as a Semantic Category in Modern Chinese(2009)