Posts

Domain types for interactions with probability monads

Image
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 worldCompile-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.
Task 2) Build upon our chosen categories som…

Composed stochastic proof : joint distribution monad as dependent type

Image
composed stochastic proofs - motivationI 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 typeWe define our strong typed stochastic computing structure in these 3 stages1) 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*IdrisAgda, Coq, Isabelle, HOL, MMTScala 3 (Dotty)Restating the WHAT:  The software types defined formally in 3 are refinements of the informal types from 1, relying on an infrastructur…

Application Authoring in RDF

In ~2014, we published an open source authoring technology called glue-ml, as part of glue.ai(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-source for query.Semantic …

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 dataB) Choosing best portfolio allocation, based on investor preferences and the estimates from AWe 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 not  m…

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 theoryInformal Survey of open satisfaction solvers and proversInfrastructure Options for typed knowledge graphsNow 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
with perfect liquid…

Infrastructure for Typed Knowledge Graphs

In this post we explore infrastructure required for our emerging synthetic field:Infrastructure for Typed Knowledge GraphsTGKT = 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 quantitative r…

Solve, Search, or Prove?

Satisfied?Declarative Mathematical ProgrammingExplicit 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 problem -…