46

私はさまざまな型システムとラムダ計算について調べてきましたが、ラムダ キューブ内の型指定されたラムダ計算はすべて、同等のチューリングではなく、強く正規化されていることがわかりました。これには、単純に型付けされたラムダ計算とポリモーフィズムである System F が含まれます。

これにより、次の質問に至りましたが、これに対する包括的な答えを見つけることができませんでした。

  • (例えば) Haskell の形式主義は、それが表向きに基づいている微積分とどのように違うのですか?
  • Haskell のどの言語機能が System F 形式に当てはまらない?
  • チューリングの完全な計算を可能にするために必要な最小限の変更は何ですか?

これを理解するのを手伝ってくれた人に感謝します。

4

1 に答える 1

52

一言で言えば、一般再帰です。

Haskell では任意の再帰が可能ですが、System F には再帰の形式がありません。無限の型がないということfixは、閉じた用語として表現できないことを意味します。

名前と再帰の原始的な概念はありません。実際、純粋な System F には、定義などの概念はありません。

したがって、Haskell では、この単一の定義がチューリングの完全性を追加します。

fix :: (a -> a) -> a
fix f = let x = f x in x

実際、この関数はより一般的なアイデアを示しています。完全に再帰的なバインディングを持つことで、チューリングの完全性が得られます。これは、値だけでなく、型にも適用されることに注意してください。

data Rec a = Rec {unrec :: Rec a -> a}

y :: (a -> a) -> a
y f = u (Rec u)
  where u x = f $ unrec x x

無限型を使用すると、Y コンビネータ (いくつかの展開を法とする) を記述し、それを使用して一般的な再帰を行うことができます!

純粋な System F では、定義の非公式な概念がよくありますが、これらは精神的に完全にインライン化される単純な略記です。Haskell では無限項が作成されるため、これは不可能です。

の概念のないHaskell 用語のカーネルはlet、whereまたは=強く正規化されています。これは、無限の型がないためです。この中心的な用語である微積分でさえ、実際にはシステム F ではありません。システム F には「大きなラムダ」または型の抽象化があります。idSystem F におけるの完全な用語は

id := /\ A -> \(x : A) -> x

これは、System F の型推論が決定できないためです。ポリモーフィズムが予想される場合はいつでもどこでも明示的に記します。Haskell では、このようなプロパティは煩わしいので、Haskell の機能を制限します。特に、注釈なしで Haskell ラムダ引数のポリモーフィック型を推論することはありません(条件が適用される場合があります)。これがMLとHaskellの理由です

let x = exp in foo

と同じではありません

(\x -> foo) exp

exp再帰的でない場合でも！これは、「let generalization」と呼ばれる HM 型推論とアルゴリズム W の核心です。

于 2014-08-12T03:08:55.803 に答える