ソフトウェア論理学 4/11

lecture 
評価について
期末の頃にレポートと試験を課す
試験で殆ど問題解けない人を救済するためにレポートは存在する
試験が何かconferenceか何かと被った時は要連絡
日本語と英語のを用意する


    

  • -
    • 

Logic and Software
ロジックをソフトウェアの視点から勉強する

Logicというのは一言で言うと
推論(reasonig)を研究する非常に古い分野
アリストテレス
議論する文章作るときの論理の組み立てを勉強する

この授業で勉強するのは更にその一分野の
Mathematical Logic
あるいは
Symbolic Logic
微妙にニュアンスが違う
論理学の一分野かつ数学の一分野
ただし数学科では勉強しないかも

数学(広い意味、コンピュータサイエンスを含む)における
推論を数学的に研究する
対象が数学

整数論であれば整数を研究対象
解析だったら複素関数を研究対象
数理論理学の場合は数学自体の推論を研究対象とする


    

  • -
    • 

ソフトウェア、もしくはコンピュータサイエンスとの関わり

・Turing Machine
→ Computability 計算可能性

Turing Machine で問題を解くことができる
連立方程式は計算可能
でも例えば整数係数不定方程式はわからない

計算という概念を定義しようとした
Turing Machine は計算機が生まれる以前からあった

・ブール代数(命題論理)
↓
論理回路
デジタル回路の基礎

・Lambda Calculus ラムダ計算
関数を基本とする体系
↓
関数型言語 Functional Programming Language
関数を値のように使うことができる
Scheme Haskell
Javaでも将来のヴァージョンでは関数クロージャが入る


    

  • -
    • 

数理論理学とソフトウェアの
共通点としては

・数理論理学
数学の命題や証明を記号化する
論理学の基本となる手法
形式化 Formalize

・ソフトウェア
プログラムというのは
アルゴリズム、計算方法を形式化、記号化したもの

形式化するというのが肝
形式化、記号化が共通している


    

  • -
    • 

今日は 自然演繹 Natural Deduction の復習を行う

Natural Deduction とは何か
・Proof theory 証明論の一つ

証明論とは何か

数学において基本となるのは
・命題 Proposition
　「〜である」という文章
　これは true false（命題の意味）を判断し得る
・正しさ
・証明
　正しさを導く過程

命題というのを形式化、記号化したものが論理式
A ::= P(t1,...,tn)
    | (?A)
    | (A∧B)
    | (A∨B)

正しさを formalizeしたものが意味論 Semantics
例 
((A->B)->A)->A これはトートロジー Tautology
  TT T T T T T
  TF F T T T T
  FT T ..
命題論理における semantics

証明を形式化する理論proof theory
・Natural Deduction
・Sequent Calculus シーケント計算
・Hilbert Style
一長一短ある


    

  • -
    • 

証明
仮定 assumptions
↓推論規則 inference rule
結論 conclution

仮定から木構造のように導く

Natural deduction の嫌な所

1.仮定に関する水増し操作weakeningがあって気持ち悪い

[A] 仮定がAで結論がA

[ A     ] 
[----->I] 
[B->A   ] AとBを仮定をしてAを結論する

[ [A]     ]
[---------]
[ B->A    ]
[---------]
[A->(B->A)] 仮定なし 結論

2.古典論理（背理法）が難しい！

真偽値法で確かめれば簡単なのに
証明を書くのが難しい

例 ((A->B)->A)->A の証明

理由は対象性のなさ

T と F は古典論理では対象
∧  ∨

?(A∧B)<->(?A)∨(?B)
?(∀xA)<->∃x(?A)

# Synmetric でない例がいろいろ

2つの嫌な所を改良したものが
Sequent Calculus

証明とは思えないくらい人工的なもの


    

  • -
    • 

証明をformalizeしたものが証明図
 |                         |
正しさ                 semantics

これれらはどちらも正しさを定義している
これらの関連性を示す性質が
完全性completenessと健全性soundness

Aの証明がある


    

    -A
    


↓soundness ↑completeness

Aが正しい


    

    =A
    


命題論理は健全性も完全性も成り立つ
述語論理も成り立つが自然数とか入れると成り立たなくなる
集合論では完全性は成り立たない

ZF 集合論 （普通の数学言語)
＋C 選択公理 真でも偽でも良い

∀x∃y P(x,y)
↓
∃f∀x P(x,f(x))

すべてのベクトル空間に基底が存在する
（Zornの補題が…）