A Canonical Local Representation of Binding

Add 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 sexprs since $\sexpr[\atom]$ is a natural extension of Lisp symbolic expressions introduce by McCarthy. Choosing such a subset is a nontrivial task, since the subset of the algebra must not only be closed under substitution but also it must be closed under the operation of instantiation which instantiate a lambda abstract with an arbitrary lambda term.

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 variable closed and McKinna-Pollack observed that substitution operation is capture-avoiding and hence safe on variable-closed sexps.

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)
• Cambridge talks
• Computing and Mathematics
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• Logic and Semantics Seminar (Computer Laboratory)
• Room FW11, Computer Laboratory, William Gates Building
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.