recent work in math knowledge rep 2021Q3

 

2021-Q3 survey of recent work in math knowledge rep

Background definitions and motives

Some surveys 

Some proceedings

Some libraries and datasets

Some nascent languages

Some online tools

Popular posts from this blog

Streaming analytics in Scala using ZIO and Apache DataSketches (part 1)

Image
First let's look at a trivial example of streaming analytics using ZIO Streams 2.0.9 (on Scala 2.13). https://scastie.scala-lang.org/6AHfPh02S6m0k7aN6bkacA When run, this Scastie just averages some random numbers (gaussian) in a single input stream.  That code is in the trait AvgFun . But we also see a trait called ParAvgFun with the code for rather painless parallel  implementation, using ZIO chunks, via ZStream's  grouped , zipWithIndex , and groupByKey .  Across these two traits, the clean reusability of ZSinks in different pipelines shows a nice design win for the ZIO Streams API.   The code in  ParAvgFun.parAvgUsingChunks  demonstrates a terse and reasonably efficient design for accumulating results using parallel ZStreams (within a single process).  It is applicable to  simple cases where the stream elements are lightweight and similar, and the underlying operations are uniformly easy (like summing numbers).  When instead there is great variability in the cost of proces
Read more

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
Read more

Composed stochastic proof : joint distribution monad as dependent type (part 3 of 4)

Image
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
Read more