Figure 5: A binding (solid vectors) and an alternate binding (dashed).
Let E' and E be environments with state spaces built as Cartesian products of a family of disjoint sets . The might represent the state spaces of object types like egg and fork. E' and E would then each have state spaces make of up some number of copies of egg and fork.
We will say that a projection from E' to E is simple if every component of its result is a component of its argument. That is
for some in [1,n]. Thus takes a E'-state, s', probably throws away some of its components, and possibly rearranges the rest to form a new tuple. For example, might single out a particular egg's state and/or a particular fork's state and throw the other state components away. When a projection is simple, we can define a kind of inverse for it, which we will call its back-projection. We will define the back-projection, , of to be the function whose result is s' with those components that keeps replaced by their corresponding components from s. For example, if is defined by
then its back-projection would be given by:
We will say that a simple projection is a binding of E to E' if it is also a simple reduction of E' to E (see Figure 5).
The proof follows from the definitions of simple projection and back-projection. We will say that E' is uniformly reducible to E if every simple projection from E' to E is a binding.