論文の概要: Modular Composition of Inductive Types Using Lean Meta-programming
- arxiv url: http://arxiv.org/abs/2609.25427v1
- Date: Mon, 21 Sep 2026 21:26:43 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-09-23 18:04:04.119411
- Title: Modular Composition of Inductive Types Using Lean Meta-programming
- Title（参考訳）: リーンメタプログラミングを用いたインダクティブ型のモジュール構成
- Abstract要約: 帰納型はコンストラクタのクローズドなセットであり、そこから型の値を作成することができる。
本稿ではメタプログラミングに基づく帰納型および関数実装合成アルゴリズムを提案する。
これらのアルゴリズムを実装するリーン証明アシスタントに対する構文拡張のセットが提示される。
- 参考スコア（独自算出の注目度）: 1.421397337947365
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: Inductive types are ubiquitous building blocks in many programming and theorem proving languages. An inductive type is a closed set of constructors from which values of the type can be created. That set cannot be extended though once a type is defined. This limits extensibility, reuse, and modular separation of concerns when defining types and functions operating over their values. This limitation is manifested in the expression problem, where extending an expression language with new syntactic constructors without having to modify or re-compile existing ones is a challenge in almost all programming languages. This paper presents inductive type and function implementation composition algorithms based on meta-programming. In addition, a set of syntactic extensions to the Lean proof assistant implementing those algorithms are presented. This framework allows for modular reuse, composition, and extension of a subset of Lean type and function definitions. In addition, semantic subtyping relations between component and composite types are discussed both at the type theoretic and implementation levels. The framework is demonstrated on a case study, involving the composition of syntactic and semantic artifacts of three sublanguages into one language. The case study highlights both the features and limitations of the composition framework.
- Abstract（参考訳）: 帰納型は、多くのプログラミングおよび定理証明言語においてユビキタスな構成要素である。
帰納型はコンストラクタの閉じたセットであり、そこから型の値を作成することができる。
一度型が定義されても、そのセットは拡張できない。
これにより、型や関数が値上で動作するときの関心事の拡張性、再利用、モジュール化の分離が制限される。
この制限は、式言語を新しい構文コンストラクタで拡張することで、既存の言語を変更または再コンパイルする必要がなくなる、という式問題に現れます。
本稿ではメタプログラミングに基づく帰納型および関数実装合成アルゴリズムを提案する。
さらに、これらのアルゴリズムを実装するLean証明アシスタントに対する構文拡張のセットが提示される。
このフレームワークは、Lean型と関数定義のサブセットのモジュール化、構成、拡張を可能にします。
さらに, タイプ理論と実装レベルで, コンポーネントとコンポジットのセマンティック・サブタイプ関係について論じる。
このフレームワークは3つのサブ言語から1つの言語への構文的および意味的アーティファクトの合成を含むケーススタディで実証されている。
ケーススタディでは、コンポジションフレームワークの特徴と制限の両方を強調している。
関連論文リスト
- StructLens: A Structural Lens for Language Models via Maximum Spanning Trees [52.040177523973334]
StructLensは、内部構造が全体構造とどのように関係しているかを明らかにするために設計された分析フレームワークである。
以上の結果から,StructLensは従来のコサイン類似性とは大きく異なる層間類似性パターンを呈することが明らかとなった。
論文 参考訳（メタデータ） (2026-02-10T11:30:32Z) - Prompt Decorators: A Declarative and Composable Syntax for Reasoning, Formatting, and Control in LLMs [0.0]
本稿では,コンパクトな制御トークンを通じて動作を管理する宣言的・構成可能な構文であるPrompt Decoratorsを紹介する。
それぞれのデコレータは、タスクの内容を変更することなく、冗長な推論スタイル、構造、トーンなどの振る舞いの次元を変更する。
それは、予測可能で監査可能な振る舞い合成を可能にする統一構文、スコーピングモデル、決定論的処理パイプラインを定義する。
論文 参考訳（メタデータ） (2025-10-21T17:35:49Z) - Type-Constrained Code Generation with Language Models [51.03439021895432]
本稿では,型システムを利用してコード生成を誘導する型制約デコード手法を提案する。
そこで本研究では,新しい接頭辞オートマトンと,在来型を探索する手法を開発し,LLM生成コードに適切な型付けを強制するための健全なアプローチを構築した。
提案手法は,コード合成,翻訳,修復作業において,コンパイルエラーを半分以上削減し,機能的正しさを著しく向上させる。
論文 参考訳（メタデータ） (2025-04-12T15:03:00Z) - ClassInvGen: Class Invariant Synthesis using Large Language Models [11.374431160444676]
ClassInvGenは実行可能なクラス不変量とテスト入力を共同生成するメソッドである。
ClassInvGenは、(コードから)仕様を生成するために純粋なLCMベースの技術より優れていることを示す。
また、広く使われている高積分C++内のいくつかのクラスについてケーススタディを行い、実世界のコードに適用可能であることを示す。
論文 参考訳（メタデータ） (2025-02-26T08:10:57Z) - Order-Sorted Intensional Logic: Expressing Subtyping Polymorphism with Typing Assertions and Quantification over Concepts [1.104960878651584]
サブタイプ多型(subtype polymorphism)は、プログラミング言語理論において広く研究されている概念である。
本稿では,これらの概念を知識表現の文脈で活用するための順序分類論理の能力について検討する。
論文 参考訳（メタデータ） (2025-02-13T11:51:22Z) - Teaching Type Systems Implementation with Stella, an Extensible Statically Typed Programming Language [0.0]
このコースは、古典的なコンパイラ構築の基礎、特に抽象構文表現、ビジターパターン、構文解析を前提としている。
このコースは、最小限のコアと小さな拡張セットを備えた言語Stellaを中心に構築されている。
論文 参考訳（メタデータ） (2024-07-10T23:27:21Z) - Linguistic Analysis, Description, and Typological Exploration with Categorial Grammar (TheBench Guide) [0.0]
TheBenchは自然言語でモナディック構造を研究するためのツールである。
モナディック文法を記述し、分析を探索し、それらのカテゴリを通して多様な言語を比較し、フォーム意味のペアから文法のモデルを訓練する。
論文 参考訳（メタデータ） (2024-06-03T14:39:06Z) - Compositional Program Generation for Few-Shot Systematic Generalization [59.57656559816271]
コンポジションプログラムジェネレータ(CPG)と呼ばれるニューロシンボリックアーキテクチャに関する研究
CPGには3つの重要な特徴がある: 文法規則の形で、テキストモジュラリティ、テキストコンポジション、テキストタストラクションである。
SCAN と COGS のベンチマークでは,SCAN の14例と COGS の22例を使用して,完全な一般化を実現している。
論文 参考訳（メタデータ） (2023-09-28T14:33:20Z) - Benchmarking Language Models for Code Syntax Understanding [79.11525961219591]
事前学習された言語モデルは、自然言語処理とプログラム理解の両方において素晴らしい性能を示している。
本研究では,プログラムの構文構造を特定するための,最先端の事前訓練モデルの最初の徹底的なベンチマークを行う。
この結果から,既存のプログラミング言語の事前学習手法の限界が指摘され,構文構造をモデル化することの重要性が示唆された。
論文 参考訳（メタデータ） (2022-10-26T04:47:18Z) - Language Model Cascades [72.18809575261498]
テスト時に1つのモデルで繰り返し対話する、あるいは複数のモデルの合成は、さらに機能を拡張する。
制御フローと動的構造を持つ場合、確率的プログラミングのテクニックが必要となる。
この観点から、スクラッチパッド/思考連鎖、検証器、STaR、選択推論、ツール利用など、いくつかの既存のテクニックを定式化します。
論文 参考訳（メタデータ） (2022-07-21T07:35:18Z) - Hierarchical Poset Decoding for Compositional Generalization in Language [52.13611501363484]
出力が部分的に順序付けられた集合(命題)である構造化予測タスクとして人間の言語理解を形式化する。
現在のエンコーダ・デコーダアーキテクチャは意味論のポーズ構造を適切に考慮していない。
本稿では,言語における合成一般化のための新しい階層型ポーズデコーディングパラダイムを提案する。
論文 参考訳（メタデータ） (2020-10-15T14:34:26Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。