![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
samples of final coalgebras
Jun. 15th, 2020 10:35 pmSo, we have a theory, or, rather a language (free theory, that is), looking e.g. like this:
<expr> :::= add(<expr>, <expr>)
<expr> := neg(<expr>)
<expr> := 1
As a functor, it is
T(A) = {1} + A + A×A, so that an algebra is T(A) -> A, consisting of i: {1} -> A, f: A->A, m: A×A->A.A free algebra for such a theory, aka "initial algebra", "least fixpoint" is the "set" of all possible expressions (that is, sentences in this language).
Or, not expressions, but their syntax trees, for some reason called "abstract" (AST).
Since Kiselyov had suggested a "biggest fixpoint", aka "final coalgebra", there is some kind of interest, how does that thing look like?
Suppose we did not have the binary operation m. Then the theory would consist of two constants and a unary operation; algebras would consist of i: {1} -> A and f: A->A. An initial algebra would be ℕ, with component-wise transitions, f0 and f1. You can find all the details in wikipedia, since we are essentially talking about the functor 1+A.
For that functor, the terminal coalgebra ("final") is ℕ~, where ℕ~ is the set of natural numbers with a point added, so that transition goes back, 1->0, 2->1, etc, while the new point, ω, remains intact. For an arbitrary coalgebra A -> T(A), consisting of a partial endomorphism f, an element x of A maps to such n that fn(x) == 1. We can call such an n a degree of x.
Now let's throw in the binary operation m: A×A->A. Initial algebra is still a set of expressions of our language. But a final coalgebra?
It is an infinite binary tree with ℕ~ at all nodes. An arbitrary coalgebra consists of two partial functions (with domains not intersecting): f': A⇸A, m': A⇸A×A. So for such a coalgebra, elements of A map to the following:
- to number n if f' is defined on x and f'n(x) == 1;
- to the pair of trees built for m'(x)∈A×A;
- to number 0 if x == 1
The story behind these coalgebras being final fixpoints goes back to the category of adjoint pairs, but that's not important.
If you see how this thing works, you can, I guess, build all kind of final coalgebras for finite free theories (aka languages). All this, I think, is covered in the chapter "Model Theory" of Johnstone.
I'll be glad if you point out that something is not clear here and needs a clarification.
fyi: "coalgebras"
Jun. 5th, 2020 08:46 pmWhat are these coalgebras, X => M[X]? They are just objects of Kleisli category CM for the monad M. Definition? Same objects, but arrows of the form X => M[X].
That's it. So, a terminal ("final", as Kiselyov says) coalgebra is just a terminal object in CM.
E.g. for the functor 1+_ (which is a monad) in Sets, the Kleisli category consists of the same objects and partial functions; and, btw, the terminal object ("final coalgebra") is (see https://en.wikipedia.org/wiki/Initial_algebra#Final_coalgebra) ℕ∪{ω} with "pred" as the partial endomorphism.
Do you need details?
Evaluation order, it's all about initial or "final" "algebras", right? That's about Eilenberg-Moore category and Kleisli category.
Which, incidentally, are initial and terminal objects in the category of adjunctions producing the same monad.
Oh my.
you will laugh but...
Nov. 1st, 2019 09:40 pm(My previous attempt to slap together a monad-looking functor were wrong.)
hey, what's a monad
May. 3rd, 2019 10:04 pmHere's what I wrote.
literary coding
Mar. 20th, 2019 04:10 pm
implicit class Optimist[T](opt: Result[T]) {
def iHope: T = opt.fold(
identity,
errors => throw new InstantiationException(errors.mkString(";")))
}
use case:
def asCat(source: Category): Cat = convert2Cat(source)(_.toString, _.toString) iHope
is not it hilarious
Feb. 18th, 2019 01:32 pmThe Giry monad was originally developed by Lawvere in 1962, prior to the recognition of the explicit relationship between monads and adjunctions. It wasn’t until 1965 that the constructions of Eilenberg-Moore, and Kleisi, showed that every adjoint pair gives rise to a monad.
Lawvere’s construction was written up as an appendix to a proposal to the International Atomic Energy Commission. At that time, Lawvere was working for a “think tank’‘ in California, and the purpose of the proposal was to provide a means for verifying compliance with limitations on nuclear weapons. In the 1980’s, Giry was collaborating with another French mathematician at that time who was also working with the French intelligence agency, and was able to obtain a copy of the appendix. Giry then developed and extended some of the ideas in the appendix.scaling java
Apr. 10th, 2017 03:09 pm
public static <T> T headOrNull(Iterable<T> ts) {
Iterator<T> it = ts.iterator();
return it.hasNext() ? it.next() : null;
}
when I hear "Kleisli monad"...
Feb. 14th, 2017 03:56 pmhere is the post I wrote
Jan. 10th, 2017 05:33 pmThat's James and Saunders bashing (in a generalized monoidal sense).
list via codensity
Jan. 8th, 2017 12:49 pm
List a = Codensity Endo a = forall r. (a -> r -> r) -> r -> r
nil :: List a
nil = \f z -> z
cons :: a -> List a -> List a
cons x xs = \f z -> f x (xs f z)
append :: List a -> List a -> List a
append xs ys = \f z -> xs f (ys f z)
foldr :: (a -> r -> r) -> r -> List a -> r
foldr f z xs = xs f z
Basically, it's like lambda.
Src: https://golem.ph.utexas.edu/category/2012/09/where_do_monads_come_from.html#c042100
critique will be appreciated
Jan. 7th, 2017 11:15 amhttps://vpatryshev.wordpress.com/2017/01/07/three-popular-fp-myths/ - part 1, "not every monad is strong"
