理論計算機科学における指定的ラベルの役割とその応用

点击翻译按钮获取中文摘要

(a)ラベル付き引数を使った関数型言語のコンパイル方法。コンパイル方法を提案し、それを実際の関数型言語「Objective Label」で実現した。元となった言語Objective Camlには性能的に劣らず、ラベル付き引数、省略可能引数を提供している。元のObjective Camlのライブラリは完全にラベル化され、さらに省略可能引数の実用性と利便性を証明したGUIライブラリ「LablTk」も作成された。ラベルを使ったプログラミングが可読性を上げるということは確認できた。さらに、ライブラリが提供する関数の名前と型を簡単に出せるブラウザを作成し、そのライブラリのマニュアルを読まなくとも、ラベルを含む型を見るだけで機能と使用法が分かるということも確認できた。(b)ラムダ計算のさらなる拡張。ラベルを引数だけではなく、データ構造にも応用し、多相性和型(polymorphic variant)を導入した。多相性和型は以前から研究されてきたが、実際のプログラミング言語で実現されたことはなく、そのコンパイル方法の諸問題も研究されてこなかった。今回は、多相性を持たない従来の和型と効率の変わらないコンパイル方法が見つかり、多相性和型もObjective Labelに導入された。(c)型理論。ラベル付き引数と同様に、多相性和型のための型体系を定義し、その推論が可能だと証明した。オブジェクト指向と類似の多い体系になるものの、和型の特徴を生かすために様々な面で違いもある。(d)論理との関係。上の三点を優先的に研究したので、特に進展がなかった。