Variables and Equivalence

Assignment poses the new problem of deciding whether two expressions are "the same":

When one excludes assignments and one writes:

val x = E
val y = E
// There is no assignment/variables here, so we can also write:
val x = E
val y = x

(This property is usually called referential transparency)

But once we allow the assignment, the two formulations are different. For example:

val x = new BankAccount // BankAccount is a state object
val y = new BankAccount

Here x and y are not the same, even though the expression is the same. This is better understood by the property of Operational Equivalence.

Operational Equivalence

x and y are operationally equivalent if no possible test can distinguish between them.

Operational Equivalence Test

So to test if x and y are the same, we must

• Execute the definitions followed by an arbitrary sequence of operations that involves x and y, observing the possible outcomes:

  f(x, y)

• Then, execute the definitions with another sequence obtained by renaming all occurrences of y by x

  f(x, x)

• If the results are different, then the expressions x and y are certainly different.

Example

1. Lets define a sequence as below:

   x.deposit(30)  // val res1: Int = 30
   y.withdraw(20) // java.lang.Error: insufficient funds

2. Rename all occurrences of y with x in this sequence

   x.deposit(30)  // val res1: Int = 30
   x.withdraw(20) // val res2: Int = 10

3. Results are difference, hence x and y are not same.

Establishing Operational Equivalence

If we define

val x = new BankAccount
val y = x

then no sequence of operations can distinguish between x and y, so x and y are the same in this case.

Assignment and The Substitution Model

The** substitution model ceases to be valid when we add the assignment i.e var**.

Eg. Consider the state object BankAccount:

val x = new BankAccount; val y = x
-> val x = new BankAccount; val y = new BankAccount

Here we see that we substituted in the first line to get second line, but as seen above, both the lines are different i.e. line 1 x and y are equal, line 2 they are not. So the substitution model does not hold and cannot be used since we are dealing with state object here.

It is possible to adapt the substitution model by introducing a store, but this becomes considerably more complicated.