Notes as slide-show pdfs

Theory of Computation

Definable (types-as-)closures in concurrent combinatory algebra

Dana Scott observed that in a particular model of lambda-calculus with join, the CCC of closures has a very rich structure, modelling polymorphic types, dependent types, subtyping and power-typing, a universal type, and --most importantly-- "atomic" types like unit and bool. We demonstrate that also in the term fragment of this model, these atoms are definable, but that they differ from those in the full model.

(2007:03, at Carnegie-Mellon's Math Logic Seminar)

Slides for online viewing, or without pauses for printing.

Mapping the space of Programs, Searching the space of Languages

Which programs are simple? Which programming languages are simple? We address these questions by considering the dual spaces of programs and languages:

• traversing the space of languages in search of useful languages,
• and building a large finite map of simple programs.

By treating the space of programs semantically, we can build much larger maps than would be possible treating programs syntactically. By restricting to a well-behaved class of languages (combinatory algebras), we can define a single space of programs across all languages. The space of languages then has very nice struture: it is a smooth manifold. We describe how to "fit" a language to training data in the form of useful or commonly-used programs.

(2007:07, at Stephen Wolfram's 2007 NKS Conference)

Slides and pretty datasets.

Models of randomness in programming languages

Part 1. Overview of randomness in programming languages. Probability valuations on topologies instead of measures on sigma-algebras. Plotkin's probabilistic powerdomain.

Part 2. Problems with randomness and parallelism. Lattice models and uncertainty. A lattice model with local probability spaces?

(2008:04, at Carnegie-Mellon's Math Logic Seminar)

Part 1: Slides for online viewing, or without pauses for printing.
Part 2: Slides for online viewing, or without pauses for printing.

References and Background Reading:

• Claire Jones. Probabilistic non-determinism. PhD thesis, Edinburgh, Scotland, UK, 1989 [ PS ]
• C. Jones and G. Plotkin. A probabilistic powerdomain of evaluations. In Proceedings of the Fourth Annual Symposium on Logic in computer science, pages 186-195, Piscataway, NJ, USA, 1989. IEEE Press. [ PDF ]
• A. Jung and R. Tix. The troublesome probabilistic powerdomain. In Third Workshop on Computation and Approximation, volume 13 of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 1998. [ PDF ]
• Reinhold Heckmann. Probabilistic Power Domains, Information Systems, and Locales. Lecture notes in computer science. Springer. [ PDF ]
• ...and Part 2 extends previous work described in the "definable closures" talk above.

Meaning in Mathematics --or-- Belief as Irrefutability

What mathematical statements are meaningful? What mathematical statements are true? Conservatively, only proven facts are true, only what can be deduced from assumptions. And assumptions come from science, the logic of what "might be true" and hasn't yet been falsified. Just as Godel's 1st Incompleteness Theorem limits how much can be proven, an analogous theorem limits what can be scientifically tested, ie how much can be meaningful.

In this talk, I will formulate the incompleteness theorems and discuss their relation to math and resp. science. I will also suggest some heuristics for guessing what "might be true" (step 1 in the scientific method) and prove that they are all doomed to fail.

(2008:10, at Carnegie-Mellon's Math Grad Student Seminar)

Slides for online viewing, or without pauses for printing.