Lazy Kで世界に挨拶(OCamlの練習)

Lazy KでHello, world!をやりたいがSKIコンビネータは書きたくない。
最近OCamlの勉強をはじめたのでラムダ式をLazy Kのコードに変換するプログラムを書くことにする。

変換

コンビネータ論理 - Wikipediaをみるとなんか変換する方法が書いてあるので、そのままプログラムにしてしまいたい。

  1. T[x] => x
  2. T[(E₁ E₂)] => (T[E₁] T[E₂])
  3. T[λx.E] => (K T[E]) (if x does not occur free in E)
  4. T[λx.x] => I
  5. T[λx.λy.E] => T[λx.T[λy.E]] (if x occurs free in E)
  6. T[λx.(E₁ E₂)] => (S T[λx.E₁] T[λx.E₂])

変換の過程でラムダ項とコンビネータ項が混在したものを扱う必要があることがわかる。

ラムダ項・コンビネータ項を定義

そういうわけで、ラムダ項とコンビネータ項をまとめて定義してしまった。

type term =
  | Var of string
  | Abs of string * term
  | App of term * term
  | S
  | K
  | I

最初はわけて定義するつもりだったが、そうすると関数適用が重複したりして面倒なことになりそうである。もしかして多相ヴァリアントの機能を使うとうまく定義できたりする?

ついでに項を文字列化する関数string_of_termを作成したが、これはHello, world!には使わないので折り畳んでおく。

string_of_term

括弧の省略規則がややこしくて苦労した。もっとエレガントな書き方があるかもしれない。

let rec string_of_term t =
  let parenthesize s = "(" ^ s ^ ")" in
  let rec abs v t isBegin =
    let sep = ". " in
    (if isBegin then "λ" else " ")
    ^ v
    ^
    match t with
    | Abs (v', t') -> abs v' t' false
    | App (t1', t2') -> sep ^ app t1' t2' true
    | _ as t' -> sep ^ string_of_term t'
  and app t1 t2 isBegin =
    ( match t1 with
    | Abs (v', t') -> parenthesize (abs v' t' true)
    | App (t1', t2') -> app t1' t2' false
    | _ as t' -> string_of_term t' )
    ^ " "
    ^
    match t2 with
    | Abs (v', t') ->
        let s = abs v' t' true in
        if isBegin then s else parenthesize s
    | App (t1', t2') -> parenthesize (app t1' t2' true)
    | _ as t' -> string_of_term t'
  in
  match t with
  | Var v' -> v'
  | Abs (v', t') -> abs v' t' true
  | App (t1', t2') -> app t1' t2' true
  | S -> "S"
  | K -> "K"
  | I -> "I"

抽象除去

基本的にWikipediaに書いてあることをそのままプログラムに書くと抽象除去ができる。

