介绍 ：
在词源上，集合是不同元素的集合，这些元素可能具有某些特定的共同点和类型的意思——“特定类型的”。
这两个术语在数学方面至关重要，因为它们产生了集合论和类型论。本文提供了集合和类型在数学上的语义差异。
1套 ：
套装概览 –
- 在数学中，集合是不同元素的集合。
- 集合用大写字母斜体表示，如A、E、D等。
- 与 set 相关的问题可能会导致正确或错误的结果。
- 集合导致集合论。
- 成立于19世纪。
- George Cantor 发现了集合论，也被称为集合论之父
- 集合论最终导致格的概念，然后是布尔代数。它是布尔代数的根。
集合论
意识形态——
- 集合的意识形态是“集合”。
- 考虑数学中的预定义对象。这些预定义的对象可以被分析、研究，并且可以根据某些因素放在不同的组中。这些组形成集合，一个集合就是一个“集合”。
- 例如圆、点和线位于一个平面内，因此它们可以形成一个集合。
套装特点——
- 集合具有与之关联的“元素”。
- 在集合论中，一个元素可以属于多个集合。
- 数字可以用来表示集合。 (0 表示空集，1 表示包含空集的集)。
- 集合论源于逻辑。因此，诸如谓词逻辑之类的概念需要一个单独的系统。
- 集合具有与之关联的操作。一些基本操作是-联合、交集、补集和笛卡尔积。
- 为了检查一个元素是否属于一个集合，需要“证明”。
集合的应用 –
- 集合在数学中有它的应用。集合在数学中是通用的(就语言而言)。集合用于构造关系。
- Set 用于识别和存储计算机编程中的唯一元素。
- Set 奠定了布尔代数的基础。
- Set 奠定了计算机科学一个非常重要的分支——数字电子学——的基础。
- Set 最终导致了类型论的基础。
例子 –
N 是所有自然数的集合，使得 N={1,2,3,4,..} .Z 是所有整数的集合，使得 Z={-3,-2,-1,0,1, 2,3,..}。集合 B={true, false} 是一组布尔值。
2. 类型：
类型论
类型概述 –
- 数学中的类型是在评估一个术语时产生的某种值的集合。
- 一个类型用 τ 表示。
- 第一类需要证明所问的问题是否有意义。
- 类型导致类型理论。
- 类型理论最终在 1902 年至 1908 年间奠定了基础，当时伯特兰·罗素提出了各种类型理论。
- 类型源于集合论。
- 类型论是为了消除形式逻辑的不一致，重写系统和朴素集合论而产生的。
意识形态——
- 类型的意识形态是“建设”。
- 在数学中，对象是根据规则构造的。
- 这些对象的组织根据它们的构造将它们分类为不同的“类型”。
- 数学中的对象以独特的方式构造，从而产生独特的类型。
类型特征——
- 类型具有与之关联的“术语”。
- 在类型论中，术语通常只属于一种类型。
- 在类型理论中，数字用于表示函数。术语“and”和“or”可以编码为类型本身。不需要单独的系统。
- 与类型相关的特征是依赖类型、相等类型、归纳类型、Universe 类型和计算组件。
- 为了检查术语是否属于特定类型，需要“算法”。
类型的应用 –
- 类型理论对证明助手、编程语言、数学基础、语言学和社会科学产生实际影响。
- 在编程语言中，类型系统用于识别错误。
- 证明检查器、证明助手、自动证明定理使用类型理论对数学中的证明进行编码。
- Gregory Bateson 逻辑级别和双重绑定概念源自类型理论。
- 不同类型的语法使用类型理论对类型(如名词、动词)进行分类。
- 类型理论用于语言语义。
例子 –
如果 3 的类型为nat ，则存在类型为I nat 3 3 的项。 3+(7*8) 5也是 Nat 类型。 (在集合中，这可以用表达式 3∈{n∈N∣∀x,y,z∈N+(xn+yn≠zn)} 表示)。类型理论中的 M:A 被评估为 M 是数据类型 A 的项。
简短而基本的例子
结论 –
虽然集合和类型不同，但它们有明显的相关性。每种类型都会产生一组该类型的实体。事实上，类型论的根源在于集合论。如果在扩展中考虑，集合也可以被视为类型。不同的类型可能会产生相同的集合。