2012/09/13にくいなちゃんさん主催で開催された6さいカンファレンスのまとめ。 第2回は「数学の定理を自動で発見するAI を Haskellで作ろう！」です。 勝手にまとめてしまったので、何か問題があれば@shogo82148まで。 WELCOME TO HELL!! くいなちゃん: それでは、まず、数学の「定理」とは何か、について説明したいと思います。 みなさん、日常的に「定理」という言葉を使っていると思いますが、「定理」とは何か、説明できますか くいなちゃん: 「教科書に載っている公式が、定理だ！」と思うかもしれませんね。 確かに、教科書にも定理は載っています。 くいなちゃん: では、曖昧な理解の方のために、厳密かつ ゆるふわに説明しましょう。 くいなちゃん: 定理とは、次のように定義できます。 公理であるならば、定理である。 定理を推論規則によって推論したものは、定理である。 以上。 くいなちゃん: はい、みなさんこれで定理が何かを理解したと思いますので、数学の定理を自動で発見するAIを作ろうと思います。 くいなちゃん: Haskellで。 Haskell! くいなちゃん: そもそも、Haskellって何？ という方もおられるかと思いますので、まずは Haskell について簡単に説明しておきたいと思います。 くいなちゃん: Haskell は、関数型言語です。 宣言的プログラミングによって、プログラムしていくプログラミング言語です。「○○は××である！」というのを繰り返してプログラミングする感じですね。　「まずは○○して、次に××しろ！」という C言語(手続き型言語)とはかなり異なります。 くいなちゃん: では具体的に、今回定理を発見するための数学の体系を説明しながら、同時に Haskell で実装してみることにしましょう。 くいなちゃん: 最終的には 大規模な数学体系の定理を発見するとしても、まずは試しに小さな体系で定理を発見してみることを考えます。 今回は、命題論理を対象としてみます。 定義 くいなちゃん: では、今回対象とする命題論理を、厳密に定義していきましょう。 まず、この体系で用いられる記号は、P　Q　R　￢　⇒　の5種類です。 この5種類をうまく並べると、この数学体系でのあらゆる式や命題が記述できます。 くいなちゃん: まあ、たとえば、　P⇒P　(PならばPである)　といった感じですん。 わかりますね。 くいなちゃん: ￢　は数学における否定によく使われる記号ですが、いまのところ、単なる記号にすぎず、意味は定義されていません くいなちゃん: ちなみに、くいなちゃんはポーランド記法が好きなので、　P⇒P　を、　⇒PP　と書くことにしましょう

だいぶ時間がたってしまったけど、2012/09/06にくいなちゃんさん主催で開催された6さいカンファレンスのまとめ。 第1回は「C言語で作る、はじめてのDAWソフト制作」です。 勝手にまとめてしまったので、何か問題があれば@shogo82148まで。 BATTLE START!! くいなちゃん: みなさんは、既にC言語の基本的なところはマスターしていると思いますが、念のために軽く復習しておきましょう。　まずは、このソースコードをご覧ください。 http://kuina.tes.so/6saiconf/a.png(魚拓) #include <stdio.h> #include <math.h> int main(void) { return 0; } くいなちゃん: 右下の100% は気にしなくてOKです。　このプログラムは、「何もせず終了するだけ」のプログラムとなっています。　ソースコードを順に解説しましょう。 くいなちゃん: まず、1行目と2行目に書かれている #include ですが、これはおまじないです。　プログラムの本質は、4行目からとなります。 くいなちゃん: int main(void) { } が、プログラムの本質となります。　コンピュータがこのプログラムを起動すると、int main(void) { } の { と } に囲まれた部分を上から順に実行していきます。 } に辿り着いたら終了です。 くいなちゃん: よって、このプログラムは、 return 0; を実行するだけのプログラムとなります。　return 0; とは、おまじないです。　えへへ☆ DAWを作ってみる くいなちゃん: はい、もう、C言語の基本的なところは全てマスターできましたね。　では、早速 DAWソフトを作ってみましょう。 くいなちゃん: DAWとは、簡単にいいますと、曲を作るソフトです。　それでは、int main(void) { } の中に、DAWっぽいプログラムを書いていきましょう。　とりあえず、int i, j; を書きます。

先週土曜日は第28回NDS(長岡技術者勉強会)でした。 スーツ vs ギーク Togetterのまとめを見ながら、内容を頑張って思い出してみる。 (せっかくローカルでブログ書ける環境作ったんだから、ちゃんとメモっとくべきですね・・・と思いつつ毎回できない) プログラマは誰でもいい？ 人に依存しないことはいいこと でも、本当にそれでいいの？ 能力があれば誰もいいのかも 社長の方が誰でもいい (自称)ギークなスーツ 「これからはHadoopらしいよ」 ギークにもユーザの対応して欲しい 「技術的な制限で無理」なことを説明するときとか 浅い知識だけでは矛盾点を突かれて、Yesと言わざる負えない時も 「ときどき行く→ギーク行くといいじゃんってなる→ときどきが毎回になる」と困るよね 判断を全部ギークに丸投げしないで！ 例えば、初期コストを取るか、拡張性を取るか、とか 技術的な利点・欠点は説明するけど、実際どっち使うかの判断はスーツな人にお願いしたい スーツを手玉に取るコミュ力 コミュ力の低いギークは技術力を生かせなくてもったいない！ ギークもコミュ力を身につけるべき 名選手と名監督は両立しない 技術者からの叩き上げでマネージメントする側になった人は他人を上手く使えない マネージメント系は手足のように他人を使えなければならない 社会は怖いところです。 通常セッション マッチョ見積もり by @hiro55bsさん 「つまり、見積りは予想ではなく、帳尻をあわせるものなんだよ！」 見積もりはリスク管理、プロジェクト初期だけでなく随時やっていくもの プロジェクト初期では見積もりに幅があって当然 もる いろんな統計データからざっくり見積もれるんですね。勉強になります。 ワンライナーでノイズミュージック by @neko_gata_sさん Experimental music from very short C programsに触発されたというお話 RIFFヘッダつけるとこは Perl でやってます！ 波といえば正弦波の組み合わせで・・・と思っていたので、ビット演算で音を出してみるというのはおもしろいです。ぜひやってみたいです。 LT SIの現場から感じた未来 by @nemuzukaさん 現在の契約形態に対する問題提起 皆さんで考えて行きましょう RubyMotionでiOSゲームを作るっきゃない by @jewel_x12さん Pythonが主人公のゲーム Android版はまだですか？ Echigo Network Operators’ Group について by @yyasuyukiさん コイントスで決めよう お姉さんのコンピュータを高速化したお話 補足とか スライド上げようと思ったんですけど、よく考えたら半分他人さまの画像使ってるのであまりよろしくないですね。 検索アルゴリズムの紹介などは「おねえさんのコンピュータを作ってみた」を ご覧ください。

まだやってたのか、と言われてしまいそうですが、おねえさんが計算にかけた時間と比べればまだまだです。 『フカシギの数え方』 おねえさんといっしょ！ みんなで数えてみよう！ この動画で出てくるおねえさんのコンピュータを作ってみた、というお話。 おねえさんのコンピュータからアクセスできます。 検索アルゴリズム HTML+CSSでコンピュータの画面を再現してみました。Javascriptを組むより、そっちの方に時間がかかった気がする。 経路の描画にはCanvasを使ってます。 この問題は自己回避歩行(Self-avoiding walk)と呼ばれるものらしいです。 単にグラフ上を移動するだけなので、小さいなサイズなら単純な深さ優先検索(DFS)で解けます(大きなサイズで何が起こるのか・・・それは動画で)。 実装では、DFSによる検索プログラムをWeb Workerを使って走らせ、スタートとゴールを結ぶ経路を見つけたらメッセージを飛ばしてます。 さすがに全部は表示できないので、実際に表示するのは50ms秒程度の間隔。 4×4以下ではそれだと速すぎて何が何だかわからないので、待ち時間を入れてある。 さあ、君も10×10にチャレンジだ！！ おねえさんに教えて上げよう！ しかしながらDFSだけだとなんだか負けた気がして悔しいので、高速化したアルゴリズムも試してみた。 「おねえさんに教えてあげる」のチェックボックスにチェックを入れると高速化したアルゴリズムで問題を解きます。 ゼロサプレス型二分決定グラフ 自分が色々試行錯誤している間に他の人が解いてしまった(「フカシギの数え方」の問題を解いてみた) ので、それを参考に実装してみた。 今回の問題は「グラフ上の経路問題」ですが、どの枝を通ってどの枝を通らないかという「枝の選択問題」として考えることができます。 その組み合わせを効率良く表すための方法が、ゼロサプレス型二分決定グラフ(ZDD; Zero-Suppressed Binary Decision Diagram)。 ZDDは数学の組み合わせでよく使う樹形図の一種で、 同じ結果になる枝を集めることで樹形図を効率良く表したものです。 概要はBDD/ZDDを基盤とする離散構造と処理演算系の最近の展望 を参照。 もっと詳しい説明はThe Art of Computer Programmingに書いてあるらしい(まだ読んでない)。 ZDDを考えた湊先生は最初の動画の企画・監修も努めている方なので、 動画中の数値もZDDを使って求めたものと思われます。 Simpath ZDDは単なる組み合わせの表現方法なので、別途グラフからZDDを求める手法が必要になります。 これに関する簡単な解説がZDDを用いたパスの列挙と索引生成 から見られます。 上のセミナー資料ではZDDの基本演算を使った列挙の方法が紹介されているけど、 今回はクヌース先生のSimpathを採用。 Simpathでは(既約でない)ZDDを作ることができます。 経路の両端にのみ着目し、この情報をmateという配列で管理。 frontierと呼ばれる頂点のmateを用いてZDD上のノードを共有することで簡略化を行います。 実際使ったアルゴリズム セミナー資料では幅優先でノードを作ってみるように見えるけど、今回の実装では深さ優先で経路数だけカウント。 ZDDのノードを作るのが面倒だったんです。 しかし、覚えなければならないmateが大量になってしまいメモリがああああ！！ すべて覚えるのは諦め、一部のmateだけ覚えるようにしました。 「おねえさんに教えてあげる」のチェックを入れると、適当実装のSimpathで計算します。 計算中一部の枝が灰色になるのは、ZDD上でノードの共有化が行われたため、実際には枝が処理されなかったためです。 格子上の点に丸がついているのはfrontier。 この点の継続情報を用いて共有化を行います。 まとめ おねえさんのコンピュータの実装と高速化を行いました。 高速化の結果、処理に数分かかっていた6×6の計算が200msで終わるようになりました。 10×10も1分程度で終わります。 ただ、表示のためのオーバーヘッドがあるとはいえ、他の人と比べると少し遅いような。 なにか実装間違っているかも。 The Art of Computer Programmingを読んで勉強しないとかな。

Vagrant VagrantはコマンドラインからVirtualBoxを扱えるようにするツール。 仮想マシンの起動・再起動をコマンドライン上から行えるのはもちろん、Chefや Puppet と連携することで必要なソフトウェアのインストールを行なってくれます。 Vagrantを使うには仮想マシンのひな形であるBase Boxが必要です。 Vagrantbox.esにいろんなOSのBoxがあるけど、 インストールされているOSのバージョンが古かったり、タイムゾーンがUTCになっていたりして 不具合発生。 そこでBoxを自分で作ってみようと思い立ち、やってみたのでそのメモ。 作ったBoxは GitHub にあげておいたので使いたい方はどうぞ。 Ubuntu 12.04.2 Server + VirtualBox 4.2.10 で作ってあります。 vagrant box add myubuntu https://shogo82148.github.io/boxes/ubuntu-12.04.2-amd64.box VeeWee VeeWeeはBoxの作成を自動化してくれるツール。 OSのインストール、不要なパッケージの削除、Box化なんかを自動でやってくれるらしい。 VagrantとVeeWeeのインストール Rubyの実行環境とVirtualBoxのインストールを済ませたら、 gemを使ってVagrantとVeeWeeをインストール。 gem install vagrant gem install veewee 使ってみる vagrant basebox templates と打つとテンプレートの一覧が出てくる。 現時点でのUbuntu最新版であるUbuntu 12.04をテンプレートとして使ってみる。 vagrant basebox define myubuntu ubuntu-12.04-server-amd64 これでdefinitions/myubuntuの中に設定ファイルができる。 そのままだとisoのダウンロードで404が帰ってくるので設定ファイルを書き換え。 加えて日本語が使えるようにLocaleをja_JPに、タイムゾーンをAsia/Tokyoにしておく。 --- templates/ubuntu-12.04-server-amd64/definition.rb 2012-08-31 18:23:28.000000000 +0900 +++ definitions/myubuntu/definition.rb 2012-08-31 21:17:52.000000000 +0900 @@ -6,8 +6,8 @@ :hostiocache => 'off', :os_type_id => 'Ubuntu_64', :iso_file => "ubuntu-12.

Octopressでツイートを引用しようと思ったけど 使えそうなプラグインがなかったので作ってみた。 ツイートに限らずいろんなものを挿入できるよ！ OEmbed 調べてみるとツイートの表示はOEmbedというのを使うとできるらしい。 これはURLを埋め込み適した形に変換してくれるプロトコル。 ツイートのURLから引用のためのHTMLを作ったり、YouTubeのURLから動画再生用のHTMLを作ることができる。 せっかくだからOEmbedに対応してしまえばいろんなものを埋め込めて便利だよね！ってことでやってみた。 インストール ruby-oembedをインストール。 gem install ruby-oembed ruby-oembedは名前から想像できる通り、RubyでOEmbedプロトコルを扱うためのライブラリ。 Provider(OEmbedの提供者)を自分で追加したり、Discovery(HTMLドキュメントにProviderの情報を入れる)にも対応している。 しかし、プロキシ環境下で動かなかったり、文字コードのエラーを吐いて死んだりしたので、 フォークして改造版ruby-oembedを作った。 もしオリジナルで不具合が出るようなら、こちらもどうぞ。 oembed_tagからoembed_tag.rbをダウンロードして、pluginsフォルダに置く。 Gemfileを適当なテキストエディタで開き、「gem ‘ruby-oembed’」の行を追加 source "http://rubygems.org" group :development do gem 'rake' gem 'rack' gem 'jekyll' gem 'rdiscount' gem 'pygments.rb' gem 'RedCloth' gem 'haml', '>= 3.1' gem 'compass', '>= 0.11' gem 'rubypants' gem 'rb-fsevent' gem 'stringex' gem 'liquid', '2.2.2' gem 'ruby-oembed' #追加 end gem 'sinatra', '1.2.6' これでとりあえずは動くはず。 以上の作業に加えて、キャッシュファイルがリポジトリに含まれないよう.gitignoreに.oembed-cacheを追加しておく。 使い方 以下の様に書くと、適切な埋め込み方法をWebから取得して変換してくれる。 &#123;% oembed URL %&#125; 例 Twitter &#123;% oembed https://twitter.

久しぶりにOMakeを使おうと思ったら、使い方を忘れてしまったので復習。 基本的な流れ 初期化 OMakeのインストールはaptitudeやyumやDownload OMakeあたりで頑張る。 OMakeがインストールできたら、まずは初期化のおまじない。 omake --install カレントディレクトリにOmakefileとOmakerootが作られる。 自分のプロジェクト内容に合わせてOmakefileを編集。 具体的な例は後述。 ビルドする 単に「omake」と打つとビルド omake 継続監視ビルド 「-P」オプションで継続監視ビルド omake -P 関連するファイルを監視して、変更があれば自動的にビルドしてくれる。 キャッシュの削除 OMakeでビルドすると環境依存なパスの設定とかを書き込んだファイルが作成される。 Dropboxなどの同期ソフトはこれらの設定ファイルも同期してしまうので、 別環境で作業しようとするとエラーを吐いて止まってしまう。 次のコマンドでキャッシュファイルを無視すれば大丈夫。 omake --flush-includes Omakefileの例 TeXの文章をビルドするOMakefileの例。 LinuxとWindowsでデフォルトの文字コードが違って面倒なので、文字コードはutf-8に統一。 PDF出力はA3サイズ。 {% gist 3300749 OMakefile %} prosperを使ってプレゼン資料を作った時のOMakefile。 dvipdfmでは処理できない場合があるので、一度PostScriptにしてからPDFに変換するようにルールを上書き。 数式を多用するようなプレゼン資料だと便利。 {% gist 3300749 OMakefile-slide %} 参考 OMake つかったらC言語でプログラム書く手間がバカみたいに減った OMake つかって LaTeX コンパイルしたら簡単すぎて身長が5cm伸びた OMake マニュアル日本語訳 omakeが動かない …. 動いた [卒論] LaTeXのビルドにOMakeを使ってみた おまけ Dropboxと連携するとこんなことも。 Dropboxで同期しているフォルダで、「omake -P」を実行して自動コンパイルする設定のまま放置してきちゃった。別のPCでソース書き換えると、Dropboxが同期→リモートのomakeが自動コンパイル→Dropbox経由でコンパイル結果が帰ってきた。 — Ichinose Shogoさん (@shogo82148) 9月 27, 2011

さあ、皆さん！今年も長岡の大花火大会の季節がやって参りました！ 花火大会といえば、 光と音の速度差を体感できる絶好の機会です。 というわけで、去年もこんなアプリを作って遊んでました。 このアプリを頑張って改良したので、改めて紹介したいと思います。 アプリをダウンロード 使い方 起動すると、こんな画面が表示されます。 花火が開いたら画面をタップ！ そして、花火が画面中央に来るよう素早く端末を動かします。 (※画像ははめ込み合成です) 花火の音がしたら、目標をセンターに入れてタップ！ タップの間隔から花火までの距離を計算し表示してくれます。 さらに、加速度センサの値から端末の仰角を読み取り、花火の高さや水平距離などを算出してくれるという機能もついてます。 去年からの変更点 と、ここまでは、去年と一緒。 今年はさらにパワーアップしました。 地図へのマッピング スマートフォンには磁気センサがついており、方位が分かります。 加えて、GPSもついているので、スマートフォンの現在位置も分かります。 これだけの情報が揃えば、地図にプロットできるはず！ 結果表示の画面で「地図を表示」を選ぶとマッピングしてくれます。 この画面でメニューキーを押すと、TwitterやGoogle+などで、花火の位置をみんなに知らせることもできます。 GPS測位ができない場合は、デフォルトの位置を使用します。 この位置は設定画面で変更できます。 自動花火検出 去年からの課題であった、花火の自動検出も試みてみました。 初期画面でメニューキーを押すと設定画面へ飛べます。 ここで「花火を自動的に検出する」「花火の音を検出する」を選択すると、自動検出してくれるはずです(※理論値)。 花火が開いたことは、画面が明るくなったことで検出します。 明るさの検出は初期画面中央の四角の中が使われます。 設定画面でこの四角の大きさを変えることができます。 明るさの変化が閾値を超えたら測定開始です。 音は音量で検出します。 音声にDFTをかけて、周波数フィルタリングをかけてあります。 これで人ごみにまぎれても花火の音が検出できる・・・はず。 周波数0Hzにすると、周波数フィルタを通さずに振幅のみで判定します。 検出した値は、画面の右上に表示しているので、設定の時の参考にしてください。 ダウンロード アプリをダウンロード 野良アプリなので、「設定→アプリケーション→提供元不明のアプリ」をチェックする必要があります。 スマートフォンの機能をフル活用するので権限をたくさん要求してきますが、きっとだいじょうぶ。 そろそろマーケットでの公開も試してみたいですね。 ** Google Play にリリースしました！ ** Google Play からアプリをダウンロード まとめ それでは、大幅に機能UPしたアプリと一緒に、長岡の大花火大会をお楽しみください。 打ち上げはこのあたりらしいです。 ちゃんとマッピングできますかね？

背景・目的 なぜだか研究室のWiFi経由でSSHが通らないので、 GithubがBitbucketに繋がらない＞＜。 有線LAN経由なら通るので、ネットワークの問題だと思うのですが、 よくわからないのでとりあえずHTTPS経由で頑張ることにしました。 うちの学校ではHTTPSで外部に出るにはプロキシの設定が必要です。 そういうわけで、Gitでプロキシを使う方法を調べて見ました。 方法 .ssh/config に以下の設定をしました。 Host github.com User git Port 22 # or 443 Hostname github.com # or ssh.github.com IdentityFile /path/to/ssh.key TCPKeepAlive yes IdentitiesOnly yes ProxyCommand nc -X connect -x proxy.example.com:8080 %h %p 参考文献 git pull/push to github.com in proxy environment http proxy 越えの ssh SSHでプロキシ経由でアクセス

第27回NDS(長岡技術者勉強会)に参加してきました。 Gitハンズオン 今回はNiigata.scmとのコラボで GitハンズオンといつものLTの二本立てでした。 @masaru_b_clさんのGitの歴史や利点についての解説の後、 @dictavさんによる解説・演習。 addしてcommitする logやreflogでログ確認 reset –hard で元に戻す merge rebaseでコミットログを一本道に あたりをやりました。 一つのファイルの同じ行を20人でいじるという怖いこともしました。 凄まじいコンフリクト発生頻度と、すごい勢いで分岐していくログ。 実際の現場であったら恐ろしいですね。 gitはプラグインが使えるので、いろんなプラグインが出てます。 今回紹介があったのはgit-nowとgit-master。名前だけは聞いたことあるんだけど、使ってみますかね。 git-now masuru_b_clさんバージョン git-master あと、コミットログ英文の書き方とか Changelogのための英文テンプレート集 ust Gitの説明 ust 午前の演習その1 ust 午前の演習その2 ust 午後の部 push戦争 いつものLT 電子国土と地形図(その後) (@yu_hori)[http://twitter.com/yu_hori]さん NDS23での電子国土地図の発表の続き。 利用者にとって価値ある使いやすい電子国土基本図を目指して(中間提言) 電子国土ポータル 長岡にギークハウスを @geek_niigataさん やったーPICで作曲できたよー＼(^o^)／ @aokcub うおおおおおおおおおお！！！！ 期待の21世紀枠最後の昭和枠 NDS27に参加してきたよ！よ！ git-svn @masaru_c_blさん svnのリポジトリをgitにしてしまう奴。 ソフトウェアメトリクス調査2012を読み解く @hiro55bsさん ソフトウェアメトリックス調査2012 COBOL… 品質が低いと顧客満足度も低いけど、逆に品質が高すぎても顧客満足度は低い お客さんの要望に十分に答えられないのが原因？ やったーPerlでにゃん読化ツールできたよー＼(^o^)／ @neko_gata_sさん Niigata.pm 遊びに来てね NDSから大切なお知らせ @civicさん プロジェクトアンブレラ Niigata.pmはNDSの傘下 SRNDS(それNDSでできるよ) PSO aokcubさんの使ってたPSO面白そうだったので現実逃避に実装。 実際の効果はよくわからない。 初期値の時点でミニマムの近辺から外れると、ローカルミニマムに落ちることもしばしば。 それなら最急降下法でも・・・という気もしないでもない。 問題設定が悪いのか、パラメータが悪いのか。