In verified generic programming, one cannot exploit the structure of concrete data types but has to rely on well chosen sets of specifications or abstract data types (ADTs). Functors and monads are at the core of many applications of functional programming. This raises the question of what useful ADTs for verified functors and monads could look like. The functorial map of many important monads preserves extensional equality. For instance, if $f, g : A \rightarrow B$ are extensionally equal, that is, $\forall x \in A, \ f \ x = g \ x$, then $map \ f : List \ A \rightarrow List \ B$ and $map \ g$ are also extensionally equal. This suggests that preservation of extensional equality could be a useful principle in verified generic programming. We explore this possibility with a minimalist approach: we deal with (the lack of) extensional equality in Martin-L\"of's intensional type theories without extending the theories or using full-fledged setoids. Perhaps surprisingly, this minimal approach turns out to be extremely useful. It allows one to derive simple generic proofs of monadic laws but also verified, generic results in dynamical systems and control theory. In turn, these results avoid tedious code duplication and ad-hoc proofs. Thus, our work is a contribution towards pragmatic, verified generic programming.
相關內容
Friedman's chi-square test is a non-parametric statistical test for $r\geq2$ treatments across $n\ge1$ trials to assess the null hypothesis that there is no treatment effect. We use Stein's method with an exchangeable pair coupling to derive an explicit bound on the distance between the distribution of Friedman's statistic and its limiting chi-square distribution, measured using smooth test functions. Our bound is of the optimal order $n^{-1}$, and also has an optimal dependence on the parameter $r$, in that the bound tends to zero if and only if $r/n\rightarrow0$. From this bound, we deduce a Kolmogorov distance bound that decays to zero under the weaker condition $r^{1/2}/n\rightarrow0$.
This work proposes a fast iterative method for local steric Poisson--Boltzmann (PB) theories, in which the electrostatic potential is governed by the Poisson's equation and ionic concentrations satisfy equilibrium conditions. To present the method, we focus on a local steric PB theory derived from a lattice-gas model, as an example. The advantages of the proposed method in efficiency lies on a key idea that ionic concentrations as scalar implicit functions of the electrostatic potential, i.e, generalized Boltzmann distributions, are numerically available. The existence, uniqueness, boundness, and smoothness of such distributions are rigorously established. A Newton iteration method with truncation is proposed to solve a nonlinear system discretized from the generalized PB equations. The existence and uniqueness of the solution to the discretized nonlinear system are established by showing that it is a unique minimizer of a constructed convex energy. Thanks to the boundness of ionic concentrations, truncation bounds for the potential are obtained by using the extremum principle. The truncation step in iterations is shown to be energy, residual, and error decreasing. To further speed-up computations, we propose a novel precomputing-interpolation strategy, which is applicable to other local steric PB theories and makes the proposed methods for solving steric PB theories as efficient as for solving the classical PB theory. Analysis on the Newton iteration method with truncation shows local quadratic convergence for the proposed numerical methods. Applications to realistic biomolecular solvation systems reveal that counterions with steric hindrance stratify in an order prescribed by the parameter of ionic valence-to-volume ratio. Finally, we remark that the proposed iterative methods for local steric PB theories can be readily incorporated in well-known classical PB solvers.
Several formal systems, such as resolution and minimal model semantics, provide a framework for logic programming. In this paper, we will survey the use of structural proof theory as an alternative foundation. Researchers have been using this foundation for the past 35 years to elevate logic programming from its roots in first-order classical logic into higher-order versions of intuitionistic and linear logic. These more expressive logic programming languages allow for capturing stateful computations and rich forms of abstractions, including higher-order programming, modularity, and abstract data types. Term-level bindings are another kind of abstraction, and these are given an elegant and direct treatment within both proof theory and these extended logic programming languages. Logic programming has also inspired new results in proof theory, such as those involving polarity and focused proofs. These recent results provide a high-level means for presenting the differences between forward-chaining and backward-chaining style inferences. Anchoring logic programming in proof theory has also helped identify its connections and differences with functional programming, deductive databases, and model checking.
We study random graphs with latent geometric structure, where the probability of each edge depends on the underlying random positions corresponding to the two endpoints. We focus on the setting where this conditional probability is a general monotone increasing function of the inner product of two vectors; such a function can naturally be viewed as the cumulative distribution function of some independent random variable. We consider a one-parameter family of random graphs, characterized by the variance of this random variable, that smoothly interpolates between a random dot product graph and an Erd\H{o}s--R\'enyi random graph. We prove phase transitions of detecting geometry in these graphs, in terms of the dimension of the underlying geometric space and the variance parameter of the conditional probability. When the dimension is high or the variance is large, the graph is similar to an Erd\H{o}s--R\'enyi graph with the same edge density that does not possess geometry; in other parameter regimes, there is a computationally efficient signed triangle statistic that distinguishes them. The proofs make use of information-theoretic inequalities and concentration of measure phenomena.
Some of today's greatest challenges in urban environments concern individual mobility and rapid parcel delivery. Given the surge of e-commerce and the ever-increasing volume of goods to be delivered, we explore possible logistic solutions by proposing algorithms to add parcel-transport services to ride-hailing systems. Toward this end, we present and solve mixed-integer linear programming (MILP) formulations of the share-a-ride problem and quantitatively analyze the service revenues and use of vehicle resources. We create five scenarios that represent joint transportation situations for parcels and people, and that consider different densities in request types and different requirements for vehicle resources. For one scenario, we propose an alternative MILP formulation that significantly reduces computation times. The proposed model also improves scalability by solving instances with 260% more requests than those solved with general MILP. The results show that the greatest profit margins occur when several parcels share trips with customers. In contrast, with all metrics considered, the worst results occur when parcels and people are transported in separate dedicated vehicles. The integration of parcel services in ride-hailing systems also reduces vehicle waiting times when the number of parcel requests exceeds the number of ride-hailing customers.
We propose the first non-trivial generic decoding algorithm for codes in the sum-rank metric. The new method combines ideas of well-known generic decoders in the Hamming and rank metric. For the same code parameters and number of errors, the new generic decoder has a larger expected complexity than the known generic decoders for the Hamming metric and smaller than the known rank-metric decoders. Furthermore, we give a formal hardness reduction, providing evidence that generic sum-rank decoding is computationally hard. As a by-product of the above, we solve some fundamental coding problems in the sum-rank metric: we give an algorithm to compute the exact size of a sphere of a given sum-rank radius, and also give an upper bound as a closed formula; and we study erasure decoding with respect to two different notions of support.
Road networks exist in the form of polylines with attributes within the GIS databases. Such a representation renders the geographic data impracticable for 3D road traffic simulation. In this work, we propose a method to transform raw GIS data into a realistic, operational model for real-time road traffic simulation. For instance, the proposed raw to simulation ready data transformation is achieved through several curvature estimation, interpolation/approximation, and clustering schemes. The obtained results show the performance of our approach and prove its adequacy to real traffic simulation scenario as can be seen in this video 1 .
Controllers for autonomous systems that operate in safety-critical settings must account for stochastic disturbances. Such disturbances are often modelled as process noise, and common assumptions are that the underlying distributions are known and/or Gaussian. In practice, however, these assumptions may be unrealistic and can lead to poor approximations of the true noise distribution. We present a novel planning method that does not rely on any explicit representation of the noise distributions. In particular, we address the problem of computing a controller that provides probabilistic guarantees on safely reaching a target. First, we abstract the continuous system into a discrete-state model that captures noise by probabilistic transitions between states. As a key contribution, we adapt tools from the scenario approach to compute probably approximately correct (PAC) bounds on these transition probabilities, based on a finite number of samples of the noise. We capture these bounds in the transition probability intervals of a so-called interval Markov decision process (iMDP). This iMDP is robust against uncertainty in the transition probabilities, and the tightness of the probability intervals can be controlled through the number of samples. We use state-of-the-art verification techniques to provide guarantees on the iMDP, and compute a controller for which these guarantees carry over to the autonomous system. Realistic benchmarks show the practical applicability of our method, even when the iMDP has millions of states or transitions.
In this paper, from a theoretical perspective, we study how powerful graph neural networks (GNNs) can be for learning approximation algorithms for combinatorial problems. To this end, we first establish a new class of GNNs that can solve strictly a wider variety of problems than existing GNNs. Then, we bridge the gap between GNN theory and the theory of distributed local algorithms to theoretically demonstrate that the most powerful GNN can learn approximation algorithms for the minimum dominating set problem and the minimum vertex cover problem with some approximation ratios and that no GNN can perform better than with these ratios. This paper is the first to elucidate approximation ratios of GNNs for combinatorial problems. Furthermore, we prove that adding coloring or weak-coloring to each node feature improves these approximation ratios. This indicates that preprocessing and feature engineering theoretically strengthen model capabilities.
In this paper, we study the optimal convergence rate for distributed convex optimization problems in networks. We model the communication restrictions imposed by the network as a set of affine constraints and provide optimal complexity bounds for four different setups, namely: the function $F(\xb) \triangleq \sum_{i=1}^{m}f_i(\xb)$ is strongly convex and smooth, either strongly convex or smooth or just convex. Our results show that Nesterov's accelerated gradient descent on the dual problem can be executed in a distributed manner and obtains the same optimal rates as in the centralized version of the problem (up to constant or logarithmic factors) with an additional cost related to the spectral gap of the interaction matrix. Finally, we discuss some extensions to the proposed setup such as proximal friendly functions, time-varying graphs, improvement of the condition numbers.
小貼士
登錄享
注冊地址： 北京市海淀區羊坊店路18號2幢3層301-191