| 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) | |||