More Related Content
What's hot (17)
Similar to 型无しラムダ计算―翱颁补尘濒による実装― (20)
Recently uploaded (13)
![ElasticsearchでSPLADEする [Search Engineering Tech Talk 2025 Winter]](https://cdn.slidesharecdn.com/ss_thumbnails/searchtech-250228102455-ddc5ce09-thumbnail.jpg?width=560&fit=bounds)
型无しラムダ计算―翱颁补尘濒による実装―
- 2. 自己紹介 @Pro_ktmr ? 大阪府立大手前高等学校 最近プロコンを主催しました。関西弁がちょくちょく入ってきます。 ? SuperCon2018 本選出場 何もしてませんが明日から行ってきます。スケジュールが鬼です。 ? PCK2018モバイル部門 本選出場 競プロだけじゃなくて実務っぽいこともやってます。
- 3. これから話すこと ? 型無しラムダ計算を プログラムで動かしたい！ →インタプリタをつくる レキサー(字句解析器)とパーサ(構文解析器)は既存のものを使用 ? 自動メモリ管理やパターンマッチ があるOCamlを使って書いてみる ※OCaml(オーキャムル、オーキャメル)???オブジェクト指向のML系(関数型)言語 ? 競プロの問題で きちんと動くか確認！
- 4. 発表の流れ 1. 抽象構文木の実装 2. シフトと代入関数の実装 3. 評価器の実装 4. 競プロの問題を解く
- 6. 抽象構文木の実装① type term = TmVar of info * int * int | TmAbs of info * string * term | TmApp of info * term * term ? info型の要素を注記として利用 (エラー表示用)
- 7. 抽象構文木の実装② ?変数 TmVar TmVar of info * int * int 1. 数(de Brujinインデックス)で表現 2. 変数が現れる文脈全体の長さも保 持して一貫性検査を行う
- 8. 抽象構文木の実装③ ?ラムダ抽象 TmAbs TmAbs of info * string * term 1. 束縛変数名(文字列) 2. ラムダ抽象の本体である部分項 を保持
- 9. 抽象構文木の実装④ ?関数適用 TmApp TmApp of info * term * term 適用される2つの部分項を保持
- 10. 発表の流れ 1. 抽象構文木の実装 2. シフトと代入関数の実装 3. 評価器の実装 4. 競プロの問題を解く
- 12. シフトの実装 let termShift d t = let rec walk c t = match t with TmVar(fi,x,n) -> if x>=n then TmVar(fi,x+d,n+d) else TmVar(fi,x,n+d) | TmAbs(fi,x,t1) -> TmAbs(fi,x,walk (c+1) t1) | TmApp(fi,t1,t2) -> TmApp(fi,walk c t1,walk c t2) in walk 0 t 項tをd個シフトする 内部のシフトは内部関数walkで表現
- 13. 代入関数の実装 let termSubst j s t = let rec walk c t = match t with TmVar(fi,x,n) -> if x=j+c then termShift c s else TmVar(fi,x,n) | TmAbs(fi,x,t1) -> TmAbs(fi,x,walk (c+1) t1) | TmApp(fi,t1,t2) -> TmApp(fi,walk c t1,walk c t2) in walk 0 t 項tのj番の変数へ項sを代入する 実際の処理は内部関数walkで表現
- 14. 発表の流れ 1. 抽象構文木の実装 2. シフトと代入関数の実装 3. 評価器の実装 4. 競プロの問題を解く
- 15. 補助述語の実装 let rec isval ctx t = match t with TmAbs(_,_,_) -> true | _ -> false 項が値であるかを検査する関数 次の評価関数の中で補助的に用いる
- 16. 評価関数の実装① let rec eval1 ctx t = match t with TmApp(fi,TmAbs(_,x,t12),v2) when isval ctx v2 -> termSubstTop v2 t12 | TmApp(fi,v1,t2) when isval ctx v1 -> let t2' = eval1 ctx t2 in TmApp(fi, v1, t2') | TmApp(fi,t1,t2) -> let t1' = eval1 ctx t1 in TmApp(fi, t1', t2) | _ -> raise NoRuleApplies 1ステップの評価関数 項tと文脈ctxを渡す
- 17. 評価関数の実装② let rec eval ctx t = try let t' = eval1 ctx t in eval ctx t' with NoRuleApplies -> t 多ステップの評価関数 項tと文脈ctxを渡す 1ステップの評価関数を呼び出す
- 18. 実装したもの ? 抽象構文木 ? シフト、代入関数 ? 評価器 以下は本のWebページから拝借 ? 字句解析器、構文解析器 ? 表示周りの処理 これにてインタプリタ完成！
- 19. 発表の流れ 1. 抽象構文木の実装 2. シフトと代入関数の実装 3. 評価器の実装 4. 競プロの問題を解く
- 20. ここで問題発生！ ? 標準入力はOCamlにラムダ式を渡 すのに使ってしまっている??? ? 標準出力もデバッグ情報が表示さ れるようになっちゃってる??? ? オンラインジャッジは無理 ? 入力サンプルをラムダ式中に手打 ちしよう！(無理やり)
- 22. ラムダ式による実装① c_0 = lambda s. lambda z. z; scc = lambda n. lambda s. lambda z. s (n s z); plus = lambda m. lambda n. lambda s. lambda z. m s (n s z); times = lambda m. lambda n. m (plus n) c_0; fix = lambda f. (lambda x. f (lambda y. x x y)) (lambda x. f (lambda y. x x y)); cn = lambda f. lambda m. if iszero m then c_0 else scc (f (pred m)); churchnut = fix cn; realnut = lambda m. m (lambda x. succ x) 0; 使う関数等をいろいろ宣言しとく
- 23. ラムダ式による実装② w = 4; bit = (churchnut 32); answer = times (churchnut w) bit; realnut answer; 変数wに手打ちで4を入れとく 32をChurch数に変換してbitに入れとく 答えは4と32をかけたものである 答えをChurch数からプリミティブな数に変換
- 24. 実行結果 正解！
- 25. もう一问！(おまけ)
- 26. ラムダ式による実装 c_1 = lambda s. lambda z. s z; tru = lambda t. lambda f. t; fls = lambda t. lambda f. f; pair = lambda f. lambda s. lambda b. b f s; fst = lambda p. p tru; snd = lambda p. p fls; zz = pair c_0 c_0; ss = lambda p. pair (snd p) (plus c_1 (snd p)); prd = lambda m. fst (m ss zz); a = 5; b = 7; answer = times (prd (churchnut a)) (prd (churchnut b)); realnut answer;
- 27. 実行結果 正解！
- 28. まとめ ? 抽象構文木(項を保持する木構造) を実装した ? シフト(インデックスの書き換え) と代入関数を実装した ? 評価関数を実装した ? (入力手打ちだけど)競プロの問題 が解けた！