論文の概要: The nature of loops in programming

• arxiv url: http://arxiv.org/abs/2504.08126v1
• Date: Thu, 10 Apr 2025 20:58:55 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-04-21 22:23:41.260603
• Title: The nature of loops in programming
• Title（参考訳）: プログラミングにおけるループの性質
• Authors: Bertrand Meyer,
• Abstract要約: プログラムのセマンティクスと検証では、ループに関する推論は2つの異なる数学的引数を生成する必要があるため複雑である。 単一かつ単純な定義が可能で、この分割を取り除くことができる。 ループが正しいことを証明するには、不変量と不変量を考案する必要はない。 関係を識別するのに十分であり、部分的正当性と終了の両方をもたらす。
• 参考スコア（独自算出の注目度）: 37.48416208168878
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In program semantics and verification, reasoning about loops is complicated by the need to produce two separate mathematical arguments: an invariant, for functional properties (ignoring termination); and a variant, for termination (ignoring functional properties). A single and simple definition is possible, removing this split. A loop is just the limit (a variant of the reflexive transitive closure) of a Noetherian (well-founded) relation. To prove the loop correct there is no need to devise an invariant and a variant; it suffices to identify the relation, yielding both partial correctness and termination. The present note develops the (small) theory and applies it to standard loop examples and proofs of their correctness.
• Abstract（参考訳）: プログラムのセマンティクスと検証では、ループについての推論は、機能的特性(終端を無視する)のための不変(invariant)と、終端(終端を無視する)のための変項(invariant)という2つの異なる数学的引数を生成する必要性によって複雑である。 単一かつ単純な定義が可能で、この分割を取り除くことができる。 ループは、ネーター関係(十分に基礎付けられた)の極限(反射的推移的閉包の変種)である。 ループの正しさを証明するために不変量と変分を考案する必要はない; 関係を識別するのに十分であり、部分的正しさと終了の両方をもたらす。 このノートは(小さい)理論を発展させ、標準的なループの例とそれらの正しさの証明に適用する。

関連論文リスト

• Chain-of-Probe: Examining the Necessity and Accuracy of CoT Step-by-Step [81.50681925980135]
  モデル推論における心の変化を探索する手法を提案する。 心的変化のパターンを解析することにより,モデルの推論の正しさを検証した。 我々の検証では、最終回答では正しいが、多くの応答が推論プロセスに誤りを含んでいることが明らかになった。
  論文  参考訳（メタデータ） (2024-06-23T15:50:22Z)
• Neuro-Symbolic Integration Brings Causal and Reliable Reasoning Proofs [95.07757789781213]
  LLMの複雑な推論には2行のアプローチが採用されている。 1行の作業は様々な推論構造を持つLLMを誘導し、構造出力は自然に中間推論ステップと見なすことができる。 他方の行では、LCMのない宣言的解法を用いて推論処理を行い、推論精度は向上するが、解法のブラックボックスの性質により解釈性に欠ける。 具体的には,Prologインタプリタが生成した中間検索ログにアクセスし,人間可読推論に解釈可能であることを示す。
  論文  参考訳（メタデータ） (2023-11-16T11:26:21Z)
• Invariant Relations: A Bridge from Programs to Equations [1.3342735568824553]
  任意のレベルにネストしたループを持つプログラムを含む,C型プログラムの関数を導出する手法を提案する。 ループの意味を捉えるために、不変関係の概念を用いる。
  論文  参考訳（メタデータ） (2023-10-07T04:11:23Z)
• On Loop Formulas with Variables [2.1955512452222696]
  最近、フェラーリス、リー、リフシッツはグラウンド化に言及しない安定モデルの新たな定義を提案した。 我々は、Chen, Lin, Wang, Zhang による変数を持つループ公式のアイデアとの関係を示す。 論理プログラムの構文を拡張して、明示的な量化を許容し、その意味論を安定モデルの新しい言語のサブクラスとして定義する。
  論文  参考訳（メタデータ） (2023-07-15T06:20:43Z)
• A Circuit Complexity Formulation of Algorithmic Information Theory [1.5483078145498086]
  インダクティブ推論のソロモノフ理論に着想を得て,回路複雑性に基づく先行モデルを提案する。 回路複雑性によって測定された単純な説明に対する帰納的バイアスがこの問題に適切であると主張する。
  論文  参考訳（メタデータ） (2023-06-25T01:30:37Z)
• Will Bilevel Optimizers Benefit from Loops [63.22466953441521]
  AID-BiOとITD-BiOの2つの一般的な双レベルマトリクスは、自然に1つまたは2つのサブプロブレムを解決する。 AID-BiO と ITD-BiO の両ループ実装選択に適用可能な統合収束解析をまず確立する。
  論文  参考訳（メタデータ） (2022-05-27T20:28:52Z)
• Complexity assessments for decidable fragments of Set Theory. III: A quadratic reduction of constraints over nested sets to Boolean formulae [0.0]
  変換は、$x=ysetminus z$, $x neq ysetminus z$, $z =x$ という形のリテラルの結合からなる。 対象言語の式は、集合のブール環にまたがる変数と、等式、非可分性、包含性を指定する差分演算子とレギュレータを含む。 提案した翻訳は2次アルゴリズムの時間複雑度を持ち、どちらもNP完全満足度問題を持つことが知られている2つの言語を橋渡しする。
  論文  参考訳（メタデータ） (2021-12-09T09:36:39Z)
• multiPRover: Generating Multiple Proofs for Improved Interpretability in Rule Reasoning [73.09791959325204]
  我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。 PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。 本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
  論文  参考訳（メタデータ） (2021-06-02T17:58:35Z)
• GroupifyVAE: from Group-based Definition to VAE-based Unsupervised Representation Disentanglement [91.9003001845855]
  他の誘導バイアスを導入しないと、VAEベースの非監視的非絡み合いは実現できない。 グループ理論に基づく定義から導かれる制約を非確率的帰納的バイアスとして活用し,vaeに基づく教師なし不連続に対処する。 提案手法の有効性を検証するために,5つのデータセット上で,vaeベースモデルが最も目立つ1800モデルをトレーニングした。
  論文  参考訳（メタデータ） (2021-02-20T09:49:51Z)
• Recursive Rules with Aggregation: A Simple Unified Semantics [0.6662800021628273]
  本稿では,集約を伴う再帰の統一的意味論について述べる。 意味論を形式的に定義し、意味論の重要な性質を証明し、先行意味論と比較する。 私たちのセマンティクスはシンプルで、すべてのケースで望ましい結果と一致しています。
  論文  参考訳（メタデータ） (2020-07-26T04:42:44Z)

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

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