| 研究概要 |
関数型プログラムでは優先順序をもつパターンマッチングによって関数を定義することができる.しかし,定義のパターンに重なりが生じた場合,通常の項書き換えシステムによるリダクションでは,プログラムの意味を直接表現することができない.そのため,優先順序付き項書き換えシステムによるリダクションに基づいてプログラムの意味を与える必要がある
優先順序付き項書き換えシステムの意味は,リダクションの近似に基づく条件付き項書き換えシステムとして与えることができる.一方,多くの関数型プログラムは優先順序付き構成子システムとして形式化可能である.優先順序付き構成子システムの意味を与える方法としては,上記のリダクションの近似に基づく方法以外に,構成子項の補パターンから生成される項書き換えシステムのリダクションに基づく方法がある.
研究では,補パターンに基づく方法を発展させ,補代入の概念を用いて項書き換えシステムを構成する手法を提案した.我々の提案した手法は,リダクションの近似を使わずに優先順位付き書き換えの意味を与えることができ,計算機上の実装が容易である.さらに,リダクションの近似による意味付けでは取り扱うことができない非線形パターンに対しても適用可能な場合がある.さらに,本研究では,リダクションの近似に基づく意味付けと補代入に基づく意味付けを理論的に解析し,左線形で十分完全な順序付き構成子システムでは,両者の意味付けが計算モデルとしては等価となることを明らかにした.
|
