Search Results 1-20 of 239

  • Algebraic Representation for Structure of Chinese Characters : An Aspect of Formal Content in Humanities  [in Japanese]

    白須 裕之

    … The notion of formal system is an important subject underlying knowledge information technologies. … In order to present it, we use equational logic and term rewriting as formal systems. … An equational calculus presents unification rules for Chinese characters, and a term rewriting system produces an abstract model of their verification. …

    東方学報 = Journal of Oriental studies 94, 282-268, 2019-12

    IR  DOI 

  • Proving Level-confluence of Conditional Term Rewriteing Systems  [in Japanese]

    加賀谷 有輝 , 青戸 等人

    項書き換えシステム(TRS)は等式理論に基づく計算モデルであり,様々な性質の検証法が研究されている.合流性は項書き換えシステムによる計算解の一意性に関する重要な性質である.条件付き項書き換えシステム(CTRS)はTRSの書き換え規則に条件を付加して得られる計算モデルであり,関数型プログラムを考える場合にはより自然なモデルとなっている.TRSの階層合流性はCTRSの計算の階層ごとに合流性が成立すると …

    情報処理学会論文誌プログラミング(PRO) 12(5), 5-5, 2019-11-20

    IPSJ 

  • Proving Local Sufficient Completeness of Term Rewriting Systems  [in Japanese]

    白石 智輝 , 青戸 等人

    等式論理に基づく計算モデルとして項書き換えシステムがある.項書き換えシステム上で,関数がすべての入力に対して解を持つかという性質は十分完全性と呼ばれる.十分完全性は項書き換えシステムにおける帰納的定理の自動証明に重要な役割を果たしている.十分完全性の十分条件の1つは停止性と擬簡約性を持つことである.停止性については様々な自動証明法が研究されており,様々な検証ツールも開発されている.また,擬簡約性に …

    情報処理学会論文誌プログラミング(PRO) 12(5), 4-4, 2019-11-20

    IPSJ 

  • Automatically Proving Sufficient Completeness of Conditional Term Rewriting Systems  [in Japanese]

    東和田 直輝 , 青戸 等人

    項書き換えシステム(TRS)は,関数型プログラミング言語の形式的な計算モデルであり,書き換え規則の集合として与えられる.TRSでは,プログラムに関する様々な性質や操作を言語の制約にとらわれず柔軟に取り扱うことが可能である.TRSの拡張として,条件部が加わった書き換え規則を扱う条件付き項書き換えシステム(CTRS)がある.TRS上で,関数がすべての入力に対して解を持つかという性質は十分完全性と呼ばれ …

    情報処理学会論文誌プログラミング(PRO) 12(5), 3-3, 2019-11-20

    IPSJ 

  • Extending Narrowing Trees to Basic Narrowing in Term Rewriting  [in Japanese]

    前田 侑也 , 西田 直樹 , 酒井 正彦 , 小林 倫也

    電子情報通信学会技術研究報告 = IEICE technical report : 信学技報 118(384), 73-78, 2019-01-15

  • An Attempt to Formalize Unification Rules of Chinese Characters Based on Term Rewriting System  [in Japanese]

    守岡 知彦

    項書き換え系を用いた漢字の包摂規準の形式化手法を提案する.漢字の包摂規準は本質的に木構造のパターンに対する書き換えとして記述されているため,項書き換え系における書き換え規則として表現することは容易である.また,完備化アルゴリズムを用いることで計算機にとってより扱いやすい形に変換することができる.しかしながら,包摂除外をはじめとする包摂規準の例外や定義の不完全さ,符号化された漢字レパートリの不斉一さ …

    情報処理学会論文誌 59(2), 332-340, 2018-02-15

    IPSJ  IR 

  • Reversible computation in term rewriting

    Nishida Naoki , Palacios Adrián , Vidal Germán

    ファイル公開:2020-01-01

    Journal of Logical and Algebraic Methods in Programming (94), 128-149, 2018-01

    IR 

  • On the Unification of Rational Terms.  [in Japanese]

    IWAMI Munehiro

    <p>有限項に対する(一階の)単一化アルゴリズムは推論規則を用いて形式化され,その停止性,健全性と完全性が多くの文献で示されている.また,いくつかの先行研究において,正則項に対する単一化アルゴリズムも推論規則を用いて与えられている.しかしながら,それらの研究において,与えられた等式集合から推論規則により得られた集合の解ともとの集合の最汎単一化子である正則代入が一致することは明確に示され …

    Computer Software 35(4), 151-163, 2018

    J-STAGE 

  • Static Dependency Pair Method in Functional Programs

    KUSAKARI Keiichirou

    … <p>We have previously introduced the static dependency pair method that proves termination by analyzing the static recursive structure of various extensions of term rewriting systems for handling higher-order functions. … To bring the static dependency pair method close to existing functional programs, we also extend the method to term rewriting models in which functional abstractions with patterns are permitted. …

    IEICE Transactions on Information and Systems E101.D(6), 1491-1502, 2018

    J-STAGE 

  • Proving Confluence of Hierarchical Conditional Term Rewriting Systems without Sufficient Completeness  [in Japanese]

    黒田 貴之 , 西田 直樹 , 関 浩之

    電子情報通信学会技術研究報告 = IEICE technical report : 信学技報 116(512), 103-108, 2017-03-09

  • On Proving Termination and Inductive Theorems Simultaneously for Constrained Term Rewriting Systems  [in Japanese]

    川本 佳史 , 西田 直樹 , 酒井 正彦

    電子情報通信学会技術研究報告 = IEICE technical report : 信学技報 115(419), 75-80, 2016-01-25

  • On Proving Termination and Inductive Theorems Simultaneously for Constrained Term Rewriting Systems  [in Japanese]

    川本 佳史 , 西田 直樹 , 酒井 正彦

    電子情報通信学会技術研究報告 = IEICE technical report : 信学技報 115(420), 75-80, 2016-01-25

  • Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent

    Sakai Masahiko , Oyamaguchi Michio , Ogawa Mizuhito

    … A term is weakly shallow if each defined function symbol occurs either at the root or in the ground subterms, and a term rewriting system is weakly shallow if both sides of a rewrite rule are weakly shallow. …

    Lecture Notes in Computer Science (9195), 111-126, 2015-07-25

    IR 

  • An Equivalent Transformation of Constrained Term Rewriting Systems by Pattern Elimination  [in Japanese]

    長尾 貴浩 , 西田 直樹 , 酒井 正彦

    電子情報通信学会技術研究報告 = IEICE technical report : 信学技報 115(154), 167-172, 2015-07-22

  • An Equivalent Transformation of Constrained Term Rewriting Systems by Pattern Elimination  [in Japanese]

    長尾 貴浩 , 西田 直樹 , 酒井 正彦

    電子情報通信学会技術研究報告 = IEICE technical report : 信学技報 115(153), 167-172, 2015-07-22

  • Heuristics for Automatically Proving Commutativity of Function Composition for Constrained Term Rewriting Systems  [in Japanese]

    KURIKI Ryutaro , NISHIDA Naoki , SAKAI Masahiko , SAKABE Toshiki

    制約付き項書換え系における帰納的定理を書換え帰納法で検証するには,適切な補題等式を与える必要がある場合が多い.制約付き項書換え系における既存の補題生成法では,関数合成の可換性を表すような等式に対して適切な補題を生成できない.本稿では,そのような等式の自動証明に向けて2種類の補題生成法を提案する.それぞれの手法に関するヒューリスティックを提案し,既存手法で証明できない例題を本手法で自動証明できること …

    Technical report of IEICE. SS 114(510), 91-96, 2015-03-09

  • A Heuristic to Solve Inverse Unfolding Problem for Functions Dealing with Tree Structure Data  [in Japanese]

    KATO Tomofumi , NAGASHIMA Masanori , SAKAI Masahiko , NISHIDA Naoki , SAKABE Toshiki

    Unfold/Fold変換はプログラム変換や定理証明などに広く利用されている.Unfold変換とFold変換はそれぞれの逆変換の関係にはなく,多くの場合において一方の変換結果を他方の変換で元に戻すことはできない.そのため,Unfold変換の逆変換を行うことを目的とすることは意味があり,逆Unfold問題とその発見的解法が提案された.しかし,この発見的解法では自然数やリストなどの線形なデータ構造を引 …

    Technical report of IEICE. SS 114(510), 85-90, 2015-03-09

  • Implementing a Conditional Dependency Pair Method for Proving Termination of Functional Programs with Exception Handling  [in Japanese]

    OTA Koichi , HAMAGUCHI Takeshi , SAKAI Masahiko , YAMADA Akihisa , NISHIDA Naoki , SAKABE Tohiki

    本論文では,例外処理を含む関数型プログラムの停止性証明法のひとつである条件付き依存対法の実現について議論する.この手法の実現に必要となる依存対に付帯する制約の充足不能性判定は決定不能問題であるため,本論文ではその充足不能性の十分条件を示す.具体的には,制約中に用いられる組込み関数を定義する書換え規則の集合が合流性と停止性を持つことを利用して十分条件を設計する.また,提案手法を項書換え系の停止性証明 …

    Technical report of IEICE. SS 114(416), 55-60, 2015-01-26

  • On Efficacy of Narrowing in Proving Termination of Constrained Term Rewriting Systems  [in Japanese]

    UEYAMA Tomoya , NISHIDA Naoki , SAKAI Masahiko , SAKABE Toshiki

    項書換え系の停止性証明の強力な枠組みとして依存対フレームワークが提案されており,制約付き項書換え系の停止性証明のために拡張されている.そこで利用されているナローイングを用いた依存対の変換は,拡張したフレームワークにおいては停止性の反証における有効性のみが示されていた.本論文では,ナローイングを用いた依存対の変換が制約付き項書換え系の停止性の証明にも有効であることを示す.さらに,停止性の証明力を向上 …

    Technical report of IEICE. SS 114(416), 43-48, 2015-01-26

  • Implementing a Conditional Dependency Pair Method for Proving Termination of Functional Programs with Exception Handling  [in Japanese]

    OTA Koichi , HAMAGUCHI Takeshi , SAKAI Masahiko , YAMADA Akihisa , NISHIDA Naoki , SAKABE Tohiki

    本論文では,例外処理を含む関数型プログラムの停止性証明法のひとつである条件付き依存対法の実現について議論する.この手法の実現に必要となる依存対に付帯する制約の充足不能性判定は決定不能問題であるため,本論文ではその充足不能性の十分条件を示す.具体的には,制約中に用いられる組込み関数を定義する書換え規則の集合が合流性と停止性を持つことを利用して十分条件を設計する.また,提案手法を項書換え系の停止性証明 …

    Mathematical Systems Science and its Applications : IEICE technical report 114(415), 55-60, 2015-01-26

Page Top