hpprc/llmjp-kaken huggingface dataset:
Ｊ．Ｓ．バッハのヴァイマール時代におけるフーガ書法の発展――転回技術を着眼点に

本研究は、J. S.バッハの楽曲にみられる転回の用いられ方の変遷を実証的に跡付けるものである。バッハはヴァイマール時代に、浩瀚な蔵書を誇ったJ. G.ヴァルターと懇意な間柄にあった。本研究では、バッハがヴァルターを通して様々な転回に触れたとの仮説を立て、ヴァイマール時代を主要な対象に、1、バッハの楽曲の分析、2、バッハやヴァルターが筆写した他者楽曲の分析、3、ヴァルターが所持していた理論的手稿の読解を行う。昨年度は、サンプルとなる楽曲を抽出し、そのモデル化を行い、楽曲を分類することで、変遷の過程を示すための土台を築いた。多くの楽曲を対象に試験的分析を行う中で三点の課題が浮かび上がったため、本年度はそれらの解決に注力した。以下は昨年度の実績報告書の「今後の研究の推進方策」と対応する。1、転回可能であるか否か、その判断の拠り所とされたであろう「基準」を明らかにすべく、バッハの不協和音の扱い方の時期ごとの特徴を確認した。2、転回の用いられ方の変遷の過程をよりつまびらかにすべく、本研究が主要な対象とするヴァイマール時代の前後に由来するバッハの楽曲をも検討した。他者楽曲については、バッハやヴァルターが筆写したものに限らず、目にした可能性の高いものをも視野に入れた。更に、ヴァルターが所持していた理論的手稿と関連の深い、転回を扱った同時代の理論的手稿の読解にも着手した。3、楽曲分析の精度を高めるべく、関連文献のとる手法を参考に、計九つの着眼点を定めた。二年間に亘る本研究の成果をもとに提出される博士論文では、十把一絡げに捉えられて来たきらいがある「転回」という一観点からみた、バッハの作曲技法の発展の道筋を描き出す。先行する様式研究において導かれる傾向と照合しながら総合的な記述を目指すことで、バッハの成熟へ向けた歩みの様相について、より多面的な理解がもたらされよう。28年度が最終年度であるため、記入しない。本研究の目的は以下の二点である。一、J. S.バッハの個々の楽曲の様式研究に転回(声部交換)技術という一観点を加えること。即ちその楽曲に対し資料的、様式的見地からなされて来たあらゆる研究を踏まえた上で、とりわけ器楽曲の成立を巡る議論に新たな光を投じること。二、バッハのヴァイマル時代を中心とした約二十年に亘る様式発展過程の一側面に、転回技術を主要着眼点として迫ること。その際、ヴァイマルでバッハと懇意な間柄にあり浩瀚な蔵書を誇ったJ. G.ヴァルターによる知識伝達の可能性に着目し、バッハのヴァイマル時代を、自身の演奏実践に根差した書法に厳格な対位法技術を織り込んでいった過程として捉え直すこと。本年度の成果は以下の通りである。一、ヴァルターが筆写した手稿から転回技術を扱った部分を検討し、音程への配慮が最低限にとどめられた「簡潔にして明快な」規則と、反行や逆行、拡大の可能性をも考慮に入れた「技巧的な」規則とが理論上区別されていたことを確認した。更にバッハやヴァルターが筆写あるいは所持していたと考えられる他者楽曲を分析し、実践においても見出されたこうした指向の差異について、即興演奏や、自らの学術性を知らしめることを目的とした出版などの創作背景を踏まえて考察した。二、主題と対主題の転回可能性、不都合な響きが生じた際の修正の施され方といった観点からバッハの楽曲を分析し、そこに用いられた転回技術の厳格さが一様でないことを確認した。そして、上述の観点を中心に厳格さの度合いを示すファクターを設定し、楽曲を分類し、バッハの対位法書法の変遷が、大まかに言えば厳格さの度合いの低いものから高いものへと移行するいくつかのモデルによって解釈可能であることを示した。また、最も厳格さの度合いの高い楽曲においても、鳴り響きの多彩さを決して犠牲にすることのないような工夫がなされていることを確認した。転回技術の厳格さという観点から、サンプルとなる楽曲の抽出、そのモデル化およびモデルごとの楽曲の分布図作成に着手し、バッハの対位法書法の変遷を描き出すための土台を築くことが出来た。

2、転回の用いられ方の変遷の過程をよりつまびらかにすべく、本研究が主要な対象とするヴァイマール時代の前後に由来するバッハの楽曲をも検討した。他者楽曲については、バッハやヴァルターが筆写したものに限らず、目にした可能性の高いものをも視野に入れた。更に、ヴァルターが所持していた理論的手稿と関連の深い、転回を扱った同時代の理論的手稿の読解にも着手した。3、楽曲分析の精度を高めるべく、関連文献のとる手法を参考に、計九つの着眼点を定めた。二年間に亘る本研究の成果をもとに提出される博士論文では、十把一絡げに捉えられて来たきらいがある「転回」という一観点からみた、バッハの作曲技法の発展の道筋を描き出す。先行する様式研究において導かれる傾向と照合しながら総合的な記述を目指すことで、バッハの成熟へ向けた歩みの様相について、より多面的な理解がもたらされよう。来年度取り組むべき主な課題は、以下の三点である。一、主題と対主題が転回可能であるか否か、その判断の拠り所とされたであろう「基準」を明らかにすること。二、更に多くの楽曲を対象に分析を行い、モデルごとの楽曲の分布図を充実させること。三、転回技術の厳格さの度合いを示すファクターをより洗練させること。28年度が最終年度であるため、記入しない。
機能複合型の新しい光・電子用有機-無機複合系の開拓

今年度に購入した恒温乾燥機を用いて、水溶性のテトラ(4-カルボキシフェニル)ボルフィンナトリウム塩(TPPC)およびメゾポルフィリンナトリウム塩をアルミナゲルに分散した試料の作成をゾルゲル法により行った。ゾルゲル法による透明アルミナバルク体の作成は、アルコキシド法および無機塩法が報告されている。本研究では、両法を試み、出発溶液のpHや希釈率、乾燥制御剤の添加量などを変化させ、ポルフィリンが化学変化しない範囲でなるべく緻密な乾燥ゲル体を得る条件を検討した。最終的には、アルコキシド法で乾燥制御剤としてジメチルホルムアミドを添加した系で良好な試料を得た。いずれの色素を用いた試料でも、試料を20Kに冷却してPHBを行ったところ、高効率でホールを形成し、色素が均一に分散していることが確認された。次に、温度サイクル実験を行い、ホールの熱安定性を調べたところ、低温に再冷却した際のホールの埋まり混み易さおよびホール幅の広がり易さは、ポリマー系の中で最も良い部類の試料と同程度であった。一方、高温で観測されたホール面積は、ポリマー系よりも大きく、特にTPPC系はデバイ・ワーラー因子の温度依存性が極めて小さい系であることがわかった。128KでTPPC系にレーザーを照射し、差スペクトルを測定したところ、ホールが形成されていることが確認できた。これは、水素化ポルフィリンを用いた系の中では最高温度である。以上のように、色素アルミナ複合系でPHBを行い、良好な特性が得られることを確認したが、現在、新たにジルコニアなどを用いた系の作成を試み、機能複合化の可能性を探っている段階である。
慢性的な鉄欠乏状態がビタミン類代謝産物の体内動態と加齢性疾患に及ぼす影響

これまでの研究結果から、幼若期(被験動物)における鉄欠乏状態は1骨脆弱化を招くこと、2諸臓器においてタンパク質の酸化を亢進させ、3各種ミネラル分布も変動させるといった結果を得ている。しかしながら、『鉄欠乏状態が何故、骨脆弱化とビタミン類代謝関連酵素を変動させるのか?』については明らかにされていない。そこで本研究では、慢性的な鉄欠乏状態がビタミン類代謝産物の体内動態と加齢性疾患に及ぼす影響についてin vivoおよびin vitroの両面から検討を行った。In vivoの結果から、慢性的な鉄欠乏状態は(1)肝臓・血漿中α-トコフェロールが通常食群に対して増加すること、(2)脂質過酸化が亢進することを明らかにした。In vitroの結果から、肝臓油彩細胞であるFAO細胞を用いた鉄枯渇条件下において、抗加齢タンパク質でもありビタミンC律速酵素であるSMP30の発現が有意に低下することを明らかにした。以上のことより、慢性的な鉄欠乏状態はビタミン類の体内動態を変動させることで細胞老化を引き起こしていることが示唆された。本研究では、若年層が今後超高齢化に拍車をかける我が国において、幼若期および青年期における過度なダイエットや偏食による「鉄摂取不足がビタミンDの体内動態を変化させることで加齢性疾患の発症状態を増悪する可能性」という次世代につながる未だ不透明なポイントを明らかにすることを目的とし研究を遂行した。実験動物を用いた解析から、通常食と比較して、鉄欠乏食摂取により骨脆弱化は認められたものの、ビタミンD水酸化酵素(CYP27b1)の活性に影響は認められなかった。加えて、肝臓細胞株FAO細胞に鉄キレート剤を用いた鉄枯渇モデルを作成し、CYP27b1の発現を解析した結果、in vivoと同様に無処理群と比較しても影響が認められなかった。そこで研究計画(申請書)とは異なるが、ラット肝臓および腎臓と鉄キレート剤処理を行ったFAO細胞を用いてDNAマイクロアレイ解析を行った。その結果、ビタミンD代謝関連酵素群は鉄欠乏時に遺伝子レベルでは減少していることを明らかにした。加えて、骨強度に関するコラーゲンの合成に関与するビタミンCの律速酵素であるSMP30が候補として挙がった。そこでSMP30と鉄欠乏について詳細な検討を行った。その結果、鉄キレート剤処理時にSMP30は無処理群に対し、遺伝子およびタンパク質レベルで有意に減少するのみならず、活性酸素種の産生および細胞老化が亢進することを明らかにした。また、鉄キレート剤処理に対し、SMP30の過剰発現を行うことで活性酸素種および細胞老化の亢進が有意に抑制された。以上のことより、鉄欠乏時においてビタミンD関連酵素の発現低下のみならず、ビタミンC律速酵素であるSMP30の発現を負に制御することで細胞老化を亢進することを明らかにした。鉄欠乏時におけるビタミンD代謝関連物質に関しては検討が進んではいないが、DNAマイクロアレイの結果から、新たにビタミンCとの関連を見出すことができた。現在、ビタミンD関連代謝産物を測定できるようLC/MSの設定およびルシフェラーゼ活性の測定系を立ち上げている。一方で、DNAマイクロアレイで新たに見出すことができた鉄欠乏とSMP30に関しては、現在、投稿論文として執筆準備中である。本研究では、現代食生活において若年層の過度なダイエットによる摂取不足が懸念されている鉄に着目した。鉄は必須微量元素であり、反応性に富む金属元素であることから生体内恒常性の維持に必要不可欠な栄養素である。これまでに、鉄過剰についてはフェントン反応を介したフリーラジカル産生を増大させることで様々な疾患の発症に関与する報告がある。一方、鉄欠乏に関しては、鉄欠乏性貧血や月経、運動選手に多く見られるスポーツ心臓といった生理現象が報告されている。加えて、カルシウムやマグネシウムといったミネラルのみならず、若年期における鉄摂取不足は、骨密度の低下を招くことが報告されており、超高齢社会を迎えた現代において無視できない問題である。しかしながら、鉄欠乏状態とこれら疾患との関係をつなぐ分子栄養学的な知見はあまりない。そこで本年度は、培養細胞と動物試験を行うことで、鉄欠乏時のビタミン類との関連を明らかにすることとした。まずはじめに、鉄キレート剤であるDFOをFAO細胞に処理することで、抗加齢タンパク質であるSMP30が減少することを定量的PCRおよびwestern blot法にて明らかにした。加えて、DFO処理濃度依存的に活性酸素種(ROS)が増大すること、細胞老化マーカーであるβ-Galactosidase活性が上昇することを明らかにした。これはSMP30過剰発現株で抑制されることを合わせて明らかにした。培養細胞において、SMP30はビタミンC合成酵素群としても知られていることからも、鉄欠乏状態はビタミンC合成能を低下させることが示唆された。動物試験を用いた結果、鉄欠乏食投与を行うことで、ビタミンD水酸化酵素であるCYP27b1の発現が膜画分において減少することを見出した。一方でビタミンE関連酵素については変動が見られなかった。今後、ビタミンDおよびE関連タンパク質群を網羅的に解析していく。本申請課題では、鉄欠乏状態における脂溶性ビタミン類の変動を明らかにしていくことを目的としている。しかしながら、鉄欠乏時における脂溶性ビタミン類関連タンパク質群の変動が安定せず、実験条件の検討を行っている。一方で、マイクロアレイを用いた実験から、抗加齢およびビタミンC合成酵素群として知られているSMP30が鉄欠乏時において減少することを明らかにし、報告している。

