Proving a theorem in intuitionistic propositional logic, with implication as its single connective, is known as one of the simplest to state PSPACE-complete problem. At the same time, via the Curry-Howard isomorphism, it is instrumental to find lambda terms that may inhabit a given type.
However, as hundreds of papers witness it, all starting with Gentzen’s LJ calculus, conceptual simplicity has not come in this case with comparable computational counterparts. Implementing such theorem provers faces challenges related not only to soundness and completeness but also too termination and scalability problems.
In search for an efficient but minimalist theorem prover, on the two sides of the Curry-Howard isomorphism, we design a combinatorial testing framework using types inferred for lambda terms as well as all-term and random term generators.
We choose Prolog as our meta-language. Being derived from essentially the same formalisms as those we are covering, it reduces the semantic gap and results in surprisingly concise and efficient declarative implementations. Our implementation is available at: https://github.com/ptarau/TypesAndProofs.
Curry-Howard isomorphism Propositional implicational intuitionistic logic Type inference and type inhabitation Simply typed lambda terms Logic programming Propositional theorem provers Combinatorial testing algorithms
This is a preview of subscription content, log in to check access.
This research has been supported by NSF grant 1423324. We thank the reviewers of PADL’19 for their constructive comments and suggestions for improvement.
Howard, W.: The formulae-as-types notion of construction. In: Seldin, J., Hindley, J. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479–490. Academic Press, London (1980)Google Scholar
Bendkowski, M., Grygiel, K., Tarau, P.: Random generation of closed simply typed \(\lambda \)-terms: a synergy between logic programming and Boltzmann samplers. TPLP 18(1), 97–119 (2018)MathSciNetzbMATHGoogle Scholar
Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of haskell programs. SIGPLAN Not. 46(4), 53–64 (2011)CrossRefGoogle Scholar
Palka, M.H., Claessen, K., Russo, A., Hughes, J.: Testing an optimising compiler by generating random lambda terms. In: Proceedings of the 6th International Workshop on Automation of Software Test, AST 2011, pp. 91–97. ACM, New York (2011)Google Scholar
Szabo, M.E.: The collected papers of Gerhard Gentzen. Philos. Sci. 39(1), 91 (1972)Google Scholar
Rémy, J.L.: Un procédé itératif de dénombrement d’arbres binaires et son application à leur génération aléatoire. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 19(2), 179–195 (1985)CrossRefGoogle Scholar
Knuth, D.E.: The Art of Computer Programming, Volume 4, Fascicle 4: Generating All Trees-History of Combinatorial Generation (Art of Computer Programming). Addison-Wesley Professional, Upper Saddle River (2006)Google Scholar
Tarau, P.: Declarative algorithms for generation, counting and random sampling of term algebras. In: Proceedings of SAC 2018, ACM Symposium on Applied Computing, PL track. ACM, Pau, April 2018Google Scholar