かけ算の問いに関して「何を何回足したのかを確認する」。問題の意図と、そこでの規則を確認する。回数を右に書くと決めてるなら、それも良い
かけ算の順序はそのまま積分や群の作用につながる
かけ算の対称的な定義は存在しない。なので無理に「かけ算には順序はない」と主張すると、累加の定義を拒否することになる。それではかけ算を理解することはできない
普通に累加でかけ算を定義して交換法則があると考える方が正統だし柔軟。面積などの積で表される物理量をそれで理解できる
＊ 右かけ算と左かけ算
回数を右に取るか左に取るかで、右かけ算と左かけ算を回数で交換則と同時に帰納法的に定義していく方法でかけ算を対称的に定義したい
しかし、それは右かけ算と左かけ算が同じであることを意味しない。それを無理に同じとすると矛盾が生じる
右かけ算とかは右作用とかに対応するから無意味とまでは言わないが、交換則があるなら二つ使うのは無駄ではある。片方で良い
右かけ算と左かけ算は以下のように定義できる
lmul : ℕ → ℕ → ℕ
lmul zero x = zero
lmul (suc x) y = lmul x y + y
rmul : ℕ → ℕ → ℕ
rmul x zero = zero
rmul x (suc y) = rmul x y + y
ね。rmul x y ≡ lmul y x でも良い(この方が簡単)
rmul x y ≡ lmul x y が交換則
＊ 関数外延性
rmul x y ≡ lmul x y から
rmul ≡ lmul を導くのが関数外延性
関数外延性を仮定すると、実装の違う関数を定義することが禁止されてしまう。それは制約が大きい。それを無視すると矛盾する
世の中に乗算器は一つの回路しかないみたいな感じ。詳細に立ち入れない。同じだから
rmul x y ≡ lmul x y
と
rmul ≡ lmul
を区別するのは高階直観論理でも一階述語論理でもそう
LISPで関数同士をeqで比較するような話ね。あるいはCの関数のアドレスの比較
* 面積を使う
面積で縦横変えて自明に交換則が成立すると主張したい
その形が違う点の集合は違うものなので単純に同じとは言えない
まず、それが個数として同じことを確認する。そして、それが足し算の繰り返しになってることを確認する
回転は実数が必要なので大変。止めないけど
No comments:
Post a Comment