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

Program verification based on higher order rewriting systems

Research Project

Project/Area Number 07680347
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeSingle-year Grants
Section一般
Research Field 計算機科学
Research InstitutionJapan Advanced Institute of Science and Technology, Hokuriku

Principal Investigator

TOYAMA Yoshihito  Japan Advanced Institute of Science and Technology, Hokuriku, Computer Science Department, Professor, 情報科学研究科, 教授 (00251968)

Co-Investigator(Kenkyū-buntansha) SAKAI Masahiko  Nagoya University, Graduate School of Engineering, Associate Professor, 大学院・工学研究科, 助教授 (50215597)
Project Period (FY) 1995 – 1997
Project Status Completed (Fiscal Year 1997)
Budget Amount *help
¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 1997: ¥400,000 (Direct Cost: ¥400,000)
Fiscal Year 1996: ¥300,000 (Direct Cost: ¥300,000)
Keywordsterm rewriting system / higher order rewriting / confluence property / termination / reduction
Research Abstract

We have studied the termination property, the confluence property, and the reduction strategy of rewriting systems, which are the basis of higher order rewriting techniques. Through theoretical analysis and experiment, we have obtained the following results :
(1) An extended recursive decomposition ordering for higher order rewriting systems is proposed. This recursive decomposition ordering is useful for proving termination of higher order rewriting systems.
(2) Composable properties of term rewriting systems is presented. The key idea of our composability result is a top-down labeling. Using this labeling, it is proven that modular properties are composable for a naive sort attachment.
(3) It is shown that index reduction is normalizing for the class of stable balanced joinable strong sequential systems. This result offers the basis of effective computation methods of functional language.
(4) The modular property of left-linear complete term rewriting systems is proven, which is important in building algebraic specifications.
(5) We give an operational semantics of priority term rewriting systems by using conditional systems. By defining the class of strong sequential systems, we show that the index rewriting gives a normalizing strategy for priority term rewriting systems.

Report

(4 results)
  • 1997 Annual Research Report   Final Research Report Summary
  • 1996 Annual Research Report
  • 1995 Annual Research Report
  • Research Products

    (28 results)

All Other

All Publications (28 results)

  • [Publications] Y.Toyama: "Church-Rosser property and unique normal form property of non-duplicating term rewriting systems" Lecture Notes in Comput.Sci.968. 316-331 (1995)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Y.Toyama: "Termination for the direct sumof left-linear complete term rewriting systems" J.ACM. 42. 1275-1304 (1995)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] M.Sakai: "Semantics and strong sequentiality of priority term rewriting systems" Lecture Notes in Comput.Sci.1103. 377-391 (1996)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] M.Sakai: "Left-incompatible term rewritisg systems and functional strategy" IEICE Trons.on Information andSystem. E88-D. 1176-1182 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] T.Aoto: "On Composable properties of term rewriting systems" Lecture Notes in Comput.Sci.1298. 114-128 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] T.Aoto: "Persistency of confluence" J.of Universal Comput.Sci.3. 1134-1147 (1997)

    • Description
      「研究成果報告書概要(和文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Y.Toyama: "Church-Rosser Property and unique normal form property of non-duplicating term rewriting systems" Lecture Notes in Comput.Sci.968. 316-331 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] Y.Tayama: "Termination for the direct sum of left-limear complete term rewriting systems" J.ACM. 42. 1275-1304 (1995)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] M.Sakai: "Semantics and strong sequentiality of priority term rewriting systems" Lecture Notes in Comput.Sci.1103. 377-391 (1996)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] M.Sakai: "Left-in compatible term rewriting systems and functional strategy" IEICE Trons.on Information and System. E88-D. 1176-1182 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] T.Aoto: "On Composable properties of term rewriting systems" Lecture Notes in Comput.Sci.1298. 114-128 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] T.Aoto: "Persistoncy of Confluence" J.of Universal Comput.Sci.3. 1134-1147 (1997)

    • Description
      「研究成果報告書概要(欧文)」より
    • Related Report
      1997 Final Research Report Summary
  • [Publications] T.Aoto: "On Composable properties of term rewriting systems" Lecture Notes in Comput.Sci.1298. 114-128 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] T.Aoto: "Persistency of Confluence" Journal of Universal Comput.Sci.3.11. 1134-1148 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] T.Aoto: "Tree lifting orderings for termimation trans formation of term rewriting systems" Proc.of LA symposium(1997-07). 109-114 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] 岩見宗弘: "項書換え系の停止性の順序ソ-トに関する永続性について" ソフトウエア科学会第14回大会論文集. 357-360 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] 草刈圭一郎: "項書換え系の停止性自動証明法の提案" ソフトウエア科学会第14回大会論文集. 361-364 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] 佐賀正芳: "リスト生成法に基づくプログラム変換" 電気関係学会北陸支部連合大会予稿集(1997). 287-287 (1997)

    • Related Report
      1997 Annual Research Report
  • [Publications] M.Sakai: "Semantics and strong seguentiality of priority term rewriting systems" Lecture Notes in Comput. Sci.1103. 377-391 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 高橋宜孝: "条件付き項書き換え系の合流性について" 信学会論文誌. J79-D-1 No.11. 897-902 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 長谷崇: "重なりのある強遂次系のインデックス簡約について" 信学技報. COMP96-32. 39-48 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 青戸等人: "項書き換え系のパ-システント性の順序付ソ-トによる拡張" 信学技報. COMP96-31. 29-38 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 岩見宗弘: "高階項書換え系における改良再帰分解順序について" 信学技報. COMP96-73. 17-24 (1996)

    • Related Report
      1996 Annual Research Report
  • [Publications] 酒井正彦,外山芳人: "優先順位付き項書き換え系の意味論とその強逐次性" 信学技報. SS95-40. 31-38 (1996)

    • Related Report
      1995 Annual Research Report
  • [Publications] 草刈圭一朗,酒井正彦,外山芳人: "非線形項書き換え系の合流性について" 信学技報. COMP95‐86. 123-129 (1996)

    • Related Report
      1995 Annual Research Report
  • [Publications] 岩見宗弘,酒井正彦,外山芳人: "高階項書き換え系の停止性について" 信学技報. COMP95‐85. 113-121 (1996)

    • Related Report
      1995 Annual Research Report
  • [Publications] T.Nagaya,M.Sakai,Y.Toyama: "NVNF‐sequentiality of Left‐linear Term Rewriting Systems" 数理解析研究所講究録. 918. 109-117 (1995)

    • Related Report
      1995 Annual Research Report
  • [Publications] Y.Toyama,M.Oyamaguchi: "Church‐Rosser Property and Unique Normal Form Property of Non‐Duplicating Term Rewriting Systems" 数理解析研究所講究録. 918. 139-149 (1995)

    • Related Report
      1995 Annual Research Report

URL: 

Published: 1996-04-01   Modified: 2016-04-21  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi