• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2006 Fiscal Year Annual Research Report

限量子付き等式仕様からのプログラム生成に関する研究

Research Project

Project/Area Number 16650005
Research InstitutionNagoya University

Principal Investigator

坂部 俊樹  名古屋大学, 大学院情報科学研究科, 教授 (60111829)

Co-Investigator(Kenkyū-buntansha) 酒井 正彦  名古屋大学, 大学院情報科学研究科, 教授 (50215597)
草刈 圭一朗  名古屋大学, 大学院情報科学研究科, 准教授 (90323112)
Keywords限量子付き等式仕様 / 項書換え系 / 被覆集合 / 論理式変換系
Research Abstract

本研究の目的は,変換規則によりr_i ; r_iをR_<i+1> ; R_<i+1>に変換することを繰り返えしてプログラムを自動生成する方法を開発することである.ここに,E_iは∀とヨを許した等式だけからなる論理式の集合であり,仕様という.R_iは項書換え系であり,実行可能であるのでプログラムとみなせる.R_0は既に開発済みのプログラムであり,E_0はR_0を基礎に新たに定義したい関数の定義である.あるnでE_nが空集合になれば変換プロセスは終了し,R_nが生成されたプログラムとなる.
今年度は以下の研究を行った。
1.新しい変換規則の考案:新たな関数の仕様を追加する変換規則"Introduction"を導入し,この導入によっても健全性が損なわれないことを証明した.また,この規則が必要なプログラム生成例を示した.
2.対話的変換ツールの作成:変換を対話的に進めるためのツールを開発した.変換対象の論理式が複雑になるにつれて変換候補の数が爆発的に増加する問題に対応するために,変換に有効でない候補を除去する戦略が求められる.本ツールには変換候補の枝刈りを行う戦略を組み込んだ.
3.その他:本研究が提案する変換に基づくプログラム自動生成法に密接に関係する項書換え系の停止性について,新たな決定可能なクラス解明,既存の証明法の拡張などを行った.

  • Research Products

    (5 results)

All 2007 2006

All Journal Article (5 results)

  • [Journal Article] Decidability of Innermost Termination for Semi-Constructor Term Rewriting Systems2007

    • Author(s)
      Keita Uchiyama, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, Keiichirou Kusakari
    • Journal Title

      LA-Symposium 2005 (Winter)

      Pages: 26.1-26.4

  • [Journal Article] 単純型項書き換え系上の依存対法における実効規則と直積型項へのラベル付け2007

    • Author(s)
      櫻井敬大, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹
    • Journal Title

      電子情報通信学会論文誌 J90-D・4

      Pages: 978-989

  • [Journal Article] GeneSysによるプログラム生成例とIntroduction規則の追加2006

    • Author(s)
      近藤 悟, 酒井 正彦, 西田 直樹, 坂部 俊樹, 草刈 圭一朗
    • Journal Title

      電子情報通信学会技術研究報告(SS2006-46) 106・324

      Pages: 37-42

  • [Journal Article] On Non-looping Term Rewriting2006

    • Author(s)
      Wang Yi, Masahiko Sakai
    • Journal Title

      Proc. of Eighth International Workshop on Termination

      Pages: 17-21

  • [Journal Article] 強計算依存対法による高階書換え系の停止性証明2006

    • Author(s)
      磯谷泰巨, 草刈圭一朗, 酒井正彦, 坂部俊樹, 西田直樹
    • Journal Title

      電子情報通信学会技術研究報告(SS2006-6) 106・15

      Pages: 31-36

URL: 

Published: 2008-05-08   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi