「こうすればCoqに入門できそうだ （誰も書かないCoq入門以前 5）」： 次にCoqに関する記事を書くとすれば、「Coq入門以前」から「Coq入門」にしようと思います。 と言っておきながら、「入門」ではない重箱の隅のような事を書きます； 「Coqの証明ゲームの…

少し悟ったぞ。Coq入門以前でとどまってしまう事情Coqはゲームソフトだ（と僕は認識してます）から、理屈や内部構造は後回しだと思えてきました。僕自身は、どうしても理屈や内部構造に目がいってしまうので、それを納得しないまま先に進むことが出来ないの…

Coqの理解が進まないで難儀しております。でもまー、J言語よりはマシ。J言語、演算子の記憶が辛過ぎる。Coqのコマンド名は省略なしのフルスペルだから、書くのが面倒だけど記憶はしやすいです。思うに、僕が難儀しているのは年寄りだからでしょう。理解力や…

「Coqの証明はカリー／ハワード対応に基づいていて云々」とはよく言われてますが、その本質は真偽値をどう解釈するか？ というあたりじゃないか、と思います。スローガンは「真偽値は、なんだっていいのだ」です。Coqにおいて、真偽や論理演算（AND、ORなど…

うーむ、ムズカシイ。Coq、難しいなぁ。Coqのプロモーションのために、「大丈夫、あなたも出来ます」みたいなこと言っちゃダメですよ。予備知識も心構えもなく安易に入門しても挫折するもの。「女子高校生でもやってます」って、ものすごく特殊な女子高校生…

「WindowsへのCoqのインストール」： 事情があって、AgdaかCoqを触ってみようか、と。 事情というのは、個々の命題の証明（確認）は割と簡単そうだが、命題がイッパイあるのでウンザリな状況のことです。家計簿の計算が筆算だと面倒だから電卓を使いたい、と…

事情があって、AgdaかCoqを触ってみようか、と。WindowsマシンへのAgdaのインストールはうまくいきませんでした。次の記事にあるような状況らしいですが、かなり萎えます。 http://d.hatena.ne.jp/kiiiino3+lab/20141114/1415947022 http://d.hatena.ne.jp/k…

配列について考えます。この記事では、配列、リスト、タプル、シーケンスなどの言葉をあまり区別せずに、総称的に用語「配列」を使います。内容： 配列のスライスとセレクション セレクションの演算 セレクションのダイアグラム表示 単調単射の圏 セレクショ…