Context
A LocalContext is a mathematical structure. It has a universe of nodes of varying types. In the mathematical world, the recursion equations define a specific representative of the isomorphism class of that mathematical structure. The universe of that representative consists of some subset of the integers. In the implementation to be constructed here, the "index" field of a node contains the node value to be used in the mathematical world. i.e., if n is a node representation, ER(n) is simply n.index and F(n) = n.index.
We assume that when an operation on a LocalContext, lc, involves nodes of that structure, these will be nodes within ER(lc). The implementation checks for this. The key reason that this works is that under these conditions, the rest of the body of n is in the ER(lc), even though not in ER(n). This requires a slight modification to the assumptions in the paper. In particular, definition 7.3 makes too strong a requirement. The conclusions of def 7.3 need only follow for some recursion equations, not all. Exactly how to state this I have not yet figured out. I will write a more detailed justification later.
Notice that we assume ER(n) is unmodifiable, thus there is no sharing between n and its containing LocalContext.
In addition, we remark that one need not actually include the index field in the implementation, or the checks. Presumably one has proven that for all reachable configurations the check will succeed, hence one need not perform it. Second, the code never looks at the index field, hence if the field is removed then the resulting computation will be isomorphic to a computation including the index field. Hence, the resulting LocalContext representation will be isomorphic to the representation of the computation that includes the field, hence isomorphic to the result in the mathematical world.
WARNING: All of the above leads to the following remarks. Some of the mathematical values below are represented by a rather indirect means, namely a pointer to a record with a field containing the value. (Or without the field...) Other mathematical values are reprsenented by large data structures that include some of the records just described. Whenever an operation is to be performed on more than one mathematical value, where the representations have this form, then one must always be sure that all the records involved belong to the same large data structure.
LocalContext
LocalContext: BaseType;
CreateEmptyContext:
BaseFunction [ ]
Returns [ LocalContext ];
FakeDamageContext:
BaseFunction [ LocalContext.arg ]
Returns [ LocalContext.res ]
DamagedReps [ LocalContext.arg ];
Paint
Paint: BaseType;
GetUnpaintedPaint:
BaseFunction [ LocalContext.arg ]
Returns [ LocalContext.res, Paint ]
DamagedReps[ LocalContext.arg ];
GetUniquePaint:
BaseFunction [ LocalContext.arg ]
Returns [ LocalContext.res, Paint ]
DamagedReps[ LocalContext.arg ];
(doesn't really damage LocalContext.arg, but makes for easier writing of some function bodies, e.g., MakeType)