利用者‐会話:I.hidekazu

ページのコンテンツが他言語でサポートされていません。
ウィキペディア日本語版へようこそ!

こんにちは、I.hidekazuさん。はじめまして! ウィキペディア日本語版へようこそ!

ファーストステップ・ガイド
  • 初心者の方はまずガイドブックを読んでください。今後の編集活動にとってとても大切な内容が書かれています。
  • 児童・学生のみなさんは児童・生徒の方々へをお読みください。
  • サンドボックスでは、自由に試し書きをすることができます。
  • トレーニングも兼ねて自己紹介をしてみましょう。
  • 隣の利用者ページは自己紹介や作業用のスペースとして利用することができます。
  • 執筆・編集するときは五本の柱に注意してください。
ヘルプ
  • 利用案内 - ウィキペディアの機能や使い方に関する質問はここでできます。
  • FAQ - ウィキペディアについてのよくある質問と回答集です。
  • ヘルプ - ウィキペディアの使い方を説明したページの一覧です。
  • コミュニティ・ポータル - 利用者のための総合的なポータルページです。
ワンポイント情報
間違えてしまったら?
  • ウィキペディアはウィキというシステムを使っています。ちょっとした間違いなら、すぐに直して投稿すれば問題ありません。
  • ウィキペディアのページそのものは削除することができません。詳しくは削除の方針に書かれています。
Hello, I.hidekazu! Welcome to Japanese Wikipedia. If you are not a Japanese speaker, you can ask a question in Help. Enjoy!
ウィキペディアの機能や使い方に関してわからないことがあったら利用案内で質問できます。
I.hidekazuさんがウィキペディアにおいて実り多き執筆・活動をなされることを楽しみにしております。--ロボットAlexbotAlexshによる自動操作 2010年10月30日 (土) 12:31 (UTC)[返信]

「圏論」の記事について[編集]

こんにちは.NGiraffe といいます.圏論関連の記事の編集お疲れ様です.標記の記事を読ませて頂き,幾つか気が付いたことがありますので余計なお世話と思いつつコメントしに参りました.

  • 2011年 8月の版で記載されていた「歴史」と「他分野への影響」が最新版では無くなっています.百科事典の性格上,主題がどのように定式化されてきたか,他の主題とどのように関連しているかを記載するのは有益であると思います.プロジェクト:数学#数学記事の構造として提案されているものもご参照ください.
  • リンクが殆どなく,web で閲覧する事典の利点が生かされていません.無理にリンクの数を増やす必要はありませんが,記事内で説明のされない「線型空間」「(余)ドメイン」や,独立記事が存在する「自然変換」「関手」などにはリンクが必要かと思います.
  • おそらく別行立ての数式と思われる行が引用を示すマークアップで記載されていて,他の記事と比較したときに違和感があります(たとえば「関手(functor)」の節の第三パラグラフ homC(A,B) = {f | f は C の射 f : A → B} など).プロジェクト:数学#TeXを利用するには,このような場合「行頭にコロン(:)を置く」という方法が紹介されています.

単なる一編集者の感想で私が誤解している部分もあるかと思いますが,今後の編集の際の参考になれば幸いです.NGiraffe会話2012年7月1日 (日) 15:53 (UTC)[返信]

回答[編集]

下記のとおり回答する。

「歴史」、「他の分野への影響」の項目について。[編集]

「歴史」項目の削除を行った理由

過去の「歴史」項目の記述には誤り及び思い込みによる記述が多く多分に不要な先入観を与えるものであり、圏論の理解の大きな妨げになっていたため。

  • ガロア、ネーターに関する記述はほぼこじつけ
  • ブルバキに関する記述は年代の順序がおかしい。普遍性については圏論の登場以後である。サミュエルの普遍写像性問題に一切触れていない。
  • 圏論は代数的位相幾何の問題が始まりではなく群の指標に関するものが大元である。

再度の記載についてはLeo Corry の Modern Algebra and the Rise of Mathematical Structures を元に記載を行う予定である(未定)。

「他の分野への影響」項目の削除を行った理由

記載内容の正当性を確認できる信頼出来る文献が見当たらず、その正当性に大きな疑念があった。また、圏論の関連項目として記載があるがこれはホモロジー代数の関連項目である。

こちらの項目については、納得できる根拠からなる文献を見つけることができた際に順次記載を行う予定である(未定)。

リンク箇所が少ないことについて[編集]

単語にリンクを付与する行為も記述行為であると理解している。リンク先の記述内容が要領を得ず意味不明である場合、リンクを付与する行為はリンク元の記述内容の理解をも混乱させる。リンク項目が存在するとしてもそのような不誠実な行為を行うことは甚だ受け入れがたく、要請に応えることはできない。ただし、リンク先の記述が改められた場合はこの限りではない。

数式については引用ではなく「行頭にコロン(:)を置く」ことにすることについて[編集]

了解した。但し、数式を引用している場合は引用を行う。

---I.hidekazu会話2012年7月2日 (月) 12:06 (UTC)[返信]

ご回答ありがとうございます.将来歴史や他分野との関連について執筆される予定であるとのことで,記事の充実を楽しみに待ちたいと思います.リンクについても了解しました.NGiraffe会話2012年7月3日 (火) 14:17 (UTC)[返信]

ファイル:ProductDiag.pngには著作権上の問題があります[編集]

警告 著作権の状態が不明です

こんにちは。ファイル:ProductDiag.pngをアップロードして頂き、ありがとうございます。しかし、この画像(ファイル)には著作権の状態またはライセンスが明記されていないため、著作権上の問題があります。出典とライセンスのないファイルは、1週間後に削除されますので御注意ください。

ウィキペディアにアップロードされるすべてのファイルは、画像利用の方針に従っており、かつ詳細な出典とライセンスが明記されている必要があります。ファイルの著作権表示タグを参照し、適切なライセンスを表すタグを貼付してください。どうぞよろしくお願いします。

出典とライセンスを明記する際はファイルページにアクセスし「編集」タブをクリックして記載してください。同ファイルを再アップロードしても記入した内容は反映されません。

重要: あなたがこのファイルの他にもファイルをアップロードされているならば、あなたのアップロード記録を見て、他のファイルにも同様に出典とライセンスが明記されているかどうか今すぐ確認してください。それらのファイルや、今後あなたがアップロードされたファイルに出典やライセンスが記載されていなければ、同様に削除されます203.90.20.40 2013年1月1日 (火) 05:52 (UTC)[返信]

記事の移動[編集]

記事の移動は改名提案とその合意形成後に『移動コマンド』で行ってください。

移動は編集画面上部 ▼ にあります。詳しくはWikipedia:ページの改名参照。--LearningBox会話2013年4月22日 (月) 05:09 (UTC)[返信]

  • 移動コマンド及び合意形成について存じませんでした。お教えいただきありがとうございます。改名の案を提出したいと思います。

--I.hidekazu会話2013年4月22日 (月) 14:07 (UTC)[返信]


一括投稿のお願い[編集]

こんにちは。I.hidekazuさんが同じ記事に対して節ごとに分けて連続して投稿されているようでしたので、一括投稿のお願いに参りました。Wikipedia:同じ記事への連続投稿を減らすにあるとおり、同じ記事への連続投稿は履歴の見通しが悪くなるなど、さまざまな面で支障をきたすおそれがあります。細かい節がたくさんある場合は、節ごとに細かく投稿をするのではなく、上位の節または項目全体の編集を行い、一括して投稿していただきますようにお願いいたします。

投稿時、中央のボタンを押すとプレビューできます。(詳細画像

その際に細かいところでミスを起こすのではないかと心配な場合は、「投稿する」ボタンの右隣にある「プレビューを実行」ボタンを活用されることをお勧めします(画面右側の図を参照)。投稿される前に「プレビューを実行」のボタンを押すと、成形結果を先に見ることができます。これを使うことで、

などをあらかじめチェックし、修正した上で記事を投稿することができますので、是非ともご活用ください。

また、編集競合を避けたい場合は、Template:Inuseをお使いください。ご迷惑をおかけしますが、ご理解とご協力をよろしくお願いします。--Kiruria281会話2013年6月1日 (土) 15:20 (UTC)[返信]

努力します。--I.hidekazu会話2013年6月1日 (土) 15:30 (UTC)[返信]

数学基礎論記事について[編集]

ノート:数学基礎論にてあなたの編集方針について疑問を提示しましたので返事をいただけると幸いです。--Tkcom会話2013年8月22日 (木) 04:49 (UTC)[返信]

回答を行った。--I.hidekazu会話2013年8月22日 (木) 13:24 (UTC)[返信]

等価線量について[編集]

はじめまして(ですよね?)。等価線量にて参考文献を追加されていますが、執筆者の皆様はこの参考文献を元に記事を書いたのでしょうか?そうでなければ「関連文献」とするか外部リンクに含めるべきだと思います。--JapaneseA会話2013年10月12日 (土) 16:41 (UTC)[返信]

放射能について[編集]

放射能で出典の17番目がおかしくなっています。修正御願いします。--JapaneseA会話2013年11月5日 (火) 15:13 (UTC)[返信]

対応した。--I.hidekazu会話2013年11月5日 (火) 16:57 (UTC)[返信]

記事間をまたぐ編集における注意事項[編集]

おはようございます。I.hidekazu様は放射線関連の記事に対し、大量の編集をされているようですが、それに関して少々。御存知でしょうが、放射線関連の記事は被曝放射線の説明があったり、その逆だったりしてカオス状態でした。かねてより問題だと思っておりましたが、是正するにはあまりにもごちゃごちゃ過ぎて手をこまねいておりました。それをI.hidekazu様が正しく是正されているのであれば、好ましい事だと思いますし、応援致します。ただ、この際気をつけて頂きたいのが、記事を跨いだ記述の移動などです。ルールとして要約蘭に履歴継承が必要な事は勿論ですが、統合提案分割提案が必要な場合もあります。このような事は先刻御承知でしょうし、このような事を申し上げるのは失礼かと思いましたが、私の会話ページに他者様より危惧する声もあり、転ばぬ先の杖として申し上げました。どうか気を悪くされないで下さい。--JapaneseA会話2013年12月5日 (木) 22:37 (UTC)[返信]

お知らせいただきありがとうございます。項目を跨がるものについては、なるべく該当する項目記事の方に記述するべきなので、該当記事の方にすでに書かれている場合はなるべくその記事への案内に代えてます。お知らせのとおり、統合提案、分割提案が必要な場合は提案します。
ただ、関連記事に記載されている一文や一段落を移動させる場合は、提案は必要ない理解していますので、その場合は要約欄にどこの記事から移動させてきたかということを記載した上で記述を移動させています。もし問題がありましたらお手数ですが、またお知らせいただければありがたいです。--I.hidekazu会話2013年12月6日 (金) 14:36 (UTC)[返信]

告知について[編集]

こんばんわ。こちらの利用者ページにもアカウント「原子力関連記事編集」はI.hidekazu様と同一人物だという告知が必要かと思います。--JapaneseA会話2013年12月28日 (土) 09:45 (UTC)[返信]

いやーはじめに話しておいてよかったです。どうもどうも。対応します。ただちょっと考えたのですが、二つ使うのはやっぱり大変かな、と思い直したりもしちゃいますね。どうしようかな。。--I.hidekazu会話2013年12月28日 (土) 10:29 (UTC)[返信]
私は2つ使っていますが、結構大変です。同じ分野は同じアカウントで編集したいのですが、誤字修正や分野の境界線にあるような記事だと非常に悩ましいです。なお、これまで1つめのアカウントで編集していた記事を、新アカウントで編集する際は、要約蘭に「I.hidekazu=原子力関連記事編集です」のような一言を入れるべきでしょう。--JapaneseA会話2013年12月28日 (土) 10:35 (UTC)[返信]
そうですね。わかりました。--I.hidekazu会話2013年12月29日 (日) 06:08 (UTC)[返信]

ボレル集合の改名提案について[編集]

標記の件ですが、Wikipedia:改名提案での告知およびボレル集合に貼付された告知タグにあるノート:ボレル集合にて改名提案を起こされた跡がございません。これでは告知不十分と言うより、提案そのものを行っているとは言えません。よって、改名したいのであれば、ノート:ボレル集合に提案をしていただき、1週間以内に異論が出ないのを待って改名するようにしてください。現状では改名したとしても、改名提案なき改名として差し戻し改名となります。以上よろしくお願いいたします。--Don-hide会話2013年12月28日 (土) 12:43 (UTC)[返信]

了解しました。--I.hidekazu会話2013年12月29日 (日) 06:08 (UTC)[返信]

マイケルソン・モーリーの実験について[編集]

ノート:マイケルソン・モーリーの実験にも書きましたが、実験の目的についての記述は、正しくそのように参考文献に記されているのでしょうか? と、いいますのも、この実験が行われた時代には光速が不変であるとは信じられておらず、マイケルソンやモーリーも「光速度 c」という物理定数が存在するとは思っていなかったたはずです。従って、そもそも「(v/c)^2 を検出しよう」という発想は生じないと考えられます。参考文献には「特殊相対性理論の観点からいえば、このように意味付けすることもできる」というような表記になっているのではないでしょうか?Francesco Nagoya会話2014年2月26日 (水) 04:20 (UTC)[返信]

言葉足らずなので追加です。マックスウェルが測定を依頼というか、そういう測定ができないといけないと伝えたのは、マイケルソンとモーレーじゃなくて、デイヴィッド・ペック・トッドという人です。マイケルソンはその人の同僚だったのでそのマックスウェルの話(手紙)を知って、β2 を検出する実験を始めることになったんです。実は、マイケルソンのみで一回ロシアで実験したりしているのですが、誤差が大きくてあまり信じられなかったようです。モーレーは後で一緒に実験をすることになったんです。詳しくは [1] の六章を読んでください。--I.hidekazu会話2014年2月26日 (水) 12:57 (UTC)[返信]
お返事ありがとうございます。en:Michelson-Morey experimentでは唐突にMaxwellがβ2などと言い出しているように読めて、いまいち意味がよくわからず、ローレンツ変換あたりの話と混乱があるのかと、首をかしげておりました。Maxwellはエーテル問題とは半ば独立に、(今日でいう)電磁波の性質を巡る議論から出発したのでしょうか。ご紹介の文献にあたってみます。--Francesco Nagoya会話2014年2月26日 (水) 14:27 (UTC)[返信]
β2 についてはやはりエーテルの存在を示すために問題視されたものです。おっしゃるとおり詳しくはその文献読んでください。私も今、調べている最中の話が多いので、はっきりしたことはわからないです。--I.hidekazu会話2014年2月28日 (金) 15:07 (UTC)[返信]
また補足ですが、気をつけるべきは光と電磁波が同一のものだという話になったのはマックスウェルの理論以降だということです。エーテルの存在を強く主張したのは確かフレネルだったハズですが、それは光を伝達しているものはエーテルだ、という話であって電場と磁場の伝達については関知してないです。マックスウェルは電磁気理論を設計するにあたってほぼ間違いなく流体力学の一種として設計したのですが、その電磁場を媒介する物質は何がふさわしいか?という課題に対してエーテルを持ち込んだということなのだと思います(ただ、しっかりした資料を見つけてないので推測が入っている可能性はあります)。
ちょっと話が飛んでるような内容ですが、その区分けをしとかないと意味がわからないところが出てくることがあるので参考までに。--I.hidekazu会話2014年2月28日 (金) 15:24 (UTC)[返信]

自然変換について[編集]

Kikさんと同じように以前の版に戻しました。内容についての批判ではなく記事構成の問題ですのでI.hidekazuさんの知識を批判しているわけではないことは予め断っておきます。圏 (数学)を読んでいたら自然変換という言葉がひっかかったので、自然変換という記事に飛んだら定義は圏 (数学)へ戻されるという形は好ましくありません。異なる記事間で内容の重複をさせすぎるのも好ましくないかもしれませんが、重複を嫌い過ぎるのも好ましくありません。2つの記事が別個に存在する場合、基本的には自然変換の記事には自然変換の詳細な説明が書かれ、それを含む圏 (数学)という大きな分野の項目の方に自然変換を入れるときは簡単な要約(詳しい事は自然変換の項目を見てください)という形であるべきと思います。定義ではなく些末な応用的な事で圏 (数学)に書いた方が妥当というような内容であればそちらに移動しても構わないと思いますが、定義節は説明の本体の部分に含まれると考えられる内容なのでKikさんのされた通り戻すという選択をしました。ご了承いただければ幸いです。--Sureturn会話) 2014年11月30日 (日) 15:01 (UTC) 自然変換の記事を元に戻させてもらい、定義を記載しました。--I.hidekazu会話2014年12月3日 (水) 13:12 (UTC)[返信]

