User:Michiexile/MATH198/Lecture 9
Recursion patterns[edit]
Meijer, Fokkinga & Patterson identified in the paper Functional programming with bananas, lenses, envelopes and barbed wire a number of generic patterns for recursive programming that they had observed, catalogued and systematized. The aim of that paper is to establish a number of rules for modifying and rewriting expressions involving these generic recursion patterns.
As it turns out, these patterns are instances of the same phenomenon we saw last lecture: where the recursion comes from specifying a different algebra, and then take a uniquely existing morphism induced by initiality (or, as we shall see, finality).
Before we go through the recursion patterns, we need to establish a few pieces of theoretical language, dualizing the Eilenberg-Moore algebra constructions from the last lecture.
Coalgebras for endofunctors[edit]
Definition If Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle P: C\to C} is an endofunctor, then a Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle P} -coalgebra on Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A} is a morphism Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle a: A\to PA} .
A morphism of coalgebras: Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f: a\to b} is some Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f: A\to B} such that the diagram
commutes.
Just as with algebras, we get a category of coalgebras. And the interesting objects here are the final coalgebras. Just as with algebras, we have
Lemma (Lambek) If Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle a: A\to PA} is a final coalgebra, it is an isomorphism.
Finally, one thing that makes us care highly about these entities: in an appropriate category (such as Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \omega-CPO} ), initial algebras and final coalgebras coincide, with the correspondence given by inverting the algebra/coalgebra morphism. In Haskell not quite true (specifically, the final coalgebra for the lists functor gives us streams...).
Onwards to recursion schemes!
We shall define a few specific morphisms we'll use repeatedly. This notation, introduced here, occurs all over the place in these corners of the literature, and are good to be aware of in general:
- If Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle a: TA\to A} is an initial algebra for Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T} , we denote Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle a = in_A} .
- If Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle a: A\to TA} is a final coalgebra for Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle T} , we denote Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle a = out_A} .
- We write Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mu f} for the fixed point operator
mu f = x where x = f x
We note that in the situation considered by MFP, inital algebras and final coalgebras coincide, and thus Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle in_A, out_A} are the pair of isomorphic maps induced by either the initial algebra- or the final coalgebra-structure.
Catamorphisms[edit]
A catamorphism is the uniquely existing morphism from an initial algebra to a different algebra. We have to define maps down to the return value type for each of the constructors of the complex data type we're recursing over, and the catamorphism will deconstruct the structure (trees, lists, ...) and do a generalized fold over the structure at hand before returning the final value.
The intuition is that for catamorphisms we start essentially structured, and dismantle the structure.
Example: the length function from last lecture. This is the catamorphism for the functor Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle P_A(X) = 1 + A\times X} given by the maps
u :: Int
u = 0
m :: (A, Int) -> Int
m (a, n) = n+1
MFP define the catamorphism by, supposing T
is initial for the functor F
:
cata :: (F a b -> b) -> T a -> b
cata phi = mu (\x -> phi . fmap x . outT)
We can reframe the example above as a catamorphism by observing that here,
data F a b = Nil | Cons a b deriving (Eq, Show)
type T a = [a]
instance Functor (F a) where
fmap _ Nil = Nil
fmap f (Cons n a) = Cons n (f a)
outT :: T a -> F a (T a)
outT [] = Nil
outT (a:as) = Cons a as
lphi :: F a Int -> Int
lphi Nil = 0
lphi (Cons a n) = n + 1
l = cata lphi
where we observe that mu
has a global definition for everything we do and out
is defined once we settle on the functor F
and its initial algebra. Thus, the definition of phi
really is the only place that the recursion data shows up.
Anamorphisms[edit]
An anamorphism is the categorical dual to the catamorphism. It is the canonical morphism from a coalgebra to the final coalgebra for that endofunctor.
Here, we start unstructured, and erect a structure, induced by the coalgebra structures involved.
Example: we can write a recursive function
first :: Int -> [Int]
first 1 = [1]
first n = n : first (n - 1)
This is an anamorphism from the coalgebra for Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle P_{\mathbb N}(X) = 1 + \mathbb N\times X} on Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \mathbb N} generated by the two maps
c 0 = Left ()
c n = Right (n, n-1)
and we observe that we can chase through the diagram
to conclude that therefore
f 0 = []
f n = n : f (n - 1)
which is exactly the recursion we wrote to begin with.
MFP define the anamorphism by a fixpoint as well, namely:
ana :: (b -> F a b) -> b -> T a
ana psi = mu (\x -> inT . fmap x . psi)
We can, again, recast our illustration above into a structural anamorphism, by:
-- Reuse mu, F, T from above
inT :: F a (T a) -> T a
inT Nil = []
inT (Cons a as) = a:as
fpsi :: Int -> F Int Int
fpsi 0 = Nil
fpsi n = Cons n (n-1)
Again, we can note that the implementation of fpsi
here is exactly the c
above, and the resulting function will - as we can verify by compiling and running - give us the same kind of reversed list of the n first integers as the first
function above would.
Hylomorphisms[edit]
The hylomorphisms capture one of the two possible compositions of anamorphisms and catamorphisms. Parametrized over an algebra Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \phi: T A\to A} and a coalgebra Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \psi: B \to T B} the hylomorphism is a recursion pattern that computes a value in Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A} from a value in Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A} by generating some sort of intermediate structure and then collapsing it again.
It is, thus the composition of the uniquely existing morphism from a coalgebra to the final coalgebra for an endofunctor, followed by the uniquely existing morphism from the initial algebra to some other algebra.
MFP define it, again, as a fix point:
hylo :: (F a b2 -> b2) -> (b1 -> F a b1) -> b1 -> b2
hylo phi psi = mu (\x -> phi . fmap x . psi)
First off, we can observe that by picking one or the other of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle in_A, out_A} as a parameter, we can recover both the anamorphisms and the catamorphisms as hylomorphisms.
As an example, we'll compute the factorial function using a hylomorphism:
phi :: F Int Int -> Int
phi Nil = 1
phi (Cons n m) = n*m
psi :: Int -> F Int Int
psi 0 = Int
psi n = Cons n (n-1)
factorial = hylo phi psi
Metamorphisms[edit]
The metamorphism is the other composition of an anamorphism with a catamorphism. It takes some structure, deconstructs it, and then reconstructs a new structure from it.
As a recursion pattern, it's kinda boring - it'll take an interesting structure, deconstruct it into a scalar value, and then reconstruct some structure from that scalar. As such, it won't even capture the richness of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle hom(F x, G y)} , since any morphism expressed as a metamorphism will factor through a map Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x\to y} .
Paramorphisms[edit]
Paramorphisms were discussed in the MFP paper as a way to extend the catamorphisms so that the operating function can access its arguments in computation as well as in recursion. We gave the factorial above as a hylomorphism instead of a catamorphism precisely because no simple enough catamorphic structure exists.
Apomorphisms[edit]
The apomorphism is the dual of the paramorphism - it does with retention of values along the way what anamorphisms do compared to catamorphisms.
Further reading[edit]
- Erik Meijer, Maarten Fokkinga, Ross Paterson: Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire [1]
- L. Augusteijn: Sorting morphisms [2]
Further properties of adjunctions[edit]
RAPL[edit]
Proposition If Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle F} is a right adjoint, thus if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle F} has a left adjoint, then Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle F} preserves limits in the sense that Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle F(\lim_{\leftarrow} A_i) = \lim_{\leftarrow} F(A_i)} .
Example: Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (\lim_{\leftarrow_i} A_i)\times X = \lim_{\leftarrow_i} A_i\times X} .
We can use this to prove that things cannot be adjoints - since all right adjoints preserve limits, if a functor Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle G} doesn't preserve limits, then it doesn't have a left adjoint.
Similarly, and dually, left adjoints preserve colimits. Thus if a functor doesn't preserve colimits, it cannot be a left adjoint, thus cannot have a right adjoint.
The proof of these statements build on the Yoneda lemma:
Lemma If Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle C} is a locally small category (i.e. all hom-sets are sets). Then for any Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle c\in C_0} and any functor Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle F: C^{op}\to Sets} there is an isomorphism
- Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle hom_{hom_{Sets^{C^{op}}}}(yC, F) = FC}
where we define Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle yC = d\mapsto hom_C(d,c) : C^{op}\to Sets} .
The Yoneda lemma has one important corollary:
Corollary If Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle yA = yB} then Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A = B} .
Which, in turn has a number of important corollaries:
Corollary Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (A^B)^C = A^{B\times C}}
Corollary Adjoints are unique up to isomorphism - in particular, if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle F: C\to D} is a functor with right adjoints Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle U, V: D\to C} , then Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle U = V} .
Proof Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle hom_C(C, UD) = hom_D(FC, D) = hom_C(C, VD)} , and thus by the corollary to the Yoneda lemma, Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle UD = VD} , natural in Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle D} .
Functors that are adjoints[edit]
- The functor Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle X\mapsto X\times A} has right adjoint Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Y\mapsto Y^A} . The universal mapping property of the exponentials follows from the adjointness property.
- The functor Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \Delta: C\to C\times C, c\mapsto (c,c)} has a left adjoint given by the coproduct Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (X,Y)\mapsto X + Y} and right adjoint the product Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (X,Y)\mapsto X\times Y} .
- More generally, the functor Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle C\to C^J} that takes Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle c} to the constant functor Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle const_c(j) = c, const_c(f) = 1_c} has left andright adjoints given by colimits and limits:
- Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle \lim_\rightarrow -| \Delta -| \lim_\leftarrow}
- Pointed rings are pairs Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle (R, r\in R)} of rings and one element singled out for attention. Homomorphisms of pointed rings need to take the distinguished point to the distinguished point. There is an obvious forgetful functor Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle U: Rings_* \to Rings} , and this has a left adjoint - a free ring functor that adjoins a new indeterminate Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle R\mapsto (R[x], x)} . This gives a formal definition of what we mean by formal polynomial expressions et.c.
- Given sets Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A, B} , we can consider the powersets Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle P(A), P(B)} containing, as elements, all subsets of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A, B} respectively. Suppose Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f:A\to B} is a function, then Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f^{-1}: P(B)\to P(A)} takes subsets of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle B} to subsets of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle A} .
- Viewing Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle P(A)} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle P(B)} as partially ordered sets by the inclusion operations, and then as categories induced by the partial order, Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f^{-1}} turns into a functor between partial orders. And it turns out Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f^{-1}} has a left adjoint given by the operation Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle im(f)} taking a subset to the set of images under the function Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f} . And it has a right adjoint Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f_*(U) = \{b\in B: f^{-1}(b)\subseteq U\}}
- We can introduce a categorical structure to logic. We let Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle L} be a formal language, say of predicate logic. Then for any list Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x = x_1, x_2, ..., x_n} of variables, we have a preorder Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Form(x)} of formulas with no free variables not occuring in Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} . The preorder on Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle Form(x)} comes from the entailment operation - Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f |- g} if in every interpretation of the language, Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f \Rightarrow g} .
- We can build an operation on these preorders - a functor on the underlying categories - by adjoining a single new variable: Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle *: Form(x) \to Form(x, y)} , sending each form to itself. Obviously, if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f |- g} with Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle x} the source of free variables, if we introduce a new allowable free variable, but don't actually change the formulas, the entailment stays the same.
- It turns out that there is a right adjoint to Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle *} given by Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f\mapsto \forall y. f} . And a left adjoint to Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle *} given by Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle f\mapsto \exists y. f} . Adjointness properties give us classical deduction rules from logic.
Homework[edit]
- Write a fold for the data type
data T a = L a | B a a | C a a a
and demonstrate how this can be written as a catamorphism by giving the algebra it maps to. - Write the fibonacci function as a hylomorphism.
- Write the Towers of Hanoi as a hylomorphism. You'll probably want to use binary trees as the intermediate data structure.
- Write a prime numbers generator as an anamorphism.
- * The integers have a partial order induced by the divisibility relation. We can thus take any integer and arrange all its divisors in a tree by having an edge Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle n \to d} if Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle d|n} and Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle d} doesn't divide any other divisor of Failed to parse (SVG (MathML can be enabled via browser plugin): Invalid response ("Math extension cannot connect to Restbase.") from server "https://wikimedia.org/api/rest_v1/":): {\displaystyle n} . Write an anamorphic function that will generate this tree for a given starting integer. Demonstrate how this function is an anamorphism by giving the algebra it maps from.
- Hint: You will be helped by having a function to generate a list of all primes. One suggestion is:
primes :: [Integer]
primes = sieve [2..]
where
sieve (p:xs) = p : sieve [x|x <- xs, x `mod` p > 0]
- Hint: A good data structure to use is; with expected output of running the algorithm:
data Tree = Leaf Integer | Node Integer [Tree]
divisionTree 60 =
Node 60 [
Node 30 [
Node 15 [
Leaf 5,
Leaf 3],
Node 10 [
Leaf 5,
Leaf 2],
Node 6 [
Leaf 3,
Leaf 2]],
Node 20 [
Node 10 [
Leaf 5,
Leaf 2],
Node 4 [
Leaf 2]],
Node 12 [
Node 6 [
Leaf 3,
Leaf 2],
Node 4 [
Leaf 2]]]