「こうすれば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…

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

http://return0.info/note/2014-11.html#id2014-11-26 ： 俺は今でもCatyスキーマが今のところ世界でもっとも使いやすいスキーマ言語だと思っている Kuwataさんや僕がこういうことを言うと手前味噌なわけですが、実際のところCatyスキーマより書きやすいスキ…

「オートマトンの定義を書き換えてみる」で説明した事情により、オートマトンとは「小さい圏から任意の圏への関手」ということになります。関手の定義域を小さい自由圏に限るなら、自由圏の生成系である有向グラフを考えて「有向グラフから任意の圏へのグラ…

オートマトンとラベル付き遷移系（labeled transition system）はほとんど同じものです。ここでは区別せずに遷移系全般をひっくるめて「オートマトン」と呼ぶことにします。オートマトンによりモデル化できることは多いですが、目的によっては通常の定義では…

「零の概念とmax-plus半環の紹介」において： max-plus半環やmin-plus半環の計算技術は、トロピカル代数（tropical algebra、より一般にはエキゾチック代数）と呼ばれたりします。[...snip...] 例えば、プログラム意味論に計量的な要素を入れるとき、トロピ…

「1 = 0 のとき、いったい何が起きるのか？」に補足をします。普通に考えると、1 = 0 という等式が変だと感じるのはなぜか？ をもう少し詮索します。また、「1 = 0 のとき、いったい何が起きるのか？」の最後で触れた以下のような「もっと奇妙な例」も紹介し…

2008年から2010年くらいに、トロピカル代数や一元体F1の話をよくしていました。今でもウッスラと興味は続いています。ずっと疑問に感じているのは、「一元体では、なぜ足し算がないのだろうか？」ということです。「定義より足し算を持たない」と言ってしま…

1 = 0 が成立する世界では、何が起きるでしょうか。次の2つの回答が考えられます。 世界が崩壊する。 何ごとも起きない。 普通は、世界が潰れて縮退する事態となります。しかし、エキゾチックな世界では、 1 = 0 は「それがなにか？」という程度のことで、特…

PowerShellでは、echo、cat、lsといったよく知られたコマンドは最初から用意されています。ただし、これらは別名（alias）であって、PowerShell本来の名前は Write-Output、Get-Content、Get-ChildItem です。コマンドラインから対話的に使うには短い名前が…

AとBを集合として、直積を A×B とします。2つの射影を p:A×B→A と q:A×B→B とします。具体的に書くと、p(a, b) = a、q(a, b) = b です。さて、ある人に「射影って全射ですよね？」と聞かれたので「もちろん、そうだよ」と答えました。となると、「直積の射影…

「【喧嘩上等！】ガチで喧嘩が強い芸能人」という、紙芝居風YouTube動画があるのですが、それによると： 渡瀬恒彦 元プロキックボクサーの安岡力也さんをタイマンで倒している。 ジョー山中 安岡力也さんをタイマンで半殺しにしたという噂も。 石倉三郎（石…

10月から、またKuwataさんと一緒に仕事してます。「また」と書いたのは、実は、Kuwataさんと僕は2010年の春（Catyプロジェクトはその一年前）から某社の某システムの一部を作っていたのです。その某システムについて書いたことは一度もありません。守秘義務…

アブラムスキーの抽象スカラーを一般化して、ダガー圏と組み合わせると、内積ベクトル空間の性質をある程度は再現できます。関係圏の構造（の一部）をこの枠組で説明できます。内容： その後の抽象スカラー スカラーとベクトルの計算 ダガー圏 ベクトルの内…

圏論では、形容詞的接頭辞として「余（co）」や「双（bi）」をよく使います。しかし、その使い方が統一されているわけではありません。用語法は歴史的な積み重ねの産物なので、必ずしも整合的とは言えないのです。モノイド、余モノイド、双モノイド「余」と…

このブログで何度か名前を出している（例えばコレ）M.W.ホプキンス（Mark William Hopkins）は、パリクの定理（Parikh's theorem ）に興味を持っていたようです。「Mark W. Hopkinsは今どこに？」で紹介した"Parikh's Theorem in Commutative Kleene Algebra…

久しぶりにGNU Makeを使いました。 $ make --version GNU Make 3.81 Copyright (C) 2006 Free Software Foundation, Inc. This is free software; see the source for copying conditions. There is NO warranty; not even for MERCHANTABILITY or FITNESS F…

N = {0, 1, 2, 3, ...} に足し算を考えた可換モノイドは、一番お馴染みの代数系と言えるでしょう。Nは無限の長さ（大きさ）を持ちますが、この長さを2倍に引き伸ばして、その上で足し算を考えてみます。まず、集合Nの2つ分の直和 N + N を作ります。分かりや…

二値真偽値 {true, false} のブール代数は、論理ORを足し算、論理ANDを掛け算として半環となります。集合Aのベキ集合Pow(A)は、合併を足し算、共通部分を掛け算として半環です。アルファベットΣの言語の代数 Lang(Σ) = Pow(Σ*) も（たいていは非可換の）半環…

僕は、WindowsでもMinGW/MSYSのbashを主に使っています。でも、cmd.exeもけっこう使います。bashだと、/etc/profile、~/.bash_profile、~/.bashrc とか、スタートアップ・ファイルが幾つもあります（あり過ぎだよな）。昔は、cmd.exe（つうよりcommand.comか…

「引き算と無限個の足し算は両立しない」で述べた内容は、一種のダメ定理（no-go theorem、ダメな定理のことではなくて、「そりゃダメだ、無理だわさ」と主張する定理）です。引き算（あるいは負の元）が自由に使える状況では無限和が使えないということです…

クレジットカードの利用記録を見ると、「ＫＤＤＩ 通話料金」という項目で、毎月950円が引き落とされています。思い当たるフシがない。謎だ。思い切って電話で問い合わせてみました。過去に、携帯も入れると6個くらいの電話番号を使ったことがあるので、調べ…

2000年代の初頭に、マーク・ウィリアム・ホプキンス（Mark William Hopkins）は次のように語っていました。 形式言語理論と場の量子論は似ている。 この認識と主張を「M.W.ホプキンスの観察」と呼ぶことにします。ゴラン（Jonathan S. Golan）は、彼の2003年…

アマゾンのおすすめが神がかりで不思議な（むしろ不気味な）件、何度か記事にしました。 2011-04-06 「アマゾンからのおすすめの本」-- 『やめないよ』三浦知良 僕はスポーツ関係の本をアマゾンから買ったことなんて全然ないです。一般書店で入手しにくい理…