A Catalogue of Small Process Translation Schemes

J.R.W. Glauert Technical Report SYS-C95-ZZ

UEA Norwich, UK

1 Introduction

This document is a catalogue of schemes developed by various people to translate the λ– Calculus with various extensions to small process notations such as the π–Calculus and our newer π^{π}–Calculus.

We aim to present the translations in their original formulation, but also use a standard process notation similar to the π–calculus of Milner, Parrow, and Walker.

A number of translations obey the restriction of Honda and Tokoro in which asynchronous communication models are derived by insisting that output actions are followed by inaction (tail communication).

In the translations below, the binary application operator combining λ-terms is made explicit and a subscript L, V, or S is added to indicate lazy, call-by-value, or sequential evaluation respectively. Hence the operators are @_{L}, @_{V}, and @_{S}.

The pure λ–calculus is not of great practical use. Constants, such as boolean and integer data values, and operations on them must be added to make a practical functional language. These constants must be modelled by process networks which behave correctly within the translation scheme. Since data values may appear as arguments, they must behave like abstractions.

Both call-by-value and sequential versions of binary operations are supported by some schemes. The examples are labelled Mult_{V} and Mult_{S}. Curried versions of the operations can be produced using suitable λ–expressions. For example, for the binary operation Mult_{V} we can make the curried version λx. λy. Mult_{V} (x, y).

For some translations, an expression will automatically yield the result on its interface channel. Other translations expect to receive a result channel before execution takes place. The result will then be returned on this channel. We describe briefly the characteristics of the translation.

We assume that a program yields a data value as result. For some schemes it is necessary to add some process structure to extract this value, using an agent P rint to display the final result. For this purpose, a rule for translating a whole program is given.

2 Translation Schemes

2.1 Milner’s Original Lazy π–Calculus Scheme

Name: OrigLazy

Origin: Lazy λ–Calculus translation from Milner’s Functions As Processes.

Syntax: Standard λ–calculus. No constants or operators.

Semantics: Standard lazy λ–calculus.

Operation: Abstraction expects argument then result channel. Variable identity communicated to result channel.

Implementation: Uses synchronous communication, so not implemented.

[[x]]_{u} = \overline{x} u
[[λx. M]]_{u} = u(x) · u(v) · [[M]]_{v}
[[@_{L} M N]]_{u} = (ν v) ([[M]]_{v} | (ν x) (\overline{v} x · \overline{v} u ·! x(w) · [[N]]_{w}))

2.2 Milner’s Original Strict π–Calculus Scheme

Name: OrigStrict Origin: Strict λ–Calculus translation from Milner’s Functions As Processes. Syntax: Standard λ–calculus. No constants or operators. Semantics: Standard sequential λ–calculus. Operation: Abstraction announces handle on which it receives argument then

result channel. Result channel identity communicated to variable channel. Implementation: Uses synchronous communication, so not implemented.

[[x]]_{u} = \overline{u} x
[[λx. M]]_{u} = (ν y) (\overline{u} y ·! y(w) · w(x) · w(q) · [[M]]_{q})
[[@_{V} M N]]_{u} = (ν a)(ν f) ([[M]]_{f} | f(y) · (ν v) (\overline{y} v · a(z) · \overline{v} z · \overline{v} u) | [[N]]_{a})

2.3 Our New Scheme

Our scheme supports a mixed calculus so there are rules for both forms of application. For comparison with other schemes, we need a pure translation. The translation NewLazy results when every application is treated as @_{L}, and NewStrict results if every application is treated as @_{V} New Scheme

[[x]]_{u} = ! u(v) · \overline{x} v
[[k]]_{u} = ! u(v) · \overline{v} k
[[λx. M]]_{u} = ! u(x, q) · [[M]]_{q}
[[@_{V} M N]]_{u} = (ν a)(ν f) ([[M]]_{f} | \overline{f} (a, u) | [[N]]_{a})
[[@_{L} M N]]_{u} = (ν t)(ν f) ([[M]]_{f} | \overline{f} (t, u) |! t(v) · (ν a) (\overline{a} v | [[N]]_{a}))
[[Succ(M)]]_{u} = (ν a)(ν x) ([[M]]_{a} | \overline{a} x | x(m) ·! u(v) · \overline{v} (m + 1)))
[[Mult_{V} (M, N)]]_{u} = (ν b)(ν a)(ν y)(ν x) ([[M]]_{a} | [[N]]_{b} | \overline{a} x | \overline{b} y | x(m) · y(n) ·! u(v) · \overline{v} (m ∗ n))

To translate a program, P, we use the rule:

[[P]] = (ν u)(ν c) ([[P]]_{u} | \overline{u} c | c(v) · P rint( v))

Technical Report SYS-C95-ZZ UEA Norwich, UK

The translations of a variable and of @_{L} M N are a simplification, v being shorthand for a pair, say (p, q). The translation scheme with the full forms is as follows:

[[x]]_{u} = ! u(p, q) · \overline{x} (p, q)
[[k]]_{u} = ! u(v) · \overline{v} k
[[λx. M]]_{u} = ! u(x, q) · [[M]]_{q}
[[@_{V} M N]]_{u} = (ν a)(ν f) ([[M]]_{f} | \overline{f} (a, u) | [[N]]_{a})
[[@_{L} M N]]_{u} = (ν t)(ν f) ([[M]]_{f} | \overline{f} (t, u) |! t(p, q) · (ν a) (\overline{a} (p, q) | [[N]]_{a}))
[[Succ(M)]]_{u} = (ν a)(ν x) ([[M]]_{a} | \overline{a} x | x(m) ·! u(v) · \overline{v} (m + 1)))
[[Mult_{V} (M, N)]]_{u} = (ν b)(ν a)(ν y)(ν x) ([[M]]_{a} | [[N]]_{b} | \overline{a} x | \overline{b} y | x(m) · y(n) ·! u(v) · \overline{v} (m ∗ n))

2.4 Asynchronous π–Calculus Schemes

The original translations do not comply with the asynchronous form of Honda and Tokoro. We can, however, use their techniques to convert the translations to asynchronous form. The first will be called PiLazy and the second PiStrict:

PiLazy

[[x]]_{u} = \overline{x} u
[[k]]_{u} = u(v) · \overline{v} k
[[λx. M]]_{u} = u(d) · (ν a) (\overline{d} a | a(x) · u(v) · [[M]]_{v})
[[@_{L} M N]]_{u} = (ν v)(ν d) ([[M]]_{v} | \overline{v} d | d(a) · (ν t) (\overline{a} t | \overline{v} u |! t(w) · [[N]]_{w}))
[[Succ(M)]]_{u} = (ν a)(ν s) ([[M]]_{a} | \overline{a} s | s(m) · u(v) · \overline{v} (m + 1))
[[Mult_{V} (M, N)]]_{u} = (ν b)(ν a)(ν y)(ν x) ([[M]]_{a} | [[N]]_{b} | \overline{a} x | \overline{b} y | x(m) · y(n) · u(v) · \overline{v} (m ∗ n))

To translate a program, P, we use the rule:

[[P]] = (ν u)(ν c) ([[P]]_{u} | \overline{u} c | c(v) · P rint( v))

PiStrict

