Correspondence Between Axioms of Logic and Computer Programming Techniques - a Puzzle

[Charlie-Boo]

Ask someone how logic relates to computer programming, and there are a
number of possible reasonable responses you might hear:

1. The sets that are representable in logic [ wff w(x) represents { x
| w(x) is provable } ] are the sets that are accepted by some program
[ program w represents { x | w halts yes when input x } ].

2. The argument to an IF command in a program can be simplified by
applying rules of logic, e.g. DeMorgan’s lets us replace IF (~A)v(~B)
with IF ~(A^B).

3. More recent proofs of incompleteness in logic use a computer
program instead of a wff in the argument e.g. let program M be Foreach
Proof x If x proves M does not Halt then HALT. (This program relies
on the fact that the set of proofs is r.e. and whether x proves y is
recursive, which are in effect utilized in the proof.) M halts iff we
can prove that M does not halt, so (assuming our logic is sound) it is
true that M must not halt but we can’t prove it, which is one of
Godel’s theorems.

What other correspondences are there between logic and computer
programs?

Now consider the axiom of logic x+0=x (for all x.) Computer
programmers use this fact to simplify programs. The program SET X =
EXPR1 ; IF CONDITION SET X=X+Y initializes variable X to the value of
some expression and then, if some condition is true, adds Y to X.

The use of the IF command can be eliminated by utilizing the fact that
x+0=x. We (and I do mean we) concoct an expression EXPR2 such that if
CONDITION is true then EXPR2 evaluates to Y, and if CONDITION is false
then EXPR2 evaluates to 0. Then SET X=EXPR1+EXPR2 accomplishes the
same thing as the above program with an IF command (allowing us to use
only a “nonprocedural” expression EXPR1+EXP2 in place of x, rather
than using a “procedural” IF command) because x+0=x.

What technique of computer programming corresponds to the axiom x * 0
= 0 ?

C-B