2023 Fiscal Year Research-status Report
Expansion of the Reasoning Library of Analysis for Formal Verification
| Project/Area Number |
23K11242
|
|---|
| Research Institution | Gifu National College of Technology |
|---|
Principal Investigator |
遠藤 登 岐阜工業高等専門学校, その他部局等, 教授 (30342497)
|
|---|
| Project Period (FY) |
2023-04-01 – 2028-03-31
|
| Keywords | 片側微分 / 不定積分 / 部分積分法 / 置換積分法 / 重積分 |
|---|
| Outline of Annual Research Achievements |
本研究は解析学を中心とした大学理工系学部修了程度の実用的な数学推論ライブラリの構築を目的としている．本年度の研究成果は論文誌「Formalized Mathematics」に4編の論文掲載を行った．以下に詳細を示す．
１．"Differentiation on Interval"では，閉区間上の微分について証明を行った．従来のライブラリは微分を開区間上の演算で定義しており，閉区間上の演算である積分との相性が悪い．具体的には微積分の基本定理に見られる微分と積分の関係で，一方が開区間，もう一方が閉区間の演算となると端点の問題が解消できない．このため微分演算を左微分，右微分により再定義することで閉区間上での微分演算を導入した．また合成関数の微分に関するChain Ruleについても証明した．
２．"Antiderivatives and Integration"では，１で導入した微分演算により不定積分を定義し，各種基本定理を証明した．さらに部分積分，置換積分についても証明を行い，実一変数関数の積分論については概ね形式化が終了した．
３．"Multidimensional Measure Space and Integration"では，直積空間上の測度の構成についてライブラリを構築した．従来までのライブラリでは2つの測度空間の直積測度しか扱えなかったが，これを拡張しn重直積に対する直積測度を構成した．また従来ライブラリの派生としてn変数連続関数のn重直積空間上の積分をn-重積分に変換可能であることも証明した．
４．"Integral of Continuous Two Variables Functions"では，３の結果を踏まえ，実2変数関数の積分について報告した．特に実2変数連続関数についてはリーマン積分による2重積分への変換について証明した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
今年度の研究結果により，実1変数関数のRiemann積分論については概ね形式化が終了した．区分的連続関数など現在のライブラリでは直接評価ができないものも残ってはいるが早急に処理すべきテーマではない．また多変数の積分についてはLebesgue積分論を先に処理した．特に2変数関数についてはRiemann積分により具体的な積分計算が可能な定理群を構築した．
|
| Strategy for Future Research Activity |
本研究で扱う関数解析，ベクトル解析，フーリエ解析，確率論について，今年度の研究結果を踏まえた今後の研究方針は以下のとおりである．
関数解析については可積分関数の空間についての形式化を進める．ベクトル解析については積分論を3次元実数空間に限定した形でLebesgue積分の形式化を行い，これを元にグリーンの定理，ストークスの定理の形式化への基礎理論を構築する．合わせて線積分についても形式化を行うことで実変数関数に対するベクトル解析の基礎理論を構築する．フーリエ解析については，実1変数関数のRiemann積分について，変数変換が可能となったことから，フーリエ級数の基礎理論を構築する．確率論については概収束，測度収束などの概念の形式化を行い，大数の法則，中心極限定理などを目標に基礎理論を構築する．
研究を遂行する上での課題として，現在も含めライブラリは個々の研究者が独立に行ってきた経緯があり，各種概念の表現に若干の違いがある．このことは理論形成において大きな障害となる可能性もあり，異なる表現の同値性を証明するなど本来の研究対象とは異なる手間が存在する．また上記の方針では一般的な教科書に沿った流れで理論の構築を進めていくことになるが，形式化における複雑性を完全には検討しきれていない．このため今後進捗に若干の遅れが発生する可能性は否定できない．
|
| Causes of Carryover |
当初の予定では4回の国内旅費を計上していたが，その他業務との日程調整がつかず，今年度は研究会参加が1回となったためである．このため今年度以降は学会参加がかなわない状況であれば後日論文集の購入等により必要な情報収集を行うことで対応する予定である．
|
