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

Smullyan (1985)は，多くの組合せ子を紹介している．これらの組合せ子に関してラムダ計算，組合せ子論理，項書き換えシステムの分野において多くの研究が行われてきた．岩見(2009)は，組合せ子の非循環性に対する十分条件を与え，その十分条件を用いて，組合せ子LとOの非循環性を示した．また，組合せ子Oが停止性を持たないことを示した．さらに，組合せ子Oは非基礎ループ性を持つことを示した．岩見と青戸(2012)は，無限項上の項書き換えシステムに対するω-強頭部正規化可能性の反証手続きを提案し，多くの組合せ子の書き換え規則に対するω-強頭部正規化可能性の自動反証実験を行った．Smullyan (1994)は，Smullyan (1985)で紹介した組合せ子以外にも多くの組合せ子を紹介している．これらの新しく紹介された組合せ子の書き換え規則に対するω-強頭部正規化可能性は研究されていない．また，これらの組合せ子の停止性，非循環性，非基礎ループ性，非ループ性も研究されていない．本論文では，先行研究で提案した反証手続きを用いて，これらの組合せ子の書き換え規則に対するω-強頭部正規化可能性を反証する．さらに，これらの組合せ子が停止性，非循環性，非基礎ループ性，非ループ性を持つかどうかを明らかにする．

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.