5ちゃんねる ★スマホ版★ ■掲示板に戻る■ 全部 1- 最新50  

■ このスレッドは過去ログ倉庫に格納されています

論理学の議論スレッド

1 :774-Trash:2021/07/21(水) 18:08:24.95 ID:ZQPlWh+wM
VIPのスレ↓から派生しました

大学行く(´・ω・`)
https://hebi.5ch.net/test/read.cgi/news4vip/1626847853/

このスレは>>1とID:4ocU5SAy0が使います
ただし時限付きです

2 :774-Trash:2021/07/21(水) 18:16:16.26 ID:ZQPlWh+wM
時限は7/28 0:00までです
俺は7/23 20:00まで別のレポートに追われているので、このスレが主に活動するのは
7/23 20:00~7/28 0:00の期間だと思われます

3 :774-Trash:2021/07/21(水) 18:17:41.11 ID:ZQPlWh+wM
ID:4ocU5SAy0さんは通りすがりのアドバイザーなので、本当に気楽に覗いてください
ご自分の都合を優先して、このスレに縛られることのないようにして下さい

4 :774-Trash:2021/07/21(水) 18:21:31.65 ID:nROmezbg0
こんな板初めて知ったわ

5 :774-Trash:2021/07/21(水) 18:24:06.64 ID:ZQPlWh+wM
>>4
ウェルカム
数年前にちょっとした移住騒動があって知ったわ

6 :774-Trash:2021/07/21(水) 20:25:40.66 ID:tlMrUK3Wd
ここが過疎った事件があったってこと?たしかにスレはここ数年以内のものばかり。

7 :774-Trash:2021/07/21(水) 20:56:29.44 ID:xzr4L/EX0
いや、ここは数年前に出来たばかりの板で、VIPからここに移住しようという動きがあった
だけどそれが沈静化した結果廃墟と化してる

8 :774-Trash:2021/07/21(水) 22:22:34.94 ID:nROmezbg0
なんだそりゃ、成功する見込みあったんか?

9 :774-Trash:2021/07/21(水) 22:25:15.88 ID:nROmezbg0
https://itest.5ch.net/test/read.cgi/news4vip/1515685036/
これか。

10 :774-Trash:2021/07/22(木) 10:53:01.30 ID:m3dX2/++0
成功する見込みは低かったけど盛り上がってはいたね
>>9みたいなスレが沢山立ってた

11 :774-Trash:2021/07/22(木) 11:30:30.97 ID:AbVAfFCF0
https://www.slideshare.net/yorisilo/slide-42646656
とりあえず概要の分かりやすそうなスライド

12 :774-Trash:2021/07/22(木) 13:38:06.60 ID:m3dX2/++0
ありがとう!!
本来自分で探すべきものなのに…助かります
ちょっとずつ読んでみるわ

13 :774-Trash:2021/07/22(木) 18:47:42.66 ID:AbVAfFCF0
ちょいちょい調べてみると、古典論理に比べて直観主義論理はタブロー法が使いづらいっぽいな。別のアプローチも検討してみるわ。

14 :774-Trash:2021/07/22(木) 22:55:14.81 ID:vf2Uty+C0
  皿
 ( ë) 死にかけの板ですまない
と_)

15 :774-Trash:2021/07/22(木) 23:58:22.50 ID:AbVAfFCF0
>>14
かわいい

16 :774-Trash:2021/07/23(金) 07:53:46.54 ID:CCfOoTqS0
>>13
なるほど…こちらも探してみるよ
今日の夜8時から本腰入れられるので

17 :774-Trash:2021/07/24(土) 04:13:04.86 ID:H9n+2O460
昨日の20時〆の課題が終わってない…
期限後提出だ……はぁ

18 :774-Trash:2021/07/25(日) 14:09:05.45 ID:JpxaTbWn0
お疲れ様です。出さないよりマシでしょ。

19 :774-Trash:2021/07/25(日) 14:09:48.78 ID:JpxaTbWn0
金曜から悪寒と微熱が出たからまさかと思ったが収まったのでただの風邪だった模様。

20 :774-Trash:2021/07/25(日) 14:21:55.48 ID:esdu9eFfM
おおお、安静になさってくれ(´・ω・`)
こんなご時世なのでね
課題は今朝2日遅れで出したよ
まぁ大丈夫だろう…

21 :774-Trash:2021/07/25(日) 14:23:08.72 ID:esdu9eFfM
さて、論理学の課題を本腰いれてやりますか
その前に風呂入ってくるけど

22 :774-Trash:2021/07/25(日) 16:56:05.61 ID:JpxaTbWn0
いま輪読で型推論周りやってるんだがちょうどやりたいことの逆なんだよな。

