|
|
|---|
|
|
|
|---|
Functions and theorems about peeling frames and scopes.
We introduce functions to peel off any number of frames and scopes from a computation state, and we prove properties of these functions. These functions are not used in the definition of the dynamic semantics, but they are useful to express and prove inductive properties of the dynamic semantics. Since the execution functions of the dynamic semantics push/pop frames and enter/exit scopes, some desired properties of the execution functions need to be first proved in a more general way on computation states obtained by peeling frames and scopes, so that the properties are inductively sufficiently strong; then the desired properties, not involving peeling frames and scopes, follow as special cases of peeling no frames and no scopes.