TY - GEN

T1 - Decision algorithms for checking definability of order-2 finitary PCF

AU - Kawata, Sadaaki

AU - Asada, Kazuyuki

AU - Kobayashi, Naoki

N1 - Funding Information:
We thank anonymous reviewers for useful comments. This work was partially supported by JSPS Kakenhi 15H05706, and 23220001.
Publisher Copyright:
© Springer International Publishing Switzerland 2015.

PY - 2015

Y1 - 2015

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84952326448&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84952326448&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-26529-2_17

DO - 10.1007/978-3-319-26529-2_17

M3 - Conference contribution

AN - SCOPUS:84952326448

SN - 9783319265285

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 313

EP - 331

BT - Programming Languages and Systems - 13th Asian Symposium, APLAS 2015, Proceedings

A2 - Park, Sungwoo

A2 - Feng, Xinyu

PB - Springer Verlag

T2 - 13th Asian Symposium on Programming Languages and Systems, APLAS 2015

Y2 - 30 November 2015 through 2 December 2015

ER -