Research Paper 正当性自動保証機能を備えた高階プログラム自動変換技術

千葉, 勇輝

Description
項書き換えに基づくパターンによるプログラム変換の枠組みを拡張し,高階関数を直接取り扱うことが出来るプログラム変換枠組みの構築を目指した.理論的計算モデルとして,単純型付項書き換えシステム(Simply Typed Term Rewriting System,STTRS)を採用した.プログラム変換の正当性を検証するための手続きとしてSTTRS等価変換手続きを提案し,その理論的正しさを証明した.STTRSの枠組みで変換パターンを作成するために,STTRSパターンの概念を提案した.また,STTRSパターンによるプログラム変換を実現するために,STTRSパターンマッチングアルゴリズムを提案した. : We construct a framework of program transformation by templates which can directly deal with higher order functions by extending the framework based on first order term rewriting. Simply typed term rewriting systems (STTRS, for short) are adopted as a computational model in our framework. In order to verify the correctness of transformation in our framework, we propose an equivalent transformation of STTRSs and give sufficient condition for guaranteeing the correctness of transformation based on the equivalent transformation. We introduce the notion of STTRS patterns for creating transformation templates in our framework. STTRS pattern matching algorithm is proposed to analyze how to apply templates for transforming STTRSs.
研究種目:若手研究(B)
研究期間:2011~2014
課題番号:23700034
研究者番号:10509756
研究分野:項書き換え
Full-Text

https://dspace.jaist.ac.jp/dspace/bitstream/10119/12818/1/23700034seika.pdf

Number of accesses :  

Other information