Automated Equational Reasoning in Nondeterministic λ-Calculi Modulo Theories H^*
Ph.D. Thesis of Fritz Obermeyer

Abstract Motivation Thesis Defense Software GitHub

Topics

Bayesian inference of probabilistic programs

The practical motivation of this thesis was to implement Bayesian inference over a space of programs in some programming language. The resulting software system Johann implements Bayesian inference of functional programs as well as emprical Bayes learning of a PCFG for functional programs.

Automated deduction and verification

The bulk of effort in Johann was to enumerate the first few-thousand programs-modulo-equivalence, for use in Bayesian inference. Johann implements saturation-based equational theorem proving for various fragments of untyped λ-calculi. This theorem prover is used to formally verify much of the thesis.

λ-Calculus theories and extensions

Since typed programming languages have some advantages over untyped langauges, this thesis develops/discovers a novel interpretation of typed λ-calculus into untyped λ-calculus with joins (for indeterminism/ambiguity).

Data-driven conjecturing in undecidable theories

The optimal equivalence relation for Bayesian inference is the maximally coarse theory H^*; however, this theory is undecidable, in fact Π₂-complete. Nevertheless, in practice Johann can decide over 90% of equations among the first 10000 equivalence classes, using a combination of saturated deduction and data-driven automated conjecturing.

Foundations of Math

Although the Kolmogorov-Chaitin-Solomonoff definition of complexity suggests that the universal Bayesian priors should favor constructive concepts with short programs, we know from experience that implicit definitions are also useful: simple concepts may reference our collective mathematical knowledge without incurring complexity cost. Thus this thesis develops a λ-calculus foundation for predicative mathematics, in which implicit definitions may factor into Bayesian priors.

Bibtex

@phdthesis{Obermeyer09,
  author    = {Obermeyer, Fritz},
  title     = {Automated equational reasoning in nondeterministic $lambda$-calculi modulo theories $H^*$},
  year      = {2009},
  publisher = {Carnegie-Mellon University},
  address   = {Pittsburgh, PA, USA},
  url       = {http://fritzo.org/thesis},
  pdf       = {http://fritzo.org/thesis.pdf},
  topics    = {automated deduction, lambda-calculus, Bayesian inference},
}