2026-07-23T18:19:13Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20480 2024-08-20T13:53:45Z ddc:004 open_access

Finite Combinatory Logic with Predicates Dudenhefner, Andrej Stahl, Christoph Chaumet, Constantin Laarmann, Felix Rehof, Jakob combinatory logic inhabitation intersection types program synthesis 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Andrej Dudenhefner and Christoph Stahl and Constantin Chaumet and Felix Laarmann and Jakob Rehof 2024 Is Part Of LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TYPES.2023.2 urn:nbn:de:0030-drops-204808 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.2 eng https://creativecommons.org/licenses/by/4.0/legalcode