ATND アテンド β PRODUCED BY RECRUIT

ログイン or 無料登録

計算機言語で定理証明

Proof Party.JP

Default latent
日時 :
2009/10/24 (土) 10:00 ~ 20:00
定員 :
10人
会場 :
東京 大久保(東京都新宿区百人町2-27-6)
URL :
http://ranha.kerox.info/proofparty/
主催者 :

発表

当日なにか発表したいものがある!

質問事項を纏めてスライドにしてぶちまけたい!という方は勝手にやりましょう。

会場

http://www.its-kenpo.or.jp/restaurant/okubo_kaigisitu/index.html

B室を全日で予約してあります。

注意点

  • 会場を借りるにあたり9450円の費用が生じます。これは当日参加した人数で割って各人が負担する事にします。
  • 会場への飲食物持ち込み一応禁止
  • 食事(お昼)は周辺で取る事に成っています。

定理 について

以下で述べている「定理」というのは、数学的な意味での「定理」と言えるほど強くて素晴らしげな存在に限ったものでは無いです。

取り消し線が使えないATNDさん凄い!!

コメントがあるので元の文を消さずに言い訳を書いておくと、定理=「数学のある定理」という意味では無いので、

数学の定理の証明とかはちょっと難しそうで出来ないよなー、という人でも大丈夫ですね!

意図

個々の言語だとこういうスタイルで出来るよね、とかそういう話を自由気ままに。

もしくは、個々の言語はどういう考えに基づいて作られているのか。似た様な事としてどういうものがあるのか、など言語自体に関する話も出来れば。



あとは、今一使い方が分からない、英語が読めないとかいう人の為に、個々の系を使っている人がこういう流れでやると良いんだよ、という事をその場で見せると凄く幸せなんじゃないかなーと。

当日出て来て欲しい何か

当日の流れ

個々の人で、超小規模、小規模ぐらいの問題を解いて来てもらって、こうこうこうすると出来るよねーみたいな話を楽しく繰り広げる。他の人は、実際にやりながらはぁなるほど!!みたいな感じでやりとり。

こんなのに来る人もそう居ないと思うので気ままに?

当日にその場で簡単な定理の証明もアクティブに出来ると良いかも。

ですから、原則参加者は発表者、では無くて説明者に成ります。

取りあえず4,5人ぐらい集まれば出来そうですね!!

日程に関しては

10がつ24にち けっきしゅうかい。

何を決起するんだろう…

その他あらゆる事に関して

コメントで!

お題は在った方が良い?

Wiki側を弄ってるので、Wikiの方を見てください。

お題は当日までにやっておいてください 適当に

在ったとすると何が良いだろう は コメントで!

さんすう

  • 自然数(エンコーディングは問わず)の加算での可換法則、結合法則、分配法則を証明。
  • (1 + 2 + … + n)/2 = n*(n+1) / 2の証明

すうがく

  • Bolzano–Weierstrassの定理(収束するとかいうヤツの方)
  • 中間値の定理(The Intermediate Value Theorem)
  • むしろ実数の構成周辺を埋める?

アルゴリズムの性質

    1. concat(nil,l) = l
    2. concat(cons(h,l1),l2) = cons(h,concat(l1,l2))

    とした時に、concat(l1,concat(l2,l3)) = concat(concat(l1,l2),l3)を証明する。


  • reverse (reverse list) = list : リストのリバース のリバースが元のリストと等しい事を証明する。

  • あるソート関数がちゃんとソートする事を証明?(ソート関数が何かはご自由)

数理論理学

  • 何か簡単なモノ
  • 直観主義論理での二重否定除去と排中律の同値性(m.sakaiさんthx!!)>

パズル

  • 何か簡単なモノ
  • 最もスタンダードなハノイの塔で、最短の手数が(2^n)-1に成る事を示す。

簡単では無い系

  • optional : Church-Rosserの定理(型無しλ計算の合流性証明)
  • optional : 古典一階命題論理の完全性証明(ヒルベルト流 Lukasiewiczの公理系)

