# Translation Correctness for Expressions

## Notation

Functions:

• evaluation:
• compilation:
• virtual machine:

For simplicity we will omit environments mapping variables

• does not affect this proof

We often write X instead of List(X) when X is one element

Also, we often use same symbol '*' for

• operator in the tree
• operator in instruction sequence
• corresponding mathematical operator

## Key Facts

Evaluation of expressions:

Translation:

Here

• the last occurrence of is the imul instruction
• denotes a tree with node type and children ,

run-virtual machine: From definition of and by induction on ,

Of course

where is the result of computing , and

for constant , and

For every ,

## Attempt at Inductive Proof

Induction on structure of

## Induction Hypothesis

For every expression and every list of integers ,