|Error Sensitive Multivariate Polynomial Interpolation
|Kirk Haller and Stephen Mann
|In this paper, we make a strong connection between algebraic geometry and interpolation. In particular, we use algebraic geometry tools to develop a machinery for the analysis of Newton or nested multivariate interpolation schemes. The main practical result coming out of our analysis is that for robustness, one should replace the condition of minimal degree with a minimally complete condition that is introduced in this paper. We show how to construct minimally complete schemes and provide examples.
|May 14, 2021
|Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and Recursion
|Yizhou Zhang and Nada Amin
|Metareasoning can be achieved in probabilistic programming languages (PPLs) using agent models that recursively nest inference queries inside inference queries. However, the semantics of this powerful, reflection-like language feature has defied an operational treatment, much less reasoning principles for contextual equivalence.
We give formal semantics to a core PPL with continuous distributions, scoring, general recursion, and nested queries. Unlike prior work, the presence of nested queries and general recursion makes it impossible to stratify the definition of a sampling-based operational semantics and that of a measure-theoretic semantics—the two semantics must be defined mutually recursively. A key yet challenging property we establish is that probabilistic programs have well-defined meanings: limits exist for the step-indexed measures they induce.
Beyond a semantics, we offer relational reasoning principles for probabilistic programs making nested queries. We construct a step-indexed, biorthogonal logical-relations model. A soundness theorem establishes that logical relatedness implies contextual equivalence. We demonstrate the usefulness of the reasoning principles by proving novel equivalences of practical relevance—in particular, game-playing and decision-making agents. We mechanize our technical developments leading to the soundness proof using the Coq proof assistant. Nested queries are an important yet theoretically underdeveloped linguistic feature in PPLs; we are first to give them semantics in the presence of general recursion and to provide them with sound reasoning principles for contextual equivalence.
|November 30, 2021