DYNAMIC BINDING AND LEXICAL BINDING IN A TRANSFORMATION CALCULUS (preliminary version)

JACQUES GARRIGUE Research Institute for Mathematical Sciences, Kyoto University, Kitashirakawa-Oiwakecho, Sakyo-ku, Kyoto 606-01.

                       E-mail: garrigue@kurims.kyoto-u.ac.jp

ABSTRACT

While dynamic and lexical binding for variables have both their uses in programming, no language gives an equal access to them. By encoding them simultaneously in an extension of the λ-calculus, we show that there is no contradiction between them, and give a better understanding of their respective roles. Moreover we give a simple type system for the encoding calculus, showing that not only lexical binding, but also dynamic binding, can be correctly typed without abusive restrictions.

1. Introduction

When local variables appear in a program, one may think of two strategies to define the binding of names to values. With dynamic binding, it is dynamically changed; that is, during the execution of the program, while the local variable exists, all uses of its name are interpreted as references to it, even in subroutines out of the syntactic scope of this local definition.

On the contrary, with lexical binding, only the syntactic structure of the program is considered. A variable name is interpreted according to the syntactically closest variable definition in the program, even if the execution has gone through other variable definitions before accessing this name.

It has long been observed that, if we think of a purely functional use of variables, in which variables can be assigned a value only once, lexical binding is to prefer, since it is the only one to preserve referential transparency. However, if we think of mutable variables, this argument disappears, since anyway the value stored in the variable may change over time. And there are cases where dynamic binding offers advantages, for instance when one wants to modify non-destructively the binding context.

The goal of this paper is, by defining a referentially transparent calculus, close to the lambda-calculus, in which we can encode the two binding strategies, to show how they differ but are not incompatible.

Moreover, by giving a simple type system for this calculus, we show that dynamic binding can be typed without restricting it more than lexical binding. The fact this type system ensures strong normalization is also interesting.

Section 3 presents our transformation calculus. In Section 4 it is shown how we can encode dynamic binding into it. Section 5 introduces local labels, and encodes lexical binding. Then Section 6 gives a type system for this last calculus, and Section 7 concludes. No proofs are given in this paper, but please refer to other reports ^{2,3} for more details.

2. Previous encodings

One could object that such calculi, close to the lambda-calculus, and in which we can encode mutable variables, already exist.

For instance, dynamic binding is easily encoded in the untyped lambda-calculus (with symbols or strings). We just have to add to each function an argument, the store, represented as a function from symbols to values, and recover it from the output. This can easily be extended to lexical binding by using some form of name binding, like in the λν-calculus ^{7}. However, there is a default to this encoding: our store will be always growing, since there is no way to discard a binding. As a result such an encoding does not provide a proper model for mutable variables.

To overcome this discarding problem, one may represent the store as a record. For this we need several operations: extension, to introduce a new variable; modification, to change the value of a variable; and restriction, to suppress a variable once it gets useless^{a}. This, combined with local labels, works well with lexical binding. However, dynamic binding becomes heavy: when creating a local variable one has to explicitly save the previous binding of the label, and to restore it afterwards, whereas intuitively the old binding is only hidden. Moreover, in both cases we have to manipulate explicitly the store, which means a low level of integration between the original calculus and mutable variables.

A slight simplification to these manipulations is obtained by translating programs (expressed as λ-terms) into a continuation passing style ^{10,5}. Since we do not come back from functions, there is no longer any need to get the store in return. The transformation itself is automatic, and we can chose it to use either call-by-value or call-by-name semantics. But this last possibility shifts the problem. In fact we do not need all the framework of CPS just to talk about binding strategies, and do not want to chose a priori between call-by-value and call-by-need for the whole calculus.

There also exist various systems dedicated to one of the binding strategies ^{1,8}. Comparison between these systems may be another way to tackle the problem, but we think that the framework of a unique calculus is instructive.

3. Transformation calculus

