Infinitary lambda calculus

被引：85
|
作者：
Kennaway, JR
Klop, JW
Sleep, MR
deVries, FJ
机构：
[1] UNIV E ANGLIA,SCH INFORMAT SYST,NORWICH NR4 7TJ,NORFOLK,ENGLAND
[2] CWI,DEPT SOFTWARE TECHNOL,NL-1090 GB AMSTERDAM,NETHERLANDS
[3] HITACHI LTD,ADV RES LAB,HATOYAMA,SAITAMA 35003,JAPAN
来源：
THEORETICAL COMPUTER SCIENCE | 1997年 / 175卷 / 01期
基金：
英国工程与自然科学研究理事会;
关键词：
D O I：
10.1016/S0304-3975(96)00171-5
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
In a previous paper we have established the theory of transfinite reduction for orthogonal term rewriting systems. In this paper we perform the same task for the lambda calculus. From the viewpoint of infinitary rewriting, the Bohm model of the lambda calculus can be seen as an infinitary term model. In contrast to term rewriting, there are several different possible notions of infinite term, which give rise to different Bohm-like models, which embody different notions of lazy or eager computation.
引用
收藏
页码：93 / 125
页数：33
相关论文
共 50 条
  • [1] Applications of infinitary lambda calculus
    Barendregt, Henk
    Klop, Jan Willem
    INFORMATION AND COMPUTATION, 2009, 207 (05) : 559 - 582
  • [2] Highlights in infinitary rewriting and lambda calculus
    Endrullis, Jorg
    Hendriks, Dimitri
    Klop, Jan Willem
    THEORETICAL COMPUTER SCIENCE, 2012, 464 : 48 - 71
  • [3] An Infinitary Affine Lambda-Calculus Isomorphic to the Full Lambda-Calculus
    Mazza, Damiano
    2012 27TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2012, : 471 - 480
  • [4] Weakening the Axiom of Overlap in Infinitary Lambda Calculus
    Severi, Paula
    de Vries, Fer-Jan
    22ND INTERNATIONAL CONFERENCE ON REWRITING TECHNIQUES AND APPLICATIONS (RTA'11), 2011, 10 : 313 - 328
  • [5] A NEW COINDUCTIVE CONFLUENCE PROOF FOR INFINITARY LAMBDA CALCULUS
    Czajka, Lukasz
    LOGICAL METHODS IN COMPUTER SCIENCE, 2020, 16 (01)
  • [6] The infinitary lambda calculus of the infinite eta Bohm trees
    Severi, Paula
    De Vries, Fer-Jan
    MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2017, 27 (05) : 681 - 733
  • [7] Decomposing the Lattice of Meaningless Sets in the Infinitary Lambda Calculus
    Severi, Paula
    de Vries, Fer-Jan
    LOGIC, LANGUAGE, INFORMATION AND COMPUTATION, WOLLIC 2011, 2011, 6642 : 210 - 227
  • [8] A Functorial Bridge Between the Infinitary Affine Lambda-Calculus and Linear Logic
    Mazza, Damiano
    Pellissier, Luc
    THEORETICAL ASPECTS OF COMPUTING - ICTAC 2015, 2015, 9399 : 144 - 161
  • [9] Non-uniform Polytime Computation in the Infinitary Affine Lambda-Calculus
    Mazza, Damiano
    AUTOMATA, LANGUAGES, AND PROGRAMMING (ICALP 2014), PT II, 2014, 8573 : 305 - 317
  • [10] Berarducci trees observational equivalence infinitary lambda calculus Bohm out technique
    Dezani-Ciancaglini, M
    Severi, P
    de Vries, FJ
    THEORETICAL COMPUTER SCIENCE, 2003, 298 (02) : 275 - 302
12345