Denotational models of type theory, such as set-theoretic, domain-theoretic, or category-theoretic models use (actual) infinite sets of objects in one way or another. The potential infinite, seen as an extensible finite, requires a dynamic understanding of the infinite sets of objects. It follows that the type $nat$ cannot be interpreted as a set of all natural numbers, $\lbrack\!\lbrack nat \rbrack\!\rbrack = \mathbb{N}$, but as an increasing family of finite sets $\mathbb{N}_i = \{0, \dots, i-1\}$. Any reference to $\lbrack\!\lbrack nat \rbrack\!\rbrack$, either by the formal syntax or by meta-level concepts, must be a reference to a (sufficiently large) set $\mathbb{N}_i$. We present the basic concepts for interpreting a fragment of the simply typed $\lambda$-calculus within such a dynamic model. A type $\varrho$ is thereby interpreted as a process, which is formally a factor system together with a limit of it. A factor system is very similar to a direct or an inverse system, and its limit is also defined by a universal property. It is crucial to recognize that a limit is not necessarily an unreachable end beyond the process. Rather, it can be regarded as an intermediate state within the factor system, which can still be extended. The logical type $bool$ plays an important role, which we interpret classically as the set $\{true, false\}$. We provide an interpretation of simply typed $\lambda$-terms in these factor systems and limits. The main result is a reflection principle, which states that an element in the limit has a ``full representative'' at a sufficiently large stage within the factor system. For propositions, that is, terms of type $bool$, this implies that statements about the limit are true if and only if they are true at that sufficiently large stage.

翻译：类型论的指称模型，如集合论模型、域论模型或范畴论模型，都以某种方式使用了（实）无限的对象集合。潜无限被视为可扩展的有限，需要对无限对象集合进行动态理解。因此，类型 $nat$ 不能被解释为所有自然数的集合 $\lbrack\!\lbrack nat \rbrack\!\rbrack = \mathbb{N}$，而应解释为一个递增的有限集族 $\mathbb{N}_i = \{0, \dots, i-1\}$。任何对 $\lbrack\!\lbrack nat \rbrack\!\rbrack$ 的引用，无论是通过形式语法还是元层次概念，都必须是对某个（足够大的）集合 $\mathbb{N}_i$ 的引用。我们提出了在此类动态模型中解释简单类型 $\lambda$-演算片段的基本概念。一个类型 $\varrho$ 被解释为一个过程，形式上是一个因子系统及其极限。因子系统与正向系统或逆向系统非常相似，其极限也通过泛性质定义。关键在于认识到极限并不一定是过程之外不可达的终点，而可以被视为因子系统内部仍可扩展的中间状态。逻辑类型 $bool$ 扮演着重要角色，我们将其经典地解释为集合 $\{true, false\}$。我们给出了简单类型 $\lambda$-项在这些因子系统及极限中的解释。主要结果是一个反射原理，该原理表明极限中的元素在因子系统内的某个足够大的阶段具有一个“完全代表元”。对于命题（即类型为 $bool$ 的项），这意味着关于极限的陈述为真当且仅当其在那个足够大的阶段为真。