Practical Foundations of Mathematics

Paul Taylor

6.8 Exercises VI

Construct FV(t), the set of free variables of a term in a free algebra for a free theory, as an example of the conjunctive (or, rather, disjunctive) interpretation.
Any subset U Ě A has a characteristic function c_U:AŽ W (Notation 2.8.2). Suppose that U is a T-subalgebra of A and endow W with the conjunctive interpretation. Is c_U a homomorphism? What is the effect of applying the heredity operator (Definition 2.5.4) to it?
Define the additive interpretation in N of any finitary free theory in an analogous way to the conjunctive interpretation in W. Describe the free algebra F1 on one generator and the interpretation [[-]]:F1Ž N in terms of trees. Generalise to an interpretation of infinitary free theories with the class of sets as its carrier.
Explain how the set of streams in an alphabet G is the final coalgebra for T = (-)xG. Derive the final coalgebra for an infinitary free theory from Proposition 6.1.11.
Show that the functor List preserves pullbacks, and P_f preserves monos.
Show that the functor T of Definition 6.1.1 preserves directed unions iff the arities of all of the operations are finitely generable.
Prove Remark 1.6.12, that each of the rules of natural deduction for the predicate calculus preserves validity of formulae in any interpretation, in the sense defined by Example 6.1.9.
Define a function List(R+{+, -,x,¸})Ž List(R)+{*} which evaluates arithmetic expressions written in Polish notation.
Formulate and prove the Substitution Lemmas 1.1.5 and 1.1.12.
Use the List functor, head, tail, their analogues for reversed lists, and equalisers to construct the set of morphisms of the free category on a graph (Theorem 6.2.8(a)). Use append and a pullback to define composition.
Show that if the set W of operation-symbols of a finitary free theory has decidable equality then so does the initial algebra.
Let e:X\twoheadrightarrow Y. Consider the free theory with W = X+{r}, where ar[x] = Ć and ar[r] = Y. Let F be its free algebra. Consider also the algebra A = Y+(Y+1)^Y with x_A = n₀(e(x)) and \opr_A(g) = n₁(g;k) for g Î A^Y, where k = (id+!):A Ž Y+1. Show that each n₀(y) is in the smallest W- subalgebra of A, and hence so is n₁(\expx n₀). But if this lies in the ( Set-)image of the unique homomorphism p:FŽ A then e is split.
Give a direct categorical proof of Corollary 6.3.6.
Let ev:TWŽ W be the characteristic map of the subset T{T} Ě TW. Use this to show that the recursion scheme implies the induction scheme for any functor T ( cf Remark 6.3.10).
Show that if \parse_X:XŽ TX is well founded or extensional then so is T\parse_X:TXŽ T²X ( cf Exercise 3.40 and Lemma 6.3.11 ).
Show that any colimit of well founded coalgebras and homomorphisms is well founded. Discuss extensionality for filtered colimits and pushouts.
Let W Ě X be a subcoalgebra and suppose that W (but not X) is well founded. Show that it is the largest well founded subcoalgebra iff the square is a pullback: omitted diagram environment
Show that for every well founded relation (X,\prec ) there is a wff-system (for a free theory) of which it is the immediate sub-expression relation. [Hint: take tgt:(\prec )Ž X as the arity display of the theory.]
Show how to apply the General Recursion Theorem 6.3.13 to Remark 6.2.10 and Proposition 6.2.6.
Give the symbolic proofs in set theory and algebra corresponding to Proposition 6.3.9, Lemma 6.3.12 and the last part of Theorem 6.3.13, cf the comments after Lemma 6.3.11.
Follow the particular cases of the predecessor function and the Euclidean algorithm through Section 6.4.
A natural transformation s_G,A:GxT AŽ T(GxA) is called a strength for the functor T if it satisfies

s_1,A = \id_TA s_GxD,A = (\id_D xs_G,A);s_D,GxA.