23 :774-Trash:2021/07/25(日) 18:14:32.50 ID:8VMnywxm0
型推論かぁ(´・ω・`)
授業でちょっとやったな
型方程式を解くアルゴリズムがあるんだっけな…

24 :774-Trash:2021/07/25(日) 20:16:21.90 ID:6tHJIRFNd
unification使うやつね(結構色々やってるのな)

25 :774-Trash:2021/07/25(日) 21:33:39.96 ID:JpxaTbWn0
Twitter上にIPC-botってのがあって、IPCってのはIntuitionistic Propositional Logicの頭文字なんだけど、リプで論理式送ると証明可能性と証明図返してくるbotがある。
んでその実装見つけたんだけどGitHubアカウントを2ちゃんに貼って良いものか。

26 :774-Trash:2021/07/25(日) 21:35:20.96 ID:JpxaTbWn0
ちなみに実装はKripke modelでrefutationを示してた。やっぱそれが王道なのかな。

27 :774-Trash:2021/07/25(日) 21:46:47.56 ID:JpxaTbWn0
ちなみにそのプログラムはOCaml製だけど、何の言語使うつもりでいる?

28 :774-Trash:2021/07/26(月) 06:24:15.51 ID:ZwU5l4+p0FOX
スライドを読んで考えていたら寝落ちしてしまった(´・ω・`)

>>24
まぁ厳密なことは抜きでさわりだけだけどね

>>25
おお!公開されてるものならいいんじゃない?

29 :774-Trash:2021/07/26(月) 06:25:17.28 ID:ZwU5l4+p0FOX
>>26
クリプキモデルっていうのはスライドにも出てきてたね
refutationっていうのはタブロー法とは違うのかな

>>27
Ocamlかぁ…読めない(´・ω・`)
Pythonを使うつもりでいるよ

30 :774-Trash:2021/07/26(月) 06:29:51.55 ID:ZwU5l4+p0FOX
ちょっと確認なんだけど「単純型付ラムダ計算」の場合はandやorは考えなくても良いんだよね…?

31 :774-Trash:2021/07/26(月) 07:45:11.45 ID:ZwU5l4+p0FOX
いや、でもせっかくならandやorも扱えたほうが高機能だしそうしようかな...

32 :774-Trash:2021/07/26(月) 08:41:53.70 ID:ZwU5l4+p0FOX
https://www.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=&ved=2ahUKEwiHirjnpf_xAhXhbt4KHXtgDtgQFjABegQIBxAD&url=https%3A%2F%2Fresearchmap.jp%2Fmultidatabases%2Fmultidatabase_contents%2Fdownload%2F233038%2F56c341162da76d03d3b1f7f4abb87754%2F4322%3Fcol_no%3D2%26frame_id%3D508325&usg=AOvVaw0mv33TfvvdMa5ld57oxHfr

ここが非常にわかりやすい
けど二重否定の規則が入ってるな…
二重否定は直感主義命題論理には含まれないけど単純にタブロー法から除けばいいんだろうか

33 :774-Trash:2021/07/26(月) 09:07:30.36 ID:NBKh9KBm0FOX
>>32
そうはいかなくて、古典論理だとαが成り立たなければ¬αが成り立つけど、直観主義論理だとどっちも成り立ってないことがあり得る。
だからKripke modelみたいに「最初αは成り立ってなかったけど、ある時を境にαが成り立つと分かった」ってのを表現できるモデルでなければいけない。

34 :774-Trash:2021/07/26(月) 09:09:02.30 ID:NBKh9KBm0FOX
>>30
授業で習った時に直和型や直積型は出てきたのかな?それ次第だと思う。

35 :774-Trash:2021/07/26(月) 09:09:33.13 ID:ZwU5l4+p0FOX
タブロー法は完全に理解したけど、出来たツリーからどうやってラムダ計算の項を構成すればいいんだろうか…(´・ω・`)

36 :774-Trash:2021/07/26(月) 09:10:59.69 ID:ZwU5l4+p0FOX
>>34
単純型付ラムダ計算の拡張として出てきたけど、まぁandやorの実装はそんなに難しくなさそうだし実装することにするわ

37 :774-Trash:2021/07/26(月) 09:13:59.63 ID:ZwU5l4+p0FOX
>>33
むむむ…難しい(´・ω・`)
じゃあタブロー法の、結論の否定を示すっていうスタンスがそもそもダメなんじゃ?

38 :774-Trash:2021/07/26(月) 09:18:21.60 ID:NBKh9KBm0FOX
>>37
だから>>11はそれをクリアするための方法を模索しているワケよ。

39 :774-Trash:2021/07/26(月) 09:25:00.81 ID:NBKh9KBm0FOX
https://github.com/qnighy/ipc_solver
↑IPC-botの実装。よくよく見るとminisat使ってるな。課題の条件に触れないだろうか。

40 :774-Trash:2021/07/26(月) 09:27:43.05 ID:NBKh9KBm0FOX
授業中にパーサーについて勉強したかね?もしそうだったら素朴に式を読み解いて証明を作る方式でいいのかもしれない。

41 :774-Trash:2021/07/26(月) 09:41:04.22 ID:ZwU5l4+p0FOX
>>38
おーなるほど!そういう話の流れなのね

>>39
これは難解だな…(´・ω・`)

42 :774-Trash:2021/07/26(月) 09:43:29.21 ID:ZwU5l4+p0FOX
>>40
パーサーについては全くやってないけど、正規表現とかはある程度扱えるから行けると思う
入力された型の解析は、以下のBNFでやろうと思ってる
identifierを英数字として

basic_type := <identifier>
type := basic_type | ( type ) | type -> type