それと上記の#一括投稿のお願いと同じですが、複数の版を取り消したい場合、取り消し機能を繰り返し多用して履歴を積み重ねなくても戻したい版を開いて編集画面を開いて要約欄にその版に戻した事を書いておけば十分で、無駄に履歴を重ねずに済みます。--Sureturn会話2014年12月2日 (火) 02:28 (UTC)[返信]

ありがとうございます。それは知りませんでした。てっきり特別な権限を持ったユーザのみが使用可能な機能だと思っていました。Kikさんのように書籍を購入して読み込んだ上で書いている部分についても一括で消されてしまうと立ち直るのに時間がかかります。独自研究的な深みにはまったものは仕方ありませんが、正当な文献にはっきりと記載してあることについてまで知られていないからという理由で消されてしまうのは正直納得いきません。学者の世界だけに閉じた話ならまだしも一般の人に知られたもので誤解がはびこり、不毛な論争が発生して問題だと思われるものについては、その誤解は解かないといけないものだと思うからです。 一括投稿については努力しているのですが、あまり守れておらず申し訳ないです。--I.hidekazu会話2014年12月3日 (水) 13:12 (UTC)[返信]

一括で消してるというのは間違いです。元あった記事とあなたが最初から全て書き直した記事を比較して、まともなほうを残しているだけです。元あった記事を書いた人だってあなたに一括で消されてしまったと思ってますよ。元の記事がある場合はそれを書いた人の努力も尊重してください。一から書き直さないといけない記事なんてほとんどないはずです。あと、あなたの型付きラムダ計算は無茶苦茶です。本を読んで勉強しているとは全く思えません。 --Kik会話2015年1月18日 (日) 12:51 (UTC)[返信]
とくに理由ないのに消すのやめてもらえますか。なんといわれましても私のお金と時間をかけて調べたものです。--I.hidekazu会話2015年1月19日 (月) 11:50 (UTC)[返信]
それはこちらのセリフです。自然変換の元の記事は今より12kBも多かったんですよ。説明画像も豊富な例も載っていたのにどうして消してしまうのですか? --Kik会話2015年1月19日 (月) 15:40 (UTC)[返信]
圏論は自然さの概念を定式化するために導入されました。自然でない変換というものは考えることはありません。ほか例については二重双対空間については挙げています。--I.hidekazu会話2015年1月20日 (火) 15:26 (UTC)[返信]
まずフォーマルな文章の書き方をもう少し学んでください。あなたの書き方では二重双対空間は例になっていません。これが例として正しく記述されるためには、圏として何を定めるか(この場合は有限次元線形空間の圏)、2つの関手として何を選ぶか(恒等関手と二重双対関手)、最後に変換のコンポーネントに何を選ぶか(長いので元の記事参照)を全て記述して初めて例として記述されるのです。
次に、元の記事では自然にならない例として双対空間が載っていました。こちらの例のほうがはるかに大切ですし、とても長い解説がついていました。これを消す理由があるとは思えません。
最後についでですが、「^ つまりVにおいて自然である。」などのような脚注の付け方はやめてください。圏論についている全ての脚注も同様です。こういう脚注の付け方は、知識をひけらかす様に見えるので、読む側からはふざけてるのかとか最悪馬鹿にしてるのかと取られます。こういう文章では避けるべき脚注の付け方です。
内容についてもいいたいことはたくさんあるのですが、まず正しい文章の書き方になるようにしてください。
一度リバートするので、すでにある重要な例を消さないようにして、追加したいことがあればもっとフォーマルな文章で追加してください。 --Kik会話2015年1月20日 (火) 16:30 (UTC)[返信]
ちょっとやっってることが理解しかねますね。礼を残せということですね、わかりました、元に戻しますが例は残しましょう。--I.hidekazu会話2015年1月21日 (水) 14:33 (UTC)[返信]
ふざけないで下さい。元の記事に書いてあったことがまだたくさん消えたままです。画像も適当に貼り付けただけ。こういう画像をつけるときは「以下の図式を可換にする~」とか文章を添えるものです。元の記事にはちゃんとありました。
多少はまともな数学カテゴリの体裁を持った記事を書けるようになって欲しくて、レビューしてあげているのに真剣に記事を改善しようとしないなら、数学記事をこれ以上書いていただく必要はないです。 --Kik会話2015年1月21日 (水) 18:18 (UTC)[返信]

管理者への立候補について[編集]

こんにちは、ぱたごんです。Wikipedia:管理者への立候補では過去ログ化は早くても3日後(推奨5日後)になっています。つまり、今回は私が終了宣告しましたが終了宣告後最低3日間はそのままにしておくわけです(なにか異議がつくかもしれないので)。今回はたしかに雪玉かもしれませんが。もしも過去ログ化なさるのであればWikipedia:管理者への立候補/ログへの追記もお願いします。--ぱたごん会話2014年12月30日 (火) 03:11 (UTC)[返信]

