Decision algorithms for checking definability of order-2 finitary PCF

Sadaaki Kawata, Kazuyuki Asada, Naoki Kobayashi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish
Title of host publicationProgramming Languages and Systems - 13th Asian Symposium, APLAS 2015, Proceedings
EditorsSungwoo Park, Xinyu Feng
PublisherSpringer Verlag
Pages313-331
Number of pages19
ISBN (Print)9783319265285
DOIs
Publication statusPublished - 2015
Externally publishedYes
Event13th Asian Symposium on Programming Languages and Systems, APLAS 2015 - Pohang, Korea, Republic of
Duration: 2015 Nov 302015 Dec 2

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9458
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference13th Asian Symposium on Programming Languages and Systems, APLAS 2015
CountryKorea, Republic of
CityPohang
Period15/11/3015/12/2

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Decision algorithms for checking definability of order-2 finitary PCF'. Together they form a unique fingerprint.

Cite this