文献

J-GLOBAL ID：202102268466685541   整理番号：21A0027566

型付きラムダ計算システムのための停止証明へのHowardベクトル表記システムの簡易適用【JST・京大機械翻訳】

A Simplified Application of Howard’s Vector Notation System to Termination Proofs for Typed Lambda-Calculus Systems

著者 (2件)： Okada Mitsuhiro (Keio University, Minato-ku, Tokyo, Japan) ,  Takahashi Yuta (IHPST (UMR 8590), Universite Paris 1 Pantheon-Sorbonne, CNRS, Paris, France)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 12328  ページ： 136-155  発行年： 2020年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 再帰的経路順序付けとTait-Girard計算可能性議論を組み合わせるいくつかの重要な方法があり,高次書き込みシステムの終端証明のための順序付けを提供する。JouannaudとRubioによる高次の再帰的経路順序HORPOとBlanqui,JouannaudとRubioによる計算可能性経路順序CPOは,そのような順序の用例であった。本論文では,上記の研究において,Tait-Girardの可算性法を避けて,再帰的経路順序付けのそのような拡張のもう一つの方向に関する事例研究を示した。この動機は,RTA開放問題19におけるLevyの質問から来ており,それは,あるよく見出された規則化における単純な型[数式:原文を参照]-計算[数式:原文を参照]の合理的に直接的な解釈を問う。HORPOとCPOの場合のように,[数式:原文を参照]引き抜きと経路順序付けへの適用は一つの解決策と考えられるが,次の疑問はまだ残されている。[数式:原文を参照]の終端は,[数式:原文を参照]引き抜き/応用が順序付けで直接構築されないという意味で,一次のよく見出された規則化における解釈によって証明できる。証明理論研究に関するHowardの仕事の1つを考慮して,Levyの質問に関する更なる研究に向けた事例研究として,Howard代数による経路順序付けを導入した。Copyright Springer Nature Switzerland AG 2020 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： *ベクトル ,  計算可能性 ,  事例研究 ,  λ計算
準シソーラス用語： 順序づけ , 【Automatic Indexing@JST】

著者キーワード (5件)： 経路順序付け ,  停止証明 ,  項書換え理論 ,  単純型[数式:原文を参照]計算 ,  有限型の原始再帰汎関数

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

タイトルに関連する用語 (5件)： ラムダ計算 ,  証明 ,  ベクトル ,  表記 ,  簡易