Posted in Code, Projects

The Real Theorem Generator: a Context Free Grammar

I should probably document the real origin of the Theorem of the Day and Philosophy of the Day. Coffee and Henry David Thoreau are perhaps less involved than originally indicated.

nothoreauThe theorem generator was written by a good friend of mine, Matt Gline, as a project for CS51: Abstraction and Design in Computer Programming, which we took together as freshmen.

The assignment was to use LISP to implement a context free grammar — basically a set of rules for computer-generated mad libs. The subject was whatever we wanted. Good ones from past years include computer-generated mystery novellas, course-guide reports, and performance art directions. Every year there’s a contest, and Matt’s theorem generator was hysterical enough to win him lunch at the faculty club.

Context-Free Grammars

Each rule in a context-free grammar consists of a term, and a set of choices for how to make that term. The choices can contain text, or other terms, or even refer recursively to the term being defined. For instance, a grammar like

nounphrase ::= <noun> | <adj> <adj> <noun> | super <nounphrase>
noun ::= apple | pear | mailman
adj ::= smelly | chartreuse | enormous

can produce phrases like “apple,” “enormous smelly mailman,” or “super super smelly chartreuse mailman.” The original grammars we wrote for CS51 were hundred-line clumps of LISP code that spit out un-punctuated paragraphs in all-caps. Over the years, my roommate Mike and I spiffed-up the theorem generator a bit, resulting in the current shiny ajax/latex version.

The current theorem grammar is defined in a grammar file (thm.gram) that looks like this

theorem ::= \begin{theorem}[<thname>]<thmstatement>.
          \end{theorem} \begin{proof} <proof>

proof ::= <statement>. <conclusion>. | See <citation>.
    | <statement>. <conclusion>. | <statement>. <conclusion>.

conclusion ::= 
    The result follows by d\'evissage | The theorem follows trivially
    | The conclusion is self-evident | Clearly, the theorem holds
    | We leave the rest as an exercise | This is the desired result
    | The rest follows from <citation> | QED
    | A simple application of <famoustheorem> completes the proof

famoustheorem ::=
    <mathguy>'s theorem
    | Hilbert's problem <nzdigit><zdigit>
    | the Riemann Hypothesis
    | Perelman's theorem (formerly the Poincar\'e Conjecture)
    | horizontal Iwasawa theory | Kummer theory | the different
    | Dynkin diagrams | Gegenbauer polynomials
    | trichotomy

A perl script (compile-grammar):

print "parsing grammar '$gram' into '$out.ml'...";
foreach (@entries) {
    s/\s* \# .* $//xmg;
    if (/\s*(\S*)\s*::=\s*(.*)/s) {
        $lhs = $1;
        $rhs = $2;

        if (!defined ($mainphrase)) {
            $mainphrase = $lhs;
            print OUT "let rec $lhs = Opts [|\n";
        } else {
            print OUT "and $lhs = Opts [|\n";

        @opts = split(/\s*\|\s*/, $rhs);
        foreach $opt (@opts) {
            print OUT "  [|";
            $opt =~ s/\s*\n\s*/ /g;

            # split just before < and after >

processes the grammar file and compiles it into OCaml code (thm.ml).

type phrase = Str of string | Opts of phrase array array

let _ = Random.self_init ()

let randelt a = a.(Random.int (Array.length a))
let rec print phr = match phr with
  Str  s       -> print_string s
| Opts options ->
    let parts = randelt options in
    Array.iter print parts

(* Grammar definitions *)
let rec top = Opts [|
  [| theorem;|];

and theorem = Opts [|
  [| Str "\\begin{theorem}["; thname; Str "]"; thmstatement; Str ". \\end{theorem} \\begin{proof} ";
 proof; Str " \\end{proof}";|];

This is almost certainly more elaborate than necessary, but OCaml is a lovely language for recursive structures, and the code is nice and simple. Running thm.ml spits out a ready-made LaTeX-ed theorem, which gets run through LaTeX to png, and cached, ready for viewing.

The Philosophy of the Day

My entry into the CS51 contest was a philosophy generator, which spits out semi-plausible definitions of philosophies from numerous cultural and intellectual traditions. It was never as clever as the theorem generator (which still cracks me up every time it produces anything attributed to Lipschitz), and the philosophies tend to involve concepts that are only of interest to nerdy Harvard freshmen. It’s still amusing, though. Here’s the grammar definition.

Have Fun!

The system I set up to create and run context-free grammars is pretty easy to use. Grammar files are simple to write, and from there all you need is compile-grammar and an OCaml installation. Here, once again, are the relevant files

  1. Some example grammar files: thm.gram, philo.gram
  2. Parse grammar files into ml code: compile-grammar

Anyone’s absolutely welcome to send extensions to thm.gram and philo.gram, or any new grammars you might write. I’ll ajaxify them and post them here, if you like. Have fun!

2 Responses to “The Real Theorem Generator: a Context Free Grammar” Comment Feed, Comments are closed.

  1. Jiang says: Dec 21, 2009 @ 6:31 am

    Thanks for this post. I love your concise yet readable format for specifying CFG’s, and have written a Python CFG class around it that works properly with philo.gram.

    My primary purpose was to generate words and names, so I needed to be able to specify the “empty” pseudo-character. My solution was to do a general search-and-replace for pseudo-nonterminals in the form of . Well, thanks again for this enlightening post. Awesome theorem generator ;p

  2. Trackback: Travels in a Mathematical World Jul 02, 2010 @ 5:13 am

    Carnival of Mathematics #67…

    Meanwhile, the Theorem of the Day generator is cooking up realistic looking ‘theorems’ and ‘proofs’ using a context free grammar….