fs2.Pull#compile 勉強会 その3
#fs2　#fs2.Pull#compile_勉強会
前: fs2.Pull#compile 勉強会 その2
次: fs2.Pull#compile 勉強会 その4
今回やりたいこと
fs2.Pull#compile 勉強会 その0 より
cats-effect の IOFiber の実装 (つまり、cats.effect.IO から Future などへどう変換するか) 、の中身を見る
fs2.Pull#compile 勉強会 その2 より
ラムダ計算 ✅ → (単純なスタックベースの抽象機械 →) CEK 機械 → IOFiber
…というつもりだったんですが、ちょうど良い複雑度の「単純なスタックベースの抽象機械」を僕が思いつけなかったので、いきなり CEK 機械を見ます
Kory.iconメモ： 逆に、CEK 機械の一般の話をしつつ、算術式の実行ってこうできますよね～という話をしていくのがいいかも
ThenApplyAbstraction 継続が現れないような CEK 機械の trace を見せるイメージ
今回の旅行のしおり
そもそも、何をするために CEK 機械を持ち出してくるのか
λ計算 + α の項 (プログラムっぽいもの) の計算 (つまりプログラムの実行) を自動的に行うことができて、うれしい
想定質問: 別に、そんなにガチャガチャ機械っぽく動くようなものを持ってこなくても、前回我々は手作業でラムダ項を簡約していったわけだし、それと同じようなことをすれば済むのでは？
Kory.icon: ラムダ計算の簡約は非決定的
例: Ω = (\x. x x)(\x. x x) としたとき、(λx. λy. x) (λz. z) Ω のどこを簡約するか、によって、正規形 \z. z に到達できるかが変わる
「+ α」、とは？
拡張λ計算
\n. (+) n 1 みたいな項を書きたい
Scala でいう n => n + 1
(\n. (+) n n) 3 → (+) 3 3 → 6 という簡約列を期待したい
CEK 機械に何を (初期入力として) 与えて、何を最終的に (出力として) 取り出すのか？
入力は (拡張) λ項
下の「REPL に入力できるプログラム例」に書いているようなやつ
出力は「値」
拡張λ計算における「値」とは何か？
定数　もしくは　ラムダ抽象
値であるもの
3 (定数)
true (定数)
\x. x
\x. (\a b. a)(\y. x)
簡約されると \x b y. x になるんだけど…
「関数の中身にまでは立ち入らない / 簡約はしない」
値でないもの
[Add 42 5] (組み込みオペレータ呼び出し)
[Add [Mul 3 2] 4]
[If true 2 1]
(\a b. a)(\x. x) (適用)
CEK 機械 + REPL を作ってきたので、まずは戯れてもらう
https://github.com/kory33/scala3-lambda-calculus
frontends/cli/src/main/scala/io/github/kory33/scala3_lambda_calculus/CLI.scala
sbt ターミナルで次を実行するとよい
cliFrontend / runMain io.github.kory33.scala3_lambda_calculus.CLI
実際の動作履歴を見ながら、CEK機械の一般の状態とはどういうものなのか、というのを説明し、CEK 機械の状態の遷移関係とはどういったものであるか、というかむしろ、どうなっていないとおかしいのか、というのを見ていく
「項 (プログラム) 側で評価が進められるときは進めていく、その際に未評価の部分を一旦脇に置いておく必要があるときには、「戻ってきたときにその未評価の部分についてどうこうする」という情報を継続側に積み、評価できなくなったら継続を切り崩していく」ことでプログラムの評価が進められる、という話をする
ここまで見ていれば次回は IOFiber を見ていってﾊﾊｰﾝとなれるはず (？)
REPL に入力できるプログラム例
[Mul [Add 3 [Mul 2 4]] 5]
つまり、 (3 + (2 * 4)) * 5
これの実行跡はこんな感じ
## は「評価結果を代入する予定の穴」。
CEK(Cl<[Add 3 [Mul 2 4]], {}>, [Mul ## Cl<5, {}>] -> HALT) というのは、「[Add 3 [Mul 2 4]] を評価した後、Mul ## Cl<5, {}> の ## の部分に結果を入れて他の引数 (今回は Cl<5, {}>) を評価し、Mul 全体を評価し、HALT せよ」という状態。
code:arith_cek_trace.ini
Eval, step 0> CEK(Cl<[Mul [Add 3 Mul 2 4] 5], {}>, HALT)
Eval, step 1> CEK(Cl<[Add 3 Mul 2 4], {}>, Mul ## Cl<5, {}> -> HALT)
Eval, step 2> CEK(Cl<3, {}>, [Add ## Cl<Mul 2 4, {}>] -> Mul ## Cl<5, {}> -> HALT)
Eval, step 3> CEK(Cl<Mul 2 4, {}>, Add Cl<3, {}> ## -> Mul ## Cl<5, {}> -> HALT)
Eval, step 4> CEK(Cl<2, {}>, Mul ## Cl<4, {}> -> Add Cl<3, {}> ## -> Mul ## Cl<5, {}> -> HALT)
Eval, step 5> CEK(Cl<4, {}>, Mul Cl<2, {}> ## -> Add Cl<3, {}> ## -> Mul ## Cl<5, {}> -> HALT)
Eval, step 6> CEK(Cl<8, {}>, Add Cl<3, {}> ## -> Mul ## Cl<5, {}> -> HALT)
Eval, step 7> CEK(Cl<11, {}>, Mul ## Cl<5, {}> -> HALT)
Eval, step 8> CEK(Cl<5, {}>, Mul Cl<11, {}> ## -> HALT)
Eval, step 9> CEK(Cl<55, {}>, HALT)
Evaluation terminated successfully
Result term: 55
env: {}
(\f x. f(f(x)))(\x. x)
前回の演習問題 1
code:practice_1_cek_trace.js
Eval, step 0> CEK(Cl<(\f x. f (f x)) (\x. x), {}>, HALT)
Eval, step 1> CEK(Cl<\f x. f (f x), {}>, (## Cl<\x. x, {}>) -> HALT)
Eval, step 2> CEK(Cl<\x. x, {}>, (Cl<\f x. f (f x), {}> ##) -> HALT)
Eval, step 3> CEK(Cl<\x. f (f x), {f -> Cl<\x. x, {}>}>, HALT)
Evaluation terminated successfully
Result term: \x. f (f x)
env: {f -> Cl<\x. x, {}>}
(\f x. f(f(x))) (\x. x) 3
↑のやつに 3 を適用したもの
code:practice_1_3_cek_trace.js
Eval, step 0> CEK(Cl<(\f x. f (f x)) (\x. x) 3, {}>, HALT)
Eval, step 1> CEK(Cl<(\f x. f (f x)) (\x. x), {}>, (## Cl<3, {}>) -> HALT)
Eval, step 2> CEK(Cl<\f x. f (f x), {}>, (## Cl<\x. x, {}>) -> (## Cl<3, {}>) -> HALT)
Eval, step 3> CEK(Cl<\x. x, {}>, (Cl<\f x. f (f x), {}> ##) -> (## Cl<3, {}>) -> HALT)
Eval, step 4> CEK(Cl<\x. f (f x), {f -> Cl<\x. x, {}>}>, (## Cl<3, {}>) -> HALT)
Eval, step 5> CEK(Cl<3, {}>, (Cl<\x. f (f x), {f -> Cl<\x. x, {}>}> ##) -> HALT)
Eval, step 6> CEK(Cl<f (f x), {f -> Cl<\x. x, {}>, x -> Cl<3, {}>}>, HALT)
Eval, step 7> CEK(Cl<f, {f -> Cl<\x. x, {}>, x -> Cl<3, {}>}>,
(## Cl<f x, {f -> Cl<\x. x, {}>, x -> Cl<3, {}>}>) -> HALT)
Eval, step 8> CEK(Cl<\x. x, {}>, (## Cl<f x, {f -> Cl<\x. x, {}>, x -> Cl<3, {}>}>) -> HALT)
Eval, step 9> CEK(Cl<f x, {f -> Cl<\x. x, {}>, x -> Cl<3, {}>}>, (Cl<\x. x, {}> ##) -> HALT)
Eval, step 10> CEK(Cl<f, {f -> Cl<\x. x, {}>, x -> Cl<3, {}>}>,
(## Cl<x, {f -> Cl<\x. x, {}>, x -> Cl<3, {}>}>) -> (Cl<\x. x, {}> ##) -> HALT)
Eval, step 11> CEK(Cl<\x. x, {}>,
(## Cl<x, {f -> Cl<\x. x, {}>, x -> Cl<3, {}>}>) -> (Cl<\x. x, {}> ##) -> HALT)
Eval, step 12> CEK(Cl<x, {f -> Cl<\x. x, {}>, x -> Cl<3, {}>}>,
(Cl<\x. x, {}> ##) -> (Cl<\x. x, {}> ##) -> HALT)
Eval, step 13> CEK(Cl<3, {}>, (Cl<\x. x, {}> ##) -> (Cl<\x. x, {}> ##) -> HALT)
Eval, step 14> CEK(Cl<x, {x -> Cl<3, {}>}>, (Cl<\x. x, {}> ##) -> HALT)
Eval, step 15> CEK(Cl<3, {}>, (Cl<\x. x, {}> ##) -> HALT)
Eval, step 16> CEK(Cl<x, {x -> Cl<3, {}>}>, HALT)
Eval, step 17> CEK(Cl<3, {}>, HALT)
Evaluation terminated successfully
Result term: 3
env: {}
(\x.x(x)(\a.a)) (\x.x(x)(\a.a))
止まらなくなるやつ　val maxSteps = 20 くらいで実行することをお勧めします
(\f z. f (f (f z))) (\n. [Mul n 2]) 1
「「×2」を 1 に対して 3 回行う」、つまり、(((1) * 2) * 2) * 2
code:repeated_times_two.js
Eval, step 0> CEK(Cl<(\f z. f (f (f z))) (\n. Mul n 2) 1, {}>, HALT)
Eval, step 1> CEK(Cl<(\f z. f (f (f z))) (\n. Mul n 2), {}>, (## Cl<1, {}>) -> HALT)
Eval, step 2> CEK(Cl<\f z. f (f (f z)), {}>, (## Cl<\n. Mul n 2, {}>) -> (## Cl<1, {}>) -> HALT)
Eval, step 3> CEK(Cl<\n. Mul n 2, {}>, (Cl<\f z. f (f (f z)), {}> ##) -> (## Cl<1, {}>) -> HALT)
Eval, step 4> CEK(Cl<\z. f (f (f z)), {f -> Cl<\n. Mul n 2, {}>}>, (## Cl<1, {}>) -> HALT)
Eval, step 5> CEK(Cl<1, {}>, (Cl<\z. f (f (f z)), {f -> Cl<\n. Mul n 2, {}>}> ##) -> HALT)
Eval, step 6> CEK(Cl<f (f (f z)), {f -> Cl<\n. Mul n 2, {}>, z -> Cl<1, {}>}>, HALT)
...
Eval, step 24> CEK(Cl<2, {}>, Mul ## Cl<2, {n -> Cl<2, {}>}> -> (Cl<\n. Mul n 2, {}> ##) -> HALT)
Eval, step 25> CEK(Cl<2, {n -> Cl<2, {}>}>, Mul Cl<2, {}> ## -> (Cl<\n. Mul n 2, {}> ##) -> HALT)
Eval, step 26> CEK(Cl<4, {}>, (Cl<\n. Mul n 2, {}> ##) -> HALT)
Eval, step 27> CEK(Cl<Mul n 2, {n -> Cl<4, {}>}>, HALT)
Eval, step 28> CEK(Cl<n, {n -> Cl<4, {}>}>, Mul ## Cl<2, {n -> Cl<4, {}>}> -> HALT)
Eval, step 29> CEK(Cl<4, {}>, Mul ## Cl<2, {n -> Cl<4, {}>}> -> HALT)
Eval, step 30> CEK(Cl<2, {n -> Cl<4, {}>}>, Mul Cl<4, {}> ## -> HALT)
Evaluation terminated successfully
Result term: 8
env: {}
(\x y. x) (\z. z) ((\x. x x)(\x. x x))
(\x y. x) id Ω
Ω を Ω のまま (\x y. x) id の方を先に簡約していけば正規形 (id) に到達するはずだが…
CEK 機械は、まず引数を値になるまで評価しようとするので、終わらない
CEK 機械の一般論
CEK 機械は…
call-by-value (「値呼び」と訳されることがある)、つまり、「関数の引数を評価しきってからβ簡約する」ような実行方式
引数よりも先に関数側を評価する
X Y のような適用があったとき、 X が値 v_X になるまで評価を進めて、v_X がラムダ抽象 (\x. b_X) であることを確認してから Y の評価を進めて、Y が v_Y になったら、b_X.substitute(x, v_Y) を評価していく
組み込みオペレータ呼び出しに関しては、「左から右」に引数を評価していく
[Add X Y] みたいな組み込みオペレータ呼び出しがあったとき、まず X を値にまで評価し、次に Y を値にまで評価し、最後に、二つの値にて Add を実行する
[Add X Y] → … → [Add v_X Y] → … → [Add v_X v_Y] → (v_X + v_Y) のような簡約をする
(今回の組み込みオペレータのセット (算術演算とブール演算) では、「左から右」に引数を評価しているという事実は (機械の内部状態からしか) 観測できない。これが例えば、[Print x] のような組み込みオペレータ (x を出力して x を結果として返す) があれば、[If [Print "Left"] Ω [Print "Right"]] を評価しようとしたときに Left と Right のどちらが出力されるかを見ることで左から右に評価しているのか、逆順に評価しているのかがわかる)
↑の前提があれば計算跡を読み取れるはず？
Kory.icon C 言語とかもこんな感じに「先に関数を評価して、引数を左から順に評価して、呼び出す」ですよね？
hsjoihs.icon そんなことはなく、C とは大変におおらかな言語でございまして、規格書に In the function call (*pf[f1()]) (f2(), f3() + f4()), the functions f1, f2, f3, and f4 may be called in any order. All side effects have to be completed before the function pointed to by pf[f1()] is called. とある
Kory.icon あ～なるほど。関数呼び出しが発生するときに「関数と引数が評価し終わっている」ことだけ保証されているのか。じゃあ CEK 機械はそれよりも強く評価順が決まっている機械ということになりますね
この辺の話の理論的な議論はこちらがおすすめ
https://www.youtube.com/watch?v=UfBYznSIqKE