# HG changeset patch # User hamase # Date 1541663267 -32400 # Node ID ecb5281ed1a93611e8027051d091fab6d20838e5 # Parent c9b5432397b7e3a0cea9a0cde0929704c945bb74 2nd commit diff -r c9b5432397b7 -r ecb5281ed1a9 .DS_Store Binary file .DS_Store has changed diff -r c9b5432397b7 -r ecb5281ed1a9 midterm/.DS_Store Binary file midterm/.DS_Store has changed diff -r c9b5432397b7 -r ecb5281ed1a9 midterm/midterm.aux --- a/midterm/midterm.aux Thu Nov 08 10:57:19 2018 +0900 +++ b/midterm/midterm.aux Thu Nov 08 16:47:47 2018 +0900 @@ -1,22 +1,20 @@ \relax -\citation{Yasutaka:2016} -\citation{agda} +\citation{oculus} \@writefile{toc}{\contentsline {section}{\numberline {1}研究目的}{1}} -\@writefile{toc}{\contentsline {section}{\numberline {2}Countinuation based C (CbC)}{1}} -\newlabel{src:singlelinked}{{1}{1}} -\@writefile{lol}{\contentsline {lstlisting}{\numberline {1}CbCによるStack}{1}} -\@writefile{toc}{\contentsline {section}{\numberline {3}Agda}{1}} +\@writefile{toc}{\contentsline {section}{\numberline {2}VR(仮想現実)}{1}} +\@writefile{toc}{\contentsline {section}{\numberline {3}LeapMotion}{1}} +\@writefile{toc}{\contentsline {section}{\numberline {4}シミュレーションシステムの概要}{1}} +\@writefile{toc}{\contentsline {subsection}{\numberline {4.1}エディットモード}{1}} +\@writefile{toc}{\contentsline {subsection}{\numberline {4.2}プレイモード}{1}} +\@writefile{toc}{\contentsline {subsection}{\numberline {4.3}オーディエンスモード}{1}} +\@writefile{toc}{\contentsline {section}{\numberline {5}課題(腕の長さ問題)}{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: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 {1}{\ignorespaces RedBlackTreeの例}}{2}} -\newlabel{fig:rbtree}{{1}{2}} -\@writefile{toc}{\contentsline {section}{\numberline {5}今後の課題}{2}} +\bibcite{oculus}{1} +\@writefile{toc}{\contentsline {subsection}{\numberline {5.1}範囲外設置の禁止}{2}} +\@writefile{toc}{\contentsline {subsection}{\numberline {5.2}演奏者の移動を可能とする}{2}} +\@writefile{toc}{\contentsline {subsection}{\numberline {5.3}手の延長線上を選択可能とする}{2}} +\@writefile{toc}{\contentsline {subsubsection}{\numberline {5.3.1}具体的な手法}{2}} +\@writefile{toc}{\contentsline {subsubsection}{\numberline {5.3.2}利き目の位置の測定}{2}} +\@writefile{toc}{\contentsline {section}{\numberline {6}今後の課題}{2}} diff -r c9b5432397b7 -r ecb5281ed1a9 midterm/midterm.bbl --- a/midterm/midterm.bbl Thu Nov 08 10:57:19 2018 +0900 +++ b/midterm/midterm.bbl Thu Nov 08 16:47:47 2018 +0900 @@ -1,25 +1,7 @@ \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). +\bibitem{oculus} +Oculus rift dk2 setup ― leapmotion documentation. +\newblock \url{https://developer.leapmotion.com/vr-setup/dk2}. \end{thebibliography} diff -r c9b5432397b7 -r ecb5281ed1a9 midterm/midterm.blg --- a/midterm/midterm.blg Thu Nov 08 10:57:19 2018 +0900 +++ b/midterm/midterm.blg Thu Nov 08 16:47:47 2018 +0900 @@ -3,45 +3,45 @@ The top-level auxiliary file: midterm.aux The style file: junsrt.bst Database file #1: reference.bib -You've used 5 entries, +You've used 1 entry, 2270 wiz_defined-function locations, - 561 strings with 4741 characters, -and the built_in function-call counts, 806 in all, are: -= -- 44 -> -- 14 + 541 strings with 4162 characters, +and the built_in function-call counts, 161 in all, are: += -- 8 +> -- 1 < -- 0 -+ -- 8 -- -- 3 -* -- 5 -:= -- 87 -add.period$ -- 12 -call.type$ -- 5 -change.case$ -- 5 ++ -- 1 +- -- 0 +* -- 2 +:= -- 19 +add.period$ -- 2 +call.type$ -- 1 +change.case$ -- 1 chr.to.int$ -- 0 -cite$ -- 5 -duplicate$ -- 55 -empty$ -- 121 -format.name$ -- 6 -if$ -- 201 +cite$ -- 1 +duplicate$ -- 11 +empty$ -- 25 +format.name$ -- 0 +if$ -- 39 int.to.chr$ -- 0 -int.to.str$ -- 5 +int.to.str$ -- 1 missing$ -- 0 -newline$ -- 25 -num.names$ -- 3 -pop$ -- 63 +newline$ -- 7 +num.names$ -- 0 +pop$ -- 12 preamble$ -- 1 purify$ -- 0 quote$ -- 0 -skip$ -- 47 +skip$ -- 11 stack$ -- 0 substring$ -- 0 -swap$ -- 5 +swap$ -- 1 text.length$ -- 0 text.prefix$ -- 0 top$ -- 0 type$ -- 0 warning$ -- 0 -while$ -- 3 -width$ -- 6 -write$ -- 44 -is.kanji.str$ -- 33 +while$ -- 0 +width$ -- 2 +write$ -- 9 +is.kanji.str$ -- 6 diff -r c9b5432397b7 -r ecb5281ed1a9 midterm/midterm.log --- a/midterm/midterm.log Thu Nov 08 10:57:19 2018 +0900 +++ b/midterm/midterm.log Thu Nov 08 16:47:47 2018 +0900 @@ -1,6 +1,7 @@ -This is e-pTeX, Version 3.14159265-p3.8.0-180226-2.6 (utf8.euc) (TeX Live 2018) (preloaded format=platex 2018.11.8) 8 NOV 2018 10:52 +This is e-pTeX, Version 3.14159265-p3.8.0-180226-2.6 (utf8.euc) (TeX Live 2018) (preloaded format=platex 2018.11.8) 8 NOV 2018 16:35 entering extended mode restricted \write18 enabled. + file:line:error style messages enabled. %&-line parsing enabled. **midterm.tex (./midterm.tex @@ -205,35 +206,14 @@ (Font) Font shape `JT1/gt/m/n' tried instead on input line 48. 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 48. -LaTeX Font Info: Try loading font information for OMS+cmr on input line 113. - - (/usr/local/texlive/2018/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 113. -LaTeX Font Info: External font `cmex10' loaded for size -(Font) <7> on input line 113. -LaTeX Font Info: External font `cmex10' loaded for size -(Font) <5> on input line 113. -LaTeX Font Info: Try loading font information for OML+cmr on input line 113. - - -(/usr/local/texlive/2018/texmf-dist/tex/latex/base/omlcmr.fd -File: omlcmr.fd 2014/09/29 v2.5h Standard LaTeX font definitions -) -LaTeX Font Info: Font shape `OML/cmr/m/n' in size <10> not available -(Font) Font shape `OML/cmm/m/it' tried instead on input line 113. - -Underfull \hbox (badness 1275) in paragraph at lines 125--128 -[]\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: Font shape `JT1/mc/bx/n' in size <12> not available +(Font) Font shape `JT1/gt/m/n' tried instead on input line 73. +LaTeX Font Info: Font shape `JY1/mc/bx/n' in size <12> not available +(Font) Font shape `JY1/gt/m/n' tried instead on input line 73. File: ../pic/emblem-bitmap.pdf Graphic file (type pdf) <../pic/emblem-bitmap.pdf> + Package Fancyhdr Warning: \headheight is too small (0.0pt): Make it at least 20.37784pt. We now make it that large for the rest of the document. @@ -243,16 +223,27 @@ ] -File: ../pic/rbtree.pdf Graphic file (type pdf) -<../pic/rbtree.pdf> - (./midterm.bbl) [2] (./midterm.aux) ) +LaTeX Font Info: Font shape `JT1/mc/bx/n' in size <10> not available +(Font) Font shape `JT1/gt/m/n' tried instead on input line 105. +LaTeX Font Info: Font shape `JY1/mc/bx/n' in size <10> not available +(Font) Font shape `JY1/gt/m/n' tried instead on input line 105. +LaTeX Font Info: External font `cmex10' loaded for size +(Font) <7> on input line 110. +LaTeX Font Info: External font `cmex10' loaded for size +(Font) <5> on input line 110. + (./midterm.bbl +Underfull \hbox (badness 10000) in paragraph at lines 4--6 +\OT1/cmtt/m/n/10 https : / / developer . leapmotion . com / vr-[]setup / + [] + +) [2] (./midterm.aux) ) Here is how much of TeX's memory you used: - 2841 strings out of 493281 - 35755 string characters out of 6145041 - 272533 words of memory out of 5000000 - 6775 multiletter control sequences out of 15000+600000 - 13256 words of font info for 52 fonts, out of 8000000 for 9000 + 2538 strings out of 493281 + 33006 string characters out of 6145041 + 114497 words of memory out of 5000000 + 6484 multiletter control sequences out of 15000+600000 + 13871 words of font info for 54 fonts, out of 8000000 for 9000 929 hyphenation exceptions out of 8191 - 37i,16n,45p,369b,1854s stack positions out of 5000i,500n,10000p,200000b,80000s + 26i,16n,43p,362b,363s stack positions out of 5000i,500n,10000p,200000b,80000s -Output written on midterm.dvi (2 pages, 17680 bytes). +Output written on midterm.dvi (2 pages, 15236 bytes). diff -r c9b5432397b7 -r ecb5281ed1a9 midterm/midterm.pdf Binary file midterm/midterm.pdf has changed diff -r c9b5432397b7 -r ecb5281ed1a9 midterm/midterm.synctex.gz Binary file midterm/midterm.synctex.gz has changed diff -r c9b5432397b7 -r ecb5281ed1a9 midterm/midterm.tex --- a/midterm/midterm.tex Thu Nov 08 10:57:19 2018 +0900 +++ b/midterm/midterm.tex Thu Nov 08 16:47:47 2018 +0900 @@ -39,300 +39,124 @@ \input{dummy.tex} %\renewcommand{\abstractname}{Abstract} \begin{document} -\title{CbC言語によるプログラムの検証} -\author{145750B 氏名 {外間}{政尊} 指導教員 : 河野 真治} +\title{VRを用いた総合楽器シミュレーションシステム} +\author{155718B 氏名 {浜瀬}{裕暉} 指導教員 : 河野 真治} \date{} \maketitle \thispagestyle{fancy} \section{研究目的} -%% Agdaのお勉強のこと、CbCをAgdaに直したこと、CbC側のDeletionのこと - -%% CbC でソフトウェアを検証できるかを CbCで書いた RBTree と Agda で同様に書いた RBTree を検証することで示す - -%% ソフトウェアの規模が大きくなるにつれて期待されない動作をすることが増える。ここでは期待される動作を仕様、期待されない動作をバグと呼ぶことにする。 -%% それにはソフトウェアが期待される仕様を満たすか検証する手法と、仕様を直接証明する手法とがある。 -%% 期待される仕様を満たすか検証する手法と、仕様を直接証明する手法とがある。 - -%% 特に実際に動作するソフトウェアを検証、証明できることが望ましい。 -%% そのために当研究室では CodeSegment 、 Data Segment という単位を用いてソフトウェアを記述する手法を提案している。 -%% 処理の単位である CodeSegment は、メタ計算によって相互に接続される。 -%% メタ計算を切り替えることで CodeSegment を変更することなくソフトウェアの性質を検証することができる。 -% CbC検証と実装が同一の言語で行える言語である。 -% CbCの特徴はだいじょうぶ？完全じゃなくていいけどある程度は乗せなきゃ駄目だよね - -ソフトウェアの信頼性を保証することは重要である。現在ソフトウェアの信頼性を保証する方法として代表的なものはモデル検査と、定理証明が存在している。 -モデル検査はソフトウェアの状態をすべて数え上げ、すべての状態で仕様が正しいことを確認する方法である。 -定理証明はソフトウェアが満たすべき仕様を論理式で記述し、その論理式が恒真であることを証明することである。%% atton-master papar より -%% モデル検査や、証明でソフトウェアを検証する際、検証に使われる言語と実装に使う言語が異なるという問題がある。 -%% そのため、二重で同じソフトウェアを記述する必要があるうえ、検証に用いるソースコードは状態が遷移する形で記述する必要があるなど実装されているコードに比べて記述が困難である。 -%% 検証されたコードから実行可能なコードを生成可能な検証系もあるが、生成されたコードが検証のコードと別の言語であったり、既存の実際に対する検証は行えないなどの問題がある。 +3D空間上に物体を用意することは簡単である。 +それに対し、現実に物体を作成することはしばしば大きな困難を伴う。 -% この問題を解決する為に -当研究室では検証と実装を同一の言語で行える Continuation based C ( CbC )言語を開発している。 -本研究では、検証や証明に直接使用できる言語として CbC を用いる。 - - %% CbC 上に構築されたプログラムが持つ状態を数え挙げ、仕様を満たすか調べるモデル検査的手法は、比嘉(2016)\cite{Yasutaka:2016}により提案、実装されている。 -%% また、赤黒木の仕様が、限定的な木の大きさの範囲内で検証されている。 - -%% 木の大きさを制限せず実装が仕様を満たすことを示すには証明が必要である。 - -%% プログラムにおける証明は Curry-Howard Isomorphism で型付き $\lambda$計算に対応していることが知られている。 - -%% 部分型を用いて CbC の項を型付けすることで、CbC の形式的定義を型システムより相似的に得る。 - -本研究では CbC を用いて RedBlackTree を実装し、 Insert、Delete などの操作の際に RedBlackTree が常にその仕様を満たせているかを検証、証明する。 - -%%検証と証明の話書かないとAgda出せなくない？ - -\section{Countinuation based C (CbC)} -Continuation based C (CbC) とは、当研究室で開発されているプログラミング言語である。 -CbC では OS や組み込みソフトウェアを主な対象としている。 -CbC は C 言語とほぼおなじ構文を持ち、よりアセンブラに近い形でプログラムを記述する。 +現在、様々な音楽家が伝統ある楽器ではなく、全く新しい楽器や演奏システムを使用したパフォーマンスを行なっているが、これらの開発には莫大なコストがかかり、小規模なアーディストがこれらの新しい楽器や演奏システムを開発することは難しい。 -CbC では C の関数の代わりに CodeSegment を用いて処理を記述する。 -CodeSegment は値を入力として受取り、出力を行う処理の単位で、それらの状態を goto で遷移して記述する。この goto による処理の遷移を継続と呼ぶ。 -CbC の CodeSegment を定義するには C とは少し異なり関数定義のの先頭に \_\_code が付く。 -DataSegment は CodeSegment が扱うデータの単位であり、処理に必要なデータが全て入っている。CodeSegment の入力となる DataSegment は Input DataSegment　出力 を Input DataSegment は関数の引数として定義する。次の CodeSegment に処理を移す際は、 goto の後に CodeSegment 名と Input DataDataSegment を指定する。 -% 図\ref{fig:CSContinuation}は CodeSegment 感の処理の流れを表している。 - -%%% figure -%% \begin{figure}[htbp] -%% \begin{center} -%% \includegraphics[width=60mm]{../pic/codesegment.pdf} -%% \end{center} -%% \caption{ goto による CodeSegment 間の接続} -%% \label{fig:CSContinuation} -%% \end{figure} - -CbC ではこの継続処理にをメタ計算として定義されていて、実装や環境によって切り替えることできる。検証を行うメタ計算を定義することで、 CodeSegment の仕様を変更せずソフトウェアの検証を行う事ができる。 -例として CbC による Stack に対する操作のコード示す。 - -\newpage -\lstinputlisting[label=src:singlelinked, caption=CbCによるStack]{./src/SingleLinkedStack.cbc.replace} - -このコードでは Stack に対する push と pop を定義している。 - -push や pop は必要があるときに外から呼ばれる。 +そこで、新しい楽器を開発する際、実際に楽器を用意する前に簡便にその使用感、外見、その他の特徴を把握し、構想した楽器を製造するかどうかの指標を定められるようなソフトウェアを開発する。 -push では element で新しい要素を作って、次の要素との関係、 push する要素を入れ、Stack の top を書き換えて次のCodeSegmentに飛ぶ。 - -pop では Stack の top に data があればその data を next に入れ、次のCodeSegmentに飛ぶ。 top に data が無ければ NULL を next の Input Data に入れて次のCodeSegmentに飛ぶ。 - -%% また CbC で Functional に書かれた CodeSegment は等価な Agda のコードに置き換えることが可能だと考えている。 - -比嘉(2016)\cite{Yasutaka:2016}では CbC における CodeSegment 、 DataSegment が部分型で定義できることが示されている。 -これより、 CbC で Functional に書かれたプログラムは等価な Agda のコードの置き換えることができる。 -本研究では CbC の代わりに等価なAgdaのコードに変換することで証明を行う。 - -\section{Agda} -Agda\cite{agda} とは定理証明支援器であり依存型を関数プログラミング言語である。 -依存型とは型も第一級オブジェクトとする型システムであり、型の型や型を引数に取る関数、値を取って型を返す関数などが記述することができる。 +\section{VR(仮想現実)} +VR(仮想現実)とは、コンピュータグラフィクスで作られた世界を、あたかも現実であるかのように体験することができるシステムである。現在、多くのVRデバイスが開発中であるが、それらの多くは「視覚」「聴覚」「触覚」に作用するものである。本研究では、「視覚」「聴覚」に注目してシステムを開発する。 -CbC を Agda に変換する場合 DataSegment をレコード型、 CodeSegment は関数型となる。 - -前項で示した CbC で書かれた Stack の操作をAgda に変換したコードを示す。 - -\lstinputlisting[label=src:stack-agda, caption=AgdaによるStack]{./src/stack.agda.replace} - -%CbC で書かれた Stack の CodeSegment が要素、Tree、 - -Agda のコードで関数を定義するときは関数名、型を記述した後に関数本体を指定する。関数の型では → または \verb/->/ を使い定義する。 -%% 引数は変数で受けることもできるが、具体的な型構築子を渡された時の挙動を定義することができる。これはパターンマッチと呼ばれ、型構築子で case 文を行っているようなものである。 -%% パターンマッチはすべての場合を含む必要があり、特定のものだけ異なる挙動にしたい場合は構築子を幾つか指定した後に変数で受けることで解決できる。なお、マッチした値を変数として利用しない場合は _ で値を捨てることもできる。 - -関数にはリテラルが存在し、関数を定義せずにその場で値を生成することもできる。これは ラムダ式と呼ばれ、 \verb/\arg1 arg2 -> function body/ または $ \lambda $ arg1 arg2 → function body のように記述できる。上の例では pushStack の \verb/\s1 -> next (record {stack = s1})/ や、 popStack の \verb/\s1 -> next s0/ が ラムダ式である。 +VRコンテンツはその没入感が非常に重要であり、これを欠いたVRコンテンツは不快感、疲労、体調不良を引き起こす原因となりうる。 -%%%%%%%% - Agda のレコード型も存在する。定義をする際は record キーワードのあとにレコード名、型、 where の後に field キーワードを入れ、フィールド名 : 型名 と列挙する。レコードを構築する際は record キーワードの後に {} 内部に fileName = value の形で列挙していく。複数の値を列挙する際は ; で区切る。上の例では \verb/record {stack = s1}/ がそれにあたる。 +\section{LeapMotion} +LeapMotion\cite{oculus}とはVR向けに開発されたデバイスの一つで、使用者の手の相対位置、開き具合等を取得することができる装置である。LeapMotionを使用することにより、コントローラー、その他の入力デバイスを手に所持することなくVRシステムの操作を行うことが可能にとなる。 - +\section{シミュレーションシステムの概要} +本シミュレーションシステムはVR空間上に楽器を構築していくソフトウェアで、オブジェクトの直交座標配置、および極座標配置をサポートする。 +また、VR空間上での動作をすることにより、演奏者の背後に配置されるオブジェクトへの作用を簡単に行うことが可能となるなど、VR空間上でなければなしえない動作を可能とする。 -%% リテラル is 何 +打楽器、弦楽器等、複数の奏法を複合するような楽器へのシミュレーションを没入感を損なうことなく可能にすることは、コントローラー等の「手を握った状態から開くことが不可能」である入力デバイスでは困難であるが、LeapMotionを組み込むことによりこれを可能とする。 + +楽器の構築をする「エディットモード」、構築した楽器を試奏する「プレイモード」、演奏の様子を観客視点から見る「オーディエンスモード」を切り替えながら操作していく。 +\subsection{エディットモード} +あらかじめ定められた楽器パーツ、およびシミュレーター使用者が独自に作成したパーツをインポートしたものを、直交座標、または極座標にしたがって配置していく。配置される座標は、数値での座標入力で決定する。 +配置された楽器パーツは、手で触れることで選択状態になり、再配置することが可能となる。 +\subsection{プレイモード} +エディットモードで配置された各パーツに触れることにより、規定の音が再生される。シミュレーター使用者は、このモードにより無理なく各パーツが配置されているかどうかを確認することができる。 +\subsection{オーディエンスモード} +プレイモードでは演奏者の視点で楽器を観察することができたが、オーディエンスモードでは演奏の様子を観客視点で見ることができる。このモードにより、シミュレーター使用者は想定した通りの演奏の様子となっているかどうかを確認することができる。 -%% このコードでは push 、 pop の関数を定義をしている。 -%% push では要素を追加した新しいStackを返す。 -%% pop では data があればそのデータを pop し、しない場合はそもそも - -このように CbC のコードを Agda に変換し、証明を行う。 +%\begin{figure}[htpb] +% \begin{center} +% \includegraphics[width=50mm]{../pic/rbtree.pdf} +% \end{center} +% \caption{RedBlackTreeの例} +% \label{fig:rbtree} +%\end{figure} -% 証明を行う前に自然演繹について説明 -%% 自然演繹とは 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) が成り立つという三段論法を証明をする。 - -%% この三段論法を自然演繹による証明木にすると次のようになる。 - -%% \begin{figure}[htpb] -%% \begin{center} -%% \includegraphics[width=95mm]{../pic/modus-ponens.pdf} -%% \end{center} -%% \caption{自然演繹での三段論法の証明} -%% \label{fig:modus-ponens} -%% \end{figure} - - -%% この証明木に対応するAgdaによる証明は次のようになる。 +\section{課題(腕の長さ問題)} +エディットモード中、楽器パーツを手の届く範囲外に配置してしまった場合、手で触れることができなくなり再選択が不可能となる問題がある。 +これを解決するためには、いくつかの方法が考えられる。 +\subsection{範囲外設置の禁止} +演奏者から一定距離以上離れた位置へのオブジェクト配置を禁止する方法は、最も簡単にこの問題を解決する。 -%% \begin{lstlisting}[basicstyle=\ttfamily\footnotesize, frame=single] -%% 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 を導いている。 +しかし、この方法は演奏者の創造性を阻害する可能性がある。 +\subsection{演奏者の移動を可能とする} +シミュレーター利用者の現在位置を変更可能にすることは、この問題を解決する。 -%% 仮定に相当する変数 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の知識ってどう出す？ - -%TODO 定理証明とプログラムの話 - -%% \begin{prooftree} -%% \AxiomC{ $ [A] $ $_{(1)}$} -%% \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } -%% \RightLabel{ $ \land 1 \mathcal{E} $ } -%% \UnaryInfC{ $ (A \Rightarrow B) $ } -%% \RightLabel{ $ \Rightarrow \mathcal{E} $} -%% \BinaryInfC{ $ B $ } - +しかし、本シミュレーターはLeapMotion操作を基本としており、正確な移動操作が難しいため、視点操作を搭載するとシミュレーター利用者とVR映像との間に齟齬が発生してしまう場合がある。 +その場合、シミュレーター利用者に不快感を与える原因となりうる。 +\subsection{手の延長線上を選択可能とする} +本シミュレーターでは、手が直接触れていなくても、画面上で手と重なっている楽器パーツを選択可能にすることで、この問題を解決する。 +\subsubsection{具体的な手法} +厳密に手の中心延長線上のオブジェクトを選択する場合、遠方にある小さなオブジェクトを選択することは困難である。これは、ユーザーとオブジェクトの距離が離れることにより、わずかな手の位置の誤差が遠方では大きな位置の誤差となるからである。よって、選択するオブジェクトは手の延長線上との誤差が一定値以下の集合の中で、その誤差が最小値であるオブジェクトである。 +\subsubsection{利き目の位置の測定} +VRのうち視覚に関する立体視は左右の目にそれぞれ異なる位置からのカメラ映像情報を与えることで実現している。よって、「どちらの目からの延長線をとるか」「顔の中心から目までの距離」を決定する必要がある。 -%% \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ } -%% \RightLabel{ $ \land 2 \mathcal{E} $ } -%% \UnaryInfC{ $ (B \Rightarrow C) $ } - -%% \RightLabel{ $ \Rightarrow \mathcal{E} $} -%% \BinaryInfC{ $ C $ } -%% \RightLabel{ $ \Rightarrow \mathcal{I} _{(1)}$} -%% \UnaryInfC{ $ A \Rightarrow C $} -%% \RightLabel{ $ \Rightarrow \mathcal{I} _{(2)}$} -%% \UnaryInfC{ $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $} -%% \end{prooftree} - - -%% Agdaによる三段論法の証明 - -%% 定理証明支援器では Curry-Howard 同型対応により書いた命題通りに書いたプログラムをコンパイルが通ることはその命題を証明することが等しい。 - -%% 以下に CbC で書かれた Stack の 定義の一部と それを Agda に変換したものの定義の一部分を示す。 -%% push だけじゃなく pop も入れたほうがいい…のかな - -%%% CbCのCodeSegmentの例 - -%% context.h - - -%% \begin{lstlisting}[basicstyle=\ttfamily\footnotesize, frame=single] -%% \end{lstlisting} - - % Stack.agdaのコード -%% \begin{lstlisting}[basicstyle=\ttfamily\footnotesize, frame=single] -%% record Stack {a t : Set} (stackImpl : Set) : Set where -%% field -%% stack : stackImpl -%% push : stackImpl -> a -> (stackImpl -> t) -> t - -%% pushStack : {a t : Set} -> Stack a -> a -> (Stack t -> t) -> t -%% pushStack {a} {t} s0 d next = (push s0) (stack s0) d (\s1 -> next (record {stack = s1} )) -%% \end{lstlisting} - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% - +カメラ中心の位置ベクトル$\vec{O}$および方向ベクトル$\vec{D}$をそれぞれ +\begin{eqnarray} +\vec{O}&=&(0,0,0)\\ +\vec{D}&=&(0,1,0) +\end{eqnarray} +とし(これは、ある一点の方向に顔を向けることで実現できる)、利き目測定用オブジェクト$W_1$、$W_2$の位置ベクトルをそれぞれ +\begin{eqnarray} +\vec{w_1}&=&(1,1,0)\\ +\vec{w_2}&=&(-1,1,0) +\end{eqnarray} +とした時に、シミュレーター使用者がそれぞれ決定した手の位置ベクトル$\vec{h_1}$、$\vec{h_2}$が +\begin{eqnarray} +\vec{h_1}&=&(x_1,y_1,z_1)\\ +\vec{h_2}&=&(x_2,y_2,z_2) +\end{eqnarray} +であった時、2直線 +\begin{eqnarray} +\vec{l_1}&=&\vec{w_1}+a(\vec{h_1}-\vec{w_1})(a:実数)\\ +\vec{l_2}&=&\vec{w_2}+b(\vec{h_2}-\vec{w_2})(b:実数) +\end{eqnarray} +間の距離が最小となる点Eの座標を求めれば、これがカメラ中心に対する利き目の相対位置となる。 -\section{RedBlackTree} -RedBlackTree とは拡張された二分探索木で、木のバランスを取るための情報として各ノードにそれぞれ赤、黒の色を持っている。 -また、通常の二分探索木の条件に加えて、各ノードが赤か黒の色を持つ、ルートノードの色は黒、葉ノードの色は黒、赤ノードは二つの黒ノードを子として持つ、ルートから末端のノードへの経路に含まれる黒ノードの数は一定などの条件を持つ。 -%%RedBlackTree は通常の二分探索木の性質とは別に次のような性質を持っている。 - -%% \begin{itemize} -%% \item 各ノードは赤か黒の色を持つ。 -%% \item ルートノードの色は黒である。 -%% \item 葉ノードの色は黒である。 -%% \item 赤ノードは2つの黒ノードを子として持つ(= 赤ノードが続くことは無い)。 -%% \item ルートから最下位ノードへの経路に含まれる黒ノードの数はどの最下位ノードでも一定である。 -%% \end{itemize} - -数値を要素に持つ RedBlackTree の例を以下の図\ref{fig:rbtree}に示す。 -条件に示されている通り、ルートノードは黒であり、赤ノードは連続していない。 -加えて各最下位ノードへの経路に含まれる黒ノードの個数は全て2である。 -%% atton-master fig3.1 - -%%%%figure -\begin{figure}[htpb] - \begin{center} - \includegraphics[width=50mm]{../pic/rbtree.pdf} - \end{center} - \caption{RedBlackTreeの例} - \label{fig:rbtree} -\end{figure} - -本研究で検証する RedBlackTree は非破壊であり、一度構築した木構造は破壊される操作ごとに新しい木が生成される。非破壊である理由は並列実行時のデータ保存である。 - - -%% atton-master@13p - -%% figure -%\begin{figure}[htbp] -% \begin{center} -% \includegraphics[width=50mm]{../pic/treeVnc.pdf} -% \end{center} -% \caption{構成される木構造} -% \label{fig:tree} -%\end{figure} - -%% \lstinputlisting[label=src:agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda.replaced} - +$l_1$、及び$l_2$上の任意の点P、Qの位置ベクトルはそれぞれ +\begin{eqnarray} +\vec{p}&=&(1,1,0)+a(x_1-1,y_1-1,z_1)\\&=&(a(x_1-1)+1,a(y_1-1)+1,az_1)\\ +\vec{q}&=&(-1,1,0)+b(x_2+1,y_2-1,z_2)\\&=&(b(x_2+1)-1,b(y_2-1)+1,bz_2)\\ +\end{eqnarray} +であるから、 +\begin{eqnarray} +PQ^2&=&[a(x_1-1)+1-\{b(x_2+1)-1\}]^2\\&+&\{a(y_1-1)-b(y_2-1)\}^2+(az_1-bz_2)^2 +\end{eqnarray} +となり、$\vec{h_1}$及び$\vec{h_2}$は既知であることから式(14)はa,bの2変数式であり、この$PQ^2$を最小とする$(a,b)$の組を求めることで$PQ$間を最小とする点P,Qの座標がわかるため、この位置ベクトルをそれぞれ$\vec{P_{min}}$,$\vec{Q_{min}}$とすると、求める利き目の位置ベクトル$\vec{E}$は +\begin{eqnarray} +\vec{E}&=&\frac{\vec{P_{min}}+\vec{Q_{min}}}{2} +\end{eqnarray} +とわかる。 +また、そのような$(a,b)$の組は、それぞれ +\begin{eqnarray} +PQ^2\frac{\partial}{\partial a}&=&0\\ +PQ^2\frac{\partial}{\partial b}&=&0 +\end{eqnarray} +を解けば求まる。 \section{今後の課題} -現段階では CbC で書かれた RedBlackTree の一部を Agda のコードに変換した。 -今後は CbC での RedBlackTree の Deletion 、Agda での証明を実装していく。また、依存型を導入することで CbC で自身を証明できるようにするなどの課題があるため、今後はこれらの課題に着手していく。 +現段階では本シミュレーターの概要のみ考案した。 +今後、これらの構想の実装に着手していく。 \nocite{*} \bibliographystyle{junsrt} \bibliography{reference} +%\begin{thebibliography}{9} +%\bibitem{Oculus}OculusRiftDK2Setup \url{https://developer.leapmotion.com/vr-setup/dk2} +%\end{thebibliography} \end{document} diff -r c9b5432397b7 -r ecb5281ed1a9 midterm/reference.bib --- a/midterm/reference.bib Thu Nov 08 10:57:19 2018 +0900 +++ b/midterm/reference.bib Thu Nov 08 16:47:47 2018 +0900 @@ -1,33 +1,4 @@ -@Misc{Yasutaka:2016, - author = "{比嘉 健太, 河野 真治}", - title = "{メタ計算を用いた Continuation based C の検証手法}", - journal = "琉球大学工学部情報工学科平成 28 年度学位論文", - year = 2016 -} - -@Misc{Tatsuki:2016, - author = "{伊波 立樹, 東恩納 琢偉, 河野 真治}", - title = "{Code Gear 、Data Gear に基づく OS のプロトタイプ}", - journal = "{情報処理学会システムソフトウェアとオペレーティングシステム研究会}", - year = 2016 -} - -@Misc{kaito:2015, - author = "{徳森 海斗, 河野 真治}", - title = "{LLVM Clang 上の Continuation based C コンパイラ の改良}", - journal = "{琉球大学工学部情報工学科平成 27 年度学位論文}", - year = 2015 -} - -@misc{agda, - title = {The Agda wiki}, - howpublished = {\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}}, - note = {Accessed: 2017/10/24(Tue)} -} - - -@misc{agda-documentation, - title = {Welcome to Agda’s documentation! — Agda 2.6.0 documentation}, - howpublished = {\url{http://agda.readthedocs.io/en/latest/index.html}}, - note = {Accessed: 2017/10/24(Tue)} +@misc{oculus, + title = {Oculus Rift DK2 Setup — LeapMotion documentation}, + howpublished = {\url{https://developer.leapmotion.com/vr-setup/dk2}} } \ No newline at end of file diff -r c9b5432397b7 -r ecb5281ed1a9 midterm/referenceのコピー.bib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/midterm/referenceのコピー.bib Thu Nov 08 16:47:47 2018 +0900 @@ -0,0 +1,33 @@ +@Misc{Yasutaka:2016, + author = "{比嘉 健太, 河野 真治}", + title = "{メタ計算を用いた Continuation based C の検証手法}", + journal = "琉球大学工学部情報工学科平成 28 年度学位論文", + year = 2016 +} + +@Misc{Tatsuki:2016, + author = "{伊波 立樹, 東恩納 琢偉, 河野 真治}", + title = "{Code Gear 、Data Gear に基づく OS のプロトタイプ}", + journal = "{情報処理学会システムソフトウェアとオペレーティングシステム研究会}", + year = 2016 +} + +@Misc{kaito:2015, + author = "{徳森 海斗, 河野 真治}", + title = "{LLVM Clang 上の Continuation based C コンパイラ の改良}", + journal = "{琉球大学工学部情報工学科平成 27 年度学位論文}", + year = 2015 +} + +@misc{agda, + title = {The Agda wiki}, + howpublished = {\url{http://wiki.portal.chalmers.se/agda/pmwiki.php}}, + note = {Accessed: 2017/10/24(Tue)} +} + + +@misc{agda-documentation, + title = {Welcome to Agda’s documentation! — Agda 2.6.0 documentation}, + howpublished = {\url{http://agda.readthedocs.io/en/latest/index.html}}, + note = {Accessed: 2017/10/24(Tue)} +} \ No newline at end of file