研究室メンバーによる論文・発表

本論文では単一化の履歴を記憶する型推論アルゴリズムを基礎として，型推論の経緯に基づいたエラーメッセージを生成するアルゴリズムを提案する．既存のエラーメッセージでは，プログラミング初学者・熟達者に関わらず，生じたエラーの内容や修正すべきプログラムの箇所を理解するために知識や経験あるいは時間と労力が必要となる．こうしたエラーメッセージの問題はコンパイラが扱う型とプログラマが想定する型の間の齟齬に原因があるとして，本研究ではこの齟齬を埋めることによるエラーメッセージの改善を目的とする．改善にあたり，既存のコンパイラへの自明なアドオンを実現するために型推論アルゴリズムへの大きな変更は与えない．この目的を達成するために，本研究では最初に，型別名がもたらす型のギャップを埋めるための型理論および型推論アルゴリズムを開発した．この型理論を基礎として，本論文では型が同一視された履歴をもとに型推論の経緯を説明するエラーメッセージを生成する方法を構築する．本論文の提案手法は単一化器は大きく形を変える一方で，型推論器にはわずかな変更しか要求しない．本論文では最後に，ML言語の小さなサブセットにアドオンした詳細を報告する．

本論文では，コンパイルコマンドで記述されたビルドプロセスから，部分評価によってMakefileを自動生成する方式を提案する．一般的にソフトウェアのビルドではMakeが用いられる．しかし，現実のソフトウェアプロジェクトのビルドではそのMakefileは巨大かつ複雑であり，ソフトウェアの開発・保守には多大なコストがかかる．現状のソフトウェア開発では，メタプログラミングによってMakefileの維持・発展を行っている．しかし，メタプログラミングによるMakefile自動生成手法は，ツールごとに独自言語を覚えなければならず，Makefileを直接修正することができないといった課題がある．本論文では，この問題の解決に向けて，メタプログラミングによらないMakefile自動生成手法を提案する．ビルドプロセスは，Makeの部分ビルドなどの機能を諦めれば，コマンドスクリプトとして記述できる．そして，コマンドの部分評価結果がMakefileルールと対応するはずである．これら洞察に基づき，スクリプト言語とそのインタプリタ，部分評価器を実装した．本論文では，実装したスクリプト言語の概要を示すと共に，幾つかのソフトウェアプロジェクトに適用した結果を報告する．そして，本手法の展望を述べる．

Language Server Protocol (LSP)によりエディタ上の言語サポート機能が標準化されたことで、言語ごとのサポート機能の実装はlanguage serverとして個々のエディタから分離可能となった。一方で、サポート機能の実現には、コンパイラと同等の解析機能を要するため、コンパイラと同程度に複雑な実装が必要となり、多くのコストがかかる。サポート機能を、コンパイラがコンパイルのために持っている解析器と統合して実現することができれば、その開発と保守のコストを削減することができるはずである。この達成に向けて本研究では、SML#コンパイラ自体の記述言語であるSML#によってLSPのlanguage serverを実装する。この実装は、SML#の動的型付け機構を活用しVisual Studio CodeとJSONを用いて通信することで、ある特定のプログラム例に対して色付けを行う。また、コンパイラの字句解析器を本実装からリンクすることができることを確認した。

本論文では、型付き関数型言語に計算の中断と再開を行う機能を追加する軽量な方式を提案する。計算の中断と再開は、継続やasync/awaitなどの言語機構としてすでに提案されている一方で、その実現には言語処理系の設計段階での検討を要し、既存のコンパイラに組み込むことは容易ではない。提案する方式では、継続を関数ごとに限定し、その限定継続を合成することで、関数呼び出しのネストを含む継続を構築する。これにより、既存のコンパイラへの根本的な変更を加えることなく、限定継続機能を実現する。本方式は、継続の切り取りを行う_shift式、合成を行うwait関数、および中断され得る計算を表すiter型からなり、ユーザはこれらを組み合わせて計算の中断と再開を表現する。本研究では、SML#コンパイラに提案方式を実装することで、その実現可能性を示す。また、ジェネレータや非決定的な計算を記述した例を通じて、提案方式の有用性を確認する。