今後はLC-MSなどの質量分析装置を用いて、鉄欠乏時の組織中脂溶性ビタミン類を測定することで関連性を明らかにしていく予定である。以上のことから、やや遅れているとの判断を致しました。これまでの研究結果から、幼若期(被験動物)における鉄欠乏状態は1骨脆弱化を招くこと、2諸臓器においてタンパク質の酸化を亢進させ、3各種ミネラル分布も変動させるといった結果を得ている。しかしながら、『鉄欠乏状態が何故、骨脆弱化とビタミン類代謝関連酵素を変動させるのか?』については明らかにされていない。そこで本研究では、慢性的な鉄欠乏状態がビタミン類代謝産物の体内動態と加齢性疾患に及ぼす影響についてin vivoおよびin vitroの両面から検討を行った。In vivoの結果から、慢性的な鉄欠乏状態は(1)肝臓・血漿中α-トコフェロールが通常食群に対して増加すること、(2)脂質過酸化が亢進することを明らかにした。In vitroの結果から、肝臓油彩細胞であるFAO細胞を用いた鉄枯渇条件下において、抗加齢タンパク質でもありビタミンC律速酵素であるSMP30の発現が有意に低下することを明らかにした。以上のことより、慢性的な鉄欠乏状態はビタミン類の体内動態を変動させることで細胞老化を引き起こしていることが示唆された。本年度は、前年度の結果をもとに本研究では、FAO細胞(ラット肝臓)、L2細胞(ラット腎臓)、HepG2細胞(ヒト肝臓)、HK2(ヒト腎臓)を用い、老化を伴う鉄欠乏状態がビタミンDおよびC代謝に及ぼす機序を明らかにすることを目的とする。具体的には、鉄欠乏モデルには鉄キレート剤(DFO)処理を行い、細胞からはビタミンDおよびC代謝関連酵素であるCYP27b1, SMP30を、炎症に関わる細胞内シグナル伝達機構(JNK1/2-AP-1シグナル)と生体防御機構(Nrf2を介したシグナル)およびの3大シグナル伝達経路をreal time PCR法による遺伝子発現、western blotting法によるタンパク質発現・翻訳後修飾の観点から明らかにする。前年度の結果をもとに本年度では、FAO細胞(ラット肝臓)に加え、L2細胞(ラット腎臓)、HepG2細胞(ヒト肝臓)、HK2(ヒト腎臓)を用い、老化を伴う鉄欠乏状態がビタミンDおよびE代謝に及ぼす機序を明らかにすることを目的とする。具体的には、鉄欠乏モデルには鉄キレート剤(DFO)処理を行い、その後、ビタミンDおよびE代謝関連酵素であるCYP27b1, CYP3a1含むチトクロームファミリー、炎症に関わる細胞内シグナル伝達機構(JNK1/2-AP-1シグナル)と生体防御機構(Nrf2を介したシグナル)およびの3大シグナル伝達経路をreal time PCR法による遺伝子発現、western blotting法によるタンパク質発現・翻訳後修飾の観点から明らかにする。また、前年度の動物組織試料があることからも、LC-MSを用いた脂溶性ビタミン類の検出を並行して行う予定である。以上のことから、本年度は、まず細胞レベルでの検討を行い、動物試験へと移行していく予定である。
多様体内の準正曲面と接触構造に関する研究と複素特異点論への応用

複素2次元ベクトル空間内で、原点からの距離が1である点の集合は3次元球面となる。この3次元球面S上の点xにおける接平面Hを複素構造Jを使って回転させたものをJHとすると、HとJHの共通部分はSの接平面内の2次元平面となる。点xをS上で動かして得られるこのような平面の集まり(つまり平面場)を3次元球面の標準的接触構造という。本研究では、複素多項式とその複素共役多項式の積で与えられる多項式写像の孤立特異点のミルナー束について、それと両立する接触構造が標準的接触構造でないことを示した。複素多項式のミルナー束は常に標準的接触構造と両立することから、複素共役が混ざることでミルナー束の接触構造が変化することが観察できる。3次元多様体のオープンブック分解と両立する接触構造のtight性の研究は,その構造が4次元多様体の複素構造から定まるものかを特徴づける重要な概念であり,特に複素特異点論におけるミルナー束と基本的なレベルで密接に関連している。今年度は3次元ホモロジー球面内のファイバー性をもつグラフリンクについて,それと両立する接触構造の研究の行い,3次元球面内のファイバー性をもつグラフリンクで,各ザイフェルトピースが正の方向に捻られているものに対し,そのグラフリンクと両立する接触構造がtightであることと,グラフリンクの各成分の向きがすべて同じ向きであることが必要十分であることを示した.またその系として,f\bar g型の特異点のミルナー束と両立する接触構造は常にovertwistedであるこ、とを示した.また,埼玉大の下川航也氏およびカリフォルニア州立大学チコ校のThomas Mattman氏との共同研究として,結び目補空間の基本群のSL(2,C)表現から定まるA多項式と呼ばれる結び目不変量について,その多項式がいつ他の結び目のA多項式を因子に含むような因数分解をもつか、という問題についての研究を進め,ある特別な図式をもつ結び目について,そのような因数分解が存在するという結果が得られた.3次元多様体のオープンブック分解と両立する接触構造のtight性の研究は,その構造が4次元多様体の複素構造から定まるものかを特徴づける重要な概念であり,特に複素特異点論におけるミルナー束と基本的なレベルで密接に関連している.今年度は、この枠組みの高次元化が可能かどうかについて考察した。東京理科大学の岡睦雄氏によりstrong lypolar weightedhomogeneousなmixed多項式について、ある良い条件が満たされると、そのミルナー束が標準的な接触構造と両立することが示された。この例は一般次元のもので、準正曲面を考える上で参考になった。この話を踏まえて、標準的接触構造と両立するオープンブック分解に対し、そのsuspensionにより得られるオープンブック分解も標準的接触構造と両立することが分かりつつある.また,埼玉大の下川航也氏およびカリフォルニア州立大学チコ校のThomas Mattman氏との共同研究として,結び目補空間の基本群のSL(2,C)表現から定まるA多項式と呼ばれる結び目不変量について,結び目がある特殊なタングル分解をもつと、そのA多項式はその1つのタングルから得られる結び目のA多項式を因子として含むことを示すことができた.これはA多項式という計算の難しい対象の特徴を図式から導きだすもので、極めて珍しい結果といえる.3次元多様体のオープンブック分解と両立する接触構造のtight性の研究は,その構造が4次元多様体の複素構造から定まるものかを特徴づける重要な概念であり,特に複素特異点論におけるミルナー束と基本的なレベルで密接に関連している.前年度に引き続き,この枠組みの高次元化が可能かどうかについて考察し、標準的接触構造と両立するオープンブック分解に対し、そのsuspensionにより得られるオープンブック分解も標準的接触構造と両立することついて、その証明の大筋を掴むことができた.具体的には,Kauffmanによる位相的suspensionをアイデアを用いて,標準的接触構造と両立する2n+1次元球面内のオープンブック分解をファイバーリンクの2n+3次元球面内の近傍で少しずらし,2n+1次元球面を分岐とする分岐被覆により2n+3球面のk重分岐被覆として2n+3次元球面内の標準的接触構造を実現する.

