KLabGames Tech Blog

KLabは、多くのスマートフォン向けゲームを開発・提供しています。 スマートフォン向けゲームの開発と運用は、Webソーシャルゲームと比べて格段に複雑で、またコンシューマゲーム開発とも異なったノウハウが求められる領域もあります。 このブログでは、KLabのゲーム開発・運用の中で培われた様々な技術や挑戦とそのノウハウについて、広く紹介していきます。

カテゴリ: その他

はじめに

この記事は KLab Advent Calendar 2017 15日目の記事です。
こんにちは。S-Typeと申します。普段はプランナーをしている企画の人間ですが、何か書いてみたいと言ってみたところ参加させてもらえることになりました。
Google Home miniから勤怠メールを送る方法をまとめます。

勤怠報告は大変

季節の変わり目は体調を崩しがちです。無理してもパフォーマンスは上がりませんし、そういうときは休みましょう。
しかし、重い体を動かしながら、一生懸命勤怠メールを打とうにも誤字脱字が多発し、修正に時間を取られてしまう……なんてことはありませんか。

byouki_oldman

そこで、Google Home miniの出番です。
Google Home miniに勤怠を送ってほしいと、寝たまま声を発するだけで送ってくれる仕組みをご紹介します。

Google Home miniとは

Google Home miniは、Google アシスタントが利用可能なスマートスピーカーであるGoogle Homeの小型版です。価格も約半額の6,000円で購入することが可能です。
「OK, Google」もしくは「ねえ、Google」から会話を開始し、以降に続けた音声コマンドを実行してくれます。例えば「OK, Google. 明日の天気は?」と聞くと「明日の〜は最高気温〜、最低気温〜で晴れるでしょう」と回答してくれます。
その他にも計算式、radikoやNHKニュースの再生、タイマーや目覚ましアラームなど、日常においての頼れるパートナーとしての役目を担ってくれます。

IFTTTとは

IFTTTは、 If This Then That をコンセプトに生まれたウェブサービスです。
トリガーである【This】とアクションである【That】、それぞれ別々のサービスを設定し、連携させることができます。
IFTTTで特筆すべきはトリガーとアクションそれぞれに設定可能なウェブサービスが豊富にあることと、こうした流れを コードを書くことなく ユーザーが任意に設定できるということです。
そして、こうした設定をレシピと呼び、公開すれば多数のユーザー間で共有することが可能です。
今回は、このIFTTTのトリガー部分にGoogle Homeで利用可能なGoogleアシスタントを設定し、Gmailから勤怠メールを送ってみることを試してみようと思います。

IFTTTレシピ作成前の準備

では、さっそく、レシピを作ってみましょう。準備するものは以下の通りです。

  • Googleアカウント(Gmailで送る際に使用)
    • IFTTTに登録可能なGmailアカウントは一つだけです
  • IFTTTのアカウント

そして、処理の流れは以下の通りとなります。

  • This:Google Home miniに「今日は会社を休みたい」と言う。
  • That:Gmailから勤怠メールが送られる。Google Home miniから「お大事にして下さい」と返される。

レシピの追加

  1. IFTTTにログインし、My AppletからNew Appletをクリックします。

recipe_0

  1. この画面が表示されるのでThisをクリックします。

recipe_1

  1. Google Assistantをクリックします。探しにくい場合は検索で見つけましょう。

recipe_2

  1. Say a simple phraseをクリックします。
    これは「今日は会社を休みたい」という単一のフレーズでの処理結果が確定しているためです。
    今回は解説しませんが、今日ではなく明日だったり、休む理由を体調不良や私用など条件分岐させたい場合はSay a phrase with a text ingredientを選択します。

recipe_3

  1. Google Homeに話しかけるときのフレーズを指定します。
    対象の項目は
    What do you want to say?
    What's another way to say it? (optional)
    And Another way? (optional)
    以上の3つです。
    What do you want the Assistant to say in response? はどんな返事をしてほしいかを設定します。
    日本語で指示し、日本語で返してほしいので Language はJapaneseにしてください。
    ここまで終わったらCreate triggerをクリックしてトリガーの作成を終わらせましょう。

recipe_4

  1. 次にThatをクリックし、トリガーをきっかけに実行される内容を設定しましょう。

recipe_5

  1. Gmail をクリックします。

recipe_6

  1. メールを送りたいので、Send an emailをクリックします。

recipe_7

  1. メール送信にあたって必要な情報を埋めていきます。
    ここで設定しているのは以下の項目です。
    To address で送信先を、Subject で件名を、そして Body で本文を設定します。
    Bodyに改行を含む場合は <pre> タグで文章を全て囲わないと、改行されませんので注意してください。
    ここまで終わったらCreate actionをクリックしてアクションの作成を終わらせましょう。

recipe_8

  1. 最後にレシピの名前を設定します。デフォルトでIfから始まる文章が入っていますので、このままでも良いでしょう。
    Receive notifications when this Applet runs のスイッチはOFFにしておくことをオススメします。
    このスイッチがONになっていると、そのレシピが実行されたらその度にメールで通知されます。
    Finishで完了します。

recipe_9

検証

では、さっそく検証してみましょう。

前提条件

  • メールの送り元は私用のアドレスです
  • メールの送り先は社用のアドレスです

実践

私「ねえ、Google。今日は会社を休みたい」
Google Home mini「お大事にして下さい」
……しばらくしてから ピコン!(メールの着信音)

スクリーンショット

出来ましたね!!

recipe_10

最後に

今回はGoogle Home miniとIFTTTの連携によるメールの送信を紹介しました。
100%衝動買いだったGoogle Home miniでしたが、IFTTTのおかげで様々なウェブサービスとの連携が楽しめるので、無駄にはならなさそうです。
何よりもコードを書く必要がなく、GUIで入力項目を埋めていきながら設定が出来るため、私のような開発職以外の人間でも簡単に出来ました。

余談

Google Home miniを今後も活用していきたいので、nature remoを注文しました。
nature remoと組み合わせることで、音声による赤外線リモコン家電のコントロールが可能になります。
これが出来るようになると、寝たまま部屋のリモコン照明のON/OFFが出来るようになります。もう完全に未来ですね。
本稿を書くまでに届いていれば、そちらをテーマに書こうと思っていたぐらいでしたが、間に合わなかったため、またいつか別の機会で書かせてもらえたらと思っています。

この記事は KLab Advent Calendar 2017 10日目の記事です。

こんにちは。このブログでは4度めまして、kakkun61 です。

この記事では、10月22日に開催された同人誌即売会技術書典3に KLab の有志で作った同人誌を頒布しましたので、その報告をします。

頒布した同人誌は電子版が無料で、この記事の下部にダウンロード用のリンクを張っています。

技術書典とは

技術書典は、プログラミングについての同人誌を作成しているサークル TechBooster達人出版会が主催する技術・科学系同人誌即売会で、今回含めナンバリングイベントが3回、超会議での超技術書典が1回開催されています。

今回は秋葉原のアキバ・スクエアで開催され、ユニークの来場者数では2750名とかなり大規模なイベントとなっています。

なぜ参加することにしたか

発案は筆者で、筆者は技術書典1と技術書典2そしてその間のコミックマーケット91とで Haskell の同人誌を頒布して同人誌を作る楽しさみたいなものを感じていたことと、KLab のアドベントカレンダーは過去2度ともすぐに枠が埋まってしまっていたので、社内に書きたいと思っている人がある程度いるのではないかと思い、会社に相談し会社として参加することになりました。

どう作ったか

TechBooster の『技術書をかこう!』にしたがって Re:VIEW を使い、GitHub 上で Pull Request 運用で作っていきました。

各章を1人で担当し、章ごとに PR を作成しレビュー後マージという運用をしました。ふだんのソースコードの開発と似せた方が分かりやすいかと思いこのようにしました。

どんな同人誌になったか

表紙

7名で執筆し、校正の協力に1名、表紙の協力に1名という体制のメンバーになりました。

内容は下記です。

  • 物理ベースレンダラーを Rust 実装して、表紙絵をレンダリングした話
  • Sprache を CPS 変換
  • Emscripten で動画再生する
  • テキストマクロプロセッサ「M4」のチューリング完全性
  • FPGA 初心者が試行錯誤しながら疑似乱数生成回路を作る
  • 家庭内ネットストーカーシステムを作った
  • とある KLab のスマホアプリのビルド事情

