戻る

pretty print ができたので、簡約用に de bruijn index にするか

lo48576/xslt10-lambda-calculus: [experimental] Lambda calculus by XSLT
https://github.com/lo48576/xslt10-lambda-calculus

XSLT は純粋関数型言語なので、簡単に de bruijn index 化が実装できた(???)

ワンステップ簡約ならできそうだけど、一気に簡約するなら exslt の拡張を使わないと厳しそうだ (簡約後の XML ツリーを再度テンプレートに投げて変換みたいなことをしないといけないので)

EXSLT - exsl:node-set
http://exslt.org/exsl/functions/node-set/

ワンステップ簡約でも、変数の shift とか代入にどうやら exsl:node-set が欲しいので、もうあきらめて使うことにする

XSLT プログラミング、デバッグがめっちゃ面倒なんだが……

やはり快適なデバッグのためには評価途中の処理系の状態や変数が覗き見できる必要がある、自分で XSLT 処理系を作るしかない……

ワンステップ評価できた

(λ λ (λ λ $2) $1 ($2 $1))
を簡約すると
(λ λ (λ $NaN) ($2 $1))
になった、うれしい(しろめ)

exsl:node-set() の挙動がアレすぎてドツボに嵌まっている

exsl:node-set($var) が新しいドキュメント扱いされてルートが変わるところまでは理解できるんだけど、その結果マッチされるのが var に突っ込んでいない xsl:template[@ match=/] で吐いたはずの要素だったりして、意味がわからん

デバッグ用コードを最初から綺麗に埋め込んで書き直したところ、やっとバグの特定に至ったっぽい (ただしまだ修正していないので当たりかは不明)

当たりだった

普通の評価器実装できた、もう少し整理したら push する

lo48576/xslt10-lambda-calculus: [experimental] Lambda calculus by XSLT
https://github.com/lo48576/xslt10-lambda-calculus

できた (いま README 書いてる)

ひととおり必要なものは整備できたので、 Y コンビネータあたりを使うクソデカテストケースを用意したい気持ちになった

SKI コンビネータからの変換も書くか……

どうせなら変数定義があった方がいい？

先にη変換を実装した方がよさそう (テストケースの作り方的に)

Merge branch 'feature/eta-reduction' into develop · lo48576/xslt10-lambda-calculus@82ab57d
https://github.com/lo48576/xslt10-lambda-calculus/commit/82ab57d2f996ac84815da3f21ed6ffb970ab9599

η変換を実装したのでテストが書きやすくなった、次は let 式の実装かな

フラットな apply とどちらをやるか悩む……

よく考えたら、フラットな apply も let 式も、脱糖によって実現できてしまうのか……いよいよ悩ましい

しかし脱糖してから評価となると、テストケースで脱糖後の項と向き合うことになってつらそうだ……どうしたものか

や、でも評価器に組込むのは(一部構文だけを別機能に分離するのに比べれば)多少は簡単だろうし、メンテナンスを考えると構文糖衣として実装すべきだな

Merge branch 'feature/desugar-apply-at-once' into develop · lo48576/xslt10-lambda-calculus@7f93e0e
https://github.com/lo48576/xslt10-lambda-calculus/commit/7f93e0e11d3e7d956c416d767d6ae34f6c6507f0

(a b c d) を (((a b) c) d) に脱糖する機能を実装した

次は (λa b c. x) から (λa. (λb. (λc. x))) への脱糖を実装して、それができたら let 式の実装

複数パラメータの脱糖はできたけど、 pretty printer が脱糖前の省略記法を使うべきかそうでないかという問題が出てきた
たとえば S コンビネータを
λx. λy. λz. x z (y z)
と
λx y z. x z (y z)
のどちらで表示すべきか

((x z) (y z)) を (x z (y z)) とするオプションは「括弧の省略」という名目で実装してあるんだけど、これがそもそも単なる括弧の省略ではなく構文糖衣の利用であると捉えるべきなのかな

でも (λx. (λy. x)) を ( λx. λy. x) と表示するのは単なる括弧の省略だし……

ひとまずλ抽象における複数引数と、 let 式のサポートは実装した (let* と letrec は面倒なので後回し、気が向いたらやる)

let* の方が let より簡単だし、そっちは今実装してもいいんだけど、「*」が XML の要素名として使えないのでどういう名前にしようかと迷ったところで後回しにすることを決めた

SKI コンビネータで 1+2 が計算できた

3+4 のテストケースを書こうとしたらさすがに let だけだとつらかったので、 let* 相当のものも作るわ……

Add a test case 09-ski-one-plus-two · lo48576/xslt10-lambda-calculus@af29d79
https://github.com/lo48576/xslt10-lambda-calculus/commit/af29d79952961eb2c1fc08f315331bd8cda21ea6

テストケースは温かみのある手計算を併用して書いています