检索结果-内蒙古大学图书馆

The extended predicative Mahlo universe in Martin-Lof type theory

JOURNAL OF LOGIC AND COMPUTATION 2023年第6期34卷 1032-1063页

作者： Dybjer, Peter Setzer, Anton Chalmers Univ Technol Dept Comp Sci & Engn Gothenburg Sweden Swansea Univ Dept Comp Sci Swansea Wales

This paper addresses the long-standing question of the predicativity of the Mahlo universe. A solution, called the extended predicative Mahlo universe, has been proposed by Kahle and Setzer in the context of explicit mathematics. It makes use of the collection of untyped terms (denoting partial functions) which are directly available in explicit mathematics but not in Martin-Lof type theory. In this paper, we overcome the obstacle of not having direct access to untyped terms in Martin-Lof type theory by formalizing explicit mathematics with an extended predicative Mahlo universe in Martin-Lof type theory with certain indexed inductive-recursive definitions. In this way, we can relate the predicativity question to the fundamental semantics of Martin-Lof type theory in terms of computation to canonical form. As a result, we get the first extended predicative definition of a Mahlo universe in Martin-Lof type theory. To this end, we first define an external variant of Kahle and Setzer's internal extended predicative universe in explicit mathematics. This is then formalized in Martin-Lof type theory, where it becomes an internal extended predicative Mahlo universe. Although we make use of indexed inductive-recursive definitions that go beyond the type theory $\mathbf {IIRD}$ of indexed inductive-recursive definitions defined in previous work by the authors, we argue that they are constructive and predicative in Martin-Lof's sense. The model construction has been type-checked in the proof assistant Agda.

关键词： Martin-Lof type theory Mahlo universes meaning explanations extended predicativity predicativity explicit mathematics inductive-recursive definitions indexed induction-recursion constructive mathematics Agda partial functions

来源：评论

学校读者我要写书评

暂无评论

Indexed induction-recursion

引用

JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING 2006年第1期66卷 1-49页

作者： Dybjer, P Setzer, A Chalmers Univ Technol Dept Comp Sci & Engn S-41296 Gothenburg Sweden Univ Wales Swansea Dept Comp Sci Swansea SA2 8PP W Glam Wales

An indexed inductive definition (IID) is a simultaneous inductive definition of an indexed family of sets. An inductive-recursive definition (IRD) is a Simultaneous inductive definition of a set and a recursive definition of a function on that set. An indexed inductive-recursive definition (IIRD) is it combination of both. We present a closed theory which allows Lis to introduce all IIRD in a natural way without Much encoding. By specialising it we also get a closed theory of IID. Our theory of IIRD includes essentially all definitions of sets which Occur in Martin-Lof type theory. We show in particular that Martin-Lof's computability predicates for dependent types and Palmgren's higher order universes are special kinds of IIRD and thereby clarify why they are constructively acceptable notions. We give two axiomatisations. The first formalises a principle for introducing meaningful IIRD by using the data-construct in the original version of the proof assistant Agda for Martin-Lof type theory. The second one admits a more general form of introduction rule, including the introduction rule for the intensional identity relation, which is not covered by the first axiomatisation. If we add an extensional identity relation to our logical framework, we show that the theories of restricted and general IIRD are equivalent by interpreting them in each other. Finally, we show the consistency of our theories by constructing a model in classical set theory extended by a Mahlo cardinal. (c) 2005 Elsevier Inc. All rights reserved.

关键词： dependent type theory Martin-Lof type theory inductive definitions inductive-recursive definitions inductive families initial algebras normalisation proofs generic programming

来源：评论

学校读者我要写书评

暂无评论

Partial recursive functions in Martin-Lof type theory

引用

2nd Conference on Computability in Europe (CiE 2006)

作者： Setzer, Anton Univ Coll Swansea Dept Comp Sci Swansea SA2 8PP W Glam Wales

ISBN: (纸本)3540354662

In this article we revisit the approach by Bove and Capretta for formulating partial recursive functions in Martin-Lof Type Theory by indexed inductive-recursive definitions. We will show that all inductive-recursive definitions used there can be replaced by inductive definitions. However, this encoding results in an additional technical overhead. In order to obtain directly executable partial recursive functions, we introduce restrictions on the indexed inductive-recursive definitions used. Then we introduce a data type of partial recursive functions. This allows to define higher order partial recursive functions like the map functional, which depend on other partial recursive functions. This data type will be based on the closed formalisation of indexed inductive-recursive definitions introduced by Dybjer and the author. All elements of this data type will represent partial recursive functions, and the set of partial recursive functions will be closed under the standard operations for forming partial recursive functions, and under the total functions.

关键词： Martin-Lof type theory computability theory recursion theory Kleene index Kleene brackets partial recursive functions inductive-recursive definitions indexed induction-recursion

来源：评论

学校读者我要写书评

暂无评论

Induction-recursion and initial algebras

引用

ANNALS OF PURE AND APPLIED LOGIC 2003年第1-3期124卷 1-47页

作者： Dybjer, P Setzer, A Chalmers Univ Technol Dept Comp Sci SE-41296 Gothenburg Sweden Univ Coll Swansea Dept Comp Sci Swansea SA2 8PP W Glam Wales

Induction-recursion is a powerful definition method in intuitionistic type theory. It extends (generalized) inductive definitions and allows us to define all standard sets of Martin-Lof type theory as well as a large collection of commonly occurring inductive data structures. It also includes a variety of universes which are constructive analogues of inaccessibles and other large cardinals below the first Mahlo cardinal. In this article we give a new compact formalization of inductive-recursive definitions by modeling them as initial algebras in slice categories. We give generic formation, introduction, elimination, and equality rules generalizing the usual rules of type theory. Moreover, we prove that the elimination and equality rules are equivalent to the principle of the existence of initial algebras for certain endofunctors. We also show the equivalence of the current formulation with the formulation of induction-recursion as a reflection principle given in Dybjer and Setzer (Lecture Notes in Comput. Sci. 2183 (2001) 93). Finally, we discuss two type-theoretic analogues of Mahlo cardinals in set theory: an external Mahlo universe which is defined by induction-recursion and captured by our formalization, and an internal Mahlo universe, which goes beyond induction-recursion. We show that the external Mahlo universe, and therefore also the theory of inductive-recursive definitions, have proof-theoretical strength of at least Rathjen's theory KPM. Crown Copyright (C) 2003 Published by Elsevier B.V. All rights reserved.

关键词： dependent type theory Martin-Lof type theory inductive definitions inductive-recursive definitions initial algebras large cardinals Mahlo cardinals Mahlo universes

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：