Haskell でλ計算のインタプリタを作っていこう～その1. データ型

f:id:todays_mitsui:20171008025323p:plain

Haskell ネタです。
先日の記事で宣言したとおり、λ計算のインタプリタを作っていこうと思います。

ソースコード全体は GitHub に置いておきます。

プロジェクト名は Mogul (モーグル) 。
なので作っていくインタプリタの名前も Mogul です。

全体的な注意

このシリーズではλ計算の理論を Haskell で実装していきます。ある程度 Haskell が読み書きでき、かつ、型無しλ計算にある程度親しんでいる人を読者として想定しています。

関数適用の記法には Unlambda記法 を採用しています。が、これはあまり一般的ではないため面食らうかも知れません。

Unlambda記法とは何でしょうか。
関数 f を引数 x で呼び出すとき、C 言語などでは f(x) と書きます。Haskell では f x ですね。Unlambda 記法ではこれを `fx と書きます。関数適用のための ` という演算子をポーランド記法で書いていると思うと理解しやすいかも知れません。
Unlambda 記法には 括弧 () を使わずにあらゆる式が書ける というメリットがあります。が、今回の採用にあたっていちばんの決め手になったのは 筆者が書き慣れているから です。ご了承ください。

その他、解説に使う用語や記号はなるべくλ計算・計算論・関数型プログラミングの分野で一般的なものに統一していくつもりです。

一応以下に参考サイトと参考文献を挙げてみます。

では行ってみましょう。

データ構造

Haskell らしく最初はデータ型の定義から始めます。
今回 Mogul でやろうとしていることを簡単に云ってしまうと λ式を良い感じに β 簡約していく ってな感じなので、まず定義するべきはなんと云っても λ式です。

結論から見せましょう、データ型の定義はこのようにしました。

import Data.Text

-- | 識別子
data Ident = Ident Text
  deriving (Eq, Ord, Show, Read)

-- | λ式
data Expr = Var Ident      -- 変数
          | Ident :^ Expr  -- 関数抽象
          | Expr  :$ Expr  -- 関数適用
  deriving (Eq, Show, Read)

infixl 9 :$
infixr 7 :^

解説を加えます。

『計算論計算可能性とラムダ計算』の第2章「λ計算の基礎」から引用すると、λ式は以下のように再帰的に定義される式です。

変数 ${x_0, x_1, \cdots}$ はそれ単体でλ式である
${M}$ がλ式で ${x}$ が変数のとき ${\lambda x . M}$ はλ式である (関数抽象)
${M}$ と ${N}$ がλ式のとき ${MN}$ はλ式である (関数適用)

これをそのまま Haskell のコードに落としていけば素朴なデータ型の定義ができそうです。幸いに Haskell の柔軟な表現力によって、定義式をそのままコードに落とすことができました。

ただし、しっかりと型推論の恩恵にあずかるために 識別子としての変数 と λ式の一部として現れる単体の変数 を別々の型として区別することにしました。前者は identifier (識別子) を略して Ident という型にしました。後者は variable を略した Var :: Ident -> Expr という値構築子で表現します。

λ計算に追加したいもの

ところで、Mogul ではλ計算の系にいくつかの要素を追加したいと考えています。その一つが 関数定義 です。
関数定義とは λ式に名前を付けて複数の場所で使い回してやろう というアイデアです。みなさんが親しんでいるどの言語にも当たり前にありますよね？

関数定義を許すのには二つの狙いがあります。一つは λ式に適当な名前を付けて参照することで可読性を上げられるであろうこと。もう一つは、 λ式に名前を付けたものでコンビネータを表現できるだろう というものです。

例えば S コンビネータ(『ものまね鳥をまねる』で云うところのホシムクドリ)は以下のように定義出来ますが、

```Sxyz = ``xz`yz

これはλ式 ^x.^y.^z.``xz`yz に S という名前を付けることと同義です。

というわけで識別子とλ式を Map で紐付けるようなデータ型を定義します。

import Data.Map.Lazy

-- | 無名関数
data Func = Func
    { args     :: [Ident]
    , bareExpr :: Expr
    } deriving (Eq, Show, Read)

-- | 関数定義の集合
type Context = Map Ident Func

無名関数を表す Func 型を定義した上で、 Map Ident Func によって識別子と関数を対応付けています。
なぜ素朴に type Context = Map Ident Expr とせずに、わざわざ Func 型を定義するかというと、それは アリティ を考慮したいからなのですが。それは、まぁ、β簡約を実装するときにでもあらためて触れましょう。

λ式の同値性

話は少し戻りますが、 Expr の定義で deriving (Eq) として Eq クラスのインスタンスを自動導出していることに注目してください。
deriving 句は便利ですが、Eq クラスのインスタンス定義を自動導出してしまうと意味的には等しいはずの ${\lambda x . x}$ と ${\lambda y . y}$ が 等しくない ということになってしまいます。

-- | ^x.x == ^y.y ?
Ident "x" :^ Var (Ident "x") == Ident "y" :^ Var (Ident "y")
  -- => False

ご存知の通り、α変換のアイデアで云えば、上記の ${\lambda x . x}$ と ${\lambda y . y}$ は同じ関数を表しているはずです。これらの式を比べたとき等しくなるようにするには (==) の定義にα変換のアイデアを持ち込まなければいけません。
これが結構厄介で、上手い実装はないかと長らく考えあぐねていたところに @dif_engine さまから「ド・ブラン・インデックスを使わない手はないだろう」というアドバイス(空リプ)をいただきました。

ド・ブラン・インデックスを使うと束縛変数の名前( x や y など)が表現から完全に消えてしまい、 ${\lambda x . x}$ も ${\lambda y . y}$ も同じ ${\lambda . 1}$ という表記で書けるようです。なるほどこれなら複雑なα変換のロジックを持ち出すまでもなく、より賢い (==) の定義が書けそうです。

というわけで、 Expr の定義を以下のように変更しようかと考えています。

type Index = Int

data Expr = Var (Maybe Index) Ident  -- 変数
          | Ident :^ Expr            -- 関数抽象
          | Expr  :$ Expr            -- 関数適用
  deriving (Eq, Show, Read)

Var (Maybe Index) Ident として各変数にインデックスを持たせています。
自由変数にはインデックスを振ることができないので Nothing を割り当てます。

たとえば ${\lambda x . \lambda y . FOO \ y \ x}$ という式をデータに落とすと、

Ident "x" :^ Ident "y" :^ Var Nothing "Foo" :$ Var (Just 1) "y" :$ Var (Just 2) "x"

となります。
...という構想をしていますが、まだ実装してテストはしていません。これも追々で。

まとめ

というわけで初回はλ計算の世界を表現するデータ型についてつらつらと書いてきました。
次回は Mogul の文法を紹介しつつパーザ(parser)の実装を眺めていこうと思います。

私からは以上です。

無駄と文化

実用的ブログ

Haskell でλ計算のインタプリタを作っていこう～その1. データ型

全体的な注意

データ構造

λ計算に追加したいもの

λ式の同値性

まとめ