LLプログラミング言語 obake

論理学の考え方で、
関数型プログラミング言語の定義＆実装の仕方の例に触発されて、
深夜アニメを見ながら
OCamlでつくられた、
脱関数型プログラミング言語
obake (おばけ)を紹介します。

関数型言語とかは前世紀に置いていって、21世紀は論理学を基にした新しいプログラミングパラダイムで脱関数型言語しましょう！

break world

break

「Hello, world!」を書こうと思ったのですが、あまりに難しいので最初はすぐ停止するプログラムです。プログラムは「命令」からできていて、命令は２つの要素、「値」と「計算」の組み合わせです。

「命令」 = 「値」 + 「計算」

breakは組み込み「計算」になります。これだけでは「命令」にはならないので、プログラム起動時に自動的に「現実世界」という「値」が設定されて、「命令」が作られます。値を組み合わせることによって

< world | break >

という命令ができます。そして、この命令を実行すると現実世界は否定され消滅します。その結果、計算はここでおしまいです。

μ式を導入

λ式に変わるものとしてμ式を導入します。引数をひとつ束縛しますが、本体に書けるのは命令だけです。ここまでに出てきた構文をまとめると

E (式)    ::= x        (変数)
            | mu x, C  (μ式)

C (命令)  ::= < E1 | E2 >

μ式を使って、最初の例を改造してみましょう

mu kitkat, <kitkat | break>

この新しい式を実行すると、最初に現実世界が渡されてきて、

< world | mu kitkat, <kitkat | break>>

これは1ステップ実行が進んで

< world | break >

になり、結局は現実世界を否定して終了します。

操作的意味論

上の例でほとんどの場合が尽くされています！命令が

< v | mu x, c >

の形をしていた場合は、cの中に出てくるxをvで置き換えるだけです。

c[v/x]

反対向きもあります。

< mu x, c | v >

も同じ結果になります！ポイントは構文木の根だけ見ればわかるところです。普通のラムダ計算よりはるかに機械的な操作で実行できます。

停止しない例

< mu x, < x | x > | mu x, < x | x > >

を上の方法で実行していくといつになっても終わりません。困りました。

合流しない例

< mu x, c1 | mu x, c2 >

は２通りの方法で実行できます。しかも結果が違います。困りました。

現実世界のバックアップが作れる

mu world, < world | mu world2, < world | break >>

この計算は受け取った現実世界を２回使ってます。しかもworld2の方はそのまま使わずに放置してます。困りました。

型システムを導入！

正しい型システムを使うことで、上の問題を全部一度に解決できます。普通の整数型

int

と現実世界型

world

の２つを基本型とします。

型を否定する

それぞれの基本型にたいして、否定した型も追加します。obakeでは「-型名」で否定した型を書くことにします。

-int  (* intを否定した型 *)
-world (* worldを否定した型 *)

すでに、-worldの型を持つ式は出てきました。

break : -world

型を合成する

いくつかの型を使って新しい型を作るのは基本ですから、たくさん導入しますが、その前に型を正の型と負の型に分類します。今のところ

intとworldは正の型
-intと-worldは負の型

正の型は値の型で、負の型は計算の型です。

新しい型を作るごとに、正か負かを書いていくことにします。

正の型PとQに対して、積と和の型を定義します。これは正の型です。

P * Q  (* 積の型 *)
P + Q  (* 和の型 *)

負の型NとMに対して、parとwithの型を定義します。これは負の型です。

N @ M  (* parの型 *)
N & M  (* withの型 *)

これだけでは足りなそうなので、正の型Pと負の型Nに対して、of courseとwhy notとupとdownの型を定義します。これらはそれぞれ、正、負、負、正の型です。

!P  (* of courseの型 *)
?N  (* why notの型 *)
^P  (* upの型 *)
#N  (* downの型 *)

再び型を否定する

新しく追加した型も否定できるようにしましょう。これは新しい型にはなりません。否定すると他の型がでてきます。

