Structures definable in polymorphism

被引：2
作者：
Yuxi Fu
机构：
[1] Shanghai Jiao Tong University,Department of Computer Science
来源：
Journal of Computer Science and Technology | 1998年 / 13卷 / 6期
关键词：
Polymorphic types; type theory;
D O I：
10.1007/BF02946501
中图分类号：
学科分类号：
摘要：
Encodings in polymorphism with finite product types are considered. These encodings are given in terms ofI-algebras. They have the property that the ground terms are precisely the closed normal terms of the encoded types. The proof of a well-known result is transplanted to the setting and it is shown why weak recursion is admissible. The paper also shows how to carry out the dual encodings using the existential quantifier.
引用
收藏
页码：579 / 587
页数：8
相关论文
共 8 条
  • [1] Böhm C(1985)Automatic synthesis of typed λ-program on term algebras Theoretical Computer Science 39 135-154
  • [2] Berarducci A(1986)Generalized algebraic theories and contextual categories Annals of Pure and Applied Logic 32 209-243
  • [3] Cartmell J(1996)Recursive models of general inductive types Fundamenta Informatiae 26 115-131
  • [4] Fu Y(1997)Categorical properties of logical frameworks Mathematical Structures in Computer Science 7 1-47
  • [5] Fu Y(1997)Constructive sets in computable sets Journal of Computer Science and Technology 12 425-440
  • [6] Fu Y(1991)Inductive types and type constraints in the second-order lambda calculus Annals of Pure and Applied Logic 51 159-172
  • [7] Mendler N(1992)The extended calculus of constructions (ECC) with inductive types Information and Computation 99 231-264
  • [8] Ore C(undefined)undefined undefined undefined undefined-undefined
1