2020-05-04

なんちゃって水晶仮晶を室内で形成する

鉱物 3Dプリンタ

鉱物とは，wikipediaによると，

地質学的作用により形成される、天然に産する一定の化学組成を有した無機質結晶質物質

と書かれています．

先日，3Dプリンタと低融点金属を使って，なんちゃって水晶仮晶を地質学的作用を用いずに形成したので，その理由と方法についてまとめました．

まず，水晶（石英）にいてどの程度ご存知でしょうか．

地殻に最も多く含まれるケイ素を主成分とすることから，石英は最も一般的な鉱物と言えるでしょう．安定度の高い圧電体でもあることから，時計やスマホ・通信などにも広く使われているので，一度も見たことがない人は，そうそういないのではないかと思います．
これが結晶化すると水晶と呼ばれ，六方晶系・三方晶系に分類される結晶構造ととります．みなさんもご存知の，6角柱状のあれです．

条線と3Dプリンタの関係

水晶に限らず，結晶化した鉱物には条線が見られることがあります．これは水晶の場合は柱面に現れ，水晶の場合は６角柱の６角形面同士を結ぶ線分とは垂直に形成されます（=晶帯と平行）．
岩石でいう条線とは異なり，鉱物での条線は，結晶の成長が広がる方向（水晶の場合は，六角形を大きくする方向）と伸びる方向（六角形面同士を結ぶ線分が長くなる方向）の成長速度にある程度差が生まれた際に，その時形成されている柱面にその速度の差が段のように形成されることによって生じます．
なるべく厳密に書きましたが，要は，太くなる速度が遅いと，その前後で柱面の太さが若干変化する，それが線のように見えているということです．
で，この条線，3Dプリンタの印刷物に見える，積層ピッチそのものですよね？
時間連続的に積み上げるわけでなく，ノズルが一本しかないので離散的にならざるを得ない３Dプリンタの造形方法はまさしくこの条線を表しているのです．
すなわち，3Dプリンタを使えば，明瞭な条線をもつ水晶がつくれるわけです．
実際，この気づきが今回の作品のきっかけになりました．

仮晶

ご存知かもしれませんが，そうでない方のために説明すると，鉱物の世界では仮晶という現象があります．
これは，鉱物の結晶構造が保ったまま，結晶を構成する原子や化学式が別のものに置換される現象です．
有名なところだと，オパール化したアンモナイトなどはショップや博物館などでも見た事があると思います．
wikipediaにある黄鉄鉱仮晶がだいぶ綺麗な写真ですが，より一般的にわかりやすいであろう，水晶に置換された方解石仮晶の写真URLを貼っておきます．
方解石だった水晶 - iStone

ご存知の通り，方解石 $CaCo_3$ は菱面平行六面体として形成されることで有名ですが，上の写真ではその形を維持したまま水晶に置換されてしまっています．あはれなり．

色々な仮晶があり，下記URLのように通販もされています．
仮晶(カショウ) Pseudomorph

水晶仮晶

ケイ素が多いからなのが，水晶に置換された鉱物は多いですが，私が調べた限りでは水晶からべつのものに置換された例は見つけられませんでした．ご存知の方がいたら教えてください．

低融点金属

MONOTAROで先日，低融点金属が安く手に入ることを知りましたこんなに安く手に入るんですね，びっくり
低融点金属ケニスその他学童用実験器具・実験用品【通販モノタロウ】 Uアロイ70P〜
Uアロイというアサヒメタル製造の合金で，Uは”湯”で融けるかららしいです．日本製ということがよくわかります．
鉛・カドミウムフリーもあるらしいですが，私が購入した製品はCd，Bi，Sn，Pbの合金らしいです．
取り扱いには注意しましょう．

水晶仮晶を形成する（物品）

必要なものは以下の通り

3Dプリンタ・樹脂
- Uアロイの融点が70度なので，ABS, PLAどちらでも良い．
Uアロイ 50gx5個　（=1袋）
- 私の作例では４個で足りました
湯煎用鍋
- 雪平鍋を使いました．万能です
ガラス瓶
- Uアロイを融かすのに使用．Pb含有のため蓋付がbetter
軍手
- ガラス瓶を安全にもつため．
キッチンペーパー
- Uアロイ作業場所 & ガラス瓶の水気を拭うため
ハンマー，ニッパ，ラジオペンチ，超音波カッターなど
- 鋳型の破壊に使います．壊せ壊せ壊せ！！私は昔鉱物用に買ったEstwingのロックピックハンマーを使いましたが，このように先の尖ったものの方が作業性は良いと思います．

水晶仮晶を形成する（手順）

サポート材なしで鋳型を印刷します．私の場合は，フリー素材で水晶のSTLを探してきて，TinkerCadで読み込み，立方体をくり抜くことで鋳型を作りましたが，まるまる立方体で覆うと破壊のプロセスで苦労したので，下半分だけ立方体にするとか，ところどころきれこみを入れるなどして，樹脂の節約と破壊のし易さを追求すると時間も短縮できてbetter．

なお，このファイルのURLを以下に貼っておきます．
3D design Crystal | Tinkercad
f:id:wvogel00:20200504120541p:plain

