Unassignable-ABCDXYZ equivalency proof

Converting ABCDXYZ to :≠ is trivial. Below is a way to convert :≠ to ABCDXYZ.

For each object in a :≠ program, there are three things to do:

• Replace its declaration with one that declares just ABCD object(s).
• Replace its definition with definitions for each new ABCD object.
• Replace method calls on it with ones on the new ABCD object(s).

Once this is done, it is trivial to convert to ABCDXYZ... nearly.

:≠ allows initial values; ABCDXYZ sets everything to A. So we add an object named (say) unao_init, which sets every other object's initial value, then does main->call;; this becomes object number 0 in ABCDXYZ.

And io->output(c) is converted into "c.

Types

Each type will be dealt with separately:

• ABCD
• function
• integer
• unat_io -- made up name for io's type
• unat_bit -- new type to help convert integers (see below)

(Names starting with una are reserved for use of the implementation. Here, the prefix unat_ is used for new types and prefix unao_ for new objects.)

ABCD

Nothing to do.

unat_io

Cannot declare anything of this type.

function

Let f be a function object. Then:

Declarations

function f = activated;       ==>   ABCD unao_fun_f = B;
function f = deactivated;     ==>   ABCD unao_fun_f = C;

Definition

f { run { statements } }      ==>   unao_fun_f { event { statements } }

Method calls

f -> activate;                ==>   unao_fun_f -> Z;
f -> deactivate;              ==>   unao_fun_f -> Y;
f -> call;                    ==>   unao_fun_f -> X, Z;

(Note: obj -> m1, m2; is shorthand for obj -> m1; obj -> m2;.)

unat_bit

A unat_bit is a one-bit integer, with the following methods:

bit->toggle;      Toggle bit. 
bit->increment;   Toggle bit. If it becomes clear, run the carry event.
bit->decrement;   Toggle bit. If it becomes set, run the borrow event.
bit->loop;        Run the iterate event.
bit->loopifset;   If currently set, run the iterateifset event.

A unat_bit is implemented with 4 ABCD objects, named (poorly and unimaginatively) a, b, c, and d:

a handles the carry event. b handles the borrow event. c handles the iterate event. d handles the iterateifset event.

a, b and d's values are updated in tandem when the bit is toggled (c stays in state B).

Declarations

unat_bit bit = init;

becomes (A_or_C = A if init==set, C if init==clear):

ABCD unao_bita_bit = A_or_C;
ABCD unao_bitb_bit = A_or_C;
ABCD unao_bitc_bit = B;
ABCD unao_bitd_bit = A_or_C;

Definitions

bit {
   carry        { stmts_carry }
   borrow       { stmts_borrow }
   iterate      { stmts_iterate }
   iterateifset { stmts_iterateifset }
}

becomes

unao_bita_bit { event { stmts_carry   } }
unao_bitb_bit { event { stmts_borrow   } }
unao_bitc_bit { event { stmts_iterate   } }
unao_bitd_bit { event { stmts_iterateifset } }

Method calls

bit->toggle    ==> unao_bita_bit->X, Y; unao_bitb_bit->X, Y; unao_bitd_bit->X, Y;
bit->increment ==> unao_bita_bit->X, X; unao_bitb_bit->X, Y; unao_bitd_bit->X, Y;
bit->decrement ==> unao_bita_bit->X, Y; unao_bitb_bit->Y, Y; unao_bitd_bit->X, Y;
bit->loop      ==> unao_bitc_bit->X, Z;
bit->loopifset ==> unao_bitd_bit->X, X, X, Y;

integer

Let x be an integer object. First, it is converted into individual unat_bits, which can be converted into ABCDs as above.

Declaration

integer x(max) = init;

is converted to

unat_bit unao_i0_x = init0
unat_bit unao_i1_x = init1
unat_bit unao_i2_x = init2
unat_bit unao_i3_x = init3
...
unat_bit unao_i(n-1)_x = init(n-1)

(where n is number of bits in max, and init_k is kth bit of init.)

Definition

x {
   overflow  { stmts_overflow }
   underflow { stmts_underflow }
   iterate   { stmts_iterate }
}

is converted to

unao_i0_x {
   carry        { unao_i1_x->increment; }
   borrow       { unao_i1_x->decrement; }
   iterate      { stmts_iterate }
   iterateifset { stmts_iterate }
}
unao_i1_x {
   carry        { unao_i2_x->increment; }
   borrow       { unao_i2_x->decrement; }
   iterate      { unao_i0_x->loop, loop; }
   iterateifset { unao_i0_x->loop, loop; }
}

...

unao_ik_x {
   carry        { unao_i(k+1)_x->increment; }
   borrow       { unao_i(k+1)_x->decrement; }
   iterate      { unao_i(k-1)_x->loop, loop; }
   iterateifset { unao_i(k-1)_x->loop, loop; }
}

...

unao_i(n-2)_x {
   carry        { unao_i(n-1)_x->increment; } 
   borrow       { unao_i(n-1)_x->decrement; } 
   iterate      { unao_i(n-3)_x->loop, loop; } 
   iterateifset { unao_i(n-3)_x->loop, loop; } 
}
unao_i(n-1)_x {
   carry        { stmts_overflow }
   borrow       { stmts_underflow }
   iterate      { unao_i(n-2)_x->loop, loop; }
   iterateifset { unao_i(n-2)_x->loop, loop; }
}

Method calls

x -> increment(r);
x -> decrement(r);

become (where r = 2 ** k)

unao_ik_x -> increment;
unao_ik_x -> decrement;

and

x -> loop;

becomes

unao_i0_x -> loopifset;
unao_i1_x -> loopifset;
unao_i2_x -> loopifset;
...
unao_i(n-1)_x -> loopifset;

How does all this work?

When incrementing/decrementing x, it increments/decrements the bit required, and if there is a carry/borrow, the next highest bit is incremented/decremented. looping on x will loopifset on each of its bits. Each set bit k of x then performs x.iterate 2 ** k times, by looping the next-lower-order bit twice.

Example

Say x = 6 (dec) = 0110 (bin). So

x -> loop;

becomes

unao_i0_x -> loopifset;
unao_i1_x -> loopifset;
unao_i2_x -> loopifset;
unao_i3_x -> loopifset;

The 0th loopifset does nothing. The 1st loopifset runs x.iterate 2 times. The 2nd loopifset runs x.iterate 4 times. The 3rd loopifset does nothing.

In all, x.iterate is run 6 times.