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.