2019-06-01

(Z/2^nZ)*の構造(オマケに高校数学風クイズ)

これは何？

金子晃先生の「応用代数講義」の命題4.26の証明がよくわからなかったし、わかったにしても構成が具体的でなくやっぱりよくわからないので、本の証明をヒントに自分でもうちょっと具体的な証明をつけなおしてみた。
最後にこれを考えてたらできた高校数学風クイズもあるよ！

示す命題

n≧3とし、 $G=\mathbb{Z}_{2^n}^*$ とする。 $G\simeq C_{2^{n-2}}\times C_2$ となる。
ここで、 $G=\mathbb{Z}_{2^n}^*$ は $\mathbb{Z}/{2^n}\mathbb{Z}$ の乗法群である。

大事な観察

3の「2の羃」乗を2進法で表記すると、次のような法則が観察される:

$3 = \texttt{11}$ ←末尾の「1」と次の「1」との間に「0」は現れない
$3^{2^1} = 9 = \texttt{1001}$ ←末尾の「1」と次の「1」との間に「0」は2個あらわれる
$3^{2^2} = (3^{2^1})^2 = 81 = \texttt{1010001}$ ←末尾の「1」と次の「1」との間に「0」は3個あらわれる
$3^{2^3} = (3^{2^2})^2 = 6561 = \texttt{1100110100001}$ ←末尾の「1」と次の「1」との間に「0」は4個あらわれる

そういうわけで、i≧1について、 $3^{2^i}$ を2進法で表記したとき、末尾の「1」と次の「1」との間に「1」は $i+1$ 個あらわれるらしい。つまり、「1」が1つずつ左にずれていっているらしい。このことはあとでちゃんと示す。

したがって、 $3, 3^{2^1}, 3^{2^2}, \dots, 3^{2^{n-3}}$ の2進法表記を下n桁(ただしn≧3)とったものを考えるとき、そのとったものたちはすべて相異なる。例えば、

n=3なら、 $3 = \texttt{11}$ の2進法表記での下3桁は「001」で(1個しかないので当たり前だけど)相異なる。
n=4なら、 $3 = \texttt{11}$ の2進法表記での下4桁は「0001」、 $3^{2^1} = \texttt{1001}$ は「1001」でこの2つはやっぱり相異なる。
n=5なら、 $3 = \texttt{11}$ の2進法表記での下5桁は「00001」、 $3^{2^1} = \texttt{1001}$ は「01001」、 $3^{2^2} = \texttt{1010001}$ は「10001」でこの3つはやっぱり相異なる。
…

となる。

証明

まず、Gは $2^n$ 未満の奇数全体からなるので、位数は $2^{n-1}$ である。
「大事な観察」と、位数が2羃でありGの部分群の位数は2羃にならざるを得ない*1ことから3の位数*2はちょうど $2^{n-2}$ である。

ところで、 $2^{n-1}-1$ か $2^{n-1}+1$ との差は2なので、このうち少なくとも一方は3の倍数ではなく、したがって3の羃でもない。その3の羃でないほうをaとよぶことにする。aは(当然 $2^n$ のmodをとって) $a^2=1$ である。
$a\not\in \langle 3 \rangle$ であり、<3>の指数は2なので、G=<3>∪ a・<3>である。

群準同型 $\varphi\colon C_{2^{n-2}}\times C_2 \to G$ を、φ(0, 1)=a, φ(1, 0)=3で定める。これが同型であることを示そう。全射は $\phi(x, y)=3^x \cdot ya$ とG=<3>∪ a・<3>より明らかである。
単射も<3>∩a・<3>=∅に注意すれば簡単である。これで同型が示された。

これでこういうクイズが作れますね

高校数学風に、こういう問題が作れますね(多分うまく誘導作れば本当に高校数学の問題になるんですけど)。

431をn(正の自然数)乗して1024で割った余りを計算すると1になったという。そのようなnのうち最小のものを求めよ。ただし、431は511×81を1024で割った余りである。

