For testing automated theorem provers we have Seventy-Five Problems for Testing Automatic Theorem Provers by Pelletier.

Are there any such standard/well regarded tests for a λ-calculus that verify the evaluation?


The best λ-Calculus evaluator I have found so far is:

Lambda calculus reduction workbench with info here.

I like this one because
1. It is a working example that seems to corretly pass every example I can find.
2. Has a trace option for the output.
3. Can do multiple reduction strategies
* normal order
* call-by-name
* head spine reduction
* call-by-value
* applicative order
* hybrid normal order
* hybrid applicative order
4. Has a list of pre defined abbreavtions such as
* S, K, I
* 0 - 5
* pair
* pred
* succ
* add
* mul
5. Has source code in SML

  • $\begingroup$ What would you like to test? Whether the evaluation works correctly? These days cool people prove it works using a theorem prover (which uses $\lambda$-calculus underneath...) $\endgroup$ Jan 17 '13 at 22:15
  • $\begingroup$ @AndrejBauer Yes I would like to verify that the evaluation works correctly for my implementation of a λ-calculus. Which theorem prover(s) are you refering to that use λ-calculus underneath? Some of us recently did this and it did not use λ-calculus. $\endgroup$
    – Guy Coder
    Jan 18 '13 at 0:16
  • $\begingroup$ Coq would be an obvious one. Just implement Church numerals and compute $6 \times 7$. You know the answer. $\endgroup$ Jan 18 '13 at 7:55
  • 1
    $\begingroup$ I am not suggesting that you do it in Coq. I am suggesting that you write a program in lambda calculus which computes $6 \times 7$ using Church numerals. If you're up to implementing lambda calculus, this would be an easy exercise. $\endgroup$ Jan 19 '13 at 11:00
  • 2
    $\begingroup$ Pelletier problems test the power of ATP systems. Nowadays it is tested against TPTP. Implementation correctness is a different story. You could test random formulas against a known good implementation. $\endgroup$ Jan 20 '13 at 14:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.