2014-01-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…
配列について考えます。この記事では、配列、リスト、タプル、シーケンスなどの言葉をあまり区別せずに、総称的に用語「配列」を使います。内容: 配列のスライスとセレクション セレクションの演算 セレクションのダイアグラム表示 単調単射の圏 セレクショ…
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、ダメな定理のことではなくて、「そりゃダメだ、無理だわさ」と主張する定理)です。引き算(あるいは負の元)が自由に使える状況では無限和が使えないということです…
クレジットカードの利用記録を見ると、「KDDI 通話料金」という項目で、毎月950円が引き落とされています。思い当たるフシがない。謎だ。思い切って電話で問い合わせてみました。過去に、携帯も入れると6個くらいの電話番号を使ったことがあるので、調べ…
2000年代の初頭に、マーク・ウィリアム・ホプキンス(Mark William Hopkins)は次のように語っていました。 形式言語理論と場の量子論は似ている。 この認識と主張を「M.W.ホプキンスの観察」と呼ぶことにします。ゴラン(Jonathan S. Golan)は、彼の2003年…
アマゾンのおすすめが神がかりで不思議な(むしろ不気味な)件、何度か記事にしました。 2011-04-06 「アマゾンからのおすすめの本」-- 『やめないよ』三浦知良 僕はスポーツ関係の本をアマゾンから買ったことなんて全然ないです。一般書店で入手しにくい理…