You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
This is just a small humble project where I began to sketch my ideas for formalizing a particular phenomenon. For me it is good practice as I continue to learn more about categorical modeling. I’ll just share it here in case someone wants to give me some feedback on it. I only just started, and I know it’s not very good, but I’ll be working on it. Thanks.
This is cool, I think I would engage with the existing literature on mathematical finance and build off of it. IMO it's a difficult task to say anything really new and interesting about a subject before having a working understanding of what has already been established in that area.
By the way it's possible you may have misunderstood what "derivative" referred to in this context. I think a derivative in finance is a bit closer to, say, when someone says "Boy that movie was really derivative" - it means that it follows or mimics something else that exists. A financial derivative is a security that you can buy or sell, whose value is determined by the price of another security or a commodity. For example, I could buy a future contract on nickel, whose price is determined by (derived from) the price of nickel in six months. Or I could buy put options on Apple stock, which are a kind of insurance policy against Apple stock dropping in price, this gives a certain payout if Apple stock falls to a certain price. In this sense, a put option is a derivative of Apple stock, its value is derived from the price of Apple stock.
Julius Hamilton said:
This is just a small humble project where I began to sketch my ideas for formalizing a particular phenomenon. For me it is good practice as I continue to learn more about categorical modeling. I’ll just share it here in case someone wants to give me some feedback on it. I only just started, and I know it’s not very good, but I’ll be working on it. Thanks.
This is a great starting point! I agree with Patrick's suggestion to explore existing literature. Blockchain technology, in particular, presents several open questions and areas needing research for formalization. For inspiration, you might consider reviewing work like Axiomatization of Blockchain Theory.
Additionally, @Chad Nester has explored formalizing ledger logic, which could be another potential direction for your project. Check out A Foundation for Ledger Structures for more insights.
Any effort in formalizing financial structures related to blockchain is worthwhile as we move towards needing robust methods to ensure transaction accuracy. This will be especially pertinent when Ethereum integrates fully homomorphic encryption, where all information will be encrypted. Consequently, blockchain operations will rely heavily on logical processes rather than plaintext equality checks, given that the data will be encrypted.
(Tangent: Note sure what exactly you mean re FHE @Rémy Tuyéras, do you expect smart contracts or just the off-chain portions of dApps to use FHE?
I don't think you're saying this but I would not hold my breath on "FHE Aave" etc. taking over any time soon, although its very cool to think about. Centralized businesses or short-term swaps on DEXes can almost always use hash-commitments + time-locks instead of FHE, and truly-decentralized protocols using ZKPs or strong-encryption on financial flows directly run a very real and serious risk of just getting blacklisted by various governments (= devs could go to prison) as soon as Lazarus group et al. starts to move money through their protocol... Very cool tech, but lots of nasty roadblocks to adoption.)
Thanks for sharing your insights, @Eric M Downes . I really appreciate hearing more opinions on this topic. However, I won’t go too much into the potential future directions of FHE, as that would be more speculative than informed. I will keep your feedback in mind until we see more advances in this area. :blush:
I do want to address the blacklisting aspect, though. Encryption is indeed a trade-off. While ransomware uses encryption, so do government intelligence agencies. Interestingly, governments are very invested in developing FHE. Here are a few links you might find interesting:
Eric M Downes said:
Tangent: Note sure what exactly you mean re FHE Rémy Tuyéras, do you expect smart contracts or just the off-chain portions of dApps to use FHE?
Any data that needs to stay private (imagine a memory dump attack) but must also be used in a computation
Rémy Tuyéras said:
Any data that needs to stay private (imagine a memory dump attack) but must also be used in a computation
Totally.
This is a different topic, but I just want to point out that "plain ol" one-operation additive homomorphic encryption (like Pallier cryptosystem), can be used for many computations much more cheaply. Like, if you need to keep individual data private, but want the average to be public you don't need Ring or Field FHE: you keep track of the sum of data and the sum of "total number" separately. Then you divide the two upon decryption, without fear of leaking privacy, so long as is large. If you log or transform on both sides you can do geometric and harmonic means as well. We use this in our patent for trading on the quality of carbon-emissions or carbon-capture data. (We still had a helluva time attracting VCs or business partners! So yeah, very bullish on homomorphic encryption technology-wise, but want folks to be careful and remember the lessons of VHS vs Betamax!)
One of my friends showed me the electricity bill for an FHE database they are building... its frankly insane, and you can still only run certain very specific queries... So imagining the gas costs to convince a validator to include that in a proposed block... not yet, I'm afraid! But maybe the first additively homomorphic AMM could work, electricity-cost-wise? We shall see!
Okay, I promise I'll open another topic if there are more replies on this. :)
Eric M Downes said:
my friends showed me the electricity bill for an FHE database they are building... its frankly insane, and you can still only run certain very specific queries... So imagining the gas costs to convince a validator to include that in a proposed block... not yet, I'm afraid! But maybe the first additively homomorphic AMM could work, electricity-cost-wise? We shall see!
:rolling_on_the_floor_laughing: wait for openai/microsoft/google to develop the necessary nuclear-energy-based infrastructures for alimenting their LLM technologies, and VCs will probably be less suspicious at these proposals... :thinking:
In case anyone has any ideas on this:
There is work on formalizing ologs which I haven’t studied yet.
I think that a challenge in writing ologs is that while the mathematics (i.e., category theory) may be well-developed, the way you represent a real-world phenomenon in a formal structure may not have cut-and-dry rules.
Consider the most basic guidelines that in an olog, the objects of a category “represent things”, and the morphisms represent “relationships between things”.
I can say, “Well, Bitcoin is a ‘thing’. So I’ll make an object labeled ‘Bitcoin’ in my olog.”
In my experience, as you try to make the olog more detailed, you run into more nuanced questions than you realized at first.
Semantically, I think of ‘Bitcoin’ as a “general noun”, similar to “time”. I think the mind can hold representations of general concepts, in a way that differs from the representations it holds for specific things, like “dogs”. Someone might argue the only difference here is countability vs. uncountability. That conjecture might be insightful, or it might be over-simplifying. I’m not sure yet.
I think that Spivak provides the guideline that in an olog, the (categorical) objects should be labeled by nouns with an indefinite article, “a/an”. I wonder, what does this imply? It sounds like an object in an olog does not represent a specific thing, like “dog ”. Instead, it represents a dog in general. This reminds me of the concept of “generalized elements” in category theory. Set-theoretically, the idea of “some dog, any dog - but a dog” can be represented as . If Spivak suggests labeling objects with an indefinite article, does this imply that, to him, the proper formalism for ologs is to think of (categorical) objects, technically, as sets of real-world things?
I think that one can view any set as being a collection of things sharing a property. In the case of “the set of all dogs”, what the elements of the set have in common is not just obvious, but it is a property that determines “identity”, in a way. I think we feel we have a class of things, or a type of things. In contrast, a set of things that “have red somewhere on them” (a ladybug, the American flag, a person bleeding) share a property, but I think at least to the human mind, they don’t feel like a class of the same type of thing. And in the most trivial case, a set of very disparate things can still be said to be “the set of things in that set”. Sometimes, I think saying this does not feel arbitrary, but can actually be useful information. I think these thoughts can prove useful in deciding what rules we use in writing ologs.
I considered yesterday that I was going to go forward with the assumption that objects are sets of things “sharing a property”, because I think it is a simple way to provide more structure to the olog, and because while I think alternatives are possible, I need more time to think about what they are.
If an object is not a set of things, but just “a specific thing”, I think making an olog-type structure is still possible, but it becomes clear once you start drawing arrows that there is an implicit internal structure to the object that needs to be worked out, first.
Reference:
Julius Hamilton said:
I think that Spivak provides the guideline that in an olog, the (categorical) objects should be labeled by nouns with an indefinite article, “a/an”. I wonder, what does this imply? It sounds like an object in an olog does not represent a specific thing, like “dog ”. Instead, it represents a dog in general. This reminds me of the concept of “generalized elements” in category theory. Set-theoretically, the idea of “some dog, any dog - but a dog” can be represented as . If Spivak suggests labeling objects with an indefinite article, does this imply that, to him, the proper formalism for ologs is to think of (categorical) objects, technically, as sets of real-world things?
If you look at https://arxiv.org/pdf/1706.00526 in section 6.1 (and below), you will see specific examples of how ologs can be used, namely they are used as the domains of functors going to (or sometimes ).
Section 6.1 also shows how ologs can intuitively be seen as the collection of attributes for a database (i.e. the names of the columns in your database) while the images of your functor give you, for every english concept/attribute , the collection of elements /datapoints registered as being of type .
For example, if you take , then:
Then, depending on the model (whether you decided to take a functor going to or ), a table in your database is
If you translate all this to model theory for set theory, your olog defines a theory and the functors define the models for that theory. If your olog has limits (has shown in your pdf), then your models should also preserve those limits
This was the initial reason why I linked the paper on the Axiomatization of Blockchain Theory, I thought you could potentially have fun turning their theory into an olog?
Thanks. I think I can and will. However, I want to try to develop a theory on my own for this before I turn to any reading material.
This is the “refreshed” presentation of my first draft (above).
The next question I will contemplate is if I should model this in a category or bicategory of relations, rather than the category of sets. The reason why is that since functions are defined as sets in set theory, it occurs to me that I should work in an environment in which there is less of a distinction between sets and functions. I’ll show what I mean in a moment.
@Rémy Tuyéras I find your message and also Patterson’s paper really helpful in this, I’m excited to absorb them more fully, when I’m ready.
I’m going to take a break now, but the thought in my mind right now is this.
In my above screenshot, I say I want to bring in time as a factor in the model.
I am picturing an object, , which, as I say, is isomorphic to the real numbers. Or, perhaps we can represent time as the real numbers themselves, with arrows to or from that object to other objects, to represent how time “indexes” things.
I wonder how I should represent “ownership at time ” in my model. I have seen Spivak include variables within the objects’, and I think the arrows’, names. So for example, he might write, “people ->(own at time ) asset”.
I think I want to avoid this, because it makes the conventions of the model more complicated before I have a good grasp over a simpler version. I don’t think I have an adequate definition of what it “means”, mathematically, to have a variable inside an object or arrow name. In my screenshot, I think I tried to convey that the names of the objects and arrows are just text labels for sets. I think this means that I have not provided a sufficient framework to allow “mathematics inside the names” of the objects.
So I think I will avoid variables in text labels. I think this will be pretty easy. I think any label which would have a variable in it can be converted so that that variable is an element of an object. I think any object which would have multiple variables can be expressed as the categorical product of distinct objects, as I explored in my PDF.
I wonder what the implications of that I think my category needs products are.
Let’s consider that the function is I think “logically false”. I wonder if we could use model theory to show more clearly that the statement “ owns asset ” is I think “decidable” only if we interpret it as having a time.
I think the function requires a subset of the real numbers as an argument. I think that subset can be any kind of subset, such as a collection of I think “discrete” points, I think open or closed intervals, etc.
Now I’ll see if I can update what the diagram looks like.
@Julius Hamilton If the power set is really the type of object you want, then I would recommend to map your models to a category of monoids. The reason for this is that the power set is the free commutative idempotent monoid over . In this world, the elements of your database are expressed as sums of the form:
Similarly, monoids allow you to consider unions of people such that you can now assess their joint assets. However, commutative idempotent monoids also require that every element is idempotent, meaning that:
While this may seem an oddity at first, it could actually be quite relevant for modeling ledgers, as explained in Section 2.2 of the paper I linked earlier (see the idempotent relations that are mentioned in Section 2.2).
image
So, if you take the category of idempotent commutative monoids , then your olog is essentially this:
And your models for this olog are given by morphisms of the following form in :
where contains people and their sums, and contains assets and their sums. These -morphisms will be linear maps with associations of the following form:
And if we also have:
then we have:
And if you want a time variable added to your models, then I would feel like a natural category to send your models to is now the functor category
where is the category made of intervals (with ) and inclusions between intervals. The interval represent what happens from time to time .
This means that your olog arrow:
will be modeled, for every interval in , by a morphism in as follows:
That looks really awesome, I am going to work up to that, but I have to get there through my own process of questioning and understanding.
I think I can identify a question which would help me move forward.
I think the following question may be related to ‘constructive mathematics’, or ‘coproducts’.
I think that in many or all abstract categories, a person can state that for a given diagram, all products exist. I mean that I think nothing is stopping them from adding this as I think an “axiom”.
However, I think my olog is not an abstract category. I think I defined the objects as sets, so I think the categorical structure of the sets and functions between them is an a posteriori truth. I think this means that I should not declare that products exist, but that I have to show how to construct them.
I think the categorical product of two objects is defined as an object which has a certain well-known universal property, expressible in a certain well-known diagram. I think John Baez once explained to me that the product of two objects is not a uniquely determined object, but that it does uniquely determine a class of isomorphic objects.
I think an example of that there can be multiple objects exhibiting the universal property of products is that for sets , , and , where is the Cartesian product, , but . As an aside, I wonder if there is a way related to this to express “a relation between three elements” where the order does not matter. I think a set expresses this, but I wonder if the set of product objects of two objects has useful properties or “expresses” a useful idea related to this.
This leads me to the following. In order to express “a person owns an asset at a time”, I think I should use a construction which “bundles together” the objects , , and , to show which person owns which asset at which time. However, I think that the order of the elements in these triples should not matter. I think the information is “essentially” captured by associating a person, asset, and time to each other. But I think the convention in set theory is for functions and relations to be defined as ordered pairs.
I am also thinking about how I think functions are defined as sets (total, well-defined relations, where relations are subsets of products, and I think products use power sets in their set-theoretic, “Kuratowski” definition). Therefore, if I want to “capture” the information of who owns what asset and when, I wonder why I should represent that as an object or as an arrow, in my categorical model, because I think that every arrow in the category of sets is also an object in the category of sets. This makes me think about what the implications are of that I think that all the information in the category of sets is already expressed in the I think “proper class” of all sets; as if we do not need the structure of a category in the first place.
In case it is not clear, these questions are supporting questions for my central question of what interesting alternatives there are to “encoding” relations in terms of products, which I think are sets of ordered pairs. It also occurs to me that for a categorical product, I think we have two projection arrows out of the product into and . Intuitively, I think it would feel more like a “construction” if we chose the dual of the product, the coproduct, which I think has two inclusion maps into from and . I think this feels more like a “construction”, because we are saying, “if you have and , you can make ”, but with the product, it feels like saying, “If you have , I’ll show you how to ‘get’ or ”; but I think this does not work if we don’t know if we have yet. It reminds me of an exercise in Mike Shulman’s intro to categorical logic textbook, in which I think you have to prove that in a category with products, monoid objects are bimonoids. I think this is due to a “diagonal map”. I am wondering if this could be related to proving that products are constructible, in the setting of my olog.
Thanks!
As you said, I think it is important that you explore various architectures for your ologs, just to go through the process and develop a feel for it. Maybe one piece of advice from me would be to design your ologs such that your maps generally decompose information.
For example, I would probably have used (maybe giving the middle time of the interval) as opposed to . The reason for this is to allow you to use logical propositions of the form:
Take X, which has A, B and C, such that ...
Here, you obtain A, B and C, by using mappings , and . For example, a given middle time can have many intervals, but one interval has a single canonical middle time.