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 problem - the MiniZinc compiler can translate it into different forms suitable for a wide range of solvers, such as Constraint Programming (CP), Mixed Integer Linear Programming (MIP) or Boolean Satisfiability (SAT) solvers."

Slightly Boring General Thoughts on Modeling Methodology

Results from a constrained optimization study provide insight that leads us to ask more questions, which in turn lead us to refine and restate our model (our "what?").  In parallel, we work to validate and clarify our application goals (our "why?").  We may venture in an idiosyncratic experimental direction by applying agent simulation and visualization techniques, or we may seek to operationalize our model in some data analysis system, which may use huge datasets and machine learning techniques.  Separately, to deepen our abstract understanding and consequent leverage, we may further formalize our model as a theory, adapted from existing theories.

Formalization with SMT

SMT-LIB offers an incremental pathway to formalization of our relationship model into a theory.
From Wikipedia page for SMT:

"...the satisfiability modulo theories (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order logic with equality."
"SMT can be thought of as a form of the constraint satisfaction problem and thus a certain formalized approach to constraint programming."   "An SMT instance is a generalization of a Boolean SAT instance in which various sets of variables are replaced by predicates from a variety of underlying theories. "

The SMT community has defined a common language, called SMT-LIB:

Finally, a tremendous resource for many logical languages and solvers is Hakank's Home Page.






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

Overview of AxLam model : Nouns, Types, Morphisms

2023-Feb-03 picking up from tweet thread of 220909  AxLam model: Noun (space), Type (paint), Morphism (arrow) AxLam is for writing models using [concepts, types, and morphisms].  Our concepts may be in the form of some data, or less specifically as things we choose to name or refer to in a model.  Over this concept space, we use types and morphisms to define an adjustable descriptive model that directs and regulates processing of the concept data (or other manifestation).  Alternatively and  more approachably we may write in terms of [nouns,  formal classes, and mappings], and this framing is mostly equivalent for informal purposes. Nouns / Concepts / Terms / Data Nouns (i.e. concepts) describe anything we wish to refer to, and need not be explicit or named.  We think of nouns as the space of things we might try to describe, name or refer to.  "Terms" in a type-theoretic sense are nouns.  Real things in the human world that someone cares about are nouns.  In practice when we
Read more

AxioMagic under Spark on cloud (AWS, Azure, ...)

AxioMagic under Spark on ${ cloud  } AxioMagic relies on functional composition over immutable inputs, thus matching modern evaluation frameworks like Apache Spark, which defines a structured approach to managing data contexts of functional evaluation over data frames.  Spark embodies a refinement of both  ETL and MapReduce methodology.  State machines like Spark require computation and storage resources which may come from any cluster, but today are commonly provided from cloud environments, yielding high volume functional computation at predictable usage-based costs.  We especially value Spark for open scientific dataset analysis, where it is common to work with large data files in interchange formats. Essential features of Spark distributed evaluation Spark assembles batch pipelines to pump datasets of structured records through functional tasks (which may  invoke side-effects, with all necessary stipulations).  This pipeline serves to evaluate a given distributed functional algorit
Read more