Finite Combinatory Logic with Predicates

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.