2017年冬〜春アニメまとめ

概要

冬は「この素晴らしき世界に祝福を!2」「CHAOS;CHILD」くらいしか面白いものがなくて不作であった…と思ったら、あとで追いついた幼女戦記がここ一番の出来だった。。春は完走は多かったものの「有頂天家族2」が突出していてベルセルク2期は安定、次点は「つぐもも」か。

リアルタイムではないが2017年上半期に後から完走したものとして「響け!ユーフォニアム」2期、東京喰種√A、青の払魔師、この素晴らしき世界に祝福を!、SAOおよびSAO2、有頂天家族1期、幼女戦記Charlotteなどが高評価だった。

個別

昨年秋アニメも残していないものがいくつかあったので合祀。面白いところはネタバレしないように気をつけています。

  • 無星: 見る価値がない。一応完走
  • ★: 一度は見ておいた方がよい
  • ★★: もう一度見返しておきたい
  • ★★★: 他人に自信をもって勧めたいレベル

幼女戦記 ★★★

前世紀の魔法大戦物だけど、転生もの。空戦の描写はハリウッド的で迫力があってSEもよい。なんとも言えぬ閉塞感の中でとにかく勝ちまくるのが非常に気持ちがよい。帝国が滅ぶところが全然想像できない。アニメでは時間が足りなかったが、漫画だとすれ違いが強調されていてこれは別にまた面白い。2017年上半期個人的No.1をあげたい。

eYe's 【通常盤】

eYe's 【通常盤】


オープニングテーマが非常に気に入ったのでアルバムを買ったら、Re:ゼロでもいくつか曲提供している人たちだった

ゼロから始める魔法の書

傭兵とゼロの魔法の国のお話。国が案外小さいのと、ゼロの魔術師団があまり賢くなくて悲しい。傭兵のハイパー超人クライミング技術はすごいんじゃないかと思う。

終末何してますか?忙しいですか?救ってもらっていいですか?

ようわからんかった…原作みたら面白いと思えるのかもしれないけど、ファンタジー度が高くて俺には難しそう。ヒロインが14、15歳なのに結婚とかいうのもちょっとオッサンにはきつい。

ソートオラトリア ダンまち外伝

ダンまちが面白かっただけにちょっと残念。59階層に着いて終わりで、アイズの正体は生い立ちに切り込んでからが面白そうなのだけど、2期がちょっとなさそうな感じ…

有頂天家族2 ★★★

一家の心温まるドタバタ喜劇に、天狗親子の確執と愛情を織り交ぜてより面白くなった。

有頂天家族 ★★★

一家の心温まるドタバタ喜劇。ウィットのある会話と話のおかしさと家族の絆がとてもよい。優しくなれるお話

有頂天家族 (幻冬舎文庫)

有頂天家族 (幻冬舎文庫)

武装少女マキャベリズム

武闘派学園ハーレムもの。

ベルセルク2期 ★★

安定。断罪の塔編終了後から

ロクでなし魔術講師と禁忌教典

肌の露出多い以外はなかなか面白い魔法学園もの。主人公がやる気がないっていう典型的なところが感情移入できてすばらしい。結局アカシックレコードのカケラも出てこなかったが、二期は厳しそう。

つぐもも ★★

軽快でテンポのよい定番コメディ。戦闘シーンはまあまあ迫力があるし、主人公の成長もよい。今思ったけど、かなり「かんなぎ」にクリソツじゃね…?

この素晴らしい世界に祝福を!2 ★★

安心してゲラゲラ笑いながら見れるのでよい

この素晴らしい世界に祝福を! ★★

ゲラゲラ笑いながら見れるのでよい

CHAOS;CHILD

妄想科学ADVっていうけど全然科学的じゃなくて悲しい。10年前のテキストゲーをみているよう

風夏

ひたすらだるい、人気絶頂のアイドルと幼馴染で三角関係とか30過ぎたオッサンにはきつい少年誌ファンタジー。そんな簡単にベース覚えたり作曲したりできるわけねえだろ!

ガンダムTHE ORIGIN IV ★

UC最初のモビルスーツ戦のやつ。まあこれはガンダム税なので…

響け!ユーフォニアム2 ★★★

前期は地方予選。全国大会まで行って…部活する女子高生がどんどん成長していくのがよい。

響け!ユーフォニアム ★★★

とにかくみんなかわいい。部活する女子高生の機微がこれでもかと描かれていて(当時理解できなかったのが)つらい。

鉄血のオルフェンズ2期 ★

ガンダム税とられましたって感じ…ラスタルエリオンがそのままってのはどーも納得いかないですね

終末のイゼッタ

なんか考え方が封建っぽい、魔法戦闘のシーンはかっこいいのだけど、幼女戦記を見てしまった今では非常に色あせてみえる。

双星の陰陽師

陰陽師幽霊戦闘、体の一部が人間じゃなくなった変態系の中学生〜高校生の成長モノ。長かった、普通に分かりやすく少年誌でよいはなし。

セイレン

9話までみたけどだる過ぎて切った。ストーリーはともかく作画崩壊が多くて原作の魅力が台無しなのでは。原作みてないけど。

非リアルタイム

dアニメストアで配信された過去の作品を少しずつ見ていく。

Charlotte ★★★

面白くて一気に見てしまった。展開がベタで分かりやすいのだけど、友利がかわいい(そればっかりだけど)のでつい見てしまう。途中で出てきた華僑系っぽいマフィアはえらく中途半端で弱かったり、1年かそこら?で世界中の能力者から能力を奪うなんてできるのか?それだとせいぜい数千人くらいしか能力を奪えない気がするのだけども。

結城友奈は勇者である

まあまあいい話だったけど、最後の出来事(大赦が勇者を解放したアレ)だけがどうしてもわからない。女の子に「うおおおおおおおおおおおお!!!!」って言わせるのを楽しむやつ。

未確認で進行形 ★★

日常系なんだけど小紅がとにかくかわいい。前半だるいけど後半からテンポ上がって飽きなくなる。

ソードアート・オンラインII

GGO編とエクスカリバー編。詩乃がとにかくかわいいが、展開が1期に比べてちょっと平凡というかスリルに欠ける。スリル要素が少数の悪役に絞られてしまったところが厳しいか。

ソードアート・オンライン ★★

最強主人公モノはやっぱり定番で王道。SAO編はやっぱり命がかかっているというスリルがあって非常によかったが、ALO編はヒールを倒すだけの話になってしまってちょっと残念。あと、2年も寝たきりで意識のない人間はもっとやつれてると思うゾ。

青の祓魔師 ★★

少年誌らしい、飽きさせない展開でつい最後まで観てしまった。

東京喰種√A ★★★

漫画も :re まで全部読んでしまった。喰種という天敵が人間社会に潜伏してるというそのプロットがすでにずるい。登場人物がみんなキャラが立ってて、いくらでも四コマ漫画が書けるみたいだ。

氷菓 ★★

ウィットに富んだ謎解きの話。しかし高校生にしては教養ありすぎじゃないか?!えるの作画がときどき「あざといなー」と思いながらもついつい見てしまった。

トリニティセブン

ラッキースケベ学園ハーレム異世界転生もの。敵役との妙な馴れ合いとか、モブの命が軽すぎるとかいろいろ感情移入しにくい要素があった。

東のエデン劇場版 Paradise Lost

記憶を取り戻して母親を探したり。ラストは納得行かない展開だけど、Juisだけはかわいい。100億円使って日本をよくするという話、ニーチェ的な超人論に持ち込んでいて既視感満載だったのでちょっと楽しめなかった。いやそんなに単純じゃねーから…というのは野暮。

東のエデン劇場版 The King of Eden

記憶をなくしてリセットされたところから。ニューヨーク編

東のエデン

巷で言われてるほど…って感じだった。アニメで完結せず劇場版に続く

完走できず

sin 七つの大罪

魔導学園HxH枠。マリアが可愛くてみていたが、巨乳はそんなに好きじゃないしHxH以上にストーリー皆無だった。

ガリレイドンナ

時間切れ。ガリレイの秘密はまあよいが、それにしても科学まわりのファンタジープロットがいささかお粗末。

BanG Dream!

切った。アニメは最高につまらなかったがゲームが出て売れていると聞いて、ああ俺はお呼びではなかったのかと得心した。

グラスリップ

PAworksということで期待しながら半年くらいかけて少しずつみていたがついに断念(2017/6/7)。岡田麿里路線を目指してみたようが狂気とインパクトに欠ける

P言語の素晴らしさについて

先週Microsoft社がP言語に関するブログ記事を公開し一部界隈で話題となった。

「いまさら一文字言語かよ…」「何個目だ?」といった批判的諦念的なものから、「RustとGoとErlangの間の子みたいなのだなあ」「なんか読みにくい」といった反応が多くこの言語の重要性やインパクトに対して正しく理解しているものがあまりなかった。尊敬しているTD勢ですらあまり重要性が伝わってないようだ 1 2 。上記のブログ記事を読んだり、マニュアルを読んだらすぐ分かるようなことではあるが、日本語で解説しておこうと思う。なおいわゆる言語入門とかそういった類のものではないことをご理解いただきたい。

TL;DR

  • 並行処理や分散システムの形式証明や形式検証はそれ自体が非常に難しいことが知られていた
  • 証明や検証のツールも、実装のフレームワークも、テストのツールもあったが、形式検証と実装を同時に記述することはできなかった
  • 並行処理や分散システムのプログラムについて、形式検証と実装を同時にできるようになったのがP言語

これを読んですごさが分からなかった人は私のスライドを見てからここに戻ってくるとすごさが伝わるかも。

並行処理や分散システムの正しさを保証するのはとても難しい

そもそも人類にはマルチスレッドが早すぎたのであって、マルチスレッドプログラミングなんてものは常人がやるべきではない類のものであることは一般に知られているといっていいだろう。しかしながらCPUのクロック数IPCは頭打ちになりムーアの法則は演算コアを増やすという方向に進みつつあり、マルチスレッドプログラミング(並行処理)は、夏休みの宿題の終わっていない小中学生に対する9月1日のように差し迫ってきている。

CAS命令などの同期プリミティブが用意されている並行処理でさえその難しさが知られており、いわんや故障の含まれる分散システムをや。FLP不可能性やCAP定理といった「できない」尽くしの世界で、それでも人類はOSを発明し、RDBMSを発明し、非同期IOで動作するHTTPサーバーで日々ネットサーフィンを行い、Hadoopビッグデータを処理してきたのである。これらのソフトウェアに人類が一体どれだけのリソースを投入し、非決定論的に発生する並行バグのせいでいったいどれだけの時間と機会を失っただろうか。

手続き型のプログラミングでの正しさの保証は実践的にはまだ難しいとはいえ、多くの技術が普及しようとしている。いわゆる型推論に基づいたコンパイル時の型検査と静的リンクの強制(Haskell, OCaml)や、カリー=ハワードの同型対応を用いたプログラムの形式証明があればプログラムが正しいことを理論的に保証することができるようになった。言語仕様や処理系の実装からそういった形式証明をつけにくいプログラミング言語でも、QuickCheckを始めとしたテストパターンの網羅的な生成とエラーケースの推定をやってくれる強力なツールが登場(普及…?)している。日本語だとxuweiさんのScalaCheckの資料が非常によくできていて分かりやすい。

一方で並行処理や分散システムの正しさの保証は難しい。実装面からのテストツールはしばらく決定版がなかったが2013年のJepsenの登場によって状況は変わった。JepsenはいわゆるFault Injectionと言われる類のテストツールで、特にiptablesを操作してネットワーク分断をシミュレートするものであった。Jepsenによって Kafka, MongoDB, ElasticSearch といった多くの分散システムにバグが見つかり、それから分散システムはJepsenのテストを通ることが登竜門のようになった。ちなみにOverview of Infrastructure TestingというGoogleの記事を見てると、Googleは21世紀のかなり早い段階でネットワーク分断のFault Injectionもやっていたのだろうと推測される。実用的で著名なFault InjectionのツールとしてはChaos Monkeyがかなり早くから知られていたが、これはサービス全体に対する大規模なものであって、特定のソフトウェアを試すようなものではなかった。

他方では、分散システムのアルゴリズムプロトコル)を形式的に証明して正しさを保証しようという試みはそのもっと昔からあった。上記のMSのブログにあるTLA+SPINモデルチェッカが代表的なものだ。しかしこれらはいずれも、アルゴリズムを検証するために独自言語が必要であり、実用的なものではなかった。具体的には、これを使ってアルゴリズムが正しいことを証明できても、実際に動作するソフトウェアは別の実用的な汎用言語(CやJavaなど)で記述する必要があり、プログラムが証明された通りに実装されていることを保証する方法はなかった。ちなみに形式記述とFault Injectionの間の子としては最近、MollyNetflixで実用化されたことが話題になった。Mollyは Dedalus というDSLで記述したアルゴリズムに形式的にFault Injectionを網羅的に仕掛けてバグを出すものである。わたしは上のブログ記事で埋め込まれているPeter Alvaro のRICONでの講演を見ることができたが、これは本当に面白かった。トップレベルの研究者は話も上手くないといけない。

少し話を戻して、並行処理のプログラム(いわゆるマルチスレッドで動作するプログラム)の正しさを検証する方法で私が一番良く知っているのはErlangのQuickCheckが持っているPULSEだ。これは相互作用する2つのFSMを並べて状態とメッセージの組み合わせを網羅的に試してRaceが起きる条件を絞り出していくというものだ。他にも eqc_statemなど素晴らしいツールがあるので、ErlangやElixir使いでRace conditionに悩んでいる諸君がいたら是非使うべきだ。決して値段は安くはならしいが、本番で競合で悩むくらいならこれをサクッと買った方がよい。Erlang以外の処理系でここまで踏み込んだものはあまり知らない。もっともそこまで必要ないという話かもしれないが… 他の言語なり処理系だと、GoのRace detectorClangのThread Sanitizerくらいが有名だろうか。僕も詳しくないので教えてほしい。まあDTraceやBPF, ClangのXRayを使えばどうにでもなるという話かもしれないが、どのツールも私のような凡人に無理じゃないかと思う。

おわかりだろうか。これだけ日進月歩で研究と実践の歴史が積み重ねられてなお、 1) 分散システムや並行処理を形式検証するDSL, 2) Fault Injectionしてみて動くかどうか確かめてみるテストフレームワーク, 3) とりあえずトレース仕掛けてじっと様子を睨む といった方法くらいしかないのである。ここに颯爽とP言語が登場するのである。

P言語そのものについて

実はP言語は先々週登場したわけではなく、2012年には存在が公表され2013年にはPLDIに論文が登場した。さらに昨年10月にはソースコードが公開された。余談だが、実は遅くとも2014年にはCodePlexでコードが公開されており、たとえば "a1cd6fa" は完全に一致している: Codeplex, GitHub。じゃあ一体このInfoQの記事は何だったのか。このInfoQではP言語で書いたコードをZingという謎システムに入れて検証できるようにしたと書いてある。今年の記事では、P言語からC#の形式検証用のコードを吐いてツールに食わせることができると書いてある。2012年からいろいろあったんだね…

P言語のどこがすごいかというと、P言語でシステムを書くと、本番で動作する分散システムのC言語でのプログラムと、形式検証ツールに食わせるためのC#のプログラムが同時に生成されるのである。このP言語のコンパイラツールチェインが正しく作られている限りにおいては、形式検証済みの分散システムを本番で使うことができるのである。理論的にはバグがないというやつである。ネットワーク分断も死んだふり故障も(もしかしたら、書き方によってはビザンチン故障も)もう恐れなくてよいのである。TLA+は僕にはちょっと難しいのだけど、僕がもし次に分散システムを手作りする必要があったら、まず最初にP言語での実装を検討するだろう。なのでまずはMacPortsで使えるようになってくr(軟弱

ここまで来ると、Rust的なメモリ管理とか、Go的な軽量プロセスや、Erlang的な状態遷移マシンの記述なんていうのはモダンなシステム実装言語にはあって当たり前で、そこからもう一歩進んで何があるかが決め手になるということが分かる(もちろんRustやGoが劣っているということではなく、他によいところがある)。

ちなみに、この手のものは実はP言語とは違うMicrosoftの別チームが同様のものを出している。その名もIronFleet だ(よくわからない日本語解説よくわかる解説)。カタログスペックのコンセプトは、実は全く同じだ。何だか強そう。著者の名前を見比べるとわかるが、P言語とは全く別のチームだ。キャンパスが違うんだろうか、仲はいいのか悪いのか、実績からいうとP言語の方が強そうだよなとか、いろいろ妄想できてなんか楽しい^^;

