文章基本信息

标题：A TIER-BASED TYPED PROGRAMMING LANGUAGE CHARACTERIZING FEASIBLE FUNCTIONALS
本地全文：下载
作者：Emmanuel Hainry ; Bruce M. Kapron ; Jean-Yves Marion 等
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2022
卷号：18
期号：1
页码：1-31
DOI：10.46298/lmcs-18(1:33)2022
语种：English
出版社：Technical University of Braunschweig
摘要：The class of Basic Feasible Functionals BFF$_2$ is the type-2 counterpart of the class FP of type-1 functions computable in polynomial time. Several characterizations have been suggested in the literature, but none of these present a programming language with a type system guaranteeing this complexity bound. We give a characterization of BFF$_2$ based on an imperative language with oracle calls using a tier-based type system whose inference is decidable. Such a characterization should make it possible to link higher-order complexity with programming theory. The low complexity (cubic in the size of the program) of the type inference algorithm contrasts with the intractability of the aforementioned methods and does not overly constrain the expressive power of the language.
关键词：Feasible Functionals;BFF;implicit computational complexity;tiering;type-2;type system