This is the calculus binding strategies will be encoded in. The definition is done in four steps. 1) We present a simplified version of the transformation calculus, without labels. 2) We define streams, a data structure on which we base our calculus. 3) We give a syntactic definition of terms in the transformation calculus, and add a structural equivalence on these terms. 4) Then we define reduction rules for these equivalence classes.

aThis last operation is often absent, being delegated to garbage collection. This makes things look simpler, but introduces some opaque part in the system.

3.1. Simple transformation calculus

The initial idea of the transformation calculus is to add to the lambda-calculus a capacity to pipe the output of one term into another. This is stronger than composition, because we want to be able to return not only values, but also sequences of values.

The calculus includes two new constructs:

M ::= x | λx.M | M.M | ↓ | M; M

First remark that, to simplify notations, we write application in a reversed way: in N.M, M is applied to N. As usual N_{1}.N_{2}.M is N_{1}.(N_{2}.M).

The two new constructs are used to introduce and destroy sequences of values, the only associated rule being (weak) ↓-elimination:

N_{1}. · · · .N_{n}.↓; M → N_{1}. · · · .N_{n}.M

To that, we of course add β-reduction:

N.λx.M → [N/x]M

With this simple transformation calculus, we can easily simulate a stack machine. For instance switching two elements at the top of the stack is written C = λx.λy.y.x.↓, and reduces as follows.

c.b.a.↓; C → c.b.a.λx.λy.x.y.↓ → c.a.b.↓

This is enough to encode imperative algorithms, but not named variables. That is why we introduce labeled streams.

3.2. Streams

The transformation calculus is essentially defined in terms of operations on streams. We give one definition for their set here, but transformation calculus can be defined on any “reversible” monoid: the monoid operation, or concatenation, gives us uncurrying, while its inverse, or extraction, gives us currying.

We will note the concatenation on streams by a simple dot “·”, and the monoid of streams is (S, ·).

l ::= pn  p ∈ L_{s}, n ∈ N
M ::= x  variable
| ↓  transformation constructor
| λ{l ⇒x, …}.M (stream) abstraction
| {l ⇒M, …}.M (stream) application
| M; M  composition

Figure 1: Syntax of the transformation calculus

Preliminaries • L_{s} is a set of names, N = IN \ {0}.

• L = L_{s} × N is the set of labels, lexicographically ordered.

• l will always represent an element of L; p, q elements of L_{s}; m, n elements of N.

Definition 1 (stream) The set S(L, A) of streams on a domain A is the set of finite partial functions from L to A.

S(L, A) = {s ∈ A^{L} | |s| ∈ IN}

• D_{s} is the definition domain of a stream s.

• {} is the function defined nowhere (D_{{}} = ∅).

• We note labels pn, and defining pairs {pn⇒a} with a ∈ A.

• The following equivalences of notation are admitted for labels and streams:

- n denotes ϵn, p denotes p1

- if l = pn then l + m = p(n + m)

- (a_{1}, …, a_{n}) = {1⇒a_{1}, …, n⇒a_{n}} For the details of operations on streams, see Appendix A.

3.3. Syntax

Notations. In the following definitions we will use the abbreviations A ∩̸ B for A∩B = ∅, F V (M) for the free variables of M, and V (R) for the values contained in the stream R. Definition 2 Terms of the transformation calculus, or Λ_{T}, are those generated by M in the grammar of figure 1, where variables should be distinct in abstractions, and labels distinct in streams. Composition has lower priority than dots.

They are considered modulo ≡, the minimal congruence defined by the closure of the equalities in figure 2.

S.R.M ≡_{.} (R · S).M
λR.λS.M ≡_{λ} λ(S · R).M  V (R) ∩̸ V (S)
R.λS.M ≡_{.λ} λψ_{R}(S).ψ_{S}(R).M F V (R) ∩̸ V (S), D_{R} ∩̸ D_{S}
(R.M_{1}); M_{2} ≡_{.;} R.(M_{1}; M_{2})
(λR.M_{1}); M_{2} ≡_{λ;} λR.(M_{1}; M_{2})  V (R) ∩̸ F V (M_{2})
(M_{1}; M_{2}); M_{3} ≡_{;} M_{1}; (M_{2}; M_{3})