確かに最低3日でした(Wikipedia:管理者への立候補#過去ログ)。精進いたします。あの様子からすれば異議がつくことはないと思いますので、早いですが過去ログにしたいと思います。過去ログへ追記したいと思います。--I.hidekazu会話2014年12月30日 (火) 09:16 (UTC)[返信]
ありがとうございます。尚、管理者についてですが、人によっては管理者は「用務員」とか「ボタン押し係り」などと揶揄されています。つまり管理者はコミュニティの意思を実行に移す係りで、考え決めるのはコミュニティです。管理者が判断をしてはいけません。もちろん、緊急を要する案件やコミュニティの意思が賛否拮抗してなかなか決められないがそれでもあえてどちらかに決めなければならないケースなどでは管理者が判断するわけですし、明白な荒しへの対処など管理者が裁量で動いてよいケースもありますが認められた範囲を逸脱し、権限の私物化を計ると解任されてしまう事でしょう。実際そういう例がありますし。--ぱたごん会話2014年12月30日 (火) 13:17 (UTC)[返信]
なるほど、というか質問されるのと回答を繰り返している間に自分の認識が間違っていたのは気付きました。まぁでもそういう管理系業務は雑用の一種だからやりたくないとみんな言っていたらダメですし、管理者がどういう仕事をやっているのかということを一利用者として理解しておくのは有益ですし、管理系業務については関わっていきたいと思います。お手間かけていただいてありがとうございます。少なくとも自分の成長にはなりました。--I.hidekazu会話2014年12月30日 (火) 13:32 (UTC)[返信]

完全性定理に関する参考文献[編集]

完全性定理に関する文献を知りたい(ノート:ラッセルのパラドックス)とのことですが、ノートの使用目的とずれるので、こちらで紹介することにします。Gödel-Henkinの完全性定理については現代的なロジックの教科書であれば必ず載っています。以下に紹介する文献も「おすすめのロジックの教科書」と大差ないような気もします。

  1. 鹿島亮: 数理論理学, 朝倉書店 (完全性定理, 不完全性定理, カット除去定理, 非古典論理, Kripke意味論)
  2. 小野寛晰: 情報科学における論理, 日本評論社 (完全性定理, Herbrandの定理, 導出原理, 様相論理)
  3. 古森雄一, 小野寛晰: 現代数理論理学序説, 日本評論社 (Curry-Howardの対応, 正規化定理, カット除去定理, Glivenkoの定理, 完全性定理, 非古典論理, Kripke意味論, 代数的意味論, 普遍代数, 部分構造論理)
  4. 戸次大介: 数理論理学, 東京大学出版会 (完全性定理, Herbrandの定理, カット除去定理, タブロー法)
  5. 青山広 編著: 論理体系と代数モデル, 八千代出版 (代数的意味論, 完全性定理, Stoneの表現定理, Rasiowa-Sikorskiの埋め込み定理)
  6. R. M. Smullyan (高橋昌一郎 監訳, 村上祐子 訳): 数理論理学 述語論理と完全性定理, 丸善出版 (Königの補題, 完全性定理, Craigの補間定理, 定義可能性)
  7. 江田勝哉: 数理論理学―使い方と考え方:超準解析の入口まで, 内田老鶴圃 (完全性定理, 超積と超冪, 超準解析)
  8. 坪井明人: 数理論理学の基礎・基本, 牧野書店 (完全性定理, 超準解析)
  9. 田中一之 編著: ゲーデルと20世紀の論理学(ロジック) 2 完全性定理とモデル理論, 東京大学出版会 (完全性定理, Löwenheim-Skolem-Tarskiの定理, 量化記号除去)
  10. 田中一之, 角田法也, 鹿島亮, 菊池誠: 数学基礎論講義―不完全性定理とその発展, 日本評論社 (完全性定理, 再帰的関数論, 不完全性定理, 組み合わせ論的独立命題, 証明可能再帰的関数, 算術の超準モデル, 有界算術)
  11. 新井敏康: 数学基礎論, 岩波書店 (完全性定理, カット除去定理, 不完全性定理, Friedberg-Muchnikの定理)

([2][3][9][10]はとくにおすすめ) 完全性定理の証明はどれにでも載っています。上に挙げた文献には、Henkin拡大を用いた古典的なもののほか、超フィルター補題やKönigの補題を用いた証明など現代的なものも含まれます。Herbrandの定理は完全性定理のある種の精緻化であり、論理プログラミングの基礎でもあります。完全性定理から導かれるコンパクト性定理も重要な定理です。これは超準解析のほか超準モデルの理論への応用があります。コンパクト性定理の系としてはLöwenheim-Skolem-Tarskiの定理も重要でしょう。完全性定理を理解するには何より色々と応用してみるのがいいです。--Sillycrown会話2015年1月13日 (火) 16:50 (UTC)[返信]

なるほど。わざわざありがとうございます!オススメの一つの現代数理論理学序説は前々から気になっていたんですよね〜。ヒルベルト、アッケルマンは非常にいい本なのですが、やっぱり現代的な視点が抜けているので持っておかないと完全性定理を理解するには難がありますね。論理プログラミングの基礎のロビンソンの導出原理については長尾・淵の論理と意味を持っているのですが、エルブランの定理/導出原理がやっぱり一番の応用なんでしょうね〜。--I.hidekazu会話2015年1月14日 (水) 12:42 (UTC)[返信]

ウィキメディアンとしてのご経験とご意見をシェアする世界的調査[編集]

  1. ^ この調査では、ウィキメディア財団の現在の問題についてのご意見をお伺いするためのもので、長期的な戦略について論じるものではありません。
  2. ^ 法的事項: 購入の必要はありません。未成年者は参加できません。ウィキメディア財団 (149 New Montgomery, San Francisco, CA, USA, 94105) により後援されています。2017年1月31日に終了します。但し、禁止されている場所では無効。コンテストルールを参照するにはこちらをクリック

あなたのフィードバックが重要です:ウィキメディア財団のグローバル調査ご協力への最後のお願い[編集]

I.hidekazu さんへのコメント依頼[編集]

I.hidekazu さんへのコメント依頼を提出しました。--Hexirp会話2021年4月29日 (木) 06:39 (UTC)[返信]

中間子について[編集]

現在の素粒子物理では中間子は素粒子では無く複合粒子であり、核力も基本相互作用では無いとされます。強い相互作用を媒介する基本粒子は中間子では無くグルーオンです。現代素粒子物理の観点から言えば原子爆弾を理解する上で所謂、クオーク理論が登場する以前の中間子理論は不可欠、という訳では無いので文頭で特に強調する必要は無いと考えます。歴史的にも、まず戦時中に原子爆弾が完成して、戦後になって中間子が発見され湯川理論が「実証」されました。

2021年ウィキメディア財団選挙の候補者を紹介します[編集]

こんにちは!

2021年ウィキメディア財団選挙が8月に始まります。今年の理事会選挙は、2021年8月4日から17日まで実施されます。ウィキペディア日本語版の編集者を含むウィキメディア・コミュニティのメンバーは、3年の任期で4人の新しい理事を選出する機会があります。理事会選挙の開始に先立ち選挙運動期間が設けられており、この期間中にコミュニティが候補者と顔を合わせる機会があります。

  • ウィキメディア財団における理事会の役割は何ですか?
理事会の簡単な説明はこちらをご覧ください
  • 候補者紹介
今回の選挙には20名の立候補者がいます。候補者についてはこちらをご覧ください

理事選挙をサポートするファシリテーター チームは、選挙運動期間中にいくつかの活動を用意しています。
7月31日(土)の19:30(JST)から、日本を含むアジア・太平洋地域のユーザーが候補者と交流できるオンラインイベントが開催されます。日本語による同時通訳も提供される予定ですので、どうぞお気軽にご参加ください。

こちらのフォームから事前に参加登録をお願いします。
フォームのプライバシーポリシーをご確認ください。

その他の活動については、メタウィキの理事選挙ページをご覧ください。

ご質問がございましたら、ファシリテーター選挙ボランティアまでお問い合わせください。

選挙ボランティア一同 2021年7月24日 (土) 15:04 (UTC)

このお知らせは2021年ウィキメディア財団理事会選挙ボランティアにより作成され、botにより配信されました。 •フィードバック •購読解除

まもなく終了 理事会選挙へ投票のお願い[編集]

I.hidekazuさん

こんばんは。お忙しい時間帯に恐れ入ります。

2021年ウィキメディア財団選挙は最終盤に入っております。これまでご協力いただいた皆様、ご投票いただいた皆様に心より御礼申し上げます。

もしI.hidekazuさんが投票をお済ませでなければ、ぜひこちらから清き一票をお願いいたします。

ウィキペディア日本語版の運営にも深く関与する理事会の候補者の選出に際し、投票資格をお持ちの数少ないユーザーの一人であるI.hidekazuさんのご意見を反映することは非常に重要だと考えています。

投票いただくに際し、まず19名の候補者からI.hidekazuさんが支持する方をお選びください。 支持する候補者を選んだら、支持する順に候補者の名前を選び、投票ボタンを押すだけです。 所要時間は5分未満で、完全な匿名性が保証されます。

投票は、日本時間の9月1日(水)の朝9時に締め切られます。

ウィキメディア財団の運営にウィキペディア日本語版コミュニティの意見を反映させるために、I.hidekazuさんのご協力を重ねてお願い申し上げます。

どうぞよろしくお願いいたします。

--選挙ボランティア一同 2021年8月31日 (火) 11:17 (UTC)

このお知らせはウィキメディア財団2021年理事会選挙ボランティアにより作成され、botにより配信されました。 •フィードバック •購読解除

利用者ページのカテゴリについて[編集]

こんにちは。I.hidekazuさんの利用者ページ「利用者:I.hidekazu/直観主義型理論」ですが、Category:直観主義など通常記事(標準名前空間)で使うことが想定されているカテゴリが複数、付与されています。そのため、カテゴリページにてI.hidekazuさんの利用者ページが表示されてしまっています。Wikipedia:カテゴリの方針#カテゴリ編集の指針により、利用者ページには(書きかけの記事/下書き/Sandboxであっても)通常記事と同じカテゴリは付与しないことになっていますので、Wikipedia:利用者ページ#カテゴリ、テンプレート、リダイレクトを参考に利用者ページのカテゴリを<!---->で囲んでコメントアウトするなどの対処をお願いします。

1週間ほどお待ちしてもご対処いただけなければ、不躾ながらWikipedia:利用者ページ#他者による編集や削除依頼のガイドラインに従い利用者ページを他の利用者が直接修正させていただく場合もありますので、ご容赦ください。--Keruby会話2021年9月6日 (月) 17:57 (UTC)[返信]

ご連絡ありがとうございます。利用者ページのカテゴリも反映されるとは知りませんでした。該当箇所は削除してカテゴリページには表示されないようにします。--I.hidekazu会話2021年9月7日 (火) 11:23 (UTC)[返信]

翻訳記事における翻訳元表示のお願い[編集]

I.hidekazuさんが英語版から翻訳作業をなされている記事(直観主義型理論等)についてですが、Wikipedia記事がCC-BY-SAおよびGFDLでライセンスされているために、翻訳元記事の版指定または該当版への固定リンクを要約欄に記載する必要があります。今後の編集の際にはお気をつけいただき、もし可能であれば既に編集された分の補完作業をお願いします(補完作業自体は誰がやってもいいので、もしご都合が悪ければひとまず翻訳元とした版をお教えいただければと思います)。 具体的な作業手順等について詳しくはWikipedia:翻訳のガイドラインをご参照ください。--Merliborn (会話) 2021年9月18日 (土) 15:47 (UTC)[返信]

お知らせいただきありがとうございます。すでに翻訳してしまったものについて、ガイドラインに従い補完作業を行おうと思います。--I.hidekazu会話2021年9月19日 (日) 12:05 (UTC)[返信]

出典の明記のお願い[編集]

一般相対性原理』で I.hidekazu さんが 2022年2月21日 (月) 01:04‎ に追加した記述が IP:2400:4050:afe0:3700::/64会話 / 投稿記録2022年3月2日 (水) 05:21‎ の編集で除去されたのを見かけまして、こうして連絡させていただきます。ウィキペディアでは、記述を追加する際に、それらそれぞれに対して出典を付記する方法(個別参照)が推奨されております。このようなことはガイドライン「出典を明記する」で示されています。 I.hidekazu さんが 2022年2月26日 (土) 22:06 の編集の要約にて「具体例と出典を探して補填するようにします」と書いておられるように出典がないことを他の人に指摘されてから出典を探すというのは、 I.hidekazu さんが出典を示さずに編集しているということで、方針「検証可能性」に反してしまっている行為です。 I.hidekazu さんが、今後も、このような行動について指摘を受けているのにもかかわらず、このような行動を繰り返すならば、 I.hidekazu さんが投稿ブロックされる可能性があります。そのようなことにならないように方針「検証可能性」とガイドライン「出典を明記する」を守っていただけると嬉しいです。 -- Hexirp会話2022年3月2日 (水) 17:48 (UTC)[返信]

ご連絡いただきありがとうございます。記事は基本的に出典に基づいて記載しています。当該記事の一般共変性に関する記述についても、リーマン、リッチ、レビ=チビタ、アインシュタイン、マイヤー 著、矢野健太郎(訳) 編『リーマン幾何とその応用』共立出版、1971年。 のp.107,108に基づいた内容です。ただ、最初から共変的なテンソルを導入せず、一般的な物理表現から出発して、式の形が変わらないということとテンソルという要件が必要ということを説明するために書いた内容に疑義をもたれたという話です(加えて、検討しなおしたところ、ゼロテンソルになる導出が自明でないということもわかりましたが)。差し戻しされた匿名の編集者の方は、解析力学の記事で同じ物理現象を記述するラグラジアンでも直角座標 L(x,y) と極座標 L(r,θ) では L(x,y) = L(r,θ) と座標を変えてもイコールは成り立たないというあまり聞いたことがない立場に立たれています。Hexirpさんが匿名の編集者の意見を尊重された理由はなんでしょうか?--I.hidekazu会話) 2022年3月3日 (木) 14:24 (UTC) -- Hexirp氏のリンク先と表記が一か所間違っていたので修正しました。--I.hidekazu会話2022年3月4日 (金) 12:26 (UTC)[返信]
訂正します。ランダウ=リフシッツの力学はラグラジアンを座標系によって区別していました。自分の勉強した本は区別してなかったのでそちらが一般的だと思って書きました。--I.hidekazu会話2022年3月3日 (木) 15:40 (UTC)[返信]
お答えいただきありがとうございます。矢野健太郎の『リーマン幾何とその応用』の 107 ページから 108 ページを出典としているということ、了解しました。「匿名の編集者の意見を尊重された理由はなんでしょうか?」とのことで、この質問にお答えします。導入では ref タグを使って出典の情報が書かれていて「方程式の一般共変性」節では出典の情報が書かれていなかったので、「方程式の一般共変性」節には出典がないのだと判断したためです。このように誤解をしてしまったことをお詫びします。ただし、このような誤解を予防する意味合いも含めて、ウィキペディアでは、あらかじめ、ガイドライン「出典を明記する」において、記述を追加する際に、それらそれぞれに対して出典を付記する方法(個別参照)が推奨されております。 I.hidekazu さんが個別参照に従って「方程式の一般共変性」節に矢野健太郎の『リーマン幾何とその応用』の 107 ページから 108 ページを出典に使っていることを書いていただければ嬉しいです。 -- Hexirp会話2022年3月4日 (金) 06:58 (UTC)[返信]
ご回答いただきありがとうございます。参考文献には入れています。一括参照方式も認められているという認識ですが、個別参照が推奨されているのだから個別参照せよというお願いということですか?参考文献の内容を読み込んで各ポイントをまとめた形で記載する場合、個別の言明にその根拠を記載しようとすると脚注が膨大になったり、脚注のつけ方が難しいケースがあると思うんですがそういう場合もつけてくださいというお願いになるのでしょうか?なるべく沿いたいという気持ちはありますが、Hexirpさんはたびたびこういうお願いを、おなじようなケースを見つけた場合、編集者にお願いされているのでしょうか(いままで同様のお願いを何度かされてきたのでしょうか)?
話は変わりますが、正直に申しますと、最初私はてっきり議論に全然関係ない人がろくに何を議論しているのかもわからず暇つぶしでコメントしてきたのではないかと思ってしまいました。しかし、よく読むと以前に何度かやり取りした方で単にお願いをされてきただけということがわかり、これはすぐに全く私の誤解だとわかりました。Hexirpさんは利用者ページにあるようにプログラミングや数学基礎論にご関心がある人だと認識しておりましたが、一般相対性理論にもご関心がある上に一家言あるとは認識外でした。たびたび物理学の記事に関してもコメントをされてらしたんですね?
一般共変性原理について私の無理解を披露することになり恥ずかしいかぎりです。よければご意見いただきたいのですが、コメントいただきました一般共変性原理に関してうまく説明されている文献などご存じないでしょうか?--I.hidekazu会話2022年3月4日 (金) 12:26 (UTC)[返信]
私は「Wikipedia:コメント依頼/I.hidekazu」でガイドライン「出典を明記する」を守ることをお願いしており、今回のお願いをしたのも、その関連となっています。「一括参照方式も認められているという認識」ということですが、これは以前までその通りでしたが、しかし今では「Template:参照方法」のような注意喚起のテンプレートが存在するなど個別参照方式のみが適切なものであるということになっています。ひとまずここまでお答えします。 -- Hexirp会話2022年3月23日 (水) 12:30 (UTC)[返信]
ご返事いただきありがとうございます。まず「Template:参照方法」には、「出典が羅列してあると、記事のどの部分がどの出典を参照しているか分からないため、検証したり不要な出典を除いたりするのが困難になります。」とあります。これは一括参照方式の出典が多数存在する場合に、どの文言がどの出典に基づいているかわからないのでその是正を求めるテンプレートで、一般的に個別参照方式の出典をつけることを求めるものではないと思います。ただ、「出典を明記する」の方を改めてみると1月に改定されたみたいですね。確かに、「単に一括参照内で出典を明記しただけの文章については、Wikipedia:検証可能性を満たしているとは見なされません。」とあります。一括参照方式で出典は明記したつもりでしたがガイドライン改定されていたとは知りませんでした。
加えて、「私は「Wikipedia:コメント依頼/I.hidekazu」でガイドライン「出典を明記する」を守ることをお願いしており、今回のお願いをしたのも、その関連となっています。」ということですがつまり常時監視する必要があるのでしているということですか?--I.hidekazu会話2022年3月24日 (木) 15:04 (UTC)[返信]

