Decision algorithms for checking definability of order-2 finitary PCF

Abstract

We consider a definability problem for finitary PCF, which asks whether, given a function (as an element of a cpo), there exists a term of finitary PCF whose interpretation is the function. The definability problem for finitary PCF is known to be decidable for types of order at most 2. However, its complexity and practical algorithms have not been well studied. In this paper, we give two algorithms for checking definability: one based on Sieber’s sequentiality relation, which runs in quadruply exponential time for the size of the type of the given function, and the other based on a saturation method, which runs in triply exponential time for the size. With the recent advance of higher-order model checking, our result may be useful for implementing a tool for deciding observational equivalence between finitary PCF terms of types of order at most 3.