|
|
|---|
|
|
|
|---|
The
The
Conceptually, this transformation could be split into two:
one that disambiguates variables, and one that disambiguates functions;
the two are independent, and can be applied in any order.
We follow this approach,
by formalizing the disambiguation of variables and functions separately,
and by defining
There are many possible ways to rename variables or functions so that they are globally unique. To avoid committing to a specific renaming approach, we characterize these transformations relationally instead of functionally: instead of defining a function that turns the original code into the transformed code, we define a predicate over original and transformed code that holds when the two have the same structure except for possibly the variable or function names.
This relational formulation of
the disambiguation of variables and functions
opens the door to defining each as the combination of
a renaming relation that may or may not yield globally unique names,
and an additional uniqueness requirement on the transformed code.
Thus, the