43 :774-Trash:2021/07/26(月) 09:48:21.42 ID:ZwU5l4+p0FOX
授業でもそこまで高度な事をやったわけじゃないから、>>40の素朴にやる方法でいいのかもね(´・ω・`)
「自然演繹の証明木を作ってからラムダ計算の項に直す」っていう手法は、ラムダ計算の課題としては回りくどいようにも感じる

だから->が出てきたらラムダ抽象を作る、だとかそういう逐次的なアルゴリズムでもできるかも

44 :774-Trash:2021/07/26(月) 10:06:56.02 ID:ZwU5l4+p0FOX
構文木を作れたら、授業資料にある片付け規則を適用していけば行ける気がしてきた

Γ |- const : τ (定数)
Γ(x)=τ ⇒ Γ |- x : τ
Γ, x : τ₁︎ |- M : τ₂︎ ⇒ Γ |- λx : τ₁︎. M : τ₁︎→τ₂︎
Γ |- M : τ₁︎→τ₂︎, Γ |- N : τ₁︎ ⇒ Γ |- M N : τ₂︎

45 :774-Trash:2021/07/26(月) 10:32:13.43 ID:NBKh9KBm0FOX
BNFはパーサーじゃないと処理できないのでは

46 :774-Trash:2021/07/26(月) 10:37:35.50 ID:ZwU5l4+p0FOX
まぁ、パーサーに似たようなものを作ることになるね…(´・ω・`)
授業でパーサーを習ってないだけで、コンパイラの作り方的な本は読んだことがあるので言語の解析とかは多少分かる

47 :774-Trash:2021/07/26(月) 10:38:33.83 ID:ZwU5l4+p0FOX
とりあえずプログラム書き始めてみるわ(´・ω・`)
今日と明日しか無いしね、大変だ

48 :774-Trash:2021/07/26(月) 11:25:42.97 ID:NBKh9KBm0FOX
Pythonかぁ、関数型言語なら協力できるんだが。

49 :774-Trash:2021/07/26(月) 19:46:01.12 ID:ZwU5l4+p0
逆に俺は関数型言語は一切無理だw
ところで、やっとこさ入力の型を解析してツリー構造に直すプログラムができたよ…

あとはどうやってラムダ項を作るか…まぁこれが本命なんだが

50 :774-Trash:2021/07/26(月) 19:47:38.82 ID:ZwU5l4+p0
解析に使ったBNFを貼っておくね

最初は↓でやろうとしたんだけど
type := basic_type | ( type ) | type -> type | type /\ type | type \/ type

演算子の優先順位とか左再帰とかを考えてたら↓に落ち着いた
parenthesis = ( arrow_expr )
basic_type_expr = <identifier> | parenthesis
and_expr = basic_type_expr | basic_type_expr /\ and_expr
or_expr = and_expr | and_expr /\ or_expr
arrow_expr = or_expr | or_expr -> arrow_expr

51 :774-Trash:2021/07/26(月) 19:56:01.35 ID:ZwU5l4+p0
テスト結果

https://i.imgur.com/MEW91ew.jpg

52 :774-Trash:2021/07/26(月) 20:15:11.26 ID:ZwU5l4+p0
そういえば否定を入れるの忘れてた
まぁ簡単に出来そうだし後でいいか…

53 :774-Trash:2021/07/26(月) 21:02:59.33 ID:z8Vw1+Wid
おおお、いい感じ!

54 :774-Trash:2021/07/26(月) 21:05:14.30 ID:z8Vw1+Wid
型定数は追加できるかね?できるならボトム型⊥を追加して、否定¬αはα→⊥で表現できる。

55 :774-Trash:2021/07/26(月) 21:09:17.57 ID:z8Vw1+Wid
ツリー構造を自然演繹の導出図と見立てて、導出図からラムダ項を生成できるはずだ。型と論理式が一対一で、証明(導出図)とプログラム(ラムダ項)も一対一だ。

56 :774-Trash:2021/07/26(月) 22:09:51.47 ID:ZwU5l4+p0
>>54
おお、それは知ってる

>>55
まだ上のツリーは入力をバラしただけだからなぁ(´・ω・`)
型付け規則が10個あるから、その適用の仕方を全探索してラムダ項に直す作業が残っている…

57 :774-Trash:2021/07/26(月) 22:11:40.98 ID:ZwU5l4+p0
というわけで、今から風呂に入ってネカフェに行き、徹夜です(`・ω・´)ゞ
締切に間に合うか心配で寝たくないんでね

58 :774-Trash:2021/07/26(月) 22:27:01.41 ID:BykoIgYGd
タフだな、俺はもう翌日の失速を恐れて徹夜できないくらいにはジジイになった。

全探索より良い方法をちょっと考えてみるわ。IPCbotのコード読みでもするかな。

59 :774-Trash:2021/07/27(火) 01:11:30.41 ID:HhPl3q6F0
おお、全探索じゃない方法は俺も知りたいな(´・ω・`)
だがもう俺は締め切りに間に合わす事が第一になってる…

60 :774-Trash:2021/07/27(火) 01:13:02.75 ID:HhPl3q6F0
というか終電に間に合わなそうでパンクした自転車で猛ダッシュした挙げ句急いで入った改札はチャージが足りてないという地獄www
完全にヤベー奴になってる…
代金は到着の駅で払いますた

