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
PPL2016-9-3
Search
Kyoko KADOWAKI
March 08, 2016
Science
650
0
Share
Embed
Copy iframe code
Copy JS code
Copy link
Start on current slide
PPL2016-9-3
Agda による定式化された型推論器の拡張と改良
Kyoko KADOWAKI
March 08, 2016
Other Decks in Science
See All in Science
Tensor Factorization Meets Deformed Information Geometry: Convex Relaxation under Deformed Algebra
gkazunii
0
130
Physical AIを支えるWeights & Biases
olachinkei
1
530
第67回コンピュータビジョン勉強会論文紹介「RoboWheel: A Data Engine from Real-World Human Demonstrations for Cross-Embodiment Robotic Learning」
x_ttyszk
0
160
Van Dare naar Durf
voginip
0
290
機械学習 - DBSCAN
trycycle
PRO
0
2k
20260820_アウトカムが二値のデータに対するCausal Impact@LINEヤフー Data Science Share #2 / Causal Impact for Binary Outcomes
brainpadpr
2
820
AIを用いた PID制御で部屋 の温度制御をしてみた
nearme_tech
PRO
0
230
共生概念の整理と AIアライメントの構想
hiroakihamada
0
260
AIPシンポジウム 2025年度 成果報告会 「因果推論チーム」
sshimizu2006
3
600
チュートリアル:世界モデル
hf149
0
2.1k
ハミルトン・ヤコビ方程式の解の性質と物理的意味
enakai00
0
870
Sstニューロンによる睡眠不足と回復の制御:データ駆動型トランスクリプトーム解析
tagtag
PRO
0
120
Featured
See All Featured
Avoiding the “Bad Training, Faster” Trap in the Age of AI
tmiket
0
210
WENDY [Excerpt]
tessaabrams
11
39k
Easily Structure & Communicate Ideas using Wireframe
afnizarnur
194
17k
I Don’t Have Time: Getting Over the Fear to Launch Your Podcast
jcasabona
35
2.8k
CSS Pre-Processors: Stylus, Less & Sass
bermonpainter
360
30k
We Have a Design System, Now What?
morganepeng
55
8.3k
Are puppies a ranking factor?
jonoalderson
2
3.8k
Agile Leadership in an Agile Organization
kimpetersen
PRO
0
210
Prompt Engineering for Job Search
mfonobong
0
420
Thoughts on Productivity
jonyablonski
76
5.3k
Helping Users Find Their Own Way: Creating Modern Search Experiences
danielanewman
31
3.3k
Building Adaptive Systems
keathley
44
3.2k
Transcript
Agda ʹΑΔఆࣜԽ͞Εͨܕਪ ثͷ֦ுͱվྑ ͓ͷਫঁࢠେֶɹ߳ࢠɹઙҪ݈Ұ
1͡Ίʹ •ݚڀ֓ཁ •ݚڀഎܠ •ຊݚڀͷߩݙ •ൃදͷྲྀΕ
ݚڀ֓ཁ w"HEBΛ༻͍ͯɺఆࣜԽ͞ΕͨܕਪثʹHFOFSJD QSPHSBNNJOHෆ੍ࣜͳͲͷςΫχοΫΛ༻ ͍ͯɺ࣮Λ؆໌ʹ͠ɺߏจͷ֦ுΛ؆୯ʹͨ͠ wHFOFSJDQSPHSBNNJOH wෆ੍ࣜ
Agda ʹ͍ͭͯ wґଘܕΛ༻͍Δ͜ͱͷͰ͖Δɺఆཧূ໌ࢧԉγες Ϝ͓Αͼϓϩάϥϛϯάݴޠ w)BTLFMMͳͲʹจ๏͕ࣅ͍ͯΔ
ґଘܕ(Dependent Types) wʹґଘ͢ΔܕΛͭ͘Δ͜ͱ͕Ͱ͖Δܕ wྫ7FDOܕ OJOUܕͷ ͕͞OͷϕΫτϧΛ ܕͷϨϕϧͰ දݱ͍ͯ͠Δ wྫ͑ɺ0$BNMͷϦετͰ͕͞ܕϨϕϧͰࢦ
ఆͰ͖ͳ͍ MFOHUIؔͳͲͰऔΓग़͢͜ͱ͕ඞཁ
ఆࣜԽ ೖྗʢܕແ͠ݴޠʣ ग़ྗʢܕ͖ݴޠʣ ܕਪ n = 1 let f x
= match x with 0 -> “zero” | _ -> “not zero” n : int n = 1 f : int -> string f x = match x with …
ܕ ఆࣜԽ ೖྗʢܕແ͠ݴޠʣ ग़ྗʢܕ͖ݴޠʣ ܕਪ n : int f :
int -> string
ܕ ఆࣜԽ ೖྗʢܕແ͠ݴޠʣ ग़ྗʢܕ͖ݴޠʣ ܕਪ n : int f :
int -> string ݕূػߏ νΣοΫ ᶃ
ఆࣜԽ ೖྗʢܕແ͠ݴޠʣ ग़ྗʢܕ͖ݴޠʣ ܕਪ ܕΛফڈ ܕແ͠ݴޠ ಉ͡Ͱ͋Δ͜ͱΛอূ͢Δ
ݚڀഎܠ wܕਪΛ͢ΔʹVOJpDBUJPOͷػߏ͕ඞཁ͕ͩɺ ී௨ʹ࣮͢Δͱมͷॻ͖͑ͳͲ͕ඞཁͰɺ "HEBͰͰ͖ͳ͍ wͦ͜Ͱ.D#SJEFܕมͷΛົʹཧ͢Δܗ ͰVOJpDBUJPOͷػߏΛQVSFGVODUJPOBMʹ࣮ݱͨ͠ w͜ΕʹΑΓɺ"HEBͰܕਪثΛͭ͘Δ͕ग़དྷ ͨ
ຊݚڀͷߩݙ w.D#SJEF͕ࣔͨ͠VOJpDBUJPOͷػߏ<.D#SJEF >Λ֦ு͠ɺ୯ ҰԽͰ͖͍ͯΔূ໌ฦ͢ܗͰఆࣜԽͨ͠ʢ11-ʣ w͜ͷVOJpDBUJPOͷػߏΛͱʹͯ͠ɺ"HEBͰఆࣜԽ͞Εͨܕਪث Λ࣮ͨ͠ʢ11-ʣ w͜ͷܕਪثʹෆ੍ࣜΛಋೖ͢Δ͜ͱͰܕมΛࢦఆ͢Δͷ Έͷ࣮ΑΓ؆୯ʹ࣮͢Δํ๏Λࣔ͠ɺͦΕΛܕنଇͷܗͰఆ ࣜԽͨ͠ wVOJpDBUJPOͷػߏΛHFOFSJDQSPHSBNNJOHʹΑΓҙͷܕʹ
֦ு͠ɺܕͷ֦ுΛ؆୯ʹͨ͠ wܕਪͷ݁ՌɺಘΒΕͨܕ͖߲͔ΒܕΛऔΓআ͘ͱݩͷ߲͕ಘ ΒΕΔ͜ͱূ໌ͨ͠ wܕਪͷ֦ுͷྫͱͯ͠ɺΛಋೖͨ͠
ࠓͷίϯςϯπ ͡Ίʹ VOJpDBUJPO ܕఆٛ HFOFSJDQSPHSBNNJOHͱෆ੍ࣜ ܕਪ ·ͱΊ
2 unification •McBrideʹΑΔख๏ •unificationͷఆࣜԽ
McBride ʹΑΔ unification ͷػߏ McBrideɺܕมΛ༗ݶू߹Ͱදݱ͢Δख๏Ͱఀࢭੑ͕໌ Β͔ͳ unificationΛ࣮ݱͨ͠ ܕН B B
B N ܕมͷू߹ ࠷େͰNݸ ༗ݶू߹ pOJUFTFU N
McBride ʹΑΔ unification ͷػߏ ܕН B JOU B
N N ܕมೖʹΑΓ۩ମԽʢ۩ମతͳܕʹͳΔʣՄೳੑ͕͋Δ
ܕUBˠ BˠB B B B ܕUBˠ BˠJOU B
JOU B
ܕUBˠ BˠB B B B ܕUBˠ BˠJOU B
JOU B VOJpDBUJPO BJOU B JOU B
ܕUBˠ BˠB B B B ܕUBˠ BˠJOU B
JOU B VOJpDBUJPO BJOU B JOU B ❌ ۩ମԽ͞ΕͨܕΛू߹͔Βআ
ܕUBˠ BˠB B B B ܕUBˠ BˠJOU B
JOU B VOJpDBUJPO BJOU B B Bˠ BˠJOU ܕมͷ͕͔֬ʹݮ͍ͬͯΔ
ܕUBˠ BˠB B B B ܕUBˠ BˠJOU B
JOU B VOJpDBUJPO BJOU B B Bˠ BˠJOU ܕมͷ͕͔֬ʹݮ͍ͬͯΔ ܕม͕۩ମԽ͞ΕΔͨͼʹɺ۩ମԽ͞Ε͍ͯͳ͍ܕมͷ ͕ͻͱͭݮΔ
ܕUBˠ BˠB B B B ܕUBˠ BˠJOU B
JOU B VOJpDBUJPO BJOU B B Bˠ BˠJOU ܕมͷ͕͔֬ʹݮ͍ͬͯΔ ܕม͕۩ମԽ͞ΕΔͨͼʹɺ۩ମԽ͞Ε͍ͯͳ͍ܕมͷ ͕ͻͱͭݮΔ ఀࢭੑ͕໌Β͔
unificationͷఆࣜԽ wઌ΄Ͳࣔͨ͠ख๏ͰɺVOJpDBUJPOΛ"HEB্Ͱ࣮Ͱ͖ͨ wܕਪثΛఆࣜԽ͢Δʹz͔֬ʹVOJGZ͞Ε͍ͯΔzূ໌ Λฦ͢͜ͱඞཁ ɹࣜʹ͢ΔͱTVCTUМUTVCTUМU ʮೖͨ͠ޙͷܕ͕͔֬ʹಉҰʯ wVOJpDBUJPOͷؔΛ֦ுͯ͠ɺ͜ͷূ໌Λฦ͢Α͏ʹ͠ ͨʢ11-ʣ
3 ܕఆٛ •ܕɺܕஅɺ߲ •ຊݚڀʹ͓͚Δಛघͳදݱ
ܕఆٛ ߲
ܕఆٛ ߲ N൪ͷܕม ؔܕ
ܕఆٛ ߲ ม ϥϜμந ؔద༻
ܕஅ ਪنଇ
ܕஅ ਪنଇ ʮܕڥϵͷͱͰɺ߲.ͷܕНʹͳΔʯ
ܕஅ ਪنଇ
ܕਪͷಛघͳදݱ ܕΛܭࢉͯ͠ग़ྗ͢ΔͨΊͷنଇ
ܕਪͷಛघͳදݱ ೖྗ ग़ྗ
ܕਪͷಛघͳදݱ ᶃ߲.ͱ ܕมΛ࠷େͰNݸͭܕڥϵ͕ೖྗ͞ΕΔ
ܕਪͷಛघͳදݱ ᶄ৽͍͠ܕม͕ܕਪதʹN``NݸׂΓͯΒΕΔ
ܕਪͷಛघͳදݱ ᶅܕมͷΛN`ݸ·ͰݮΒ͢ೖ͕ಘΒΕΔ
ܕਪͷಛघͳදݱ ᶇܕมͷ͕N`·ͰݮͬͨܕН͕ฦͬͯ͘Δ
unification ͷಛघͳදݱ ܕНͱНΛಉ͡ʹ͢Δ VOJGZ͢Δ ೖМΛಘΔ
unification ͷಛघͳදݱ ೖྗ ग़ྗ
unification ͷಛघͳදݱ ܕมΛ࠷େͰN``ݸ࣋ͭܕН ͱН ܕมΛN``ݸ͔ΒN`ݸ·ͰݮΒ͢ೖМʹΑͬͯ VOJpDBUJPO ୯ҰԽ ͞ΕΔ
4 generic programmingͱ ෆ੍ࣜ •generic programming •ෆ੍ࣜ
generic programming wී௨ܕΛίϯετϥΫλͰఆٛ͢Δ w͜ͷ߹ɺܕΛૢ࡞͢Δؔʹ͓͍ͯɺܕΛ࠶࣮͢Δͨ ͼʹύλʔϯϚονΛ࠶࣮͢Δඞཁ͕͋Δ wܕΛHFOFSJDʹੜ͢Δ͜ͱͰɺύλʔϯϚονͷ࠶࣮ Λආ͚ɺϢʔβ͕ࢦఆͨ͠ҙͷܕΛ࠶࣮ͳ͘ਪͰ͖ ΔΑ͏ʹͳΔ wຊݚڀͰɺ3FHVMBS</PPSUΒ >ΛݩʹHFOFSJDͳ
ܕΛ࣮ͨ͠
generic programming ͷߏจ $POT 'TU 4OE Λ૿͍ͨ͠ͱ͖ɺ ੵܕΛՃ͢Δඞཁ͕༗Δ
generic programming ͜ͷΑ͏ʹܕΛ૿ͯ͠ɺ VOJpDBUJPOܕʹؔ͢Δิͷ࣮Λมߋ͢Δඞཁ͕ͳ͍
generic programming ߏจΛ૿͢ͱ͖ɺ ߏจͦͷͷͷܕਪʹूதͰ͖Δ
generic programming ܕΛ#/'ͷΑ͏ͳܗͰදݱ͢Δ
generic programming ܕΛ#/'ͷΑ͏ͳܗͰදݱ͢Δ
generic programming ܕΛ#/'ͷΑ͏ͳܗͰදݱ͢Δ
generic programming ܕΛ#/'ͷΑ͏ͳܗͰදݱ͢Δ
generic programming ܕΛ#/'ͷΑ͏ͳܗͰදݱ͢Δ
generic programming ܕΛ#/'ͷΑ͏ͳܗͰදݱ͢Δ ͜ΕͰɺܕͷදݱ͕Ͱ͖ͨ
generic programming ۩ମతͳܕͷදݱ
generic programming දݱͷҙຯΛ༩͍͑ͯΔ
generic programming ࣗࣗΛ༩͑Δ͜ͱͰ࠶ؼ͢Δ
generic programming ࠶ؼΛด͡ΔͨΊͷܕ
generic programming ࠶ؼΛด͡ΔͨΊͷܕ
generic programming ࠶ؼΛด͡ΔͨΊͷܕ
generic programming ҙʹେ͖͍ܕΛදݱͰ͖Δ
ෆ੍ࣜ ܕਪΛ࣮͢ΔࡍɺҎલN``ΛݫີʹܕʹΈ ࠐΜͰ͍ͨ
ෆ੍ࣜ ͨͱ͑-BNTΛܕਪ͢Δͱ͖ N``/BU N``DPVOUT ϵ`$YUN`` ϵʜ
ෆ੍ࣜ ͨͱ͑-BNTΛܕਪ͢Δͱ͖ N``JOU N``DPVOUT ϵ`$YUN`` ϵʜ ܕͷϨϕϧͰܕΛ߹Θͤͯূ໌͠ͳ͍ͱ͍͚ͳ͘ͳΔ
ෆ੍ࣜ N``N≤N`Λຬ͍ͨͯ͠ΕΑ͘ɺ۩ମతͳ Ҏޙ࣋ͪา͘ඞཁ͕ͳ͍ ΘΓʹN≤N``ͱ͍͏ূ໌Λ࣋ͪา͘
5 ܕਪ • ؔఆٛ • ܕਪͷྫ - ؔద༻ -
ؔఆٛ ೖྗ TNݸͷܕมΛͭXFMMTDPQFEUFSN ϵܕڥ ग़ྗ N⒌⒌ N⒌ࣗવ N≤N⒌⒌N≤N⒌⒌Ͱ͋Δ͜ͱͷূ໌ МN⒌⒌ݸͷܕมΛ࣋ͭܕΛN⒌ݸͷܕมΛ࣋ͭܕʹ͢Δೖ Нਪ݁Ռͷܕ
Xਪ͞ΕͨXFMMUZQFEUFSNɻܕมΛN⒌ݸͭ FSBTFX㲇Tฦ͞ΕͨXFMMUZQFEUFSNT͔ΒܕใΛআͨ͠ͷ͕ɺ ͱͷXFMMTDPQFEUFSNͱ͍͠ͱ͍͏ূ໌ JOGFS
ؔఆٛ ೖྗ TNݸͷܕมΛͭXFMMTDPQFEUFSN ϵܕڥ .BZCF ग़ྗ N⒌⒌ N⒌ࣗવ N≤N⒌⒌N≤N⒌⒌Ͱ͋Δ͜ͱͷূ໌ МN⒌⒌ݸͷܕมΛ࣋ͭܕΛN⒌ݸͷܕมΛ࣋ͭܕʹ͢Δೖ
Нਪ݁Ռͷܕ Xਪ͞ΕͨXFMMUZQFEUFSNɻܕมΛN⒌ݸͭ FSBTFX㲇Tฦ͞ΕͨXFMMUZQFEUFSNT͔ΒܕใΛআͨ͠ͷ͕ɺ ͱͷXFMMTDPQFEUFSNͱ͍͠ͱ͍͏ূ໌ JOGFS
ؔఆٛ ೖྗ TNݸͷܕมΛͭXFMMTDPQFEUFSN ϵܕڥ .BZCF ग़ྗ N⒌⒌ N⒌ࣗવ N≤N⒌⒌N≤N⒌⒌Ͱ͋Δ͜ͱͷূ໌ МN⒌⒌ݸͷܕมΛ࣋ͭܕΛN⒌ݸͷܕมΛ࣋ͭܕʹ͢Δೖ
Нਪ݁Ռͷܕ Xਪ͞ΕͨXFMMUZQFEUFSNɻܕมΛN⒌ݸͭ FSBTFX㲇Tฦ͞ΕͨXFMMUZQFEUFSNT͔ΒܕใΛআͨ͠ͷ͕ɺ ͱͷXFMMTDPQFEUFSNͱ͍͠ͱ͍͏ূ໌ JOGFS OPUIJOH͕ฦΔܕΤϥʔͰ͋Δ
ؔఆٛ ίʔυͰ͜ͷΑ͏ʹͳΔʢࢀߟʣ
ܕਪͷྫ (App) "QQTTͷܕਪ TΛܕਪ͠ɺМͱНΛಘΔ ϵʹМΛࢪ্ͨ͠ͰTΛܕਪ͠ɺМͱНΛಘΔ ННˠЌ Ќ৽͍͠ܕม ͱͳΔΑ͏VOJGZ͠ ޭͨ͠ΒМΛಘΔ
ฦ͞ΕΔܕЌͱͳΔ
ܕਪͷྫ (App) "QQTTͷܕਪ TΛܕਪ͠ɺМͱНΛಘΔ ϵʹМΛࢪ্ͨ͠ͰTΛܕਪ͠ɺМͱНΛಘΔ ННˠЌ Ќ৽͍͠ܕม ͱͳΔΑ͏VOJGZ͠ ޭͨ͠ΒМΛಘΔ
ฦ͞ΕΔܕЌͱͳΔ
ܕਪͷྫ (App) "QQTTͷܕਪ TΛܕਪ͠ɺМͱНΛಘΔ ϵʹМΛࢪ্ͨ͠ͰTΛܕਪ͠ɺМͱНΛಘΔ ННˠЌ Ќ৽͍͠ܕม ͱͳΔΑ͏VOJGZ͠ ޭͨ͠ΒМΛಘΔ
ฦ͞ΕΔܕЌͱͳΔ
ܕਪͷྫ (App) "QQTTͷܕਪ TΛܕਪ͠ɺМͱНΛಘΔ ϵʹМΛࢪ্ͨ͠ͰTΛܕਪ͠ɺМͱНΛಘΔ ННˠЌ Ќ৽͍͠ܕม ͱͳΔΑ͏VOJGZ͠ ޭͨ͠ΒМΛಘΔ
ฦ͞ΕΔܕЌͱͳΔ
ܕਪͷྫ (App) TΛܕਪ͠ɺМͱНΛಘΔɻ ϵʹМΛࢪ্ͨ͠ͰTΛܕਪ͠ɺМͱНΛಘΔɻ
ܕਪͷྫ (App) TΛܕਪ͠ɺМͱНΛಘΔɻ ϵʹМΛࢪ্ͨ͠ͰTΛܕਪ͠ɺМͱНΛಘΔɻ
ܕਪͷྫ (App) TΛܕਪ͠ɺМͱНΛಘΔɻ ϵʹМΛࢪ্ͨ͠ͰTΛܕਪ͠ɺМͱНΛಘΔɻ
ܕਪͷྫ (App) ϵʹМΛࢪ্ͨ͠ͰTΛܕਪ͠ɺМͱНΛಘΔɻ ННˠЌ Ќ৽͍͠ܕม ͱͳΔΑ͏VOJGZ͠
ܕਪͷྫ (App) ϵʹМΛࢪ্ͨ͠ͰTΛܕਪ͠ɺМͱНΛಘΔɻ ННˠЌɹɹɹɹͱͳΔΑ͏VOJGZ͠ N`൪ͷܕมΛ৽͘͠औΓग़͢
ܕਪͷྫ (App) ННˠЌɹɹɹɹͱͳΔΑ͏VOJGZ͠ ޭͨ͠ΒМΛಘΔ
ܕਪͷྫ (App) ННˠЌɹɹɹɹͱͳΔΑ͏VOJGZ͠ ޭͨ͠ΒМΛಘΔ
ܕਪͷྫ (App) "QQͷܕنଇΛద༻͢Δɻ
"QQͷܕنଇΛద༻͢Δɻ
ܕਪͷྫ (App) "QQͷܕنଇΛద༻͢Δɻ ඞཁͳೖ
ܕਪͷྫ (App) "QQͷܕنଇΛద༻͢Δɻ ͳΔೖМΛฦ͍ͨ͠
ܕਪͷྫ (App) "QQͷܕنଇΛద༻͢Δɻ ͳΔೖМΛฦ͍ͨ͠
ܕਪͷྫ (App)
ܕਪͷྫ (App) ଞͷߏจ 'TU 4OEͳͲ ʹؔͯ͠ಉ༷ʹূ໌Ͱ͖Δ
·ͱΊ wܕมΛͰͳ͘ෆࣜΛ༻͍ͯදݱ͢Δํࣜʹ վྑ͠ɺ·ͨܕఆٛΛHFOFSJDQSPHSBNNJOHͷߟ ͑ํΛऔΓೖΕͯΑΓҰൠతʹվྑ͢Δ͜ͱͰɺܕ ਪثʹ͓͚ΔTZOUBYͷ֦ுͱূ໌ͷ؆ུԽΛ࣮ ݱͨ͠ wιʔείʔυHJUIVCDPNLEYVJOGFSBHEB "HEB߹ܭߦ
ࠓޙͷ՝ wߏจͷ֦ு ଟ૬ͷ-FUจͳͲ 1PMZ1<+BOTTPOΒ >*OEFYFE'VODUPST<-ÖIΒ >ͳͲܕύϥϝλΛѻ͑ΔͷΛ͏ඞཁ͕͋Δ wશੑͷূ໌ ܕ͕͔ͭͳ͍߹