Outside The Rectangle

(Important:  I did not create the image shown in blogger preview - it is from NCat Lab website!) Composed stochastic proof for low-dimensional applications  Following up on previous post on Composed Stochastic Proof , we now enumerate: What the typed world owes the authored world Compile-time access to categorical knowledge about probability monads  (overview page at NCat Lab site) over our dependent type system for measure theory  (at MathLib/Lean site).   To knit this knowledge into useful, portable applications, we proceed with four major tasks: Task 1) Starting from a shared library conceptual math knowledge, we identify applicable categories that are useful in our application model.  The NCatLab website is a great current resource on existing work.  The page on monads of probability, measures, and valuations contains this  summary table of the most useful, widely known functional probability concepts. These are the core ingredient math concepts needed for robust, general proce

composed stochastic proofs - motivation I posted some background links and concepts on Reddit r/DepdendentTypes Dependent Types for Giry probability monads, e.g. Kantorovich / Wasserstein  (+ followup comment ) In this post, we begin tackling the kinds of distributions needed for our Asset Allocation Example . joint distribution monad as dependent type We define our strong typed stochastic computing structure in these 3 stages 1) Mathematically, in informal human-readable equations and type descriptions      (formally encoded and exposed as visible API in 3 below, using infra from 2) 2) As functional abstractions, using the kantorovich monad formulation      (formally encoded as submerged infrastructure, used by 3 below) 3) As a formal dependent-typed API usable from suitably strong-typed environments such as Lean, F* Idris Agda, Coq, Isabelle, HOL, MMT Scala 3 (Dotty) Restating the WHAT:  The software types defined formally in 3 are refinements of the informal types from 1, relying o

In ~2014, we published an open source authoring technology called glue-ml , as part of  glue.ai  v1.0 (used to be glue.ai, but...ask me what happened, after class -  Apache 2.0 license). In structural terms, this technique is authoring by graph:    Authors create declarative descriptive graphs, governed by ontology types. In the simplest example, an author can save a .ttl (RDF-turtle) file from a text editor, or from an RDF-aware editor such as Protege or TopBraid. Other authors may instead use spreadsheets, or a customized domain-specific editor. Semantic and logical validity of authored graphs is up to the author and tools.   Applications read the graphs as RDF using the most convenient technology. The app reading approach is independent of the authoring tool used, since only the information content of the RDF model is important. Application code knows the ontology used by authored graph, which provides the logical design contract. App impl  may use a code-binding approach, when th