## Equational Characterization of Binding (Extended Abstract)

**Sun, Yong**
*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.

*ECS-LFCS-89-94*

Previous |

Index |

Next