パイプライン指向JSON処理プログラミング言語 jq - 檜山正幸のキマイラ飼育記 (はてなBlog)
jq（https://stedolan.github.io/jq/）の紹介では、「JSON処理のワンライナー〈一行野郎〉としてめちゃくちゃ便利！」とアピールするのが定番です。もちろんそれは本当で、「めちゃくちゃ便利！」です。が、実は jq は、ワンライナー記述にとどまらない、かなり本格的なプログラミング言語です。 JSON処理のためのDSL〈Domain Specific Language | 領域特化言語〉なので、汎用言語ではありません。しかし、汎用言語が備えている言語機能の一部（関数定義、モジュールシステムなど）を jq も持っています。また jq は、独特で楽しいプログラミング・パラダイム -- “パイプライン指向”に基づいて設計されています。 この記事では、ワンライナーを超えた jq の使い方と、プログラミング言語としての jq の特徴を紹介します。長い記事になってしまったので、一
ド・ラーム・コホモロジーとホッジ分解のオモチャ (1/2) - 檜山正幸のキマイラ飼育記 (はてなBlog)
技術者・プログラマが、ド・ラーム理論〈de Rham theory〉やホッジ理論〈Hodge theory〉を必要とすることなんてあるのか？ ほとんどないとは思うのですが、「稀にはある」というのはどうも事実のようです。 なので、そのテの話をします。簡単なオモチャ〈toy model〉に関して、ド・ラーム・コホモロジーと調和形式によるその表示を、線形代数の技法だけで定式化します。その際、多様体や微積分の知識は仮定しませんし、使いもしません。ただし、背景や周辺のオハナシではいろんな概念が登場します、オハナシとして。 今回・前編(1/2)と次回・後編(2/2)の2回に分けて書きます。「ド・ラーム・コホモロジーとホッジ分解のオモチャ」の中核となる有限次元線形代数の議論は次回に行います。今回は、全体像や周辺知識、準備的な項目についてウダウダ述べます。 内容： 予備知識は線形代数だけ 背景のオハナシ（
「確率変数」の正体は米田埋め込み - 檜山正幸のキマイラ飼育記 (はてなBlog)
確率変数（random variable, stochastic variable）という言葉の意味が分からない！ と何度か書いています。 2015-05-26 「確率変数」と言うのはやめよう 2015-05-27 「分布、測度、密度」は同じか違うか 2015-06-17 まだ「確率変数」が分からない 結局分からないままでした。「慣れ」の問題かも？ と思ったこともあります。 2015-05-28 「慣れれば分かる」問題 慣れることも出来ませんでした。 最近、「これなら納得できるかな」という解釈に出会いました。 [追記 date="翌日"]最後に分かりやすいマトメを付けました。[/追記] 内容： 「確率変数」はなぜ分からないのか アレックス・シンプソンのアイディア 「確率変数」の2つの用法 確率空間と圏Prob 測度論的確率変数 曖昧な確率変数 前層と米田埋め込み 米田埋め込みとしての確率変
コンピュータ科学や組み合わせ論を“微分幾何”とみなす：CADGの夢 - 檜山正幸のキマイラ飼育記 (はてなBlog)
『シン・ゴジラ』は僕のツボにはまったんですよね。コワ面白かった！ 最近、もうひとつ「これは面白い！」と思っていることがあります。微分幾何の応用の話です。多くの人が「応用」という言葉から連想する内容とはちょっと違います。微分幾何を換骨奪胎して、その枠組を、微分とも幾何ともまったく無関係と思える分野にも適用するのです。 「微分とも幾何ともまったく無関係と思える分野」には、コンピュータ科学や組み合わせ論が含まれます。これには驚きました。好奇心を刺激されて、しばらく猿になって調べまくってました。 調べても理解できないことがたくさんあるので、断片的で中途半端な知識を推測（妄想？）でつなぎ合わせるという手法（いつものやり口）で語ってみます。圏と多様体の定義くらいは仮定しますが、それ以外の知識は要求しないオハナシ調です。 内容： リソース計算が微分計算だってぇぇ?! 微分の計算が出来る圏 組み合せ論とデ
もうGitは怖くない： 自信を持って使いたいあなたへ - 檜山正幸のキマイラ飼育記 (はてなBlog)
2014初頭に書いた「WindowsにおけるGit利用環境は整った： Git for Windows と SourceTree for Windows」の最後の文： ブランチは、Gitのなかで最も重要でありながら最も分かりにくい概念でしょう。表面的な言葉に騙されず、先入観を持たず、SourceTreeの視覚的表示（樹形図）の力を借りながら学習するのが、理解への一番の近道です。 そんへんの詳しいことはまたの機会に述べるかも知れません。 1年半以上たってしまいましたが、「またの機会」がやって来ましたよ。ええ、Gitの説明をします、ブランチを中心に詳しく。 「基礎編」と「ブランチ編」で2回に分けようかと思ったけど、長大な記事として一挙公開。これからGitを使う人が対象ではありません。Gitが何をやっているのか、自分が何をやっているのかイマイチ自信が持てない方向けです。 ブランチやマージって、なん
カリー／ハワード対応に親しむ （誰も書かないCoq入門以前 3） - 檜山正幸のキマイラ飼育記 (はてなBlog)
「Coqの証明はカリー／ハワード対応に基づいていて云々」とはよく言われてますが、その本質は真偽値をどう解釈するか？ というあたりじゃないか、と思います。スローガンは「真偽値は、なんだっていいのだ」です。 Coqにおいて、真偽や論理演算（AND、ORなど）をどう考えるかについて書いてみます。「Coqにおいて」と言いましたが、Coqの操作やスクリプトは全然出てきません。背景となる考え方の話です。 内容： C言語の真偽値 集合全体を真偽値に使う 空集合ではない証拠 論理システムと型システム 関連する記事： 型推論に関わる論理の概念と用語 その5：型付けの簡単な例から型判断へ デカルト閉圏を計算するスタックマシン、シーケント計算、カリー／ハワード対応 シーケント計算と例外処理コード カリー／ハワード（Curry-Howard）のお絵描きを楽しもう C言語の真偽値 C言語では、真偽値用の型（bool
中学レベル代入計算からカリー／ハワード流証明の圏へ - 檜山正幸のキマイラ飼育記 (はてなBlog)
Coqをいじっていると、カリー／ハワード対応の威力を実感します。一方で、証明といえども所詮は計算なんだな、とも思います。中学校くらいでやる代入計算の直接的な延長線上に証明の合成操作があるんですよね。中学レベルの計算と形式的証明では、用語や記号がまったく違うのですが、そこにうまく通路を作ってやると、やってることは大差ないことが分かります。 「寄り道Coq： exactタクティクと型理論と圏論」の最後の節「大きなラムダ式／小さなラムダ式」で述べたことの敷衍です。 内容： 1次式の代入計算 代入の圏 代入をシーケントで表す 型判断を成分とする代入 カリー／ハワード対応による再解釈 Coqにおける実例 まとめと展望 1次式の代入計算 話を簡単にするために、式としては1次式だけを考えます。1次式による計算結果を変数に代入することを次の形で書きます。 v := 2x + 3y - 1 連立の場合もあり
パズル：スワップ・マシンの並列プログラミング - 檜山正幸のキマイラ飼育記 (はてなBlog)
とある問題を考えていたら、パズルに出会ったのですが、僕はパズルが苦手なので、どなたか代わりに考えてください(苦笑)。 k個のメモリセルと1種類の機械語命令を持つ“マシン”を考えます。 メモリセルにはアドレスを付けます。ここでは番号付けを1番からはじめて、1, 2, ..., k がアドレスだとします。0からが好きなら、そうしてもけっこう。 iは、1からk-1のアドレスのどれかとして、機械語命令は s.i の形。その意味は、セルiの内容とセル(i+1)の内容を交換すること。 例えばメモリセルは4個だとして、その内容が AABB だったとします。次の命令列を実行してみます。 s.2, s.1, s.3, s.2 次のように状態遷移します。 AABB s.2 ABAB s.1 BAAB s.3 BABA s.2 BBAA さて、このマシンはマルチコア(?)だとします。同時に複数の命令を実行できま
「わたしはウソをつきません」と言い張る命題やプログラムを書けるのか？ - 檜山正幸のキマイラ飼育記 (はてなBlog)
エイプリルフールに「わたしはウソをつきません。」と書きました。たいした意味はなくて、すぐにウソだと分かるようなひと言のつもり。 そしたら、id:sasa2718さんに、 「この文は証明可能である」という命題を構成するとその命題は証明可能でしょうか？ というクイズ(?)を出されてしまいました。 「私はウソつきです」が矛盾を引き起こしそうなことは誰でも感じるでしょう。一方、「私はウソをつきません」だと、矛盾する言明かどうかは分からないですが、直感的に胡散臭い気はしますよね。「私はウソをつきません」と言っている人を信じますか？ ふつう信じないでしょ。 さて、「この文は証明可能である」という命題も、「私はウソをつきません」と言っている人みたいなもので、どうも胡散臭い。「この文は証明可能である」はホントなんでしょうか、ウソなんでしょうか？ ある程度ちゃんとした形に定式化してみます。このテの話題は何度
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
