Objects and their lambda calculus

AbstractA kind of parallel typed lambda calculus is presented based on the language and structure of objects. The term “object” is used here in a sense different from that related to the expression “object-oriented language (programming)”. By “objects” here we mean any class of entities which (a) are resource dependent and (b) combine to each other (via some fitness relation) to form more complex ones. Two operators, λ and its dual λ̄, are used, and two operations, a binary one, ⊙, for juxtaposition, and an n-ary one, |, for every n, for branching. The construct λv.x represents, roughly, a receiving scheme producing copies of x when fed with proper objects y to fill the empty place v of x, while the dual construct λ̄y.z represents a sending scheme that throws y out z in proper surroundings. The interaction of these two constructs takes place when they are matched together by ⊙ and yields an exchange of resources in a way that preserves the total amount of them. The calculus captures such notions as concurrency, interaction and branching in a way analogous to that of (Berrey and Boudol, Theoret. Comput. Sci. 96 (1992) 217–248; Boudol, Lecture Notes in Computer Science, Vol. 351, Springer, Berlin, pp. 149–161) [3,4], but with a quite different meaning of the operations. What is described here is “situations” of coexisting entities rather than computations, and resource-preserving transformations between them. The terms are shown to have unique normal forms. Object structures that model the simple theory of objects are extended here in suitable graph structures that provide sound and complete semantics of the calculus