35 Matching Annotations
  1. Oct 2019
    1. categorical formalism should provide a much needed high level language for theory of computation, flexible enough to allow abstracting away the low level implementation details when they are irrelevant, or taking them into account when they are genuinely needed. A salient feature of the approach through monoidal categories is the formal graphical language of string diagrams, which supports visual reasoning about programs and computations. In the present paper, we provide a coalgebraic characterization of monoidal computer. It turns out that the availability of interpreters and specializers, that make a monoidal category into a monoidal computer, is equivalent with the existence of a *universal state space*, that carries a weakly final state machine for any pair of input and output types. Being able to program state machines in monoidal computers allows us to represent Turing machines, to capture their execution, count their steps, as well as, e.g., the memory cells that they use. The coalgebraic view of monoidal computer thus provides a convenient diagrammatic language for studying computability and complexity.

      monoidal (category -> computer)

  2. Sep 2019
    1. from falsehood you can derive everything ** false \leq truerestrict: don't talk about elements -> you have to talk about arrows (relations) .... interview the friends *product types: [pairs, tuples, records,...]

  3. Aug 2019
    1. But there is an alternative. It’s called denotational semantics and it’s based on math. In denotational semantics every programing construct is given its mathematical interpretation. With that, if you want to prove a property of a program, you just prove a mathematical theorem
    1. hierarchy of questions: "What about the relationships between the relationships between the relationships between the...?" This leads to infinity categories. [And a possible brain freeze.] For more, see here.)  As pie-in-the-sky as this may sound, these ideas---categories, functors, and natural transformations---lead to a treasure trove of theory that shows up almost everywhere.

      Turtles all the way up

  4. Jul 2018
    1. “pulls it back”

      minor quibble, maybe this should be surrounded by parantheses

  5. Jun 2018
    1. Exercise1.75.Doesbù3chave a right adjointR:N!N? If not, why? If so, does itsright adjoint have a right adjoint?
    2. Remark1.73.IfPandQare total orders andf:P!Qand1:Q!Pare drawn witharrows bending as in Exercise 1.72, we believe thatfis left adjoint to1iff the arrows donot cross. But we have not proved this, mainly because it is difficult to state precisely,and the total order case is not particularly general
    3. The preservation of meets and joins, and hence whether a monotone map sustainsgenerative effects, is tightly related to the concept of a Galois connection, or moregenerally an adjunction.
    4. Galois connections between posets were first considered by Évariste Galois—whodidn’t call them by that name—in the context of a connection he found between “fieldextensions” and “automorphism groups”. We will not discuss this further,
    5. In his work on generative effects, Adam restricts his attention to maps that preservemeets, even while they do not preserve joins. The preservation of meets implies that themapbehaves well when restricting to a subsystem, even if it can throw up surpriseswhen joining systems
    6. n [Ada17], Adam thinks of monotone maps as observations. A monotone map:P!Qis a phenomenon ofPas observed byQ. He defines generative effects of such a mapto be its failure to preserve joins (or more generally, for categories, its failure topreserve colimits)
    7. Example1.61.Consider the two-element setPfp;q;rgwith the discrete ordering.The setAfp;qgdoes not have a join inPbecause ifxwas a join, we would needpxandqx, and there is no such elementx.Example1.62.In any posetP, we havep_pp^pp.Example1.63.In a power set, the meet of a collection of subsets is their intersection,while the join is their union. This justifies the terminology.Example1.64.In a total order, the meet of a set is its infimum, while the join of a set isits supremum.Exercise1.65.Recall the division ordering onNfrom Example 1.29: we say thatnmifndivides perfectly intom. What is the meet of two numbers in this poset? Whatabout the join?

      These are all great examples. I htink 1.65 is gcd and lcm.

    8. These notions will have correlates in category theory, called limits and colimits,which we will discuss in the Chapter 3. For now, we want to make the definition ofgreatest lower bounds and least upper bounds, called meets and joins, precise.
    9. Ifxyandyx, we writexyand sayxandyareequivalent. We call a set with a preorder aposet.
    10. Example1.49.Recall from Example 1.36 that given a setXwe defineEXto be theset of partitions onX, and that a partition may be defined using a surjective functions:XPfor some setP.Any surjective functionf:X!Yinduces a monotone mapf:EY! EX, going“backwards”. It is defined by sending a partitions:YPto the compositef:s:XP
    11. Example1.42 (Opposite poset).Given a posetπP;∫, we may define the opposite posetπP;op∫to have the same set of elements, but withpopqif and only ifqp.
    12. Example1.40 (Product poset).Given posetsπP;∫andπQ;∫, we may define a posetstructure on the product setPQby settingπp;q∫  πp0;q0∫if and only ifpp0andqq0. We call this theproduct poset. This is a basic example of a more generalconstruction known as the product of categories
    13. Contrary to the definition we’ve chosen, the term poset frequently is used to meanpartiallyordered set, rather than preordered set. In category theory terminology, therequirement thatxyimpliesxyis known asskeletality. We thus call partiallyordered setsskeletal posets
    1. In some sense, by studying one model deeply enough, we can study them all.

      This may be where math like category theory is particularly powerful as a map between these different areas which are really the same (isomorphic).

  6. Dec 2015
    1. Lemma 2.5.1.14

      Invoke universal property of products

    2. Since ducks can both swim and fly, each duck is found twice inC, once labeled as aflyer and once labeled as a swimmer. The typesAandBare kept disjoint inC, whichjustifies the name “disjoint union.”

      The disjoint union reminds me of algebraic datatypes in functional programming languages, whereas a set-theoretic union is more like a union in CS: the union has no label associated with it, so additional computation (or errors) may arise due to a lack of ready information about elements in the union.

    3. facts, which are simply “path equivalences” in an olog. It isthe notion of path equivalences that make category theory so powerful.Apathin an olog is a head-to-tail sequence of arrows
    4. Consider the aspectpan objectqhas››››—pa weightq. At some point in history, thiswould have been considered a valid function. Now we know that the same objectwould have a different weight on the moon than it has on earth. Thus as world-views change, we often need to add more information to our olog. Even the validityofpan object on earthqhas››››—pa weightqis questionable. However to build a modelwe need to choose a level of granularity and try to stay within it, or the whole modelevaporates into the nothingness of truth!
    5. An aspect of a thingxis a way of viewing it, a particular way in whichxcan be regardedor measured. For example, a woman can be regarded as a person; hence “being a person”is an aspect of a woman. A molecule has a molecular mass (say in daltons), so “havinga molecular mass” is an aspect of a molecule. In other words, byaspectwe simply meana function. The domainAof the functionf:A—Bis the thing we are measuring, andthe codomain is the set of possible “answers” or results of the measurement.

      Naïvely (since my understanding of type theory is naïve), this seems to mesh with the concepts of inheritance for the "is" relationships, and also with type-theory more generally for "has" relationships, since I believe we can view any object or "compound type", as defined here, as being a subtype of another type 'o' if one of its elements is of type 'o'. Though we have to be careful for functional mapping when thinking of aspects: we can't just say Int is an aspect of Pair(Int, Int), since this is ambiguous (there are two ints) --- we must denote which Int we mean.

    6. We represent eachtype as a box containing asingular indefinite noun phrase.
    7. Data gathering is ubiquitous in science. Giant databases are currently being minedfor unknown patterns, but in fact there are many (many) known patterns that simplyhave not been catalogued. Consider the well-known case of medical records. A patient’smedical history is often known by various individual doctor-offices but quite inadequatelyshared between them. Sharing medical records often means faxing a hand-written noteor a filled-in house-created form between offices.
    8. As mentioned above category theory has branched out into certain areas of scienceas well. Baez and Dolan have shown its value in making sense of quantum physics, itis well established in computer science, and it has found proponents in several otherfields as well. But to my mind, we are the very beginning of its venture into scientificmethodology. Category theory was invented as a bridge and it will continue to serve inthat role.
    9. All this time, however, category theory was consistently seen by much of the mathe-matical community as ridiculously abstract. But in the 21st century it has finally cometo find healthy respect within the larger community of pure mathematics. It is the lan-guage of choice for graduate-level algebra and topology courses, and in my opinion willcontinue to establish itself as the basic framework in which mathematics is done
    10. In 1980 Joachim Lambek showed that the types and programs used in computerscience form a specific kind of category. This provided a new semantics for talking aboutprograms, allowing people to investigate how programs combine and compose to createother programs, without caring about the specifics of implementation. Eugenio Moggibrought the category theoretic notion of monads into computer science to encapsulateideas that up to that point were considered outside the realm of such theory.
    11. Bill Lawvere saw category theory as a new foundation for all mathematical thought.Mathematicians had been searching for foundations in the 19th century and were reason-ably satisfied with set theory asthe foundation. But Lawvere showed that the categoryof sets is simply a category with certain nice properties, not necessarily the center ofthe mathematical universe. He explained how whole algebraic theories can be viewedas examples of a single system. He and others went on to show that higher order logicwas beautifully captured in the setting of category theory (more specifically toposes).It is here also that Grothendieck and his school worked out major results in algebraicgeometry.

      I haven't studied toposes, but I can at least see how introductory algebraic geometry, i.e. the study of Groebner bases, relates to propositional logic.

    12. The paradigm shift brought on by Einstein’s theory of relativity brought on the real-ization that there is no single perspective from which to view the world. There is nobackground framework that we need to find; there are infinitely many different frame-works and perspectives, and the real power lies in being able to translate between them.It is in this historical context that category theory got its start.
    13. These theorems have not made theirway out into the world of science, but they are directly applicable there. Hierarchies arepartial orders, symmetries are group elements, data models are categories, agent actionsare monoid actions, local-to-global principles are sheaves, self-similarity is modeled byoperads, context can be modeled by monads.
    14. No one would dispute that vector spaces are ubiquitous.But so are hierarchies, symmetries, actions of agents on objects, data models, globalbehavior emerging as the aggregate of local behavior, self-similarity, and the effect ofmethodological context.
    15. I will use a mathematical tool calledologs, or ontology logs, to givesome structure to the kinds of ideas that are often communicated in pictures like theone on the cover. Each olog inherently offers a framework in which to record data aboutthe subject. More precisely it encompasses adatabase schema, which means a system ofinterconnected tables that are initially empty but into which data can be entered.
    16. Agreementis the good stuff in science; it’s the high fives.But it is easy to think we’re in agreement, when really we’re not. Modeling ourthoughts on heuristics and pictures may be convenient for quick travel down the road,but we’re liable to miss our turnoff at the first mile. The danger is in mistaking ourconvenient conceptualizations for what’s actually there. It is imperative that we havethe ability at any time to ground out in reality.