印刷が終わったら，Uアロイを融かしていきます，料理にも使う鍋を使用する場合は，ガラス瓶に蓋をした方が安全かもしれません．私は蓋せずにやりました．溶けはじめはものすごく臭いので，臭気を吸わないようにして，換気もしましょう．この時，軍手を二重にしてはめておくとガラス瓶をつかめます．私はふり混ぜながら融かしました．当然ですが，一度融解が始まったら振った方が速いです．

f:id:wvogel00:20200504120604p:plain

全部溶けたら，ガラス瓶を取り出し，軍手が濡れないように瓶の周りの水気を拭ってから鋳型に流し込みます．この時，樹脂と金属を剥離しやすいように何か手を講じた方が良いです，油を塗る，石膏粉をまぶすなどを考えていますが，効果的かどうかはわかりません，

固まるのを待ちます．融点低いので冷めるのも速い気がします．私は2hくらい放置しました．

解体します．オススメはニッパで切り込みを入れながらハンマーの尖端を打ち込み外径を破壊し，金属に近づいてきたらニッパと超音波カッターで頑張る方法です．

飾ります．
1. 3Dプリンタの積層ピッチがいい感じに条線を表現してくれていますね！これで金属に置換された水晶仮晶の完成です！

f:id:wvogel00:20200504120629p:plain

以上です．
鉱物好きな人が増えてくれたら嬉しいなと思って作りました．

参考資料

必携鉱物鑑定図鑑 / 藤原卓【編著】/益富地学会館【監修】 - 紀伊國屋書店ウェブストア
 水晶の構造と形
 レムリアンシード - iStone

2020-04-30

未使用言語をAtCoderで触る

先日，ふと思い立って，使ったことのない言語を触ってみたくなりました．

ただHello Worldするのは面白みがないので，AtCoderのA,B問題を解いてみました．触ったことないと言いつつ，F#やFortranも含まれているので，触ったけれど記憶が薄れた言語も含まれています．

ソースコードはこちら

ルール

・1日でやる（あくまで遊び）

・AtCoderの同じ問題を解いた他人の提出コードはみない

・「言語名　競技プログラミング」での検索は許す

できるだけB問題は関数化なども試しましたが，Kotlin, Ruby, F#に関しては友人と実装速度（もとい検索力）を競いながら書いたのでそんな余裕はありませんでした笑

なお，当初は触ることが目的だったので，上で述べた3言語以外は全て同じ問題セットを解いています．

第一言語：D言語

いい言語でした．この言語のおかげで他の言語も楽勝や！と思ってしまいました．A・B問題を解く限りではCの文法をそのまま使うだけなので，抵抗は感じませんでした．これは非常に大事ですね．マルチパラダイムな機能をもっと色々試したくなりました．

第二言語：Go

適当に書いたら，関数宣言や変数の型の宣言方法がこれまでみたことない形式なので戸惑いました．あと，{}の改行位置でエラーが出るのは勘弁してほしい．推論機能がコンパイル時にどれだけ厳しく検査されるのか今回は見ることがなかったので，今思うと少し勿体無かった．

第三言語：Fortran

こいつに一番苦しみました．おかしいな...昔触ったことがあるなのに...最も初期に誕生した高級言語であることをすっかり失念していて，if分が一行でかけないことや入出力方法の検索に苦労しました．Fortranに関しては，よもや口伝で実装方法を伝承してきたのかと思うほどに情報があちこちに分散していて非常に学習コストが高かったです．まあ一度慣れれば非常にシンプルなんですが．

昨今のスパコン事情を知りませんが，できれば触りたくない言語です．

第四言語：OCaml

唯一，main関数の書き方でつまずきました．まさか単語mainが出てこないとは思いませんでした．Fortranでさんざ苦しんだ後なので，パターンマッチに出会えて文明世界に戻ったようで嬉しかったです．純粋関数も副作用をもつ関数も渡し合うことが可能でやや戸惑いましたが，実装は非常に楽です．しっかり関数化すればあまり恐れることはないように思います．

第五言語：Kotlin

いままでずっと（コットリン）と読んでいました．Kotlinユーザには常識でしょうか，varとvalの違いにハマりました．また，些細ですがuntil文法は可読性をあげるいい例だと感じます．C#的で割と素直な言語ですね．最近ユーザーが伸びていると聞きますが，他にも理由があるのでしょう（調べる気0）

第六言語：Ruby

今回チャレンジした中で唯一の国産言語を初体験です．kotlinに似ているようで，ややfortranみも感じました．あとelsifってなんですか？elifがelse ifじゃだめなんでしょうか．割とサクサク実装できましたが，少しモヤモヤしてしまいます．いやまあPythonにももやもやしているのでそれと同種のものでしょう．

第七言語：F#

学生時代に.Netアプリケーションも作ったことあるのでサクサクいけるだろうと思ったらすっかり記憶から抜けていました．しかしOCamlで慣れた後なのでそれほど苦しむ事もありません．ただ型推論が不完全らしいので，大規模開発するときの苦労が気になります．

まとめ

頭の体操にはちょうど良かったです．

ただ，一番苦労したのは,gitアカウントの切り替えに伴うgitの設定だったかもしれません．

いや，やっぱりFortranの入出力か．

以上

2020-04-14

楕円曲線暗号（EC Elgamal）を実装する

Haskell EC Elgamal

