Why OCaml?

Since learning OCaml, after spending my career in languages like C/C++ and python, I have become enamored with OCaml and ML overall. I will try and share the source of my excitement in the following story, where I implement a reasoning framework for sentential logic in OCaml. If I really wanted to do this story justice I would have had a parallel experience in C or C++, but I don't have that much pain tolerance.

One evening, I was doing logic homework. The assignments involve proving statements in a formal proof system of sentential logic. The proof system (and when I say system I mean a series of rules and not a computer program) is designed to be mechanically applicable and decidable. In the sentential logic of formal proofs we have the following symbols that constitute a language:

  • Atomic sentences, denoted by A, B, C, etc…
  • Connectives, for now the two connectives we support are negation (~) and implication (->)

The language is pretty skeletal! The formal proof system starts you off with three axioms that are known to be true, and a single rule, modus ponens. Modus ponens specifies that if A is asserted to be true, and A -> B, then B is asserted to be true.

Creating these proofs generally involves tediously searching for applications of the axioms and statements proven so far to reach some kind of further conclusion which will eventually carry you towards the statement to be shown.

While I was working on this assignment, I asked myself: could I write a solver to do this work for me? Also, I asked "could I just feed my homework to the Z3 solver" and the answer is "yes" but I wanted to see how long it would take me to write a solver from scratch in OCaml.

It took about 2 hours and I attribute this entirely to the power of OCaml. The code includes a parser and grammar for the sentential logic as well as some basic solving and searching tactics to go from a set of facts to a proof of a terminal statement. The solver works 'forwards', and is pretty basic.

So, what does the code looks like? My implementation is here.

First, we define an Abstract Syntax Tree (AST) data structure to hold statements in sentential logic. Statements will look like this:

type expr =
    | AtomicSentence of char
    | Negation of expr
    | Implication of expr*expr

Note how the definition of the 'expr' type is recursive such that an Expr is an Implication that has two exprs. Each expr could then in turn be atomic sentences, negations, or implications. hooray recursion!

We'll also define a proof environment, that being, a set of statements that we have proven / rely on, and the proof goal:

type proof_environment =
        proven_statements : expr list;
        statement_to_show : expr;

Sweet! So this just says that we have a list of expressions and then an expression that we are trying to work towards. This is just plumbing.

alright, now the parser. I want to turn strings like the above into structures like the above. What does this look like? using ocamllex and ocamlyacc we wind up with a token definition and grammar specification as follows:


 open Parser
 exception Eof
rule token = parse
  [' ' '\t' '\n' '\r']  { token lexbuf }
| '(' { LP }
| '.' { DOT }
| ')' { RP }
| "->" { ARROW }
| ['A'-'Z'] as lxm { ID(lxm) }
| "~" { NEGATE }
| eof { EOF }
| _ as lxm { Printf.printf "Illegal character %c" lxm; failwith "Bad input" }

The parser skips newlines, tabs, whitespaces, and we define our tokens.


      open Ast

%token <char> ID
%start proof_env
%start expr
%type <Ast.expr list> expr_list
%type <Ast.expr> expr
%type <Ast.proof_environment> proof_env

ID { AtomicSentence($1) }
| LP expr RP { $2 }
| LP expr RP ARROW expr { Implication($2,$5) }
| NEGATE expr { Negation($2) }

DOT { [] }
| expr expr_list { $1::$2 }

    expr_list expr EOF { { proven_statements=$1; statement_to_show=$2 } }

We define an expr as something that can be an ID, or itself encased in parens, or a negation. I've gone to some tricks here to remove shift/reduce conflicts but the real meat is on the 5 lines of the expr: grammar.

How does our OCaml code use this grammar to parse a file?

let parse_file name : proof_environment =
    let chan = open_in name in
    let lexbuf = Lexing.from_channel chan in
    let p = Parser.proof_env Lexer.token lexbuf in
    close_in chan;

This is function that goes from a string to a proof_environment. It passes the contents of the file to the generated parser which then parses it and turns it into a proof environment. And that's it! We don't need to worry about parsing any more. We can suck in text that specifies sentences in sentential logic and have them in a recursive, tree-based data type that we defined.

Alright, so what next? Well, we can implement a very simple solving strategy that says, effectively, "try and perform modus ponens over and over until either you can't or we arrive at the answer". So what does an application of modus ponens look like in this framework?