投稿ブロック依頼提出のお知らせ[編集]

Wikipedia:投稿ブロック依頼/I.hidekazuを提出しました。--Kik会話2022年3月30日 (水) 17:41 (UTC)[返信]

独自研究を除去してください[編集]

あなたの執筆されたミルズの構造化プログラミングは独自研究が多いことが以下のように指摘されているので対応をお願いします。 Wikipedia:投稿ブロック依頼/I.hidekazuより引用

    • 前にも書きましたが「ミルズの構造化プログラミング」を直してくれませんか?現状は本文の内容だけで矛盾していますし、独自研究だらけのように見えます。これを放置した状態で、「私はこれからルールを守って活動する」のような宣言をされたとしても説得力に欠けますから、最初に手を付けて欲しいです。要出典等のタグをつけておいたのでどうか直してください。矛盾している箇所は、「連接・選択・繰り返しから構成されていれば検証できる」と「goto文を一行でも入れてしまうと検証できない」と「goto文のあるプログラムは連接・選択・繰り返しだけのものに必ず変換できる」という3つの両立しない主張が行われている点にあります。独自研究としては特に「ペール・マルティン=レーフは自身の直観主義型理論において、フローチャートの代わりにゲンツェン流の自然演繹を拡張したものを採用した上で、正しさを確認できるものとしての構造化文に代わるものとしてカノニカル表現(canonical expression)と呼ばれるものを採用している」は出典がないだけでなく内容も正しくないと思います。例えば、繰り返しを行う式として「natrec(a,b,c)」がありますが、これは非カノニカルです。https://www.cse.chalmers.se/research/group/logic/book/book.pdf のAppendix AからCを読めば確認できます。--Kik会話) 2022年4月14日 (木) 19:04 (UTC)
      • コメント ここでいう「検証できる」とはどういう意味なのでしょうか。Whileプログラムのような言語はホーア論理のような形式検証の体系で検証できるということでしょうか。(ホーア論理はWhileプログラムのために作られた体系なのだから当然ですが。)Whileプログラムのループ構文ではループ不変条件を見つけることによって検証が進みます。これは数学的帰納法における帰納法を適用する論理式を探す作業と本質的には同じことですから、前後の文中で数学的帰納法云々に言及していることと整合的です。しかしSpecial:Permalink/78826085#cite_note-14の「ここで、順次プログラムの中にgoto文を一行でも入れてしまうと、数え上げ推論による正当性検証ができなくなってしまい、「ソフトウェア全体の正しさ」というものが原理的に定義できなくなってしまう」は意味不明ですし出典もありません。さらに、これも言うまでもないことですが、Hoare論理以外を使ってソフトウェア全体の正当性を証明することは当然できます。そのプログラム言語の言語仕様が数学で取り扱える程度に形式化されて記述されているのなら、そのプログラムの正当性というものを数学的に記述し、それを数学的に証明したり反証したりすることは可能です。たとえば計算可能性理論でよく用いられる計算モデルであるレジスタマシンはgoto構文を持ちます。この言語で書かれたアッカーマン関数のプログラムが正しくその関数を計算すること(正当性)は数学的に証明できますよね。通常の数学的命題なのですから。(もちろん正当性を表す命題が独立命題となってしまうケースもあるわけですが。これはホーア論理にしても同じことです。)ホーア論理のようなものをジャンプ命令を持つような言語に対して定義しようとすると著しく難しい、ということはあるかもしれませんが、そうだとしてもそのことを述べている信頼できる文献を挙げるべきです。なおSpecial:Permalink/78826085#cite_note-12の「この数学的帰納法を用いる検証については計算機による自動化を行うことができる」は偽です。失敗の可能性のあるヒューリスティックなアルゴリズムないし停止しない可能性のある半決定アルゴリズム(正当性の証明か反証が見つかるまで全証明を探索し続ける)ならありますが、完全自動化は不可能です。このことはライスの定理からも明らかでしょう。以上の点からミルズの構造化プログラミングの編集内容の信頼性に問題があるという主張に同意します。 --Sillycrown会話) 2022年4月15日 (金) 15:15 (UTC)

独自研究を載せないというのはウィキペディアの基本となる方針ですので、参加者には必ず守って頂く必要があります。独自研究であると指摘されているにも関わらず自主的に除去しない場合も間接的に独自研究を載せているのと同じですので、I.hidekazuさんには自らすすんで除去の作業を行って欲しいです。この作業をどうしてもやりたくないと言う場合はそのように書いてください。代わりに私が作業を行います。ただし、このことによってI.hidekazuさんは基本方針を守る気がない参加者であると他の参加者に認識される恐れがあることを伝えておきます。複数の参加者から方針を守るように説明されても理解されない場合はコミュニティを消耗させる利用者としてブロックされます。WP:NORに明記されているように「独自研究ではないことを示す唯一の方法は、その記事の主題に直接関連のある情報を提供している信頼できる資料を参考文献として記し、その資料に記された内容に忠実に記述すること」ですので、他にも独自研究を載せてしまったかもしれないという心当たりがある場合は自分から直してくれることを希望します。--Kik会話2022年4月21日 (木) 14:20 (UTC)[返信]

  • 投稿ブロックの審査中に?なんで?--I.hidekazu会話2022年4月23日 (土) 14:33 (UTC)[返信]
    • 投稿ブロックの審査中は記事をそのままの状態で残しておかないというルールは無いと思うので関係ないんじゃないでしょうか。独自研究を載せないというのはウィキペディアの基本方針ですから、それが守られている状態を維持しないといけないわけで、「ミルズの構造化プログラミング」は早めに修正する必要があります。以前コメント依頼でこういう発言(特別:差分/83260983)がありましたので、「ミルズの構造化プログラミング」はこちらで対応する前に確認を取っているのです。この発言は当然「問題のある記事を修正する予定だったが、ちょっと時間が取れなかった間に修正されてしまった。それを尻拭いと言われるのは遺憾である」という意味だと私は理解していますので、I.hidekazuさんが対応する予定があるのかどうか確認しているのです。--Kik会話2022年4月23日 (土) 20:22 (UTC)[返信]
  • 投稿ブロックの審査中に記事編集しろというのはどう考えてもおかしい。ただ、修正しろというなら修正しないでもないが、記事編集自体は投稿ブロック審査のクローズ後である。とりあえず、ここでは矛盾しているという指摘に対して反論し、クローズ後に記事に反映させるという段取りを考えるものとする。あと、話がごちゃごちゃになるし時間も一気にそんなかけられないので1点づつ書く。
Q.「検証できる」の意味は?
→ ベースにあるのはダイクストラの構造化プログラミングであり、検証できるの意味はダイクストラの意味で検証できるという意味だ。つまり、3つの知性の道具立て(数え上げ推論、数学的帰納法、抽象)の3つでできる確認方法のことを言っている。3つの構造化文は数え上げ推論と数学的帰納法を使えば正しさを確認できるし、それらを大規模に組み合わせたフローチャートもネストさせれば残る道具立ての抽象をつかって全体のプログラムの正しさは確認できる。ただ、goto文は、C言語でいうところのbreak文とかcontinue文、例外処理など局所的な決まった使い方であればまだしも、無規則・無秩序としか言えないような一般的分岐命令としては、「人間の能力では」正しさを確認する手段がないということだ(特別な直観をもつプログラマが、第六感的にgoto文の正しさを確信できるということはありえるかもしれませんが、ダイクストラはあくまで人間の能力には限りがあるという前提に立っているので、使える道具立ては普通の教育課程を受けた人間が使える道具にかぎられます)。
ただ、構造化プログラミングの本で「検証」という用語をダイクストラは使っていないので「プログラムの正しさの証明の理解」と言い換える、あとは該当箇所には「ダイクストラは」とつけて対応することを提案する。
(1)「連接・選択・繰り返しから構成されていれば検証できる」、(2)「goto文を一行でも入れてしまうと検証できない」、(3)「goto文のあるプログラムは連接・選択・繰り返しだけのものに必ず変換できる」
この3つが矛盾しているということだが、(1),(2)はダイクストラの立場で一貫している(矛盾してない)。問題だと言いたいのは(3)のことだろう。つまり、いいたいこととしては機械的にgoto文を構造化文の構成に等価変換したプログラムであれば正しさを検証できるはずなんだから、goto文が含まれたプログラムであっても「プログラムで機械的に等価変換させることをすれば」正しさは確認できるはずなんだから話が矛盾しているんじゃないかということであろう。ダイクストラは「goto文有害論」の最後の方にプログラムの機械的な自動変換を推奨していないことからわかるように、「プログラムでの機械的な等価変換」みたいなことをすることは前提にしていない。なので、脚注「goto文を含むプログラムの正しさを他者に証明して納得させる方法がないからである」というのはダイクストラの立場的なプログラムでの機械的な等価変換を許さないという前提の言明であり、別に矛盾はしていない。ただ、前提はわかりにくいかもしれないので当該脚注に前提を記載することを提案する。--I.hidekazu会話2022年5月16日 (月) 16:42 (UTC)[返信]
とりあえず、現状の本文を素で読むと(1)(2)(3)が矛盾してるように読めるというのは理解いただけたようでよかったです。(1)「連接・選択・繰り返しから構成されていれば検証できる」というのは本当に正しいのですか?私の勘ではプログラムの構成要素が何であるかというのは、検証できるかどうかの決定要素ではないのではないかという感じがします。以前にリュカ–レーマー・テストの証明された実装をCoqで書いたことがあるのですが、プログラムとしては繰り返しが1個と分岐が1個と四則演算が少しの8行しかない簡単なものであるにも関わらず、証明には2週間ぐらいの手間がかかりました。「3つの知性の道具立て」があるから検証できるはずでしょと言われても無理に決まってるじゃんとしかいいようがないです。何が言いたいかというと、プログラムの正しさというのは「プログラム自体」だけをパラメータとして考えているのではなくて、示したい「プログラムの性質」とか「プログラムの仕様」いったものとの組がパラメータとなっています。そのため、「リュカ–レーマー・テスト」の検証の場合は「テストはリュカ数列のp-2番目の値がMpで割り切れるかどうかを返す」という性質と「テストはMpが素数であるかを返す」という性質とでは検証の難易度が大きく違うのです。つまり、プログラムの構文の構成要素がなんであるかなんていうものが検証できるかどうかやその難易度に与える影響なんて微々たるものなのです。それにも関わらず、ミルズの構造化プログラミングの本文ではまるでプログラムの構文の構成要素がなんであるかが検証に決定的な影響を与えているがごとく書いてあり、しかも証明したい性質についての言及が全くなく強い違和感を感じます。ダイクストラが本当にこのような主張をしていたとは思えません。そこで、まず出典を明らかにすべきではないでしょうか?
他にも最近流行っていた https://arxiv.org/abs/2110.01111 のソートアルゴリズム
for i = 1 to n do
  for j = 1 to n do
    if A[i] < A[j] then
      swap A[i] and A[j]
これの証明つき実装も書いたのですが、これはループ不変条件が大変複雑でした。自動証明なんてとても不可能ですし、「数学的帰納法」を使えば確認できるなどというのも軽率だと思うのですが、やはり本文ではプログラムの構文の構成要素が繰り返しなんだから数学的帰納法でできると理由もなく書いてあります。これもダイクストラが言ってるとは思えませんので、出典が必要だと思います。また、このプログラムの2重のループと分岐は互いに複雑に影響しあっていて、関数に分離して抽象化によって検証が簡単になることもありません。私の感覚では、抽象化によって証明が簡単になるのは構文的にネストされた構造であるかとは関係なく、抽象化してくくりだした部分の仕様が単純であるかどうかで決まるのではないかと思います。それについてもダイクストラは何か言ってないのでしょうか?とにかく必要なのは記述の補足を追加することやダイクストラはこう考えていたはずだではなくて、出典を明記することであることを理解してください。--Kik会話2022年5月17日 (火) 13:24 (UTC)[返信]
Sillycrown氏の指摘になんで的確にこたえられるのか不思議ですが、回答します。
書きましたように「検証」と書いたのは不適切でした。ダイクストラは「検証」とは言っておらず「プログラムの正しさの証明の理解」というように、プログラムを証明と見立てて人間の力で確認する(プログラムを理解する)ことを問題視しています。
出典と言われれば、
いままで3つの型の分解をみてきました。それらは、おのおの連接(concatenation)、選択(selection)、繰り返し(iteration)とよべるでしょう。最初の2つは数え上げの推論で、また最後のは数学的帰納法で理解されます。
構造化プログラミング(1975) p.22
と主張しています。
そもそも、ダイクストラの構造化プログラミングの立場というもの自体が、
ここで、正しいプログラムを作り出すばかりでなく、納得のいくやり方で正しさを証明するのがプログラマの仕事であるという立場に立てば、上述のことは、プログラマの活動に深くかかわり合いをもちます。つまり、プログラマが作り出すものは、うまく構造化されていなければならないのです。
構造化プログラミング(1975) p.6
というもので、「プログラムの正しさを証明する」という行為は一般のプログラマの仕事であると言っています。当時は形式手法もないわけで、意味するところはそれこそ高校数学もしくは大学学部レベルの数学の証明を目視して確認するという行為のことを指しているわけです。
「検証」という用語は、「実現が仕様を満たしていることを証明すること」と定義されます(『ソフトウェアクリーンルーム手法』(1997)二木厚吉著)が、そういう見方が出てきたのはホーアのホーア論理以降であり、年代的に後の話です。
ダイクストラが本当にこのような主張をしていたとは思えませんということですが、そもそもプログラムの証明と書いたからといって、それと現代的な形式手法で証明したらどうだという話を比較されても意味ないでしょう。それにしても構造化プログラミング読まずに、信じられないから独自研究だとつけているんじゃないですか?--I.hidekazu会話2022年5月18日 (水) 16:55 (UTC)[返信]
あまりにコメントの内容がひどいので一か所だけにしますが、「そういう見方が出てきたのはホーアのホーア論理以降であり、年代的に後の話」であるから、ダイクストラが「プログラムの仕様」と「プログラムの実装」を比較して何かしらの正しさについて議論しているはずがないという主張だと思いますが、そんな無茶苦茶な話があるはずないでしょう。「仕様」と「実装」を比較せずにプログラムの「検証」だとか「テスト」だとか「内容の理解」だとか「人へ説明」だとかプログラムに関する議論することが不可能であるのは、時代にかかわらずプログラミングの常識です。こんな根本的なところから間違っているのに議論している気になってるのは本当に不快です。これ以上続けても時間の無駄なのでこの話はもうやめましょう。--Kik会話2022年5月19日 (木) 12:44 (UTC)[返信]
では次の言明「この数学的帰納法を用いる検証については計算機による自動化を行うことができる」について書きます。
私もテクニカルタームの「検証」とダイクストラの言う「プログラムの正しさの証明」とを混同していたところがありますし、ライスの定理というのは知らなかった(記事読んでも詳細はあまり理解できてないですが)ので、この脚注については削除してもいいです。SPINモデルチェッカを念頭に置いたつもりですが、Spinは正直そんなによく知らないので、そんな頑張るつもりもないです。--I.hidekazu会話2022年5月21日 (土) 12:45 (UTC)[返信]
次に進む前に上のを問題を解決してからにしてくれませんか?このまま上の話をうやむやにして放置するという今までのあなたのやり方はもう通用しないので、解決するまで他の話題の話をする気はないです。--Kik会話2022年5月21日 (土) 14:01 (UTC)[返信]
「そういう見方が出てきたのはホーアのホーア論理以降であり、年代的に後の話」、Floydの論文は1967年、ホーアの論文は1969年。ダイクストラのgoto文有害論は1968年で逆。
Floydがプログラムを一つの入力に対して一つの出力に限定しろと主張しているかどうかはしらない。--I.hidekazu会話2022年5月21日 (土) 14:14 (UTC)[返信]
それはもう聞いたので、トンデモではなく常識ベースの話をする気になったら呼んでください。--Kik会話2022年5月21日 (土) 17:08 (UTC)[返信]
「この話はもうやめましょう」というので次の話題にしたら「上の問題を解決してからにてくれませんか?」と言い出して結局「それはもう聞いた」というのはちょっと理解しがたい態度だ。気分で(投稿ブロックの)審査をしているとしか思えない。これは本当にWikipedia:投稿ブロック依頼/I.hidekazuの審査の一環なのか。
人には言明の出典を強く求めるくせに、自分の発言には気分でころころかわったり、根拠をつけないというのはやめてもらいたい。例えば、このゲーデルの不完全性定理の記事におけるリバート(特別:差分/54188939)などはちゃんと根拠ある出典の言明を記載しているところを理由なく行っている。これはどういうことかその理由を求めたい。嘘つきパラドックスを通して一般読者を啓蒙することを目的とした本(長いので以下「嘘つき本」という。)を書いているような著者ではないかもしれないが、権威ある学者の著作の言明であり、理由なく消すというのは全く納得できない。常識は自分の気分で決めるというつもりだとしか思えない。はっきりいっていったい何がいいたいのか全く意味がわからない。--I.hidekazu会話2022年5月23日 (月) 14:17 (UTC)[返信]
なんでそんなにゲーデルの業績を過小評価した記述をやりたがるんですか?意味が分からないんですが、ゲーデルに何か恨みでもあるとかなんですか?--Kik会話2022年5月23日 (月) 15:05 (UTC)[返信]
過小評価も過大評価もしないです。中立的な観点から記述するというのがウィキペディアの方針ですので、ゲーデルの不完全性定理が出てくる背景の当事者の一人であるヒルベルトの著作を出典に記述しました。なんでゲーデルの不完全性定理の意義を具体的に書いたらゲーデルに恨みがあることになるんですか?
逆に聞きたいのですが、数学基礎論とか圏論の記事のメンテナンスと称する編集は、私事じゃなくてなんかの仕事でやってないですか?すごく不自然なんですが。--I.hidekazu会話2022年5月25日 (水) 15:00 (UTC)[返信]
ノート:ラッセルのパラドックスSillycrownさんが7年前にすでに説明しているはずなんですが、他人の助言を聞いても復習するという行為をやってないですよね。今まで他人から説明を受けて復習してない項目が大量に積みあがってますよね。そんな状態でどうして追加の説明を受けられると思ってるんですか?--Kik会話2022年5月25日 (水) 18:40 (UTC)[返信]
つまり、Sillycrown氏の説明を理由に取り消したということですね。理由言わないとわからんよ。不完全性定理の系として紹介する分には問題ないわけですね。数理論理学の編集については理由なく無条件で消すつもりなのかと思っていたがそうではないかは、まだわかりませんね。てっきり嘘つきパラドックスに何らかの理由ですごく思い入れがあるのかと思ってました。
それにしても、あなたは他人から説明受けたらなんでもかんでも全部はいそうですかって了承するのですね。そんな純朴な方だったとは思いもよりませんでした。--I.hidekazu会話2022年5月27日 (金) 15:11 (UTC)[返信]
復習するって言葉も通じませんか?例えば、ノート:ラッセルのパラドックスのSillycrownさんのコメントなら、「不完全性定理は二階述語論理が(標準的意味論に対し)完全でないことを述べた定理ではありません。」に対しては不完全性定理のステートメントを確認します。私はちゃんと確認しました。「系として導けることは確かですが不完全性定理として紹介するのは不適切」も系となってることを確認しました。「二階述語論理が(強い意味で)完全ではないことは不完全性定理に訴えるまでもなく証明できます」も証明を読んで確認しました。なぜstandard semanticsだと超準モデルを持たないかなどの行間も埋めました。より強く範疇性があることも理解しました。Henkin semanticsだと完全になることは一階の場合と同じ感じで証明できそうという気分にはなりました。少なくともstandard semanticsより多くのモデルがあるので完全性が成り立ちやすくなることは理解しています。数学の項目を編集しているほかの人たちもみんなちゃんとやっているはずです。「あなたは他人から説明受けたらなんでもかんでも全部はいそうですかって了承するのですね。」なんて暴言は一体どこから出てくるのですか?数学をやっている人間はみんな https://www.ms.u-tokyo.ac.jp/~yasuyuki/sem.htm をマスターして卒業しています。
そもそも、この完全性ってヒルベルトプログラムの役に立つんですか?有限の立場からはほど遠いところで完全性が導けて何がうれしいのかよくわからないんですが。それに比べて元の不完全性定理は有限の立場に近くてヒルベルトプログラムにとっても重要なのは分かるのですが、なぜわざわざ有限の立場から遠い二階述語論理の完全性の否定に使おうとするのか意味が分からないのですが。--Kik会話2022年5月28日 (土) 12:00 (UTC)[返信]
ヒルベルト・アッケルマンの『記号論理学の基礎』にそう書いてあるからだと言っているでしょう。ではそれは確認したんですか?当の本人の一人であるヒルベルトのゲーデルの不完全性定理の解釈がそうであるならそれを書くのは当然でしょう。そもそも、記号論理学の基礎では命題論理、第一階述語論理、第二階述語論の真偽決定問題を問題にしていて、記号論理学の基礎の話の流れからいえば、ゲーデルの不完全性定理の意味は第二階述語論理が不完全という系が導かれるというのはぴったりパズルのピースのように当てはまるのだからそれを無視するというのは明らかにおかしい。ヒルベルト研究者だとも標榜しているゲーデルの研究者である京都大学の某教授もそこを意図的に無視しているのも明らかにおかしい、わざとやってる。ミルズの構造化プログラミングもそうですが、当事者の時代の後の道具を持ってきて話をわざとごちゃごちゃにしている。随伴関手の意味するところもそうですが、隠したいことがあるのが透けて見えるのであるから、それをはっきり白日の下にさらそうとしているわけで、それに仕事として妨害をかけてくるのは全く理にかなっているが、これは常識ベースではないので無視すべき話であるわけでしょう。--I.hidekazu会話2022年5月28日 (土) 13:33 (UTC)[返信]
上の質問はどうせ常識ベースではないとでもいって無視するでしょうし、時間の無駄なので、回答を続けます。
「ペール・マルティン=レーフは自身の直観主義型理論において、フローチャートの代わりにゲンツェン流の自然演繹を拡張したものを採用した上で、正しさを確認できるものとしての構造化文に代わるものとしてカノニカル表現(canonical expression)と呼ばれるものを採用している」ということですが、ここで言いたいのは「正しさを確認できるもの」、言い換えると判断できるものが、ダイクストラの構造化プログラミングだと構造化文であるけれど、マルティン=レーフの体系だと命題に対するそのカノニカルな証明だと言っているのです。ダイクストラの構造化プログラミングの構造化文を直観主義型理論にそのまま置き換えてそれが肯定的判断が可能かどうかということを問題にしているわけではありません。
独自研究になるので書いていませんが、マルティン=レーフの型理論というのは、要するにホーア論理の表明(assertion)をカリー=ハワード同型対応よろしく型としての命題(proposition-as-type)のテーゼに沿って表明部分を型に置き換えて、自然演繹部分をダグ・プラウィッツ流の自然演繹で置き換えたものというのが皮相的なアイディアの一部だと思うので、構造化プログラミングと無関係というわけでもない(ホーア論理)と思います。
読み返すと唐突な感じもするので、ここも別に削除してもいいです。そんな頑張るつもりもないです。--I.hidekazu会話2022年5月25日 (水) 15:21 (UTC)[返信]
「構造化プログラミングだと構造化文」「マルティン=レーフの体系だと命題に対するそのカノニカルな証明」と書いていますけど、後者は「Aに対するB」なのに前者は「B」単独なんですか?本当は前者ではAのところにプログラムの仕様が入ってくるんじゃないのですか?--Kik会話2022年5月26日 (木) 11:49 (UTC)[返信]
自分もそうは思うが、ダイクストラはそんなことは全く言ってない。ぜんぜん書いてないことをもっともらしく作文するというのはそれこそ独自研究になる。この記事については独自研究をしろとでも言うのか?あなたがいったい何を聞きたいのかさっぱりわからない。--I.hidekazu会話2022年5月27日 (金) 15:14 (UTC)[返信]
変だと思うところがあるならちゃんと復習してくださいよ--Kik会話2022年5月28日 (土) 12:00 (UTC)[返信]
おかしいことというなら、そもそもマルティン=レーフの型理論は正しいのか、非常に怪しい。主張内容が一介のコンピューターサイエンティストが理解できる範囲を超えているし、理解しているというのも胡散臭い。龍田真の『型理論』とレイモンド・ターナーの『人工知能と論理』という本を持っていてそれぞれマルティン=レーフの型理論の解説が乗っているが共通性がほとんどない。そもそも命題を集合に置き換えても同様の判断ができるらしいが「Aは集合である」はそもそも命題なんだから、命題をそのまま集合に入れ替えられるというのはかなり眉唾。さらにいえば、ブレンターノを引かないと判断形式云々についてなんにもいえないはずだけれど、ブレンターノの著作はほとんど隠されていてアクセス不可能。
さらにいえば、ブラウワーの直観主義の元ネタはどう考えてもブレンターノかフッサールの現象学で、ヒルベルトはカントに通じていたという話だったんだから、数学基礎論争はブレンターノV.S.カントの哲学論争だともいえるわけだけれどもなぜかだれもその点を突っ込まない。わからない。というのならなんでマルティン=レーフの型理論を賛美するのかわからない。ゲーデルの不完全性定理の俗説の理性の限界を示したというのも、カントの純粋理性批判が元ネタだと思われるがなぜかだれも言わない。
なんか言うと都合が悪いことがあるんだろうなーとは思うけれど、それを言って無期限ブロックでも食らったらたまったもんじゃないと思って言っていないわけで、わざわざなんで言わせたいのだろうか?--I.hidekazu会話2022年5月28日 (土) 13:45 (UTC)[返信]
マルティン=レーフの型理論は定義ですので、正しいのか正しくないのか言及すること自体的外れです。定義が正しくないという言葉遣いは、すでによく知られている常識的な定義があって、それを学生が間違って覚えていたときにその定義は間違っているというような状況で使う表現です。型理論のように新しい定義を作ったときに、それが正しくないというような議論を行うことはありません。古いバージョンは矛盾が導けたという話があって、それは定義がよくなかったわけではありますが、そういうのを正しくないというのは言い過ぎだと思います。新しいバージョンでは証明されているかは知りませんが、修正されていると聞きますし正しくないというのはおかしいと思います。
「式と型」「証明と命題」「元と集合」の所属関係はみんな同じ規則で(健全に)導出できるので、型と命題と集合を入れ替えてもいいのは当然なのですが、何を問題にしているか分かりません。
「Aは集合である」が命題であるというのはなぜですか?まず「Aは集合である」というのはメタ理論の文なのか対象理論の文なのか全然分からないです。メタ理論の文なら普通の数学ですので、ZFCでは「Aは集合である」は普通の数学用語としての命題ではないです。対象理論の文なら「Aは集合である」みたいな表現が命題なのかどうかを判定するような構文はないはずです。
判断の定義はマルティン=レーフの型理論に完全に書いてあるので、他の文献をあさらないと読めないということはないと思います。
哲学の部分は私は何も知りません。
マルティン=レーフの型理論を誰が賛美しているのか知りませんが、私は正直使いにくいと思いますよ論文もこれでもかというぐらい読みにくいし。calculus of constructions (CoC)を学んだ方がはるかにいいと思うのですが・・・--Kik会話2022年5月28日 (土) 17:57 (UTC)[返信]
正しい、正しくないが不適当だというなら、マルティン=レーフの型理論はそれらしい言明の寄せ集め理論、だと思います。マルティン=レーフ自身が異様に判断(judgement)にこだわるのは、マルティン=レーフの型理論自体を勉強しようとする当人がその妥当性を判断せよ、と暗にヒントを出しているからなんじゃないかと思います。ゲーデルの不完全性定理の解説本で「噓つき」のパラドックスをやたら強調してくることも同様の感想を抱きます。
Aが命題、aがその証明であるとき、a:Aに対して肯定的なり否定的判断を下すというのは理解できます。Aが仕様、aがプログラムでも納得はできます。でもAが集合、aがその要素でa:Aに対して判断を下すというのは、はっきりいえば意味不明だと思います。この場合そもそもなにを判断するのか理解しがたいです(なのにマルティン=レーフは知る限りなにも注釈をつけてない)。
かろうじてAをもってこれは「Aは集合である」という言明の省略表現だというのならかろうじてわかると思ってそう書きました。メタ理論、対象理論で云々の話は正直よくわかりません。
AgdaやNurPRLはマルティン=レーフの型理論に基づいているといわれますし、NordstromのProgramming in Martin-Loef's type theoryはまるでマルティン=レーフの型理論がプログラミングにすぐに活かせるかのようなタイトルです(これも読んでもよくわからない)。Nordstromは少なくとも賛美しているんじゃないでしょうか。
マルティン=レーフの論文は確かに何言っているのかよくわかりません。比較的まだなんとか読めるのが哲学的な部分だったのでそこを中心に読んでいましたが、他は正直読む気がしない。Calculus of Constructions(CoC)をご紹介いただいてありがとうございます。ただ、正直、ここら辺の分野は、なんだか喩えると流体力学を実解析だけで説明する試みのような印象を受けるので、まともにやる気はないです。常識ベースの話でなくなりますが、まったく別アプローチの簡単な方法が存在している気がしてならないです。複素数化した論理学とか。一般確率論相当のものが数理論理学にあるのではないかと疑っているということです。
やるなら、圏論も考えてグラフ理論でしょう。もしやるのであれば、4色問題のコンピュータでの証明とかが多分入り口として正しい気がします。説明できるような根拠は提示できませんが。--I.hidekazu会話2022年5月29日 (日) 15:00 (UTC)[返信]
そりゃ命題論理のところからあの状態じゃ何もわからないに決まっています。特別:差分/48710733/48750884の復習を先にしないと絶対に無理です。これ何度も言ってるはずなんですがいつやるつもりなんですか。--Kik会話2022年5月29日 (日) 17:35 (UTC)[返信]
何度も聞いた記憶はないですが、十中八九やるつもりはないです。数理論理学はマルティン=レーフの型理論を理解したいという理由で勉強していましたが、上に書いたように最近疑念の方が強くなっているのでやる気ありません。数理論理学は発展経緯がよくわからず歴史的経緯の部分もかけないので、いまいちモチベーションがでないです。数学基礎論としても、最近自分は論理主義でも形式主義でも直観主義でもない経験主義者だとわかり、具体的応用がわからない理論はやる気がしないです。トンデモ数学でよければ、スペンサー・ブラウンの形式の法則の方がまだやる気あります。
あと書きたいのは、個人ページに書いたこれから書きたかった記事ぐらいです。せめてクラス (コンピュータ)の記事は書き直したいのでいい加減審査終えてもらえないですかね。--I.hidekazu会話2022年5月30日 (月) 13:09 (UTC)[返信]
「いまいちモチベーションがでないです」みたいな大事なことは最初に言ってくれませんか?そしたらわざわざここが間違ってるとか説明とかしないですみますから。--Kik会話2022年5月31日 (火) 14:23 (UTC)[返信]
ずっと書いてなかったでしょう。やたら数理論理学的なところを煽ってきたので、不完全性定理の話を振ったわけです。--I.hidekazu会話2022年6月2日 (木) 15:08 (UTC)[返信]
ずっと書いてないといいますが、ここ最近の2週間ほどずっと基礎論かその親戚みたいな話しかお互い書いてないじゃないですか?煽ってたというのはどこの話ですか?--Kik会話2022年6月2日 (木) 18:21 (UTC)[返信]
なぜかミルズの構造化プログラミングの話で、その基礎論かその親戚みたいな話しか指摘してこないことを煽っていると言っているわけです。記事の独自研究を問題にしているのに、記事と関係ない独自研究的なことを指摘していたのはなにか理由があったのではないですか?不自然すぎると何度か書いたと思いますが。--I.hidekazu会話2022年6月3日 (金) 14:45 (UTC)[返信]
唐突に不完全性定理の話を振ってきたのはそちらでしょう特別:差分/89659932。それまではダイクストラの話してたじゃないですか。だいたい、不完全性定理の話にしても構造化プログラミングにしても、ノート:ラッセルのパラドックスノート:構造化プログラミングですでにおかしいことが指摘されているのに、なんでわざわざ私が追加でこれ以上説明しないといけないんですか。昔から変わらず他の人のコメント読む気ないですよね。「記事と関係ない独自研究的なこと」とは何の話ですか?何が不自然なのかさっぱりわかりません。こちらは具体的に復習して欲しいところを書いているんですが、そちらももっと具体的に書いてくれないとエスパーじゃないのでさっぱりわかりません。--Kik会話2022年6月3日 (金) 20:16 (UTC)[返信]
だから、構造化プログラミングの話をしているのに数理論理学的な話をやたらしてくるのは話が外れているでしょう。そこで唐突に不完全性定理の話をしても、話が違うというわけでもなく、そのまま話をすることに応じてきたようなそぶりをするのは、構造化プログラミングの話はどうでもよくて結局数理論理学の話がしたいだけだと思われて当然と言えます。
あれだけワーワーしつこく絡んできたのに「記事と関係ない独自研究的なこと」がなにかわからないんですか?仕様とプログラムの関係です。正当性の確認方法のためかしりませんが、そんなことは構造化プログラミングの本に書いてありません。なんで書いてないことを独自研究的に書かないといけないんですか?
昔から都合が悪くなると話を逸らそうとするのは辟易です。エスパー云々はこっちのセリフです。一字が万事エスパーしないと何言いたいのかさっぱりわからない、だからこっちが聞き出さないと意味わからないです(やりとりしている間にリバートかけてくるので最近はその気力もなくなってきましたが、やりとりしている最中にリバートかけるのはルール違反です)。例えば、ミルズの構造化プログラミングのこの指摘特別:差分/89029942。これだけでなにが独自研究か詳細わかれといってわかりますか?
これだけの指摘からエスパーできた利用者:Sillycrown氏にはすごいなと思いますが、なんで数理論理学的な意図もくみ取って補足できるんですか。今まで証拠もないから黙っていましたが、これ同一ユーザーなんじゃないですか?関心領域にプログラミングなんて入ってないし、なんで構造化プログラミングの話に唐突に補足できるんですか。--I.hidekazu会話2022年6月5日 (日) 15:29 (UTC)[返信]
正しいプログラムであると主張するのは仕様と実装を比較しないと不可能であり、実装だけ見てこれは正しいプログラムであるということはできないってことをこれ以上説明しないとだめなんですか?時間の無駄ですから常識をまず身に着けてくれませんか。
説明してもそちらは読まないんだからするだけ無駄ですよね。昔のノート:図式_(圏論)なんて、こちらが「このドメインの圏 J のことをこの図式の添字圏 (index category) やスキーム(scheme)と呼ぶ。」という文にスキームが何なのか書いてあるって何度説明しても読みませんでしたよね。この1文を読んでスキームが何か理解するのにエスパー力は必要でしたか?読めばわかりますよね。もともと読む気がない人に説明するなんて時間の無駄でしかありません。結局これも復習されることなく放置されていますね。前のds/dtが0になるってのも、「sをtで微分したら0になり矛盾します。微分というのはこれこれこういう風に計算します。これに従って計算したらかくかくのように0になりました」って説明が必要だったんですか?結局、これも復習せずに放置する気ですよね。--Kik会話2022年6月5日 (日) 17:52 (UTC)[返信]
また話を逸らされるわけですね。うんざりです。どっかで誰かと相談してるんじゃないですか。
いいですか。私にはデメリットがないので微に入り細に入り説明すれば、図式スキームというのは(多重)有向スキームのことであってこれは前圏と同じ意味でいいわけで、それは圏論の基礎にも書いてあるわけですからそこについてとやかくいわれるいわれはなく、いったい何を問題にしているのかどういうスキームかどうかときかれても図式スキームとどういうスキームであるかどうかという意味が違うと言われてもこの文脈では違うという話はリンク先ではよくわかってないわけで、つまり圏とは前圏を拡張したもので前圏と圏とは密接な関係であるわけでグラフ理論と圏論という関係についてオイスティン=オアとマックレーンの関係がどのうこうのということは、一部しかわかっておらず、いうなれば随伴してれば忘却関手なりで構造を忘れてグラフの世界に言って解いてから戻ってくればいい話であって,つまりマックレーンの圏論の基礎の不自然なところは随伴に関する記述であって、でもだからといってそれは大まかなスキームについて書かれた文献は見つけられても具体的にどうすればいいかということについてかかれた本にリーチしているわけではないわけで,つまり構造化プログラングと関数型あプログラミング、圏論についての合流点という最も大事で私も非常にあ関心を抱いているということが一目瞭然なことに触れれば、O'CAMLのCAMLというのはCategorical Abstract Machin Languageという言葉の略であり圏論的抽象に関する機会言語という非常に関心を全く抱く話につながるわkです。
一々説明がどうのこうの言うのも、私にはデメリットがいまのところ全く思い至らないので、機会があれば微に入り細に入り説明する必要があるのならすればいいでしょう。面倒くさいとかそういうのがあればまだしも、だれか迷惑するわけでもなし、わからないという人がいるなら細かく説明していちいちなぞなぞみたいな状況にする必要はないわけです。学術的なことであるわけですし、だれか迷惑するわけでもなし。ds/dt=0になるという話もベクトル場じゃなくて双対の微分形式で説明しろというのなら、それはその意図がわからないので自分は説明しかねるとはいえるでしょう。--I.hidekazu会話2022年6月6日 (月) 15:51 (UTC)[返信]
常識が通じないで話は終わりでしょ。そらす以前にもう話す必要ないですよね。残りをまとめると「このドメインの圏 J のことをこの図式の添字圏 (index category) やスキーム(scheme)と呼ぶ。」は読んでないし読む気もない。編集前の文章なんて読まずに編集したし今でも読む気はさらさらない。sをtで微分したら何になるか計算する気もない。書いた数式の検算もしないってことですね。--Kik会話2022年6月7日 (火) 11:41 (UTC)[返信]
常識が通じない(非常識である)という点については私はどういうものであるか具体的に知らない。「私にはデメリットが思い至らない」ので微に入り細に入り説明するニーズがあるのであれば止めるものはない。
スキームのスキームの記述がどういう意図にあるものか知らない。どういうものを導来(guide)するための圏に関する記述なのかどこへ導来(guide)する圏であるのか判断はつかない。
つまり、書いた数式の検算はしているので不当な言いがかりは止めてもらえませんかということだ。--I.hidekazu会話2022年6月7日 (火) 16:36 (UTC)[返信]
プログラムの仕様が必要だという常識ですよ。そんなに自信があるなら、あなたの言うダイクストラ流の仕様に関係なく証明かなんか知らないですがそれっぽいことができるプログラムの例を1個書いてみればいいじゃないですか。
導来(guide)するって何ですか?それが編集前の文章を読まずに編集することと何か関係があるんですか?
ということは当時は検算はしてたけどうっかり計算間違えてたってことで、今はちゃんとds/dt=0になってたのを理解しているってことですか?--Kik会話2022年6月7日 (火) 19:18 (UTC)[返信]
なんで私が実証するプログラムを書くことになるんですか。
構造化プログラミングの本に書いてないことを書くことは独自研究になると言っているんです。むしろ構造化プログラミングで仕様を用いたプログラムの正しさの証明というものがどういうことを指すのか示してくれませんか。
ダイクストラのプログラムの正しさの証明の例は構造化プログラミングのpp.13-16に具体的に書いてあります。もちろん仕様がどうのこうのということは書いてません。(せいぜい言えて、ダイクストラはプログラムとその計算プロセスの関係について正しさの妥当性確認をしているようだと言える程度です。)
s ではなく S と書いたはずですが、もう忘れたんですか。--I.hidekazu会話2022年6月10日 (金) 16:25 (UTC)[返信]
s ではなく S と書いたらsが未定義になるだけで何も解決してないんですが問題点を全く理解してなくないですか?
構造化プログラミングの日本語訳は持ってないので、https://dl.acm.org/doi/pdf/10.5555/1243380 にある英語版の話しかできませんが、該当するのはおそらく6ページから始まる4章の話をしてるんだろうという前提で話しますが、4.1節の最初に

I regard as an appeal to enumeration the effort to verify a property of the computations that can be evoked by an enumerated set of statements performed in sequence, including conditional clauses distinguishing between two or more cases. Let me give a simple example of what I call "enumerative reasoning".

と書いてあります。日本語訳でどうなってるのかはしりませんが、verifyする対象はpropertyだとはっきり書いてあります。直後に書いてある例でも
dd : = dd/2;
if dd <= r do r : = r - dd
というプログラムに関して
0 <= r < dd
という関係が不変であるという性質を確かめるという内容になっています。これは私が上でずっと常識であると指摘していたプログラムの性質とプログラムを比較して検証するという話そのものが書いてあるのに等しいと思います。逆にあなたが言っていた「ダイクストラは「検証」とは言っておらず「プログラムの正しさの証明の理解」というように、プログラムを証明と見立てて人間の力で確認する(プログラムを理解する)ことを問題視しています。」というのはこの例ではどこ見て理解すればいいのですか?私の言っていたことは最初の一文にちゃんと記述されていたのですが、あそこまで煽ってきて実はしょっぱなから読めてなかったとか完全に時間の無駄でしたね--Kik会話2022年6月10日 (金) 21:43 (UTC)[返信]
前提が違います。私が言っているのは、5節の「正しさの証明の例」です。
それに「これは私が上でずっと常識であると指摘していたプログラムの性質とプログラムを比較して検証するという話そのものが書いてあるのに等しい」、ということですが、言っていたのはプログラムと仕様の話でしょう。仕様の話はどこ行ったのですか。都合が悪くなったからと言って話を変えるのはやめてください。仕様なんて一言もでてきてないじゃないですか。
『「ダイクストラは「検証」とは言っておらず「プログラムの正しさの証明の理解」というように、プログラムを証明と見立てて人間の力で確認する(プログラムを理解する)ことを問題視しています。」というのはこの例ではどこ見て理解すればいいのですか?』この例そのものじゃないですか。逆に仕様とプログラムの関係がどこに書いてあるんですか。
曲線 α(t) の原点から t 地点までの弧長を s と定義して、
とすればいいでしょう。τが出てきてわかりにくくなるのであまり書きたくないですが。--I.hidekazu会話2022年6月11日 (土) 14:41 (UTC)[返信]
5節に書いてあるのは4節に書いてある例をちょっと複雑にしただけでやってることは同じじゃないですか。ちょっと難しいプログラムが出てきて、「割り算の余りを求める」てのが仕様なんですけど分かりませんか?
あと、最初のうちはプログラムの仕様やプログラムの性質というふうにちゃんと書いてたんですが、途中からめんどくさいのでまとめて仕様としか書いてないので、仕様なのか性質なのかは形式的に区別できるものではないので適当に同じものだと思って読んでください。
4.1節のverifyは検証じゃないのですか?5節でもverifyって書いてあるところがありますけど。
「プログラムを証明と見立てて」ってのはこの例では一体どこで行われているんですか?なんでプログラムと証明を同列に並べているのか全く意味が分からないです。ダイクストラは別行立てで書いてある式がプログラムなのか命題なのかを丁寧に区別して書いてるように見えるのですが(プログラム片であるテキストは必ず引用符でくくってある)。
sについてはそう定義する以外に正しく書けないんですが、まだ前の書き方でも正しいとか思ってませんか?--Kik会話2022年6月11日 (土) 15:25 (UTC)[返信]
具体的な正しさの確認の例を出せというから5節だといったんです。
ほかも独自研究だとしか言えませんね。そんなこと書いてないし。書きたければ自分で書けばいいでしょう。毒研究タグをつけるだけですが。
verifyという用語を使っていても仕様とプログラムの関係なんて言ってないんだから専門用語として使っているとはいえない。
「プログラムを証明と見立てて」→Euclid幾何学の証明と並べています。p.11--I.hidekazu会話2022年6月11日 (土) 15:45 (UTC)[返信]
「プログラムの正しさの証明ってEuclid幾何学の証明みたいで難しいしめんどくさいよね」って書いてあるのが、どう飛躍したら「プログラムを証明と見立てて人間の力で確認する」になるんですかね--Kik会話2022年6月11日 (土) 16:25 (UTC)[返信]
あなたの言っていることがそのまま「プログラムを証明と見立てて人間の力で確認する」ということになっているじゃないですか。いちいち根拠のないことをつっかかってこないでください。--I.hidekazu会話2022年6月11日 (土) 16:34 (UTC)[返信]
「プログラムの正しさの証明」と「Euclid幾何学の証明」を比較しているのに、「プログラムを証明と見立てて」が出てくるのは完全に意味不明ですしこんなん時間の無駄だからこれ以上はやめましょう。そもそも常識が足りてなくて議論のスタート地点から合っていないのにレスバしても何にもなりませんよ。--Kik会話2022年6月11日 (土) 16:46 (UTC)[返信]
また都合が悪くなると話を逸らす。仕様とプログラムの話なんて書いてないんだからそもそも話として出してくる方がおかしい。こちらもより不毛な話はやめたい。--I.hidekazu会話2022年6月11日 (土) 17:00 (UTC)[返信]
特別:差分/89049170/89055896のことだと思いますが、これは@Kik氏の主張をエスパーして補足したのではなく、私が独自に記事を読んでみて発見した問題点をいくつか指摘しただけです。利用者:Sillycrownでは「メインエリア」として「数学」と「哲学」と書いてありますが、このことは私の関心が数学と哲学に限られるということも、それ以外の領域についての知識を持ち合わせていないことも、どちらも読み取れません。そもそも数学は計算機科学と深い関わりあるわけですから、仮に私が「数学」だけに関心と知識を持っていたとしても、プログラミングに関する記事について評価を行うことは何ら不思議ではないでしょう。(例えば構造化定理標準形定理英語版による証明は私が加筆したものです。)@Kikと同一ユーザーではないかという勘繰りは強く否定します。もっとも、個人情報を開示しない限り決定的な反証のできない事柄ですし、仮にそうだったとしてもあなた方の口論の正否には何ら関わりのないことですから、ただ実りのない口論に巻き込まないでほしいという要望だけ残しておきます。--Sillycrown会話2022年6月8日 (水) 23:16 (UTC)[返信]
エスパーして補足したわけではないということで、そうするとこれは独自研究云々の指摘ではないということになりますね。Kik氏があまりにも指摘を自家篭絡に回答してくるのでほとんど一体物だと認識しています。
問題点の指摘に対しては、「検証」という用語を用いたのは不適切で、ダイクストラは「プログラムの正しさの証明の理解」といっており、プログラム検証論とはやや開きがあるということにつきます。Kik氏は仕様をことさら問題にしてきますが、Sillycrown氏としてはどういう回答になりますか。
この実りのない意図不明の議論をしっかり読まれたということとご要望は私は理解しました。--I.hidekazu会話2022年6月10日 (金) 16:40 (UTC)[返信]

「アインシュタインは自然の一般法則は座標系に依存しない形式、すなわち(テンソル)=0という性質を持つものであると仮定しました。」が独自研究であることについて[編集]

I.hidekazuさんはWikipedia:投稿ブロック依頼/I.hidekazuにおいて、以下を出典として挙げられています。

ここでの「アインシュタインは自然の一般法則は座標系に依存しない形式、すなわち(テンソル)=0という性質を持つものであると仮定しました。」というのは当時p.107,108だけに基づいたものではなく、それに加えて『リーマン幾何とその応用』の訳者の矢野健太郎氏の解説 p.208,209も参考にした記述で、引用すると、
アインシュタインはまず、特殊相対性原理の代わりに、
(1)すべての物理法則は、互いに任意の運動をするすべての観測者に対して同一の形式で与えられる(一般相対性原理

ということを要求した。

・・・中略・・・

まず、上の第1の一般相対性原理は、物理法則を

(テンソル)=0
の形に書き表すことによって満足される。なぜなら、テンソルの成分がある座標系においてすべて0であれば、その成分は、変換法則からわかるように、他のすべての座標系においても、すべて0であるからである。 — リーマン幾何とその応用,p.208,209
という記述です。一応言っておけば訳者解説は二次資料ですし、そもそもここは今問題とすべき箇所ではないと思います。嘘というのは人聞きが悪いのでここも訂正していただきたい。
独自研究かどうかということについてですが、(テンソル)=0ということの意味を式で表現しようとすることがそれに該当するのでしょうか?

しかし、この出典で主張されているのは「アインシュタインは一般相対性原理を公理に採用した」と「物理法則が(テンソル)=0と書かれていれば、それは一般相対性原理を満たす」の2点であり、「アインシュタインは自然の一般法則は座標系に依存しない形式、すなわち(テンソル)=0という性質を持つものであると仮定しました。」という主張はなされていません。そもそも、一般相対性原理を公理として採用した上に「自然の一般法則は(テンソル)=0で書ける」も仮定することは論理的におかしいことです。後者を仮定すると前者は必然的に成り立つわけですから、前者は公理として重複していることになり全くの無駄です。以後こういうことがないように、WP:NORをよく読んでください。特に「独自研究ではないことを示す唯一の方法は、その記事の主題に直接関連のある情報を提供している信頼できる資料を参考文献として記し、その資料に記された内容に忠実に記述することです。」が守られているかを出典を挙げる前に自分で確認してください。--Kik会話2022年4月23日 (土) 20:47 (UTC)[返信]

「任意の曲線は、パラメータをその曲線の弧長に変更することでその速さを1にすることができる。」の出典について[編集]

Wikipedia:投稿ブロック依頼/I.hidekazuで出典として以下を挙げられています。

出典の該当箇所を引用すると、
曲線の研究では、曲線の軌跡だけに関心があり、曲線の速さを問題にしないことがある。そのような場合に、退化しない曲線に対しては速さを1に標準化する方法がある:
定理2.7 ユークリッド空間の退化しない任意の曲線αに対して、そのパラメータを変更してできる曲線βで、速さ||β'||が1であるものが存在する。
証明
-略-

 速さが1である曲線をパラメータが弧長である曲線ともいう。定理2.7での弧長によるパラメータの変更では、ds/dt > 0が成り立っているから、ここでのパラメータの変更は曲線の向きを保つ変更になっている。

— 『微分幾何学入門』関沢正躬著 p.26,27
とあり虚偽ではありません。

これでは出典になっていません。これについては、「独自研究ではないことを示す唯一の方法は、その記事の主題に直接関連のある情報を提供している信頼できる資料を参考文献として記し、その資料に記された内容に忠実に記述することです。」の「忠実に記述する」を注意深く行ったください。--Kik会話2022年4月23日 (土) 21:10 (UTC)[返信]

「英語版で"disjoint union"(分離和)と書いてあった」について[編集]

特別:差分/87702516で「英語版で"disjoint union"(分離和)と書いてあった」とコメントされましたが、そのような事実はありませんでしたので、次からはこのようなことがないように反省してください。--Kik会話2022年4月23日 (土) 21:21 (UTC)[返信]

履歴継承について[編集]

利用者:I.hidekazu/クラス_(プログラミング)を作成しておられるようですが、こちらはクラス_(コンピュータ)の複製を元に編集しておられませんでしょうか?#翻訳記事における翻訳元表示のお願いでの指摘と全く同じ内容になりますが、Wikipediaで記載される文章には全てライセンスがありますので、複製する場合には適切な手順に則る必要があります。先日指摘があった直観主義型理論についても、適切な対応すべてが完了していませんので、改めてWikipedia:著作権Wikipedia:翻訳のガイドラインの熟読をお願いいたします。 --紅い目の女の子(会話/履歴) 2022年5月31日 (火) 03:03 (UTC)[返信]

利用者サブページは対象外という認識でしたが、Wikipedia:利用者ページ#利用者ページでできることに記載ありましたね。今から要約欄に記載しておきます。
直観主義型理論についてはWikipedia:翻訳のガイドライン#要約欄への記入忘れ・誤記入の「翻訳投稿の際、要約欄に翻訳元記事へのリンクは書いたが、版指定を忘れた場合」に準拠して補遺を記載したことで対応しましたが、「上記以外の場合には、状況に応じ、版指定削除、全削除、あるいは即時削除を依頼してください。」に該当するのではないかということですか。対応する必要があるにせよ現在審査中で本記事編集は不適当と考えます。--I.hidekazu会話2022年6月2日 (木) 14:45 (UTC)[返信]
  • コメント 利用者サブページについても例外なく版指定削除などの対応が必要になります。利用者サブページは現状あなたの投稿記録しかありませんから、即時削除による対応をとっていただくと手続きが簡便かと思います。
直観主義型理論についてどのような対応を取られるかはあなたの自由ではありますが、ライセンス違反の状態が継続しているという認識はお忘れにならないようお願いいたします。 --紅い目の女の子(会話/履歴) 2022年6月3日 (金) 02:25 (UTC)[返信]
利用者サブページについては補遺を要約欄に記載しましたが、これだとまずいので即時削除による対応が必要ということですか。
直観主義型理論については審査が終わったら対応を考えます。
ところで投稿ブロックの審査が異常に長いのですが、いったいいつになったら終わるのですか?--I.hidekazu会話2022年6月3日 (金) 14:50 (UTC)[返信]

投稿ブロックのお知らせ[編集]

あなたは無期限ブロックされました。 あなたは無期限ブロックされました。これ以上ウィキペディアの編集を行うことはできません。ブロックが自動的に解除されることはありませんのでご留意ください。今後の対話ならびに異議申し立て、解除依頼はあなたの会話ページで受け付けます(投稿ブロック解除依頼作成の手引き投稿ブロックへの異議申し立て参照)。会話ページも編集できないブロックの場合は、IRC#wikipedia-ja-unblock、もしくはメーリングリストで、会話ページの編集許可を求めてください(ヘルプ)。--Sumaru会話2022年8月14日 (日) 14:41 (UTC)[返信]

方針によりブロックされたこの利用者 (ブロック記録 | 現在有効なブロック | 自動ブロック | ブロック解除 | 投稿記録 | 削除された投稿 | 不正利用記録) はブロックの解除を依頼しましたが、管理者がブロックを再検討し、依頼を却下しました。他の管理者がこのブロックを更に再検討することは可能ですが、充分な理由がない限り、この決定を覆すべきではありません(投稿ブロックの方針参照のこと)。ブロックが継続している間は、このブロック解除依頼を除去しないでください。

ブロック解除依頼の理由: 「Wikipedia:投稿ブロック依頼/I.hidekazuにて無期限ブロック理由となっていた事柄について対処を行っていた最中(#独自研究を除去してください)に、理由を変えてWikipedia:削除依頼/ミルズの構造化プログラミングを出してくるなど、無期限ブロック提出者の言動が一貫しておらず無期限ブロックに至る理由がはっきりしないため。 --I.hidekazu会話2022年9月23日 (金) 15:42 (UTC)[返信]


却下の理由: 依頼のあったブロック解除は、あなたがブロックされた理由を明示していない、あるいはその他の不適切な点があるため、却下いたします。ブロックが解除となるためには、以下の点について管理者を納得させる必要があります。
  • ウィキペディアに対する妨害・損害を避けるためにあなたをブロックする必要はないこと または
  • あなたが
    • なぜブロックされたのか理解し、
    • ウィキペディアに対する妨害や破壊をやめ、
    • 今後は有用な貢献を行うため、
      ブロックがもはや必要でなくなったこと

投稿ブロック解除依頼作成の手引きもぜひお読みください。 Jkr2255 2023年4月15日 (土) 00:32 (UTC)[返信]

ブロック解除の依頼を再度行いたい場合には、投稿ブロック解除依頼作成の手引きをまずお読みになり、もう一度 {{unblock}} テンプレートを使用してください。なお、これらのテンプレートの乱用があった場合は、あなたの会話ページの保護や、会話ページへのブロックを実施する場合もありますのでご注意ください。
  • コメント ブロック依頼において、依頼者は単に依頼を提出しただけの存在です(極端な例ですが、依頼提出後に依頼者がソックパペットであることが判明したものの、依頼の内容自体は妥当だったために他者からの賛成票が入り、ブロックされた例も存在します)。他の参加者も含めた依頼内容を評価して自身の行動と照らし合わせるプロセスすら行わないのでは、解除依頼のスタートラインにすら立てていないと言って過言ではありません。--Jkr2255 2023年4月15日 (土) 00:32 (UTC)[返信]

Kik 氏sについて[編集]

  • 版番90472383 要約欄:『クラスとコルーチンが強く結合した言語は初期のSimulaのみであり、以降の言語ではクラスとコルーチン等の並列化機能を直交した機能として提供している。しかも、Simula67ですでにdetach文で明示的に指定しないとコルーチンとならないほか、detach状態でブロックを起動する文も追加されており、クラスとコルーチンはほとんど分離している。』あれ?と思って考えたら、結構絞れた。
  • 特別:差分/88709977 ここらへんから本格的に怪しんできた。
  • 特別:差分/90419505/90445125 おかしいものはおかしい。雑なミスリードにはいそうですかなんて言うわけないでしょう。
要約
  • 今までのことを総合して、ソックパペットではなくミートパペット。百歩譲ってソックパペットと言ったことは謝りましょう。
  • 『嘘つき』のパラドックスとはよく言ったもんですね。都合が悪いからと言って素人をなぶるとはどういうつもりでしょうか。
  • Wikipedia の物理・数学・計算機科学の裏側がわかりました。

--以上の署名のないコメントは、I.hidekazu会話投稿記録)さんが 2022年9月23日 (金) 15:42 (UTC) に投稿したものです(Keruby会話)による付記)。[返信]

再度の投稿ブロック解除依頼について[編集]

このブロック中の利用者は、ブロックの見直しを求めています。

I.hidekazuブロック記録現在有効なブロックグローバルブロック自動ブロック投稿記録削除された投稿記録編集フィルター記録アカウント作成記録ブロック設定変更解除


ブロック解除の理由:

Jkr氏の提示されたフォーマットに沿って下記のとおり解除依頼を行います。

 記

  • なぜブロックされたのか:プログラミング数学物理学のジャンルにおいて、結果的に一部編集者を消耗させる活動を行ったため。
  • ウィキペディアに対する妨害や破壊をやめ:誓約として今後はプログラミング数学物理学のジャンルの編集は原則行わない。具体的にはカテゴリーとしてCategory:プログラミングCategory:数学Category:物理学のタグが入っているものは編集しない。
  • 今後は有用な貢献を行うため:今後は数学の哲学よりの哲学、哲学的概念、歴史をメインで出典付きで記載することとし、以後その分野に関して有用な貢献をすることができるものと考える。
  • (自己申告)哲学、哲学的概念、歴史をメインで記載するため、新規にアカウント利用者:Ph.Clemensを作成してしまいました。ジャンルは違ってもやはり新規アカウントの作成は憚れると考え、4回しか編集してないのでご容赦ください。

以上。

上記を踏まえ、ブロックがもはや必要でなくなったことを主張します。

注意:

  • 実際にはブロックされていない、またはすでにブロック期間が終了している場合があります。ブロックログを確認してください。ブロックの記録がない、もしくは直近のブロックがすでに終了していれば、荒らし対策の自動システムにより自動ブロックに巻き込まれています。この場合は、このテンプレートではなく{{Unblock-auto}}をご利用ください。Wikipedia:自動ブロックもご参照ください。
  • 投稿ブロック解除依頼作成の手引きを読んで、あなたのブロック解除依頼が妥当なものか検討してください。依頼はいつでも改変してかまいません。

--I.hidekazu会話2023年11月8日 (水) 12:37 (UTC)[返信]

コメント 確認なのですが、アカウント「利用者:Ph.Clemens」はI.hidekazuさんがブロック破りを行うために作ったアカウントと言う事でしょうか?--TFhhtt会話2024年2月15日 (木) 23:20 (UTC)[返信]