最後に分岐被覆はReebベクトル場とファイバー曲面の横断性を保つことを確認して,主張は証明される.また,埼玉大の下川航也氏およびカリフォルニア州立大学チコ校のThomas Mattman氏との共同研究として,前年度に結び目補空間の基本群のSL(2,C)表現から定まるA多項式と呼ばれる結び目不変量について,結び目がある特殊なタングル分解をもつと,そのA多項式はその1つのタングルから得られる結び目のA多項式を因子として含むことを示したが,これらの結び目に対してのCuller-Shalen理論の帰結として得られるcyclic surgeryの非存在の関係について厳密な考察を与えた.研究の目的で述べた、準正曲面を多様体のオープンブック分解、接触構造、結び目理論、ミルナー束についての研究においては、f\bar g型の特異点のミルナー束の接触構造が決定できたので、一段落ついたといえる.また、高次元化についてもsuspensionによる考察が進みつつあるので、順調に進んでいるといえる.24年度が最終年度であるため、記入しない。24年度が最終年度であるため、記入しない。
アンジオポエチン2阻害によるぶどう膜炎軽症化の検討

抗ANG2抗体を用いた眼炎症抑制効果を検討するにあたり、まず眼炎症の抑制に寄与し得る抗体の至適投与量について検討した。この検討には、エンドトキシン誘導ぶどう膜炎(EIU)マウスを用いた。6週齢のC57BL/6マウスを用い、抗ANG2抗体を用いた治療群では10mg/kgまで投与量を変化させ、眼炎症抑制効果の変化を検討した。抗体の腹腔内投与から24時間後にリポポリサッカライド(LPS)を腹腔内注射し、EIUを誘導した。さらに24時間後に過剰量の麻酔薬投与下で、左心室よりコンカナバリンAで灌流し、眼球を摘出し、網膜フラットマウントを作製した。網膜白血接着数を検討したところ、治療群(抗ANG2抗体投与量:10mg/kg)において非治療群と比べて有意に減少した。この結果から、眼炎症抑制に要する抗ANG2抗体の至適投与量を10mg/kgと推定できた。この投与量を目安として自己免疫性ぶどう膜網膜炎に対する眼炎症の抑制効果を検討することとした。この検討には実験的自己免疫性ぶどう膜網膜炎(EAU)マウスを用いた。C57BL/6マウスにヒト視細胞間レチノイド結合蛋白(IRBP)由来合成ペプチドと結核菌強化完全フロインドアジュバントエマルジョンで皮下免疫し、追加免疫として百日咳菌毒素を0.1μg腹腔内投与してEAUを惹起した。EAUマウスの眼所見を経時的に確認し、重症度が最も高くなる21日目にマウスを安楽死させ、眼球を摘出して眼病理組織標本を作製した。今後これを用いてマウスEAU網膜におけるAng1、およびAng2の局在を免疫組織化学的に検討する。これまでの研究で、眼炎症抑制に寄与しうる抗ANG2抗体の投与量を検証できたが、投与間隔や期間についてはさらなる検討が必要である。EAUマウスモデルでの炎症抑制効果の検討に加え、網膜組織の免疫染色などによるさらなる解析を行っていく。EAUマウスモデルの作成については順調に行っているが、中和抗体を用いた炎症抑制効果の検討についてはやや遅れがある。抗ANG2抗体を用いた治療群では10mg/kgまで投与量を変化させ、眼炎症抑制効果の変化を検討した。現在、抗体の提供先から抗体が十分に得られていないため、出来うる範囲での見当を行っている。眼炎症抑制に要する抗ANG2抗体の至適投与量を推定できたが、最適な投与間隔や投与期間についての検討も必要である。抗体量が十分量確保出来次第、EAUマウスモデルでの炎症抑制効果の検討、網膜組織の免疫染色などを行い、さらなる解析を行っていく。基本的な抗体の至適投与量についての見当がついた。実験的自己免疫性ぶどう膜炎の動物モデルの作製に関する手技は確立しており、免疫組織化学的な変化を検討するための病理組織標本はすでに作製している。抗体量が十分量確保出来次第、EAUマウスに関する眼炎症抑制効果について最適な投与間隔や投与期間についての検討も進めていく予定である。具体的にはEAUの臨床的重症度と病理組織学的重症度の検討を行う。また、抗体投与により重症度の軽症化が確認された場合、その分子メカニズムについての解析を行う。抗Ang2中和抗体による抗炎症作用の分子機構を検索するため、摘出眼球を抗NF-κB抗体で免疫染色を行う。NF-κB p65の核内への移行を検討し、ぶどう膜炎による網膜ぶどう膜の障害とNF-κBの関与について評価する。さらにIκB-αの発現変化についてもwestern blottingを用いて評価する。今後はこの投与量を目安としてEAUに対する眼炎症の抑制効果を検討する。また上記の実験とともに、実験的自己免疫性ぶどう膜網膜炎(EAU)マウスを作製し、眼病理組織標本を作製した。C57BL/6マウスにヒト視細胞間レチノイド結合蛋白(IRBP)由来合成ペプチドと結核菌強化

完全フロインドアジュバントエマルジョンで皮下免疫し、追加免疫として百日咳菌毒素を0.1μg腹腔内投与してEAUを惹起した。重症度が最も高くなる21日目にマウスを安楽死させ、眼球を摘出して眼病理組織標本を作製した。今後これを用いてマウスEAU網膜におけるAng1、およびAng2の局在を免疫組織化学的に検討する。これまでの研究で、眼炎症抑制に寄与しうる抗ANG2抗体の投与量を検証できた。これらの結果に基づき、EAUマウスモデルでの治療効果の検討、網膜組織の免疫染色などを行い、さらなる解析を行っていく。EAUマウスモデルの作成については順調に行っている。中和抗体を用いた炎症抑制効果の検討についてはやや遅れがある。現在、抗体の提供先から抗体が十分に得られていないため、出来うる範囲での見当を行っている。抗体量が十分量確保出来次第、EAUマウスに関する眼炎症抑制効果について見当をさらに進めていく予定である。抗ANG2抗体を用いた眼炎症抑制効果を検討するにあたり、まず眼炎症の抑制に寄与し得る抗体の至適投与量について検討した。この検討には、エンドトキシン誘導ぶどう膜炎(EIU)マウスを用いた。6週齢のC57BL/6マウスを用い、抗ANG2抗体を用いた治療群では10mg/kgまで投与量を変化させ、眼炎症抑制効果の変化を検討した。抗体の腹腔内投与から24時間後にリポポリサッカライド(LPS)を腹腔内注射し、EIUを誘導した。さらに24時間後に過剰量の麻酔薬投与下で、左心室よりコンカナバリンAで灌流し、眼球を摘出し、網膜フラットマウントを作製した。網膜白血接着数を検討したところ、治療群(抗ANG2抗体投与量:10mg/kg)において非治療群と比べて有意に減少した。この結果から、眼炎症抑制に要する抗ANG2抗体の至適投与量を10mg/kgと推定できた。この投与量を目安として自己免疫性ぶどう膜網膜炎に対する眼炎症の抑制効果を検討することとした。この検討には実験的自己免疫性ぶどう膜網膜炎(EAU)マウスを用いた。C57BL/6マウスにヒト視細胞間レチノイド結合蛋白(IRBP)由来合成ペプチドと結核菌強化完全フロインドアジュバントエマルジョンで皮下免疫し、追加免疫として百日咳菌毒素を0.1μg腹腔内投与してEAUを惹起した。EAUマウスの眼所見を経時的に確認し、重症度が最も高くなる21日目にマウスを安楽死させ、眼球を摘出して眼病理組織標本を作製した。これまでの研究で、眼炎症抑制に寄与しうる抗ANG2抗体の投与量を検証できたが、投与間隔や期間についてはさらなる検討が必要である。EAUマウスモデルでの炎症抑制効果の検討に加え、網膜組織の免疫染色などによるさらなる解析を行っていく。EAUマウスモデルの作成については順調に行っているが、中和抗体を用いた炎症抑制効果の検討についてはやや遅れがある。抗ANG2抗体を用いた治療群では10mg/kgまで投与量を変化させ、眼炎症抑制効果の変化を検討した。
フィプロネクチンタイプIII様ドメインの機能開発

本研究は、原核生物に見いだされたタイプIII様ドメインの構造と機能を解明することを目的として行ったものである。その目的を達成するために、(1)タイプIII様ドメインを欠失した変異キチナーゼA1を用い、タイプIII様ドメイン欠失の影響を分析する、(2)もともとタイプIII様ドメインをもたないキチナーゼにタイプIII様ドメインを挿入し、その影響を分析する、(3)大腸菌を用いてタイプIII様ドメインを大量発現し、立体構造を解析して構造と機能について分析する、という方針で研究を行い以下のような重要な成果を得ることが出来た。(1)PCR法になどにより、Bacillus circulans WL-12のキチナーゼA1遺伝子からタイプIII様ドメインを欠失した変異キチナーゼ遺伝子を構築し、その遺伝子産物の性質を分析した。その結果変異キチナーゼは不溶性基質の分解活性が低下していることが明らかとなった。(2)B.circlans WL-12のキチナーゼDの、タイプIII様ドメインの部分をコードするDNA領域をPCR増幅し、これをS.marcescens QMB1466のキチナーゼA遺伝子の、活性ドメインとキチン吸着ドメインの間のヒンジ領域に挿入した。この変異キチナーゼは大腸菌での分泌が異常となり初期の目的を達成することは出来なかったが、ヒンジ領域に機能について重要な情報を得ることが出来た。(3)大腸菌を用いてタイプIII様ドメイン単独の大量発現系の構築を試み、これに成功した。現在精製系の検討を行っており、ごく近い将来結晶化を試みることが出来る段階にある。
生体防御のサイトカインネットワークのダイナミックモデルと最適制御の数理的研究

[1]JAK-STAT1経路シミュレータの解析シグナル伝達経路のひとつとして知られるJAK-STAT1経路において,STAT1は防御に関わる様々な遺伝子の転写因子として働く.STAT1が核へ移行し転写を誘導するには,それらのダイマー化が必要であるが,それにより実現されるシステムの有利性に注目し,実験データに基づいて構築されたJAK-STAT1経路のシミュレータ(Yamada et al. ; 2003)およびそれを改変したtoy modelを用いて解析を行った.昨年度の段階では,各モデルに含まれるパラメータ値の再推定など不十分な点が残されていたが,Dr.Jin Yangの協力を得て解決することができた.STAT1がダイマー化されることによって,JAK/STAT1経路は,シグナル量に対してより非線形性の強い応答を実現し,様々な反応係数のゆらぎに対して頑強な応答を実現できることがわかった.[2]C型肝炎ウイルス-薬剤動態;パラメータ推定値の精度の向上昨年度に引き続き,Dr.A.S.Perelsonの研究室を再訪問し,資料収集を行った.従来,患者の治療に必要とされるウイルス-薬剤動態のパラメータ推定は,血中ウイルス量の時系列データを用いて行われてきたが,薬剤動態が従来の薬よりも複雑な新薬"ペグインターフェロンα2b"による治療下では,推定値が大きな誤差を含む危険性が指摘され,血中薬剤量データを併用した複雑な解析が試みられてきた(Talal et al.2006).しかしながら,血中薬剤量のアッセイは,技術的経済的な問題から,治療の主流としては用いられていない.よって研究代表者らは,血中ウイルス量データのみを用いて正確な推定値を得ることを目ざし,新しいモデルを導出,その精度の解析を行った.以上二報の論文を現在投稿中である.[1]マウスの実験に基づいて構築されたJAK7STAr経路の遺伝子・タンパク質動態のシミュレータ(Yamada et al.(2003))を数理的に解析したJAK-STAT経路はSOCS1を必要な期間必要な量だけ生産するシステムである(Yamada et al(2003))JAK-STAT経路では、IFN-gammaのシグナルによってSOCS1遺伝子転写が促されるが、合成されたSOCS1タンパクは自身のmRNA転写を抑制する.フィードバックループを含むダイナミクスを構築し、諸分子動態を明らかにした.また、マウスで実現されているJAK-STAT経路の仕組みは、シグナルのゆらぎや、反応係数のゆらぎに対して頑強なシステムであることがわかった.現在、論文を投稿中である.[2]アメリカLos Alamos National Laboratory Perelson教授の研究室は、ダイナミックスに必要なパラメータを実験データから算出し、それを用いて免疫細胞のシミュレータを作成し、重要な論文を多数発表しているが、同研究室を訪問し、その手法習得のための資料収集を行った.ペグインターフェロンα2bは、C型肝炎患者の治療に画期的な新薬であるが、その薬剤動態が従来の薬と比較して複雑なため、従来パラメータ推定に使われてきた数式を用いると、観察者がしばしば誤った推定値を得てしまう.本研究では、患者体内で起こる、ウイルスと細胞のダイナミクスに薬剤動態をとりいれた研究を行い、パラメータ推定における真の値と推定値の誤差を研究した.現在、論文を作成中である.[1]JAK-STAT1経路シミュレータの解析シグナル伝達経路のひとつとして知られるJAK-STAT1経路において,STAT1は防御に関わる様々な遺伝子の転写因子として働く.STAT1が核へ移行し転写を誘導するには,それらのダイマー化が必要であるが,それにより実現されるシステムの有利性に注目し,実験データに基づいて構築されたJAK-STAT1経路のシミュレータ(Yamada et al. ; 2003)およびそれを改変したtoy modelを用いて解析を行った.昨年度の段階では,各モデルに含まれるパラメータ値の再推定など不十分な点が残されていたが,Dr.Jin Yangの協力を得て解決することができた.STAT1がダイマー化されることによって,JAK/STAT1経路は,シグナル量に対してより非線形性の強い応答を実現し,様々な反応係数のゆらぎに対して頑強な応答を実現できることがわかった.[2]C型肝炎ウイルス-薬剤動態;パラメータ推定値の精度の向上昨年度に引き続き,Dr.A.S.Perelsonの研究室を再訪問し,資料収集を行った.従来,患者の治療に必要とされるウイルス-薬剤動態のパラメータ推定は,血中ウイルス量の時系列データを用いて行われてきたが,薬剤動態が従来の薬よりも複雑な新薬"ペグインターフェロンα2b"による治療下では,推定値が大きな誤差を含む危険性が指摘され,血中薬剤量データを併用した複雑な解析が試みられてきた(Talal et al.2006).しかしながら,血中薬剤量のアッセイは,技術的経済的な問題から,治療の主流としては用いられていない.よって研究代表者らは,血中ウイルス量データのみを用いて正確な推定値を得ることを目ざし,新しいモデルを導出,その精度の解析を行った.以上二報の論文を現在投稿中である.
再生組織工学の手法を用いた肺気腫・肺線維症・肺高血圧症治療法の開発

