論文の概要: Coinduction Plain and Simple
- arxiv url: http://arxiv.org/abs/2007.09909v2
- Date: Wed, 22 Jul 2020 08:23:10 GMT
- ステータス: 処理完了
- システム内更新日: 2022-11-08 14:24:12.096437
- Title: Coinduction Plain and Simple
- Title(参考訳): 簡素で簡素な造語
- Authors: Fran\c{c}ois Bry
- Abstract要約: コインダクション(Coinduction)とは、無限のストリームを定義する手法、いわゆるコデータ、およびコインダクテッド指定コデータの等価性を証明する技術である。
本稿では、まず、宣言型プログラミングにおける造語をレビューする。次に、コデータを特定するためによく使われる形式主義をレビューし、少し拡張する。第三に、元々は等式述語のみに規定されていた造語証明の原理を他の述語に一般化する。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: Coinduction refers to both a technique for the definition of infinite
streams, so-called codata, and a technique for proving the equality of
coinductively specified codata. This article first reviews coinduction in
declarative programming. Second, it reviews and slightly extends the formalism
commonly used for specifying codata. Third, it generalizes the coinduction
proof principle, which has been originally specified for the equality predicate
only, to other predicates. This generalization makes the coinduction proof
principle more intuitive and stresses its closeness with structural induction.
The article finally suggests in its conclusion extensions of functional and
logic programming with limited and decidable forms of the generalized
coinduction proof principle.
- Abstract(参考訳): コインダクション(Coinduction)とは、無限ストリームの定義手法、いわゆるコデータ(codata)、および帰納的特定コデータの等価性を証明する技術である。
この記事では、最初に宣言型プログラミングの造語をレビューします。
第2に、codataの指定に一般的に使用される形式をレビューし、わずかに拡張する。
第3に、元々は等式述語のみに指定されていた造語証明の原理を他の述語に一般化する。
この一般化は、造語証明の原理をより直感的にし、構造的帰納と密接性を強調する。
この記事は最終的に、一般化造語証明原理の限定的で決定可能な形式を持つ関数型および論理型プログラミングの結論拡張について提案する。
関連論文リスト
- An elementary proof of a universal approximation theorem [0.0]
本稿では、3つの隠れた層を持つニューラルネットワークに対する普遍近似定理の基本的な証明と、連続的、有界な活性化関数の増大について述べる。
結果は最もよく知られた結果よりも弱いが、学部分析以外の機械は使われていないという意味では初等的な証明である。
論文 参考訳(メタデータ) (2024-06-14T13:16:48Z) - Proving Theorems Recursively [80.42431358105482]
本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。
従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。
また,POETRYが検出した最大証明長は10~26。
論文 参考訳(メタデータ) (2024-05-23T10:35:08Z) - Range-Restricted Interpolation through Clausal Tableaux [0.0]
一階述語論理の入力からクレイグの出力へ、範囲制限とホーン特性の変動がどのように受け継がれるかを示す。
証明システムは、一階ATPに由来するクラウスアル・タドーである。
論文 参考訳(メタデータ) (2023-06-06T10:42:40Z) - Abductive Commonsense Reasoning Exploiting Mutually Exclusive
Explanations [118.0818807474809]
帰納的推論は、イベントのもっともらしい説明を見つけることを目的としている。
自然言語処理における帰納的推論のための既存のアプローチは、しばしば監督のために手動で生成されたアノテーションに依存している。
この研究は、ある文脈に対して、説明のサブセットのみが正しいという事実を活用する、帰納的コモンセンス推論のアプローチを提案する。
論文 参考訳(メタデータ) (2023-05-24T01:35:10Z) - A Proof of Specker's Principle [0.0]
私は3つの仮定からSpeckerの原理を導出します。
これら3つの仮定を議論し、これら2つの命題を満たす非Specker集合の正準例を記述する。
証明の核心は、私が紙を開けたニネヴェのシーザーについてのスペクターの物語の変種によって説明されている。
論文 参考訳(メタデータ) (2023-05-13T13:25:16Z) - Don't Explain Noise: Robust Counterfactuals for Randomized Ensembles [50.81061839052459]
我々は確率論的問題として、堅牢な対実的説明の生成を定式化する。
アンサンブルモデルのロバスト性とベース学習者のロバスト性との関係を示す。
本手法は, 反実的説明から初期観測までの距離をわずかに増加させるだけで, 高いロバスト性を実現する。
論文 参考訳(メタデータ) (2022-05-27T17:28:54Z) - ProofWriter: Generating Implications, Proofs, and Abductive Statements
over Natural Language [19.917022148887273]
トランスフォーマーは自然言語理論上の論理推論をエミュレートすることが示されている。
ProofWriterと呼ばれる生成モデルは、理論の意味とそれらをサポートする自然言語の証明の両方を確実に生成できることを示しています。
論文 参考訳(メタデータ) (2020-12-24T00:55:46Z) - A Unified Taylor Framework for Revisiting Attribution Methods [49.03783992773811]
我々はTaylor属性フレームワークを提案し、7つの主流属性メソッドをフレームワークに再構成する。
我々はTaylor属性フレームワークにおいて、良い属性の3つの原則を確立する。
論文 参考訳(メタデータ) (2020-08-21T22:07:06Z) - Partial Orders, Residuation, and First-Order Linear Logic [0.20305676256390934]
各列の先行式上の一意線型順序を定義するような部分順序制約を加えることで、多くの有用な論理作用素を定義できることを示す。
論文 参考訳(メタデータ) (2020-08-14T13:06:21Z) - Random extrapolation for primal-dual coordinate descent [61.55967255151027]
本稿では,データ行列の疎度と目的関数の好適な構造に適応する,ランダムに外挿した原始-双対座標降下法を提案する。
一般凸凹の場合, 主対差と目的値に対するシーケンスのほぼ確実に収束と最適サブ線形収束率を示す。
論文 参考訳(メタデータ) (2020-07-13T17:39:35Z) - Adversarial Domain Adaptation with Prototype-Based Normalized Output
Conditioner [63.66680896910619]
まず、識別器の入力として出力予測を用いて特徴を予測する単純な連結条件付け戦略を再検討する。
我々は、同じノルムを持つノルム予測を拡大し、連結条件を改善するとともに、導出法を正規化アウトプットディショナー(NOUN)として表現する。
出力空間ではなく,プロトタイプ空間におけるクロスドメイン特徴アライメントを条件にすることを提案する。
オブジェクト認識とセマンティックセグメンテーションの両方の実験により、NOUNはマルチモーダル構造を効果的に整列し、最先端のドメイン逆行訓練方法よりも優れていることが示されている。
論文 参考訳(メタデータ) (2020-03-30T08:50:32Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。