<div class="notebook">
<div class="nb-cell markdown" name="md1">
# Declarative Programming for Mathematics
> [Declarative programming](https://en.wikipedia.org/wiki/Declarative_programming) is a programming paradigm—a style of building the structure and elements of computer programs—that expresses the logic of a computation without describing its control flow.
In general terms this means solving a problem by describing _what_ the problem is rather than specifying _how_ to solve as is done in the common imperative languages. Declarative programming often considers programs as theories of a formal logic, and computations as deductions in that logic space, Prolog being an example based on first order logic. But for purely practical reasons, arithmetic in Prolog is non-logical as evidenced by the modal nature of the builtin arithmetic predicates (`is/2, =:=/2, >/2`, etc.). Since arithmetic expressions containing variables normally result in errors, an order is imposed on any sequence of expression evaluation, i.e., you must specify *how* to evaluate such a sequence.
CLP's over numeric domains, e.g., `clpfd` over the finite domain of integers, attempt to rectify this. Constraints can be defined in any order restoring the declarative nature to arithmetic evaluation. `clpBNR` extends this model to the continuous domain of real numbers and booleans (represented by the integers `0` and `1`).
So the challenge when trying to solve mathematical problems is how to model the problem in terms of equalites and inequalities of numeric variables, i.e., in `clpBNR`, variables constrained to be a set of real values between a lower and upper bound, which are specific values in the set. Syntactically, a constraint is just an arithmetic goal wrapped in a set of curly brackets; more than one constraint can be defined in the same set of curly brackets using `,` as a separator, like goals in a clause body. Semantically, contraints are boolean expressions that must be true for the top level goal to be true; inconsistent constraints reult in failure at the point where the inconsistency is detected. Examples:
</div>
<div class="nb-cell program" data-background="true" data-singleline="true" name="p1">
:- use_module(library(clpBNR)).
</div>
<div class="nb-cell query" name="q5">
{X == Y}.
</div>
<div class="nb-cell query" name="q3">
{X == cos(X)}.
</div>
<div class="nb-cell query" name="q1">
{X =< 0}, X=10.
</div>
<div class="nb-cell markdown" name="md4">
The more readable ellipsis postfix notation in the second example displays the fractional digits that the lower and upper bounds have in common.
</div>
<div class="nb-cell query" name="q4">
{X**2+Y**2==2, Y-X**2==0, X>=0}.
</div>
<div class="nb-cell markdown" name="md3">
Historically CLP(BNR) uses `==` for equality but `is` and `=:=` are treated as synonyms for convenience.
In the first example =|X|= and =|Y|= are totally unconstrained (any real value inclusing the infinites) but the last two examples define adequate constraints for the variable(s) to narrow to the limits supported by the floating point representation.
CLP is declarative, so try re-ordering, e.g.,
</div>
<div class="nb-cell query" name="q6">
{X>=0, Y-X**2==0, X**2+Y**2==2}.
</div>
<div class="nb-cell query" name="q2">
X=42, {X>=0, Y-X**2==0, X**2+Y**2==2}.
</div>
<div class="nb-cell markdown" name="md5">
An under-constrained problem may have multiple solutions, in which case any interval results must contain all solutions (may not be the narowest possible interval):
</div>
<div class="nb-cell query" name="q7">
{Y-X**2==0, X**2+Y**2==2}.
</div>
<div class="nb-cell markdown" name="md6">
To generate individual solutions, use alternative constraints to create sub-problems for each potential solution:
</div>
<div class="nb-cell query" name="q8">
{Y-X**2==0, X**2+Y**2==2},({X=<0} ; {X>=0}).
</div>
<div class="nb-cell markdown" name="md7">
This process is sometimes called labeling. But labeling for a continuous domain requires interval splitting (rather than enumeration). And in lieu of explicit splitting as shown in the previous example, the `clpBNR` library provides `solve/1`. This predicate attempts to recursively split an interval (or list of intervals) at a point (or points) which are not solutions. (This avoids creating multiple apparent solutions for a single real solution.) Intervals which are too narrow (defined as digits of precision specified by the environment flag `clpBNR_default_precision`) are not subject to splitting, and `solve/1` terminates when all intervals can no longer be split.
Using `solve/1` on the previous example:
</div>
<div class="nb-cell query" name="q9">
{Y-X**2==0, X**2+Y**2==2}, solve(X).
</div>
<div class="nb-cell markdown" name="md8">
While the constraints are declarative here, the total solution is not. It doesn't make any sense to `solve` before defining the constraints, so there is a _how_ factor - apply constraints then `solve`. This is pretty standard practice for any CLP where labeling is performed after constraints are defined.
Here's another [example](https://www.youtube.com/watch?v=KXXwyuE497Q), one of the "Math Olympiad" problems commonly found on YouTube:
</div>
<div class="nb-cell query" name="q10">
{X**2 == Y+73, Y**2 == X+73}.
</div>
<div class="nb-cell markdown" name="md9">
The answer to this query isn't very helpful. But the quadratic form of the equations suggests there are multimple solutions, so trying `solve/1`:
</div>
<div class="nb-cell query" name="q11">
{X**2 == Y+73, Y**2 == X+73}, solve([X,Y]).
</div>
<div class="nb-cell markdown" name="md10">
But this yields a perhaps unexpected answer at the end. This is because constraint propagation cannot definitevely prove there are no answers in the interval between the maximum finite floating point value and infinity.
Intervals with an bound of =|±inf|= can be problematical for constraint propagation (e.g., `inf+X == inf`), but an variable in a constraint expression will be initialized to bounds `(-inf,+inf)` (the extended set of reals). For this reason, it's a good paractice to "declare" real variables using the `::/2` predicate. (For convenience, `::` is also defined as a binary operator by `clpBNR`.) Now:
</div>
<div class="nb-cell query" name="q12">
[X,Y]::real, {X**2 == Y+73, Y**2 == X+73}, solve([X,Y]).
</div>
<div class="nb-cell markdown" name="md11">
In this case =|X|= and =|Y|= will start with large but finite bounds, but the bound can also be explicitly defined:
</div>
<div class="nb-cell query" name="q13">
[X,Y]::real(0,100), {X**2 == Y+73, Y**2 == X+73}, solve([X,Y]).
</div>
<div class="nb-cell markdown" name="md12">
Declarations act much like constraints so the order is unimportant preserving the declarative behaviour:
</div>
<div class="nb-cell query" name="q14">
{X**2 == Y+73, Y**2 == X+73}, [X,Y]::real(0,100), solve([X,Y]).
</div>
<div class="nb-cell markdown" name="md13">
Finally, declarations can also be used to constrain the values to integer (or boolean) subset of the extended real domain:
</div>
<div class="nb-cell query" name="q15">
[X,Y]::integer, {X**2 == Y+73, Y**2 == X+73}, solve([X,Y]).
</div>
<div class="nb-cell markdown" name="md14">
The default bounds for each type:
</div>
<div class="nb-cell query" name="q16">
B::boolean, N::integer, R::real.
</div>
<div class="nb-cell markdown" name="md15">
There is another reason why constraints alone may be insufficient to narrow an interval to the narowest possible value - the so-called dependancy issue in interval arithmetic. Consider the following example:
</div>
<div class="nb-cell query" name="q17">
X::real(-1,1), {Y == X*(X+1)}.
</div>
<div class="nb-cell markdown" name="md16">
The answer indicates that domain of `Y` is `(-2,2)` which is true but not an optimally narrow value,i.e., `(-1/4.2)`. Rewriting the constraint improves the result but is still not optimal:
</div>
<div class="nb-cell query" name="q18">
X::real(-1,1), {Y == X**2+X}.
</div>
<div class="nb-cell markdown" name="md17">
The problem as stated by Moore in 1966 is that overestimation can be prevented only if each variable in the constraint has only one occurrence. Rewriting the constraint (again) to satisfy this critera:
</div>
<div class="nb-cell query" name="q19">
X::real(-1,1), {Y == (X+1/2)**2 - 1/4}.
</div>
<div class="nb-cell markdown" name="md18">
But this is not obvious even in this simple example. `solve/1` can used (at some runtime expense) to "force" the interval to its (approximate) optimal value:
</div>
<div class="nb-cell query" name="q20">
X::real(-1,1), {Y == X*(X+1)}, solve(Y).
</div>
<div class="nb-cell markdown" name="md19">
This is an unfortunate property of interval arithmetic which has not been overcome (to my knowledge). As a consequence mathematically equivalent expressions may not be equivalent in terms of performance. Another example (not detailed here) is that the Horner form of polynomials (e.g., `{X*(X-2)+1 == 0}`) is usually better "behaved" than the more natural form (e.g., `{X**2-2*X+1 == 0}`). For most practical purposes, this problem dependant performance issue can be ignored when a search predicate like `solve/1` is used.
</div>
<div class="nb-cell markdown" name="md2">
#### Summary
Standard Prolog arithmetic is modal, losing the the basic relational property that enables declarative programming. Constraints over numeric domains restore this logical property to Prolog arithmetic. Some claim that traditonal arithmetic should be considered "legacy" to be replaced by constraint based arithmetic (see "Legacy Predicates" in [Prolog Integer Arithmetic](https://www.metalevel.at/prolog/clpz)). That is probably a bridge too far for many users familiar with standard functional arithemtic, but the ability to find solutions to mathematical problems just by (declaratively) writing a set of equations demonstrates the benefits of a CLP based approach.
</div>
</div>