کد مقاله کد نشریه سال انتشار مقاله انگلیسی ترجمه فارسی نسخه تمام متن
4661566 1344843 2016 24 صفحه PDF ندارد دانلود رایگان
عنوان انگلیسی مقاله
A constructive manifestation of the Kleene–Kreisel continuous functionals
ترجمه فارسی عنوان
تظاهر سازنده از توابع مستمر کلین ـ کریسل
کلمات کلیدی
ریاضیات و سازنده؛ تداوم یکنواخت؛ فن های کاربردی. قرقره؛ توابع مستمر کلین کریسل؛ نظریه نوع شهودی
03B15; 03F50; 03C90; 03D65Constructive mathematics; Uniform continuity; Fan functional; Sheaves; Kleene–Kreisel continuous functionals; Intuitionistic type theory
موضوعات مرتبط
مهندسی و علوم پایه ریاضیات منطق ریاضی
چکیده انگلیسی

We identify yet another category equivalent to that of Kleene–Kreisel continuous functionals. Reasoning constructively and predicatively, all functions from the Cantor space to the natural numbers are uniformly continuous in this category. We do not need to assume Brouwerian continuity axioms to prove this, but, if we do, then we can show that the full type hierarchy is equivalent to our manifestation of the continuous functionals. We construct this manifestation within a category of concrete sheaves, called C-spaces, which form a locally cartesian closed category, and hence can be used to model system T and dependent types. We show that this category has a fan functional and validates the uniform-continuity principle in these theories. Our development is within informal constructive mathematics, along the lines of Bishop mathematics. However, in order to extract concrete computational content from our constructions, we formalized it in intensional Martin-Löf type theory, in Agda notation, and we discuss the main technical aspects of this at the end of the paper.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Annals of Pure and Applied Logic - Volume 167, Issue 9, September 2016, Pages 770–793
نویسندگان
, ,