Abstract
For use in earlier approaches to automated module interface adaptation, we seek a restricted form of program synthesis. Given some typing assumptions and a desired result type, we wish to automatically build a number of program fragments of this chosen typing, using functions and values available in the given typing environment. We call this problem term enumeration. To solve the problem, we use the Curry-Howard correspondence (propositions-as-types, proofs-as-programs) to transform it into a proof enumeration problem for an intuitionistic logic calculus. We formally study proof enumeration and counting in this calculus. We prove that proof counting is solvable and give an algorithm to solve it. This in turn yields a proof enumeration algorithm.
Supported by grants: EC FP5/IST/FET IST-2001-33477 “DART”, EPSRC GR/L 41545/01, NSF 0113193 (ITR), Sun Microsystems EDUD-7826-990410-US.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Aponte, M.V., Di Cosmo, R., Dubois, C., Yakobowski, B.: Signature subtyping modulo type isomorphisms (2004) (in preparation)
Ben-Yelles, C.-B.: Type-assignment in the lambda-calculus; syntax and semantics. PhD thesis, Mathematics Dept., University of Wales Swansea, UK (1979)
Broda, S., Damas, L.: On the structure of normal λ-terms having a certain type. In: 7th Workshop on Logic, Language, Information and Computation (WoLLIC 2000), Brazil (2000)
Dyckhoff, R.: Proof search in constructive logics. In: Logic Colloquium 1997 (1998)
Dyckhoff, R., Pinto, L.: Cut-elimination and a permutation-free sequent calculus for intuitionistic logic. Studia Logica 60(1) (1998)
Dyckhoff, R., Pinto, L.: Permutability of proofs in intuitionistic sequent calculi. Theoret. Comput. Sci. 212(1–2) (1999)
Haack, C.: Foundations for a tool for the automatic adaptation of software components based on semantic specifications. PhD thesis, Kansas State University (2001)
Haack, C., Howard, B., Stoughton, A., Wells, J.B.: Fully automatic adaptation of software components based on semantic specifications. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, p. 83. Springer, Heidelberg (2002)
Herbelin, H.: A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure. In: Pacholski, L., Tiuryn, J. (eds.) CSL 1994. LNCS, vol. 933. Springer, Heidelberg (1995)
Herbelin, H.: A λ-calculus structure isomorphic to Gentzen-style sequent calculus structure (1994), Available at http://coq.inria.fr/~herbelin/LAMBDA-BAR-FULL.dvi.gz
Hindley, J.R.: Basic Simple Type Theory. Cambridge Tracts in Theoretical Computer Science, vol. 42. Cambridge University Press, Cambridge (1997)
Howe, J.M.: Proof Search Issues In Some Non-Classical Logics. PhD thesis, University of St Andrews (1998), http://www.cs.kent.ac.uk/pubs/1998/946/
Pinto, L.: Cut formulae and logic programming. In: Dyckhoff, R. (ed.) ELP 1993. LNCS, vol. 798. Springer, Heidelberg (1994)
Pinto, L., Dyckhoff, R.: Sequent calculi for the normal terms of the λΠ and λΠΣ calculi. In: Galmiche, D. (ed.) Electronic Notes in Theoretical Computer Science, vol. 17. Elsevier, Amsterdam (2000)
Zaionc, M.: Fixpoint technique for counting terms in typed lambda calculus. Technical Report 95-20, State University of New York (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wells, J.B., Yakobowski, B. (2005). Graph-Based Proof Counting and Enumeration with Applications for Program Fragment Synthesis. In: Etalle, S. (eds) Logic Based Program Synthesis and Transformation. LOPSTR 2004. Lecture Notes in Computer Science, vol 3573. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11506676_17
Download citation
DOI: https://doi.org/10.1007/11506676_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-26655-6
Online ISBN: 978-3-540-31683-1
eBook Packages: Computer ScienceComputer Science (R0)