2017-03-04

読んだ: 証明と論理に強くなる～論理式の読み方から，ゲーデルの門前まで～

ツイッターで見かけて気になったので読んだ。

作者: 小島寛之
出版社/メーカー: 技術評論社
発売日: 2017/01/11
メディア: 単行本（ソフトカバー）
この商品を含むブログ (2件) を見る

1年くらい前に、別の論理学の本を読んだときは分からな過ぎて断念したが、この本は理解できてないなりになんとか読み進めることができた。

特に2部が面白かった。というか、3部以降はだんだんわからない箇所が多くなったのできちんと理解できてない。

学校で数学の証明はやったことがあったが、内容が正しいかどうかという点に注目して解いていた。この本では、そうではなくもっと形式的なものとして扱える（演繹というらしい）ことが説明されており、演繹のやり方から完全性・健全性という話に進んでいく。（この辺りまでがなんとなくわかった限界だ）

読んでいて「あれこれプログラミングじゃね？」と思うことがたびたびあって、ちょっと調べたところ「数理論理学」というのがあって、情報工学にも関係あるらしい。

気になったこと

ホフスタッターの定理、

MIUの演繹システムでは、項MUを演繹できない

をホフスタッター数を利用して証明するってところで、なぜ

M→3, I→1, U→0

となるのか分からなかった。

他の書籍

参考書籍に上げられている本で「ゲーデル、エッシャー、バッハ―あるいは不思議の環 20周年記念版」というのがあって気になった。でも安くないししかもページ数が多い。体力ないと読めなさそうだ…

ゲーデル、エッシャー、バッハ―あるいは不思議の環 20周年記念版

作者: ダグラス・R.ホフスタッター,Douglas R. Hofstadter,野崎昭弘,柳瀬尚紀,はやしはじめ
出版社/メーカー: 白揚社
発売日: 2005/10
メディア: 単行本
購入: 14人クリック: 432回
この商品を含むブログ (145件) を見る

数理論理学面白そうなので何か入門書を探して読んでみよう。

2017-02-28

apexでAWSのprofileの指定

apexを使ってデプロイするときに、AWSのprofileを切り替えたい。

オプションを使う

--profile を使う。

apex --profile=another deploy func

たまに切り替えるならこれで良いと思う。

project.json に指定する

profileという項目で設定できる。

{
  "name": "linebot-demo",
  "description": "linebot demo",
  "memory": 128,
  "timeout": 5,
  "role": "arn:aws:iam::218010143316:role/linebot-demo_lambda_function",
  "environment": {},
  "runtime": "golang",
  "profile": "another"
}

アプリとしては認証情報に依存しないと思うので、この設定は良くないかもしれない。開発環境とCI/CD環境でprofile名を統一しないといけないとか、色々メンドくさそう。

環境変数を使う

AWS_PROFILE で指定することができる。

export AWS_PROFILE=another
apex deploy

これが一番良さそう。

ただ、aws cliだと AWS_DEFAULT_PROFILEを使うので、できたらこっちに合わせて欲しいような気もする。

2017-02-21

swagger.json のルーティングをCLIで確認する

goaを使ってAPIのデザインをしているときに、ルーティングの確認がしたくなる。

ikawahaさんの、goa tips : swagger-ui を使って手っ取り早く API を試す - 押してダメならふて寝しろにあるように、swagger-ui用のルーティングを使うことで確認ができるのだが、正直もんにょりする。

という話を会社で話していたところ、後輩がCLIのツールを作ってくれた。

GitHub - decafe09/swrt

swagger.json をパースして、ルーティングを表示してくれる。

$ curl -s http://petstore.swagger.io/v2/swagger.json > swagger.json
$ swrt
http://petstore.swagger.io/v2
   PUT  /pet
  POST  /pet
   GET  /pet/findByStatus
   GET  /pet/findByTags
   GET  /pet/{petId}
  POST  /pet/{petId}
DELETE  /pet/{petId}
  POST  /pet/{petId}/uploadImage
   GET  /store/inventory
  POST  /store/order
   GET  /store/order/{orderId}
