| On the internal structures of inductive types |
| |
| 作者姓名： | 傅育熙 |
| |
| 作者单位： | Department of |
| |
| 基金项目： | Center of Basic Studies in Computing Science，Shanghai Education Commission，BASICS is affiliated to the Department of Computer Science at Shanghai Jiaotong University |
| |
| 摘 要： | The paper investigates the internal structures of hereditary inductive types in logical type theory. By defining a bisimulation equality on the inhabitants of each hereditary inductive type, one is able to show that the inhabitants of a hereditary inductive type satisfy the basic properties of sets. A hereditary inductive type can therefore be conceived as a universe of sets.
|
On the internal structures of inductive types |
| |
| FU Yuxi.On the internal structures of inductive types[J].Science in China(Technological Sciences),2000,43(5). |
| |
| Authors: | FU Yuxi |
| |
| Abstract: | The paper investigates the internal structures of hereditary inductive types in logical type theory. By defining a bisimulation equality on the inhabitants of each hereditary inductive type, one is able to show that the inhabitants of a hereditary inductive type satisfy the basic properties of sets. A hereditary inductive type can therefore be conceived as a universe of sets. |
| |
| Keywords: | type theory inductive type construction |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
