Mercurial > hg > Papers > 2017 > ryokka-midterm

changeset 5:8f91a416343d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix midterm.tex, remove aux,dvi,etc
author ryokka
date Thu, 26 Oct 2017 14:35:55 +0900
parents 0a6686180a13
children 3be2444dacc5
files midterm/midterm.aux midterm/midterm.bbl midterm/midterm.blg midterm/midterm.dvi midterm/midterm.fdb_latexmk midterm/midterm.fls midterm/midterm.log midterm/midterm.pdf midterm/midterm.tex
diffstat 9 files changed, 77 insertions(+), 515 deletions(-) [+]
line wrap: on
line diff
--- a/midterm/midterm.aux	Thu Oct 26 14:21:59 2017 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,24 +0,0 @@
-\relax 
-\citation{Yasutaka:2016}
-\citation{agda}
-\@writefile{toc}{\contentsline {section}{\numberline {1}研究目的}{1}}
-\@writefile{toc}{\contentsline {section}{\numberline {2}Countinuation based C (CbC)}{1}}
-\@writefile{toc}{\contentsline {section}{\numberline {3}Agda}{1}}
-\@writefile{lof}{\contentsline {figure}{\numberline {1}{\ignorespaces 自然演繹での三段論法の証明}}{1}}
-\newlabel{fig:modus-ponens}{{1}{1}}
-\citation{*}
-\bibstyle{junsrt}
-\bibdata{reference}
-\bibcite{Yasutaka:2016}{1}
-\bibcite{agda}{2}
-\bibcite{Tatsuki:2016}{3}
-\bibcite{kaito:2015}{4}
-\bibcite{agda-documentation}{5}
-\newlabel{src:singlelinked}{{1}{2}}
-\@writefile{lol}{\contentsline {lstlisting}{\numberline {1}CbCによるStack}{2}}
-\newlabel{src:stack-agda}{{2}{2}}
-\@writefile{lol}{\contentsline {lstlisting}{\numberline {2}AgdaによるStack}{2}}
-\@writefile{toc}{\contentsline {section}{\numberline {4}RedBlackTree}{2}}
-\@writefile{lof}{\contentsline {figure}{\numberline {2}{\ignorespaces RedBlackTreeの例}}{2}}
-\newlabel{fig:rbtree}{{2}{2}}
-\@writefile{toc}{\contentsline {section}{\numberline {5}今後の課題}{2}}
--- a/midterm/midterm.bbl	Thu Oct 26 14:21:59 2017 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-\begin{thebibliography}{1}
-
-\bibitem{Yasutaka:2016}
-{比嘉 健太, 河野 真治}.
-\newblock {メタ計算を用いた Continuation based C の検証手法}, 2016.
-
-\bibitem{agda}
-The agda wiki.
-\newblock \url{http://wiki.portal.chalmers.se/agda/pmwiki.php}.
-\newblock Accessed: 2017/10/24(Tue).
-
-\bibitem{Tatsuki:2016}
-{伊波 立樹, 東恩納 琢偉, 河野 真治}.
-\newblock {Code Gear 、Data Gear に基づく OS のプロトタイプ}, 2016.
-
-\bibitem{kaito:2015}
-{徳森 海斗, 河野 真治}.
-\newblock {LLVM Clang 上の Continuation based C コンパイラ の改良}, 2015.
-
-\bibitem{agda-documentation}
-Welcome to agda’s documentation! ― agda 2.6.0 documentation.
-\newblock \url{http://agda.readthedocs.io/en/latest/index.html}.
-\newblock Accessed: 2017/10/24(Tue).
-
-\end{thebibliography}
--- a/midterm/midterm.blg	Thu Oct 26 14:21:59 2017 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,47 +0,0 @@
-This is pBibTeX, Version 0.99d-j0.33 (utf8.euc) (TeX Live 2016)
-Capacity: max_strings=35307, hash_size=35307, hash_prime=30011
-The top-level auxiliary file: midterm.aux
-The style file: junsrt.bst
-Database file #1: reference.bib
-You've used 5 entries,
-            2270 wiz_defined-function locations,
-            561 strings with 4741 characters,
-and the built_in function-call counts, 806 in all, are:
-= -- 44
-> -- 14
-< -- 0
-+ -- 8
-- -- 3
-* -- 5
-:= -- 87
-add.period$ -- 12
-call.type$ -- 5
-change.case$ -- 5
-chr.to.int$ -- 0
-cite$ -- 5
-duplicate$ -- 55
-empty$ -- 121
-format.name$ -- 6
-if$ -- 201
-int.to.chr$ -- 0
-int.to.str$ -- 5
-missing$ -- 0
-newline$ -- 25
-num.names$ -- 3
-pop$ -- 63
-preamble$ -- 1
-purify$ -- 0
-quote$ -- 0
-skip$ -- 47
-stack$ -- 0
-substring$ -- 0
-swap$ -- 5
-text.length$ -- 0
-text.prefix$ -- 0
-top$ -- 0
-type$ -- 0
-warning$ -- 0
-while$ -- 3
-width$ -- 6
-write$ -- 44
-is.kanji.str$ -- 33
Binary file midterm/midterm.dvi has changed
--- a/midterm/midterm.fdb_latexmk	Thu Oct 26 14:21:59 2017 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,55 +0,0 @@
-# Fdb version 3
-["bibtex midterm"] 0 "midterm.aux" "midterm.bbl" "midterm" 0
-  "junsrt.bst" 0 -1 0 ""
-  "midterm.aux" 1508332725 633 cb1069f0c006f1deecf5bae23f48fb04 ""
-  "midterm.bcf" 0 -1 0 ""
-  "reference.bib" 1508162081 342 e4f45eba33cb4afbbc5c44615e595cbc ""
-  (generated)
-  "midterm.bbl"
-["dvipdf"] 0 "midterm.dvi" "midterm.pdf" "midterm" 0
-  "midterm.dvi" 0 -1 0 "latex"
-  (generated)
-  "midterm.pdf"
-["latex"] 1508332725 "midterm.tex" "midterm.dvi" "midterm" 1508332725
-  "/usr/local/texlive/2016/texmf-dist/fonts/map/fontname/texfonts.map" 1272929888 3287 e6b82fe08f5336d4d5ebc73fb1152e87 ""
-  "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmbx12.tfm" 1136768653 1324 c910af8c371558dc20f2d7822f66fe64 ""
-  "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmmi12.tfm" 1136768653 1524 4414a8315f39513458b80dfc63bff03a ""
-  "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmmi6.tfm" 1136768653 1512 f21f83efb36853c0b70002322c1ab3ad ""
-  "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmmi8.tfm" 1136768653 1520 eccf95517727cb11801f4f1aee3a21b4 ""
-  "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmr12.tfm" 1136768653 1288 655e228510b4c2a1abe905c368440826 ""
-  "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmr17.tfm" 1136768653 1292 296a67155bdbfc32aa9c636f21e91433 ""
-  "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmr6.tfm" 1136768653 1300 b62933e007d01cfd073f79b963c01526 ""
-  "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmr8.tfm" 1136768653 1292 21c1c5bfeaebccffdb478fd231a0997d ""
-  "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm" 1136768653 1124 6c73e740cf17375f03eec0ee63599741 ""
-  "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmsy6.tfm" 1136768653 1116 933a60c408fc0a863a92debe84b2d294 ""
-  "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmsy8.tfm" 1136768653 1120 8b7d695260f3cff42e636090a8002094 ""
-  "/usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmtt10.tfm" 1136768653 768 1321e9409b4137d6fb428ac9dc956269 ""
-  "/usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisg-h.tfm" 1463242385 780 9d56a8f9483b0d090553358c515b7835 ""
-  "/usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisg-v.tfm" 1463242385 504 db18a8c0bf0b51f5d6237cc98872380d ""
-  "/usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisr-h.tfm" 1463242385 780 9d56a8f9483b0d090553358c515b7835 ""
-  "/usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisr-v.tfm" 1463242385 504 db18a8c0bf0b51f5d6237cc98872380d ""
-  "/usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/infwarerr.sty" 1463608860 8253 473e0e41f9adadb1977e8631b8f72ea6 ""
-  "/usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/ltxcmds.sty" 1463608860 18425 5b3c0c59d76fac78978b5558e83c1f36 ""
-  "/usr/local/texlive/2016/texmf-dist/tex/latex/abstract/abstract.sty" 1252025310 5128 640a4c0ff76b3e578a4c5482af27ec14 ""
-  "/usr/local/texlive/2016/texmf-dist/tex/latex/dvipdfmx-def/dvipdfmx.def" 1460062417 13436 2dcadf39017cb9d8459661645611b649 ""
-  "/usr/local/texlive/2016/texmf-dist/tex/latex/fancyhdr/fancyhdr.sty" 1160175134 20521 e5d13d98d57bd53d4fed3aa61bd29c86 ""
-  "/usr/local/texlive/2016/texmf-dist/tex/latex/graphics-cfg/graphics.cfg" 1459978653 3103 f32642b1cd56c010cdfb6545539b7f0b ""
-  "/usr/local/texlive/2016/texmf-dist/tex/latex/graphics/graphics.sty" 1462915952 14391 bd64a9e5d07473b936423b5f3280ed2c ""
-  "/usr/local/texlive/2016/texmf-dist/tex/latex/graphics/graphicx.sty" 1428932888 8125 557ab9f1bfa80d369fb45a914aa8a3b4 ""
-  "/usr/local/texlive/2016/texmf-dist/tex/latex/graphics/keyval.sty" 1428932888 2594 d18d5e19aa8239cf867fa670c556d2e9 ""
-  "/usr/local/texlive/2016/texmf-dist/tex/latex/graphics/trig.sty" 1454284088 3980 0a268fbfda01e381fa95821ab13b6aee ""
-  "/usr/local/texlive/2016/texmf-dist/tex/latex/url/url.sty" 1388531844 12796 8edb7d69a20b857904dd0ea757c14ec9 ""
-  "/usr/local/texlive/2016/texmf-dist/tex/platex/base/jarticle.cls" 1462837567 25231 a08460ff81096cb3e80d7be01474f985 ""
-  "/usr/local/texlive/2016/texmf-dist/tex/platex/base/jsize10.clo" 1462837567 9313 f538ec39b9e111bf9320856d312460b2 ""
-  "/usr/local/texlive/2016/texmf-dist/web2c/texmf.cnf" 1463093894 31953 b9489e6e586f798610c60aec1f5ec548 ""
-  "/usr/local/texlive/2016/texmf-var/web2c/euptex/uplatex.fmt" 1492015395 4047635 b3cd114470c56155cdcfdd945c0f085e ""
-  "/usr/local/texlive/2016/texmf.cnf" 1463979140 577 2938757e76f31531e65cc647e3507693 ""
-  "dummy.tex" 1508162081 2711 ebf4ee4460f50857f8ebbbf2d432d91e ""
-  "midterm.aux" 1508332725 8 a94a2480d3289e625eea47cd1b285758 ""
-  "midterm.bbl" 1508229470 270 0ff43ed253eb90c3e1f0aa4c2531e4d9 "bibtex midterm"
-  "midterm.tex" 1508332620 2829 be97b3f887631e620bc0f43b4aa0ae20 ""
-  "picins.sty" 1508162081 17807 916739e9c8f52c6a085688f05d1594e2 ""
-  (generated)
-  "midterm.aux"
-  "midterm.log"
-  "midterm.dvi"
--- a/midterm/midterm.fls	Thu Oct 26 14:21:59 2017 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-PWD /Users/ryokka/cr/ryokka-midterm/midterm
-INPUT /usr/local/texlive/2016/texmf.cnf
-INPUT /usr/local/texlive/2016/texmf-dist/web2c/texmf.cnf
-INPUT /usr/local/texlive/2016/texmf.cnf
-INPUT /usr/local/texlive/2016/texmf-var/web2c/euptex/uplatex.fmt
-INPUT midterm.tex
-OUTPUT midterm.log
-INPUT /usr/local/texlive/2016/texmf-dist/tex/platex/base/jarticle.cls
-INPUT /usr/local/texlive/2016/texmf-dist/tex/platex/base/jarticle.cls
-INPUT /usr/local/texlive/2016/texmf-dist/tex/platex/base/jsize10.clo
-INPUT /usr/local/texlive/2016/texmf-dist/tex/platex/base/jsize10.clo
-INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/graphics/graphicx.sty
-INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/graphics/graphicx.sty
-INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/graphics/keyval.sty
-INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/graphics/keyval.sty
-INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/graphics/graphics.sty
-INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/graphics/graphics.sty
-INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/graphics/trig.sty
-INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/graphics/trig.sty
-INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/graphics-cfg/graphics.cfg
-INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/graphics-cfg/graphics.cfg
-INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/dvipdfmx-def/dvipdfmx.def
-INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/dvipdfmx-def/dvipdfmx.def
-INPUT /usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/infwarerr.sty
-INPUT /usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/infwarerr.sty
-INPUT /usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/ltxcmds.sty
-INPUT /usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/ltxcmds.sty
-INPUT picins.sty
-INPUT picins.sty
-INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/fancyhdr/fancyhdr.sty
-INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/fancyhdr/fancyhdr.sty
-INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/abstract/abstract.sty
-INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/abstract/abstract.sty
-INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/url/url.sty
-INPUT /usr/local/texlive/2016/texmf-dist/tex/latex/url/url.sty
-INPUT dummy.tex
-INPUT dummy.tex
-INPUT midterm.aux
-INPUT midterm.aux
-OUTPUT midterm.aux
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/map/fontname/texfonts.map
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisr-v.tfm
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisr-h.tfm
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmr17.tfm
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmr12.tfm
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmr8.tfm
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmr6.tfm
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmmi12.tfm
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmmi8.tfm
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmmi6.tfm
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmsy10.tfm
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmsy8.tfm
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmsy6.tfm
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisr-v.tfm
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisr-h.tfm
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmr12.tfm
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisg-v.tfm
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/uptex-fonts/jis/upjisg-h.tfm
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmbx12.tfm
-INPUT midterm.bbl
-INPUT midterm.bbl
-INPUT /usr/local/texlive/2016/texmf-dist/fonts/tfm/public/cm/cmtt10.tfm
-OUTPUT midterm.dvi
-INPUT midterm.aux
--- a/midterm/midterm.log	Thu Oct 26 14:21:59 2017 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,262 +0,0 @@
-This is e-pTeX, Version 3.14159265-p3.7-160201-2.6 (utf8.euc) (TeX Live 2016) (preloaded format=platex 2017.4.13)  25 OCT 2017 17:25
-entering extended mode
- restricted \write18 enabled.
- %&-line parsing enabled.
-**midterm.tex
-(./midterm.tex
-pLaTeX2e <2016/05/07> (based on LaTeX2e <2016/03/31>)
-Babel <3.9r> and hyphenation patterns for 83 language(s) loaded.
-(/usr/local/texlive/2016/texmf-dist/tex/platex/base/jarticle.cls
-Document Class: jarticle 2006/06/27 v1.6 Standard pLaTeX class
-\c@@paper=\count81
-(/usr/local/texlive/2016/texmf-dist/tex/platex/base/jsize10.clo
-File: jsize10.clo 2006/06/27 v1.6 Standard pLaTeX file (size option)
-)
-\c@part=\count82
-\c@section=\count83
-\c@subsection=\count84
-\c@subsubsection=\count85
-\c@paragraph=\count86
-\c@subparagraph=\count87
-\c@figure=\count88
-\c@table=\count89
-\abovecaptionskip=\skip41
-\belowcaptionskip=\skip42
-\symmincho=\mathgroup4
-LaTeX Font Info:    Overwriting symbol font `mincho' in version `bold'
-(Font)                  JY1/mc/m/n --> JY1/gt/m/n on input line 593.
-\toclineskip=\dimen118
-\@lnumwidth=\dimen119
-\bibindent=\dimen120
-\heisei=\count90
-)
-(/usr/local/texlive/2016/texmf-dist/tex/latex/graphics/graphicx.sty
-Package: graphicx 2014/10/28 v1.0g Enhanced LaTeX Graphics (DPC,SPQR)
-
-(/usr/local/texlive/2016/texmf-dist/tex/latex/graphics/keyval.sty
-Package: keyval 2014/10/28 v1.15 key=value parser (DPC)
-\KV@toks@=\toks15
-)
-(/usr/local/texlive/2016/texmf-dist/tex/latex/graphics/graphics.sty
-Package: graphics 2016/05/09 v1.0r Standard LaTeX Graphics (DPC,SPQR)
-
-(/usr/local/texlive/2016/texmf-dist/tex/latex/graphics/trig.sty
-Package: trig 2016/01/03 v1.10 sin cos tan (DPC)
-)
-(/usr/local/texlive/2016/texmf-dist/tex/latex/graphics-cfg/graphics.cfg
-File: graphics.cfg 2016/01/02 v1.10 sample graphics configuration
-)
-Package graphics Info: Driver file: dvipdfmx.def on input line 96.
-
-(/usr/local/texlive/2016/texmf-dist/tex/latex/dvipdfmx-def/dvipdfmx.def
-File: dvipdfmx.def 2016/04/06 v4.08 LaTeX color/graphics driver for dvipdfmx (T
-eX Live/ChoF)
-
-(/usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/infwarerr.sty
-Package: infwarerr 2016/05/16 v1.4 Providing info/warning/error messages (HO)
-)
-(/usr/local/texlive/2016/texmf-dist/tex/generic/oberdiek/ltxcmds.sty
-Package: ltxcmds 2016/05/16 v1.23 LaTeX kernel commands for general use (HO)
-)))
-\Gin@req@height=\dimen121
-\Gin@req@width=\dimen122
-)
-(./picins.sty Option `picins' Version 3.0 Sep. 1992, TH Darmstadt/HRZ
-\@BILD=\box41
-\@TEXT=\box42
-\d@breite=\dimen123
-\d@hoehe=\dimen124
-\d@xoff=\dimen125
-\d@yoff=\dimen126
-\d@shad=\dimen127
-\d@dash=\dimen128
-\d@boxl=\dimen129
-\d@pichskip=\dimen130
-\d@tmp=\dimen131
-\d@tmpa=\dimen132
-\d@bskip=\dimen133
-\hsiz@=\dimen134
-\p@getot@l=\dimen135
-\c@breite=\count91
-\c@hoehe=\count92
-\c@xoff=\count93
-\c@yoff=\count94
-\c@pos=\count95
-\c@shad=\count96
-\c@dash=\count97
-\c@boxl=\count98
-\c@zeilen=\count99
-\@changemode=\count100
-\c@piccaption=\count101
-\c@piccaptionpos=\count102
-\c@picpos=\count103
-\c@whole=\count104
-\c@half=\count105
-\c@tmp=\count106
-\c@tmpa=\count107
-\c@tmpb=\count108
-\c@tmpc=\count109
-\c@tmpd=\count110
-\d@leftskip=\skip43
-\ptoti=\dimen136
-\ptotii=\dimen137
-\env@box=\box43
-\d@envdp=\dimen138
-\c@hsize=\count111
-\c@envdp=\count112
-\d@envb=\dimen139
-)
-(/usr/local/texlive/2016/texmf-dist/tex/latex/listings/listings.sty
-\lst@mode=\count113
-\lst@gtempboxa=\box44
-\lst@token=\toks16
-\lst@length=\count114
-\lst@currlwidth=\dimen140
-\lst@column=\count115
-\lst@pos=\count116
-\lst@lostspace=\dimen141
-\lst@width=\dimen142
-\lst@newlines=\count117
-\lst@lineno=\count118
-\lst@maxwidth=\dimen143
-
-(/usr/local/texlive/2016/texmf-dist/tex/latex/listings/lstmisc.sty
-File: lstmisc.sty 2015/06/04 1.6 (Carsten Heinz)
-\c@lstnumber=\count119
-\lst@skipnumbers=\count120
-\lst@framebox=\box45
-)
-(/usr/local/texlive/2016/texmf-dist/tex/latex/listings/listings.cfg
-File: listings.cfg 2015/06/04 1.6 listings configuration
-))
-Package: listings 2015/06/04 1.6 (Carsten Heinz)
-
-(./jlisting.sty
-Package: jlisting 2006/02/20 0.2 (Thor)
-\lst@nextchar=\count121
-\lst@inputfile=\read1
-)
-(/usr/local/texlive/2016/texmf-dist/tex/latex/fancyhdr/fancyhdr.sty
-\fancy@headwidth=\skip44
-\f@ncyO@elh=\skip45
-\f@ncyO@erh=\skip46
-\f@ncyO@olh=\skip47
-\f@ncyO@orh=\skip48
-\f@ncyO@elf=\skip49
-\f@ncyO@erf=\skip50
-\f@ncyO@olf=\skip51
-\f@ncyO@orf=\skip52
-)
-(/usr/local/texlive/2016/texmf-dist/tex/latex/abstract/abstract.sty
-Package: abstract 2009/06/08 v1.2a configurable abstracts
-\abstitleskip=\skip53
-\absleftindent=\skip54
-\absrightindent=\skip55
-\absparindent=\skip56
-\absparsep=\skip57
-)
-(/usr/local/texlive/2016/texmf-dist/tex/latex/url/url.sty
-\Urlmuskip=\muskip10
-Package: url 2013/09/16  ver 3.4  Verb mode for urls, etc.
-) (./bussproofs.sty
-Proof Tree (bussproofs) style macros. Version 1.1.
-\theLevel=\count122
-\myMaxLevel=\count123
-\myBoxA=\box46
-\myBoxB=\box47
-\myBoxC=\box48
-\myBoxD=\box49
-\myBoxLL=\box50
-\myBoxRL=\box51
-\thisAboveSkip=\dimen144
-\thisBelowSkip=\dimen145
-\newScoreStart=\dimen146
-\newScoreEnd=\dimen147
-\newCenter=\dimen148
-\displace=\dimen149
-\leftLowerAmt=\dimen150
-\rightLowerAmt=\dimen151
-\scoreHeight=\dimen152
-\scoreDepth=\dimen153
-\htLbox=\dimen154
-\htRbox=\dimen155
-\htRRbox=\dimen156
-\htRRRbox=\dimen157
-\htAbox=\dimen158
-\htCbox=\dimen159
-) (./dummy.tex)
-
-LaTeX Warning: Unused global option(s):
-    [9.5pt].
-
-(./midterm.aux)
-\openout1 = `midterm.aux'.
-
-LaTeX Font Info:    Checking defaults for OML/cmm/m/it on input line 53.
-LaTeX Font Info:    ... okay on input line 53.
-LaTeX Font Info:    Checking defaults for T1/cmr/m/n on input line 53.
-LaTeX Font Info:    ... okay on input line 53.
-LaTeX Font Info:    Checking defaults for OT1/cmr/m/n on input line 53.
-LaTeX Font Info:    ... okay on input line 53.
-LaTeX Font Info:    Checking defaults for OMS/cmsy/m/n on input line 53.
-LaTeX Font Info:    ... okay on input line 53.
-LaTeX Font Info:    Checking defaults for OMX/cmex/m/n on input line 53.
-LaTeX Font Info:    ... okay on input line 53.
-LaTeX Font Info:    Checking defaults for U/cmr/m/n on input line 53.
-LaTeX Font Info:    ... okay on input line 53.
-LaTeX Font Info:    Checking defaults for JY1/mc/m/n on input line 53.
-LaTeX Font Info:    ... okay on input line 53.
-LaTeX Font Info:    Checking defaults for JT1/mc/m/n on input line 53.
-LaTeX Font Info:    ... okay on input line 53.
-\c@lstlisting=\count124
-LaTeX Font Info:    External font `cmex10' loaded for size
-(Font)              <12> on input line 60.
-LaTeX Font Info:    External font `cmex10' loaded for size
-(Font)              <8> on input line 60.
-LaTeX Font Info:    External font `cmex10' loaded for size
-(Font)              <6> on input line 60.
-LaTeX Font Info:    Font shape `JT1/mc/bx/n' in size <14.4> not available
-(Font)              Font shape `JT1/gt/m/n' tried instead on input line 62.
-LaTeX Font Info:    Font shape `JY1/mc/bx/n' in size <14.4> not available
-(Font)              Font shape `JY1/gt/m/n' tried instead on input line 62.
-
-Underfull \hbox (badness 1275) in paragraph at lines 129--130
-[]\JY1/mc/m/n/10 比嘉 \OT1/cmr/m/n/10 (2016)[[]] \JY1/mc/m/n/10 では \OT1/cmr/m
-/n/10 CbC \JY1/mc/m/n/10 における \OT1/cmr/m/n/10 Code-Seg-ment \JY1/mc/m/n/10 
-、
- []
-
-LaTeX Font Info:    External font `cmex10' loaded for size
-(Font)              <7> on input line 139.
-LaTeX Font Info:    External font `cmex10' loaded for size
-(Font)              <5> on input line 139.
-File: ../pic/modus-ponens.pdf Graphic file (type pdf)
-<../pic/modus-ponens.pdf>
-Overfull \hbox (17.80374pt too wide) in paragraph at lines 151--152
- [] 
- []
-
-[1
-
-
-]
-LaTeX Font Info:    Try loading font information for OMS+cmr on input line 237.
-
- (/usr/local/texlive/2016/texmf-dist/tex/latex/base/omscmr.fd
-File: omscmr.fd 2014/09/29 v2.5h Standard LaTeX font definitions
-)
-LaTeX Font Info:    Font shape `OMS/cmr/m/n' in size <10> not available
-(Font)              Font shape `OMS/cmsy/m/n' tried instead on input line 237.
-File: ../pic/rbtree.pdf Graphic file (type pdf)
-
-<../pic/rbtree.pdf> (./midterm.bbl) [2] (./midterm.aux) ) 
-Here is how much of TeX's memory you used:
- 2621 strings out of 493693
- 35150 string characters out of 6149787
- 348144 words of memory out of 5000000
- 6171 multiletter control sequences out of 15000+600000
- 13613 words of font info for 54 fonts, out of 8000000 for 9000
- 929 hyphenation exceptions out of 8191
- 27i,7n,43p,246b,1003s stack positions out of 5000i,500n,10000p,200000b,80000s
-
-Output written on midterm.dvi (2 pages, 15628 bytes).
Binary file midterm/midterm.pdf has changed
--- a/midterm/midterm.tex	Thu Oct 26 14:21:59 2017 +0900
+++ b/midterm/midterm.tex	Thu Oct 26 14:35:55 2017 +0900
@@ -1,15 +1,17 @@
 %% TODO Agdaに関してやったこと書く
 %% TODO AgdaのStackとcbcのstackを例として出す。
+%% TODO 自然演繹の推論規則を表にまとめて乗っける
+
 
 \documentclass[twocolumn,twoside,9.5pt]{jarticle}
 \usepackage[dvipdfmx]{graphicx}
 \usepackage{picins}
 \usepackage{listings,jlisting}
 \usepackage{fancyhdr}
-\usepackage{abstract}
+%\usepackage{abstract}
+%\pagestyle{fancy}
 \usepackage{url}
 \usepackage{bussproofs}
-%\pagestyle{fancy}
 \lhead{\parpic{\includegraphics[height=1zw,keepaspectratio,bb=0 0 251 246]{../pic/emblem-bitmap.pdf}}琉球大学主催 工学部情報工学科 中間発表予稿}
 \rhead{}
 \cfoot{}
@@ -52,7 +54,7 @@
 \renewcommand{\abstractname}{Abstract}
 \begin{document}
 
-\title{CbC言語による検証}
+\title{CbC言語によるプログラムの検証}
 
 \author{145750B 氏名 {外間}{政尊} 指導教員 : 河野 真治}
 \date{}
@@ -95,8 +97,6 @@
 
 %% プログラムにおける証明は Curry-Howard Isomorphism で型付き $\lambda$計算に対応していることが知られている。
 
-しかし、現段階ではCbCでCbC自身を証明することはできない。そのため本研究では依存型を持つ証明支援系 Agda を用いて証明を行なう。
-
 %% 部分型を用いて CbC の項を型付けすることで、CbC の形式的定義を型システムより相似的に得る。
 
 本研究では CbC を用いて RedBlackTree を実装し、 Insert、Delete などの操作の際に RedBlackTree が常にその仕様を満たせているかを検査、証明することで、 CbC 上で動くプログラムが正しく検証できることを示す。
@@ -122,27 +122,53 @@
 %% \end{figure}
 
  %% CbC ではこの継続処理にをメタ計算として定義されていて、実装や環境によって切り替えることできる。検証を行うメタ計算を定義することで、 CodeSegment の仕様を変更せずソフトウェアの検証を行う事ができる。
+例として CbC による Stack のコード示す。
+
+\lstinputlisting[label=src:singlelinked, caption=CbCによるStack]{./src/SingleLinkedStack.cbc.replace}
 
 
 %CbC で Fanctional に書かれた CodeSegment は等価な Agda のコードに置き換えることが可能だと考えている。
 
+現状の CbC では CbC 自身を証明する事ができない。
 比嘉(2016)\cite{Yasutaka:2016}では CbC における CodeSegment 、 DataSegment が部分型で定義できることが示されている。
-
 これより、 CbC で Fanctional に書かれたプログラムは等価な Agda のコードの置き換えることができる。
-
+本研究では代わりに等価なAgdaのコードに変換することで証明を行う。
 
 \section{Agda}
-Agda\cite{agda} とは定理証明支援器であり依存型という強力な型を持つ関数プログラミング言語である。
-
+Agda\cite{agda} とは定理証明支援器であり依存型を関数プログラミング言語である。
 依存型とは型も第一級オブジェクトとする型システムであり、型の型や型を引数に取る関数、値を取って型を返す関数などが記述することができる。
+例として 前項で示した CbC で書かれた Stack をAgda に変換したコードを示す。
 
-型システムは Curry-Howard 同型対応により命題と型付き$\lambda$計算が一対一に対応する。
+\lstinputlisting[label=src:stack-agda, caption=AgdaによるStack]{./src/stack.agda.replace}
+%CbC で書かれた Stack の CodeSegment が要素、Tree、
+
+Agda のコードに変換した後証明を行う。
+
+%% 証明を行う前に自然演繹について説明
+自然演繹とは Gentzen によって作られた論理とその証明システムである。命題変数と記号を用いた論理式で論理を記述し、推論規則を使って変形することで求める論理式を導く。
 
-論理式は型に相当し、その型が持つ値の導出が証明となる。
-
+始めに、自然演繹と型付き$ \lambda $ 計算の対応を定義する。
+\begin{center}
+\begin{table}[htbp]
+\scalebox{0.75}{
+\begin{tabular}{|c|c|} \hline
+ Natural Deduction           & 型付き $ \lambda $ 計算  \\ \hline \hline
+ $ A $                       & 型 A を持つ変数 x \\ \hline
+ $ A \Rightarrow B $         & 型 A を取り型 B の変数を返す関数 f \\ \hline
+ $ \Rightarrow \mathcal{I} $ & ラムダの抽象化 \\ \hline
+ $ \Rightarrow \mathcal{E} $ & 関数適用 \\ \hline
+ $ A \land B $               & 型 A と型 B の直積型 を持つ変数 x \\ \hline
+ $ \land \mathcal{I} $       & 型A,Bを持つ値から直積型へのコンストラクタ \\ \hline
+ $ \land 1 \mathcal{E} $     & 直積型からの型Aを取り出す射影fst \\ \hline
+ $ \land 2 \mathcal{E} $     & 直積型からの型Bを取り出す射影snd \\ \hline
+\end{tabular}
+}
+\caption{natural deuction と 型付き $ \lambda $ 計算との対応(Curry-Howard Isomorphism)}
+\label{table:curry}
+\end{table}
+\end{center}
 
-
-ここでは A ならば B かつ B ならば C のとき A ならば C が成り立つという三段論法を例にとる。
+ここでは例として ((A ならば B) かつ (B ならば C)) ならば (A ならば C) が成り立つという三段論法を証明をする。
 
 この三段論法を自然演繹による証明木にすると次のようになる。
 
@@ -154,14 +180,39 @@
    \label{fig:modus-ponens}
 \end{figure}
 
+
 この証明木に対応するAgdaによる証明は次のようになる。
 
 \begin{lstlisting}[basicstyle=\ttfamily\footnotesize, frame=single]
-  f : {A B C : Set} → ((A → B) × (B → C)) → (A → C)
-  f = λ {x → (snd p) ((fst p) x)}
+data _×_ (A B : Set) : Set where
+  <_,_> : A → B → A × B
+
+fst : {A B : Set} → A × B → A
+fst < a , _ > = a
+
+snd : {A B : Set} → A × B → B
+snd < _ , b > = b 
+
+
+f : {A B C : Set} → ((A → B) × (B → C)) → (A → C)
+f = λ p x → (snd p) ((fst p) x)
 \end{lstlisting}
 
+三段論法の証明は、1つの仮定から $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ を用いて仮定を二つ取り出し、それぞれに $ \Rightarrow \mathcal{E} $ を適用した後に仮定を $ \Rightarrow \mathcal{I}$ して導出していた。
 
+$ \Rightarrow \mathcal{I}$ に対応するのは関数適用である。
+よってこの証明は「一つの変数から fst と snd を使って関数を二つ取り出し、それぞれを関数適用する」という形になる。
+%% これをラムダ式で書くとリスト~\ref{src:agda-modus-ponens}のようになる。
+仮定 $ (A \rightarrow B) \times (B \rightarrow C) $  と仮定 A から A $ \rightarrow $ C を導いている。
+
+仮定に相当する変数 p の型は$ (A \rightarrow B) \times (B \rightarrow C) $ であり、p からそれぞれの命題を取り出す操作が fst と snd に相当する。
+fst p の型は $ (A \rightarrow B) $ であり、snd p の型は $ (B \rightarrow C) $ である。
+もう一つの仮定xの型は A なので、fst p を関数適用することで B が導ける。
+得られた B を snd p に適用することで最終的に C が導ける。
+
+%% \lstinputlisting[label=src:agda-modus-ponens, caption=Agda における三段論法の証明] {src/AgdaModusPonens.agda.replaced}
+
+このように Agda では証明を記述することができる。
 
 % Agdaの知識ってどう出す？
 
@@ -193,14 +244,9 @@
 
 %% 定理証明支援器では Curry-Howard 同型対応により書いた命題通りに書いたプログラムをコンパイルが通ることはその命題を証明することが等しい。
 
-現状の CbC では CbC 自身を証明する事ができないため本研究では代わりに等価なAgdaのコードに変換することで証明を行う。
-
-CbC から Agda への変換は比嘉(2016)より、DataSegment がrecord型、 CodeSegmentが関数型で定義することが可能である。
 %% 以下に CbC で書かれた Stack の 定義の一部と それを Agda に変換したものの定義の一部分を示す。
 %% push だけじゃなく pop も入れたほうがいい…のかな
 
-以下にCbC で書かれた Stack の 定義と それを Agda に変換したものの定義を示す。
-
 %%% CbCのCodeSegmentの例
 
 %% context.h
@@ -220,28 +266,21 @@
 %%     pushStack {a} {t} s0 d next = (push s0) (stack s0) d (\s1 -> next (record {stack = s1} ))
 %% \end{lstlisting}
 
-\newpage
-\lstinputlisting[label=src:singlelinked, caption=CbCによるStack]{./src/SingleLinkedStack.cbc.replace}
-
-\lstinputlisting[label=src:stack-agda, caption=AgdaによるStack]{./src/stack.agda.replace}
-%CbC で書かれた Stack の CodeSegment が要素、Tree、
-
 
 
 
 \section{RedBlackTree}
 RedBlackTree とは拡張された二分探索木で、木のバランスを取るための情報として各ノードにそれぞれ赤、黒の色を持っている。
-RedBlackTree は通常の二分探索木の性質とは別に次のような性質を持っている。
+また、通常の二分探索木の条件に加えて、各ノードが赤か黒の色を持つ、ルートノードの色は黒、葉ノードの色は黒、赤ノードは二つの黒ノードを子として持つ、ルートから末端のノードへの経路に含まれる黒ノードの数は一定などの条件を持つ。
+%%RedBlackTree は通常の二分探索木の性質とは別に次のような性質を持っている。
 
-\begin{itemize}
-    \item 各ノードは赤か黒の色を持つ。
-    \item ルートノードの色は黒である。
-    \item 葉ノードの色は黒である。
-    \item 赤ノードは2つの黒ノードを子として持つ(= 赤ノードが続くことは無い)。
-    \item ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である。
-\end{itemize}
-
-%%また、通常の二分探索木の条件に加えて、各ノードが赤か黒の色を持つ、ルートノードの色は黒、葉ノードの色は黒、赤ノードは二つの黒ノードを子として持つ、ルートから末端のノードへの経路に含まれる黒ノードの数は一定などの条件を持つ。
+%% \begin{itemize}
+%%     \item 各ノードは赤か黒の色を持つ。
+%%     \item ルートノードの色は黒である。
+%%     \item 葉ノードの色は黒である。
+%%     \item 赤ノードは2つの黒ノードを子として持つ(= 赤ノードが続くことは無い)。
+%%     \item ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である。
+%% \end{itemize}
 
 数値を要素に持つ RedBlackTree の例を以下の図\ref{fig:rbtree}に示す。
 条件に示されている通り、ルートノードは黒であり、赤ノードは連続していない。
@@ -274,7 +313,7 @@
 
 \section{今後の課題}
 現段階では CbC で書かれた RedBlackTree の一部を Agda のコードに変換した。
-今後は CbC での RedBlackTree の Deletion 部分が実装中であることと、Agdaでの証明が未完成である。また、依存型を導入することで CbC で自身を証明できるようにするなどの課題がある。今後はこれらの課題に着手していく。
+今後は CbC での RedBlackTree の Deletion 、Agda での証明を実装していく。また、依存型を導入することで CbC で自身を証明できるようにするなどの課題があるため、今後はこれらの課題に着手していく。
 
 \nocite{*}
 \bibliographystyle{junsrt}