COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > A Canonical Local Representation of Binding

## A Canonical Local Representation of BindingAdd to your list(s) Download to your calendar using vCal - Masahiko Sato (Graduate School of Informatics, Kyoto University)
- Friday 18 September 2009, 14:00-15:00
- Room FW11, Computer Laboratory, William Gates Building.
If you have a question about this talk, please contact Matthew Parkinson. In this talk, we address the problem of concrete representation of lambda terms which can handle the subtle problem of defining substitution operation on lambda terms neatly. In defining lambda terms it has been more common to use only one sort of symbols for both global and local variables. However, historically, Frege and later Gentzen already used two sorts of symbols, and recently advantage of using two sorts of symbols has come to be recognized in computer science, and we take this approach here. Our definition of lambda terms is carried out in two steps. In the first step, we introduce a notion of B-algebras which captures the notion of variable binding as a binary algebraic operation on variables (represented by atoms) and elements of the algebra. In the second step, we use the free B-algebra $\sexpr[\atom]$ over a
fixed set of atoms and define lambda terms as a subset of
$\sexpr[\atom]$. Elements of $\sexpr[\atom]$ are called We remark here that we cannot use $\sexpr[\atom]$ itself as the set of lambda-terms for the following two reasons. The first reason is that local variables may appear unbound (or free)
in sexprs, although it is necessary that a local variable must always
appear within the scope of a binder which binds the variable. A
trivial example is a local variable, that is, an atom itself. This
problem can be fixed by choosing a subset of $\sexpr[\atom]$ with no
unbound local variables. An sexpr with this property is called However, variable-closed sexprs cannot canonically represent lambda-terms since different sexprs can be alpha-equivalent, e.g., λx.x and λy.y. This is the second reason why $\sexpr[\atom]$ itself cannot serve as the set of lambda-terms. In our previous work we solved the second difficulty above by introducing a specific concrete subset of $\sexpr[\atom]$. In this talk we will generalize the work and give a general criteria which can be used to characterize subsets of $\sexpr[\atom]$ which canonically (that is no two distinct but alpha equivalent sexprs are in the subset) represent lambda-terms. This is a joint work with Randy Pollack. This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. ## This talk is included in these lists:- All Talks (aka the CURE list)
- Computer Laboratory talks
- Computing and Mathematics
- Logic and Semantics Seminar (Computer Laboratory)
- Room FW11, Computer Laboratory, William Gates Building
- School of Technology
- Trust & Technology Initiative - interesting events
Note that ex-directory lists are not shown. |
## Other listsArts, Culture and Education BioLunch Seminar## Other talksThe homelands of the plague: Soviet disease ecology in Central Asia, 1920s–1950s Time Reversal Symmetries and the Simulation of Charge Transport in an External Magnetic Field Stopping the Biological Clock – The Lazarus factor and Pulling Life back from the Edge. Anthropological engineering and hominin dietary ecology Interrogating T cell signalling and effector function in hypoxic environments Assessing the Impact of Open IP in Emerging Technologies |