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
Note that ex-directory lists are not shown. |
## Other listsMicrosoft Research Computational Science Seminars Developmental Biology Seminar Series Graduate Students at CUED (GSCUED) Events## Other talksBayesian Generative Adversarial Networks Foster Talk - Dr Rachel Tribe "How to expect the unexpected. Prediction and prevention of preterm birth" Proton Structure from the MMHT viewpoint THE PYE STORY Information Theory Deep Learning Boosted Object Reconstruction |