Syntactic analysis of η-expansions in Pure Type Systems

被引：1
|
作者：
Joachimski, F [1 ]
机构：
[1] Univ Munich, Math Inst, D-80333 Munich, Germany
来源：
INFORMATION AND COMPUTATION | 2003年 / 182卷 / 01期
关键词：
pure type systems; q-expansion; strong normalization;
D O I：
10.1016/S0890-5401(03)00019-1
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
By a detailed analysis of the interaction between -reduction -->(beta) and eta-expansion -->((η) over bar) in the simply typed lambda-calculus, a modular and purely syntactic proof method is devised in order to derive strong normalization of the combined reduction -->(beta(η) over bar) from that of -->(beta) and -->((η) over bar). It is shown how this technique extends to beta-normalizing functional Pure Type Systems with Barthe's formulation of eta-expansion. (C) 2003 Elsevier Science (USA). All rights reserved.
引用
收藏
页码：53 / 71
页数：19
相关论文
共 50 条
  • [1] Type inference for pure type systems
    Severi, P
    INFORMATION AND COMPUTATION, 1998, 143 (01) : 1 - 23
  • [2] Pure patterns type systems
    Barthe, G
    Cirstea, H
    Kirchner, C
    Liquori, L
    ACM SIGPLAN NOTICES, 2003, 38 (01) : 250 - 261
  • [3] Modal Pure Type Systems
    Tijn Borghuis
    Journal of Logic, Language and Information, 1998, 7 (3) : 265 - 296
  • [4] Parameters in pure type systems
    Bloo, R
    Kamareddine, F
    Laan, T
    Nederpelt, R
    LATIN 2002: THEORETICAL INFORMATICS, 2002, 2286 : 371 - 385
  • [5] TYPING IN PURE TYPE SYSTEMS
    JUTTING, LSV
    INFORMATION AND COMPUTATION, 1993, 105 (01) : 30 - 41
  • [6] INTERPOLATION THEOREMS AND EXPANSIONS BY SYSTEMS OF FOURIER TYPE
    DZHRBASHIAN, MM
    RAFAELIAN, SG
    DOKLADY AKADEMII NAUK SSSR, 1985, 285 (04): : 782 - 787
  • [7] A module calculus for pure type systems
    Courant, J
    TYPED LAMBDA CALCULI AND APPLICATIONS, 1997, 1210 : 112 - 128
  • [8] The Expansion Postponement in Pure Type Systems
    宋方敏
    Journal of Computer Science and Technology, 1997, (06) : 555 - 563
  • [9] Realizability and Parametricity in Pure Type Systems
    Bernardy, Jean-Philippe
    Lasson, Marc
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, 2011, 6604 : 108 - +
  • [10] The expansion postponement in Pure Type Systems
    Fangmin Song
    Journal of Computer Science and Technology, 1997, 12 (6) : 555 - 563
12345