特にジャンルなどは指定せずみなが書きたいことを書いてもらったのですが、直接しごとと関係あるものは「とある KLab のスマホアプリのビルド事情」のみで、他は各々好き好きな内容になりました。

参加してどうだったか

さいわい印刷した冊数の7割ほど頒布することができました。印象としては KLab だからというよりは、内容で購入してくれていたように思いました。どれもコアな内容なので一部の人には刺さっていたようでよかったです。

メンバーでのふりかえりで、一般にも役に立ちそうなことを下記に抜粋します

ぱっと見てどんな内容の本か分からない

雑多な内容でタイトルに何も情報がないのでどんな本か分からなかったのは失敗でした。表紙に概要を書いたり、内容を書いたものを机に立てるなどしようと思います。

カラーのフェルトペンがあるとよかった

上の項目にも関連して、現地で札などを立てることになったときに黒ペンしかなかったので、見栄えが悪かったです。

人だかりができると立てたものは反対に見にくい

宣伝に札を立てたりしたのですが、人が近くで立って机を見たら上から見下ろすことになるので、そのときは紙を置く形の方がよかったです。机の前に人がいるいないで立てと寝かせとをうまく変えられるとすごくいいと思いました。

レビューに PR を使うことについて

今回は GitHub で PR を作る方式にしたのですが、いくつか問題に感じることがありました。

  • 書きかけの状態で全部の章を合わせてビルドするのが PR 方式だとやりにくい
    • マージしたブランチを作成しないといけないため
  • レビュワーが PR 上で指摘するのはリードタイムが長くなるので、明らかに問題のない修正はレビュワーが直接書きかえたかった

次回は、著者が直接 master にコミットし、レビュワーも直接コミットして訂正する方法を試そうと思います。

余談

調査不足でブースが隣りの Wantedly の書籍と名前かぶりしていました。「Tech Book ください」と言われて「どちらの?」となることがありすみませんでした。あちらの方が技術書典1からその書名を使っていらしたのでこちらがかぶせてしまいました。

電子版

ダウンロード

このエントリーは、KLab Advent Calendar 2017 の12/4の記事です。

今年のISUCONはKLabが作問するということで、ゲームが題材だと予想していた方も多かったと思います。 その期待(?)に応えるべく、本選ではCookie Clickerを元にしたゲームを出題しました。 これを複数人で協力プレイできるようにして、WebSocketを使っていて、クッキーではなく椅子を増やし、椅子の数が多倍長整数になる、というゲームでした。

この記事では @hasi_t がISUCON7本選の作問でやったことを書きます。

プロトタイプ作成

まずプロトタイプ作成を担当しました。 Cookie Clickerを元にする、という案が出ていたので、自分がやりたい要素を入れたプロトタイプを作りました。

一つ目の要素は未来計算と操作遅延です。 サーバが未来の値を計算できるようなデータを返し、クライアント側で各時点での値を計算するようにする、という設計です。 そして操作を遅延させることで可能な限り同時刻での見え方が同じになるようにしました。 このような設計によって通信頻度を下げる、というのは、 CEDEC 2015で発表したことの実践で(参考)、 それを実現するための技術や開発体制について普段の業務で日頃考えていたりするのですが、 その実態を見せる機会と考え、この要素を入れました。

二つ目の要素は多倍長計算です。 以前、 ICFPC 2016 というプログラミングコンテストに参加したときに多倍長有理数を使って、 こういう多倍長計算を使った問題を作りたいと思っていた、というのがあります。 あと、メモリを消費させて、ただキャッシュするだけでは駄目なようにしたい、というのも考えていました。

ちなみに、作問チームのうち3人 (@mecha_g3, @___Johniel, @hasi_t) はここ4年ほど、この3人だけではないですが、DiamondPrincessというチームでそのICFPCに参加しています。そして今年は2位でした!

プロトタイプの時点ではWebSocketではなく、普通のHTTP通信で、サーバはPHPで雑に書いた状態でした。 ver0とver1を作ったのですが、ver0の時点ではミリ秒単位ではなく秒単位だったりしました。 あと、命名が雑すぎて抽象的な一文字変数名だらけになっていたので、本実装時に名前の調整が結構大変でした。

本実装作成

WebSocketを使うことになり、初期実装は他の人に任せて、 ゲーム画面を作るためにJavaScriptコードをロジックとビューに分割したり、 いい感じのフォントを探したりしていました。

ベンチマーカのバリデーション作成

未来計算の設計時点で、ベンチマーカから見て検証可能にすることを考えていました。 誤差を許容するには、許容範囲やそれに合わせた計算など、考えることが多く、それを避けた結果、厳密な検証になりました。 そのため、値が1でもずれるとfailするという厳しいコンテストになりました。

負荷走行前の検証はaddIsu, buyItemに対するレスポンスが必ず存在するので良かったのですが、 負荷走行後の検証はタイムアウトなどでレスポンスが無い場合を考える必要があり、 上限と下限を考えて検証する必要があってちょっと大変でした。

エラーメッセージを参加者にとってわかりやすくする、という作業をするのがぎりぎりになってしまい、 初期実装作成者には苦労をかけてしまいました。

ベンチマーカのチューニング

当然といえば当然ですが、初期実装そのままで検証していたら、 負荷走行後の検証の実行時間が長すぎる問題が発生し、高速化をしました。

やったこととしては、指数表記変換関数の高速化、item価格と生産速度のキャッシュ、1000回ループの回避、指数表記変換関数内の10のn乗のキャッシュ、addingの累積和を使う、などです。

実装は以下の通りです。指数表記変換関数(big2exp)はutil.goにあります。

とりあえず、Go言語のbig.Intは、つらい、という感想でした。

マスタデータ調整

いい感じのマスタデータにしないと多倍長使う意味が無い、と思っていたので、 1分間のベンチマークで10の10万乗ぐらいまで到達できるようにマスタデータを調整しました。 調子に乗って1個目の購入価格が10の10万乗ぐらいあるアイテムを作ったら、 初期実装の時点でそこが重すぎて、リハーサルやってみたけどまともにチューニングできない、 みたいなことも起きたりして申し訳ない感じだったりしました。

ちなみに、Excelで値を調整して、Pythonスクリプトで雑なシミュレーションをする、ということをしていました。 もちろん、値を直接扱えないので、対数をとって計算していました。

おわりに

参加者の皆様、運営の皆様、お疲れ様でした! いろいろご迷惑おかけしましたが、出題することができて嬉しく思っています。 ありがとうございました!

(本稿はKLab Advent Calendar 2017 の3日目の記事になります)

昨今、電子工作やマイコンプログラミングへのハードルが急激に下がっているという印象があります。皆さんの身の周りでもArduinoやRaspberry Piに秋葉原で買ったセンサーを繋いで遊んでいる人がいるのではないでしょうか?

私の所属しているKLab株式会社にも「Make部」という部活があり、毎年Maker Faire Tokyoで各個人が作品を展示したり社内勉強会を開いたりして、業務と無関係に電子工作を楽しんでいたりします。

ふつうのLinuxマシンでもセンサー類を扱いたい

とはいえ、ArduinoもRaspberry Piも普段使っているLinuxマシンやmacOSマシンとは随分異なる環境です。ふつうのLinuxマシンにセンサーを接続して、気軽に扱えないものでしょうか?

Raspberry Piでセンサー類を簡単に扱えるのは、GPIOインターフェースが存在するためです。GPIOピンと各種センサー類やサーボモータなどを接続することで、Linux+電子工作の組み合わせが簡単に実現できるよ、というのがRaspberry Piの強みだと言えるでしょう。

Raspberry PiのGPIOピン

一方で、多くのLinuxマシンにはGPIOインターフェースが存在しません。たとえばUSB to I2C変換モジュールを使えばLinuxマシンでも電子工作的な遊びはできますが、追加の出費が必要ならRaspberry Piを買った方がマシだよ、となってしまいそうです。

本稿では、DigiTempを使ってLinuxマシンで比較的安価に温度センサーを扱う方法を紹介します。DigiTempはLinuxのシリアル通信インターフェース経由で1-Wire接続のセンサーを扱うOSSで、多くのLinuxディストリビューションで標準パッケージとして採用されています。

ソフトウェアのインストール

まずはソフトウェアのインストールをしましょう。大抵の環境でDigiTempはコマンド一発で入るはずです。

Debian系なら apt でインストールできます。

$ sudo apt install digitemp

RedHat系は yum でインストールできます。

$ sudo yum install digitemp

macOSでも遊べます。Homebrewからインストールしましょう。

$ brew install digitemp

後述するようにシリアル通信ドライバも必要です。こちらは利用するシリアル変換ICに応じて適切なドライバをインストールしてください。

ハードウェアの準備

当然ですが、ソフトウェアだけで外気温の測定はできません。DigiTempの利用には下記のような準備が必要です。

USB to シリアル変換モジュール

USBからシリアル通信(UART)への変換モジュールです。Arduinoで遊んだことがあれば必ず1個は持っているのではないでしょうか。変換ICとしてはFTDI社のFT232RLなどが有名ですが、他にもSilicon Labs社CP2102やProlific社 PL2303を採用した変換モジュールも容易に入手できます。

ちなみに私はCP2102ベースの変換モジュールを利用しています。これはeBayで1.15ドルでした。

CP2102 USB to シリアル変換モジュール

FTDI製ICを使っているモジュールであればドライバは標準でインストールされていることが多いかもしれません。それ以外の場合は手動でドライバをインストールする必要があるはずです。

温度センサ DS18B20

DS18B20はMaxim Integrated Products社製の温度センサです。秋月で買うと1個250円ですが、eBayなどを探せばもっと安いものも見つかります。

DS18B20

このセンサーは1-WireというMaxim独自のプロトコルで動作します。このプロトコルがUART経由で扱う上でのキモです。1-Wireはデータレートが低速かつ通信線1本で動作するので、UARTからでもドライブできるのです。他のプロトコルのセンサーであれば何らかのICが必須になるでしょう。

UARTとDS18B20の接続用ボード

UARTとDS18B20を直結しても動くことは動くらしいのですが、逆流防止などの用心のため、簡単な回路を工作してみました。

UART to DS18B20 接続用ボード

これはdword1511/onewire-over-uartで紹介されている下記の回路図を元に作成したものです。

回路図

材料は下記の通りです。

  • ユニバーサル基板
  • L型ピンソケット(1×6、メス)
  • 5.1kΩ 抵抗
  • スイッチングダイオード 1N4148
  • ポリウレタン銅線(配線用)

動かしてみる

これらを組み合わせると次のような見た目になります。思ったより場所を取る感じの仕上がりになってしまいました。

完成図

これをLinuxマシンのUSBに接続して、先ほどインストールしたDigiTempを起動すると温度が取れます。

コマンドの使い方として、まずは-wオプションを指定して1-Wireデバイスのスキャンを行う必要があります。-sオプションはシリアルポートの指定です。

$ /usr/bin/digitemp_DS9097 -s/dev/ttyUSB0 -w
DigiTemp v3.7.1 Copyright 1996-2015 by Brian C. Lane
GNU General Public License v2.0 - http://www.digitemp.com
Turning off all DS2409 Couplers
.
Devices on the Main LAN
28FF933161150389 : DS18B20 Temperature Sensor

これで接続されているセンサーの情報が$HOME/.digitemprcに記録され、次回以降の起動でこの情報を参照するようになります。

$ /usr/bin/digitemp_DS9097 -a -d 2 -n 5
DigiTemp v3.7.1 Copyright 1996-2015 by Brian C. Lane
GNU General Public License v2.0 - http://www.digitemp.com
Dec 02 21:21:27 Sensor 0 C: 21.50 F: 70.70
Dec 02 21:21:29 Sensor 0 C: 21.56 F: 70.81
Dec 02 21:21:31 Sensor 0 C: 21.50 F: 70.70
Dec 02 21:21:33 Sensor 0 C: 21.50 F: 70.70
Dec 02 21:21:35 Sensor 0 C: 21.44 F: 70.59

上記は2秒間隔でセンサーの値を5回取得する指定です。摂氏と華氏で温度が取れているのがわかります。

ちなみに、筆者はこれを家のLinuxルータに刺した上で取得した値をMackerelに書き出しています。

温度変化グラフ

上記のグラフが作りたいだけならRaspberry Piで温度センサーを扱った方が楽なのでは?と思われるかもしれません。理屈で言えばそうかもしれませんが、個人的にRaspberry Piは長期間電源を入れっぱなしにする気が起きないので、ふつうのLinuxマシンで運用できることに価値があるように感じています。同じ感覚の方が他にいらっしゃるかはわかりませんが…。

まとめ

  • DigiTempというLinux/macOS上で温度センサーDS18B20を扱うOSSを紹介しました
    • シリアル通信(UART)経由で1-Wireセンサーをドライブできます
    • 多くのLinuxディストリビューションで標準パッケージ採用されています
  • Raspberry Piで同じことをするより適用範囲が広かったり長期運用しやすかったりするかもしれません

@hnw

こんにちは、@trigottです。この記事では、社内で行っている Agda ハンズオンの紹介をします。

はじめに

Agda とは、依存型の使える関数型プログラミング言語、あるいは定理証明支援系です。Coq などとは違いタクティックは使わず証明項を直接記述するスタイルですが、Emacs 上で対話的に証明を進めるためのインタフェースが用意されているため、効率的に証明を進めることができます。Agda で n * 2n + n が等しいことを証明する動画を撮影してみました。雰囲気がつかめれば幸いです。

KLab では月に1回 ALM(All Layers Meeting)という社内勉強会を開催しています。学生のころから Agda が好きで触っていたこともあって、Agda に関する発表をしたところ、先輩からハンズオンを開いてほしいということを言われました。ハンズオンとかやったことないし、Agda も人に教えられるほどではないし・・・と最初は不安だったのですが、まあ全3回くらいでやってみよう、という軽い気持ちで開催することにしました。社内から参加者を募り、集まるか不安でしたが5人の方が参加してくれることになりました。この勉強会は昨年の10月から始まり、現在も継続中です。

ハンズオンということで、一人で進められるような資料を作成しました。具体的には、資料は Agda のプログラムとして実行可能なファイルで、コメントとして説明を記載し、さらに演習として、埋めるべき箇所を指定したプログラムを所々に配置しています(Software Foundations の真似をしました)。演習の問題は以下のように作成しました。

-- ==================================================================
-- Exercise: (2 star) app-assoc
-- _++_ の結合法則を証明してください。_++_ は右結合なので、xs ++ ys ++ zs
-- は xs ++ (ys ++ zs) と解釈されます。
-- ==================================================================

app-assoc : ∀ {A : Set} (xs ys zs : List A)
            → xs ++ ys ++ zs ≡ (xs ++ ys) ++ zs
app-assoc = ?

2 star は問題の難易度を示しています。特に基準を設けず難易度付をしてしまったせいで、あてになりません。コメントに問題の解説を書いています。問題の本文は実際の Agda のプログラムです。基本的にどれも証明すべき命題=プログラムの型だけを記述し、値は ? だけの未完成なものになっています。Agda ではプログラムの代わりに ? を書くことができ、プログラムとしては不完全ですがコンパイルを通すことができます。なので、まだ解けていない問題がある状態でプログラムをコンパイルしてもエラーにはなりません。また、Emacs でファイルをロードすると埋めるべき ? の一覧が表示されるので、現在の進捗が分かります。

資料は https://github.com/krtx/agda-handson にあります。最初は全3回くらいで終わる予定でしたが、資料を作成しているうちに内容が膨らみ、気づいたらDay1からDay6までの全6部構成になっていました。以下、各ファイルについて解説と作成時の苦労について書きます。

Day1

一番最初に作ったので、一番気合が入っていて、一番長いです。真偽値と自然数を題材にして Agda での基本的な定理証明の仕方を解説しています。≡などの文字の入力の仕方や、Emacs でのコマンドを使った対話的な証明のやり方などです(そう、このハンズオンは Emacs が前提です)。Day1 の最後は、自然数の大小関係を定める2つのデータ型が互いに等価であることを証明する問題になっています。Day1 と言いつつ、1日ではまったく終わりませんでした。

Day2

等しいことの証明をする際によく使われる Rewrite パターンと equational reasoning combinator というものについて(あとおまけで自動で証明してくれる SemiringSolver について)解説しています。Day2 の演習の最後は (a + b) * (c + d)(a * c + b * c) + (a * d + b * d) が等しいことを証明する問題です。Rewrite パターンか equational reasoning combinator を使ってこの問題が証明できれば、初等的なものに限れば等しいことの証明は大体できるのではないでしょうか。

Day3

新しい構造としてリストの解説を、またリストに関する証明を題材として With abstraction の解説をしています。真偽値→自然数→リストという順番でデータ構造を紹介するのは、構造が徐々に複雑になっていくという点で自然に難易度を上げることができているのではないかと思います。rev-involutiverev-injective は Software Foundations のものを真似しています。with abstraction が説明できたので with abstraction を使うことで実現できる inspect パターンというものも説明しようと思ったのですが、例が思い浮かばず断念しました。

Day4

レコード型及び依存型を伴うレコード型について解説しています。レコード型の例として二次元平面上の点を定義し、それを使ったマンハッタン距離に関する性質の証明を演習としています。マンハッタン距離が三角不等式を満たすことの証明はやってみると意外と面倒なのですが、面白かったのでそのまま演習に残しています。ただレコード型の理解に貢献する問題ではないので、余力がある人向けとなっています。この辺から例を考えるのがかなりしんどくなっています。

Day5

偽及び Absurd パターンの解説をしています。偽についての説明は、自分の力量不足で怪しいかもしれません。演習には古典論理にまつわる命題をいくつか与えており、そのために必要なので「かつ」と「または」についても解説しています。

Day6

最後は新しいことはなしで、これまでの知識を使って正しいソートアルゴリズムを定義するという演習です。どこまでヒントを出すかは悩みましたが、ソート済みであることなどの定義はすべて与えて、ソートするプログラムだけを書いてもらう形にしました。insert-sort は単にソートするだけでなく、命題を見ると結果のリストがソート済みであることも要求しています。想定解法では、ソートをしつつ証明も同時に行うようにしています。このように、証明とプログラムが一緒になった証明のスタイルを intrinsic な証明と呼び、一方プログラムを単体で書き、それに対する証明を別で与えるスタイルを extrinsic な証明と呼びます。Agda では intrinsic な証明が多いようなので、insert-sort の型もそれを推奨するように作ってみました(ただ説明がないので、ちょっと中途半端...)。

やってみての感想

実際にハンズオンをしていく中で出てきた感想です。

refl が分からん

Day1 である2つの項が等しいとはどういうことか、またそれはどのようにして証明できるか、について説明したのですが、これが分からないという意見が非常に多かったです。Agda では等しいという関係 _≡_ は以下のように定義できます。

data _≡_ {A : Set} : A → A → Set where
  refl : ∀ {x} → x ≡ x

以下のような点から、_≡_ を理解するのは非常に難しかったようです。

  • 関係をデータ型として定義するというのは、普通のプログラミングでは出てこない考え方であること
  • _≡_ という型自体が値を受け取っていること(依存型)
  • refl の引数が implicit になっていること
  • Agda が値を比較する際には正規形に計算してから比較するため、プログラムの字面とは違う値が比較されていること

等しいというのはとても馴染み深い関係のように思えるにもかかわらず、初心者にとっては超えるべきハードルがいくつもあります。自分でも説明に窮する場面が何度もあり、まだまだ十分に理解できていないなと感じました。もう少し簡単な関係から始めるべきだったかもしれません。

Agda がどこまで計算してくれるのか分からん

Day1 では足し算を以下のように定義しています。

_+_ : ℕ → ℕ → ℕ
zero    + m = m
(suc n) + m = suc (n + m)

このため、以下の命題中に現れる (suc x) + y という項は suc (x + y) に計算されます。

prop : ∀ x y → (suc x) + y ≡ suc (x + y)
prop = refl