61 :774-Trash:2021/07/27(火) 01:44:24.09 ID:mFS8EQie0
大丈夫かwwwチャリのパンクはさっさと直しとかないとここぞという時に足留めしてくるから気をつけてな。

62 :774-Trash:2021/07/27(火) 01:46:51.36 ID:mFS8EQie0
最寄駅じゃないとこのネットカフェなのね。

63 :774-Trash:2021/07/27(火) 01:52:51.61 ID:HhPl3q6F0
まだ起きてたのかw
徹夜の奴に合わせてると生活ペースが乱れるぞ…(´・ω・`)
俺が住んでるとこは閑散としてるからちょっと遠くまで行かないと店がないんだよね

64 :774-Trash:2021/07/27(火) 02:07:38.68 ID:mFS8EQie0
自分の課題もやってるので()
確か論理式を元手にcanonicalなKripke modelを作って、それが元手の式を充足するならば恒真みたいなことが出来た気がしてる。
関数型だったら再帰的データ型誂えてちゃっちゃと素朴に作れそうだけど、Pythonだとちょっと面倒くさそうだから全探索が無難かもね。

65 :774-Trash:2021/07/27(火) 02:21:56.83 ID:HhPl3q6F0
なんだ同じ人種だったのか…
やっぱりこういうことは関数型のほうが得意なんだな
俺は手続き人間だからHaskellとか使えるのは憧れるわw

ちょっと暫く落ちる

66 :774-Trash:2021/07/27(火) 02:28:40.24 ID:mFS8EQie0
了解、俺はそろそろ寝て8時くらいから再開する。

67 :774-Trash:2021/07/27(火) 03:24:36.76 ID:HhPl3q6F0
乙カレー
コーヒーガンギマリで元気100倍!(白目

68 :774-Trash:2021/07/27(火) 03:52:33.14 ID:HhPl3q6F0
お腹いてぇ〜…
二回もトイレ行ったのになんで痛いんじゃ(´・ω・`)

69 :774-Trash:2021/07/27(火) 04:46:08.66 ID:HhPl3q6F0
直積型(and)の扱いがやばい…
命題Aを示す、から命題A∧Bを示すに言い換えられて実質Bは何でも取れるから扱いがむずい

70 :774-Trash:2021/07/27(火) 06:08:48.00 ID:HhPl3q6F0
やべぇ…めっちゃ今考えてるのやべぇ(´・ω・`)
俺結構考えるアタマあるじゃn!ということに驚いている

71 :774-Trash:2021/07/27(火) 06:09:40.04 ID:HhPl3q6F0
(アイデアが)出る!!イけそう!!

72 :774-Trash:2021/07/27(火) 06:10:13.59 ID:HhPl3q6F0
でもそれがなんで正しいかわからないんだよなぁ…

73 :774-Trash:2021/07/27(火) 07:38:09.81 ID:HhPl3q6F0
ヤバすぎる…andの解析の仕方にずっと悩んで朝が来た
Γ |- M : A∧B ⇒ Γ |- fst(M) : A ←この規則を逆から適用しようとするとめちゃくちゃバリエーションが多くなって詰む

今思いついたのはこの規則を常に順張りで使うように固定するってことだけど如何かな

74 :774-Trash:2021/07/27(火) 07:40:06.98 ID:HhPl3q6F0
神よお助けあれ

75 :774-Trash:2021/07/27(火) 08:14:55.86 ID:HhPl3q6F0
andの解析なんだけど、例えばAを示したければA∧Bを示してもいいし、(A∧B)∨(A∧C)を示しても良いんだよね
これだと無限にバリエーションが増えちゃうんだけど、まぁある規模までで制限すれば無限ループは回避できるかも知れないけどもっとスマートなやり方はないものかね?

示したいものをカノニカルな形にして、仮定もカノニカルにすれば必ず示せるのかな?
これが一番の疑問だ

76 :774-Trash:2021/07/27(火) 08:36:15.08 ID:HhPl3q6F0
http://proofcafe.org/sf/UseAuto_J.html

どうもここを読む限りCoqの自動証明機能でも結構いい加減らしい…
完全に命題を解くプログラムは不可能なんだろうか

77 :774-Trash:2021/07/27(火) 10:24:48.91 ID:mFS8EQie0
起きた(不眠が祟って寝過ぎた)

78 :774-Trash:2021/07/27(火) 10:43:47.83 ID:mFS8EQie0
>>76
全称量化と連言の組み合わせが仮定に来るとキツいって言ってるね。今のケースは量化が無いからCoqのやり方で問題無いはず。

79 :774-Trash:2021/07/27(火) 11:11:50.25 ID:mFS8EQie0
https://github.com/qnighy/ipc_solver/blob/master/solver.ml
↑これは直観主義論理版のタブロー法に当たるLGシステムに基づいて実装されてるらしい。
https://academic.oup.com/logcom/article-abstract/3/1/63/1043248?redirectedFrom=fulltext

80 :774-Trash:2021/07/27(火) 12:52:07.28 ID:mWwJwA1q0
おお、おはよう(´・ω・`)
俺もちょっと寝てしまった…
リンクありがとう、難解だが見てみるよ

