Refinement Type Directed Search for Meta-Interpretive-Learning of Higher-Order Logic Programs

TL;DR

This paper enhances meta-interpretive learning for higher-order logic programs by integrating polymorphic and refinement types, significantly reducing search space and synthesis time through type-based pruning and inference.

Contribution

It introduces polymorphic and refinement type checking into MIL, enabling more efficient program synthesis and type inference in ILP.

Findings

Cubic reduction in search space and synthesis time.

Successful inference of polymorphic types for clauses and programs.

Enhanced pruning of hypothesis space using refinement types.

Abstract

The program synthesis problem within the Inductive Logic Programming (ILP) community has typically been seen as untyped. We consider the benefits of user provided types on background knowledge. Building on the Meta-Interpretive Learning (MIL) framework, we show that type checking is able to prune large parts of the hypothesis space of programs. The introduction of polymorphic type checking to the MIL approach to logic program synthesis is validated by strong theoretical and experimental results, showing a cubic reduction in the size of the search space and synthesis time, in terms of the number of typed background predicates. Additionally we are able to infer polymorphic types of synthesized clauses and of entire programs. The other advancement is in developing an approach to leveraging refinement types in ILP. Here we show that further pruning of the search space can be achieved, though the SMT solving used for refinement type checking comes