Figure 2: Structural equivalences

Equalities ≡_{.} and ≡_{λ} are derived from the monoidal structure. ≡_{.;}, ≡_{λ;} and ≡_{;} are intuitive.

Equality ≡_{.λ} is the “symmetrical” of β-reduction. It comes from the need to close the equality ^{b}

(R′ ⊎ S′).λ(R ⊎ S).N ≡_{.} ψ_{R}(S′).R′.λS.λψ_{S}(R).N,

with D_{R′} = D_{R}, D_{S′} = D_{S} and V (S) ∩̸ V (R). If we take M = λψ_{S}(R).N, and apply R′.λS.M to ψ_{R}(S′), then ≡_{.λ} preserves confluence: it gives

(R′ ⊎ S′).λ(R ⊎ S).N ≡ ψ_{R}(S′).λψ_{R}(S).ψ_{S}(R′).λψ_{S}(R).N.

3.4. Reductions

Substitutions are done in the same way as for lambda-calculus, composition not interacting with variable binding. Terms will always be considered modulo αconversion. That is λ{l ⇒x}.M ≡ λ{l ⇒y}.[y/x]M when y ∉ F V (M). Definition 3 → is defined on transformation calculus terms by β-reduction and ↓- elimination^{c}.

\begin{aligned}\{l ⇒N\}.λ\{l ⇒x\}.M & →_{β} & [N/x].M \\ ↓; M & →_{↓} & M \end{aligned}

Theorem 1 The transformation calculus is confluent.

bψ is the reverse shifting function, such that R ⊎ S = R · ψ_{R}(S), where ⊎ is the union of disjoint partial functions.

cRemark that, thanks to the structural rules, the new ↓-elimination is stronger the first one we introduced (it even works when ↓ is prefixed by abstractions). We chose to make ↓-elimination a reduction rule rather than a structural equality because it reduces the size of terms, while the structural equalities of Definition 2 do not change it.

4. Encoding dynamically bound variables

We call this kind of variable scope free. By this we mean that the extent of their use is not determined by a syntactic scope, but simply by their presence as argument in a sequence of transformations.

A scope free variable is essentially a name v whose use in labels is exclusively reserved in the concerned sequence of transformations. This sequence is delimited by the creation of the variable with value a, encoded {v ⇒ a}.↓, and its destruction by an abstraction, λ{v ⇒ x}.↓. Between these, all transformations using or modifying this variable should once take it (through abstraction) and then put it back (by application), identical or modified. Typically a modification can be written λ{v ⇒ x}.{v ⇒M}.↓. That is, the sequence has form:

{v ⇒a}.↓; …; λ{v ⇒x}.{v ⇒M}.↓; …; λ{v ⇒x}.M

The fundamental property of scope free variables is that, like (lexically bound) scoped variables, they have no effect outside of the sequence they are used in. That is, we can use the same label v outside of the sequence our scope-free variable is local to, without interference. A scope free variable may even be used in a subsequence of another scope free variable using the same label:

\{v ⇒a\}.↓; …; \underline{\{v ⇒b\}.↓; …; λ\{v ⇒x\}.↓}; …; λ\{v ⇒x\}.↓

In the underlined subsequence the external scope-free variable is identifiable by the label v + 1 but comes back to v after.

Still, we must be careful that scope-free variables are not variables in the meaning of lambda-calculus: they appear on a completely different level, that of labels. Nor are they pervasive like would be references. We do not add side-effects to functions, but just provide some implicit way to manipulate a “stream” of arguments. That means that a function that is not called directly on this stream (through composition) will not access the scope-free variables it contains, and as such cannot have any imperative behavior with respect to this stream^{d}. This is this limitation which permits us to assimilate scope-free variables with arguments, and still be a conservative extension of lambda-calculus.

