cormoran's note


cormoran

競技プログラミング・電子工作・ロボットなどで遊びます



Recent Post




LazyK HelloWorldを目指す

1ヶ月くらい前に少し遊んだLazyKですが再びやる気が出てきたので今回はHelloWorld出力を目指します。

概要

 まずLazyKについて復習的なところから。今回はお話中心。

LazyK

  • 3つの関数 S K I と括弧のみを使う
I x = x #恒等写像

K x y = x #定数関数

S x y z = (x z)(y z) #関数の適用
  • 標準入力が

 チャーチ数のスコットエンコードされたリストにエンコードされ

 関数の引数として渡される。

  • 関数の返り値が逆にデコードされて標準出力に。

  • 使用するにも、処理系を実装するにも、コンビネータ論理の知識が必要

→SKI? チャーチ数? スコットエンコード? コンビネータ理論?

謎が多いので色々調べたのですがHelloWorldまでに必要な勉強のおおまかな流れは以下のような感じです

HelloWorldまでの道

  1. コンビネーターって何?
  2. コンビネータとラムダ計算
  3. ラムダ計算でチャーチ数とか演算
  4. ラムダ計算でスコットエンコードリスト
  5. T[]変換でLazyKに回帰
  6. HelloWorld!

実は現状3あたりまでやって停止中。ついでに型付ラムダ計算とかをやったので力尽きました。

コンビネーター理論

なんとなくイメージでは「有限個の原始関数を使った計算モデル」という感じ?説明できるほどわかってないのでWikipedia:コンビネータ理論参照。

SKIコンビネータ

LazyKで使われる3つの関数SKIを原始関数とする計算モデル。

詳しくはWikipedia:SKIコンビネータ計算を参照ください。

形式的定義では

以下の3つのみがコンビネータ項

x : 変数

p : 原始的関数(SKIのどれか)

(E1 E2) : 項の適用(E1 E2は項)

 SKIコンビネータ計算はラムダ計算を単純化したひとつの計算モデルで、任意のラムダ項に対し、それと外延的に等価かつ同じ自由変数を持つ。逆も成り立つ。つまりラムダ計算で計算可能であることとSKIコンビネータで計算可能であることは同値。だそうです。さらに、ラムダ計算可能であることとチューリングマシンで計算可能なことは同値なのでSKIコンビネータはチューリング完全。だからLazyKもチューリング完全。

 また T[]変換というものによりラムダ項をSKIコンビネータ項に(機械的に)変換することができます。

 で、どうやってプログラム書くのかということですが、使えるのはSKIという関数と括弧、変数のみ。数字は??

関数だけで自然数を扱う

数字がないのにどうするの?ということですがチャーチ数と言うものを使います。

以下は定義

0:(K I)

1:(I)

2:(S (S (K S) K) I)

3:(S (S (K S) K) (S (S (K S) K) I))

こんな感じで関数のかたまりを数と対応付けます。

プログラム書く

 雰囲気はチャーチ数表現のASCIIコードのリストを作ってそれを出力する関数を書く。するとHelloWorldが出せます。

しかしどうすればいいのか全くわからない。そこでT[]変換でラムダ項はSKIコンビネータ項に変換可能というのを利用し、もう少しわかりやすいラムダ計算の力を借ります。というわけでHelloWorldは次回以降に持ち越し。

comments powered by Disqus