Find s for the covariant powerset and for the functor which codes a free algebraic theory.
The notions of T-coalgebra and algebra with parameters in G are given by parse:GxXŽ TX and ev:GxTQŽ Q, in the presence of a strength s. Explain how the diagram on the left describes the parametric recursion scheme, in particular in the cases of the powerset and a free algebraic theory: omitted diagram environment If the category is cartesian closed show how a solution of the non-parametric recursion on the right solves the given one, cf Remark 6.1.6.
Using Corollary 6.3.6, show that if XŽ TX (doesn't depend on G and) is well founded then so is GxXŽ T( GxX). Without using cartesian closure, formulate and prove directly the parametric version of Proposition 6.3.9, and hence of the General Recursion Theorem 6.3.13.
Recursion may be parametric in another sense, namely that the argument is used in the evaluation phase. This issue itself divides into two parts, depending on whether the argument is used in parsed or unparsed form. The second case is given by the diagram on the left: omitted diagram environment By a similar method to the previous exercise, show that this is equivalent to the form on the right in a cartesian closed category, where T has a strength s. Again, formulate and prove the parametric General Recursion Theorem directly without using cartesian closure.
If the original argument is used in parsed form, the recursion scheme simplifies to omitted diagram environment Derive this from the previous case by putting Q = FxX. Conversely, reduce that one to this using \ev_X = parse^-1_X, in the case where X is the initial T-algebra (an extensional well founded coalgebra is enough, \ev_X being partial).
A unary recursion problem is one which makes at most one recursive call at each level, but where the argument may be used again after the return from the nested call. Explain how this is coded by a functor of the form T = K+Cx(-) and show how to reduce this to the diagram on the left (allowing the argument as a parameter as in Exercise 6.25): omitted diagram environment The map a:XxQŽ Q gives a homomorphism List(X)Ž [QŽ Q] of monoids. Suppose that this factors through another monoid M, which is called an accumulator. Show how to reformulate the problem as a tail recursion with functor T˘ = (-)+(NxM), as on the right.
Explain how the case M = List(X) corresponds to a stack, and how M = N suffices if a does not depend on X. The last map QxMŽ Q is itself defined by recursion over M: to what part of the execution of a recursive program does it correspond?
Express the factorial program in this form and apply the transformation, using the monoid M = (N,x). Do the same for the Fibonacci function, which is calculated using the unary recursion on N²

p(0) = (0,1) p(n+1) = (v,u+v) where (u,v) = p(n),

using the monoid of (2×2) matrices under multiplication. Hence show that p(n) = (0,1)(0 1 || 1 1)ⁿ, so by calculating (0 1 || 1 1)^{2^k} the problem can be solved in logarithmic time. What features of a recursive program must a compiler recognise in order to make use of optimisations of this kind?
Express fold and append for lists (Definition 2.7.4) using Exercise 6.26, with M = List(X), and translate these back into functional programs. What advantage, if any, do the tail- recursive programs have over the original non-tail recursion using a stack?
General recursion extends primitive recursion by use of the search or minimalisation operator m. For any partial recursive function f:GxN \rightharpoonup 2, mn.f(x,n) is the n (if any) for which f(x,n) = 1 but f(x,m) = 0 for all m < n (if any of these values is undefined then so is mn.f(x,n)). Express this as a while program, and hence as recursion over a certain coalgebra structure (GxN)\rightharpoonup (GxN)+N.
Show that (L,z,s) ş (List(X),[ ], cons) iff the diagrams omitted diagram environment are respectively a coproduct and a coequaliser, cf Example 6.4.13.
Modify the Floyd rules of Remarks 4.3.5, 5.3.2 and 5.3.9 for partial correctness, as in Remark 6.4.16ff.
Express the unification algorithm in the style of Sections 6.3-6.4.
Investigate unification in equationally free algebras that are not necessarily well founded, so that the equation x = r(x) can be solved.
Show that the unifier is the quotient by the parsing congruence, and that the congruence is the kernel of the unifier, cf Section 5.6. Allow infinitely many equations, and infinite arities.
Investigate the non-determinacy in the unification algorithm.
Apply the unification algorithm as given to Remark 6.5.4(a).
Explain why, in Definition 6.6.2(b), any coequaliser diagram k\rightrightarrows n generates a finite equivalence relation on n.
Prove the pigeonhole principle, which is that, for any function f:n+1Ž n, there are some i < j Ł n with f(i) = f(j). Deduce Bo Peep's theorem (Exercise 1.1).
Develop a Kuratowski-style unary induction scheme for finitely enumerable sets, and use it to prove the pigeonhole principle in an extensive category (Section 5.5) without assuming the existence of N, or using numbers at all.
By considering the orders of elements of its Sylow subgroups, show that there is no simple group of order 105.
Show that {*|f} (Remark 2.2.7) is finitely enumerated iff f is decidable. [Hint: exactly how many elements does it have?] Show that this also holds for finite generability.
Show that every finitely presented set is finitely enumerable.
Develop the results about Kuratowski finiteness and the finite powerset starting from the unary induction scheme in Lemma 6.6.10(b), in the style of Definition 3.8.6.
Show that the following binary Kuratowski induction scheme is equivalent to the unary one:

omitted prooftree environment
Let R:X\leftharpoondown \rightharpoonup Y be any binary relation, and suppose that U Ě X, V Ě Y are finitely generable sets which match in the sense that

ć
č "u.$v.u R v ö
ř Ů ć
č " v.$u.u R v ö
ř .

Show that U and V have matching listings, ie U = {\argu₀, ź,\argu_n-1} and V = {\argv₀,ź,\argv_n-1} with "i.\argu_i R \argv_i. Deduce the following results by taking R to be equality or an order relation.

(a)

The kernel pair of the set of elements function List (X)Ž P(X) is generated by the laws for a semilattice; use Section 5.6 to deduce that P_f(X) is the free semilattice on X.

(b)

Let (X, Ł ) be a preorder. Suppose P_f(X) also carries a preorder \sqsubseteq ( not inclusion) with respect to which Č:P_f(X)xP_f(X)Ž P_f(X) and {-}:XŽ P_f(X) are monotone. Then if U,V Ě X are finitely generable and match with respect to Ł , ie U\cvx Ł V in the notation of Exercise 3.55, then U\sqsubseteq V.
Let L be a single-sorted algebraic theory with only finitely many operation-symbols and laws, and let A be an L-algebra. Show that if the carrier of A is a finite set then A is finitely presentable as an algebra.
Let L be a single-sorted algebraic theory which is finitary in the stronger sense that it has finitely many ( ie a finitely enumerated set of) operation-symbols, each of finite arity, and finitely many laws (where, for example, the associative law counts as one law). Let A be an algebra whose carrier is Kuratowski-finite, so there is a surjection n\twoheadrightarrow A for some n. Show that there are a finitely enumerated algebra B and a surjective homomorphism B\twoheadrightarrow A. [Hint: show that n is an algebra for the operation-symbols of L but not necessarily the laws, and that the laws of L define a finite equivalence relation k\rightrightarrows n.]
Find a finitely generated monoid with no finite presentation.
(Only for those who have studied ring theory.) Using the fact that polynomial rings are Noetherian, show that every finitely generable commutative ring is finitely presentable.
Let G be a set with decidable equality equipped with a map GŽ G which has no cycles ( cf Exercise 2.47). Construct functions n:GxP_f (G)Ž G and s:P_f(G)xP_f(G)Ž P_f (G) such that n(x,U) Ď U and s(U,V) ş U+V, where the coproduct inclusions are also to be found. The functions must not depend on the order in which the elements of the finite sets are given.
Using the results of Section 2.6, show how to code w^w , w^{w^w}, etc either as special orders on N or with the arithmetical order on Q.
Describe the three product relations on axa defined in Propositions 2.6.7- 2.6.9, for each of a = w, w2 and w². If the result is not extensional, describe the extensional quotient as a binary operation axaŽ b. [Hint: one of them gives ordinal multiplication and another intersection.]
Given a Choice function c:P(Q)\ {Ć} Ž Q (Exercise 2.15), define T:P(Q)\{Ć} Ž P( Q) by T(U) = UČ{c(Q\U)} for U š Q and T(Q) = Q. Let a Ě P(Q) be the smallest set closed under T and union ( cf Proposition 3.7.11 and Exercise 3.46). Show that a is in bijection with Q, and that every non-empty subset of a has a first ( Ě -greatest) element (without using Hartogs' Lemma; this was Zermelo's proof).
Show, using excluded middle, that if a poset X has a least fixed point for every monotone endofunction s:XŽ X then X has a least element and all ordinal-indexed joins. [Hint: for ^, take s = id; for y Î X and a diagram x_(-):aŽ X consider whether { b|x_b Ł y} is a or an element of a, and in the second case use the successor.]
Show that the relation x\prec y ş (\lnot xŮy ) on W is extensional and well founded, but that the reflexive closure of this relation is sparser than Ţ unless excluded middle holds. Show that this structure has no non-trivial automorphism, and that (up to isomorphism) this is the only extensional well founded relation on W.
Let X be a set with a bijection X+X ş X. Construct a bijection HXxHX ş HX. An ordinal k is said to be a cardinal (or an initial ordinal) if it is least amongst the ordinal structures on the same underlying set. Show that Ć, H- and Č generate the class of cardinals, and hence deduce that kxk ş k for any cardinal k. Hk ş k⁺ is called its successor cardinal.
Show that any transitive extensional well founded relation is trichotomous, using proof boxes, making explicit the use of excluded middle in the form \lnot \lnot f\vdash f. [This is not easy: try Remark 2.4.10.]