Upgrade to Pro
— share decks privately, control downloads, hide ads and more …
Speaker Deck
Features
Speaker Deck
PRO
Sign in
Sign up for free
Search
Search
私を SKI に連れてって
Search
Susisu
December 11, 2015
Programming
0
280
私を SKI に連れてって
Lazy K の紹介のつもりが型無しラムダ計算の説明から入ったので長くなりすぎたもの
Susisu
December 11, 2015
Tweet
Share
More Decks by Susisu
See All by Susisu
null or undefined
susisu
25
6.8k
Mackerel のフロントエンドフレームワーク移行 序章 / Hatena Engineer Seminar #13
susisu
0
2k
スクリーンショット撮影のために Puppeteer を操る / Kyoto.js 16
susisu
0
790
BuckleScript 使ってみた
susisu
0
280
Atom パッケージ開発のすゝめ
susisu
1
2.1k
5分でわかる Curry–Howard 同型対応
susisu
0
900
ジェネレータを有効活用し隊 / Kyoto.js 11 LT
susisu
2
2.1k
遅延評価と健康
susisu
0
580
楽しく学ぶ難解プログラミング言語
susisu
0
730
Other Decks in Programming
See All in Programming
生成 AI を活用した toitta 切片分類機能の裏側 / Inside toitta's AI-Based Factoid Clustering
pokutuna
0
560
Nuxt UI Pro、NuxtHub、Nuxt Scripts、Nuxtエコシステムをふんだんに利用して開発するコーポレートサイト@Vue Fes Japan 2024
shingangan
3
880
Boost Performance and Developer Productivity with Jakarta EE 11
ivargrimstad
0
790
PLoP 2024: The evolution of the microservice architecture pattern language
cer
PRO
0
1.5k
ECSのサービス間通信 4つの方法を比較する 〜Canary,Blue/Greenも添えて〜
tkikuc
11
2.3k
What’s New in Compose Multiplatform - A Live Tour (droidcon London 2024)
zsmb
1
330
go.mod、DockerfileやCI設定に分散しがちなGoのバージョンをまとめて管理する / Go Connect #3
arthur1
10
2.3k
Piniaの現状と今後
waka292
5
1.4k
現場で役立つモデリング 超入門
masuda220
PRO
12
2.9k
JaSST 24 九州:ワークショップ(は除く)実践!マインドマップを活用したソフトウェアテスト+活用事例
satohiroyuki
0
260
Sidekiqで実現する 長時間非同期処理の中断と再開 / Pausing and Resuming Long-Running Asynchronous Jobs with Sidekiq
hypermkt
6
2.6k
/←このスケジュール表に立ち向かう フロントエンド開発戦略 / A front-end development strategy to tackle a single-slash schedule.
nrslib
1
590
Featured
See All Featured
Bootstrapping a Software Product
garrettdimon
PRO
305
110k
How to Ace a Technical Interview
jacobian
275
23k
Optimising Largest Contentful Paint
csswizardry
33
2.9k
Designing for humans not robots
tammielis
249
25k
Designing Experiences People Love
moore
138
23k
Fontdeck: Realign not Redesign
paulrobertlloyd
81
5.2k
For a Future-Friendly Web
brad_frost
175
9.4k
Optimizing for Happiness
mojombo
376
69k
Done Done
chrislema
181
16k
Build your cross-platform service in a week with App Engine
jlugia
229
18k
CoffeeScript is Beautiful & I Never Want to Write Plain JavaScript Again
sstephenson
159
15k
Java REST API Framework Comparison - PWX 2021
mraible
PRO
28
7.9k
Transcript
ࢲΛ SKI ʹ࿈Εͯͬͯ 201x年m月d日 第3回 OUCC LT会 のつもりだったけど長すぎてボツ
͓લ୭ͬͯਓͷͨΊͷ すしす Twitter: @susisu2413 GitHub: susisu
ຊͷ༧ఆ λ計算入門 SKIコンビネータ入門 Lazy K の紹介
λܭࢉೖ
λܭࢉͱ "計算"を関数とその適用でモデル化 したもの 関数型言語の理論的基盤 ここでは型無しλ計算を紹介します 型付きもあるんだよ
λࣜ 変数 a, b, c, ..., x, y, z, ...
λ抽象 λx.x, λx.λy.(x y), ... 関数適用 (f x)
λࣜ λx.λy.* は λx y.* と略記する 関数適用の括弧は曖昧でない場合は 省略する x y
= (x y) 関数適用は左結合 f x y = ((f x) y)
α-ม λ抽象の束縛変数名は重要ではない 例えば λx.x = λy.y 束縛変数名を別の名前に置き換える 操作をα-変換と呼ぶ α-変換で同じλ式にできるなら等価
β-؆ 要はただの関数適用の評価 λ抽象内部の束縛変数を全て引数で 置き換える 例えば (λx.f x) y = f
y β-簡約で同じλ式にできるなら等価
η-ม どんな引数に対しても同じ結果にな るならば、それらは同じといっても いいよね (外延的等価性) 例えば f = λx.f x
これらの間の変換をη-変換と呼ぶ η-変換で同じλ式にできるなら等価
Quiz 1. λx.x y = λy.y y ? 2. (λx.λx.x
y) y = λy.y y ? 3. λx.x = (λx y z.x z (y z)) (λx y.x) (λx y.x) ?
Answer 1. No 2. No 3. Yes
λܭࢉ λ式と変換・簡約の規則をまとめて λ計算と呼ぶ λ計算はチューリング完全 どんな手続き (プログラム) もλ式 で表現できる
Q. Ͳ͏ܭࢉ͢Δͷ 入力 x が与えられるとする 手続きを表すλ式 p をうまく選べば、 例えば y
= p x で出力が得られる y を変換・簡約すれば解読できそう
Q. ͱ͔Ͳ͏͢Δͷ 数値がなければ、λ式を使えばいい じゃない 真理値がなければ、λ式を使えば リストがなければ、λ式を
Church λ式で自然数を表わすひとつの方法
Church 0 := λf x.x 1 := λf x.f x
2 := λf x.f (f x) ...
Church 次の自然数を求める関数 Succ Succ := λn f x.f (n f
x) 足し算 Add Add := λa b f x.a f (b f x) 掛け算はどうなるか考えてみよう
Church 掛け算 Mul Mul := λa b f x.a (b
f) x
Church 前の自然数を求める関数 Pred Pred := λn f x. n (λg
h.h (g f)) (λy.x) (λy.y) ただし Pred 0 = 0 キリがないのでこれ以上はやめる
Churchਅཧ True := λx y.x False := λx y.y If
:= λp x y.p x y = λp.p
Churchਅཧ AND, OR, NOT And := λp q.p q False
Or := λp q.p True q Not := λp.p False True
ड़ޠͷྫ Church数 n が 0 かどうか調べる 0 = λf x.x
だった IsZero := λn. n (λx.False) True だんだんとプログラムが書ける気が してきませんか?
Churchର リストや木構造は対 (pair) の連鎖 で表現できる [1, 2, 3] = (1,
(2, (3, 空))) 対をλ式で表現できればいいよね
Churchର 対をつくる関数 Cons Cons := λx y c.c x y
かんたん!べんり!
Churchର 対の前後を取り出す関数 Car, Cdr Car := λp.p (λx y.x) Cdr
:= λp.p (λx y.y)
Churchର 空 (リストの終端) は? 好きなものを使えば良い False が一般的っぽい?
Quiz 入力 x が 2 つのChurch数 a, b の Church対で与えられる
出力 y = p x が、a = 0 なら y = b、 それ以外なら y = a * b となる p を書いてみよう Succ などこれまでに定義したものは 使ってもよい
Answer 例: λx.IsZero (Car x) (Cdr x) (Mul (Car x)
(Cdr x))
܁Γฦ͠ॲཧ 繰り返し処理を関数で表現したい時 は、再帰的な関数を書けばいい f(0) = 1, f(n) = n *
f(n - 1) けれどλ計算では"再帰的な定義"が できないので、単純には書けない
ؔͷෆಈ 関数 f に対して、f x = x となる ような x
を f の不動点と呼ぶ
Fix 関数 f を引数にとり、その不動点を 返す関数 Fix が存在したとする Fix f =
f (Fix f) f = λx n. IsZero n True (x (Pred n)) Fix f n は n 回の空ループになる
Fix Fix があれば、繰り返し処理を表現 することが出来る このような関数 Fix をなんとかλ式 だけで表現できないか?
Fix できる! Fix := λf.(λx.f (x x)) (λx.f (x x))
実際に Fix f = f (Fix f) となるか 確かめてみるとよいです
λܭࢉͷ·ͱΊ λ計算は、計算を関数とその適用で モデル化したもの チューリング完全 数値も真理値もリストもλ式で表現 できる 繰り返し処理だってできちゃう
SKIίϯϏωʔλೖ
ίϯϏωʔλܭࢉͱ ! 高階関数 (コンビネータ) を用いて計算 を行う λ計算と同じく、簡約が存在 (P x y
z ...) = E 簡約の結果 E は、コンビネータ P の 定義による
ίϯϏωʔλͷྫ B x y z = x (y z) C
x y z = x z y W x y = x y y
ίϯϏωʔλͷྫ S x y z = x z (y z)
K x y = x I x = x 実は I = S K K とも書ける
SKIίϯϏωʔλܭࢉ S、K、I の 3 つのコンビネータを、 "基底"として用いる 他のコンビネータは S、K、I の組み 合わせで表現する
スキーとは関係がない
SKI ͰԿ͕Ͱ͖Δ͔ SKIコンビネータ計算はチューリング 完全 λ抽象と相互に変換することができる SKI→λ は自明 λ→SKI については Wikipedia
の 「コンビネータ論理」のページを 見るとよいかも
SKI ͰChurch 0 := KI 1 := I 2 :=
S(S(KS)K)I ... Succ := S(S(KS)K)
SKI ͰChurchਅཧ True := K False := KI If :=
I
SKI ͰChurchର Cons := S(S(KS)(S(KK)(S(KS) (S(K(SI))K))))(KK) 笑っちゃうよね
SKI ͰFix (Y) Fix よりも、不動点コンビネータ Y と呼ぶことが多い (きがする) Y :=
SSK(S(K(SS(S(SSK))))K)
Quiz Church数の掛け算、足し算を SKI で 書いてみよう 足し算の方が難しくなるはず
Answer Mul = S(KS)K Add = S(KS)(S(K(S(KS))) (S(KK)))
SKI ͷ·ͱΊ S, K, I という 3 つのコンビネータ と適用だけで計算をする チューリング完全
λ抽象と相互に変換できる データも表せるし、繰り返し処理も できる
ͩΜͩΜࣗͷ SKI ྗ͕ͲΕ΄Ͳͷͷ͔ ͔֬Ίͨ͘ͳ͖ͬͯ·ͨ͠ΑͶʁ
Lazy K
͜͜Ζ Նᕸੴ
lਫ਼ਆతʹ্৺ͷͳ͍ͷഅࣛͩz
lਫ਼ਆతʹ্৺ͷͳ͍ͷഅࣛͩz Eager K
Lazy K ͱ SKIコンビネータ計算をベースにした 言語 遅延評価、故に Lazy 対義語: Eager, Strict
こころの K とは関係がない
ԆධՁ 結果に必要のない部分を評価 (計算) しないための仕組み 例えば K x y = x
の y は必要ない ので、評価を省略したい
ԆධՁ ほとんどのプログラミング言語では、 引数は適用の前に評価される Lazy K では、引数はそれ自身が関数 として適用に使われるまで評価が遅延 される (使わなければ評価されない) これによって、Yコンビネータによる
停止するループや、無限の長さをもつ リストが実現できる
ೖྗ 入力は文字コードをChurch数で表現 したものの、Church対によるリスト で与えられる 入力の終端はChurch数 256 256 = SII(SII(S(S(KS)K)I)) ただし"リストの終端"ではない
ग़ྗ 入力 X とプログラム P に対して、 出力は Y = P
X 出力も文字コードをChurch数で表現 したものの、Church対によるリスト 出力の終端も 256 以上のChurch数
ه๏ Lazy K には 4 つの記法がある コンビネータ計算 …… S(KI)I unlambda
…… ``s`kii Iota …… * と i だけ Jot …… 0 と 1 だけ
ه๏ ͦͷଞ 空白、改行は無視される # の後は改行までコメント 空ファイルは I
Lazy K ॲཧܥ http://esoteric.sange.fi/essie2/ download/lazy-k.zip Windows 用のバイナリ同梱 GCC でコンパイルするときは lazy.cpp
にパッチを当てる https://gist.github.com/ susisu/831e06af2ddee14938c8
Lazy K ॲཧܥ 実行はファイルから、または -e で 直接プログラムを指定 $ lazy <file>
$ lazy -e <program>
Lazy K ॲཧܥ ためしになにか動かしてみる $ lazy eg/calc.lazy $ lazy -e
SKK 中身を見るともっとたのしい SKI を組み合わせて、君だけの最強 プログラムを作ろう!
Lazy K ͷҋਂ͍
ࢀߟจݙ 大体 Wikipedia を読めばいいと思う ラムダ計算 コンビネータ論理 SKIコンビネータ計算 不動点コンビネータ
ࢀߟจݙ The Lazy K Programming Language https://tromp.github.io/cl/lazy- k.html ↑の日本語訳 http://legacy.e.tir.jp/wiliki?%CB
%DD%CC%F5%3A%A5%D7%A5%ED %A5%B0%A5%E9%A5%DF %A5%F3%A5%B0%B8%C0%B8%ECLazy_K