BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:A Canonical Local Representation of Binding - Masa
hiko Sato (Graduate School of Informatics\, Kyoto
University)
DTSTART;TZID=Europe/London:20090918T140000
DTEND;TZID=Europe/London:20090918T150000
UID:TALK19058AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/19058
DESCRIPTION:In this talk\, we address the problem of concrete
representation of\nlambda terms which can handle t
he subtle problem of defining\nsubstitution operat
ion on lambda terms neatly.\n\nIn defining lambda
terms it has been more common to use only one sort
\nof symbols for both global and local variables.
However\,\nhistorically\, Frege and later Gentzen
already used two sorts of\nsymbols\, and recently
advantage of using two sorts of symbols has come\
nto be recognized in computer science\, and we tak
e this approach here.\n\nOur definition of lambda
terms is carried out in two steps.\n\nIn the first
step\, we introduce a notion of B-algebras which
captures\nthe notion of variable binding as a bina
ry algebraic operation on\nvariables (represented
by atoms) and elements of the algebra.\n\nIn the s
econd step\, we use the free B-algebra $\\sexpr[\\
atom]$ over a\nfixed set of atoms and define lambd
a terms as a subset of\n$\\sexpr[\\atom]$. Elemen
ts of $\\sexpr[\\atom]$ are called _sexprs_\nsince
$\\sexpr[\\atom]$ is a natural extension of Lisp
symbolic\nexpressions introduce by McCarthy. Choo
sing such a subset is a\nnontrivial task\, since t
he subset of the algebra must not only be\nclosed
under substitution but also it must be closed unde
r the\noperation of instantiation which instantiat
e a lambda abstract with an\narbitrary lambda term
.\n\nWe remark here that we cannot use $\\sexpr[\\
atom]$ itself as the set of\nlambda-terms for the
following two reasons.\n\nThe first reason is that
local variables may appear unbound (or free)\nin
sexprs\, although it is necessary that a local var
iable must always\nappear within the scope of a bi
nder which binds the variable. A\ntrivial example
is a local variable\, that is\, an atom itself.
This\nproblem can be fixed by choosing a subset of
$\\sexpr[\\atom]$ with no\nunbound local variable
s. An sexpr with this property is called _variabl
e closed_ and McKinna-Pollack observed that substi
tution\noperation is capture-avoiding and hence sa
fe on variable-closed sexps.\n\nHowever\, variable
-closed sexprs cannot canonically represent\nlambd
a-terms since different sexprs can be alpha-equiva
lent\, e.g.\, \n λx.x and λy.y. This is the sec
ond reason why\n$\\sexpr[\\atom]$ itself cannot se
rve as the set of lambda-terms.\n\nIn our previous
work we solved the second difficulty above by\nin
troducing a specific concrete subset of $\\sexpr[\
\atom]$. In this\ntalk we will generalize the wor
k and give a general criteria which can\nbe used t
o characterize subsets of $\\sexpr[\\atom]$ which
canonically\n(that is no two distinct but alpha eq
uivalent sexprs are in the\nsubset) represent lamb
da-terms.\n\nThis is a joint work with Randy Polla
ck.\n
LOCATION:Room FW11\, Computer Laboratory\, William Gates Bu
ilding
CONTACT:Matthew Parkinson
END:VEVENT
END:VCALENDAR