We give two examples of the use of scope free variables. The first one is a simple encoding of an imperative programming language à la Algol. The second one shows how dynamic scoping can be more accurate than a syntactic one.

dAs a result, mutable variables behave like in call-by-name. But this does not mean that we make any hypothesis on the evaluation strategy used for the transformation calculus. The calculus itself being confluent, any strategy will do.

Here is the first program and its translation:

        begin
          var x=5, y=10;
          x := x+y;
          begin
            var x=3;
            y := x+y
          end
          x := x-y;
          return(x)
        end

{x⇒5, y ⇒10}.↓; λ{x⇒x, y ⇒y}.{x⇒x + y, y ⇒y}.↓; {x⇒3}.↓; λ{x⇒x, y ⇒y}.{x⇒x, y ⇒x + y}.↓; λ{x⇒x}.↓; λ{x⇒x, y ⇒y}.{x⇒x − y, y ⇒y}.↓; λ{x⇒x, y ⇒y}.x

We expect this program to evaluate to 5 + 10 − (3 + 10) = 2. It goes through the following steps, and gives the expected result.

{x⇒5, y ⇒10}.↓; …

{x⇒5, y ⇒10} .λ · · · .{x⇒x + y, y ⇒y}.↓; …
{x⇒15, y ⇒10} .{x⇒3}.↓; …
{x1⇒3, x2⇒15, y ⇒10} .λ · · · .{x⇒x, y ⇒x + y}.↓; …
{x1⇒3, x2⇒15, y ⇒13} .λ{x⇒x}.↓; …
{x⇒15, y ⇒13} .λ · · · .{x⇒x − y, y ⇒y}.↓; …
{x⇒2, y ⇒13} .λ{x⇒x, y ⇒y}.x

2

Note here that since we encode dynamic binding, we would get the same result even if the central part was defined as a subprogram: with scope-free variable, even Basic’s subprograms would behave correctly, since we can create a scope free variable before the call to pass a parameter, and destroy it after.

The above example still respects a scoping discipline: variables are created and destroyed in opposite order. To show the specificity of scope free variables, we must disobey it.

Imagine a program with structure

\overline{A;}\underline{\overline{B}; C}

in which we want the console to be redirected in part A; B, and the screen to be changed in B; C. We suppose that we have mutable variables con and scr to indicate respectively which console and which screen should be used. Moreover we do not know which were the console and screen before entering A.

The scope free answer is:

\begin{matrix}\{con⇒newc\}.↓; A; \{scr ⇒news\}.↓; B; \\ λ\{con⇒c\}.↓; C; λ\{scr ⇒s\}.↓ \end{matrix}

We didn’t define any new variable, but did just temporarily hide the original value by the redirected one. With a syntactic scope, one of the two scopes (that of con or scr)

νp.M ≡ M  p ∉ FN (M)
νp.M ≡ νq.[q/p]M  q ∉ FN (M)
νp.νq.M ≡ νq.νp.M
λ{pm⇒x}.νq.M ≡ νq.λ{pm⇒x}.M p ≠ q
{pm⇒N}.νq.M ≡ νq.{pm⇒N}.M p ≠ q, q ∉ FN (N)
M; νp.N ≡ νp.(M; N)  p ∉ FN (M)
νp.M; N ≡ νp.(M; N)  p ∉ FN (N)

Figure 3: Structural equivalences for label scoping

would necessarily have included all A; B; C, whereas here they are both restricted to their area of concern.

5. Local labels, for lexical binding

To encode lexical binding, or scoped variables, we need the new concept of local label. Once we have it, a scope free variable defined on a local label becomes very naturally a scoped variable. Definition 4 Terms of the scoped transformation calculus are those of Λ_{T} extended with a label-scoping construct,

M ::= x | λ{l ⇒x, …}.M | {l ⇒M}.M | ↓ | M; M | νp.M

where p is a name in L_{s}.

