論文の概要: Subtyping in DHOL -- Extended preprint

• arxiv url: http://arxiv.org/abs/2507.02855v1
• Date: Thu, 03 Jul 2025 17:59:00 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-07-04 15:37:16.873109
• Title: Subtyping in DHOL -- Extended preprint
• Title（参考訳）: DHOLのサブタイプ-拡張プレプリント
• Authors: Colin Rothgang, Florian Rabe,
• Abstract要約: 最近導入された依存型高階論理(DHOL)は、表現性と自動化サポートの妥協を提供する。 我々はこの設計を活用してDHOLを改良および商型で拡張する。 拡張言語のためのHOLの構文,意味論,翻訳について述べる。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The recently introduced dependent typed higher-order logic (DHOL) offers an interesting compromise between expressiveness and automation support. It sacrifices the decidability of its type system in order to significantly extend its expressiveness over standard HOL. Yet it retains strong automated theorem proving support via a sound and complete translation to HOL. We leverage this design to extend DHOL with refinement and quotient types. Both of these are commonly requested by practitioners but rarely provided by automated theorem provers. This is because they inherently require undecidable typing and thus are very difficult to retrofit to decidable type systems. But with DHOL already doing the heavy lifting, adding them is not only possible but elegant and simple. Concretely, we add refinement and quotient types as special cases of subtyping. This turns the associated canonical inclusion resp. projection maps into identity maps and thus avoids costly changes in representation. We present the syntax, semantics, and translation to HOL for the extended language, including the proofs of soundness and completeness.
• Abstract（参考訳）: 最近導入された依存型高階論理(DHOL)は、表現性と自動化サポートの間の興味深い妥協を提供する。 標準HOLよりも表現性を著しく拡張するため、型システムの決定性を犠牲にしている。 しかし、これは音による強力な自動定理の証明とHOLへの完全翻訳を維持している。 我々はこの設計を活用してDHOLを改良および商型で拡張する。 これらは一般に実践者によって要求されるが、自動定理証明者によって提供されることは滅多にない。 これは本質的には決定不能な型付けを必要とするため、決定不能な型システムに再適合することが非常に難しいためである。 しかし、DHOLはすでに重い持ち上げをしているので、追加は可能であるだけでなく、エレガントでシンプルだ。 具体的には, サブタイピングの特別な事例として, 精細化と商型を付加する。 これにより、関連する標準包含respが変換される。 プロジェクションマップをアイデンティティマップにマップし、表現のコストのかかる変更を避ける。 本稿では,音質と完全性の証明を含む拡張言語HOLの構文,意味論,翻訳について述べる。

関連論文リスト

• Neuro-Symbolic Query Compiler [57.78201019000895]
  本稿では,このギャップを埋めるために,言語文法規則とコンパイラ設計に触発されたニューラルシンボリックなフレームワークQCompilerを提案する。 理論上は、複雑なクエリを形式化するのに最小でも十分なバックス・ナウアー形式(BNF)の文法を$G[q]$で設計する。 葉のサブクエリの原子性は、より正確な文書検索と応答生成を保証し、複雑なクエリに対処するRAGシステムの能力を大幅に改善する。
  論文  参考訳（メタデータ） (2025-05-17T09:36:03Z)
• Type-Constrained Code Generation with Language Models [51.03439021895432]
  本稿では,型システムを利用してコード生成を誘導する型制約デコード手法を提案する。 そこで本研究では,新しい接頭辞オートマトンと,在来型を探索する手法を開発し,LLM生成コードに適切な型付けを強制するための健全なアプローチを構築した。 提案手法は,コード合成,翻訳,修復作業において,コンパイルエラーを半分以上削減し,機能的正しさを著しく向上させる。
  論文  参考訳（メタデータ） (2025-04-12T15:03:00Z)
• Experiments with Choice in Dependently-Typed Higher-Order Logic [3.072340427031969]
  ヒルベルトの不定選択作用素 $epsilon$ により DHOL 項構造を拡張する。 選択項のHOL選択への変換を定義し、既存のDHOLからHOLへの変換を拡張する。 選択を必要とするHOL問題に対する拡張翻訳の評価を行った。
  論文  参考訳（メタデータ） (2024-10-11T14:49:45Z)
• Theorem Proving in Dependently-Typed Higher-Order Logic -- Extended Preprint [0.0]
  高階論理 HOL は、型付きデータ構造を表現および推論するための非常に単純な構文と意味論を提供します。 依存型理論はそのようなリッチな型システムを提供するが、HOLとはかなり概念的な違いがある。 本稿では,HOLのスタイルと概念的枠組みを維持した,依存型拡張DHOLを提案する。
  論文  参考訳（メタデータ） (2023-05-24T17:40:54Z)
• TypeT5: Seq2seq Type Inference using Static Analysis [51.153089609654174]
  本稿では,型予測をコード入力タスクとして扱う新しい型推論手法を提案する。 本手法では静的解析を用いて,型シグネチャがモデルによって予測されるコード要素毎に動的コンテキストを構築する。 また,モデルの入力コンテキストに事前の型予測を組み込んだ反復復号方式を提案する。
  論文  参考訳（メタデータ） (2023-03-16T23:48:00Z)
• Recent advances in the Self-Referencing Embedding Strings (SELFIES) library [1.9573380763700712]
  文字列に基づく分子表現は、化学情報学の応用において重要な役割を果たす。 SMILESのような伝統的な文字列ベースの表現は、生成モデルによって生成される場合、しばしば構文的および意味的誤りを引き起こす。 SELF-referencIng Embedded Strings (SELFIES) が提案された。
  論文  参考訳（メタデータ） (2023-02-07T17:24:08Z)
• Few-Shot Semantic Parsing with Language Models Trained On Code [52.23355024995237]
  Codexは同等のGPT-3モデルよりもセマンティックパーシングが優れていることがわかった。 GPT-3とは異なり、Codexは意味表現を直接ターゲットとする場合、おそらく意味解析で使われる意味表現がコードと似た構造になっているように、同じように機能する。
  論文  参考訳（メタデータ） (2021-12-16T08:34:06Z)
• Asking without Telling: Exploring Latent Ontologies in Contextual Representations [12.69022456384102]
  事前学習した文脈エンコーダは、明示的な監督なしに言語構造の意味ある概念を符号化する。 その結果,既存のアノテーションからの離脱を含む事前学習エンコーダにおける創発的構造を示す新たな証拠が得られた。
  論文  参考訳（メタデータ） (2020-04-29T23:20:40Z)
• Improve Variational Autoencoder for Text Generationwith Discrete Latent Bottleneck [52.08901549360262]
  変分オートエンコーダ(VAE)は、エンドツーエンドの表現学習において必須のツールである。 VAEは強い自己回帰デコーダで潜伏変数を無視する傾向がある。 よりコンパクトな潜在空間において暗黙的な潜在特徴マッチングを強制する原理的アプローチを提案する。
  論文  参考訳（メタデータ） (2020-04-22T14:41:37Z)

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

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