ﻻ يوجد ملخص باللغة العربية
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 Bellmans 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.
We consider a specific class of tree structures that can represent basic structures in linguistics and computer science such as XML documents, parse trees, and treebanks, namely, finite node-labeled sibling-ordered trees. We present axiomatizations o
We provide a computer verified exact monadic functional implementation of the Riemann integral in type theory. Together with previous work by OConnor, this may be seen as the beginning of the realization of Bishops vision to use constructive mathematics as a programming language for exact analysis.
This paper concerns the question to what extent it can be efficiently determined whether an arbitrary program correctly solves a given problem. This question is investigated with programs of a very simple form, namely instruction sequences, and a ver
We develop an approach to choice principles and their contrapositive bar-induction principles as extensionality schemes connecting an intensional or effective view of respectively ill-and well-foundedness properties to an extensional or ideal view of
Let S be a commutative semiring. M. Droste and P. Gastin have introduced in 2005 weighted monadic second order logic WMSOL with weights in S. They use a syntactic fragment RMSOL of WMSOL to characterize word functions (power series) recognizable by w