FC2ブログ
--.--
--
上記の広告は1ヶ月以上更新のないブログに表示されています。
新しい記事を書く事で広告が消せます。

08.01
Fri
NJでの証明にはまっています。
所謂カリーハワード対応のおかげでNJ provableな論理式を型としてもつ型付きラムダ項を得たり
逆に型付きラムダ項からNJの証明図を得たりできます。なんか楽しいです。
ということで以下の型をもつラムダ項を証明図を書いてもとめてみようと思います




Screenshot_from_2014-08-01 00:16:40

コロンを挟んで右(の論理式)がラムダ項の型を表しています。
つまり、右だけ見てけば普通に上の論理式をNJで証明していく過程を表していることになります。
で左側がラムダ項を表しています。推論規則MPを適用するときには項をくっつけて、
仮定が落ちるときはラムダをくっつけてやればいい感じです。おおまかいうと。

で得られた関数をHaskellで実際に定義してみたら以下のようになりました。


GHCi, version 7.4.2: http://www.haskell.org/ghc/ :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Prelude> data A
Prelude> data B
Prelude> data C
Prelude> let fun :: (A -> (B -> C)) -> ((A -> B) -> (A -> C)); fun x z y = ((x y) (z y))
Prelude> :type fun
fun :: (A -> B -> C) -> (A -> B) -> A -> C
Prelude>


おおーちゃんと定義できたみたい?ですね。



スポンサーサイト

comment 0 trackback 0
トラックバックURL
http://telracsmoratori.blog.fc2.com/tb.php/190-ddd5d791
トラックバック
コメント
管理者にだけ表示を許可する
 
上記広告は1ヶ月以上更新のないブログに表示されています。新しい記事を書くことで広告を消せます。