OCamlのwith typeの使い方を失敗から学んだ話(ファンクタシグネチャの返り値でモジュールを制限したくなったときどうすればよいか)

OCamlでのSetの使い方がよくわからない(どれがいいんでしょう) - ashiato45の日記に引き続き、有限オートマトンOCamlで記述することを考えます(前の記事は読んでなくても大丈夫です)。今回は文字列を読んで受理拒否を判定する関数は載せず、純粋に有限オートマトンのデータ構造を提供することを考えます。ただし、アルファベットと状態をあらわす値は好きなものを選べるように、ジェネリック的にしたいとしましょう。
2.3 ファンクタなんかを参考にしながら書くとこんな感じになります。
gist.github.com

これで良さそうな気もするのですがここでさらに、ファンクタAutomに具体的によく使う集合を与えて、具体的なオートマトンのモジュールも作ってこのライブラリで提供することを考えましょう。次のように書いてみます。
gist.github.com
今回はZeroとOneを持っているalph型を定義し、その集合をアルファベット集合AlphSetにします。状態集合は文字列集合StringSetということにします。そしてこれらをAutomファンクタに与え、ZeroOneAutomモジュールを作ります(autom_dame2.mliの19行目)。モジュールはシグネチャで制限してインターフェースを提供してやらないことには外部からアクセスできませんので、4行目で定義したファンクタシグネチャAUTOMを使って

module ZeroOneAutom: AUTOM(AlphSet)(StringSet)

と制約することを考えます…が、これはコンパイルエラーになります。文法が定義してあるOCamlの公式マニュアルの
7.10  Module types (module specifications)を見てみると、そもそもこういう書き方はできず、コロンの右側には基本的にはシグネチャを置かなければならないということがわかります。

そこで、仕方がないのでファンクタで帰ってくるものだけを取り出して書き(以下AUTOM')、AUTOMはAUTOM'を返すようにすることを考えてみます。
gist.github.com
ただし、AUTOM'の定義のときには引数のモジュールの情報は使えませんので、とりあえず必要な型だけをast, sst, aset, ssetとして定義しておいて、それを使って全体を定義しておきます(autom_ok.mliの4-15行目)。そして、AUTOMの定義のなかでwith typeを使って、AUTOM'で仮置きした型と、得られたモジュールの型とが一致するという制約をかけます。これで、ZeroOneAtomはAUTOM'シグネチャとtype withを使って無事制限をかけることができました。ついでに、AlphSetとStringSetも外部からきちんとアクセスできるようにtype withで制約をかけてあります。type withのはたらきですが、merlinの表示する情報を見るのがわかりやすい気がします。

module ZeroOneAutom: AUTOM'
with type ast = AlphSet.t
with type sst = StringSet.t
with type aset = AlphSet.Elt.t
with type sset = StringSet.Elt.t

の情報をmerlinで表示させると、次のようになります

sig
type ast = AlphSet.t
type sst = StringSet.t
type sset = StringSet.Elt.t
type aset = AlphSet.Elt.t
type t = {
alph : ast;
states : sst;
trans : sset -> aset -> sset;
init : sset;
final : sst;
}
end

対して、

module ZeroOneAutom: AUTOM'

の情報は

sig
type ast
type sst
type sset
type aset
type t = {
alph : ast;
states : sst;
trans : sset -> aset -> sset;
init : sset;
final : sst;
}
end

となります。このように、type withを使うと、型の後ろにイコールとその型が何かを追加することができるようです。このことを「シグネチャに型の等価性情報を追加する」というようです*1

ちなみに、先の文法のページ(2.4 ファンクタを使った型の抽象化])を見ていたところ、type withならぬmodule withというのもあるようだったので、これも試してみました。すると、次のようになります。
gist.github.com
「module with M = M2」のようにすることで、AUTOM'シグネチャ内で仮置きしたAlphSetモジュールとStateSetモジュールに(autom_ok2.mliの5、6行目)、モジュールの等価性情報を追加することができています(行18、19や30、31)。実際、

module ZeroOneAutom: AUTOM'
with module AlphSet = AlphSet
with module StateSet = StringSet

の情報をmerlinで見てみると、

sig
module AlphSet :
sig
module Elt :
sig
type t = alph
val t_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t
val sexp_of_t : t -> Ppx_sexp_conv_lib.Sexp.t
(略)
val sexp_of_t : t -> Base__.Ppx_sexp_conv_lib.Sexp.t
end
module StateSet :
sig
module Elt :
sig
type t = string
val t_of_sexp : Ppx_sexp_conv_lib.Sexp.t -> t
(略)
val sexp_of_t : t -> Base__.Ppx_sexp_conv_lib.Sexp.t
end
type t = {
alph : AlphSet.t;
states : StateSet.t;
trans : StateSet.Elt.t -> AlphSet.Elt.t -> StateSet.Elt.t;
init : StateSet.Elt.t;
final : StateSet.t;
}
end

