labg:emoto-lab:jssst2019

以下、発表の質疑周りのメモ

村田君の発表

東大の森畑先生
- Regular Functor も行く？ cata_charn の証明を与えるなら、他の functor でもいいんじゃない？　polynomial functor に限らなくてもいいよね。
  - initial_algebra が一般的な functor を型クラスのインスタンスで受け取るようにしておいて、polynomial functor については cata_charn を自動証明して initial_algebra のインスタンスを生成するようなものを用意しておくとか。
- Adjoint fold/余モナドの話は、Ralf Hinze の conjugate hylo でまとめられているが？
  - Hylo が……
- hylo できないのは残念ですね。
- Rel でやらなかったん？　Coq の関数を rel に見て、ゴニョゴニョして戻ってこれればいいんじゃない？
  - まあ、うまく戻ってくるのが簡単ではなさそうなので、とりあえず別にしてます。
- Haskell の deriving みたいな？　ADT定義から色々出せるといいけどね。
  - Coq 自体に手を入れればできるだろうけど……　テンプレート Coq があればいいのだろうか。
    - 実はそれらしきものは発見しているのだが、まだ全然追えていないです by muratak
      - https://github.com/MetaCoq/metacoq
- そして、プログラム変換は何ができたらいいんだろうね、と。
- 少し先のものなら、polynomial を regular とかにしようか？　join list とか rose tree とか。すぐに polynomial じゃ無くなっちゃうから。

東大の佐藤先生（黒い佐藤さん）
- Coq で generic programming はよくあること？　Coq 本に何かあったような？
  - Certified Programming with Dependent Types に何かあったような。

神野君の発表

筑波大学の長谷部先生
- 何でこういうグラフを作るんでしょうか？　シミュレーション？
  - テクニカルでない質問で難しいところですが、より具体的に性能評価にこのように使うと答えられたほうが良かった。
- 頂点 100万くらいだとスケールしていないのは？
  - HDFS の話をもう少しちゃんと補足できていれば説明がしやすかっただろう。
京大の平石先生
- 完全に同じではないですよね？
  - 神野回答：はい、違います。
- 明らかに違う性質はありますか？
  - 神野回答：分かりません。
    - なにか見つけられると面白いかも？
- 素朴には衝突検出してやり直せばいいじゃない？　全体の計算をやり直せばいいじゃん。
  - これについては……　衝突自体の発生確率が一定なので、悩ましい。大きなグラフなら衝突を無視できるので気にしないという方向には持っていけるが……
    - まあ、最初の方で生成していたのが小さかったので仕方ないとも言う
産総研の中澤先生
- P は再接続の確率だけど、K = 4 のときに……　P=1.0のときには全部再接続とかですよね？　現実的には重複あまりしないですよね？　重なったら性質変わっちゃうんですか？
  - 神野回答：とくに検証してない。
    - まあ、単純性という重大な性質が無くなるのと、重複辺の検出・処理の手間が増えるのだけど。
- K が小さければ重複無視できるだろうけど……　まあ、K は現実的にどの程度ですかね？
  - 神野回答：小さくはない（？）
    - ぶっちゃけ確率的を考えると、次のようになる。
      - a が b を選ぶ確率は PK/N で、b が a を選ぶ確率は PK/N で、ところで a も b も N の自由度があるから、重なる確率は P^2 K^2 / N^2 * N^2 = P^2 K^2 程度。
      - 重なる本数の期待値を出すと、\sigma_{a < b} (P^2 K^2 / N^2) = 1/2 * N(N-1) * (P^2 K^2 / N^2) = P^2 K^2 / 2 程度。N に依存しないところに注意。
        
        これについては簡単なプログラムを書いて試してみてみれば良い。実際に書いて実験してみてもこの程度。
      - 全部で NK 本の辺があるので、N を大きくすれば重複の割合は減る。その重複率は P^2 K / (2N) 程度。
      - とはいえ、ほぼ必ずコンスタントに重複辺が生じるので、「一本も重複辺がないグラフが出来上がる」という確率は悩ましい。