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