| 1. |
- Botta, Nicola, 1961, et al.
(författare)
-
Extensional equality preservation and verified generic programming
- 2021
-
Ingår i: Journal of Functional Programming. - 1469-7653 .- 0956-7968. ; 31
-
Tidskriftsartikel (refereegranskat)abstract
- In verified generic programming, one cannot exploit the structure of concrete data types but has to rely on well chosen sets of specifications or abstract data types (ADTs). Functors and monads are at the core of many applications of functional programming. This raises the question of what useful ADTs for verified functors and monads could look like. The functorial map of many important monads preserves extensional equality. For instance, if f, g : A → B are extensionally equal, that is, ∀x ∈ A, f x = g x , then map f : List A → List B and map g are also extensionally equal. This suggests that preservation of extensional equality could be a useful principle in verified generic programming. We explore this possibility with a minimalist approach: we deal with (the lack of) extensional equality in Martin-Löf’s intensional type theories without extending the theories or using full-fledged setoids. Perhaps surprisingly, this minimal approach turns out to be extremely useful. It allows one to derive simple generic proofs of monadic laws but also verified, generic results in dynamical systems and control theory. In turn, these results avoid tedious code duplication and ad-hoc proofs. Thus, our work is a contribution towards pragmatic, verified generic programming.
|
|
| 2. |
- Botta, Nicola, 1961, et al.
(författare)
-
Responsibility Under Uncertainty: Which Climate Decisions Matter Most?
- 2023
-
Ingår i: Environmental Modeling and Assessment. - : Springer Science and Business Media LLC. - 1573-2967 .- 1420-2026. ; 28:3, s. 337-365
-
Tidskriftsartikel (refereegranskat)abstract
- We propose a new method for estimating how much decisions under monadic uncertainty matter. The method is generic and suitable for measuring responsibility in finite horizon sequential decision processes. It fulfills “fairness” requirements and three natural conditions for responsibility measures: agency, avoidance and causal relevance. We apply the method to study how much decisions matter in a stylized greenhouse gas emissions process in which a decision maker repeatedly faces two options: start a “green” transition to a decarbonized society or further delay such a transition. We account for the fact that climate decisions are rarely implemented with certainty and that their consequences on the climate and on the global economy are uncertain. We discover that a “moral” approach towards decision making — doing the right thing even though the probability of success becomes increasingly small — is rational over a wide range of uncertainties.
|
|
| 3. |
- Brede, Nuria, et al.
(författare)
-
On the correctness of monadic backward induction
- 2021
-
Ingår i: Journal of Functional Programming. - 1469-7653 .- 0956-7968. ; 31
-
Tidskriftsartikel (refereegranskat)abstract
- In control theory, to solve a finite-horizon sequential decision problem (SDP) commonly means to find a list of decision rules that result in an optimal expected total reward (or cost) when taking a given number of decision steps. SDPs are routinely solved using Bellman's backward induction. Textbook authors (e.g. Bertsekas or Puterman) typically give more or less formal proofs to show that the backward induction algorithm is correct as solution method for deterministic and stochastic SDPs. Botta, Jansson and Ionescu propose a generic framework for finite horizon, monadic SDPs together with a monadic version of backward induction for solving such SDPs. In monadic SDPs, the monad captures a generic notion of uncertainty, while a generic measure function aggregates rewards. In the present paper, we define a notion of correctness for monadic SDPs and identify three conditions that allow us to prove a correctness result for monadic backward induction that is comparable to textbook correctness proofs for ordinary backward induction. The conditions that we impose are fairly general and can be cast in category-theoretical terms using the notion of Eilenberg-Moore algebra. They hold in familiar settings like those of deterministic or stochastic SDPs, but we also give examples in which they fail. Our results show that backward induction can safely be employed for a broader class of SDPs than usually treated in textbooks. However, they also rule out certain instances that were considered admissible in the context of Botta et al. 's generic framework. Our development is formalised in Idris as an extension of the Botta et al. framework and the sources are available as supplementary material.
|
|
| 4. |
- Montero, Marina Martínez, et al.
(författare)
-
Lost options commitment: how short-term policies affect long-term scope of action
- 2024
-
Ingår i: Oxford Open Climate Change. - 2634-4068. ; 4:1
-
Tidskriftsartikel (refereegranskat)abstract
- We propose to explore the sustainability of climate policies based on a novel commitment metric. This metric allows to quantify how future generations’ scope of action is affected by short-term climate policy. In an example application, we show that following a moderate emission scenario like SSP2-4.5 will commit future generations to heavily rely on carbon dioxide removal or/and solar radiation modification to avoid unmanageable sea level rise.
|
|
| 5. |
- Montero, Marina Martinez, et al.
(författare)
-
SURFER v2.0: a flexible and simple model linking anthropogenic CO2 emissions and solar radiation modification to ocean acidification and sea level rise
- 2022
-
Ingår i: Geoscientific Model Development. - : Copernicus GmbH. - 1991-959X .- 1991-9603. ; 15:21, s. 8059-8084
-
Tidskriftsartikel (refereegranskat)abstract
- We present SURFER, a novel reduced model for estimating the impact of CO2 emissions and solar radiation modification options on sea level rise and ocean acidification over timescales of several thousands of years. SURFER has been designed for the analysis of CO2 emission and solar radiation modification policies, for supporting the computation of optimal (CO2 emission and solar radiation modification) policies and for the study of commitment and responsibility under uncertainty. The model is based on a combination of conservation laws for the masses of atmospheric and oceanic carbon and for the oceanic temperature anomalies, and of adhoc parameterisations for the different sea level rise contributors: ice sheets, glaciers and ocean thermal expansion. It consists of 9 loosely coupled ordinary differential equations, is understandable, fast and easy to modify and calibrate. It reproduces the results of more sophisticated, high-dimensional earth system models on timescales up to millennia.
|
|