レポジトリをもうちょっとうろうろすると、入門PPTがなんとそのまま入っていて(ノ∀`)アチャーと思ったがその内容が思ったよりすごい。なんとHololensやOfficeでも使われているというのだ。実績も十分だ。こんなすごい言語が使われているAzureやWindowsを使ってみたくなるね^^;

f:id:kuenishi:20170525081934p:plain

参考

P.S. とりあえずMacOSでの最初のビルドは見事にコケた。Sierra 10.12.5, commit 601520c8, monoとcmakeはMacPortsから。
P.S. mono >= 4.5 が必要だと id:matarillo さんにブコメで教えてもらった。
P.S. コメントで本文は形式的証明と形式検証を混同していることを指摘していただいた。その辺りは割り引いて理解していただけると助かる。
P.S. プログラムと検証を一致させる試みは何もPやIronFleetが初めてなわけではなく先行者がいることもコメントで指摘いただいた。割り引いて読んでくれ。
P.S. TD勢に対する煽りが少し攻撃的だったのでマイルドな表現に修正した。

一次情報を確認しなければ信頼性のある記事にはならない

こんばんは、やっと先週ガノンの打倒という宿願を果たし、ハイカラシティからもいささか足が遠のいてしまった私であるが、なんとか季節の変わり目にも風邪を引かずに過ごせている。読者諸賢はいかがお過ごしだろうか。はや4ヶ月、1年の1/3が過ぎてしまったが、先日の大🔥炎🔥上🔥騒🔥ぎで2017年のクラウドを何だか占い損ねた件を覚えておられるだろうか。これが公共のメディアに書く価値があるどころか、記事で取り上げられた会社の名誉や主張を歪曲しかねないものであったことを。

本日、友人に教えられ、同じ記者が同様に見過ごせない記事を書いたことを知ったので、いっそ皿まで、いやとりあえず再度批評することとしたい。それがこれである。リンクを踏んでPVに貢献することは結構だが、後悔するのでやめておいた方がよい。

it.impressbm.co.jp

リンク先を読んでない方は、次の指摘からもおおよそのクオリティがおわかりいただけるだろう。

この平氏を直接は私は存じ上げないが、Redhat Linuxに非常に精通しており、恵比寿でコンピュータ・ソフトウェアに関する仕事をしているということは事実のようだ。

AWSとの戦略的提携を発表、OpenShift Container PlatformからAmazon Redshift、Amazon AuroraなどAWSのマネージドサービスがダイレクトに利用可能に

これが平氏の指摘であるが、AWSRedhatはもともと戦略的提携をしており、双方の公式発表をみても Red Hat and AWS Extend Strategic Alliance to Package Access to AWS Services Within Red Hat OpenShift , Red Hat and AWS Extend Strategic Alliance to Package Access to AWS Services Within Red Hat OpenShift と、いずれも "Extend Strategic Alliance" という表現を使っている。これは、素直に英語を読めば「もともと戦略的提携をしていたが、提携を拡大しOpenShiftからAWSを使えるようになった」という話になる。まったく提携していなかった2社が提携を始めるわけではないので、これではニュースバリューを偽って誇張している表現である。

これまでどのような提携をしていたかは、Redhatが出しているフォローアップの記事 AWS and Red Hat -- Digging a little deeper を見ればすぐに分かる。本文の早い時点で "March 2010 was an exciting month in the collaboration history of Red Hat" (2010年3月はRedhatの歴史上とてもエキサイティングな月だった)と書かれており、ここからAWSRedhatの提携が始まったことがわかる。具体的にはEC2のMarketPlaceでRedhatサブスクリプションつきのイメージが買えるようになったのだと記憶している。こちらの記事 - AWS Partner SA ブログ: AWS上のRHELのサポート体制とアップデートサーバー は2015年であるが、その内容がわかりやすく日本語で書かれている。また、今回の提携拡大の伏線としては Deploy Red Hat OpenShift on Amazon Web Services | AWS Partner Network (APN) Blog が分かりやすい。AWSが大好きな顧客の声を汲むなら、「ここまで来てるんならもういっそAWS隠蔽して適当に使えるようにしてくれよ!」だろう。

次はこちらだ。

コンテナベースでクラウドネイティブなアプリケーション開発環境「Red Hat OpenShift.io」を開発者向けに無償提供

OpenShift.io The Gathering – Summit 2017 – Developer Tools, Overview and Roadmap Part I には、

OpenShift.io is the next generation OpenShift platform, based on OpenShift 3, for building and running applications in the cloud.

と書かれている。ここで重要なのは "building and running applications" という部分で、正確に訳すなら「アプリケーションの開発と実行」である。つまり、OpenShift platformはアプリケーションの開発環境と実行環境を兼ね備えたものであり、開発環境だけのものではない。この記事を丁寧に読んでいけば、OpenShift(コンテナのオーケストレーション技術)がどのようなものかはすぐに分かるだろう ( 新野さんの記事も非常に分かりやすい )。2017年のクラウドを占ったときの「これからはDevOpsがクラウドで重要になる」というフワッとした指摘を奇しくも裏付けた形になり、それをベースに記述を肉付けしたら伏線を拾ったもっとよい記事になったであろうに、勿体ない。

Disney、Pixarなどのユースケースに見るOpenStackおよびコンテナ関連のビジネスの拡張

これは、どうしてこういう表現になるのか分からない。残念ながら私も現地には行っていないので分からないが、おそらく Disney Studios and Pixar use OpenShift to accelerate the delivery of platforms and services のセッションを指しているのだろうと思うが、少なくともOpenStackという文字は文中になく、むしろOpenShift推しなのが分かるだろう。また、セッションの検索 をしてみても、OpenStackは32件、OpenShiftは95件のセッションがマッチした。これをみても分かるようにOpenStackは下火で、OpenShiftとコンテナオーケストレータの採用が拡大している傾向の方がニュースとしては正確である。ひょっとしてOpenShiftとコンテナとOpenStackの関係が理解されていないのでは…とうっかり疑ってしまうので、その関係がよく整理されている OpenStack、Docker、OpenShiftの関係を理解する! レッドハット朝活セミナーのご紹介 | RED HAT OPENEYE を紹介しておこう。

そして、推測にみちたこの文章

今回、その距離を一気に縮める提携を発表したことは、AWSと近しい関係を構築するほうがメリットが大きいと判断したといえる。

は、「ただのパートナー→戦略的提携」という前提にもとづいているが、もともと戦略的提携していたのだからこの文章はほとんど意味がない。私の考えでは、今回のサミットで特に距離を縮めたということは別になくて、その傍証として、キーノートにAWSからの有名人(例えばWerner VogelsやHamilton)どころか、誰もキーノートで話していないことを挙げておこう。しかも、セッションスピーカーで検索してもAWSのスピーカーが3人しか見つからなかったことも付け加えておこう。

で、「プライベートクラウドパブリッククラウドの境界線がより曖昧になっている流れ」とは一体何なのか。ハイブリッドクラウドユースケースが増えていることを指すのだろうか。境界線が曖昧とは一体どういう意味なのだろうか。少なくともシステムの管理主体と利用者がはっきりしている限りは境界線が明確にあると思うのだが、考えれば考えるほど意味がわからない。

次は「エンタープライズ企業によるDockerの採用が増えるにしたがい、オープンソースコミュニティを重視するスタイルをビジネスと両立させることが難しくなってきたのも事実だ」という表現だ。何が難しいのだろうか。私は仕事で体感したから知っているが、難しい理由は具体的にはモノによって様々に異なっており一般論として述べるにはまだ十分早いと思う。なぜなら直後に記事でべた褒めしているRedhatサブスクリプションモデルで成功しているからだ。

いちおうDocker CEO 退任の挨拶から以下の文を引用しておこう。

Docker has the potential to become not only one of the most enduring technology companies, but also a transformational platform, technology, and movement; I can’t think of a better or more qualified individual to lead us to that future than Steve.

オープンソースソフトウェアでビジネスをするのは難しいということであるが、さてここでCrunchBaseのランキングを指摘しておこう。この記事で取り上げた Docker (26位) よりも Hortonworks (152位) よりも、第2のRedhatに近い存在がいる。 "Open Source" "Enterprise Software" でカテゴリを any 検索するとすぐに出てくる、12位の、先日IPOしたヤツである。

f:id:kuenishi:20170509235744p:plain

まあこのランキング、IPOしてるしてないとかゴッチャだしRedhatは登場しないし、IBMがかなりの下位だったりと独自のランキング手法であるが、今調べたら時価総額で3.5倍程度差がついているこの会社をスルーしてHortonworksを取り上げるのは数字上はかなりアンフェアだと私は思う。ちなみに、150位くらいまでに出てくるOSS企業は MongoDB (56位), Pivotal (128位), Elastic (168位), Databricks (182位), あたりがある。

Windowsで作ったzipファイルをMacで展開するとファイル名が文字化けする問題

日本の商習慣として未だに残っているのが「ファイルをまとめてzipで渡す」というやつである。数年前までビジネスで使われるコンピュータはWindowsデファクトスタンダードだったので、zipファイルを作成するのも、展開するのも同じソフトウェアを使っていたから特に問題が起きることはなかった。古き良き時代であるが、近年ではMacOSも普及し、ビジネスでファイルをやりとりするのに使えるようになってきた。複数のOSが併用されるようになったが、相変わらずファイルのやりとりはzipで行われるという商習慣の形として残った。

私の意見はそもそもそういう商習慣を撤廃するべきだということに尽きるのだが、家族を養う手前既存の商習慣に従わなければならない。そしてここ数年は、仕事でもMacOSを使っている。MacOSWindowsの間でファイルをやり取りするときの問題その1は暗号化zipである。問題その2は表題にあるとおり、日本語のファイル名を持つファイルが文字化けしてしまい、意味のあるファイル名だったときにビジネス上のコミュニケーションに支障が出てしまうことである。

もしビジネスでなかったらそんなファイルはすぐにrmしてしまうべきであるが、ここまで読んで頂いたということは、読者諸賢もこの問題でお困りのことであろうから、私の調べたことがいくらかでもお役に立てば幸いである。

TL;DR

なぜファイル名が文字化けするのか

Windowsファイルシステムでは、基本的に日本語のファイル名はcp932でエンコードされている。後方互換姓のためこれが今後も変わることはないと思われる。また、最新のWindowsでもUTF-8などでファイル名をエンコードしてzipアーカイブを作ることはできないようだ。Explororのメニューからアーカイブを作るとcp932でファイル名もzipアーカイブ内に保存されてしまう。7zipなどのサードパーティのアプリケーションを使えば、Unicodeアーカイブすることができる。

また、ZIPの仕様では、ファイル名のエンコーディングに関する指定はAppendix Dに 「歴史的にIBMコードページ437しかサポートしていなかった」と書かれている。CP437とは何かというと、いわゆるASCIIのセットにラテン文字を追加したもののようで、当然日本語の文字が入っているわけではない。CP437はDOSOEMコードセットというらしい。ここでいうDOSはMS DOSのことであるから、WindowsIBMコードページが追加されていき、日本語版Windowsファイルシステムの標準文字コードとして、また、そこから作られるZIPアーカイブでCP932が採用されることのは歴史的な経緯としては自然なようだ。

一方、MacOSのファイルシステムは、 APFS でも HFS+ では、基本的にUTF-8でファイル名がエンコードされている

APFS has case-sensitive and case-insensitive variants. The case-insensitive variant of APFS is normalization-preserving, but not normalization-sensitive. The case-sensitive variant of APFS is both normalization-preserving and normalization-sensitive. Filenames in APFS are encoded in UTF-8 and aren’t normalized.

HFS+, by comparison, is not normalization-preserving. Filenames in HFS+ are normalized according to Unicode 3.2 Normalization Form D, excluding substituting characters in the ranges U+2000–U+2FFF, U+F900–U+FAFF, and U+2F800–U+2FAFF.

Finderのメニューで展開しても、 `/usr/bin/unzip` を利用しても、基本的には zip アーカイブ内のファイル名のところにあるバイト列をそのままファイル名として展開する。したがって、UTF-8しか対応していないHFS+のファイル名に、CP932でエンコードされた文字列が保存されてしまう。Finderを始めとした各種アプリケーションはHFS+の仕様に従ってUTF-8だと思ってCP932のファイル名を表示するので、よくわからない化けたファイル名が表示されることになる。
 
まとめると、WindowsではCP932でZIPを作る、ZIPは慣習的にCP932やCPxxxでのファイル名のエンコードを許容している、MacOSはそんなことしらないでUTF-8として扱う、のコンボで、結果的にこういうことになるようだ。

f:id:kuenishi:20170508224724p:plain

ワークアラウンド、今後の期待

Macに含まれているInfo-ZIPが6.00であるから、それが最新版にアップデートされれば解決するか?という答えは半分正解で、半分不正解だ。まず、このCP932対応が含まれているバージョンがまだ正式にリリースされておらず、ベータ版が 2010年にリリースされて以来ずっと放置されている。どうもやる気がないないらしい。スレも立っているがやはり放置されているので期待できない。こんなに必要とされているソフトウェアなのにリリースされないとは、OSSはさすがにかくあるべしといった感がある。

もし万が一これがリリースされたとして、MacPortsに入るのは早いだろうが、MacOSのリリースにバンドルされるのはいつのことになるやら知れたものではない。現にPythonは2.7だし、Rubyだって今みたら未だに2.0.0である。

つまり公式は期待できないので、ZIPファイルを受け取るMacOS側がどうするべきかというと、

くらいが関の山である。

次点で期待できるものとして、Goで書かれた mholt/archiver にパッチを当てるというものがある。 x/text/encoding/japanese を使うとよさそう。有志に期待している。もしGoを書きたくなったら僕がやるかもしれない。

ZIPアーカイブを作る側、Windows側でできることがあるとすれば、 UTF-8 によるエンコードはサポートされていないようなので、もし相手がMacユーザーだと分かっている場合は、予め 7zip 等のサードパーティツールを使ってUTF-8でZIPアーカイブを作成するのがよさそうである。

おまけ、問題3、逆: Macで作ったzipアーカイブが中に日本語のファイル名を持つときにWindowsでファイル名を文字化けさせずに展開できるか

UTF-8のファイル名が保存されたものは Windows 7のあるバージョンからできるようになっている。これは、ZIPの仕様に、ファイル名がUTF-8エンコードされていることを示すフラグがあり、それに従ってファイル名を変換しているようだ。

   4.4.4 general purpose bit flag: (2 bytes)
   ...(snip)...
        Bit 11: Language encoding flag (EFS).  If this bit is set,
                the filename and comment fields for this file
                MUST be encoded using UTF-8. (see APPENDIX D)


しかしながら、 MacOS のFinderでのアーカイバはそのフラグをつけずに UTF-8エンコードしてしまうらしい。

一方MacOSに含まれている "/usr/bin/zip" コマンドは Info-ZIP の 3.0 なので問題はなさそうだ *1 。リリースノートに "Unicode (UTF-8) filename and (partial) comment support" と書かれている。

*1:Finderはこのツールを使っていないということか…?!

最近のトレ

もともと健康のために始めたトレーニングだが、なんというか一区切りついたのでここに記録しておこうと思う。いろいろな記述があるが全て個人の感想であり科学的根拠はないので眉に唾をつけて読んでいただきたい。

目標

健康診断で脂肪肝と診断され体脂肪率が23%まで増え、体重は 75kg くらいまで増加した。全く運動をする機会はなく、しかも週のほとんどを在宅勤務にしており、息子を朝幼稚園に送っていく(徒歩1分)のみ、という危機的な状況であった。

一年発起してジムに通い水泳や筋力トレーニング、有酸素などをやってみるも水泳と有酸素はなかなか景色が変わらず飽きやすかった。筋力トレーニングは集中力が重要な一発勝負で好みに合っていたので続けることにした。その際いくつか目標を立てた。

メニュー

コンディショニングは 2016年のまとめ - kuenishi's blog に書いたとおりだ。いまの会社は遠方なので仕事後にジムに行くのは少し気力が必要だったので基本的には土日のどちらか週1回しか行っていない。余裕があるときは帰宅後夜遅くの週2になる。週1回なので基本的には毎回同じメニューをこなす。メニューはビッグ3を中心に

  • チンニング
  • ベンチプレス
  • フルデッドリフト
  • ケーブルプレスダウン
  • ローロー
  • ラットプルダウン
  • ドラゴンフラッグ
  • レッグエクステンション
  • ダンベルリストカール
  • ダンベルベントオーバーローイング
  • レッグプレス

などから数種目、気が向いたものをこなす。余裕があればまれに新しい種目も挑戦する。ビッグ3は定期的にYouTubeの動画でいろんな人のフォームを勉強する。このうちチンニング、ベンチプレス、デッドリフトはリストラップをつけてやる。チンニングは手首や肩の保護が目的だが、ベンチプレスやデッドリフトはパワーアップに多少貢献している(気がする)ので使っている。Schiekの24インチのものを使っている。締め付けは十分だが、やはり手首の保護となるともう少し長いやつがほしい気もするが、概ね満足している。アフィリエイト:

トレ前は時間の余裕次第だが、マッサージチェア、ストレッチポール(Pole)、ストレッチボール(Ball)を使って背中と肩を中心に15分程度コンディショニングする。下半身も基本的なストレッチをしておく。

トレ後は特に何もしない。シャワーを浴びて帰るか、帰ってシャワーを浴びるかだ。

肩がまだ状態がよくないのでチンニングはパラチンか逆手が多い。順手はまだ手首に負荷がかかる気がしているので少なめだ。Yチンは背筋がまだ弱くて十分に上がらない。

ベンチプレスはロシア式?の 5x5 をやっている ( 伝統の8×2と高頻度トレーニング、5×5ルーティンの解説 | SBD Apparel Japan コラム , パワーフォームを導入した「ベンチプレスを強くするためのトレーニング」(3/4) ) 。5x5 は5repまわしたらすぐ重量を増やすのでルーティンに入りやすい、完全にバーをコントロールすることが増量の条件、始めは軽いのでアップ少なめでも始めやすいので結局時間の節約になる、等々メリットが多く、普通の6~8rep x3set のものよりも私に合っているように感じる。

デッドリフトはビッグ3の中でも最も難しい種目のはずなので、重量や効果よりもフォームを意識している。これは始めてまだ2ヶ月程度なので、背中と腰が常に伸びた状態を維持することを心がけている。むしろ少し尻を出して反らせるくらいのイメージ。背中を伸ばしたまま地面をゆっくり押して、最後に体をまっすぐにする。背中が少しでも曲がると腰に負担がかかって怪我のリスクが増大することを実感しているので、慎重に継続していきたい。フルデッドリフトやるときは体の柔軟性も重要なので、ストレッチはまめにやっておこうと心がけている。

他のメニューは主に背中と腹の基本的な筋肉を広めにカバーするようにしている。

レッグプレスはまあ、一番大きい筋肉を鍛えてテストステロンを増やしたいのでやっている。これが一番きついので基本的には最後にやる。

ジムに行けないとき

どうしても諸々が積み重なってジムに行けないときは上記のようなハードめのメニューがこなせない。それで2週間とか開いてしまうとかなりつらいので、もらいもののパワーブロックで2,3日に一度なるべく家でトレーニングするようにしている。これ(アフィリエイト)は新型のもの:

だが、僕は1世代前のものを使っている。普通のトレーニーなら23kg程度はすぐに軽くなってしまうので、できれば90ポンド(~41kg) asin:B0029NHOMI のものを買っておくのがよいだろう。これと椅子を適当に組み合わせて

  • プッシュアップ、プランク
  • ダンベルアームカール
  • ダンベルショルダープレス
  • ブルガリアンスクワット
  • ダンベルベンチプレス

などを(ごくまれに)やっている。ダンベルベンチプレスが特に面白くて、ストレッチポールを縦にして背中〜腰を乗せてダンベルを押すと左右のバランス感覚も同時に鍛えることができるので面白い種目になる。床の上でやるとどうしても可動域が小さくなってしまうが、そこはまあ仕方がない。ストレッチポールを何か厚めのマットの上に乗せてやるとよいかもしれない。

口に入れるもの

食事は妻が作るものに合わせる。要望を聞いてくれるので、ブロッコリーや脂肪の少ない肉を中心に作ってもらうことが多い。自分のための外食は極力避けるようにしているが、妻に負担をかけないとか友人との付き合いの場合は外食も厭わない…とはいえなるべく高タンパク低脂肪の店を選ぶようにしている。

朝夕にエランバイタルを1錠とプロテインを飲んでいる。エランバイタルは本当は一回6錠なのだがちょっときついので1錠だけにしている。エランバイタルを飲むようになってから翌日の疲労感が少なくなった。プロテインは学生時代から使っているこれ(アフィリエイト):

ウイダー マッスルフィット プロテイン   バニラ味 2.5kg

ウイダー マッスルフィット プロテイン バニラ味 2.5kg

を、低脂肪乳と水の1:1の混合液に溶かして飲んでいる。なぜ混合するかというと、水だけでは味が残念だし、牛乳だけでは余計な脂肪を取りすぎてしまう(気がする)からだ。まあ私程度の雑魚ではどっちにしてもあまり変わらない。

トレーニング前は特になにも摂らない。トレーニング中にCCDを700cc程度摂って血糖値を下げ切らないようにしている(アフィリエイト)。

CCDの代わりにスポーツ飲料や茶を飲むことはない。そういった飲料では血糖値が下がりきってしまい1時間弱で集中力が切れてしまうからだ。CCDがあればそんなことは起きない。気合を入れてハードにやる覚悟をしたときはこれにBCAAを5~10g添加する。

ゴールドジム BCAA アルギニンパウダー 400g [その他]

ゴールドジム BCAA アルギニンパウダー 400g [その他]

BCAAはトレ中のCCDに混ぜるか、トレーニングした日の夜のプロテインに必ず入れることにしている。BCAAがあると筋肉の疲労がとれやすい。

トレーニング直後30分程度の時間をゴールデンタイムといって、プロテインの摂取が最も効果的だと言われている。しかし私は朝夕のプロテインだけにして、トレーニング直後に何か摂取することはしていない。理由は

  • そもそもCCDを飲みまくって腹がふくれているので、追加で入らない
  • BCAAのようなアミノ酸ならともかく、内臓での消化吸収に数時間〜数十時間はかかるので結局アミノ酸が細胞に到達して合成に使われる時間はもっと後なのでそんなにタイミングは重要ではない
  • ジムに持っていくのはかさばって邪魔

といったところだ。特に科学的根拠があって結論しているわけではないので、反論は聞きたいところ。

脂肪はなるべく摂らない。できれば量を毎日測定する。脂肪はなるべく摂るべきではないという話には異論があって、脂肪酸は細胞膜の合成などにも使われるので人体には必須の栄養素だ。だから融点のなるべく低い(なるべく酸化していない)脂質を中心に最低限の量は毎日摂るべきだと思う。ただし僕はそこまで食事をコントロールできていないので単に「肉の白い部分や、液体の油を使った料理はなるべく摂らない」という運用にしている。

炭水化物は、特に制限していない。本当は基礎代謝から一日の摂取量を算出すべきだが、これも私はあまり我慢せずに食べることにしている。なぜなら、私は空腹になると体全体が倦怠感に覆われてしまって能力が大幅に落ちてしまうからだ。知能も低下する。これは血糖値の低下が原因だと思われるが、おそらくその際に体内の筋肉を分解してエネルギーに変換していると思われる。これではトレーニングした意味がないので、朝昼夕は炭水化物と蛋白質をなるべく均等量摂るようにしている。それでも昼食と夜の間は時間が開いてしまうので、オニギリなどを食べて血糖値を下げないようにしている。夕食が早かった場合は寝る前に空腹になるので、夕食を多めに摂るか夜食を摂ることにしている。あえて気をつけているのは、アミロペクチン系のものよりもアミロース系のデンプンが多いものを選ぶようにしているくらいか。後者の方が血糖値が上がりにくい(=持続しやすい)らしい。

カーボを恐れるな

モチベーションの維持

これが一番難しい。基本的には「重い物を持ち上げるのは楽しいことだ」と繰り返すのがよいのだが、自助努力だけでは限界があるので、いくつか組み合わせている。

  • 雑誌(アイアンマン)を毎月購入、読めなくても見えるところに積む
  • 毎日プッシュアップくらいはやる(コンディションの低下を早めに検知してトレーニングの心理的優先度を上げる)
  • 定期的にムービング・ターゲット moriyoshi や ymotongpoo に会って自らの肉体を恥じる。

特にアイアンマンの購読はよい。毎月いろんな人のいろんな技術があるので試してみたくなるし、いろんな写真を見てふと足元を見ると「はー」という気持ちになれる。

アイアンマン2017年4月号

アイアンマン2017年4月号

結果

久しぶりに会う人に「肩が厚くなったね」と言われることが増えた。腹はそんなに変わっていない。太股は太くなった。ジーンズは腰回りを2サイズ落とした。子供を抱っこできる持久時間が少しだけ長くなった。

ベンチプレスの結果に注目いただきたい。ついに自重を超えたのである。体重は一度70kgを切った(その後減量をやめてパワーアップに振った)ので、目標 2/4 を達成したことになる。ベンチプレスは100kgまではすぐに誰でも上げられるようになるそうだが、私のような軟弱エンジョイ勢でも週一回続けていればここまで来れることが分かった。感覚としては5x5とコンディショニングが効いてるなと思う。

近所にゴールドジムがほしいなぁ…

こういうの本当にやめていただきたい

f:id:kuenishi:20170215024411p:plain

いやまあこれなんだけど。昨日急に通知があったということは計画停止じゃないというわけで、そんな前日にダウンロードしてくださいませ!とか言われてもできるわけねえだろ!ダウンロードするくれえなら見るわ!



過去もだいたいこの時間。


たとえば検索すると「重要なお知らせ」が引っかかるんだけど…この時間に止めるということはこの時間が一番トラフィック少ないわけで、みんな割と昼間とか朝観てるの…まじで…っていう感じです。

こんなにメンテナンスばかりしていて本当に大丈夫なの、システムちゃんと作れているのかとても心配、というか、まあ安いから入ってるんだけど、こういう感じで何もアナウンスなくメンテナンス入られるんならまた移行考えちゃうYo...

大根はなぜ消化によいのか

夕食で大根の煮物が出てきた。冬はやはりこういうものに限る。暖まるなあ…消化にもいいらしいし…と思ったところで、ふと大根はなぜ消化によいのだろうか?という疑問がわいた。大根は動物ではないのだから食物を消化する必要はないわけだ、消化酵素というものが含まれているが、酵素は通常は動物の体温程度の方が活性が高いので地面に埋まってる大根が低温で持ってても使う機会ないんでは…?などと疑問は尽きない。

我々取材班は早速Google経由でWikipediaに向かった(夕食を食べてダンベルのメニューとブルガリアンスクワットと、スプラトゥーンのガチマッチを10戦ほどこなした後で)。

f:id:kuenishi:20170211213057j:plain

大根おろし - Wikipediaには「大根にはアミラーゼ、プロテアーゼ、リパーゼなどの消化酵素が豊富に含まれているが、これら酵素は熱に弱いため、加熱をともなう調理法では有効に利用できない」と書かれており、主に三種類の消化酵素が含まれていることが分かる。この三種類の酵素について、調べていこう。

アミラーゼ

アミラーゼは、デンプンを分解する酵素だ。というのはあちこちの料理サイトから、いかがわしい健康ダイエット系のサイトまで、どんなところでも書かれている。過熱すると酵素はこわれちゃいから大根はなるべく生で食べましょう、消化がよいのでダイエットに効果ありますぜ!と、そういうのは無視したいのだけど、もうWebは汚れてしまっていてほしい情報に辿り着くのは非常に難しい。

しかしアミラーゼについては案外簡単に答えがみつかった。ダイコンのアミラーゼ | みんなのひろば | 日本植物生理学会が非常に詳しい。いわく「大根にはほとんどデンプンがないのに、どうしてその消化酵素が多く含まれているのですか?」という非常に鋭い質問だ。しかも実験までされている。最近の塾ってすごいんだな…とにかく、要点を引用すると

  • デンプンはデンプン粒として1〜0.5%存在しているとのことです(澱粉科学35: 19 (1988))
  • ダイコンの根は〜90%が水分であることからすれば、そんなに少ないわけでもありません
  • アミラーゼは植物細胞中で、原形質ではなく成熟細胞の大部分の体積を占める液胞の中に局在
  • デンプン粒は液胞の中ではなく、原形質に存在
  • 相互に接触していないため、デンプン粒がアミラーゼによって分解を受けることはありません
  • 冬大根であれば秋―冬での光合成産物を根に貯え、春に種子ができるときそのエネルギー源として根のデンプンを利用していると考えられます

ということだ。動植物が冬を越すためにエネルギーを蓄え、その中でデンプンと同様にアミラーゼも蓄えられているという精巧な仕組みになっている。ではデンプンの消化を助けるというが効果のほどはどうなのか。唾液や膵液に含まれているアミラーゼの含有量はわからないけど、

から、なんとなくオーダーが推測でき…ない。大根おろしを1リットルほど食べれば補助にはなるかな。食べ過ぎかな。

まとめ

分子生物学とか化学ちゃんと分かってないと説明するのは難しい。あと市井の情報源はほとんど信頼に足らず、どれだけ食べたらどういう定量的効果が得られたのかといったデータを全く語っていない。
タンパクを壊すタンパク・プロテアーゼのような面白いページで時間を溶かしてしまって簡単には目指す知識にたどり着けなかった。人類の膨大な知的資源を投資し続けているだけのことはある。

筑波大学で分散システムの話をしてきました

また呼んでいただいたので、筑波大学の情報システム特別講義D(1/19, 20 - 20日4限)で話してきました。これは業界で川島さんに無茶振りをされた人が聴講に来た大学生を置き去りにして講師陣に実力を試されるという素敵なイベントです。発表に使ったスライドはこちらです。自分で論文読んで証明を考えながら作ったスライドなので曖昧なところや誤りがあれば指摘いただきたいです。

前回はデータベースの話をしました。

kuenishi.hatenadiary.jp

今回は、転職もしたし、NoSQLブーム的なのも一通り終わったのでもうデータベースの話でもねーだろってことで、分散システムの理論面に入門した内容になっています。分散システムの理論面は20世紀に一通り出揃ってしまって、21世紀の最初の15年は実装と運用の時代でした。具体的には、理論と実装のギャップをどう埋めるかという研究や試行錯誤が盛んで、理論それ自体の進歩はそれほどでもなかったと思います。…と言いながら、自然言語で記述する分散システムの証明に限界があって人類には難しすぎるのも事実なので、その検証や証明を補助するツールや理論がいくつか試された時代でもありました。そのあたりは発展編として、私はカバーできませんしませんでしたが、10年後には現場でも必要になっている技術だと思うので、いまから入門しておいてもよいかと思います。

おまけ

データサイエンス根性論

Kota UENISHIさん(@kuenishi)が投稿した写真 -