項書き換えシステムにおける生成性と局所十分完全性について

関数型プログラムでは，関数に値を入力して呼び出すことで計算を行う．そのため，関数呼び出しに対して，つねに計算が終了するという性質は重要なものである．十分完全性は，計算モデルの1つである項書き換えシステムにおいてそのような性質をモデル化したものである．項書換えシステムでは，十分完全性は，書き換えによって基底項を必ず基底構成子項に書き換えることができることをいう性質をいう．また，特定の関数呼び出しについてはつねに構成子項に書き換えられることをいう性質を，局所十分完全性と呼ぶ(Shiraishi et al., 2021)．一方，ストリームのような，要素を無限個含むようなものを対象とした計算は一般に終了することはないが，ストリームの先頭から任意個の要素を取り出しても，その次の要素を適切な値として求められることがあり，そのようなことを保証する性質を生成性と呼ぶ．生成性についても，項書き換えシステムに基づく形式化や検証方法が提案されている(Endrullis and Hendriks, 2011)．局所十分完全性と生成性の間には，計算が終了しないことがあるシステムを対象とし，値の取り出しを保証する点が共通している．しかし，従来，この2つの性質の関連性などについてはあまり報告されていない．そこで本発表では，項書き換えシステムに基づく形式化における，両者の性質の関連について報告する．そして，その関連性に基づく，生成性の検証手法を用いた局所十分完全性の検証手法を提案する．

Computations in functional programs are performed by applying functions to values. Thus, it is important to ensure calculations for function calls always terminate. Using term rewriting systems (TRSs), a computational model based on equational logic, this property is modeled as sufficient completeness. A TRS is sufficiently complete if any ground terms can be rewritten into ground constructor terms. A property that ensure particular function calls can be rewritten into constructor terms is called local sufficient completeness. There is a property known as productivity which concerns computations of infinite stream of elements. A system is called productive when one can obtain the next value after comsuming finite number of first parts of the stream. A formalization of the notion of productivity based on TRSs and its verification method are proposed in Endrullis and Hendriks (2011). Local sufficient completeness and productivity share a feature that it deals with systems that may not terminating and that ensures possibility of getting some values. However, it seems that relations of these two properties have not been investigated. In this presentation, we will report a relation of two properties based on formalization using TRSs. We also propose a verification method for local sufficient completeness using the one for productivity.