Posts

Laurie Wired on Richard Gabriel's 35-year-old essay "Worse Is Better"

Image
It sounds like Richard Gabriel is the inventor of the term Software Architecture . See his 1996 book  Patterns of Software . See  https://dreamsongs.com/ . In answer to her question at the end: I think the best thing is to make stuff better and better. So for example, I think it would be nice if Lean's Mathlib one day proved the Generalised Stokes Theorem on differential manifolds and derived the proofs of the Fundamental Theorem of Calculus from that. At the same time, it would be nice if people could work on teaching the basic ideas of simplicial forms and cohomology to high school students so they could understand the Generalised Stokes Theorem in simplicial complexes before they were taught how to do epsilon-delta proofs of calculus on the real line. In computer science, the equivalent process is one where, instead of designing new languages like C++ and Lean and producing a never-ending stream of concrete implementations that are all different, people specified the lang...

Mike Titelbaum and Ted Theodosopoulos - Topological Obstacles to Shared Priors

Image
From the video description : Given a finite collection of probability measures defined on subsets of a measurable space, how can we determine if they are compatible, in the sense that they can be realized as conditional distributions of a single probability measure on the full space? This formulation of the consistency problem for conditional probabilities is significant in Bayesian epistemology and probabilistic reasoning, as it describes the conditions under which a collection of agents can reach agreement by sharing information. We derive a necessary and sufficient condition under which joint compatibility is equivalent to pairwise compatibility. This condition is stated in terms of the cohomology of a simplicial complex constructed from the given probability measures, exposing a novel application of algebraic topology to Bayesian reasoning. See also  Aumann's Agreement Theorem is Fifty Years Old . Subscribe to  Relatorium .  I had a strange dream this morning. I had l...

Spiritually Depraved and Misery Inducing Landscapes of North America Episode IV

Image
With a guest host in North Carolina,... See  Spiritually Depraved, Misery Inducing Landscapes of North America Episode III .  Subscribe to Crime Pays but Botany Doesn't . 

Terence Tao Formalising Riemann-Stieltjes Integrals in Lean Mathlib

Image
6:03 In Mathlib they try to formalise theories at the highest level of abstraction they can to avoid having to prove the same theorems many times for specific instantiations.  So for example, they use a general multi-dimensional integration theory of box-additive measures in  Mathlib.Analysis.BoxIntegral.Basic : In this file we define the integral of a function over a box in ℝⁿ. The same definition works for Riemann, Henstock-Kurzweil, and McShane integrals. As usual, we represent ℝⁿ as the type of functions ι → ℝ for some finite type ι. A rectangular box (l, u] in ℝⁿ is defined to be the set {x : ι → ℝ | ∀ i, l i < x i ∧ x i ≤ u i}, see BoxIntegral.Box . Let vol be a box-additive function on boxes in ℝⁿ with codomain E →L[ℝ] F. Given a function f : ℝⁿ → E, a box I and a tagged partition π of this box, the integral sum of f over π with respect to the volume vol is the sum of vol J (f (π.tag J)) over all boxes of π. Here π.tag J is the point (tag) in ℝⁿ associated with the ...

Sci-Fi Short - Bisected

Image
See  https://dannypineros.com/  This is going to be something amazing!  Subscribe to  Dust  and  Daniel Piñeros . 

Kathryn Hess - Comonads to Calculus

Image
See  Wiesław Kubiś - Generic Mathematical Structures .  55:12 Wouldn't it be great if you could cook up a comonad that gives a tower of categories that sum to differential calculus on a real vector space? See below .  Subscribe to  Topos Institute .  What is a comonad on a category? It's just a monad on the opposite category:  ... "Set theory is linear coalgebra on vector spaces":  Subscribe to  Sheafification of G .  But they have to make everything much more complicated: We discuss differentiable smoothness structures on 𝑹⁴ from three different categorical perspectives. The first one relies on considering open atlases on 𝑹⁴ with certain (not all) of its local charts residing in a smooth topos. Thus exotic smooth functions on 𝑹⁴ are finelly approached without any use of Casson handles and handle decompositions. The second approach takes into account entire space of all smoothness structures on 𝑹⁴ . Forcing extensions naturally order the...

Wiesław Kubiś - Generic Mathematical Structures

Image
See the video description : A mathematical object can be called “generic” if it appears, up to isomorphism, with probability one as the result of a natural stochastic process. Instead of [using] probability, one may [give] its topological counterpart, using the Baire category theorem . Yet another option is using a natural infinite game for two players, declaring an object U ”generic” if one of the players has a suitable winning strategy leading to the isomorphic copy of U.... ... The story of generic mathematical structures goes back to Cantor, who was the first to identify the set of rational numbers as the generic countable linearly ordered set. About half a century later, Fraïssé developed an abstract theory of universal homogeneous structures (nowadays called ”Fraïssé limits”) which until recent years was viewed as a part of model theory. As it happens, Fraïssé limits are particular cases of generic mathematical objects which can be found in several branches of mathematics, starti...

Elle Cordoba - A Grammatical Murder Mystery

Image
Subscribe to Elle Cordoba . 

Assumptions of Physics - From Classical Mechanics to Field Theory

Image
13:13 How do you define volume in an infinite dimensional phase space on a finite whiteboard ?  1:05:39 I enjoyed listening to this discussion. Thanks to everyone who took part.  I was thinking about causal sets as modeling those second countable collections of empirically verifiable statements. That may not be how Sorkin sees it though! See  Geometry from order: causal sets .  Subscribe to  Assumptions of Physics .  See also this discussion with Urs Schreiber on Gauge fields and configuration spaces at 44:33 . The earlier discussion he referred to on differential geometry and compact spaces is at 17:05 . He's saying that you do not want to restrict physics to describing only compact spaces. But you do want to restrict observations to compact spaces. At 26:03 you can get a coherent notion of field configuration spaces in a topos. 35:10 Lawvere started out in physics, but then he asked "What is a vector space, really?" and within a decade wrote a paper...