なぜПタイプに別の表記が必要なのですか？

Aug 24 2020

メイン

λ2以降の型システムで見られる、П型の別個の表記法の必要性の背後にある動機について私は混乱しています。答えは通常はそうように書きます-それはすることができます- 1は恒等関数のシグネチャを表現することができる方法を考えますλa:type.λx:a.xかλb:type.λx:b.x。微妙な部分は、彼らが言う、これら2つの署名だけではなく、ということですnot equal、彼らはアルファ同等の型の変数としてではありませんaし、bその対応の抽象化内部の自由変数です。したがって、この厄介な構文上の問題を克服するために、アルファ変換でうまく機能するПバインダーを紹介します。

だから質問：それはなぜですか？なぜアルファ等価の概念を修正しないのですか？

更新z：

ああ、私はばかげている、λa:type.λx:a.xそしてλb:type.λx:b.xアルファと同等である。しかし、なぜa:type -> a -> aそしてb:type -> b -> bそれから失礼します。

更新sucz：

ああ、興味深い、これは選択的盲目= Dの完璧な例だと思います

私はこの本読んでいますタイプ理論と正式な証明を、とlambda2著者に関する章での存在動機П議論のまさにそのような使用- 1であると言うカント\t:*.\v:t.v：* -> t -> tこれは2つのα-同等の条項になるため\t:*.\v:t.vと\g:*.\v:g.vさまざまな種類があり、対応するタイプなどをのような型t:* -> t -> tが実際にはアルファ不変である場合、アルファと同等ではありません。違いマインドt:* -> t -> tとを* -> t -> t。しかし、それはこの引数はビット些細な作り、そしてそれはタイプについての話に有意義なものでもあるしないと、任意の数量変数によって結合していないです。コメントで指摘されたa -> babAndrej BauerП 確かに、いくつかの追加のベルとホイッスルを備えたラムダ抽象化に似ています。

全体として、私はそれで終わりました、皆さんありがとう。

回答

7 AndrejBauer Aug 24 2020 at 18:19

ここでいくつかのことをまっすぐにする必要があると思います。

式で $\lambda a : \mathsf{type} . \lambda x : a . x$ 変数 $a$ バインドされています（外側によって$\lambda$）。式$\lambda a : \mathsf{type} . \lambda x : a . x$ そして $\lambda b : \mathsf{type} . \lambda x : b . x$ です $\alpha$-等しい。
表現 $\lambda a : \mathsf{type} . \lambda x : a . x$ は恒等関数であり、「恒等関数の署名」ではありません。
「恒等関数の署名」とは「恒等関数の種類」という意味の場合、次のようになります。 $\Pi_{a : \mathsf{type}} . (a \to a)$、または製品タイプのみが必要な場合は、 $\Pi_{a : \mathsf{type}} \Pi_{x : a} a$。

まだ質問はありますか？

多分これは役立つでしょう：

恒等関数のタイプ $\lambda x : a . x$ です $a \to a$
恒等関数のタイプ $\lambda y : b . y$ です $b \to b$
機能 $\lambda x : a . x$ そして $\lambda y : b . y$ 異なっています
タイプ $a \to a$ そして $b \to b$ 異なっています
多形恒等関数のタイプ$\lambda c : \mathsf{type} . \lambda z : c . z$ です $\Pi_{c : \mathsf{type}} . c \to c$。
機能 $\lambda a : \mathsf{type} . \lambda x : a . x$ そして $\lambda c : \mathsf{type} . \lambda z : c . z$ です $\alpha$-等しい
タイプ $\Pi_{a : \mathsf{type}} . a \to a$ そして $\Pi_{c : \mathsf{type}} . c \to c$ です $\alpha$-等しい。

補足：お茶を飲みながらアレックスシンプソンと話した後、私が言えることがもう1つあります。別々にする必要はありません$\lambda$ そして $\Pi$コンストラクターは、どちらも構文の形がまったく同じであるため（2つの引数を取り、1つの変数をバインドします）。実際、私の記憶が私に正しく役立つ場合、Automathは同じ表記法を使用しました$\lambda$-抽象化と $\Pi$-タイプ。しかし、重要なのは、2つの異なるコンストラクターを使用したいということです。なぜなら、それらは異なる概念を示しているからです。