Domain types for interactions with probability monads

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 processing of probability models in functional computing environments. Probability monads overview at

Composed stochastic proof : joint distribution monad as dependent type

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

Application Authoring in RDF

In ~2014, we published an open source authoring technology called glue-ml , as part of   (Apache 2.0 license). In structural terms, essentially this technique is just  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 Protege. 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 that feels comfortable. Alternately the app impl may treat the authored RDF as a data-sour

Asset Allocation example - continued (part 02)

In our last post on Explainable Models: Asset Allocation Example , we separated our asset allocation problem into two parts: A) Estimating future asset performance and correlation, based on model assumptions and available data B) Choosing best portfolio allocation, based on investor preferences and the estimates from A We define these challenges as being entirely separate, when facilitated by our careful design of the data flowing out of estimation process A.   This clear separation provides practical benefits   to teams and systems undertaking either challenge.   We consider A to be primarily a scientific endeavor, albeit one involving some prognosticator's discretion and potential for folly.  Generally this estimation will rely in large part on commonly available data, and be comparable with  estimates provided by alternative sources.  Improvement of these estimates may be pursued in an objective manner.   Meanwhile B involves idiosyncratic decisions by investors, which are often

Explainable models : Asset Allocation example (part 01)

  Here we build on the approach outlined in the last 3 blog posts: General Background in knowledge graphs and mathematical type theory Informal Survey of open satisfaction solvers and provers Infrastructure Options for typed knowledge graphs Now we outline a practical modeling approach in an example knowledge domain:        Asset Portfolios and the Allocation Decision Problem We develop a flexible, minimalist theory for describing collections of assets, and estimated knowledge about the assets and collections. These descriptions may be aligned with FIBO ontology concepts, for commercial integration purposes.  Here we are concerned only with  abstract mathematical description sufficient to analyze portfolio allocation decisions, in the context of available knowledge about the constituent assets, and given investor objectives.    Here is a first simple problem, to motivate our thinking: Given a list of 10 available equity ticker symbols, assuming we may buy any fraction of a share w

Infrastructure for Typed Knowledge Graphs

In this post we explore infrastructure required for our emerging synthetic field: Infrastructure for Typed Knowledge Graphs TGKT = Typed Graph Knowledge Theory    is a mathematical definition space (purely functional), in which we obtain proofs as knowledge.    TGKT is an open-world compile-time artifact, used to produce closed-world runtime artifacts    deployed into TGKB below. TGKB = Typed Graph Knowledge Base    is a stateful space of applied effects, in which we reason using compiled artifacts from TGKT above.    Data  received  (effect) in TGKB serves as explicit axioms in a queryable form until purged (effect).    TGKB is closed, predicative, replacable, and equivalent at any moment to a simple set of data files.    One TGKB is always grounded in a single, permanently fixed immutable TGKT.    We derive explainable results from such a TGKB.       Complex behavior is composable as a sequence of TGKBs, based on a sequence of TGKTs. General needs  Store and present information from

Solve, Search, or Prove?

Satisfied? Declarative Mathematical Programming Explicit math models may be harnessed in current (2020)  software applications in several broad ways. Suppose we start from a paper sketch from some application domain, such as finance or planetary science. Our sketch describes some relationships, including mathematical equalities and inequalities, and objective functions to be minimized or maximized.   Any group of such relationships may be treated as a model for use in computer analysis. Our equalities, inequalities and objective functions are defined over some named terms, which are typed.   Typing of each term is fixed by our model.  One practical way to study this model is to encode these relationships in a model language for constrained optimization , such as MiniZinc.  From the MiniZinc Handbook introduction:  "MiniZinc is a language for specifying constrained optimization and decision problems over integers and real numbers. A MiniZinc model does not dictate how to solve the