古典線形論理のプログラミング言語への応用
スポンサーリンク
概要
- 論文の詳細を見る
線形論理のプログラミング言語への応用について考察する.変数の線形性を利用し,証明の変形を実行と見る仕組みについて述べる.線形論理は,その証明の正規形(cutのない証明)が一意に定まる構成主義論理のため,cut除去の過程を計算の実行と見ることが可能である.また,仮定の自由なコピーを許さないという線形論理の性質は,プログラミング言語での変数の出現の線形性との対応関係がある.変数に線形性があれば,変数を参照することはそこへ結合された構造体の破壊を意味するから,その参照の時点で構造体を再利用可能な資源として回収する.つまり,どこからも参照のない構造体をシステム全体から探してきて回収するプロセス(つまりゴミ集め)の必要がないシステムとなる.また,参照が一回であるという性質は,データフローによる実行の可能性も示唆する.
- 一般社団法人情報処理学会の論文
- 1994-01-20
著者
関連論文
- 「多態実行環境」: 高級言語の制御機械の高性能実現法
- 古典線形論理のプログラミング言語への応用
- OZ+の多言語インターフェース
- オブジェクト指向プログラミングのハードウェア・ファームウェアサポート (オブジェクト指向プログラミング)