81 :774-Trash:2021/07/27(火) 14:24:05.45 ID:mFS8EQie0
課題終わらせた。これから授業2連チャンだが時々こっちも考えるわ。

82 :774-Trash:2021/07/27(火) 14:52:41.38 ID:mWwJwA1q0
頑張えー(´・ω・`)
俺の方は10個ある型付け規則のうち8個目をカバーしてるとこだ
デバッグしてないからどうせ動かないけど…

83 :774-Trash:2021/07/27(火) 14:58:36.45 ID:mWwJwA1q0
でもよくわからないのは
A → B∨C という論理式が仮定にあって、これを何とか適用したりしてバラしたい場合はどうすればいいのだろう?

84 :774-Trash:2021/07/27(火) 15:00:16.53 ID:mWwJwA1q0
A → B∧C が仮定にある場合はまだやりようがある
直感主義論理だけでA→B とA→Cに分解できるから展望は開ける
でもORの場合は古典論理を持ち出さないと分解できない

85 :774-Trash:2021/07/27(火) 15:15:11.68 ID:mFS8EQie0
∨の消去規則は古典も直観主義も同じだった気がするけどな。

86 :774-Trash:2021/07/27(火) 15:18:41.21 ID:mWwJwA1q0
あら、そうなのかな(´・ω・`)
まぁB∨Cを消すだけなら場合分けすればいいのだけど、A→(B∨C)みたいに「ならば」と複合してるとどうやって消したものかわからなくなるわ

87 :774-Trash:2021/07/27(火) 15:30:01.71 ID:mFS8EQie0
なるほど。それを簡約する方法はなかった気がする。
A∨B→C ≡ A→C ∧ B→C
は成り立つけど、後件に∨が来る場合は一般論はないはずだ。

88 :774-Trash:2021/07/27(火) 15:35:35.52 ID:mWwJwA1q0
そうだよね…(´・ω・`)
昨日の夜証明してたら二重否定が出てきたわ
でも、今Coqでinductionタクティックを試してみたら、A→(B∨C)の形の仮定は
1) Bのみから結論を導く
2) Cのみから結論を導く
3) Aを導く
の3段階の場合分けで乗り切れるみたい?

89 :774-Trash:2021/07/27(火) 15:45:51.51 ID:mWwJwA1q0
inductiveってのは帰納的という意味らしい(´・ω・`)

本来証明探索は結論から大元を目指してボトムアップで(規則を逆にたどりながら)やっていくものだけど
ゴールを予想してしまってゴールからトップダウンに証明の現在位置まで降りてくるという方法でも良いということかも

90 :774-Trash:2021/07/27(火) 15:47:19.71 ID:mFS8EQie0
>>88
それって→消去と∨消去を順番にやってる気がするんだが。

91 :774-Trash:2021/07/27(火) 15:52:34.16 ID:mWwJwA1q0
>>90
まぁそうだね(´・ω・`)
でもコンピュータでやることを考えると、「いま示すべき命題を無理矢理B∨Cに変形してA→(B∨C)を適用してAにする」という流れよりは
「いま示すべき命題をBから示す。さらに、今示すべき命題をCから示す。最後にAを仮定から示す」という流れのほうがやりやすいんじゃないかなぁ

92 :774-Trash:2021/07/27(火) 15:53:26.80 ID:mWwJwA1q0
でもinductiveを使えば必ず証明が上手く行くのかどうかは俺には分からない…(´・ω・`)

93 :774-Trash:2021/07/27(火) 16:09:15.53 ID:mWwJwA1q0
なんか自分でも何言ってるのかよくわからなくなってきたよ…論理難しすぎ…
整理するとだね

証明探索の基本はボトムアップ
だから推論規則を逆に使って手当たり次第に探索していく
これが俺の信じる基本なんだけど、時々A→((X∧Y)∨(X∧Z))のような仮定が出てきてボトムアップでやるのはキツい

94 :774-Trash:2021/07/27(火) 16:09:47.69 ID:mWwJwA1q0
[ボトムアップ]
今示すべきことがXだったとすると、示すべきことをX∧Yに狭めても良い、かつX∧Zに狭めても良い
これらのどちらを示してもいいから(X∧Y)∨(X∧Z)を示せばいい
よって上の仮定が使えて示すべきことはAになる

95 :774-Trash:2021/07/27(火) 16:10:06.22 ID:mWwJwA1q0
これは明らかに不自然な手順で、もっと自然にやるならば(X∧Y)∨(X∧Z)からXが証明できるはずだ、
と予想してしまって、推論規則を順方向に使って示すほうが良い

[トップダウン]
(X∧Y)∨(X∧Z)を場合分けして、(X∧Y)が成り立つとき当然Xは成り立つ。(X∧Z)も然り。

この違いが>>91なんだろうな

96 :774-Trash:2021/07/27(火) 16:31:28.35 ID:mFS8EQie0
むむむなるほど。古典論理なら標準形が作りやすいけど直観主義論理は全探索すら面倒臭いな…

97 :774-Trash:2021/07/27(火) 16:34:34.56 ID:mWwJwA1q0
なんか高校受験の漸化式とかで、解答用紙にいきなり答えの数列を書いて、漸化式に当てはめて「ホラ合ってるでしょ?」ってやるイメージだな

