| 1. |
- Botta, Nicola, et al.
(författare)
-
Contributions to a computational theory of policy advice and avoidability
- 2017
-
Ingår i: Journal of Functional Programming. - 1469-7653 .- 0956-7968. ; 27, s. 1-52
-
Tidskriftsartikel (refereegranskat)abstract
- We present the starting elements of a mathematical theory of policy advice and avoidability. More specifically, we formalize a cluster of notions related to policy advice, such as policy, viability, reachability, and propose a novel approach for assisting decision making, based on the concept of avoidability. We formalize avoidability as a relation between current and future states, investigate under which conditions this relation is decidable and propose a generic procedure for assessing avoidability. The formalization is constructive and makes extensive use of the correspondence between dependent types and logical propositions, decidable judgments are obtained through computations. Thus, we aim for a computational theory, and emphasize the role that computer science can play in global system science.
|
|
| 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. |
- Botta, N., et al.
(författare)
-
Sequential decision problems, dependent types and generic solutions
- 2017
-
Ingår i: Logical Methods in Computer Science. - 1860-5974. ; 13:1
-
Tidskriftsartikel (refereegranskat)abstract
- 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.
|
|
| 4. |
- Botta, Nicola, 1961, et al.
(författare)
-
The impact of uncertainty on optimal emission policies
- 2018
-
Ingår i: Earth System Dynamics. - : Copernicus GmbH. - 2190-4979 .- 2190-4987. ; 9:2, s. 525-542
-
Tidskriftsartikel (refereegranskat)abstract
- We apply a computational framework for specifying and solving sequential decision problems to study the impact of three kinds of uncertainties on optimal emission policies in a stylized sequential emission problem. We find that uncertainties about the implementability of decisions on emission reductions (or increases) have a greater impact on optimal policies than uncertainties about the availability of effective emission reduction technologies and uncertainties about the implications of trespassing critical cumulated emission thresholds. The results show that uncertainties about the implementability of decisions on emission reductions (or increases) call for more precautionary policies. In other words, delaying emission reductions to the point in time when effective technologies will become available is suboptimal when these uncertainties are accounted for rigorously. By contrast, uncertainties about the implications of exceeding critical cumulated emission thresholds tend to make early emission reductions less rewarding.
|
|
| 5. |
- Ingegnoli, Francesca, et al.
(författare)
-
A comparison between nailfold capillaroscopy patterns in adulthood in juvenile and adult-onset systemic sclerosis: A EUSTAR exploratory study
- 2015
-
Ingår i: Microvascular Research. - : Elsevier BV. - 1095-9319 .- 0026-2862. ; 102, s. 19-24
-
Tidskriftsartikel (refereegranskat)abstract
- Objective: Qualitative capillaroscopy patterns in juvenile- and adult-onset systemic sclerosis (SSc) were studied in adulthood using data from the EULAR Scleroderma Trials and Research (EUSTAR) database. Methods: Data collected between June 2004 and April 2013 were examined with focus on capillaroscopy. In this retrospective exploratory study, series of patients with juvenile-onset SSc were matched with series of adult-onset SSc having the same gender and autoantibody profile. Results: 30 of 123 patients with juvenile-onset and 2108 of 7133 with adult-onset SSc had data on capillaroscopy. Juvenile-onset SSc showed scleroderma pattern more frequently than adult-onset SSc (93.3% and 88%). The OR was 2.44 and 95% Cl 0.57-10.41. An active scleroderma pattern was present in 58% of juvenile- and 61% of adult-onset SSc. The OR was 0.91 and 95% Cl 0.28-2.93. The late scleroderma pattern was present in 61% of juvenile- and 55.5% of adult-onset SSc. The OR was 1.06 and 95% Cl 0.34-3.56. Conclusion: This is the first exploratory study on the comparison of capillaroscopy between juvenile- and adult-onset SSc in adulthood. Juvenile-onset SSc had an increase prevalence of sderoderma pattern, but a similar distribution of the three patterns was suggested. Further studies are needed to define this issue. (C) 2015 Elsevier Inc. All rights reserved.
|
|
| 6. |
- Ionescu, Cezar, et al.
(författare)
-
Dependently-typed programming in scientific computing: Examples from economic modelling
- 2013
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. ; 8241 LNCS
-
Konferensbidrag (refereegranskat)abstract
- Computer simulations are essential in virtually every scientific discipline, even more so in those such as economics or climate change where the ability to make laboratory experiments is limited. Therefore, it is important to ensure that the models are implemented correctly, that they can be re-implemented and that the results can be reproduced. Typically, though, the models are described by a mixture of prose and mathematics which is insufficient for these purposes. We argue that using dependent types allows us to gradually reduce the gap between the mathematical description and the implementation, and we give examples from economic modelling. We discuss the consequences that our incremental approach has on programming style and the requirements it imposes on the dependently-typed programming languages used.
|
|
| 7. |
- Ionescu, Cezar, 1968, et al.
(författare)
-
Domain-Specific Languages of Mathematics: Presenting Mathematical Analysis using Functional Programming
- 2016
-
Ingår i: Electronic Proceedings in Theoretical Computer Science, EPTCS. - 2075-2180. ; 230, s. 1-15
-
Konferensbidrag (refereegranskat)abstract
- We present the approach underlying a course on Domain-Specific Languages of Mathematics, currently being developed at Chalmers in response to difficulties faced by third-year students in learning and applying classical mathematics (mainly real and complex analysis). The main idea is to encourage the students to approach mathematical domains from a functional programming perspective: to identify the main functions and types involved and, when necessary, to introduce new abstractions; to give calculational proofs; to pay attention to the syntax of the mathematical expressions; and, finally, to organise the resulting functions and types in domain-specific languages.
|
|
| 8. |
- Ionescu, Cezar, et al.
(författare)
-
Testing versus proving in climate impact research
- 2013
-
Ingår i: Leibniz International Proceedings in Informatics, LIPIcs. - 1868-8969. - 9783939897491 ; 19, s. 41-54
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 9. |
- Ionescu, Cezar, 1968, et al.
(författare)
-
Type theory as a framework for modelling and programming
- 2018
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. ; 11244:1, s. 119-133
-
Konferensbidrag (refereegranskat)abstract
- In the context provided by the proceedings of the UVMP track of ISoLA 2016, we propose Type Theory as a suitable framework for both modelling and programming. We show that it fits most of the requirements put forward on such frameworks by Broy et al. and discuss some of the objections that can be raised against it.
|
|
| 10. |
- Jansson, Patrik, 1972, et al.
(författare)
-
Domain-Specific Languages of Mathematics
- 2022
-
Bok (övrigt vetenskapligt/konstnärligt)abstract
- The main idea behind this book is to encourage readers to approach mathematical domains from a functional programming perspective: to identify the main functions and types involved and, when necessary, to introduce new abstractions; to give calculational proofs; to pay attention to the syntax of the mathematical expressions; and, finally, to organize the resulting functions and types in domain-specific languages. The book is recommended for developers who are learning mathematics and would like to use Haskell to make sense of definitions and theorems. It is also a book for the mathematically interested who wants to explore functional programming and domain-specific languages. The book helps put into perspective the domains of Mathematics and Functional Programming and shows how Computer Science and Mathematics are usefully taught together.
|
|
