ON COMPLETENESS AND PARAMETRICITY IN THE REALIZABILITY SEMANTICS OF SYSTEM F

被引:0
|
作者
Pistone, Paolo [1 ]
机构
[1] Eberhard Karls Univ Tubingen, Wilhelm Schickard Inst, Sand 13, D-72076 Tubingen, Germany
关键词
System F; realizability; parametricity; completeness;
D O I
10.23638/LMCS-15(4:6)2019
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We investigate completeness and parametricity for a general class of realizability semantics for System F defined in terms of closure operators over sets of lambda-terms. This class includes most semantics used for normalization theorems, as those arising from Tait's saturated sets and Girard's reducibility candidates. We establish a completeness result for positive types which subsumes those existing in the literature, and we show that closed realizers satisfy parametricity conditions expressed either as invariance with respect to logical relations or as dinaturality. Our results imply that, for positive types, typability, realizability and parametricity are equivalent properties of closed normal lambda-terms.
引用
收藏
页码:6:1 / 6:54
页数:54
相关论文
共 50 条
  • [41] REALIZABILITY SEMANTICS FOR QUANTIFIED MODAL LOGIC: GENERALIZING FLAGG'S 1985 CONSTRUCTION
    Rin, Benjamin G.
    Walsh, Sean
    REVIEW OF SYMBOLIC LOGIC, 2016, 9 (04): : 752 - 809
  • [42] A REALIZABILITY SEMANTICS FOR INDUCTIVE FORMAL TOPOLOGIES, CHURCH'S THESIS AND AXIOM OF CHOICE
    Maietti, Maria Emilia
    Maschio, Samuele
    Rathjen, Michael
    LOGICAL METHODS IN COMPUTER SCIENCE, 2021, 17 (02) : 21:1 - 21:21
  • [43] Algebraic semantics and model completeness for Intuitionistic Public Announcement Logic
    Ma, Minghui
    Palmigiano, Alessandra
    Sadrzadeh, Mehrnoosh
    ANNALS OF PURE AND APPLIED LOGIC, 2014, 165 (04) : 963 - 995
  • [44] Algebraic Semantics and Model Completeness for Intuitionistic Public Announcement Logic
    Sadrzadeh, Mehrnoosh
    Palmigiano, Alessandra
    Ma, Minghui
    LOGIC, RATIONALITY, AND INTERACTION, 2011, 6953 : 394 - +
  • [45] SOUNDNESS AND COMPLETENESS OF PARTIAL DEDUCTIONS FOR WELL-FOUNDED SEMANTICS
    PRZYMUSINSKA, H
    PRZYMUSINSKI, T
    SEKI, H
    LECTURE NOTES IN ARTIFICIAL INTELLIGENCE, 1992, 624 : 1 - 12
  • [46] COMPLETENESS FOR COUNTER-DOXA CONDITIONALS - USING RANKING SEMANTICS
    Raidl, Eric
    REVIEW OF SYMBOLIC LOGIC, 2019, 12 (04): : 861 - 891
  • [47] Completeness for Ancestral Logic via a Computationally-Meaningful Semantics
    Cohen, Liron
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2017, 2017, 10501 : 247 - 260
  • [48] SOME REMARKS ABOUT COMPLETENESS OF SYSTEM [F(ALPHAKAPPAZ)]KAPPA/INFINITY=O
    IBRAGIMO.II
    NAGNIBID.NI
    DOKLADY AKADEMII NAUK SSSR, 1973, 210 (06): : 1277 - 1279
  • [49] COMPLETENESS OF CHARACTERISTIC SYSTEM
    KLEIMAN, SL
    ADVANCES IN MATHEMATICS, 1973, 11 (03) : 304 - 310
  • [50] Unknown Truths and False Beliefs: Completeness and Expressivity Results for the Neighborhood Semantics
    Jie Fan
    Studia Logica, 2022, 110 : 1 - 45