next up previous
Next: Remarks Up: CORRECTNESS OF A COMPILER Previous: The compiler

Proof of Theorem 1.

The proof is accomplished by an induction on the expression e being compiled. We prove it first for constants, then for variables, and then for sums on the induction hypothesis that it is true for the summands. Thus there are three cases.

I.isconst(e). We have

displaymath168

II.isvar(e). We have

displaymath174

III.issum(e). In this case, we first write

displaymath179

displaymath187

displaymath455

using the relation between concatenating programs and composing the functions they represent. Now we introduce some notation. Let

displaymath195

so that tex2html_wrap_inline457 . Further let

displaymath203

so that tex2html_wrap_inline459 = outcome(compile( tex2html_wrap_inline461 , and we want to prove that

displaymath463

We have

displaymath213

and

displaymath219

Now

displaymath224

and

displaymath233

Next

tex2html_wrap_inline465

= tex2html_wrap_inline469

Here we again use the induction hypothesis that s2(e) is compiled correctly. In order to apply it, we need c(loc( tex2html_wrap_inline405 ,map), tex2html_wrap_inline477 for each variable tex2html_wrap_inline405 which is proved as follows:

displaymath237

Now we can continue with

displaymath256

Finally,

displaymath263

This concludes the proof.



John McCarthy
Wed Sep 29 13:40:01 PDT 1999