何をすると 定理証明 になるの?

型=命題とか型レベルでじゃないとダメなの? 値レベル(実際に計算しても何とか)だと?? などの話もコメントで!

ただ1つ言えるのは、やりたい様にやってもらえると良いかなーっていう感じです。

そういう「方向性」を持って改めて自分の道具としての言語を見直せるとアリアリかなぁとは。

まぁコメントで!

  • このコメントは全員が閲覧、すべてのログインユーザが投稿することができます
ranha
ranha - (2009/09/10 (木) 00:35)
10日と書きましたが、11日の方が良いかもしれません。

12日も休みらしいので、10月10,11,12の何れかトータル的に都合の良い日が良さそうです。
m0h1can
m0h1can - (2009/09/11 (金) 10:08)
"数学的な意味での「定理」と言えるほど強くて素晴らしげな存在に限ったものでは無いです"というのは、逆に数学的な「定理」と言えるほど強くて素晴らしげな存在を扱っても良いんでしょうか?

その場合はプログラムでどう証明するの?翻訳ですか、僕分かりません。だからその、いわゆるロジックじゃないプログラム証明とかあるんですか?僕知らないです。

何言ってるのか分からなくなってきたので、とりあえず参加出来るようにスケジュール考えます。
ranha
ranha - (2009/09/11 (金) 12:27)
ああなんか「数学的な意味での定理」っていうのがまずくて、「数学の定理」の方が良かったかもしれません。

そう、私には定理=数学の定理っていうのがあって、定理はどこに行ったんや?って感じで、既に数学に存在している定理を証明しなおすだけ??な印象を与えたく無かったので書いた一文だったりします。

