Proof appendix: Composition of functions with accumulating parameters
Janis Voigtl · 2004
In this appendix to the article \Composition of functions with accumulating we prove Theorem 5.2 of that paper, showing that Construction 5.1 produces an mtt that is equivalent to the composition of the two given ones. Firstly, we will formalise the idea of \walking upwards in the intermediate result to obtain the context parameters of calls of the second mtt’s states on the context parameters of the rst mtt, as presented in Subsection 4.6. To that purpose, we introduce functions that|as we will prove|give answers to the question Q in Subsection 4.5. We will introduce some auxiliary notions, in particular an ordering relation that will be useful to prove the \cutting of potential cycles mentioned in Subsection 4.10. We present some properties of the mentioned functions and relations, and prepare the main proof by establishing some necessary technical lemmata. In the following, let M1 and M2 be two xed mtts as in Construction 5.1. We will also use the notations and names introduced there. For technical reasons, we assume without loss of generality that there are no name conicts between M1 and M2, i.e., all involved ranked alphabets are pairwise disjoint. This can always be achieved by renaming and guarantees, e.g., that rewrite rules of M1 and M2 can be applied in arbitrary order ()R1[R2 is conuen t). As noted below Theorem 5.2, we could generalise the weakly single-use property in Denition 3.6 by dropping condition (ii) and requiring condition (i) only for states g that do have context parameters, without requiring any change to Construction 5.1. In fact, the proofs in this appendix will from Denition 3.6 only use condition (i) and this only for states of M2 with rank greater than one. Also, the non-copying restriction ofM1 and the weakly single-use restriction ofM2 will not be needed if one of the two is a tdtt. Thus, our correctness proof for Construction 5.1 also incorporates proofs for the known results TOP ; MAC MAC (Engelfriet, 1981) and MAC ;TOP MAC (Engelfriet & Vogler, 1985). Firstly, we introduce functions that can be used to answer question Q from Subsection 4.5.