INFINITARY COMBINATORY REDUCTION SYSTEMS: NORMALISING REDUCTION STRATEGIES

被引：1

作者：

Ketema, Jeroen ^{[1
]}

Simonsen, Jakob Grue ^{[2
]}

机构：

[1] Tohoku Univ, Elect Commun Res Inst, Aoba Ku, Sendai, Miyagi 9808577, Japan

[2] Univ Copenhagen DIKU, Dept Comp Sci, DK-2100 Copenhagen O, Denmark

来源：

LOGICAL METHODS IN COMPUTER SCIENCE | 2010年 / 6卷 / 01期

关键词：

term rewriting; higher-order computation; combinatory reduction systems; lambda-calculus; infinite computation; reduction strategies; normal forms;

D O I：

10.2168/LMCS-6(1:7)2010

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We study normalising reduction strategies for infinitary Combinatory Reduction Systems (iCRSs). We prove that all fair, outermost-fair, and needed-fair strategies are normalising for orthogonal, fully-extended iCRSs. These facts properly generalise a number of results on normalising strategies in first-order infinitary rewriting and provide the first examples of normalising strategies for infinitary lambda-calculus.

引用

页数：35

共 25 条

[1]

[Anonymous], LMCS

[2]

Barendregt Hendrik Pieter, 1985, Studies in logic and the foundations of mathematics, V103

[3]

GLAUERT J, 1994, LECT NOTES COMPUTER, V968, P144

[4]

Hanus M, 1996, LECT NOTES COMPUT SC, V1103, P138

[5]

Huet G.P., 1991, Computational Logic-Essays in Honor of Alan Robinson, P395

[6]

KAHRS S, 1993, LECT NOTES COMPUTER, V816, P169

[7] Infinitary lambda calculus [J].

Kennaway, JR ;

Klop, JW ;

Sleep, MR ;

deVries, FJ .

THEORETICAL COMPUTER SCIENCE, 1997, 175 (01) :93-125

[8] TRANSFINITE REDUCTIONS IN ORTHOGONAL TERM REWRITING-SYSTEMS [J].

KENNAWAY, R ;

KLOP, JW ;

SLEEP, R ;

DEVRIES, FJ .

INFORMATION AND COMPUTATION, 1995, 119 (01) :18-38

[9]

KENNAWAY R, 2003, CAMBRIDGE TRACTS THE, V55, pCH12

[10] On confluence of infinitary combinatory reduction systems [J].

Ketema, J ;

Simonsen, JG .

LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2005, 3835 :199-214

← 1 2 3 →