Michael Wolman's Home Page
I am a third year graduate student at Caltech studying mathematical logic and descriptive set theory. My supervisor is Alexander Kechris.
Contact me: mwolman ~at~ caltech ~dot~ edu
Papers
-
Probabilistic programming semantics for name generation, joint with Marcin Sabok, Sam Staton and Dario Stein, Proc. ACM Program. Lang. 5, POPL, Article 11 (January 2021). [pdf, arxiv, doi]
Abstract
We make a formal analogy between random sampling and fresh name generation. We show that quasi-Borel spaces, a model for probabilistic programming, can soundly interpret the đ-calculus, a calculus for name generation. Moreover, we prove that this semantics is fully abstract up to first-order types. This is surprising for an âoff-the-shelfâ model, and requires a novel analysis of probability distributions on function spaces. Our tools are diverse and include descriptive set theory and normal forms for the đ-calculus.
-
Abstractness of the nu-calculus in quasi-Borel spaces at first-order types, Master's thesis, 2020. Supervised by Marcin Sabok and Prakash Panangaden. [pdf, McGill library]
Abstract
The nu-calculus is a simply typed, higher-order, call-by-value language that models fresh name generation [PS93]. In this language, names can be checked for equality and newly generated names are guaranteed to be distinct from all others.
In this thesis, we show that we can interpret names to be elements of a probability space, modelling fresh name generation as sampling names from a continuous measure. Specifically, we show that the nu-calculus can be soundly interpreted in the category of quasi-Borel spaces, a recent construction providing a model of higher-order probabilistic programming [Heu+17].
We then provide a novel analysis of higher-order functions in both the nu-calculus and the category of quasi-Borel spaces. In the nu-calculus, we construct a normal form for terms at first-order types eliminating the use of private names. We then analyze the structure of higher-order quasi-Borel spaces to prove that our semantics are abstract at first-order types.
Le nu-calcul est un langage simplement typĂ©, dâordre supĂ©rieur, appel par valeur qui modĂ©lise la gĂ©nĂ©ration de noms frais [PS93]. Dans ce langage, lâĂ©galitĂ© des noms peut ĂȘtre vĂ©rifiĂ© et les noms nouvellement gĂ©nĂ©rĂ©s sont garantis dâĂȘtre distincts de tous les autres.
Dans cette thĂšse, nous montrons que nous pouvons interprĂ©ter les noms comme des Ă©lĂ©ments dâun espace de probabilitĂ©, modĂ©lisant la gĂ©nĂ©ration de noms frais comme Ă©chantillonnage de noms Ă partir dâune mesure continue. Plus prĂ©cisĂ©ment, nous montrons que le nu-calcul peut ĂȘtre correctement interprĂ©tĂ© dans la catĂ©gorie dâespaces quasi-borĂ©liennes, une construction rĂ©cente fournissant un modĂšle de programmation probabiliste dâordre supĂ©rieure [Heu+17].
Nous fournissons ensuite une nouvelle analyse de fonctions dâordre supĂ©rieur, Ă la fois dans le nu-calcul et dans la catĂ©gorie des espaces quasi-borĂ©liennes. Dans le nu-calcul, nous construisons une forme normale pour les termes de types de premier ordre, Ă©liminant lâutilisation de noms privĂ©s. Nous analysons ensuite la structure des espaces quasi-borĂ©liennes dâordre supĂ©rieur pour prouver que notre sĂ©mantique est abstraite aux types du premier ordre.
Notes
-
An effective version of Nadkarni's Theorem, joint with Alexander Kechris. [pdf]
Abstract
Nadkarniâs Theorem asserts that for a countable Borel equivalence relation (CBER) exactly one of the following holds: (1) It has an invariant Borel probability measure or (2) it admits a Borel compression, i.e., a Borel injection that maps each equivalence class to a proper subset of it. An effective version of Nadkarniâs Theorem was included in Ditzenâs unpublished PhD thesis [D], where it is shown that if a CBER is effectively Borel, then either alternative (1) above holds or else it admits an effectively Borel compression. In his thesis, Ditzen also proves an effective version of the Ergodic Decomposition Theorem. These notes contain an exposition of these results. We include Ditzenâs proof of the Effective Nadkarniâs Theorem, and use this construction to provide a different proof of the Effective Ergodic Decomposition Theorem. In addition, we construct a counterexample to show that alternative (1) above does not admit an effective version.
