文献

J-GLOBAL ID：202002250808823647   整理番号：20A1795907

良くスコープされたde Bruijnシンタックス上のバインダを意識した再帰【JST・京大機械翻訳】

Binder aware recursion over well-scoped de Bruijn syntax

著者 (3件)： Kaiser Jonas (Saarland University, Germany) ,  Schaefer Steven (Saarland University, Germany) ,  Stark Kathrin (Saarland University, Germany)
資料名： ACM Proceedings  (ACM Proceedings)
号： CPP 2018  ページ： 293-306  発行年： 2018年 
JST資料番号： D0698C  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 結合による構文のde Bruijn表現は,通常使用されるが,しかし,それが再帰するときに欠陥がある。誘導型表現に関連した構造再帰原理は,結合規律に認識されないので,各再帰的定義は,可変インスタンス化による互換性の別の証明を必要とする。構文的トラバースのAllaisの概念を拡張することによりこの問題を解決し,インスタント化互換性再帰性のためのフレームワークを得た。フレームワークは,多変量,潜在的相互再帰的構文システムを扱うのに十分に一般的である。このフレームワークにより,システムFに対する可変再命名とインスタンス化,構文指向タイピング,およびある非ary論理関係を定義した。これらの定義は,弱いおよび強い正規化と同様に,タイプ保存の簡潔な証明につながる。本フレームワークは,Autosubst Coqライブラリの将来のバージョンの理論的基礎として役立つように設計した。すべての開発と事例研究を,Coq証明支援で定式化した。Please refer to this article’s citation page on the publisher website for specific rights information. Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 互換性 ,  *構文論 ,  事例研究 ,  定式化 ,  正規化 ,  再帰性
準シソーラス用語： 構文 ,  多変量 , 【Automatic Indexing@JST】

著者キーワード (4件)： - ,  - ,  - ,  -

分類 (1件)： 数理言語学  (JB05000V)

タイトルに関連する用語 (3件)： シンタックス ,  バインダ ,  意識