本机类型理论
本机类型理论是我和Mike Stay撰写的新论文。我们提出了一种编程语言推理的统一方法：将一种语言建模为一种理论，形成预滑轮类，并使用主题的内部语言。
语言→Λ分类→𝒫topos→Φ类型系统\ mathtt {language} \ xrightarrow {\; \ Lambda \;} \ mathtt {category} \ xrightarrow {\; \ mathscr {P} \;} \ mathtt {topos} \ xrightarrow {\; \ Phi \;} \ mathtt {type \;系统}
尽管这些步骤是已知的，但最初的方面只是组合及其在软件中的应用。如果实施得当，我们相信本机类型对虚拟世界非常有用。在这里，我想分享到目前为止我们学到的一些知识。
本文最大的教训是对约翰·贝兹（John Baez）所说的“数学之道”有信心。两年来，Mike和我以及Greg Meredith一直在寻找生成编程语言逻辑的方法。我们尝试了许多方法，但最终解决方案是最简单的。
1.每个类别都嵌入到其书前主题中。 \文本1。每个类别都嵌入到其预备主题中。}
2.每个主题都有丰富的内部语言。 \ text {2。每个主题都有丰富的内部语言。}
嵌入保留了限制和指数，因此我们可以将其应用于“高阶理论”。
现在，我们探讨主题语言。有多种视图，并且经常不使用其全部功能。目的支持几何逻辑，谓词逻辑以及从属类型理论。我们强调后者：从属类型具有表达性和普遍性，但在数学中并未得到充分利用。
我的思想受到这样一个观念的影响，即连基础都是绝对的。几乎所有语言都可以建模为结构化类别：我发现的最全面的参考文献是Bart Jacobs的分类逻辑和类型理论。
逻辑研究最多的分类结构可能是主题。以滑轮为目的，将数据连贯地分配给空间的函子首先应用于代数几何。连续贴图f：X→Y f：X \ to Y产生逆像f：Sh（Y）→Sh（X）f：Sh（Y）\ to Sh（X）是保留有限极限的左伴随。这给出了假肢的几何形态，而几何逻辑（∧\ wedge和∃\ exists）是对假肢进行分类的语言。
尽管几何逻辑是普遍性的重要水平，但是姿势的语言却更为强大。 1965年，在加利福尼亚的拉霍亚，萌芽类别理论界将格洛腾迪克的滑轮类别视为从根本上讲是集合理论的逻辑结构。基本主题是具有有限限制的笛卡尔封闭类别和子对象分类器，该子对象表示谓词和子对象的对应关系。
谓词纤维化ΩT→T关于谓词（如子集）的原因； \ text {谓词纤维化} \; \ Omega \ text {T} \至\ text {T} \; \ text {关于谓词的原因，例如子集；}
共域纤维化ΔT→T是有关依赖类型（如索引集）的原因。 \ text {共域纤维化} \; \ Delta \ text {T} \至\ text {T} \; \ text {有关依赖类型的原因，例如索引集。}
在整个数学中，我们使用Set的内部谓词逻辑。这是一个典型的典范例子：谓词，例如φ（x）=（x + 3≥5）\ varphi（x）=（x + 3 \ geq 5）是一个函数φ：X→2 = {t ，f} \ varphi：X \ to 2 = \ {t，f \}，这与它的理解相对应，即真项{x∈X | （（x）= t}⊆X \ {x \ in X \; | \; \ varphi（x）= t \} \ subseteqX。
在任意集合X X上的谓词形成布尔代数P（X）= [X，2] P（X）= [X，2]，按蕴涵顺序排序。每个函数f：X→Y f：X \ to Y给出一个逆像P（f）：P（Y）→P（X）P（f）：P（Y）\ to P（X）。这就定义了一个函子P：设置op→Bool P：Set ^ {op} \到Bool，它是一阶高阶学说：每个P（f）P（f）都有伴随词∃f⊣P（f）∀f \ exist_f \ dashv P（f）\ dashv \ forall_f表示量化，它满足Beck-Chevalley条件。
∀x，y：ℚ。 ∃z：ℚ。 x ＜ ∧ y \ forall x，y：\ mathbb {Q}。\; \ exists z：\ mathbb {Q}。\\ x \ lt z \ wedge z \ lt y
∀f：Y X。 y y：是的。 ∃x：X。 f（x）= y⇒g：X Y。 ∀y：是的。 f（g（y））= y \ forall f：Y ^ X。\; \ forall y：Y. \; \存在x：X。\; f（x）= y \ Rightarrow \存在g：X ^ Y。\; \ forall y：Y. \; f（g（y））= y
这个想法是众所周知的。人们经常谈论主题的“ Mitchell-Benabou语言”。但是，这种语言是基于简单类型理论的谓词逻辑，这意味着唯一的类型形成规则是乘积和函数。数学中的许多构造都不适用于该语言，因为类型通常取决于术语：
ℤp：＝ℤ/⟨x〜y∃z：ℤ。 （x − y）= z⋅p⟩\ mathbb {Z} _p：= \ mathbb {Z} / \ langle x \ sim y \ equiv \存在z：\ mathbb {Z}。\ （x-y）= z \ cdot p \ rangle
这是通过使用依赖类型扩展谓词逻辑来提供的，这将在下一节中进行介绍。
因此，我们已经简要讨论了Set的结构如何允许日常数学中使用的谓词的显式构造。重要的是可以在任何主题中构建这些逻辑：因此，我们概括了逻辑的历史概念。
例如，在PREPHEAF TOPOS [C OP，SET] [C ^ {OP}，\ TEXT {SET}]中，排除中间的法律并没有持有，并且有充分的理由。对筛子的否定必然比对子集的否定更微妙，因为我们必须排除态势不在但“预示”筛子中的可能性。这将在申请帖子中进行更多。
依赖性在整个数学中都是普遍存在的。什么是一条龙？它是一个设置的m m，然后在m m，e m，e上的操作，然后在m，e m，e上的条件。大多数对象都以图层构建，每个对象依赖于之前。类型理论通常被视为“花哨”，只有在复杂的情况下必要，类似于类别理论的误解;然而，无处不在的类型。
基本思想是表示使用预报的依赖性。一种类型，取决于另一种类型的术语，x：a∈B（x）：x：\ vdash b（x）：类型，可以理解为索引集{b（x）} x：a \ { B（x）\} _ {x：a}，又表示为函数∐x：a。 b（x）→a \ coprod x：a。 b（x）\ to a。因此，“依赖a”的“类型的世界”是切片类别设置/ A / A。
“A-redicates”的POSET坐在“A-型”的类别内：理解为注射{x∈A| φ（x）}→a \ {x \中的\; | \; \ varphi（x）\} \ to a。这是一种退化类型的依赖类型，其中Premages是真理值而不是集。因此，我们正在扩展到更大的环境，该环境共享所有相同的结构。切片类别设置/ a / a是p（a）p（a）的分类：其态度是通勤三角形，理解为一个索引的函数。
每个功能f：a→b f：a \ to b给出了函授f *：f ^ \ ast：set / b→/ b \ toset / a / a / a按回调;这概括了预测，并且可以表达为替代：给定P：S→B P：S \到B，我们可以形成A型
此函数具有伴随σf⊣f*⊣πf \ sigma_f \ dashv f ^ \ ast \ dashv \ pi_f，称为依赖和和依赖性产品：这些是构造依赖类型的强大工具。它们不仅概括量化，还概括了产品和HOM：三重协调会在Set / B / B上引导伴随CO / Monad
σf∘f* = - ×f⊣[f， - ] =πf∘f*。 \ sigma_f \ circ f ^ \ ast = - \ times f \ dashv [f， - ] = \ pi_f \ circ f ^ \ ast。
索引总和通过允许第二坐标的类型取决于第一坐标中的术语来概括产品类型。例如：Σn：ℕ。 List（n）\ Sigma n：\ mathbb {N}。\ text {List}（n）由依赖对pairs n，l组成：List（n）⟩\ langle n，l：\ text {List}（n） \ rangle。
索引产品通过允许共域的类型取决于域中的术语来概括功能类型。例如：S S：设置。列表（S）\ Pi S：\ text {Set} .List（S）由相关函数λS：Set组成。 φ（S）：列表（S）\ lambda S：\ text {Set}。\ varphi（S）：List（S）。
看看它们有多自然？我们一直在无意识地使用它们。只需使用原像进行索引，我们就可以将产品和功能类型泛化为“分支”版本，从而使我们能够构建诸如
Monoid：=ΣM：设置。 ∑m：M 2→M。 Σe：1→M。 。 。 \ text {Monoid}：= \ Sigma M：\ text {Set}。\ Sigma m：M ^ 2 \至M. \ Sigma e：1 \至M ...
任何主题都可以使用这种丰富的语言。我认为我们几乎还没有开始看到它在数学，计算和日常生活中的作用。
主题有两个系统，谓词逻辑和从属类型理论。每种模型都通过纤维化，仿射器建模，而A的原像是A A谓词/ A A型。域中的态射是对形式的一种判断，即“在这些（相关）类型的变量的上下文中，该术语属于该（相关）类型”。
这两个纤维通过将谓词转换为类型的理解和通过将类型转换为谓词的图像分解连接在一起。这些结果表明谓词纤维化是纤维化类型的反射性子类别。
总之，这构成了主题的完整的高阶依赖类型理论。 据我所知，就其全部荣耀而言，这就是应该被称为“主题”的“语言”。 这种类型理论用于Coq和Agda等证明助手中。 最终，这种表达逻辑+依赖类型将在许多编程语言中使用。 本机类型理论为多种语言提供了一个共享的推理框架。 我们认为，如果将其集成到现有系统中，这可能会对软件和系统设计产生重大影响。 在下一篇文章中，我们将探讨为什么这种语言对理论上的先发制人主题如此有用。 请让我知道有关此职位，尤其是本文的任何想法或问题。 谢谢你。 UTC于2021年2月20日上午1:59发表
