論理学の議論スレッド

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

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

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

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

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

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

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

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

50774-Trash2021/07/26(月) 19:47:38.82ID: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

51774-Trash2021/07/26(月) 19:56:01.35ID:ZwU5l4+p0

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

53774-Trash2021/07/26(月) 21:02:59.33ID:z8Vw1+Wid
おおお、いい感じ!

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

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

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

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

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

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

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

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

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

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

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

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

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

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

ちょっと暫く落ちる

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

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

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

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

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

71774-Trash2021/07/27(火) 06:09:40.04ID:HhPl3q6F0
(アイデアが)出る!!イけそう!!

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

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

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

74774-Trash2021/07/27(火) 07:40:06.98ID:HhPl3q6F0
神よお助けあれ

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

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

76774-Trash2021/07/27(火) 08:36:15.08ID:HhPl3q6F0
http://proofcafe.org/sf/UseAuto_J.html

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

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

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

79774-Trash2021/07/27(火) 11:11:50.25ID: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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

107774-Trash2021/07/27(火) 20:12:53.66ID:E291eMs7d
>>103
α∧¬α
---------

が出ないってこと?

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

133774-Trash2021/08/20(金) 22:21:35.84ID:q58dtelm0
Linux派か。

134774-Trash2021/08/21(土) 08:51:40.40ID:wVTvB9J00
うむ(´・ω・`)
Linuxはいい

135774-Trash2021/08/22(日) 11:48:56.06ID: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

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

137774-Trash2021/08/22(日) 14:31:53.20ID:SKZ5IBn50
最高評価神。

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

139774-Trash2021/08/22(日) 14:40:48.92ID:SKZ5IBn50
https://pastebin.ubuntu.com/p/TXkM753mTW/

やっつけなSAT solver。

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

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

142774-Trash2021/08/22(日) 16:26:26.34ID:uL+w792n0
>>137
thx!(´・ω・`)

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

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

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

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

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

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

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

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

新着レスの表示
レスを投稿する