Higher-Order Decision Theory
This paper investigates a surprising relationship between decision theory and proof theory. Using constructions originating in proof theory based on higher-order functions, so called quantifiers and selection functions, we show that these functionals mode
- PDF / 202,953 Bytes
- 14 Pages / 439.37 x 666.142 pts Page_size
- 7 Downloads / 237 Views
Department of Computer Science, University of Oxford, Oxford, UK [email protected] 2 Department of Electronic Engineering and Computer Science, Queen Mary University of London, London, UK [email protected] 3 Department of Economics, University of Mannheim, Mannheim, Germany [email protected] 4 OICOS GmbH, Mannheim, Germany [email protected] 5 Department of Economics, University of St. Gallen, St. Gallen, Switzerland [email protected]
Abstract. This paper investigates a surprising relationship between decision theory and proof theory. Using constructions originating in proof theory based on higher-order functions, so called quantifiers and selection functions, we show that these functionals model choice behavior of individual agents. Our framework is expressive, it captures classical theories such as utility functions and preference relations but it can also be used to faithfully model abstract goals such as coordination. It is directly implementable in functional programming languages. Lastly, modeling an agent with selection functions and quantifiers is modular and thereby allows to seamlessly combine agents bridging decision theory and game theory. Keywords: Decision theory order functions · Quantifiers
1
· Utility functions · Preferences · Higher-
Introduction
A higher-order function (or functional ) is a function whose domain is itself a set of functions. In this paper we investigate a surprising and deep connection between decision theory on one side and a higher-order construction that originated in proof theory [3,4] on the other side: We use a particular class of higher-order functions as a way of describing the choice behavior of individual agents. Assume X is the overall set of alternatives, and R a set of observable outcomes or measures. For instance, X could be the set of all books, and R = R+ the nonnegative reals representing prices. We then see functions of type X → R as describing the agent’s decision context, e.g. X → R+ as the mapping from books to prices. c Springer International Publishing AG 2017 J. Rothe (Ed.): ADT 2017, LNAI 10576, pp. 241–254, 2017. DOI: 10.1007/978-3-319-67504-6 17
242
J. Hedges et al.
The core idea we explore here is to model agents’ decision goals as higherorder functions of type (X → R) → R. Functionals of this type have been called quantifiers [14], since the standard ∃ and ∀ logical quantifiers are particular cases of these when R = B is the type of booleans. Going back to the example of books and prices, an agent who prefers the cheapest book will be modeled by the quantifier min : (X → R+ ) → R+ saying that given any catalogue of prices p : X → R+ the agent will choose to pay the cheapest price on the catalogue min(p). Therefore, quantifiers describe the outcome (e.g. price paid for the choice of book) an agent considers to be good in any given decision context. A corresponding notion is that of a selection function, i.e. a higher-order function of type (X → R) → X which calculates a concrete choice that meets the desired goal
Data Loading...
