R言語をインストールしたので、練習に離散力学系の挙動をアニメーションにしてみました。以下の2つのMP4ファイルは、同じ現象を2つの方法で表現したものです。 3次元グラフによる表現 ddds-example-3d.mp4 メッシュを細かくしたヤツ ddds-example-3d_2.mp4 …

世間で統計が流行っている？ んじゃ、Rでも入れてみますか。Coqをインストールしたとき、拍子抜けするくらい簡単でした（Proof Generalは少しめんどくさかった）。歴史のあるソフトウェアは、インストーラーの作り込みもシッカリしてるなー、と感心しました…

「微分のチェーンルール」で接関手（tangent functor）を話題にしたので、誰かなんか接関手について書いてないか？ と"tangent functor"で検索したら、次の論文が引っかかりました。 Title: The Tangent Functor Monad and Foliations Author: Benoît Jubin …

合成関数の微分公式というのがあり、チェーンルール（chain rule）と呼ばれたりします。そのチェーンルールを僕は次の形で覚えています。 単純でいいでしょ。しかし、この単純な形になることをちゃんと説明するのは意外と大変そうだ、と気付きました。以下、…

パウル・ブラ・レヴィ（Paul Blain Levy）による計算モデルにCall-By-Push-Value（CBPVと略記）があります。最近知ったのですが、昔（20世紀）から有名らしいです。CBPVの理論には、ラムダ計算の拡張である項言語（term language）が登場するのですが、コレ…

例えば、配列 [0, 2, 4, 6, 8] に対して、0 + 2 + 4 + 6 + 8 を計算するようなJavaScript関数： function total(a) { var tot = 0; for (var i = 0; i < a.length; i++) { tot += a[i]; } return tot; } > total([0, 2, 4, 6, 8]) 20次のようなTypeScriptク…

今回のラムダ期の課題は、デカルト閉とは限らない非標準な状況でのセマンティック駆動なラムダ計算かな。セマンティック駆動なラムダ計算とは、まず意味領域があって、その意味領域における計算をするためにラムダ式やシーケントを手段として使う計算法のこ…

小説や映画の話じゃないですよ、昨日に続いて「お花見の桜」の話。ここ20年は桜の名所に居るんですが、その前も桜と縁がありました。一時期、上野公園のそばに仕事場があったのです。お花見のシーズン、不忍池から動物園や美術館があるほうに上野公園をズー…

このブログは2005年から始めたのですが、その年の4月12日の記事は： 桜が散ってホッとした です。なぜホッとするのかと言うと： それというのも、ウチの周辺はちょっとした桜の名所で、花見客がうるさいんですよ、深夜まで。桜の期間、ここらへんの人口がい…

変な引き算自然数（0を含む）の範囲内だけで考えます。7 - 5 は2です、では 3 - 5 は？ 自然数の範囲で 3 - 5 の引き算は出来ません。未定義とするのがひとつの案です。どうしても何か値を出せと言われたら、しょうがないので0とするのもアリです。引けない…

ラムダ抽象と定積分を混ぜた計算をしていたら、次の公式が欲しくなったのです。見た目の上では、「ラムダ束縛と積分記号を交換してもいいよ」という形で覚えやすいんですが、これが何を意味しているかハッキリしない。なんだこれは？ と思って考えたら、思い…

ここのところ、ラムダ計算ベースのプログラム意味論とか、また考えてます。フレイド圏を基本的な道具にしようかと。ベーシックなフレイド圏に対して追加したい構造には次のようなものがあるでしょう。 閉構造（指数構造） トレース インデキシング（パラメー…

アロー（Arrows; http://www.cse.chalmers.se/~rjmh/Papers/arrows.pdf）は、2000年前後にヒューズ（John Hughes）によって導入されたプログラミング手法／計算モデルです。これって面白いような、面白くないような？ 僕にとってアローは微妙な概念なんです…

「TypeScriptと関手やモナドなど」において、TypeScriptでリストモナドを書いてみたのですが、コモナド（モナドの双対概念）も扱ってみます。通常、リストモナドと呼ばれているものは、リスト関手の上の載っている自然変換による代数構造です。同じリスト関…

アマゾンが間違いメール？ なんなんだ、これは!? 続・アマゾンが間違いメール？ 事情が判明しました。身に覚えがないメールが来たのが発端。アマゾンに注文したご本人であるX氏宛のメールが檜山に届きました。X氏のアカウントと檜山のメールアドレスがどこか…

「TypeScriptと関手やモナドなど」： 型構成子と型パラメータを持つ関数があれば、とりあえずモナドは定義できるのですが、モナドを構成する型構成子と総称関数達をうまくまとめる機構が欠けている感じはします。 TypeScriptの「まとめる機構」にモジュール…

TypeScript、ごく最近、初めて触りました。名前にTypeと付いているくらいだから、型システムがウリのひとつなんでしょう。パッと見ですが、TypeScriptの型システム、なかなか良さそうです。あえて意地悪に、うまくいかなそうなケースをツツいてみました。例…

2008年に書いた記事「CPS（継続渡し方式）変換をJavaScriptで説明してみるべ、ナーニ、たいしたことねーべよ」はCPSの説明にJavaScriptを使っています。しかし、JavaScriptでは型宣言や型総称（ジェネリックス）が使えないので、「未来のJavaScript」という…

引数を持たない純関数と定数って、区別すべきでしょうか。f() と f を別物とみなすか、それとも f() と f は同じものだとしちゃうか、という問題です。（副作用の話とかは考えません。）別にどうでもいい些細なことのようですが、この問題のせいで微妙な齟齬…

いつからか、「させていただきます」「させていただきました」をよく聞くようになりました。最初は、政治家が使っているのが印象に残ったんだけど、いつのまにかみんなが使うように。例えばプレゼンテーションで、「……の目的で企画させていただきました」「……

「アマゾンが間違いメール？ なんなんだ、これは!?」の続き： 次の可能性を考えました。 アマゾンに複数のメールアドレスを登録できる。 複数のメールアドレスに通知が同報される。 そのうちのひとつのメールアドレスを間違えて入力。 しかし、アマゾンに複…

なにがあったのかというと（少し前のことなので、「ありのまま 今 起こった事」ってセリフは適当じゃないです）、詐欺メールみたいなのが来たのですが、なんか本物のようなんです。本物だとすると、なんで僕（檜山）宛に届いたの？ 事情も対処も分かりません…

間欠的にラムダ計算に対する興味が再燃するのですが、今はその時期かも。Coqを触ったみたのが刺激になったようです。最近の「型付きラムダ計算のモデルの作り方」、「セマンティック駆動な圏的ラムダ計算とシーケント」と、ラムダ計算の記事が続いてます。そ…

「型付きラムダ計算のモデルの作り方」の最後において次のように述べました。 デカルト閉圏によるモデル構成はちゃんとやってみたほうが良いんじゃないかな、と思いながらも割とイイカゲンな記述でした。まー、オオスジはこんな感じなので、あとは細部を埋め…

型付きラムダ計算のモデルをデカルト閉圏で作れるのだけど、ちょっとした注意と工夫が必要です。Cがデカルト閉圏だとして、ラムダ項Mに対して、Mの表示（denotation）をC内に直接作るもんだと思っている人がいるかも知れませんが、それはあんまりウマくない…

圏のなかで指数（exponential, exponentiation）演算が登場することがあります。例えば、Cがデカルト閉圏*1だとして、カリー化／反カリー化による同型は次のように書けます。 C(A×B, C) C(A, CB) ここで出てきたCBが指数です。Cが集合圏のときは、CBは関数集…

僕が豊饒圏の話をするとき、定義を最後まで書き切らないで「他にいくつかの法則を満たす必要があります」みたいな言い方でお茶を濁しています。その理由は、定義を書くだけでもとてもめんどくさいからです。ちゃんと（若干の省略がありますけどね）記述して…

うーむ、話はそんなに単純じゃないみたい。「Coq小ネタ：関数の外延的等値性とか」において、f, g:A→B に対して、f ≡ g ⇔ ∀x.(f(x) = g(x)) として、関数の外延的等値性「≡」を定義したのですが、これではすぐにボロが出ますね。f ≡ g を定義するために f(x)…

A, Bが集合で、f, g:A→B のとき、Coqの組み込みのイコールによる f = g はあんまり具合がよくないようです。普通「関数が等しい」とは、「Aのすべての点において関数値が等しい」ことです。Coqのイコールはそうなってないのです。そこで、ユーザー定義のイコ…

Coqと一緒にOCamlもあったほうがいいのかな、と。インストールするだけで終わるかもしんないけど。 http://protz.github.io/ocaml-installer/ から ocaml-4.01.0-i686-mingw64-installer3.exe をダウンロード。これは普通のインストーラーです。 デフォルト…