ラムダ計算から Grass へのコンパイラ作ったったｗWWｗｗｗｗWWｗｗ

esolangs プログラミング

github.com

いつものように JavaScript で書いたので, npm でインストールできます.

npm i -g @susisu/grasspiler

例えば,

(* fixed-point operator *)
let fix = fun f ->
    (fun x -> f (fun y -> x x y))
    (fun x -> f (fun y -> x x y))

(* infinite loop *)
let loop = fix (fun loop c ->
    let _ = Out c in
    loop c
)

let main _ = loop (In w)

のような ML 風のプログラム (resonance.ml とする) をコンパイルすると,

$ grasspile resonance.ml -o resonance.w
$ cat resonance.w
wwWWwwWwwvwwWWWwWWWwvwWWwWWWwwWwwvwwWWWWWWwWWWwwvWWwvwWWWWWWWWWWwwwwwwwwwWWWw

みたいに草が生えて, 実行すると,

$ grass resonance.w
A
AAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA...

みたいにうるさい.

ラムダ計算から Grass に至るまで

ちょっと草植えときますね型言語 Grass にある通り

型無しラムダ計算を

  • e ::= x | λx.e | e e

CPS変換して，

  • t ::= x | λx.r
  • c ::= k | μx.e
  • e ::= r c | x x c | c t
  • r ::= δk.e

逆CPS変換して，

  • e ::= x | λx.r | x x
  • r ::= e | let x = e in r

lambda liftingとか使って全ての関数をトップレベルに集めて，

  • e ::= x | x x
  • m ::= e | let x = e in m
  • f ::= λx.f | λx.m
  • r ::= e | let x = f in r | let x = e in r

de Bruijn Index化して，

  • n ::= • | n ↑
  • e ::= n | n n
  • m ::= e | let e in m
  • f ::= λf | λm
  • r ::= e | let f in r | let e in r

あとは草を生やすだけｗｗｗｗｗ

基本的にはこれと同じことをやりました.

de Bruijn index 化

正直変数名があると変換が面倒なので, 最初から de Bruijn index 化しました.

  • n ::= • | n ↑
  • e ::= n | λe | e e

A-正規化

CPS 変換, 逆 CPS 変換の代わりに, A-正規化で大体同じことをしました (参考: A正規形まとめ - Scheme VM を書く - Higepon’s blog).

  • n ::= • | n ↑
  • t ::= n | λr
  • e ::= t | t t
  • r ::= e | let e in r

ただし, 見て分かる通り, このままだと元の CPS → 逆 CPS 変換をしたものと異なっている (関数適用が変数同士だけでない) ので, 少し変更を加えて, 以下のようにオリジナルと同じとなるようにしました.

  • n ::= • | n ↑
  • e ::= n | n n | λr
  • r ::= e | let e in r

(と言いながら, これは後で没になるのですが.)

Lambda lifting

適当にやりました (r の部分に f が増えていますが, そこはさほど重要ではないので気にしない).

  • n ::= • | n ↑
  • e ::= n | n n
  • m ::= e | let e in m
  • f ::= λf | λm
  • r ::= e | f | let e in r | let f in r

ちゃんと書くとこんな感じ (\uparrow_c^d は index の shift, \updownarrow_i^j は index の swap). index は面倒なので自然数で書いています. (自分で書いたコードを見ながら適当に書き写しただけなので, 元のコードを見たほうが見やすいかもしれません.)

