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

この記事のなかでは,互換,すなわち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:当然風呂用の椅子よりも

商環の同値関係a/s≡b/tをat=bsで定義してはいけない理由(あとまたAlloy)

またAtiyah-MacDonaldの可換環論入門を読んでいて、こんなことが書いてあった。

そのつくり方は、a,s∈A, s≠0なるすべての順序対(a, s)をとり、これらの組に対して次のように同値関係を定義することからなる。 (a,s)\equiv (b,t) \iff at-bs=0.この定義はAが整域であるときだけうまく昨日する。なぜなら、この関係が推移的であることの証明は消去律が成り立つこと、すなわちAは0と異なる零因子をもたないことを意味しているからである。

確かに商環の定義を at-bs=0としていけないとは習ったのだが、なんでそうしてはいけないのか、どんな例で推移律が失敗するのかを考えたことはなかった。とりあえず電車のなかで Z/4Zを積閉集合{1, 3}で商環にしたときのことを考えてみたのだがうまく行かなかったのでAlloyで調べてみた。

コードはgistに上げてある:
https://gist.github.com/ashiato45/0d0d0272dc6b2dc0ab22db2673a35d6b

  • isMultClosedでiが積閉集合であることの判定をする。
  • pEquiv [a, s, b, t]でa/sとb/tが上の意味で「等しい」かどうかを判定する。この関係をa/s \sim b/tと書くことにする。

これでmain3で、
「mcを積閉集合とし、a,b,cを環の元とし、s,t,uをmcの元とし、 a/s\sim b/t b/t\sim c/uがみたされているとする。このとき、 a/s\sim c/uが成り立つ。」と主張し、「check main3」でその反例を探しにいく。すると、次のような例がみつかった。
f:id:sle:20170531232016p:plain
これは、環 Z/2Zを考え、積閉集合として環全体をとり、 a/s=0/1, b/t=0/0, c/u=1/0を考えることに相当する。確かに at-bs=bu-ct=0だが、 au-cs=1となっていて、 0/1\sim 0/0, 0/0\sim 1/0だが 0/1\not\sim 1/0となっている。

そういうわけで一応反例は見つかったのだが、分母に0が来るのはなんとなく反則感があるので「積閉集合に0が入らない」という制約を追加して調べてみる。これがmain4である。実行すると、次のような例がみつかった。和と積は次のように入っている。
f:id:sle:20170531232919p:plain

this/Ring<:add={Ring$0->Element$0->Element$0->Element$2,
Ring$0->Element$0->Element$1->Element$3,
Ring$0->Element$0->Element$2->Element$0,
Ring$0->Element$0->Element$3->Element$1,
Ring$0->Element$1->Element$0->Element$3,
Ring$0->Element$1->Element$1->Element$2,
Ring$0->Element$1->Element$2->Element$1,
Ring$0->Element$1->Element$3->Element$0,
Ring$0->Element$2->Element$0->Element$0,
Ring$0->Element$2->Element$1->Element$1,
Ring$0->Element$2->Element$2->Element$2,
Ring$0->Element$2->Element$3->Element$3,
Ring$0->Element$3->Element$0->Element$1,
Ring$0->Element$3->Element$1->Element$0,
Ring$0->Element$3->Element$2->Element$3,
Ring$0->Element$3->Element$3->Element$2}
this/Ring<:mult={Ring$0->Element$0->Element$0->Element$0,
Ring$0->Element$0->Element$1->Element$1,
Ring$0->Element$0->Element$2->Element$2,
Ring$0->Element$0->Element$3->Element$3,
Ring$0->Element$1->Element$0->Element$1,
Ring$0->Element$1->Element$1->Element$1,
Ring$0->Element$1->Element$2->Element$2,
Ring$0->Element$1->Element$3->Element$2,
Ring$0->Element$2->Element$0->Element$2,
Ring$0->Element$2->Element$1->Element$2,
Ring$0->Element$2->Element$2->Element$2,
Ring$0->Element$2->Element$3->Element$2,
Ring$0->Element$3->Element$0->Element$3,
Ring$0->Element$3->Element$1->Element$2,
Ring$0->Element$3->Element$2->Element$2,
Ring$0->Element$3->Element$3->Element$3}

