論文の概要: A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem

• arxiv url: http://arxiv.org/abs/2604.16477v1
• Date: Sat, 11 Apr 2026 20:45:58 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-04-28 14:37:02.559144
• Title: A Constructive Proof of Rice's Theorem and the Halting Problem via Hilbert's Tenth Problem
• Title（参考訳）: ヒルベルトの十番目の問題による米の定理とハルティング問題の構成的証明
• Authors: Jonathan Brossard,
• Abstract要約: ライスの定理は、プログラムの非自明な意味的性質は決定不可能である。 Hilbert's Tenth Problem (MRDP) の不決定性に対する構成的証明を提案する。 議論は2つの別個の含意として構成され、可解性に関する解離を主張せず、P(bot)を検査しない。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Rice's theorem states that no non-trivial semantic property of programs is decidable. Classical proofs proceed by reduction from the halting problem, invoking the law of excluded middle (LEM) twice: once through diagonalization, and once through a case split on whether the always-diverging program bot satisfies the property in question. We present a proof that is constructive relative to the undecidability of Hilbert's Tenth Problem (MRDP): valid in intuitionistic logic, requiring neither diagonalization nor self-reference, and adding no classical reasoning beyond the MRDP assumption itself. The key idea is a two-witness construction. Given a non-trivial property P, we attach to each Diophantine polynomial D a pair of programs S^0_D, S^1_D that behave like the negative and positive witnesses for P when D is solvable, and both diverge identically when it is not. A hypothetical decider for P would therefore decide Diophantine solvability via the difference delta_D = DecideP(S^1_D) - DecideP(S^0_D) -- contradicting the MRDP theorem. The argument is structured as two separate implications, never asserting a disjunction about solvability, and never examining P(bot). The undecidability of the halting problem follows as an immediate corollary: a single application of Rice's theorem to the Terminates property. A formalization in the Rocq proof assistant confirms both results within a step-indexed model of computation, with the undecidability of Hilbert's Tenth Problem as the sole external axiom. Both Rice_Theorem and Halting_Problem are closed under the global context.
• Abstract（参考訳）: ライスの定理は、プログラムの非自明な意味的性質は決定不可能である。 古典的な証明は停止問題から減らし、排除された中性(LEM)の法則を2回、対角化によって1回、常に発散するプログラムボットが問題となる性質を満たすかどうかを1回に分けて行う。 Hilbert's Tenth Problem (MRDP) の不確定性に対する構成的証明として、直観論的論理において有効であり、対角化も自己参照も必要とせず、MRDPの仮定自体を超越した古典的推論を加えない。 鍵となるアイデアは、2人の知性の構築だ。 非自明な性質 P が与えられたとき、各ディオファンティン多項式 D にプログラム S^0_D と S^1_D をアタッチし、D が解けるときに P の負の証人や正の証人のように振る舞う。 したがって、P の仮説決定器は delta_D = DecideP(S^1_D) - DecideP(S^0_D) という差でディオファンチンの可解性を決定する。 この議論は2つの別個の含意として構成され、可解性に関する解離を主張することはなく、P(bot) を調べることもない。 停止問題の不確定性は、即ち、ライスの定理の終端性への1つの応用である。 Rocq証明アシスタントの形式化は、ヒルベルトの10番目の問題(英語版)を唯一の外部公理として決定不能にすることで、ステップインデクシングされた計算モデル内で両方の結果を確認する。 Rice_Theorem と Halting_Problem はどちらもグローバルコンテキスト下で閉じている。

関連論文リスト

• Exact Structural Abstraction and Tractability Limits [0.0]
  正確な正確性は、誘導されたクラス $s sim_R simation' iff MathrmAdm_R(s)$ にのみ依存する。 決定、探索、近似、統計的、ランダム化された地平線、分布保証は全て同じ商-回復問題に還元される。
  論文  参考訳（メタデータ） (2026-04-08T17:59:47Z)
• Aumann's theorem beyond ontology: quantum, postquantum, and indefinite causal order [0.0]
  我々は、世界の客観的な状態を仮定することなく、オーマンの合意定理の運用版を導出する。 これにより、量子論や不明確な因果順序や仮説的な後量子現象を含む状況においても、定理の妥当性を確立することができる。 我々は、文学における一見矛盾した結果についてコメントし、定理が失敗するかもしれない一箇所を指摘する: ウィグナーの友人型状況。
  論文  参考訳（メタデータ） (2026-03-24T18:00:00Z)
• A Theory of $θ$-Expectations [2.1756081703276]
  我々は、ドライバーがポイントワイズ幾何学である微分方程式のクラスのためのフレームワークを開発する。 システムのトラクタビリティは、世界的なユニークかつグローバルな存在を前提としている。 ドライバー関数に対するリプシッツ最大値写像。
  論文  参考訳（メタデータ） (2025-07-27T16:56:01Z)
• Proving Theorems Recursively [80.42431358105482]
  本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。 従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。 また,POETRYが検出した最大証明長は10～26。
  論文  参考訳（メタデータ） (2024-05-23T10:35:08Z)
• Some consequences of Sica's approach to Bell's inequalities [55.2480439325792]
  ルイ・シカ(Louis Sica)は、ベルの不等式は、あるステーションで観測された結果の時系列が、他のステーションの設定が変更されても変化しないという仮説から導いた。 本稿では,Sicaのアプローチを非理想的効率と実時間構造に拡張する。
  論文  参考訳（メタデータ） (2024-03-05T13:59:52Z)
• Connecting classical finite exchangeability to quantum theory [45.76759085727843]
  交換性は確率論と統計学の基本的な概念である。 観測順序が重要でない状況のモデル化を可能にする。 両定理が有限交換可能な列に対して成り立たないことはよく知られている。
  論文  参考訳（メタデータ） (2023-06-06T17:15:19Z)
• Connes implies Tsirelson: a simple proof [91.3755431537592]
  コンヌ埋め込み問題は同期的ツィレルソン予想を意味することを示す。 また、コンネスの代数 $mathcalRomega$ の異なる構成もコンネス埋め込み問題に現れる。
  論文  参考訳（メタデータ） (2022-09-16T13:59:42Z)
• A possibilistic no-go theorem on the Wigner's friend paradox [0.0]
  局所親和性定理の確率自由版を示す。 これは局所隠れ変数に対するハーディのノーゴー定理に基づいている。
  論文  参考訳（メタデータ） (2022-05-24T17:31:54Z)
• multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning [73.09791959325204]
  我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。 PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。 本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
  論文  参考訳（メタデータ） (2021-06-02T17:58:35Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。