为什么我们需要单独的 П 类型表示法？

Question

主要的

我对 П 类型需要单独表示法的动机感到困惑，您可以在从 λ2 开始的类型系统中找到这种表示法。答案通常是这样的 - 想想如何表示恒等函数的签名 - 它可以是 λa:type.λx:a.x 或者 λb:type.λx:b.x. 。他们说，微妙之处在于这两个签名不仅 not equal, 它们与类型变量的 alpha 不等价 a 和 b 是其相应抽象内部的自由变量. 。因此，为了克服这个讨厌的语法问题，我们提出了 П 绑定器，它可以很好地处理 alpha 转换。

所以问题是：这是为什么？为什么不直接修正 alpha 等价的概念呢？

更新z：

哦，我真傻， λa:type.λx:a.x 和 λb:type.λx:b.x 是阿尔法等价的。但为什么 a:type -> a -> a 和 b:type -> b -> b 那就不行了。

更新如下：

啊哈，有趣，我想这是选择性失明的完美例子=D

我正在看书 类型论和形式证明, ，在关于 lambda2 的章节中，作者提出了 П 正是使用这种论证——人们不能这么说 \t:*.\v:t.v : * -> t -> t 因为这使得两个 alpha 等价项\t:*.\v:t.v 和 \g:*.\v:g.v 有不同的类型，因为相应的类型不是 alpha 等价的，其中类型如 t:* -> t -> t 实际上是 alpha 不变的。 注意之间的区别 t:* -> t -> t 和 * -> t -> t. 。但是，这不是让这个争论变得有点微不足道吗？谈论类型甚至有意义吗？ a -> b 在哪里 a 和 b 不受任何量词变量的约束。Andrej Bauer 在评论中指出 П 它确实类似于带有一些附加功能的 lambda 抽象。

总而言之，我已经完成了，谢谢大家.

Answer 1

我认为我们只需要在这里弄清楚一些事情：

1. 在表达式中 $\lambda a :\mathsf{类型} 。\lambda x ：A 。x$ 变量 $a$ 已绑定 （由外 $\lambda$）。表达式 $\lambda a :\mathsf{类型} 。\lambda x :A 。x$ 和 $\lambda b :\mathsf{类型} 。\lambda x :b.x$ 是 $\阿尔法$-平等的。
2. 表达方式 $\lambda a :\mathsf{类型} 。\lambda x :A 。x$ 是 恒等函数，它是 不是 “身份函数的签名”。
3. 如果“恒等函数的签名”是指“恒等函数的类型”，那么它会是这样的 $\Pi_{a：\mathsf{类型}} 。（一个\到一个）$, ，或者如果您只想要产品类型，那么它是 $\Pi_{a：\mathsf{类型}} \Pi_{x :a} a$.

还有问题吗？

也许这会有所帮助：

• 恒等函数的类型 $\lambda x :A 。x$ 是 $a \到a$
• 恒等函数的类型 $\lambda y :b.y$ 是 $b \到 b$
• 功能 $\lambda x :A 。x$ 和 $\lambda y :b.y$ 是不同的
• 类型 $a \到a$ 和 $b \到 b$ 是不同的
• 的类型 多态性 恒等函数 $\lambda c :\mathsf{类型} 。\lambda z ：C 。z$ 是 $\Pi_{c：\mathsf{类型}} 。c \ 到 c$.
• 功能 $\lambda a :\mathsf{类型} 。\lambda x :A 。x$ 和 $\lambda c :\mathsf{类型} 。\lambda z ：C 。z$ 是 $\阿尔法$-平等的
• 类型 $\Pi_{a：\mathsf{类型}} 。一个\到一个$ 和 $\Pi_{c：\mathsf{类型}} 。c \ 到 c$ 是 $\阿尔法$-平等的。

补充： 在与亚历克斯·辛普森喝杯茶交谈后，我还可以说一件事。我们不 需要 分离 $\lambda$ 和 $\Pi$ 构造函数，因为它们都具有完全相同的语法形状（采用两个参数，绑定一个变量）。事实上，如果我没记错的话 自动数学 使用相同的符号 $\lambda$- 抽象和 $\Pi$-类型。但重点是我们 想 使用两个不同的构造函数，因为它们表示 不同的概念.