Published on May 27, 2015

Over the last few days I wrote prover, a program that can reduce terms and prove equality in the untyped lambda calculus.

Such a tool ought to exist, but I couldn’t find anything like that.

Occasionally I want to prove stuff, such as `Monad`

or `Applicative`

laws for various types. Very seldom such proofs require induction; mostly they involve simple reductions and equational reasoning.

Sometimes I specifically want to do it in the untyped lambda calculus just to prove a point. Other times, I’m interested in a typed theory (say, System F as an approximation for Haskell). Fortunately, the subject reduction property guarantees us that the results proven in ULC will hold in System F just as well.

Algebraic datatypes are more tricky. From the practical perspective, I could add data declarations and case expressions to `prover`

, and desugar them via the Church encoding, just like I did with Maybe by hand. But there’s also the theoretical side of proving that the results about Church-encoded types translate back into the original language. Intuitively, that should hold, but I’d appreciate links to proper proofs if anyone is aware of them.

Finally, part of the motivation was to experiment with some pieces of Haskell tech that I don’t use in my day-to-day work and evaluate them. This part was certainly successful; I may share some specific impressions later. Until then, feel free to read the code; at this point it’s not too convoluted and yet I’m sure you’ll find some interesting bits there.

Here is an example invocation that establishes the right identity monad law for the reader monad:

```
% prover -i examples/reader.lam --equal 'bind a return' a
bind a return
{- inline bind -}
= (λb c d. c (b d) d) a return
{- inline return -}
= (λb c d. c (b d) d) a (λb c. b)
{- β-reduce -}
= (λb c. b (a c) c) (λb c. b)
{- β-reduce -}
= λb. (λc d. c) (a b) b
{- β-reduce -}
= λb. (λc. a b) b
{- β-reduce -}
= λb. a b
{- η-reduce -}
= a
```

The file `examples/reader.lam`

(included in the repository) contains the definitions of `return`

and `bind`

:

```
return = \x r. x ;
bind = \a k r. k (a r) r ;
```

You can also ask `prover`

to reduce an expression:

```
% prover -i examples/arith.lam --reduce 'mult two three'
λa b. a (a (a (a (a (a b)))))
```

Files are optional; you can give an entire term on the command line:

```
% prover --reduce '(\x. y x) (\z . z)'
y (λa. a)
```

`prover`

uses De Bruijn indices, so bound variable names are not preserved.

One thing to note is that right now `--reduce`

reports a fixed point of the reduction pipeline and not necessarily a normal form:

```
% prover --reduce '(\x. x x) (\x. x x)'
(λa. a a) (λa. a a)
```

If `prover`

can’t find a reduced form, it will say so:

```
% prover --reduce '(\x. x x) (\x. x x x)'
No reduced form found
```

`prover`

has a couple of knobs for more complicated cases. There is the number of iterations configured with `--fuel`

; and for the `--equal`

mode there is `--size-limit`

, which instructs the tool to ignore large terms. E.g. this invocation completes immediately:

```
% prover -i examples/pair.lam -i examples/bool.lam -i examples/arith.lam --reduce 'pred one'
λa b. b
```

But in order to get a nice proof for the same reduction, you’ll need to find the right limits and wait for about 7 seconds. You will also be surprised how non-trivial the proof is.

```
% prover -i examples/pair.lam -i examples/bool.lam -i examples/arith.lam \
--equal 'pred one' zero \
--fuel 50 --size-limit 40
pred one
{- inline pred -}
= (λa b c. snd (a (λd. pair true (fst d b (λe. e) (snd d))) (pair false c))) one
[...]
= λa b. pair true ((λc. c (λd e. e) b) (λc d. c) a (λc. c) ((λc. c (λd e. e) b) (λc d. d))) (λc d. d)
[...]
= λa b. b
zero
{- inline zero -}
= λa b. b
```

This is because `--equal`

has to consider all reduction paths to find the minimal one, and there are too many different ways to reduce this term.

Finally, its majesty factorial:

```
% prover -i examples/pair.lam -i examples/bool.lam -i examples/arith.lam -i examples/fixpoint.lam \
--fuel 20 \
--reduce 'fact three'
λa b. a (a (a (a (a (a b)))))
```

(I didn’t manage to compute `fact four`

, though.)