Process predicate-variable

An instantiation of a Process/ predicate-variable transforms the heads HX of the induction parameter X into a vector HY of heads of the other parameter Y. An instantiation of a Composepredicate-variable computes the other parameter Y from its heads HY (obtained by processing the HX) and tails TY (obtained by recursion on the TX). Step 6 does this simultaneously, and hence actually looks for an instantiation of a ProcCompk predicate-variable that computes the other parameter Y from the heads HX and tails TY. Step 6 yields LA(fr) by first invoking the MSG Method (see Chapter 10) and assessing its results via some heuristics if these results are not satisfying, then a so-called Synthesis Method (see Section 14.2.4) is invoked. 

Schema-guided synthesis was argued for in Section 8.1 because schemas are an interesting way of incorporating algorithm design knowledge into a synthesis process. Schema-guided synthesis is naturally a stepwise synthesis, as the predicate-variables are not all instantiated at the same time. A most interesting approach was then advocated in Section 8.3, namely to deploy an entire tool-box of predicate-variable instantiating methods, rather than a unique method. In Chapter 9 (Proofs-as-Programs Method) and Chapter 10 (MSG Method), we described two of the more sophisticated methods we have developed so far. Note that these methods are entirely dissociated from specific schemas or predicate-variables.

An instantiation of the Discriminate predicate-variable tests the values of HX, TX, Y to see whether SolveNonMinj, respectively Process/ a Compose), is applicable. 

We must now connect these various predicates to be able to derive state variables from other state variables. The process of transitioning from one... 

---