ほんとに困っている問題と対策

その他 説明
  1. [含意問題] 含意と論理順序が混同されており、その混同が常態化している。
  2. [メタ問題] オブジェクトレベルとメタレベルの区別、命題と判断〈メタ命題〉の区別や使用法が難しい。
  3. [イコール問題 1] イコール記号が等値じゃなくても使われる。やめさせたいが、適切な記号がない。
  4. [イコール問題 2] イコール記号を使っていい状況でも、使わないことがある。
  5. [イコール問題 3] 恒等としてのイコールと、等値述語が区別されてない。
  6. [変数問題 1] 自由変数と束縛変数という概念の理解、自由変数と束縛変数を区別することが難しい。
  7. [変数問題 2] 変数〈名前〉のスコープと可視性に注意を向けるのが難しい。
  8. [主観位置問題] 主観位置を意識すること、頻繁に迅速に変更するのが難しい。$`\newcommand{\mrm}[1]{\mathrm{#1} }\newcommand{\Imp}{\Rightarrow }\newcommand{\In}{\text{ in } }\newcommand{\Lis}[1]{ \langle{ #1 }\rangle }\newcommand{\Iff}{\Leftrightarrow}`$

内容：

含意問題

ブール値〈真偽値〉の順序も、普通の記号 $`\le, \lt`$ を使う。$`0 \lt 1`$ のように。ブール値〈真偽値〉の等値も、普通の記号 $`=`$ を使う。$`1 = 1, 0 \ne 1`$ のように。ブール値に対する二項演算 $`(\Imp)`$ の演算結果と順序関係 $`(\le)`$ の真偽が一致するのはたまたまだと割り切って、他の場面まで「$`\Imp`$ と $`\le`$ は同じ」を適用しない！

ブール値関数、つまり述語も普通の関数と同様に扱う。

  • ブール値関数にも、演算記号 $`\Imp`$ はオーバーロードして使う（それは普通）。
  • ブール値関数にも、関係記号 $`=, \le`$ はオーバーロードして使う（それは普通）。
  • イコールの使用が抵抗がある／混乱を招くなら $`\equiv`$ を使う。
  • $`\le`$ は、自然数や実数の大小順序と記号コンフリクトを起こすが、それはしょうがない。諦める。オーバーロードだと思って都度オーバーロード解決する。

$`\text{For }X \in |{\bf Set}|\\
\text{For }p, q\in \mrm{Map}(X, {\bf B})\\
\text{Define } p \Imp q := \lambda x\in X.(\, p(x) \Imp q(x) \,)\\
\text{Define } p = q := \forall x\in X. p(x) = q(x)\\
\text{Define } p \le q := \forall x\in X. p(x) \le q(x)\\
\text{Define } p \equiv q := \forall x\in X. p(x) = q(x)
`$

上の定義もオブジェクトレベルの演算や述語をメタレベルで定義していることになるので、[メタ問題]に関わる。メタレベルから見るとき主観位置を変更しているので、[主観位置問題]にも関わる。

次のように書くと、事情が分かりやすくなるかも。$`\mrm{eqBool}`$ はブール値の等値、その他の $`\mrm{xxxBool}`$ も同様。

$`\text{For }X \in |{\bf Set}|\\
\text{We Will Define }\mrm{Imp}_X : \mrm{Map}(X, {\bf B})\times \mrm{Map}(X, {\bf B}) \to \mrm{Map}(X, {\bf B}) \In {\bf Set}\\
\text{We Will Define }\mrm{Eq}_X : \mrm{Map}(X, {\bf B})\times \mrm{Map}(X, {\bf B}) \to {\bf B}\In {\bf Set}\\
\text{We Will Define }\mrm{Le}_X : \mrm{Map}(X, {\bf B})\times \mrm{Map}(X, {\bf B}) \to {\bf B}\In {\bf Set}\\
\:\\
\text{For }p, q\in \mrm{Map}(X, {\bf B})\\
\text{Define } \mrm{Imp}_X(p, q) := \lambda x\in X.(\, \mrm{impBool}(p(x), q(x))\;\in {\bf B} \,)\\
\text{Define } \mrm{Eq}_X(p, q) := \forall x\in X. \mrm{eqBool}(p(x), q(x)) \\
\text{Define } \mrm{Le}_X(p, q) := \forall x\in X. \mrm{leBool}(p(x), q(x))
`$

$`\mrm{Imp}, \mrm{Eq}, \mrm{Le}`$ を対象化して（自分＝主観がメタレベルに昇って）プロファイルを書くと：

