文献

J-GLOBAL ID：202202233352094500   整理番号：22A1053062

一般化応用のための遠隔縮小の忠実で定量的な概念【JST・京大機械翻訳】

A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications

著者 (4件)： Santo Jose Espirito (Centro de Matematica, Universidade do Minho, Braga, Portugal) ,  Kesner Delia (Universite de Paris, CNRS, IRIF, Paris, France) ,  Kesner Delia (Institut Universitaire de France (IUF), Paris, France) ,  Peyrot Loiec (Universite de Paris, CNRS, IRIF, Paris, France)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 13242  ページ： 285-304  発行年： 2022年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 一般化アプリケーションの交換変換に頼ることなく,[数式:原文を参照]-レデックスを非ブロック化できる遠隔縮小の概念を統合する一般化アプリケーションと呼称したラムダ-計算[数式:原文を参照]を導入した。簡単なタイプ項の強い正規化を示し,次に,定量的タイピングシステムによる強い正規化を完全に特性化した。このキャラクタリゼーションは,強い正規化の自明でない帰納的定義を用い,これは,文献中の他のものに関連しており,これは,弱いヘッド正規化戦略に基づいている。この計算は,強い正規化を保持するという意味で,忠実である2つの形式間の翻訳による明示的な置換計算に関係する。著者らは,著者らの計算[数式:原文を参照]とよく知られた計算[数式:原文を参照]が,強い正規化の等価概念を決定することを示した。結果として,[数式:原文を参照]は明示的な置換に忠実な翻訳を受け継ぎ,その強い正規化は[数式:原文を参照]のために設計された定量的タイピングシステムによって特性化されるが,定量的主題減少が交換変換に失敗するという事実にもかかわらず,その強い正規化は[数式:原文を参照]のために設計された定量的タイピングシステムによって特性化できる。Copyright The Author(s) 2022 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： 応用プログラム ,  キャラクタリゼーション ,  λ計算 ,  *正規化 ,  置換

著者キーワード (3件)： ラムダ計算 ,  一般化応用 ,  定量的タイプ

分類 (1件)： 計算理論  (JB02000A)

タイトルに関連する用語 (6件)： 一般化 ,  応用 ,  縮小 ,  忠実 ,  定量 ,  概念