{"id":32817,"date":"2026-01-21T17:02:42","date_gmt":"2026-01-21T17:02:42","guid":{"rendered":"https:\/\/lamarr-institute.org\/publication\/finite-combinatory-logic-with-predicates\/"},"modified":"2026-09-17T11:26:26","modified_gmt":"2026-09-17T11:26:26","slug":"finite-combinatory-logic-with-predicates","status":"publish","type":"publication","link":"https:\/\/lamarr-institute.org\/de\/publication\/finite-combinatory-logic-with-predicates\/","title":{"rendered":"Finite Combinatory Logic with Predicates"},"content":{"rendered":"<p>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.<\/p>\n<p>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.<\/p>\n<p>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.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>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 [&hellip;]<\/p>\n","protected":false},"author":14,"featured_media":0,"template":"","meta":{"_acf_changed":false,"footnotes":""},"publication-type":[32],"class_list":["post-32817","publication","type-publication","status-publish","hentry","publication-type-inproceedings"],"acf":[],"publishpress_future_workflow_manual_trigger":{"enabledWorkflows":[]},"_links":{"self":[{"href":"https:\/\/lamarr-institute.org\/de\/wp-json\/wp\/v2\/publication\/32817","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/lamarr-institute.org\/de\/wp-json\/wp\/v2\/publication"}],"about":[{"href":"https:\/\/lamarr-institute.org\/de\/wp-json\/wp\/v2\/types\/publication"}],"author":[{"embeddable":true,"href":"https:\/\/lamarr-institute.org\/de\/wp-json\/wp\/v2\/users\/14"}],"version-history":[{"count":0,"href":"https:\/\/lamarr-institute.org\/de\/wp-json\/wp\/v2\/publication\/32817\/revisions"}],"wp:attachment":[{"href":"https:\/\/lamarr-institute.org\/de\/wp-json\/wp\/v2\/media?parent=32817"}],"wp:term":[{"taxonomy":"publication-type","embeddable":true,"href":"https:\/\/lamarr-institute.org\/de\/wp-json\/wp\/v2\/publication-type?post=32817"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}