The Proof of Compiler Correctness

What we want to do is prove

Theorem: Let RUN be the restriction of RUN* to CMP. Then RUN is a homomorphism from CMP to SEM.
end

To accomplish this we will first prove the following result

Proposition: For any LANG1Syn-term t:

If tTLANG1Syn_<be>or tTLANG1Syn_<ae> , mStt, and h_SEM(t)(m) = <m, v> then

run[h_STP(t)](m, s, r, 1) = <m, v

s, r', |h_STP(t)|+1>

If tTLANG1Syn_<st> , mStt, and h_SEM(t)(m) = m' then

run[h_STP(t)](m, s, r, 1) = <m', s, r', |h_STP(t)|+1>

end

Definition: A StackM program is said to be well-formed if never fails to terminate because of a program error (i.e., because it has the wrong number or wrong type of elements on the stack for the next instruction to be performed).
A StackM program is said to be side-effect-free if it does not contain any put instructions.
A StackM program is said to be a straight-line program if it does not contain any branch instructions.
end

Fact: If tTLANG1Syn_<be>or tTLANG1Syn_<ae> then h_STP(t) is a well-formed, side-effect-free, straight-line program and thus all StackM programs in CMP_<be>and CMP_<ae>are well-formed, side-effect-free, straight-line programs.
Proof: Left to the reader.
end

Proposition: If p is a well-formed, side-effect-free, straight-line program then for each k< |p|, and each choice of mStt, sVal* and rVal, there exist s'Val* and r'Val such that run[p₁p_k](m,s,r,1) = <m, s's, r', k+1> and run[p](m,s,r,1) = run[p](m, s's, r', k+1).
Proof:
end

Proposition: Let be1, be2 CMP_<be>, with the property that, for b{be1, be2}, if h_CMP(t)= b then h_SEM(t) = RUN(b), then

RUN(true_CMP) = true_SEM
RUN(false_CMP) = false_SEM
RUN(not_CMP)(be1) = not_SEM (RUN(be1))
RUN(and_CMP)(be1, be2) = not_SEM (RUN(be1), RUN(be2))

Proof: We proceed as follows:
i.) By definition true_CMP = true where, for any m

Stt, s

Val* and r

Val, we have run[true](m, s, r, 1) = < m, true

s, r, 2> whence RUN( true_CMP)(m) = <m, true> = true_SEM(m). [ Note that "true" is overloaded in the preceeding sentence -- representing, in different contexts, a LANG1Syn-term, a StackM instruction, a StackM program, and a value from the set {true, false}.]

ii.) Essentially the same as above.

iii.) By definition, not_CMP(be1) = be1toRfrRfrRnand. By assumption, RUN(be1):SttStt{true, false}, and, for mStt, if RUN(be1)(m) = <m, v> then not_SEM(RUN(be1))(m) = <m, v>. But then

run[be1tRfrRfrRnand](m, s, r, 1)
= run[be1toRfrRfrRnand](m, vs, r', |be1|+1)
= run[be1toRfrRfrRnand](m, s, v, |be1|+2)
= run[be1toRfrRfrRnand](m, vs, v, |be1|+3)
= run[be1toRfrRfrRnand](m, vvs, v, |be1|+4)
= run[be1toRfrRfrRnand](m, nand(v, v)s, v, |be1|+5)
= run[be1toRfrRfrRnand](m, vs, v, |be1|+5)

So RUN(not_CMP(be1))(m) = <m,

v> = not_SEM(RUN(be))(m) as desired.

iv.) By definition, and_CMP(be1, be2) = be1be2nandtoRfrRfrRnand. By assumption, RUN(be1):SttStt{true, false}, and RUN(be2):SttStt{true, false}, and, for mStt, if RUN(be1)(m) = <m, v> and RUN(be2)(m) = <m, w> then and_SEM(RUN(be1), RUN(be2))(m) = <m, v&w>. But then

run[ be1be2nandtoRfrRfrRnand](m, s, r, 1)
= run[ be1be2nandtoRfrRfrRnand](m, vs, r, |be1|+1)
= run[ be1be2nandtoRfrRfrRnand](m, wvs, r, |be1|+|be2|+1)
= run[ be1be2nandtoRfrRfrRnand](m, nand(w, v)s, r, |be1|+|be2|+2)
= run[ be1be2nandtoRfrRfrRnand](m, (w&v)s, r, |be1|+|be2|+2)
= run[ be1be2nandtoRfrRfrRnand](m, s, (w&v), |be1|+|be2|+3)
= run[ be1be2nandtoRfrRfrRnand](m, (w&v) s, (w&v), |be1|+|be2|+4)
= run[ be1be2nandtoRfrRfrRnand](m, (w&v)(w&v) s, (w&v), |be1|+|be2|+5)
= run[ be1be2nandtoRfrRfrRnand](m, nand( (w&v), (w&v)) s, (w&v), |be1|+|be2|+6)
= run[ be1be2nandtoRfrRfrRnand](m, v&ws, (w&v), |be1|+|be2|+6)

So RUN(and_CMP(be1, be2))(m) = <m, v&w> = and_SEM(RUN(be1), RUN( be2))(m) as desired.
end