小学校算数における乗算の非可換性について(書きなおした)(書きなおした)

↓今読みなおすと頭抱えたくなるような記事なんですが残しておきます

基本的なことは 黄金原本更新, 【もはや最短理解でもなんでもない】なぜ5×3ではなく3×5なのか - 跡地, たくさんの反響ありがとうございます - ワタタツの日記!(2010-11-13)に譲るとして。あとその時点での「数」は自然数だから、実数と混同しないでほしい>混同してる人。

なんで乗算を非可換で定義するかって話だけど、それは非可換なまま定義すれば、乗算を構成的に定義できるからじゃないかな。うまく説明できないけど。

Coqだと、自然数の乗算は以下のようになる。(Coqだけの話ではないと思う…)

Fixpoint mult (n m:nat) : nat :=
  match n with
  | O => 0
  | S p => m + p * m
  end

「n×mっていうのは、mをn回足したものですよー」(小学校算数とは逆のようだが)

Lemma mult_comm : forall n m, n * m = m * n.
Proof.
intros; induction n; simpl; auto with arith.
rewrite <- mult_n_Sm.
rewrite IHn; apply plus_comm.
Qed.

「n×mとm×nは同じなんですよー。nについての帰納法で証明できますー」

ちゃんと帰納的に定義している。効率は悪いけど、自然数の乗算の定義は構成的だから、定義を見れば計算できる、みたいな。

実数の定義は違うんだよね。

Parameter Rmult : R -> R -> R.

「実数の乗算ってのがあるんですよー、あるって信じろー」

Axiom Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1.

「実数には可換性が成り立つんですよー、成り立つって信じろー」

やっぱ僕としては前者を支持したいな。

それからさ、数学ガールで言うとこの知らないふりゲームをする機会って、集合論をやり始めたときと小学校算数の2回くらいしかないと思うんだよね。だからさ、ここでちゃんと一個ずつ手順を踏む経験をすることは大事じゃないかな。

ネタ元
黄金原本更新, 【もはや最短理解でもなんでもない】なぜ5×3ではなく3×5なのか - 跡地, たくさんの反響ありがとうございます - ワタタツの日記!(2010-11-13)
かけ算の5×3と3×5って違うの? - Togetter