Realizability at Work: Separating Two Constructive Notions of Finiteness
Marc Bezem, Thierry Coquand, Keiko Nakata, Erik Parmann · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2018
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.