よく入力された型の悪いラムダ用語

Question

私は、適用されたラムダ計算を理解しようとしています。これまでは、型推論の仕組みを理解していました。しかし、私は、用語がよくタイプされているか、またはタイプミスであるということの意味に従うことができません。そして、どのタイプが適切なタイプのものか、タイプの悪いものかを決定する方法はありますか？ たとえば、λ用語twをλx[(x x)]と定義します。どのようにそれはよく型付けされたまたは悪い型の用語であると結論ですか？

Answer 1

さらにいくつかの定数および基本タイプ（すなわちラムダ計算）が適用されているSimply Typed Lambda Calculusについて言えば、λx:σ. (x x)という表現は整形式ですが型が不正です。

「整形式」は、構文的に正しいことを意味します。つまり、STLCのパーサーによって受け入れられます。 'ill-typed'は、型チェッカーがそれ以上のものを渡すことを意味しません。 タイプチェッカーは、typing rulesに従って動作します。これは通常、多くのタイピング判定（各構文形式の1つのタイピングスキーム）として表されます。

あなたが提供した言葉は実際にはタイプミスであることを示してください。 ルール（3）[型付きルールのリンクを参照]によると、λx:σ. (x x)は一般的な形式の型でなければなりません（はの関数、より正確には抽象であるため）。しかし、本体(x x)は、あるタイプτ（x : σと仮定する）を持っていなければなりません。これは基本的に自然言語で表現された同じルール（3）です。ですから、関数の本体の型を理解する必要があります。これはアプリケーションです。今

、アプリケーションのためのルールは、（4）私たちは、この(e1 e2)ような表現を持っている場合、適切な型の引数でなければならない、そしてe1は、いくつかの機能e1 : α -> βとe2 : αでなければならないと述べています。この規則を体の式(x x)に適用してみましょう。 （1）x : α -> βおよび（2）x : αである。 STLCの用語は1つの型しか持てないため、式はα -> β = αです。 しかし、αはα -> βのサブパートであるため、両方のタイプを統合する方法はありません。だから、これは型チェックをしません。

ちなみに、STLCの主なポイントの1つは、（タイプなしの）ラムダ計算を論理として使用することを妨げるため、自己申請を禁止することです（(x x)など）。アプリケーション（例えば、Y-combinatorを参照）。