取りあえず「春香さんは可愛い」を証明する事を頑張るっていうのは、おっけーだよっていう感じ気持ち心雰囲気です。おっけーだからどう、というのは分かりません。
ranha
ranha - (2009/09/14 (月) 21:24)
私は11、12日いずれも大丈夫です。他の皆さん(て誰...?)はどうでしょうか。
ranha
ranha - (2009/09/14 (月) 21:36)
と思ったんですが、10月10日は、第一回層圏トポス米田フェスティバル(http://d.hatena.ne.jp/hiroki_f/20090913/1252807999)に参加しようと思うので、11日の方が良いとかいう事かもしれません。まぁ12日でも大丈夫です。
h-iwk
h-iwk - (2009/09/22 (火) 09:38)
難しいテーマのお話しですね。

『何をすると 定理証明 になるの?』ということだけれど、多分取っ掛かりとしては、例えば、『1』という極めて単純なプログラムが存在したとして、それをどう証明すればよいのだろうか?ということを考えるのがいいのではなかろうかと思います。

定理証明系はさっぱりだし、マーチンレーブの理論もさっぱりですが、とりあえず自分なりに回答すると、証明を行う主体が1と呼べるものを持っている、存在することを知っているなら、

1EXIST

で正しい、とされているのだと推測してま
h-iwk
h-iwk - (2009/09/22 (火) 09:41)
切れた。

推測しています。

構成的プログラミングの基礎を持っているranhaさんは実現可能性解釈やBHK解釈のところを読むのがいい。

当日実りある話をするならその2つの解釈とeval関数の動作内容について検討するのが建設的だと自分は思います。
h-iwk
h-iwk - (2009/09/22 (火) 09:47)
なお、1や複素数iはまだしも、他の難しい数学的対象物となるとオントロジーの問題になるので深く突っ込まないほうが無難です。

ちなみに、自分は未だに極めてややこしいことに巻き込まれて動けないので、参加できません(><)。
h-iwk
h-iwk - (2009/09/22 (火) 21:07)
補足:

eval関数については、実装の中身が見えないと何にもならないので、SICPかevalの中身が見えて実際に動く処理系blackとかを用意しておくか、難しいですが、構成的プログラミングの基礎における言語cvFLの定義18,19,20,21付近を読むといいと思います。

んで、できればeval関数の中身は削って、データが存在するかどうかの判定を行う節のみ残して、証明マシンとしては何をやっていることに対応するのか考えるといいかと思います。
m0h1can
m0h1can - (2009/09/29 (火) 08:06)
この会、内容的にも人数的にも場所が見つかるのか不安
m0h1can
m0h1can - (2009/09/29 (火) 08:15)
↓とか5人部屋で大体1100-1500Yen/Hour

https://www.ginzarenoir.jp/grms/pub/pc/schedule.php?c_type=
h-iwk
h-iwk - (2009/09/30 (水) 05:20)
このまま人数が増えないということであれば、止めにしてしておくほうが無難と思います。

スライドはそれに関係なく作ります。


それにしても、この流れどこかでブレーキかけるべきです、意味不明かもしれませんが。このまま進めても良い結果に帰結するとは思えません。
h-iwk
h-iwk - (2009/09/30 (水) 05:32)
少し前と異なり、多種多様な思惑が絡んできています。もはや、オープンに話をすすめていくことは危険性すら感じます(気のせいだとは思えません)。私もどういう思惑がからんでいるのか、全容は把握できていません。

 

もはや面白そうだからやろう、ではすまない話になりつつあるのだと思います。ここらで誰か全容を把握しており統制が可能な方に登場願いたいのですが、それは虫の良い話、そもそも統制可能な方が存在しない、のでしょうか。
h-iwk
h-iwk - (2009/09/30 (水) 05:42)
私は特になにか権利を主張したりはしないですし、策ももはやありません。というか、かなり前からネタ切れです。
ranha
ranha - (2009/10/01 (木) 12:11)
企画者ですが、ここの所忙しいっていうか10月10日はまず無理です。

11日なら大丈夫ですが、お題とかも決まって無い感じなのでこのまま11日に強行でやるのは可能なのかなーというのと、

場所も現時点でまだ取って無いので大変そうです。

ので、一週間ずらして17日か18日にしたいのですけど、大丈夫でしょうかね。
ranha
ranha - (2009/10/01 (木) 12:16)
一週間というか、10月中に取りあえずやりたいっていうそれなので、日時に書いてる10/10はあてにしないでください。

取りあえずお題が何か1つ出れば、それで内容は大体埋まってそこから色々話せて時間経つと思ってるので何か無いかなーみたいな。
m0h1can
m0h1can - (2009/10/01 (木) 15:20)
内容的に、ホワイトボードか何かがあるところが良いですね。

今とても忙しいんですが10日頃には暇になってるので、11でも17でも問題無いです。

ranhaさんがビシッと日程を決めてくれれば僕は調整するので。

ヒッソリ…とはいけません、ビシッとビシッと。あと、お題なにか欲しいですね。

僕がAgdaやCoqやっても駄目だなーと思うので、それ以外のアプローチで証明します。
h-iwk
h-iwk - (2009/10/02 (金) 08:12)
日程は追随します。

私のお題はかなり基本的な話で,なんで証明マシンが言語処理系に対応するのかという話です。

ゲーデル論文の46個の関数をHaskellで実装して動かして見ようと思っているのですが,見切り発車で動くかどうかわからない点,間に合うかどうかわからない点が厄介です。なので伸ばすのは賛成です。

算術ゲームはムリポ。
h-iwk
h-iwk - (2009/10/02 (金) 08:19)
あと,多分当日説明するだけだと細かい点で意味不明になると思うので,事前に資料配布(pdf)します。
masahiro.sakai
masahiro.sakai - (2009/10/03 (土) 13:01)
適当にお題の案でも
* (A→B→C)→(A→B)→A→C
* 偶数と偶数の和が偶数であること
* (直観主議論理の場合) 二重否定除去と排中律の同値性
* クイックソート
* √2が無理数であること
* チャーチロッサーの定理
h-iwk
h-iwk - (2009/10/03 (土) 18:55)
(直観主議論理の場合) 二重否定除去と排中律の同値性

に一票入れます。

あと追加で、『0』とか『1』の証明。プログラム『0』がなぜ正しくなるか、等。
m0h1can
m0h1can - (2009/10/05 (月) 11:34)
場所ですが、どこにも無ければ僕は別に筑波まで行くのもやぶさかじゃないですよ。

お題ですが、XXが決定可能かどうかは(他の会と被りますが)良いんじゃないでしょうか。

個人的には、このアルゴリズムの時間計算量がO(N^3)である、くらい証明出来てくれないと楽しくないなーとか思いますが、機械でどうやるんだろう?分からん。

sqrt(2)が無理数の証明みたいに、入力Aの場合にどうだ、みたいな証明は出来るようになりたいですね、個人的に。いやそれ機械がするのか?分からん。<b
h-iwk
h-iwk - (2009/10/07 (水) 20:04)
連動しているわけではないのですけど、上で書いたややこしいことのウェイトが増えてきた点とその他より、自分も見送りますというか、もともとこれを(説得力無いけど)最後に最後の旨を述べようと思っていたので、「言語」という文脈において偶然私に会うことは多分もう無いです。

 

ゲームのルールに従っているだけだと収拾がつかなくなる、というの自分の教訓です。
ikegami__
ikegami__ - (2009/10/10 (土) 06:00)
10/24(Sat)前後に上京します。10/26,27以外なら参加できます。10/9にranhaさんとそーたろさんとぼくで夕食したときに方向性を見いだしました。たのしみにしています!(参加できる日程...なら...)
m0h1can
m0h1can - (2009/10/13 (火) 10:08)
10/24了解です。ところで場所の目星はあるでしょうか?

市ヶ谷か大久保なら10人部屋半日が3000円ちょいで借りられます。

http://www.its-kenpo.or.jp/restaurant/okubo_kaigisitu/index.html

http://www.its-kenpo.or.jp/restaurant/itigaya_kaigisitu/index.html
ikegami__
ikegami__ - (2009/10/15 (木) 06:06)
個人的には、大久保 Best 市ヶ谷 Better です。けど、他の皆が 10 時に集まるとなると、市ヶ谷のほうがいいのかなあ... 気合い入れて早起きするぜ、とか、全日借り切っちゃうぜとかいうなら、大久保ですが...
ranha
ranha - (2009/10/15 (木) 10:02)
m0h1canさん場所の提案ありがとうございます。



上に書いてる10時っていうのは割と適当なので、今日カッチリ決めますが、ITSの両会場9:00 - 17:00 か 13:00 - 21:00でなんだろうちょっと・・・という感じに成ってますね。



そもそも懇親会とかやる気あるんだろうか、というか何を懇親するのか謎っていうかそれはさておき、頑張って全日借り切っちゃうというのも有りかなー。
m0h1can
m0h1can - (2009/10/15 (木) 11:18)
ITS借りる場合は、組合員の僕が予約しますので連絡ください。

筑波でやるのもそれはそれでフリーな感じが良いなーと思いますから僕はどっちでも良いです。

ただITSはネットワーク環境が無いと思いますからemobileか何か科学とお金を駆使して下さい。
m0h1can
m0h1can - (2009/10/15 (木) 14:00)
山崩し(パズル)

N個の山があり、夫々の山はM個の○から出来ている。先手、後手の順で自由な山から好きなだけ○を取る。

但し1度に1つの山から、残りの個数以下しか取ってはいけない。またパスは出来ないものとする。

最後に○を取ったら負けとなる。必勝法を証明せよ。



N=1の場合は自明、N=2の場合も自明ですが計算機証明は少し工夫?それ以外は難しいと思います。
m0h1can
m0h1can - (2009/10/15 (木) 14:20)
Bolzano–Weierstrassの定理(数学)

有界な数列は収束部分列を持つ、を証明せよ。



解析学の初歩で自明だと思いますが、構成的な証明なので計算機でもやはり自明かなと思います。

うーん、でも何を使うかでちっとも自明じゃない気がしてきました…。
ranha
ranha - (2009/10/15 (木) 17:10)
パズルはなんていうか、釣りっぽいソレですね。
釣りっていうのは、今回のコレに来ない人もちょっと考えてみましょう、というのにあたって取っ付き易いかな?だめかな?っていう。

少し前にはてダのどこかでハノイの塔の何ソレみたいなものがあったから入れてみました。

ので山崩しよりもうちょっと簡単な方が良いかなーと個人的に。でもどんなんが良いだろう・・・。

ワイエルシュトラスの定理は良いかなーと思います。ので入れておきます。とか私が選ぶべきじゃないよなぁ・・・。でも選びます!
ranha
ranha - (2009/10/15 (木) 17:26)
それから、場所に関してですが、私も大久保の方に一票です。

時間は、考えることが面倒臭いですから、全日で取っちゃって良いんじゃないかなぁと思います。

今日中(10/15)に他の提案が無ければ、大久保という事にしたいと思うので、m0h1canさんコメント見てたらそういう流れなんだなぁと思っておいてください〜
ぴらぴら
ぴらぴら - (2009/10/16 (金) 00:36)
Bolzano–Weierstrassの定理って、RCA_0とかその手の弱い数学だと、成り立たないので、それなりに強いらしい。
ぴらぴら
ぴらぴら - (2009/10/16 (金) 00:41)
中間値の定理とか、楽しそう。というか実数を構成して実数らしいことを示すだけでも楽しそう。
ぴらぴら
ぴらぴら - (2009/10/16 (金) 00:45)
あと、コンビネータSとKがあればいろいろ作れるぜというのも楽しそう。
ぴらぴら
ぴらぴら - (2009/10/16 (金) 00:46)
あっちからこっち、こっちからあっちに単射があれば、実は全単射があります、とかいうのも楽しそう。
ぴらぴら
ぴらぴら - (2009/10/16 (金) 00:50)
古典命題論理の完全性とか。主張を書き下すまでが面倒かもしれないけど。
ranha
ranha - (2009/10/16 (金) 12:55)
>> 実数を構成して実数らしいことを示す
これは良いですね。良いですねっていうか、なんだろ無いと悲しいですし・・・。



>> あっちからこっち、こっちからあっちに単射があれば、実は全単射があります
集合集合したものが入っていないので、これくらいは入れてみましょう。
ranha
ranha - (2009/10/16 (金) 12:55)
SKI-Combinatorはちょっと今回は避けてみようと思います。あと古典命題論理の完全性は個人的にはやりたいよーって感じですけどうーん・・・。



ヒルベルト流ウカシェビチの公理系(公理3つとモーダスポネンスのアレだけ)でやるとすると今回でも出来そうですが・・・。



あんまり大きいのをやって時間をそこに沢山時間割くのは、今回の本義では無い気がするので悩みますね。お題を当日までこなして来てもらって時間掛かりそうな所だけ徹底するっていうのでも良いと思いますが。
ikegami__
ikegami__ - (2009/10/16 (金) 16:32)
10/24 (土) 当日に空輸されます。10:00 には遅刻します。ほんとうにありがとうございました。
Dien island
Dien island - (2014/03/18 (火) 11:03)
記事にある情報はとても大切なものだと思います。これから定期的に読ませてもらうために、ブロブブログをブックマークさせてもらいました。ここで色々な、新しいことについて勉強させてもらいます!更新を楽しみにしています! web content development
lucas
lucas - (2014/06/20 (金) 18:32)
凄く興味深いです。あなたはとても良いブロガーですね。フィードに追加させてもらったので、これからもステキなポストを楽しみにしていますね。あと、私のフェイスブックでもシェアさせてもらいました! continue reading

コメントを投稿するには、ログインしてください。

掲載されるイベント情報は、利用者の皆様によりご提供いただくものであり、株式会社リクルートホールディングスは本情報の正確性や内容について、一切保証するものではございません。詳しくは利用規約をご参照ください。