zbMATH — the first resource for mathematics

Functional computation in a uniformly concurrent calculus with logical variables. (Funktionale Berechnung in einem uniform nebenläufigen Kalkül mit logischen Variablen.) (German) Zbl 0931.03050
Saarbrücken: Univ. des Saarlandes, Naturwissenschaftliche Fakultät, 145 S. (1994).
Summary: We present the \(\delta\)-calculus, a model of uniformly concurrent computation. It integrates eager and lazy functional computation and describes the intended complexity behavior in both cases.
We call concurrent computation uniformly concurrent, if result, termination and complexity are independent from the computation order. We establish theses properties for the \(\delta\)-calculus by proving its uniform confluence.
The \(\delta\)-calculus extends to models of concurrent computation providing for consumable resources and indeterminism. Such are the \(\gamma\)-calculus, a foundation of concurrent computation with constraints, and the \(\pi\)-calculus, a successor of CCS based on channel communication.
The \(\delta\)-calculus is a relational calculus with procedural abstraction and application. It provides for communication over logical variables and for suspension on their instantiation. Both mechanisms come naturally with parallel composition and declaration.
We embed the eager and the lazy \(\lambda\)-calculus into the \(\delta\)-calculus. Using explicit references we guarantee that functional arguments are evaluated at most once. Explicit references are a special form of logical variables. These are needed too for representing lazy functional control. We prove the adequacy of the embedding of the eager \(\lambda\)-calculus with respect to termination and complexity. We conjecture that the embedding of the lazy \(\lambda\)-calculus preserves termination and improves complexity.

03B70 Logic in computer science
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B40 Combinatory logic and lambda calculus
68N18 Functional programming and lambda calculus