AI作曲ツールが進化する一方で、人間が直接作曲することで得られる「作曲の楽しさ」や、未知の表現を生み出す創造性は、AIによる作曲には変え難い。人間にとっての音楽の楽しさや創造性をAIによる支援を含めて高めるためには、音の高さや長さなどの物理現象を直接記述する楽譜に代わる、人間の着想を直接表現し得る演奏可能な音楽記述言語が望まれる。その実現を目指し、本研究では、旋律や和音進行を簡潔かつ高水準に記述可能な音楽記述言語の設計および実装を試みる。この言語は、SML#に対するドメイン固有埋め込み言語として設計されており、和音進行の直接記述、コメントによる曲想の表現、変数を用いた楽曲の組み立てなど、作曲者が想起した抽象的な音楽の構成の記述を可能とする。さらに、SML#のMIDIライブラリを通じて記述された楽曲をMIDIファイルとして出力することができる。本論文ではこの言語の設計・実装・作曲例を詳細に報告する。

多くの有益なデータは表形式のファイルで表現されており、その取り込みと解析は様々な問題の解決を模索する上で重要な役割を果たす。関数型言語の実用性を高めるには、表形式データを自然なデータ型で取り込み、容易に操作できることが求められる。表形式データは一般に、文字列のリストのリストとして表現できるものの、そこから有益な解析結果を得るには、煩雑なデータ変換やリスト操作を要し、扱いやすいとは言えない。一方で、それ以外の型を表形式データに与えて取り込むことは型付き関数型言語では一般に難しい。本論文では、SML#の動的型付け機構を活用し、表形式データを数値を含むレコードのリストとして取り込む機構を提案する。この機構では、最初の一行をレコードのラベルとし、各行からそのラベルを持つレコード構造を構成した上で、動的型付け機構により各行にレコード型を与える。さらに、具体例を通じて提案手法とPythonによる手法を比較する。

（非公開）

ゲームのルールは説明を受けなくても直ちに理解できるほど簡単であることが望まれる一方で、そのルールをソフトウェアとして実現するためには、オブジェクト指向などの技術に基づく詳細な設計と実装を要する。このルールと実装の乖離を埋めることができれば、ゲーム開発をより簡単にできるはずである。本研究では、オブジェクト指向によらず、プレイヤー目線のルールを直接コードとして書くことでゲームを実現することを目指し、Unreal Engineのレベルブループリントのみを用いてゲームを実装する技術を探究する。本論文では、レベルブループリントのみでゲームを記述するための技法を述べたのち、テトリスを題材に、プレイヤー目線のルールを自然言語で整理したうえで、レベルブループリントのみによる実装を行った事例を報告し、ルールとの乖離を評価するとともに、従来のブループリントクラスによる実装と比較する。

本研究では、対戦型オンラインゲームにおける対戦プレーヤーの選択を、プレーヤー間での相互評価に基づいて決定する方式を提案する。オンラインゲームで迷惑行為を繰り返すプレイヤーは、ゲームの楽しさの上でも、また健全な運営・管理の上でも、様々な問題を引き起こしている。この問題に対する主要な対策の多くは、通報窓口の設置と運営判断によるアカウント削除に基づく。しかしながら、誰もが納得できる迷惑行為の認定は難しく、通報への対応にもコストがかかる。本研究では、プレーヤーの相互評価をPageRankに基づく数理モデルとして表現することで、互いに認め合ったプレーヤー間の距離を与え、距離の近いプレーヤー同士を優先的にマッチするアルゴリズムを構築する。それにより、互いに迷惑ではない行動をするプレーヤー同士の自動的な棲み分けを目指す。さらに、異なる性格のプレイヤーを想定した適用例を通じてその実用性を議論する。

本研究では、関数型言語とC言語との高度な連携のための、レコードおよびポインタの扱いに関する言語拡張を提案する。正確なガベージコレクション（GC）の下では、GCためのメタ情報を含まないデータ構造へのポインタを、それを含む構造へのポインタと混同することはできない。一方で、GCを装備した関数型言語からC言語へのシームレスで安全な連携のためには、C言語のポインタを、関数型言語においてそれらと同型のデータ構造と同様に操作できることが望ましい。本研究では、関数型言語SML#への拡張として、構造体へのポインタ型および書き換え可能なレコード型を導入し、その型付きの操作体系を設計する。SML#がすでにC互換なデータ表現を持つことにより、本拡張はSML#コンパイラへの軽微な変更で達成された。この拡張を用いて、構造体の書き換えや配列の中間へのポインタを扱うzlibをSML#から安全に呼び出せることを確認した。

