様々な組合せ子の非ω-強頭部正規化可能性・非基礎ループ性・非循環性

• Item type: Trans(1)
• 公開日: 2023-08-28
• タイトル: 様々な組合せ子の非ω-強頭部正規化可能性・非基礎ループ性・非循環性
• タイトル / 言語: en
• タイトル: Non-ω-Strong Head Normalization, Non-Ground Loop and Acyclic of Several Combinators
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [通常論文] 組合せ子，非ω-強頭部正規化可能性，非基礎ループ性，非循環性，項書き換えシステム，ラムダ計算，組合せ子論理
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 島根大学総合理工学部知能情報デザイン学科
• 著者所属(英): en
• 著者所属(英): Shimane University
• 著者名: 岩見, 宗弘
• 著者名(英): Munehiro, Iwami
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: Smullyan (1985)は，多くの組合せ子を紹介している．これらの組合せ子に関してラムダ計算，組合せ子論理，項書き換えシステムの分野において多くの研究が行われてきた．岩見(2009)は，組合せ子の非循環性に対する十分条件を与え，その十分条件を用いて，組合せ子LとOの非循環性を示した．また，組合せ子Oが停止性を持たないことを示した．さらに，組合せ子Oは非基礎ループ性を持つことを示した．岩見と青戸(2012)は，無限項上の項書き換えシステムに対するω-強頭部正規化可能性の反証手続きを提案し，多くの組合せ子の書き換え規則に対するω-強頭部正規化可能性の自動反証実験を行った．Smullyan (1994)は，Smullyan (1985)で紹介した組合せ子以外にも多くの組合せ子を紹介している．これらの新しく紹介された組合せ子の書き換え規則に対するω-強頭部正規化可能性は研究されていない．また，これらの組合せ子の停止性，非循環性，非基礎ループ性，非ループ性も研究されていない．本論文では，先行研究で提案した反証手続きを用いて，これらの組合せ子の書き換え規則に対するω-強頭部正規化可能性を反証する．さらに，これらの組合せ子が停止性，非循環性，非基礎ループ性，非ループ性を持つかどうかを明らかにする．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Smullyan (1985) introduced many combinators. Many works were done with respect to these combinators in the field of lambda-calculus, combinatory logic and term rewriting systems. Iwami (2009) gave a sufficient condition for acyclic of combinators. We showed that acyclic of combinators L and O using this condition. Also, we showed that combinator O is not terminating. Furthermore, we showed that combinator O admits no ground loops. Iwami and Aoto (2012) proposed disproving procedure of ω-strong head normalization for infinitary term rewriting systems. We conducted experiments to disprove ω-strong head normalization of many combinators automatically. Smullyan (1994) introduced many combinators other than those introduced in Smullyan (1985). ω-Strong head normalization for these newly introduced combinators has not been studied. Also, termination, acyclicity, non-ground loop and non-loop of these combinators have not been studied. In this paper, we disprove ω-strong head normalization of these combinators using the disproving procedure proposed in the previous work. In addition, we study termination, acyclicity, non-ground loop, and non-loop of these combinators.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 16, 号 3, p. 14-27, 発行日 2023-08-28
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会