8.1
18 Bisimulation
\(\newcommand{\la}{\lambda}
\newcommand{\Ga}{\Gamma}
\newcommand{\ra}{\rightarrow}
\newcommand{\Ra}{\Rightarrow}
\newcommand{\La}{\Leftarrow}
\newcommand{\tl}{\triangleleft}
\newcommand{\ir}[3]{\displaystyle\frac{#2}{#3}~{\textstyle #1}}\)
This chapter is not part of CS 747, and I have not provided a local version. The idea of bisimulation is important, though. It arises when considering new language features implemented entirely in terms of old ones, such as let using lambda from the More chapter. If one can show that every computational sequence in the new language has a corresponding sequence in the old language, one can lift theorems proved for the old language to the new language. More generally, compilers do a lot of internal transformations (for the purpose of optimization) between parsing and native code generation. One would generally like to know that these transformations preserve the semantics of programs, and bisimulation is one way of demonstrating this.