Commit 69dab95e authored by Nicola Botta's avatar Nicola Botta
Browse files

ENMO submission.

parent ab395837
% -*-Latex-*-
%if False
> module Application
> import Effects
> import Effect.Exception
> import Effect.StdIO
> import Basic.Predicates
> import FastSimpleProb.Measures
> import FastSimpleProb.Functor
> import NonNegDouble.NonNegDouble
> import NonNegDouble.Constants
> import NonNegDouble.BasicOperations
> import NonNegDouble.Operations
> import NonNegDouble.Predicates
> import NonNegDouble.Properties
> import NonNegDouble.LTEProperties
> import Double.Predicates
> import LocalEffect.Exception
> import LocalEffect.StdIO
> import Fun.Operations
> import Theory
> import Specification
> import Generic
> %default total
> %access public export
> %auto_implicits off
> bestmMeas : (t, n : Nat) -> X t -> String
> bestmMeas t Z x = "The horizon must be greater than zero!"
> bestmMeas t ( S m) x =
> let ps = bi (S t) m in
> let p = bestExt ps in
> let b = p x in
> "Horizon, best, mMeas: " ++
> show (S m) ++ ", " ++ show b ++ ", " ++ show (mMeas t (S m) x)
> bestmMeass : (t : Nat) -> List Nat -> X t -> IO ()
> bestmMeass t Nil x = putStrLn "done!"
> bestmMeass t (n :: ns) x = do putStrLn (bestmMeas t n x)
> bestmMeass t ns x
%endif
\section{The impact of uncertainties on responsibility measures}
\label{section:application}
In sections \ref{section:responsibility} and \ref{section:generic} we
have discussed a new method for assessing how much decisions under
uncertainty matter in specific states and at specific decision steps of
time-discrete decision processes.
We have introduced a small domain-specific language to encode the
goal of decision making in terms of simple verb-predicate clauses and
implemented a generic function \cs{|mMeas|} that fulfills the avoidance
condition put forwards in \citep{10.1111/ecoj.12507} per construction.
%
In this section, we show that, for the stylized decision process of
section \ref{section:specification}, our measure of responsibility also
fulfills the third condition discussed by \cite{10.1111/ecoj.12507}:
\cs{|mMeas|} is zero for decisions that are \emph{causally irrelevant}.
Further, we discuss how uncertainties affect how much decisions matter
for that process. We argue that understanding how uncertainties affect
the importance of decisions in (relatively) simple problems is a
pre-condition for studying more realistic problems like, for example,
those tackled in \citep{esd-10-453-2019, Nordhaus12261}.
%
As a first step, we study the impact of uncertainties about the
capability of decision makers to actually implement decisions on
\cs{|mMeas|}. As in section \ref{section:responsibility}, we focus on values
of \cs{|mMeas|} in \cs{|DHU|}, the initial state of the decision process.
\subsection{The impact of uncertainty about the effectiveness of decision makers}
\label{subsection:impacts1}
%% \begin{figure}[h]
%% \center{\input{figure5.tex}}
%% \label{figure:5}
%% \end{figure}
The results discussed in section \ref{section:responsibility} have been
obtained for decision makers who are 90\% effective: \cs{|pS_Start =
pD_Delay = 0.9|}. Specifically, we have seen that in \cs{|DHU|} at
decision step 0 and for a horizon of 7 decision steps \cs{|mMeas|} was
about 0.173
< *Application> :exec show (mMeas 0 7 DHU)
< "0.1730602684132721"
and that in states with no alternatives, \cs{|mMeas|} is zero
< *Application> :exec show (mMeas 0 7 SHU)
< "0"
and thus fulfils the avoidance condition mentioned above. What if
decisions become \emph{causally irrelevant}? Remember that the
transition function of the decision process from section
\ref{section:specification} is completely defined through products of
the 12 conditional probabilities that define the tables of the nodes of
the belief network of figure \ref{fig:network}, see section
\ref{subsection:next}.
%
Of these conditional probabilities, only \cs{|pS_Start|} and \cs{|pD_Delay|}
depend on the decision to start or to delay a green transition. This implies that, in our decision process,
decisions become ``causally irrelevant'' when
< pS_Start = pS_Delay ! && ! pD_Start = pD_Delay
Because \cs{|pD_Start|} is equal to \cs{|1 - pS_Start|} and \cs{|pS_Delay|} is equal to
\cs{|1 - pD_Delay|}, this is equivalent to
< pS_Start = 1 - pD_Delay
and we can test whether \cs{|mMeas|} fulfills the causality relevance from
\citep{10.1111/ecoj.12507} by replacing the definitions of \cs{|pS_Start|}
and \cs{|pD_Delay|} in section \ref{section:specification} with definitions
that make decisions causally irrelevant. For example, setting
< pS_Start = cast 0.9
< pD_Delay = cast 0.1
yields
< *Application> :exec show (mMeas 0 7 DHU)
< "0"
as one would expect. The same results obtains for \cs{|pS_Start = pD_Delay =
0.5|} and for all decision processes in which the sum of \cs{|pS_Start|} and
\cs{|pD_Delay|} is one.
Having ascertained that our measure of responsibility fulfills two of
the three \emph{natural} conditions put forward in
\citep{10.1111/ecoj.12507}\footnote{The third one, the ``capability to
act intentionally, to plan, and to distinguish right and wrong and
good and bad'', is a property of decision makers rather than a feature
of decision processes. It is relevant for the attribution of blame,
praise, sanctions or retributions to specific individuals but
irrelevant for our work.}, we can turn the attention to the question
of how uncertainties on the capability of decision makers to actually
implement decisions affect measures of responsibility.
Let's start by observing that it is not very realistic to assume that
decision makers are equally effective in implementing the decision to
\cs{|Start|} and to \cs{|Delay|} green transitions: delaying means following a
minimal resistance, ``business as usual'' path.
%
By contrast, implementing a global green transition requires a
significant level of coordination and mutual trust between global
players, not to mention huge economic investments and legislative
efforts.
It follows that it makes sense to study the impact of uncertainty about
the effectiveness of decision makers by fixing \cs{|pD_Delay|}, the
probability that a green transition is delayed given that the decision
was to delay it, to a relatively high value, say 0.9, and vary
\cs{|pS_Start|}.
%
What happens to our measure of responsibility when \cs{|pS_Start|} decreases?
%
We have seen that, for \cs{|pS_Start = pD_Delay = 0.9|}, the measure of
responsibility for a horizon of 7 decision steps was about 0.173 in \cs{|DHU|}
and at decision step 0.
We know that \cs{|mMeas 0 7 DHU|} has to become zero as \cs{|pS_Start|} goes down
to 0.1 (\cs{|pD_Delay|} is fixed to 0.9) because for these values decisions
become causally irrelevant. Does the measure of responsibility \cs{|mMeas 0
7 SHU|} linearly decrease from 0.173 to 0 as \cs{|pS_Start|} decreases from
0.9 to 0.1?
%
Table \ref{table:t2} shows that, in contrast to the popular intuition
that ``if decisions can hardly become true, they do not matter after
all'', this is not the case:
\begin{table}[h]
\begin{center}
\begin{tabular}{ ||c||c||c||c|| }
\hline
\cs{|pS_Start|} & best decisions & \cs{|mMeas 0 7 DHU|} & \cs{|mMeas 1 7 DHU|} \\
\hline
1.0 & \cs{|Start|} & 0.155 & 0.581 \\
0.9 & \cs{|Start|} & 0.173 & 0.567 \\
0.8 & \cs{|Start|} & 0.187 & 0.551 \\
0.7 & \cs{|Start|} & 0.196 & 0.530 \\
0.6 & \cs{|Start|} & 0.199 & 0.504 \\
0.5 & \cs{|Start|} & 0.195 & 0.469 \\
0.4 & \cs{|Start|} & 0.181 & 0.420 \\
0.3 & \cs{|Start|} & 0.153 & 0.348 \\
0.2 & \cs{|Start|} & 0.100 & 0.230 \\
0.1 & \cs{|Start|}, \cs{|Delay|} & 0.000 & 0.000 \\
0.0 & \cs{|Delay|} & 0.138 & 0.337 \\
\hline
\end{tabular}
\end{center}
\vspace{2mm}
\caption{|pS_Start|, best decisions and responsibility measures in |DHU|
at decision steps 0 and 1 and for a horizon of 7 decision steps.}
\label{table:t2}
\end{table}
\noindent
Far from being linear, the measure of responsibility is not even
monotonous! For the case in which a decision to start a green transition
is implemented with only 50\% of probability, |mMeas 0 7 DHU| is
actually higher than for the case in which such decision is realized
with certainty.
%
Computations of |mMeas 1 7 DHU| confirm these observations. In this case
the responsibility decreases monotonically with |pS_Start| but, again,
non-linearly.
Notice also that the best decision for |pS_Start = 0| is \cs{|Delay|}. This
is not surprising: the decision to delay a green transition implies a
10\% probability that the transition is actually started. This is low
but higher than 0, the probability that a green transition gets started
if the decision was \cs{|Start|}.
This concludes the study of the impact of \cs{|pS_Start|} and \cs{|pD_Delay|} on
our measure of responsibility. Before turning the attention to the
impact of uncertainties about commitment to severe impacts from climate
change on \cs{|mMeas 0 7 DHU|}, let's remark that values of \cs{|mMeas 0 7|} and
\cs{|mMeas 1 7|} in \cs{|DLU|} are qualitatively similar to those in \cs{|DHU|} albeit
higher: for \cs{|pS_Start = 0.2|}, for example \cs{|mMeas 0 7 DLU = 0.144|}, 44\%
higher than in initial states with high economic wealth. We do not show
detailed results for \cs{|mMeas 0 7 DLU|} and \cs{|mMeas 1 7 DLU|} but these are
available at \citep{papers}. We will come back to these observations in
section \ref{section:conclusion}.
%% %
%% \REMARK{Nuria}{Include some of Marina's plots?}
%% %
%% \REMARK{Nicola}{Which ones? Where? Specific suggestions? We could also
%% plot the tabulated data, there is no need to recompute them.}
%if False
< pS_Start = 1.0, ! Start, ! mMeas 0 7 DLU = 0.218
< pS_Start = 0.9, ! Start, ! mMeas 0 7 DLU = 0.236
< pS_Start = 0.8, ! Start, ! mMeas 0 7 DLU = 0.249
< pS_Start = 0.7, ! Start, ! mMeas 0 7 DLU = 0.258
< pS_Start = 0.6, ! Start, ! mMeas 0 7 DLU = 0.261
< pS_Start = 0.5, ! Start, ! mMeas 0 7 DLU = 0.257
< pS_Start = 0.4, ! Start, ! mMeas 0 7 DLU = 0.242
< pS_Start = 0.3, ! Start, ! mMeas 0 7 DLU = 0.209
< pS_Start = 0.2, ! Start, ! mMeas 0 7 DLU = 0.144
< pS_Start = 0.1, ! *****, ! mMeas 0 7 DLU = 0
< pS_Start = 0.0, ! Delay, ! mMeas 0 7 DLU = 0.219
< pS_Start = 1.0, ! Start, ! mMeas 1 7 DLU = 0.608
< pS_Start = 0.9, ! Start, ! mMeas 1 7 DLU = 0.598
< pS_Start = 0.8, ! Start, ! mMeas 1 7 DLU = 0.583
< pS_Start = 0.7, ! Start, ! mMeas 1 7 DLU = 0.565
< pS_Start = 0.6, ! Start, ! mMeas 1 7 DLU = 0.542
< pS_Start = 0.5, ! Start, ! mMeas 1 7 DLU = 0.511
< pS_Start = 0.4, ! Start, ! mMeas 1 7 DLU = 0.466
< pS_Start = 0.3, ! Start, ! mMeas 1 7 DLU = 0.397
< pS_Start = 0.2, ! Start, ! mMeas 1 7 DLU = 0.273
< pS_Start = 0.1, ! *****, ! mMeas 1 7 DLU = 0
< pS_Start = 0.0, ! Delay, ! mMeas 1 7 DLU = 0.440
%endif
%% \subsection{The impact of uncertainty about economic downturns.}
%% \label{subsection:impacts2}
%% \REMARK{Nicola}{Marina, all do we want to study/discuss this?}
\subsection{The impact of uncertainty about commitment}
\label{subsection:impacts3}
In section \ref{section:specification}, we have accounted for the
possibility of transitions to states that are committed to severe
impacts from climate change in terms of four conditional probabilities
\cs{|pU_S_0|}, \cs{|pU_D_0|}, \cs{|pU_S|}, \cs{|pU_D|} and their complements.
Remember that \cs{|pU_S_0|} represents the probability of entering
uncommitted states right after the first decision step given that a
green transition was implemented.
%
Similarly, \cs{|pU_S|} represents the probability of entering uncommitted
states at later decision steps given that a green transition was
implemented in those steps or earlier. Similarly for \cs{|pU_D_0|} and
\cs{|pU_D|}.
In all scenarios discussed so far \cs{|pU_S_0|}, \cs{|pU_D_0|}, \cs{|pU_S|}, \cs{|pU_D|}
were set to 0.9, 0.7, 0.9 and 0.3, respectively. This means assuming a
10\% chance of committing to future severe impacts from climate change
if we manage to start a green transition at the first decision step and
a 30\% chance if we fail to do so.
%
We have also assumed that the chance of committing to future impacts
from climate change if we fail to start a green transition increases
from 30\% at the first decision step to 70\% at later decision steps.
This is perhaps a little bit too optimistic if we consider that, in the
Oct.~2018 ``Summary for Policymakers'', the \cite{IPCC_SR15_summary}
estimates that about 50\% of the ``pathways limiting global warming to 2
degrees Celsius with at least 66\% probability'' will attain zero net
$CO_2$ emissions between about 2060 and 2080 whereas more ambitious
paths (limiting global warming to 1.5 degrees Celsius) reach zero net
$CO_2$ emissions earlier.
%
The IPCC report suggests that a more realistic estimate of \cs{|pU_S_0|} (if
we identify our green transition corridor with one that attains
zero net $CO_2$ emissions between about 2060 and 2080 and associate
commitment to severe impacts from climate change with violating the 2
degrees Celsius goal) would perhaps be about 0.66.
What if we assume \cs{|pU_S_0 = 0.7|} and lower \cs{|pU_D_0|} accordingly, say to
50\%? For consistency, we also need to decrease \cs{|pU_S|} and \cs{|pU_D|}, say
to 0.7 and 0.1. The corresponding measures of responsibility in \cs{|DHU|} at
decision steps zero and one and for an horizon of 7 steps are reported
in table \ref{table:t3}.
\begin{table}[h]
\begin{center}
\begin{tabular}{ ||c||c||c||c|| }
\hline
\cs{|pS_Start|} & best decisions & \cs{|mMeas 0 7 DHU|} & \cs{|mMeas 1 7 DHU|} \\
\hline
1.0 & \cs{|Start|} & 0.141 & 0.748 \\
0.9 & \cs{|Start|} & 0.159 & 0.733 \\
0.8 & \cs{|Start|} & 0.171 & 0.713 \\
0.7 & \cs{|Start|} & 0.177 & 0.689 \\
0.6 & \cs{|Start|} & 0.178 & 0.658 \\
0.5 & \cs{|Start|} & 0.170 & 0.616 \\
0.4 & \cs{|Start|} & 0.154 & 0.557 \\
0.3 & \cs{|Start|} & 0.125 & 0.468 \\
0.2 & \cs{|Start|} & 0.077 & 0.315 \\
0.1 & \cs{|Start|}, \cs{|Delay|} & 0 & 0 \\
0.0 & \cs{|Delay|} & 0.098 & 0.485 \\
\hline
\end{tabular}
\end{center}
\vspace{2mm}
\caption{Like table \ref{table:t2} but with \cs{|pU_S_0|}, \cs{|pU_D_0|}, \cs{|pU_S|}
and \cs{|pU_D|} set to 0.7, 0.5, 0,7 and 0.1 (instead of 0.9, 0.7, 0.9 and
0.3).}
\label{table:t3}
\end{table}
\noindent
By comparing these results with those of table \ref{table:t2}, we see
that the effect of increasing the probability of severe impacts from
climate change by 20\% has been to systematically \emph{decrease}
% \cs{|mMeas 0 7 DHU|}
how much decisions matter at the first decision step
and to \emph{increase}
% \cs{|mMeas 1 7 DHU|}.
how much decisions matter at the second decision step.
%
We will come back to this observation in the conclusion.
%
%%\REMARK{Nuria}{``in the next section'' $\mapsto$ ``in the
%%conclusion''?}
%
%% Nicola: done
%if False
< *Application> :exec (bestmMeas 0 7 DHU)
< "Horizon, best, mMeas: 7, Start, 0.1415395735405339"
< pS_Start = 1.0, ! Start, ! mMeas 0 7 DHU = 0.141 -- 0.155
< pS_Start = 0.9, ! Start, ! mMeas 0 7 DHU = 0.159 -- 0.173
< pS_Start = 0.8, ! Start, ! mMeas 0 7 DHU = 0.171 -- 0.187
< pS_Start = 0.7, ! Start, ! mMeas 0 7 DHU = 0.177 -- 0.196
< pS_Start = 0.6, ! Start, ! mMeas 0 7 DHU = 0.178 -- 0.199
< pS_Start = 0.5, ! Start, ! mMeas 0 7 DHU = 0.170 -- 0.195
< pS_Start = 0.4, ! Start, ! mMeas 0 7 DHU = 0.154 -- 0.181
< pS_Start = 0.3, ! Start, ! mMeas 0 7 DHU = 0.125 -- 0.153
< pS_Start = 0.2, ! Start, ! mMeas 0 7 DHU = 0.077 -- 0.100
< pS_Start = 0.1, ! *****, ! mMeas 0 7 DHU = 0
< pS_Start = 0.0, ! Delay, ! mMeas 0 7 DHU = 0.098 -- 0.138
< pS_Start = 1.0, ! Start, ! mMeas 1 7 DHU = 0.748 -- 0.581
< pS_Start = 0.9, ! Start, ! mMeas 1 7 DHU = 0.733 -- 0.567
< pS_Start = 0.8, ! Start, ! mMeas 1 7 DHU = 0.713 -- 0.551
< pS_Start = 0.7, ! Start, ! mMeas 1 7 DHU = 0.689 -- 0.530
< pS_Start = 0.6, ! Start, ! mMeas 1 7 DHU = 0.658 -- 0.504
< pS_Start = 0.5, ! Start, ! mMeas 1 7 DHU = 0.616 -- 0.469
< pS_Start = 0.4, ! Start, ! mMeas 1 7 DHU = 0.557 -- 0.420
< pS_Start = 0.3, ! Start, ! mMeas 1 7 DHU = 0.468 -- 0.348
< pS_Start = 0.2, ! Start, ! mMeas 1 7 DHU = 0.315 -- 0.230
< pS_Start = 0.1, ! *****, ! mMeas 1 7 DHU = 0
< pS_Start = 0.0, ! Delay, ! mMeas 1 7 DHU = 0.485 -- 0.337
%endif
% -*-Latex-*-
%if False
> module Conclusion
%endif
\section{Conclusion}
\label{section:conclusion}
In this paper, we have studied the notion of responsibility under
uncertainty in sequential decision processes in the context of
global climate policy.
%
Specifically, we have extended the verified theory of policy advice and
avoidability \citep{2017_Botta_Jansson_Ionescu} with a family of methods
for measuring how much decisions under uncertainty do matter and the
degree of responsibility associated with such decisions.
We have also introduced a small domain specific language for specifying
sustainability goals in GHG emissions decision processes.
%
We have applied the DSL to formalize a stylized decision process in
which a decision maker repeatedly faces two options over a finite number
of decision steps: start a ``green'' transition to a decarbonized
society or delay such transition. We have studied how uncertainties (on
the capability of decision makers to actually implement their decisions
and on the consequences of starting or delaying green transitions)
affect how much decisions at specific points in time do matter and the
degree of responsibility associated with these decisions.
Some of the results presented in sections \ref{section:responsibility},
\ref{section:generic} and \ref{section:application} are consistent with
common intuitions on how responsibility changes when the capability of
decision makers to actually impose their decisions increases or
decreases.
Perhaps more surprisingly, we have also found that the measures of
responsibility discussed in section \ref{section:responsibility} suggest
that a ``moral'' approach towards decision making -- doing the right
thing even though the probability of success becomes increasingly small
-- is perfectly rational over a wide range of uncertainties.
The fact that these results are based on verified methods for computing
optimal policies is crucial for their interpretation: they are a logical
consequence of the assumptions about the decision process specified in
section \ref{section:specification} and of the goals of decision making
(avoiding short term economic downturns and long term negative impacts
from climate change) explicitly stated in section \ref{section:generic}
and not the result of programming errors.
%
%% \REMARK{Nuria}{Change to ``and we can be sure that they are not the
%% result...''? Not using ``verified methods'' does not necessarily mean
%% that the results are ``the result of programming errors''.}
%
%% Nicola: the statement seems perfectly fine to me. It does not suggest
%% that not using verified methods necessarily leads to programming
%% errors.
%
The fact that ``best'' decisions are stable with respect to both
decision horizons (the number of decision steps to look forward in order
to define measures of responsibility) and to the amount of uncertainty
suggest that our results could be valid for more realistic decision
processes than the one studied here.
In the last section, we have also shown that the measures of
responsibility introduced in section \ref{section:responsibility}
fulfill two of the three natural conditions put forward in
\citep{10.1111/ecoj.12507}. For the third condition, see footnote 14 on
page 41.
%
%%\REMARK{Nuria}{Maybe rather spell this out?}
%
%% Nicola: suggestion?
Also in section \ref{section:application}, we have shown that, in DHU
(green transition delayed, economic welfare high, uncommitted to
negative impacts from climate change) the importance of taking the right
decision (starting a green transition) at decision step 0 systematically
\emph{decreases} (as compared to the importance of taking the right
decision -- also starting a green transition -- at decision step 1) as
the probability of severe impacts from climate change \emph{increases}.
It is important to point out that this result is only in apparent
contradiction with the intuition (that inspires, among others, the
``Fridays for future'' movement) that current climate decisions matter
more than decisions to be taken in the upcoming decades. This is because
of two reasons.
The first one is that the probability of facing the decision to either
start or to delay a green transition in DHU at decision step 1 is less
than one. In other words: it is true that, if the next generation will
happen to be in DHU, they will face a decision that matters more than
the current one. But the probability that the next generation
\emph{will be} in DHU is relatively low, especially if the current
decision is to further delay a green transition!
The second reason why the results discussed in section
\ref{section:application} are not in contradiction with the notion that
current climate decisions matter more than decisions to be taken in the
upcoming decades is more subtle and needs to be discussed with some
care.
In the introduction, we have pointed out a fundamental difficulty of
climate policy advice: the lack of agreement on how to account for the
chances and the risks of climate change.
In the language introduced in section \ref{section:generic}, lack of
agreement on how to account for the chances and the risks of climate
change means lack of agreement on how to define \cs{|goal|}. Remember that
the results discussed in section \ref{section:application} have been
obtained with
< goal = Avoid isCommitted <&&> Avoid isDisrupted
In other words, we have measured how much decisions matter and how to
attribute responsibility to specific decisions with respect to the goal
of avoiding negative impacts from climate change and economic
downturns.
This encodes notions of sustainability but not necessarily of
\emph{fairness} (balanced share of responsibility between generations),
not to mention \emph{justice}: there is nothing in the above definition
of \cs{|goal|} that prevents optimal decisions to lead to states in which the
set of options available to upcoming generations has shrunk or to states
in which decision makers have to face more crucial decisions than the
current one.
By contrast, the idea that current climate decisions matter more than
decisions to be taken in the upcoming decades is based on notions of
fairness and justice that are not encoded in \cs{|goal|} and thus are not
accounted for in the analysis presented in section
\ref{section:application}.
%
As far as one can define predicates on states that encode notions of
fairness and justice, one can apply the measures of responsibility from
section \ref{section:generic}.
The problem to agree on what is to be considered fair and just
limits the applicability of rigorous decision theories to climate
policy. But it is a problem that, to quote Hardin \citep{hardin1968},
``has no technical solution'' and cannot be avoided -- neither by
verified decision making \citep{2017_Botta_Jansson_Ionescu}, nor by
generalizations of cost-benefit analysis \citep{shape2021},
multi-objective optimal control \citep{CARLINO202016593} or storylines
\citep{shepherd2019}.
%% At the same time, it is crucial that both advisors
%% and decision makers fully understand the implications of this problem
%% for policy advice.
From this perspective, this paper can also be seen as a contribution
from verified decision theory towards understanding the limits of
applicability of decision theories to policy advice.
% -*-Latex-*-
%if False
> module Generic
> import Data.So
> import Effects
> import Effect.Exception
> import Effect.StdIO
> import Basic.Predicates
> import FastSimpleProb.Measures
> import FastSimpleProb.Functor
> import NonNegDouble.NonNegDouble
> import NonNegDouble.Constants
> import NonNegDouble.BasicOperations
> import NonNegDouble.Operations
> import NonNegDouble.Predicates
> import NonNegDouble.Properties
> import NonNegDouble.LTEProperties
> import Double.Predicates
> import LocalEffect.Exception
> import LocalEffect.StdIO
> import Fun.Operations
> import Theory
> import Specification
> %default total
> %access public export
> %auto_implicits off
> infixr 5 <&&>
> infixr 4 <||><