61–70 of 73 posts
Earlier quoted context omitted.
These days, Microsoft requires model-checking proofs before accepting new device drivers. That's their secret weapon that finally got (mostly) rid of the BSOD. I suspect that Apple is also using model-checking at various layers, but I have no proof :)
and how does it work? Do they write drivers in some verifiable subset of C?
I'm not experienced/well-read in either ML or CT, but awhile ago I remember hearing Tai-Danae Bradley equate "knowing a word by the company it keeps" to the Yoneda lemma, and I always thought that was kind of interesting (although I guess I'm not qualified enough to know whether that statement is useful or vacuous)
I'm still shocked no one has developed language learning software along these lines. I had a prototype in the works for thai years ago but never got time to get it off the ground. using statistical models trained on web corpus for a language learning app seems like a no brainer.
think of it like navigating a word as a point in a graph connected to every example context it is in, with associated words being clickable into similar context bundles. then make it differential between host and target language given a translation so you can see which contexts the translation fails and succeeds in.
I have recently written a paper on understanding machine learning via the lens of Hopf algebra https://arxiv.org/abs/2302.01834 . Hopf algebras (which are really just tensors with recurrence relations built in) subsume convnets, transformers and diffusion model and also provide a theoretically better autodiff that operates within single layers as opposed to across entire graphs. Furthermore, there is a correspondence…
Your paper didn't pass my smell test at all, tbh. For example the formula you write about "product" and "coproduct" in section 3 is literally identical (as "=" is symmetric). In section 4.2 you write "the product is the standard tensor product" with a formula that doesn't at all involve the map m: A \otimes A \to A. The formula you write is the induced product on A \otimes A, assuming that you already have a product…
Earlier quoted context omitted.
I'm saying there's a difference between equal sign that defines something and equal sign that declares a relation.
Sure. In mathematics this is why we often use ":=" for definitions, or we indicate in the surrounding text that the next equation is a definition. That would be helpful. But even then, you cannot define "C" as "C \otimes C", because the right hand side only makes sense if "C" is already defined. And in math you cannot define something twice. As soon as you defined something, it stays the same in the given context.
Earlier quoted context omitted.
I'm saying there's a difference between equal sign that defines something and equal sign that declares a relation.
Sure. In mathematics this is why we often use ":=" for definitions, or we indicate in the surrounding text that the next equation is a definition. That would be helpful. But even then, you cannot define "C" as "C \otimes C", because the right hand side only makes sense if "C" is already defined. And in math you cannot define something twice. As soon as you defined something, it stays the same in the given context.
Think of it as a signature in say Rust
fn coproduct(in: C) -> (C, C)
Also you were talking about my knowledge of Hopf algebras, this is not knowledge of Hopf algebra but quibbling about things that are pretty clear from context.
Earlier quoted context omitted.
Your paper didn't pass my smell test at all, tbh. For example the formula you write about "product" and "coproduct" in section 3 is literally identical (as "=" is symmetric). In section 4.2 you write "the product is the standard tensor product" with a formula that doesn't at all involve the map m: A \otimes A \to A. The formula you write is the induced product on A \otimes A, assuming that you already have a product…
Same here. Sloppily written with very little content. If the author can't take the time to proofread his own paper why should anyone else waste their time?
You are right, it can be more polished but also it covers quite a lot and it was surprisingly hard to fit it all in.
The main response I have been getting though is "I won't believe this until I see the implementation" so I have been concentrating on that.
Earlier quoted context omitted.
Sure. In mathematics this is why we often use ":=" for definitions, or we indicate in the surrounding text that the next equation is a definition. That would be helpful. But even then, you cannot define "C" as "C \otimes C", because the right hand side only makes sense if "C" is already defined. And in math you cannot define something twice. As soon as you defined something, it stays the same in the given context.
It's a type signature, not a formula. Cs are not values. Think of it as a signature in say Rust fn coproduct(in: C) -> (C, C) Also you were talking about my knowledge of Hopf algebras, this is not knowledge of Hopf algebra but quibbling about things that are pretty clear from context.
For example, if someone works with a probability space (Ω, F, P), they would state so very clearly in their paper even though it is quite obvious from the notation that it is supposed to be a probability space.
Similarly, if someone writes "Given a symmetric monoidal category C with tensor product ⊗...", it is understandable what is going on, or at least it is understandable what I should look up. But in that paper I have no idea how I am supposed to interpret "C", "⊗" and "=" in such a way that the formulas make sense.
> It's a type signature, not a formula. C is not values.
I am not sure what distinction you are trying to draw, but surely any sequence of symbols that adheres to a given formal grammar is a (well-formed) formula; and surely if by value you mean a mathematical object, types and type signatures are values.
Earlier quoted context omitted.
It's a type signature, not a formula. Cs are not values. Think of it as a signature in say Rust fn coproduct(in: C) -> (C, C) Also you were talking about my knowledge of Hopf algebras, this is not knowledge of Hopf algebra but quibbling about things that are pretty clear from context.
I don't know what prerequisite knowledge is implied for that paper, but for someone who had to dabble in theoretical econometric and ML papers during my graduate studies it is absolutely not clear what is going on. In my experience, a paper written in such fashion where you don't even define what objects you are working with wouldn't even pass as an acceptable undergraduate paper. For example, if someone works with a…
Don't read it, it's apparently too stressful for you. You are right, I assume some knowledge but I don't know if this discourse is productive, you are too hung up on things that don't matter.
C is general. Coproduct is a general construct.
Read the Diaconis paper first, you might get what I'm getting at.
Earlier quoted context omitted.
I don't know what prerequisite knowledge is implied for that paper, but for someone who had to dabble in theoretical econometric and ML papers during my graduate studies it is absolutely not clear what is going on. In my experience, a paper written in such fashion where you don't even define what objects you are working with wouldn't even pass as an acceptable undergraduate paper. For example, if someone works with a…
> In my experience, a paper written in such fashion where you don't even define what objects you are working with wouldn't even pass as an acceptable undergraduate paper. Don't read it, it's apparently too stressful for you. You are right, I assume some knowledge but I don't know if this discourse is productive, you are too hung up on things that don't matter. C is general. Coproduct is a general construct. Read the…
category theory is 'native 2-dimensional' math. i.e. category theory explains everything in terms of graphs, where a graph is made from two different sorts of 'entities', nodes and vertices i.e. categories and morphisms this being math, I wonder to which extent can category theory be re-expressed in terms of sets. perhaps a better question is if category theory can be re-expressed (or founded on) functions? lastly, I…
Since you are concerned with sets and functions, the following analogy is helpful to build your intuition for the subject.
Dimension 0: sets
Dimension 1: functions
Dimension 2: commutative squares
Dimension 3: commutative cubes
The majority of categories, expressed in terms of structured sets and functions, never touch on the second dimension. That is the domain of 2-categories, which although they have three types of elements are nonetheless considered to be two dimensional because we count from zero. That is also where commutative squares come in to play, because as you can imagine squares are quite obviously two dimensional.
Functions are 1-dimensional lines or arrows from one place to another. Sets are more analogous to points then anything else, and so naive set theory is zero dimensional. But I think you have the wrong question. You should ask the opposite question: what if functions can be re-expressed or founded on higher dimensional category theory?