これは環 Z/2Z\times Z/2Zで、積閉集合として \{(0, 1), (1, 1)\}を考えている。
すると、 (1, 0)/(0, 1)\sim (0, 0)/(0, 1), (0, 0)/(0, 1)\sim (1, 0)/(1, 1)となっているが、
 (1, 0)/(0, 1)\not\sim (1, 0)/(1, 1) (1, 0)\cdot (1, 1) - (0, 1)\cdot (1, 1) = (1, 1) \neq (0, 0)よりわかる。

整域じゃない環について商環を真剣に考えたことがなかったので良い例が手に入って面白かった。あと、またAlloyが使えたので満足。

Alloyを使って可換環(有限)を調べてみる

ashiato45.hatenablog.jpで、prime avoidance lemma

環Aとそのイデアル\frak aと素イデアル\frak p_1,\dots,\frak p_nについて、
\frak a \subset \bigcup_{i=1}^n \frak p_iとなっているとする。
このとき、あるiに対して\frak a \subset \frak p_iとなる。

から素イデアル条件を外したときの反例を探していて、とりあえずn=2だと見つからないということを証明したのでした。
そこで、n=3のときの反例をAlloyで探そうとAlloyの勉強をしていたのですが、その前にid:qnighyさんが見つけてくれました(記事参照)。
とはいえ、やはりここでAlloyの使い方を覚えて反例探しを効率化したかったので、私は私でAlloyを使って見つけようと思っていたのでした。
ashiato45.hatenablog.jp
この記事で練習は済んだので、早速反例を探してみます。
コードはhttps://gist.github.com/ashiato45/bf148bfd114e45b0857baba6231e2a7cに貼ってあります。
あとちょっと補足しておくと、Alloyを使っている以上有限のものしか相手にできないので、もしも反例が無限の環にしかないのならお手上げです。

コードは群のときと大体同じです。今回は加法に対する単位元はzeroと名前をつけてあり、乗法に対する単位元はunと命名してあります。
oneにしなかったのは、Alloyのキーワードとぶつかっているからで、とりあえずフランス語の「1」にしておきました。
途中で可換環の定義が正しくできていることを確かめるために例を表示してみたのですが(50行目)、割と初心者殺しの観がある零環*1が見つかったのを見て、
「確かにAlloyで予めモデリングしておけばバグ発見に役立ちそうだなあ」と思いました。

そして、我々の例について位数8以下の環について例を探させたところ、次のものを得ました。
f:id:sle:20170219150720p:plain
元は8個で、Elements(番号)という形で出てくるので、ここではそれらをa_0,\dots,a_7と書くことにします。
出力によると1=a_3であり、0=a_7です。
そして、イデアル
{\frak a} = \{a_4,a_5,a_6,a_7\}{\frak p}_1 = \{a_6, a_7\}{\frak p}_2 = \{a_5, a_7\}{\frak p}_3 = \{a_4, a_7\}
でした。これを見ながら、これがどのような環かを考えてみます。

まず、8つの元の環なので、有限生成アーベル群の分類定理から、加法については{\mathbb Z}/8{\mathbb Z}{\mathbb Z}/4{\mathbb Z} \times {\mathbb Z}/2{\mathbb Z}({\mathbb Z}/2{\mathbb Z})^3のいずれかであることが分かります。
イデアル{\frak p}_1,{\frak p}_2,{\frak p}_3を見ると、2倍にすると0になる異なる元が3つあることになるので、とりあえず{\mathbb Z}/8{\mathbb Z}ではなさそうです。
2倍したときの性質は気になるので、さらにa_0,a_1,a_2,a_3の様子を加法の表(画像参照)で調べると、
a_0+a_0 = a_1 + a_1 = a_2 + a_2 = a_3 + a_3 = a_4となることがわかります。2倍して非零な同じものa_4になる異なる元が4つあるので、({\mathbb Z}/2{\mathbb Z})^3でもなさそうです。よって、この環の和についての構造は{\mathbb Z}/4{\mathbb Z} \times {\mathbb Z}/2{\mathbb Z}だということが分かります。
この環のなかで2倍された元でかつ非零な元というのは(2,0)しか有り得ないので、a_4=(2,0)が分かります。
さらに、a_0+a_0 = a_1 + a_1 = a_2 + a_2 = a_3 + a_3 = a_4ということを考えてみると、
a_0,a_1,a_2,a_3はそれぞれ(1,0),(3,0),(1,1),(3,1)のどれかであることがわかります。a_5,a_6は2倍すると0になる元でかつa_4=(2,0)ではないので、(2,1),(0,1)のいずれかであることがわかります。

積については何も見ていないのですが、(1,1)が多分乗法についての単位元だろうという気がするのでそれで辻褄が合うかを見てみます。
つまり、この環は{\mathbb Z}/4{\mathbb Z} \times {\mathbb Z}/2{\mathbb Z}に要素毎の加法と乗法を入れたもので、0=(0,0)であり、1=(1,1)であるものであり、
{\frak a}=\{(2,0),(2,1),(0,1),(0,0)\}{\frak p}_1=\{(0,0),(2,0)\}{\frak p}_2=\{(0,0),(2,1)\}{\frak p}_3=\{(0,0),(0,1)\}であるということになります。考えてみると、これで確かに辻褄があっていて、無事に反例が見つかり、その構造がわかりました。めでたしめでたし。

*1:元が1つで、その元が0でもあり1でもある環。この上では(かの有名な)0=1が成立する。

Alloyを使って有限群を調べてみる

Alloyはモノを抽象的に記述したり、それらの関係を数学で言うところの「関係」でもって記述する言語です。
さらに、そこで記された制約を満足する例を見つけたり、制約に対する反例を見つけたりするための解析器がついてます。
プログラムの仕様をこれで記述して、それに対して見落しがないかを探すのに便利みたいです。
公式サイトhttp://alloy.mit.edu/alloy/の記述を引用すると、

Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks.

ということになります。

以前http://ashiato45.hatenablog.jp/entry/2017/02/08/220148で、環に対する反例を見つけるのにAlloyを使おうと思ってこの本

抽象によるソフトウェア設計−Alloyではじめる形式手法−

抽象によるソフトウェア設計−Alloyではじめる形式手法−

で勉強していたのですが、ざっくり読んだのでid:qnighyさんが以前群でやっていたのを思い出しつつAlloyで群の性質を調べてみました。

できたコードはhttps://gist.github.com/ashiato45/b46837f5ff1237fa9c12e64ddaf4711eにあります。

sig Element{}

one sig Group{
	elements: set Element,
	unit: one elements,
	mult: elements -> elements -> one elements,
	inv: elements -> one elements
}

fact NoRedundantElements{
	all e: Element | e in Group.elements
}

まず元としてElementを宣言しておきます。これで、何らかの集合Elementが定義されます*1

それで、群を定義します。群は要素を持ち、うち丁度1つが単位元で、2つの元に対して丁度1つ元を定めるmultがあり、1つの元に対してその逆元を求めるinvがあるということを記述します。いま1つの群についてのみ考えたいので、「one sig Group」とすることでGroupは群を丁度1つだけ含む集合ということにします*2。NoRedundantElementsというfactで、このモデルにあらわれる要素というのはすべて群で使うものとします。この制約がないと、特に意味のない元が例に現れてしまって邪魔です。

fact UnitLaw1{
	all a: Group.elements | Group.mult [a] [Group.unit] = a
}

fact UnitLaw2{
	all a: Group.elements |
	Group.mult [Group.unit] [a] = a
}

fact AssociativeLaw{
	all a: Group.elements | all b: Group.elements | all c:Group.elements |
	Group.mult [Group.mult [a] [b]] [c] = Group.mult [a] [Group.mult [b] [c]]
}

fact InvLaw1{
	all a: Group.elements | Group.mult [Group.inv[a]] [a] = Group.unit
}

assert InvLaw2 {
	all a: Group.elements | Group.mult [a] [Group.inv[a]] = Group.unit
}

check InvLaw2

さらに、群の制約を書き足します。単位元の制約、結合則はいいのですが、逆元について制約は、「任意の元aについて、aのinvは左からかけると単位元になる」ということしか言っていません。InvLaw2は同じことを右からで言っているのですが、こちらは制約ではなくただの成り立ってほしいと思っている命題です。ここで、最後の行でこの命題が成り立つかを検査します。結果、Alloyの検査器は「多分正しい」と教えてくれます。「多分」というのはAlloyは有限個の範囲でしか検査せず、デフォルトだとすべての集合が3つ以下しか元を持たないという制約のもとで(上手に)総当たりします*3。これで、「多分正しいだろう」と人間も予想できるので証明してみます。示すことは、「任意の元bについて、ここで定義した意味でのbのinvは右からかけると単位元になる」ということ。bのinvのことを、b^{-1}と書くことにし、単位元はeで書きます。

