Metabolism involves performing the same transformation uniformly to instances of the same type of object: cooking all the eggs, or cleaning/dirtying all the forks. Often times, however, an agent will work toward different kinds of goals at once. This can often be done by interleaving the actions from solutions to the individual goals. We will say that an interleaving I is a function that returns one or the other of its first two arguments, depending on a third state argument:
When the last two arguments of I are policies, the result is itself a policy, so we will define the notation:
If we wanted to simultaneously make toast and cook an egg, then a good interleaving of a toast-making policy and an egg-cooking policy would be one that chose the egg-making policy whenever the egg had finished its current cooking step (and so was ready to be flipped or removed from the pan) and chose the toast-making policy when the egg was busy cooking. A bad interleaving would be one that always chose the toast-making policy.
An interleaving I is fair for and if starting from any state, will after some finite number of steps have executed both and at least once. Finally, we will say that two bindings are independent if they map disjoint sets of components to their images. Binding independence is a special case of subgoal independence: two policies can't possibly interfere if they alter distinct state components. Fairness and binding independence are sufficient conditions for an interleaving to solve a conjunctive goal:
Proof: Since I is a fair interleaving, each of the two policies will be executed in finite time, regardless of starting state. By induction, for any n, there is a number of steps after which I is guaranteed to have executed at least n steps of each policy.
The policy is the composition of a policy for a state space with a binding. If solves and halts, then it must do so by having solve and halt in some finite number of steps n. During execution, the environment goes through a series of states
which project under to a series of states
we claim that any execution of the interleaving must bring the environment through a sequence of states that project under to
that is, a string of states in which appears at least once, then , appears at least once, and so on. The only state transitions that appear are from some to itself or to . Suppose it were otherwise. Then there must be a point at which this series is broken:
where s is neither nor . We have two cases. Case 1: executed the transition. Then we have that , a contradiction. Case 2: executed the transition. Then has changed one of the state components mapped by and so and are not independent, a contradiction. Thus the interleaving solves . By the same reasoning, it must halt in , since halts in . Also by the same reasoning, it must solve and halt, and hence, must solve the intersection and halt.
A useful corollary to this is that when the same policy is applied under two independent bindings, the bindings can be safely interleaved, that is, interleaving commutes with binding: