A Framework for Binding Operators

Sun Yong

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)

Previous | Index | Next