利用者:Fumiexcel/Mogensen-Scott encoding

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

定義

Dを、Nというコンストラクタを持つデータ型とする。$\{C_{i}\}_{i=1}^{N}$。このようなコンストラクタC_iは、アリティA_iを持つ。

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

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

$\lambda x_{1}\ldots x_{A_{i}}.\lambda c_{1}\ldots c_{N}.c_{i}(x_{1}c_{1}\ldots c_{N})\ldots (x_{A_{i}}c_{1}\ldots c_{N})$

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

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

$\lambda x_{1}\ldots x_{A_{i}}.\lambda c_{1}\ldots c_{N}.c_{i}x_{1}\ldots x_{A_{i}}$

Mogensen–Scott encoding

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

${\begin{matrix}[x]&=&\lambda abc.ax\\\ [MN]&=&\lambda abc.b[M][N]\\\ [\lambda x.M]&=&\lambda abc.c(\lambda x.[M])\\\end{matrix}}$

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

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

リンク

• ラムダ計算で代数的データ型を表現する方法 - Meta reifier @syamino

参照

• Directly Reflective Meta-Programming
• Torben Mogensen (1992). Efficient Self-Interpretation in Lambda Calculus. Journal of Functional Programming.