*Abstract:* Binding appears in logic, programming and
concurrency, e.g. it appears in Lambda Calculus, say the
lambda-abstraction. However, the binding in Lambda Calculus is
*unary*. Certainly, we can generalize the idea of unary
binding to an arbitrary-finite numbers of binding. Algebraically,
we can extend the framework of Universal Algebra [23,28,56] and
take arbitrary finite bindings as primitives. Therefore, operations
in the new extended signature must be of second order instead of
first order, and we name them as *Binding Operators*. The
resulting framework is named as a *Framework for Binding
Operators*, which coincides with Shapiro's diminished second
order language [138].

With a modification of Aczel's Frege Structure [4], we derive
the algebras for Binding Operators, i.e. *eBAs*. The usual
first order algebras, Plotkin's *Pw*-model of Lambda Calculus
, and Girard's qualitative domains [47] turn out to be special
cases of eBAs. And also eBAs turn out to be i a generalization of
Kechris and Moschovakis' *suitable class of functionals* in
Recursion in Higher Types [83] and (ii) a generalized Volken's
lambda- family [7, p.127]. Following Birkhoff [16], we would like
to equationally characterize Binding Operators. Kechris and
Moschovakis' Enumeration Theorem [83] suggests that an algebraic
characterization of such might be possible.

Unfortunately, eBAs and the usual satisfaction |=*eBA* of
*Binding Equations* over these eBAs, in Birkhoff's approach,
do not work. Therefore, we have to find either a *remedy* for
it or a new semantic model for Binding Operators. We will present
two solutions, one for each.

(a) For a remedy, we discover a condition for Birkhoff's
approach to work. This condition is necessary and sufficient, and
we call it an *admissible* condition, which turns out weaker
than Plotkin's *Logical Relations* [121] in the sense that
``logical'' implies ``admissible''. An admissible equational
calculus |-*eBA* for Binding Equations is obtained, which is
sound and complete with respect to admissible satisfaction
|=*eBA*. The relationship between Completeness and Admissible
Completeness (or between satisfaction |=*eBA* and admissible
satisfaction |=*eBA*) is discussed, although it is not
completely clear. Other problems remain open as well, say the
closedness of direct products and the admissible variety
problem.

(b) For a new semantic model, we will give a new binding
algebra, i.e. *iBA*, which is intensional in contrast to the
previous (extensional) one. Actually, an iBA is a generalization of
Friedman's Prestructures [46]. A sound and complete equational
calculus |-*iBA* (in iBAs) is established. However, the
derivability of |-*iBA* is weaker than the one of
|-*eBA*. In other words, to share a same proof power with
|-*eBA*, |-*iBA* has to use axiomatic schemas instead of
pure axioms. Also, the relations between extensional satisfaction
|-*eBA* and intensional satisfaction |-*iBA*, and between
admissible calculus |-*eBA* and calculus |-*iBA* are
discussed.

Examples of applications with present Framework for Binding
Operators and |-*iBA* are given. They are equationalizations
of (i) First Order Logic [140,139], (ii) Lambda Calculus and
Combinatory Logic [32,33,7]. and (iii) Milner's Calculus of
Communicating Systems [108,109] with data-dependency. These
demonstrate that the Framework for Binding Operators provides a
unified algebraic framework for all of logic, computation and
parallel computation.

**PhD Thesis - Price £10.00**

*LFCS report ECS-LFCS-92-207 (also published as
CST-91-92)*