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 条
  • [31] On Minimal Expansions in Redundant Number Systems: Algorithms and Quantitative Analysis
    Clemens Heuberger
    Helmut Prodinger
    Computing, 2001, 66 : 377 - 393
  • [32] On minimal expansions in redundant number systems: Algorithms and quantitative analysis
    Heuberger, C
    Prodinger, H
    COMPUTING, 2001, 66 (04) : 377 - 393
  • [33] Syntactic complexity and discourse type
    Véliz, M
    ESTUDIOS FILOLOGICOS, 1999, (34): : 181 - 192
  • [34] A SYNTACTIC APPROACH TO TYPE SOUNDNESS
    WRIGHT, AK
    FELLEISEN, M
    INFORMATION AND COMPUTATION, 1994, 115 (01) : 38 - 94
  • [35] EXACT AND APPROXIMATE EXPANSIONS WITH PURE GAUSSIAN WAVE PACKETS
    De Hoop, Maarten V.
    Groechenig, Karlheinz
    Romero, Jose Luis
    SIAM JOURNAL ON MATHEMATICAL ANALYSIS, 2014, 46 (03) : 2229 - 2253
  • [36] LARGE CLUSTERS OF CESIUM FROM PURE VAPOR EXPANSIONS
    GSPANN, J
    ZEITSCHRIFT FUR PHYSIK D-ATOMS MOLECULES AND CLUSTERS, 1991, 20 (1-4): : 421 - 423
  • [37] Syntactic analysis of natural language sentences based on rewriting systems and adaptivity
    Massa Cereda, Paulo Roberto
    Miura, Newton Kiyotaka
    Neto, Joao Jose
    9TH INTERNATIONAL CONFERENCE ON AMBIENT SYSTEMS, NETWORKS AND TECHNOLOGIES (ANT 2018) / THE 8TH INTERNATIONAL CONFERENCE ON SUSTAINABLE ENERGY INFORMATION TECHNOLOGY (SEIT-2018) / AFFILIATED WORKSHOPS, 2018, 130 : 1102 - 1107
  • [38] Ml2 -: A module calculus for Pure Type Systems
    Courant, Judicael
    JOURNAL OF FUNCTIONAL PROGRAMMING, 2007, 17 : 287 - 352
  • [39] Equality is typable in Semi-Full Pure Type Systems
    Siles, Vincent
    Herbelin, Hugo
    25TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS 2010), 2010, : 21 - 30
  • [40] SYNTACTIC CHECKING OF MICROPROCESSOR SYSTEMS
    GLADSHTEIN, MA
    KOMAROV, VM
    SHUBIN, NA
    AVTOMATIKA I VYCHISLITELNAYA TEKHNIKA, 1987, (05): : 89 - 93
12345