ラムダ式→SKIコンビネータ項

概要

ラムダ式をSKIコンビネータの式に変換するプログラムを書きました。
koba-e964/ski-comb · GitHub

やったこと

ラムダ式→SKIコンビネータの項の変換

実装は
高階ことりちゃんと学ぶSKIコンビネータ
を参考にしました。

例

Haskell風の書き方で説明します。やり方は上のリンク先に書いてあるので、ここでは実例だけ紹介します。
C = \x y z -> x (y z)
をSKIコンビネータ項に直してみましょう。
(1) 全てのλ抽象を新しく導入した関数に直す。このとき、新しく導入される関数の定義は、
関数名 自由変数... ラムダ式で束縛される変数
の形になる。
まずトップレベルの\x->...を直しましょう。

C = M
M x = \y z -> x (y z)

続いてM xの内部の\y -> ...を直します。

C = M
M x = N x
N x y = \z -> x (y z)

同様にして最終的には以下のようになります。

C = M
M x = N x
N x y = O x y
O x y z = x (y z)

(2) 関数の引数を消去してS,K,Iのみで表す
O x y z = x (y z)
O x y z = (K x z) (y z)
O x y z = S (K x) y z
O x y = S (K x) y
O x = S (K x)
O x = (K S x) (K x)
O x = S (K S) K x
O = S (K S) K

C=M=N=O*1より、結局
C = S (K S) K
がわかる。

課題


ここのやり取りで気付いたのですが、今のままだと実行時間も出力されるコードも線型よりも速いペースで増大します。現在のところどのくらいのペースで増大するのか見積もりができていないので、

  • 計算量・出力されるコードの大きさの増大の速さの見積もり
  • 高速化・サイズ削減

が目標になるかと思います。

*1:実際のコードではここもちゃんとやっているのでコードが肥大化します