FN (M), the set of free names in M, is defined in the usual way, νp.N hiding occurrences of p in N.

The structural equivalences of Figure 2 still hold, but we add to them those of Figure 3.

We have to extend variable substitution with

[N/x](νp.M) = νp.[N/x]M p ∉ FN (N)

but reduction rules themselves are not modified. Theorem 2 The scoped transformation calculus is Church-Rosser.

The key point in the new structural rules is that we don’t equate {pm⇒νq.N}.M and νq.{pm⇒N}.M. This would, in this form, make the calculus incoherent, scopes depending of the form on which we apply β-reduction —if the νq is out all residuates of N are in the same scope, otherwise they are in different ones—, and even if we restrict β reductions to terms containing no ν, this would lose the name generating power: once all ν are pushed out we can just forget about them for all internal reductions.

By keeping the ν in the applications, we create different scopes for each residual of N. This amounts to creating news names for each of them, and gives us lexical binding.

For instance, the equivalent of a reference cell can be defined as follows

cell = νr. \{ \begin{matrix}mk ⇒λ\{x\}.\{r ⇒x\}.↓ \\ get⇒λ\{r ⇒x\}.\{x, r ⇒x\}.↓ \\ set⇒λ\{x, r ⇒y\}.\{r ⇒x\}.↓ \\ del ⇒λ\{r ⇒x\}.↓ \end{matrix} \} .↓

When you want to use it you need to first unpack it (actually create the new name), then to compose the mk transformation, some transformations using the cell, and the del transformation. For instance,

\begin{matrix}cell; λ\{mk ⇒mk, get⇒get, del ⇒del\}. \\ (\{1\}.mk; \{r ⇒10\}.↓; get; λ\{x\}.\{x + 1\}.set; get; del) \end{matrix}

Here unpacking is done by composing the definition of the cell with a function that takes its transformations, and uses them locally.

This transformation evaluates to {2, r ⇒10}.↓, because of the scoping (otherwise it would have been {11, r ⇒1}).

Remark however that this does not mean that the transformation calculus suddenly changed from dynamic to lexical binding. That only means that they are different problems: scope free variables are about where a variable is available in a program, whereas name scopes are about how one can access it (or not).

6. Simple type system

To obtain a simply typed form of the scoped transformation calculus, we annotate variables with some type in abstractions, just the same way it is done in lambda calculus. But first we must define what are these types.

The two most important novelties are that, first, stream types are introduced, and second, that function type are not from any type to any other, but only from stream types to stream or base types. This last particularity “flattens” types, but still contains as a subset all simple types of lambda-calculus. Moreover we introduce name abstraction in types^{e}. Definition 5 (simple type) Simple types in the transformation calculus are generated by t in the grammar of Figure 4, with a structural congruence^{f}, and a (reflexive) subtyping relation defined modulo this congruence. Note that a stream type is a stream of types, as defined in Appendix A. This means that we can use stream composition on these types.

eWe note it equivalently νp⃗.t or νp_{1} … νp_{n}.t if p⃗ = (p_{1}, …, p_{n}).

fBecause of this congruence, the equality on types is not trivial, but we can test it by 1) taking a normal form, where all abstracted labels appear at least once in their scopes; 2) matching combinatorially the abstracted labels for every type.

Types

u ::= u_{1} | …  base types
r ::= {l ⇒t, …} stream types
w ::= u | r  return types
t ::= r → w | νp.t types

Congruence

νp.τ = τ p ∉ FN (τ)
νq.τ  = νp.[p/q]τ p ∉ FN (τ)
νp.νq.τ = νq.νp.τ

Subtyping

\frac{r′_{1} ≺ r_{1} r_{2} ≺ r′_{2}}{νp⃗.(r_{1} → r_{2}) ≺ νp⃗.(r′_{1} · r → r′_{2} · r)}

\frac{r′ ≺ r}{νp⃗.(r → u) ≺ νp⃗.(r′ → u)}

