[BINSU.REC]
[Post version of binary sum]
[To sum two binary numbers using Post's Productions, we set up
two addition tables for the terminal digits of the numbers.
One table is used initially, and when there is no carry present.
The other is used to incorporate a propagated carry into the
sum. Auxiliary symbols are naturally incorporated into the
sum by writing the Axiom in the form a+b=c. The digits to be
removed from a and b are identified by their proximity to + and
=, respectively. As the sum is developed, its digits are inserted
to the right of the = sign. The computation terminates when the
auxiliary symbols are dropped after at least one of them
reaches the front of its summand.]
[Post Productions can deal with the digits to be summed even
though they are widely separated. In a Markov Algorithm it is
necessary to move one of them until it is in contact with the
other before the addition table can be applied.]
[[]]
{
[cr, lf] (2573TL;)&
[read console] (R13%='';T08%(=2080[sp,bs]TL)(@J|;L@J;);)J
[logon message] ('
A Post Production scheme which will sum two binary
numbers written in the form a+b=c; for example
111110+011=
Each successive keystroke will display one more step
in the transformation until the sum is finished.
'TL@&'Initial Axiom:'TL@&@JI;:)R
[to shorten program] (UQzml;)U
[write workspace] (JZqt;)W
[to shorten program] (zZQml;)Z
[signoff message] (@&'Theorem:'TL@&JZqt;)X
(@R(@&@WRL
JZ''E'0+'@U1$S('0+'E'0='@U2$S('0='E@Z3$S(
JZD''I1$ryGI'+'I2$ryGI'=0'I3$ryGI''I;)nL;nL)nL;nL)nL:
JZ''E'0+'@U1$S('0+'E'1='@U2$S('1='E@Z3$S(
JZD''I1$ryGI'+'I2$ryGI'=1'I3$ryGI''I;)nL;nL)nL;nL)nL:
JZ''E'1+'@U1$S('1+'E'0='@U2$S('0='E@Z3$S(
JZD''I1$ryGI'+'I2$ryGI'=1'I3$ryGI''I;)nL;nL)nL;nL)nL:
JZ''E'1+'@U1$S('1+'E'1='@U2$S('1='E@Z3$S(
JZD''I1$ryGI'+'I2$ryGI'*0'I3$ryGI''I;)nL;nL)nL;nL)nL:
JZ''E'0+'@U1$S('0+'E'0*'@U2$S('0*'E@Z3$S(
JZD''I1$ryGI'+'I2$ryGI'=1'I3$ryGI''I;)nL;nL)nL;nL)nL:
JZ''E'0+'@U1$S('0+'E'1*'@U2$S('1*'E@Z3$S(
JZD''I1$ryGI'+'I2$ryGI'*0'I3$ryGI''I;)nL;nL)nL;nL)nL:
JZ''E'1+'@U1$S('1+'E'0*'@U2$S('0*'E@Z3$S(
JZD''I1$ryGI'+'I2$ryGI'*0'I3$ryGI''I;)nL;nL)nL;nL)nL:
JZ''E'1+'@U1$S('1+'E'1*'@U2$S('1*'E@Z3$S(
JZD''I1$ryGI'+'I2$ryGI'*1'I3$ryGI''I;)nL;nL)nL;nL)nL:
JZ''E'+'@U1$S('+'E'='@U2$S('='E@Z3$S(
JZD''I1$ryGI''I2$ryGI''I3$ryGI''I;)nL;nL)nL;nL)nL:
JZ''E'+'@U1$S('+'E'*'@U2$S('*'E@Z3$S(
JZD'0'I1$ryGI'+0'I2$ryGI'*'I3$ryGI''I;)nL;nL)nL;nL)nL:;)@X;)}
[end]