論文の概要: A Formalization of Operads in Coq
- arxiv url: http://arxiv.org/abs/2303.08894v1
- Date: Wed, 15 Mar 2023 19:29:40 GMT
- ステータス: 処理完了
- システム内更新日: 2023-03-17 18:08:29.220397
- Title: A Formalization of Operads in Coq
- Title(参考訳): coqにおけるオペラの形式化
- Authors: Zachary Flores, Angelo Taranto, Eric Bond, Yakir Forman
- Abstract要約: 本稿では,証明アシスタントであるCoqで操作された関数の形式化について論じる。
CoqはV-SPELLS内でのメタ言語開発のための公式な数学的基盤を提供する。
私たちの研究は、私たちの知る限りでは、重要な自動化を備えた証明アシスタント内でのオペラッドの初めての公式化も提供しています。
- 参考スコア(独自算出の注目度): 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: What provides the highest level of assurance for correctness of execution
within a programming language? One answer, and our solution in particular, to
this problem is to provide a formalization for, if it exists, the denotational
semantics of a programming language. Achieving such a formalization provides a
gold standard for ensuring a programming language is correct-by-construction.
In our effort on the DARPA V-SPELLS program, we worked to provide a foundation
for the denotational semantics of a meta-language using a mathematical object
known as an operad. This object has compositional properties which are vital to
building languages from smaller pieces. In this paper, we discuss our
formalization of an operad in the proof assistant Coq. Moreover, our definition
within Coq is capable of providing proofs that objects specified within Coq are
operads. This work within Coq provides a formal mathematical basis for our
meta-language development within V-SPELLS. Our work also provides, to our
knowledge, the first known formalization of operads within a proof assistant
that has significant automation, as well as a model that can be replicated
without knowledge of Homotopy Type Theory.
- Abstract(参考訳): プログラミング言語における実行の正確性に対する最高レベルの保証を提供するものは何か?
この問題に対する私たちの解決策は、プログラミング言語の表記意味論(denotational semantics)が存在する場合、形式化を提供することです。
このような形式化を実現することは、プログラミング言語が正しい構成であることを保証するための金の標準を提供する。
DARPA V-SPELLSプログラムの取り組みとして,オペラッドとして知られる数学的対象を用いたメタ言語の意味論の基盤を提供する。
このオブジェクトは、小さな部品から言語を構築するのに不可欠な合成特性を持っています。
本稿では,証明アシスタントcoqにおける操作の形式化について述べる。
さらに、Coq内での定義は、Coq内で指定されたオブジェクトが操作可能であるという証明を提供することができる。
この研究は、V-SPELLSにおけるメタ言語開発のための公式な数学的基礎を提供する。
私たちの研究は、我々の知る限り、非常に自動化された証明アシスタント内のオペラッドの最初の公式化や、ホモトピー型理論の知識なしに複製できるモデルも提供しています。
関連論文リスト
- Natural Language Embedded Programs for Hybrid Language Symbolic
Reasoning [86.92053166457116]
本研究では,数学・記号的推論,自然言語理解,後続の課題に対処するための統合フレームワークとして,自然言語組み込みプログラム(NLEP)を提案する。
我々のアプローチは,構造化知識の自然言語表現を含むデータ構造上の関数を定義する完全なPythonプログラムを生成するよう,言語モデルに促す。
Pythonインタープリタが生成されたコードを実行し、出力をプリントする。
論文 参考訳(メタデータ) (2023-09-19T17:54:21Z) - Oracle Computability and Turing Reducibility in the Calculus of
Inductive Constructions [0.0]
インダクティブ・コンストラクションの計算におけるオラクル計算可能性とチューリング再現性の概念を総合的に展開する。
通常、合成手法では、メタレベル関数に基づいたオラクル計算の定義を用いる。
チューリングの再現性は上半格子を形成し、決定可能性を持ち、真理値の再現性よりも厳密に表現可能であることを示す。
論文 参考訳(メタデータ) (2023-07-28T13:16:46Z) - Enhancing Language Representation with Constructional Information for
Natural Language Understanding [5.945710973349298]
構成文法(CxG)を導入し,形式と意味のペアリングを強調した。
使用法に基づく構築文法を作業の基盤として採用する。
HyCxGフレームワークは3段階のソリューションを通じて言語表現を強化するために提案されている。
論文 参考訳(メタデータ) (2023-06-05T12:15:12Z) - Implementing Dynamic Programming in Computability Logic Web [0.0]
本稿では,アルゴリズムとその対応するアルゴリズム言語であるCoLwebについて述べる。
CoLwebは、非分散コンピューティングと分散コンピューティングの両方のためのアルゴリズム設計に対して、高レベルの、証明付き、分散スタイルのアプローチを強制します。
我々は,Hhorn節の定義を視覚的ユニバーサリー量子化(BUQ)と並列ユニバーサリー量子化(PUQ)の2種類に洗練する。
論文 参考訳(メタデータ) (2023-04-04T05:33:43Z) - Towards Autoformalization of Mathematics and Code Correctness:
Experiments with Elementary Proofs [5.045988012508899]
オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。
本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
論文 参考訳(メタデータ) (2023-01-05T17:56:00Z) - Q# as a Quantum Algorithmic Language [0.0]
我々はQ#の形式的な言語定義を提供することを目標とし、言語をしっかりとした数学的基礎の上に置きます。
$lambda$-Q#は、Q#を量子アルゴル(algorithmic language)と見なす方法を示している。
論文 参考訳(メタデータ) (2022-06-07T18:42:50Z) - ReACC: A Retrieval-Augmented Code Completion Framework [53.49707123661763]
本稿では,語彙のコピーと類似したセマンティクスを持つコード参照の両方を検索により活用する検索拡張コード補完フレームワークを提案する。
我々は,Python および Java プログラミング言語のコード補完タスクにおけるアプローチを評価し,CodeXGLUE ベンチマークで最先端のパフォーマンスを実現する。
論文 参考訳(メタデータ) (2022-03-15T08:25:08Z) - Learning Symbolic Rules for Reasoning in Quasi-Natural Language [74.96601852906328]
我々は,ルールを手作業で構築することなく,自然言語入力で推論できるルールベースシステムを構築した。
本稿では,形式論理文と自然言語文の両方を表現可能な"Quasi-Natural"言語であるMetaQNLを提案する。
提案手法は,複数の推論ベンチマークにおける最先端の精度を実現する。
論文 参考訳(メタデータ) (2021-11-23T17:49:00Z) - Procedures as Programs: Hierarchical Control of Situated Agents through
Natural Language [81.73820295186727]
エージェント命令と制御のための階層的な手続き的知識を表現する強力な手法である,プログラムとしての手続きの形式化を提案する。
NL命令に対するIQAおよびALFREDデータセット上で、このフレームワークをインスタンス化する。
論文 参考訳(メタデータ) (2021-09-16T20:36:21Z) - Hierarchical Poset Decoding for Compositional Generalization in Language [52.13611501363484]
出力が部分的に順序付けられた集合(命題)である構造化予測タスクとして人間の言語理解を形式化する。
現在のエンコーダ・デコーダアーキテクチャは意味論のポーズ構造を適切に考慮していない。
本稿では,言語における合成一般化のための新しい階層型ポーズデコーディングパラダイムを提案する。
論文 参考訳(メタデータ) (2020-10-15T14:34:26Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳(メタデータ) (2020-09-07T19:50:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。