純関数背後のシーリングポインタベース最適化【JST・京大機械翻訳】

Selsam Daniel; Hudon Simon; de Moura Leonardo

プレプリント

J-GLOBAL ID：202202201720417952 整理番号：22P0118933

純関数背後のシーリングポインタベース最適化【JST・京大機械翻訳】

Sealing Pointer-Based Optimizations Behind Pure Functions

出版者サイト {{ this.onShowPLink() }} 複写サービスで全文入手
高度な検索・分析はJDreamⅢで

この文献はプレプリントです。プレプリントについてはこちらをご確認ください。

著者 (3件)： , ,
資料名：
発行年： 2020年03月03日プレプリントサーバーでの情報更新日： 2020年05月30日
JST資料番号： O7000B 資料種別：プレプリント
記事区分：プレプリント発行国：アメリカ合衆国 (USA) 言語：英語 (EN)

機能的プログラミング言語は,自動推論システムの構築に特に良く適合し,(他の理由の)論理的用語は帰納的タイプによってよくモデル化されるので,用語を高次結合者として一般的に実行でき,バックトラッキングは持続的データ構造によって劇的に単純化される。しかし,既存の純粋機能プログラミング言語は,これらのドメインにおいて大きな制限を受け,そのグラフサイズとは対照的に用語のツリーサイズに比例する時間を必要とする。この限界は,LeanとCoqのような対話型定理証明者のための自動化を構築するとき,特に壊滅的であり,そのために,項木サイズの指数関数的ブローアップは,一般的で,予防するのが難しいことを証明した。最適スケーリングを回復するのに必要な全ては,項のメモリアドレスに関する簡単な操作を実行する能力であり,これらの操作を自由に使用することは,参照透明性の基本的前提を明確に破る。純粋な機能的インタフェイスの背後の必要なポインタアドレス操作をシールするために依存タイプを用いる方法を示し,一方,無視できる量の付加的信用しか必要としなかった。このアプローチをLeanの到来バージョン(v4)に実装し,また,著者らのアプローチを,依存型理論に基づく他の言語によって採用することができた。【JST・京大機械翻訳】

, , , , , , , , , , ,
, , , 【Automatic Indexing@JST】

計算理論 , 汎用プログラミング言語 , 計算機システム開発 , 応用プログラミング言語 , 数理言語学

前のページに戻る