Mercurial > hg > Members > atton > seminar_slides

comparison slides/20140415/slide.md @ 38:1fde03546bbc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add slide for seminar
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 15 Apr 2014 17:55:37 +0900
parents
children
comparison
equal deleted inserted replaced
37:c7d57cf16fdb 38:1fde03546bbc
1 title: プログラムのデバッグ支援(仮)
2 author: Yasutaka Higa
3 cover:
4 lang: Japanese
5
6
7 # 研究目的(仮)
8
9 * プログラムのデバッグは複雑になることがある
10 * 例えば、あるif文の条件を満たすには、必要な状態がある
11 * そういった状態を自動で導出したい
12 * model checking を使えばいける?
13
14 # 近況報告
15
16 * 印鑑ください
17 * System F on Agda
18 * List に手を出しました
19
20 # List on Agda
21
22 * List : X -> (U -> X -> X) -> X
23 * nil : List U
24 * nil = \x -> \y -> x
25 * cons : U -> List U -> List U
26 * cons u t = \x -> \y -> y u (t x y)
27
28 # 例としては
29
30 * u1,u2 : U
31 * cons u1 (cons u2 nil)
32 * X な x と (U -> X -> X) な f を渡すと
33 * f u1 (f u2 x)
34
35 # つまづいているところ
36
37 * t に nil と cons を渡せば t になる、というやつ
38 * U と List U を It するためにlevel は2つ
39 * でも合わない
40
41 <!-- vim: set filetype=markdown.slide: -->