$`\quad \mrm{Imp} \in \prod_{X\in |{\bf Set}|}\mrm{Map}(\, \mrm{Map}(X, {\bf B})\times \mrm{Map}(X, {\bf B}) , \mrm{Map}(X, {\bf B})\,)\\
\quad \mrm{Eq} \in \prod_{X\in |{\bf Set}|}\mrm{Map}(\mrm{Map}(X, {\bf B})\times \mrm{Map}(X, {\bf B}) , {\bf B} )\\
\quad \mrm{Le}\in \prod_{X\in |{\bf Set}|}\mrm{Map}(\mrm{Map}(X, {\bf B})\times \mrm{Map}(X, {\bf B}) , {\bf B} )
`$

タプルを山形括弧で囲むとして、ラムダ記法だけで定義を書けば：

$`\text{Define }\mrm{Imp} := \\
\quad \lambda\, X\in |{\bf Set}|.\\
\quad \lambda\, \Lis{p, q}\in \mrm{Map}(X, {\bf B})\times \mrm{Map}(X, {\bf B}).(\\
\qquad \lambda\, x\in X.(\, \mrm{impBool}(p(x), q(x))\; \in {\bf B}\,)\; \in \mrm{Map}(X, {\bf B} )\\
\quad )
`$

$`\text{Define }\mrm{Eq} := \\
\quad \lambda\, X\in |{\bf Set}|.\\
\quad \lambda\, \Lis{p, q}\in \mrm{Map}(X, {\bf B})\times \mrm{Map}(X, {\bf B}).(\\
\qquad \forall x\in X.(\, \mrm{eqBool}(p(x), q(x))\,) \in {\bf B}\\
\quad )
`$

$`\text{Define }\mrm{Le} := \\
\quad \lambda\, X\in |{\bf Set}|.\\
\quad \lambda\, \Lis{p, q}\in \mrm{Map}(X, {\bf B})\times \mrm{Map}(X, {\bf B}).(\\
\qquad \forall x\in X.(\, \mrm{leBool}(p(x), q(x))\,) \in {\bf B}\\
\quad )
`$

イコール問題

等値関係が対称であるという事実（正しいと認める命題）をどう書くか？

$`\quad a = b \Iff b = a`$

が普通だろう。次はダメだろうか？

$`\quad (a = b) = (b = a)`$

中央のイコールを関数のイコールと解釈するなら：

$`\text{For }X \in |{\bf Set}|\\
\quad \left(\lambda\, \Lis{a, b}\in X^2.( a = b)\right)
=
\left(\lambda\, \Lis{a, b}\in X^2.( b = a) \right)
`$

関数のイコールはすべての引数値に対して関数値が等しいことだから：

$`\text{For }X \in |{\bf Set}|\\
\quad \forall \Lis{a, b}\in X^2.(\, ( a = b) = ( b = a) \,)
`$

内側のイコールを $`\mrm{eq}`$ と書くと：

$`\text{For }X \in |{\bf Set}|\\
\quad \forall \Lis{a, b}\in X^2. \mrm{eq}(a, b) = \mrm{eq}( b, a)
`$

これは、関数 $`\mrm{eq} : X\times X \to {\bf B}`$ が対称関数であることを主張している。

最初の $`a = b \Iff b = a`$ も同じように、イコールをニ引数関数と解釈すると：

$`\quad \mrm{eq}(a, b) \Iff \mrm{eq}(b, a)`$

$`\Iff`$ は関係記号ではなくて演算子記号だから、次の関数を定義できる。

$`\text{For }X \in |{\bf Set}|\\
\quad \lambda\, \Lis{a, b}\in X^2.(\, \mrm{eq}(a, b) \Iff \mrm{eq}(b, a)\; \in {\bf B}\,)
`$

これは関数を定義しただけなので、「正しい命題だ」という情報がない。それを明示するなら：

$`\text{For }X \in |{\bf Set}|\\
\quad \mrm{True} \le \lambda\, \Lis{a, b}\in X^2.(\, \mrm{eq}(a, b) \Iff \mrm{eq}(b, a)\; \in {\bf B}\,)
`$

ここで、$`\mrm{True}`$ は、$`\mrm{True} \in {\bf B}`$ ではなくて、定数値関数 $`\mrm{True}_X`$ 。

$`\text{For }X \in |{\bf Set}|\\
\text{Define }\mrm{True}_X := \lambda\,x\in X.(\, 1 \;\in {\bf B}\,)
`$

述語 $`p`$ に対して、$`\mrm{True}_X \le p`$ は $`\mrm{True}_X = p`$ と同じ。この事実を書くと：

$`\text{For }X \in |{\bf Set}|\\
\text{For }p \in \mrm{Map}(X, {\bf B})\\
\quad (\mrm{True}_X \le p) \Iff (\mrm{True}_X = p)
`$

話が循環してしまった。