ニューラルネットワークの実用のために供されるソフトウェアとして、一部のベンダーが提供する限られたライブラリが広く用いられている。そのため、人工知能技術の利用は、ベンダーへの強い依存や、技術的基礎と特定のライブラリの使用法の混同に繋がりかねない。この状況に対して、Hsuらは、高効率な畳み込みニューラルネットワークを関数型言語APLで簡潔に実装し、高度な人工知能技術の実装が一般ユーザーによってもベンダーに依存することなく可能であることを示した。この流れを受け、本研究では、APL以外の関数型言語でも同様のことが可能かどうか、ひいては関数型言語が人工知能技術の開かれた基盤として活躍する可能性を検討する。この検討を、Hsuらの提案を踏まえ、U-net CNNの一部をStandard MLで実装することを通じて行う。Standard MLとAPLでの実装を互いに比較し、その記述性や可読性について議論する。

本研究では、対戦型オンラインゲームにおける対戦プレーヤーの選択を、プレーヤー間での相互評価に基づいて決定する方式を提案する。オンラインゲームで迷惑行為を繰り返すプレイヤーは、ゲームの楽しさの上でも、また健全な運営・管理の上でも、様々な問題を引き起こしている。この問題に対する主要な対策の多くは、通報窓口の設置と運営判断によるアカウント削除に基づく。しかしながら、誰もが納得できる迷惑行為の認定は難しく、通報への対応にもコストがかかる。本研究では、プレーヤーの相互評価をPageRankに基づく数理モデルとして表現することで、互いに認め合ったプレーヤー間の距離を与え、距離の近いプレーヤー同士を優先的にマッチするアルゴリズムを構築する。それにより、互いに迷惑ではない行動をするプレーヤー同士の自動的な棲み分けを目指す。さらに、異なる性格のプレイヤーを想定した適用例を通じてその実用性を議論する。

自動車の原動機から駆動輪に至る一連の機構を自動制御するソフトウェア「パワトレアプリ」は、自動車・人・情報技術の交わりにおいて大きな要素のひとつである。このアプリの完成度は、自動車という製品の評価や「運転の楽しみ」に直結する。本研究では、自動車・人・情報技術の三者の関わりを俯瞰したのち、パワトレアプリの開発手法への改善策を提案する。小川らは、高機能が要求されるパワトレアプリのマルチコア化に向けて解決すべき問題を定式化しその解決手法を与えた。この流れを汲み、本研究では、その問題を制約条件集合として再設定し、SMTソルバによる解法を提案する。ソルバで解くことで、定式化の範囲を超えたより柔軟なアプリ開発が可能になると期待できる。本論文では、問題自体がSMTソルバで解けることを述べるとともに、コアへの自動割り付けなどの未解決の問題についても記述・求解できる可能性があることを議論する。

本研究では、「味わい」や「香り」のような、個人の体験の中だけにあり、表現として取り出し得ない対象を、表現のみを扱う情報技術によって探求するための方法を模索する。食物を味わった時に人が感じる味わいは、その人だけのものであり、「甘い」「辛い」などの過度な一般化や抽象化をしなければ、それそのものを表現として取り出すことは難しい。一方で、その繊細な味わいを再現したり、他者と共有したりするためには、材料や調理法の特定など、その味わいを表現する何らかの手段を見つけなければならない。本研究では、ChatGPTへの質問として自ら感受した体験を表現すること、およびChatGPTの回答からその表現の可能性を質問者自身が発見することを通じて、質問者だけが答えを知っている味わいに情報技術で迫ることを試みる。その結果を報告するとともに、味わいの表現をChatGPT から抽出するための、プロンプトの入力方法や表現方法を提案する。

