プログラミング」カテゴリーアーカイブ

Cabal sandboxのメモ

Cabalを使ってHaskellのパッケージ管理をやっていると、依存関係がもつれて酷い事になる。あるプロジェクトで使うパッケージと別のプロジェクトで使うパッケージが干渉したりとかなんかそういうアレだ。こういう時はsandboxを使うと良いらしい。マニュアル

自分のプロジェクトのディレクトリで

$ cabal sandbox init

を実行すれば、新しいsandboxができる。何かパッケージを入れようと思ったら、そのディレクトリで普通に

$ cabal install ほげほげ

を実行すればそのパッケージはそのディレクトリに入る。

sandbox内のパッケージを使ってghciを起動したい場合は、

$ cabal repl

を使う。

sandbox内のパッケージを使ってghcやrunghcなどのコマンドを叩きたい場合は、1.20.0で追加された(?)execコマンドを使うといいようだ。

$ cabal exec ghc -- --make hogehoge.hs

この記事はcabal-install 1.21.0.0の時点の情報をテキトーに調べた結果を書いたので、もしかしたらもっと正しい使い方とかあるのかもしれないが、そんなもん知らん。

(9月21日: typoを修正)

TypeScriptで組み込みオブジェクトを拡張できない

最近、自分で書くWebアプリ、ブラウザアプリには、JavaScriptの代替言語としてTypeScriptを使っている。

TypeScriptの気に入っている点は、

  • 静的型がついているので、変数名のタイポのような、初歩的だけど実行してみないとわからない面倒なバグをコンパイル時に検出できる
  • 文法やセマンティクスがほぼJavaScriptの上位互換なので、すでにJavaScriptを習得している身としては学習コストが低い
  • JavaScriptの資産を活用しやすい
  • 標準の型定義に入っていないブラウザの拡張API等にも、自分で型定義を書けば利用できる

あたりである。逆に、不満があるとすれば

  • セマンティクスがJavaScriptに沿ったものなので、演算子オーバーロードのようなJavaSciptに1:1で翻訳できない機能が使えない
  • 型クラスとかがない
  • ECMAScript 6で導入される予定の、letや分割代入やジェネレーターなどの、言語の文法に対する拡張に対応していない(新しいラムダ式のような一部の機能は既に導入されているので、将来的には入るかもしれないが)

あたりであろうか。まあ不満があったら他のaltJSを使えばいい話だが。

[2015年1月18日 追記] 以下の内容はTypeScript 1.4のリリースに伴い古くなりました。詳しくはこちら

ECMAScript 6で導入されるライブラリ関数は、一部は型宣言を書いてやることでTypeScriptからも使えるようになる。例えば、前の記事で Math.hypotMath.sinh などの関数に触れたが、それらは[sourcecode lang=”js”]
interface Math {
hypot(…values: number[]): number;
sinh(x: number): number;
}
[/sourcecode]のような宣言を書いておけば、コンパイルが通るようになる。まだこれらの関数を実装していないブラウザ用に、polyfill(shim)も書いておくか、読み込むといいだろう。

このほか、例えば、Array.prototype.find の型宣言は[sourcecode lang=”js”]
interface Array<T> {
find(callback: (element: T, index: number, array: T[]) => boolean, thisArg?: any): T;
}
[/sourcecode]というふうにできる。

ここまではいい。

JavaScriptのイディオムとして、配列ライクなオブジェクトを変換するのに、Array.prototype.slice が使われる。もちろんこのイディオムはTypeScriptでも使えるが、Array.prototype の型は Array<any> となっているので、要素の型に対する型チェックや型推論が働いてくれない。幸い、ECMAScript 6では、Array.from という関数が導入される予定なので、こいつの型を[sourcecode lang=”js”]
from<T>(arrayLike: {[n: number]: T; length: number}): T[];
[/sourcecode]のように宣言してやれば型推論とかが効いて便利なはずだ。

だがしかし。組み込みの Array オブジェクトの型は標準の lib.d.ts において[sourcecode lang=”js”]
declare var Array: {
new (arrayLength?: number): any[];

prototype: Array<any>;
}
[/sourcecode]のように宣言されている。こいつに from メソッドを追加しようとして自分のコードで[sourcecode lang=”js”]
declare var Array: {
from<T>(arrayLike: {[n: number]: T; length: number}): T[];
}
[/sourcecode]と書くとエラーが出る。既存のメソッドも書かないとダメかと思って[sourcecode lang=”js”]
declare var Array: {
new (arrayLength?: number): any[];

prototype: Array<any>;
from<T>(arrayLike: {[n: number]: T; length: number}): T[];
}
[/sourcecode]と書いてもエラーになる。モジュールならばどうかと思って[sourcecode lang=”js”]
module Array {
from<T>(arrayLike: {[n: number]: T; length: number}): T[];
}
[/sourcecode]と書いてもエラーになる。組み込みの Array オブジェクトの型は lib.d.ts で書かれたものから変更できないのだ。