1)ビーグル犬8匹(体重9.014.5kg)の左肺に気管支鏡を挿入し、区域気管支に豚膵エラスターゼを50mg(3750U)生理食塩水5mlに溶解し10回にわけ散布した。28日の期間をおき、肺気腫モデルとして使用した。2)肺気腫モデルの動脈血液ガス分析、スパイロメトリー、ダイナミックMRIを行い、動脈血液ガス分析においては動脈血酸素分圧の低下を認め、スパイロメトリーでは排気量の増大を認めた。ダイナミックMRIにおいては、正常の右肺に比べ、左肺の造影後MRI信号値の低下を認めた。3)8匹の肺気腫モデルのうち4匹を治療群とし、b-FGF200μgをゼラチンマイクロスフェアーに染み込ませ左肺に、気管支鏡を使用し10回にわけ散布した。残りの4匹を非治療群としゼラチンマイクロスフェアーのみを同量投与した。4)投与後28日後に動脈血液ガス分析、スパイロメトリー、ダイナミックMRIを行い、動脈血液ガス分析では治療群において動脈血酸素分圧の上昇を認めた。非治療群では酸素分圧の上昇は認められなかった。ダイナミックMRIでは治療群において左肺の造影後MRI信号値の有意な上昇を認めた。非治療群ではMRIによる信号値の上昇は認められなかった。現在、重症肺気腫モデルを作成し、b-FGFによる肺機能の改善状況を観察している。
非古典論理の代数的証明論とラムダ計算の交差型システムの研究

前年度に引き続き、順序数解析における重要技法の1つであるΩ規則について、代数的観点から研究を行った。Ω規則は可術的なカット除去証明に用いられる構文論的な手法であるが、ブール代数・ハイティング代数の文脈で解釈するとMacNeille完備化と密接な関係にあることがわかる。後者の完備化は、代数的なカット除去証明のエッセンスでもある。そこでこの発見に基づいてΩ規則の代数版・Ω解釈の概念を導入し、二階述語論理の部分体系に対して可術的かつ代数的なカット除去の証明を与えた。二階算術Z2の1無矛盾性が二階述語論理全体のカット除去と同値であることは竹内外史以来よく知られている。上記の応用として、同様の対応関係が帰納的定義の算術理論IDn(ω未満)と二階述語論理のパラメータフリーな部分体系LIPnについて成り立つことを、代数的意味論を用いて証明した。以上の成果については、概要を国際学会CSL2018にて発表し、詳細を雑誌論文にまとめ上げ投稿済みである。その他に行った研究として、(i)線形論理の証明ネットと量子計算に関する基礎研究、(ii)線形論理の有限表示意味論を用いた証明ネットの高速評価の研究が挙げられる。(i)については、過去に調べたブール回路との正確な対応関係を量子回路へと拡げる可能性を模索した。(ii)については、過去の研究で線形論理のスコットモデルを用いてラムダ項の意味論的評価を行う手法を考案したが、代わりに(集合版)整合空間モデルを用いることにより、意味論的評価を(証明ネットの意味での)「実験」とみなし、証明ネットへと適用範囲を拡げる研究を行った。本研究課題は(1)非古典論理の代数的証明論の推進、および(2)ラムダ計算における交差型(共通型)システムの意味論的基礎と応用の2点を眼目とするものである。(1)について、非古典論理の代数的証明論の根本にあるのは、証明論的技法は代数の文脈に直接適用可能であり、またその逆も成り立つという洞察である。平成25年度は、証明論における超シークエント計算と代数(双対性理論)における正準拡大のアイデアを融合し、「超正準拡大」の手法を確立した。これは、よい性質を保ちつつFL代数を完備化するための手法である。応用として、様々な非古典述語論理についてエルブランの定理を代数的に証明し、エルブランの定理の代数的本質をとらえることに成功した。また、超シークエント計算における稠密規則除去定理のアイデアを順序代数の文脈に応用し、与えられた全順序FL代数を稠密化するための統一的手法を開発した。応用として、ファジー論理の重要な体系の一つであるuninorm logicが標準意味論について完全であることの代数的証明をはじめて与えることに成功した。以上2件について国際学会の招待講演で発表した。(2)について、単純型付きラムダ計算における交差型(共通型)は、ある種の文脈で高速なプログラム実行(つまりラムダ項の評価)に応用できること、また線形論理のスコットモデルと密接な関係のあることが過去の研究により明らかになっている。平成25年度は過去の研究を継承し、ラムダ計算の別のモデルであるエンゲラーモデルとの関係を明らかにした。また不動点演算子を含む単純型付きラムダ計算へと研究を広げた。未だ継続中であるが、現段階までの予備的成果を国際学会の招待講演で発表した。(1)の中心課題は、非古典論理の証明論におけるさまざまな証明変形の技法が、代数的にも意味を持つことを明らかにすることである。平成26年度は、まず前年度の研究を引き継ぎ、超シークエント計算における稠密規則の代数的解釈を行った。証明論で稠密化規則を除去することは、代数では全順序代数を稠密化することに相当する。このアイデアを応用し、uninorm logicをknotted axiomsで拡張した論理体系一般について、標準完全性定理を証明した。また、ブラウワーの不動点定理がヴカシェヴィッチ無限多値論理に不動点を加えた体系の無矛盾性と等価であることを証明した。それゆえもし後者の論理についてカット除去定理が証明できれば、ブラウワーの不動点定理の別証明(証明論による証明)が得られることになる。(2)については、交差型と線形論理の表示的意味論(とくに整合空間意味論)との対応関係を念頭においた上で、計算可能解析における表現の理論へと応用する研究を始めた。実直線、ユークリッド空間、連続関数空間などは整合空間を用いて表現することができる。すると整合空間上の安定写像によって連続写像や連続作用素がぴったり表現できる。また興味深いことに、整合空間における線形写像は、実直線上では一様連続写像にちょうど対応することがわかった。このことからハイネの定理(実直線のコンパクト区間上で連続性と一様連続性が一致すること)の計算内容に当たる安定写像が存在することを示した。また別研究として、対数領域計算量を特徴づける論理(parsimonious logic)を非一様計算量へと拡張し、ラムダ計算の型システムとして整備を行った。

