Software in Mathematics Demonstration Track in Hakata Workshop 2014
Hakata Workshop(博多ワークショップ)~Discrete Mathematics and its Applications
九州大学 マス・フォア・インダストリ研究所
数学理論先進ソフトウェア開発室
Software in Mathematics Demonstration Track in Hakata Workshop 2014
Hakata Workshop(博多ワークショップ)~Discrete Mathematics and its Applications
九州大学 マス・フォア・インダストリ研究所
数学理論先進ソフトウェア開発室
研究対象の造船所では、造船工程計画をEXCEL上で手作業にて行っており、作業者 の負担となっている。そのため、当研究室では計画自動化を目指し、Max-Plus代数を 基にしたHEAPモデル法の提案を行った。 HEAPモデル法とは、使用するリソース（機械・資材）を横方向に、使用する時間を 縦方向に取ることで、パズルゲームのテトリスのブロックのようなピースとして表現 し、それを操作することで、リソースを厳格に管理しつつ計画を行う手法である。 本研究では、このHEAPモデル法を造船所の工程計画データへ適用するため、MATLAB を用いて、HEAPモデル法によるプル型スケジューリングプログラムの開発を行ってい る。 工程計画では、どの順番で製造するのか、製造した部品をどの区画へ蔵置するの か、という組合せ問題が無駄な時間の削減に大きく関わる。そのため、最終的には組 合せ問題を解きつつ、建造計画を立てるスケジューリングプログラムを開発する必要 がある。 今回は、HEAPモデル法の概要と、プル型スケジューリングプログラムを紹介する。
現在の機械翻訳は，SVO言語である欧米の言語の間では実用レベルに達している ようです．特に，文脈によって適切な訳語を選択し，滑らかな訳を作ることはう まくいっています． 一方，SVO言語を日本語などのSOV言語に訳す場合に，文法的な誤りが目立つよう になります． そこで私は、C言語等で構文解析の精度を高めた英文和訳ソフトを作っています． 品詞を特定し語順を変換し文型を表示し文法解説を付けるソフトです．今のとこ ろ登録している単語と文法事項に関してはほとんど間違えることはありません． 文型表示や文法解説を付けているので，英語教育ソフトとしても使えると思いま す． また和文英訳では，日本語を英文法の枠組みで構文解析することにより，日本語 にはない品詞を生成することを試みています．
このソフトウェアは、サッカー試合中のボールと選手の時間ごとの位置データか ら、主 に選手の守備範囲を同定したいとの依頼を受けて開発を始めた。現在は可視化が 必要で あるためJavaで記述している。 まず集団スポーツの研究では、選手の位置関係に基づく分析のために、縄張りを 表す計 算幾何の概念であるボロノイ図を応用した優勢領域図が利用されている。我々は これに 時間制限を設けた時間制限付き優勢領域図(Time-Restricted Dominant Region Diagrams,TRDRD) を提案している。 ボロノイ図はアルゴリズムの点からも比較的容易に求められるが、優勢領域図や TRDRD では選手間の境界を数値計算により求める必要があり、また選手の移動モデルが 数通り 考えられるので、数値微分を用いたNewton法(収束を保証するため2分法と併用) を利用 している。 現在はTRDRDの有効性を確認するため、TRDRDを用いて試合中に計測されるデータ を抽出 するモデルを構築し、実際のデータと比較している。
Two Java-based applications are presented. The first one (jPortRob) is about the financial model of portfolio optimization, which is known to be extremely sensitive to small perturbations in input data, especially asset expected returns (means). Through a simulation-oriented approach evaluating portfolios' performance through multiple scenarios of assets means, slightly and randomly derived from a nominal case, the aim is to select robust portfolios to errors affecting the means. The source of the considered portfolios is diverse, namely the evolutionary algorithms plus quadratic programming procedure. On the other hand, the second application (GetAssetsDataSet) is an automatized downloader for market asset prices. Based on Selenium, which is a software framework for automate web browsers usually used for testing purposes of web applications, the application allows the user, for input parameters as the beginning and end date of data, the frequency of data plus asset names, to download multiple financial prices in a short time. Keyword: financial engineering, portfolio optimization, robustness assessment, simulation model.
重み付グラフの埋め込み手法の一つであるラプラシアン固有マップ法の改善方 法を提案した．具体的には，低次元ユークリッド空間に埋め込むとき，各軸の価 値を定義し，それに応じて縮尺を改善した．利用の例としては，移動時間だけが 与えられた交通網から，妥当な都市配置を推測することが可能である． また応用として，補間手法の一つSpectral-Based Interpolation(以後 SBI)が 適用できる範囲を簡易的に広げた．この手法は，人間のように集団を意識した動 きを補間可能である．しかし，補間対象はユークリッド空間上の点集合のみで あった．そこで，範囲を重み付グラフ上に簡易的に広げた． 以上の内容を視覚化するためR言語を用いて，「改善を施したラプラシアン固 有マップ法と従来のものを比較するプログラム」および「重み付グラフ上へ拡張 したSBIの補間結果の例をアニメーションで表示するプログラム」を作成した．
オートマトンと言語理論に現れる対象や関数を証明支援系言語Coqを用いて実装しその性質に形式的証明を与えた。言語に現れるアルファベットは有限集合であるが、言語そのものは無限集合であり、その列挙プログラムは停止しない。無限の要素を持つ言語の性質はCoqの拡張系であるssreflectを用いて機能的に証明される。DNA計算モデルの一つであるスティッカー系もCoqによって実装した。 PaunとRozenbergはオートマトンをスティッカー系へ変換する具体的な手続きを1998年に提案している。我々の目標の一つは、PaunとRozenbergが与えた手続きの正しさを形式的に証明することである。証明には我々が作成したオートマトンとスティッカー系のCoqによる実装を用いている。 今回のデモでは、さらにCoqを用いたオートマトンやスティッカー系の簡単な命題の形式証明とその自動検証例をいくつか示す。