だがちょっと待て。Math オブジェクトは自前で拡張できたではないか。これは何でだったかというと、Math オブジェクトは[sourcecode lang=”js”]
interface Math {

}
declare var Math: Math;
[/sourcecode]という風に定義されていて、Math インターフェースにメソッドを追加すれば Math オブジェクトを拡張できたのだ。Array も[sourcecode lang=”js”]
interface ArrayConstructor {
new (arrayLength?: number): any[];

prototype: Array<any>;
}
declare var Array: ArrayConstructor;
[/sourcecode]と定義されていれば良かったのに。Array だけではなくて、Object, Number, String 等の組み込みオブジェクトも同じ問題を抱えている。

ググってみたらすでに同じ問題で悩んでいる人がいた。

最初のStack Overflowの回答によると、「自前の lib.d.ts を用意しろ」らしい。つらい。

[2015年1月18日 追記] 以上の問題点はTypeScript 1.4のリリースにより解決しました。詳しくはこちら

滑らかな曲線をベジエ曲線で近似する

目次

ベジエ曲線とは

ベジエ曲線とはWikipedia(英語版)によると(本当はちゃんとした文献を当たるべきなのだろうが)、\(n+1\) 個の点 \(x_0, x_1, \dots, x_n\) が与えられた時に\[
B(t)=\sum_{i=0}^{n}\binom{n}{i}t^i(1-t)^{n-i}x_i, \quad 0\le t\le 1
\]で定まる曲線らしい。始点 (\(t=0\)) は \(x_0\)、終点(\(t=1\))は \(x_n\) である。\(n\) のことを次数という。

(1次の場合は単なる線分なので置いておいて)よく使われるのは2次の場合と3次の場合である。それぞれ\begin{align*}
\mathit{quadratic B\acute{e}zier}(t)&=(1-t)^2x_0+2t(1-t)x_1+t^2x_2, \\
\mathit{cubic B\acute{e}zier}(t)&=(1-t)^3x_0+3t(1-t)^2x_1+3t^2(1-t)x_2+t^3x_3
\end{align*}で与えられる。

2次の場合は始点 \(x_0\) と終点 \(x_2\) の他に1個の制御点 \(x_1\)、3次の場合は始点 \(x_0\)、終点 \(x_3\) の他に2個の制御点 \(x_1\), \(x_2\) によって決まる。制御点は始点及び終点における接線を与えるためにある。ここではベジエ曲線についてはこれ以上突っ込んだ事は取り扱わない。

こういう、「制御点を与えて曲線を描く」のは、ドロー系の描画ソフトウエアを使ったことのある方はおなじみだろう。SVGやPostScriptなどのベクター画像形式でも、ベジエ曲線は基本的な描画対象である。

プログラミングに関して言うと、大抵のグラフィックAPIには2次か3次のベジエ曲線を描画するAPIがある。例えば、HTML5 Canvasの場合

context.quadraticCurveTo(cpx, cpy, x, y) /* 2次 */
context.bezierCurveTo(cp1x, cp1y, cp2x, cp2y, x, y) /* 3次 */

というAPIがあり、Cocoaの場合は

NSBezierPath
-(void)curveToPoint:(NSPoint)aPoint controlPoint1:(NSPoint1) controlPoint2:(NSPoint)controlPoint2 /* 3次 */

というAPIがある。いずれも始点を指定する引数がないが、これらのAPIを使った時の始点は「現在の点の位置」になる。つまり、最後の描画操作における終点か、あるいはmoveToなどのAPIを使って指定した点である。

滑らかな曲線をベジエ曲線で近似する

さて、滑らかな曲線 \(f\colon[0,1]\to\mathbf{R}^2\) をベジエ曲線で近似するということを考えよう。動機としては例えば、プログラミングで曲線を描きたい時に、大抵のグラフィックスAPIには任意の曲線を描画するようなAPIはないので(2次か3次の)ベジエ曲線を使って近似する事になる。2次か3次と書いたが、以後3次のベジエ曲線で近似する事を考える。

続きを読む

ECMAScriptでのいくつかの数学関数の実装

C言語をはじめとする多くのプログラミング言語には、exp, log, sqrt などの指数、対数、平方根の関数や、 cos, sin, tan などの三角関数、cosh, sinh, tanh などの双曲線関数が備わっている。これらの数学関数はECMAScript (JavaScript)からは、Mathオブジェクト経由で Math.expMath.cos などのようにアクセスできる(が、現状ECMAScriptには双曲線関数はない)。

さて、C99でこれらに加えて、acosh, asinh, atanh などの逆双曲線関数や、expm1log1p などの「精度を意識した」関数などが追加された(expm1は\(\exp x-1\), log1p は \(\log(1+x)\) を計算する関数である)。これらの関数をECMAScriptで使うにはどうすればいいか?

ECMAScriptの次期標準であるECMAScript 6では、双曲線関数 Math.(cosh|sinh|tanh) や、C99で追加された関数に対応する Math.(acosh|asinh|atanh)Math.expm1, Math.log1p が入るらしい(Firefoxなどでは既に実装されている)。しかし、ECMAScript 6に非対応の環境では、これらの関数は自前で実装するしかない。

幸い、双曲線関数は指数関数で書ける。よって、例えば Math.sinh はECMAScriptに既に存在する Math.exp 関数を使って次のように書ける:

[sourcecode lang=”js”]
Math.sinh = Math.sinh || function(x) {
return (Math.exp(x)-Math.exp(-x))/2;
};
[/sourcecode]

Mozillaのサイトにも代替コード(Polyfill)として同じようなコードが載っている。めでたしめでたし。

といいたいところだが、精度を気にする場合はそうはいかない。例えば、\(x\) にとても小さい数、例えば \(x=10^{-20}\) を代入してみるとどうなるだろうか。\(\sinh\) のテーラー展開\[
\sinh x=x+\frac{x^3}{3!}+\cdots
\]を考えると(\(x^3\) は微小なので無視して)値はおおよそ \(x=10^{-20}\) と一致するはずである。この場合、ECMAScriptの「数」はIEEE754の64bit浮動小数点数で、精度は53bitしかないため、\(x\) が十分に小さければ \(x+\frac{x^3}{3!}+\dots\) は完全に \(x\) と一致する。

一方、指数関数のテーラー展開は\[
\exp x=1+x+\frac{x^2}{2!}+\cdots
\]で、今書いたのと同じ理由で Math.exp(x)Math.exp(-x) は完全に 1 と等しくなる。従って、さっき実装したオレオレ Math.sinh は0を返す。情報落ちだか桁落ちだか忘れたが、なんかそういう現象が起こっている。これは理想的とはいえない。ちなみに、C言語の sinh はこの場合「正しい」 \(10^{-20}\) を返す。

同様に、Math.expm1 を次のように愚直に実装しても、同じ問題が発生する。

[sourcecode lang=”js”]
Math.expm1 = Math.expm1 || function(x) {
return Math.exp(x)-1;
};
[/sourcecode]

では、どうすれば \(x\) が小さい時でも「正しい」答えを出す expm1 関数を作れるか?(双曲線関数よりも指数関数の方が単純なので、以後こちらを議論する)

まあ単純な答えとしては、 \(x\) が小さいときに関数のテイラー展開を使って多項式として計算してやれば良い。さっきのように \(x=10^{-20}\) とかだと1次近似で \(x\) そのものを返してやればよかったが、この近似は \(x\) がどのぐらい小さければ問題ないのか?あるいは、近似の次数をどのぐらい増やしてやれば誤差はどれぐらい小さくなるか?

仮に、\(\exp x\) を \(n\) 次の多項式で近似するとしよう。すると、真の値(無限級数で表される)との差は\[
\left\lvert(\text{差})\right\rvert=\left\lvert\exp x-1-\sum_{k=1}^{n}\frac{x^k}{k!}\right\rvert=\left\lvert\sum_{k=n+1}^{\infty}\frac{x^k}{k!}\right\rvert
\]となる。これを適当に評価してやれば良い。実際にやってみると、例えば次のようになる。\begin{align*}
\left\lvert(\text{差})\right\rvert=\left\lvert\sum_{k=n+1}^{\infty}\frac{x^k}{k!}\right\rvert
&\le\sum_{k=n+1}^{\infty}\frac{\lvert x\rvert^k}{k!} \\
&=\frac{\lvert x\rvert^{n+1}}{(n+1)!}\sum_{k=0}^{\infty}\frac{\lvert x\rvert^k}{(n+2)\cdot\dots\cdot(n+k+1)} \\
&\le\frac{\lvert x\rvert^{n+1}}{(n+1)!}\sum_{k=0}^{\infty}\frac{1}{(n+2)^k} \quad (\left\lvert x\right\rvert <1\text{を仮定}) \\
&\le\frac{\left\lvert x\right\rvert^{n+1}}{(n+1)!}\frac{1}{1-\frac{1}{n+2}} \\
&\le\frac{\left\lvert x\right\rvert^{n+1}}{(n+1)!}\frac{n+2}{n+1}=\frac{(n+2)\left\lvert x\right\rvert^{n+1}}{(n+1)(n+1)!}
\end{align*}
では、どういうときに \(n\) 次の多項式近似の値を使ってよいかというと、近似値 \(\sum_{k=1}^{n}\frac{x^k}{k!}\) の大きさに対してこの \(\left\lvert(\text{差})\right\rvert\) の大きさが(精度が53bitの浮動小数点数の場合は) \(2^{-53}\) よりも小さければ確実に問題ない(十分条件)。つまり\begin{align*}
\left\lvert\frac{(\text{差})}{\sum_{k=1}^{n}\frac{x^k}{k!}}\right\rvert<2^{-53}
\end{align*}だ。この左辺をもうちょっと分かりやすい形で評価すると
\begin{align*}
\left\lvert\frac{(\text{差})}{\sum_{k=1}^{n}\frac{x^k}{k!}}\right\rvert&\le\left\lvert\frac{(\text{差})}{x}\right\rvert \\
&=\left\lvert\frac{1}{x}\frac{(n+2)\left\lvert x\right\rvert^{n+1}}{(n+1)(n+1)!}\right\rvert \\
&=\frac{(n+2)\left\lvert x\right\rvert^n}{(n+1)(n+1)!}
\end{align*}
となる(書いた後に気付いたが、最初の行の評価が \(x<0\) のときにマズい気がする)。つまり、\(n\) 次近似を使っても良い十分条件として\[
\frac{(n+2)\left\lvert x\right\rvert^n}{(n+1)(n+1)!}<2^{-53},
\]すなわち\[
\left\lvert x\right\rvert<\sqrt[n]{\frac{(n+1)(n+1)!}{n+2}2^{-53}}
\]が得られる。

例えば、\(n=3\) として右辺を計算すると \(1.286976\ldots\times 10^{-5}\) が得られるので、さっきのオレオレ Math.expm1 の実装は

[sourcecode lang=”js”]
Math.expm1 = Math.expm1 || function(x) {
if (Math.abs(x) <= 1.28e-5) {
return x*(1+x/2*(1+x/3));
} else {
return Math.exp(x)-1;
}
};
[/sourcecode]

のように改良できる。

まあ、改良したと言っても所詮お遊びで、実際のC言語のライブラリの実装はこんな適当なコードよりもちゃんとやっているので、真面目にやりたい人はC言語のライブラリの実装を移植しよう。

Math.expm1 の他に、Math.log1p, Math.sinh, Math.tanh, Math.asinh, Math.atanh あたりの関数を実装する時にも同じような(小手先の)テクニックが使える。

ところで、MDNに載っている Math.tanh のPolyfillに問題があるのを見つけた。MDNのPolyfillでは xInfinity かどうかを関数の最初でチェックしているが、xInfinity でなくても Math.exp(x)Infinity になる場合を考慮していない。その結果、Math.tanh(x) に 1 を返してほしいのに実際には NaN が返ってくる場合がある。

最後に全く関係ない話だが、プログラミング言語Luaは標準ライブラリに math.sinh などの双曲線関数を計算する関数(中ではC言語のライブラリ関数を呼び出す)を持っている。しかし、どうやら将来的にはこれらの双曲線関数を標準ライブラリから外すようだ(次期バージョン5.3でdeprecated扱い)。理由として作者は「あまり使われていない」「必要なら mathx などの外部ライブラリを使えば良い」としている(この記事に書いた理由により、「math.exp で実装できる」は理由にならない)。ECMAScript と Lua はよく似ていると言われる事が多いが、一方がWebの世界のアセンブラとなるべく数学関数・浮動小数点数関係の関数を追加しようとしているのに対し、もう一方はそれを削減しようとしているのは対照的だと思った。(まあ筆者自身はLuaを活発に触っていたのは5.1時代の事で、5.2が出て以降はあまり触っていないので、ぶっちゃけどうでもいいのだが)

さくらのレンタルサーバーにGHC+Cabalを導入した

環境

  • さくらのレンタルサーバー スタンダード
  • FreeBSD 9.1-RELEASE-p15 (x86_64)
  • もちろんroot権限なし
  • ここでは、シェルはbashを使う(デフォルトはcshだった気がする)
  • ここでは、プレフィックスは $HOME/usr にする($HOME/usr/bin とか $HOME/usr/lib にファイルが入るということ)

1. GHCをインストールする

FreeBSD向けにはHaskell Platformは出ていない。しかしGHCのバイナリは配布されているので、ここからとってくる。この記事を書いている2014年7月6日の時点では、最新バージョンは7.8.2である。

$ curl -O http://www.haskell.org/ghc/dist/7.8.2/ghc-7.8.2-x86_64-portbld-freebsd.tar.xz
$ tar xf ghc-7.8.2-x86_64-portbld-freebsd.tar.xz
$ cd ghc-7.8.2
$ ./configure --prefix=$HOME/usr

この後に gmake install をするのだが、ghc-pkgやghcが使っている共有ライブラリにパスが通っていないので、 LD_LIBRARY_PATH を設定してやる。…なんかもっといい方法があると思う。

$ echo "export LD_LIBRARY_PATH=$HOME/usr/lib/ghc-7.8.2/terminfo-0.4.0.0:$HOME/usr/lib/ghc-7.8.2/bin-package-db-0.0.0.0:$HOME/usr/lib/ghc-7.8.2/binary-0.7.1.0:$HOME/usr/lib/ghc-7.8.2/Cabal-1.18.1.3:$HOME/usr/lib/ghc-7.8.2/process-1.2.0.0:$HOME/usr/lib/ghc-7.8.2/pretty-1.1.1.1:$HOME/usr/lib/ghc-7.8.2/directory-1.2.1.0:$HOME/usr/lib/ghc-7.8.2/unix-2.7.0.1:$HOME/usr/lib/ghc-7.8.2/time-1.4.2:$HOME/usr/lib/ghc-7.8.2/old-locale-1.0.0.6:$HOME/usr/lib/ghc-7.8.2/filepath-1.3.0.2:$HOME/usr/lib/ghc-7.8.2/containers-0.5.5.1:$HOME/usr/lib/ghc-7.8.2/bytestring-0.10.4.0:$HOME/usr/lib/ghc-7.8.2/deepseq-1.3.0.2:$HOME/usr/lib/ghc-7.8.2/deepseq-1.3.0.2:$HOME/usr/lib/ghc-7.8.2/array-0.5.0.0:$HOME/usr/lib/ghc-7.8.2/base-4.7.0.0:$HOME/usr/lib/ghc-7.8.2/integer-gmp-0.5.1.0:$HOME/usr/lib/ghc-7.8.2/ghc-prim-0.3.1.0:$HOME/usr/lib/ghc-7.8.2/rts-1.0:$HOME/usr/lib/ghc-7.8.2/haskeline-0.7.1.2:$HOME/usr/lib/ghc-7.8.2/ghc-7.8.2:$HOME/usr/lib/ghc-7.8.2/transformers-0.3.0.0:$HOME/usr/lib/ghc-7.8.2/template-haskell-2.9.0.0:$HOME/usr/lib/ghc-7.8.2/hpc-0.6.0.1:$HOME/usr/lib/ghc-7.8.2/hoopl-3.10.0.1" > ~/ghc-ld-path.sh
$ source ~/ghc-ld-path.sh
$ gmake install

2. Cabalをインストールする

このへんからCabalのソースコードを落としてくる。

$ curl -O http://www.haskell.org/cabal/release/cabal-install-1.20.0.2/cabal-install-1.20.0.2.tar.gz
$ tar xf cabal-install-1.20.0.2.tar.gz
$ cd cabal-install-1.20.0.2
$ emacs bootstrap.sh

本来なら cabal-install-* の中にある bootstrap.sh を実行すればいいのだが、sedの仕様の違いかなんだか知らないがリンカのコマンドがおかしなことになるので、テキストエディタで bootstrap.sh を編集してリンカを ld に決め打ちしてやる。

LINK=/usr/bin/ld

また、そのままだと tar が /dev/sr0 だかなんだかにアクセスして死ぬので、ググって出てきた情報を元に tar の代わりに tar -f - を使うようにする。これは bootstrap.sh を書き換えなくても環境変数で上書きできる。

あと、Haddockでドキュメントを生成するのがうまくいかなさそうな気配を感じたので、 --no-docをつけてドキュメントを生成しないようにする。

$ TAR="tar -f -" ./bootstrap.sh --no-doc

これでインストールされるはず。

環境変数 PATH がcabalとかを見に行くように、.bash_profile をいじってやる。

$ emacs ~/.bash_profile
export PATH=$HOME/.cabal/bin:$HOME/usr/bin:$PATH

あとは普通にcabalが使える。

$ cabal update
$ cabal install cabal-install

3. せっかくなのでCabalでいろいろインストールしてみる

なんとなくIdrisを入れてみよう!と思った。依存関係がよくわからないが、コマンドとしては

$ cabal install --upgrade-dependencies --force-reinstalls idris

ぐらいでいけるはず。…だが現実はそううまくはいかない。

遭遇した問題としては大きく分けて二つあって、テンポラリディレクトリ /var/tmp 以下で作業してるのがなぜか実行権限が与えられなくてconfigureとかでこけるのと、ソースコード中に非US-ASCII文字が入っていてこけるの。

前者は、テンポラリディレクトリを自前で用意したディレクトリに変えれば良い。つまり ~/tmp 的なディレクトリを作ってやって、環境変数 TMPDIR=~/tmp とすればよい。

後者は、 hGetContents が失敗する的なエラーが出る。

hGetContents: invalid argument (invalid byte sequence)

file コマンドで問題のファイルを見るとUS-ASCIIではなくUTF-8になっているのが分かる。そこで、問題のファイルから非US-ASCII文字を探し出してやって、それをUS-ASCII文字で置き換えてやればファイルがUS-ASCIIになって hGetContents で問題なく読み込める…という方法でビルドしたが、冷静に考えてHaskellはUnicode対応してるはずだし hGetContents でUTF-8を読み込めないのがおかしい。終わった後に気づいたが、おそらく文字エンコーディングが設定されていない的な問題な気がするので、 LANG=en_US.UTF-8 あたりを指定すれば良かった。

結局、

$ mkdir ~/tmp
$ TMPDIR=~/tmp LANG=en_US.UTF-8 cabal install --upgrade-dependencies --force-reinstalls idris

とすれば深いこと考えずにビルドできるはず。

以前やった時はどこかで挫折してしまっていたが、今回は気合いでなんとか頑張った。普段OS X と (Arch) Linux ばかり触っていて、 FreeBSD はよくわからないのだが、まあなんとかなった。

あとはレンタルサーバーの環境にnode.jsが入れば楽しそうなのだが…。

共用サーバーに処理系をいろいろ入れていろいろやりたいというのが間違いで、そういうのがしたいならVPSでも契約しろというのは正論だろう。

Five LemmaのダイアグラムチェースをするWebページを作った

最近、Webの標準技術であるSVGとMathMLを組み合わせて、Webページ上で数学の図式などを表現できないかと考えている。

このブログでもたまに図式や証明図を載せているが、今までのは画像として貼り付ける形だった。静的なコンテンツならこれでもいいのだが、JavaScriptを使ってインタラクティブなコンテンツを作ろうとした時に、画像では動的に内容を変えるというようなことがやりにくい。そこで考えられるのが、Web標準技術のSVGやMathMLといった、HTMLやJavaScriptと相性のいい技術を使って数学の図式を記述するということである。

SVGは基本的に図を記述する言語で、MathMLは数式を記述する言語だが、ブラウザが対応していれば、SVGの図の中にMathMLを埋め込むことは難しくない。だが、数式の幅、高さを見ながら図のレイアウトを決めてやるのは正直楽しい作業ではない。JavaScriptを使えば、ブラウザがレンダリングした数式の大きさを見て適切に位置を合わせるということができるだろう。また、JavaScriptを使えば、ユーザーのクリックに反応して数式を変えたり、色を変えたりできるだろう。