[[x]]_{u} = \overline{u} x
[[k]]_{u} = \overline{u} k
[[λx. M]]_{u} = (ν y) (\overline{u} y |! y(w) · w(t) · (ν d) (\overline{t} d | d(x) · w(q) · [[M]]_{q}))
[[@_{V} M N]]_{u} = (ν a)(ν f) (([[M]]_{f} | f(y) · (ν v) (\overline{y} v | a(z) · (ν t) (\overline{v} t | t(d) · (\overline{d} z | \overline{v} u))) | [[N]]_{a})
[[Succ(M)]]_{u} = (ν a) ([[M]]_{a} | a(m) · \overline{u} (m + 1))
[[Mult_{V} (M, N)]]_{u} = (ν b)(ν a) ([[M]]_{a} | [[N]]_{b} | a(m) · b(n) · \overline{u} (m ∗ n))

To translate a program, P, we use the rule:

[[P]] = (ν u) ([[P]]_{u} | u(v) · P rint( v))

For both of these translations the handling of constants and operators is simple, but abstractions and applications require many communications.

2.5 Tupled π–Calculus Schemes

The tupled communication of our notation can be exploited to produce optimised versions of PiLazy and PiStrict, called NewPiLazy and NewPiStrict respectively:

NewPiLazy

[[x]]_{u} = \overline{x} u
[[k]]_{u} = u(v) · \overline{v} k
[[λx. M]]_{u} = u(x, v) · [[M]]_{v}
[[@_{L} M N]]_{u} = (ν v)(ν t) ([[M]]_{v} | \overline{v} (t, u) |! t(w) · [[N]]_{w})
[[Succ(M)]]_{u} = (ν a)(ν s) ([[M]]_{a} | \overline{a} s | s(m) · u(v) · \overline{v} (m + 1))
[[Mult_{V} (M, N)]]_{u} = (ν b)(ν a)(ν y)(ν x) ([[M]]_{a} | [[N]]_{b} | \overline{a} x | \overline{b} y | x(m) · y(n) · u(v) · \overline{v} (m ∗ n))

To translate a program, P, we use the rule:

[[P]] = (ν u)(ν c) ([[P]]_{u} | \overline{u} c | c(v) · P rint(v))

NewPiStrict

[[x]]_{u} = \overline{u} x
[[k]]_{u} = \overline{u} k
[[λx. M]]_{u} = (ν y) (\overline{u} y |! y(w) · w(x, q) · [[M]]_{q})
[[@_{V} M N]]_{u} = (ν a)(ν f) ([[M]]_{f} | f(y) · (ν v) (\overline{y} v | a(z) · \overline{v} (z, u)) | [[N]]_{a})
[[Succ(M)]]_{u} = (ν a) ([[M]]_{a} | a(m) · \overline{u} (m + 1))
[[Mult_{V} (M, N)]]_{u} = (ν b)(ν a) ([[M]]_{a} | [[N]]_{b} | a(m) · b(n) · \overline{u} (m ∗ n))

To translate a program, P, we use the rule:

[[P]] = (ν u) ([[P]]_{u} | u(v) · P rint(v))

2.6 Improved π–Calculus Schemes

The NewPiStrict scheme can be further simplified: the protocol between an abstraction and an application creates a special link simply to exchange a pair of values, whereas it is possible just to communicate the pair directly. The resulting scheme is the best purely strict scheme investigated so far.

ImpPiStrict

[[x]]_{u} = \overline{u} x
[[k]]_{u} = \overline{u} k
[[λx. M]]_{u} = (ν y) (\overline{u} y |! y(x, q) · [[M]]_{q})
[[@_{V} M N]]_{u} = (ν a)(ν f) ([[M]]_{f} | f(y) · a(z) · \overline{y} (z, u) | [[N]]_{a})
[[Succ(M)]]_{u} = (ν a) ([[M]]_{a} | a(m) · \overline{u} (m + 1))
[[Mult_{V} (M, N)]]_{u} = (ν b)(ν a) ([[M]]_{a} | [[N]]_{b} | a(m) · b(n) · \overline{u} (m ∗ n))

To translate a program, P, we use the rule:

[[P]] = (ν u) ([[P]]_{u} | u(v) · P rint(v))

We are also interested in sequential schemes where the function is to be evaluated before the argument, so that side effects will be deterministic. This can be achieved by making simple changes to the rules for ImpPiStrict so that there are input guards before the translation of expressions which are to be delayed.

We use a new apply operator with subscript S. The rules for binary operators also enforce sequential operation. The operator is given a subscript as well:

SeqPiStrict

[[x]]_{u} = \overline{u} x
[[k]]_{u} = \overline{u} k
[[λx. M]]_{u} = (ν y) (\overline{u} y |! y(x, q) · [[M]]_{q})
[[@_{S} M N]]_{u} = (ν f) ([[M]]_{f} | f(y) · (ν a) (a(z) · \overline{y} (z, u) | [[N]]_{a}))
[[Succ(M)]]_{u} = (ν a) ([[M]]_{a} | a(m) · \overline{u} (m + 1))
[[Mult_{S}(M, N)]]_{u} = (ν a) ([[M]]_{a} | a(m) · (ν b) ([[N]]_{b} | b(n) · \overline{u} (m ∗ n)))

To translate a program, P, we use the rule:

[[P]] = (ν u) ([[P]]_{u} | u(v) · P rint(v))

These last schemes are entirely compatible with each other. The same number of communications will take place if a program terminates, although the sequential apply operator will delay execution of the argument.

We show a combined scheme called MixPiStrict:

MixPiStrict

[[x]]_{u} = \overline{u} x
[[k]]_{u} = \overline{u} k
[[λx. M]]_{u} = (ν y) (\overline{u} y |! y(x, q) · [[M]]_{q})
[[@_{V} M N]]_{u} = (ν f)(ν a) ([[M]]_{f} | f(y) · a(z) · \overline{y} (z, u) | [[N]]_{a})
[[@_{S} M N]]_{u} = (ν f) ([[M]]_{f} | f(y) · (ν a) (a(z) · \overline{y} (z, u) | [[N]]_{a}))
[[Succ(M)]]_{u} = (ν a) ([[M]]_{a} | a(m) · \overline{u} (m + 1))
[[Mult_{V} (M, N)]]_{u} = (ν a)(ν b) ([[M]]_{a} | [[N]]_{b} | a(m) · b(n) · \overline{u} (m ∗ n))
[[Mult_{S}(M, N)]]_{u} = (ν a) ([[M]]_{a} | a(m) · (ν b) ([[N]]_{b} | b(n) · \overline{u} (m ∗ n)))

To translate a program, P, we use the rule:

[[P]] = (ν u) ([[P]]_{u} | u(v) · P rint(v))