雑感等

音楽,数学,語学,その他に関するメモを記す.

命題論理のメモ "Theorem com12"の証明

com12 - Metamath Proof Explorer
com12 - Intuitionistic Logic Explorer

Hypothesis

Ref Expression
com12.1 ⊢(𝜑→(𝜓→𝜒))

Assertion

Ref Expression
com12 ⊢(𝜓→(𝜑→𝜒))


Proof of Theorem com12

Step Hyp Ref Expression
1 com12.1 ⊢(𝜑→(𝜓→𝜒))
2 ax-2 ⊢((𝜑→(𝜓→𝜒))→((𝜑→𝜓)→(𝜑→𝜒)))
3 1, 2 ax-mp ⊢((𝜑→𝜓)→(𝜑→𝜒))
4 ax-1 ⊢( ((𝜑→𝜓)→(𝜑→𝜒)) →( 𝜓 → ((𝜑→𝜓)→(𝜑→𝜒)) ))
5 3, 4 ax-mp ⊢(𝜓→((𝜑→𝜓)→(𝜑→𝜒)))
6 ax-2 ⊢( (𝜓→((𝜑→𝜓)→(𝜑→𝜒))) → ((𝜓→(𝜑→𝜓))→(𝜓→(𝜑→𝜒))) )
7 5, 6 ax-mp ⊢( (𝜓→(𝜑→𝜓)) → (𝜓→(𝜑→𝜒)) )
8 ax-1 ⊢(𝜓→(𝜑→𝜓))
9 7, 8 ax-mp ⊢(𝜓→(𝜑→𝜒))

"what"のイメージ

文献

  • 伊藤和夫. “Chapter 4 what節”. 英文解釈教室. 改訂版, 研究社, 1997, p.69-92.

疑問詞"what"は単語単体の意味として,
話し手が断定できないモヤモヤした「モノ」を意味すると考えた.

ここで,この「モノ」とは,話し手の主観として,

  1. 存在が認識できる
  2. 不定性を含む

ようなものだとする.


"what"には次のような「様態の不定性」を指す用法がある.

  • 疑問代名詞 "What is this?"

これは,「モノ」が何かを問うている.

  • 関係代名詞 "I have no words for what I then saw."

この文では,「モノ」を先に示し(what),それから「モノ」の詳細(I then saw)を示している.


一方,「様態の不定性」とはいいがたい用法もある.

  • 関係形容詞 "They robbed him of what little money he had."

この用法における"what"は,all the"の意味を含むことを文献が示す.

この場合に,上に示す「様態の不定性」が転じ,
「数量・範囲の不定性」を示すようになり,
さらに,「考えうるものすべて」を示すようになったと考えてみる.
f:id:kazmus:20170324134802p:plain

すると,関係形容詞の用法を受け入れやすいのではないかと考える.

順序対に関する命題のメモ

 文献のp.197のA.2.7の命題の証明の準備

  \{a,b\}=\{a,c\}ならb=c.(中略) a \neq bならb \in \{a,c\}だからb=c.

これに関するメモを記す.

文献

  • 齋藤正彦. “付録 公理的集合論”. 数学の基礎: 集合・数・位相. 東京大学出版会, 2002, p.195-197, (基礎数学, 14).

 外延性公理: \forall x \forall y [ \forall z [ z\in x \leftrightarrow z\in y ]\rightarrow x=y ].
 x= \{ a,b \}  y= \{ a,c \} とすると,
  \forall z [ z\in \{ a,b \} \leftrightarrow z\in \{ a,c \} ]\rightarrow \{ a,b \}=\{ a,c \}.

さらに, z= b とすると,
  [ b\in \{ a,b \} \leftrightarrow b\in \{ a,c \} ] \rightarrow \{ a,b \}=\{ a,c \}.
 b\in \{ a,b \} は明らかに真である.
そして, b\in \{ a,c \} が真となる条件を考える.

 b\in \{ a,c \} が真となる条件は, b=a が真,または, b=cが真であることだ.
条件 a \neq bより, b=cが成立すべきであることが分かる.

常微分方程式の数値解法:ルンゲ=クッタ法,クッタ=シンプソンの方法(1/3法則)

文献が示すルンゲ=クッタの公式を整理する.
文献の"表 8.3 ルンゲ-クッタの公式"と"表 8.4 ルンゲ-クッタの公式(連立方程式)"をもとにする.

文献

藪忠司, 伊藤惇. “8.2 ルンゲ-クッタ法”. 数値計算法. コロナ社, 2002, p.100-101, (機械系教科書シリーズ, 12).

クッタ=シンプソンの方法(1/3法則)

離散化した際の最小単位時間:  h
初期値:  t,\, x,\, y,\, z
次の値:  t+h,\, x+\varDelta x,\, y+\varDelta y,\, z+\varDelta z

2変数(t, x)

 \displaystyle \frac{dx}{dt}=f(t, x)を解く.
 \displaystyle k_1=h f(t, x)
 \displaystyle k_2=h f \left( t+\frac{h}{2},\, x+\frac{k_1}{2} \right)
 \displaystyle k_3=h f \left( t+\frac{h}{2},\, x+\frac{k_2}{2} \right)
 \displaystyle k_4=h f(t+h,\, x+k_3)
 \displaystyle \varDelta x=\frac{k_1 + 2 k_2 + 2 k_3 + k_4}{6}