本研究では、競馬における過去のレース結果と競走馬の将来の活躍の関連を情報理論的観点から分析することを試みる。競馬のオッズには、各競走馬に対する馬券購入者の期待が反映されている。その期待は各馬の過去の実績に基づくと思われる。このような、過去に基づく将来への期待は、競馬に限らず一般に、例えば就職などにおいても、見込まれる場面が少なくない。しかしながら、過去の実績と将来の活躍の間にどの程度の関連があるかは、必ずしも明らかではない。本研究では、このことを情報理論的な視点から分析する。情報理論を用いることで、過去の実績を知ることが次のレース結果への驚きに与える影響を、過去と今回のレース結果の間の相互情報量として定量化できる。この方針に基づき、本研究では、競馬のレース結果から、オッズと結果の関連など、いくつかの要素を抽出し、それらの相互情報量を求めることで、競馬における実績と活躍の関連を導く。

近年の音楽ライブでは、チケットの高額転売の横行が問題視されている。この問題に対して、音楽関係者、記者、学者などが業界の事情とともにそれぞれ独自の見解や解決策を語っている。その一方で、この問題に対する統一的な合意や対応はいまだ得られていない。この根本的な原因のひとつは、経済や商業よりもむしろ、転売のための買い占めを誰にでも可能にした「bot」と呼ばれるソフトウェアにあり、従ってこの問題を本質的に議論するにはbotに関する知識が不可欠である、と思われる。しかしながら、アンダーグラウンドビジネスであるbotに関する情報は、攻撃側と対策側の両面において、大部分が秘匿されている。本研究では、例えば銃社会の危険性を議論するには銃の模型があれば十分であるように、転売問題の建設的な議論に向けたbotの模型を含む技術説明基盤の構築を目指す。その一歩として、フォームへの自動入力やアクセス元の秘匿を備えたbotの模型を提案する。

Unityでは、ゲームをオブジェクトの集まりとして制作する。個々のオブジェクトは機能の単位であるコンポーネントの複合体として表される。このモデルに基づく汎用のプログラミング言語が実現できるならば、新たなオブジェクト指向プログラミングに繋がる可能性がある。本研究では、以上の考えのもとで、Unityからゲームオブジェクト／コンポーネントモデルの抽出を行い、Standard MLを拡張した言語である SML#のレコード型の結合と動的型付け機構を用いて、そのモデルに基づく汎用のプログラミング機構を設計し実装した。また、この機構を用いて、簡単なプログラミングを試み、コンポーネントを用いたオブジェクトの生成と管理が可能なことを確認した。本稿では以上の試みを報告するとともに、その過程で得られた SML#の動的型付けに関する改良を提案する。

オートマトンや数理論理学といった知能情報システムプログラムで学ぶ様々な項目は、コンピュータだけでなく、それ以外のものにも適用できる。本研究では、その一例として、鉄道玩具「プラレール」に計算機科学の知見を応用し、新たな遊びの可能性を探究する。プラレールには「ターンアウトレール」と呼ばれる、自由に動くレバーを一つ持つ分岐レールが存在し、これは 1 ビットの記憶素子とみなせる。従ってプラレールの線路全体は複数ビットの状態を自律的に変化させる計算機とみなせる。本稿では、プラレールを、複数ビットの状態と列車の位置を計算する関数として形式化する。その形式化を使用し、「$n$ 個のターンアウトレールを用いたとき、列車が自律的にすべてのルートを通るようなレールのつなぎ方はあるか」という仮説を立て、SML#プログラムによって、この仮説の真偽を検証した。その結果、$n=2$では成立するが、$n=4$では成立しないことが判明した。

Functional Reactive Programming（FRP）は、外界からの入力に反応するアニメーションの宣言的なプログラミングを可能とする手法である。この手法に基づくプログラミングを行うためには、専用の言語やライブラリが必要である。しかし、その実装には高度な抽象化を施した時間の概念が要求され、緻密な設計や複雑なコーディングが避けられない。本研究では時間を捨象せず、しかしFRP と同等の記述力を持つプログラミング手法と、その実現方式を提案する。提案手法では、時間をある瞬間の世界の切り取りとして定義する。SML#のグラフィックスライブラリにこの定義に基づく型や関数を加え、提案手法によるグラフィックスプログラミングを可能とした。ライブラリの改良は、SML#の組み込み型だけを用いて、十数行程度の変更で完了し、従来の実装方法よりも軽量であることが示された。