let apply_mp (env:proof_environment) (e:expr) : expr = match e with
    | Implication(a,b) ->
        if List.mem a env.proven_statements then b else e
    | Negation _ | AtomicSentence _ -> e

So what does apply_mp do? Well, we go from a proof_environment and an expr to an expr. lets dig into the first line a bit:

= match e with
    | Implication(a,b) ->

This shows off some of the power of the type system. When we say 'match X with' we can demand a specification. It's like asking a class its subtype, we know that this value is an expression, but is it an Implication, a Negation, or an AtomicSentence? In apply_mp, we only care about Implications since those are the only statements we can affect. If it is anything else, we hit the case at the bottom described by:

| Negation _ | AtomicSentence _ -> e

And this says "if the type of expr is not an Implication, evaluate to the expr argument", aka do nothing. So something like

apply_mp (A)

would evaluate to (A) again.

So what happens if it's an Implication? We check the proof_environments list of proven_statements to see if the left hand side of the Implication has at any point before been proven. If it has, we will evaluate just to the right hand side. if it hasn't, we just evaluate to the expression again.

The expr in the base case will be something like (A)->(B). It could be simpler, like (A), but that is not of type Implication so we would just evaluate to the expr again.

So if we have an environment where we know A, and we say A->B, then that expression will fold down to B.

And this is it! then we have some plumbing logic which is boring that will just iterate over all of the rules and try to apply MP until it gets the answer or it can't try anything else, and we describe a proof to it, and watch it construct the proof:

The proof input looks like this:

$ cat example_1
( A ) -> ( ( B )->( A ) )
( ( A ) -> ( (B) -> (C) ) ) -> ( ( (A) -> (B) ) -> ( (A) -> (C) ) )
(~(A) -> (B) ) -> (( ~(A) -> ~(B) ) -> (A) )
( A ) -> ( B )
( A ) -> (( (B) -> (C) ))
. ( (A) -> (C) )

Where the first three lines are the axioms given in the system of formal proofs, the next two are given in the context of the particular proof problem, and then the last line is the line that we have to show. So, we run the solver:

$ ./awsolve example_1
Starting with proof environment:
(A) -> ((B) -> (A))
((A) -> ((B) -> (C))) -> (((A) -> (B)) -> ((A) -> (C)))
(~((A) -> (B))) -> ((~((A) -> (~(B)))) -> (A))
(A) -> (B)
(A) -> ((B) -> (C))
. (A) -> (C)
Beginning solving...

(A) -> ((B) -> (A))
((A) -> ((B) -> (C))) -> (((A) -> (B)) -> ((A) -> (C)))
(~((A) -> (B))) -> ((~((A) -> (~(B)))) -> (A))
(A) -> (B)
(A) -> ((B) -> (C))
. (A) -> (C)

(A) -> ((B) -> (A))
((A) -> ((B) -> (C))) -> (((A) -> (B)) -> ((A) -> (C)))
(~((A) -> (B))) -> ((~((A) -> (~(B)))) -> (A))
(A) -> (B)
(A) -> ((B) -> (C))
((A) -> (B)) -> ((A) -> (C))
. (A) -> (C)

(A) -> ((B) -> (A))
((A) -> ((B) -> (C))) -> (((A) -> (B)) -> ((A) -> (C)))
(~((A) -> (B))) -> ((~((A) -> (~(B)))) -> (A))
(A) -> (B)
(A) -> ((B) -> (C))
((A) -> (B)) -> ((A) -> (C))
(A) -> (C)
. (A) -> (C)

And it shows it! Welcome to having (the beginning of) your very own mechanical proof framework!

You can see from the output at each stage the statements it adds and the discoveries the search makes. It goes like this:

  1. (A) -> ((B) -> (C))
  2. ((A) -> (B)) -> ((A) -> (C))
  3. (A) -> (C)

This is a very very simple search that only rarely works. Incompleteness shows/proves that I can't construct an algorithm that will work for every set of axioms / given statements (and exactly what that means, I'm still learning).

But enough math! This was all done with a little OCaml! Bask in the power! It actually took longer to write this post than it did to write the code.

Of course, my friend Kris did this when he was 16 or so, and implemented most of the "state of the art" as it comes to solvers in SML. So this is still coloring with crayons to a large degree, in terms of cracking solver state of the art. But I think that this is still a pretty decent case study in why ML is a good language!