DECIDABILITY AND CONFLUENCE OF BETA-ETA-TOP(LESS-THAN-OR-EQUAL-TO) REDUCTION IN F(LESS-THAN-OR-EQUAL-TO)

被引：6

作者：

CURIEN, PL ^{[1
]}

GHELLI, G ^{[1
]}

机构：

[1] UNIV PISA,DIPARTIMENTO INFORMAT,I-56100 PISA,ITALY

来源：

INFORMATION AND COMPUTATION | 1994年 / 109卷 / 1-2期

关键词：

D O I：

10.1006/inco.1994.1014

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We contribute to the syntactic study of F less-than-or-equal-to a variant of second-order lambda-calculus F which appears as a paradigmatic kernel language for polymorphism and subtyping. The type system of F less-than-or-equal-to has a maximum type Top and bounded quantification. We endow this language with the beta-rules (for terms and types), to which we add eta-rules (for terms and types) and a rule which equates all terms of type Top. These rules are suggested by the axiomatization of cartesian closed categories. We exhibit a weakly normalizing and confluent reduction system for this theory betaeta top less-than-or-equal-to and show that it is decidable. It is also confluent, but decidability does not follow from confluence, since reduction is not effective. Our proofs rely on the confluence and decidability of a corresponding system on F1 (the extension of F with a terminal type). (C) 1994 Academic Press, Inc.

引用

页码：57 / 114

页数：58

共 50 条

[31] PHOTOPRODUCTION OF NA-24 FROM TARGETS WITH 63 LESS-THAN-OR-EQUAL-TO AT LESS-THAN-OR-EQUAL-TO 238
JARUND, A
FORKMAN, B
ZEITSCHRIFT FUR PHYSIK A-HADRONS AND NUCLEI, 1977, 281 (1-2): : 39 - 45
[32] COULOMB DISPLACEMENT ENERGIES BETWEEN ANALOG LEVELS FOR 44 LESS-THAN-OR-EQUAL-TO A LESS-THAN-OR-EQUAL-TO 239
ANTONY, MS
BRITZ, J
PAPE, A
ATOMIC DATA AND NUCLEAR DATA TABLES, 1988, 40 (01) : 9 - 56
[33] ISOTOPIC COMPOSITION OF COSMIC-RAYS WITH 5 LESS-THAN-OR-EQUAL-TO Z LESS-THAN-OR-EQUAL-TO 26
FISHER, AJ
HAGEN, FA
MAEHL, RC
ORMES, JF
ARENS, JF
ASTROPHYSICAL JOURNAL, 1976, 205 (03) : 938 - 946
[34] SHELL STRUCTURE EFFECTS UPON LEVEL DENSITIES FOR 38 LESS-THAN-OR-EQUAL-TO A LESS-THAN-OR-EQUAL-TO 57
BECKERMAN, M
BULLETIN OF THE AMERICAN PHYSICAL SOCIETY, 1977, 22 (04): : 529 - 529
[35] AL(N,XGAMMA) REACTIONS FOR 5.3 LESS-THAN-OR-EQUAL-TO EN LESS-THAN-OR-EQUAL-TO 9.0 MEV
DICKENS, JK
PHYSICAL REVIEW C, 1972, 5 (01): : 100 - +
[36] THEORETICAL IONIZATION ENERGIES AND GEOMETRIES FOR NIN (4 LESS-THAN-OR-EQUAL-TO N LESS-THAN-OR-EQUAL-TO 9)
NYGREN, MA
SIEGBAHN, PEM
WAHLGREN, U
AKEBY, H
JOURNAL OF PHYSICAL CHEMISTRY, 1992, 96 (09) : 3633 - 3640
[37] PREPARATION AND PROPERTIES OF LIXVS2 (0 LESS-THAN-OR-EQUAL-TO X LESS-THAN-OR-EQUAL-TO 1)
MURPHY, DW
CROS, C
DISALVO, FJ
WASZCZAK, JV
ABSTRACTS OF PAPERS OF THE AMERICAN CHEMICAL SOCIETY, 1977, 174 (SEP): : 7 - 7
[38] MEASUREMENT OF THE KL(0)P ELASTIC CROSS-SECTION FOR 3 LESS-THAN-OR-EQUAL-TO P LESS-THAN-OR-EQUAL-TO 13GEV-C AND 0.1 LESS-THAN-OR-EQUAL-TO [T] LESS-THAN-OR-EQUAL-TO 1.3 GEV2
CITTOLIN, S
GASPARINI, F
LIMENTANI, S
MITTNER, P
POSOCCO, M
VOCI, C
CHAUVEAU, J
CROZON, M
DIACZEK, A
LEFIEVRE, B
LERUSTE, P
MAS, J
SENE, R
TOCQUEVILLE, J
NUCLEAR PHYSICS B, 1979, 157 (02) : 197 - 211
[39] 1H-NMR STUDIES OF THE SYSTEMS TA1-XVXHY (0.0 LESS-THAN-OR-EQUAL-TO X LESS-THAN-OR-EQUAL-TO 1.0-0 LESS-THAN Y LESS-THAN-OR-EQUAL-TO 0.9), AND NB1-XVXHY (0.0 LESS-THAN-OR-EQUAL-TO X LESS-THAN-OR-EQUAL-TO 0.5-0 LESS-THAN Y LESS-THAN-OR-EQUAL-TO 0.9) - MAGNETIC-SUSCEPTIBILITY, KNIGHT-SHIFT, AND LONGITUDINAL RELAXATION
RICHTER, KH
WEISS, A
BERICHTE DER BUNSEN-GESELLSCHAFT-PHYSICAL CHEMISTRY CHEMICAL PHYSICS, 1988, 92 (07): : 833 - 840
[40] BULK PLASMON DISPERSION IN SI FOR O LESS-THAN-OR-EQUAL-TO Q LESS-THAN-OR-EQUAL-TO 1.5 QF
CHEN, CH
MEIXNER, AE
KINCAID, BM
BULLETIN OF THE AMERICAN PHYSICAL SOCIETY, 1980, 25 (03): : 436 - 436

← 1 2 3 4 5 →