22/11/27 08:06:43.65 3pqSuWQI.net
>>181-183
>望月側の問題は、分かり易い解説というか、分かって貰える解説がない
>「論文に書いてあるから、注意深く読め！」というだけ
望月新一は自分でも証明できていないと思ってるんでしょう
しかしそれを認めたくない だから解説抜きで「読め！」の一点張り
ショルツェの指摘に逆上したのは、まさに図星を突かれたからでしょう
人間なんてもろいもんです
201:１３２人目の素数さん
22/11/27 08:15:50.24 3pqSuWQI.net
>>181-183
＞１）~７）
某スレでどなたかも指摘されてましたが、番号付けが奇妙ですね
いったい何の意味があるのか、一度も説明がありませんが
さて
＞ソフトのプログラムに、”コメント”を付けるとか、
＞プログラムの意図を表す名前を付ける、
＞使う変数も意図がわかるようにとか
＞プログラムの可読性を上げる手法はいろいろあるし
それは、Knuthレベルですな
Knuthレベルなら立派じゃん、というかもしれません
私がいいたいのは「全然ナイーブじゃん」ということです
DijkstraとかHoareとか、御存知ですか？
プログラムが仕様を満たしているかどうかは証明可能なのですよ
とくに、Hoare logicは、プログラムの正当性を検証するための論理ですね
ホーア論理
URLﾘﾝｸ(ja.wikipedia.org)
せめて、この程度のことは最低限の常識として知っておいてほしいですね
つまり注釈として書くべきことはホーア論理のステートメントである、と
まあ、実際にはそんなことしてるプログラマはほぼいないのでしょうが
実に嘆かわしいことだといわざるを得ませんね
202:１３２人目の素数さん
22/11/27 08:20:17.43 3pqSuWQI.net
>>186
＞フローチャートや、プログラムの設計図あるいは概念図を描くとか
いまだにフローチャートなんていってる人は
頭の中が１９６０年代のままなんでしょうか？
いわゆるフローチャートは構造化以前のものです
構造化以降もっと進化されたものがあります
まあ、それも今となっては前世紀のものですね
重要なのは流れではなく仕様の検証 おわかりですか？
203:１３２人目の素数さん
22/11/27 08:27:23.40 3pqSuWQI.net
>>181-183
>フーリエ変換で言えば、
>関数とそれに関する微分作用素・積分作用素をフーリエ変換をすれば、
>微分作用素・積分作用素が簡単に計算できて
>それを逆変換すると、微分方程式が簡単に解ける
なぜ、簡単に計算できるか説明しないんですか？ そこが要なのに
ぶっちゃけていえば、掛け算に還元できるからですね
大学にいけば、誰でも教わることなんですがね
ああ、大学にはいかれなかったんでしたね
それじゃ御存知ないのも無理ないですね
＞楕円曲線を、IUTで変換して遠アーベル界に持っていくと、
＞変換後の楕円曲線もどきの高さ評価が出来て
＞それを逆変換して、もとの楕円曲線の高さ評価が
＞ある軽微な誤差（不定性）で得られる
高さ評価はIUT以前の楕円曲線論でしょう
そもそも楕円曲線論 分かってますか？
＞IUTの変換で圏論的手法を使い、楕円曲線もどきがフロベニオイド圏？になる
＞それに、（絶対）ガロア理論を適用して、
＞（絶対）ガロア群の遠アーベル理論で、
＞楕円曲線の数体との対応がつく みたいな
わけもわからず喋っても、
数学にはならないし数学は理解できませんよ
残酷ですが、それが現実ですから
圏論が分かってない人に限って圏論といいたがるのも滑稽です
帰納極限と射影極限、直和と直積、の区別もつかない人が
何をいっても無意味というものですよ
204:１３２人目の素数さん
22/11/27 08:36:27.18 3pqSuWQI.net
>>181-183
＞上記は、個人的妄想ですが
あなたの知識が１９６０年代で終わってることだけはよくわかりました
失礼ですがおいくつですか？８０代？
＞“7 = 49”や一種の 「同義反復的解決」に見える部分を、厚く解説する必要あり
ただの誤りでしょう
当人は恥ずかしくて説明できないようですが
いずれほかの誰かが指摘して、望月新一を埋葬してくれると思いますね
あと、蛇足ですが
＞中島啓IMU総裁が何か考えて、「IUTの理解と普及」の差配をする
とか、なんか中島啓氏に勝手に期待してるようですが、
専門外の人が、なぜ「以前同じRIMSに居た」というだけで
望月新一個人のためだけに何かをする義務が発生するのか
まったく理解できませんね そんな義務ないし実際何もできないでしょう
＞あと、若手が頑張って欲しい
個人的には、星も南出も山下剛ですらも、
望月新一の勝手な行動の犠牲者だと思ってますが
＞サッカーのドイツ戦と同じなんだよね。ちゃんと勝利を挙げてくれ
数学はスポーツの試合ではありません
勝利？失礼ですが脳を梅毒に冒されてますか？それともAIDS？
205:１３２人目の素数さん
22/11/27 08:44:05.80 3pqSuWQI.net
>>181-183
”radical simplifications”に文句をつけてるようですが
そもそも望月新一のやってることが論理的にわけわからんので
バッサリ割愛された結果が”radical simplifications”なので、
自分のやってることが論理的に整合していることを説明する義務は
当然ながら望月新一一人にあります
IUTT論文は望月新一個人の論文なので星や南出が口出しする義務もありません
山下剛？いきなり呼ばれたってなにもできないでしょうな
彼も内心こんなはずじゃなかったと後悔してることでしょう 同情します
今IUTTに全賭けするのは、統一協会に全財産を寄進するのとおなじく
完全な狂気の行
206:為であると、断言しましょう
207:１３２人目の素数さん
22/11/27 09:07:45.99 sb8QiqJm.net
学会賞を取った時から胡散臭い奴と思っていた
208:１３２人目の素数さん
22/11/27 09:23:15.20 zRSM0dm/.net
>>184-188
これはこれは
数学板で有名な
数学落ちこぼれの狂犬さん
誰彼構わ噛みつき吠えまくることで有名ですよｗｗｗ
>別スレからの亡命 ご苦労様
亡命でもなんでもない
ここは、なんでもありの５ｃｈですからｗ
さて、
１）>>IUT理論は正しいと思うが
>根拠は？
・根拠は、査読が終わり出版されたこと（IUT本体及び5人論文の）
・さらに、IUTに対する数学的な反論はショルツェ氏のＳＳ文書のみ>>153
（ＳＳ文書以外は、新しい用語が多すぎて、読めないという人が多数いるが、数学的反論ではない
（一方、読めた・読んだという人も多数いる））
２）> 望月新一は自分でも証明できていないと思ってるんでしょう
>しかしそれを認めたくない だから解説抜きで「読め！」の一点張り
望月氏は、シンポジウムで彼なりの説明をしている
（勿論、IUTを理解している別の人たちも、シンポジウムでIUTについて説明をしているｗ）
３）> 某スレでどなたかも指摘されてましたが、番号付けが奇妙ですね
> いったい何の意味があるのか、一度も説明がありませんが
番号付けは、自分が後で引用するときに、
過去レスのこの番号に書いたと明示するための便宜のためですｗ
> それは、Knuthレベルですな
> Knuthレベルなら立派じゃん、というかもしれません
> 私がいいたいのは「全然ナイーブじゃん」ということです
意味分からんｗ ここは数学板なのであって、プログラム板ではないしょうよｗ
なおKnuth氏は、数学屋なら、TEX (TeX) の開発者と言えば分かるだろう cf URLﾘﾝｸ(ja.wikipedia.org)
>DijkstraとかHoareとか、御存知ですか？
>ホーア論理
Dijkstra、ホーア論理知っている。Hoare知らなかったが、今知ったｗ それがどうかしましたか？ｗｗｗ
つづく
209:１３２人目の素数さん
22/11/27 09:24:06.18 zRSM0dm/.net
つづき
４）> いまだにフローチャートなんていってる人は
>頭の中が１９６０年代のままなんでしょうか？
違うと思うよ。フローチャートは、いまでも有用だよ
フローチャートも詳細版と概略版を使い分ければ、良い
なお、いまIUTに求められているのは、あるレベル以上のプロ数学者がIUTの全体の流れが把握できる概略版だろう
そもそも、おっさんの批判は、「おれプログラムこれだけ詳しい」というハナタカ自慢でしょｗ アホじゃんｗｗ
> いわゆるフローチャートは構造化以前のものです
> 構造化以降もっと進化されたものがあります
批判が全く的外れ
いま問題にしているのは、IUTの構成ロジックをどう概略図として視覚化して表すかだ
おっさんが言っているのは、コンピュータプログラムの進化の話でしょ？ アホじゃんｗ
５）> 圏論が分かってない人に限って圏論といいたがるのも滑稽です
批判が全く的外れｗ
数学落ちこぼれのヤクザが、必死に因縁つけてくるんだねｗ アホ丸出しｗ
圏論を使ったと、望月氏自身が言っていることよ（下記百回音読してねｗｗｗ）
(参考)
URLﾘﾝｸ(ja.wikipedia.org)
宇宙際タイヒミュラー理論
、遠アーベル幾何などを拡大した圏の宇宙際 (IU) 幾何を構想した数学理論である[2]。望月によれば、自身が2000年代に開発した、p進タイヒミュラー理論、楕円曲線のホッジ・アラケロフ理論、および、数論的log Scheme圏論的表示の構成等に続いた、いわば「楕円曲線を備えた数体のタイヒミュラー理論の算術版」
(引用終り)
以上
210:１３２人目の素数さん
22/11/27 09:34:07.75 sb8QiqJm.net
圏論を知らなくても
望月氏が圏論を使ったということを事実として述べることは可能
望月論文に傷があったとしても
望月論文は正式の手続きを経て専門誌に掲載されたということを
事実として述べることは完全に正当
211:１３２人目の素数さん
22/11/27 09:37:25.72 zRSM0dm/.net
>>189-190
>＞中島啓IMU総裁が何か考えて、「IUTの理解と普及」の差配をする
> とか、なんか中島啓氏に勝手に期待してるようですが、
中島啓IMU総裁の課題の一つに、IUTの処理があると思っています
かれは、次のICMで、IUTを入れると思うよ。遠アーベル理論の一部になるのか、あるいはIUTの中で遠アーベルを扱うのかは知らないが
>そもそも望月新一のやってることが論理的にわけわからんので
>バッサリ割愛された結果が”radical simplifications”なので、
>自分のやってることが論理的に整合していることを説明する義務は
>当然ながら望月新一一人にあります
義務？ ない�
212:ﾈい あるはずがないｗ 例えば 論理的にわけわからん ↓ バッサリ割愛された結果が”radical simplifications”なので ↓ 自分のやってることが論理的に整合していることを説明する義務 もしこれで、あなた（当然かつ明白にIUTの理解能力の無い人）が ”radical simplifications”で、因縁つけたら？ 相手（望月氏）に義務が発生する？ アホでしょ！ その議論はｗｗ
213:１３２人目の素数さん
22/11/27 09:40:46.23 sb8QiqJm.net
>>195
>>中島啓IMU総裁の課題の一つに、IUTの処理があると思っています
>>かれは、次のICMで、IUTを入れると思うよ。
ソースは？
214:１３２人目の素数さん
22/11/27 09:41:25.00 zRSM0dm/.net
>>194
>望月論文に傷があったとしても
>望月論文は正式の手続きを経て専門誌に掲載されたということを
>事実として述べることは完全に正当
ありがとう
同意です
”望月論文の傷”さがし
もっと広く、望月論文の拡張や一般化や応用
それをするのが、数学者の仕事ですね
215:１３２人目の素数さん
22/11/27 09:57:39.35 3pqSuWQI.net
>>192-193
まあまあ、そうコーフンしないでｗ
さて
＞・根拠は、査読が終わり出版されたこと（IUT本体及び5人論文の）
他人まかせってことですね
ところで認知バイアスって知ってますか？
URLﾘﾝｸ(ja.wikipedia.org)
「都合のいい情報を好み逆を嫌う傾向」はその典型ですね
＞・さらに、IUTに対する数学的な反論はショルツェ氏のＳＳ文書のみ
あれがピンポイントでIUTの問題的を指摘してますからね
他は要らんでしょう
＞一方、読めた・読んだという人も多数いる
誰ですか？具体的に名前を挙げてくれませんか？
まあ、無理でしょう あなたの心の中の架空の人物の名前を言われてもわかりませんから
＞望月氏は、シンポジウムで彼なりの説明をしている
誰も理解できてませんがね
＞番号付けは、自分が後で引用するときに、
＞過去レスのこの番号に書いたと明示するための便宜のためです
いままで一度でもそのような形で明示してましたっけ？
個人的にはあなたの文章は無駄に長いので
番号つけするより、番号の単位で一件にするべきだと思いますね
そうすれば、アンカーだけで特定できますから
もしかして、一度もそのアイデアを思いつかなかったんですか？
脳味噌・・・つかってます？
216:１３２人目の素数さん
22/11/27 10:03:42.43 3pqSuWQI.net
>>192-193
＞フローチャートは、いまでも有用だよ
＞フローチャートも詳細版と概略版を使い分ければ、良い
こういうこといってる人は、自分ではフローチャート一つも書いたことない
書いたことがあればそんなのんきなことはいえませんから
＞批判は、「おれプログラムこれだけ詳しい」というハナタカ自慢でしょ
自分の知らないことを他人がいうと、そうやってブチ切れる人は沢山いますが
だいたいそういう人は勉強嫌いで頭が悪いですね
まあ、知的な人はどんな形で知ってもそれが面白いことなら興味を持ちます
馬鹿な人はただ他人に自慢したいだけのためにわけもわからずコピペするので
他人が同じことやるとブチ切れますね 哀れなもんです
＞いま問題にしているのは、
＞IUTの構成ロジックをどう概略図として視覚化して表すかだ
そもそもIUTが分かってないのに「正しい」と言い切っちゃう
あなた自身の心が一番の問題じゃないですか？
217:１３２人目の素数さん
22/11/27 10:08:10.60 3pqSuWQI.net
>>195
＞中島啓IMU総裁の課題の一つに、IUTの処理があると思っています
あなたが勝手にそう思いたがってるだけでしょう
＞かれは、次のICMで、IUTを入れると思うよ。
あなたが勝手にそう思いたがってるだけでしょう
＞遠アーベル理論の一部になるのか、
＞あるいはIUTの中で遠アーベルを扱うのかは知らないが
将来、系3.12は望月のパラドックスとして啓蒙書でとり上げられるかもしれませんね
さて本題
>>自分のやってることが論理的に整合していることを説明する義務は
>>当然ながら望月新一一人にあります
>義務？ ないない あるはずがないｗ
本気でいってます？
成果を他人に認めてもらいたいから論文書いたんでしょ？
だったら上記は義務ですよ
義務を負わないなら論文書いて発表したらダメですよ
チラシの裏にでも書いとけばいいんじゃないですか？マジで
218:１３２人目の素数さん
22/11/27 10:10:59.01 zRSM0dm/.net
>>196
>>>中島啓IMU総裁の課題の一つに、IUTの処理があると思っています
>>>かれは、次のICMで、IUTを入れると思うよ。
>ソースは？
これを説明すると長くなるが、書いてみるね
＜事実＞
１．IUTが数学界内で対立していることは事実で
この対立解消が、数学の発展に資すること
及び、この対立が一般マスコミの話題になっていることから
対外的にも、対立解消が是
（本来、数学ではこのような対立はまれ。論理の問題だから、普通は早期に解決されるもの。
10年ちかく論争して未決着。数学者の恥と思う人いるかもねｗ）
なので、この対立解消が、IMUの課題として考えて良いと思う
２，次�
219:ⅹMU総裁に、日本人の中島啓が選ばれたことは事実 （森重文→カルロス・ケニグ→中島啓。これに違和感を覚えるのが普通でしょ。なんで、飛び石だが日本人が続く？） ３．森重文氏は、2018年3月の望月 vs ショルツェ氏のRIMSでの集中討議をセットしたことは既知 また、結果としては、これは大失敗で、かえって事態をこじらせたと解せられる（ここ、多くの人は同意するだろう） つづく
220:１３２人目の素数さん
22/11/27 10:11:21.12 zRSM0dm/.net
>>201
つづき
＜個人的見解＞
１．まず、”森重文→カルロス・ケニグ→中島啓”について
下記で次期総裁を選ぶ実行委員会(EC)のメンバーに、前総裁の森重文が入っていること
だれが、中島啓を次期総裁押したのか？ 当然、森重文でしょう
２．では、なぜ中島啓氏？
勿論、中島啓氏が次期総裁にふさわしいことは当然として
加えて、上記の森重文氏の大失敗のリカバリーの意図もあったと思う
３．森氏以外の他の実行委員会(EC)のメンバーも、森氏の推薦に同意して、決まったこともこれは事実です
４．思うに、他のメンバーも、数学界内のIUTについての対立解消が必要との認識はあったのでは？
(参考)
URLﾘﾝｸ(ja.wikipedia.org)
国際数学連合（IMU: International Mathematical Union）
組織と実行委員会
国際数学連合は、連合の業務を行う実行委員会(EC: Executive Committee)によって運営されている[5]。ECは、総裁(President)1名、副総裁(Vice-Presidents)2名、書記(Secretary)1名、4年の任期で選出された特別会員(Members-at-Large)6名、および前総裁(Past President)で構成されている。ECは、全ての政策事項と、ICMプログラム委員会や各種賞委員会の委員の選出などの業務の責を負う。
2019-2022
アルゼンチン(実質は米国) カルロス・ケニグ（英語版）
(引用終り)
以上
221:１３２人目の素数さん
22/11/27 12:01:51.89 3pqSuWQI.net
>>201-202
妄想はチラシの裏に書いてくれｗ
だいたい、今は東大IPMUの人なんだが
URLﾘﾝｸ(www.ipmu.jp)
222:１３２人目の素数さん
22/11/27 12:25:06.44 zRSM0dm/.net
>>203
おまえに言ってないんだけど？ｗ
223:１３２人目の素数さん
22/11/27 15:11:26.02 YbNUAbXh.net
>>202
森とのしがらみが中島にはあるということは
事実だが
ソースと言えるほどのものではなかろう。
224:１３２人目の素数さん
22/11/27 15:19:18.91 3pqSuWQI.net
>>204
誰に対しても妄想をいうなよ ●違いｗ
225:１３２人目の素数さん
22/11/27 15:30:58.06 zRSM0dm/.net
>>205
>森とのしがらみが中島にはあるということは
>事実だが
>ソースと言えるほどのものではなかろう。
まあ、そだねー
”文春砲”未満であることは、認めるよｗ
(参考)
URLﾘﾝｸ(dic.pixiv.net)
ピクシブ百科事典
文春砲
ぶんしゅんほう
週刊文春によるスキャンダルスクープの通称。
目次[非表示]
1 概要
2 主な文春砲の犠牲者
2.1 政治関係者
2.2 芸能関係者
概要
もともとはAKB48系などのアイドルファンを中心に発生した用語。多数のメンバーや運営幹部がそのスクープにより吹っ飛んだインパクトからつけられた。後にアイドル以外の芸能人や政界・スポーツ界のスキャンダルのスクープでもこう呼ばれることが多い。
アイドルや芸能人の場合は降格やグループ脱退・契約解除・謹慎・芸能界引退、政治家やスポーツ選手の場合は辞職等仕事を失うダメージを受けた者も多い。
ただし、スクープ対象から法的措置を含めた反撃をされることも多く、敗訴して賠償を支払ったこともある。また知名度的に世間の関心が起きなかったり、キャラクターイメージ的に元々「ヨゴレキャラ」「清純路線では売っていない」ためファンからも「何を今更」とスルーされる事もある。
また本人や所属事務所が無視してうやむやになるなどして殆どダメージを受けなかった者達も多く、単なる交際報道だとジャンルによってはファンも対してショックを受けないどころかただのお祝いムードになることすらあり、こうした空振りを「空砲」と揶揄されることもある。
また、虚偽の情報の記載など文春側の取材や記事構成に不適切な点が多いと見なされて文春側が炎上する場合もあり「暴発」などとも揶揄される。
226:１３２人目の素数さん
22/11/27 16:24:33.66 3pqSuWQI.net
>>207
💩1、文春砲という言葉を覚える、の巻ｗ
227:１３２人目の素数さん
22/11/27 16:27:28.20 3pqSuWQI.net
1が中島啓の名前を持ち出したらネタ切れ
困ると権威にすがるのは最後期発展途上国日本の土民の惨めな光景
228:１３２人目の素数さん
22/11/27 18:45:14.25 3pqSuWQI.net
中島啓も💩1みたいな中卒ヤンキーに勝手に期待されていい迷惑だろう
229:１３２人目の素数さん
22/11/27 19:01:13.20 c9KxK2aO.net
このコンピュータは使われているLSI、OS、すべてに渡って多重のフェイルセーフ、
誤り防止の機能が万全に組み込まれているため、決してエラーを起こさないように
なっています。先ほど、完成しました。長年の努力の成果です。
うむ。それでは、さっそく実演をしてみてくれたまえ。
それでは、パワーオン。パワーオン。パワーオン。あれっ？電源が入らない？？
どうやら、エラー対策は万全なようだな。
230:１３２人目の素数さん
22/11/27 19:22:00.97 zRSM0dm/.net
>>211
>それでは、パワーオン。パワーオン。パワーオン。あれっ？電源が入らない？？
>どうやら、エラー対策は万全なようだな。
それ面白い
１）エラー対策は良いとして
しかし、プログラムを走らせて、実際に使ってみて出てくるエラーというかトラブルもある
２）数学も同じで、実際に使って走らせて分かるバグもあるだろうね
それでも、大きなバグがなければ、それはそれで
231:１３２人目の素数さん
22/11/27 19:22:31.49 zRSM0dm/.net
>>207 補足
１）中島啓総裁が、望月IUTを自分のテーマとして
国際的な数学者間の対立解消を、考える動機はいくつかある
２）>>201-202に書いたような場合がある
３）他に、森重文氏から、「中島くん、望月IUT頼むよ」と一言言えば済む話
４）森重文氏と中島啓総裁とは、当然一回以上の会話の機会があったろうし
これからも、あるはず
５）あとは、中島啓総裁がどう考えるか
だな
232:１３２人目の素数さん
22/11/27 19:25:03.53 YbNUAbXh.net
余り共感を覚えない憶測だな
233:１３２人目の素数さん
22/11/27 19:34:18.89 3pqSuWQI.net
>>213 自民党かよｗ
234:１３２人目の素数さん
22/11/27 19:36:54.61 3pqSuWQI.net
1に問題
1からnまでの数の長さnの順列を考える
これを隣同士の数を入れ替える操作だけで
1から順にnまで並べる順列に直すとする
Q. 最大何手で戻せるか証明つきで示せ
235:１３２人目の素数さん
22/11/27 19:40:53.82 zRSM0dm/.net
>>214
>余り共感を覚えない憶測だな
どうもありがとう
まあ、ここで議論しても仕方ない話だ
実際、中島啓総裁がどういう方針で
どういう施策をするか
見ていれば、
236:自然に分かってくる 私は、乞うご期待 そう思っている
237:１３２人目の素数さん
22/11/27 19:43:50.78 3pqSuWQI.net
>>217 馬鹿は期待しかしないｗ
216、答えろよ 馬鹿ｗ
238:１３２人目の素数さん
22/11/27 20:04:41.80 zRSM0dm/.net
URLﾘﾝｸ(nazology.net)
ナゾロジー
なぜアインシュタインは相対性理論でノーベル賞を受賞できなかったのか？ (3/3)
2022.11.26 SATURDAY
光量子仮説は、確かに理論物理学にとって重要な成果です。しかし、相対性理論の方がより画期的で目を引き、21世紀においても有名だと思われるでしょう。
ノーベル物理学賞の受賞者を選定するスウェーデン王立科学アカデミーにも、相対性理論によるアインシュタインの受賞を推薦する回答が多く寄せられました。
アインシュタインは1910年から1922年まで、ほぼ毎年受賞者としてノミネートされていたのです。
しかし、物理学界の中にはアインシュタインの成果に対し異論を唱える科学者もいました。そこで物理学賞委員会は1921年、二人のメンバーに説明を依頼しました。
その一人が、1911年に生理学・医学賞を受賞し、物理学賞受賞者にノミネートされたこともあるグルストランドです。その批判には誤りがあったことがのちに判明します。
1921年のノーベル賞受賞者決定は暗礁に乗り上げ、延期されました。翌年、アインシュタインは受賞者にノミネートされます。
グルストランドは再度、相対性理論を批判。一方、光電効果に関する説明は、賞賛に満ちたものでした。
委員会も光電効果に関する研究成果を認め、アインシュタイン受賞をめぐる対立はついに解消されました。
239:１３２人目の素数さん
22/11/27 20:05:37.72 zRSM0dm/.net
>>218
アホが
ほざいてろｗ
240:１３２人目の素数さん
22/11/27 20:09:35.14 zRSM0dm/.net
>>217
朝日新聞のインタビューも希望
URLﾘﾝｸ(www.nikkei.com)
国際数学連合の総裁に就く東大教授 中島啓氏
国またぐ交流が研究の礎
このヒト
2022年11月27日 2:00 [有料会員限定] （遠藤智之）日経
世界80カ国・地域以上の数学者が集まる国際数学連合（IMU）の総裁に2023年1月、就任する。任期は4年で、数学のノーベル賞ともいわれる「フィールズ賞」の選考委員会のトップも務める。
新しい図形を作る「幾何学的表現論」の研究などで多くの受賞歴を持つ。「研究の礎になった」と振り返るのは、1990年に京都で開かれた国際数学者会議だ。
自分の専門と離れた分野の発表に触れたことがきっかけで多くの成果につながった。「若い人にもそういう経験をしてもらいたい」と話す。
ロシアのウクライナ侵攻は学術界にも影を落とし、22年にロシアで開催予定だった4年に1度の国際数学者会議はオンライン開催になった。それでも「数学の発展に不可欠な国際交流は絶やさない」と心に決めている。
IMUは第1次大戦後の1920年に設立されたが、敗戦国のドイツを排除したことに異論が出て解散した過去がある。51年に再興した後、東西冷戦下で研究者の往来が難しくなった時期も交流を続けてきた。
「ロシアを排除しようというアカデミア（研究機関）もあるが、IMUは今後もそうした方針はとらない」。決意は固まっている。
241:１３２人目の素数さん
22/11/27 21:07:00.05 zRSM0dm/.net
>>182
(引用開始)
７）あと、若手が頑張って欲しい
サッカーのドイツ戦と同じなんだよね。ちゃんと勝利を挙げてくれ
望月は、もう地位も名誉もある。彼は（仙人みたいに）「なんとか賞？いらねー」というかもだが
南出やそれ以下の若手、RIMSや東工大にいる若手は、まだ地位や名誉いるよね。数学を職業として生業にするためには
若手がもっとハングリーに、「IUTの理解と普及」に向けた動きして良いと思うよ
ドイツ戦のように、貪欲に勝利を勝ち取ってほしい！
応援しています！
(引用終り)
日本対コスタリカ
敗戦
やれやれ
やっぱり勝たないとね
IUTも同じだよ
(参考)
URLﾘﾝｸ(www.yomiuri.co.jp)
日本対コスタリカ【速報】クリアミスから失点、痛い黒星…後半攻めまくるもナバスに防がれる
20:52
サッカーワールドカップ
日本代表・ワールドカップ
コスタリカ代表・ワールドカップ
サッカーのＦＩＦＡワールドカップ（Ｗ杯）カタール大会は２７日、グループリーグの第２戦が行われ、Ｅ組の 日本代表 （世界ランキング２４位）は、 コスタリカ代表 （同３１位）に０－１で敗れ、コスタリカとともに１勝１敗となっ…
242:１３２人目の素数さん
22/11/27 21:07:20.63 zRSM0dm/.net
>>182
(引用開始)
７）あと、若手が頑張って欲しい
サッカーのドイツ戦と同じなんだよね。ちゃんと勝利を挙げてくれ
望月は、もう地位も名誉もある。彼は（仙人みたいに）「なんとか賞？いらねー」というかもだが
南出やそれ以下の若手、RIMSや東工大にいる若手は、まだ地位や名誉いるよね。数学を職業として生業にするためには
若手がもっとハングリーに、「IUTの理解と普及」に向けた動きして良いと思うよ
ドイツ戦のように、貪欲に勝利を勝ち取ってほしい！
応援しています！
(引用終り)
日本対コスタリカ
敗戦
やれやれ
やっぱり勝たないとね
IUTも同じだよ
(参考)
URLﾘﾝｸ(www.yomiuri.co.jp)
日本対コスタリカ【速報】クリアミスから失点、痛い黒星…後半攻めまくるもナバスに防がれる
20:52
サッカーワールドカップ
日本代表・ワールドカップ
コスタリカ代表・ワールドカップ
サッカーのＦＩＦＡワールドカップ（Ｗ杯）カタール大会は２７日、グループリーグの第２戦が行われ、Ｅ組の 日本代表 （世界ランキング２４位）は、 コスタリカ代表 （同３１位）に０－１で敗れ、コスタリカとともに１勝１敗となっ…
243:１３２人目の素数さん
22/11/27 21:11:38.62 zRSM0dm/.net
あら連投になったかｗ
書込み失敗と出たから
再度書いたんだが
まあ、ともかく
IUTがんばれよ
244:１３２人目の素数さん
22/11/28 08:28:33.86 uXOIRXLP.net
>>222
>敗戦 やれやれ やっぱり勝たないとね
↓に書けよｗ
日本代表サッカー板
URLﾘﾝｸ(mevius.5ch.net)
245:１３２人目の素数さん
22/11/28 18:44:53.45 uOaPOR++.net
>>183
本当にお前は浅慮かつ望月贔屓だな｡
√√16を2と書き換えるのも radical simplifications だ｡
よくもまぁ何が外道なのか本当に確認したわけでも無く侮辱罪レスしまくれるな｡
数学板三大引きこもり
・このスレの>>1レス投稿者の集合A
・高木
・旧コテ「学問」「バカボンパパ」
246:１３２人目の素数さん
22/11/28 22:55:19.25 Kej7nTOW.net
>>226
>√√16を2と書き換えるのも radical simplifications だ｡
ショルツェ氏のデタラメ radical simplificationsと
√√16＝2 とは全く別ものだろ？ｗ
話は逆で
ショルツェのradical simplifications ＝ 望月IUT
この等式をショルツェ氏が証明しないかぎり
デタラメのそしりは免れまいｗ
>よくもまぁ何が外道なのか本当に確認したわけでも無く
上記の通りだよ
１）数学は厳密な論理で成り立つもの
文系のような類推解釈は、学生への講義ならともかく
証明の成否の議論において
”おれさま radical simplifications したら矛盾→IUT不成立”
こういう論法は、数学では基本は御法度だ
２）もし、上記を数学的な厳密な議論にしたいならば
”おれさま radical simplifications したら矛盾→IUT不成立”
↓
”元のIUTでも矛盾”（ここで数学的に厳密な論証を行うべし）
↓
”IUT不成立”とすべき。
ここまでやらないと、真っ当な数学の議論ではない！
（文系のディベートと類似の噴飯議論ですよ）
247:１３２人目の素数さん
22/11/28 23:51:45.77 EOM96xAY.net
Theory of Relativety
だった。つまり相対性「理論」である。
元来、ノーベル賞は物理学の場合には実験物理に対して与えられる賞であって、
理論だけで実証性がないとかのような数学と変わらないような内容については
出ない性格のものだったのだ（それは後の時代には変化する）。
湯川秀樹の中間子論も「論」であって、証明や実験事実に基づいた中間子の
存在証明ではなかったので、授賞はずっと後になる。パウリは、
素粒子をでっち上げて増やすというそんな考えは安易であり、気に入らない
というような嫌みを述べてたぐらいだし。
248:１３２人目の素数さん
2022/11/29(�
249:ﾎ) 00:12:14.18 ID:0njE1WcS.net
250:１３２人目の素数さん
22/11/29 06:40:22.83 EuVmTTh6.net
>>229
誤 ニュートン以来の絶対空間を否定した
正 ニュートン以来の絶対同時を否定した
ニュートンが否定したのは絶対静止（絶対同位置）
まあ、絶対同時を否定すれば空間を否定したことになるがね
（「相対空間」という言葉は空間を肯定したことにはならない）
251:１３２人目の素数さん
22/11/29 08:29:22.37 0njE1WcS.net
>>230
絶対空間で合っているよ
というか、絶対時間もありだが
絶対空間という用語の方が、より知られているよ
URLﾘﾝｸ(kotobank.jp)
コトバンク
絶対空間（読み）ぜったいくうかん
日本大百科全書(ニッポニカ)「絶対空間」の解説 ［田中 一］
絶対空間
ぜったいくうかん
ニュートンの運動の法則は慣性系という座標系でのみ成り立つが、このように基本法則が成り立つ不変、無限、等質な空間のことを絶対空間という。太陽に固定された（静止した）座標系は近似的には慣性系であるが厳密にはそうでない。ニュートンは「仮説をつくらず」という自らの主張に反して、特定の物体によらない絶対的な空間を設定してこの空間で運動の法則が成り立つとした。マクスウェルの電磁場の方程式が電磁波の存在を予見したことはよく知られているが、電磁波の媒体として導入されたエーテルが電磁法則の絶対空間と考えられたことがあった。一般相対性理論によれば運動法則には広い相対性が成り立ち、任意の加速度をもつ座標系からみても運動法則は同じ形式をもつ。この立場からすれば、力学において絶対空間の概念は必要とされない。空間に絶対的に静止していると考える絶対静止系が考えられないのもいうまでもない。
URLﾘﾝｸ(ja.wikipedia.org)
絶対時間と絶対空間
絶対時間（ぜったいじかん、英: absolute time ）と絶対空間（ぜったいくうかん、英: absolute space ）はアイザック・ニュートンが『自然哲学の数学的諸原理』（Philos
252:ophia Naturalis Principia Mathematica, 1687年刊）で初めて導入した概念で、古典力学が発展するための理論的基盤となった[1]。ニュートンによれば、絶対時間と絶対空間はそれぞれ何物にも依存しない客観的実在の一部である[2]。
253:１３２人目の素数さん
22/11/29 09:49:35.27 4a/LQM96.net
>>231
あのさ、辞書の文章じゃなく
ガリレイ変換とローレンツ変換の式
読もうよ
式、読めないの
じゃ、数学は無理だよ 悪いけど
254:１３２人目の素数さん
22/11/29 11:16:23.97 Q3sSo2OE.net
IUTTは数学の素領域理論
255:１３２人目の素数さん
22/11/29 11:31:41.77 4a/LQM96.net
>>233
スピンネットワークみたいな？
256:１３２人目の素数さん
22/11/29 11:53:57.18 Fea49eUi.net
素領域というのは湯川先生だった？
257:１３２人目の素数さん
22/11/29 16:38:35.62 5teOe0vX.net
>>230 補足
絶対空間という用語の方が圧倒的に有名である
カントの哲学で論じられているからである（下記）
（参考）
URLﾘﾝｸ(www.jstage.jst.go.jp)
Vol.13No.4科学基礎論研究
カントと絶対空間
1768年論文をめぐって
中島義道 東京大学大学院 修士課程 修了
カントは1768年の論文『空間における方位の第1根拠
について』において,ニュートンの絶対空間を証明しよ
うとしており,それよりわずか2年後に書かれた1770
年の論文r可感界と可想界との形式と原理』において,
ニュートンの絶対空間を否定している。この間の急激
な変化は,諸家によってこれまで様々に論じられてきた
が,結局論点は1768年論文のうちに1770年論文の萌芽が
どの程度認められるかにかかっている。これを色濃く認
める.4.RiehlやH.Cohen等は,1768年論文は直接1770
年論文に発展したと主張しうるわけであるが,これを認
めないE.CbssirerやB.Erdmanm等は,この2年間
のカントの生活歴にライプニッツ哲学の再吸収という事
件を想定する。しかし後者はあくまで臆測の域を出ない
ものである。しかも1768年論文そのものの解釈とこの臆
測とは一応別のものであり,この臆測によって逆に1768
年論文のうちに1770年論文の萌芽が全く認められなくな
るわけではない。
*この問題に関する手際よい要約としては,理想社刊
『カント全集第3巻』の解説を参照。かのM.Jammer
の名著Conceptsofspaceはカントに触れていな
い。またKmtstntmおよびIsisには,この問題
を扱った論文は皆無である。
本稿では,A.Rtiehl等の立場を継承し,特に1768年
論文のうちに見られる身体の思想が,1770年論文におけ
る「主観の形式」へとそのまま変身しうるものであった
ことを示す。「絶対空間」と身体との極限的な妥協点が
「主観の形式」であり,これこそがカントによるニュート
ン空間論の独自の摂取に他ならないのではあるまいか。
(引用終り)
以上
258:１３２人目の素数さん
22/11/29 16:49:22.30 5teOe0vX.net
>>235
>素領域というのは湯川先生だった？
そうですね
素領域とは
量子力学が、点粒子を扱うと、その計算が発散して
「繰り込み理論」を必要とする
それに不満で、空間を点でなく、拡がりを持つ素領域と考えようしたみたいな
数学でも、点でなくε近傍(or 開集合)をベースに考えようみたいな
いまの超弦理論（弦は点でなく1次元の拡がりを持つ）を先取りした思想だったかも
（参考）
URLﾘﾝｸ(kotobank.jp)
259:%A0%E9%A0%98%E5%9F%9F%E7%90%86%E8%AB%96-90431 素領域理論（読み）そりょういきりろん（英語表記）theory of elementary domain ブリタニカ国際大百科事典 小項目事典「素領域理論」の解説 素領域理論 そりょういきりろん theory of elementary domain 四次元時空を分割不可能な最小領域 (素領域という) に区分し，エネルギーが加わって励起された素領域が素粒子であるとみなして，素領域間のエネルギーの授受によって素粒子の生成・消滅などを論じようとした試論。 1966年湯川秀樹により提唱された。 https://ja.wikipedia.org/wiki/%E7%B9%B0%E3%82%8A%E8%BE%BC%E3%81%BF 繰り込み（くりこみ、アメリカ英語：Renormalization イギリス等英語及びフランス語：Renormalisation ）とは、場の量子論で使われる、計算結果が無限大に発散してしまうのを防ぐ数学的な技法であり、同時に場の量子論が満たすべき最重要な原理のひとつでもある。 くりこみにより、場の量子論を電磁相互作用に適用した量子電磁力学が完成した。場の量子論にくりこみを用いる方法は、以後の量子色力学およびワインバーグ・サラム理論を構築する際の規範となる。
260:１３２人目の素数さん
22/11/29 17:44:09.03 xxTXnKMF.net
>>236
>カントの哲学
なんだコイツ、文学部哲学科卒の数痴数盲かw
261:１３２人目の素数さん
22/11/29 17:56:56.01 Fea49eUi.net
>>238
>>なんだコイツ、文学部哲学科卒の数痴数盲かw
文学部哲学科卒以外の者は
カントの哲学が有名だと言うことを
禁じられているのか？
262:１３２人目の素数さん
22/11/29 20:38:37.84 EuVmTTh6.net
>>239
いまどき「カントがー」とかいうのが
文学部哲学科的アナクロニズム
ってことだろ
263:１３２人目の素数さん
22/11/29 21:58:15.75 yL/XROQY.net
>>240
コピペだから
文学も哲学もないだろう
264:１３２人目の素数さん
22/11/29 23:09:13.15 0njE1WcS.net
>>241
>コピペだから
>文学も哲学もないだろう
同意
というか、仰る通りです
カントなど一冊も読んだことはないが
しかし、カントの名言「わが頭上の星辰をちりばめた天空と、わが内なる道徳法則」下記
ここに、カントが当時最先端のニュートン物理に興味をもって研究したことが分かる
ニュートンの絶対空間について、哲学的視点で論じたことも、有名な話
URLﾘﾝｸ(christianpress.jp)
クリプレ（クリスチャンプレス）
断片から見た世界連載・コラム
【哲学名言】断片から見た世界 カントの言葉
philo1985 東京大学博士課程で学んだのち、キリスト者として哲学に取り組んでいる。現在は、主にブログ「イデアの昼と夜」とTwitterで活動を行っている。2021.07.19
今回の哲学名言は、カントの主著の一つである『実践理性批判』から、道徳法則に関する有名な一節を取り上げてみることにしましょう。
わたしたちが頻繁に、そして長く熟考すればするほどに、
ますます新たな賛嘆と畏敬の念が心を満たす二つのものがある。
それはわが頭上の星辰をちりばめた天空と、わが内なる道徳法則である。
カント
つづく
265:１３２人目の素数さん
22/11/29 23:09:58.90 0njE1WcS.net
>>242
つづき
この一節自体、倫理学の名言としてはこれを引いておけばまず間違いはないというくらいによく知られており、高校生の倫理の教科書などでもひんぱんに引用されているものです……が、率直に言って、現代を生きている私たちが、この一節を理解するにあたって小さからぬ困難を覚えることは否定できません。というのも、私たち現代人は、カントが生きてい�
266:ｽ、敬虔主義的な雰囲気が濃厚に漂う十八世紀ドイツの社会よりも、道徳的に見て少しばかり奔放な社会を生きていると言わざるをえないからです。 少しばかり、というのはきわめて控えめな言い方であって、実際には、彼らから見たらほとんど無法状態にも近い自由を謳歌してしまっている、と言うべきかもしれません。現代の大人たちは、確かに純愛ものの連続ドラマに涙を流すことも時にはありますが、基本的には、不倫と殺人を題材にしたフィクションの世界にどっぷりと浸かっています。若者たちは、連日連夜の合同コンパにひたすら明け暮れながら、それでも次のコンパは果たしていつだろうと、あくまでも貪欲に求め続けています。今日、道徳的に見て「安全」であるのはもはや、『とっとこハム太郎』に目を輝かせている子供たちくらいのものであると言えるのかもしれません。 (引用終り) 以上
267:１３２人目の素数さん
22/11/30 02:38:26.11 lUk+rUEf.net
カントの時空間の理論が一世を風靡していたために、
論争に巻き込まれるのを恐れたガウスは、自分の発見した
非ユークリッド幾何学を公表せず秘匿していて、
友人にさわりの部分の内容を手紙で漏らしているだけである。
ユークリッドの幾何学こそが数学の王様分野だった時代だから、
それに弓を射るように世間から見える言動を慎まないと、あいつは
インチキ数学者だとかいわれて、非難の声が高まれば、パトロンが手を退いたり
しかねないことを警戒したのだと思われる。
アインシュタインの特殊相対性理論も、当時無理解の人間に
散々に糾弾されたことを思えば、賢明であったというべきだろう。
268:１３２人目の素数さん
22/11/30 05:53:13.46 ke8ZZyTl.net
>>244
そういう精神のヤツが国に殺される
269:１３２人目の素数さん
22/11/30 06:34:41.76 ke8ZZyTl.net
カントは哲学者ということになってるが、実際やってることは宗教家である
宗教家というのは「我思う、ゆえに我正しい」と唱える●違いのことである
ドイツ観念論なんてのは、ただの宗教に過ぎない
文学部哲学科は、新たな神学部に過ぎないのであるｗｗｗ
270:１３２人目の素数さん
22/11/30 06:37:58.12 ke8ZZyTl.net
>>244
＞パトロン
ブラウンシュヴァイク公ね
ちなみにカール・ヴィルヘルム・フェルディナントも
息子のフリードリヒ・ヴィルヘルムもナポレオン戦争で死んだ
そして、その息子の代でブラウンシュヴァイク公家は断絶した
271:１３２人目の素数さん
22/11/30 06:41:54.89 ke8ZZyTl.net
カントは所詮18世紀の人である
ガウスは19世紀の人である
50年の差は絶大
272:１３２人目の素数さん
22/11/30 06:43:20.36 ke8ZZyTl.net
絶対空間が嘘であるように、道徳法則も所詮嘘である
人は所詮おサルさんｗｗｗ
273:１３２人目の素数さん
22/11/30 06:43:40.41 ke8ZZyTl.net
ということで
1は死ね！ｗ
274:１３２人目の素数さん
22/11/30 07:28:28.29 +1taHnfC.net
>>250
>新たな賛嘆と畏敬の念が心を満たす二つのものがある。
>>それはわが頭上の星辰をちりばめた天空と、わが内なる道徳法則である。
この言葉を発した人は死んだが
この言葉がウソになったわけではない
275:１３２人目の素数さん
22/11/30 08:13:52.06 lvNLqkJH.net
>>251
レスありがとう
スレ主です
＞この言葉がウソになったわけではない
なるほど
そうだね
276:１３２人目の素数さん
22/11/30 08:21:43.31 lvNLqkJH.net
>>244
>カントの時空間の理論が一世を風靡していたために、
>論争に巻き込まれるのを恐れたガウスは、自分の発見した
>非ユークリッド幾何学を公表せず秘匿していて、
>友人にさわりの部分の内容を手紙で漏らしているだけである。
> アインシュタインの特殊相対性理論も、当時無理解の人間に
>散々に糾弾されたことを思えば、賢明であったというべきだろう。
なるほど
そうだったんだ
アインシュタインの相対性理論が
如何に革新的なのかで
カントの絶対空間論は知っていたが
ガウスの話とか、
アインシュタインが糾弾されたことは
あまり知らなかった
なお、下記のマッハの話は有名です
(参考)
URLﾘﾝｸ(ja.wikipedia.org)
277:F エルンスト・ヴァルトフリート・ヨーゼフ・ヴェンツェル・マッハ（Ernst Waldfried Josef Wenzel Mach、 1838年2月18日 - 1916年2月19日）は、オーストリアの物理学者、科学史家、哲学者。日本ではマッハ数の由来でも知られる。 科学史・科学哲学 科学史の分野では『力学の発達』（1883年）、『熱学の諸原理』（1896年）、『物理光学の諸原理』（1921年）が科学史三部作と呼ばれる。 『力学の発達』1883年では、当時の物理学界を支配していた力学的自然観を批判した。 ニュートンによる絶対時間、絶対空間などの基本概念には、「形而上学的な要素が入り込んでいる」として批判した。この考え方はアインシュタインに大きな影響を与え、特殊相対性理論の構築への道を開いた。そしてマッハの原理を提唱した。このマッハの原理は「物体の慣性力は、全宇宙に存在する他の物質との相互作用によって生じる」とするものである。この原理は一般相対性理論の構築に貢献することになった。マッハは「皆さん、はたしてこの世に《絶対》などというのはあるのでしょうか？」と指摘したことがある。なお、マッハ自身は相対論に対しては、生涯否定的な立場をとった。
278:１３２人目の素数さん
22/11/30 09:10:35.28 BvfjwubP.net
>>253
中卒は黙ろうな
279:１３２人目の素数さん
22/11/30 11:42:31.68 lXwCP6yL.net
>>254
えー、えー、
あなたは某数学科修士だったかな
えらいえらい
思うに、数学科からコンピューターのプログラマーになったのだろうね
聞くところ
コンピュータープログラムの世界では
システムエンジニア（対人交渉と全体設計）とプログラマー（力仕事）*）
に二分されるそうだね
対人交渉スキルがあると思えないから
プログラマー（力仕事）どまりかな？ｗ（＾＾；
プログラマー（力仕事）も、納期が大変な仕事で
納期が遅れ遅れになるから、最後は徹夜みたいになるし
納期に追いまくられて、精神にダメージを負う人も・・
統合失調症の薬を飲んでいるんだって？
ご苦労様です
某数学科修士のころは、もうちょっと数学できたんだろうね
いま、その片鱗も見えない？
（いや、たまにだがｗ、
少し見えるときもあるかもだがｗｗ）
まあ、また～りしていきなよ（＾＾
（参考）
*）プログラマー（力仕事）について
いまや古典だが、下記などご参照
URLﾘﾝｸ(ja.wikipedia.org)
『人月の神話』（にんげつのしんわ、英: The Mythical Man-Month: Essays on Software Engineering）は、フレデリック・ブルックスが著したソフトウェア工学とソフトウェアプロジェクト管理の書籍である。
概要
ブルックスの考察は、自身がIBM で OS/360 というオペレーティングシステムの開発に携わったときの失敗に基づいている。 プロジェクト管理者がソフトウェアプロジェクト管理において、繰り返し何度もこのような誤りを犯すという傾向があるため、ブルックスは自分の本について、次のような皮肉を述べている。
この本は「ソフトウェア工学の聖書」と呼ばれている。なぜなら、誰もがこの本を読んでいるが、誰もこの本で述べていることを実践しないからである。
最初に刊行されたのは1975年である。1995年に20周年記念版として再刊された。
(引用終り)
以上
280:１３２人目の素数さん
22/11/30 12:00:22.41 lXwCP6yL.net
>>255 補足
＞IBM で OS/360 というオペレーティングシステムの開発に
OS/360 は、オペレーティングシステムの最初期だね
下記に、メインフレームのカウントがないね・・ｗ
いまや普通のサーバーで、ある程度は代用できるのかも
残っているのは、日本では銀行系くらいかな？
（参考）
URLﾘﾝｸ(ja.wikipedia.org)
オペレーティングシステム
コンピュータのタイプごとの主なオペレーティングシステム
スマートフォンのOSおよびそのシェアは、2021年9月時点でAndroidが約72%、iOSが 約27%である[1]。Androidは広い意味でのLinuxの一種であり、Linuxのカーネルを一部改編し他のオープンソース・ソフトウェアを組み合わせたものである。
ノートPCやデスクトップPCのOSおよびそのシェアは、2021年時点でWindows 75.4%、macOS 15.93%、Chrome OS 2.59%、Linux 2.33%となっている[2]。macOSはFreeBSDを基にしたUNIX系のOSである。
スーパーコンピュータのOSは、2000年ころはUNIXが9割ほどを占めていたが、その後の10年間でそのほぼ全てがLinuxに置き換わり、2021年現在では世界のスーパーコンピュータのTOP500のほぼ100%がLinuxである[3]。
組み込みシステムでは組み込みオペレーティングシステムと呼ばれるOSを用いる。小規模な組み込みシステムのなかには明確なOSを内蔵していないものもあるので曖昧な面もあるが、組み込みOSを搭載しているものに関しては2019年時点でのシェアでTRON（トロン）系がおよそ60%であり、24年連続トップを占める[4]。TRON系のなかでもITRON（アイトロン）が最も普及している[4]。TRON以外では、次いでPOSIX系つまりUNIX系、Linux類などである[4]。米リナックスワークスのLynxOS（リンクスオーエス）、米ウィンドリバーのVxWorks（ヴイエックスワークスト）、米シンビアンのSymbian OS（シンビアン・オーエス）など。
「オペレーティングシステムの一覧」および「:en:Usage share of operating systems」も参照
281:１３２人目の素数さん
22/11/30 13:08:20.65 HnuqW6V8.net
>>255
匿名板で相手が誰だか特定しようとするのは
●違いのすること
特定されたくないなら癖を消すこと
まずコピペは止めるこったw
さて、あんたは生まれてから一度も
プログラム書いたことなさそうだね
会社では専ら口先三寸で誤魔化す営業畑かな
馬鹿の典型的な配属先だね（嘲）
で鬱病でドロップアウトかい
典型的な社畜の最期だな（憐）
『人月の神話』も『プログラミングの心理学』も読んだが
ああいうのは、文系向きの読み物だな。
どうせならグリースの『プログラミングの科学』とか読めよ。
ま、でも、対偶が理解できなくて高校中退した君には無理かw
282:１３２人目の素数さん
22/11/30 13:22:55.61 HnuqW6V8.net
>>257
グリースの『プログラミングの科学』は
論理が分かる程度のフツーの学生なら誰でも読める
別に超絶テクニック本とかではない
出てくる課題は当たり前のものばかり
しかしきっちり読んで理解すれば
プログラム検証について理解出来る
ただ日本語訳は訳者のこだわりで
訳さんでもいい言葉まで訳しているので
平成キッズには読み難いかもしれん
(プログラムを算譜と訳す等)
なお訳者は国粋主義者ではないw
283:１３２人目の素数さん
22/11/30 14:25:51.75 lXwCP6yL.net
>>257-258
>匿名板で相手が誰だか特定しようとするのは
>●違いのすること
>特定されたくないなら癖を消すこと
それ、自問自答かｗ
自分に言っているのか？ｗ
数学科オチコボレの猿石こと>>5
サイコパスのピエロさん
テンプレに、あんたのことは入れてあるよ
(余談だが、専ブラのJane使っているので、あんたの使う絵文字は化けて見えないんだｗｗｗ)
>>まずコピペは止めるこったw
よく誤解されれるが
検索して初めて知ったことをコピペしているみたく思われるが
だが、知っていることを検索してコピペしている
こうすれば、最初から自分で筆を起こすより
数倍早く言いたいことを投稿できるし
典拠があるので、説得力数倍
かつ、大学数学教授のPDFからのコピペに突進するバカもいて
それって、岩にぶつかっているが如し（そんなとこに突っ込んでも頭にコブ作るだけさｗｗｗ）
>さて、あんたは生まれてから一度も
>プログラム書いたことなさそうだね
プログラムは、簡単な自分用の数値計算プログラム程度で
業務用のプログラムは無いけど
余談だが、昔々”bit”という雑誌があって、愛読書だった
なので、門前の小僧状態だよ
なお、会社のメインフレームのシステム開発プロジェクトには参加したことがある
こっちは、クライアントで(SE（システムエンジニア）から見て)、だから、こっちの意見は尊重してくれたね
（”bit”誌を読んでたから、コンピュータ用語では困らなかったな。SEの話は、よく理解できた）
>グリースの『プログラミングの科学』
知らない。大した本では無い気がするけどｗｗ
（参考）
URLﾘﾝｸ(ja.wikipedia.org)
共立出版
雑誌
月刊「bit」 - 2001年4月号にて休刊
284:１３２人目の素数さん
22/11/30 14:42:16.89 lXwCP6yL.net
>>259
>>グリースの『プログラミングの科学』
>知らない。大した本では無い気がするけどｗｗ
グリースの『プログラミングの科学』
下記だね
1991年か。多分、もう内容が古いだろう
筧 捷彦 (翻訳)氏か
この人、”bit”誌にもいろいろ書いていた気がするな
”bit”誌は、
上はメインフレームやスパコンから、下はワークステーションやPCまで
コンピュータ関係の話題を幅広く取り上げていたと思う
（参考）
URLﾘﾝｸ(www.)<)
筧 捷彦（かけひ かつひこ、1945年（昭和20年）[1] - ）は、日本の計算機科学者。学位は工学修士。東京通信大学情報マネジメント学部教授。
経歴・人物
1970年（昭和45年）東京大学工学系大学院修了後、同大学工学部助手、立教大学理学部講師、同大学理学部助教授、早稲田大学理工学部教授、同大学基幹理工学部教授を経て2016年（平成28年）早稲田大学名誉教授となった[2]。
ほか、ACM-ICPC 日本ICPC Board 議長、パソコン甲子園プログラミング部門審査委員長、特定非営利活動法人情報オリンピック日本委員会理事長、公益財団法人情報科学国際交流財団理事長などを歴任した[2]。情報処理学会名誉会員[2]。2020年（令和2年）現在、東京通信大学情報マネジメント学部教授[3]。
285:１３２人目の素数さん
22/11/30 14:59:43.89 lXwCP6yL.net
>>260 補足
> 1970年（昭和45年）東京大学工学系大学院修了後、同大学工学部助手、立教大学理学部講師、同大学理学部助教授、
数学科オチコボレの猿石こと>>5
サイコパスのピエロさん
あんた、立教の数学科かい？
えらく東大の数学科に詳しかったし、
そもそも立教と東大の数学科と交流があったようだ（今でもと思うが）
上記のように、
立教と東大は結構人事交流がある
（というか立教の
286:アカデミックポストに東大出身者が多数いる） らしいから そう思ったのだが 立教の数学科出身で、 アカデミックポストをゲットしようとするならば なにか学会賞（若手奨励賞とか）でも取って 箔をつけないとね 多分難しい 学会賞（若手奨励賞とか）も よほど実力と運がないと、難しいだろうね あんた、東大受けたのかい？ 立教は、滑り止めかい？ で、不遇の身になって ５ｃｈの数学板でうさばらしか まあ、 また～りしていきなよｗｗ
287:１３２人目の素数さん
22/11/30 15:10:52.22 83lMDEZ7.net
>>259
>知っていることを検索してコピペしている
>こうすれば、最初から自分で筆を起こすより
>数倍早く言いたいことを投稿できるし
>典拠があるので、説得力数倍
言葉だけしか知らんから
検索結果をコピペして誤魔化すんだろw
大体見当違いだけどな
読まずにコピペしてるだろw
>プログラムは、簡単な自分用の数値計算プログラム程度
で、バグりまくり、とw
>会社のメインフレームのシステム開発プロジェクト
>には参加したことがある
完全に昭和の爺ィだなw
288:１３２人目の素数さん
22/11/30 15:20:38.71 83lMDEZ7.net
>>260
>>グリースの『プログラミングの科学』
>知らない。大した本では無い気がするけど
笑われるよw
>1991年か。多分、もう内容が古いだろう
原著は1981年 シュプリンガーの銀表紙な
>筧 捷彦 (翻訳)氏か
>この人、”bit”誌にもいろいろ書いていた気がするな
7bitsの前のコラムの執筆者の一人だよ
bit読者なら常識なw
ていうか、基本的な本で古いもクソもない
あんた、線形代数で佐武や斎藤正彦を古いって言っちゃう軽率馬鹿だろw
289:１３２人目の素数さん
22/11/30 15:25:15.58 83lMDEZ7.net
>>261
>あんた、立教の数学科かい？
違うけどなんでそう決めつけた？w
290:１３２人目の素数さん
22/11/30 15:34:45.21 83lMDEZ7.net
>>263
>もう内容が古いだろう
というか、今どきHoare logicなんて教えんらしい
Curry-Howard correspondenceとかのほうが
カッコイイもんな でもそれも前世紀かw
291:１３２人目の素数さん
22/11/30 15:51:49.91 LLmeCN5f.net
>>265
それにしても萩谷昌己氏ももう東大退官か(しみじみ)
292:１３２人目の素数さん
22/11/30 18:48:26.41 lXwCP6yL.net
>>266
>それにしても萩谷昌己氏ももう東大退官か(しみじみ)
萩谷昌己氏か
名前だけは、聞いたことがあるけど・・
Kyoto Common Lispか
なるほど
URLﾘﾝｸ(www.i.u-tokyo.ac.jp)
【延期のお知らせ】萩谷昌己特命教授最終講義2022.7.16（土）
2022/06/20?2022年3月31日に情報理工学系研究科（コンピュータ科学専攻）教授を退職した萩谷昌己特命教授（2022年4月1日より現職）の最終講義を以下の日程で実施
URLﾘﾝｸ(www.jstage.jst.go.jp)
コンピュータソフトウェア, Vol.37, No.2 (2020), pp.19?24. 2019 年 10 月 4 日受付.
トピックス
bitがあった頃の研究
萩谷昌己 東京大学情報理工学系研究科
1はじめに
本稿は，2019年の日本ソフトウェア科学会大会の
際に行われた，2018年度基礎研究賞の受賞講演に基
づいている．
bitは，1969年から2001年にかけて共立出版が刊
行を続けたコンピュータサイエンスに関する専門的
な商業雑誌である．創刊号は1969年3月号であり，
休刊号は2001年4月号である．休刊になってからも
う20年近く経つ．本稿のもとになった講演の背景に
は，bitのことを時々思い出してやらないといけない
という思いがあった．
一方，何だか付け足しのようであるが，基礎研究賞
をいただいた理由は，以下のようであった．
?処理系に関連する一連の研究
?KyotoCommonLisp[17][18]その他
?型付き言語に対する超循環インタプリタ[6]
?証明の一般化に関連する一連の研究
?高階型理論における一般化[4]
?高階単一化を用いた例によるプログラミングと証明[7]
URLﾘﾝｸ(ja.wikipedia.org)
Kyoto Common Lisp (KCL)は湯淺太一、萩谷昌己らによるCommon Lispの実装である。C言語で書かれ、主にUnix系OSで広く動作した。KCLはANSI Cへとコンパイルするのが特徴。
KCLの特筆すべき点は、Common Lisp仕様標準委員会の外部で、Common Lisp仕様に基づいてゼロから実装されたことである。
仕様のみに基きゼロから実装したKCLは、それまで気づかれなかったCommon Lisp仕様の多くの穴や間違い、暗黙の前提を露呈させた。
293:１３２人目の素数さん
22/11/30 18:49:15.39 lXwCP6yL.net
>>262
>>会社のメインフレームのシステム開発プロジェクト
>>には参加したことがある
> 完全に昭和の爺ィだなw
開発プロジェクトは、平成だったよ
そういうあんたも昭和生まれだったよねｗ
（遠山啓を読んだとか）
>>263
>>筧捷彦(翻訳)氏か
>>この人、”bit”誌にもいろいろ書いていた気がするな
> 7bitsの前のコラムの執筆者の一人だよ
7bitsか
あったね
その前？ あまり記憶に残っていない（＾＾；
> ていうか、基本的な本で古いもクソもない
> あんた、線形代数で佐武や斎藤正彦を古いって言っちゃう軽率馬鹿だろw
理系の本で「古い」はあるよ
というか、理系は原則最新の書物を読むべし！
その上で、古典も読めば良い
>>264
>>あんた、立教の数学科かい？
> 違うけどなんでそう決めつけた？w
ふふふ
その書き方
胡散臭いなｗｗｗ
(ゴマカシ？)
294:１３２人目の素数さん
22/11/30 19:38:37.92 ke8ZZyTl.net
なんか耄碌爺の１がメインフレームがーとか昔話してんな
死ねよｗ
295:１３２人目の素数さん
22/11/30 19:41:31.86 ke8ZZyTl.net
>>268
＞理系は原則最新の書物を読むべし！
はい馬鹿ｗ
微積分や線型代数で新しいもクソもない
昭和の耄碌爺はさっさと死ね
貴様の時代は終わったんだよｗｗｗ
296:１３２人目の素数さん
22/11/30 19:54:20.51 EywtAE6Q.net
特殊相対論やカント哲学までコピペ引用だなコイツ
そのうち中学数学までコピペ引用しだす積もりかコイツは
297:１３２人目の素数さん
22/11/30 20:01:36.25 ke8ZZyTl.net
>>272
馬鹿は文章が書けないｗ
298:１３２人目の素数さん
22/11/30 20:02:07.39 ke8ZZyTl.net
>>271
馬鹿は文章が書けないｗ
299:１３２人目の素数さん
22/11/30 20:24:25.51 lvNLqkJH.net
>>271
>特殊相対論やカント哲学までコピペ引用だなコイツ
>そのうち中学数学までコピペ引用しだす積もりかコイツは
へー
で？
今日そのIDで何を書いたの
下記必死チェカーもどき見ると、これだけみたいだね
だったら、何かこのスレに書いてみな
大口叩くならｗｗｗ
どうせ、ろくなこと書けないだろ！？
大口叩くやつって、大概そうなんだｗｗｗ
バカじゃね
アホじゃね
ｗｗｗ
(参考)
URLﾘﾝｸ(hissi.org)
必死チェカーもどき
トップページ > 数学 > 2022年11月30日 > EywtAE6Q
使用した名前一覧 書き込んだスレッド一覧
１３２人目の素数さん
純粋・応用数学・数学隣接分野（含むガロア理論）11
書き込みレス一覧
純粋・応用数学・数学隣接分野（含むガロア理論）11
271 ：１３２人目の素数さん[sage]：2022/11/30(水) 19:54:20.51 ID:EywtAE6Q
特殊相対論やカント哲学までコピペ引用だなコイツ
そのうち中学数学までコピペ引用しだす積もりかコイツは
300:１３２人目の素数さん
22/11/30 21:13:14.69 ke8ZZyTl.net
>>274
馬鹿はおまえじゃｗ
結局
時枝「箱入り無数目では、同値類の代表を使えば
確率99/100で、選んだ箱の中身を当てられる」
選ま「同値類の代表の選出は実行不能なので当てられない！」
まで退化した中卒ｗｗｗｗｗｗｗ
301:１３２人目の素数さん
22/11/30 21:21:03.58 ke8ZZyTl.net
1の戯言
ヴィタリ「R/Qから、代表を選べば非可測集合ができる」
選ま 「同値類の代表の選出は実行不能なので可測集合しか存在しない！」
ｷﾞｬﾊﾊﾊﾊﾊﾊ!!!
302:１３２人目の素数さん
22/11/30 22:51:16.84 lvNLqkJH.net
>>275-276
(引用開始)
時枝「箱入り無数目では、同値類の代表を使えば
確率99/100で、選んだ箱の中身を当てられる」
選ま「同値類の代表の選出は実行不能なので当てられない！」
まで退化した中卒ｗｗｗｗｗｗｗ
(引用終り)
ホイよ
スレタ�
303:C 箱入り無数目を語る部屋6 https://rio2016.5ch.net/test/read.cgi/math/1669635809/36 アホやなお前 いまだに、 何年も時枝（下記）の不成立が理解できないやつｗｗｗ https://rio2016.5ch.net/test/read.cgi/math/1669635809/1 （参考） 時枝問題（数学セミナー201511月号の記事） 「箱入り無数目」抜粋 純粋・応用数学（含むガロア理論）8 https://rio2016.5ch.net/test/read.cgi/math/1620904362/401 時枝問題（数学セミナー201511月号の記事） 「箱がたくさん，可算無限個ある.箱それぞれに，私が実数を入れる. どんな実数を入れるかはまったく自由，例えばn番目の箱にe^πを入れてもよいし，すべての箱にπを入れてもよい. もちろんでたらめだって構わない.そして箱をみな閉じる. 今度はあなたの番である.片端から箱を開けてゆき中の実数を覗いてよいが，一つの箱は開けずに閉じたまま残さねばならぬとしよう. どの箱を閉じたまま残すかはあなたが決めうる. 勝負のルールはこうだ. もし閉じた箱の中の実数をピタリと言い当てたら，あなたの勝ち. さもなくば負け. 勝つ戦略はあるでしょうか?」
304:１３２人目の素数さん
22/11/30 22:51:54.54 lvNLqkJH.net
これ面白い
URLﾘﾝｸ(www.youtube.com)
#個別指導塾CASTDICE
【神々の世界】 余裕で東大に合格する天才たちの実態に迫る！
CASTDICE TV
チャンネル登録者数 13.4万人
59,291 回視聴 2022/10/28
勇介
6 日前
次元が違い過ぎて笑えてきました。
色んな分野で能力を発揮して頂きたいです。
Tc
1 か月前
1人目は東大どころか、世界においての同世代でもトップな存在
305:１３２人目の素数さん
22/11/30 23:16:55.75 lvNLqkJH.net
>>278 補足
これの二人目が、山下 真由子氏です
URLﾘﾝｸ(ja.wikipedia.org)
山下 真由子（やました まゆこ）は、日本の数学者。専門は微分幾何学[1]。京都大学数理解析研究所助教。2022年、マリア・スクウォドフスカ＝キュリー賞最優秀賞。
306:１３２人目の素数さん
22/11/30 23:19:01.56 lvNLqkJH.net
>>278-279
下記は逆の意味で面白い
東大生4人に対して、森内九段の４面指し
森内九段の考慮時間数秒
圧倒的に、森内九段の力が上
これぞプロの世界
だから、クイズ東大王（雑学）って意味あるの？
って話になる
URLﾘﾝｸ(www.youtube.com)
【東大VS天才棋士】東大生4人vs天才棋士・森内九段！どっちが勝つ！？【検証】
QuizKnock
チャンネル登録者数 196万人
2,149,627 回視聴 2019/09/27
提供：大阪王将
URLﾘﾝｸ(www.osaka-ohsho.com)
QuizKnockの頭脳が4人集まれば天才棋士・森内九段にも勝てる？
前代未聞の特殊ハンデ「持ち駒シェアOK」でまさかの展開に…
flower flower
3 年前
「ふくらさん歩借ります」
「香と角くれ」
みたいな本来の将棋では絶対ありえない台詞&普段競い合ってるメンバーが共闘して強敵に立ち向かってる感めっちゃ好き
M Fukunaga
3 年前
森内九段が優しすぎてもはやただの将棋教室
ユウユウ
3 年前
偉大なプロ棋士さんを招いて将棋界の普及にもなりつつ、エンターテイメント性たっぷりな面白い動画に仕上げているのが素晴らしいですね
森内先生も物腰柔らかな接し方で、指導対局のように上手く盛り上げておられて流石の一言だなと思います
コメント欄で森内先生のエピソード紹介がたくさんされているのも笑顔になります
いい動画でした、楽しかったです??
307:１３２人目の素数さん
22/12/01 04:50:29.64 Lhx+Jl2m.net
>>277
>アホやなお前
>いまだに、何年も「箱入り無数目」の不成立が理解できないやつｗｗｗ
アホは貴様じゃ
スレタイ 箱入り無数目を語る部屋6
ｽﾚﾘﾝｸ(math板:30番)
「選ま」（＝選択公理はマチガッテル！）
「整ま」（＝整列定理はマチガッテル！）
のアホ吠えまくる
時枝「箱入り無数目では、同値類の代表を使えば
確率99/100で、選んだ箱の中身を当てられる」
選ま「同値類の代表の選出は実行不能なので当てられない！」
ヴィタリ「R/Qから、代表を選べば非可測集合ができる」
選ま 「同値類の代表の選出は実行不能なので可測集合しか存在しない！」
ｷﾞｬﾊﾊﾊﾊﾊﾊ!!!
308:１３２人目の素数さん
22/12/01 04:59:31.52 Lhx+Jl2m.net
>>278-280
何度頑張っても対偶の法則が理解できずに
工業高校を1年で中退したアホが
東大卒を羨ましがってますｗｗｗｗｗｗｗ
309:１３２人目の素数さん
22/12/01 07:34:38.84 9ADCB0B7.net
>>281-282
空気読めという言葉は好きじゃない
だが、今のあんたには適切かもなｗ
いま、お主に賛同する人少ない
特に、時枝>>277についてはねｗｗｗ
310:１３２人目の素数さん
22/12/01 08:51:48.59 RV+GSxCX.net
>>283
1に賛同する奴ぁ0
代表の選択は実行不能だから箱入り無数目はナンセンスとか
選択公理を否定する「選ま」でしたかwww
311:１３２人目の素数さん
22/12/01 10:04:09.23 kl2o24qP.net
>>284
言いたいことは
それだけか？
ならば
逝って良し！ｗ
312:１３２人目の素数さん
22/12/01 11:04:30.44 kl2o24qP.net
>>265
>>もう内容が古いだろう
> というか、今どきHoare logicなんて教えんらしい
> Curry-Howard correspondenceとかのほうが
> カッコイイもんな でもそれも前世紀かw
お主、統合失調症の薬飲みだしてからか、
最新の情勢に疎いなｗ
私もそれほど詳しくないがｗ
１）下記”数理科学 2022年12月号 連載 計算機科学の数学 2 ～ ラムダ計算(2) ～龍田 真 ”
これ現在進行形
２）ラムダ計算とカリー＝ハワード同型対応とは、関連している（下記）
３）下記カリー＝ハワード同型対応の「自然演繹とラムダ計算との間の対応」ご参照
４）下記「特にLISP、ML、Haskellといった関数型プログラミング言語の理論的基盤として、その誕生に大きな役割を果たした。」
５）下記「ラムダ計算と最も密接な関係をもつプログラミング言語は関数型言語と呼ばれる諸言語で、本質的にはいくつかの定数とデータ型を用いてラムダ計算を実装している。Lispでは関数の定義にラムダ記法の一変形を用いており、さらに、純Lispと呼ばれるLispのサブセットはラムダ計算と真に等価になっている。」
６）下記「カリー＝ハワード＝ランベック対応 直観主義論理、型付きラムダ計算およびデカルト閉圏との間の対応として知られる」
なので、カリー＝ハワード同型対応＋ラムダ計算＋圏論＝→現在進行形の計算機科学の数学
じゃないかな？ｗ
（参考）
URLﾘﾝｸ(www.saiensu.co.jp)
数理科学 2022年12月号
目次
連載
計算機科学の数学 2
～ ラムダ計算(2) ～
龍田 真
つづく
313:１３２人目の素数さん
22/12/01 11:04:58.49 kl2o24qP.net
>>286
つづき
URLﾘﾝｸ(ja.wikipedia.org)
ラムダ計算
ラムダ計算（ラムダけいさん、英語: lambda calculus）は、計算
314:模型のひとつで、計算の実行を関数への引数の評価（英語: evaluation）と適用（英語: application）としてモデル化・抽象化した計算体系である。ラムダ算法とも言う。関数を表現する式に文字ラムダ (λ) を使うという慣習からその名がある。アロンゾ・チャーチとスティーヴン・コール・クリーネによって1930年代に考案された。1936年にチャーチはラムダ計算を用いて一階述語論理の決定可能性問題を（否定的に）解いた。ラムダ計算は「計算可能な関数」とはなにかを定義するために用いられることもある。計算の意味論や型理論など、計算機科学のいろいろなところで使われており、特にLISP、ML、Haskellといった関数型プログラミング言語の理論的基盤として、その誕生に大きな役割を果たした。 ラムダ計算がチューリングマシンと等価な数理モデルであることを意味している。チューリングマシンがハードウェア的なモデル化であるのに対し、ラムダ計算はよりソフトウェア的なアプローチをとっている。 この記事ではチャーチが提唱した元来のいわゆる「型無しラムダ計算」について述べている。その後これを元にして「型付きラムダ計算」という体系も提唱されている。 歴史 元々チャーチは、数学の基礎となり得るような完全な形式体系を構築しようとしていた。彼の体系がラッセルのパラドックスの類型に影響を受けやすい（例えば論理記号として含意 → を含むなら、λx.(x→α) にYコンビネータを適用してカリーのパラドックスを再現できる）ということが判明した際に、彼はそこからラムダ計算を分離し、計算可能性理論の研究のために用い始めた。この研究からチャーチは一階述語論理の決定可能性問題を否定的に解くことに成功した。 つづく
315:１３２人目の素数さん
22/12/01 11:05:26.94 kl2o24qP.net
>>287
つづき
ラムダ計算とプログラミング言語
ピーター・ランディン（英語版）は1965年に発表したA Correspondence between ALGOL 60 and Church's Lambda-notationにおいて、ラムダ計算が手続的な抽象化と手続き（サブプログラム）の適用のしくみを提供しているがために、多くのプログラミング言語がラムダ計算にその基礎を置いているとみることができるとしている。
ラムダ計算をコンピュータ上に実装するには、関数を第一級オブジェクトとして取り扱う必要があり、これはスタック・ベースのプログラミング言語においては問題となってくる。これはFunarg問題（英語版）として知られている。
ラムダ計算と最も密接な関係をもつプログラミング言語は関数型言語と呼ばれる諸言語で、本質的にはいくつかの定数とデータ型を用いてラムダ計算を実装している。Lispでは関数の定義にラムダ記法の一変形を用いており、さらに、純Lispと呼ばれるLispのサブセットはラムダ計算と真に等価になっている。
URLﾘﾝｸ(ja.wikibooks.org)
Haskell/カリー=ハワード同型
カリー=ハワード同型(Curry-Howard isomorphism)は数学の一見無関係に思えるふたつの領域、型理論と構造論理を結びつける実に驚くべき関係である。
つづく
316:１３２人目の素数さん
22/12/01 11:05:47.61 kl2o24qP.net
>>288
つづき
URLﾘﾝｸ(ja.wikipedia.org)
カリー＝ハワード同型対応
カリー＝ハワード同型対応（カリー＝ハワードどうけいたいおう、英語: Curry?Howard correspondence）とは、プログラミング言語理論と証明論において、計算機プログラムと証明との間の直接的な対応関係のことである。「プログラム＝証明」(proofs-as-programs)・「型＝命題」(formulae-as-types)などとしても知られる。
通常はこの論理と計算の関連性はカリーとハワードに帰属される。しかしながら、このアイデアはブラウワー、ハイティング、コルモゴロフらが定式化した直観主義論理の操作的解釈の一種（ブラウワー＝ハイティング＝ コルモゴロフ解釈（BHK 解釈）（英語版））と関係している。[要出典]
自然演繹とラムダ計算との間の対応
ハスケル・カリーがヒルベルト流の体系とコンビネータ論理の構文的対応を強調した後、ウィリアム・アルヴィン・ハワードは1969年に単純型付きラムダ計算と自然演繹との構文的な同型性を明確にした。以下、左辺で直観主義的自然演繹の含意断片を形式化し、右辺でラムダ計算の型付け規則を示す。
ハワードの対応は自然演繹およびラムダ計算の拡張に対しても自然に延長できる。網羅的ではないがここに列挙しておく：
・グロタンディーク位相に於ける局所真理(▽)様相、あるいは同じことだが Benton, Bierman, and de Paiva (1998) のlax様相(〇)は計算型を記述するCL論理と対応する。[2][3]
BHK解釈
BHK解釈は直観主義的な証明の含意と全称化を関数として解釈するが、解釈における関数のクラスがどのようなものであるかを指定してはいない。もし関数のクラスとしてラムダ計算を取るならば、BHK解釈は自然演繹とラムダ計算との間の対応と同じことを述べていることになる。
カリー＝ハワード＝ランベック対応
ヨアヒム・ランベックは1970年始めに直観主義命題論理とデカルト閉圏の等式理論と対応するある種の型付きコンビネータとの対応関係の証明を示した。このカリー＝ハワード＝ランベック対応は直観主義論理、型付きラムダ計算およびデカルト閉圏との間の対応として知られる。
(引用終り)
以上
317:１３２人目の素数さん
22/12/01 12:08:48.53 2j+KSHjn.net
>>286-289
>私もそれほど詳しくないが
誤 それほど
正 まったく
>カリー＝ハワード同型対応＋ラムダ計算＋圏論
>＝→現在進行形の計算機科学の数学
と言ってたのが前世紀末
龍田真さんも、いいお歳
1はde BruijnのAutomath プロジェクトも知らなそう
ていうか、de Bruijn、読めなそうwww
318:１３２人目の素数さん
22/12/01 17:14:33.39 kl2o24qP.net
>>290
>>カリー＝ハワード同型対応＋ラムダ計算＋圏論
>>＝→現在進行形の計算機科学の数学
> と言ってたのが前世紀末
１）じゃ、現在完了進行形と言えばいいかな？ｗ
２）Nicolaas_Govert_de_Bruijnは、和文 ニコラース・ホーヴァート・ド・ブラウンとあるけど（発音記号をみるとあやしそうだｗ）
３）Automathは、”starting in 1967””never widely publicized at the time”か
４）自動証明検証システム Mizarに影響を与えたとあるね
５）こういうコンピュータを使った数学（数式処理と証明検証）は、神戸大数学の高山信毅先生が熱心だったよね
お主、新しい動きフォロー出来てないねｗ
（下記情報も古いかもだが（最近はMathematica？））
（参考）
URLﾘﾝｸ(en.wikipedia.org)
Nicolaas Govert (Dick) de Bruijn (Dutch: [niko??la?s ?xo?v?rt d? ?br?yn];[1] 9 July 1918 ? 17 February 2012) was a Dutch mathematician, noted for his many contributions in the fields of analysis, number theory, combinatorics and logic.[2]
URLﾘﾝｸ(ja.wikipedia.org)
ニコラース・ホーヴァート・ド・ブラウン（Nicolaas Govert de Bruijn、1918年7月9日 - 2012年2月17日）はオランダ人数学者であり、アイントホーフェン工科大学の名誉教授を勤めた。アムステルダム自由大学で1943年に博士号を取得した。
つづく
319:１３２人目の素数さん
22/12/01 17:14:53.52 kl2o24qP.net
>>291
つづき
URLﾘﾝｸ(en.wikipedia.org)
Automath
Automath ("automating mathematics") is a formal language, devised by Nicolaas Govert de Bruijn starting in 1967, for expressing complete mathematical theories in such a way that an included automated proof checker can verify their correct
320:ness. Contents 1 Overview 2 See also 3 References 4 External links Automath was never widely publicized at the time, however, and so never achieved widespread use; nonetheless, it proved very influential in the later development of logical frameworks and proof assistants.[2][3] The Mizar system, a system of writing and checking formalized mathematics that is still in active use, was influenced by Automath. https://en.wikipedia.org/wiki/Mizar_system Mizar system https://ja.wikipedia.org/wiki/Mizar Mizar 自動証明検証システム Mizar（ミザー、ミザール）は、まったく厳密に形式的な形で数学的な定義や証明を記述するためのデータ記述言語（Mizar-言語）、実際にその言語で記述された証明の内容を検証することができる計算機プログラム（証明検証プログラム）、プログラムから参照して新たな証明の際に利用可能な定義と証明済みの定理からなるライブラリ (MML) の三者から構成される。 Mizar と同様の目的を持つプロジェクトに、ロバート・ボイヤーのQEDプロジェクトがある。 MMLはタルスキー・グロタンディーク集合論の公理に基づいて構築される。2008年5月現在、8,800の定義と46,000の定理を含む[3]。例えばハーン・バナッハの定理、ケーニヒの補題、ブラウワーの不動点定理、ゲーデルの完全性定理、カントール集合に関するいくつかの事実、などがMMLに含まれる。 つづく
321:１３２人目の素数さん
22/12/01 17:15:32.05 kl2o24qP.net
>>292
つづき
URLﾘﾝｸ(www.math.kobe-u.ac.jp)
KNOPPIX/Mathと方程式
高山信毅 神戸大
2007.07.11
P68
3.9 機械検証が可能な証明の集積
coq [?], mizar (mizar のデータベース).
URLﾘﾝｸ(coq.inria.fr)<)
高山 信毅
神戸大学理学部数学科
解析数理講座 教授
いまから(2004年2月の記述). 10 年の目標の一つは, 数学関連学科の数学ソフトウアの開発能力を アメリカ, カナダ, 西ヨーロッパの国程度までに引き上げる こと. 数学ソフトウエアは, 数学の研究のために利用されたり, 上のような"計算できるか？"という問題の答えを実証してみたり, またその技術成果が産業界に技術移転されている. こういった能書きはともあれ, 開発はとてもたのしい. 数学ソフトの開発を振興するため研究集会もいろいろ企画している. たとえば 2002 年の ICM のサテライトで 国際数学ソフト会議 を北京で開催.
URLﾘﾝｸ(researchmap.jp)
高山 信毅
タカヤマ ノブキ (Nobuki Takayama)
URLﾘﾝｸ(ja.wikipedia.org)
Mathematica
(引用終り)
以上
322:１３２人目の素数さん
22/12/02 05:14:02.58 4wsfTfen.net
>>291-292
1は劣等感に苛まれてる中卒だから火ィつけるとあっちゅー間に燃えるなｗｗｗ
>>293
証明検証の話なのに、数式処理とか言い出すのが、1の残念なところ
1にとって数学って数式の計算でしかないんだな
ま、中卒は線型方程式系の変数消去でもやってろｗｗｗｗｗｗｗ
323:１３２人目の素数さん
22/12/02 05:17:34.16 4wsfTfen.net
自動証明の理屈は実は簡単だ
URLﾘﾝｸ(ja.wikipedia.org)
ただ、述語論理の場合、証明が存在しない式で実施すると止まらない
「決定不能」というのはそういうこと
証明が存在するなら、必ず終わる
324:１３２人目の素数さん
22/12/02 05:20:13.93 4wsfTfen.net
数学＝方程式を解くこと、としか思わない計算馬鹿は数学板に書くなｗ
325:１３２人目の素数さん
22/12/02 07:15:17.51 fZZ7hap7.net
>>294-296
笑えるな
> 1は劣等感に苛まれてる中卒だから火ィつけるとあっちゅー間に燃えるなｗｗｗ
別にぃ～ｗ
守備範囲に近い事項だから書いただけ
de Bruijn、Automathは、知らなかったが
高山信毅 神戸大とMizarは、名前だけは知っていた
それを書いただけ
>URLﾘﾝｸ(ja.wikipedia.org)
>ただ、述語論理の場合、証明が存在しない式で実施すると止まらない
>「決定不能」というのはそういうこと
>証明が存在するなら、必ず終わる
正確に引用した方が良いぞｗｗ
「決定可能性
タブローの方法は命題論理や一引数の一階述語論理において決定可能である。つまり有限ステップで必ず判定を行える。しかし、二引数以上の一階述語論理において決定不可能である。つまり充足可能な場合(例えば∀x∃yR(x,y))、有限ステップで終了せず、延々と手続きが続く状況に陥ることがあるからである。」
つまり、二引数以上 例えば∀x∃yR(x,y) で、すでに決定不可能であるｗｗ
あと、下記 有限時間に終わるとしても、”P≠NP”問題のような計算複雑性がからむ
いま、ある証明検証のプログラムを走らせてまだ終わらないとする
人は、あと何日か続けて終わるのか？ それとも永遠に終わらないのか？ その判断ができない
これが、計算複雑性の話
(参考)
URLﾘﾝｸ(ja.wikipedia.org)
P≠NP予想
P≠NP予想（P≠NPよそう、英: P is not NP）は、計算複雑性理論（計算量理論）における予想 (未解決問題) の1つで、「クラスPとクラスNPが等しくない」というものである。
理論計算機科学と現代数学上の未解決問題の中でも最も重要な問題の一つであり、2000年にクレイ数学研究所のミレニアム懸賞問題の一つとして、この問題に対して100万ドルの懸賞金がかけられた。
概要
クラスPとは、決定性チューリングマシンにおいて、多項式時間で判定可能な問題のクラスであり、クラスNPは、Yesとなる証拠（Witnessという）が与えられたとき、多項式時間でWitnessの正当性の判定（これを検証という）が可能な問題のクラスである。
326:１３２人目の素数さん
22/12/02 07:39:29.64 4wsfTfen.net
>>297
>守備範囲に近い事項だから書いただけ
観客に守備範囲はないだろｗｗｗ
>有限時間に終わるとしても、”P≠NP”問題のような計算複雑性がからむ
1は、NP完全の最初の例が、命題論理の充足可能性問題だってこと知らなそうｗ
充足可能性問題
URLﾘﾝｸ(ja.wikipedia.org)
もちろん、述語論理の充足可能性問題は、決定不能である
327:１３２人目の素数さん
22/12/02 07:58:25.24 4wsfTfen.net
今日のできごと
・日本サッカーW杯 ドイツにつづきスペイン撃破で決勝進出
・1、「箱入り無数目」に完敗で死亡
ｽﾚﾘﾝｸ(math板:58番)
さて、
ｐ進数x＝Σ(i=z~∞)a_i*p^i∈Qp (z∈Z)
のどの項が０か当てるのに、箱入り無数目の戦略が使える
ｐ進数100個を用意する、その中から１個を選ぶ
他の99個の最小項の次数中の、最小値z_minを求める
z_min+1番目の項が０だと答えれば、確率99/100で当たる
この問題は、全く選択公理を用いない
328:１３２人目の素数さん
22/12/02 08:19:39.58 fZZ7hap7.net
>>296
>数学＝方程式を解くこと、としか思わない計算馬鹿は数学板に書くなｗ
あ～ら、すねちゃったｗ
ガキだねｗ
まあ、広く 数学 ←→ コンピュータサイエンス
の絡み合いと考えれば、よかんべｗ
数学の自動証明は、コンピュータサイエンスではプログラムの検証問題だし
要するに、数学はコンピュータやコンピュータサイエンスの成果を取り入れるべきだし（下記東大 数学科）
コンピュータサイエンスに対する貢�
329:｣もありだろう そういう広い始点を持つべきでしょ あ、あんたには無理かな？ (参考) https://www.s.u-tokyo.ac.jp/ja/admission/undergraduate/pdf/ms2022.pdf 東大 理学部数学科紹介 2022/05/19 P3 図書 コンピュータなど勉学の環境 P34 最近の発展 Fn=Z*・・*Z (ｎ個の)自由群 ｎ>=5のときAut(Fn)はproperty(T)をもつ （Kaluba-小沢-Nowok,2019） -コンピュータを使った(rigorousな)証明 -human proofはまだない
330:１３２人目の素数さん
22/12/02 09:15:11.86 4wsfTfen.net
>>300 1 必死の余裕ｗ
数学だけでなくコンピュータサイエンスも全然わかってませんでしたぁｗ
>最近の発展 Fn=Z*・・*Z (ｎ個の)自由群
>ｎ>=5のときAut(Fn)はproperty(T)をもつ
ドヤ顔で手書きのメモを手打ちで丸写しするも
肝心のproperty(T)が何だか全然分かっておらずｗ
1は結局ヌケサク中卒ｗｗｗｗｗｗｗ
331:１３２人目の素数さん
22/12/02 09:17:28.56 4wsfTfen.net
中卒1が見つけられなかったもん、ドヤ顔でリンク！
URLﾘﾝｸ(en.wikipedia.org)(T)
だからいってるだろ 中卒は検索コピペでも大卒に完敗だってな
ｷﾞｬﾊﾊﾊﾊﾊﾊ!!!
332:１３２人目の素数さん
22/12/02 09:21:28.88 4wsfTfen.net
ていうか、自由群持ち出すなら、まずこの話をしろや 選ま、整まのアホ１
バナッハ＝タルスキ―のパラドックス
URLﾘﾝｸ(ja.wikipedia.org)
証明の概要
定理の証明を与える。
ここでの方法はバナッハとタルスキーによるものと似ているが全く同一ではない。
証明は本質的に4つのステップに分かれる。
１．2つの生成元を持つ自由群F_2の「パラドキシカルな分割」を見つける。
２．自由群F_2と同型な3次元の回転群を見つける。
３．2で作った回転群のパラドキシカルな分割と選択公理を用いて2次元球面の分割を作る。
４．3の2次元球面の分割を3次元球の分割に拡張する。
333:１３２人目の素数さん
22/12/02 09:24:36.64 4wsfTfen.net
>>303
ステップ1
2つの生成元aとbから生成される自由群は
4つの文字a、a^－1、b、b^－1からなる
有限の長さを持つ文字列から構成される。
ここでaがa^－1の直前直後に現れるような文字列は許されない。bについても同様である。
2つのこのような文字列があったとき、
それらの積をそれらの文字列をつなげたものと定義する。
ただしそれにより「許されない文字列」が生じたときは、
その部分を「空の文字列」で置き換えることで対処する。
例えばabab^－1a^－1とabab^－1aの積は
abab^－1a^－1abab^－1aとなるが、
これはa^－1aという「許されない文字列」を含むため、
この部分を「空の文字列」で置き換えてabaab^－1aとなる。
このような文字列の集合はここで定義した演算によって、
「空の文字列」を単位元eに持つ群になることが確かめられる。
この群をF2と書く。
F2の要素は有限の長さを持つ文字列であるので、
F2は可算集合である。
(これはゲーデル数を用いて容易に証明できる)
334:１３２人目の素数さん
22/12/02 09:35:11.53 4wsfTfen.net
>>304
群F_2は以下のようにして「パラドキシカルな分割」が可能である:
S(a)をaで始まるF_2の文字列全体の集合とする。
S(a－1)、S(b)、S(b－1)についても同様である。
明らかに、
F_2={e}∪S(a)∪S(a^-1)∪S(b)∪S(b^-1)
一方
F_2=aS(a^-1)∪S(a)
および
F_2=bS(b^-1)∪S(b)
である。
aS(a－1)という表記は、S(a－1)の元の左にaをかけた文字列の全体である。
最後の行がこの証明の核心である。
例えば集合aS(a^-1)はaa^-1bという文字列を含む。
aはa^-1の直前直後に現れてはいけないというルールにより、
この文字列はbとなる。
同様に、aS(a^-1)はa^-1で始まる全ての文字列を含む。
（例えば文字列aa^-1a^-1はa^-1となるため）
このようにして、aS(a^-1)はb,
335: b^-1, a^-1で始まる全ての文字列を含む。 （つまり、aS(a^-1)={e}∪S(b)∪S(b^-1)∪S(a^-1) )
336:１３２人目の素数さん
22/12/02 09:40:27.00 4wsfTfen.net
バナッハ＝タルスキーのパラドックスの核心は
>>304-305で述べた、階数２以上の自由群のパラドキシカルな分割なので
変換群が階数２以上の自由群を持てば、選択公理を使って
パラドキシカルな分割を構成できる
RがQを部分群として持てば、ヴィタリ集合が構成できるのと同じこと
選択公理が核心、というわけではない
（ＲはＺを部分群としてもつから、選択公理を使わずして
Ｒ全体を１とする測度で、区間[0,1)が非可測になると示せるｗ）