98 :774-Trash:2021/07/27(火) 16:46:07.32 ID:mWwJwA1q0
で思いついたんだけど、アンドやオアって推論規則に加えて、このinductiveを組み合わせればこの世から消し去ることが出来るんじゃまいか?
まぁ代償として大量の場合分けが出るけど、アンドやオアが消えればもうこれらに関する推論規則は考えなくていいから機械的に証明しやすくなるな

99 :774-Trash:2021/07/27(火) 19:03:31.21 ID:vpX7fJ80d
授業関連終わり。∨と∧に関してはトップダウン的にinductiveって戦略で調べるってことか。

100 :774-Trash:2021/07/27(火) 19:41:20.14 ID:mWwJwA1q0
>>99
お疲れ様〜
そのとおり

101 :774-Trash:2021/07/27(火) 19:41:58.36 ID:mWwJwA1q0
なんか一切デバッグして無くて期限に間に合う自信なかったんだけど

一発で完璧に動いてもうヤバい

102 :774-Trash:2021/07/27(火) 19:43:42.16 ID:mWwJwA1q0
Coqみたいな動きしてる…もう凄い俺のプログラム

103 :774-Trash:2021/07/27(火) 19:51:51.81 ID:mWwJwA1q0
ちなみに今Contradiction(仮定同士の矛盾)が使えなくて詰んでるんだけど
単純型付きラムダ計算ではどう表現すれば良いんだろう

104 :774-Trash:2021/07/27(火) 20:03:50.64 ID:6ig6RbWbM
デバッグのために作ったインタプリタ↓

https://i.imgur.com/K973iGP.jpg

まだ自動証明のアルゴリズムは組んでない…(´・ω・`)
まぁ既に書いた関数を組み合わせるだけだと思うけど

105 :774-Trash:2021/07/27(火) 20:06:00.82 ID:q/P7xNhhd
有能だわ(結局俺何もしてない)

106 :774-Trash:2021/07/27(火) 20:10:19.16 ID:mWwJwA1q0
>>105
いやいや、人と話すっていうのは頭が整理されるしモチベーションもらえたからほんと感謝してるよ
何にせよ期限に間に合いそうでよかった

107 :774-Trash:2021/07/27(火) 20:12:53.66 ID:E291eMs7d
>>103
α∧¬α
---------

が出ないってこと?

108 :774-Trash:2021/07/27(火) 20:13:41.80 ID:mWwJwA1q0
>>107
そうそう
それってラムダ計算だと定数用意しなきゃいけないんだっけ

109 :774-Trash:2021/07/27(火) 20:25:37.19 ID:mFS8EQie0
>>108
undefinedを表す定数を用意するのは一つの手かな。

110 :774-Trash:2021/07/27(火) 20:31:20.95 ID:mFS8EQie0
通常のプログラムだと矛盾する体系は想定しないわな、意味がないから。HaskellだとVoid型という値のない型が⊥役で与えられてるらしいけど、Voidをプログラムに組み込むのは言語拡張を使わない限り禁じられてるとか。undefinedで代用するのは一つの手だと言われてる。

111 :774-Trash:2021/07/27(火) 20:35:00.47 ID:mFS8EQie0
つーか普通にすげえわ。学部でこういうの出して学生が普通に解けるのって結構レベル高いな。

112 :774-Trash:2021/07/27(火) 20:38:14.27 ID:mWwJwA1q0
なるほど…定数もいじれるようにしておこうかな
あと3時間でGUIチャレンジ行けるかな…

113 :774-Trash:2021/07/27(火) 20:39:50.51 ID:mFS8EQie0
そ、そこまで採点対象じゃないと思うがすごい情熱だ。

114 :774-Trash:2021/07/27(火) 20:39:53.91 ID:mWwJwA1q0
>>111
いや、正直言うと他の人は解けないと思う
今回の課題は複数問から1問選択して出すって感じだったんだけど俺は難しめのものを選んだ
一番軽いのは授業に関連する事を調べてA4で2,3枚にまとめるやつかな

115 :774-Trash:2021/07/27(火) 20:41:29.25 ID:mWwJwA1q0
>>113
いやまぁやるかは分からんけど…

116 :774-Trash:2021/07/27(火) 20:45:24.89 ID:mFS8EQie0
>>114
でた優等生宣言wまあでも大学2年だったら東大生でも半分以上は解けなさそうな問題。

選択問題なら異常に長い入力みたいな意地悪も無さそうだし全探索で合格点貰えると思うわ。

117 :774-Trash:2021/07/27(火) 20:48:56.82 ID:mWwJwA1q0
>>116
おお、ほんとできて良かったわ
今朝はかなり焦ってたけど今日はよく寝られそう
VIPにここまで論理学に詳しい人がいるとは思わなかったよ、付き合ってくれてありがとう

118 :774-Trash:2021/07/27(火) 20:55:17.21 ID:mFS8EQie0
>>117
(結局何もしてない…)
というかCoqモチーフでCUIまともに作るの偉い。ラムダ項をペッて吐き出す程度のプログラム思い描いてた。

119 :774-Trash:2021/07/27(火) 20:59:04.30 ID:mWwJwA1q0
>>118
コード600行くらいになってるからバグだらけだと思ったんよね
それで関数一つ一つを調べられるようにって作ったんだけど
これも評価に入れてほしいねw

120 :774-Trash:2021/07/27(火) 21:11:22.82 ID:mFS8EQie0
>>119
Pythonでモジュール化出来てるのは評価対象やろ笑お疲れ様です!

121 :774-Trash:2021/07/27(火) 21:16:28.02 ID:mWwJwA1q0
>>120
ありがとう!!(´・ω・`)
今日はこれから細かいバグ取りとレポート作成をやるので落ちます
俺は常にVIPにいるのでまた会うかもね

