Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userOn the correctness of monadic backward induction
149
0
0.0
(
0
)
Added by
Nicola Botta
Publication date
2020
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic 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 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.
rate research
Read More
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 of the monadic second-order logic (MSO), monadic transitive closure logic (FO(TC1)) and monadic least fixed-point logic (FO(LFP1)) theories of this class of structures. These logics can express important properties such as reachability. Using model-theoretic techniques, we show by a uniform argument that these axiomatizations are complete, i.e., each formula that is valid on all finite trees is provable using our axioms. As a backdrop to our positive results, on arbitrary structures, the logics that we study are known to be non-recursively axiomatizable.
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 very simple problem, namely the non-zeroness test on natural numbers. The instruction sequences concerned are of a kind by which, for each $n > 0$, each function from ${0,1}^n$ to ${0,1}$ can be computed. The established results include the time complexities of the problem of determining whether an arbitrary instruction sequence correctly implements the restriction to ${0,1}^n$ of the function from ${0,1}^*$ to ${0,1}$ that models the non-zeroness test function, for $n > 0$, under several restrictions on the arbitrary instruction sequence.
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 these properties. After classifying and analysing the relations between different intensional definitions of ill-foundedness and well-foundedness, we introduce, for a domain $A$, a codomain $B$ and a filter $T$ on finite approximations of functions from $A$ to $B$, a generalised form GDC$_{A,B,T}$ of the axiom of dependent choice and dually a generalised bar induction principle GBI$_{A,B,T}$ such that: GDC$_{A,B,T}$ intuitionistically captures the strength of $bullet$ the general axiom of choice expressed as $forall aexists b R(a, b) Rightarrowexistsalphaforall alpha R(alpha,alpha(a))$ when $T$ is a filter that derives point-wise from a relation $R$ on $A times B$ without introducing further constraints, $bullet$ the Boolean Prime Filter Theorem / Ultrafilter Theorem if $B$ is the two-element set $mathbb{B}$ (for a constructive definition of prime filter), $bullet$ the axiom of dependent choice if $A = mathbb{N}$, $bullet$ Weak K{o}nigs Lemma if $A = mathbb{N}$ and $B = mathbb{B}$ (up to weak classical reasoning) GBI$_{A,B,T}$ intuitionistically captures the strength of $bullet$ G{o}dels completeness theorem in the form validity implies provability for entailment relations if $B = mathbb{B}$, $bullet$ bar induction when $A = mathbb{N}$, $bullet$ the Weak Fan Theorem when $A = mathbb{N}$ and $B = mathbb{B}$. Contrastingly, even though GDC$_{A,B,T}$ and GBI$_{A,B,T}$ smoothly capture several variants of choice and bar induction, some instances are inconsistent, e.g. when $A$ is $mathbb{B}^mathbb{N}$ and $B$ is $mathbb{N}$.
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 weighted automata, where the semantics of quantifiers is used both as arithmetical operations and, in the boolean case, as quantification. Already in 2001, B. Courcelle, J.Makowsky and U. Rotics have introduced a formalism for graph parameters definable in Monadic Second order Logic, here called MSOLEVAL with values in a ring R. Their framework can be easily adapted to semirings S. This formalism clearly separates the logical part from the arithmetical part and also applies to word functions. In this paper we give two proofs that RMSOL and MSOLEVAL with values in S have the same expressive power over words. One proof shows directly that MSOLEVAL captures the functions recognizable by weighted automata. The other proof shows how to translate the formalisms from one into the other.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