Web アプリは、クライアント側のプログラムとサーバ側のプログラムからできている。クライアント側のプログラムには、Web アプリの作成者が管理していないサーバにある複数のファイルが含まれる。Web ブラウザはそれらのファイルをサーバから取得して結合することでプログラムを得る。サーバのファイルが変更される可能性があるため、作成者が作ったプログラムそのものを、使用者も得ているとは限らない。これを Web アプリの完全性の問題という。本稿では、この問題に対して、Web アプリ本体のプログラムを実行する前にプログラムの働きをテストすることで、問題の発生をアプリ実行前に検出することを提案する。簡単な Web アプリに対して、プログラムの内容からテストの対象と方法を抽出し、テストプログラムを作成し、アプリ本体の実行前にテストが行われるようにアプリを変更した。この試みを通じて、テストによる完全性の問題の検出における様々な課題を特定した。

プログラムのデバッグをする際に、計算機内で行われている計算が一目でわかる形式で表現できるとプログラムの問題点がわかりやすい。本研究の一般的な目的は、プログラムの動きをプログラマが見たいタイミングで切り取り表示することである。その第一歩として本稿では、表示に供するデータを得るために、計算の順序や関数の入出力を自動的に記録する機構を構築する。この機構では、計算過程を記録するデバッグコードを、コンパイラが自動的に挿入することによって系統的にプログラムの動きを表すデータを取得する。この方針のもとでSML#コンパイラに変更を加え、さらに、このコンパイラを用いてゲームプログラムのデータを収集した。データ収集のオーバーヘッドが小さいことを確認し、各関数が呼び出される順序と引数と返り値に関する詳細なデータを得た。本稿では以上の試みの詳細を報告するとともに、それに基づくデバッグのための可視化に関する展望を議論する。

英語文法が確立しているのに対して、日本語の文法には共通の認識が得られていない。もし日本語の文法に関する確立した理解があるならば、その理解に基づき日本語の取り扱いを手続き化できるはずである。逆に言えば、日本語を扱う手続きを構成できればその手続きは日本語の理解の一端を示しているはずである。本研究では、三上章の提唱した「無題化」という操作に着目し、この操作を行うプログラムを構築する。このプログラムは日本語の文を成す文節のリストを入力すると、無題化の結果の可能性を列挙する。このプログラムは、まず文節のリストから提題の助詞「は」を持つ文節を探す。次に、「は」を「が」や「を」や「に」などに置き換えた文の候補を生成する。最後に、同格の補語の重複がある文を取り除き、文末に「koto」を付け加え、結果の候補を得る。このプログラムの出力は日本語として意味を持たないものも含まれる。この結果に基づき、より深い日本語の理解への展望を議論する。

オンラインゲームで横行している「チート」と呼ばれる不正行為は、誠実なプレイヤーに損害を与えゲームの成立を脅かす悪質な行為でありその対策が求められている。本稿では、オンライン一人称視点シューティングゲームにおけるチート行為のうち、クライアント側のプログラムの改竄によるものを対象とし、チート耐性を高めるためのプログラムの構造上の工夫を提案する。提案手法では、クライアント側のプログラムは複数の機能が互いに出力する値の組を計算しサーバーに送信する。これによって、チートの実現のために改竄すべき箇所を増やし、かつサーバーサイドで改竄を検出する可能性を高める。オンラインゲームを模したプログラムを作成し、提案手法を適用した結果、エイムボットと呼ばれるチート行為に対して、改竄箇所の増加と中途半端な改竄の検出に成功した。さらに、提案手法の現実のゲームへの適用に向けた展望を述べる。

楽曲の演奏は、演奏者による音符列の解釈に基づいて成立する。演奏者による解釈は、和声法と呼ばれる定石が知られているものの、多くは演奏者の感性に委ねられる。一方、もし楽曲の解釈を手続き化できるならば、その手続きは、楽曲理解の一助や未知なる解釈の可能性を示唆する、新たな音楽の意味づけの枠組みとなり得る。本研究では、その一歩として、和声法における和音の機能の分類とその繋がりに着目し、与えられた和音列に対して機能分類に基づく解釈の可能性を列挙する手続きを与える。この手続きでは、各和音が持ち得る意味の可能性を論理式で、また隣り合う和音の間で満たされるべき性質を形式的規則として表現する。和音列の意味は、規則と論理式を共に充足する解として与えられる。充足の判定は論理式の構造に基づく総当たりによって行う。本稿では、以上の手続きを示すと共に、計算に基づく楽曲の理解に向けた展望を述べる。