ラムダ計算の評価器とBöhm tree

気持ち

『きつねさんでもわかるLLVM』を読んだので何か書いてみようと思い, 一回書いておくかというのもあってラムダ計算の評価器を書くことにしました. 書いた結果, LLVMを使っても仕方ないことに気がついた(遅い！) のでLLVMはつかっていません. ついでにBöhm treeを出力させることにしました.

Böhm tree

ググると詳しく解説したPDFなどが見つかるので簡単に書きます.

任意のラムダ項は

${ \displaystyle \lambda x_0 . \cdots \lambda x_n . x M_0 M_1 \cdots M_m \ \ (n, m \geq 0) }$
${ \displaystyle \lambda x_0 . \cdots \lambda x_n . (\lambda x M) M_0 \cdots M_m \ \ (n \geq 0 , m \geq 0) }$

のどちらかの形にかけます*1. 1 を頭正規形といい, 2 の $(\lambda x M) M_0$ という部分を頭基といい, 頭基をβ簡約することを頭変換といいます. あるラムダ項が頭正規形をもつなら頭変換だけで頭正規形に変換できることが知られています.

これらの性質を使ってラムダ項を木として表現したものをBöhm tree といいます. 以下が定義です.

ラムダ項 ${M}$ が

頭正規形の形のとき, BT( ${M}$ ) = 親 : $\lambda x_0 . \cdots \lambda x_n . x$ , 子 : BT( ${M_0}$ ), ${\cdots}$ , BT( ${M_m}$ )
2の形のとき, 頭正規形になるまで頭変換を繰り返します. 頭正規形にならないときは無限木は書いていられないので BT( ${M}$ ) ${= \bot}$ とします.

これらを繰り返すことで得られる木がBöhm treeです.

コード

出力の形式をどうするか考えましたが, 手軽さと, ひょっとしていつか使えるかもしれないと思い $\LaTeX$ のコードとして出力することにしました. 木を表示には tikz-qtree*2というパッケージをつかいました.*3.

C++で書きました. 良いC++書き方がわからないので変なことをしている可能性があります. 定義通りではないのですが, 正規形があるかわからない場合はある程度繰り返して止まるようになっています.

github.com

例

出力された $\LaTeX$ のコードから出力された結果です. 入力とともに出力されています.

f:id:wkwkes:20160309221223p:plain f:id:wkwkes:20160309221230p:plain f:id:wkwkes:20160309221236p:plain f:id:wkwkes:20160309221242p:plain f:id:wkwkes:20160309221249p:plain