Document Open Access Logo

Finite Combinatory Logic with Predicates

Authors Andrej Dudenhefner , Christoph Stahl , Constantin Chaumet , Felix Laarmann , Jakob Rehof

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2023.2.pdf
  • Filesize: 0.94 MB
  • 22 pages

Document Identifiers

Author Details

Andrej Dudenhefner
  • TU Dortmund University, Germany
Christoph Stahl
  • TU Dortmund University, Germany
Constantin Chaumet
  • TU Dortmund University, Germany
Felix Laarmann
  • TU Dortmund University, Germany
Jakob Rehof
  • TU Dortmund University, Germany
  • Lamarr Institute for Machine Learning and Artificial Intelligence, Dortmund, Germany

Funding

  • Chaumet, Constantin: Deutsche Forschungsgemeinschaft (DFG, German Research Foundation – Project Number: 276879186).

Cite As Get BibTex

Andrej Dudenhefner, Christoph Stahl, Constantin Chaumet, Felix Laarmann, and Jakob Rehof. Finite Combinatory Logic with Predicates. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 2:1-2:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.TYPES.2023.2

Abstract

Type inhabitation in extensions of Finite Combinatory Logic (FCL) is the mechanism underlying various component-oriented synthesis frameworks. In FCL inhabitant sets correspond to regular tree languages and vice versa. Therefore, it is not possible to specify non-regular properties of inhabitants, such as (dis)equality of subterms. Additionally, the monomorphic nature of FCL oftentimes hinders concise specification of components.
We propose a conservative extension to FCL by quantifiers and predicates, introducing a restricted form of polymorphism. In the proposed type system (FCLP) inhabitant sets correspond to decidable term languages and vice versa. As a consequence, type inhabitation in FCLP is undecidable. Based on results in tree automata theory, we identify a fragment of FCLP with the following two properties. First, the fragment enjoys decidable type inhabitation. Second, it allows for specification of local (dis)equality constraints for subterms of inhabitants.
For empirical evaluation, we implement a semi-decision procedure for type inhabitation in FCLP. We compare specification capabilities, scalability, and performance of the implementation to existing FCL-based approaches. Finally, we evaluate practical applicability via a case study, synthesizing mechanically sound robotic arms.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • combinatory logic
  • inhabitation
  • intersection types
  • program synthesis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Henk Barendregt. Introduction to generalized type systems. J. Funct. Program., 1(2):125-154, 1991. URL: https://doi.org/10.1017/S0956796800020025.
  2. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. The Journal of Symbolic Logic, 48(4):931-940, 1983. URL: http://www.jstor.org/stable/2273659.
  3. Catriel Beeri and Raghu Ramakrishnan. On the power of magic. J. Log. Program., 10(3&4):255-299, 1991. URL: https://doi.org/10.1016/0743-1066(91)90038-Q.
  4. Jan Bessai. A type-theoretic framework for software component synthesis. PhD thesis, TU Dortmund University, 2019. Google Scholar
  5. Jan Bessai, Lukasz Czajka, Felix Laarmann, and Jakob Rehof. Restricting tree grammars with term rewriting. In Amy P. Felty, editor, 7th International Conference on Formal Structures for Computation and Deduction, FSCD 2022, August 2-5, 2022, Haifa, Israel, volume 228 of LIPIcs, pages 14:1-14:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.FSCD.2022.14.
  6. Jan Bessai, Boris Düdder, George Heineman, and Jakob Rehof. Combinatory synthesis of classes using feature grammars. In Formal Aspects of Component Software: 12th International Conference, FACS 2015, Niterói, Brazil, October 14-16, 2015, Revised Selected Papers 12, pages 123-140. Springer, 2016. Google Scholar
  7. Jan Bessai, Andrej Dudenhefner, Boris Düdder, Tzu-Chun Chen, Ugo de’Liguoro, and Jakob Rehof. Mixin composition synthesis based on intersection types. In Thorsten Altenkirch, editor, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), volume 38 of Leibniz International Proceedings in Informatics (LIPIcs), pages 76-91, Dagstuhl, Germany, 2015. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TLCA.2015.76.
  8. Jan Bessai, Andrej Dudenhefner, Boris Düdder, Moritz Martens, and Jakob Rehof. Combinatory Logic Synthesizer. In Tiziana Margaria and Bernhard Steffen, editors, Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change - 6th International Symposium, ISoLA 2014, Imperial, Corfu, Greece, October 8-11, 2014, Proceedings, Part I, volume 8802 of Lecture Notes in Computer Science, pages 26-40. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-45234-9_3.
  9. Jan Bessai and Anna Vasileva. User support for the combinator logic synthesizer framework. In Paolo Masci, Rosemary Monahan, and Virgile Prevosto, editors, Proceedings 4th Workshop on Formal Integrated Development Environment, F-IDE@FLoC 2018, Oxford, England, 14 July 2018, volume 284 of EPTCS, pages 16-25, 2018. URL: https://doi.org/10.4204/EPTCS.284.2.
  10. Bruno Bogaert, Franck Seynhaeve, and Sophie Tison. The recognizability problem for tree automata with comparisons between brothers. In Wolfgang Thomas, editor, Foundations of Software Science and Computation Structure, Second International Conference, FoSSaCS'99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings, volume 1578 of Lecture Notes in Computer Science, pages 150-164. Springer, 1999. URL: https://doi.org/10.1007/3-540-49019-1_11.
  11. Anne-Cécile Caron, Hubert Comon, Jean-Luc Coquidé, Max Dauchet, and Florent Jacquemard. Pumping, cleaning and symbolic constraints solving. In Serge Abiteboul and Eli Shamir, editors, Automata, Languages and Programming, 21st International Colloquium, ICALP94, Jerusalem, Israel, July 11-14, 1994, Proceedings, volume 820 of Lecture Notes in Computer Science, pages 436-449. Springer, 1994. URL: https://doi.org/10.1007/3-540-58201-0_88.
  12. Giuseppe Castagna. Programming with union, intersection, and negation types. CoRR, abs/2111.03354, 2021. URL: https://arxiv.org/abs/2111.03354.
  13. Giuseppe Castagna, Mickaël Laurent, and Kim Nguyen. Polymorphic type inference for dynamic languages. Proc. ACM Program. Lang., 8(POPL):1179-1210, 2024. URL: https://doi.org/10.1145/3632882.
  14. Constantin Chaumet and Jakob Rehof. CLS-CAD: Synthesizing CAD Assemblies in Fusion 360, 2023. URL: https://arxiv.org/abs/2311.18492.
  15. Constantin Chaumet, Jakob Rehof, and Thomas Schuster. A knowledge-driven framework for synthesizing designs from modular components, 2023. URL: https://arxiv.org/abs/2311.18533.
  16. Hubert Comon and Florent Jacquemard. Ground reducibility is EXPTIME-complete. Inf. Comput., 187(1):123-153, 2003. URL: https://doi.org/10.1016/S0890-5401(03)00134-2.
  17. Mariangiola Dezani-Ciancaglini and J. Roger Hindley. Intersection types for combinatory logic. Theor. Comput. Sci., 100(2):303-324, 1992. URL: https://doi.org/10.1016/0304-3975(92)90306-Z.
  18. Boris Düdder, Moritz Martens, Jakob Rehof, and Paweł Urzyczyn. Bounded combinatory logic. In Patrick Cégielski and Arnaud Durand, editors, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France, volume 16 of LIPIcs, pages 243-258. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPICS.CSL.2012.243.
  19. Andrej Dudenhefner. Algorithmic aspects of type-based program synthesis. PhD thesis, TU Dortmund University, 2019. Google Scholar
  20. Andrej Dudenhefner, Felix Laarmann, Jakob Rehof, and Christoph Stahl. Finite combinatory logic extended by a Boolean query language for composition synthesis. In 29th International Conference on Types for Proofs and Programs TYPES 2023-Abstracts, page 105, 2023. Google Scholar
  21. Andrej Dudenhefner, Christoph Stahl, and Jan Bessai. Combinatory Logic Synthesizer with Predicates. URL: https://github.com/tudo-seal/clsp-python.
  22. Jonas Duregård, Patrik Jansson, and Meng Wang. Feat: functional enumeration of algebraic types. In Janis Voigtländer, editor, Proceedings of the 5th ACM SIGPLAN Symposium on Haskell, Haskell 2012, Copenhagen, Denmark, 13 September 2012, pages 61-72. ACM, 2012. URL: https://doi.org/10.1145/2364506.2364515.
  23. Thom W. Frühwirth, Ehud Shapiro, Moshe Y. Vardi, and Eyal Yardeni. Logic programs as types for logic programs. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), Amsterdam, The Netherlands, July 15-18, 1991, pages 300-309. IEEE Computer Society, 1991. URL: https://doi.org/10.1109/LICS.1991.151654.
  24. George Heineman, Jan Bessai, Boris Düdder, and Jakob Rehof. A long and winding road towards modular synthesis. In Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques: 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part I 7, pages 303-317. Springer, 2016. Google Scholar
  25. George Heineman, Armend Hoxha, Boris Düdder, and Jakob Rehof. Towards migrating object-oriented frameworks to enable synthesis of product line members. In Proceedings of the 19th International Conference on Software Product Line, pages 56-60, 2015. Google Scholar
  26. Florent Jacquemard. Extended Tree Automata Models for the Verification of Infinite State Systems. PhD thesis, École normale supérieure de Cachan-ENS Cachan, 2011. Google Scholar
  27. Fadil Kallat, Tristan Schäfer, and Anna Vasileva. CLS-SMT: bringing together combinatory logic synthesis and satisfiability modulo theories. In Giselle Reis and Haniel Barbosa, editors, Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019, volume 301 of EPTCS, pages 51-65, 2019. URL: https://doi.org/10.4204/EPTCS.301.7.
  28. Alexander Mages, Carina Mieth, Jens Hetzler, Fadil Kallat, Jakob Rehof, Christian Riest, and Tristan Schäfer. Automatic component-based synthesis of user-configured manufacturing simulation models. In 2022 Winter Simulation Conference (WSC), pages 1841-1852. IEEE, 2022. Google Scholar
  29. Peter-Michael Osera and Steve Zdancewic. Type-and-example-directed program synthesis. In David Grove and Stephen M. Blackburn, editors, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, pages 619-630. ACM, 2015. URL: https://doi.org/10.1145/2737924.2738007.
  30. Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. Program synthesis from polymorphic refinement types. In Chandra Krintz and Emery D. Berger, editors, Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, pages 522-538. ACM, 2016. URL: https://doi.org/10.1145/2908080.2908093.
  31. Jakob Rehof. Towards combinatory logic synthesis. In 1st International Workshop on Behavioural Types, BEAT, 2013. Google Scholar
  32. Jakob Rehof and Paweł Urzyczyn. Finite combinatory logic with intersection types. In C.-H. Luke Ong, editor, Typed Lambda Calculi and Applications - 10th International Conference, TLCA 2011, Novi Sad, Serbia, June 1-3, 2011. Proceedings, volume 6690 of Lecture Notes in Computer Science, pages 169-183. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21691-6_15.
  33. Andreas Reuß and Helmut Seidl. Bottom-up tree automata with term constraints. In Christian G. Fermüller and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings, volume 6397 of Lecture Notes in Computer Science, pages 581-593. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-16242-8_41.
  34. Tristan Schäfer, Jim Bergmann, Rafael Garcia Carballo, Jakob Rehof, and Petra Wiederkehr. A synthesis-based tool path planning approach for machining operations. Procedia CIRP, 104:918-923, 2021. Google Scholar
  35. Cas van der Rest and Wouter Swierstra. A completely unique account of enumeration. Proc. ACM Program. Lang., 6(ICFP):411-437, 2022. URL: https://doi.org/10.1145/3547636.
  36. Maarten H. van Emden and Robert A. Kowalski. The semantics of predicate logic as a programming language. J. ACM, 23(4):733-742, 1976. URL: https://doi.org/10.1145/321978.321991.
  37. Jan Winkels, Julian Graefenstein, Tristan Schäfer, David Scholz, Jakob Rehof, and Michael Henke. Automatic composition of rough solution possibilities in the target planning of factory planning projects by means of combinatory logic. In Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice: 8th International Symposium, ISoLA 2018, Limassol, Cyprus, November 5-9, 2018, Proceedings, Part IV 8, pages 487-503. Springer, 2018. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact