先週に続いて、Categories for the Working MathematicianのAbelian Categoriesの章で勉強している。
ExercisesのThe middle 3×3 lemmaを証明しようとしたのだが、どうにも証明できそうにない。
問題文曰く、上の図式の全ての列、それに第一行と第三行が短完全列ならば第二行も短完全列であることを証明せよ、だそうだ。与えられた短完全列の両端に0を付加すると次の図式になる。
手始めに、真ん中の行の2つの射を合成すると0となることを証明しようとしたが、どうにも方法が浮かばない。先週は勘違いでさんざん悩んだので、これはもしや成り立たないのではないか、と思って、調べてみることにした。（反例を考えるのは面倒くさかった）
手持ちの別の本を参照したところ、真ん中の行の2つの射を合成すると0となることは仮定しなければならないそうである。反例もあった。ググって出てきたnLabの項にも書かれていた。
せっかく作ったブログをいつまでも放置するのもアレなので、最近勉強していることを書くことにする。
先学期の授業で登場したけど全然理解しないまま終わったホモロジーとかを理解したくて、どうせやるならと思ってアーベル圏の勉強をしている。本はCWMの、アーベル圏の章を進めている。
アーベル圏というのはどういう圏のことを言うのかというと、単純なものから順に定義を書いておくと
各 hom-set にアーベル群の構造が入っていて、射の合成が bilinear になっている圏を preadditive category という。CWMでは Ab-category と呼んでいる。
Kernel, cokernel や biproduct などの概念を定義することができる(kernel, cokernel は preadditive category でなくても、ゼロ射さえあれば定義できる)。
Preadditive category であって、ゼロ対象と biproduct (直和) をもっている圏を additive category という。
Additive category であって、全ての射が kernel と cokernel を持っていて、全ての monic 射が kernel であり、全ての epi 射が cokernel である圏を abelian category という。
Abelian category では、射の image や coimage の概念を定義することができる。また、完全列の概念も定義できる。
…という風になる。
アーベル圏で完全列を定義できるということは、five lemma とか snake lemma を定式化できるということである。この辺のレンマの証明は、CWMではアーベル圏の章のセクション4に書かれている。
このセクションの最初の方にアーベル圏 A の短完全列の圏 Ses A が加法圏であるとさらっと書かれているが、最初に読んだときに Ses A もアーベル圏なんだと勘違いして証明を考えるのに数週間費やしてしまった。おかげで図式の扱いには慣れた気がするし、短完全列の射のカーネル、コカーネルがどうなるのかという話はスネークレンマに繋がってくるとはいえ、とんだ時間の浪費だった。
アーベル圏を勉強する前は、授業などでこれらの補題の証明にいわゆる “diagram chase” を使っているのを見て（加群の圏上ではあったが）、
「元を取ってdiagram chaseなんてしたら圏論的な証明にならないのでは！？」
と思っていたが、蓋を開けてみたら、一般のアーベル圏上で「元」に相当する概念を定義して、その「元」に対して monic や epi がそれぞれ普通の単射、全射と同じような振る舞いをすることを証明し、five lemma や snake lemma などの補題の証明では元を取って証明していたのだった。もちろん、圏論的な証明であるから、「dual を取って証明の半分を省略する」というようなことはできる。
この記事では、連続撮影した静止画を動画に変換する方法について書く。状況としては、微速度撮影・タイムラプス撮影のように、カメラで写真を一定時間ごとに撮影したものを動画にしたい、というものを想定している。
ここで使うのはffmpegという、動画や音楽ファイルのフォーマットを変換するのに使われる無料のプログラムである。マウスで操作するようなGUIはついておらず、コマンドラインからコマンドを叩いて使う。ffmpegのインストール方法は割愛する。
この記事を書いている時点でのffmpegの最新版は2.2.1なので、ffmpeg 2.2.1の使い方について書く。おそらく、多少バージョンが違っても同じように使えるのではないかと思う。
まず、動画の各コマとなる静止画を用意する。適当にフォルダを作って、その中に使いたい画像をコピーする。静止画の形式はJPEGにしておく。ファイル名は連番になるようにする。
ターミナルを開き、先に画像ファイルを準備したフォルダに移動する。ffmpegコマンドの使い方はおおざっぱに言うと
ffmpeg [入力に関するオプション] -i (入力ファイル名) [出力に関するオプション] (出力ファイル名)
となる。以下、オプションの詳細について。
入力に関するオプション・入力ファイルの指定
-framerate (rate)
-s:v (size) または -video_size (size)
(幅)x(高さ) の形で指定する。あるいは、 vga や hd720 のような名前も使える。詳しくは公式のドキュメント(英語)を参照。-start_number (n)
-i (ファイル名)
IMG_nnnn.JPG という形をしていれば、パターンとしては IMG_%04d.JPG を指定する。出力に関するオプション・出力ファイル名
-r:v (fps)
-s:v (size)-b:v (bitrate)
k (103)や M (106)などの接尾辞も使えるようだ。-vcodec (codec) または -codec:v (codec)
mpeg4 や h264 など。利用できるコーデックはffmpeg -codecs で確認できる。オプションの一部は入力にも出力にも指定できる。入力と出力に異なるフレームレートを指定した場合、一部のコマが複製されたり取り除かれたりする。各コマのサイズは入力と出力どちらにも指定できるが、どちらに指定するとどう変わるのか筆者はよく分かっていない。
コマンドの実行例は、例えば
ffmpeg -framerate 24 -start_number 7836 -i 'IMG_%04d.JPG' -r:v 24 -b:v 10M -s:v 1080x720 -vcodec mpeg4 output.mov
となる。この場合、IMG_7836.JPG から始まる連番のファイルが処理対象となり、出力ファイルは output.mov となる。
distccという、ネットワーク越しに複数のマシンを使って分散コンパイルを行うツールがある。これを使うと、最低限の設定で、同じアーキテクチャ・OSのマシン複数台での分散コンパイルができる。だが、アーキテクチャ・OSの異なるマシンを使いたい場合はどうか。その場合はクロスコンパイラを使う必要がある。
しかし、全てのマシンにクロスコンパイラを導入するのは面倒である。特に、ビルドしたいターゲットの環境のGCCがパッケージ管理システムに登録されていない場合は、わざわざ自前でGCCをビルドしなければならない。これはできればやりたくない。
そういう時は、コンパイラとしてclangを使おう。最近のclangは、-targetオプションを指定することでクロスコンパイラとして使うことができる(昔は-ccc-host-tripleだった)。clangは大抵の環境でパッケージとして用意されていると思うので、容易に導入できるだろう。-targetオプションに指定する文字列は、$ clang --versionで出てくる文字列を使えば良いだろう。
例えば、必ずしもMacばかりではないマシンを使って、Mac向けのプログラムをビルドしたい場合、configureには次のようなオプションを与えれば良い:
$ ./configure CC="distcc clang -target x86_64-apple-darwin13.1.0" CXX="distcc clang++ -target x86_64-apple-darwin13.1.0"
ただし、DISTCC_HOSTSなどの環境変数は適切に設定されており、ビルドに使うマシンではdistccdが動いているものとする。あとは$ make -j10のように適当に並列ビルドのオプションを指定すれば、適当に分散コンパイルしてくれる。
distccにはプリプロセッサの処理も分散させるpump modeという動作モードがあるが、どうも-targetオプションには対応していないようで、うまく動いてくれなかった。
自分で使ったときのメモ。備忘録。
入力を1.jpg, 2.jpg, ..., n.jpg、出力をoutput.jpgとする。
加算合成：
$ convert 1.jpg 2.jpg ... n.jpg -background none -compose plus -flatten output.jpg比較明合成：
$ convert 1.jpg 2.jpg ... n.jpg -background none -compose lighten -flatten output.jpg2つの画像が切り替わる（2コマ）アニメGIFを作りたい。
1コマ目をa.png, 2コマ目をb.pngとし、0.01*t 秒で1コマ目から2コマ目に切り替わるとする。繰り返しはしない。
$ convert -delay t -loop 1 a.png b.png output.gif-loop 1を-loop 0に変えると無限ループになる。詳細はこの辺とかを参照。
東大の後期課程や大学院に在籍する人は必ずお世話になるであろうUT-mateだが、その使い勝手はお世辞にも良いとは言えない。まず、ログイン画面でEnterキーを押してもログインできない。他にもいろいろある。
さて、世の中のWebブラウザには、ユーザー側でWebページの見た目とか使い勝手をいじくれるものがある。Firefoxの場合はGreasemonkeyという拡張機能をインストールすれば、そういう”user script”を導入できるようになる。つまり、Greasemonkeyを導入したFirefoxであれば、user scriptによってUT-mateのページを構成するHTMLとかをいじることができ、使い勝手を向上させられる可能性があるということだ。（他のブラウザは筆者はあまり使っていないのでこの記事では扱わない）
というわけで私が書いたuser scriptがこれ→Better UT-mate.user.jsになる。Greasemonkeyを導入済みであれば、このリンクをクリックすることでこのuser scriptをインストールできるはずだ。ソースを見れば分かる通り、至極簡単なスクリプトであって、怪しい動作はしない。
現在のところ、実装している機能は
である。気が向いたらさらに機能を追加するかもしれない。
【2015年9月3日】GitHubに公開。user scriptへのリンクをGitHubのものへと変更。
デジカメで撮った写真の転送については先の記事に書いた。この記事では、撮影時の連携について書く。デジカメと書いているが、ここに書くような連携に対応しているのはほとんどがデジタル一眼レフカメラだと思う。
デジタル一眼レフとパソコンをUSBで繋いで連携させる話は知っているだろうか。デジタル一眼レフに繋いだパソコンでライブビューができたり、パソコンで設定をいじって撮影できたりするアレだ。もしも携帯端末がUSBホストに対応していれば、携帯端末で同じことができる。
USBホスト付きAndroid端末でデジタル一眼レフを制御する例はググるといくつか見つかったが、iPadでそれをしたという情報は見当たらなかった。iPadでは技術的に不可能なのか、それともAppleの制限が厳しくて許可されていないのか、あるいは単に誰もアプリを作っていないのかは知らない。ここでは、USBホストを搭載したAndroid端末での話をする。
Android端末に搭載されているのはmicroUSBポートなので、適切な変換ケーブルを介してデジタル一眼レフに繋ぐことになる。この用途に使えるAndroid側のアプリとしては、Canon製一眼レフ向けではDSLR Controller (BETA)(有償)というのが定番のようだ。他社製一眼レフカメラについては、少なくともNikon向けのものはアプリがあるようだ(Helicon RemoteはCanon製カメラと一部のNikon製カメラに対応。アプリは無料だが全ての機能を使うには有償のライセンスが必要)。
多くのデジタル一眼レフカメラはワイヤレスリモコンに対応している。別途発売されている専用ワイヤレスリモコンを使えば、ワイヤレスでシャッターを押せるというわけだ。このワイヤレスリモコンは赤外線を使っているので、もしお手持ちの携帯電話が赤外線通信に対応していれば、わざわざ専用のワイヤレスリモコンを買わなくても携帯電話をワイヤレスリモコンとして使える可能性がある。
iPhoneが赤外線通信に対応していないのは周知の通りである。ではAndroid端末はどうかというと、赤外線通信に関するAPIはAndroid標準ではなくメーカーの独自機能になっている。シャープは赤外線通信・リモコンに関するAPIを公開(ここから参照)しているので、赤外線機能のついたシャープ製端末についてはアプリを作ることで端末を赤外線リモコンとして使えるようになる。
そのようなアプリはもうすでにあって、IRリモコン for DSLRやNexRemoteがある。どちらも、カメラの方は複数のメーカーに対応しているが、端末の方はシャープのみである。
シャープ以外の携帯電話メーカーが赤外線に関するAPIを公開しているという話は聞かないので、シャープ以外の端末向けにこのようなアプリを作ることはできなさそうだ。古き良きフィーチャーフォン(ガラケー)はキャリアごとにその辺の仕様が決まっていたので、フィーチャーフォン向けのアプリでカメラ用のリモコンアプリを作ることは一応可能だろうが、実際にそういうアプリが存在するのかは筆者は知らない。
携帯端末本体に赤外線通信機能がなくても、イヤホンジャックなどを使って赤外線LEDを外付けすることはできる。イヤホンジャックに付けた赤外線LED向けのリモコンアプリを作ることは一応可能だろうが、あるのかどうかは筆者は知らない。
デジタル一眼レフのリモコンとしては、赤外線リモコン以外に有線リモコンもある。しかし、有線リモコン用の端子は大抵メーカー独自なので、出来合いのケーブルを使って携帯端末と繋ぐことはできない。
ただ、もちろん電気的にはとても単純だと考えられるので、頑張ればスマートフォンなどのイヤホンジャックなどにつなげるケーブルを作ることはできるだろう。健闘を祈る。
SmartTriggerという製品があって、iPhoneからデジタル一眼レフカメラのシャッターを押せるらしい。iPhoneとSmartTriggerの間はBluetooth LEで繋ぎ、SmartTriggerとデジタル一眼レフカメラは有線リモコンの端子、または赤外線で繋ぐようだ。
理想を言えば、カメラ自身がWi-FiまたはBluetoothに対応して、余分な機器なしに携帯端末と連携できるようになると良い。実際、最近の一部のカメラはWi-Fiに対応しており、スマートフォンと連携できるようである(参考)。
外出先で撮った写真をSNSなどにアップロードしたいとき、皆さんはどうしているだろうか。おそらく、ほとんどの人がスマートフォンやタブレット内蔵のカメラを使って写真を撮っていることだと思う。しかし、スマートフォンやタブレットのような携帯端末のカメラが貧弱なので、デジタルカメラで撮った写真をアップロードしたいという場合はどうだろうか。そういう時に使える方法をこの記事でいくつか紹介してみたい。この記事は個々の製品のレビューではないので、製品ジャンルの紹介と一般的なメリット、デメリットの列挙にとどめる。
カメラ本体がWi-Fi対応していれば多分最強なのだろうが、そういうカメラはまだ多くはない。なので、以下ではカメラに依存しない方法を見ていく。
携帯端末がUSBホスト機能を持っていれば話は楽だ。携帯端末にSDカードリーダーをつないでSDカードから読むか、カメラを直接USBでつないで写真を読み込める。パソコンに写真を取り込むのと一緒だ。
この方法が使えるのはiOSではiPadの仲間に限られる(iPhoneやiPod touchでは使えない)。Android端末では、タブレットは基本的に対応していると思う（例外はあるかもしれない）が、スマートフォンは機種に依存する。
iPadの場合は、30pin Dockの場合（初代～第3世代iPad）は純正のCamera Connection Kit、あるいはサードパーティーの類似製品（カードリーダーに加えてUSBコネクタを備えているもの、SDカード以外のメモリーカードにも対応したものを見かけた）がある。iPad mini、あるいは第4世代以降のiPadの場合は純正のLightning – SDカードカメラリーダーとLightning – USBカメラアダプタが販売されている。Lightningコネクタに繋がるサードパーティー品はまだ見たことがない（秋葉原の路地裏で売られていた怪しげな品を除けば）。純正品はいずれも3000円程度である。写真を取り込む際は、カードリーダーにSDカードを差し込む、あるいはUSBでカメラを接続すると自動的に「写真」アプリが立ち上がり、写真を取り込むことができる。
Android端末の場合はスマホ対応を謳ったカードリーダーや変換ケーブルが販売されている。量販店で見かけたことのある人もいるだろう。安いものだと1000円を切っているものもある。AndroidにはSDカードやカメラから写真を取り込むアプリは（少なくともNexus 7の場合は）標準では付属しないようだ。Nexus Media Importerというアプリ(有償;Nexus Photo Viewerというアプリがお試しとして使えるようだ)がどうやら定番のようなので、筆者はそれを購入した。
この方法のメリットは、
である。デメリットは、
などが挙げられる。
携帯端末がUSBホスト機能を持っていない場合はどうだろう。携帯端末と外の機器をつなぐ方法というのはそんなに多くなくて、広く普及していると言えるのはせいぜいWi-FiとBluetoothぐらいだろう。Bluetoothを使ってカメラから写真を転送するというのはあまり聞かないので、Wi-Fiを使って転送するものを見ていこう。
SDカードにWi-Fiのアンテナから何やら組み込んで、SDカードに保存した写真をWi-Fi越しにアクセスできるようにした製品がある。Eye-Fiが代表的だが、東芝のFlashAirやTranscendのWi-Fi SDのような他社の類似製品も登場している。PQI Air Cardという、microSD-SD変換アダプターとして働く製品もある。
こういうSDカードには、SDカード自身がアクセスポイントとして働くものと、既存のアクセスポイント(モバイルルーターなど)に接続するものがある。両方のモードで動作する製品もある。スマートフォンからのアクセスには、大抵はメーカーから専用アプリが提供されているのでそれが使える。これらのSDカードは大抵はWebサーバーを搭載しているので、PCからの無線でのアクセスにはWebインターフェースが使える。個々の製品の情報についてはメーカーのWebサイトやWeb上の具体的な製品のレビューに譲る。
モノによっては、Webインターフェースや、起動時の動作をカスタマイズできるものもあるようだ。Flash Airはなんだか知らないがAPIが公開されている。PQI Air Cardは起動時にシェルスクリプトを走らせられるらしい。
この方法のメリットは、
という点である。デメリットは、
などが挙げられる。
筆者はこのうち、TranscendのWi-Fi SDカードを使っている。SDカード自身がアクセスポイントとして働くモード（ダイレクトシェアモード）のほか、既存のアクセスポイントを3つまで登録することができる（インターネットモード）。既存のアクセスポイントにつながらなかった場合はダイレクトシェアモードになる。遭遇した問題点は
などである。こういった相性問題が他社の類似製品でも起こるのかは筆者は知らない。
AirStashが代表的だが、最近は他社の類似製品もいろいろ出てきた。筆者が耳にしたことがあるのはPQIのAir Drive、SonyのWG-C10,WG-C20、プリンストンのToaster Pro、TAXANのMeoBank SD Plusなどであるが、探せば他にもあるだろう。
これらの製品群（Wi-Fiストレージとかポータブルワイヤレスサーバーとか呼ばれるようだ）は、ただのWi-Fiカードリーダーとしての機能ではなくて、付加機能を搭載していることが多い。具体的にどういう付加機能があるかはもちろん製品に依存するが、例としては
などがある。どうせならSIMカードを差し込んでモバイルルーターとして使える製品があってもいい気がするが、残念ながら聞いたことがない。
メリットは、
である。デメリットは、
という点である。
筆者はこのジャンルの製品を持っていないので、個々の製品についてあまり突っ込んだことは書けない。
前回は等号の証明に使える公理や規則(Idrisの組み込み関数)をいくつか紹介した。
これに加え、Idrisの標準ライブラリには自然数の性質に関する補題(?)がいくつか用意されている。そのうち、後で使う2つを紹介する。
一つ目は、和と後続者に関するものである。ペアノ算術にはちょうどこのような公理があったはずだ。
もう一つは、和の可換性である。ペアノ算術ではこれを証明するためには帰納法を使うが、証明(関数の実装)は標準ライブラリで用意されているので、ここではそれを使うだけにとどめておく。
さて、前回証明したいと言っていた命題は\[x=y+\mathtt{difference}\ p\]であった。ただし、\(p\) の表す命題は \(y\le x\), Idrisの型で言うと LTE y x である。この等式を証明するには、
[sourcecode lang=”plain”]
differenceP : {x:Nat} -> {y:Nat} -> (p : LTE y x) -> (x = y + difference p)
[/sourcecode]
という型の関数を実装すれば良い。
例によって場合分けする。
p=lteZero の場合:
refl を返せば良い。p=lteSucc p' の場合:
differenceP p' : x' = y' + difference p' が使える。S x' = (S y') + difference p' を示せば良い。(difference の定義を見れば difference p = difference p' なので、S x' = (S y') + difference p は自動的に導いてくれるようだ)
となる。
となる。ただし、一部をアンダースコアで省略している。これらをまとめて、Idrisの式として書けば
[sourcecode lang=”plain”]
differenceP : {x:Nat} -> {y:Nat} -> (p : LTE y x) -> (x = y + difference p)
differenceP lteZero = refl
differenceP {x = S x’} {y = S y’} (lteSucc p’) = trans (trans (cong {f=S} (trans (differenceP p’) (plusCommutative _ _))) (plusSuccRightSucc _ _)) (plusCommutative _ (S y’))
[/sourcecode]
となる。一部の式をアンダースコアで省略しているが、最後の (S y') まで省略してしまうと処理系に怒られたので、そこは明示的に書いている。
今回は、自然演繹の証明図をCurry-Howard対応で翻訳することによって、命題を証明(関数を実装)した。等式の変形のところがやや煩雑になっているが、それはもとの自然演繹の証明図がそういうことになっていたことに起因するもので、Curry-Howard対応のせいでどうこうというものではない。
次回は量化子を含む命題を証明する予定である。Tacticを使った証明は筆者が不勉強なのでまだ扱わない。
前回はIdrisで2つの自然数を比較し、結果とその証明を返す関数 compareNats を作った。今回は、それに追加していくつかの関数を実装してみる。
まず、二つの自然数 \(x\) と \(y\) の差、\(x-y\) を計算する関数 difference を作る。\(y\le x\) の場合は良いが、\(x\lt y\) の場合はどうするか考えどころである。0を返すようにしてもよいが、ここは「\(y\le x\) であることの証拠を要求する」ことにして、\(x\lt y\) の場合は考える必要がない、という仕様にする。型を書けば
[sourcecode lang=”plain”]
difference : (x:Nat) -> (y:Nat) -> LTE y x -> Nat
[/sourcecode]
となる。前回書いたように、LTE y x は命題 \(y\le x\) に対応する型である。
実装には、例によって引数によるパターンマッチをする。
lteZero である。difference x 0 lteZero = x となる。
lteSucc p の形をしている。difference x' y' p によって \(x’-y’\) を計算できる。\(x-y=x’-y’\) なので、それをそのまま返せば良い。difference (S x') (S y') (lteSucc p) = difference x' y' p となる。まとめると
[sourcecode lang=”plain”]
difference : (x:Nat) -> (y:Nat) -> LTE y x -> Nat
difference x 0 lteZero = x
difference (S x’) (S y’) (lteSucc p) = difference x’ y’ p
[/sourcecode]
となる。
さて、よく考えてみると、第1引数 x と第2引数 y の情報は第3引数の型を見れば自動的に得られる。したがって、第1引数と第2引数は省略できるのではないか？
Idrisにはimplicit argumentsという機能があるので、この場合実際に x と y を省略できる。Implicit argumentsを使うと、difference は次のように書ける:
[sourcecode lang=”plain”]
difference : {x:Nat} -> {y:Nat} -> LTE y x -> Nat
difference {x} lteZero = x
difference (lteSucc p) = difference p
[/sourcecode]
この difference という関数は、\(y \le x\) を満たす任意の自然数 \(x\), \(y\) および \(y \le x\) の「証拠」p : LTE y x に対して、\[x = y + \mathtt{difference}\>p\]という関係を満たす。この関係式を「証明」するにはどうすればよいだろうか？
その前に、述語論理における等号の公理と、それがIdrisではどうなっているか見ておこう。自然演繹チックに書けば、述語論理の等号の公理と関連する推論規則は
などがある。あとの三つは最初の二つから出るので、本質的というわけではない。それぞれにIdrisの式を対応させていくと、
となる。つまり、refl, replace, cong, trans, sym という関数があって、それぞれ適切な型を持っている。
以後、命題の左に項を書いていくと上下で重複が多くなって大変なので、以後
のように、使った規則を横棒の右に書くことにする。
長くなるので、一旦記事を分割することにする。今回はここまで。
2月28日：「等号規則(派生)」を追加。