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


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 Π2-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.


  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       = {},
  pdf       = {},
  topics    = {automated deduction, lambda-calculus, Bayesian inference},