少し前の記事でIUT理論に関する書籍を読んでいましたが，その中で楕円曲線の対称性を利用したという記述がありました．また，楕円曲線の持つ特殊性から暗号分野にも応用されていると．
恥ずかしながら私はRSA暗号・AES暗号あたりしか触ったことがなく，楕円曲線暗号の理論を知らなかったので，今回その基本機能を実装することにしました．最近javaを強いられていて心が疲弊しているので，久々にHaskellを使います．
今回は下記書籍が大変参考になりました．

暗号理論と楕円曲線数学的土壌の上に花開く暗号技術 | 森北出版株式会社
後ろの章で扱う定理や用語が大分前の章で使われるなど，ページをいったりきたりしたものの，
練習問題も多く，総じて学部以来ご無沙汰な人間にもとても分かりやすかったです．
その他参考にした文献は末尾にまとめました．

楕円曲線上の加算

楕円暗号は，RSA暗号での鍵長1024bitに相当する安全性を，わずか160bitで実現することができます．
$E : Y^2 = x^3 + aX + b$
の楕円曲線方程式上で，大きな素位数において巡回群となるよう
Eと $\mathbb{F}_p$ を選ぶことが出来れば，暗号実装の舞台は整います．
なお，以下ではすべて，pによる剰余類群上での話として扱います．
この際，楕円曲線上の点の数がほとんど素数であれば安全性が高いと言え，スクーフのアルゴリズムで計算可能です．ただ，今回は楕円方程式の探索は行っていないので詳しいことは資料を当たってください．
※ $\mathbb{F}_p$ :: $\mathbb{Z}/p\mathbb{Z}$ でpが素数の時， $\mathbb{Z}/p\mathbb{Z}$ は０を除いて逆元を有し有限個の元をもつ有限体を形成する．また，これを $\mathbb{F}_p$ と書く．通常，暗号では $\mathbb{F}_2$ が使用されるようです．本記事では書籍に則りp=31を使います．
楕円曲線暗号のアルゴリズムについては多くのwebサイトで開設されているのでそちらに譲りますが，剰余類楕円曲線上の加法演算についてはまとめておきます．

楕円曲線 $E$ 上の点 $P_1, P_2$ があるとき， $P_1 + P_2$ とは，単純に二点の座標を座標軸ごとに加算する方法は，楕円曲線上に乗りませんので成立しません．
そこでまず，この二点を結ぶ直線を考えます．( $P_2 = P_1$ の時は $P_1$ での接線となる)
すると，ベズーの定理より，全次数3のEと全次数1の直線は， $nm=3$ 個の点，すなわち， $P_1,P_2$ 以外にもう一点，直線と曲線が交わる点が存在します．この点と単位元Oを結ぶ直線も，[tex;E]ともう一点で交わります．この点を， $P_1+P_2$ と定めています．
このように定めると，座標の足し算は成立し，Oは単位元なので $P+O=P$ とならなければなりませんが，これが成立することも図を描けば誰でも容易に確認できます．なお，このOの存在性は有理数体上では難しいらしいのですが，暗号で扱う有限体上では必ず存在するそうです．ありがたい！
そして暗号理論では特に， $P_1 = P_2$ を利用しています．この時， $P_1 + P_2 = P_1 + P_1 = 2P_1$ の倍々算が可能となり，暗号計算の高速化が実現されます．
この倍算については以下でちらっと登場します．

※全次数 :: 方程式を構成する多項式中の単項式のうち，すべての変数の次数の和の最大値

暗号化と復号

今，
送信元の秘密鍵 ... a
送信先の秘密鍵...b
送信先の公開鍵 ... 楕円座標，計算の開始点（ベースポイント）P，B(=bP)
に関する情報が送信元に与えられたとします．

送信元

送信元は，メッセージ $M$ を公開鍵を使って暗号化されたメッセージ $M' = M+aB = M+abP$ を生成し，送信先に， $(M', A(=aP))$ を送信します．

送信先

