I jotted a time ago a Sage snippet for options pricing in elementary calculus terms, pasted here https://pastebin.com/tTMp6fPk.
The idea is that the clean picture is done in terms of log-prices (not prices). Probability of log-prices follows a diffusion with an initial Dirac delta at-the-money. At expiration the profit function is deterministic (0 out of the money, a ramp if in the money) and the probability is certain gaussian. The expectancy of the value of a function applied to a random var of given density is like a weighted sum of the values, weighted by the frequency/density, as in a dot product (an integral here). Add to that the "time value of money" (see Investopedia) that works as linear drift, and you are done.
I'm reading Ansible for devops (imperative, isn't it) but find declarative configuration management intriguing also. On paper NixOS premise is wow, super. But some random blogging say that not so much in real life. How's adoption/hurdles, in the field?
But it's still pretty usable and EXTREMELY better than mainstream distros automated with Ansible. The real issue is that most people still do not know such systems (NixOS/Guix System) do exists and they are arguably the future.
Random blogging has been complaining about imperative approach to management for a long time as well. There's a lot of nuance in different cases, but both have their bad/good sides. Having used both a lot, I'm using nix on everything these days though. You'll have to try and experience them yourself.
My main pain point is random bash scripts you find on the internet no longer work reliably without modification. It feels like 99% of the bash scripts in the wild reference #!/bin/bash or #!/usr/bin/bash neither of which exist on NixOS. Similar story with downloaded binaries. There are plenty of workarounds. But it gets annoying. I find it works really well for servers where random downloads are less likely, but I ran into this constantly running as a workstation. steam-run will become your crutch.
The homogeneous thing is very nice. As you know it let's you pack translations and self linear maps in K^n into the linear maps of K^(n+1). OpenGL uses it. Also if your perspective is isometric (the projection of the 3D canonic base reminds a Mercedes-Benz logo) it is just linear K^3->K^2.
To add a bit, kudos to root-parent boil-down. Programmers have already the good representation, and call it n-dimensional array, that being a list of lists of lists ... (repeat n times) ... of lists of numbers. The only nuisance is that what programmers call dimension, math people call it rank. It is the sizes of those nested lists what math people call dimensions. It's all set up for a comedy of errors. Also in math the rank is split to make explicit how much of the rank-many arguments are vectors and how many are dual vectors. You'd say something like this is a rank 7 tensor, 3 times covariant (3 vector arguments) and 4 times contravariant (4 dual vector arguments) summing 7 total arguments. I'm assuming a fixed base, so root-parent map determines a number array.
In 1996 DC Keenan wrote "To dissect a mockingbird" [1] giving a graphical notation for lambda calculus, expressing it in pictures with an evocative semantics. 28 years later the linked piece gives a categorical string-diagram version. Applications arise when you are interested in mappings that have extra behavior other than that of functions, as in probabilistic programming, automatic differentiation.
Yep an elementary ("Lawvere-Tierney") topos is crafted to be just first order logic. 100% standrad FOL, as Category Theory is.
An elementary topos is a cartesian closed category, with finite limits and a subojbect classifier.
Cartesian closedness means that for objects A and B there is an exponential object A^B of functions from B to A. Cartesian closedness is the right intuition on functions being first class citizens and is at the center of the equivalence CCC-lambda calculus-functional programming. Limits are bread and butter categorical stuff, and the pesky subobject classifier is sort of a pain of what Category Theory understands as classifying things.
In Set, monos into X (inyections into X, subsets of X), determine the characteristic function of the subset, subset of say, U. The characteristic function is U->Bool={True, False}. Summing up, the subobject classifier in Set is Bool and provides the correspondence of functions U->X and X->Bool. In an arbitrary elementary topos, the subobject classifier would be an Ω such that monic arrows ?->X corresponds to arrows X->Ω. I would agree that this has bad digestion, maybe delving in applications one just grow accustomed.
There is an idea of one doing mathematics in an "ambient" set theory, and categorists want to look at that as an ambient category of sets. But then they asked, what are the miminum features I am really using of this ambient category of sets? The list is the requirements of a category to be an elementary topos. So the category of sets is a topos (the topos of sets) very by design. But other categories also do. When one changes Sets to other topos is when weird intepretations emerge. Topos requirements don't let you recover the axiom of choice, for instance. Excluded middle is not available anymore.
Ok, thank you. I think I will just have to sit down and write up what these conditions mean explicitly as axioms in my logic.
In general I feel category theory is a somewhat clumsy way of encoding higher-order things in a first-order way, but on the other hand I think the various type theories are not the right way to declumsify this. But that's just an impression, hopefully I will know more soon.
Ahh, nice one dares to proffer this. I can plug my own wondering about if one can formulate an aritmetic derivative that instantiates the Kähler differential concept (but I'm supposed not to ask unless I already knew the answer, so what'd'be the point).
