| 講演名 | 2019-01-16 項書換えにおけるナローイング計算木のベーシックナローイングへの拡張 前田 侑也(名大), 西田 直樹(名大), 酒井 正彦(名大), 小林 倫也(名大), |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 項書換え系（TRS）のナローイング計算とは，書換えに必要な代入を単一化により求め，その代入を適用して書換えを行う計算であり，すべての最内ナローイングにより導出される代入すべてを表す有限の木（ナローイング計算木）を生成する方法が提案されている．先行研究で構文決定的な条件付き項書換え系（SDCTRS）に拡張されたナローイング計算木は，与えられた最初の項からの最内ナローイング計算の解（代入）のすべてを生成する正規木文法で表現される．しかし，最内ナローイングに対応する書換えは構成子書換えに限定されている．%ため，ナローイング計算木を利用して解析できる書換えは構成子書換えに限定されていた．本稿では，ナローイング計算木が扱うナローイング計算をベーシックナローイングに拡張する．そして，紐解き後に右線形なTRSになるSDCTRSの書換えをベーシック書換えで模倣できることを示し，拡張したナローイング計算木を利用してそのようなSDCTRSの書換えの解析を可能にする．具体的には，右線形な正規CTRSの合流性証明への応用を示す． |
| 抄録(英) | Narrowing computation of a term rewriting system is an extension of rewriting by replacing matching with unification, which computes a most general unifier to apply a rewrite rule, resulting in a term obtained by applying the rewrite rule. A method to, given a system and an initial goal, generate a finite tree, so-called a narrowing tree, that represents all possible substitutions derived by innermost narrowing has been proposed. A narrowing tree that has been extended to syntactically deterministic conditional term rewriting systems (SDCTRSs) in our previous work can be represented as a regular tree grammar that generates all possible constructor substitutions obtained from innermost narrowing derivations from a given initial term to a ground term corresponding to an expected goal. Unfortunately innermost narrowing is a counterpart of constructor-based rewriting. In this article, we extend narrowing trees to basic narrowing. We show that every rewriting sequence of a terminating ultra-right-linear SDCTRS can be simulated by basic rewriting, and thus the extension enables us to apply the extended narrowing trees to analysis of such SDCTRSs. To be more precise, we show an application of extended narrowing trees to proving confluence of a right-linear normal CTRS. |
| キーワード(和) | 条件付き項書換え系 / ナローイング / 正規木文法 / 合流性 |
| キーワード(英) | conditional term rewriting system / narrowing / regular tree grammar / confluence |
| 資料番号 | MSS2018-68,SS2018-39 |
| 発行日 | 2019-01-08 (MSS, SS) |
| 研究会情報 | |
| 研究会 | MSS / SS |
|---|---|
| 開催期間 | 2019/1/15(から2日開催) |
| 開催地（和） | 沖縄県青年会館 |
| 開催地（英） | |
| テーマ（和） | 一般 |
| テーマ（英） | |
| 委員長氏名（和） | 名嘉村 盛和(琉球大) / 中田 明夫(広島市大) |
| 委員長氏名（英） | Morikazu Nakamura(Univ. of Ryukyus) / Akio Nakata(Hiroshima City Univ.) |
| 副委員長氏名（和） | 髙井 重昌(阪大) / 小林 隆志(東工大) |
| 副委員長氏名（英） | Shigemasa Takai(Osaka Univ.) / Takashi Kobayashi(Tokyo Inst. of Tech.) |
| 幹事氏名（和） | 豊嶋 伊知郎(東芝エネルギーシステムズ) / 金澤 尚史(阪大) / 肥後 芳樹(阪大) / 島 和之(広島市大) |
| 幹事氏名（英） | Ichiro Toyoshima(Toshiba) / Takahumi Kanazawa(Osaka Univ.) / Yoshiki Higo(Osaka Univ.) / Kazuyuki Shima(Hiroshima City Univ.) |
| 幹事補佐氏名（和） | 金城 秀樹(沖縄大) / 林 晋平(東工大) |
| 幹事補佐氏名（英） | Hideki Kinjo(Okinawa Univ.) / Shinpei Hayashi(Tokyo Inst. of Tech.) |
| 講演論文情報詳細 | |
| 申込み研究会 | Technical Committee on Mathematical Systems Science and its applications / Technical Committee on Software Science |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 項書換えにおけるナローイング計算木のベーシックナローイングへの拡張 |
| サブタイトル（和） | |
| タイトル（英） | Extending Narrowing Trees to Basic Narrowing in Term Rewriting |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 条件付き項書換え系 / conditional term rewriting system |
| キーワード(2)（和/英） | ナローイング / narrowing |
| キーワード(3)（和/英） | 正規木文法 / regular tree grammar |
| キーワード(4)（和/英） | 合流性 / confluence |
| 第 1 著者 氏名（和/英） | 前田 侑也 / Yuya Maeda |
| 第 1 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 第 2 著者 氏名（和/英） | 西田 直樹 / Naoki Nishida |
| 第 2 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 第 3 著者 氏名（和/英） | 酒井 正彦 / Masahiko Sakai |
| 第 3 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 第 4 著者 氏名（和/英） | 小林 倫也 / Tomoya Kobayashi |
| 第 4 著者 所属（和/英） | 名古屋大学(略称：名大) Nagoya University(略称：Nagoya Univ.) |
| 発表年月日 | 2019-01-16 |
| 資料番号 | MSS2018-68,SS2018-39 |
| 巻番号（vol） | vol.118 |
| 号番号（no） | MSS-384,SS-385 |
| ページ範囲 | pp.73-78(MSS), pp.73-78(SS), |
| ページ数 | 6 |
| 発行日 | 2019-01-08 (MSS, SS) |