WEKO3
アイテム
HOLを用いた代入定理の検証
https://ir.soken.ac.jp/records/3145
https://ir.soken.ac.jp/records/3145a13aca2f-65cd-447f-9a1a-78de7fd0a31a
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
要旨・審査要旨 (327.4 kB)
|
||
|
本文 (626.9 kB)
|
| Item type | 学位論文 / Thesis or Dissertation(1) | |||||
|---|---|---|---|---|---|---|
| 公開日 | 2012-09-14 | |||||
| タイトル | ||||||
| タイトル | HOLを用いた代入定理の検証 | |||||
| 言語 | ||||||
| 言語 | jpn | |||||
| 資源タイプ | ||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_46ec | |||||
| 資源タイプ | thesis | |||||
| 著者名 |
小合, 敬之
× 小合, 敬之 |
|||||
| フリガナ |
コアイ, タカユキ
× コアイ, タカユキ |
|||||
| 著者 |
KOAI, Takayuki
× KOAI, Takayuki |
|||||
| 学位授与機関 | ||||||
| 学位授与機関名 | 総合研究大学院大学 | |||||
| 学位名 | ||||||
| 学位名 | 博士（情報学） | |||||
| 学位記番号 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | 総研大甲第1518号 | |||||
| 研究科 | ||||||
| 値 | 複合科学研究科 | |||||
| 専攻 | ||||||
| 値 | 17 情報学専攻 | |||||
| 学位授与年月日 | ||||||
| 学位授与年月日 | 2012-03-23 | |||||
| 学位授与年度 | ||||||
| 値 | 2011 | |||||
| 要旨 | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | 本論文では，高階論理証明システムHOLを用いて代入定理を形式化し検証する． 代入定理とは，与えられたラムダ項と与えられたいくつかのその変数に対して，任意の弱正規化 可能な同じラムダ項を代入してもその項が弱正規化可能であるなら，任意の弱正規化可能な異なる ラムダ項を代入してもその項が弱正規化可能であるという2006年に証明された型なしラムダ計算の 新しい定理である．これは，原論文では弱正規化可能性に関する代入定理とよばれている．我々は 原論文の数学的内容を忠実に形式化する．束縛変数の名前換えの無いラムダ項を扱うために， Homeierのパッケージによって文脈alpha-同値を使用する．本検証の結果，ラムダ計算の新しく重要 な定理を検証することができた． 本論文の第1章では，序論として代入定理の検証の概要とその意義， この検証が成す貢献，関連研究，本論文の構成について説明する．先行研究において採られたラムダ 計算の形式化の手法について論じる．また，ラムダ計算の定理を検証した先行研究ではChurch-Rosser の定理など良く知られた定理が検証されているのに対して，本論文では最近証明されたラムダ計算の 新しく重要な定理を検証したことを述べる．第2章では，予備知識として型無しラムダ計算と高階論理 の自動証明システムであるHOLについて説明する．HOLについては，その論理体系と検証コードの文法， 定理の検証で用いるgoal，tactic，tacticalについて説明する．第3章では，予備知識として代入定理 の数学的記述とその数学的な証明を説明する．代入定理の記述を与え，この定理の証明に導入された コントロールパスと隣接コントロールパスの概念を導入する．代入定理を証明するための主補題を示し， それを用いて代入定理の証明を与える．第4章では，予備知識として文脈alpha-同値と二種類のラムダ 計算について説明する．pure lambda-calculusはpre-lambda-calculusのalpha-同値関係による同値類 として定義される．pre-lambda-calculus，文脈alpha-同値とalpha-同値，pure lambda-calculusを順に 定義し，lambda calculusにおいてpure lambda-calculusとalpha-同値を導入することの利点と問題点 について述べる．また，ラムダ項の代入の定義について説明する．第5章では，第3章と第4章の内容を 形式化し，代入定理の形式化を与える．検証の目標となる代入定理の論理式の形式化を与え，弱正規化 可能性など検証に必要なラムダ計算に関する概念の形式化を与える．部分項の概念を形式化するために， 部分項のindicatorを導入する．コントロールパス，隣接変数出現，隣接コントロールパスなど代入定理 の証明のために導入された概念の形式化を与える．特にラムダ項M中の集合Sからの隣接コントロールパス があることの否定について新たな述語を与えて形式化する．第6章では，代入定理の形式的な証明が得 られることを示す．ラムダ計算の概念を形式化した関数や述語について，代入定理の証明で必要な補題を 形式化して証明する．また，indicatorによる部分項の表示やコントロールパスなどの代入定理の証明に 導入された概念の性質についての補題を形式化して証明する．次に第3章で述べた代入定理の証明に用いた 補題を形式化して証明するが，円滑な証明をするために，主補題を変更する．そして代入定理の形式的証明 の実行について示し，その実行結果について述べて，コード量および処理時間を記す．第7章では，この 研究の解決した問題を論じる．問題解決の第一は，変数の捕捉による困難を解決するために，束縛変数の 名前の集合Sに対し，PWN_Sという概念を導入したことである．これは，原論文で使用される永続的弱正規化 を置き換え，あるラムダ項がこの性質をもつことを示すときに，beta-簡約により起こる代入処理を単純化 する．第二に，変数代入によりコントロールパスが保たれることを検証するために帰納法に適切な変数を 選択する工夫を用いた．この性質の形式的な記述は両方のスタイルのラムダ項を混在させて用いている． 我々は記述中に隠された内側の変数を最外部に移動して帰納法を適用する変数として使用する．第三に， 隣接コントロールパスの存在の否定を表現するために新たな述語を導入した．隣接コントロールパスの存在の 忠実な形式化は暗黙の自由変数条件を正しく表さない．このため，命題の仮定でその否定を使用する場合は， 形式的証明が進まなくなる．この問題を解決するために，我々はその否定が自由変数条件を正しく表すような 新たな述語を導入する．そして第8章では本研究についてのまとめと今後の研究課題について述べる． |
|||||
| 所蔵 | ||||||
| 値 | 有 | |||||
| フォーマット | ||||||
| 内容記述タイプ | Other | |||||
| 内容記述 | application/pdf | |||||
