ビジュアルプログラミング(7) - エレファント・コンピューティング調査報告

自然数の演算(1)

「数学とソフトウェアのページ」の「自然数の演算」の説明も書いておきます。「自然数の演算」はスマートフォンで使いやすいように「Natural」から説明等を省略したものです。説明は「Natural」の方を見てください。

(1)のリストから式を選んで(2)のボタンを押すと、(5)のテキストボックスに選択した等式が追加されます。

(3)のボタンを押すと、(1)のリストの選択された等式が削除されます。

(4)のボタンを押すと、(5)のテキストボックスの内容が削除されます。

2つの等式を選んで(2つの等式が(5)のテキストボックスに表示された状態にして)、(6)から(10)のボタンを押すと、 2つの式を組み合わせた式が、(15)のリストに表示されます。等式は1つだけ選択することもでき、その場合はその同じ等式を2つ選択したことになります。

(6)のボタンを押すと、両方の等式を左辺から右辺への書き換え規則として組み合わせます。
(7)のボタンを押すと、1つ目の等式を左辺から右辺へ、2つ目の等式を右辺から左辺への書き換え規則として組み合わせます。
(8)のボタンを押すと、1つ目の等式を右辺から左辺へ、2つ目の等式を左辺から右辺への書き換え規則として組み合わせます。
(9)のボタンを押すと、両方の等式を右辺から左辺への書き換え規則として組み合わせます。
(10)のボタンを押すと、(6)から(9)までのすべての組み合わせの結果が表示されます。

(11)のボタンを押すと、(15)のリストの内容が削除されます。

(15)のリストの等式を選択して(12)のボタンを押すと、選択した等式が(1)のリストに追加されます。

(15)のリストの等式を選択して(13)のボタンを押すと、選択した等式の $'$ を ${}^\wedge$ に変えることができるとき(両辺に $'$ が１つずつ存在し、それを除くと両辺が同じ式となるとき)、 ${}^\wedge$ に変えた等式が(1)のリストに追加されます。

(15)のリストの等式を選択して(14)のボタンを押すと、選択した等式の $0^\wedge$ を変数に変えることができるとき(両辺に $0^\wedge$ が１つずつ存在するとき)、変数に変えた等式が(1)のリストに追加されます。

「環の演算」の場合と同様、両辺が同じ $a + b = a + b$ 、 $a * b = a * b$ があります。

第2の等式の左辺(左辺から右辺に変換する場合)が第1の等式の右辺(左辺から右辺に変換する場合)の一部分になっているときに等式を組み合わせることができるようになっています。どちらも他方の一部分になっていない場合は直接組み合わせることができないため、いったん $a + b = a + b$ 、 $a * b = a * b$ と組み合わせて一方の式が他方の一部分になるようにする必要があります。

同様の理由で両辺が同じ $a' = a'$ もあります。また、 $0 = 0$ は式の一部を $0$ で置き換えるためにあります。 $1 = 0'$ は $'$ の数を減らすためにあります。

操作の例

「数学とソフトウェアのページ」の「自然数の演算」の操作の例です。

$0, 0', 0'', 0''', \cdots$ という元からなる集合に演算 $+$ を、 $a + 0 = a$ 、 $a + b' = (a + b)'$ 、演算 $*$ を、 $a * 0 = 0$ 、 $a * b' = (a * b) + a$ と定義します。

$a + b' = (a + b)'$ から $a + b'' = (a + b)'', a + b''' = (a + b)''', \cdots$ が成り立ちます。これを $a + b^\wedge = (a + b)^\wedge$ で表します。これと $a + 0 = a$ から、
$a + 0^\wedge = (a + 0)^\wedge = a^\wedge$ …… (1)
となります。また、 $a + b' = (a + b)'$ から $a + (b + c') = (a + (b + c)') = (a + (b + c))'$ となるので、 $a + (b + c^\wedge) = (a + (b + c))^\wedge$ が成り立ちます。これと $a + 0 = a$ から、
$a + (b + 0^\wedge) = (a + (b + 0))^\wedge = (a + b)^\wedge$ …… (2)
となります。 (1) と (2) から、 $a + (b + 0^\wedge) = (a + b)^\wedge = (a + b) + 0^\wedge$ となり、任意の $\{0, 0', 0'', \cdots \}$ の元 $c$ に対して、 $(a + b) + c = a + (b + c)$ が成り立つことがわかります。

(1-1) $(a + b)^\wedge = a + b^\wedge$

$\begin{matrix} a + b' = (a + b)' \\ a + b = a + b \end{matrix} \implies (a + b)' = a + b' \\ \implies (a + b)^\wedge = a + b^\wedge$
(13)のボタンを押して等式を追加したとき、このように書くことにします。

(1-2) $a + 0^\wedge = a^\wedge$

$\begin{matrix} (a + b)^\wedge = a + b^\wedge \\ a + 0 = a \end{matrix} \implies a + 0^\wedge = a^\wedge$

(1-3) $a + (b + c)' = a + (b + c'),$ $a + (b + c)' = (a + (b + c))'$

$\begin{matrix} a + b' = (a + b)' \\ a + b = a + b \end{matrix} \implies \begin{matrix} a + (b + c)' = a + (b + c') \\ a + (b + c)' = (a + (b + c))' \end{matrix}$

(1-4) $a + (b + c^\wedge) = (a + (b + c))^\wedge$

$\begin{matrix} a + (b + c)' = a + (b + c') \\ a + (b + c)' = (a + (b + c))' \end{matrix} \implies a + (b + c') = (a + (b + c))' \\ \implies a + (b + c^\wedge) = (a + (b + c))^\wedge$

(1-5) $a + (b + 0^\wedge) = (a + b)^\wedge$

$\begin{matrix} a + (b + c^\wedge) = (a + (b + c))^\wedge \\ a + 0 = a \end{matrix} \implies a + (b + 0^\wedge) = (a + b)^\wedge$

(1-6) $a + (b + c) = (a + b) + c$

$\begin{matrix} a + (b + 0^\wedge) = (a + b)^\wedge \\ a + 0^\wedge = a^\wedge \end{matrix} \implies a + (b + 0^\wedge) = (a + b) + 0^\wedge \\ \implies a + (b + c) = (a + b) + c$
(14)のボタンを押して等式を追加したとき、このように書くことにします。