一般部分計算における形式的推論体系の利用について(<特集>一般発表)
スポンサーリンク
概要
- 論文の詳細を見る
一般部分計算では様々な手法を複合的に利用して実行前のプログラムを変換しその効率化を図る。これら諸手法を統合的に記述し問題点や適用限界を分析する枠組として、数理論理学で良く知られたシーケント推論のカット除法理論や形式的算術体系の無矛盾性証明の方法論が有効であろうと考える。本稿ではそのような研究の第一歩としてLisp関数をシーケント推論の推論図に対応付ける具体的な方法を提示し、そのカット除法の手順について論じる。また、この手順を拡張して帰納法(=原始再帰的関数)を含む推論図の冗長性を取り除くための指針についても述べる。
- 一般社団法人情報処理学会の論文
- 1998-03-23
著者
関連論文
- 変数の出現条件を用いた融合変換とその反復適用について (プログラム変換と記号・数式処理)
- 変数条件に基づく原始帰納関数の再帰融合について
- 一般部分計算における形式的推論体系の利用について(一般発表)
- 証明論的手法による一般部分計算の記述
- Shrinkability of Unbounded Sets in the Cohen Extention(Metamathematics and it's applications)