  |
はてなキーワード:帰納的関数とは
第1章 有限オートマトンD.Perrin：橋口攻三郎1. 序論2. 有限オートマトンと認識可能集合3. 有理表現4. Kleeneの定理5. 星の高さ6. 星自由集合7. 特殊なオートマトン8. 数の認識可能集合第2章 文脈自由言語J.Berstel and L.Boasson：富田 悦次1. 序論2.言語2.1記法と例2.2 Hotz 群2.3曖昧性と超越性3. 反復3.1 反復補題3.2 交換補題3.3 退化4. 非生成元の探求4.1 準備4.2 生成元4.3 非生成元と代入4.4 非生成元と決定性4.5 主錐の共通部分5. 文脈自由群5.1 文脈自由群5.2 Cayleyグラフ5.3 終端第3章形式言語とべき級数A.Salomaa：河原 康雄1. 序論2. 準備3. 書換え系と文法4. Post正準系5. Markov系6. 並列書換え系7. 射と言語8. 有理べき級数9.代数的べき級数10. べき級数の応用第4章無限の対象上のオートマトンW.Thomas：山崎 秀記序論Ⅰ部無限語上のオートマトン記法1. Buchiオートマトン2. 合同関係と補集合演算3. 列計算4. 決定性とMcNaughtonの定理5. 受理条件とBorelクラス6.スター自由ω言語と時制論理7. 文脈自由ω言語Ⅱ部無限木上のオートマトン記法8. 木オートマトン9. 空問題と正則木10. 補集合演算とゲームの決定性11. 木の単項理論と決定問題12. Rabin認識可能な集合の分類12.1 制限された単項2階論理12.2 Rabin木オートマトンにおける制限12.3不動点計算第5章グラフ書換え：代数的・論理的アプローチB.Courcelle：會澤 邦夫1. 序論2.論理言語とグラフの性質2.1 単純有向グラフの類S2.2グラフの類D(A)2.3グラフの性質2.4 1階のグラフの性質2.5 単項2階のグラフの性質2.6 2階のグラフの性質2.7定理3.グラフ演算とグラフの表現3.1 源点付きグラフ3.2 源点付き超グラフ3.3 超グラフ上の演算3.4 超グラフの幅3.5 導来演算3.6 超辺置換3.7 圏における書換え規則3.8 超グラフ書換え規則4. 超グラフの文脈自由集合4.1 超辺置換文法4.2HR文法に伴う正規木文法4.3 超グラフの等式集合4.4 超グラフの文脈自由集合の性質5. 超グラフの文脈自由集合の論理的性質5.1 述語の帰納的集合5.2論理構造としての超グラフ5.3 有限超グラフの可認識集合6. 禁止小グラフで定義される有限グラフの集合6.1 小グラフ包含6.2 木幅と木分解6.3比較図7.計算量の問題8.無限超グラフ8.1無限超グラフ表現8.2無限超グラフの単項性質8.3 超グラフにおける等式系8.4 関手の初期不動点8.5 超グラフにおける等式系の初期解8.6 等式的超グラフの単項性質第6章 書換え系N.Dershowitz and J.-P.Jouannaud：稲垣 康善，直井 徹1. 序論2. 構文論2.1 項2.2 等式2.3 書換え規則2.4 決定手続き2.5 書換え系の拡張3.意味論3.1代数3.2 始代数3.3計算可能代数4. Church-Rosser性4.1 合流性4.2調和性5. 停止性5.1 簡約順序5.2 単純化順序5.3 経路順序5.4 書換え系の組合せ6. 充足可能性6.1 構文論的単一化6.2意味論的単一化6.3ナローイング7.危険対7.1 項書換え7.2直交書換え系7.3 類書換え7.4 順序付き書換え7.5 既約な書換え系8. 完備化8.1抽象完備化8.2 公平性8.3 完備化の拡張8.4 順序付き書換え8.5機能的定理証明8.6 1階述語論理の定理証明9. 書換え概念の拡張9.1 順序ソート書換え9.2 条件付き書換え9.3 優先度付き書換え9.4グラフ書換え第7章関数型プログラミングとラムダ計算H.P.Barendregt：横内 寛文1.関数型計算モデル2.ラムダ計算2.1 変換2.2計算可能関数の表現3.意味論3.1操作的意味論：簡約と戦略3.2 表示的意味論：ラムダモデル4.言語の拡張4.1デルタ規則4.2 型5.組合せ子論理と実装手法5.1組合せ子論理5.2 実装の問題第8章プログラミング言語における型理論J.C.Mitchell：林 晋1. 序論1.1 概論1.2純粋および応用ラムダ計算2.関数の型をもつ型付きラムダ計算2.1 型2.2 項2.3証明系2.4意味論と健全性2.5再帰的関数論的モデル2.6 領域理論的モデル2.7 カルテシアン閉圏2.8 Kripkeラムダモデル3.論理的関係3.1 はじめに3.2作用的構造上の論理的関係3.3論理的部分関数と論理的同値関係3.4証明論的応用3.5表現独立性3.6論理的関係の変種4. 多相型入門4.1引数としての型4.2 可述的な多相的計算系4.3 非可述的な多相型4.4データ抽象と存在型4.5型推論入門4.6 型変数をもつλ→の型推論4.7 多相的宣言の型推論4.8 他の型概念第9章帰納的な関数型プログラム図式B.Courcelle：深澤 良彰1. 序論2. 準備としての例3. 基本的な定義3.1 多ソート代数3.2帰納的な関数型プログラム図式3.3同値な図式4. 離散的解釈における操作的意味論4.1 部分関数と平板な半順序4.2 離散的解釈4.3 書換えによる評価4.4意味写像4.5計算規則5.連続的解釈における操作的意味論5.1連続代数としての解釈5.2 有限の極大要素と停止した計算6.解釈のクラス6.1 汎用の解釈6.2 代表解釈6.3解釈の方程式的クラス6.4解釈の代数的クラス7. 最小不動点意味論7.1 最小で唯一の解を得る不動点理論7.2 Scottの帰納原理7.3 Kleeneの列と打切り帰納法8.プログラム図式の変換8.1プログラム図式における同値性の推論8.2 畳込み，展開，書換え8.3 制限された畳込み展開9.研究の歴史，他の形式のプログラム図式，文献ガイド9.1 流れ図9.2 固定された条件をもつ一様な帰納的関数型プログラム図式9.3 多様な帰納的関数型プログラム図式9.4代数的理論9.5プログラムの生成と検証に対する応用第10章論理プログラミングK.R.Apt：筧 捷彦1. 序論1.1 背景1.2論文の構成2. 構文と証明論2.1 1階言語2.2論理プログラム2.3 代入2.4 単一化子2.5計算過程―SLD溶融2.6 例2.7 SLD導出の特性2.8 反駁手続き―SLD木3.意味論3.1 1階論理の意味論3.2 SLD溶融の安全性3.3 Herbrand模型3.4 直接帰結演算子3.5演算子とその不動点3.6 最小Herbrand模型3.7 SLD溶融の完全性3.8 正解代入3.9 SLD溶融の強安全性3.10手続き的解釈と宣言的解釈4.計算力4.1計算力と定義力4.2ULの枚挙可能性4.3帰納的関数4.4帰納的関数の計算力4.5 TFの閉包順序数5. 否定情報5.1 非単調推論5.2 閉世界仮説5.3 失敗即否定規則5.4 有限的失敗の特徴付け5.5プログラムの完備化5.6 完備化の模型5.7 失敗即否定規則の安全性5.8 失敗即否定規則の完全性5.9 等号公理と恒等5.10 まとめ6. 一般目標6.1 SLDNF-溶融6.2 SLDNF-導出の安全性6.3 はまり6.4 SLDNF-溶融の限定的な完全性6.5 許容性7. 層状プログラム7.1 準備7.2 層別7.3 非単調演算子とその不動点7.4 層状プログラムの意味論7.5 完全模型意味論8. 関連事項8.1 一般プログラム8.2他の方法8.3演繹的データベース8.4PROLOG8.5論理プログラミングと関数プログラミングの統合8.6人工知能への応用第11章 表示的意味論P.D.Mosses：山田 眞市1. 序論2. 構文論2.1 具象構文論2.2抽象構文2.3 文脈依存構文3.意味論3.1 表示的意味論3.2意味関数3.3記法の慣例4. 領域4.1 領域の構造4.2 領域の記法4.3記法上の約束事5.意味の記述法5.1リテラル5.2 式5.3 定数宣言5.4関数の抽象5.5変数宣言5.6 文5.7手続き抽象5.8プログラム5.9 非決定性5.10 並行性6. 文献ノート6.1 発展6.2 解説6.3 変形第12章意味領域C.A.Gunter and D.S.Scott：山田 眞市1. 序論2.関数の帰納的定義2.1 cpoと不動点定理2.2不動点定理の応用2.3 一様性3. エフェクティブに表現した領域3.1 正規部分posetと射影3.2 エフェクティブに表現した領域4.作用素と関数4.1 積4.2 Churchのラムダ記法4.3 破砕積4.4 和と引上げ4.5 同形と閉包性5. べき領域5.1 直観的説明5.2 形式的定義5.3普遍性と閉包性6. 双有限領域6.1 Poltkin順序6.2 閉包性7. 領域の帰納的定義7.1 閉包を使う領域方程式の解法7.2 無型ラムダ記法のモデル7.3 射影を使う領域方程式の解法7.4 双有限領域上の作用素の表現第13章代数的仕様M.Wirsing：稲垣 康善，坂部 俊樹1. 序論2.抽象データ型2.1シグニチャと項2.2代数と計算構造2.3抽象データ型2.4抽象データ型の計算可能性3.代数的仕様3.1論理式と理論3.2代数的仕様とその意味論3.3 他の意味論的理解4. 単純仕様4.1 束と存在定理4.2 単純仕様の表現能力5.隠蔽関数と構成子をもつ仕様5.1 構文と意味論5.2 束と存在定理5.3隠蔽記号と構成子をもつ仕様の表現能力5.4階層的仕様6.構造化仕様6.1構造化仕様の意味論6.2隠蔽関数のない構造化仕様6.3 構成演算6.4拡張6.5 観測的抽象化6.6構造化仕様の代数7.パラメータ化仕様7.1 型付きラムダ計算によるアプローチ7.2 プッシュアウトアプローチ8. 実現8.1 詳細化による実現8.2 他の実現概念8.3パラメータ化された構成子実現と抽象化子実現8.4 実行可能仕様9.仕様記述言語9.1 CLEAR9.2 OBJ29.3 ASL9.4 Larch9.5 その他の仕様記述言語第14章プログラムの論理D.Kozen and J.Tiuryn：西村 泰一，近藤 通朗1. 序論1.1 状態，入出力関係，軌跡1.2 外的論理，内的論理1.3歴史ノート2.命題動的論理2.1 基本的定義2.2 PDLに対する演繹体系2.3 基本的性質2.4 有限モデル特性2.5演繹的完全性2.6 PDLの充足可能性問題の計算量2.7 PDLの変形種3. 1階の動的論理3.1 構文論3.2意味論3.3計算量3.4演繹体系3.5表現力3.6操作的vs.公理的意味論3.7 他のプログラミング言語4. 他のアプローチ4.1 超準動的論理4.2アルゴリズム的論理4.3 有効的定義の論理4.4 時制論理第15章プログラム証明のための手法と論理P.Cousot：細野 千春，富田 康治1. 序論1.1 Hoareの萌芽的な論文の解説1.2 C.A.R.HoareによるHoare論理のその後の研究1.3プログラムに関する推論を行うための手法に関するC.A.R.Hoareによるその後の研究1.4 Hoare論理の概観1.5 要約1.6 この概観を読むためのヒント2.論理的，集合論的，順序論的記法3.プログラミング言語の構文論と意味論3.1 構文論3.2操作的意味論3.3 関係的意味論4. 命令の部分正当性5. Floyd-Naurの部分正当性証明手法とその同値な変形5.1 Floyd-Naurの手法による部分正当性の証明の例5.2 段階的なFloyd-Naurの部分正当性証明手法5.3 合成的なFloyd-Naurの部分正当性証明手法5.4 Floyd-Naurの部分正当性の段階的な証明と合成的な証明の同値性5.5 Floyd-Naurの部分正当性証明手法の変形6.ライブネスの証明手法6.1 実行トレース6.2 全正当性6.3 整礎関係，整列集合，順序数6.4 Floydの整礎集合法による停止性の証明6.5ライブネス6.6 Floydの全正当性の証明手法からライブネスへの一般化6.7 Burstallの全正当性証明手法とその一般化7. Hoare論理7.1意味論的な観点から見たHoare論理7.2 構文論的な観点から見たHoare論理7.3 Hoare論理の意味論7.4 構文論と意味論の間の関係：Hoare論理の健全性と完全性の問題8. Hoare論理の補足8.1データ構造8.2手続き8.3 未定義8.4 別名と副作用8.5ブロック構造の局所変数8.6goto文8.7 （副作用のある）関数と式8.8 コルーチン8.9 並行プログラム8.10 全正当性8.11プログラム検証の例8.12プログラムに対して1階論理を拡張した他の論理第16章 様相論理と時間論理E.A.Emerson：志村 立矢1. 序論2.時間論理の分類2.1命題論理 対 1階述語論理2.2 大域的と合成的2.3 分岐的 対線形2.4 時点と時区間2.5 離散 対連続2.6過去時制 対未来時制3.線形時間論理の技術的基礎3.1タイムライン3.2命題線形時間論理3.3 1階の線形時間論理4. 分岐的時間論理の技術的基礎4.1 樹状構造4.2命題分岐的時間論理4.3 1階の分岐的時間論理5. 並行計算：その基礎5.1 非決定性と公平性による並列性のモデル化5.2 並列計算の抽象モデル5.3 並列計算の具体的なモデル5.4 並列計算の枠組みと時間論理の結び付き6.理論的見地からの時間論理6.1表現可能性6.2命題時間論理の決定手続き6.3演繹体系6.4モデル性の判定6.5無限の対象の上のオートマトン7.時間論理のプログラムの検証への応用7.1 並行プログラムの正当性に関する性質7.2 並行プログラムの検証：証明論的方法7.3時間論理による仕様からの並行プログラムの機械合成7.4 有限状態並行システムの自動検証8.計算機科学における他の様相論理と時間論理8.1古典様相論理8.2命題動的論理8.3確率論理8.4不動点論理8.5 知識第17章 関係データベース理論の構成要素P.C.Kanellakis：鈴木 晋1. 序論1.1 動機と歴史1.2 内容についての案内2. 関係データモデル2.1 関係代数と関係従属性2.2 なぜ関係代数か2.3 なぜ関係従属性か2.4 超グラフとデータベーススキーマの構文について2.5論理とデータベースの意味について3. 従属性とデータベーススキーマ設計3.1 従属性の分類3.2データベーススキーマ設計4. 問合わせデータベース論理プログラム4.1 問合わせの分類4.2データベース論理プログラム4.3 問合わせ言語と複合オブジェクトデータモデル5. 議論：関係データベース理論のその他の話題5.1 不完全情報の問題5.2データベース更新の問題6. 結論第18章 分散計算：モデルと手法L.Lamport and N.Lynch：山下 雅史1. 分散計算とは何か2. 分散システムのモデル2.1メッセージ伝達モデル2.2 それ以外のモデル2.3 基礎的概念3. 分散アルゴリズムの理解3.1挙動の集合としてのシステム3.2安全性と活性3.3システムの記述3.4 主張に基づく理解3.5アルゴリズムの導出3.6仕様記述4.典型的な分散アルゴリズム4.1 共有変数アルゴリズム4.2 分散合意4.3ネットワークアルゴリズム4.4データベースにおける並行性制御第19章 並行プロセスの操作的および代数的意味論R.Milner：稲垣 康善，結縁 祥治1. 序論2. 基本言語2.1 構文および記法2.2操作的意味論2.3 導出木と遷移グラフ2.4ソート2.5フローグラフ2.6拡張言語2.7 その他の動作式の構成3.プロセスの強合同関係3.1 議論3.2 強双模倣関係3.3 等式による強合同関係の性質3.4 強合同関係における置換え可能性3.5 強等価関係上での不動点の唯一性4.プロセスの観測合同関係4.1 観測等価性4.2 双模倣関係4.3 観測合同関係4.4プロセス等価性上での不動点の唯一性4.5 等式規則の完全性4.6プロセスの等価性に対するその他の概念5. 双模倣等価関係の解析5.1等価性の階層構造5.2階層構造の論理的特性化6. 合流性をもつプロセス6.1 決定性6.2 合流性6.3 合流性を保存する構成子7. 関連する重要な文献