3変数(t, x, y)

 \displaystyle \frac{dx}{dt}=f(t,\, x,\, y),\, \frac{dy}{dt}=g(t,\, x,\, y)を解く.
 \displaystyle k_1=h f(t,\, x,\, y)
 \displaystyle k_2=h f \left( t+\frac{h}{2},\, x+\frac{k_1}{2},\, y+\frac{l_1}{2} \right)
 \displaystyle k_3=h f \left( t+\frac{h}{2},\, x+\frac{k_2}{2},\, y+\frac{l_2}{2} \right)
 \displaystyle k_4=h f(t+h,\, x+k_3,\, y+l_3)
 \displaystyle \varDelta x=\frac{k_1 + 2 k_2 + 2 k_3 + k_4}{6}

 \displaystyle l_1=h g(t,\, x,\, y)
 \displaystyle l_2=h g \left( t+\frac{h}{2},\, x+\frac{k_1}{2},\, y+\frac{l_1}{2} \right)
 \displaystyle l_3=h g \left( t+\frac{h}{2},\, x+\frac{k_2}{2},\, y+\frac{l_2}{2} \right)
 \displaystyle l_4=h g(t+h,\, x+k_3,\, y+l_3)
 \displaystyle \varDelta y=\frac{l_1 + 2 l_2 + 2 l_3 + l_4}{6}

4変数(t, x, y, z) –2変数・3変数の式から推測し,導出した.

 \displaystyle \frac{dx}{dt}=f(t,\, x,\, y,\, z),\, \frac{dy}{dt}=g(t,\, x,\, y,\, z),\, \frac{dz}{dt}=j(t,\, x,\, y,\, z)を解く.

 \displaystyle k_1=h f(t,\, x,\, y,\, z)
 \displaystyle k_2=h f \left( t+\frac{h}{2},\, x+\frac{k_1}{2},\, y+\frac{l_1}{2},\, z+\frac{m_1}{2} \right)
 \displaystyle k_3=h f \left( t+\frac{h}{2},\, x+\frac{k_2}{2},\, y+\frac{l_2}{2},\, z+\frac{m_2}{2} \right)
 \displaystyle k_4=h f(t+h,\, x+k_3,\, y+l_3,\, z+m_3)
 \displaystyle \varDelta x=\frac{k_1 + 2 k_2 + 2 k_3 + k_4}{6}

 \displaystyle l_1=h g(t,\, x,\, y,\, z)
 \displaystyle l_2=h g \left( t+\frac{h}{2},\, x+\frac{k_1}{2},\, y+\frac{l_1}{2},\, z+\frac{m_1}{2} \right)
 \displaystyle l_3=h g \left( t+\frac{h}{2},\, x+\frac{k_2}{2},\, y+\frac{l_2}{2},\, z+\frac{m_2}{2} \right)
 \displaystyle l_4=h g(t+h,\, x+k_3,\, y+l_3,\, z+m_3)
 \displaystyle \varDelta y=\frac{l_1 + 2 l_2 + 2 l_3 + l_4}{6}

 \displaystyle m_1=h j(t,\, x,\, y,\, z)
 \displaystyle m_2=h j \left( t+\frac{h}{2},\, x+\frac{k_1}{2},\, y+\frac{l_1}{2},\, z+\frac{m_1}{2} \right)
 \displaystyle m_3=h j \left( t+\frac{h}{2},\, x+\frac{k_2}{2},\, y+\frac{l_2}{2},\, z+\frac{m_2}{2} \right)
 \displaystyle m_4=h j(t+h,\, x+k_3,\, y+l_3,\, z+m_3)
 \displaystyle \varDelta z=\frac{m_1 + 2 m_2 + 2 m_3 + m_4}{6}

Haskellプログラミングの考え方

データ変換の連鎖

理想的なHaskellのソースは,

  • 欲しいデータの性質を記述したもの?
  • データの変換手順だけを記述したもの?

関数型というコンセプトの要は、ビジネスロジックを「データの変換」と捉えることにある。

型の細分化

データの意味と型をできる限り一致させるべき.
変換後のデータが既存の型で表せるとしても
新たな型を作り,別の意味を持つデータであることを明示すべきだ.

機能が必要十分―最小のものを使う

MaybeモナドをListモナドで代用してはいけない
事例:返す値の個数が0個1個の関数なのに,Listモナドを使った.
結果:「値の個数が1個以上の場合があるのではないか?」というモヤモヤ感を抱えることになった.

ラテン語版聖書

Latin Vulgate Bible with Douay-Rheims and King James Version Side-by-Side+Complete Sayings of Jesus Christ

in principio creavit Deus caelum et terram

in prīncipiō creāvit Deus caelum et terram.

単語

  • in
    • 前置詞 対奪 「~の中に/~の中で
  • principio
    • prīncipiō←prīncipium 中性名詞 単数 奪与 「最初」
  • creavit
    • creāvit<-creō 直接法 能動 完了 三人称単数「作った」<-「作る」
  • Deus
    • 男性名詞 単数 主呼 「神」
  • caelum
    • 中性名詞 単数 主呼対 「空」
  • et
    • 接続詞 andと同じ
  • terram
    • ←terra 女性名詞 単数 対 「大地」

解釈

<in前 prīncipiō名>
  • 前置詞は直後に名詞句を取り,前置詞句を作る
  • 前置詞句は動詞を含まない

よってin prīncipiōで前置詞句は終わる.意味は「初めに」

creāvit以降は

creāvit動 Deus名 [caelum名 et接 terram名]
  • etがつなぐ語はcaelumとterramだと考え,両者は対格と考える
  • creāvit動 Deus主だとわかる