論文の概要: Programming Really Is Simple Mathematics
- arxiv url: http://arxiv.org/abs/2502.17149v1
- Date: Mon, 24 Feb 2025 13:40:42 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-02-25 15:55:01.983812
- Title: Programming Really Is Simple Mathematics
- Title（参考訳）: プログラミングは単純な数学だ
- Authors: Bertrand Meyer, Reto Weber,
- Abstract要約: 本稿では,基本集合論に基づく小数理理論(PRISM)としてのプログラミングの基礎を再構築する。
プログラムとプログラミングの重要な性質を特徴づける数十の定理を導出する。
- 参考スコア（独自算出の注目度）: 33.351872273350885
- License:
- Abstract: A re-construction of the fundamentals of programming as a small mathematical theory (PRISM) based on elementary set theory. Highlights: $\bullet$ Zero axioms. No properties are assumed, all are proved (from standard set theory). $\bullet$ A single concept covers specifications and programs. $\bullet$ Its definition only involves one relation and one set. $\bullet$ Everything proceeds from three operations: choice, composition and restriction. $\bullet$ These techniques suffice to derive the axioms of classic papers on the "laws of programming" as consequences and prove them mechanically. $\bullet$ The ordinary subset operator suffices to define both the notion of program correctness and the concepts of specialization and refinement. $\bullet$ From this basis, the theory deduces dozens of theorems characterizing important properties of programs and programming. $\bullet$ All these theorems have been mechanically verified (using Isabelle/HOL); the proofs are available in a public repository. This paper is a considerable extension and rewrite of an earlier contribution [arXiv:1507.00723]
- Abstract（参考訳）: 基本集合論に基づく小数理理論(PRISM)としてのプログラミングの基礎の再構成。
ハイライト:$\bullet$ Zero axioms。
性質は仮定されず、すべて証明される(標準集合論から)。
$\bullet$ 1つの概念は仕様とプログラムをカバーする。
$\bullet$ その定義は1つの関係と1つの集合のみを含む。
すべては、選択、構成、制限の3つの操作から始まります。
$\bullet$ これらのテクニックは、結果として"プログラミングの法則"に関する古典的な論文の公理を導き、それらを機械的に証明するのに十分である。
$\bullet$ 通常のサブセット演算子は、プログラムの正確性の概念と特殊化と洗練の概念の両方を定義するのに十分である。
$\bullet$ この基礎から、この理論はプログラムとプログラミングの重要な性質を特徴づける数十の定理を導出する。
$\bullet$ これらの定理はすべて機械的に検証されている(Isabelle/HOL を用いて)。
この論文は、初期のコントリビューション(arXiv:1507.00723)の相当な拡張と書き直しである。
関連論文リスト
- Machine learning and information theory concepts towards an AI
Mathematician [77.63761356203105]
人工知能の現在の最先端技術は、特に言語習得の点で印象的だが、数学的推論の点ではあまり重要ではない。
このエッセイは、現在のディープラーニングが主にシステム1の能力で成功するという考えに基づいている。
興味深い数学的ステートメントを構成するものについて質問するために、情報理論的な姿勢を取る。
論文 参考訳（メタデータ） (2024-03-07T15:12:06Z) - Generalised Kochen-Specker Theorem for Finite Non-Deterministic Outcome Assignments [0.0]
Kochen-Specker (KS) の定理は、集合 $0, p, 1-p, 1$ for $p in [0,1/d) cup (1/d, 1/2]$ で結果を与えるような隠れ変数理論を規定する。
論文 参考訳（メタデータ） (2024-02-14T14:02:37Z) - Tempered Calculus for ML: Application to Hyperbolic Model Embedding [70.61101116794549]
MLで使用されるほとんどの数学的歪みは、本質的に自然界において積分的である。
本稿では,これらの歪みを改善するための基礎的理論とツールを公表し,機械学習の要件に対処する。
我々は、最近MLで注目を集めた問題、すなわち、ハイパーボリック埋め込みを「チープ」で正確なエンコーディングで適用する方法を示す。
論文 参考訳（メタデータ） (2024-02-06T17:21:06Z) - Hierarchies for Semidefinite Optimization in
$\mathcal{C}^\star$-Algebras [0.0]
本稿では,$mathcalCstar$-algebras上での一般コーンプログラムの有限次元緩和法を提案する。
我々は NPA のような一般化された問題に対するよく知られた階層性やラッサール階層、一般 SDP の拡張対称性の低下を示す。
論文 参考訳（メタデータ） (2023-09-25T09:01:30Z) - TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
GPT-4のこれらの問題を解決する能力は非並列であり、Program-of-Thoughts Promptingの精度は51%である。
TheoremQAは、350の定理をカバーする800の高品質な質問を含むドメインの専門家によってキュレートされる。
論文 参考訳（メタデータ） (2023-05-21T17:51:35Z) - Finite mathematics as the most general (fundamental) mathematics [0.0]
標数$p$の有限環に基づく量子理論は、標準量子論よりも一般である、なぜなら後者は形式的な極限$ptoinfty$における前者の退化の場合であるからである。
論文 参考訳（メタデータ） (2022-03-09T18:46:57Z) - Quantum double aspects of surface code models [77.34726150561087]
基礎となる量子double $D(G)$対称性を持つ正方格子上でのフォールトトレラント量子コンピューティングの北エフモデルを再検討する。
有限次元ホップ代数$H$に基づいて、我々の構成がどのように$D(H)$モデルに一般化するかを示す。
論文 参考訳（メタデータ） (2021-06-25T17:03:38Z) - Discrete Math with Programming: A Principled Approach [0.0]
離散数学はプログラミングでよりよく教えられると長年主張されてきた。
本稿では、離散数学のすべての中心的な概念をサポートするアプローチを紹介する。
数学や論理文は高いレベルで正確に表現され、コンピュータ上で実行される。
論文 参考訳（メタデータ） (2020-11-28T03:41:27Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。