Renaming-variables-execution
Proof that variable renaming preserves the execution behavior.
We start by extending the variable renaming relation
from the abstract syntax to the dynamic semantic entities,
namely function environments and computation states
(and their constituents).
For these, we define the relation as a predicate,
instead of a function that may return errors,
as we never need to return anything if the relation holds
(while, for certain abstract syntax entities,
we need to return additional information, e.g. the extended renaming.
Then we prove theorems relating variable renamings
to the various dynamic semantic operations.
Examples of these operations are writing variables,
finding functions in environments, and so on.
Next, we show some properties of computation states and variable renamings,
which do not involve dynamic semantic operations.
Then we prove theorems saying
that executing a list of statements yields a computation state
with a superset of the starting variables,
and that executing loop iterations yields a computation state
with the same variables as the starting state.
These theorems are independent from variable renaming,
and could be moved to a more central place,
possibly complemented by similar properties
for executing other kinds of abstract syntax entities.
Then we prove some theorems about limit errors.
In particular, we prove that
several dynamic semantic operations never return limit errors.
These theorems are actually independent from variable renaming,
and could be moved to a more central place.
Before proving the main theorems,
we prove two preliminary ones having to do with
the use of restrict-vars in execution,
when dealing with parallel executions related by variable renaming.
Finally we prove theorems
about the execution functions and variable renaming.
We do that by induction, using a custom induction schema.
Subtopics
- Restrict-vars-when-renamevar
- Theorems about restricting variables and variable renaming.
- Function-environments-when-renaming-variables
- Theorems about function environments and variable renaming.
- Exec-when-renamevar
- Main theorems of the proof that
variable renaming preserves the execution behavior.
- Exec-when-renamevar-restrict-vars-lemmas
- Theorems about restricting variables
in parallel executions related by variable renaming.
- Lstate-match-renamevarp
- Value matching part of the
variable renaming relation over local states.
- Soutcome-result-renamevarp
- Variable renaming relation over statement outcome results.
- Lstate-renamevarp
- Variable renaming relation over local states.
- Reserr-limitp-theorems
- Theorems about reserr-limitp.
- Eoutcome-result-renamevarp
- Variable renaming relation over expression outcome results.
- Eoutcome-renamevarp
- Variable renaming relation over expression outcomes.
- Soutcome-renamevarp
- Variable renaming relation over statement outcomes.
- Cstate-renamevarp-with-larger-renaming
- Theorems about computation states and variable renamings,
not involving dynamic semantic operations.
- Cstate-renamevarp
- Variable renaming relation over computation states.
- Funinfo-renamevarp
- Variable renaming relation over function information.
- Funscope-renamevarp
- Variable renaming relation over function scopes.
- Funenv-renamevarp
- Variable renaming relation over function environments.
- Path/paths-renamevar-theorems
- Theorems about variable renaming for paths.
- Init-local-when-renamevar
- Theorems about local state initialization and variable renaming.
- Write-var/vars-value/values-when-renamevar
- Theorems about writing variables and variable renaming.
- Add-var/vars-value/values-when-renamevar
- Theorems about adding variables and variable renamings.
- Read-var/vars-value/values-when-renamevar
- Theorems about reading variables and variable renaming.
- Vars-of-cstate-after-exec
- Theorems about the variables in a computation state
after execution of certain kinds of constructs.
