Abstract: Binding appears in logic, programming and concurrency, e.g. it appears in lambda calculus [Church 41, Barendregt 84] say the lambda abstraction of lambda calculus. However, the binding in lambda calculus is unary. Certainly, we can generalize the idea of the unary binding to an arbitrary finite number of binding. Algebraically, we can consider an extension of the framework of universal algebra to accommodate the new feature of binding. Therefore, the new extended signature is of second- order instead of first-order. Like the well-known Church-Rosser property of lambda calculus leads to equational presentation of lambda calculus, we seek an equational characterizsation of binding in the new framework.
Peter Aczel has given a Church-Rosser theorem for bos-squared in [Aczel 78] and a definition for binding algebras in [Aczel 80], which is in Birkhoff's approach. Naturally, we would like to characterize binding in this Birkhoff's approach. Unfortunately, the semantics given in this way for binding equations does not work. Therefore, we have to find either a remedy for it or a new semantics model for binding. We will present a solution for each.
(a) For a remedy, we discover the admissible condition for the Birkhoff's approach to work. This condition is necessary and sufficient. A deduction system of admissible binding equations can be supplied. Some problems are remained open.
(b) For a new semantics model, we will give a new definition for binding algebras. The new binding algebras are intentional, since the previous definition is extensional. A sound and complete equational calculus for intentional binding algebras will be provided. Examples of its application can be given as well.
Due to space limit, this extended abstract mainly serves as an introduction to new concepts and results. Since every new framework has to defend itself in the beginning, this abstract can be regarded to serve this purpose and it defends in an intuitive (or informal) way.Previous | Index | Next