となっており、確かになかのAlphSetやStateSetにmodule withで与えたAlphSet(これは外側のalph型のためのモジュールの名前!)やStringSetの情報が反映されていることがわかります。

OCamlでのSetの使い方がよくわからない(どれがいいんでしょう)

前々からOCamlのSetの使い方、というかベストプラクティスがよくわからないと思っていたのですが、うまく言葉にできなかったのですがいい例が作れたのでその例にそって「これをどう書くべきなんだろう」というお話をします。

例として考えるのは普通の決定性有限オートマトン(DFA,
決定性有限オートマトン - Wikipedia)です。
DFAのデータを保持できて、かつある文字列(語)を受理するかどうかの判定ができるものを考えます。素朴にlistを使って実装するとこんな感じになります(getのあたりはレコードで書くべきだったかも…):
gist.github.com

ただ、本来はアルファベットや状態は集合であってリストではないので、これを集合を使って書き直したいと思います。
このときありうる実装をとりあえず2つ作ってみたのですが、それぞれ気持ち悪いところがあってどうすればいいのかよくわからないので誰か教えてください…

オートマトンをあらわすファンクタを作って、それにアルファベットや状態の値のを渡す

gist.github.com
今回はまあいいのですが、状態集合やアルファベット集合はオートマトンとはそもそも別の文脈で作っていて、その集合をオートマトンの状態にしたいなというシナリオのときに、集合を作りはじめる前からMyAutomを作りはじめている(21行目)のが気持ち悪いなという気がしています。

オートマトンをあらわすファンクタを作って、それにアルファベットや状態の値の集合のモジュールを渡す

gist.github.com



先の点を解消するために、集合のモジュールはファンクタの外側で作ってしまって、その集合のモジュールをオートマトンをあらわすファンクタに渡すべきでしょうか。まあやっぱり動くのですが、オートマトンの型は値の型に応じて決まってほしくて、その集合に対する操作の仕方まで規定している集合モジュールを取らせるのは気持ち悪くない…?という気がしています。

あるいはそもそもオートマトンの状態をどう持っているかはシグネチャで隠蔽してしまう?

それで外からappend_statesみたいな命令を使って追加していく形にすべきでしょうか。そのほうが疎結合的な意味では衛生的な気もするのですが、そのために手持ちの状態集合をfoldなりで逐一追加して計算コストをかけるのもな…という気がします…

7/30追記


教えていただきました。ありがとうございます。

QEPCADのインストールと簡単な使い方

QEPCADは量化子除去(QE, Quantifier Elimination)のためのアカデミックツールで、作者のサイト
QEPCAD - Quantifier Elimination by Cylindrical Algebraic Decomposition
で公開されています。インストールのために自前ビルドが必要な上に、サイトの案内
Downloading and Installing QEPCADにそのまま従ってもいまのUbuntuだとインストールに失敗するので覚書をしておきます。

# インストール
1. 必要なライブラリsaclibとQEPCAD本体を(適当なディレクトリで)ダウンロードする

$ wget https://www.usna.edu/CS/qepcadweb/INSTALL/qepcad-B.1.69.tar.gz
$ wget https://www.usna.edu/CS/qepcadweb/INSTALL/saclib2.2.6.tar.gz

2. saclibのビルドに必要になるので先にcshを入れておく

$ sudo apt install csh

3. 普通はccはCコンパイラを指している気がするが、一応ccと叩いて確認しておく。もしも指していないならgccを指すようにしておく。
4. saclibを展開して中に入る。

$ tar xf saclib2.2.6.tar.gz
$ cd saclib2.2.6

5. 変数saclibがそのディレクトリを指すようにする。makeが使うのでexportしておく必要がある。いまはsaclibディレクトリのなかにいるのでpwdでやってしまう。

export saclib=`pwd`

6. 以下を順次叩いてビルドする。何かhoge.hが足りないと言われたら適当にぐぐってそれを含むubuntuパッケージを見つけ(普通はhoge-devみたいな名前になっている)、aptでインストールする。

$ cd $saclib/bin
$ ./sconf
$ ./mkproto
$ ./mkmake
$ ./mklib all

