思いつきメモ

まだExercise 1.5の続き。

tabulate : forall {n X} -> (Fin n -> X) -> Vec X n
tabulate {n} f = ?

を完成させる。{n}0としてC-cC-cをして、後はひたすらC-cC-aをすると、型としては正しい式が完成する。

tabulate {zero} f = <>
tabulate {suc y} f = f fzero , tabulate (\ _ -> f fzero)

というもの。fにずっとfzeroを与えたものをn個集めたVecを答えとしている。でも多分これは問題の答えとしては期待通りのものではない。イメージとしては、fにfzero, fsuc fzero, fsuc (fsuc fzero), ... を引数に与えたものをn個集めたものを得たい。つまり、f 0, f 1 ...

Dependently Typed Metaprogramming (in Agda) メモの続き。

Exercise 1.5では、有限集合を表す型Finを定義している。

data Fin : N -> Set where
   fzero : {n : N} -> Fin (suc n)
   fsuc : {n : N} -> Fin n -> Fin (suc n)

ここで、fzero, fsucとしたのは、自然数の型で使用しているzero, sucと区別しやすいようにするため。

有限集合Finは、依存型言語で良く取り上げられる例題のようだが、理解するのは簡単ではないように思う。次のように考えると良いと分かった：

Dependently Typed Metaprogramming (in Agda)のメモ

Agdaの編集方法：
Emacsのagda-modeを使えば、TeXの感覚で記号を入力できる。例：
太字のN : \bn
下付の数字 : _0, _1など
× : \times
→ : \rightarrow