平成27年度は、証明論に由来する剰余フレームの基礎理論に着手した。すでに剰余フレームは、カット除去と代数的完備化、稠密規則除去と代数的稠密化などの関係を統一的に理解するのに有用なことがわかっているが、これをさらに敷衍し、代数的論理の根幹部分へと推し進めるのが目標である。P. Cintula氏との共同研究では、証明論におけるエルブランの定理と順序代数におけるコンパクト完備化の関係について考察を進めた。またそれと関連して、一階述語部分構造論理や無限積・無限和を伴う部分構造論理の完全性定理を証明するための新しい手法を考案した。(2)の中心課題は、交差型の理論を線形論理の表示的意味論に沿って発展させること、また応用としてラムダ計算の様々な性質を見ていくことにある。平成27年度は、前年度に引き続き、線形論理の整合空間を計算可能解析に応用する研究を進めた(松本慧氏との共同研究)。とくに基幹部分を再構成し、整合空間に基づく実現可能性解釈として圏論的に定式化した。またこの圏がこれまでに考案された種々の実現可能性解釈とは異なることを証明した。最後に関連研究として、伝統的証明論をラムダ計算へ応用する研究に着手した。具体的にはBuchholzのオメガ規則を応用することにより、多相型ラムダ計算のパラメータフリーな部分体系について、強正規化定理を「可術的に」証明することに成功した(秋吉亮太氏との共同研究)。(1)については、前年度までに投稿した論文が順次採択されており、目に見える実績となりつつある。またCintula氏との共同研究を通して、部分構造論理における無限積の完全性など、新たな課題も見えてきた。ただし前年度に残されていたいくつかの問題(ブラウワーの不動点定理の証明論的証明、解説論文の作成など)は未だ中途段階にあり、引き続き努力が必要である。(2)については、整合空間意味論の計算可能解析への応用というテーマが集約しつつある。成果をまとめた論文を近日中に投稿する予定である。また、伝統的証明論のラムダ計算への応用は、前者の専門家である秋吉氏との共同研究によって初めて見えてきた興味深い課題であり、大きな潜在力を秘めていると思う。すでに論文一本が採択されており、今後の展開についてもある程度の見通しがある。一方で本来掲げていた目標の一部、たとえば交差型(線形論理の表示的意味論)を用いてラムダ計算における種々の問題の決定可能性を示すという目標は、やや滞っている。引き続き努力が必要である。本研究課題は(1)非古典論理の代数的証明論の推進、および(2)ラムダ計算における交差型(共通型)システムの意味論的研究と応用の2点を眼目とするものである。(1)については、非古典論理の証明論をブラウワー流の不動点定理と関連付ける研究を集中的に行った。Lukasiewiczの無限多値論理(およびその下位論理)は自己否定を始めとする不動点演算子を加えても無矛盾なことが知られており、その証明には普通ブラウワーの不動点定理が用いられる。本年度はその逆方向、つまりLukasiewicz論理+不動点演算子の無矛盾性を証明論的に示すことにより、ブラウワーの定理に別証明を与える可能性を追求した。成功すれば非古典論理証明論の純数学的応用としての意義がある。
小胞体機能異常による細胞内カルシウムシグナルと記憶学習の障害

申請者は、小胞体機能を担うジャンクトフィリン遺伝子欠損マウスの解析の結果、ジャンクトフィリン遺伝子欠損マウスでは、認知機能の有意な低下が認められ、その細胞内機序として神経細胞の活動電位における再分極機構であるAfterhyperpolarization(AHP)の機能異常ならびにカルシウム活性型カリウムチャンネル(SK channel)の異常により、認知機能の低下が惹起されていること、さらに、細胞内で認知機能と密接に関与しているカルシウム/カルモデュリン依存性プロテインキナーゼII(CaMKII)の活性異常が認められ、小胞体機能異常が誘発されると、細胞内のカルシウム恒常性の異常が起こり、認知機能の獲得に異常が認められることを明らかとした。申請者の最近の研究により、小胞体機能異常と統合失調症との関与についても新しい知見を得た。覚醒剤であるメタンフェタミンを慢性的に実験動物に投与すると、経日的な異常行動、すなわち行動逆耐性が誘発する。しかしながら、ジャンクトフィリン遺伝子欠損マウスでは、行動逆耐性の誘発は認められない。情動行動に関与する線条体においてシナプス可塑性の変化について電気生学的検討を行った結果、皮質-線条体に投射するグルタミン酸シナプスにおいて、通常見出される長期抑圧現象(LTD)がジャンクトフィリン遺伝子欠損マウスでは認められなかった。さらに、メタンフェタミンは線条体の細胞内CaMKIIの活性を低下させるが、ジャンクトフィリン遺伝子欠損マウスではCaMKIIの活性の低下は認められなかった。すなわち、小胞体機能による細胞内カルシウム調節が行動逆耐性の誘発に関与する可能性が示唆された。本研究により、新しい認知機能ならびに統合失調症の細胞内機序の確立を行った。今後、小胞体機能異常により様々な病態との関与について検討を行う予定である。本領域研究において、小胞体機能を担うジャンクトフィリンならびにBSRPの記憶学習に及ぼす影響についてジャンクトフィリン遺伝子欠損マウスならびにBSRP遺伝子欠損マウスを作成し、電気生理学的手法、生化学的手法、免疫組織化学的手法、行動薬理学的手法を利用して解析した。その結果、ジャンクトフィリン遺伝子欠損マウスでは、行動解析により有意な記憶学習機能の低下が認められ、同時に、海馬CA1領域におけるLTPの有意な低下が認められた。さらに、Afterhyperpolarization(AHP)の解析をスライスパッチ法により検討した結果、ジャンクトフィリン遺伝子欠損マウスではAHPが認められず、Ca2+ activated K+ channel(SK channel)の異常が誘導されていることが、記憶学習機能の低下に関与していることが明らかとなった。また、海馬CA1領域では、記憶学習に重要な役割を果たすことが報告されているCaM Kinase IIの活性に異常が認められた。以上の結果は、小胞体機能を担うジャンクトフィリンが記憶学習機能に重要な役割を果たしていることが明らかとなった。(Moriguchi et al.,PNAS(2006))一方、BSRP遺伝子欠損マウスにおいても同様に記憶学習機能の低下が行動解析により明らかとなった。現在、より詳細な解析を遂行中である。本研究により、記憶学習機能において小胞体が重要な役割を果たしている可能性が明らかとなり、今後、より詳細に検討を予定している。
進んだ型システムを持ったプログラミング言語における型検証器の機械的な証明