refl は対応する命題の左辺と右辺が同一の項であることを要求します。(suc x) + y という項と suc (x + y) という項は構文解析をした時点では違う形ですが、Agda によって (suc x) + ysuc (x + y) に計算されるため、refl を使うことができるようになります。このように、Agda が自動で計算を行うということを知っていないと、なぜ証明が通るのかが理解できません。また、足し算の定義を覚えていないと、どこまで計算が進むかも分かりません。自分もこの辺りの理解が甘く、テキストには解説を書けていませんでした。

名前が読めない

Agda の標準ライブラリを見ていると、n ≤ m → n ≤ suc m という命題に n≤m⇒n≤sm という名前をつけるなど、空白だけ詰めた名前を採用していることが多いです。Agda では : など一部の例外を除いて基本的に空白で区切られるため、n≤m⇒n≤sm のような名前でもひと続きの識別子として認識されます。このハンズオンでも同様の命名法を採用したのですが、やはり n≤m⇒n≤sm はひと続きの名前としては認識しづらいとのことでした。

rewrite はロードが必要

rewrite は 文脈中のある項を別の項で置き換えるパターンです。以下の例のように使います。

posulate
  A : Set
  a : A
  b : A
  eq : a ≡ b

lem : suc a ≡ suc b
lem rewrite eq = {! ここの命題は suc b = suc b となる !}

ただし、rewrite を書いただけでは反映されません。rewrite を書いてからロードして初めて文脈に反映されます。テキストのなかでも注意がなかったため、ここで戸惑う参加者の方が多かったです。

reasoning combinator はよしなに推論してくれない

Day2 ではある2つの項が等しいという命題について、rewrite と reasoning combinator それぞれを使った証明法を解説しています。上述の例と同じ命題を reasoning combinator を使って証明すると以下のようになります。

lem′ : suc a ≡ suc b
lem′ = begin
  suc a
    ≡⟨ cong suc eq ⟩
  suc b
    ∎

rewrite の場合は eq だけを指定すればよかったのですが、reasoning combinator を使う場合は suc がついていることを明示してあげる必要があります。

reasoning combinator は対象となる項を書く必要があり、また完全な証明を与えなければならないため、冗長な記述になります。ですが、冗長になっている分、説明が多いためこちらのほうが分かりやすくなっています。実際参加者の間では rewrite による証明よりも reasoning combinator を使ったほうがわかりやすいと評判でした。

標準ライブラリに何があるか把握するのが難しそう

演習を進めていく上で補題が必要になったとき、それが標準ライブラリにあるかどうかが分からない、という声がありました(このハンズオンでは標準ライブラリの解説は対象外にしていたのでそのあたりの話は特にテキストには書きませんでした)。これは実際もっともで、自分もいまだにどのように探せばいいのか分かりません。補題を探すときはファイルを標準ライブラリから直接目で見ることが多いし、モジュールの構成も完全には頭に入っていません。どうすればいいんでしょうか。

1週間空くと何をやっていたか忘れる

普通のプログラミングではないし、週に1時間しかやっていないため、どうしても前回やっていたことを忘れてしまうという声が多かったです(1時間の最初は前回やっていたことを思い出すところから始まる)。しょうがないところもあるとは思いますが、この問題に対しては対策を思いつきませんでした...。

おわりに

初めにも書いたとおり、当初は3回完結の想定(本気で3回でソートまでできると思っていた)だったし、やる内容からしても(そして最初の依頼に沿う形としても)ハンズオン形式が相応しいと考えて、ハンズオン用の資料を作成しました。ところが、蓋を空けてみるともう半年以上も続いています。ハンズオンという自分で進める形式の勉強会が長期に渡ると、参加者の間で進度に差が出てしまうという問題が発生します。途中から参加者が少ない場合は開催を中止するようにして、なるべく差が出ないよう配慮をしました。

ハンズオンをやることになったときに思ったことの1つとして、Agda が非常に入門難易度の高い言語であり苦労した経験から、自分が教えることでその障壁を少しでも和らげることができたらいいな、ということがありました。同じ証明支援系である Coq などと比較すると、決定版と言えるような教科書はなく(教科書は最近出版された1冊だけあり、入門にはよさそう)、日本語の情報もそこまで多くはありません。一体、世間の人はどのようにして Agda を学んでいるのでしょうか? 標準ライブラリを使いこなしている人間がどれだけいるのか、気になります。

↑このページのトップヘ