それと型構成子×は、open import Data.Productを書かないと使えなかった。また、最初はData.Productが開けなかったので、(custom-set-variables '(agda2-include-dirs (quote ("." "agda-lib-folder/src"))))を.emacs.elに追加する必要があった。

------------------------------------
C-cC-lで現在開いているagdaファイルをロードしてチェックしてくれる。

zip : forall {n S T} -> Vec S n -> Vec T n -> Vec (S × T) n ...

高速にメモリ上のデータをWindowsで表示する方法について調査してみた。

経験上OpenCVは余り高速ではない。OpenGLでテクスチャに貼り付ける、という方法は高速で、プラットフォームにもあまり依存しない方法なのだが、カメラと対象物との位置関係で、勝手に変形されてしまう(これはOpenGLの目的からして当然であるが、ちゃんとデータを1対1で画像ピクセルに反映させたい、というような場合には問題となる)、という問題がある。

また、OpenGLを使用する場合、ウィンドウ管理はGLUTに任せてしまうと、自分で作成するWindows上のウィンドウに描画するときに問題になる(理論上は可能なはずだが、面倒なのであまり調べていない)。

目標としては、Windowsで、自分で管理するウィンドウの内部に、高速にメモリ上のデータを表示したい。

少し調べてみた結果、Vista以降のWindowsであれば、Direct2Dを使用するのが目的にかなっているようだ。もちろんWindowsにべったりになってしまうのだが、仕方がない。

なんとなく、ID2D1HwndRenderTargetでBitmapを作成し、CopyFromMemoryを行ってDrawBitmapという流れで出来そうな気がしてきた。これだとオフスクリーンではないかも知れない。でも、この応用で何とかなりそうな気がする。

今度実験してみよう。

===================
ちなみに、調べてみると、MacではOpenGLのFramebuffer objectという方法があるようだ。自分がWindows上のOpenGLで試したときには、FBOはそれほどパフォーマンスが良くなかった印象がある。Macだとまた違うかも知れないが。

いわゆるWebCamというものを、自分で作成するプログラムはどうすれば作成できるのか、というのを調査している。

一番手っ取り早いのは、多分OpenCVを使用してcvQueryFrameで取ってくる方法だと思われるが、USB Video Classの機能をもっと使用することを考えているので(Extension Unitsというのを使いたい)、cvQueryFrameは高レベルすぎる。

Windows VistaからMedia FoundationというAPIが提供されており、これを使用するのが推奨のようだ。とりあえずMFCaptureD3D Sampleのページから、サンプルプログラムをダウンロード(Download from MSDN Code Galleryというリンク)し、VS Express for Desktopでビルドして実行したら、正常にWebCamから動画をキャプチャ、表示できることが確認できた。試したカメラはYUV2形式のデータだった。

追記: どうやらExtension Unitsは、DirectShowのAPIのようだ。果たしてMedia Foundationを使ったプログラムでも使用できるのか？よく分からない。さっぱりMedia Foundationは諦めて、DirectShowのサンプルでも探した方が良いかも知れない...

DirectShowのプログラミングには、良い情報源(体系的な資料)が無いような気がする。知っている人は知っているが ...

先日、某所にてスタバに入った。注文したら、なにやら店員が「****(突然の質問だったので失念)はご存じですか？」と聞いてきた。「いいえ」と答えると、どうやら、スタバには「当たりレシート」なるものが存在するらしい。参考：【何でも一杯無料】スターバックス「当たりレシート」の全貌。

自分はおそらく100回も利用したことはないのではないかと思うが、この当たりレシートに運良く当選したらしい。あまり個人情報を答えなければならないようなアンケートだったら無視しようかと思ったが、そんなことはなく、利用店舗についてのいろいろな意見を調査するものだった(上のリンク先に質問ページが全部あるようだ)。

超ラッキー! 久々にいいことあったなぁ。生きてて良かった! 何を注文するかじっくり考えよう。

これまではスマホでない方の携帯をずっと使用してきたけれど、利便性を考えて現代の便利品を揃えてみることにした。

ただ、スマホは、まだ月額使用料が(自分が感じる価値からして)高いので、SIMフリー端末とMVNOのSIMを試してみよう、ということになった。

いろいろ検討したのだけれど、EXPANSYSというのが日本でSIMフリー端末を購入する店舗として有名らしい。ただ、こちらで販売されている端末は、基本的には技適マークがないものがほとんど。つまり、MVNOのSIMを差して、日本国内で使用するのは、厳密には違法行為ということになるらしい。もちろん、FCCの認可はあったりするので、米国で使用するのは問題ないだろう。

---- ここは少し脱線 -----
もっとも、海外からの旅行者が、海外で販売されているSIMフリー端末を日本国内で使用するのは例外として認められているっぽい。SIMフリー端末もいろいろな周波数に対応しているわけだけれど、日本国内の電波と干渉してしまう、ということは無いのだろうか？全バンドが国内で使える訳ではないと思う(詳しくは未調査)。それとも、携帯は、基地局からの電波に周波数を合わせて、拾えた場合だけ電波を発信するという仕組みなのだろうか？
-------------------------------

ということで、法的にも問題ない方法としては、技適マーク付きSIMフリー端末を使用することになる。SIMフリー端末を使用するには、自分でスマホを契約するか、SIMフリーになっているスマホを中古で購入する、(種類は少ないが)国内で販売されている技適あり新品SIMフリー端末を購入する、という方法が考えられる。さんざん考えた末、まずはお手軽に試すことにして、AWR-100TKというWiFIルータにした。端末は、手持ちのNexus7でしのぐ予定。



そして ...

twitter経由で、CycloneVに重大な欠陥がある、というようなものを見つけた。Errata Sheet for CycloneV Devicesによると、重大な問題というのは、2番目のFractional PLL Phase Alignment Errorのようだ。PLLの位相が設定値よりもずれてしまう場合がある、というようなことらしい。影響を受ける事例としてLVDSが挙げられている。例えば、受信クロックをPLLでロックさせてnビットデシリアライズする、といったときに影響するのかも知れない。確かに、ここに問題があるとすれば、用途によっては使い物にならなくなってしまうかも知れない。

PLLの詳しい仕組みには詳しくないが、PLLだけでも本が何冊も書けるくらいだから、アナログ回路の真骨頂なのだろう。それだけに問題も起きやすいところかも知れない。

いずれにせよ、しばらくはXilinx優位ということになりそうだ。

アルテラ、ソフトウェア・プログラマの FPGA 利用を可能にする OpenCL 向け SDK と市販ボードの一般提供を開始

SDKについて詳しく調和したわけではないが、OpenCLではそれほどFPGAのメリットが引き出せないのではないか、と思う。OpenCLは基本的に、メモリとデータを何度かやりとりしながら処理を進めるプログラミングモデルが利用されていると思う。一方、FPGAを用いて処理を高速化したいという場合、一般的にはメモリから一気に回路パイプラインに流し込んで、パイプラインから出てきた結果をまたメモリに書き戻す、というイメージではないかと思う。メモリとのやりとりが多くなると、結局演算よりもそちらがボトルネックになってくるはず。それに、メモリ帯域という事で言えば、ほとんどのFPGAを載せたボードでは、最新のGPUボードのメモリ帯域には太刀打ちできないだろう。

ということで、OpenCLのプログラミングモデルはFPGAの高速化に向くものではない、ということである。それよりは、普通に高位合成でパイプライン処理を合成し、必要なメモリとのやりとりをくっつければ良いのではないだろうか。

Androidのアプリケーションを開発しているときに、昨日までは普通にIDE(IntelliJ/IDEA)からUSB接続した実機にアプリケーションをダウンロードして実行できていたのに、今日になって、できなくなってしまった。エラーとして、

Failure [INSTALL_PARSE_FAILED_INCONSISTENT_CERTIFICATES]

困ったので色々検索してみると、どうやらWindowsの場合、C:\Users\(ユーザ名)\.androidの下に、debug.keystoreというのが自動的に作成されるらしい。ここに、アプリケーションの署名に必要な証明書が格納されている。Androidでは、たとえデバッグであっても、アプリケーションは署名を付けないといけない。さらに、少なくとも次の場合は、一度インストールしたアプリケーションを再インストールしようとしても、上記メッセージが表示されて失敗する。

• アプリケーションを異なる証明書で署名した。
• アプリケーションの署名に使用された証明書の期限が切れた。

自動生成されるdebug.keystoreの証明書には有効期限があり、デフォルトの有効期間は1年間であるようだ。自分の場合、上記の2番目の原因でエラーが発生していた。

いろいろ対処法があるらしいが、とりあえず怠惰なプログラマとしては、もっとも楽な方法を使用した：インストールしたアプリケーションを一度アンインストールし、再度(削除後に再生成されたdebug.keystoreで署名して)インストールする。

ただ、この方法の欠点は、アプリケーションで作成されていたデータもすべて削除されてしまうことである。それが許容できれば、とりあえず一番簡単な対処法であると思う。いずれにせよ、リリースするときには正式に署名を付けるので ...