2014-12-01から1ヶ月間の記事一覧
「こうすれば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…
配列について考えます。この記事では、配列、リスト、タプル、シーケンスなどの言葉をあまり区別せずに、総称的に用語「配列」を使います。内容: 配列のスライスとセレクション セレクションの演算 セレクションのダイアグラム表示 単調単射の圏 セレクショ…