AlohakunKotobaZeme
書き替え推奨。
会場情報詳細などはETSeminar2008をみてください.
来そうな人?
- 名前: コメント: 29夜: 31昼: 30夜
- shinh:あくまで問い詰める会です:△(不明):○:○
- soutaro:○:○
- kmizu: 旭川のとき(http://alohakun.blog7.fc2.com/blog-entry-807.html)はあんまり問い詰められなかったので、今度こそ: ○:○:○
- kimura 31日との昼ということで○ です。△△△ かなあ? あろはさんの卒論途中までしか読んでない。
- odz: ×:○:○ あれ、気がついたら定員埋まってる?キャンセル待ちで。
- YT
- wo: 問い詰めたいです:△:○:○
- y14c: イクイク詐欺:○:○:○
- naoya_t: 素人(言葉責め的な意味で)ですが行ってもいいっすか:○:○:○
- s1061123: LL当日じゃなければどっちでも大丈夫な予感です:○:○:△
- shelarcy: 大所帯になってきましたね。こちらにも参加する予定です。:○:○:○
- m0h1can : 麻縄で大丈夫ですか?蝋燭は?:○:○:○
- masa_edw:うふふ:○:○:○
- __tad__
- ふじさわ:○:○:○ すみません。急用で行けなくなりました。
- kinaba 行けるっぽい:○:○:○
- hogelog:○:○:○
- koguro:まだ大丈夫かな?:○:○:○
- ryoakg:希望:○:○:○
- ココサブ :×:○:△
- sakai :○:○:○
- yhara LLの打ち上げと以下略。:○:○:△
- アキラ :○:○:×
- melpon :○:○:×
- NyaRuRu これはご挨拶せねば.集中講義扱いで2単位ぐらい欲しい.:○:○:○
- Theoria 「なんか発表するから参加さして」とかダメ?:○:○:○
- yoshihiro503 キャンセル待ち。:△:○:○
- takahashim キャンセル待ち。 :△:○:△
- ujihisa キャンセル待ち。 :△:○:○
- yas キャンセル待ち。 :○:○:△→8/31 9:40 すみません。所用で11:00頃到着になりそうですm(_ _)m
- bero キャンセル待ち。
30人になったので一端締め切ります.後はキャンセル待ちでお願いします.
ラボの人
無理そうな人リスト (間違って移動してたらごめんなさい)
- TAKESAKO:東京に誘った張本人として責任を…(と思ったけど第3回審査G委員会があったので参加できず…):×:×:×
- QLeap: 行くかもしれません(31日に開催されるみたいなので無理です...):×:×:○
- hyoshiok :○:○
- hi_saito: 行けなくなってしまいました。申し訳ないです。:×:×:×
- Isoparametric仕事でいけなくなってしまいました。残念です。orz...
- kosakiこれって会場ドコー?:キャンセルらしす
hyoshiokさんはぜんぶ来れるという意味ではないのかな?
会場
29日はどこか決まってますか?
31日 10:00〜17:00 サイボウズ・ラボ(http://labs.cybozu.co.jp/access.html ) 最大30人ですが,参加者の中に2名ラボの人間がいるため,後1〜2人OK.
アジェンダ(パネルディスカッション以外はこんな感じの流れになればいいかなぁと。実際は自由討論or講義中の質問が長くなると思われる): http://shinh.skr.jp/h/?ETSeminar2008 ←なんかこれがアジェンダみたいな雰囲気で書かれてるけどあくまで本当のアジェンダは下記。あくまでセミナーじゃなくて問い詰める会。
アジェンダ
あろは先生が泣くまで問い詰めるのをヤメない感じで!
↓せっかく北海道からいらっしゃってるので、 普段議論しにくいことをなるべく議論したいと思っています。 ですから、示された論文を読むとかは難しいにしても、 あろはさんのブログ の ET タグ、研究関係タグあたりはざっと目を通してることは 前提として議論ができるといいなぁと思っています。 わがままですが、当初の目的は「問い詰める」ことにあるため、 全員がついて来れることよりは詳細な議論を優先したいと 強く思っています。 あと個人的には講義中にも突っ込みが入りまくるのが望ましい。 来た人は kmizu さんによる Scala 勉強会のイメージで (shinh)。
alohakunがETについての解説(もちろん本来の目的のLLに差し支えない範囲で).ただし,多少のバックグラウンド知識は共有したいので,何のために何を目標にしてるのかをざくっと.できればPrologの初歩から(あるいは最低ここまでは各自予習しておくことを示してくださると助かります).そのあと or 随時質問タイム.他に発表したい人はいらっしゃるのかしら(→alohakunの集中講義が嬉しい).
ET
- 基本的に、やりたいこと、はたぶんわかってると思う。どうやってやるかがわからない。
- その目指す物と論理型言語が関係しそうなのはたぶんわかってると思う。しかし Prolog に対して何が良いのかよくわからない。
- how ではなく what 的な意味で what の記述はどのへんを目指してるのか。人間が口で命令とかが理想?
- 下の方に行って optimize とか本当にできると思っているのか。一般に optimizer は NP で等価変換の最適な組み合わせ? を考えるのも NP になるのでは。
- そういった制御が automagical に行われちゃうと、結局 Prolog の cut みたいに手動制御がキツくなったりしないのか。
- そもそも理論的な背景とかもうちょい知りたい。上記のようなことを等価変換の枠組を使うと嬉しい理由がよくわかってない。
- 他の人の研究とか。
- てか本当に what が重要で how は重要でないんだろうか。
- というかPrologだと how の what を書いてしまいませんか?
(両方重要で,どういう what からどういう how を生成可能なのかという関係性の研究が本質だと思います)
(他のパラダイムは,what か how のどちらかに偏っているのが良くない)
(上のレベルから,下のレベルまで,プログラムを探索する理論が無かった)
(Prolog だと,良い how が出せるような what 書けないです)
(一階述語論理とかは,プログラミングの基礎を支える理論としては不十分過ぎる)
(良い what が書けること (宣言型),良い how が書けること (低レイヤーな命令型) だけではダメ)
(良い how を得るためには,良い what から,多様なアルゴリズムを生成できる必要があります)
(ET の理論は,アルゴリズム探索のための空間 (ルールの空間) が存在するのが嬉しい点)
(余計な制限や過去の Logic 方面などのしがらみが無い,等価なものを生成して,変換していく純粋な理論があれば,安全に豊富なプログラムを探索できる)
(僕は低レイヤーの方の研究しかしてないので,理論の方面はよくわかってないので全く説明できないのですが,ET の理論は,Logic Programming の方面からセマンティックウェブ (Description Logic とか) の方面まで,新しい基礎を与えることに成功しているそう)
(自分の今の研究は,決定的なアルゴリズムを表現する D ルールの集合から,正当な命令型プログラムを生成するための理論)
- このへんを専門用語の羅列でなく、わかりやすい日本語の文章でまとめていただけませんか。できれば、短い文でかつ段落つけて一ページぐらいでまとめていただければ幸いです。おしそがしいでしょうからべつに、発表原稿にされてもかまいません。
- とりあえず具体的な例を見せてほしい
- 「理論的なことはわからない」と言って逃げるのなら、そこから始めましょう
- 「既存のパラダイム」だとできないことがあるのならそれを示せば良い
- できないって、具体的にこれを計算すると止まらない、とかじゃなくても、もっと曖昧とした面でも良いので(パラダイムってそういうことかな?)
- 非常に限られた分野でもよいので、成功している事例を教えて欲しい
- 科学技術計算の類は制約系の what からシミュレーションを自動生成する研究があったと思いますが、実際のニーズは高速なプログラムの方なので結局は how 尽しになるんですよね。それに実用上必要な規模の計算というのはSMPマシンのクラスタとか、ゴツい共有メモリ持ってるとか、それこそクロスバネットワークだとかで、専用のプログラムを書くことになる。ここの部分とかでETって活躍出来ないんでしょうかしら、G.SteeleのFortressはこれを犯るって言ってますけど
(自動生成ではありませんが,搾り出し方という方法を使うと,システマティックに確定説による仕様記述から N ルールを生成できたりします.これは,宣言的意味の概念が明確で,仕様に対して正当なルールの積み重ねにより,仕様に対して正当なプログラムを構築可能なことが,ET の理論によって保障されているからこそ可能です)
ttp://assam.cims.hokudai.ac.jp/akama/j/papers/0701.pdf
(うちのボスのサイト ttp://assam.cims.hokudai.ac.jp/akama/indexj.html)
(関数型や論理型のパラダイムの中には,たとえば Coq のような,論理式から正しいプログラムを生成可能なものがありますが,それらはルールのように分解可能性のある(単体で正当性が議論できる)コンポーネントの集合で構成されているわけではなく,そもそもインクリメンタルにプログラムを構成していく,という概念がありません.Prolog の方は,そもそも仕様記述とプログラムの空間が同一なので,どうしても理論的に生成不可能なプログラムの存在があきらかになってます)
(あと,最近の研究なので,ちょっと誰でも見れる形では公開されてない論文になってしまいますが,確定節による仕様記述から,論理等価式を経由することにより,Prolog や関数型のような従来的なプログラム変換 (同レベルのプログラムを変形していくことによる最適化)では生成することが不可能なプログラムを生成可能であることがわかっています.なんで従来のやり方では不可能だったのか ? ということを説明しだすと長くなってしまうので,いろいろ難しいのですが…)
(また逃げと言われてしまいそうですが,僕は仕様記述からの N ルール生成のあたりの,上の方の理論はあんまり深いところまでわかってなかったりします.全体ゼミの時の,概要的な説明のレベル程度.D3 の先輩や,卒業した同期がやっていたところなので.ほかに,ウェブアプリケーションなどに対する応用を研究している人たちが何人かいます (学生にアルゴリズムの作り方を教える講義の e-lerning(sic) system 自体が,ET の理論に基づいて ET 言語で書かれていたりします)N ルールから D ルールの生成のあたりは,今後輩がやってます.D ルールから命令型のプログラムを生成するための理論を,今僕が研究してます.もっと下の方の,N ルールをハードウェアの仕様記述に応用したりしようとしている人もいます)
- ETのソースはどこにありますかクローズドですか
- ETのドキュメントの公開場所、教えてください。もしくは学内のみですか
(ETI のソースはクローズドですね… 昔は公開していたらしいのですが.もうとっくの昔に卒業されて,今はほかの大学の教員をされている方が保守されているので,そこらへんの事情はよくわからない感じです.論文とかも,学会に入ってないと見れないものが多いと思います.C++ のヘッダ使って,ETI のビルトイン作るドキュメントとかは,研究室内部のみ公開になってますね)
- ETかとおもったら上記先生の御回答の中にETIとあります
- ttp://assam.cims.hokudai.ac.jp/laboj/study.html
- ではETC とあります。(高速道路ではありません)
- ETI,ETCの意味おしえてください。
(自己解決) (C コンパイラ)(I インタプリタ)
- RAで教えてる内容
- 「〜できる」は「〜できる、なぜなら〜」「〜ができそう、見通しとは〜」「〜できると〜が言っていた」「〜ができそうと〜が言っていた」のような感じじゃないと信憑性がない。
- 全体の概要よりは、よく知っている部分を聞きたい
- 10年後に自分の研究がこうなっていて欲しいという目標
(一階述語論理とかは,プログラミングの基礎を支える理論としては不十分過ぎる)
- 具体的にどういう点が問題なんでしょう?
- 一階述語論理が不十分なのは理解できますが、そういった不十分な点を補うために時相論理とかいろいろな理論があるわけですよね
- これは個人的な感覚であって、あまり意味のある質問ではないかもしれませんが、全部を包括しようと思うと、めちゃくちゃ複雑になるか(C++)、プリミティブすぎて何を言ってるのかわからなくなるか(ラムダ計算)の、どちらかだと思うのですが、ET的にはその辺どうなんでしょう?
ttp://assam.cims.hokudai.ac.jp/akama/j/papers/0701.pdf
- 赤間先生の論文は当日までには読んでおきます
(関数型や論理型のパラダイムの中には,たとえば Coq のような,論理式から正しいプログラムを生成可能なものがありますが,それらはルールのように分解可能性のある(単体で正当性が議論できる)コンポーネントの集合で構成されているわけではなく,そもそもインクリメンタルにプログラムを構成していく,という概念がありません.
- なるほど。
- Coqの方式がモジュラでないということなら、
- CoqとETの違いのうちの、どの点が違うのか?
- どの違いが、この性質の差に寄与するんでしょう?
Prolog の方は,そもそも仕様記述とプログラムの空間が同一なので,どうしても理論的に生成不可能なプログラムの存在があきらかになってます)
- なるほど。知りませんでした。
- さて、「Prologだと仕様記述とプログラムの空間が同一」というのは、Prologの計算は、ある集合からその集合そのものへの写像である、ということでしょうか?
- だとすると、ETの場合にしても、「等価」な書き換えなのだったら、結局同じ集合への写像になるような気がするのですが。Prologと何が違うのでしょう?
(良い what が書けること (宣言型),良い how が書けること (低レイヤーな命令型) だけではダメ)
(良い how を得るためには,良い what から,多様なアルゴリズムを生成できる必要があります)
- ものすごく卑近な例で言うと、高級言語から機械語まで、行って帰ってくる方法がはっきりしている(等価だから)ので、上から下まで眺めながら最適化ができる、ということでしょうか?
(数学的な計算可能性ではなく,計算を表現するための理論 (プログラミングという行為を科学する理論,プログラム生成の理論)を考えたときに,一番プリミティブな原理は等価変換なのではないか ? という仮説というか,信念ですね.それを実証するためにいろいろみんながんばってる感じです) (僕の研究は,LLVM (機械語レベルのプロファイラに基づく自動最適化)のもっと上位レベルのようなものを目指しています) (アルゴリズムを D ルールの形で表現しておいて,実行環境に合わせて自動的に適応(進化)するプログラム,のようなものを実現する理論が作れたらな,と思ってます.僕自身,プログラミング言語理論とかよりは,AI 寄りの思考を持つ人なので.要するに,インテリジェントなコンパイラというか,アルゴリズムからの実行可能なプログラム生成システム)
- http://twitter.com/kinaba/statuses/870997868
- http://twitter.com/kinaba/statuses/871000558
- http://twitter.com/kinaba/statuses/871005715
- 仕様記述→Nルール→Dルール→命令型プログラム、が基本的な流れなのでしょうか。その場合、理想的にこの枠組みが完成した場合、プログラマはどのレベルで何を記述することになるのでしょう。「仕様記述」のみ?それとも、問題ドメイン特化の知識を上位レベル(仕様記述等)の書き換え規則ライブラリか何かとして記述したり、マシン固有の知識を下位レベル(Dルール等)の書き換え規則ライブラリとして書いたりするのでしょうか。
- 「ET言語」ってどこからどこまで? NルールとDルール? 仕様記述も含む?
- 「確定節による仕様記述から,論理等価式を経由することにより,Prolog や関数型のような従来的なプログラム変換 (snip)では生成することが不可能なプログラムを生成可能」というのは、ETパラダイムでは、プログラムレベルではなく仕様記述レベルの変換をサポートしているからそこが違う、ということでしょうか。他にも違いがある?
- 全々本質じゃないですが、NとかDって何の略ですか? どっちがどっちかよく分からなくなるので
- N = Non-Deterministic ですね。半分自己解決。Nだけだと prolog と変わらないっていうのは、そういう事ですね。
- 速度の問題。WhatからHowを探索する時間って尋常じゃない気がするのだけど、現実的なのか?
- 今でも十分現実的な速度が出ている?
- 今は現実的でないけど、将来のCPUならなんとかなるという予想?
- 今は現実的でないけど、探索アルゴリズムが洗練されていくのでなんとかなるという予想?
- 体系的になれば誰でもできるのは本当?論理の体系的な知識がある人よりもPHPを書けるプログラマのほうがはるかに多い気がするが。
- 人口の問題ではなく全体の生産性を考えた場合に体系的になってるほうが生産性が高い?
- 論理の体系的な知識は勉強すればPHPと同じくらい誰でも理解できるという前提?
- 教えている学生さんの反応
- 全体的な感想はどのくらい?
- どのレベルのアプリケーションまで書けるようになるの?
- 学生さんの専門領域ってどこらへん?
- ETのプログラミングスタイルってどんな感じ?
- まずは「こいつの論理体系はUmm...」とかで始まるのか?
- 「よくわからんけどNルール書いてみてtry & error だZE!」て感じ?
- どのくらいの規模のプログラムになればETのご利益が得られるのか?
- 10行程度のtoyプログラムで有用性が示せる?
- 1000行くらいの簡単なプログラム?
- 10人月とかの大規模なプログラム?
彼女について
- 借金は2人で返すのですか?
- ご両親への挨拶はすみましたか?
(僕の借金なので,当然僕が返します)
(てか,まだそんな段階じゃありません w)
- 10年後に二人の仲がこうなっていて欲しいという目標
- もう、私と研究どっちが大事なの!
(10 年後どころか,1 年後さえ怪しいです.僕が女性の気持ちがわからない駄目人間すぎるので,怒られたり失望させてばかり… 愛想尽かされないように日々努力努力です)
- 相手の方はワットアワンダフルは読まれているのでしょうか?
(未来嫁(α版)です。 ワットアワンダフルは難しいので、始めの数ページで厭きました。)
- オナホは廃棄ですか?
(「持っていた」とカミングアウトはされたんですが…。)
- 一部で"某といつめる会は、彼女に関する質問が少なすぎるだろ。"の声もあります。
- どんどん書いてください。
- アジェンダですので、先生!ここでは返答はしなくていいですよ
- オナホに関する記事は彼女さんはご存じですか?
(書いてたんですか?)
- どっちが良いですか?
(それは私も気になります。)
- α版は出されたようですが、β版の予定がはっきりしません
- 予定をおきかせください。
- 「なめるなよ…俺のCoq(= cock)が火を噴くぜ!!」と彼女に言ったことがありますか? 言ってください。
(そのうち「なめてくれ…(以下略)」と言われそうな気がしてなりません。)
その他
- odz さんへの暴言について http://twitter.com/alohakun/statuses/863505801
(twitter は会話の流れがあるので,そこだけ取り出されるとアレすぎですが.直前になにか微苦笑ネタの流れがあったはず)
↑artonさんのコメントですね
- 本当に x86 は複雑なのか
(全く無いです)
- blogの横幅が広くて横スクロールが出るのが……
- あろはさんからの質問は? - 例: http://twitter.com/kinaba/statuses/871316013
- なんか大変なことになってきた感じなので,みなさんお手柔らかに願いします (東京って怖いところですね >_<)
Keyword(s):
References:[FrontPage] [ETSeminar2008]