SVGは最近のブラウザならだいたい対応しているが、MathMLのブラウザ側の対応はまちまちである。Firefoxはかなり昔からMathMLに対応していた。Safariは最近対応したようだが、筆者はあまり触っていない。Chromeは、数年前に見聞きした話では対応する意思がないらしい。

という感じで、とりあえず作る時はFirefoxで表示させることを優先させる。Safariは余力があれば対応させたい。Chromeは知らん。

というわけで、そういうのを実験的に実装してみた。このページは、みなさんお世話になっているであろう圏論的な直積の図式を表現している。

直積の図式を表示てきたはいいものの、これは動きがない。ユーザーの操作によって表示が変わるようなものを作ろう。というわけで、Five Lemmaのダイアグラムチェースによる証明(真ん中の射がmonicであることを示す)をするページを作った。クリックするとダイアグラムチェースが進む。かなりやっつけな書き方をしているので、例えばAndroid上のFirefoxでは表示が崩れた。Safariでは文字が途切れる。JavaScriptのソースコードもかなり汚い。改善の余地は大きいだろう。

演算子オーバーロードのないJavaScriptであまり複雑なことをしても記述性が悪い。例えばHaskellのような言語で記述してJavaScriptにコンパイルするという手順を取ると良いのかもしれない。

distccとclangを使って異なる環境のマシンで分散コンパイルする

distccという、ネットワーク越しに複数のマシンを使って分散コンパイルを行うツールがある。これを使うと、最低限の設定で、同じアーキテクチャ・OSのマシン複数台での分散コンパイルができる。だが、アーキテクチャ・OSの異なるマシンを使いたい場合はどうか。その場合はクロスコンパイラを使う必要がある。

しかし、全てのマシンにクロスコンパイラを導入するのは面倒である。特に、ビルドしたいターゲットの環境のGCCがパッケージ管理システムに登録されていない場合は、わざわざ自前でGCCをビルドしなければならない。これはできればやりたくない。

そういう時は、コンパイラとしてclangを使おう。最近のclangは、-targetオプションを指定することでクロスコンパイラとして使うことができる(昔は-ccc-host-tripleだった)。clangは大抵の環境でパッケージとして用意されていると思うので、容易に導入できるだろう。-targetオプションに指定する文字列は、$ clang --versionで出てくる文字列を使えば良いだろう。

例えば、必ずしもMacばかりではないマシンを使って、Mac向けのプログラムをビルドしたい場合、configureには次のようなオプションを与えれば良い:

$ ./configure CC="distcc clang -target x86_64-apple-darwin13.1.0" CXX="distcc clang++ -target x86_64-apple-darwin13.1.0"

ただし、DISTCC_HOSTSなどの環境変数は適切に設定されており、ビルドに使うマシンではdistccdが動いているものとする。あとは$ make -j10のように適当に並列ビルドのオプションを指定すれば、適当に分散コンパイルしてくれる。

distccにはプリプロセッサの処理も分散させるpump modeという動作モードがあるが、どうも-targetオプションには対応していないようで、うまく動いてくれなかった。

Idrisで遊んでみた (2) — 自然数に関する命題の証明

前回は等号の証明に使える公理や規則(Idrisの組み込み関数)をいくつか紹介した。

これに加え、Idrisの標準ライブラリには自然数の性質に関する補題(?)がいくつか用意されている。そのうち、後で使う2つを紹介する。

一つ目は、和と後続者に関するものである。ペアノ算術にはちょうどこのような公理があったはずだ。plusSuccRightSucc

もう一つは、和の可換性である。ペアノ算術ではこれを証明するためには帰納法を使うが、証明(関数の実装)は標準ライブラリで用意されているので、ここではそれを使うだけにとどめておく。plusCommutative

さて、前回証明したいと言っていた命題は\[x=y+\mathtt{difference}\ p\]であった。ただし、\(p\) の表す命題は \(y\le x\), Idrisの型で言うと LTE y x である。この等式を証明するには、
[sourcecode lang=”plain”]
differenceP : {x:Nat} -> {y:Nat} -> (p : LTE y x) -> (x = y + difference p)
[/sourcecode]
という型の関数を実装すれば良い。

例によって場合分けする。

  • \(y=0\), つまり p=lteZero の場合:
    • この等式は自明に成り立つ。refl を返せば良い。
  • それ以外、つまり \(x=Sx’\), \(y=Sy’\), p=lteSucc p' の場合:
    • 帰納法の仮定として differenceP p' : x' = y' + difference p' が使える。
    • この仮定を使って S x' = (S y') + difference p' を示せば良い。(difference の定義を見れば difference p = difference p' なので、S x' = (S y') + difference p は自動的に導いてくれるようだ)
    • この仮定と、先に紹介した公理、補題を使って、自然演繹っぽい証明図を書くと、prooftree1となる。
    • この証明図にIdrisの項を書き加えるとprooftree1-tとなる。ただし、一部をアンダースコアで省略している。