7. エラーが出なければsaclibのインストールはおわり。
8. qepcadのビルドに使うので先にlibreadline-devを入れておく

$ sudo apt install libreadline-dev

9. qepcadを展開し、中に入る。ディレクトリはqesourceという名前になっている。

$ tar xf qepcad-B.1.69.tar.gz
$ cd qesource

10. 変数qeを設定する。これもmakeが使うのでexportしておく必要がある。いまはqesourceのなかにいるのでpwdでやってしまう。

$ export qe=`pwd`

11. サイトだとgmakeを叩くとなっているが普通にmakeを叩く。

$ make

11. 結構時間がかかる。何もエラーがでなければおわり。
f:id:sle:20180425063610p:plain
こんな感じのエラーが出たら、やっぱり足りないものが入っているパッケージをGoogle探してaptで入れる。
12. plot2dをビルドする。先にfreeglutを入れておく。

$ sudo apt install freeglut3-dev

13. makeする

$ cd $qe/plot2d
$ make

14. これでqesource/binにqepcadがビルドされているはず。必要に応じてパスを通す。

# 使い方
例と注意点だけ示す。今回は \exists x. x^2+bx+c=0 \wedge x \ge 0の量化子を消してみる。
1. 起動する。ここでびっくりしたのだが、先の変数qeと変数saclibが有効になっていないとセグフォで落ちるので頻繁に使うのならちゃんと起動時に変数が設定されるようにしておく。
2. このプログラムは対話で進んでいく。まずタイトルを要求されるので、ブラケットで囲んで指定しEnter。今回はhogeにする。

Enter an informal description  between '[' and ']':
[hoge]

3. 式に出てくる変数を、拘束される変数も自由変数もまとめて丸括弧囲み、カンマ区切りで書く。このとき、自由変数を先に、束縛変数(量化子のなかの変数)を後に書かなければならない。今回消したいのはxなので、xをあとに書く。また、拘束される変数は、式を冠頭標準形にしたときの順番で書かなければならない(今回は1個なので関係ないが)。

Enter a variable list:
(b,c,x)

4. 自由変数の個数を指定する。いまはbとcが自由なので2にする。

Enter the number of free variables:
2

5. 式を入力する。まず量化子と拘束する文字の組を並べて丸括弧で囲んで並べる。今回は存在量化子なので「(Ex)」となる。全称量化子のときは「(Ax)]とする。また、今回は量化子が1つだが、複数のときには3で入れた順番で量化子があらわれなければならない。例えば、「(a,b,x,y)」と変数を指定していて、自由変数の個数を2と指定しながら「(Ay)(Ex)」というのは駄目。次にブラケット(丸括弧でない)で囲んで式を書く。かけ算は空白を入れればよい。アンドは「/\」で、オアは「\/」で書く。その辺の記号は公式ページ
https://www.usna.edu/CS/qepcadweb/B/user/EnterForm.htmlにも書いてある。最後にピリオドを打ってEnter。打たないといつまで立っても始まらない(計算が重いんだなと勘違いしがち)。

(Ex)[x^2+b x+c=0 /\ x>=0].

6. よくわかんないけどずっとgoって答えると答えが出る。

=======================================================

Before Normalization >
go

Before Projection (x) >
go

Before Choice >
go

Before Solution >
go

An equivalent quantifier-free formula:

4 c - b^2 <= 0 /\ [ b < 0 \/ c <= 0 ]


=====================  The End  =======================

7. もしもtrueとかしか出なくて不満足なら、ここ
QEPCAD - Entering Formulas
を見ながらBefore solutionでsolution-extension Tなどを試すとよい。

Huaweiの端末はAndroidアプリのログを握り潰す

Adding Voice Capabilities | Android Developersにしたがって、RecognizerIntentを使った音声認識のコードを書いていたのだが、音声認識画面(下画像)でBackボタンを押すとアプリが落ちるという問題が発生した。
f:id:sle:20180226005755p:plain
Android StudioのLogcatを見ても、主要なメッセージは

02-26 00:59:56.197 24384-24384/com.example.ashia.speechwithoutintent I/HwSecImmHelper: mSecurityInputMethodService is null
(中略)
02-26 00:59:56.292 24384-24384/com.example.ashia.speechwithoutintent I/Process: Sending signal. PID: 24384 SIG: 9

しか出てこず、例外が発生したようではない。はじめは、音声認識画面のBackがメインのActivityまで伝わってしまってプログラムが終了するのだと思ってBackの信号を握り潰すなどをやってみがたどうにも解決しない。


