コンテンツにスキップ

英文维基 | 中文维基 | 日文维基 | 草榴社区

利用者:Fumiexcel/Mogensen-Scott encoding

計算機科学において、スコットエンコーディングは帰納的データ型をラムダ計算に埋め込む方法の一つである。Mogensen–Scott encodingは型なしラムダ計算のすべての項を埋め込むためにわずかな変更と拡張をする。

定義

[編集]

Dを、Nというコンストラクタを持つデータ型とする。。このようなコンストラクタCiは、アリティAiを持つ。

チャーチエンコーディング

[編集]

比較のため、DのコンストラクタCiのチャーチエンコーディングを以下に示す。

スコットエンコーディング

[編集]

DのコンストラクタCiスコットエンコーディングはこうである。

Mogensen–Scott encoding

[編集]

Mogensenはスコットエンコーディングをすべての型なしラムダ項に拡張する:

チャーチエンコーディングとの比較

[編集]

The Scott and Church encodings coincide on enumerated datatypes such as the boolean datatype. スコットエンコーディングとチャーチエンコーディングは、ブール型のような列挙型では一致する。 チャーチエンコードされたデータと演算はsystem Fにおいて型付けできるが、スコットエンコードされたデータと演算は明らかにsystem Fでは型付けできない。 再帰的な型と同じくらいUniversalが必要に見える。また、強い正規化が再帰的に型付けされたラムダ計算のための予約でないため、スコットエンコードされたデータを扱うプログラムの終端は、well-typednessの決定によっては確立されない。

リンク

[編集]

参照

[編集]