論文 / 著書情報
Article / Book Information
題目(和文)

バージョンを言語要素に持つプログラミング言語の研究

Title(English)

A Programming Language with Versions

著者(和文)

田辺裕大

Author(English)

Yudai Tanabe

出典(和文)

学位:博士(理学),学位授与機関:東京工業大学,
報告番号:甲第12329号,授与年月日:2023年3月26日,
学位の種別:課程博士,
審査員:増原 英彦,鹿島 亮,南出 靖彦,脇田 建,西崎 真也,五十嵐 淳

Citation(English)

Degree:Doctor (Science),Conferring organization: Tokyo Institute of Technology,
Report number:甲第12329号,
Conferred date:2023/3/26,
Degree Type:Course doctor,
Examiner:,,,,,

学位種別(和文)

博士論文

Category(English)

Doctoral Thesis

種別(和文)

審査の要旨

Type(English)

Exam SummaryPowered by T2R2 (Tokyo Institute Research Repository)

（博士課程）論文審査の要旨及び審査員
報告番号甲第号
氏

主査名

学位申請者氏名
職

名

田邉 裕大
氏

名

職

名

増原英彦

教授

西崎真也

教授

鹿島亮准教授五十嵐淳教授

南出靖彦教授脇田建准教授

論文審査
審 査 員

審査員
審査員

論文審査の要旨（2000 字程度）
本論文は「A Programming Language with Versions（バージョンを言語要素に持つプログラミング言語の研究）」と題し、英文で全 8 章から構成されている。
大規模なソフトウェアは複数のモジュールに分割して開発し、各モジュールの変更を版(version)によって管理することが一般的である。1 つのモジュールは多数のモジュールまたは 1 モジュール中の多数の箇所から使用され得るため、使用方法の変更が必要となるモジュールの改訂は大きな問題を起こすことが多い。本論文は、この問題は 1 つのソフトウェア中で 1 つのモジュールは 1 つの版しか存在できないプログラミング言語の設計に起因すると看破し、同時に複数の版のモジュールが使用できるプログラミング言語を設計し、理論面と実現手法の点から検討を加え、その実現性を示すことで解決を試みている。
第 1 章「Introduction」では、プログラミング言語に複数の版を持つ変数や関数を扱える機能を追加することが論文の主題であると述べ、論文の貢献がその計算体系、従来型プログラムとの相互変換手法、型推論の方法および言語処理系 VL の実現であると述べている。
第 2 章「Problem Statements」では、現在のソフトウェア開発における版管理の問題点を述べている。
まずモジュールに分割したソフトウェア開発で、1 つのモジュールの異なる版が要求される状況を説明し、既存のモジュール管理ツールでは解決できない問題があることを指摘している。このような問題はソフトウェア開発者にはよく知られているものであるが、既存のツールの能力とその限界を整理して示して研究課題として提示したことは先駆的だと言える。
第 3 章「Programming with Versions」では、プログラミング言語機能に版を導入することを提案し、プログラム例を通してどのように複数の版が扱えるのか、複数の版を混同しないためにどのような検査を行うのかを示している。これまでのプログラミング言語でも、複数の版を同時に使う機能はいく
つか提案されてきたが、モジュール単位で版を限定することや、版の混同を検査できないもの等、限定的なものだった。それに対し、提案は式単位で異なる版の使用ができ、型システムによる検査ができるような強力かつ独創的なものだと言える。
第 4 章「Lambda VL」では、前章で提案する機能を扱うための計算体系を提案している。そこでは版によって異なる定義や結果を、版に対応するラベルによって異なる値を持つレコードのような「版値(versioned value)」として表現し、ある版で作られた値は同じ版の関数によって処理されるような意味論を定義している。さらに少なくとも 1 つのラベルでは計算が成功することを検査する型システムを与えている。この計算体系と型システムはコエフェクト計算 lRPCF と GrMini を拡張したものであるが、元となっているコエフェクト計算では計算資源に関する制約を扱うことを想定していたのに対し、版というこれまでにない概念に拡張でき、その型健全性まで証明した点は独自の貢献となっている。
第 5 章「Programming with Versions on Ordinary Functional Languages」では、Haskell のような関数型言語を programming with versions によって拡張する方法を提案している。具体的にはソース言語の各モジュールを前章の計算体系の式に変換し、モジュールの版に対応するラベルを付け、型推論によって版を選択した後にソース言語へ逆変換する。論文はそのための変換規則と型推論アルゴリズムを示している。Programming with versions という概念を実際のプログラミング言語に適用するための重要な点を示し解決法を与えたことから、将来のプログラミング言語設計に良い示唆を与える貢献だと言える。
第 6 章「Implementation and Case Study」では、前章までの提案を実現した VL 言語処理系の構成手法について述べている。処理系は Haskell 言語の拡張として作成され、型推論時の制約解消に Z3 証明器を用いている。さらに事例研究として実際の行列計算ライブラリで起きた仕様変更に対して VL 言語プログラムがどのように対応できるかを検討し、programming with versions によって版管理の問題が低減できる場面を指摘している。実際的なプログラムを模した状況にまで踏み込んで提案機構の有効性を検討していることは、論文が提案する概念の有用性を量る上で重要なものだと考える。
第 7 章「Related Work」では関連研究について、特にソフトウェアプロダクトライン、版適合技術、コンテナ技術、単一リポジトリ開発などのソフトウェア開発手法との着眼点の違いと優劣を議論している。またコエフェクト計算における本論文の位置付けについても議論がある。
第 8 章「Conclusion」では本論文の提案から描けるプログラミング言語設計の展望を述べるとともに論文の総括をしている。
以上のように、本論文では今日のソフトウェア開発において大きな問題となっている版管理に対し、プログラミング言語の「値」に版を導入するという独創的な提案を行い、理論体系の構成、言語処理系の作成、有用性を示す事例の提示を行っている。これら本論文で与えられた知見は、プログラミング言語設計に対して新たな方向性を示すものであり、プログラミング言語の研究分野に新たな価値を創造したという観点からも理学上貢献すること大である。よって、本論文は博士(理学)の学位論文として十分価値があるものと認める。

注意：「論文審査の要旨及び審査員」は、東工大リサーチリポジトリ（T2R2）にてインターネット公表されますので、公表可能な範囲の内容で作成してください。