Automated Equational Reasoning in Nondeterministic λCalculi Modulo Theories H^{*}
Ph.D. Thesis of Fritz Obermeyer
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 fewthousand programsmoduloequivalence, for use in Bayesian inference.
Johann implements saturationbased 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).
 Datadriven 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 datadriven automated conjecturing.
 Foundations of Math

Although the KolmogorovChaitinSolomonoff 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 = {CarnegieMellon University},
address = {Pittsburgh, PA, USA},
url = {http://fritzo.org/thesis},
pdf = {http://fritzo.org/thesis.pdf},
topics = {automated deduction, lambdacalculus, Bayesian inference},
}