3 results
Search Results
Now showing 1 - 3 of 3
- ItemClimate impact research: Beyond patchwork(München : European Geopyhsical Union, 2014) Huber, V.; Schellnhuber, H.J.; Arnell, N.W.; Frieler, K.; Gerten, D.; Haddeland, I.; Kabat, P.; Lotze-Campen, H.; Lucht, W.; Parry, M.; Piontek, F.; Rosenzweig, C.; Schewe, J.; Warszawski, L.Despite significant progress in climate impact research, the narratives that science can presently piece together of a 2, 3, 4, or 5 °C warmer world remain fragmentary. Here we briefly review past undertakings to characterise comprehensively and quantify climate impacts based on multi-model approaches. We then report on the Inter-Sectoral Impact Model Intercomparison Project (ISI-MIP), a community-driven effort to compare impact models across sectors and scales systematically, and to quantify the uncertainties along the chain from greenhouse gas emissions and climate input data to the modelling of climate impacts themselves. We show how ISI-MIP and similar efforts can substantially advance the science relevant to impacts, adaptation and vulnerability, and we outline the steps that need to be taken in order to make the most of the available modelling tools. We discuss pertinent limitations of these methods and how they could be tackled. We argue that it is time to consolidate the current patchwork of impact knowledge through integrated cross-sectoral assessments, and that the climate impact community is now in a favourable position to do so.
- ItemSequential decision problems, dependent types and generic solutions(Braunschweig : Department of Theoretical Computer Science, Technical University of Braunschweig, 2017) Botta, N.; Jansson, P.; Ionescu, C.; Christiansen, D.R.; Brady, E.We present a computer-checked generic implementation for solving finite-horizon sequential decision problems. This is a wide class of problems, including inter-temporal optimizations, knapsack, optimal bracketing, scheduling, etc. The implementation can handle time-step dependent control and state spaces, and monadic representations of uncertainty (such as stochastic, non-deterministic, fuzzy, or combinations thereof). This level of genericity is achievable in a programming language with dependent types (we have used both Idris and Agda). Dependent types are also the means that allow us to obtain a formalization and computer-checked proof of the central component of our implementation: Bellman’s principle of optimality and the associated backwards induction algorithm. The formalization clarifies certain aspects of backwards induction and, by making explicit notions such as viability and reachability, can serve as a starting point for a theory of controllability of monadic dynamical systems, commonly encountered in, e.g., climate impact research.
- ItemTesting versus proving in climate impact research(Wadern : Schloss Dagstuhl, 2013) Ionescu, C.; Jansson, P.Higher-order properties arise naturally in some areas of climate impact research. For example, "vulnerability measures", crucial in assessing the vulnerability to climate change of various regions and entities, must fulfill certain conditions which are best expressed by quantification over all increasing functions of an appropriate type. This kind of property is notoriously difficult to test. However, for the measures used in practice, it is quite easy to encode the property as a dependent type and prove it correct. Moreover, in scientific programming, one is often interested in correctness "up to implication": The program would work as expected, say, if one would use real numbers instead of floating-point values. Such counterfactuals are impossible to test, but again, they can be easily encoded as types and proven. We show examples of such situations (encoded in Agda), encountered in actual vulnerability assessments.