Announcing lambda prover

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

Motivation

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.

Demo

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.)