Our starting point is theλv-S(t)-calculus defined by Felleisen and Hieb [33].
6.2.1 The term language
The term language is a direct extension of the term language for theλv-calculus from Sec-tion 3.3 (We omit the definiSec-tion of basic constants ranged over byb):
Val v ::= b|x|λx.t|λxσ.t|σxσ.t Termσ t ::= v|t t|xσ
Herex∈ Var andxσ∈Varσ. Var is the set of variables of theλ-calculus, and Varσis the set of state variables. These two sets are disjoint but otherwise unspecified.
The term language extends theλv-calculus language by two constructs: (1) The new set of state variables Varσwhich are not values because they do not represent a single value, and (2) theσ-capabilityσxσ.twhich represents the capability to globally assign the state variable xσa value when applied, i.e. an assignment construct which itself is a value.
6.2.2 Conventions
In relation to the presentation of theλv-calculus Felleisen and Hieb mention two conven-tions:
1. Bound variables are always distinct from free variables in the various expressions of mathematical definitions and claims.
2. Abstractions that only differ by a renaming of bound variables are identified, e.g., λx.x≡λy.y.
These two conventions are taken verbatim from Felleisen and Hieb’s text. The first con-vention gives that theβ-rule can be used without the side condition that variable renaming might be needed because substitution must be capture-free. The second convention is the usual convention also used in this text making the above mentioned renaming possible:
Textual terms are representatives of the real terms, which are the classes defined by=α. 6.2.3 Theρ-application
Aρ-applicationρθ.tis a useful abbreviation. It is composed of a termtand a finite function θ = {(x1, v1), . . . ,(xn, vn)}, xi ∈ Varσrepresenting a part of the state. The abbreviation is defined via two expansion rules:
ρ{}.t ≡ t
ρ{(x1, v1), . . . ,(xj, vj)}.t ≡ (λx1. . . . λxj.(σx1.. . . σxj.t)v1 . . . vj) (λx.x). . .(λx.x) Becauseθis a finite function thexiare all different.
6.2.4 Notions of reduction
Reduction in the calculus is defined via seven contraction rules. Three of these rules rely on applicative-order reduction contexts over the revised term language:
E ::= [ ]|E t|v E
δ: q l → capp(q, l)
βv: (λx.t)v → t{v/x}
βσ: (λxσ.t)v → ρ{(xσ, v)}.t D: ρθ∪{(xσ, v)}.E[xσ] → ρθ∪{(xσ, v)}.E[v]
σ: ρθ∪{(xσ, v0)}.E[(σxσ.t)v] → ρθ∪{(xσ, v)}.E[t]
gc: ρθ∪θ0.t → ρθ0.t,ifθ6={}and Dom(θ)∩FVσ(ρθ0.t) ={}
ρ∪: ρθ0.E[ρθ.t] → ρθ∪θ0.E[t],ifθ6={}andρθ0.E6= [ ]
The notion of reduction t is defined as the union of the above seven contraction rules:
t := δ∪βv∪βσ∪D∪σ∪gc∪ρ∪
The rulesδandβvare standard from theλv-calculus of Section 3.3 (with substitution straight-forwardly extended toσ-capabilities).
A new state variable is introduced in ruleβσby extending the overall state by a new part.
According to the second expansion rule forρ-applications the contractum of aβσ-redex is (λxσ.(σxσ.t)v) (λx.x). That is, the introduction of state variables is capture-free according to the first convention in Section 6.2.2: xσ ∈/ FVσ(v), where FVσis assumed to be the straight-forward variation ofFV, the function mapping a term to its free variables — here mapping to its free state variables. FVσalso appears in the rule gc. Rules D andσare the lookup and update of a state variable, respectively wrt. the inner-most part of the state.
Remark that inρθ∪θ0.t,θ∪θ0denote a finite function. In the rules gc and ρ∪ the con-dition about the finite function not being the empty function (θ 6= {}) is not essential. We assume these conditions are included to let the last four rules be strongly normalizing, i.e., us-ing only these four rules normalization cannot possibly diverge. But in case that property is the reason for the conditions, one more condition is needed in the garbage-collection rule gc which removes an unneeded part of the state:θ∪θ0must imply a partitioning of the domain, i.e., Dom(θ)∩Dom(θ0) ={}. (This condition is not mentioned by Felleisen and Hieb.)
In ruleρ∪the second condition relies on the expansion of theρ-abbreviation and is equiv-alent to (θ0 6= {}orE6= [ ]). Henceρ∪ either ‘lifts’ a part of the state towards the root of the term (whenE6= [ ]) orρ∪merges two nontrivial parts of the state into one (whenE= [ ]).
6.2.5 One-step reduction and equality
Contexts for the term language is mentioned to be modified appropriately given contexts for terms in theλv-calculus. The definition of contexts must hence have productions according to the new constructs:
C ::= [ ]|C t|t C|λx.C|λxσ.C|σxσ.C
Felleisen and Hieb do not explicitly define one-step t-reduction→t or t-reduction→∗t, but following the rest of the paper (and the usual approach also followed in this text) definitions
are straightforward: One-step t-reduction is defined as the compatible closure of t according to the above grammar of contexts:
t→tt0 iff t=C[r], t0=C[r0],(r, r0)∈t
t-reduction →∗t is the reflexive transitive closure of →t. Equality in the calculus =t is the equivalence relation over t-reduction.
6.2.6 The Church-Rosser property
The standard property Church-Rosser of t is proved by Felleisen and Hieb. In other words,
→∗t has the usual diamond property like→∗βon page 10.
A condition is missing in connection with liftings ofρ-applications towards the root in the ruleρ∪. The following are two reduction sequences starting with the same term (where vandv0are different closed values in normal form).
((λxσ.λy.xσ)v) ((λxσ.λy.y)v0) →2t (ρ{(xσ, v)}.λy.xσ) (ρ{(xσ, v0)}.λy.y)
→t (ρ{(xσ, v)}.λy.xσ)λy.y
→t ρ{(xσ, v)}.((λy.xσ)λy.y)
→t ρ{(xσ, v)}.xσ
→t ρ{(xσ, v)}.v
→t v
((λxσ.λy.xσ)v) ((λxσ.λy.y)v0) →2t (ρ{(xσ, v)}.λy.xσ) (ρ{(xσ, v0)}.λy.y)
→t ρ{(xσ, v)}.((λy.xσ) (ρ{(xσ, v0)}.λy.y))
≡ ρ{(xσ, v)}.ρ{}.((λy.xσ) (ρ{(xσ, v0)}.λy.y))
→t ρ{(xσ, v)}.ρ{(xσ, v0)}.((λy.xσ)λy.y)
→t ρ{(xσ, v)}.ρ{(xσ, v0)}.xσ
→t ρ{(xσ, v)}.ρ{(xσ, v0)}.v0
→2t v0
The sample term has been reduced to two different normal forms. Hence they do not have a common reduct. In other words, the Church-Rosser property does not hold unless we add a condition to the ruleρ∪: FVE(E)∩Dom(θ) = {}, whereFVE maps evaluation contexts to its free state variables.3 The condition ensures that liftings of ρ-applications inρ∪ are capture-free. Usually programs are closed terms. When utilizing evaluation contexts in definitions of a one-step reduction function for a language such evaluation contexts hence cannot have free variables. In the contraction rules D,σand gc evaluation contexts in contrast are used in a non-standard way: in the context of store-parts. Here it is possible for evaluation contexts to have free variables.
6.2.7 Standard reduction
Felleisen and Hieb define a standard reduction relation via t-standard evaluation contexts:
E ::= E|ρθ.E
How to understand this grammar of contexts is not clear. We assume the definition in-corporates the applicative-order evaluation contexts also used in the contraction rules in
3The added condition is not implied byθ∪θ0which denotes a function: In generalFVE(E)*θ0.
Section 6.2.4, such that the intended grammar reads as follows:
Et ::= [ ]|Ett|v Et |ρθ.Et
such that t-standard reduction is defined as the compatible closure of t according to the grammar of t-standard evaluation contexts:
Et[r]7→t Et[r0] iff (r, r0)∈t
Remark: the above definition of evaluation contexts together with the notion of reduction does not imply unique decomposition of a non-value term (where7→tis defined) into a con-text and a t-redex. In other words,7→tdoes not define a function. According to Section 4.5.3, we only have a reduction semantics if7→tis a function. In general the rule gc can obviously be applied in various contexts, but removing gc is not enough to obtain a function.