|
項は型を持ち、仕様はその詳細型で与えられるような PX system の理論体系 S を設計した.ただし、S では詳細型は PX にならってクラスと呼ぶことにした.S の計算系は tree 型や自然数型などで増強された単純型つきλ計算系として設計した.また、この改変にともないプログラム抽出に使うための型つきの kleene realizability interpretation を定義した.当初はこれに困難がともなうと予想したが型つきの部分項論理を導入することにより極く自然に変更できることが判った.これにより PX の特徴である CIG技法がそのまま S でも使えることとなった.
また、四井賢一郎の協力により、S の計算系と Berardi の最適化理論を実装した.後者では四井が新たに考察したアルゴリズムにより、Berardi の本来の理論より高速な処理が実現された.当初は P2X systemを使って、実際の証明からプログラムを抽出する予定であったが、Sとその実現可能性の設計に手間取ったため、これを完成することはできなかった.そのため手作業で quotient remainder の例から新しい realizability を使ってプログラムを抽出し、これを最適化する実験を行ない期待どおりの効果を得た.また、quotient remainder の内、remainder のみを project すると quotient を計算する部分が消去されるという高山の extended projection method で指摘された効果が実現されることを確認した.また、Auckland 大学(NZ)における国際会議 DMTCS'96における招待講演において本研究の計画と中間成果を報告した.また、論文を会議録を編集した図書において出版した.(研究発表、図書"Combinatoric、Complexity、Logic" の内 pp.38-51.)
|
