在对当前几何的稀薄氛围进行了一次激动人心的冒险之后，我想回到一些更依赖于散文的类型-这是我书中第二章讨论的主题。几年前，在迈克发表的赞扬依赖类型的博文中，我们已经对这个主题赞不绝口，因此才有了这篇文章的标题。
我刚刚看了凯文·巴扎德的演讲--霍特是做数学的方法吗？凯文是伦敦帝国理工学院的一名数字理论家，他希望培训他的本科生在精益定理证明器中为主流理论(例如，关于环和方案的代数几何定理)提供经过计算机检查的证明。
他们使用依赖类型，即使他们不知道自己正在使用依赖类型。
让我们希望他们能像莫里埃的乔丹先生一样高兴地收到这个消息：
“Par ma foi！如果没有散文的话，我就不会这么做了，我也不会这么做，因为我不会这么做的，我不会这样做的，因为我不会这么做的，我不会让你的生活变得更美好的，因为我不会让你的生活变得更美好，也不会让你的生活变得更美好。vbl.)。
“我的信仰！四十多年来，我一直在说散文，却一无所知，我是世界上最感谢您告诉我的人。“。
因此，Kevin选择了精益而不是基于集合的证明者，因为它使用了这些依赖类型。然后他在他的演讲中继续考虑是否应该选择内置单价的系统，但这是另一天的话题。
关于数学家为什么使用依赖类型，我有一个简单的解释。他们这样做首先是因为他们是自然语言的使用者，因此他们已经在使用依赖类型了。后一点我们可能早在1994年就从Aarne Ranta的优秀的类型理论语法中学到了。
认识到自然语言和数学语言之间的共性，兰塔在最近的一篇论文中告诉我们，数学是了解语言是如何工作的一个很好的地方：
数学语言的主要特点可能是社区的不同成员可以完全同意每个单词和句子的意思。这意味着人们可以想当然地认为这些意义是理所当然的，并在不确定什么是正确的数据分析的情况下分析潜在的机制。从这个意义上说，数学语言为语义学和语用学的研究提供了“实验室条件”。(兰塔2020，第122页)。
兰塔，A.2020年。“关于数学语言中的语用学的一些评论”，“语用学杂志”第160期，第120-122页。
因此，非正式数学是一个尝试和理解潜在语言结构的好地方，他在1993年的论文“类型理论和数学的非正式语言”中研究了这一点。它考察了形式数学和非正式数学之间的两个方向：糖化和形式化。
独立类型论解释语言的重要主题是代词和量词。从后者开始，任何从属类型x：A⊢B(X)：Type x：A\vdash B(X)：Type都会产生两个非从属类型：
这些赋值是将类型C、C发送到常量依赖类型的赋值的左右附加项：
(练习：假设这些附加项，证明自然数的算术恒等式a∑bi=∏i a^{\sum b_i}=\prod_i a^{b_i}和∏i(Bi)a=(∏i bi)a\prod_i(B_I)^a=(\prod_i b_i)^a。)。
当B(X)B(X)是一个命题时，这些量化类型是“A As That are B B”(“截断”为“某个A A是B B”)和“每个A A都是B B”。
兰塔所说的数学中缺失的那种歧义在自然语言中经常出现。语言哲学家对我们如何确定量词的范围感到困惑，就像有人说“每个瓶子都是绿色的”一样。当然，这并不意味着世界上的每一瓶酒。这可能并不意味着房子里的每一瓶酒，甚至房间里的每一瓶都不是。当然，上下文很重要。例如，说这句话的人可能刚从商店带着精选的葡萄酒回来。
依赖类型理论认为存在大量的隐式参数。“Every”是“Every A Every_A”，其中A A是一种类型。指示词也是如此，各式各样。对参数的需求是由那种想要淡化语境作为意义的独立决定因素的语言哲学家感受到的，像杰森·斯坦利(Jason Stanley)一样，他可以坚持：
所有语言外语境的真值条件效应都可以追溯到逻辑形式。(语境中的语言，OUP，2007，第30页)。
Stanley谈到了“上下文依赖”、“领域索引”、“隐蔽代词元素”和“未发音的句法结构”。我的主张是，如果这有任何成功的机会，它必须通过依赖类型理论的逻辑形式来实现。当听到“每个瓶子都是绿的”中的“each”时，我们搜索对应的隐式类型。“瓶子”是一个线索，可能会引导我们找到想要的“刚从商店带回家的瓶子”的上下文。
尽管表面上看不出这一点，但这不能仅仅是随着时间的推移而量化。如果约翰总是在纽约点燃香烟，而同时伦敦又总是下雨，这就不支持这个命题。一定是和约翰在同一地点下雨。
我想说动词‘rain’有隐含的时间和地点参数。一项成就，比如“约翰点燃一支烟”，是有时间和地点的。这个命题声称，约翰点燃香烟的每一项成就都发生在一个时间和地点，以至于当时和那里都会下雨。
简而言之，关于代词，我看到的首批以依赖类型理论呈现的自然语言之一是桑德霍尔姆对驴子句子的版本：
这可能会让人觉得有点不自然，但很容易设计出类似形式的句子，特别是如果我们选择“Any”而不是“Every”的话：
(在泽诺·温德勒的“每个人、任何人和所有人”中，可以找到对这一选择和类似选择的微妙之处的论述。)。
关键是，有两种东西之间有关系，这里是人和枪，一个人可能没有，可能是一支，或者很多支。我们用不定冠词‘a’来表示枪，但似乎想用‘it’来指特定的东西。
∏z：∑x：a∑y：b R(x，y)S(p(Z)，p(q(Z))，\prod_{z：\sum_{x：a}\sum_{y：b}R(x，y)}S(p(Z)，p(q(Z)，其中p和q是第一和第二分量的投影。我们看到‘it’对应于p(q(Z))p(q(Z))。
∀x∀y(A(X)&；B(Y)&；R(x，y)→S(x，y))，\for all x\forall y(A(X)\&；B(Y)\&；R(x，y)\to S(x，y))，似乎更接近于原始的语言形式。
任何有适当因子m m的数n n都是n>；m n\gt m。
发布于世界协调时2020年5月10日下午4：57