BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:A Canonical Local Representation of Binding - Masahiko Sato (Gradu
 ate School of Informatics\, Kyoto University)
DTSTART:20090918T130000Z
DTEND:20090918T140000Z
UID:TALK19058@talks.cam.ac.uk
CONTACT:Matthew Parkinson
DESCRIPTION:In this talk\, we address the problem of concrete representati
 on of\nlambda terms which can handle the subtle problem of defining\nsubst
 itution operation on lambda terms neatly.\n\nIn defining lambda terms it h
 as been more common to use only one sort\nof symbols for both global and l
 ocal 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 take this
  approach here.\n\nOur definition of lambda terms is carried out in two st
 eps.\n\nIn the first step\, we introduce a notion of B-algebras which capt
 ures\nthe notion of variable binding as a binary algebraic operation on\nv
 ariables (represented by atoms) and elements of the algebra.\n\nIn the sec
 ond step\, we use the free B-algebra $\\sexpr[\\atom]$ over a\nfixed set o
 f atoms and define lambda 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.  Ch
 oosing such a subset is a\nnontrivial task\, since the subset of the algeb
 ra must not only be\nclosed under substitution but also it must be closed 
 under the\noperation of instantiation which instantiate a lambda abstract 
 with an\narbitrary lambda term.\n\nWe remark here that we cannot use $\\se
 xpr[\\atom]$ itself as the set of\nlambda-terms for the following two reas
 ons.\n\nThe first reason is that local variables may appear unbound (or fr
 ee)\nin sexprs\, although it is necessary that a local variable must alway
 s\nappear within the scope of a binder which binds the variable.  A\ntrivi
 al 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 lo
 cal variables.  An sexpr with this property is called _variable closed_ an
 d McKinna-Pollack observed that substitution\noperation is capture-avoidin
 g and hence safe on variable-closed sexps.\n\nHowever\, variable-closed se
 xprs cannot canonically represent\nlambda-terms since different sexprs can
  be alpha-equivalent\, e.g.\, \n   λx.x and λy.y.  This is the second re
 ason why\n$\\sexpr[\\atom]$ itself cannot serve as the set of lambda-terms
 .\n\nIn our previous work we solved the second difficulty above by\nintrod
 ucing a specific concrete subset of $\\sexpr[\\atom]$.  In this\ntalk we w
 ill generalize the work and give a general criteria which can\nbe used to 
 characterize subsets of $\\sexpr[\\atom]$ which canonically\n(that is no t
 wo distinct but alpha equivalent sexprs are in the\nsubset) represent lamb
 da-terms.\n\nThis is a joint work with Randy Pollack.\n
LOCATION:Room FW11\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR