Intuitionistic model constructions and normalization proofs
Intuitionistic model constructions and normalization proofs
复制标题
直观的模型构建和规范化证明
DOI：
--
复制
发表时间：
1997
影响因子：
0.5
通讯作者：
P. Dybjer
中科院分区：
文献类型：
--
作者：
T. Coquand;P. Dybjer
传统的强归一化和弱归一化概念是指二元约简关系的性质。在本文中，我们探索了一种标准化的替代方法，在这种方法中，我们绕过了约简关系，转而关注标准化函数，即将项映射到其正规形式的函数。我们使用直观的元语言，并将规范化函数描述为从可转换项的等价类中选择规范代表的算法。这意味着我们也得到了可兑换性的决策算法。这种归一化函数可以通过构建适当的模型和函数引用来构建，函数引用与解释函数相反。然后将引用函数与解释函数组合得到归一化函数。我们还讨论了构造函数是一对一的性质的一个简单证明，这个性质通常是作为传统意义上的Church-Rosser和归一化的推论得到的。我们通过展示粘合模型（与范畴论中使用的粘合结构密切相关）如何产生Gödel系统t的组合公式的规范化算法来说明这种方法。然后，我们展示了当我们添加笛卡尔积和不相交并（Curry-Howard解释下的完全直觉命题逻辑）和超越归纳类型（如browwer序数）时，该方法如何以一种直接的方式扩展。
The traditional notions of strong and weak normalization refer to properties of a binary reduction relation. In this paper we explore an alternative approach to normalization, in which we bypass the reduction relation and instead focus on the normalization function, that is, the function that maps a term to its normal form. We work in an intuitionistic metalanguage, and characterize a normalization function as an algorithm that picks a canonical representative from the equivalence class of convertible terms. This means that we also get a decision algorithm for convertibility. Such a normalization function can be constructed by building an appropriate model and a function quote, which inverts the interpretation function. The normalization function is then obtained by composing the quote function with the interpretation function. We also discuss how to get a simple proof of the property that constructors are one-to-one, which is usually obtained as a corollary of Church–Rosser and normalization in the traditional sense. We illustrate this approach by showing how a glueing model (closely related to the glueing construction used in category theory) gives rise to a normalization algorithm for a combinatory formulation of Gödel System T. We then show how the method extends in a straightforward way when we add cartesian products and disjoint unions (full intuitionistic propositional logic under a Curry–Howard interpretation) and transfinite inductive types such as the Brouwer ordinals.