数えると coinduction

かけ算の議論をしてて発見したんだが、

　アレイ図を数えるが定義だと思ってる反順序

が結構いるらしい。そもそも、アレイ図は、かけ算

　(ひとつ分)x(いくつ分)
　同じ数ずつを足しあわせる

のずいぶんあとで出てくるもので、交換則の証明のかわりに「アレイ図を回転して考える」ってのがあったりする

そこからの発明らしいんだよな。そこで判明するんだが

　アレイ図を書いた時点で、かけ算の値は決まっている
　だから、数えられる

と考えているらしい。まぁ、それは正しくて、

　アレイ図を書いた時点で、累加で値は決まるので、それを数えられる

「数える」ってのが自然数を分解していくならそうなる。なので累加を認めるなら累加で終わりだ

ところが「累加とは異なる数え方がある」とかおっしゃる。そもそも、ちゃんと数えないと

　「13x21=263、数えました」

が通用することになる。つまり、数えるってのは「ちゃんと数える」必要があることになる。ところがこれが結構複雑

　全単射ってことなるんだが、それを示すのは結構厄介

いや、自分も Agda での有限集合の直積の濃度を計算する証明は持ってるんだけど、泣くほどでもないが、そこそこ面倒だ

まぁ、でも

　全単射があるなら、累加と平行して数えることができるので、値は累加と同じことがわかる

実は「全単射だけでは値は決まらない」ん、ん〜? ま、そうかな。なので

　「正しく数えれば、累加と同じで、値は累加から決まる」

ってことになる。つまり、「アレイ図を数える」は、累加で決まった値を数えているだけってのがわかる。問題は

　これを理解する知性が反順序にはない

ことね。困ったもんだ。停止条件は、a x b のaとbの有限性なので、それを使わないと計算できない。それは累加なわけね

Agda にも、0からあるところまで数えるっていうのがあって、coindunction っていうんのがある。Size とかいうDataをこそこそ使う

Automaton を定式化してる時に「coinduction使えば』って言われたんだが、どうにもこうにも

　使いづらいし、入力がリストで決まるなら同じことだろ

ってことで放置中。ユーザ入力とかを codata で処理するとかあるらしいんだが、いまいちだな
-