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 条
  • [21] ARE THERE HILBERT-STYLE PURE TYPE SYSTEMS?
    Bunder, Martin W.
    Dekkers, Wil J. M.
    LOGICAL METHODS IN COMPUTER SCIENCE, 2008, 4 (01)
  • [22] Pure type systems with subtyping (Extended abstract)
    Zwanenburg, J
    TYPED LAMBDA CALCULI AND APPLICATIONS, 1999, 1581 : 381 - 396
  • [23] Condensing lemmas for pure type systems with universes
    Jiménez, BCR
    ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, 1999, 1548 : 422 - 437
  • [24] Pure Type Systems without Explicit Contexts
    Geuvers, Herman
    Krebbers, Robbert
    McKinna, James
    Wiedijk, Freek
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2010, (34): : 53 - 67
  • [25] Restrictive apposition in Romance languages: Syntactic expansions of a compound pattern
    Barbu, Ana-Maria
    WORD STRUCTURE, 2020, 13 (02) : 142 - 165
  • [26] Syntactic type abstraction
    Grossman, D
    Morrisett, G
    Zdancewic, S
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2000, 22 (06): : 1037 - 1080
  • [27] Strong normalisation in two Pure Pattern Type Systems
    Wack, Benjamin
    Houtmann, Clement
    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2008, 18 (03) : 431 - 465
  • [28] The semi-full closure of Pure Type Systems
    Barthe, G
    MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 1998, 1998, 1450 : 316 - 325
  • [29] Common Origin of Pure and Interrupted Repeat Expansions in Spinocerebellar Ataxia Type 2 (SCA2)
    Ramos, Eliana Marisa
    Martins, Sandra
    Alonso, Isabel
    Emmel, Vanessa E.
    Saraiva-Pereira, Maria Luiza
    Jardim, Laura Bannach
    Coutinho, Paula
    Sequeiros, Jorge
    Silveira, Isabel
    AMERICAN JOURNAL OF MEDICAL GENETICS PART B-NEUROPSYCHIATRIC GENETICS, 2010, 153B (02) : 524 - 531
  • [30] ON SOME PROPERTIES OF THE SYNTACTIC SEMIGROUP OF A VERY PURE SUBSEMIGROUP
    DELUCA, A
    RAIRO-INFORMATIQUE THEORIQUE ET APPLICATIONS-THEORETICAL INFORMATICS AND APPLICATIONS, 1980, 14 (01): : 39 - 56
12345