|
全研究期間にわたって，次の項目にわたって研究を進めてきた．すなわち，計算折紙に関して，（1）代数的グラフ書換理論の構築，（2) 代数的グラフ書換系に基づくグラフ書換言語の設計と実装，(3) 代数的グラフ書換系における抽象折り操作をグラフ書換操作へ具体化するための，書換系から代数系への変換である．(1)から(3)は互いに関係し，完全に順を追って研究を進められない．研究の重点は(1)から(3)へと次第に移しつつ，研究を進めた．今年度は，特に，(3)に関する研究に焦点を当て，定理証明支援系を活用して書換系を実装するプログラムの形式化をすすめ，代数系への変換とその正当性の検証を行った．定理証明支援系にはIsabelle/HOLを用い，代数系の計算にはMathematicaを用いた．両者は独立したシステムであり，プログラムや多項式の表現も異なる．このため，研究には予期した以上に多くの時間を費やした．しかし，両者には，利点，弱点があり，両者を組み合わせて研究を進めることは不可欠であった．例えば，論理的推論機能はIsabelle/HOLが優れており，高度なデータ型を駆使しての形式化も可能である．一方，制約解消計算や多項式の変形の能力は限られており，Mathematicaの利用が必要であった．
グラフ書換系の項で表現された，折紙は折紙を折るごとに，新たなグラフへと変換され，最終的に得られた折紙グラフのもつ幾何学的性質を代数計算によって証明した．この過程を形式化し，代数計算に至る推論が正しく，しかも十分に抽象的であることを確認しつつ研究を進めた．計算折紙システム（Eos)のプログラムの高度化と，Isabelle/Holの証明スクリプトが，本年度の研究成果として得られた．成果は多量のコードから成り，これらを共有可能な知見として整理するには，さらに時間を要すると考えている．
|