$(M',A$ を受信した送信先は，自分の持っている秘密鍵を使って，
$bA = abP$ を得ます．これによってメッセージ $M_{rec}$ を
$M_{rec} = M' - bA = (M+abP) - abP = M$
として復元できるのです．

倍算による高速演算

上記，暗号復号で登場した， $aP$ や $bP$ の演算は，単純に実施するとa回の演算が必要となってしまいます．ここで，aをバイナリ展開し，
$aP = \Sigma_{i=0} a_i2^i(2^iP)$ とすることで，計算量を $\log 2 a$ に抑えることができます．
また，バイナリ展開では除算が多数必要となりますが，これを1回で済ませる手法として，射影座標を用いる加算方法も存在します．詳細は割愛しますが，これまで考えてきたアフィン座標を射影座標での形に換算する方法です．私もまだ理解し終えていないので，資料を当たってください．

実装

以上を実装していきます．
ソースコードはこちらに掲載していますので，一部のみ説明します．
なお，型の設計を頑張ったものの，全然スマートでないと思うのでご意見あればよろしくお願いします．

instance Num ResidueRingInteger where
    a + b = if getn a == getn b then ResidueRingInteger ((getv a+getv b) `mod` getn a) (getn a) else undefined
    a - b = if getn a == getn b then ResidueRingInteger ((getv a-getv b) `mod` getn a) (getn a) else undefined
    a * b = if getn a == getn b then ResidueRingInteger ((getv a*getv b) `mod` getn a) (getn a) else undefined
    negate a = ResidueRingInteger ((getn a)-(getv a)) (getn a)
    abs a = ResidueRingInteger (getv a `mod` getn a) (getn a)
    fromInteger v = undefined

instance Fractional ResidueRingInteger where
	a / b = ResidueRingInteger ((getv a * (getv $ revSrc b)) `mod` getn a) (getn a)
	recip = undefined
	fromRational = undefined

ここでは，剰余還上での演算ということで，加法・乗法が定義できます．また，逆元を有するために除算も定義可能です．
値は，自分自身の値と，その剰余系での法を情報としてもつと考え，ResidueRingInteger型を用意，これについて四則演算を定義しなおしています．
fromIntegerも，fromInteger p = ResidueRingInteger 0 p　として定義しても良いかもしれませんが，混乱を生みそうなので非実装としました．（このおかげで開発中，バグを回避できた）

つづいて，楕円曲線E上での暗号ですので，暗号系は，楕円と座標に関する情報を有します．

data ECCrypto = ECCrypto{x :: ResidueRingInteger, y :: ResidueRingInteger, curve :: ECurve} deriving Eq

暗号・復号に必要な加算を実装します．
今気づいたけど，めっちゃスペース入ってますね...いつもと違う環境で書いたから..

(+++) :: ECCrypto -> ECCrypto -> ECCrypto
a +++ b = a{x = x3, y = -lambda*x3 - nu} where
			x3 = if a == b
				then lambda*lambda-multi 2 (x a)
				else lambda * lambda -(x a) - (x b)
			lambda = if a == b
				then (multi 3 (x a)*(x a) + (get1 $ curve a) ) / (multi 2 (y a))
				else ((y b)-(y a)) /((x b)-(x a))
			nu = (y a) - lambda * (x a)

そして，二審展開による加法演算を実装します．

multiplyOnEC :: ECCrypto -> Integer -> ECCrypto
multiplyOnEC ec = fromJust.snd.foldl multiplyOnEC' (ec, Nothing).toBin where
	multiplyOnEC' :: (ECCrypto, Maybe ECCrypto) -> Integer -> (ECCrypto, Maybe ECCrypto)
	multiplyOnEC' (nP,result) 0 = (nP+++nP, result)
	multiplyOnEC' (nP,Nothing) 1 = (nP+++nP, Just nP)
	multiplyOnEC' (nP,Just result) 1 = (nP+++nP, Just $ result +++ nP)

最後に，暗号・復号を書き下します．

encrypto :: PublicKey -> Rank -> SecretKey -> [Integer] -> (ECCrypto, [Integer])
encrypto (_P,bP) rank secretkey message = (aP, map encrypto' message) where
	encrypto' = flip mod rank.( + (getv $ x abP))
	aP = multiplyOnEC _P secretkey
	abP = multiplyOnEC bP secretkey

decrypto :: (ECCrypto, [Integer]) -> Rank -> [Integer]
decrypto (aP, message) rank = map decrypto' message where
	decrypto' m = (m - (getv $ x abP)) `mod` rank
	abP = multiplyOnEC aP secretkey_b

非常に素直ですね．
参考にした書籍にあった関数と例題で，正常に動作することを確認しました．
ただ，素位数=41の巡回群でのサンプルなので，[0-41]の範囲しか扱えません．
参考資料3では，もっと大きい素数たちが使用されていますので参考にしてください．

攻撃

楕円曲線暗号の解読には完全指数時間要しますが，利用されている楕円曲線上離散対数の乗法巡回群（すなわち拡大体上の離散対数）へ変換して解読する手法があるようです．(MOV攻撃，FR攻撃)
ヴェイユペアリングがよく用いられるようですが，書籍によると超特異曲線でなければこの攻撃は回避でき，埋め込み次数を高くすればよいとのことです．

※埋め込み次数 :: 有限体を拡大する時に必要となる最小の拡大次数

また，暗号の本を読んでいてグレブナ基底が出てくるとは思っていませんでした．
量子コンピュータが実現されれば既存の暗号の多くは破られる見込みですが，これに対抗する暗号として期待されているのが多変数公開鍵暗号です．ただこの暗号についても，グレブナ基底を使って順繰りに多項式を正規化していく解読手法があります．複雑な多項式の構成方法や多項式の複雑さの評価などまだまだ調査不足ですので，既存のフレームワークで量子計算に耐えうるってめちゃめちゃ格好良くないですか？また取り組んでみたいと思います．

参考文献

1. 暗号理論と楕円曲線数学的土壌の上に花開く暗号技術 | 森北出版株式会社
2. Theory and Implementation of Eliptic Curve Cryptography
3. 楕円エルガマル暗号の実装

2020-04-09

様相論理入門

療養中，特にやることもなく（医師曰く，”只管横になって体を休めること！”），仕方がないので小説を読み漁っています．
ジャンルはSFとミステリーが多くて，小川一水さんの本をはじめとして色々読んでいるのですが，
その中で井上真偽の「恋と禁忌の術語論理」がとても印象に残りました．
titleの通り，術語論理のもとに他の人の推理を検証していくだけの話なのですが，その中で様相論理について触れています．
様相論理とは，常に真とは言えない命題を扱えるようにしたもので，□φや♢φで表現されます．
私が学んできた集合論は古典的論理で展開される範疇でしたので，論理学の世界は自分が思っていたよりも奥が深いことを知り衝撃を受けました．
その後，本の中では探偵がモーダス・ポネンスを書き下していくのですが，論理学にいろんな表現があることを知って非常に興味を持ったので，書籍を購入して勉強しました．

www.kyoritsu-pub.co.jp

良い本です．古典的論理学のはじまりから最近の研究課題まで知ることができます．
しかし初学者には勿論なかなかに難しく，様相論理がどんなものかを知りたかっただけの私は，この書籍で論理学の沼を見てしまいました．
様相論理について学ぶだけなら，第一部第二部を読めば十分でした．
強制法で何が展開されるのか愚かにも興味を持ってしまったのが運の尽きです．第三部の証明は面白いところだけ拾い読みして読むのがおすすめです．
強制法がよく理解できなかったので，Hamkinsの論文(※参考文献)を少しずつ読み進めています．

書籍の中でも，当初の目的の様相論理と認識論理（時間論理を含む）の内容が面白かったので自分のために簡単にまとめておきます．
詳細な証明や厳密な定義は書籍や関連資料に当たってください．
とにかく，タルスキ・クリプキらの功績がすさまじいです．

様相論理

書籍から引用すると，「様相論理とは，伝統的には命題の必然性・可能性・不可能性などの様相概念を扱う論理」で，
必然であることを示す演算子□，可能であることを示す演算子♢を使って表現が拡張された論理です．
この表現によって時制論理や命題動的論理PDLに応用範囲を広げていきます．
命題動的論理はその記述方法自体がプログラムとも関連が深いので計算機界隈の人間ならご存知かもしれません．
ある集合上の二項関係Rについて，その定義可能性は次表で与えられます．

分類	論理式	Rの性質
T	□p → p	反射的
B	p → □♢p	対称的
4	□p → □□p	推移的
5	♢p → □♢p	ユークリッド的
D	□p → ♢p	継起的
.2	♢□p → □♢p	有向的
L	□(□p→p) → □p	推移的且つ無限上昇列がない

この表は正規様相論理の性質を探るうえで非常に重要なので，備忘録用に掲載しています．
様相論理のシークエント計算体系を進めるうえでは，扱う正規様相論理がどの性質を満たしているかによって，実行できる計算内容が変わってきます．
※なお，強制法で拡張された論理はS4.2（T,4,.2を含む正規様相論理）と一致するらしいです．このあたりを詳しく知るために上述した論文を当たっています．

この表にある性質によって，正規様相論理はグラフ構造や関係を表現でき活躍の場を広げていきます．

最初様相論理を知った時には，このような可能性をはらんだ論理で解を一意に定めることができるのかと怪しみました．
小説では，正規様相論理上で決定可能性を検証していくのですが，書籍によると正規様相論理では
・”ある実効的な手続きPが存在して，任意の論理式φをPへ入力したとき， $\vdash_\Lambda \phi$ の時にはPが真を出力し，そうでない時は偽を出力する時，決定可能”となります．

認識論理

現実においては，エージェントごとに知識の内容が変わることも多々あります．
エージェントごとに変わる知識内容は，エージェントa∈Aに対して様相演算子 $□_a$ （aは~~を知っている）を用いて，例えば正の内省”aがφであることを知っている”を $□_a φ \rightarrow □_a□_aφ$ として表現できます．
このような知識の状態を表現できることに感動しました．

次に，命題が常に真とは限らないものとして，例えば命題”彼は笑っている”は，今は真であってもその後変わるかもしれません．
このような論理について認識論理では，公開告知演算子[φ]ψで表現が拡張されます．
これは，”真なφが公開告知された後にψ”を意味し，状態の変化を表現することが可能になり，詳細な定義は割愛するとモデルMを使って
$M,\omega \models [\phi]\psi \Longleftrightarrow M,\omega \models \phi ならば M^\phi, \omega \models \psi$
で[φ]ψの充足表現は定められます．
なお， $M \models \phi$ は，φはMから意味論的に帰結可能であることを意味しています．

書籍では，公開告知演算子と様相演算子で表現しながら，有名なシェリルの誕生日問題を解いています．
難問論理クイズ「幼女とシェリルの誕生日」で有名問題を撃破せよ - 明日は未来だ！

その他雑記

当初の目的の一つだった，恋と禁忌の術語論理で扱われたモーダス・ポネンスのシークエント計算やカット除去法についてもこの本に詳しく記載されていました．
ゲーデル数はコーディング値
強制様相論理ではボタンやスイッチが専門用語として登場してきて，思わず笑ってしまいました．
集合論・論理学をなめていました．数学の表現力はすさまじいです．

参考文献

数学における証明と真理 ―様相論理と数学基礎論― / 菊池誠編佐野勝彦倉橋太志薄葉季路黒川英徳菊池誠著 | 共立出版
J.D.Hamkins : The modal logic of forcing, https://arxiv.org/pdf/math/0509616.pdf

2020-04-04

IUT理論：備忘録

先日，京大の望月教授が提唱したIUT理論の論文が8年越しにacceptedされ，ABC予想についての証明が正しいと話題になった．

最初私は，ABC予想を解いたのだと興奮したものの，よくよく調べると，ABCについて取り組んだだけではなく，IUT理論(Inter-universe Teichmüller theory)の構築をする上で解かれたと知りさらに衝撃を受けた．

私は数学の専門家でもなんでもないので，流石に膨大な量の原著をあたることはできないが，初心者にも雰囲気をつかめるよう書かれた書籍があったので一夜賭けて読んだ．本記事はその備忘録・及び関連論文を自分用にまとめたものである．
www.amazon.co.jp

ABC予想

abc-tripleについて，次式を満たすような自然数の組は高々有限個しか存在しない（であろう）．
$rad(abc)^{1+ε} < c$
注1. abc-triple ... 自然数の組(a,b,c)についてc = a+b, a < b, a,bは互いに素
注2. rad n ... 根基．互いに異なる素因数の積

IUT理論

誤解を恐れず一言で言うならば，
IUT理論は正則構造の破壊された複数の宇宙を用意し，
それぞれの宇宙間で計算された情報を対称性を介してやり取りする．
この時，対称性のやりとりだけでは正確に元の情報を復元することはできないのでひずみが生じるが，このひずみの量を定量的に評価できるようにすることがIUT理論の骨である．

対称性を使った情報のやりとりでは，対称性の制約が厳しくなるほど，復元される情報の精度も高くなり，宇宙間のやり取りで生じるひずみ量も小さくなる．このような対称性をもつものとして，遠アーベルなものの代表である楕円曲線と関係の深いテータ関数を採用している．ちなみに遠アーベルとは，可換な性質な者からより遠い性質というもので，上で述べたように対称性の条件が厳しいことに相当します．このあたりには群論も絡んでくるので，定性的にはわりとすんなり理解できるでしょう．
同一の事象に対して，複数の解釈を持つ群を得ることが可能であり（書籍では正方形を例にしている），このことから，群を使えば，対称性の粒度は違えど複数の群（=異なる解釈によって得られた群）を往来できる世界が構築できたり，入れ子構造を形成できることがわかる．IUT理論ではこれを積極的に利用し，最終的に複数の世界間の関係を関係式に落とし込む．

こういった対称性や群による復元はガロアの時代から進められてきたが，IUT理論では複数の宇宙を用意して正則条件が敗れた状態で，ひずみを許容しながら（最終的にはこのひずみが非常に小さいことを示す）情報を行き来させて関係式を得る．
書籍には終わりの方に簡単な数式があり，それを読めば不等号式が得られるまでの雰囲気をつかむことが出来る．

この，ひずみを定量的に評価できるようになった，というのがIUT理論のすごいところだと思います．そのための手法として，宇宙際を作り出してしまうところも，アラケロフ幾何にあるような周到な準備を重ねたところも，私には想像もできない苦労と知恵があったのだろうと思います．

あと，全然関係ないですが，対称性って数学の政界でも物理の世界でも非常に強力な性質なのですね...
最近，32次元でのゲージ対称性について知ったばかりなので，数学と物理の間のつながりが感じられて個人的に感動しました．

テータ関数

基本的な形は次式で与えられるが，これとは別に楕円テータ関数もある．
$\theta(z,\tau) := \Sigma^\infty_{n=-\infty} \exp^{\pi i n^2r + 2\pi inz}$
(wikipedia, ”テータ関数”より)
テータ関数は，多くの対称性と強固に関係しているらしいのですが，調べると様々な対称性を持つ形に変形できるので，このテータ関数の作り方も工夫の一つだったのだと思います．

ホッジ・アラケロフ幾何

「標数0の非特異な楕円曲線の普遍拡大における次数ｄ以下の多項式関数空間から、ｄ等分点でのｄ^2次元関数空間への自然な同型射が存在する」を定理として証明した．

参考文献

www.amazon.co.jp
テータ関数 - Wikipedia
宇宙際タイヒミュラー理論 - Yourpedia

2020-03-23

家電をRN4020+androidで一括制御するその壱(ハードウェア側)

先日妹が結婚し新居での生活を始めた．
新生活に当たり欲しいものがないか聞いたところ，下記スマートリモコンをお願いされた．

Nature スマートリモコン Nature Remo　

ネット経由でアクセスし，赤外線で家電を操作してくれるらしいです．
ちなみに，amazon echoとも連携してくれるらしい．便利．
でもなんか，これくらい作れそうじゃね？

我が家は1Kと手狭なので，机の上くらいは広く使いたいところすが，リモコンを置くことでそれなりに場所を占有されるうえに，なんか整理整頓されていない感じが出てしまっています．
うん，私も机の上からリモコンを消そう．
残念ながら我が家にはamazon echoはなく，また特に屋外から家電を操作したいという欲求もないので，シンプルにandroid/BLE/PICを使ってリモコンレスを目指します．

プロジェクト名

可視光ではないけれど光を使った装置ということで，それにちなんだ名前として今回はNightHeronを採用します．
日本語だとゴイサギなのですが，このゴイサギには”青鷺火”（別名：五位の火）といって鷺のからだが青白く発光する怪現象が伝えられているようです．

リモコンでの家電制御

リモコンからの家電制御は，シンプルに1,0のバイト列を送信しているわけではなく，およそ38kHzで変調したCW信号で制御しています．この変調波形は，家電に信号を認識させるためのReader部，LSBファーストのデータ部，そして信号の終了を示すTrailer部から構成されており
0.35ms <= T <= 0.5ms　としたとき，データ部において
'0'を送信 -> 38kHz明滅をT[ms]，消灯をT[ms]送信
'1'を送信 -> 38kHz明滅をT[ms]，消灯を3T[ms]送信
することとなっています．
ちなみにReader部は，8T変調後4T消灯，Trailer部ではT[ms]変調後，およそ40ms以上消灯します．

回路設計

何かないかと部品箱を漁ったらRN4020が出てきたのでこれを使いましょう．ドラえもんがポケット漁る時もこんな感じなのかな．
家電製品の赤外LEDはおおよそ940nm付近のものが使われており，部品箱を漁ると，こちらもちょうど940nmのものがありました．
　　・赤外LED ... L-53F3BT (940nm)
　　・フォトトランジスタ ... BPW76A (940nm)
動けばいいので回路は適当に設計します．

f:id:wvogel00:20200322235823p:plain — 回路図

なお，シンプルにエミッタ接地で制御すると，38kHz変調時に波形追従が悪く若干鈍ってしまうので，スピードアップコンデンサを追加しました．
定数は下記LTSpiceシミュレーション結果に従います．右回路がスピードアップコンデンサを追加した回路で，波形を見ると立ち上がり・立下り応答が改善されていることがわかります．画像では立下り後に若干持ち上がりがあるものの，オシロでバラック回路を観測した限りでは特に気になりませんでした．（この時のオシロ波形も保存しておけばよかった..）
解析結果を見ると，追従性能が改善したためかLEDに流れる電流量も稼げていることがわかります．

f:id:wvogel00:20200323000221p:plain — スピードアップコンデンサ定数評価

基板開発

適当に基板に起こします．
画像のピンク線で囲まれた領域は，RN4020のアンテナ特性を損なわないための開口領域なので，ここには部品・パターンを配置しないようにしましょう．
...ただ，3DCGを見るとわかるように，右上にあけたドリル穴に少しランドが残っていることを見落としてしまいました．
発注した基板にも当然残っている．そこまで影響しないはずなので目を瞑る．
ちなみに，RN4020のアンテナはメアンダ逆Fアンテナでした．

f:id:wvogel00:20200323000612p:plain — pcb図面

f:id:wvogel00:20200323000716p:plain — 3D基板

いつもはFusionPCBを使っているが，今回はお試しの意味でJLCPCBに発注．
DHLは確実ですね，1weekで届きました（この基板を発注する前に別基板を発注，SF Expressに配送を依頼していますが，一か月経つ今もまだ届かず...）

さて，基板が届いたら実装しますよね．
赤外LEDは3つまで実装できますが，指向性が強く家電との位置取りを考える必要があるため，写真では一つしか実装していません．

f:id:wvogel00:20200323001447p:plain — 届いた基板(両面)

f:id:wvogel00:20200323001609p:plain — マイコン側

f:id:wvogel00:20200323001656p:plain — RN4020側

シリアル通信を試験しなかったので，デバッグの意味も込めてシリアル-USB変換モジュールを搭載していますが，
開発が終了したらば，ただのmicro-USB端子あるいはその他電源端子でいいです．
常に給電しながら動作させるので，けちらずに32MHzで動作させます．このおかげでRN4020のdefault baud rate(115200)で通信できます．

また，フォトトランジスタが搭載されているのは，あとで家電が増えた時に信号の読み込みができるようにするためですが，まだ機能は実装していません．

ソフトウェア

さあ，適当にソースコードを書いていきます．
なお，androidアプリが実装できたらリモコンの制御バイト列データはすべてandroidから送信する予定ですが，
今はまだandroidアプリがないのでソースコードに埋め込んでいます．
github( https://github.com/wvogel00/NightHeron.X )に置いていますが，説明が必要な箇所だけ抜粋します．

まず38kHz変調をかける箇所ですが，この中での20us遅延は，赤外光の変調周波数をオシロで確認しながら決定しました．
マイコンの動作周波数が変わると当然変わるので注意していください．(8MHzクロックの時は大体12us遅延)
今思うとPWM使ったら良かったかな．

void Output1T()
{
    //pulse width = 26.2us when 38.2kHz modulation
    const int repeatN = 400/26.2; // 400us / pulse width
    for(char i = 0; i < repeatN; i++)
    {
        IR = HIGH;
        __delay_us(20);
        IR = LOW;
    }
}

続いて制御信号は，上で述べたフォーマットに従ってSendIUCommand関数で生成しています．
すでに述べたように，Reader-data-trailerから構成され，データ列はLSBファーストです．

void SendIRCommand(char* data, int n)
{
    //Reader
    for(int i = 0; i < 8; i++)
        Output1T();
    __delay_us(1600);
    
    //data
    for(int i = 0; i < n; i++)
    {
        char c = data[i];
        for(int j = 0; j < 8; j++)  //LSB first
        {
            if (0x01 & c)
                Output1();
            else
                Output0();
            c = (c >> 1);
        }
    }
    
    //Traller
    Output1();
}

RN4020の設定をします．
折角プロジェクト名を決めたのでデバイス名もこれに合わせます．
SSコマンドではサーバーサービスを決定します．今回はユーザー定義を使うので0x00000001に設定します．
SRコマンドでは使用する機能を設定します．今回はAuto Advertize, Support MDLP, No Direct Advertisement, UART Flow Controlを設定します．まあ実際にはフロー制御はしないのですが，MLDPを使うのに必要なので．
PSコマンドでprivate serviceのUUIDを設定します．
最後にPCコマンドでprivate characteristicを設定しますが，PCコマンドはPSコマンドの後に実行する必要があります．
ここでは読み書き両方設定するので0x42，そして第三引数はcharacteristicが保持する最大バイト数です．
最後にRコマンドで再起動し設定を反映します．

void SetRN4020()
{
    WAKE_HW = HIGH;
    __delay_ms(100);
    WAKE_SW = HIGH; // RN4020 send the text, "CMD", through UTX line
    __delay_ms(10);    

    SendText_UART("PZ", 2);  //clear private service
    SendText_UART("SN,NightHeron", 13);     //device name
    SendText_UART("SDM,NightHeron", 14);    //Model-Characteristic name
    SendText_UART("SDN,WTORII", 10);        //manufacture name
    SendText_UART("SS,00000001", 11);       //private profile
    SendText_UART("SR,36000000", 11);
    SendText_UART("PS,cd3152d04ddb86610f4d7fd794da92f9",35);
    SendText_UART("PC,cd3162d04ddb86610f4d7fd794da92f9,42,05", 41);
    
    SendText_UART("R,1", 3);    
}

Main関数ではMLDPモードに入るまでの監視だけ実行します．
RN4020にはMLDP機能(Microchip Low-energy Data Profile)が搭載されており，
このモードに入るとペアリングしたデバイスから送信したバイト列がシリアル通信経由でPICで受け取ることができます．
PICからMLDPをONするピンを接続し忘れましたが，ペアリングしたデバイスから何かしらのバイト列を送信するとMLDPモードに入ってくれます．

void main(void) {
    Initialize();
    SetRN4020();
    
    while(1)
    {
        __delay_ms(2000);
        if(IsEqual(uartBuf, "CMD", 3) || IsEqual(uartBuf, "ERR", 3))
        {
            ;//do nothing
        }
        else if(IsEqual(uartBuf, "MLDP",4))
        {
            waitingMode = 1;
            //SendText_UART("ready",5);
        }
    }
    return;
}

android側はこれから開発していきます．

ちなみに，まだ基板とPICだけはいくつか在庫があるので，もし欲しい方がいればお譲りします．

参考

青鷺火 : https://ja.wikipedia.org/wiki/%E9%9D%92%E9%B7%BA%E7%81%AB
メーカー純正リモコンのコード : http://shrkn65.nobody.jp/remocon/database.html
スピードアップコンデンサ：https://cc.cqpub.co.jp/system/contents/2430/
RN4020ユーザーガイド : https://ww1.microchip.com/downloads/jp/DeviceDoc/70005191A_JP.pdf

2020-02-15

Kicad5 + Tinkercadで3Dモデルを作成

kicadで自作ライブラリを使っていると，3D viewにしても画像のように実際の形状を知ることができず，部品同士の干渉の不安を抱えながら進めていくことになる．

基盤加工機でガリガリ削る分には極小パターンは作成できないため集積度が上がらずあまり問題にならないが，両面基板を外注して集積度を上げようとすると厳しくなってくる．そこで，オンラインで使えるTinkercadを使ってサクッとモデルを作成し，kicadnお3D viewに反映していく．

すでにたくさんの人がfusion360などを使用した実例を挙げてくれているのでサクサク書いていく．

この記事では秋月でも買えるTMHU28を扱う．こんな小さななりをしているにも関わらず５種類の入力が扱えるので随分前から重宝している．

http://akizukidenshi.com/catalog/g/gP-08072/

f:id:wvogel00:20200215151022p:plain — TMHU28寸法図

こいつのfootprintをkicadに登録した時には，3Dデータがないため3D viewにしても下のように見えるだけである．虚しい．ちなみに，SW1のシルクが打ってある箇所である．

早速tinkercadでCGを作成する

アカウントは以前登録していたので，直方体やら円筒やらを組み合わせていく．

出来上がったのがこちら．

天面に筋が走っているのは，おそらく0.1mmほど計算を間違えたため．しかし0.1mmを争う設計はしていないのでこのまま許容して進める．

色が違うオブケジュト単位でまとめてSTLを作成していく．

今回は

　レバーなどの黒部分...TMHU28black.stl
　端子部分...TMHU28_conn.stl
　その他...TMHU28white.stl
として出力した．

それを，MeshLabで読み込む．これは，kicad 3D viewerでみた時に色も見えるようにするためである．色が不要の場合は，MeshLabは読み飛ばそう．

MeshLabは当方の環境には未インストールだったため急いで入れた．少し癖があって使いにくいが，愛すべきTMHU28のためである．耐えよう．

MeshLabの手続きは以下のサイトの通り進めさせていただいた．
ポリゴンを削減処理が必要ない場合は色だけバシバシつける．

https://www.usagi1975.com/18may172231/

完成したら，色つきVRML(.wrl)ファイルを出力．
kicadのPcbnew画面に戻る．

TMHU28を選択してE(編集)モードに入ると，3D Settingのタブがあるので軽快にクリック．下の画像のようにファイルのパスをこれまた軽快に設定する．$(MY3D)はkicad上の環境変数なので設定したい場合は右に見える設定パスから設定する．
参考に，着色前のCG画像も掲載しておく．
色センスがないから着色後も抜群とは言えないが，ある方が良いということが伝われば幸い....

上記参考サイトではMeshLabから出力する際に縮尺を合わせていたが，
すっかり忘れていたのでkicad上で合わせる．0.394倍という数値だ．
原点がずれていたため，角度・位置を合わせ込んでいく．