ブログっ...!

最近はミソフォニアのことばかり書いています。もうミソフォニアブログです。

読んだめも1

よんだはしかたないやつだ!(それは「やんだ」である。。)(よつばとネタ)


callccによる排中律の証明 - sumiiの日記

これ面白かったw
寸劇の話はcallccというワードがヒントになって、わかったw おもしろい。

callccがカリーハワード同型で二重否定に当たる、という話は小耳に挟んだことはあるが、
あんまりよく知らなかった(調べることを忘れていた)ので、調べた。
下のリンクの「call/ccの型」

call/ccと古典論理のカリー・ハワード対応 - 再帰の反復

途中の
λx.(Left x) : A→A∨¬A
のとこで、なんでこうなんだ?と思っていたが、そうだった。
記憶が薄れてて困る。
(下、AgdaのData.Sumリンク。
http://www.cse.chalmers.se/~nad/repos/lib/src/Data/Sum.agda)
(ので、ひとつめのリンク先のInRight(λx:T. k(InLeft x)))は、
InLeft x : T v not T
k(InLeft x) : not
λx:T. k(InLeft x)) : T -> not
となって、InRight(λx:T. k(InLeft x))) : T v not T となるのが解釈。(%s/not/¬/g))
(いっこっつ型を確認する主義)

すごくわかりやすい記事だった...
しっかり理解している方の説明はしゅごいありがたい。

更にこれを読んで、納得してシメ。

http://www.kmonos.net/wlog/61.html#_0538060508

はわわ。。

あと次いでに、voidの話もよんだ。

void - sumiiの日記

Void (コンピュータ) - Wikipedia

あと、前回の記事書いた続きとして、
直観主義論理の話のリンクを超かみつまんで読んだ。

http://www.kurims.kyoto-u.ac.jp/~terui/summer2013.pdf


はっっ、こんなことをしていたらゆうがたに。。じゃあ。。

「構成的」ってなんだ

構成的という言葉の意味がわからなくなって調べてた。
調べたら、「数学的構成主義」「構成的数学」という言葉がちらちら出現。
それも追っかけてたら「数学的直観主義」などなども出現。

直感主義論理は授業でやったので覚えていた。

他もろもろ。

 

数学的直観主義 - Wikipedia

構成的数学とその周辺

数学的直観主義 数学的構成主義 形式主義

 

1) 直感主義論理

授業で先生が以下のようなことを言っていた。

------

A「私のこと本当に好きなの?」

B「好きじゃないわけじゃないよ」

古典主義なA「嬉しい♡ありがとう♡♡」

直感主義なA「ひどい!どういうことっっ」

------

 

2) 構成的論理

(二つ目のリンクがとてもよい。適当に主要だけまとめると)

  • 「現代では直観主義論理は、数学の証明は全て構成的に為されなければならないという主張(数学的構成主義)と関連が深い」(Wikipedia より)
  • あるものの存在dを示すには、dそれ自体を明示する。
  • 「非存在を仮定 => 矛盾 => 存在(背理法)」の流れでは示すことができない。
  • 「AまたはB」の成立を示すには、Aが成り立つことを示すか、Bが成り立つことを示すかどちらか。
  • 「not A かつ not Bを仮定 => 矛盾 => AまたはB」の流れでは示すことができない。
  • 「自分でそれ自体を確認するまでは何も言えない」考え
  • 古典論理に(強い)縛りをかけたものが構成的論理である。

肝心の「構成的」の意味は、「本質的」と言ったほうがしっくりくるような印象をもったんだが、どうだろうか。

 

※二つ目のリンクの冒頭で述べられていた通り、「構成的」という形容詞の解釈がゆらいでいた感じがあった。ちなみに、('constructive' の)英訳を読んでみると、日本語でのイメージとは結構違った。

Constitutively - definition of constitutively by The Free Dictionary

このページもおもしろかった。

アニヲタWiki(仮) - 数学的構成主義

 

3) 形式主義

このページ。

形式主義 ( 哲学 ) - honky tonk manの黙示録 - Yahoo!ブログ

 

でしたー。