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.