122 :774-Trash:2021/07/27(火) 23:22:59.06 ID:mFS8EQie0
おk(常にいるのかwww)。またそれっぽいスレ見かけたら覗いてみるわ。

123 :774-Trash:2021/07/28(水) 00:09:51.94 ID:x9Caf6Dv0
おお(´・ω・`)
ちなみにレポートは時間無くてアピールしたい苦労をほとんど入れられなかったけどプログラム見れば分かるでしょ(白目

124 :774-Trash:2021/07/28(水) 00:30:46.15 ID:pPZ9DbXS0
プログラムが本文やで。言語の指定があったなら動かして採点するだろうけど、なかったなら恐らくコード読みで採点される。

125 :774-Trash:2021/07/28(水) 00:36:09.65 ID:x9Caf6Dv0
マジか…人が読めるコードじゃない気がw
コードもアップしといたから動かしてほしいなぁ(´・ω・`)

126 :774-Trash:2021/08/16(月) 03:47:59.54 ID:8gAT34eZ0
形式手法の授業課題でSAT solver作った。

127 :774-Trash:2021/08/17(火) 23:17:10.10 ID:hFJQTghm0
いいね(´・ω・`)b
SAT solverというのをよく知らないけど
調べたら普通の定理証明より強い感じなのかな

128 :774-Trash:2021/08/18(水) 18:36:52.67 ID:xzTT4vXi0
古典命題論理の充足判定器で、与えられた命題論理式の真偽を判定する。面白みや難しさで言えば直観主義論理の証明器が上かな。(含意が否定と選言で書けるのがイージー。)
ただ代表的なNP完全問題、というかNP完全の定義に使われる問題で、高速なSAT solverが作れれば、他のNP完全問題をSAT問題に変換して高速で解けるという実用価値がある。

129 :774-Trash:2021/08/19(木) 19:17:14.43 ID:WyhKZKVD0
なるほど(´・ω・`)
広く応用が効くんだな
後学の人のためにここでソースコード晒してもいいかもね
ただ論理学に関心のある人がこの辺境に来るかどうかはアレだけどw

130 :774-Trash:2021/08/19(木) 19:19:09.48 ID:WyhKZKVD0
ちなみに明日成績開示なので俺が書いたコードは公開する予定(´・ω・`)
まぁ興味ある人はまずいないだろうけど万が一いたらコピペしてどうぞ

131 :774-Trash:2021/08/20(金) 16:23:29.44 ID:q58dtelm0
git晒すの気がひけるんだがパッケージごとzip化してDropboxとか使うのが無難かな?

132 :774-Trash:2021/08/20(金) 21:01:04.82 ID:AIDHesxe0
ファイル数個ならpastebin.plやubuntu pastebinでもいいかもね(´・ω・`)
俺は後者を使おうかな
ただ今日は眠いので明日やるかも…

133 :774-Trash:2021/08/20(金) 22:21:35.84 ID:q58dtelm0
Linux派か。

134 :774-Trash:2021/08/21(土) 08:51:40.40 ID:wVTvB9J00
うむ(´・ω・`)
Linuxはいい

135 :774-Trash:2021/08/22(日) 11:48:56.06 ID:uL+w792n0
Coqに似た直感主義命題論理の証明支援システム(´・ω・`)

1) parser.py - 入力された命題を解析し構文木を作成する
    https://pastebin.ubuntu.com/p/nj76dsNkpM/
2) prover.py - 命題の構文木から証明の探索・ラムダ項の構成を行う
    https://pastebin.ubuntu.com/p/Z3Q6cyjRQt/
3) main.py - ユーザーとの対話処理を行う
    https://pastebin.ubuntu.com/p/Gyn24TVzcv/

使用法: $ python3 main.py

136 :774-Trash:2021/08/22(日) 11:50:21.34 ID:uL+w792n0
拙作だが誰かの読み物になれば(´・ω・`)
ちなみに最高評価ですたv

137 :774-Trash:2021/08/22(日) 14:31:53.20 ID:SKZ5IBn50
最高評価神。

138 :774-Trash:2021/08/22(日) 14:39:06.92 ID:SKZ5IBn50
ubuntu pastebinってブラウザからだと保存期限がつく感じなんだろうか。

139 :774-Trash:2021/08/22(日) 14:40:48.92 ID:SKZ5IBn50
https://pastebin.ubuntu.com/p/TXkM753mTW/

やっつけなSAT solver。

140 :774-Trash:2021/08/22(日) 15:46:10.48 ID:SKZ5IBn50
>>139
これ単体じゃ動かせないな、yamlファイルでメタデータ管理してるのと入力データ用のファイルが別途必要になる。ディレクトリごとうpできるサービスないかな。(git)

141 :774-Trash:2021/08/22(日) 16:25:15.96 ID:uL+w792n0
Haskellは全く読めないけど、見た感じパーサがかなり簡潔に書かれてるね
調べてみたらDIMACS cnfっていう形式があるのか…
SAT/UNSATの判別は全探索なのかな?
コメントも多く書かれてて見やすい(´・ω・`)

