I’m going to assume that λ (p : τ) was meant to bind a variable other than
p so that it wouldn’t shadow the fix p; let’s go with λ (x : τ) instead.
Additionally, the dcl should obviously be inside the cmd(). Then reduction
of this term first substitutes the overall term into e and m; let’s assume
that it’s only mentioned in m, since e can’t really make much in the way of
interesting use of it. Call the overall term r for short. Then if we execute
the application of r to some value, say do r(v), we’ll step to
do cmd(dcl a := [v/x]e in [v/x][r/p]m). Say we eventually reach
do cmd(dcl a := e' in bnd(cmd(dcl a := e_2' in m_1); y.m_2)) with e_2' a
value; then we can begin to consider the actual content of the question. A step
from here will have to be given by a series of nested rules corresponding to
the constructs written above. In particular, there will be two nested instances
of the dcl rule (34.3j). In the conventions of the book, a comma means a
disjoint addition to a set, so in order for (34.3j) to apply to a dcl, the
symbol it binds must not appear in Σ. Therefore, in order to continue
evaluation, we are forced to consider an alpha-variant
do cmd(dcl a := e' in bnd(cmd(dcl b := e_2' in [b/a]m_1); y.m_2)) || μ_1 for
some fresh symbol b. This enforces the expected behavior that a dcl in a
recursive call will produce a new assignable.
I’ll skip to the generalization. We first need to give a passivity judgment
designed for the purpose of ensuring memory invariance: Since the passivity of
bnd(e; x.m) depends on the passivity of the result of evaluating e, dealing
with bnd properly requires defining a judgment on expressions stating that
their value is a passive command. The most reasonable approach seems to me to
be to introduce subtyping into the language, add a new type pcmd of passive
commands which is a subtype of cmd. We then set up the rules for passivity:
Γ |-_Σ m passive
--------------------
Γ |-_Σ cmd(m) : pcmd
Γ |-_Σ e : nat
---------------------
Γ |-_Σ ret(e) passive
Γ |-_Σ e : pcmd Γ, x : nat |-_Σ m passive
--------------------------------------------
Γ |-_Σ bnd(e; x.m) passive
Γ |-_Σ e : nat Γ |-_{Σ, a} m passive
---------------------------------------
Γ |-_Σ dcl(e; a.m) passive
--------------------------
Γ |-_{Σ, a} get[a] passive
Note that whenever m passive, also m ok, by induction on the derivation of
m passive (making use of the fact that pcmd is a subtype of cmd for the
bnd rule).
Now we can introduce this do construct:
Γ |-_Σ m passive
------------------
Γ |-_Σ do{m} : nat
Its dynamics, using the new states, is:
m || μ |->_Σ m' || μ'
-----------------------------
do{m} || μ |->_Σ do{m'} || μ'
e val_Σ
----------------------------
do{ret(e)} || μ |->_Σ e || μ
We have memory invariance for passive commands (if m || μ |->_Σ m' || μ' then
μ = μ') and for expressions, by mutual induction on typing and passive
judgments, and by inversion on evaluation-step judgments.
Such an own variable is essentially just a variable introduced outside of the body of the procedure, so that multiple calls to the procedure continue to reference the variable in the scope enclosing the procedure’s definition. We can implement this as follows:
proc p(x : τ) : ρ is {own a := e in m} in m' :=
dcl a := e in [fix p is proc(x : τ) m/p]m'
This explains the restriction that the thing the proc is being bound in must be a command—the translation must introduce a new variable, and so it cannot be an expression.
τ list := (rec l is [nil -> unit, cons -> τ × l]) ref
This is barely its own type—it’s just a reference to an immutable list.τ list := rec l is [nil -> unit, cons -> τ × l] ref
A mutable list is a reference to a “list step” (choice of nil or cons).τ list := rec l is [nil -> unit, cons -> (τ × l) ref]
A mutable list is either nil or a mutable cons cell. This is what Common
Lisp has. I’d also predict that this is pretty common in C because it is
equivalent to rec l is (τ × l) ref opt, and C pointers, being nullable,
correspond to RMA ref opts, so overall τ list corresponds to
typedef struct L *List;
struct L {
ty head;
List tail;
};
Note that (b), by contrast, would be rec l is (τ × l) opt ref—and C
pointers are ref opts, not opt refs.
τ list := rec l is [nil -> unit, cons -> τ × l ref]
This is pretty close to ©, apart from the fact that heads cannot be
modified in place.τ list := rec l is [nil -> unit, cons -> τ ref × l ref]
This looks like it’d be pretty close to © in terms of practical usage,
but the distinction seems kinda subtle, so I’m not 100% certain.τ list := rec l is [nil -> unit, cons -> τ ref × l ref] ref
I’m honestly not really sure what to make of this.It might be a good idea to mull this one over a bit more sometime. Shared mutable state is difficult.