kb84tkhrのブログ

何を書こうか考え中です あ、あと組織とは関係ないってやつです 個人的なやつ

定理証明手習い (91) おさらい(1)

さすがに間が空きすぎて、始めのうち何をやってたか忘れてるような気がするのでおさらい
ほんとは最初にざっとみてこれくらい把握しておくんだろうなあ

はじめに、とか

  • 帰納法を使うことで再帰的な関数についての事実を明らかにする方法を知る
  • 入力の可能性が無限にあるときにどう扱うのか
  • それを解決するための帰納法とはなにか
  • 主張に対して等価な式変形を繰り返して'tにすることによって定理を証明する

(reverse (reverse x))がどんなリストについてもxになるか」…(略)…読者への宿題にしておきます。
せんせい、しゅくだいわすれました!

1 いつものゲームに新しいルールを

等価な式への置き換え

  • 引数が何かわからなくても式の値について言えることもある
  • 真であると想定した基本的な仮定を公理という
  • 常に真となる式を定理という
  • 公理でない定理は、真であるという証明が必要
  • 式の一部を、それに等しい式に置き換えてよい
    • 公理または定理を使って置き換える
    • 双方向に適用可能
  • 引数がすべて確定していれば関数適用もできる
  • 置き換えようとする部分をフォーカス、その周囲を文脈という
  • atom/consの公理
  • car/consの公理とcdr/consの公理
  • equal-sameの公理
  • equal-swapの公理
  • Dethmの法則(最初のバージョン)
    • 等しいものは等しいもので置き換えられる
    • ifには対応していない
  • J-Bobは式の書き換えを支援してくれる

引数がわからなくても言えることがある、というのはつまり、
任意の◯◯について◯◯、が言えているということ、でいいのかな

2 もう少し、いつものゲームを

ifのある式の置き換え

  • if-trueの公理とif-falseの公理
  • if-sameの公理
  • equal-ifの公理
  • A部またはE部にフォーカスがあるようなif式のQ部を前提と呼ぶ
  • Dethmの法則(最終バージョン)
    • 等しいものは等しいものと置き換えてよい
    • ifのA部またはE部にある帰結を適用する場合は、前提が同じ条件であること
  • jabberwocky
  • cons/car+cdrの公理
  • if-next-Aの公理とif-next-Eの公理
  • ifの持ち上げ
    • if-same(反対向き)とif-next-A/Eを使ってifをまとめる

3 名前に何が?

証明とは何か、関数適用の置き換え

  • まだ証明されてない定理を主張という
  • 証明とは、式の書き換えを繰り返して最後には'tで終わる一連のステップを言う
  • Defunの法則(最初のバージョン)
    • 再帰的でない関数の適用は、関数本体の仮引数を実引数に置き換えたもので置き換えることができる
  • 洞察:無関係な式は飛ばそう

そういえば、ここでやる証明とゲーデルのPでやった証明とは向きが反対なんだなあ

4 これが完全なる朝食

全域性と尺度

  • 関数が全域である、とは、どんな値を渡しても関数が値を持つということ
    • 何かしら値を返していればよい
  • 組み込み関数はすべて全域
  • Defunの法則(最終バージョン)
    • 全域関数の適用は、関数本体の仮引数を実引数に置き換えたもので置き換えることができる
  • 全域でない関数を部分関数という
  • 矛盾した結果が生じる場合があるので部分関数にDefunの法則は使えない
  • 尺度とは、定義している関数が再帰的に呼び出されるたびに減少する自然数を返す式
  • natp/sizeの公理
  • size/carの公理
  • size/cdrの公理