(* 変数が項の自由変数であるかを求める *)
let rec is_free_variable v = function
  | S | K | I -> false
  | Var v' -> v = v'
  | App (t1, t2) -> is_free_variable v t1 || is_free_variable v t2
  | Abs (v', t) -> if v = v' then false else is_free_variable v t

(* 抽象除去 *)
let rec eliminate_abstraction = function
  | (S | K | I | Var _) as x -> x
  | Abs (v, App (t, Var v')) when v = v' && not (is_free_variable v t) ->
      eliminate_abstraction t
  | App (t1, t2) -> App (eliminate_abstraction t1, eliminate_abstraction t2)
  | Abs (v, t) when not (is_free_variable v t) ->
      App (K, eliminate_abstraction t)
  | Abs (v, Var v') when v = v' -> I
  | Abs (v, Abs (v', t)) ->
      eliminate_abstraction (Abs (v, eliminate_abstraction (Abs (v', t))))
  | Abs (v, App (t1, t2)) ->
      App
        ( App (S, eliminate_abstraction (Abs (v, t1))),
          eliminate_abstraction (Abs (v, t2)) )
  | _ -> assert false

条件(if x does not occur free in E)の判定のため愚直に探索する関数を用意した。非効率っぽい気がするが、どうせそれで困るほど大規模なラムダ式を書くことはないだろう…

eliminate_abstractionのパターンマッチの上から2番目はイータ変換に相当する。この行をコメントアウトしても関数は正しく動作するが、あるとコンビネータ項がいくらか小さくなる。実のところ私はイータ変換した式が必ずLazy Kの処理系で元どおりに評価されるのかどうかわかっていないのだが、今回試した範囲では問題なかった。

せっかくだからいろいろ試してみよう。

let exps =
  [
    Abs ("x", Var "x");
    App (Abs ("x", App (Var "x", Var "x")), Abs ("x", App (Var "x", Var "x")));
    Abs
      ( "f",
        App
          ( Abs ("x", App (Var "f", App (Var "x", Var "x"))),
            Abs ("x", App (Var "f", App (Var "x", Var "x"))) ) );
  ]

let show t =
  string_of_term t ^ " ==> " ^ string_of_term (eliminate_abstraction t)

let () = print_endline @@ String.concat "\n" @@ List.map show exps

出力↓

λx. x ==> I
(λx. x x) λx. x x ==> S I I (S I I)
λf. (λx. f (x x)) λx. f (x x) ==> S (S (S (K S) K) (K (S I I))) (S (S (K S) K) (K (S I I)))

よくわからないが、おそらく大丈夫だろう…

コンビネータ項の文字列化

これはとても簡単。

let rec string_of_ski = function
  | S -> "s"
  | K -> "k"
  | I -> "i"
  | App (t1, t2) -> "`" ^ string_of_ski t1 ^ string_of_ski t2
  | Abs _ -> failwith "Given expression contains lambda abstraction"
  | Var _ -> failwith "Given expression contains free variables"

ただし英語には自信がない。

リスト

Lazy Kのconsはラムダ式で表すとλx y f. f x yになる。nilはない。

次のようにconsを定義した。

let cons x y = Abs ("f", App (App (Var "f", x), y))

数と文字

最適化に気を配る余裕はない。愚直にチャーチ数を生成する関数を用意する。

(* intをチャーチ数に変換 *)
let nat n =
  let rec tailnat m t =
    if m = 0 then t else tailnat (m - 1) (App (Var "s", t))
  in
  Abs ("s", Abs ("z", tailnat n (Var "z")))

(* charをチャーチ数に変換 *)
let natc c = nat (int_of_char c)

Hello, world!

let program =
  App
    ( K,
      cons (natc 'H')
      @@ cons (natc 'e')
      @@ cons (natc 'l')
      @@ cons (natc 'l')
      @@ cons (natc 'o')
      @@ cons (natc ',')
      @@ cons (natc ' ')
      @@ cons (natc 'w')
      @@ cons (natc 'o')
      @@ cons (natc 'r')
      @@ cons (natc 'l')
      @@ cons (natc 'd')
      @@ cons (natc '!')
      @@ App (K, nat 256) )

let code = string_of_ski (eliminate_abstraction program)

let () = print_string code

プログラムの頭にKコンビネータを置くことで入力を無視することができる。
どうでもいいことだが、プログラムの先頭にAppと書いてあると「アプリケーション」の略語っぽく見えるなと思ったら、「アプリケーション」と「適用」は両方ともApplicationだから同じだった。

Lazy Kの出力の終端は256で表される。リストの終端はcons 256 I(終端以降の出力は検査されないのでconsの第2引数には適当な関数を食わせておく)などとしても良いのだが、The Lazy K Programming LanguageをみるとK 256が簡単だと書いてある。手計算してみよう。

(K 256) (λa b. a) ==> (λx. 256) (λa b. a) ==> 256

なるほど、Kの定義を考えればたしかにcarが256になる。

これでHello, world!の完成である。 出力されたLazy KのプログラムはLazy K Playgroundで手軽に試すことができた。感謝。

雑多な話題

出力されたプログラムの長さを計算したら14191バイトもあった。一方でLazy K - Esolangに載っているHello worldのコードは1000バイト弱なので、短縮の余地はいくらでもあるのだろう。Lazy Kの世界も奥が深そうだ。

Lazy Kの処理系を作りたいという願望があるのだが、いまのところ作り方がよくわからない。とりあえずラムダ計算やSKIコンビネータ計算の簡約を実装するところからはじめていきたいなぁと思っている。

追記: OCamlのコードのインデントをいくらか修正した。