[TYPES] Idea about how to simulate variable assignment in lambda calculus

[Flavio Botelho]

I don't know if the idea might be useful for anything or maybe it's
not even new (i tried to look for it), but i would like to share it
anyways.

M,N  E  Terms  ::=   x | λx.M | M N | # M # | x := M

Reduction rules:

Beta:

(λx.M) N -> M[N/x]

Boundary Removal:

# M # -> M   (condition: If doesn't exist any variable assignment ':=' inside M)

Variable Assignment:

(λx1,x2,..,xn.# ... x:=M ... #) V1 V2 ... Vn -> (λx1,x2,..,xn. (λx.#
... I ... #) M) V1 V2 ... Vn

where  I = Identity = λx.x

x:=M becomes I and the variable x becomes binded at the boundary where
a redex is created with M as the applied term.

*** Important restriction, M should only have variables which are free
within the boundary and/or closed terms. More specifically, there
shouldn't exist a variable that is binded within the boundary (#...#).
As with this rewrite rule the variable would no longer be binded to
the right lambda (it would be either free or binded to another lambda
outside the boundary).

If the variable is reassigned, the boundary will insure that the last
assignment is the closest abstraction of that variable name within the
boundary.

Examples:

#(x:=2) (x:=1) x#  --VA--> (λx.# I (x:=1) x #) 2 --VA--> (λx.(λx.# I I
x #) 1) 2 --Boundary Removal--> (λx.(λx. I I x) 1) 2  --Betas--> 1
#(x:=2) (x:=1) x#  --VA--> (λx.# (x:=2) I x #) 1 --VA--> (λx.(λx.# I I
x #) 2) 1 --Boundary Removal--> (λx.(λx. I I x) 2) 1  --Betas--> 2


Factorial:

Pure lambda calculus:

Y (λ f n. IF (n==0) 1  (n*(f (n-1))))

With this variable assignment idea :

(λ n.# (x:=1) Y (λ f. IF (n==0) x ((x:=x*n) (n:=n-1) f) ) #)

Notice that you need that (x:=1) to be evaluated before the first x:=x*n.
And that (x:=x*n) be always evaluated before the (n:=n-1)
And to keep the VAs from being applied if your strategy is spuriously
creating new instances through Y.

---

Clearly Church-Rosser is lost as expected for such a imperative
feature. It simply adds the possibility of many different normal forms
for a given term.

A specific strategy is not necessary, but you need to ensure a
specific order for the evaluation of the assignments and the "reading"
of these mutable variables to ensure equivalent results. The only
trick part is when assignments are duplicated (or triplicated etc
etc), we need to modify the beta rule so we can properly reconstruct a
ordered lattice. Usually you want to follow whatever strategy you have
for Beta until you find a variable assignment that requires some other
to be executed before.

Actually if later on we can prove certain terms with VA to be
commutative (for example x:=x+2 and x:=x+3), then they also don't need
to be ordered one to the other.
ie.:

#(x:=x+2) (x:=x+3) x#  --VA--> (λx.# (x:=x+2) I x #) x+3 --VA-->
(λx.(λx.# I I x #) x+2) x+3 --Boundary Removal--> (λx.(λx. I I x) x+2)
x+3  --Betas--> x+2+3
#(x:=x+2) (x:=x+3) x#  --VA--> (λx.# I (x:=x+3) x #) x+2 --VA-->
(λx.(λx.# I I x #) x+3) x+2 --Boundary Removal--> (λx.(λx. I I x) x+3)
x+2  --Betas--> x+2+3

---

A possible extension of this is to have "local" boundaries, attaching
a list of variable names to a boundary such that those variables that
are not in that boundary go to a farther boundary, this can be used to
mimic programming language's local variable scope...

Kudos,
Flavio Botelho