これらをまとめて、Idrisの式として書けば
[sourcecode lang=”plain”]
differenceP : {x:Nat} -> {y:Nat} -> (p : LTE y x) -> (x = y + difference p)
differenceP lteZero = refl
differenceP {x = S x’} {y = S y’} (lteSucc p’) = trans (trans (cong {f=S} (trans (differenceP p’) (plusCommutative _ _))) (plusSuccRightSucc _ _)) (plusCommutative _ (S y’))
[/sourcecode]
となる。一部の式をアンダースコアで省略しているが、最後の (S y') まで省略してしまうと処理系に怒られたので、そこは明示的に書いている。

今回は、自然演繹の証明図をCurry-Howard対応で翻訳することによって、命題を証明(関数を実装)した。等式の変形のところがやや煩雑になっているが、それはもとの自然演繹の証明図がそういうことになっていたことに起因するもので、Curry-Howard対応のせいでどうこうというものではない。

次回は量化子を含む命題を証明する予定である。Tacticを使った証明は筆者が不勉強なのでまだ扱わない。

Idrisで遊んでみた (1)

前回はIdrisで2つの自然数を比較し、結果とその証明を返す関数 compareNats を作った。今回は、それに追加していくつかの関数を実装してみる。

まず、二つの自然数 \(x\) と \(y\) の差、\(x-y\) を計算する関数 difference を作る。\(y\le x\) の場合は良いが、\(x\lt y\) の場合はどうするか考えどころである。0を返すようにしてもよいが、ここは「\(y\le x\) であることの証拠を要求する」ことにして、\(x\lt y\) の場合は考える必要がない、という仕様にする。型を書けば
[sourcecode lang=”plain”]
difference : (x:Nat) -> (y:Nat) -> LTE y x -> Nat
[/sourcecode]
となる。前回書いたように、LTE y x は命題 \(y\le x\) に対応する型である。

実装には、例によって引数によるパターンマッチをする。

  • \(y=0\) の場合
    • \(x\) を返す。第三引数は lteZero である。
    • コードで書けば difference x 0 lteZero = x となる。
  • \(x=Sx’, \>y=Sy’\) の場合
    • 第3引数は lteSucc p の形をしている。
    • difference x' y' p によって \(x’-y’\) を計算できる。\(x-y=x’-y’\) なので、それをそのまま返せば良い。
    • コードで書けば difference (S x') (S y') (lteSucc p) = difference x' y' p となる。

まとめると
[sourcecode lang=”plain”]
difference : (x:Nat) -> (y:Nat) -> LTE y x -> Nat
difference x 0 lteZero = x
difference (S x’) (S y’) (lteSucc p) = difference x’ y’ p
[/sourcecode]
となる。

さて、よく考えてみると、第1引数 x と第2引数 y の情報は第3引数の型を見れば自動的に得られる。したがって、第1引数と第2引数は省略できるのではないか?

Idrisにはimplicit argumentsという機能があるので、この場合実際に xy を省略できる。Implicit argumentsを使うと、difference は次のように書ける:
[sourcecode lang=”plain”]
difference : {x:Nat} -> {y:Nat} -> LTE y x -> Nat
difference {x} lteZero = x
difference (lteSucc p) = difference p
[/sourcecode]

この difference という関数は、\(y \le x\) を満たす任意の自然数 \(x\), \(y\) および \(y \le x\) の「証拠」p : LTE y x に対して、\[x = y + \mathtt{difference}\>p\]という関係を満たす。この関係式を「証明」するにはどうすればよいだろうか?

その前に、述語論理における等号の公理と、それがIdrisではどうなっているか見ておこう。自然演繹チックに書けば、述語論理の等号の公理と関連する推論規則は

  • 等号公理(反射律)equality
  • 等号規則equality2
  • 等号規則(派生)equality2b
  • 推移律equality3
  • 対称律equality4

などがある。あとの三つは最初の二つから出るので、本質的というわけではない。それぞれにIdrisの式を対応させていくと、

  • 等号公理(反射律)equality-t
  • 等号規則equality2-t
  • 等号規則(派生)equality2b-t
  • 推移律equality3-t
  • 対称律equality4-t

となる。つまり、refl, replace, cong, trans, sym という関数があって、それぞれ適切な型を持っている。

以後、命題の左に項を書いていくと上下で重複が多くなって大変なので、以後

  • 等号公理(反射律)equality-u
  • 等号規則equality2-u
  • 等号規則(派生)equality2b-u
  • 推移律equality3-u
  • 対称律equality4-u

のように、使った規則を横棒の右に書くことにする。

長くなるので、一旦記事を分割することにする。今回はここまで。

2月28日:「等号規則(派生)」を追加。

Idrisで遊んでみた (0)

依存型のあるプログラミング言語に慣れてみたいと思ってIdrisで遊んでみた。

依存型とは何かと言うと、普通の型付きラムダ計算はCurry-Howard対応によって直観主義命題論理に対応するが、依存型のあるラムダ計算は直観主義述語論理に対応する(という認識でいる)。

Curry-Howard対応によれば「型」は「命題」に対応する。そして、対応する論理は述語論理なので、「\(x=y\)」や「\(x\le 3\)」のような、項を含む命題(型)を扱うことができる。Integer型やString型をもつ値はまあ分かるが、\(x=y\) や \(x\le 3\) という型をもつ値は一体何を表しているのかと思われるかもしれない。まあ「その命題が成り立つことの証拠、あるいは証明」だと考えればいいだろう。たぶん。

なんでIdrisをやろうかと思ったかというと、文法がHaskellに似ていて取っつきやすそうだったからである。ただ、まだまだ発展途上で実用するには向かなさそうだ。まとまったリファレンスマニュアルみたいなものは見つけられなかったので、標準ライブラリの細かいところはソースコードを参照した。また、この記事のコードはVersion 0.9.11.2に向けて書いてある。

今回はIdrisで自然数(Nat 型)を扱ってみる。最初の自然数0に対応するものは Z : Nat である。ただし、型クラスがいい感じに定義されているので0と書いても良い。自然数 x の後続者(successor)は S x である。さて、さっき命題の例として \(x\le 3\) と書いたが、Idrisには LTE : Nat -> Nat -> Type というデータ構築子があって、自然数についての \(x\le 3\) という命題は LTE x 3 という型に対応する。LT : Nat -> Nat -> Type というものもあるが、これは LT x y = LTE (S x) y と定義されている。それぞれ、”Less Than or Equal to,” “Less Than” の略だと思われる。携帯電話の通信規格とは関係ない。

簡単な例として、二つの自然数を比較する関数を書いてみよう。普通の言語なら compareNats : Nat -> Nat -> Bool とでもするところだが、さっき書いたように「型は命題に対応」し、「値は証明、あるいは証拠を表す」と考えられるので、どうせなら「大きい方はどちらか、およびその証拠」を返す関数を作ってみよう。この関数の型は
[sourcecode lang=”plain”]
compareNats : (x : Nat) -> (y : Nat) -> Either (LT x y) (LTE y x)
[/sourcecode]
とする。この結果の Either (LT x y) (LTE y x) という型は、数学っぽく書けば \((x<y)\vee(y\le x)\) に相当する。

LTE x y型の値を作る(\(x\le y\) を証明する)には、2通りの関数(公理)がある。つまり、

  • lteZero : LTE Z y、つまり \(0\le y\)
  • lteSucc : LTE x y -> LTE (S x) (S y)、つまり \(x \le y \rightarrow Sx \le Sy\)

だ。compareNats の実装では xy の値によって場合分けして、これらの関数を使って「証拠」を作ってやれば良い。

  • \(y=0\) の場合:
    • \((x<y)\vee(y\le x)\) のうち \(y \le x\) が成り立つ。LTE y x 型の値を返したいが、\(y=0\) なので lteZero が欲しい型を持つ値である。
    • したがって、Eitherのデータ構築子(\(\vee\) の導入則)と組み合わせて、Right lteZeroを返せば良い。
  • \(x=0, y=S y’\) の場合:
    • \((x<y)\vee(y\le x)\) のうち \(x<y\) が成り立つ。したがって、LT x y 型、つまり LTE (S Z) (S y') 型の値を返したい。
    • LTE Z y' 型の値であれば lteZero で得られた。これを lteSucc に食わせて lteSucc lteZero とすれば LTE (S Z) (S y') 型の値が得られる。
    • したがって、Eitherのデータ構築子(\(\vee\) の導入則)と組み合わせて、Left (lteSucc lteZero)を返せば良い。
  • \(x=Sx’,y=Sy’\) の場合:
    • まず \(x’\) と \(y’\) を比較する。比較には compareNats x' y' が使える。
    • compareNats x' y'Left p を返してきた場合:
      • p は \(x’ < y’\) の「証拠」である。これの両辺の後続者をとれば(両辺に1加えれば)、\(Sx'<Sy’\) の「証拠」、つまり \(x<y\) の「証拠」になる。
      • つまり lteSucc p が \(x<y\) の「証拠」である。\((x<y)\vee(y\le x)\) のうち成り立つのは \(x<y\) の方なので、Left (lteSucc p) を返せば良い。
    • compareNats x' y'Right q を返してきた場合:
      • q は \(y’ \le x’\) の「証拠」である。これの両辺の後続者をとれば(両辺に1加えれば)、\(Sy’\le Sx’\) の「証拠」、つまり \(y\le x\) の「証拠」になる。
      • つまり lteSucc q が \(y\le x\) の「証拠」である。\((x<y)\vee(y\le x)\) のうち成り立つのは \(y\le x\) の方なので、Right (lteSucc q) を返せば良い。

以上をまとめると次のようなコードになる:
[sourcecode lang=”plain”]
compareNats : (x : Nat) -> (y : Nat) -> Either (LT x y) (LTE y x)
compareNats x Z = Right lteZero
compareNats Z (S y’) = Left (lteSucc lteZero)
compareNats (S x’) (S y’) = case compareNats x’ y’ of
Left p => Left (lteSucc p)
Right q => Right (lteSucc q)
[/sourcecode]
あるいは、either : (a -> c) -> (b -> c) -> (Either a b) -> c 関数を使えば次のようにも書ける:
[sourcecode lang=”plain”]
compareNats : (x : Nat) -> (y : Nat) -> Either (LT x y) (LTE y x)
compareNats x Z = Right lteZero
compareNats Z (S y’) = Left (lteSucc lteZero)
compareNats (S x’) (S y’) = either (Left . lteSucc) (Right . lteSucc) (compareNats x’ y’)
[/sourcecode]

今回はここまで。

なお、今回の記事では

  • Curry-Howard対応
  • Haskell(またはそれに類した言語)
  • ペアノ算術

あたりの知識を仮定した。初心者向けではなく、自分のための備忘録的な感じで書いた。