首页    期刊浏览 2024年11月06日 星期三
登录注册

文章基本信息

  • 标题:Realizability at Work: Separating Two Constructive Notions of Finiteness
  • 本地全文:下载
  • 作者:Marc Bezem ; Thierry Coquand ; Keiko Nakata
  • 期刊名称:LIPIcs : Leibniz International Proceedings in Informatics
  • 电子版ISSN:1868-8969
  • 出版年度:2018
  • 卷号:97
  • 页码:1-23
  • DOI:10.4230/LIPIcs.TYPES.2016.6
  • 出版社:Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
  • 摘要:We elaborate in detail a realizability model for Martin-Löf dependent type theory with the purpose to analyze a subtle distinction between two constructive notions of finiteness of a set A. The two notions are: (1) A is Noetherian: the empty list can be constructed from lists over A containing duplicates by a certain inductive shortening process; (2) A is streamless: every enumeration of A contains a duplicate.
  • 关键词:Type theory; realizability; constructive notions of finiteness
国家哲学社会科学文献中心版权所有