存在限量子を解釈する際に勘違い

松坂の集合位相入門P.19あたりにある集合系のすべての要素を対象にした和集合をCoqの帰納型で表現しようとしたが、それを使って本文の命題を証明するときに問題が発生した。

本文中では

∪V = {x|∃ A∈V (x∈A)}

というような∃量化を使った定義だったが、 これをCoqで使われるような表記に直す際に

forall x:U, exists A:Ensemble U, A∈V -> x∈A

という解釈をしてしまい、AがVに含まれない場合を考慮しなければならなくなった。集合系Vに含まれる筈の集合Aを議論する際にそれはないだろうと。

本文中の式を日本語で「定義されるXの全ての要素に対して、xを含むようなVの元Aが存在する」というように解釈すると、なんとなく後半が含意でなく論理積を表現しているようなにおいがするんだけど・・・∃より∀の方が使い慣れているので、こちらを使った定義でよく使われる含意を使った形式につられてしまったのだろうか

{x : P | Q}

というような表記を使う形式だとPを|の右側に持ってくる際に、∀の場合は含意、∃の場合は論理積というようなパターンだったので多分最初の定義が間違ってる筈。

IFPuH 3.5

 P.78-80

• Rational Numbersとはなんぞや
• canonical representation
• RationalをHaskellに前述のcanonical representationを保証しつつ導入する
• Rationalをpairとしてではなく独自の解釈によるEqやOrd、Showのインスタンスにする
• derivingを使わずにinstance宣言を書いた意義
• gcdの仕様と実装について
• totalな仕様とeuclidean algorithmによる計算
• Fractionalのinstanceとすることもできる

IFPuH ex1.2.1

問題

「x*yを評価する為にはxとyがnormal formに簡約できるということが必要である」という前提のもと、square infinityの評価が停止するかどうか

回答

square infinityという式の簡約をそのまま考える。
foo = hoge hoge

$$$$
squareinfinity




f
g


z

org-modeでblogger

http://emacs-fu.blogspot.com/2009/05/writing-and-blogging-with-org-mode.html

部分関数

• 部分関数は気持わるいものじゃない

• http://en.wikipedia.org/wiki/Relation_(mathematics)の中程にあるfunctional(also called right-unique)のことらしい
• このSpecial_types_of_binary_relationsのcheatsheet的なものはあれば便利かも

リンデンバウム代数

• 論理と代数を繋げる考え
• Lindenbaum Tarski algebraというらしい(Tarskiェ…) 
•   ゲーデルの不完全性定理を代数学を使って表現してみた
• 数理論理学では常識？
• 「位相と論理」P.40 で触れられている
• Fundamentals of mathematical logic