しばらく(5時間ぐらい)、ぐぐったり飽きてゲームをしたりしていたのだが、最後にこのような記事を見つけた:
https://stackoverflow.com/questions/38587844/msecurityinputmethodservice-is-null-in-logcat
曰く、

For my Huawei device the following helps:

Dial:

#*#2846579#*#*

and a hidden menu is shown. Go to "Background Setting" -> "Log setting" and enable the log levels.

ということで、デフォルトではHuaweiの端末では、ある程度のログレベル以下のログは握り潰されてしまうらしい。ここにあるように、
電話アプリを起動して「*#*#2846579#*#*」と打つと、以下のような画面がでる。ちなみに、打ち間違えてバックスペースで消して打つと出ないような気がするので、一発で打つ必要があると思う。
f:id:sle:20180226010644p:plain
この上で、「Background Setting」→「Log setting」と入ると、チェックボックスが4つぐらい出てくるのですべてにチェックを入れる。「This might affect the performance!」みたいなことを言われるが、まあ覚悟の上である(必要ならあとで外したほうがいいかも)。

これでデバッグ実行をしてみると、

02-26 00:59:56.265 24384-24384/com.example.ashia.speechwithoutintent E/AndroidRuntime: FATAL EXCEPTION: main
Process: com.example.ashia.speechwithoutintent, PID: 24384
kotlin.NotImplementedError: An operation is not implemented: not implemented
at com.example.ashia.speechwithoutintent.MainActivity$M.onError(MainActivity.kt:44)
at android.speech.SpeechRecognizer$InternalListener$1.handleMessage(SpeechRecognizer.java:450)
at android.os.Handler.dispatchMessage(Handler.java:102)
at android.os.Looper.loop(Looper.java:150)
at android.app.ActivityThread.main(ActivityThread.java:5621)
at java.lang.reflect.Method.invoke(Native Method)
at com.android.internal.os.ZygoteInit$MethodAndArgsCaller.run(ZygoteInit.java:794)

のように新たにエラーメッセージを得ることができて、ちゃんと例外が起こっているということがわかるようになった。

ソフトウェアの基礎を読んでてCoqで詰まったところ(というよりは帰納法の使い方の話)

Hoare論理をCoqでやってみたかったのでソフトウェアの基礎を読んでいた。何かしら書いておかないと自分のなかで記憶がまたゼロに戻ってしまうので何かしら書いておく。当たり前のことをたくさん書く。あと、答えをそのまま書くのはよくないらしいので、Coqの証明を書きたい場面では自然言語での証明を書くに留める。

ソフトウェア的なところ(数学的でないところ)

環境構築

シンタックスハイライティング
  • はじめはubuntu上にapt install coqしたのだが、coqideのシンタックスハイライティングが有効にならなかった。id:qnighyさんに教えてもらって再起動したら直ったのでとりあえず再起動すべし。
コンパイルについて

Lists_Jからは

Require Export Basics_J.

しろというのが出てくるが、その前にBasics_J.vをコンパイルしなければいけない。(自分でBasics_J.vを使ってもよいが、
http://proofcafe.org/sf/sfja.tar.gz
からダウンロードするのが簡単だと思う。)このとき、Basics_J.vを開いた上でメニューの「Compile > Compile buffer」をするのだが、このときBasics_J.vの入っているディレクトリをカレントディレクトリにしておかないとコンパイルが通らなかった。したがって、コンパイルしたいときはcoqideコマンドをそのディレクトリで叩く必要があるっぽい。

コピペについて

ウェブサイトからCoqのコードをコピペしたくなることがあるが、∀はforallに直すなどしないとcoqide上で動いてくれない(本当は何か設定があるのかもしれない)。
そういうわけで、とりあえず次のようなコマンドを作ってxselと一緒に使っていた。

#!/bin/bash

sed -r 's/→/->/g' | sed -r 's/∀/forall/g' | sed -r 's/∧/\/\\/g' | sed -r 's/∨/\\\//g' | sed -r 's/∃/exists/g'

自然数の和の可換性(basic_induction)

Basics_Jの演習のbasic_inductionのplus_commについて。
教訓としては、「とりあえずでintrosするのをやめろ」ということになる。
まず日本語で証明を書いてみるとこうなる*1

  1. nについての帰納法で示す。自然数帰納法の原理は「P(n)を示すには、(a)P(0)を示し、(b)P(n)が成り立っているという仮定のもとでP(S n)を示せばよい。」であるから、P(n)を「任意のmについて『n+m=m+n』となる」として示す。
    1. P(0)を示す。0+m=m+0を示せばよいが、これはm=m+0と同じである。
    2. mについての帰納法でm=m+0を示す。Q(m)を「m=m+0」とする。
      1. Q(0)を示す。これは0=0+0を示すことだが、自明。
      2. Q(m)を仮定し、Q(S m)を示す。Q(m)は「m=m+0」であり、このもとでQ(S m)すなわち、「S m = S m + 0」を示せばよい。
        1. S m = S (m + 0) = S m + 0なので、示された。はじめの等式で帰納法の仮定Q(m)を用い、2つめの等式で自然数の足し算の定義を用いた。
    3. P(n)を仮定し、P(S n)を示す。P(n)、すなわち「任意のmについて、n+m=m+n」を用いてよい。
    4. mについての帰納法でP(S n)、すなわち「S n+m=m+S n」を示す。Q(m)を新たに「S n+m=m+S n」とする。
      1. Q(0)、すなわち「S n+0=0+S n」を示す。S n+0=S (n+0)=S(0+n)=S n=0+ S nなので、示された。ここで、1つ目の等式は足し算の定義、2つ目は帰納法の仮定であるP(n)で、∀mでm=0としたもの。3つめは足し算の定義、4つ目も帰納法の定義。
      2. Q(m)を仮定し、Q(S m)を示す。Q(m)、すなわち「S n+m=m+S n」を用いて、Q(S m)、すなわち「S n+S m = S m + S n」を示す。S n + S m=S (n + S m)=S(Sm + n)=S(S(m+n))である。1つ目の等式は足し算の定義、2つ目はP帰納法の仮定であるP(n)で、∀mでm=S mとしたもの。3つ目は足し算の定義。一方、S m+S n=S(m+S n)=S(Sm+n)=S(S(m+n))である。1つ目の等式は足し算の定義、2つ目はplus_n_Smとしてすでに示されている。3つ目は足し算の定義。

というわけで、まず帰納法を「任意のmについて『n+m=m+n』となる」としてスタートさせなくてはいけないので、

induction n.

と始めなくてはいけない。ここで

intros.
induction n.

とすると、固定したmについて証明が始まってしまってうまく行かない。
普段の手書きの証明だと、∀の外に出たり入ったりを無意識にやってしまうが、その辺をちゃんと意識してやらないとなあと思った。

ちなみに、この命題の証明をぼくはAMSから出ているSaunders MacLane, Garrett Birkhoffの「Algebra」でしか見たことがないんですが他に何かありますか。

リストの2回反転(list_exercisesでのrev_involute)

実は何回かソフトウェアの基礎に挑戦していて、何度もLists_Jのlist_exercisesのrev_involuteで苦戦しているので、手書き証明をここに置いておく。4つ目の等式は帰納法の仮定で、5つ目の等式のために補題を置くのがポイントになる。

f:id:sle:20171203200841p:plain

条件式が常にtrueと等価なWHILE文が停止しないこと

Equiv_JのWHILE_true_nontermの証明が何やってるかよくわからなくなって、段々帰納法ってなんだっけってなったので思い出した話。簡単なところなら帰納法のことが分かっていたつもりになっていたのだが、WHILE言語ぐらい複雑になると落ち着いて振り返らないとよく分からなくなっていた。

示したいのは、

