Recursion Operator Extensions of Term Algebras and their Standard Squashing
Full text
Recursion Operator Extensions of Term Algebras and their Standard Squashing Christoph V. Meyer <christoph.meyer(at)stud.uni-heidelberg.de>1 1Ruprecht-Karls-Universität Heidelberg May 18, 2025 Abstract Let T(X)be a term algebra over a set of variables X. We introduce the concept of extensions of T(X), that add additional operators to the term algebra, and squashings, which map each of the newly created terms in the extended term algebra to a term in the original one. We define a particular kind of extension, the recursion operator extension, which allows us to express any recurring pattern in a term precisely and formally using a general recursion operator. We also define a squashing from the recursion operator extension back onto the original term algebra, the standard squashing, which unravels the recursion operator, and subsequently study the properties of recursion operator extensions and their standard squashing. Contents Contents 1 1 Introduction 3 1.1 Symbolsused........................................ 3 1.2 Statementoftheorems................................... 4 1.3 Basicdefinitions ...................................... 5 1.4 Proofsofwell-definedness ................................. 7 2 Properties of extensions, squashings and substitutions 9 2.1 Naïveapproach....................................... 9 2.2 Algebraicapproach..................................... 20 2.3 Outlook: Categorial approach . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 3 Recursion operator extensions and the standard squashing 26 3.1 Formaldefinition...................................... 26 3.2 Properties.......................................... 31 3.2.1 Basicproperties .................................. 31 3.2.2 Equivalence classes of recursion depths, generalization to the natural numbers andresultingproperties .............................. 39 1
4 Applications and Examples 57 4.1 Generalconsiderations................................... 57 4.2 A simple example: Calculating the golden ratio . . . . . . . . . . . . . . . . . . . . . 58 4.3 Observations on "big operators" of Abelianmonoids ................. 59 5 Acknowledgments 59 List of Figures 60 List of Tables 60 References 60 2
1 Introduction 1.1 Symbols used Symbol Meaning Definition ι:A ,→BInclusion map from Ato B⊇A[3, p. 5] SnSymmetric group of degree n[2, p. 30] T(X)Term algebra over X[1, p. 84] T(X)Universe of T(X)[1, p. 84] fT(X)σ(f)-ary operator of (F, σ)-type T(X)corresponding to f∈ F [1, p. 84] φHomomorphism T(X)→Ainduced by φ:X→A[1, p. 85] MSet of all 1-tuples of elements in M1.1 enMEnclosure map of M1.2 f⊎gUnion of the maps fand g1.3 f[x07→ y0]Overriding of x0by y0in f1.4 e SInduced map of the substitution S1.12 tSApplication of the substitution Sto the term t1.12 X∁Set of all non-variable terms 1.12 P(T(X)) Recursion operator extension of T(X)3.3 TP(X)Universe of P(T(X)) 3.3 Pn i=stRecursion operator 3.5 qXStandard squashing of P(T(X)) onto T(X)3.6 T(X)∁Set of all recursion operator extended terms in TP(X)3.6 t≻0Existence of a predecessor of t3.7 t−Predecessor of t3.7 ∥t∥≻Natural cardinality of t3.22 t1≡≻t2Natural congruence of t1and t23.25 nCanonical representative of [t]≡≻, where ∥t∥≻=n3.28 Table 1: Symbols used 3
Arrow Meaning Map Injective map Surjective map Bijective map Homomorphism Monomorphism Epimorphism Isomorphism 2-(mono-,epi-,iso-)morphism Induction Table 2: Arrows used in diagrams 1.2 Statement of theorems Theorem 3.32. For every recursion operator extensible term algebra T(X)over X,i∈Xand s, n1, n2, t ∈TP(X)with n1≡≻n2, the following equation holds: qXn1 P i=s t=qXn2 P i=s t=qX ∥n1∥≻ P i=s t =qX ∥n2∥≻ P i=s t .(1) Theorem 3.38 (Variable exchange theorem).For every recursion operator extensible term algebra T(X)over X,i1, i2∈Xwith i1=i2,s∈TP(X),n∈N0and t∈T(X\ {i2}), the following equation holds: qX n P i1=s t!=qX n P i2=s tenX[i17→ (i2)]!.(2) Theorem 3.41. For every recursion operator extensible term algebra T(X)over X,i∈X,k∈N, n1, . . . , nk∈N0and s, t ∈TP(X), the following equation holds: qX n1 P i=Pn2 i=... Pnk i=st ...t t =qX Pk j=1 nj P i=s t .(3) Theorem 3.46. For every recursion operator extensible term algebra T(X)over X,k∈N,i1, . . . , ik ∈X, where i1, . . . , ikare distinct, n1, . . . , nk∈N0,s∈TP(X)and t∈TP(X\ {i1, . . . , ik−1}), the 4
following equation holds: qX n1 P i1=s n2 P i2=(i1) . . . nk P ik=(ik−1) t!=qX Qk j=1 nj P ik=s t .(4) 1.3 Basic definitions Definition 1.1 (Set of all 1-tuples).Let Mbe a set. M:={(x)|x∈M}(S1T) Definition 1.2 (Enclosure map).Let Mbe a set. The enclosure map of Mis the map enM:M→M x7→ (x).(Enc1) Analogously, its inverse is given by the map en−1 M:M→M (x)7→ x.(Enc2) Definition 1.3 (Union of maps).Let A, B, C, D be sets with A∩B=∅and f:A→B,g:C→D be maps. The Union of fand gis the map f⊎g:A⊎B→C∪D x7→ (f(x), x ∈A g(x), x ∈B.(UnM) Definition 1.4 (Overriding).Let A, B be sets, f:A→Ba map, x0∈Aand y0be a mathematical object. The overriding of fin x0by y0is the map f[x07→ y0]: A→B∪ {y0} x7→ (y0, x =x0 f(x), x =x0 .(Ove) Definition 1.5 (Extensibility of a term algebra).Let T(X)be the term algebra of some type (F, σ) over Xand (G, τ)be a type. If and only if F ∩ G =∅(Ext1) and G ∩ X=∅(Ext2) apply, we say T(X)is (G, τ)-extensible and (G, τ)is extending T(X). Definition 1.6 (Extension of a term algebra).Let T(X)be the term algebra of some type (F, σ) over Xand (G, τ)be a type extending T(X). The (G, τ)-extension of T(X)is the term algebra of type (F ⊎ G, σ ⊎τ)over X. 5
Definition 1.7 (Squashability of an algebra).Let A:= (A, FA)be an algebra of some type (F, σ) and B:= (B, FB)be an algebra of some type (G, τ). We say Ais squashable with respect to Bif and only if G ⊆ F (Sqb1) τ=σG(Sqb2) B⊆A(Sqb3) apply. Definition 1.8 (Squashing of an algebra).Let A:= (A, FA)be an algebra of some type (F, σ) and B:= (B, FB)be an algebra of some type (G, τ), where Ais squashable with respect to B. A squashing of Aonto Bis a map q:A→Bwith qB= idB.(Squ) Definition 1.9 (Trivial squashing).Let A:= (A, FA)be an algebra of some type (F, σ). The trivial squashing of Ais the map idA. Definition 1.10 (Substitution).Let T(X)be the term algebra of some type (F, σ)over X. A substitution Sin T(X)is a map S:X→T(X).(Sub) Furthermore, given a subset A⊆T(X), a map S′:X→Aand the inclusion map ι:A ,→T(X), we may for the sake of simplicity omit ιwhen considering the substitution ι◦S′. Definition 1.11 (Trivial substitution).Let T(X)be the term algebra of some type (F, σ)over X. The trivial substitution in T(X)is the map enX. Definition 1.12 (Application of a substitution).Let T(X)be the term algebra of some type (F, σ) over Xand Sbe a substitution in T(X). The substitution Sinduces a map e S:T(X)→T(X) given by the restriction of its domain to Xand X∁:=T(X)\Xrespectively: e SX:X→T(X) (x)7→ S(x)(ApS1) e SX∁:X∁→T(X) (f, t1, . . . , tσ(f))7→ (f, e S(t1),...,e S(tσ(f))). (ApS2) For a term t∈T(X), the application tSis given by tS:=e S(t).(ApS3) Definition 1.13 (Set of variables).Let T(X)be the term algebra of some type (F, σ)over Xand M⊆T(X). The set of variables in Mis the set vars M∩X:= en−1 XM∩X(SoV1) vars M∩X∁:=[ σ(f) [ k=1 vars({tk})(f, t1, . . . , tσ(f))∈M∩X∁ (SoV2) vars M:= vars M∩X∪vars M∩X∁.(SoV3) 6
1.4 Proofs of well-definedness Lemma 1.14 (Well-definedness of the extension of a term algebra).For every term algebra T(X) over Xand every type (G, τ)extending T(X), the (G, τ)-extension of T(X)is well-defined. Proof. Let T(X)be the term algebra of some type (F, σ)over Xand (G, τ)be a type extending T(X). The sets Fand Gare disjoint according to (Ext1), so the map σ⊎τis well-defined. Moreover, the sets Fand Xare disjoint according to the assumption that T(X)is a term algebra, and according to (Ext2) the sets Gand Xare disjoint. Thus, F ⊎G and Xare disjoint, which is a sufficient criterion for the well-definedness of the term algebra of type (F ⊎ G, σ ⊎τ)over X. Lemma 1.15 (Existence of a squashing between every two squashable algebras).For every algebra Athat is squashable with respect to an algebra B, there exists a squashing of Aonto B. Proof. Let A:= (A, FA)be an algebra of some type (F, σ)and B:= (B, FB)be an algebra of some type (G, τ), where Ais squashable with respect to B. According to (Sqb3), Bis a subset of A, therefore there exists a map q:B→Awhich extends idA. The map qalready fulfills the requirement (Squ). Lemma 1.16 (Well-definedness of the trivial squashing).For every algebra A, the trivial squashing of Ais well-defined. Proof. Let A:= (A, FA)be an algebra of some type (F, σ). The algebra Ais squashable with respect to itself because •(Sqb1) is satisfied by F ⊆ F, •(Sqb2) by σ=σFand •(Sqb3) by A⊆A. Furthermore, idAfulfills the requirement (Squ), since idAA= idAapplies. Lemma 1.17 (Existence of a substitution in every term algebra).For every term algebra T(X) over X, there exists a substitution in T(X). Proof. Let T(X)be a term algebra over X. Since for every variable x∈X, the 1-tuple (x)is a term in T(X),Xconstitutes a subset of T(X). Hence, the inclusion map ι:X ,→T(X)exists and the composition ι◦enXalready satisfies the requirement (Sub). Corollary 1.18 (Well-definedness of the trivial substitution).For every term algebra T(X)over X, the trivial substitution of T(X)is well-defined. Proof. The claim directly follows from the proof of Lemma 1.17. Lemma 1.19 (Well-definedness of the application of a substitution).For every term algebra T(X) over Xand every substitution Sin T(X), the map induced by S, that is e S, is well-defined. Proof. Let T(X)be the term algebra of some type (F, σ)over X,t∈T(X)and Sbe a substitution in T(X). Let t= (x)∈Xwith x∈X. Then follows: tS(ApS3) =e S(t)(ApS1) =S(x)∈T(X). (5) 7
Now let t= (f, t1, . . . , tσ(f))∈X∁with f∈ F,t1, . . . , tσ(f)∈T(X). Assume that the claim has already been proven for t1, . . . , tσ(f). Thus follows: tS(ApS3) =e S(t)(ApS2) = (f, e S(t1),...,e S(tσ(f))) ∈T(X). (6) Lemma 1.20 (Well-definedness of the set of variables).For every term algebra T(X)over Xand every set M⊆T(X), the set of variables vars Mis well defined. Proof. Let T(X)be the term algebra of some type (F, σ)over Xand M⊆T(X). Clearly, M∩ X⊆X= dom en−1 X, so vars M∩Xis well-defined. In particular, vars{t}is well-defined for every t∈M∩X. Let t= (f, t1, . . . , tσ(f))∈M∩X∁and assume that the well-definedness of vars{t1},...,vars{tσ(f)}has already been proven. Then, σ(f) [ k=1 vars{tk}(7) =[ σ(f) [ k=1 vars{tk} (8) (SoV2) = vars{t}. (9) We conclude: vars M∩X∁(10) (SoV2) =[ σ(f) [ k=1 vars({tk})(f, t1, . . . , tσ(f))∈M∩X∁ (11) =[ [ (f,t1,...,tσ(f))∈M∩X∁ σ(f) [ k=1 vars({tk}) (12) =[ [ t∈M∩X∁[ σ(f) [ k=1 vars({tk})(f, t1, . . . , tσ(f))∈ {t} (13) (SoV2) =[ [ t∈M∩X∁ vars{t} (14) =[ t∈M∩X∁ vars{t} | {z } well-defined . (15) Thus, vars M∩X∁is well-defined. By (SoV3), the set vars M= vars M∩X∪vars M∩X∁ is also well-defined. 8
2 Properties of extensions, squashings and substitutions 2.1 Naïve approach When extending a term algebra T(X), we are introducing new operators to it while leaving all operators of T(X)as well as the set of variables Xintact. Consequently, any term that can be expressed in T(X)can also be expressed in any extension of the latter. This superset property also allows us to formulate a squashing from the extension back onto the original term algebra. The essence of this paper is to leverage this fact by temporarily introducing new operators to an already existing term algebra (i.e. extending it) and subsequently squashing it back. The choice of the particular squashing enables us to express far more complex terms without permanently relying on more complex term algebras and without using any kind of informal notation, like ellipsis. Lemma 2.1 (Superset property of the universe of an extension).For every term algebra T(X)over Xand every type (G, τ)extending T(X), we denote the universe of the (G, τ)-extension of T(X) with TE(X). It holds that: T(X)⊆TE(X).(16) Proof. Let T(X)be the term algebra of some type (F, σ)over X,(G, τ)be a type extending T(X) and t∈X. The claim evidently holds, hence tis a variable and T(X)and the (G, τ)-extension of T(X)share the same set of variables X. Now let t= (f, t1, . . . , tσ(f))∈X∁with f∈ F, t1, . . . , tσ(f)∈T(X). Assume that the claim has already been proven for t1, . . . , tσ(f). Then follows f∈ F ⊎ G and t1, . . . , tσ(f)∈TE(X), thus t∈TE(X)holds. Lemma 2.2 (Squashability of extensions).For every term algebra T(X)over Xand every type (G, τ)extending T(X), the (G, τ)-extension of T(X)is squashable with respect to T(X). Proof. Let T(X)be the term algebra of some type (F, σ)over Xand (G, τ)be a type extending T(X). The (G, τ)-extension of T(X)is by definition 1.6 of type (F ⊎G, σ⊎τ). Hence the requirement (Sqb1) is fulfilled by the fact F ⊆ F⊎G and (Sqb2) by σ= (σ⊎τ)dom σ= (σ⊎τ)F. The requirement (Sqb3) directly follows by applying Lemma 2.1. Remark 2.3. For every type (G, τ), every (G, τ)-extensible term algebra T(X)and every squashing qfrom E(T(X)) onto T(X), where E(T(X)) denotes the (G, τ)-extension of T(X)with universe TE(X), the following diagram commutes: T(X)E(T(X)) T(X) ι idT(X) q Figure 1: Characteristic property of squashings between term algebras The existence of ι:T(X),→TE(X)and qfollow from Lemma 2.1 and 2.2, respectively. Obviously, squashing a term that has already been squashed has no effect, as squashings do not alter terms in their codomain. This statement applies more generally to any two algebras where one is squashable with respect to the other. 9
Instead of replacing some variable i1∈Xdirectly, we might first replace i1with an "auxiliary variable" i2∈X. This operation is not completely trivial, as i2must not appear in the term operated on. Otherwise, replacing i1with i2first and replacing i1directly may result in different terms. Example 2.14. Consider the term 2x−y. If we wanted to replace xby z, yielding 2z−y, we can without any problems first replace xby some other variable w, so 2x−yturns into 2w−yand finally 2z−y. It becomes problematic when we choose yas the auxiliary variable. In that case, 2x−y turns into 2y−yand finally 2z−z. What were initially two separate variables have now become indistinguishable from one another. Lemma 2.15 (Exchange of variables in overridings of the trivial substitution).For every term algebra T(X)over X,i1, i2∈Xwith i1=i2,t∈T(X\ {i2})and u∈T(X), it holds: tenX[i17→ u] = tenX[i17→ (i2)]enX[i27→ u].(104) Proof. Let T(X)be the term algebra of some type (F, σ)over X,i1, i2∈Xwith i1=i2,t∈ T(X\ {i2})and u∈T(X). We observe: tenX[i17→ u](ApS3) = enX[i17→ u] : (t)(105) and tenX[i17→ (i2)]enX[i27→ s](106) (ApS3) = enX[i27→ s] : (tenX[i17→ (i2)]) (107) (ApS3) = enX[i27→ s] : ◦enX[i17→ (i2)] : (t). (108) We first prove the case t= (i1): tenX[i17→ u](109) (105) = enX[i17→ u] : ((i1)) (110) (ApS1) = enX[i17→ u](i1)(111) (Ove) =u(112) and tenX[i17→ (i2)]enX[i27→ u](113) (108) = enX[i27→ u] : ◦enX[i17→ (i2)] : ((i1)) (114) (ApS1) = enX[i27→ u] : ◦enX[i17→ (i2)](i1)(115) (Ove) = enX[i27→ u] : ((i2)) (116) (ApS1) = enX[i27→ u](i2)(117) (Ove) =u. (118) Next, we prove the case t= (x)∈X\ {i1, i2}, where xis an arbitrary variable in X\ {i1, i2}: tenX[i17→ u](119) 16
(105) = enX[i17→ u] : ((x)) (120) (ApS1) = enX[i17→ u](x)(121) (Ove) = (x)(122) and tenX[i17→ (i2)]enX[i27→ u](123) (108) = enX[i27→ u] : ◦enX[i17→ (i2)] : ((x)) (124) (ApS1) = enX[i27→ u] : ◦enX[i17→ (i2)](x)(125) x=i1 (Ove) = enX[i27→ u] : ((x)) (126) (ApS1) = enX[i27→ u](x)(127) x=i2 (Ove) = (x). (128) Thus, we have shown the claim for all t∈ {(i1)} ∪ X\ {i1, i2}(S1T) ={(x)|x∈ {i1}} ∪ {(x)| x∈X\ {i1, i2}} ={(x)|x∈X\ {i2}} (S1T) =X\ {i2}. Lastly, we prove the claim for t= (f, t1, . . . , tσ(f))∈X\ {i2}∁with f∈ F and t1, . . . , tσ(f)∈T(X\{i2}). Assume that the claim has already been proven for t1, . . . , tσ(f). Then follows: tenX[i17→ (i2)]enX[i27→ u]=(f, t1, . . . , tσ(f))enX[i17→ (i2)]enX[i27→ u](129) (ApS2),(ApS3) = (f, t1enX[i17→ (i2)]enX[i27→ u], . . . , tσ(f)enX[i17→ (i2)]enX[i27→ u]) (130) = (f, t1enX[i17→ u], . . . , tσ(f)enX[i17→ u]) (131) (ApS2),(ApS3) = (f, t1, . . . , tσ(f))enX[i17→ u](132) =tenX[i17→ u]. (133) Corollary 2.16 (Back-and-forth substitution of variables).For every term algebra T(X)over X, i1, i2∈Xwith i1=i2and t∈T(X\ {i2}), it holds: t=tenX[i17→ (i2)]enX[i27→ (i1)].(134) Proof. Let T(X)be a term algebra over X,i1, i2∈Xwith i1=i2and t∈T(X\ {i2}). It follows: tenX[i17→ (i2)]enX[i27→ (i1)] (135) Lemma 2.15 =tenX[i17→ (i1)] (136) Lemma 2.9 =t. (137) The next result is an occasionally useful combination of Lemma 2.12 and Lemma 2.15. 17
Lemma 2.17. For every recursion operator extensible term algebra T(X)over X,i1, i2∈Xwith i1=i2,t, u ∈T(X\ {i2})and v∈T(X), the following equation holds: tenX[i17→ u]enX[i17→ v] = tenX[i17→ uenX[i17→ (i2)]]enX[i27→ v].(138) Proof. Let T(X)be the term algebra of some type (F, σ)over X,i1, i2∈Xwith i1=i2,t, u ∈ T(X\ {i2})and v∈T(X). We first prove the case t= (i1): tenX[i17→ uenX[i17→ (i2)]]enX[i27→ v](139) = (i1)enX[i17→ uenX[i17→ (i2)]]enX[i27→ v](140) (ApS1) =uenX[i17→ (i2)]enX[i27→ v](141) Lemma 2.15 =uenX[i17→ v](142) and tenX[i17→ u]enX[i17→ v](143) = (i1)enX[i17→ u]enX[i17→ v](144) (ApS1) =uenX[i17→ v]. (145) Next, we prove the case t= (x)∈X\ {i1, i2}with x∈X\ {i1, i2}: tenX[i17→ uenX[i17→ (i2)]]enX[i27→ v](146) = (x)enX[i17→ uenX[i17→ (i2)]]enX[i27→ v](147) Lemma 2.10 = (x)enX[i27→ v](148) Lemma 2.10 = (x)(149) and tenX[i17→ u]enX[i17→ v](150) = (x)enX[i17→ u]enX[i17→ v](151) Lemma 2.10 = (x)enX[i17→ v](152) Lemma 2.10 = (x). (153) Lastly, we prove the claim for t= (f, t1, . . . , tσ(f))∈X\ {i2}∁with f∈ F and t1, . . . , tσ(f)∈ T(X\ {i2}). Assume that the claim has already been proven for t1, . . . , tσ(f). Then follows: tenX[i17→ u]enX[i17→ v](154) = (f, t1, . . . , tσ(f))enX[i17→ u]enX[i17→ v](155) (ApS3),(ApS2) = (f, t1enX[i17→ u]enX[i17→ v], . . . , tσ(f)enX[i17→ u]enX[i17→ v]) (156) = (f, t1enX[i17→ uenX[i17→ (i2)]]enX[i27→ v], . . . , tσ(f)enX[i17→ uenX[i17→ (i2)]]enX[i27→ v]) (157) (ApS3),(ApS2) = (f, t1, . . . , tσ(f))enX[i17→ uenX[i17→ (i2)]]enX[i27→ v](158) =tenX[i17→ uenX[i17→ (i2)]]enX[i27→ v]. (159) 18
Lastly, we prove the rather trivial fact that any term t∈T(X)is indeed an element of the term algebra over the set of variables that occur in t. This can be generalized to subsets M⊆T(X)and the set of variables that occur in any element in M. Lemma 2.18. For every term algebra T(X)over Xand t∈T(X), it holds that: t∈T(vars{t}).(160) Proof. Let T(X)be the term algebra of some type (F, σ)over X. Let t∈X. Then holds: t∈ {t} ∩ X(161) ⊆Ten−1 X{t} ∩ X (162) (SoV1) =Tvars {t} ∩ X (163) (SoV3) =T(vars{t}). (164) Now let t= (f, t1, . . . , tσ(f))∈X∁with f∈ F,t1, . . . , tσ(f)∈T(X)and assume that the claim has already been proven for t1, . . . , tσ(f). Thus follows: t= (f, t1 |{z} ∈T(vars{t1}) , . . . , tσ(f) |{z} ∈T(vars{tσ(f)}) )(165) ∈T σ(f) [ k=1 vars{tk} (166) =T [ σ(f) [ k=1 vars{tk} (167) =T [ σ(g) [ k=1 vars{uk}(g, u1, . . . , uσ(g))∈ {t} (168) t∈X∁ =T [ σ(g) [ k=1 vars{uk}(g, u1, . . . , uσ(g))∈ {t} ∩ X∁ (169) (SoV2) =Tvars {t} ∩ X∁ (170) (SoV3) ⊆T(vars{t}). (171) Corollary 2.19. For every term algebra T(X)over Xand M⊆T(X), it holds that: M⊆T(vars M).(172) Proof. Let T(X)be a term algebra over Xand M⊆T(X). It follows: M=[ t∈M {t} |{z} ∈T(vars{t}) Lemma 2.18 (173) 19
⊆[ t∈M vars{t}(174) = [ t∈M∩X vars{t} ∪ [ t∈M∩X∁ vars{t} (175) (10) = [ t∈M∩X vars{t} ∪vars M∩X∁(176) (SoV1) = [ t∈M∩X {en−1 X(t)} ∪vars M∩X∁(177) = en−1 XM∩X∪vars M∩X∁(178) (SoV1) = vars M∩X∪vars M∩X∁(179) (SoV3) = vars M. (180) 2.2 Algebraic approach It becomes clear from the definition of applications of substitutions (Definition 1.12), in particular from equation (ApS2), that the maps induced by substitutions possess some kind of homomorphic property. To be precise, the induced map of a substitution is an endomorphism in the term algebra it operates on. More generally, it is an homomorphism to the term algebra of the same type over the set of variables that occur in the image of the substitution. Lemma 2.20. For every term algebra T(X)over Xand every substitution Sin T(X),e Sis an endomorphism in T(X). Proof. Let T(X)be the term algebra of some type (F, σ)over Xand Sbe a substitution in T(X). We only need to consider terms in X∁, because terms in X, i.e. variables, are not the result of the application of an operator. Let (f, t1, . . . , tσ(f))∈X∁with f∈ F and t1, . . . , tσ(f)∈T(X). It follows: e S(fT(X)(t1, . . . , tσ(f))) (181) =e S((f, t1, . . . , tσ(f))) (182) (ApS2) = (f, e S(t1),...,e S(tσ(f))) (183) =fT(X)(e S(t1),...,e S(tσ(f))). (184) Lemma 2.21. For every term algebra T(X)over Xand every substitution Sin T(X),e Sis an automorphism in T(X)if SXis bijective and im S=X. In that case, the inverse of e Sis given by e S−1= enX◦SX−1◦enX : .(185) 20
Proof. Let T(X)be the term algebra of some type (F, σ)over Xand Sbe a substitution in T(X). Let SXbe bijective and im S=X. We will prove that enX◦SX−1◦enX : ◦e S= idT(X)=e S◦enX◦SX−1◦enX : . (186) Let t= (x)∈X. It follows: enX◦SX−1◦enX : ◦e S(t)(187) = enX◦SX−1◦enX : ◦e S((x)) (188) (ApS1) = enX◦SX−1◦enX : ◦S(x) |{z} ∈X (189) (ApS1) = enX◦SX−1◦enX◦en−1 X◦S(x)(190) = enX◦SX−1◦S(x)(191) im S=X = enX◦SX−1◦SX(x)(192) = enX(x)(193) = (x) = t= idT(X)(t) = t= (x)(194) = enX(x)(195) =SX◦SX−1◦enX(x)(196) =S◦SX−1◦enX(x)(197) =S◦en−1 X◦enX◦SX−1◦enX(x) | {z } ∈X (198) (ApS1) =e S◦enX◦SX−1◦enX(x)(199) (ApS1) =e S◦enX◦SX−1◦enX : ((x)) (200) =e S◦enX◦SX−1◦enX : (t). (201) Now let t= (f, t1, . . . , tσ(f))∈X∁, where t1, . . . , tσ(f)∈T(X), and assume that the claim has already been proven for t1, . . . , tσ(f). Thus follows: enX◦SX−1◦enX : ◦e S(t)(202) = enX◦SX−1◦enX : ◦e S((f, t1, . . . , tσ(f))) (203) (ApS2) = enX◦SX−1◦enX : f, e S(t1),...,e S(tσ(f)) (204) (ApS2) = f, enX◦SX−1◦enX : ◦e S(t1),...,enX◦SX−1◦enX : ◦e S(tσ(f))!(205) 21
= (f, t1, . . . , tσ(f)) = t= idT(X)(t) = t= (f, t1, . . . , tσ(f))(206) = f, e S◦enX◦SX−1◦enX : (t1),...,e S◦enX◦SX−1◦enX : (tσ(f))!(207) (ApS2) =e S f, enX◦SX−1◦enX : (t1),...,enX◦SX−1◦enX : (tσ(f))!(208) (ApS2) =e S◦enX◦SX−1◦enX : ((f, t1, . . . , tσ(f))) (209) =e S◦enX◦SX−1◦enX : (t). (210) Lemma 2.22. For every term algebra T(X)over X, every subset Y⊆Xand every substitution S in T(X)with im S⊆T(Y),e Sis a homomorphism T(X)→T(Y). Proof. Let T(X)be the term algebra of some type (F, σ)over X,Y⊆X,T(Y)be the term algebra of type (F, σ)over Yand Sbe a substitution in T(X)with im S⊆T(Y). For f∈ F and t1, . . . , tσ(f)∈T(Y), the following equation holds true: fT(X)(t1, . . . , tσ(f))(211) = (f, t1, . . . , tσ(f))(212) =fT(Y)(t1, . . . , tσ(f)). (213) We conclude for f∈ F and t1, . . . , tσ(f)∈T(X): e S(fT(X)(t1, . . . , tσ(f))) (214) =e S((f, t1, . . . , tσ(f))) (215) (ApS2) = (f, e S(t1) |{z} ∈T(Y) ,...,e S(tσ(f)) | {z } ∈T(Y) )(216) (213) =fT(Y)(e S(t1),...,e S(tσ(f))). (217) Corollary 2.23. For every term algebra T(X)over Xand every substitution Sin T(X),e Sis a homomorphism T(X)→T(vars im S). Proof. Let T(X)be a term algebra over Xand Sbe a substitution in T(X). It follows from Corollary 2.19 that im S⊆T(vars im S). Thus, according to Lemma 2.22, e Sis a homomorphism T(X)→T(vars im S). Lastly, we take a look at two special cases of overridings of the trivial substitutions, where we substitute one particular variable by another, whose induced maps happen to be surjective and bijective, respectively. Lemma 2.24. For every term algebra T(X)over Xand i1, i2∈Xwith i1=i2,enX[i17→ (i2)] : is an epimorphism T(X)→T(X\ {i1}). 22
Proof. Let T(X)be a term algebra over X,i1, i2∈Xwith i1=i2and T(X\ {i1})be of the same type as T(X). Since •X\ {i1}is a subset of X, •enX[i17→ (i2)] is a substitution in T(X)according to Lemma 2.7 and •im enX[i17→ (i2)] : ⊆X\ {i1}according to Lemma 2.11, enX[i17→ (i2)] : is a homomorphism T(X)→T(X\{i1})according to Lemma 2.22. It is left to show surjectivity. Let t∈T(X\ {i1})and consider tenX[i27→ (i1)], which is a term in T(X)according to Lemma 2.7. It follows: enX[i17→ (i2)] : (tenX[i27→ (i1)]) (218) (ApS2) =tenX[i27→ (i1)]enX[i17→ (i2)] (219) Corollary 2.16 =t. (220) Lemma 2.25. For every set Xwith i1, i2∈X, where i1=i2,enX\{i2}[i17→ (i2)] : is an isomorphism T(X\ {i2})→T(X\ {i1}). Proof. Let Xbe a set with i1, i2∈X, where i1=i2, and T(X\{i2})and T(X\{i1})share the same type. According to Lemma 2.24, enX[i17→ (i2)] : is an epimorphism T(X)→T(X\{i1}). Therefore, the restriction enX[i17→ (i2)] : T(X\{i2}) Lemma 2.13 = enX\{i2}[i17→ (i2)] : (221) inherits the homomorphic property. Following the proof of Lemma 2.24, we know that for any t∈T(X\ {i1}), the statement tenX[i27→ (i1)] ∈enX[i17→ (i2)] : −1 ({t})(222) is true. Because T(X\ {i1})is a subset of T(X),tis an element in T(X), and in combination with Lemma 2.11, we conclude tenX[i27→ (i1)] ∈T(X\ {i2}). We refine statement (222) to obtain: tenX[i27→ (i1)] ∈enX[i17→ (i2)] : T(X\{i2}) −1 ({t})(223) Lemma 2.13 = enX\{i2}[i17→ (i2)] : −1 ({t}). (224) Therefore, enX\{i2}[i17→ (i2)] : is an epimorphism T(X\ {i2})→T(X\ {i1}). It is left to show injectivity. For the sake of contradiction, assume that there exist u, v ∈T(X\ {i2})with u=v, such that enX\{i2}[i17→ (i2)] : (u) = enX\{i2}[i17→ (i2)] : (v)is true. It follows: enX\{i2}[i17→ (i2)] : (u) = enX\{i2}[i17→ (i2)] : (v)(225) Lemma 2.13 =⇒enX[i17→ (i2)] : T(X\{i2})(u) = enX[i17→ (i2)] : T(X\{i2})(v)(226) =⇒enX[i17→ (i2)] : (u) = enX[i17→ (i2)] : (v)(227) 23
(ApS3) =⇒uenX[i17→ (i2)] = venX[i17→ (i2)] (228) =⇒uenX[i17→ (i2)]enX[i27→ (i1)] = venX[i17→ (i2)]enX[i27→ (i1)] (229) u,v∈T(X\{i2}) Corollary 2.16 =⇒u=vu=v =⇒ ⊥. (230) Remark 2.26. Parts of the results of this subsection can be summarized in the following diagram, where T(X)is a term algebra over X,Sa substitution in T(X)and i1, i2∈Xwith i1=i2: T(X)T(X\ {i1}) T(X)T(vars im S)T(X\ {i2}) genX e Se S enX[i17→(i2)] : enX\{i1}[i27→(i1)] : Figure 4: Algebraic properties of substitutions 2.3 Outlook: Categorial approach We could also approach this topic in a categorial sense, but because this is not necessary for the following sections, we do not want to open that Pandora’s box and just give a quick overview. Lemma 2.27. For every algebra A,Band C, where Ais squashable with respect to Band Bis squashable with respect to C, and every squashing qfrom Aonto Bas well as every squashing r from Bonto C, the composition r◦qis a squashing from Aonto C. Proof. Let (F, σ),(G, τ)and (H, υ)be types and A,Band Cbe algebras of these types with universes A,Band C, respectively. Let Abe squashable with respect to Band Bbe squashable with respect to C. We first prove that Ais indeed squashable with respect to C: •(Sqb1): H ⊆ G ∧ G ⊆ F =⇒ H ⊆ F. •(Sqb2): υ=τH∧τ=σG=⇒υ=σGH H⊆G =σH. •(Sqb3): C⊆B∧B⊆A=⇒C⊆A. All that is left to show is that (Squ) is satisfied by r◦g, i.e. r◦qC= idC. Let c∈C. It holds: r◦qC(c) = rqC(c)(231) B⊇C =rqB(c)(232) (Squ) =r(idB(c)) (233) =r(c)(234) c∈C =rC(c)(235) B⊇C =rB(c)(236) (Squ) = idB(c)(237) 24
c∈C = idBC(c)(238) = idC(c). (239) Lemma 2.28. Let Xbe a set and Ob(Trm(X)) denote the class of all term algebras over X. Then Trm(X)forms a category, where for any T1(X),T2(X)∈Ob(Trm(X)), the hom-set HomTrm(X)(T1(X),T2(X)) is the set of all squashings from T1(X)onto T2(X)if T1(X)is squashable with respect to T2(X), and the empty set otherwise; the composition of morphisms is the composition of maps. Proof. Let Xbe a set. We conclude from Lemma 2.27 that compositions of morphisms are welldefined morphisms themselves. The associativity of the composition of morphisms follows from the associativity of the composition of maps. Furthermore, the trivial squashing of an object, which is the identity map over its universe, obviously satisfies bilateral neutrality. Lemma 2.29. Let Xbe a set and T1(X),T2(X)∈Ob(Trm(X)). Let Sqs(T1(X),T2(X)) := HomTrm(X)(T1(X),T2(X)) (240) and Ob(Sqs(T1(X),T2(X))) (241) = Ob(HomTrm(X)(T1(X),T2(X))) := HomTrm(X)(T1(X),T2(X)).(242) For any two morphisms q1, q2∈HomTrm(X)(T1(X),T2(X)), let HomTrm(X)(q1, q2)(243) := HomSqs(T1(X),T2(X))(q1, q2):={f∈Ob(Sqs(T1(X),T2(X))) |f◦q1=q2}.(244) Then Sqs(T1(X),T2(X)) forms a hom-category, where the composition of morphisms is the composition of maps. Proof. Let Xbe a set and T1(X),T2(X)∈Ob(Trm(X)). For any q1∈Ob(Sqs(T1(X),T2(X))), the identity morphism is given by q1itself, because q1◦q1=q1holds according to Lemma 2.4. For any q1, q2, q3∈Ob(Sqs(T1(X),T2(X))),f∈HomTrm(X)(q1, q2)and g∈HomTrm(X)(q2, q3), it holds: (g◦f)◦q1=g◦(f◦q1) = g◦q2=q3, (245) so g◦f∈HomTrm(X)(q1, q3). The associativity of the composition of morphisms follows from the associativity of the composition of maps. Lemma 2.28 and Lemma 2.29 let us conclude that for a set X, the category Trm(X)can also be understood as a strict 2-category (more precisely, a (2,2)-category), i.e. as a category enriched over Cat. Because all 2-morphisms of a squashing qin this new category are also 1-morphisms from the domain onto the codomain of q, we could repeat the process shown in Lemma 2.29 and construct Trm(X)as a strict n-category for arbitrary n∈Nand even as an (∞,∞)-category. Remark 2.30. Lemma 2.28 and Lemma 2.29 can be visualized using a diagram. Let Xbe a set, T1(X),T2(X)and T3(X)be term algebras over X, where T1(X)is squashable with respect to T2(X)and T2(X)is squashable with respect to T3(X). Let q1, q2, f be squashings from T1(X)onto T2(X)with f◦q1=q2and r1, r2, g be squashings from T2(X)onto T3(X)with g◦r1=r2. The following diagram, which shows a snippet of Trm(X), commutes: 25
=qXT(X)∁(u) = qXT(X)∁ n P j=s t!(274) n≻0 (StS3) =qX n− P j=(j) t!enX[j7→ qX(t)]enX[j7→ qX(s)] (275) =qX\{i} n− P j=(j) t!enX[j7→ qX(t)]enX[j7→ qX(s)] (276) =qX\{i} n− P j=(j) t!enX[j7→ qX\{i}(t)]enX[j7→ qX\{i}(s)] (277) and qX\{i}(u)(278) =qX\{i}T(X\{i})∁(u)(279) =qX\{i}T(X\{i})∁ n P j=s t!(280) n≻0 (StS3) =qX\{i} n− P j=(j) t!enX\{i}[j7→ qX\{i}(t)]enX\{i}[j7→ qX\{i}(s)]. (281) It is left to show that the equality (277)=(281), that is qX\{i} n− P j=(j) t!enX[j7→ qX\{i}(t)]enX[j7→ qX\{i}(s)] (282) =qX\{i} n− P j=(j) t!enX\{i}[j7→ qX\{i}(t)]enX\{i}[j7→ qX\{i}(s)], (283) holds. To show this, let v, w be arbitrary elements in codom qX\{i}=T(X\ {i}). It follows: venX\{i}[j7→ w](284) Lemma 2.13 =venX[j7→ w]X\{i}(285) (ApS3) = enX[j7→ w]X\{i} : (v)(286) = enX[j7→ w] : TP(X\{i})(v)(287) = enX[j7→ w] : (v)(288) (ApS3) =venX[j7→ w]. (289) In particular, for qX\{i}Pn− j=(j)t, qX\{i}(t), qX\{i}(s)∈T(X\ {i}), it holds: qX\{i} n− P j=(j) t!enX[j7→ qX\{i}(t)]enX[j7→ qX\{i}(s)] (290) 32
(289) =qX\{i} n− P j=(j) t!enX\{i}[j7→ qX\{i}(t)] | {z } ∈T(X\{i}) Lemma 2.7 enX[j7→ qX\{i}(s)] (291) (289) =qX\{i} n− P j=(j) t!enX\{i}[j7→ qX\{i}(t)]enX\{i}[j7→ qX\{i}(s)]. (292) We now observe what happens to the standard squashings of terms of the form Pn i=stin TP(X) if we remove the variable ifrom tor s. If idoes not occur in t, replacing it in every iteration has no effect. This becomes clear when we take a look at the flowchart diagram in Remark 3.11 again: If ndoes not have a predecessor, the result of the squashing is just always qX(s), otherwise, there is nothing to be replaced in qX(t), so the result is qX(t)regardless of n. Example 3.14. Let T(X)be the term algebra of type {0,1,S,+},01S+ 0 0 1 2over X:={i}. qX 0 P i=1 1+1!=1(293) qX S(0) P i=1 1+1!=1+1(294) qX S(S(S(S(0)))) P i=1 1+1!=1+1(295) Lemma 3.15. For every recursion operator extensible term algebra T(X)over X,i∈X,s, n ∈ TP(X)and t∈TP(X\ {i})with n≻0, the following equation holds: qXn P i=s t=qX(t).(296) Proof. Let T(X)be a recursion operator extensible term algebra over X,i∈X,s, n ∈TP(X)and t∈TP(X\ {i})with n≻0. Assert n−≻ 0. Then holds: qXn P i=s t(297) n≻0 (StS3) =qX n− P i=(i) t!enX[i7→ qX(t)]enX[i7→ qX(s)] (298) n−≻0 (StS3) =qX((i))enX[i7→ qX(t)]enX[i7→ qX(s)] (299) (i)∈T(X) =qXT(X)((i))enX[i7→ qX(t)]enX[i7→ qX(s)] (300) (Squ) = (i)enX[i7→ qX(t)]enX[i7→ qX(s)] (301) (ApS3),(ApS1) =qX(t)enX[i7→ qX(s)] (302) 33
t∈TP(X\{i}) =qXTP(X\{i})(t)enX[i7→ qX(s)] (303) Lemma 3.13 =qX\{i}(t) | {z } ∈T(X\{i}) enX[i7→ qX(s)] (304) Lemma 2.10 =qX\{i}(t)(305) Lemma 3.13 =qXTP(X\{i})(t)(306) =qX(t). (307) Now assert n−≻0and assume that the claim has already been proven for n−−≻ 0. Then holds: qXn P i=s t(308) n≻0 (StS3) =qX n− P i=(i) t!enX[i7→ qX(t)]enX[i7→ qX(s)] (309) n−≻0 (StS3) =qX n−− P i=(i) t!enX[i7→ qX(t)]enX[i7→ qX((i))]enX[i7→ qX(t)]enX[i7→ qX(s)] (310) =qX(t)enX[i7→ qX(t)]enX[i7→ qX((i))]enX[i7→ qX(t)]enX[i7→ qX(s)] (311) t∈TP(X\{i}) =qXTP(X\{i})(t)enX[i7→ qX(t)]enX[i7→ qX((i))]enX[i7→ qX(t)]enX[i7→ qX(s)] (312) Lemma 3.13 =qX\{i}(t) | {z } ∈T(X\{i}) enX[i7→ qX(t)]enX[i7→ qX((i))]enX[i7→ qX(t)]enX[i7→ qX(s)] (313) Lemma 2.10 =qX\{i}(t)enX[i7→ qX((i))]enX[i7→ qX(t)]enX[i7→ qX(s)] (314) Lemma 2.10 =qX\{i}(t)enX[i7→ qX(t)]enX[i7→ qX(s)] (315) Lemma 2.10 =qX\{i}(t)enX[i7→ qX(s)] (316) Lemma 2.10 =qX\{i}(t)(317) Lemma 3.13 =qXTP(X\{i})(t)(318) =qX(t). (319) If on the other hand idoes not occur in s, all instances of iwill be replaced with a term free of iin the last step of computing qX(Pn i=st), so the result will be free of ias well. Again, it helps to compare this result with the flowchart diagram in Remark 3.11. Example 3.16. Let T(X)be the term algebra of type {0,1,S,+},01S+ 0 0 1 2over X:={i}. qX S(S(0)) P i=i+i i+1!=i+i+1+1(320) qX S(S(0)) P i=1+1 i+1!=1+1+1+1(321) 34
Lemma 3.17. For every recursion operator extensible term algebra T(X)over Xand i∈X, s∈TP(X\ {i}),n, t ∈TP(X), the following statement holds: qXn P i=s t∈T(X\ {i}).(322) Proof. Let T(X)be a recursion operator extensible term algebra over X,i∈X,s∈TP(X\ {i}) and n, t ∈TP(X). We assert n≻ 0. Then holds: qXn P i=s t(323) n≻0 (StS3) =qX(s)(324) s∈TP(X\{i}) =qXTP(X\{i})(s)(325) Lemma 3.13 =qX\{i}(s)Lemma 2.11 ∈T(X\ {i}). (326) Now, we assert n≻0. Thus follows: qXn P i=s t(327) n≻0 (StS3) =qX n− P i=(i) t!enX[i7→ qX(t)]enX[i7→ qX(s)] (328) s∈TP(X\{i}) =qX n− P i=(i) t!enX[i7→ qX(t)]enX[i7→ qXTP(X\{i})(s)] (329) Lemma 3.13 =qX n− P i=(i) t!enX[i7→ qX(t)] | {z } ∈T(X) Lemma 2.7 enX[i7→ qX\{i}(s) | {z } ∈T(X\{i}) ]Lemma 2.11 ∈T(X\ {i}). (330) The combination of Lemma 3.15 and Lemma 3.17 allows for the following generalization. The corollary claims that under certain circumstances, all recursion operators over the same value in a chain of recursion operators, except for the last one, can be canceled out, which is quite a bold statement. The criteria that must be met are that all recursion-depths except the last one are nonzero, otherwise one of the recursion operators would yield its start value upon squashing, and that the variable iterated over does not occur in the start value of the last recursion operator. Example 3.18. Let T(X)be the term algebra of type {0,1,S,+},01S+ 0 0 1 2over X:={i}. qX S(S(0)) P i=i+1 S(S(S(S(0)))) P i=1 S(S(S(0))) P i=i S(S(0)) P i=1+1 i+1!=qX S(S(0)) P i=1+1 i+1!=1+1+1+1(331) qX S(S(0)) P i=i+1 S(S(S(S(0)))) P i=1 0 P i=i S(S(0)) P i=1+1 i+1!=1(332) 35
Corollary 3.19. For every recursion operator extensible term algebra T(X)over X,i∈X,k∈N and s1, . . . , sk, n1, . . . , nk, t ∈TP(X)with sk∈TP(X\ {i})and ∀j∈N<k :nj≻0, the following equation holds: qX n1 P i=s1 . . . nk P i=sk t!=qX nk P i=sk t!.(333) Proof. Let T(X)be a recursion operator extensible term algebra over X,i∈X,k∈Nand s1, . . . , sk, n1, . . . , nk, t ∈TP(X)with sk∈TP(X\ {i})and ∀j∈N<k :nj≻0. For k= 1, the claim is trivial. Now let k > 1and assume that the claim has already been proven for k−1. Because n1≻0is true, n− 1exists. Assert n− 1≻ 0. Then holds: qX n1 P i=s1 . . . nk P i=sk t!(334) =qX n1 P i=s1 n2 P i=s2 . . . nk P i=sk t!(335) n1≻0 (StS3) =qX n− 1 P i=(i) n2 P i=s2 . . . nk P i=sk t enX"i7→ qX n2 P i=s2 . . . nk P i=sk t!#enX[i7→ qX(s1)] (336) =qX n− 1 P i=(i) n2 P i=s2 . . . nk P i=sk t enX"i7→ qX nk P i=sk t!#enX[i7→ qX(s1)] (337) n− 1≻0 (StS3) =qX((i))enX"i7→ qX nk P i=sk t!#enX[i7→ qX(s1)] (338) (i)∈T(X) =qXT(X)((i))enX"i7→ qX nk P i=sk t!#enX[i7→ qX(s1)] (339) (Squ) = (i)enX"i7→ qX nk P i=sk t!#enX[i7→ qX(s1)] (340) (ApS3),(ApS1) =qX nk P i=sk t! | {z } ∈T(X\{i}) Lemma 3.17 enX[i7→ qX(s1)] (341) Lemma 2.10 =qX nk P i=sk t!. (342) Now assert n− 1≻0and assume that the claim has already been proven for n− 1 −. Thus follows: qX n1 P i=s1 . . . nk P i=sk t!(343) =qX n1 P i=s1 n2 P i=s2 . . . nk P i=sk t!(344) 36
n1≻0 (StS3) =qX n− 1 P i=(i) n2 P i=s2 . . . nk P i=sk t enX"i7→ qX n2 P i=s2 . . . nk P i=sk t!#enX[i7→ qX(s1)] (345) n− 1≻0 (StS3) =qX n− 1 − P i=(i) n2 P i=s2 . . . nk P i=sk t enX"i7→ qX n2 P i=s2 . . . nk P i=sk t!#enX[i7→ (i)] enX"i7→ qX n2 P i=s2 . . . nk P i=sk t!#enX[i7→ qX(s1)] (346) =qX nk P i=sk t!enX"i7→ qX n2 P i=s2 . . . nk P i=sk t!#enX[i7→ (i)] enX"i7→ qX n2 P i=s2 . . . nk P i=sk t!#enX[i7→ qX(s1)] (347) Lemma 2.6 =qX nk P i=sk t! | {z } ∈T(X\{i}) Lemma 3.17 enX"i7→ qX n2 P i=s2 . . . nk P i=sk t!# enX"i7→ qX n2 P i=s2 . . . nk P i=sk t!#enX[i7→ qX(s1)] (348) Lemma 2.10 =qX nk P i=sk t!enX"i7→ qX n2 P i=s2 . . . nk P i=sk t!#enX[i7→ qX(s1)] (349) Lemma 2.10 =qX nk P i=sk t!enX[i7→ qX(s1)] (350) Lemma 2.10 =qX nk P i=sk t!. (351) Due to the idempotence of squashings, it does not matter if we first squash sor tbefore applying qXto the whole term Pn i=stor not, as demonstrated in the next two lemmata. Lemma 3.20. For every recursion operator extensible term algebra T(X)over X,i∈Xand s, n, t ∈TP(X), the following equation holds: qX n P i=qX(s) t!=qXn P i=s t.(352) 37
Proof. Let T(X)be a recursion operator extensible term algebra over X,i∈Xand s, n, t ∈TP(X). Assert n≻ 0. Then holds: qX n P i=qX(s) t!(353) n≻0 (StS3) =qX(qX(s)) (354) Lemma 2.4 =qX(s)(355) n≻0 (StS3) =qXn P i=s t. (356) Now assert n≻0. Thus follows: qX n P i=qX(s) t!(357) n≻0 (StS3) =qX n− P i=(i) t!enX[i7→ qX(t)]enX[i7→ qX(qX(s))] (358) Lemma 2.4 =qX n− P i=(i) t!enX[i7→ qX(t)]enX[i7→ qX(s)] (359) n≻0 (StS3) =qXn P i=s t. (360) Lemma 3.21. For every recursion operator extensible term algebra T(X)over X,i∈Xand s, n, t ∈TP(X), the following equation holds: qXn P i=s qX(t)=qXn P i=s t.(361) Proof. Let T(X)be a recursion operator extensible term algebra over X,i∈Xand s, n, t ∈TP(X). Assert n≻ 0. Then holds: qXn P i=s qX(t)(362) n≻0 (StS3) =qX(s)(363) n≻0 (StS3) =qXn P i=s t. (364) Now assert n≻0and assume that the claim has already been proven for n−. Thus follows: qXn P i=s qX(t)(365) 38
n≻0 (StS3) =qX n− P i=(i) qX(t)!enX[i7→ qX(qX(t))]enX[i7→ qX(s)] (366) =qX n− P i=(i) t!enX[i7→ qX(qX(t))]enX[i7→ qX(s)] (367) Lemma 2.4 =qX n− P i=(i) t!enX[i7→ qX(t)]enX[i7→ qX(s)] (368) n≻0 (StS3) =qXn P i=s t. (369) 3.2.2 Equivalence classes of recursion depths, generalization to the natural numbers and resulting properties Given a term Pn i=st, we are only interested in the number of predecessors of n, not in the actual contents of n. This allows for an important generalization by defining equivalence classes that contain all terms with the same number of predecessors. We therefore first need to define the notion of the "number of predecessors", which we call the natural cardinality of a term. Definition 3.22 (Natural cardinality of a term).Let T(X)be a recursion operator extensible term algebra over Xand t∈TP(X). The natural cardinality ∥t∥≻of tis given by the following map: ∥·∥≻:TP(X)→N0 t7→ (0, t ≻ 0 ∥t−∥≻+ 1, t ≻0.(NCa) Lemma 3.23 (Well-definedness of the natural cardinality).For every recursion operator extensible term algebra T(X)over X, the natural cardinality ∥·∥≻is well-defined. Proof. Let T(X)be a recursion operator extensible term algebra over Xand t∈TP(X). Assert t≻ 0. Then holds: ∥t∥≻ (NCa) = 0 ∈N0. (370) Now assert t≻0and assume that the claim has already been proven for t−. It follows: ∥t∥≻ (NCa) =t−≻ |{z} ∈N0 +1 ∈N0. (371) Example 3.24. Let T(X)be the term algebra of type {0,1,S,+},01S+ 0 0 1 2over X:={i}. ∥0∥≻= 0 (372) ∥S(0)∥≻= 1 (373) 39
∥S(S(0))∥≻= 2 (374) ∥S(1)∥≻= 1 (375) S(S(0)) P i=1 1+1≻ = 0 (376) S(S(0)) P i=S(i) S(i)≻ = 3 (377) The next reasonable step is to define an equivalence relation based on the concept of natural cardinality. This equivalence relation, we call it the natural congruence relation, compares the natural cardinality of two terms for equality. Definition 3.25 (Natural congruence).Let T(X)be a recursion operator extensible term algebra over Xand t1, t2∈TP(X). t1≡≻t2:⇐⇒ ∥t1∥≻=∥t2∥≻(NCo) If and only if t1≡≻t2is true, we call t1and t2naturally congruent. Lemma 3.26 (Natural congruence is an equivalence relation).For every recursion operator extensible term algebra T(X)over X, the natural congruence relation ≡≻is an equivalence relation. Proof. Let T(X)be a recursion operator extensible term algebra over Xand t1, t2, t3∈TP(X). The relation ≡≻is reflexive: t1≡≻t1(378) (NCo) ⇐⇒ ∥t1∥≻=∥t1∥≻(379) ⇐⇒ ⊤, (380) symmetrical: t1≡≻t2(381) (NCo) ⇐⇒ ∥t1∥≻=∥t2∥≻(382) ⇐⇒ ∥t2∥≻=∥t1∥≻(383) (NCo) ⇐⇒ t2≡≻t1, (384) and transitive: t1≡≻t2∧t2≡≻t3(385) (NCo) ⇐⇒ ∥t1∥≻=∥t2∥≻∧ ∥t2∥≻=∥t3∥≻(386) =⇒ ∥t1∥≻=∥t3∥≻(387) (NCo) ⇐⇒ t1≡≻t3. (388) 40
Example 3.27. Let T(X)be the term algebra of type {0,1,S,+},01S+ 0 0 1 2over X:={i}. S(0)≡≻S(1)(389) S(0)≡≻S(S(0)) (390) S(S(0)) P i=S(i) S(i)≡≻S(S(S(1+1+0))) (391) S(S(S(0))) P i=1 i+1≡≻0(392) With the definition of an equivalence relation come equivalence classes. In the case of the natural congruence relation, such an equivalence class, we call it a natural congruence class, contains all terms of the same natural congruence, as desired. To simplify our work with said natural congruence classes, we pick a "simplest" representative of each class and call it the canonical representative. For the natural congruence class of terms of natural cardinality n∈N0, the canonical representative shall just be the successor operator Sapplied n-times to the zero-constant 0, very similar to Peano’s construction of the natural numbers. Definition 3.28 (Canonical representative of a natural congruence class).Let T(X)be a recursion operator extensible term algebra over Xand t∈TP(X). The canonical representative ∥t∥≻of the natural congruence class [t]≡≻is defined as follows: ∥t∥≻:=S∥t∥≻(0).(CRe) Lemma 3.29 (Well-definedness of the canonical representative of a natural congruence class).For every recursion operator extensible term algebra T(X)over Xand t∈TP(X), the canonical representative ∥t∥≻of [t]≡≻is well-defined. Proof. Let T(X)be a recursion operator extensible term algebra over Xand t∈TP(X). To prove the well-definedness of ∥t∥≻, we have to show ∥t∥≻∈[t]≡≻, i.e. ∥t∥≻≻=∥t∥≻. Let n:=∥t∥≻ and assert n= 0. Then holds: ∥n∥≻=0≻(393) (CRe) =S0(0)≻=∥0∥≻(394) 0≻0 (NCa) = 0 = n. (395) Now assert n∈N0and assume that the claim has already been proven for n. Thus follows: n+ 1≻(396) (CRe) =Sn+1(0)≻(397) =∥S(Sn(0))∥≻(398) S(Sn(0))≻0 (NCa) =∥Sn(0)∥≻+ 1 (399) (CRe) =∥n∥≻+ 1 (400) 41
Now assert n > 0and assume that the claim has already been proven for n−1. Then follows: qX n P i1=s t!(462) n>0 (StS3) =qX n−1 P i1=(i1) t!enX[i17→ qX(t)]enX[i17→ qX(s)] (463) =qX n−1 P i2=(i1) tenX[i17→ (i2)]! | {z } ∈T(X\{i2}) Lemma 3.17 enX[i17→ qX(t)]enX[i17→ qX(s)] (464) Corollary 2.16 =qX n−1 P i2=(i1) tenX[i17→ (i2)]!enX[i17→ (i2)]enX[i27→ (i1)] enX[i17→ qX(t)]enX[i17→ qX(s)] (465) Lemma 3.35 =qX n−1 P i2=(i2) tenX[i17→ (i2)] | {z } ∈TP(X\{i1}) enX[i27→ (i1)]enX[i17→ qX(t)]enX[i17→ qX(s)] (466) =qXTP(X\{i1}) n−1 P i2=(i2) tenX[i17→ (i2)]!enX[i27→ (i1)]enX[i17→ qX(t)]enX[i17→ qX(s)] (467) Lemma 3.13 =qX\{i1} n−1 P i2=(i2) tenX[i17→ (i2)]!enX[i27→ (i1)]enX[i17→ qX(t)]enX[i17→ qX(s)] (468) t∈T(X\{i2})⊂T(X) =qX\{i1} n−1 P i2=(i2) tenX[i17→ (i2)]!enX[i27→ (i1)] enX[i17→ qXT(X)(t)]enX[i17→ qX(s)] (469) (Squ) =qX\{i1} n−1 P i2=(i2) tenX[i17→ (i2)]! | {z } ∈T(X\{i1}) enX[i27→ (i1)] | {z } ∈T(X\{i2}) Lemma 2.11 enX[i17→ t]enX[i17→ qX(s)] (470) Lemma 2.17 =qX\{i1} n−1 P i2=(i2) tenX[i17→ (i2)]!enX[i27→ (i1)] enX[i17→ tenX[i17→ (i2)]]enX[i27→ qX(s)] (471) 48
Lemma 2.15 =qX\{i1} n−1 P i2=(i2) tenX[i17→ (i2)]!enX[i27→ tenX[i17→ (i2)]] | {z } ∈T(X\{i1})⊂T(X) Lemma 2.11 enX[i27→ qX(s)] (472) (Squ) =qX\{i1} n−1 P i2=(i2) tenX[i17→ (i2)]!enX[i27→ qXT(X)(tenX[i17→ (i2)])]enX[i27→ qX(s)] (473) =qX\{i1} n−1 P i2=(i2) tenX[i17→ (i2)]!enX[i27→ qX(tenX[i17→ (i2)])]enX[i27→ qX(s)] (474) Lemma 3.13 =qXTP(X\{i1}) n−1 P i2=(i2) tenX[i17→ (i2)]!enX[i27→ qX(tenX[i17→ (i2)])] enX[i27→ qX(s)] (475) =qX n−1 P i2=(i2) tenX[i17→ (i2)]!enX[i27→ qX(tenX[i17→ (i2)])]enX[i27→ qX(s)] (476) n>0 (StS3) =qX n P i2=s tenX[i17→ (i2)]!. (477) The last two theorems of this paper, Theorem 3.41 and Theorem 3.46, provide a way of simplifying nested recursion operator terms Pn i=stto a term containing just a single recursion operator by •adding the recursion depths if the nesting happens inside sor •multiplying the recursion depths if the nesting happens inside t. The commutativity of nested recursion operators then follows directly from the commutativity of addition and multiplication. We first prove a simpler version of Theorem 3.41 which considers a single nested recursion operator in the start value and later use it in the inductive step of the main theorem. Example 3.39. Let T(X)be the term algebra of type {0,1,S,+},01S+ 0 0 1 2over X:={i}. qX 3 P P2 i=1i+1 i+1 =1+1+1+1+1+1(478) qX 5 P i=1 i+1!=1+1+1+1+1+1(479) 49
Lemma 3.40. For every recursion operator extensible term algebra T(X)over X,i∈X,n1, n2∈ N0and s, t ∈TP(X), the following equation holds: qX n1 P i=Pn2 i=st t =qX n1+n2 P i=s t!.(480) Proof. Let T(X)be a recursion operator extensible term algebra over X,i∈X,n1, n2∈N0and s, t ∈TP(X). Assert n1= 0. Then holds: qX n1 P i=Pn2 i=st t (481) n1=0 (StS3) =qX n2 P i=s t!(482) n1=0 =qX n1+n2 P i=s t!. (483) Now assert n1>0. It follows: qX n1 P i=Pn2 i=st t n1>0 (StS3) =qX n1−1 P i=(i) t!enX[i7→ qX(t)]enX"i7→ qX n2 P i=s t!# | {z } =:u . (484) It is left to show the equality u=qXPn1+n2 i=st(hereinafter referred to as the subclaim). Assert n2= 0. Then holds: u(484) =qX n1−1 P i=(i) t!enX[i7→ qX(t)]enX"i7→ qX n2 P i=s t!# (485) n2=0 (StS3) =qX n1−1 P i=(i) t!enX[i7→ qX(t)]enX[i7→ qX(s)] (486) n1>0 (StS3) =qX n1 P i=s t!(487) n2=0 =qX n1+n2 P i=s t!. (488) Now assert n2>0and assume that the subclaim has already been proven for n2−1. Note that this assumption encompasses the truth of the subclaim for any s∈TP(X), in particular for (i). Thus follows: u(484) =qX n1−1 P i=(i) t!enX[i7→ qX(t)]enX"i7→ qX n2 P i=s t!# (489) 50
n2>0 (StS3) =qX n1−1 P i=(i) t!enX[i7→ qX(t)] enX"i7→ qX n2−1 P i=(i) t!enX[i7→ qX(t)]enX[i7→ qX(s)]#(490) Lemma 2.12 =qX n1−1 P i=(i) t!enX[i7→ qX(t)]enX"i7→ qX n2−1 P i=(i) t!enX[i7→ qX(t)]# enX[i7→ qX(s)] (491) Lemma 2.12 =qX n1−1 P i=(i) t!enX[i7→ qX(t)]enX"i7→ qX n2−1 P i=(i) t!#enX[i7→ qX(t)] enX[i7→ qX(s)] (492) =qX n1+n2−1 P i=(i) t!enX[i7→ qX(t)]enX[i7→ qX(s)] (493) n1+n2>0 (StS3) =qX n1+n2 P i=s t!. (494) We may now generalize to arbitrary degrees of nesting and observe that recursion operators over the same variable nested in their respective start values collapse to a single recursion operator with the sum of recursion depths as the new recursion depth. Theorem 3.41. For every recursion operator extensible term algebra T(X)over X,i∈X,k∈N, n1, . . . , nk∈N0and s, t ∈TP(X), the following equation holds: qX n1 P i=Pn2 i=... Pnk i=st ...t t =qX Pk j=1 nj P i=s t .(495) Proof. Let T(X)be a recursion operator extensible term algebra over X,i∈X,k∈N,n1, . . . , nk∈ N0and s, t ∈TP(X). For n= 1 the claim is trivial, and for n= 2 it is equivalent to Lemma 3.40. Assert n > 2and assume that the claim has already been proven for n−1. It follows: qX n1 P i=Pn2 i=... Pnk i=st ...t t (496) 51
Lemma 3.20 =qX n1 P i=qX Pn2 i=... Pnk i=st ...t t (497) =qX n1 P i=qX PPk j=2 nj i=st!t (498) Lemma 3.20 =qX n1 P i=PPk j=2 nj i=st t (499) Lemma 3.40 =qX n1+Pk j=2 nj P i=s t (500) =qX Pk j=1 nj P i=s t . (501) We conclude that all of the neat properties of sums must also apply to nested recursion operators. In particular, the nested recursion depths are commutative and we may permute them in any way. We will use symmetric groups to capture the concept of commutativity. Corollary 3.42. For every recursion operator extensible term algebra T(X)over X,i∈X,k∈N, n1, . . . , nk∈N0,s, t ∈TP(X)and π∈Sk, the following equation holds: qX n1 P i=Pn2 i=... Pnk i=st ...t t =qX nπ(1) P i=Pnπ(2) i=... Pnπ(k) i=st ...t t .(502) Proof. Let T(X)be a recursion operator extensible term algebra over X,i∈X,k∈N,n1, . . . , nk∈ N0,s, t ∈TP(X)and π∈Sk. It follows: qX n1 P i=Pn2 i=... Pnk i=st ...t t (503) Theorem 3.41 =qX Pk j=1 nj P i=s t (504) 52
=qX Pk j=1 nπ(j) P i=s t (505) Theorem 3.41 =qX nπ(1) P i=Pnπ(2) i=... Pnπ(k) i=st ...t t . (506) The next lemma provides a technical detail necessary to prove the last theorem, namely Theorem 3.46. Lemma 3.43. For every recursion operator extensible term algebra T(X)over X,i1, i2∈Xwith i1=i2,n∈N0,s∈TP(X)and t∈TP(X\ {i2}), the following equation holds: qX n P i1=(i2) t!enX[i27→ qX(s)] = qX n P i1=s t!.(507) Proof. Let T(X)be a recursion operator extensible term algebra over X,i1, i2∈Xwith i1=i2, n∈N0,s∈TP(X)and t∈TP(X\ {i2}). Assert n= 0. Then holds: qX n P i1=(i2) t!enX[i27→ qX(s)] (508) n=0 (StS3) =qX((i2))enX[i27→ qX(s)] (509) (i2)∈T(X) =qXT(X)((i2))enX[i27→ qX(s)] (510) (Squ) = (i2)enX[i27→ qX(s)] (511) (ApS3),(ApS1) =qX(s)(512) n=0 (StS3) =qX n P i1=s t!. (513) Now assert n > 0. Thus follows: qX n P i1=(i2) t!enX[i27→ qX(s)] (514) n>0 (StS3) =qX n−1 P i1=(i1) t! | {z } enX[i17→ qX(t)]enX[i17→ (i2)]enX[i27→ qX(s)] (515) (ApS3) = enX[i17→ qX(t)] : qX n−1 P i1=(i1) t! | {z } ∈T(X\{i2}) Lemma 3.17 enX[i17→ (i2)]enX[i27→ qX(s)] (516) 53
= enX[i17→ qX(t)] : TP(X\{i2}) qX n−1 P i1=(i1) t!!enX[i17→ (i2)]enX[i27→ qX(s)] (517) Lemma 2.13 = enX\{i2}[i17→ qX(t)] : qX n−1 P i1=(i1) t!!enX[i17→ (i2)]enX[i27→ qX(s)] (518) (ApS3) =qX n−1 P i1=(i1) t!enX\{i2}[i17→ qX(t)]enX[i17→ (i2)]enX[i27→ qX(s)] (519) t∈TP(X\{i2}) =qX n−1 P i1=(i1) t!enX\{i2}[i17→ qXTP(X\{i2})(t)]enX[i17→ (i2)]enX[i27→ qX(s)] (520) Lemma 3.13 =qX n−1 P i1=(i1) t!enX\{i2}[i17→ qX\{i2}(t) | {z } ∈T(X\{i2}) ] | {z } ∈T(X\{i2}) Lemma 2.7 enX[i17→ (i2)]enX[i27→ qX(s)] (521) Lemma 2.15 =qX n−1 P i1=(i1) t!enX\{i2}[i17→ qX\{i2}(t)]enX[i17→ qX(s)] (522) Lemma 3.13 =qX n−1 P i1=(i1) t!enX\{i2}[i17→ qXTP(X\{i2})(t)]enX[i17→ qX(s)] (523) =qX n−1 P i1=(i1) t!enX\{i2}[i17→ qXt)]enX[i17→ qX(s)] (524) Lemma 2.13 =qX n−1 P i1=(i1) t!enX[i17→ qXt)]X\{i2}enX[i17→ qX(s)] (525) =qX n−1 P i1=(i1) t!enX[i17→ qXt)]enX[i17→ qX(s)] (526) n>0 (StS3) =qX n P i1=s t!. (527) As of before, we first prove the statement of the main theorem for a single nested recursion operator. Example 3.44. Let T(X)be the term algebra of type {0,1,S,+},01S+ 0 0 1 2over X:= {i, j}. qX 2 P i=1 3 P j=i j+1!=1+1+1+1+1+1+1(528) qX 6 P j=1 j+1!=1+1+1+1+1+1+1(529) 54
Lemma 3.45. For every recursion operator extensible term algebra T(X)over X,i1, i2∈Xwith i1=i2,n1, n2∈N0,s∈TP(X)and t∈TP(X\ {i1}), the following equation holds: qX n1 P i1=s n2 P i2=(i1) t!=qX n1·n2 P i2=s t!.(530) Proof. Let T(X)be a recursion operator extensible term algebra over X,i1, i2∈Xwith i1=i2, n1, n2∈N0,s∈TP(X)and t∈TP(X\ {i1}). Assert n1= 0. Then holds: qX n1 P i1=s n2 P i2=(i1) t!(531) n1=0 (StS3) =qX(s)(532) 0·n2=0 (StS3) =qX 0·n2 P i2=s t!(533) n1=0 =qX n1·n2 P i2=s t!. (534) Now assert n1>0and assume that the claim has already been proven for n1−1. Thus follows: qX n1 P i1=s n2 P i2=(i1) t!(535) n1>0 (StS3) =qX n1−1 P i1=(i1) n2 P i2=(i1) t!enX"i17→ qX n2 P i2=(i1) t!#enX[i17→ qX(s)] (536) =qX (n1−1)·n2 P i2=(i1) t enX"i17→ qX n2 P i2=(i1) t!#enX[i17→ qX(s)] (537) Lemma 2.12 =qX (n1−1)·n2 P i2=(i1) t enX"i17→ qX n2 P i2=(i1) t!enX[i17→ qX(s)]#(538) Lemma 3.43 =qX (n1−1)·n2 P i2=(i1) t enX"i17→ qX n2 P i2=s t!# (539) Lemma 3.43 =qX (n1−1)·n2 P i2=Pn2 i2=st t (540) Lemma 3.40 =qX (n1−1)·n2+n2 P i2=s t (541) =qX n1·n2 P i2=s t!. (542) 55
Thus follows the general case, stating that "chained" recursion operators collapse to a single recursion operators with the product of recursion depths as the new recursion depth. Theorem 3.46. For every recursion operator extensible term algebra T(X)over X,k∈N,i1, . . . , ik ∈X, where i1, . . . , ikare distinct, n1, . . . , nk∈N0,s∈TP(X)and t∈TP(X\ {i1, . . . , ik−1}), the following equation holds: qX n1 P i1=s n2 P i2=(i1) . . . nk P ik=(ik−1) t!=qX Qk j=1 nj P ik=s t .(543) Proof. Let T(X)be a recursion operator extensible term algebra over X,k∈N,i1, . . . , ik∈X, i1, . . . , ikbe distinct, n1, . . . , nk∈N0,s∈TP(X)and t∈TP(X\ {i1, . . . , ik−1}). For n= 1, the claim is trivial, and for n= 2 it is equivalent to Lemma 3.45. Assert n > 2and assume that the claim has already been proven for n−1. It follows: qX n1 P i1=s n2 P i2=(i1) . . . nk P ik=(ik−1) t!(544) Lemma 3.21 =qX n1 P i1=s qX n2 P i2=(i1) . . . nk P ik=(ik−1) t!! (545) =qX n1 P i1=s qX Qk j=2 nj P ik=(i1) t (546) Lemma 3.21 =qX n1 P i1=s Qk j=2 nj P ik=(i1) t (547) Lemma 3.45 =qX n1·Qk j=2 nj P ik=s t (548) =qX Qk j=1 nj P ik=s t . (549) Again, the recursion depths commute. Corollary 3.47. For every recursion operator extensible term algebra T(X)over X,k∈N, i1, . . . , ik∈X, where i1, . . . , ikare distinct, n1, . . . , nk∈N0,s∈TP(X),t∈TP(X\ {i1, . . . , ik−1}) and π∈Sk, the following equation holds: qX n1 P i1=s n2 P i2=(i1) . . . nk P ik=(ik−1) t!=qX nπ(1) P i1=s nπ(2) P i2=(i1) . . . nπ(k) P ik=(ik−1) t!.(550) Proof. Let T(X)be a recursion operator extensible term algebra over X,k∈N,i1, . . . , ik∈X, i1, . . . , ikbe distinct, n1, . . . , nk∈N0,s∈TP(X),t∈TP(X\ {i1, . . . , ik−1})and π∈Sk. It follows: qX n1 P i1=s n2 P i2=(i1) . . . nk P ik=(ik−1) t!(551) 56
Theorem 3.46 =qX Qk j=1 nj P ik=s t (552) =qX Qk j=1 nπ(j) P ik=s t (553) Theorem 3.46 =qX nπ(1) P i1=s nπ(2) P i2=(i1) . . . nπ(k) P ik=(ik−1) t!. (554) Lastly, we consider a special case where all of the recursion depths are the same. The recursion depth of the collapsed recursion operator can then obviously be expressed through exponentiation. Corollary 3.48. For every recursion operator extensible term algebra T(X)over X,k∈N, i1...,ik∈X, where i1, . . . , ikare distinct, n∈N0,s∈TP(X)and t∈TP(X\ {i1, . . . , ik−1}), the following equation holds: qX n P i1=s n P i2=(i1) . . . n P ik=(ik−1) t!=qX nk P ik=s t!.(555) Proof. Let T(X)be a recursion operator extensible term algebra over X,k∈N,i1...,ik∈X, where i1, . . . , ikare distinct, n∈N0,s∈TP(X)and t∈TP(X\ {i1, . . . , ik−1}). It follows: qX n P i1=s n P i2=(i1) . . . n P ik=(ik−1) t!(556) Theorem 3.46 =qX Qk j=1 n P ik=s t (557) =qX nk P ik=s t!. (558) 4 Applications and Examples 4.1 General considerations In the following section, we are no longer interested in the actual terms themselves, but rather the values of these terms. Given a recursion operator extensible term algebra T(X)over X, an algebra Aof the same type, whose universe we call A, and an assignment φ:X→A, we can determine the value of a term t∈T(X)in Aby applying the homomorphism φ:T(X)→Ainduced by φto t, which yields φ(t). Now consider the recursion operator extension P(T(X)) and the value of a term u∈TP(X)in the same algebra A. Because P(T(X)) and Aare of different types, a homomorphism between them cannot exist, but this does not pose a problem, since we can express uuniquely as a 57