On confluence of infinitary combinatory reduction systems

被引：7
作者：
Ketema, J
Simonsen, JG
机构：
[1] Free Univ Amsterdam, Dept Comp Sci, NL-1081 HV Amsterdam, Netherlands
[2] Univ Copenhagen, DIKU, Dept Comp Sci, DK-2100 Copenhagen O, Denmark
来源：
LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS | 2005年 / 3835卷
关键词：
D O I：
10.1007/11591191_15
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We prove that fully-extended, orthogonal infinitary combinatory reduction systems with finite right-hand sides are confluent modulo identification of hypercollapsing subterms. This provides the first general confluence result for infinitary higher-order rewriting.
引用
收藏
页码：199 / 214
页数：16
相关论文
共 17 条
[1]  
ALBERT E, 2002, P 11 INT WORKSH FUNC, P7
[2]  
ARNOLD A, 1980, FUND INFORM, V4, P445
[3]   REWRITE, REWRITE, REWRITE, REWRITE, REWRITE, ... [J].
DERSHOWITZ, N ;
KAPLAN, S ;
PLAISTED, DA .
THEORETICAL COMPUTER SCIENCE, 1991, 83 (01) :71-96
[4]  
Fernández AJ, 2003, LECT NOTES COMPUT SC, V2562, P320
[5]  
Hanus M, 1996, LECT NOTES COMPUT SC, V1103, P138
[6]  
HANUS M, 1997, P 24 ACM S PRINC PRO, P80, DOI DOI 10.1145/263699.263710
[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]  
Ketema J, 2005, LECT NOTES COMPUT SC, V3467, P438
[10]  
Klop J.W., 1980, THESIS RIJKSUNIVERSI
12