Lemma WHILE_true_nonterm : ∀ b c st st',
     bequiv b BTrue →
     ~( (WHILE b DO c END) / st ⇓ st' ).

である。やりたいことは、「bが式BTrueと等価なら、WHILE b DO c END/st⇓st'がcevalの規則によって導かれるわけはない」ということなので、
cevalの規則から導かれる帰納法の原理ceval_indを上手く使って証明しなくてはいけない。
帰納法の原理ceval_indは、3つ組「c/ st ⇓ st'」についての述語「P(c/st ⇓ st')」を示すには、次のことを示せばいいことを教えてくれる。

  • ベースケース(前提に3つ組が出ない)
    • E_Skip: 任意のstについて、P(SKIP/st⇓st)が成り立つ。
    • E_Ass: 任意のst,a,l,nについて、整数式aがstのもとでnに評価されるなら、P(l::=a/st⇓(stのlをnで置換したもの)が成り立つ。
    • E_WhileEnd: 任意のb,st,cについて、bがstのもとでfalseに評価されるなら、P(WHILE b DO c END/st⇓st)が成り立つ。
  • ステップケース(前提に3つ組が出る)
    • E_Seq: 任意のc1,st,st',st'',c2について、P(c1/st⇓st')とP(c2/st'⇓st'')が成り立つなら、P(c1;c2/st⇓st'')が成り立つ。
    • E_IfTrue: 任意のb,st,st',c,c'について、bがstのもとでtrueに評価され、P(c/st⇓st')が成り立つなら、P(IF b THEN c ELSE c'/st⇓st')が成り立つ。
    • E_IfFalse: 任意のb,st,st',c,c'について、bがstのもとでfalseに評価され、P(c/st⇓st')が成り立つなら、P(IF b THEN c' ELSE c/st⇓st')が成り立つ。
    • E_WhileLoop: 任意のb,st,st',st'',cについて、bがstのもとでtrueに評価され、P(c/st⇓st')が成り立ち、P(WHILE b DO c END/st'⇓st'')が成り立つなら、P(WHILE b DO c END/st⇓st'')が成り立つ。

帰納法の原理はP(c/st ⇓ st')の形をしているので、これを示したいことである「任意のc,st,st'について、~( (WHILE b DO c END) / st ⇓ st' )」に合わせるには、P(c0/st0⇓st0')をcを固定した上で
「c0=(WHILE b DO c END)ならば、false」*2と、命題中でならばを使う。
これで示してみる。

  • Boolean式bはBTrueと等価とする。c,st,st'は固定する。
  • Pを上のように定義し、Pをcevalのの帰納法(この3つ組の導出についての帰納法)で示す。
    • E_Skipについて。P(SKIP/st0⇓st0)を示す。これは、「SKIP=(WHILE b DO c END)ならば、false」だが、「SKIP=(WHILE b DO c END)」というのは構文的におかしい。前提が偽なので、全体は真。
    • E_Assについて。これも同様に前提が「(l::=a)=(WHILE b DO c END)」となってしまって構文的におかしい。
    • E_WhlieEndについて。「bがstのもとでfalseに評価されるならば、P(WHILE b DO c0 END/st⇓st)」を示す。ところが、式bはBTrueと等価なので、前提の「bがstのもとでfalseに評価されるならば」が常に偽になり、全体が真になる。
    • E_Seqについて。「(c1;c2)=(WHILE b DO c END)」となり構文的におかしい。
    • E_IfTrueについて。やっぱり構文的におかしい。
    • E_IfFalseについて。やっぱり構文的におかしい。
    • E_WhileLoopについて。「bがst0のもとでtrueに評価され、P(c0/st0⇓st0')が成り立ち、P(WHILE b DO c0 END/st0'⇓st0'')が成り立つなら、false」を示す。
      • bがst0のもとでtrueに評価され、P(c0/st0⇓st0')が成り立ち、P(WHILE b0 DO c0 END/st0'⇓st0'')が成り立つとする。
      • 「P(c0/st0⇓st0')」は「c0=(WHILE b DO c END)ならば、false」である。
      • 「P(WHILE b DO c0 END/st0'⇓st0'')」は「(WHILE b DO c0 END)=(WHILE b DO c END)ならば、false」である。
      • 示したいのは「P(WHILE b DO c0 END/st0⇓st0'')」だったが、これは「(WHILE b DO c0 END)=(WHILE b DO c END)ならば、false」である。なので、「(WHILE b DO c0 END)=(WHILE b DO c END)」を仮定しよう。ここから、c0=cがわかる。このもとでfalseを導く。
      • 「(WHILE b DO c0 END)=(WHILE b DO c END)ならば、false」と「(WHILE b DO c0 END)=(WHILE b DO c END)」があるので、falseが得られる。示された。

多分、証明を思い付くには、「( (WHILE b DO c END) / st ⇓ st' )」が導出されたとして証明木の一番下がどう導出されたかを見ればよいんだろうなあと思う(?)

*1:Coq上でやろうとして5分行きづまったならとっとと紙と鉛筆をとって証明するべきである。本当に。

*2:この記事の書きはじめは「 任意のc,st,st'について、(c0/st0⇓st0')=(WHILE b DO c END/st⇓st')ならば、~(c0/st0⇓st0')」とやっていてこんがらがって死んでいた。P(c0/st0⇓st0')という書き方から、c0/st0⇓st0'は成立している。

順列を互換で整列するときの最小の回数

この記事のなかでは,互換,すなわち2つの位置だけを入れ替えるような置換のことをswapと呼ぶことにする.*1

長さnの順列\sigmaについて、swap列\sigma_1,\dots,\sigma_m\sigmaを整列するとは、
\sigma_m \dots \sigma_1 \sigma = \mathrm{id}となることであるとする.

命題1: 長さn\ge 3のサイクル\sigmaに対して,swap\tauを一回適用したときにできる順列\tau\sigmaをサイクル分解したときのサイクルの長さの和は少なくともn-1であり,またn-1にするような\tauは存在する.

命題1を証明する.
a\neq bについて,(場合1)(\tau\sigma)(a)\neq aかつ(\tau\sigma)(b)\neq bか,
(場合2)(\tau\sigma)(a) = aだが(\tau\sigma)(b)\neq bのどちらかが成り立つ.

場合1を考える.a\lt bと仮定して一般性を失なわない.
このとき,\tau\sigmaのサイクル分解を考えると,
1\to 2\to \dots \to a-1 \to b\to b+1\to \dots \to n \to 1というサイクルと,
a\to a+1\to \dots \to b-1 \to aというサイクルとに分解される.
ここで,場合1の仮定よりどちらの長さもきちんと2以上になっていることに注意する.
よって,サイクルの長さの和はnとなり,これはn-1以上である.

場合2を考える.\tau(1)=n,\tau(n)=1と仮定して一般性を失なわない.
このとき,1\to 2\to \dots \to n-1 \to 1という長さn-1のサイクルだけができる.
よって,サイクルの長さの和はn-1となる.これは,サイクルの長さの和をn-1にするような\tauの存在も示している.
命題1の証明おわり.

命題2: 長さn(>1)のサイクル\sigmaの整列に必要なswap列の長さの最小はn-1である.

命題2を証明する.その順列が整列されていることと,そのサイクル分解のサイクルの長さの和が0であることとは等価である.
n=2のときは明らか.n>3を考える.
命題1は,1回のswapではサイクル分解のサイクルの長さの和は高々1しか減らないこと,またそれを1減らすswapがあることを主張しているので,そこから分かる.命題2の証明おわり.

命題3: 順列\sigmaを整列するには,そのサイクル分解毎に整列するのが最短である.

命題3を証明する.順列\sigmaに対するswapのうち,2つのサイクル分解をまぜるようなもの\tauを考える.
\sigmaの分解には,(1,\dots,a)(a+1,\dots,b)とその他のサイクル\sigma_1,\dots,\sigma_mがあり,\tauaa+1を入れ替えるとして一般性を失なわない.このとき,\tau\sigmaのサイクル分解は,
1\to 2\to \dots \to a-1 \to b \to a+1 \to \dots \to b-1 \to a \to 1\sigma_1,\dots,\sigma_m
となり,サイクル分解のサイクルの長さの和は減少しない.
よって,サイクル分解毎に整列し,サイクルの長さの和を1ずつ減少させるのが最適である.
命題3の証明おわり.

*1:どっちがどっちかよく分からなくなるので.

ニトリで600円で買った風呂用の椅子を使って「君の名は。」の組紐を作ろう

f:id:sle:20170909134159j:plain
君の名は。」の聖地飛騨にやってきたので、「さくら物産館」さんで組紐作り体験をさせていただきました。
f:id:sle:20170909131518j:plain
あの映画の器械を使って組紐を作ることができ、こういうキーホルダーができます。


ちなみにこの組紐は伊賀のものらしく、飛騨は生糸の生産はやっていたけれども組紐はやっていなかったこと、映画のあとで旅行者に喜んでもらおうと思って組紐をはじめたことを教えてもらいました。実際楽しかったので是非おすすめします。

この組紐なのですが、頑張れば家でももう少ししょぼい装備でできるのではと思って、旅先で道具を調達し宿でやってみました。用意する道具材料はこんな感じです。


f:id:sle:20170909155230j:plain

  • 風呂用のイス(座面に穴が空いたやつ): 大体600円。ニトリで買った。
  • 重石(食卓用の陶製の塩の容器)9個: 1個50円。重石に使うだけなので、単1電池とかでもよい。
  • 目玉クリップ9個: 7個100円のを2個買った。先の重石の重みを支えられるぐらいの力が必要。
  • スズランテープ4色: 1色100円。組紐の材料になるので、4色必要。本当は毛糸が欲しかったのだが現地で調達できなかった。
  • ガムテープ: 100円。器械に目印をつけるのと、組紐の端を始末するのに使う。端の始末にはセロハンテープのほうが綺麗なので、あるならそちらを使うのがよい。
  • カッター: 普通のカッター。

(以下文章の簡潔さのためにである調になります。)

まず、作業に作る重石を作る。目玉クリップに紐(今回は組紐の材料のスズランテープを併用した)を通し、その両端をガムテープで重石に貼り付ける。
これを9個作る。こんな感じになる。
f:id:sle:20170909230628j:plain

次に作業台の器械を作る。
f:id:sle:20170909205016j:plain
この写真のように、6箇所にガムテープを貼っておく。これは紐の置き場所の目印になるとともに、滑り止めにもなる。

これで作業の準備にかかることができる。
1. 4色の紐から1メートル程度の長さで切り出す。あわせて8本の紐ができる。*1
2. 端をまとめてかた結びにする。
3. 結んだ端を、作業台(イス)の上から穴に通し、その端に下から重石をつける(目玉クリップではさむ)。
4. 4色に糸を、上の写真のように配置し、それらの糸が張るように、糸が座面の縁に接する少し下ぐらいに重石をつける(上の写真参照)。
5. まわりに伸びた糸が長すぎて互いに絡みそうであれば、まとめて他の糸で軽く結わえたり、クリップが余っていればそれで挟んだりする。まわりに伸びた糸を今後組紐を作る仮定で動かすことになるので、手軽に掴めるぐらいにコンパクトにしておくとよい。

これで組紐を作り始められる。
1. まず上の写真の状態から、青い紐を両手に取り時計まわりに半回転弱させる。ぶらさげた重石と残りの紐を手で包むようにして持つとよい。次の写真のようになる。青い紐と黄色い紐との位置が入れ替わったように見えることに注意。f:id:sle:20170909205035j:plain
2. 次に赤い紐を両手に取り時計まわりに半回転弱させる。赤い紐を置くときに、白い紐をもともと赤い紐があったところにずらし、赤い紐はもともと白い紐があったところに置く。次の写真のようになる。赤い紐と白い紐が入れ替わったように見えることに注意。f:id:sle:20170909205056j:plain
3. 次に、青い紐を両手に取り時計まわりに半回転弱させる。次の写真のようになる。青い紐と黄色い紐との位置が入れ替わったように見えることに注意。f:id:sle:20170909205111j:plain
4. 次に、白い紐を両手に取り時計まわりに半回転弱させる。白い紐を置くときに、赤い紐をもともと白い紐があったところにずらし、白い紐はもともと赤い紐があったところに置く。次の写真のようになる。赤い紐と白い紐が入れ替わったように見えることに注意。f:id:sle:20170909205136j:plain
5. これで1を始める前の紐の配置に戻ったことになる。あとはこの1-4を繰り返すと穴のなかに組紐がどんどんできていくことになる。

  • 作業中、周囲に垂れさがった重石がどんどん上がってきて、作業しづらくなることがある。このときはクリップの位置を変え、重石を少し下に下げる。写真参照。はじめの写真では、黄色の紐の重石の位置が上すぎるが、次の写真では少し降ろしてある。

*2
f:id:sle:20170909164341j:plainf:id:sle:20170909164355j:plain

  • また、作業中組紐が作業台の穴のなかにどんどんできていくが、そうすると組紐につけた重石(穴のなかの重石)の位置が下っていく。このとき、もし重石が床についてしまい、組紐に張る力が働かなくなるようならこの重石を(クリップを移動して)上に上げる。

十分な長さの組紐ができたら(15センチメートルも作れば満足だと思う。手首にも巻けるだろう。)、できた組紐の上の端(作業台の穴の側)にテープを巻く。
今回はガムテープしかなかったのでガムテープでやったが、セロハンテープのほうが良いと思う。作業台を少し浮かせて、作業台の下からやるのが良いと思う。
そして、巻いたテープの真ん中あたりで組紐をカッターを使って切る。作業台の下から作業することになり若干不安定なので、カッターで手を切らないように注意。
ハサミがあるならハサミのほうが良いと思う。

これで組紐が完成し、次の写真のようになる。


途中間違えたので途中がぐにゃぐにゃになっているが、はじめのほうなんかは模様が綺麗に出たのではないかと思う。

ちなみにあとで知ったのだが、世の中には「組紐プレート」というのがユザワヤあたりにあり、
これを使うと小さな装置で*3組紐が手軽に楽しめるらしい。へー。

あと、この風呂用の椅子を持って新幹線に乗って帰って大丈夫なんだろうか。

おわり。

*1:私は3メートルぐらい取ったのだが、長くなりすぎて作業しづらかった。失敗。

*2:ちなみに、オリジナルの方法では糸巻が重石を兼ねているが、紐の長さを調整できるように糸巻に紐を巻く方法がよくわからなかったのでこの方法をとった。まあ私のような素人が糸巻を使うと間違いなく絡まるのでこれで良かったのではないか。

*3:当然風呂用の椅子よりも