λ抽象(無名関数) を SKI コンビネータに展開するトランスレータを Haskell で書きました。
コード一式を GitHub に置いています。
Stack の環境が整っている人であれば、
$ git clone https://github.com/todays-mitsui/lambda2ski.git
$ cd lambda2ski
$ stack setup
$ stack install
で、たぶん入ります。
使い方
インストールしてパスを通すと ski と云うコマンドが使えるようになります。
λ抽象を含む式を与えて実行すると、
$ ski "^xy.`x`yy"
``s``s`ksk`k``sii
こんな感じで SKI まみれの式が吐き出されます。
関数型畑の方はお気づきかもしれませんが、変換後の式は Lazy_K で実行可能な式になっています。
--load オプションを使って別ファイルで定義した変数を読み込ませることもできます。
このとき読み込ませるファイルを便宜的に Context ファイルと呼びます。
$ ski --load=sample.context "ISZERO"
``s``si`k`k`ki`kk
構文
基本的に Unlambda 記法の Lazy_K を拡張した構文になっています。
追加されている構文は、
- λ抽象
- 変数定義
です。
λ抽象
λ抽象は以下のように書きます。
^xy.x
上記と同じ意味の式を幾つかのポピュラーな言語で書いてると、
-- Haskell
\x y -> x
# Python
lambda x: lambda y: x
// JavaScript
function(x) { return function(y) { return x; }; }
// ES2015 以降なら
x => y => x
となります。
全てのλ抽象は自動的にカリー化されて、内部ではすべて一変数の関数として扱われています。
もちろんλ抽象をネストしたり関数適用と組み合わせることも可能です。
$ ski "^x.^y.x"
k
$ ski "`k^x.x"
`ki
変数定義
続いて変数定義です。
Context ファイルの中では、任意の式と紐付けた変数を定義できます。
例を見てもらうと分かりやすいでしょう。
# 論理演算
TRUE = ^xy.x # 真
FALSE = ^xy.y # 偽
IF = ^BOOL THEN ELSE.``BOOL THEN ELSE
NOT = ^x.``xFALSE TRUE
AND = ^xy.``xyFALSE
OR = ^xy.``xTRUEy
XOR = ^xy.``x`NOTyy
スペースや改行は意味を持ちません。# から行末までは行コメントとして扱われ、実行時には無視されます。
変数名には英小文字と英大文字, アンダースコアが使えますが、その規則は奇妙に見えるかもしれません。
変数名として使えるのは 1文字の英小文字 ないしは 1文字以上の英大文字とアンダースコアの列 です。
xyz のように小文字を並べた場合、変数の連なりと解釈され x y z と同義になります。
また、アンダースコア1つだけであっても正しい変数名として解釈されます。
このような制約は Lazy_K の美しく密度の高いコードを余計なスペースで汚さずに済むように拡張した結果のものです。
何故こんなものを作ったの？
Lazy_K で中規模以上のプログラムを書く際の足掛かりにするためです。
Lazy_K は3つの組み込み関数 s, k, i と関数適用を表す1つのシンボル ` だけでチューリング完全な表現力を持つコンパクトな体系ですが、そのコンパクトさ故に可読性を犠牲にしています。
特に変数定義が無いのは致命的で、コードの再利用はほぼ不可能です。
また、λ抽象(無名関数) を書くことができず、記述が冗長になりがちなのも難点です。
例えば、『関数を受け取って引数の適用順を入れ替えた関数を返す高階関数 FLIP』を書いてみると、
# λ抽象を用いた場合
FLIP = ^f.^xy.``fyx
# SKI コンビネータで頑張った場合
FLIP = ``s``s`ks``s`kks`kk
どちらの書き方が意味を汲み取りやすいか、言うまでもありませんね。
そんなわけで、Lazy_K にλ抽象と変数定義を追加した体系を作り、Lazy_K として実行可能なコードに変換するツールとして lambda2ski を書いたわけです。
どのようにλ抽象を分解するか
λ抽象を SKI コンビネータに変換する過程は、型無しλ計算の基本的知識をそのままコードに落として実現しています。
任意のλ式は以下のように単純な4つの規則に従って SKI コンビネータに置き換えることができます。
^x.`MN ≡ ``s ^x.M ^x.N # 規則1
^x.x ≡ i # 規則2
# 式M の中で x が自由変数として現れないとき(式M が 変数x に依らないとき)
^x.M ≡ `kM # 規則3
^x.`Mx ≡ M # 規則4
今回書いたトランスレータはこの4つの規則を内部で愚直に適用するだけのものです。
λ式の等価性について
ちなみに、何をもってλ式同士が等しいと云うかはなかなか難しい問題です。
ここではλ式が 外延的に等しい と云う意味で等号(≡) を用いています。
外延的に等しいとは、2つのλ式 M, N に対して適当な数の任意の式を適用して、`Ma と `Na が同じ正規形を持つときにM ≡ Nとするものです。
今後
今回のようにλ抽象の展開を機械的に実行できれば、Lazy_K プログラミングは大幅に効率化されるはずです。
さて、今後の展開ですが、Lazy_K のコードを解釈して実行するインタプリタを書こうかなと考えています。
とはいえ、Haskell で Lazy_K コンパイラは 既に fumieval さまが書かれている ようなので、ちょっとひねって式がβ簡約されていくさまを順を追って見られるような、ステップ実行可能な Lazy_K インタプリタを書こうと思っています。
できれば、今回の拡張構文を SKI コンビネータに展開することなく、そのままの形でも実行可能なものにしたいですね。
私からは以上です。