\frac{τ_{1} ≺ τ′_{1} … τ_{n} ≺ τ′_{n}}{\{l_{1} ⇒τ_{1}, …, l_{n} ⇒τ_{n}\} ≺ \{l_{1} ⇒τ′_{1}, …, l_{n} ⇒τ′_{n}\}}

Figure 4: Simple types

Definition 6 (simply typed term) A term in the simply typed scoped transformation calculus is constructed according to the following syntax.

\begin{aligned}M & ::= & x | ↓ | λ\{l ⇒x:t, …\}.M | \{l ⇒M, …\}.M | M; M | νp.M \\ & | & let \{l ⇒x, …\} = M in M \end{aligned}

with the same constraints on labels and variables as before. The new let construct is present here to permit the propagation of bound labels. In an untyped context, you can see it as let {l ⇒x, …} = Min N ≃ M; λ{l ⇒x, …}.N, and as such we add the rules

let P = νp.M in N ≡ νp.let P = M in N p ∉ FN (P.N)
let P = M in νp.N ≡ νp.let P = M in N p ∉ FN (P.M)
let {} = M in N  → M; N
let {l ⇒x} · P = Q.{l ⇒M}.↓ in N → let P = Q.↓ in [M/x]N

We must slightly modify scoping/abstraction structural equivalence to cope with the presence of (possibly scoped) types in abstractions.

λ{pm⇒x:τ}.νq.M ≡ νq.λ{pm⇒x:τ}.M p ≠ q, q ∉ FN (τ)

Definition 7 (type judgement) A type judgement, written Γ ⊢ M : τ, expresses that the term M has type τ in the context Γ. Induction rules for type judgements are given in figure 5.

Γ[x ↦ τ] ⊢ x : τ  (I)
\frac{Γ[x ↦ θ] ⊢ M : νp⃗.(r → w)}{Γ ⊢ λ\{l ⇒x:θ\}.M : νp⃗.(\{l ⇒θ\} · r → w)} p⃗ ∩̸ FN \{l ⇒θ\}  (II)
\frac{Γ ⊢ M : νp⃗.(\{l ⇒θ\} · r → w) Γ ⊢ N ≺ θ}{Γ ⊢ \{l ⇒N\}.M : νp⃗.(r → w)} p⃗ ∩̸ FN \{l ⇒θ\}  (III)
Γ ⊢ ↓ : {} → {}  (IV)
\frac{Γ ⊢ M ≺ νp⃗.(r_{1} → r_{2}) Γ ⊢ N ≺ νq⃗.(r_{2} → w)}{Γ ⊢ M; N : νp⃗.νq⃗.(r_{1} → w)}  (V)
where p⃗ ∩̸ FN (r_{2} → w), q⃗ ∩̸ FN (r_{1} → r_{2}), (r_{1} → w) minimal.
\frac{Γ ⊢ M : νp⃗.\{l_{i} ⇒θ_{i}\}_{1}^{n} · r_{1} Γ[x_{i} ↦ θ_{i}]_{1}^{n} ⊢ N ≺ νq⃗.(r_{1} · r_{2} → w)}{Γ ⊢ let \{l_{i} ⇒x_{i}\}_{1}^{n} = M in N : νp⃗.νq⃗.(r_{2} → w)}  (VI)
where p⃗ ∩̸ FN (N, Γ, l⃗_{i}), q⃗ ∩̸ FN (r_{1}), (r_{2} → w) minimal.
\frac{Γ ⊢ M : τ}{Γ ⊢ νp.M : νp.τ} p ∉ FN (Γ)  (VII)

Figure 5: Typing rules for simply typed scoped transformation calculus

Rules (I,II,III) are the traditional ones for typed lambda calculus, simply extended to streams and subtyping, and preserving the scoping of names. We can go back to it by limiting labels in streams to sequences of integers starting from 1 (that is, in the above rules, having only l = ϵ1), and suppressing abstractions on names.