DELETE  /store/order/{orderId}
  POST  /user
  POST  /user/createWithArray
  POST  /user/createWithList
   GET  /user/login
   GET  /user/logout
   GET  /user/{username}
   PUT  /user/{username}
DELETE  /user/{username}

さっと確認したいときはこれで十分。便利。

jsonをPIPEで受け取れた方が楽かなぁと思ったので、そのうちプルリクしよう。

2017-02-16

作業手順書を書くときに気をつけたいこと

最近社内で手順書をレビューしてて気になったことがあったので、書いておく。

作業の目的を明確にする

まず、なんのための作業なのか明確にしておく必要がある。例えば、

管理者を追加したい
データをクリーニングしたい
リリース作業したい

など作業の目的は様々であるが、それがはっきりしないことには、そもそも手順が正しいかどうか判断できない。

「今度削除するデータをお客様の要望により念のためバックアップしたいです。」
「はい、でも対象になるデータは、n週間前のデータなので週次バッチでバックアップが残っていると思います。そもそもこの作業は不要で、削除だけの手順で十分だと思いますがどうでしょうか？」
「確かにそうですね」

みたいな不毛なことがないようにしたい。

日本語の表現を曖昧にしない

例えば履歴のデータをクリーニングするとする。

#先月までのデータを削除する
DELETE FROM hoge_table WHERE created_at < ‘2017-02-01’;

「ちょっと待って、先月までって、1月までってことで1月は含まないんじゃないでしょうか？？？いや私が勘違いしているかもしれないし、「まで」ってのは含むの含まないの？」

日本語は難しい。口語でサラッと書いてしまうと境界条件が曖昧になってしまう。 SQL見れば自明だろ！って思うかもしれないけど、日本語とSQLとどっちが正しいか確信が持てない。

スコープを揃える

スコープと言う表現が適切ではないかもしれないが。

先の例でいうと、履歴データは年月日のデータを持っているので、「先月まで」「半年」みたいな月や年単位の表現ではなく、日をベースに範囲とかを記述すべきだと思う。

#2017-02-01未満のデータを削除する
DELETE FROM hoge_table WHERE created_at < ‘2017-02-01’;

と書いてもらえると、SQLと日本語で違いがない。日本語の表現としては少し変な感じがするかもしれない。でも、境界条件はハッキリしたい。

時刻は固定された表現にする

ついでに書くと「先月」という表現は作業をする時点で変わってしまう。2月だと1月だし、6月だと5月になってしまう。

作業をする時点での、明確な時刻を指定した方が揺るぎがないので、極力時刻を固定した方が良いと思う。

作業が延期されたりすることもあるが、その際にはその時の日時で手順書を更新すべきだと思う。

後から振り返ったときに、いつやった作業なのか明確になっている方が良い。「2017-02-01データクリーニング手順書.txt」となっていても、実際には3月に作業したみたいなこともあって、そういう時にファイル名も更新すべきだし、手順書の内容もちゃんと日時を合わせるべき。

根拠を明確にする

手順書に落とし込む必要はないかもしれないが、作業の根拠は明確でないといけない。

「データクリーニングの対象レコードが1億件あるので、メモリが足りない可能性があります。」
「メモリが足りないという根拠はなんですか？」
「前回2千万件のレコード削除の際にはメモリが枯渇していました。」
「（トレンドのグラフを見つつ）前回の作業の時には明確なメモリ使用量の変化はないようですが…」
「COPYを使ったので…（モニョモニョ…）」
「逆に同じレコード件数で、別の作業の時にpg_dumpを使用していますが、コレはメモリには影響なかったんでしょうか？」
「それは…」

例えばレコード数が同じだった時にCOPYはダメでpg_dumpは大丈夫という根拠が明確でないといけない。

同じ操作ではないのでもちろんリソースの使い方も違うと思うし、一方が良くて一方が良くないという理由はちゃんと説明できないといけない。

そもそもどちらの作業も考慮が足りてなかったんじゃないか？と思ってしまう。たまたま影響がなかっただけで。

実際、何が影響して障害になったりするかわからない部分も正直あるんだけど、少なくとも自分がやる作業については、どういう作業でどういう影響があって、どういうリスクを伴うかというのは根拠を持ってないといけない。

