夜空日和 [出張版]

星を見上げながら、今日を語ってみようか

 

スポンサーサイト


Category: スポンサー広告   Tags: ---
上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

数学的なプログラム


Category: 技術   Tags: ---
[数学的に綺麗なプログラムではなく、数学のツールとなるプログラムのお話]

卒研でモデル検査というグラフ探査関連の研究をやっています。
厳密には「自動定理証明器」の分野らしいですが、そんなの知らないのでスルー。

私自信は「新しい理論を出す」ことよりも「実現的な理論とその実装を出す」方が好きです。
だから、数学的な問題の実装を考えようとかしちゃう訳です。

今回は、そんなお話。



モデル検査の中に、リージョンという概念があります。

厳密な定義は難しいので考えませんが、簡単に言っちゃうと
 「離散的な変化を実数で近似する物」
って感じです。例えば整数 0, 1 について、
 { x=0, 0<x<1 , x=1, 1<x }
という分割が行われます。

これは1次元なので簡単ですが、二次元になると、
  0<x<1 かつ 0<y<1

 { x=y , x<y, x>y }
の3つに分割されます。

これは、モデル検査では変数の関係を許可しているからです。
だから、例えば 「この部分では x > y でしか動作できない!」とか言われると、
最初の 「0<x<1 かつ 0<y<1」 では動作できるかどうか判断できないのです。


・・・と長ったらしく書いたところで。
この土日丸2日かけて、n次元のコレを計算するプログラムを書いてました。
捨てること前提で書いてたので、コピペばかりの500行です。

「内容が重複しないこと」 や 「絶対に漏れが無いこと」 を保証するために無駄にアルゴリズムを考えてました。
自分の解釈が正しければ、3次元までは保証されます。 (4次以上は人力じゃ無理w)

本当なら組み合わせを遅延評価できれば、もっと正確に計算できるアルゴリズムも思い付いたのですが・・・
C++での遅延評価の実装と、アルゴリズムの時間計算量に疑問があったので、今回はやめておきました。
次数5, 最大定数全部8だと数分で計算できます。 (ただし、結果が100MB超えます)


んで、これを卒研で使うのかと言われると。

使う予定はありません。

だから、書き捨てのプログラムなのです。
本当に使える物を書こうとしたら、1ヶ月以上は欲しいところです。
たぶん、本番では既存プログラムを書き換えることになるでしょう・・・(´・ω・`)
スポンサーサイト


Comments

Leave a Comment



08 2017
SUN MON TUE WED THU FRI SAT
- - 1 2 3 4 5
6 7 8 9 10 11 12
13 14 15 16 17 18 19
20 21 22 23 24 25 26
27 28 29 30 31 - -

07

09


 
プロフィール

ひでたそ

Author:ひでたそ
Comment:
現役大学生で天文好き。
今日もどこかで、上を見ながら歩いています。

 
 
 
最新トラックバック
 
 
検索フォーム
 
 
 
ブロとも申請フォーム
 
QRコード
QRコード
 

Archive   RSS   Login

上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。