答えは上の事実を使えばもちろん簡単で、511は512=1024/2から1を引いたものでかつ3の倍数でないので、上の証明で言うところのaとして選べる。さらに81のほうは3の4乗である。
よって、上の同型で431∈ $\mathbb{Z}_{1024}^*(=G)$ を飛ばすと、(φの逆をψと書くことにして)ψ(431)=(4,1)∈ $C_{256}\times C_2$ となる。
Gの方でn回羃をとることは、 $C_{256}\times C_2$ では両方の要素にn倍することに相当するので、n×(4,1)=(0, 0)となる最小のnを考えればよく、これは明らかに256/4=64である。よって答えは64。

*1:ラグランジュの定理

*2:3の羃の生成する巡回部分群の位数

2019-05-15

Ansible/Vagrantでubuntuを起動してaptするときにdpkgのlockのエラーが出るやつへの対処

Ansible/Vagrantでubuntuを立ち上げて、そこにaptで必要なものをインストールしたい*1ということはあると思うのだが、起動直後だとよく、「dpkgのlockファイルがあって実行できない」というメッセージが出て失敗してしまうことがある。無視すれば当然後ろの命令がうまく行かない。

Googleで「ansible ubuntu dpkg」でぐぐると、結構「dpkgのロックファイルを削除する」とか「killallでdpkgを殺してしまう」というようなどう考えても行儀のいいとは思えない対処法が出てくる。実は私も以前はそれをやっていて、大方はうまくいくのだが沢山やっていると失敗するやつが必ずあらわれて、それらのイレギュラーへの手動の対処が大変で「Infrastrcuture as a codeとは…」という気分になりやってられない。

そもそもこの原因は、Ubuntuがデフォルトだと起動時に自動アップデートをかけるのが原因なので、アップデートが終わるまで待ってからこちらのしたいことをすればいいのである。
そういうわけで、wait_for fails on apt-get / aptitude lock-file in /var/lib/dpkg/lock · Issue #16593 · ansible/ansible · GitHubのようなものも試したのだが、ロックファイルがどうもこれだけとも限らないようで成功率が100%にはならなかった。いまのところ、「そもそもdpkgが起動してるかをみるのが直接的でよくない？」ということで、今はもっぱら

 while ps -A | grep dpkg; do sleep 1; done;

を先頭に挟むことにしていて、今のところは成功率100%である。何かもっと筋の良い方法、常識などあったら教えてください。

*1:例えばvagrant awsでubuntu インスタンスを立ち上げて、そのあとVagrantで操作できるように向こう側でpythonをインストールしたいとか

2018-11-23

Visual Studio 2017でOpenCV 2.4.3をビルドする

諸事情によりOpenCVのバージョン2.4.3を使いたくなったのだが、バイナリの配布が終了していたのでVisual Studio 2017 (Community)ビルドしたくなった。そのときにコケたことがあったので(未だに全ての問題が解決したわけではないが)メモしておく。