Rule (IV) types the constant ↓. Note that any r → r is a subtype of {} → {}. Rule (V) types composition: N is applied to the result stream of M, and re-

abstracted by its abstraction part. The use of the subtyping rule permits to get a common r_{2} for M and N. The minimality constraint on r_{1} → w ensures the uniqueness of typing.

Rule (VI) types name propagation. It is needed, since we cannot make explicit the private labels of M in N’s type with the previous rule. Fresh names are first created for these, which are directly introduced in N’s environment. Again minimality ensures uniqueness.

Finally rule (VII) types name abstraction. Proposition 1 (subject reduction) Types decrease monotonously: if Γ ⊢ M : τ, and M → N or M ≡ N, then Γ ⊢ N ≺ τ. Proposition 2 (strong normalization) If Γ ⊢ M : τ in the simply typed scoped transformation calculus, then there is no infinite reduction sequence starting from M.

This last proposition lets us see that we didn’t introduce anything “impure” in the lambda-calculus. We can manipulate both dynamic and lexical variables, but this does not introduce any possibility of non-termination in the calculus, since they are independent from syntactic variables, and explicitly appear in types.

7. Conclusion

We presented here a calculus powerful enough to directly encode both dynamically and lexically bound (mutable) variables.

A first remark is that the encoding of scoped (lexically bound) variables is done in addition to the encoding of scope free (dynamically bound) variables. In our calculus the natural binding strategy is dynamic, and lexical binding is obtained by scoping the name of such a dynamic variable.

In some way this was to be expected, since the modeling of dynamic binding by stores has been known for long, but a satisfactory model of lexical binding cannot be obtained in a straightforward way ^{9,11,4,12,6}.

A second remark is that the notions behind these two binding strategy are orthogonal. Dynamic binding is about the presence of a variable in the environment, and lexical binding is about its accessibility through a name. One could argue that creating a dynamic variable potentially hides another variable with the same name as a side effect — and as such changes its accessibility —, but in the transformation calculus we can still use indexes to retrieve it.

This is an indication that these two aspects should be considered independently. Usually the first one is in fact left over to the garbage collector, but this works only for scoped variables: if a variable is scope free, the GC never knows whether we will still use it or not.

Last, by giving types to scope free variable in a way that does not unify types for all occurrences of the same name, but only when they represent the same variable, we may make possible a wider use of these variables, which are, in our theory, “lighter” —easier to model— than scoped ones.

Appendix A. Stream Monoid

The definition of stream concatenation is based on a notion of n^{th} free position in a stream, which, while intuitively clear —just imagine that undefined labels point to free positions—, looks a little complex once formalized. Definition 8 (free position) 1. The n^{th} position on p in a stream r is said to

be occupied if pn ∈ D_{r}. It is free otherwise, and F_{r} = L \ D_{r} is the set of these free positions.

2. The n^{th} free position for p in r is the n^{th} element of {i | pi ∈ F_{r}}. Namely ϕ_{r,p}(n) = min{m | |{pi ∈ F_{r} | i ≤ m}| = n}.

3. The relative index of pn in r is the number of free positions preceding n on p plus one. Namely ψ_{r,p}(n) = |{pi ∈ F_{r} | i < n}| + 1.

One notices immediately the inversion relation between free positions, used for concatenation, and relative indexes, used for extraction.

ϕ_{r,p}(n) = min{m | |{pi ∈ F_{r} | i ≤ n}| = n}
= max{m | |{pi ∈ F_{r} | i < n}| = n − 1}
= max ψ_{r,p}^{−1}(n)

