論文の概要: Complete the Cycle: Reachability Types with Expressive Cyclic References

• arxiv url: http://arxiv.org/abs/2503.07328v1
• Date: Mon, 10 Mar 2025 13:42:02 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-03-11 15:49:45.209027
• Title: Complete the Cycle: Reachability Types with Expressive Cyclic References
• Title（参考訳）: サイクルの完全性:表現的サイクル参照を持つ到達可能性タイプ
• Authors: Haotian Deng, Siyuan He, Songlin Jia, Yuyan Bao, Tiark Rompf,
• Abstract要約: Reachability Types (RT) は、関数型および高階型プログラミングにおけるエイリアスと分離を追跡するための資格型システムである。 これまでのRTシステムは、周期依存を制限する計算に基づいており、終端であることが示されている。 RTを表現的循環参照型で拡張し、ストアを通して循環依存の形成を可能にする。
• 参考スコア（独自算出の注目度）: 6.994376737187498
• License:
• Abstract: Reachability Types (RT) are a qualified type system for tracking aliasing and separation in functional and higher-order programming. By formalizing resource reachability with a sound static type system, RT enable higher-order programming patterns with runtime safety and non-interference guarantees. However, previous RT systems have been based on calculi that restrict cyclic dependencies and are shown to be terminating in the absence of built-in recursive constructs. While termination is sometimes a desirable property, simplifying reasoning and ensuring predictable behavior, it implies an inability to encode expressive programs involving non-termination and advanced recursive patterns, such as mutual recursion and various fixed-point combinators. In this paper, we address this limitation by extending RT with an expressive cyclic reference type that permits the formation of cyclic dependencies through the store, thereby allowing the system to encode recursive programming patterns without relying on extra built-in constructs. In addition, we redesign qualifier typing in the reference introduction rule, allowing separate references to point to a shared and tracked referent. We formalize the system as the $\lambda^{\circ}_{<:}$-calculus, with a mechanized soundness proof via the standard progress and preservation lemmas. As a demonstration, we implement a well-typed fixpoint operator, proving that recursive patterns can be encoded using the novel cyclic reference type.
• Abstract（参考訳）: Reachability Types (RT) は、関数型および高階型プログラミングにおけるエイリアスと分離を追跡するための資格型システムである。 健全な静的型システムでリソースの到達性を形式化することにより、RTは実行時の安全性と非干渉保証を備えた高階プログラミングパターンを実現する。 しかし、従来のRTシステムは、循環依存を制限する計算に基づいており、組み込まれた再帰的構造が欠如していることが示されている。 終端は、しばしば望ましい性質であり、推論を単純化し、予測可能な振る舞いを保証するが、それは、相互再帰や様々な固定点コンビネータのような、非終端および高度な再帰パターンを含む表現的プログラムを符号化できないことを意味する。 本稿では,RTを表現型巡回参照型で拡張することで,ストア内での循環依存の形成を可能にし,余分な組込み構造に依存しない再帰的プログラミングパターンを符号化することで,この制限に対処する。 さらに、参照紹介規則における修飾子型付けを再設計し、別の参照が共有および追跡された参照を指し示すようにした。 我々は,標準的な進歩と保存の補題を通した機械的健全性証明を用いて,このシステムを $\lambda^{\circ}_{<:}$-calculus として定式化する。 実演として、我々は、新しい循環参照型を用いて再帰的パターンを符号化できることを証明し、よく型付けされた固定点演算子を実装した。

関連論文リスト

• An Expressive Trace Logic for Recursive Programs [0.36832029288386137]
  本稿では, 2進状態述語, チョップ, 最小不動点に基づく, トレース式上の表現論理について述べる。 プログラムとトレース公式の両方に、直接的なスタイル、完全な構成的、意味論的意味論が備わっている。 我々の結果は、プログラミング構造と論理連結体との対応に光を当てた。
  論文  参考訳（メタデータ） (2024-11-20T08:35:29Z)
• COrAL: Order-Agnostic Language Modeling for Efficient Iterative Refinement [80.18490952057125]
  反復改良は、複雑なタスクにおける大規模言語モデル(LLM)の能力を高める効果的なパラダイムとして登場した。 我々はこれらの課題を克服するために、コンテキストワイズ順序非依存言語モデリング(COrAL)を提案する。 当社のアプローチでは、管理可能なコンテキストウィンドウ内で複数のトークン依存関係をモデル化しています。
  論文  参考訳（メタデータ） (2024-10-12T23:56:19Z)
• Tractable Offline Learning of Regular Decision Processes [50.11277112628193]
  この研究は、正則決定過程(RDP)と呼ばれる非マルコフ環境のクラスにおけるオフライン強化学習(RL)を研究する。 インスは、未来の観測と過去の相互作用からの報酬の未知の依存を実験的に捉えることができる。 多くのアルゴリズムは、まずこの未知の依存関係を自動学習技術を用いて再構築する。
  論文  参考訳（メタデータ） (2024-09-04T14:26:58Z)
• Transformer-Based Models Are Not Yet Perfect At Learning to Emulate Structural Recursion [14.739369424331478]
  本稿では,プログラミング言語領域における構造的再帰という抽象概念を,シーケンスモデリング問題や学習モデルの振る舞いにうまく結合する汎用フレームワークを提案する。 フレームワークを強力な概念ツールとして、さまざまな設定の下で異なる問題を特定します。
  論文  参考訳（メタデータ） (2024-01-23T18:07:38Z)
• Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
  本稿では, パール構造因果モデルにおいて, 因果関係などの部分的特定可能なクエリのバウンダリングの問題について議論する。 最近提案された反復EMスキームは初期化パラメータをサンプリングしてそれらの境界を内部近似する。 シンボルパラメータを実際の値に置き換えた回路構造を,単一のシンボル知識コンパイルによって得られることを示す。
  論文  参考訳（メタデータ） (2023-10-05T07:10:40Z)
• Gated Recurrent Neural Networks with Weighted Time-Delay Feedback [59.125047512495456]
  重み付き時間遅延フィードバック機構を備えた新しいゲートリカレントユニット(GRU)を導入する。 我々は、$tau$-GRUが、最先端のリカレントユニットやゲート型リカレントアーキテクチャよりも早く収束し、より一般化できることを示します。
  論文  参考訳（メタデータ） (2022-12-01T02:26:34Z)
• Differentiable Inference of Temporal Logic Formulas [1.370633147306388]
  信号時相論理式を学習するための最初のリカレントニューラルネットワークアーキテクチャを実演する。 本稿では,式推論法の最初の体系的比較について述べる。
  論文  参考訳（メタデータ） (2022-08-10T16:52:23Z)
• Temporally-Consistent Surface Reconstruction using Metrically-Consistent Atlases [131.50372468579067]
  そこで本稿では,時間変化点雲列から時間一貫性のある面列を復元する手法を提案する。 我々は、再構成された表面をニューラルネットワークによって計算されたアトラスとして表現し、フレーム間の対応性を確立することができる。 当社のアプローチは、いくつかの挑戦的なデータセットにおいて、最先端のものよりも優れています。
  論文  参考訳（メタデータ） (2021-11-12T17:48:25Z)
• Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules [9.1570563482476]
  2つのプログラムは、1つのプログラムをもう1つのプログラムに書き換える、書き換え規則の一連の適用が存在する場合と同値である。 本稿では,プログラムペア間の等価性の証明を生成するために,トランスフォーマーモデルに基づくニューラルネットワークアーキテクチャを提案する。 我々のシステムであるS4Eqは、1万対の等価プログラムをキュレートしたデータセット上で97%の証明成功を達成した。
  論文  参考訳（メタデータ） (2021-09-22T01:37:08Z)
• High-performance symbolic-numerics via multiple dispatch [52.77024349608834]
  Symbolics.jlは拡張可能なシンボルシステムで、動的多重ディスパッチを使用してドメインのニーズに応じて振る舞いを変更する。 実装に依存しないアクションでジェネリックapiを形式化することで、システムに最適化されたデータ構造を遡及的に追加できることを示します。 従来の用語書き換えシンプリファイアと電子グラフベースの用語書き換えシンプリファイアをスワップする機能を実証する。
  論文  参考訳（メタデータ） (2021-05-09T14:22:43Z)
• Pattern-aware Data Augmentation for Query Rewriting in Voice Assistant Systems [10.332550622090718]
  既存のトレーニングペアからパターンを学習し、ラベルの書き換えから書き換え候補を逆に生成し、不十分なQRトレーニングデータを補う拡張フレームワークを提案する。 実験の結果,QRベースラインを十分に訓練し,低リソース領域やローカライズ領域でのQR性能向上に有効である可能性が示された。
  論文  参考訳（メタデータ） (2020-12-21T16:36:32Z)

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

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