fs2.Pull#compile 勉強会 その2
今回やりたいこと
cats-effect の IOFiber の実装 (つまり、cats.effect.IO から Future などへどう変換するか、の中身を見る
やっていく（？）
どうやっていこう？いっそ CEK 機械 のような抽象機械について先に学ぶという手がある 究極的には、IOFiber というのは協調的な (「自律的に飽きてくれる」) スタックマシンなので、より簡単なモデルである CEK 機械などを先に見ておくと「あーはい、これは CEK 機械で言うところのアレかぁ」といった納得が生える可能性もある
一方、「環境」などという低レベルな概念は IOFiber には現れないので、それは悩みどころ
聴講者と進め方は相談する
まぁ、ラムダ計算 → (すごく単純なスタックベースの抽象機械 →) CEK 機械 → IOFiber でよさそう
code:js
// λ項的サムシング
a => a // λa.a
b => (a => a) // λb.(λa.a) または λb.λa.a または λba.a
a => b => a // λa.(λb.a) または λa.λb.a または λab.a
(a => a)(x) // => x
// これを (λa.a)(x) が x に「β簡約」される、と言う
// β簡約とは、なんのことはなく、ただの函数適用
// 一般に、 (λx.M)(N) を、「M 中にある x（ちょっとここで細かい話を無視します）を全部 N に置き換えたもの」に変える操作を、β簡約と言う
// 具体例
// (λx. x(x)) (λa.a) をβ簡約すると、どうなる？
// これは要するに x(x) の中の x が identity に置き換わるので、identity(identity)
// identity とは λa.a のことだったので、
// (λa.a)(identity) をもう一度β簡約すると、identityになる
// つまり、最終的に λa.a というラムダ項になる
// **練習問題**：
// (λf.λx. f(f(x)) ) (λx.x) を最大限簡約してください
// ヒント：(λx.x) と (λy.y) は同じ意味の項なので、(λy.y) と書いた方が見やすい
// その 2
// (λx.x(x)(λa.a)) (λx.x(x)(λa.a))
windymelt.icon 練習問題やるっピ〜
(λf.λx. f(f(x)) ) (λx.x)
λx. (λx.x)((λx.x)(x))
λx. (λy.y)((λz.z)(x))
λx. (λz.z)(x)
λx. x
windymelt.icon uoo
(λx.x (x) (λa.a)) (λx.x (x) (λa.a))
(λx.x (x) (λa.a)) (λx.x (x) (λa.a)) (λa.a)
(λx.x (x) (λa.a)) (λa.a)
(λa.a) (λa.a) (λa.a)
λa.a
chen.icon neko
1:
(λf.λx. f(f(x)) ) (λx.x)
λx. (λx.x)((λx.x)(x))
λx. (λx.x)(x)
λx. x
その2:
(λx.x(x)(λa.a)) (λx.x(x)(λa.a))
(λx.x(x)(λa.a)) ((λa.a)(λa.a))
(λx.x(x)(λa.a)) (λa.a)
λa.a(λa.a)(λa.a)
λa.a
hsjoihs.icon 重要ポイント：
f(x)(y) で (x)(y) を結合させて計算するわけにはいかない
Kory.icon 「先に計算」というより、(一般には) f(x)(y) != (f)(x(y))
これは JavaScript を考えれば明らかであり、
code:js
const f = (a) => ( (b) => (a + b) )
f(2)(3) とは 5 になる
f((2)(3)) は (2)(3) が計算できなくてエラーになる
ところで、このことを「ラムダ計算では、関数適用が左結合」といったりする
JavaScript では f(x) が関数呼び出しだが、ラムダ計算ではさらにそこのカッコを削って f x と表記する
f x y と書いたらそれは (f x) y、つまり ( f(x) ) (y) という意味
f と x の間の半角スペースが「関数適用」の中置演算子として振る舞う、と捉えてもいい
hsjoihs.icon さて、これを踏まえ、
(λx.x x c) (λx.x x c)
を簡約することを試みていただきたい
lemoncmd.icon これ簡約できなくなるまでやるんすか
windymelt.icon 不穏な予感がする
(λx.x x c) (λx.x x c)
(λx.x x c) (λx.x x c) c
(λx.x x c) (λx.x x c) c c
(λx.x x c) (λx.x x c) c c c
...
chen.icon meow
(λx.x x c) (λx.x x c)
(λx.x x c) (λx.x x c) c
((λx.x x c) (λx.x x c) c) c
(((λx.x x c) (λx.x x c) c) c) c
((((λx.x x c) (λx.x x c) c) c) c) c
自由変数
λx. x は Scala で言うところの identity であった
λx. y x は？
Scala や JavaScript だと、y ってなんだよ、という話になる
が、文法上は許されている
λy. λx. y x を項であるというためには、λx. y x も項であるということにしておいた方が都合が良い
λx. y x の中の x のように、外側で束縛されている (λv. ... の v の位置に現れている) ような変数を 束縛変数 と呼び、y のように、外側では束縛されていない変数のことを 自由変数 と呼ぶ
演習問題：次の項の自由変数/束縛変数を挙げてください
λx. y x
λx. y (λy. x z y)
λx. (λx. y x)
windymelt.icon
1. 自由変数 y 束縛変数 x
2. 自由変数 初出のy, z 束縛変数 xと二度目のy
3. 自由変数 y 束縛変数 x
chen.icon
束 x / 自 y
束 x, 2つ目のy / 自 z, 一つ目の y
束 x / 自 y
α変換
例えば、Scala で x => x + 2 と書いた後、x にカーソルを合わせて別の変数 y に rename すると、y => y + 2 になる
この操作自体をα変換と言う
つまり、λ抽象の束縛変数の「名前を変える」ような操作
気を付けることがあって、λx. x (λy. x) の二つ目の x を y にリネームすると壊れる
いくつか対処法があって、
そもそも、こういう状況で、 x を y にリネームすることを許さない
x が y になるんだから、内側の λy は新しい y にその名前を譲ってくださいということにする
λx. x (λy. x) -> λx. x (λz. x) -> λy. y (λz. y)
windymelt.icon 「どんどんちっちゃくなっていくから無限に再帰することはない」の、項になんらかの大小関係があると考えたら、帰納法でどんどん減っていって0(的なもの)になるからOKみたいなロジックみがある
これは、そう！実際、こういう場面では「構造帰納法」とか「整礎帰納法」といった帰納法を使いがちです
t.substitute(v, s) というのは、直感的に言えば、t の中の自由な変数 v を項 s に置き換えたもの
α変換のときと同じように、s の自由変数が捕獲されてはならないというのを気を付ける
項 t が正規である もしくは、t は正規形にあるとは、t の中に簡約できる箇所が無いことである
Ω コンビネータ
(λx. x x) (λx. x x)
どう頑張って簡約しても (というか一か所しか簡約できる場所が無くて、そこを簡約すると) 自分自身になってしまう
これは正規形ではない (簡約できる場所があるので) かつ、簡約しても元に戻るので、正規形を持たない (非自明！)
何らかの魔法ような項 o があって、o を特定の魔法のような方法で簡約していくと Ω になるけど、別の魔法ような方法で簡約してくと正規形 n に簡約しきれるかもしれない！
この時、Ω =β o =β n になっていて、Ω と n は等しい！n が Ω の正規形だ！と言えるかもしれない
安心してください、そんなことはあり得ないです。でも、これがあり得ないというのは非自明な事実です
もうちょっと意地悪なものとして (λx. x x x) (λx. x x x) がある
t を簡約していった結果正規形にある項 n が得られたとする。t を別の方法で簡約していったときに、n が得られるとは限らない。
(λx. λy. x) (λz. z) Ω
(λy. (λz. z)) Ω
λz. z
「どこを簡約していくか」というのは、ラムダ計算の体系上で実際に計算をやろうとすると結構重要
「どこを簡約していくか」という情報を「評価戦略」と呼ぶ
この評価戦略を具体的に与える方法として、CEK 機械と呼ばれる機構があります
code:Scala
// 変数。
// 実際のところ、Variable = AnyRef にしていい (値同士が区別可能で無限個あればなんでもいい) んですが、pretty-print しにくいのと、AnyRef をいっぱい作っておくのがひたすらに面倒なので、String を使います
// ちなみに、Variable = BigInteger でももちろんいいです
type Variable = String
def freshVariableNotIn(variableSet: /* 有限 */ SetVariable): Variable = { val alphabet = "abcdefghijklmnopqrstuvwxyz"
val alphabetSize = alphabet.length
def intToVariableName(n: Int): String = {
if (n <= alphabetSize) alphabet.charAt(n - 1).toString
else {
val res = n % alphabetSize
val div = n / alphabetSize
if (res == 0) intToVariableName(div - 1) + alphabet(alphabetSize - 1)
else intToVariableName(div) + alphabet(res - 1)
}
}
@annotation.tailrec
def loop(n: Int): Variable = {
val candidate = intToVariableName(n)
if variableSet(candidate) then loop(n + 1)
else candidate
}
loop(1)
}
// λ項とは…
enum LambdaTerm:
// 変数をひとつ書き下したものは λ 項
case VarReference(variable: Variable)
// 適用。(λx. x x)(λy. y) を Application(λx. x x, λy. y) として扱いたい
case Application(left: LambdaTerm, right: LambdaTerm)
// λ抽象。λx. x x のことを Abstraction("x", Application(VarReference("x"), VarReference("x"))) として扱いたい
case Abstraction(boundVar /* 束縛変数 */: Variable, body: LambdaTerm)
import LambdaTerm.*
extension (t: LambdaTerm)
def freeVariables: SetVariable = t match case VarReference(v) => Set(v)
case Application(left, right) => left.freeVariables ++ right.freeVariables
case Abstraction(boundVar, body) => body.freeVariables - boundVar
case VarReference(v) => Set(v)
case Application(left, right) => left.variables ++ right.variables
case Abstraction(boundVar, body) => body.variables + boundVar
def replaceFreeVariableWithAnother(
original: Variable,
newVariable: Variable
): LambdaTerm = t match
case VarReference(v) =>
if v == original then VarReference(newVariable) else VarReference(v)
case Application(left, right) =>
Application(
left.replaceFreeVariableWithAnother(original, newVariable),
right.replaceFreeVariableWithAnother(original, newVariable)
)
case Abstraction(boundVar, body) =>
if boundVar == original then
// original が束縛されちゃってたらその先は置き換えない
Abstraction(boundVar, body)
else
Abstraction(
boundVar,
body.replaceFreeVariableWithAnother(original, newVariable)
)
// 捕獲回避代入
// t.substitute(v, s) というのは、直感的に言えば、t の中の自由な v を s に置き換えたもの
def substitute(
varToReplace: Variable,
term: LambdaTerm
): LambdaTerm = t match
case VarReference(variable) =>
if variable == varToReplace then term else t
case Application(left, right) =>
Application(
left.substitute(varToReplace, term),
right.substitute(varToReplace, term)
)
case Abstraction(boundVar, body) =>
if (boundVar == varToReplace) {
t
} else if (!term.freeVariables.contains(boundVar)) {
Abstraction(boundVar, body.substitute(varToReplace, term))
} else {
// 捕獲回避
val newBoundVar = freshVariableNotIn(term.variables ++ body.variables)
Abstraction(
newBoundVar,
body.replaceFreeVariableWithAnother(boundVar, newBoundVar)
).substitute(varToReplace, term)
}
// β簡約
def betaReduceOnce(left: Abstraction, right: LambdaTerm): LambdaTerm =
left.body.substitute(left.boundVar, right)
code:scala
// freshVariableNotIn#intToVariableName の別実装
def col(num: Int): String =
val (a, z) = ('a', 'z')
val l = z - a + 1
val s = StringBuilder()
var n = num
while (n >= 0) do
s.insert(0, s"${(n % l + a).toChar}")
n = Math.floorDiv(n, l) - 1
s.toString()