{
\begin{align}
\mathcal{L}[n, \_] &= n \\
\mathcal{L}[n\ n', \_] &= n\ n' \\
\mathcal{L}[\lambda. r, \_] &= \mathrm{let}\ \lambda.\ e\ \mathrm{in}\ \mathcal{L}[\lambda.\ \mathrm{let}\ 1\ 0\ \mathrm{in}\ \uparrow_2^1(r'), \mathcal{F}] \qquad \text{if $\mathcal{L}[r, \mathcal{F}] = \mathrm{let}\ e\ \mathrm{in}\ r'$ and $e$ contains $0$} \\
\mathcal{L}[\lambda. r, \_] &= \mathrm{let}\ \uparrow_0^{-1}(e)\ \mathrm{in}\ \mathcal{L}[\lambda.\ \updownarrow_0^1(r'), \mathcal{F}] \qquad \text{if $\mathcal{L}[r, \mathcal{F}] = \mathrm{let}\ e\ \mathrm{in}\ r'$} \\
\mathcal{L}[\lambda. r, \_] &= \lambda. \mathcal{L}[r, \mathcal{F}] \\
\mathcal{L}[\mathrm{let}\ e\ \mathrm{in}\ r, \mathcal{C}_\mathrm{toplevel}] &= \mathcal{L}[\mathrm{let}\ e'\ \mathrm{in}\ \mathrm{let}\ r'\ \mathrm{in}\ \uparrow_1^1(r), \mathcal{C}_\mathrm{toplevel}] \qquad \text{if $\mathcal{L}[e, \mathcal{F}] = \mathrm{let}\ e'\ \mathrm{in}\ r'$} \\
\mathcal{L}[\mathrm{let}\ e\ \mathrm{in}\ r, \mathcal{T}] &= \mathrm{let}\ \mathcal{L}[e, \mathcal{T}]\ \mathrm{in}\ \mathcal{L}[r, \mathcal{T}] \\
\mathcal{L}[\mathrm{let}\ e\ \mathrm{in}\ r, \mathcal{F}] &= \mathrm{let}\ \lambda.\ e'\ \mathrm{in}\ \mathcal{L}[\mathrm{let}\ \uparrow_0^1(\mathcal{L}[e])\ \mathrm{in}\ \mathrm{let}\ 1\ 0\ \mathrm{in} \uparrow_2^1(r'), \mathcal{F}] \qquad \text{if $\mathcal{L}[r, \mathcal{F}] = \mathrm{let}\ e'\ \mathrm{in}\ r'$, $\mathcal{L}[e] \neq \lambda.\ \_$, $e' = \lambda.\ \_$, and $e'$ contains $0$} \\
\mathcal{L}[\mathrm{let}\ e\ \mathrm{in}\ r, \mathcal{F}] &= \mathrm{let}\ \uparrow_0^{-1}(e')\ \mathrm{in}\ \mathcal{L}[\mathrm{let}\ \uparrow_0^1(e)\ \mathrm{in}\ \updownarrow_0^1(r'), \mathcal{F}] \qquad \text{if $\mathcal{L}[r, \mathcal{F}] = \mathrm{let}\ e'\ \mathrm{in}\ r'$, $\mathcal{L}[e] \neq \lambda.\ \_$, and $e' = \lambda.\ \_$} \\
\mathcal{L}[\mathrm{let}\ e\ \mathrm{in}\ r, \mathcal{F}] &= \mathrm{let}\ \mathcal{L}[e, \mathcal{F}]\ \mathrm{in}\ \mathrm{let}\ \mathcal{L}[r, \mathcal{F}]\ \mathrm{in}\ \mathrm{let}\ \lambda.\ 0\ \mathrm{in}\ 0\ 1 \qquad \text{if $\mathcal{L}[r, \mathcal{F}] = \lambda.\ \_$} \\
\mathcal{L}[\mathrm{let}\ e\ \mathrm{in}\ r, \mathcal{F}] &= \mathrm{let}\ \mathcal{L}[e, \mathcal{F}]\ \mathrm{in}\ \mathcal{L}[r, \mathcal{F}]
\end{align} 
}

本来はここで「あとは草を生やすだけ」となるはずなのですが, Grass の文法では関数定義と関数適用しか存在しないため, 変数が単体で出現するような場合は • を除いて, 適当な関数適用に置き換えてやる必要があります.

つまり最終的にはこうしたい.

  • n ::= • | n ↑
  • a ::= n n
  • m ::= a | let a in m
  • f ::= λ• | λf | λm
  • r ::= a | f | let a in r | let f in r

lambda lifting の処理を書き換えても良いのですが, 正直 lambda を lift しない処理をここに加えるのも微妙なので, ここでは正規化の部分を変更しました.

Grass 正規化

というわけで, (変更を加える前の) A-正規化の後に, もうひとつ別の正規化を挟んでやります (とりあえず Grass 正規化と呼ぶことにする. 何か別の名前があるかも).

変換後の形はこんな感じです.

  • n ::= • | n ↑
  • a ::= n n
  • f ::= λ• | λr
  • r ::= a | f | let a in r | let f in r

具体的にどう処理するかはこんな感じ.


\begin{align}
\mathcal{G}[0] &= 0 \\
\mathcal{G}[n] &= \mathrm{let}\ \lambda.\ 0\ \mathrm{in}\ 0\ \uparrow_0^1(n) \\
\mathcal{G}[n\ n'] &= n\ n' \\
\mathcal{G}[\lambda.\ r] &= \lambda.\ \mathcal{G}[r] \\
\mathcal{G}[(\lambda.\ r)\ t] &= \mathrm{let}\ \mathcal{G}[\lambda.\ r]\ \mathrm{in}\ \mathcal{G}[0\ \uparrow_0^1(t)] \\
\mathcal{G}[t\ (\lambda.\ r)] &= \mathrm{let}\ \mathcal{G}[\lambda.\ r]\ \mathrm{in}\ \mathcal{G}[\uparrow_0^1(t)\ 0] \\
\mathcal{G}[\mathrm{let}\ n\ \mathrm{in}\ r] &= \mathcal{G}[\uparrow_0^{-1}([0 \mapsto \uparrow_0^1(n)]r)] \\
\mathcal{G}[\mathrm{let}\ e\ \mathrm{in}\ r] &= \mathcal{G}[\uparrow_0^{-1}([0 \mapsto \uparrow_0^1(n)]r)] \qquad \text{if $\mathcal{G}[e] = n$} \\
\mathcal{G}[\mathrm{let}\ e\ \mathrm{in}\ r] &= \mathcal{G}[e] \qquad \text{if $\mathcal{G}[r] = 0$} \\
\mathcal{G}[\mathrm{let}\ e\ \mathrm{in}\ r] &= \mathrm{let}\ \mathcal{G}[e]\ \mathrm{in}\ \mathcal{G}[r]
\end{align}

こうしてから同じ lambda lifting の手続きで処理してやると,

  • n ::= • | n ↑
  • a ::= n n
  • m ::= a | let a in m
  • f ::= λ• | λf | λm
  • r ::= a | f | let a in r | let f in r

となって, 無事目的の結果が得られました.

その他, 先頭が関数にならない (Grass の文法で許されない) 場合は適当に wv とか余計な草を生やします. また, Grass 正規化の際にプログラム中に恒等関数が大量に発生するので, 適当に重複したものを省いてやるような最適化も挟んでやりました.

まとめ

型無しラムダ計算を,

  • e ::= x | λx.e | e e

de Bruijn index 化して,

  • n ::= • | n ↑
  • e ::= n | λe | e e

A-正規化して,

  • n ::= • | n ↑
  • t ::= n | λr
  • e ::= t | t t
  • r ::= e | let e in r

Grass 正規化して,

  • n ::= • | n ↑
  • a ::= n n
  • f ::= λ• | λr
  • r ::= a | f | let a in r | let f in r

Lambda lifting (?) で全ての関数をトップレベルに集めて,

  • n ::= • | n ↑
  • a ::= n n
  • m ::= a | let a in m
  • f ::= λ• | λf | λm
  • r ::= a | f | let a in r | let f in r

あとは草を生やすだけｗｗｗｗｗ

ところで何とは言いませんがほしい物リストです.

参考