aをいま考えている群の元とする。InvLaw1から、a^{-1}\cdot a = eとなる。同様に、(a^{-1})^{-1}\cdot a^{-1} = eとなる。よって、結合則より
a=e\cdot a = (a^{-1})^{-1}\cdot a^{-1}\cdot a = (a^{-1})^{-1}となる。よって、任意のaについてa=(a^{-1})^{-1}が成立する。

bを群の元とする。先のことから、b=(b^{-1})^{-1}となり、b\cdot b^{-1} = (b^{-1})^{-1}\cdot b^{-1} = eとなる。証明おわり。

ということでこのcheckはコメントアウトして先に進む。

次に、

run {}

で、ここまでの制約をみたすような例を表示してみます。Executeを実行して、Showをクリックすると訳のわからん図が出てきます。ここで、図のなかにGroupが出てきてるのが邪魔なので、表示画面の「Theme」をクリックして、出てくる「sig Group」を選択し、「Project over this sig」をonにして「Close」すると
f:id:sle:20170218231435p:plain
こんな感じで群が出てきます。Element1に「unit」と書いてあるので、これが単位元だとわかります。この群はもちろんZ/2Zで演算を和としたものです。
さらに、Nextをクリックすると他の例を探してくれます。いくらか押すと、位数3の群も出てきます。
若干演算がよく分からないので、「Evaluator」をクリックします。ここでは、対話型で出てきた例を調べることができます。
f:id:sle:20170218231842p:plain
ここで、「Group.mult」と叩くと演算multがどうなっているかが見えます。

もう満足したので、このrunはコメントアウトして先に進みます。

assert Commutativity{
	all a: Group.elements | all b: Group.elements | Group.mult [a] [b] = Group.mult [b] [a]
}

check Commutativity for 5

このassertは群が可換であることを意味します。そして、checkでこれが本当に成立するかどうかを確かめます。「for 5」がついていて、位数5以内でこれを確かめます。Executeを押すと「多分正しい」と出てきます。これで、この命題は多分正しそうだということになり、「全ての群は可換である」という気がしてくるのですが*4、念の為もうちょっと大きく、

check Commutativity for 6

f:id:sle:20170218233114p:plain
と変えて実行すると、「反例が見つかりました」と出てきます。すごい。

これで満足したのでcheckはコメントアウトして先に進みます。
今回私が本当に調べたかったのは、

Gを群とし、AをGの正規部分群、BはAの正規部分群とする。このとき、BはGの正規部分群か?

です。これは割と落とし穴でちょっと考えるぐらいだと分かりません。このためには、

pred subgroup (g: set Element, h: set Element){
	(all a: g | a in h) and
	(Group.unit in g) and
	(all a, b: g | Group.mult [a] [b] in g) and
	(all a: g | Group.inv[a] in g)
}

pred regularSubgroup(n: set Element, g: set Element){
	subgroup [n, g] and
	(all n0: n, g0: g | Group.mult [Group.mult [g0] [n0]] [Group.inv[g0]] in n)
}

pred main(n1: set Element, n2: set Element){
	let g = Group.elements |
	regularSubgroup [n1, g] and
	(some g0: g | (not g0 in n1)) and
	regularSubgroup [n2, n1] and
	(some n10: n1 | (not n10 in n2)) and
	(not regularSubgroup [n2, g])
}

と書きます。subgroupは要素の集合2つをとる述語で、その範囲で演算が閉じているかを確かめます。
regularSubgroupも要素の集合2つをとって、正規部分群になっているかを調べます。
mainが調べたいことで、特に意味はないのですが真の正規部分群になっているという条件もついてます。これで

run main for 7

とすると「多分正しい」となります。さらに、「for 8」としてみると、今度は反例を見つけてくれます。
f:id:sle:20170218233114p:plain
めでたしめでたし。

*1:実際どういう集合かというのは制約を見つつAlloyが探してくれるわけなので、「この集合は何?」というのを記述する必要はありません。

