等価変換理論集中セミナー2008（at 溜池某所）

event
  • もともと「Alohakunを問いつめる会」と呼ばれていたもの
  • 楽しかった
  • すごい面子。「自分なんかがいていいのかなあ」というのは考えない方向で
  • 冷房が止まってたので、ちょっとしたがまん大会に
  • 自己紹介で各自、好きな言語を挙げる。たぶん一番多かったのはScheme、次がHaskellかC++あたり。どう考えても偏ってる
  • 以下、超てきとう自分用メモ
  • 第五世代コンピュータ
  • セマンティックWeb
  • 自然言語処理は死に絶えた？
  • What（問題？仕様？）とHow（アルゴリズム？）
  • PlologはWhatからHowが一意。速くしよう/Prologで解けない問題を解こうと思ったら仕様を変えるしかない
  • プログラム変換とプログラム合成
  • PrologがETのサブセット、CHRがETのサブセットであることは証明されている
  • Whatの中では仕様は変形するが意味は変えない
  • Deterministic Ruleはどの答えでもいいから仕様を満たす答えを1個出す。何と何をappendするとこれになるか、とかだと答えは複数ある
  • たとえば図を避ける
  • whatの枠組み（仕様記述言語）でwhatのようなhowを書くPrologは失敗？
  • howの枠組み（プログラミング言語）でwhatのようなhowを書くものも筋が悪い？。HaskellとかRailsとか？
  • 確定節で仕様Dと問題（定義域）Qを書くのがΣET
  • Qは無限集合
  • Qを制御すればどこまでプログラムがやればいいかがわかる。型を決めると最適化できるのと同じ
  • ETIは真のETではない。効率的な一部の実行をするのがETI
  • 構成的プログラミング。Coq。廃れた？→最近，OCamlの型システムの健全性がCoqで証明された
  • （休憩）
  • 与えられたルールが正当なルールかどうかは、前は人間が判断するしかなかったが、今は自動判定できるようになった
  • ルールを自動生成できるかどうか
  • 論理等価式をいう新しい式を入れることによって、ルールと節集合の間にワンクッション。計算の発散を収束させるルールを機械が証明できるようになった
  • ETルールはプライオリティが付けられる。誰がプライオリティを付けるのか？
  • 条件5　rv(*x, *y), rv(*x, *z) ⇒ {=(*y, *z)}, rv(*x, *y).　がキモ
  • Prologは確定節を使うので条件5のようなマルチヘッドの条件は書けない
  • 複雑な条件を優先？
  • シャピロのアルゴリズミックデバッギング
  • （休憩）
  • LispやPrologはなんでも項とリスト→豊富なデータ構造を扱えるようにするさまざまな試み
  • 入力されたデータから最適化？
  • alohakunが例として考えているのは並列実行モデル
  • Webアプリケーションを確定節で書くときれいにはまる。Eラーニングシステムはその一環ということになっている
  • Dルールは順番依存の処理なので，単体では正当性を証明できない。正当性が証明されるのはNルール
  • 懇親会
  • id:masa_edwさんのクイズに苦しむ
    • 手癖の悪い郵便配達人
    • ケーキを3人で3等分
  • ストーカーの話が思った以上に広がってた。やばい
  • 隣でSchemeのパッケージシステムの相談をしてた。CSAN？