論文の概要: Three computational models and its equivalence
- arxiv url: http://arxiv.org/abs/2010.15600v1
- Date: Mon, 26 Oct 2020 05:55:19 GMT
- ステータス: 処理完了
- システム内更新日: 2022-10-02 19:50:06.815711
- Title: Three computational models and its equivalence
- Title(参考訳): 3つの計算モデルとその等価性
- Authors: Ciro Ivan Garcia Lopez
- Abstract要約: 計算可能性の研究は、1900年のヒルベルトの会議(英語版)においてアルゴリズムの概念を正確に記述することに由来する。
数学的詳細を忘れずに、現代の方法で証明を提示するこのギャップを埋めるつもりです。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: The study of computability has its origin in Hilbert's conference of 1900,
where an adjacent question, to the ones he asked, is to give a precise
description of the notion of algorithm. In the search for a good definition
arose three independent theories: Turing and the Turing machines, G\"odel and
the recursive functions, Church and the Lambda Calculus.
Later there were established by Kleene that the classic models of computation
are equivalent. This fact is widely accepted by many textbooks and the proof is
omitted since the proof is tedious and unreadable. We intend to fill this gap
presenting the proof in a modern way, without forgetting the mathematical
details.
- Abstract(参考訳): 計算可能性の研究は、1900年のヒルベルトの会議でその起源を定めており、そこで彼が質問した質問とは、アルゴリズムの概念を正確に記述することである。
良い定義を求める中で、チューリングとチューリングマシン、G\"odelと再帰関数、チャーチとLambda Calculusという3つの独立した理論が生まれた。
後にクリーネによって古典計算のモデルが等価であると確立された。
この事実は多くの教科書で広く受け入れられており、証明は退屈で読めないため、証明は省略されている。
数学的詳細を忘れずに、現代の方法で証明を提示するこのギャップを埋めるつもりです。
関連論文リスト
- Learning Formal Mathematics From Intrinsic Motivation [34.986025832497255]
ミニモ(Minimo)は、自分自身に問題を起こし、それを解決することを学ぶエージェント(理論実証)である。
制約付き復号法と型指向合成法を組み合わせて、言語モデルから有効な予想をサンプリングする。
我々のエージェントは、ハードだが証明可能な予想を生成することを目標としています。
論文 参考訳(メタデータ) (2024-06-30T13:34:54Z) - Machine learning and information theory concepts towards an AI
Mathematician [77.63761356203105]
人工知能の現在の最先端技術は、特に言語習得の点で印象的だが、数学的推論の点ではあまり重要ではない。
このエッセイは、現在のディープラーニングが主にシステム1の能力で成功するという考えに基づいている。
興味深い数学的ステートメントを構成するものについて質問するために、情報理論的な姿勢を取る。
論文 参考訳(メタデータ) (2024-03-07T15:12:06Z) - Connecting classical finite exchangeability to quantum theory [69.62715388742298]
交換性は確率論と統計学の基本的な概念である。
有限交換可能な列に対するデ・フィネッティのような表現定理は、量子論と正式に等価な数学的表現を必要とすることを示す。
論文 参考訳(メタデータ) (2023-06-06T17:15:19Z) - ProofNet: Autoformalizing and Formally Proving Undergraduate-Level
Mathematics [7.607254619341369]
本稿では,学部レベルの数学の自己形式化と形式証明のためのベンチマークであるProofNetを紹介する。
ProofNetベンチマークは371の例で構成され、それぞれがLean 3.0の正式な定理文で構成されている。
テキスト内学習による文の自動書式化のベースライン結果について報告する。
論文 参考訳(メタデータ) (2023-02-24T03:28:46Z) - Towards a Mathematics Formalisation Assistant using Large Language
Models [5.485439959027125]
リーン定理証明器の形式化を支援するために,大規模な言語モデル(Codex)の能力について検討する。
コーデックスは、短い数学的ステートメントを120ドルの定理ステートメントに対して75%近い精度でアンダーグレードレベルで定式化することができる。
新たなプロンプト戦略により、コーデックスはこれらの証明を自然言語で定式化することができ、12のコーデックスのうち少なくとも1つの完備化は、完全な証明に容易に修正できることが示される。
論文 参考訳(メタデータ) (2022-11-14T16:52:32Z) - NaturalProver: Grounded Mathematical Proof Generation with Language
Models [84.2064569475095]
自然数理言語における定理証明は、数学の進歩と教育において中心的な役割を果たす。
本研究では,背景参照を条件づけて証明を生成する言語モデルであるNaturalProverを開発する。
NaturalProverは、短い(2-6ステップ)証明を必要とするいくつかの定理を証明でき、40%の時間で正しいと評価された次のステップの提案を提供することができる。
論文 参考訳(メタデータ) (2022-05-25T17:01:18Z) - Proofs of network quantum nonlocality aided by machine learning [68.8204255655161]
我々は[DOI40103/PhysRevLett.123.140]の量子三角形分布の族が、元の証明よりも広い範囲の三角形局所モデルを認めていないことを示した。
我々は、独立な利害関係を持つ二項結果を持つ三角形のシナリオに対して、ネットワークベルの不等式を大量に収集する。
論文 参考訳(メタデータ) (2022-03-30T18:00:00Z) - multiPRover: Generating Multiple Proofs for Improved Interpretability in
Rule Reasoning [73.09791959325204]
我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。
PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。
本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
論文 参考訳(メタデータ) (2021-06-02T17:58:35Z) - Gull's theorem revisited [0.0]
ギルの哲学はベルの定理を分散コンピューティングにおけるプロジェクトのノーゴー定理と見なすことができる。
我々は彼の主張を述べ、誤印刷を訂正し、ギャップを埋める。
論文 参考訳(メタデータ) (2020-12-01T18:29:13Z) - A Finitist's Manifesto: Do we need to Reformulate the Foundations of
Mathematics? [1.384477926572109]
このエッセイは、無限の楽園で睡眠ウォーキングをしている数学者のヒードを練習するためのものです。
数学の多くの分野は、(i)無限個の要素を含む対象の「存在」、(ii)任意の精度で計算する能力、「理論」、または(iii)任意の数の時間ステップを計算する能力「理論」に依存している。
論文 参考訳(メタデータ) (2020-09-14T14:44:08Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳(メタデータ) (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。