ラムダ計算、特に型推論に関する適切なリソースを誰かが持っているのではないかと思っていました。私は試験のために勉強していますが、ラムダ型に関する情報と、私が行ったチュートリアルで推論する方法を見つけることができないようです。
火曜日に向けて頭を悩ませようとしている試験問題があります..
以下のラムダ計算式で、すべての変数と括弧で囲まれたサブ式の型を推測します: (\denotes lambda)
(((\x.(\y.(x,y)y))g)h)
宿題じゃないって約束するよ！どんな助けでも大歓迎です。
1 に答える
0
ラムダ項の (最も一般的で単純な) 型の推論は、非常に単純で非常に有益な作業です。ラムダ項を解読しようとするとき、その型を推測することから始めることは非常に良いアプローチです。
型推論の背後にある一般的な考え方は、ジェネリック型 (型変数) を任意の識別子に関連付けることから始め、用語内の識別子の使用に従ってこの型を改良することです。これは、ラムダ計算では非常に簡単です。識別子は、関数の引数として、または関数としての 2 つの方法でしか使用できないためです。
たとえば、あなたの例では、x: α と y: β とします。しかし、x は y に適用されるため、関数型を持たなければならず、さらにその入力は引数 y の型と互換性がなければならないため、α を (β -> γ) に改良します。 ) アプリケーションの結果タイプ (xy)。
項 (xy) は y に適用されます。これは、γ も実際には関数型でなければならないことを意味します。つまり、γ = β -> δ です。
この場合、基本的にこれで分析は終了です。
わかりやすくするために、すべてのサブタームのタイプを以下に示します (すべてのアプリケーションが適切にタイプされていることを確認してください)。
x : β -> β -> γ
y : β
(x y) : β -> γ
((x y) y) : γ
\y.((x y) y) : β -> γ
\x.\y.((x y) y) : (β -> β -> γ) -> β -> γ
さらに、g:β -> β -> γ、および h:β と結論付けます。式全体は型 γ を持ちます。
もう少し興味深い例として、\y.\x.(y (yx)) という用語があります。x:αとする。その場合、y の型は α -> β である必要があります。ここで、β は結果の型 (yx) です。この項は y への入力として再び渡されます。つまり、α=β です。\y.\x.(y (yx)) : (α -> α) -> α -> α
一般に、場合によっては、同じ識別子を複数回使用する場合、それらの間で最も一般的なインスタンスを推測して、それらの型を統一する必要があります。
Damas-Milner 型推論アルゴリズムに関するウィキページはかなり適切ですが、私の意見では、このような単純で直感的なトピックについては非常に技術的です。
于 2017-02-03T11:05:54.703 に答える