2021 technical reports

CS-2021-01
Title Error Sensitive Multivariate Polynomial Interpolation
Authors Kirk Haller and Stephen Mann
Abstract 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.
Date May 14, 2021
Report CS-2021-01 (PDF)
CS-2021-02
Title Semantics and Contextual Equivalence for Probabilistic Programs with Nested Queries and Recursion
Authors Yizhou Zhang and Nada Amin
Abstract 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.
Date November 30, 2021
Report CS-2021-02 (PDF)