[FOM] Question about "fresh" variables/objects in logics
Andrej.Bauer at andrej.com
Sun Nov 27 05:18:51 EST 2005
Divianszky Peter wrote:
> Does anybody know of a formal description of the concept of "fresh"
> variable/object in logic?
You'd be better off asking computer scientists about this :-)
I believe you are looking for "nu calculus", which was (correct me if I
am wrong) proposed by A. Pitts and J. Gabbay. The paper I am aware of is
A New Approach to Abstract Syntax Involving Binders (1999)
Murdoch Gabbay, Andrew Pitts (LICS'99)
but there is probably an earlier one (it would be best to hear from
horse's mouth). They use permutation models of set theory to establish
their results. You may also look at the related work
Marcelo Fiore, Gordon Plotkin and Daniele Turi
Abstract Syntax and Variable Binding
For games semantics of nu calculus, search for "nominal games" by
S. Abramsky, D. Ghica, A. Murawski, L. Ong and I. Stark.
Depending on what you want to do, Aleksandar Nanevski's Ph.D. thesis
"Functional Programming with Names and Necessity" may also be of
interest, see http://www.eecs.harvard.edu/~aleks/thesis/thesis.ps
(references [PG00] and [Pit01] therein refer to Pitt's and Gabbay's
other relevant work).
More information about the FOM