Intel® End-To-End
Prophet
Amwaitam
So, now we continue with more examples of right-winged
and we will repeat an example that was presented to us by Mirjam a few weeks before Christmas.
This was free algebra of a function.
What did we look at exactly?
We had such a function on quantities and I assume that it is finite.
I need this because otherwise everything exists that I want.
The function that you look at, the example of our right-winged,
is therefore from algebra of the
right-winged to quantities. So, this one has corresponding left-winged,
this one goes in the other direction, so from Z to Altscha and what does it do on a quantity X?
So, X is quantity, which gives this free F algebra back to X.
And in the homework back then we also saw the construction,
how to construct this F X as a colimis of a chain and the proof that this is a free H algebra.
So, we have already seen this example.
Again, the concrete instance that you often look at is when you have such a polynomial function,
then the F X is the terms. I think we also added F sigma X,
which are sigma terms, but now over X. So, that means that the things are defined by such a grammar here.
So, variables in X and then sigma T1 to Tn. So, the sigma is here, so a N-like operation symbol and the X is from X.
That was this term formation, that is the free algebra over X.
Good. Then you can also say, well, I have now somehow entered the assumptions, namely that this is finite.
In general, for any H there is no such left-sided adjunct, because we had already seen that if you have an adjunct situation,
or even if you have an adjunct situation, then there is a universal case for the initial object here on the right,
or a delivery of an initial object over here. And we know cases of functions where there is no initial algebra.
For example...
...
Oh, wait a minute, did I write F algebra somewhere or is it bad? Yes, that must be called H algebra.
H is the type of function for algebra and F is this left-sided adjunct.
Yes, we used to call the type function F, but F should now be for the left-sided adjunct for free constructions.
So now such a shift has been created in the name. Yes, thanks for watching.
So, if I now look at the algebra of the power-magnet function, for example,
and their forget-function, then it has no left-sided adjunct,
because universal adjunct, so from the empty quantity, so such an eta empty quantity in U of some algebra A
and algebra structure follows from it that this is initial P algebra.
It is easy to check again that exactly that says, yes, because if I now look at this universal triangle,
I take any algebra here, then there is exactly one morphism in U of it.
Maybe here a little bit indicate, so if I had any other algebra, then I have here only one,
because the empty quantity is initial in Z and then the universal property says yes,
so here it says for all there is exactly one from A to B, so that when I use U on it, it commutes,
but overall, because this one is clearly there, does it merge together to say that for every algebra there is exactly one morphism from A to B,
so it must be initial A. And that does not exist in P algebra for cardinality reasons, this is this cantor sentence.
Okay, so that's the argument. So this kind of argument also proves that left-adjunct initial objects are preserved.
We have already seen that, but we get something better. On the task sheet there is, for example,
that right-adjunct all limits are preserved and the dual of it is that left-adjunct all co-limits are preserved,
so especially initial objects. We have now already proven one special case of this.
So, what else do we have for type 1? Well, in principle, any kind of free construction that you can imagine,
so if you now look at monoids and their forgetful function, then I get a left-adjunct F,
which depicts a lot of the free monoid over X, and that is known or not known,
Presenters
Zugänglich über
Offener Zugang
Dauer
00:33:04 Min
Aufnahmedatum
2018-01-15
Hochgeladen am
2019-04-20 10:49:02
Sprache
de-DE
Die behandelten Themen bauen auf den Stoff von Algebra des Programmierens auf und vertieft diesen.
Folgende weiterführende Themen werden behandelt:
-
Kategorie der CPOs; insbesondere freie CPOs, Einbettungen/Projektionen, Limes-Kolimes-Koinzidenz
-
Lokal stetige Funktoren und deren kanonische Fixpunkte; Lösung rekursiver Bereichsgleichungen insbesondere Modell des ungetyptes Lambda-Kalküls
-
freie Konstruktionen, universelle Pfeile und adjungierte Funktoren
-
Äquivalenzfunktoren
-
Monaden: Eilenberg-Moore und Kleisli-Kategorien; Freie Monaden; Becks Satz
-
evtl. Distributivgesetze, verallgemeinerte Potenzmengenkonstruktion und abstrakte GSOS-Regeln
-
evtl. Algebren und Monaden für Iteration
Lernziele und Kompetenzen:
Fachkompetenz Verstehen Die Studierenden erklären grundlegende Begriffe und Konzepte der Kategorientheorie und beschreiben Beispiele. Sie erklären außerdem grundlegende kategorielle Ergebnisse. Anwenden Die Studierenden wenden kategorientheoretische Konzepte und Ergebnisse an, um semantische Modelle für Programmiersprachen und Spezifikationsformalismen aufzustellen. Analysieren Die Studierenden analysieren kategorientheoretische Beweise, dieskutieren die entsprechende Argumentationen und legen diese schriftlich klar nieder. Lern- bzw. Methodenkompetenz Die Studieren lesen und verstehen Fachliteratur, die die Sprache der Kategorientheorie benutzt.
Sie sind in der Lage entsprechende mathematische Argumentationen nachzuvollziehen, zu erklären und selbst zu führen und schriftlich darzus