*2:普通の言語に慣れているとこれらは関数に見えるのですが、実際は数学で言うところの関係、つまり直積集合の部分集合になっています。ドットで普通のオブジェクト指向言語のように要素へのアクセスをしているように見えるのですが、実際は関係の推移になっています。これで望みのものが書けてしまうというのは結構面白いので是非やってみてください。

*3:ちなみに手元のマシンでデフォルト設定で探索したところ、位数15では反例を見つけられませんでしたが、20だとエラーになりました。

*4:しません

Atiyah-MacDonaldのProposition 1.11について(prime avoidance lemma, 2/13追記)

Atiyah-MacDonaldの「可換代数入門」のProposition 1.11では、

環Aとそのイデアル\frak aと素イデアル\frak p_1,\dots,\frak p_nについて、
\frak a \subset \bigcup_{i=1}^n \frak p_iとなっているとする。
このとき、あるiに対して\frak a \subset \frak p_iとなる。

ということが書いてある。この素イデアルの条件を外すと不味いのかなと思って、
n=2で反例を探していたのだがずっと見つからなかった。
しかし、今日n=2だと素イデアルの条件なしでも同様のことが言えてしまうと気づいたので書いておく。

示すことは、

環Aとそのイデアル\frak a,\frak b,\frak cについて、\frak a\subset \frak b \cup \frak cが成り立っているとする。
このとき、\frak a\subset \frak b\frak a\subset \frak cかのどちらかが成り立つ。

である。背理法で示す。仮に、
(1)\frak a\subset \frak b\cup \frak c、(2)\frak a \not\subset \frak b、(3)\frak a\not\subset \frak cのすべてが成立していたとする。
仮に、\frak b\subset \frak cだとすると、\frak b\cup \frak c = \frak cとなって(1)に反するので、(4)\frak b\not\subset \frak cである。
同様に、(5)\frak c\not\subset \frak bも成り立つ。(2)、(3)、(4)、(5)より、x \in (\frak b\setminus \frak c)\cap \frak a
y\in (\frak c\setminus \frak b)\cap \frak aが成り立つようなxとyが存在する*1x,y\in \frak aなので、(1)よりx+y\in \frak a\subset \frak b\cup \frak cとなる。
よって、x+y\in \frak bx+y\in \frak cかのどちらかは成立する。
前者が成立するとする。y=(x+y)-xだが、xは定義から、x+yは仮定より\frak bの元なので、y\frak bの元である。
これはyの定義に反し、矛盾である。後者が成立すると仮定すると同様にx\in \frak cが導かれ、矛盾する。
よって、どちらにしても矛盾する。証明おわり。

というわけで少なくともn≧3で探さないと意味がないっぽい。Alloyで探してみようと思う。

2/13追記

id:qnighyさんがn=3で例を見つけてくれました。


2次の項全部で割ってるので有限の環になってます。これならAlloyでも見つけられそう(勉強中)。
加群ぽく考えるのが大事みたいです。

あと、タイトルのprime avoidanceの説明をしてなかったのですが、このAtiyah-MacDonaldのProposition 1.11には
prime avoidanceという名前がついているようで、こんな記事https://en.wikipedia.org/wiki/Prime_avoidance_lemmaがあります。

*1:2/13修正

公式のPythonとAnacondaを共存させる(備忘録)

おもに備忘録。すでにPython3が入っていたのですが、科学計算用のライブラリのインストールがうまく行かなくて結局Anacondaを入れることにしました。そうすると、どちらのPythonにパスを通すかというのが問題になりますが、切り替えられるようにバッチを書くことにしました。そのとき、batファイルの書き方が奇っ怪で腹が立ったのでこれを機にPowerShellを使ってみることにしました。等号が-eqだったりするのが奇妙ですがはるかに良い。


gist63a91d89b1679e6e7cb91c3da8e7a76c

これを適当なパスの通った場所に置いておいて、PowerShellから「setpythonpath anaconda」とか叩けばOK。Pathのほうは、デフォルトとして使いたいほうだけパスを通しておく。

はじめはPythonPathという環境変数を作って、そこにPythonのパスを書き、Pathのほうには「%PythonPath%」と書いておけば、PythonPathを書き換えるだけで切り替えができるだろうと思っていたのですが、どこかの時点でPathのなかの%PythonPath%が展開されてしまうようで、PythonPathを書き換えても意味がありませんでした。