We extend both ϕ and ψ to streams by ϕ_{r}({p_{i}n_{i} ⇒ a_{i}}_{i=1}^{k}) = {p_{i}ϕ_{r,p_{i}}(n_{i}) ⇒ a_{i}}_{i=1}^{k} (resp. for ψ). Example 1 (free positions) In {p1 ⇒ a, p3 ⇒ b, p5 ⇒ c, q2 ⇒ d}, relative indexes are respectively 2 for p4 and q3, and 3 for p5 and q4. Free positions are {2, 4, 6, 7, …} on p, and {1, 3, 4, …} on q. As a result, the second free position on p is 4, and on q this is 3. Proposition 3 (reversibility) ϕ_{r} is a bijection from S to {s ∈ S | D_{r} ∩ D_{s} = ∅}. ψ_{r} ∘ ϕ_{r} = id_{S}. Definition 9 (concatenation and extraction)

1. Stream concatenation is defined as r · s = r ⊎ ϕ_{r}(s) where “⊎” denotes union of (set represented) functions on disjoint domains.

2. Sub-stream extraction is defined as r ⊎ s = r · ψ_{r}(s), where r is the extracted sub-stream and ψ_{r}(s) is the rest after extraction.

Proposition 4 (monoid) Concatenation as in Definition 9 is an associative application S × S → S, accepting {} as neutral element.

The intuition behind these definitions is that when we do r · s we insert elements of s at free positions in r: for each name p we insert the element whose index is n in s at the n^{th} free position for p in r. ϕ_{r} is the function which does this shifting. Reciprocally, extraction uses ψ_{r} to shift back positions in the rest to their relative indexes w.r.t r. Example 2 (stream concatenation)

{2⇒a} · (b, c) · {p⇒d} · {q ⇒e} · {p⇒f}
= (b, a, c) · {p⇒d} · {p⇒f} · {q ⇒e}
= {ϵ1⇒b, ϵ2⇒a, ϵ3⇒c, p1⇒d, p2⇒f, q1⇒e}.
{p1⇒a, p3⇒b, r1⇒c} · {p1⇒d, q_{2} ⇒e}
= {p1⇒a, p3⇒b} · {p1⇒d} · {q2⇒e} · {r1⇒c}
= {p1⇒a, p2⇒d, p3⇒b, q2⇒e, r1⇒c}

References

1. M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 103:235–271, 1992.

2. J. Garrigue. The transformation calculus. Technical Report 94-09, University of Tokyo, Department of Information Science, Apr. 1994.

3. J. Garrigue. Label-Selective Lambda-Calculi and Transformation Calculi. PhD thesis, University of Tokyo, Department of Information Science, Mar. 1995.

4. J. Halpern, A. R. Meyer, and B. A. Trakhtenbrot. The semantics of local storage, or what makes the free-list free? In Proc. ACM Symposium on Principles of Programming Languages, pages 245–257, 1984.

5. J. Hatcliff and O. Danvy. A generic account of continuation-passing styles. In Proc. ACM Symposium on Principles of Programming Languages, pages 458–471, 1994.

6. A. R. Meyer and K. Sieber. Toward fully abstract semantics for local variables. In Proc. ACM Symposium on Principles of Programming Languages, pages 191–203, 1988.

7. M. Odersky. A functional theory of local names. In Proc. ACM Symposium on Principles of Programming Languages, pages 48–59, 1994.

8. M. Odersky, D. Rabin, and P. Hudak. Call by name, assignment, and the lambda calculus. In Proc. ACM Symposium on Principles of Programming Languages, pages 43–56, 1993.

9. F. Oles. Type algebras, functor categories, and block strcutures. In N. Nivat and J. Reynolds, editors, Algebraic Methods in Semantics, chapter 15, pages 543–573. Cambridge University Press, 1985.

10. G. D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1, 1975.

11. J. C. Reynolds. The essence of ALGOL. In de Bakker and van Vliet, editors, Proc. of the International Symposium on Algorithmic Languages, pages 345– 372. North Holland, 1981.

12. B. A. Trakhtenbrot, J. Y. Halpern, and A. R. Meyer. From denotational to operational and axiomatic semantics for ALGOL-like languages: An overview. In E. CLarke and D. Kozen, editors, Logic of Programs, pages 474–500, Berlin, 1984. LNCS 164, Springer-Verlag.