プログラムの完全な正しさを保証するには、プログラムの論理自体を機械上に証明するしかない。この研究では,OCamlと同等の機能をもった型検証器を完全に証明し,正しさを証明されたプログラミング言語の実装の中心に据えることを目指した。具体的には、Aydemir等のEngineering Metatheoryという手法に基づいてOCaml特有の構造的多相性(オブジェクトおよび多相ヴァリアント)を形式化し、型システムの健全性、型推論の健全性と完全性、スタックベースのインタープリターの正しさを形式的に証明した。さらに副作用のための「緩和された値限定多相性」や再帰的型定義の検証の一部も証明した。この一年で、研究計画にあった検証された型推論およびインタープリタの値多相性への拡張を進めるのと同時に、前段階での結果をAPLASという上海で開催された国際学会で発表した。分かりやすくするための証明の修正も行った。また、フランスのENSリヨンから来たPierre-Marie Pedrotと一緒に、同じ定理証明支援系Coqの中で住井英二郎氏の「環境相模倣」という証明法を実現する実験を行った。環境相模倣を使うと比較的簡単にプログラムの同値性が証明できるので、最適化の正しさなどが証明できると期待されている.検証されたインタープリタなどは証明のために効率が悪くなる恐れがあるので、こういう方法でより効率の良いプログラムの正しさが証明できるはずだ。さらに、カナダのConcordia大学から来たJacques Le Normandと一緒にObjective CamlにGADTを追加した。GADTは「拡張された代数的データ型」という意味で、通常のプログラミング言語の中で証明にあるような依存性のある場合分けを可能にする。型システムを拡張しているので、ある意味で「検証された型推論」という目的をさらに難しくしているが、同時にGADTを使うことで通常のプログラミング言語でも一部の性質の証明が可能になるという利点がある。全ての性質をCoqで証明するのは難しいので、停止性等が求められていないコードについて必要な性質だけをGADTで証明し、Coqで書かれたコードと安全にリンクするというアプローチが考えられる.この一年では、データ型および可変なデータ型の実装方法を検討し、実装を始めた。そこで特に問題になったのは、今まで作って来た証明の全ての補題を拡張する必要があり、場合によって補題の命題自体も変える必要があった。このため、もっとモジュラリティの高い証明の構築方法を検討し始めた。来年度はこれを用いて拡張を完成させたい。また、今回のインタープリターに含まれないものの、再帰モジュールにおける参照関係の判定可能性に関する研究をタリン大学の中田景子さんと一緒に行っており、そのアルゴリズムの正しさをCoqで証明した。その際、扱っている対象が高階関数を含めないことを利用して、束縛変数を相対的ではなく絶対的に扱うことができた。それによって、様々な証明がやりやすくなったので、こういう方法が高階関数を含む体系にも応用できないか、検討し始めた。少し趣きが違うが、この研究の対象でもあるOCamlの開発にも遂行しており、昨年Jacques Le Normandと一緒に手がけた一般化代数データ型(GADT)の実装を完成させた。そこで今回の研究でも対象になっている主要性が問題になり、フランスのINRIAのDidier Remyと一緒に検討した結果、曖昧性の問題を解決する方法が見つかった。曖昧性のなさは主要性より弱い性質だが、GADTに関して本当の意味での主要性は完全な型注釈がなければ得られないので、曖昧性の解決がより重要な性質になる。将来的に当検証された型検証器についても、主要性と曖昧性のなさを区別する必要が出てくると思われる。この一年では、新たな型定義の形式化とその整合性のチェックを手がけた。しかし、定義される型が正則であることをチェックするアルゴリズムができたものの、その証明はまだ未完成である。この部分は今後もタリン工科大学の中田景子さんと協力して行う予定である。それ以外に、OCamlの現在の実装に関する改善や拡張も続けている。前年度に導入したGADT(一般化代数的データ型)の実装の強化や理論的な裏付けを行った。特に、フランスのINRIAのDidier Remyと一緒に考えた型推論の主要性を損なわないGADTの型システムを完全に形式化・証明し、2013年のAPLASで発表した。十分に形式化されたので、今後はCoqでの実装への導入も考えたい。もう一つの拡張はモジュールエイリアスの導入である。今まだは、OCamlで新しいモジュールを古いモジュールの別名として定義しても、型システムではモジュールの関係が分からなかった。そのせいで、型の等価性が不完全になったりした。また、効率の面でも、インターフェイスが無駄に大きくなったり、コンパイル時間にも影響していた。モジュールエイリアスの導入によって、そういう問題が解決できた。

ちなみに、モジュールエイリアスの理論は中田景子さんと一緒に再帰モジュールのために作ったものであり、この先行研究がなければ理論的な難しさから実現しなかっただろう。こちらについては、部分的なCoqでの証明があるので、検証されたインタープリターでも導入を考える。この一年では、副作用を考慮した多相性の制限を実装し、その健全性もCoqで証明した。OCamlで採用されている「緩和された値限定多相性」は通常のML系言語に比べて柔軟性があるが、その証明が「意味的な型」を利用するのが特徴的である。フランスから修士課程の研修で来たENS LyonのThomas Leventis氏と一緒に証明方針を考え、それをCoqに移した。途中結果として、その理論的な基礎であるFrancois Pottierが提案したBT(X)という型体系の健全性の証明も得られた。ただ、証明方針がもとのインタープリターと異なっているので、これからその結果を組み込む方法を考えなければならない。また、タリン工科大学の中田景子氏と一緒に、再帰型定義の整礎性・正則性を確認するアルゴリズムの形式化を始めた。具体的には、メモリ・グラフの上で定義されているOCamlのアルゴリズムをCoqで明示的なグラフ構造で実装し、証明を始めた。現時点では型の完全な展開の停止性および展開がグラフの性質を崩さないことが証明されている。これから、グラフの意味が変わらないことと、正則性のチェックに関する証明を完成させなければならない。このCoqでの証明と並行して、OCamlの型システムの拡張が続いている。2012年7月にGADT(一般化代数的データ型)を含んだOCaml 4.00がリリースされた、そこではフランスのINRIAのDidier Remyと一緒に考えた集合の単一化による曖昧性の解消法が採用されている。それについてCopenhagenのML Workshopで発表したが、最近になって具体的な証明が完成したので、近々論文を投稿する予定である。もとの方針では、機能を次々とコア言語に追加する予定であったが、これでは相乗効果で証明が複雑になり、新たに機能を追加する際の壁が段々高くなる。そのために、そういうことの起きない証明の構造を考えなければならない。25年度が最終年度であるため、記入しない。研究実績の概要に書いてあるとおり、様々な機能の証明が着実に進んでいる。しかし、もとの方針では、機能を次々とコア言語に追加する予定であったが、現時点では証明を独立に行っている。もとの方針に従って実装すると、相乗効果で証明が複雑になり、新たに機能を追加する際の壁が段々高くなる。研究実績の概要や現在までの達成度に書いたように、今までの方法で次々と新しい機能を追加して行くのはかなりの労力を必要とする。モジュラリティの高いやり方を考えながら、各機能を別々で証明して行く形で進めるつもりである。