142 :774-Trash:2021/08/22(日) 16:26:26.34 ID:uL+w792n0
>>137
thx!(´・ω・`)

>>138
投稿する時に期間をNoneみたいなのにすると期限なしになる
見た感じ保存期限が1年になってるね

>>139
何か本格的だな…(´・ω・`)
gitの捨て垢って簡単に作れたっけ

143 :774-Trash:2021/08/22(日) 18:03:23.84 ID:SKZ5IBn50
>>141
パーサー書こうかと思ったけど付属の文字列関数で十分だったわ。

DIMACSは選言式の連言で書く標準形の一種。整数で命題記号を表して、各行が選言式、全体が連言式だと見なす。負の整数は命題変数の否定を表すと考える。

SAT/UNSATは深さ優先探索。dpll_って関数の再帰の仕方に注目。また簡約の際にゴッソリ式が小さくなることが非常に多いので(連言式の中に⊥が現れたり、選言式の中にTが現れる時など)、全探索になることはそうそう無い。

144 :774-Trash:2021/08/22(日) 21:31:40.51 ID:uL+w792n0
>>143
なるほど(´・ω・`)
古典論理を扱う際のTIPSとして覚えておこう

145 :774-Trash:2021/08/27(金) 15:13:10.70 ID:A8a0l/zu0
領域理論の研究かじってるが面白い。型を位相空間、プログラム(λ項)を連続関数として計算理論や論理学を数学的に意味付ける意味論。

146 :774-Trash:2021/08/28(土) 08:04:01.80 ID:/nboC6Fi0
夏休みまで勉強とは頑張ってるな(´・ω・`)
院生って休みあるのか分からんけど…
型を数学的に扱う事が出来るのか

147 :774-Trash:2021/08/29(日) 00:22:19.50 ID:dwHNAADc0
こんな板があったのか

>>70
ちょうど20年前に卒研で関数型プログラミング言語Schemeを使ってた頃に面白いと思って
さらに20年前に書かれた中島玲二「数理情報学入門書 スコット・プログラム理論」を借りて読んだり
表示的意味論で書かれたScheme言語のR5RS仕様を読んでみたりしたけど
この20年間でどれぐらい発展したのかな?

148 :774-Trash:2021/08/29(日) 22:14:48.54 ID:WT85OmxH0NIKU
>>147
いつもの人じゃない人がまさかこのスレに来るとは…(´・ω・`)
ウェルカム!Schemeについては全く知らないので何とも言えんな
あと俺は論理学ガチ勢では無いのでコアな話は分からんぞ

149 :774-Trash:2021/08/29(日) 22:25:15.96 ID:WT85OmxH0NIKU
ubuntu pastebin がログイン必須になってるな…
以前はアカウント無しで使えた気がするが

150 :774-Trash:2021/08/30(月) 05:11:50.25 ID:kLvffr9l0
>>147
検索で来た人だろうか?論理学で検索したのかな?

Schemeは知らんけど、最近の言語系の応用だとRustのunsafeな部分を定理証明で安全性証明するパッケージの設計図としてsemantic domainが定義されてる例を見かけた。(まだ読んでないけど)
https://people.mpi-sws.org/~dreyer/papers/rustbelt/paper.pdf

151 :774-Trash:2021/08/30(月) 05:12:33.21 ID:kLvffr9l0
>>147
他には領域理論的測度論を構成する試みが25年前に出てきてて
http://www.doc.ic.ac.uk/~ae/papers/int.pdf
数年前に出た論文で計算機言語のsemantic domainにデフォで確率プログラミングの下地を仕込むとかいう面白い話を見かけた気がする。機械学習のモデル設計などで非常に楽が出来るとか言ってた気がするな。

152 :774-Trash:2021/08/30(月) 05:13:28.32 ID:kLvffr9l0
>>147
あと、関数型プログラミングでお馴染みの構造(state monadとかstored comonadとか)がElmだのReactだのの実用で使われ出してるけど、あそこら辺の背景にある具体圏は型とプログラムの圏で、それはつまりsemantic domainの圏。(俺は圏論から領域理論に手を出してる口です。)

153 :774-Trash:2021/09/03(金) 22:59:11.08 ID:hR2zsYiO0
ネットワークの勉強のためにLinux入れたぜ

154 :774-Trash:2021/09/04(土) 09:57:45.37 ID:E7lnPXgv0
Linuxは良いぞ(´・ω・`)b

35 KB
■ このスレッドは過去ログ倉庫に格納されています

★スマホ版★ 掲示板に戻る 全部 前100 次100 最新50

read.cgi ver 05.04.09 2022/06/21 Walang Kapalit ★
FOX ★