根拠が間違っているかもしれないんだけど、そこが揺らぐと何もできないし、自分で説明できるレベルで根拠はしっかりしておいてほしい。

他にもあった気がするけど、とりあえず終わり。

2017-02-15

phaserを使ってクソゲー作った

この前、社内のLT交流会があったので、その発表用にちょっとしたゲームを作ってみた。

iPhoneとパソコンで連携するウェブゲーム

プレーヤーはiPhoneをライトセーバーのようなものとして扱う。 iPhoneを左右に振ると、パソコン上のライトセーバーのようなものが同期して左右に揺れる。パソコン上では次々と敵と思わしきものが上から落ちてくるので、ライトセーバーのようなものを接触させて、消滅させる。

そんなゲーム。面白さはあまりない。

動機

最初はforceというsalesforceのデータを扱えるCLIのツールについて紹介しようと思っていた。
GitHub - heroku/force: A command-line interface to force.com

でも途中でたまにはいつもと違うことをやってみようと思い、ゲームを作ってみることにした。

phaserとは

Phaser - A fast, fun and free open source HTML5 game framework

ゲームエンジンであってるかな。ブラウザでゲームを作るためのライブラリで、色々とできるっぽい。

ゲーム内のオブジェクト管理
音声
画像
当たり判定
イベント管理

本格的なゲームを作った経験はないが、flashとかで簡単なものは作ったことがあって、思いの外苦労はしなかった。

それに、オブジェクトが当たった時の跳ね返りとか勝手にやってくれるので、かなりラクができた。

Typescriptの定義ファイルもあったので、コーディングもあまり苦労しなかった。

iPhoneとパソコンの同期

websocketを使った。サーバはGoで構築した。

iPhoneからの接続とパソコンからの接続を管理
iPhoneからのデータをパソコンに転送する

というやつを作った。

iPhoneでは、

端末の角度を取得、計算して送信
加速度を取得して、音量調整

を行なった。ライトセーバーっぽさを演出するために、強く振るとブーンの音が大きくなるようにした（がLTの時には聞こえなかったっぽい）。

パソコンでは、送信されてきた角度に合わせて、画面上のライトセーバーを傾けるようにした。

ゲームとしてのクオリティ

もともとすごいゲームを作ろうってわけでもなかったので、完成度の低さは気にしていないが、

素材が大事

ということが勉強になった。

発表の3週間くらい前からやり始めたが、websocketで通信し合うとか、ゲーム内の当たり判定とか、そういうのはライブラリなどのおかげでほとんど苦労はしなかった。

画像や音声の素材探しと調整のための加工が大変だった。正解が良く分からないし、無限に時間が吸われていく感じがした。

何でも作ると面白い

専門で仕事にしようとはあまり思わないが、自分でゲームを作るのも面白かった。

iPhoneとパソコンの画面が繋がった時にはやっぱり「おぉーー！すごいすごい！」ってなるし、こういう風に動くかな〜と思って実装したものが期待通りに動く楽しさや嬉しさがある。

良い経験になった。

2017-02-10

goaのVSCode用のスニペット書いてる

goaで設計するとして、ResourceやMediaTypeとかを地道に書くのは正直めんどくさい。

なので、少しでもラクするためにコードスニペットを書いている。まだ書き始め。

vscode goa snippets · GitHub

ざっくりとしたテンプレート的な部分と、細かく調整が必要そうなParamとか、必要に応じて書き足して行こうと思ってる。

ある程度まとまったら、MarketPlaceに公開したい。

2017-02-08

Angular入門 6日目

社内ツールをバックエンドをGo(goa)で、フロントエンドをAngularで作ることにした。

6日目。今回も少しだけ作業した。

やったこと

通知周りを表示

bulmaの通知用のCSSがあるので、それを使った部分をComponentとして独立させてみた。

通知用と本文のComponent間でのやりとりが必要になったので、その辺を調べていたが、どうやらServiceを共有するのが良いらしい。

何でもかんでもServiceだなぁと思った。ModelをラップしただけのServiceとか…。 Fat Controler → Fat Model → Fat Service という時代の流れなのかな？