BOUNDED QUANTIFICATION IS UNDECIDABLE

被引：35
|
作者：
PIERCE, BC
机构：
[1] LFCS, University of Edinburgh, The King's Buildings
来源：
INFORMATION AND COMPUTATION | 1994年 / 112卷 / 01期
关键词：
D O I：
10.1006/inco.1994.1055
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
F(less-than-or-equal-to) is a typed lambda-calculus with subtyping and bounded second-order polymorphism. First introduced by Cardelli and Wegner, it has been widely studied as a core calculus for type systems with subtyping. We use a reduction from the halting problem for two-counter Turing machines to show that the subtyping and typing relations of F(less-than-or-equal-to) are undecidable. (C) 1994 Academic Press, Inc.
引用
收藏
页码：131 / 165
页数：35
相关论文
共 50 条
  • [1] Many bounded versions of undecidable problems are NP-hard
    Klingler, Andreas
    van der Eyden, Mirte
    Stengele, Sebastian
    Reinhart, Tobias
    De las Cuevas, Gemma
    [J]. SCIPOST PHYSICS, 2023, 14 (06):
  • [2] Greedy Implicit Bounded Quantification
    Cui, Chen
    Jiang, Shengyi
    Oliveira, Bruno C. D. S.
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2023, 7 (OOPSLA):
  • [3] SEPARATION PRINCIPLES AND BOUNDED QUANTIFICATION
    DAWES, AM
    [J]. CANADIAN MATHEMATICAL BULLETIN-BULLETIN CANADIEN DE MATHEMATIQUES, 1975, 18 (02): : 295 - 296
  • [4] The undecidable
    Dudos, Jean-Francois
    [J]. FRENCH REVIEW, 2014, 88 (01): : 274 - 275
  • [5] PARALLEL BOUNDED QUANTIFICATION - PRELIMINARY-RESULTS
    ARRO, H
    BARKLUND, J
    BEVEMYR, J
    [J]. SIGPLAN NOTICES, 1993, 28 (08): : 117 - 124
  • [6] BOUNDED QUANTIFICATION AND RELATIONS RECOGNIZABLE BY FINITE AUTOMATA
    LAURINOLLI, T
    [J]. ACTA INFORMATICA, 1978, 10 (01) : 67 - 78
  • [7] Modal logic with bounded quantification over worlds
    Van Eijk, RM
    De Boer, FS
    Van der Hoek, W
    Meyer, JJC
    [J]. JOURNAL OF LOGIC AND COMPUTATION, 2001, 11 (05) : 701 - 715
  • [8] A MODEST MODEL OF RECORDS, INHERITANCE, AND BOUNDED QUANTIFICATION
    BRUCE, KB
    LONGO, G
    [J]. INFORMATION AND COMPUTATION, 1990, 87 (1-2) : 196 - 240
  • [9] RELATIONAL SEMANTICS FOR RECURSIVE TYPES AND BOUNDED QUANTIFICATION
    CARDONE, F
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1989, 372 : 164 - 178
  • [10] Basic theory of F-bounded quantification
    Baldan, P
    Ghelli, G
    Raffaetà, A
    [J]. INFORMATION AND COMPUTATION, 1999, 153 (02) : 173 - 237
12345