-(-int) = int
-(-world) = world
-(P * Q) = -P @ -Q
-(P + Q) = -P & -Q
-(N @ M) = -N * -M
-(N & M) = -N + -M
-!P = ?-P
-?N = !-N
-^P = #-P
-#N = ^-N

あと、*と+と@と&にはそれぞれ単位元になる型がありますがめんどくさいので省略。

関数型

関数型はありません。しかし、関数に似たような型「P -o N」は

P -o N := -P @ N

で定義されます。「(P * Q) -o N」と「P -o (Q -o N)」を展開すると

(P * Q) -o N  = (-P @ -Q) @ N
P -o (Q -o N) = -P @ (-Q @ N)

となるので、型に否定を導入したことで、カリー化は単にparの結合則に単純化されます。

構築子

おのおのの型には対応するコンストラクタがあります。デストラクタはありません。規則はめんどくさいから省略。

0, 1, 2, … : int
(* なし *) : world
x : P                 (* 変数、変数の型は正でなければならない *)
mu x, c : N           (* 否定、xの型は-Nでcの中でちょうど一度使う *)
(s, t) : P * Q        (* タプル *)
inl s, inr s : P + Q  (* 直和 *)
mu (x, y), c : N @ M  (* par、xとyの型は-Nと-Mで同様にちょうど一度 *)
{ mu x, c1; mu y, c2 } : N & M  (* 場合わけ、同様一度 *)
!s : !P               (* of corse, sの中ではちょうど一度の変数は使えない *)
mu !x, c : ?N         (* why not、xの型は-Nで何度でも使える *)
'mu x, c : #N         (* up、同様一度 *)
^s : ^P               (* down *)

最後に、命令は左に正の型、右には左の否定の型になる式を書きます。

型推論

すごい型推論を実装したので、型検査モードで実行すればオープンな式でもそれなりに型再構築されます。

$ echo "break" | ./obake -t
input: break
  type: -world
  constraints:
  inferred type: -world
  substitute:

というわけで、breakの型は-worldです。他には

putc: -world @ (-int @ ^world)
getc: -world @ ^(world * int)

になります。わかりやすい型ですね。worldは正と負がそれぞれあるので差し引きゼロです。よって、実行時に存在するworldは増えも減りもしません。putcではintは世界からひとつ消滅します。getcではひとつ生成されます。

Hello, world!

putcを何回か実行して、最後にbreakを実行すれば、Hello, world!を作ることができます。

mu world, < (world, 72, 継続) | putc >

とすれば、現実世界を消費して'H'が出力されたあと、新しい現実世界とともに継続の部分が実行されます。継続のところには計算ではなく値を置きます。

'mu world, < world | break >

は計算を中断した値を作ります。これを継続のところにいれれば１文字出力するプログラムは出来上がりです。

mu world, < (world, 72, 'mu world < world | break > | putc >

$ ./obake example/putc.obake 
H

実行できました！-vオプションを指定すると計算の様子がわかります。

$ ./obake -v example/putc.obake 
input: (mu w, <(w, (72, ('mu w, <w | break>))) | putc>)
Execute:
--------
  [
  ]
  <#world | (mu w, <(w, (72, ('mu w, <w | break>))) | putc>)> ===>

--------
  [
    w := #world
  ]
  <(...) | putc> ===>

--------
  [
    w := #world
  ]
  <#closure | ^#world> ===>

--------
  [
    w := #world
  ]
  <#world | break> ===>

Done
H

残りを頑張ればHello, world!はできるような気がします。

まとめ

線型型を使うことでputcのような副作用を気にしなくてよくなる
値の型と計算の型を分けることで命令の実行方法は一通りになり合流性は気にならなくなる。評価戦略なんてなかったんや。
型をつけることで停止性が得られる。ゲンツェンのカット除去定理により停止する。
命令＝カット。１ステップ実行はカット除去アルゴリズムを一回実行すること。
静的に型付けられた継続渡しスタイル
型の付いた大域脱出も書けるよ！
タイトルのLL言語って言語言語になってね？→
LL=線型論理
もっと詳しく知りたい→
http://assert-false.net/arnaud/papers/A%20dissection%20of%20L.pdf