OpenCVのgithubのtags(Tags · opencv/opencv · GitHub)から2.4.3を探しzipをダウンロード(https://github.com/opencv/opencv/archive/2.4.3.zip)。
ダウンロードしたファイルを展開。
CMake(https://cmake.org/)のWindows版を起動し、2で展開したディレクトリ(私の場合「C:/Users/ashia/Downloads/opencv-2.4.3」)を「Where is the source code」に、「Where to build the binaries」にそのなかのbuildフォルダを指定する(私の場合「C:/Users/ashia/Downloads/opencv-2.4.3/build」)を指定する。buildディレクトリは存在しないが、あとで確認の上自動で作られるので問題ない。
「Configure」をクリックしてOKとかをポチポチする(多分VS2017を使ってコンパイルする設定にデフォルトでなっていると思うが、なっていなければ直す)。CMakeがそのコンピュータのビルド環境を検出してくれる。
真ん中のおおきい窓にコンパイルオプション赤いリストが表示されるので、必要な機能に応じてつけたりけしたりするはずだが、今回の私の用途ではそのままにしておいた。
「Generate」をクリックする。CMakeがそのコンピュータのビルド環境を見て指定したbuildフォルダに、OpenCVをVS2017を使ってコンパイルするために必要なファイルを揃えてくれる。
buildフォルダのなかにOpenCV.slnができているので、VS2017で開く。
そのまま「ビルド>ソリューションのビルド」を実行するが、maxやminが未定義だと怒られるので、怒られているファイルのヘッダの先頭に「#include 」を付け加える。
もう一度やるとさっきのエラーは消える。正直気持ち悪いのだが、私が今回使う機能には関係ない部分だったので無視していた。これでbuildのbinフォルダには(ビルドが成功した分の機能の)dllファイルができているし、libフォルダにはlibファイルができている。

2018-11-04

拡張ユークリッド互除法を行列で書く

拡張ユークリッド互除法で実際に不定方程式の解を求めるとき、私は行列算で書くのが好きなのですがあんまりそういう解説を見掛けないのと、実は私もそれを思い出すのにいちいち20分ぐらいかかってしまうという理由でここにメモしておきます。

拡張ユークリッド互除法での「代入」

拡張ユークリッド互除法で $11a+7b=1$ なるa,bを求める方法は、通常次のように「代入」を用いて説明されます:
まず、

11÷7=1 あまり 4
7÷4=1 あまり 3
4÷3=1 あまり 1
3÷1=3 あまり 0

とあまりを計算する。これらのうち、「あまり=(gcd)」となっている式までを上から「あまり=わられる数-わる数×商」の形に書き直す。

4 = 11-7×1 (イ)
3 = 7-4×1 (ロ)
1 = 4 - 3×1 (ハ)

となる。これを下から順に代入して、

1 = 4 - 3×1 (ハを持ってくる)
= 4 - (7-4×1)×1 (ロを代入)
= (-1)×7 + 2×4 (整理する)
= (-1)×7 + 2×(11-7×1) (イを代入)
= 2×11 + (-3)×7 (整理する)

これで、a=2、b=(-3)と求まった。

行列で書いてみる

が、数に数を代入というのが気持ち悪いし、「整理する」のところで何を「係数」と見做して整理していいのかよく分からなくなるので、しばらくすると簡単にやり方を忘れて困ってしまう。そこで、これを行列算で書き直してみる。

ユークリッドの互除法では、(割られる数, 割る数)というペアから(割る数, あまり)というペアを計算するという操作を繰り返す。例えば上の例では、(11, 7)→(7, 3)→(3, 1)→(1, 0)となっている。
このペアに注目して、上の4本の式を行列算で書き直してみる。すると、次のようになる。

$\begin{pmatrix}0 & 1 \\\ 1 & -1\end{pmatrix}\begin{pmatrix}11\\7\end{pmatrix} = \begin{pmatrix}7\\4\end{pmatrix}$ (イ)
$\begin{pmatrix}0 & 1 \\\ 1 & -1\end{pmatrix}\begin{pmatrix}7\\4\end{pmatrix} = \begin{pmatrix}4\\3\end{pmatrix}$ (ロ)
$\begin{pmatrix}0 & 1 \\\ 1 & -1\end{pmatrix}\begin{pmatrix}4\\3\end{pmatrix} = \begin{pmatrix}3\\1\end{pmatrix}$ (ハ)
$\begin{pmatrix}0 & 1 \\\ 1 & -3\end{pmatrix}\begin{pmatrix}3\\1\end{pmatrix} = \begin{pmatrix}1\\0\end{pmatrix}$ (ニ)

ペアの第2要素は第1要素に移るので、係数行列の1行目はかならず(0, 1)になり、2行目はあまりを求めるところなので、(1, -商)となっている。
しらべたかったのは、(11, 7)に何をかけていくと(1, 0)にできるかということなので、まず(イ)の両辺に(ロ)の係数行列をかけてみる。すると、

$\begin{pmatrix}0 & 1 \\\ 1 & -1\end{pmatrix}\begin{pmatrix}0 & 1 \\\ 1 & -1\end{pmatrix}\begin{pmatrix}11\\7\end{pmatrix} =\begin{pmatrix}0 & 1 \\\ 1 & -1\end{pmatrix} \begin{pmatrix}7\\4\end{pmatrix}$ (イの両辺にロの行列をかける)
$= \begin{pmatrix}4\\3\end{pmatrix}$ (ロを「代入」)

代入するにも、先の章とは違って行列の形が変な代入を防いでくれる。あとは同様のことをすればよく、少し考えると右から

$(ニの行列)(ハの行列)(ロの行列)(イの行列)\begin{pmatrix}11\\7\end{pmatrix} = \begin{pmatrix}1\\0\end{pmatrix}$

となることがわかる。これはまさに我々がはじめ求めたかった形になっていて、答を求めるには左の行列積の連鎖を計算すればよい。

$(ニの行列)(ハの行列)(ロの行列)(イの行列)$
$= \begin{pmatrix}0 & 1 \\\ 1 & -3\end{pmatrix} \begin{pmatrix}0 & 1 \\\ 1 & -1\end{pmatrix}\begin{pmatrix}0 & 1 \\\ 1 & -1\end{pmatrix}\begin{pmatrix}0 & 1 \\\ 1 & -1\end{pmatrix}$
$= \begin{pmatrix}2 & -3 \\\ -7 & 11\end{pmatrix}$

((ちなみにこれを手計算するときは2つずつ組にしてかけ算するとちょっと楽)あとはこの第1行をとって(あるいは両辺に(1, 0)をかけて)、a=2, b=-3がわかる。

まあこう覚えておくと、アルゴリズムにするときもちょっと思い出しやすいんじゃないかなあと思う。

2018-10-15

論文ながしよみ「EXPERIENCE WITH STATIC PLC CODE ANALYSIS AT CERN」

Tsiplakiらの「EXPERIENCE WITH STATIC PLC CODE ANALYSIS AT CERN」をながしよみします。といいつつ、用語集を作ったら大体満足してしまったし、やってみた系の論文なのでそんなに内容はない。この界隈でどんな登場人物が出てくるかというまとめにはなった気がするので個人的には満足している。「この技法を産業応用してみたいぞ！」というときの参考にはなりそう。書誌情報はこちら:

@inproceedings{TsiplakiSpiliopoulou:2018avy,
author = "Tsiplaki Spiliopoulou, Christina and Blanco Viñuela,
Enrique and Fernández Adiego, Borja",
title = "{Experience with static PLC code analysis at CERN}",
booktitle = "{Proceedings, 16th International Conference on
Accelerator and Large Experimental Physics Control Systems
(ICALEPCS 2017): Barcelona, Spain, October 8-13, 2017}",
year = "2018",
pages = "THPHA160",
doi = "10.18429/JACoW-ICALEPCS2017-THPHA160",
SLACcitation = "%%CITATION = INSPIRE-1656449;%%"
}

用語集(しらべたり知ってることを書いたりしている。割と適当。)

PLC: Programming Logic Controller。工場の機械を制御するのによく使われている制御装置(の規格？)。工業用や宇宙用の丈夫なArduinoだと思っている。このためのプログラミング言語 *1があり、SiemensのSCLやSchneiderのSTといったものがある。もともとリレーをたくさん並べて機械を管理していたのをリッチにしていったらプログラミング言語になったみたいなやつらしい。この論文ではこの言語のことをPLC program languageとよんでいる。IEC 61131-3 標準規格で規格化されている。日本だとオムロンがやってるらしい。
SCL: PLC用のプログラミング言語。Siemensが作っているらしい。CERNではSCLを使っていて、この論文もこちらを対象にする。
UNICOS: UNified Industrial COntrol System。LHC(Large Hadron Collider, 大型ハドロン衝突型加速器)を制御するためのフレームワーク。この上でPLCの開発ができるらしい。 https://cds.cern.ch/record/1402490/files/WEPKS006.pdf?version=1
static analysis: 静的解析。コードを解析して、そのコードを実際に実行することなくそのコードの性質(無限ループに落ちないかとか変なメモリ操作をしてないかとか)を調べること。プログラムの品質保証の技法としてよくテストなんかと対にされる。
model checking: モデル検査。コードから数学的対象(大体ある種のオートマトン)を取り出して、その数学的対象を数学的に調べることでもとのコードの性質を調べる静的解析の一手法。コードについて網羅的に何かを調べることができてよい。
PLCverif: PLC用のモデル検査器。CERNで作られたらしい。 http://ddarvas.web.cern.ch/ddarvas/publications/icalepcs2015/WEPGF092.pdf
FB: function block。PLC言語での関数に相当するぽい。
IM: intermediate representation。PLCverifはSCLのコードを一旦中間表現に変換する。
CFG: control flow graph。オートマトンの一種で、普通の手続き型プログラムにオートマトン的な解析をしたいときは大体これに変換する。大体プログラムの各行がCFGの1状態に対応し、それらの遷移に条件分岐や代入の情報が載っていると思えばよいと思う。
nuXmv: モデル検査器。https://nuxmv.fbk.eu/で公開されている。有名なモデル検査器としてNuSMVがあるが*2、これにSAT/SMTソルバとの連携をくっつけたものらしい。
CBMC: C言語/C++用の有界 *3モデル検査器。https://www.cprover.org/cbmc/から入手できる。Oxfordのグループが作っている。結構産業応用に意欲的で、そのために地味なことを高品質でやっているイメージがある。
Xtext: プログラミング言語(特にDSL？)のための開発環境開発のためのフレームワークらしい。https://www.eclipse.org/Xtext/から入手できる。対象となるプログラミング言語の文法を書いてXtextに与えると、パーサ、コンパイラ、その言語のためのEclipse拡張、各種エディタ拡張が生成されるらしい。

アブストのアブスト

CERNで使われているPLCのやばそうなところを見つけるために、主に普通のプログラミング言語に使われている静的コード解析の技法を使ってみます。使ってみたツールややってみた経験を共有します。

内容

PLCverifを利用している。まずPLCverifの簡単な説明をしている。

PLCverifの説明

Figure2に書いてあるが、SCLのコードが与えられると、これは中間表現に変換される。このために、Xtext(というかXtextで生成されたツール)を使ってSCLコードをパースし、抽象構文木(AST)を得る。ASTの構造はFigure3に示されている。PLCverifには、このASTを解析するための「ルール」が定義されていて、その「ルール」に従っているか、あるいはviolateしているかを教えてくれるらしい。

適用例

この解析では、コードのやばい匂い(code smell)をみつけることを目的としていて、そのための「ルール」を検査している。この論文中ではうち2つの「UNICOS naming convention rule」と「Nested conditional if statements rule」を紹介している。

はじめの「UNICOS naming convention rule」は、変数名がUNICOSの命名規則(Table1)にしたがっているかを検査する。たとえば、Figure4のコード中の「AuMoSt」は、「Auto」をあらわす略語「Au」、「Mode」をあらわす「Mo」、「Status」をあらわす「St」を組合せたもので、これらの略称はちゃんと表のなかにあるので大丈夫だが、2行目の「E_FuStopI」は「Fu」が表にないので駄目である。

次の「Nested conditional if statements rule」は、深いIf文について警告を出すらしい。このルールはFigure5に示されている。

感想

タイトルで「Experience」と言っているとはいえもうちょっと検証の論文だと思っていたが、かなりソフトウェアエンジニアリングの論文でした。特に検証技法的に面白いところはなかったように思うのですが、エンジニアリング的には面白いんでしょうか…

よくわからんところ

ここに書いてある「ルール」の検査だけだとCBMCもnuXmvもいらなそうなんですがどこで使ったんですか

英語的に勉強になったところ

「The large number of industrial control systems based on PLCs (Programmable Logic Controllers) available at CERN implies a huge number of programs and lines of code.」っていうんですが、implyに物理的な「含む」っていう意味あったんですか

*1:チューリング完全かどうかは知らない…

*2:この界隈では珍しく和書の入門書が産総研から「モデル検査初級編―基礎から実践まで4日で学べる (CVS教程)」として出ている。

*3:普通モデル検査というと無限ループのような無限の挙動を扱うことができるが、有界モデル検査ではループはある程度大きい定数回の繰り返しに展開されてしまう。

2018-09-09

duneでwarningが全部errorになってしまうのをなんとかする

OCamlの(多分次期標準の)ビルドツールであるdune(https://github.com/ocaml/dune)を使ってコンパイルすると、すべてのwarningがerror扱いされてしまいます。例えば、

について

dune exec ./main.exe

を叩くと、

ocamlc .main.eobjs/main.{cmi,cmo,cmt} (exit 2)
(中略)
File "main.ml", line 2, characters 6-7:
Error (warning 26): unused variable x.

となり、未使用変数の警告がエラー扱いされてしまって実行することができません。どうもduneがocamlc(コンパイラ)にwarningすべてをerrorにする「-w @A」をわたしているようです。開発中の未使用変数ぐらい大目に見てほしいので、warningのままでいてほしいです。そこで、duneファイルを

として、ocamlcにさらにwarningすべてをerrorとして扱わない「-warn-error a」を渡すと解決します。

http://ocaml.jp/archive/ocaml-manual-3.06-ja/manual025.html

(ところで、gistで1ファイルだけ埋め込むときはgistの上のほうの埋め込みタグのURIの後ろに「?file=hoge.fuga」をつければいいのね)

2018-08-25

横内寛文「プログラム意味論」を流し読みした

本当は読書メータの感想のところに書こうと思ったのだが字数が溢れてしまったのでここに書いておく。
あんまり真面目に読んでないんだ、ごめんね。

気にはなっていたのだか積読で、一念発起して興味あるところだけ読むことにした。そういうわけで全体の話はしてません。

公理的意味論は(他の意味論のスタイルと明確な区別があるわけではないが)プログラムの構文に、その文が意味する数学的対象を直接割り付けるもの。プログラムが停止しないなどのエラーをうまく扱えるその数学的対象としては部分関数が便利で、その順序をうまく扱うためにcpo(complete partial order)という順序集合のクラスを用いる。そうするとこの上で不動点の議論ができ、それが再帰やwhile文といった自明には意味が定義できないものにも意味を割り付けることができる。この議論の後に、λにいくらかの基本型と再帰を許す関数定義μを追加したPCF(Programming language for Computable Function)を定義し、それに対して意味論を与える。

型なしラムダ計算に公理的意味論を与えるのに素朴に集合論で言うところの関数を割り当てようとすると、自由な関数適用のせいで矛盾が起こってしまう。これに対処するには、X→Xの関数がXに埋め込めるようなcpo Xを見つけなければいけない。このような要求を方程式風に書くとX=[X→X]というようになるが、このようなcpoの対象についての方程式を領域方程式という。この方程式の解が見つかれば、そこから型なしラムダ計算の意味論(モデル？)を作ることができるが、実際この解として2点以上の集合Dから埋め込みを繰り返して無限直積を取り作ったcpoであるD∞が解であることを確かめる。なお、この領域方程式を解く方法を研究したり、この状況をcpoだけではなくω-完全な圏でのcolimitを考えて本質を捉えようとするというような議論もこの本ではなされているが、とりあえず具体に興味があったのでそこは読まなかった。

疑問として、そんな風にして意味論を作ってそれで「型なしラムダ計算の理解が深まった」と言えるのか、普通にラムダ式を適当な同値関係で割ったものそのものを眺めるのと比べて何かいいのかという疑問は残ったが、真面目に読んでないからかもしれない。

(8/27追記)公理的意味論がつけば、(λx.xx)(λx.xx)に⊥が対応することがわかるよと教えてもらいました。そういう意味では公理的意味論は数学で言うところの不変量みたいな感じで使えるんですね。