msys2 上で ocaml をビルドしようとして失敗した記録

■真新しいmsys2上でomakeを使いたくなったが、周知の通り現在はWindows用のバイナリが配布されていない。
msys2上のocamlでomakeをビルドしようとしたが上手く行かない。そこで、msys2上でocamlをビルドしてみればいいのではないかというアホなことを考えて失敗した記録。

■準備。本当に必要かどうかはわからない。

$ pacman -S gamin #fam みたいなもの
$ pacman -S bison #yacc みたいなもの
$ pacman -S gcc git patch

■ocamlをビルドする

#ocaml を msys2 上でビルドする。
$ git clone https://github.com/ocaml/ocaml
$ cd ocaml
$ ./configure -host x86_64-w64-windows -cc "gcc -Wno-error=implicit-function-declaration -Wno-error=int-conversion -Wl,--stack,16777216"
$ make clean
$ make world
$ make install

ln: シンボリックリンク 'ocamlyacc' の作成に失敗しました: No such file or directory
make: *** [Makefile:606: install] エラー 1

■msys2でsymlinkを使う方法:msys2_shell.cmd をテキストエディタで編集し

rem To activate windows native symlinks uncomment next line
rem set MSYS=winsymlinks:nativestrict

となっているところを

rem To activate windows native symlinks uncomment next line
set MSYS=winsymlinks:nativestrict

に変更して保存する。そして、msys2_shell.cmd を右クリックして「管理者として実行」してmsys2のシェルを立ち上げる。

■手持ちの別のマシンでやったところ ocamlyacc のエラーは出なかったが omake のビルドで

$ ocaml configure.ml
Cannot load required shared library dllcamlstr.
Reason: dllcamlstr.so: dynamic loading not supported on this platform.
Cannot load required shared library dllunix.
Reason: dllunix.so: dynamic loading not supported on this platform.
File "./configure.ml", line 1:
Error: Reference to undefined global `Str'

となって止まってしまった。

広告

Haskell の QuickCheck を自動化する

ライブラリを開発していると、複数のテストを一挙に回したくなるかもしれませんね。そんなときはこうします。

{-# LANGUAGE TemplateHaskell #-}

import Data.List
import Test.QuickCheck

-- 与えられた2つのリストを連結する
cat :: (Eq a) => [a] -> [a] -> [a]
cat [] ys = ys
cat (x:xs) ys = x : (xs `cat` ys)

-- cat が結合律を満たすかどうかのテスト
prop_cat xs ys zs = (xs `cat` ys) `cat` zs == xs `cat` (ys `cat` zs)

-- 最初のリストから二番目のリストの要素を除去したリストを作る
sub :: (Eq a) => [a] -> [a] -> [a]
sub [] ys = []
sub (x:xs) ys | x `elem` ys = xs `sub` ys
| otherwise = x : (xs `sub` ys)

-- sub が結合律を満たすかどうかのテスト
prop_sub xs ys zs = (xs `sub` ys) `sub` zs == xs `sub` (ys `sub` zs)
--to run this test, > quickCheck prop_cap

--最初のリストに含まれている要素を除外しつつ2つの与えられたリストをマージする
ucat :: (Eq a) => [a] -> [a] -> [a]
ucat [] ys = ys
ucat (x:xs) ys | x `elem` ys = x : (xs `ucat` (ys `sub` [x]))
| otherwise = x : (xs `ucat` ys)

-- ucat が結合律を満たすかどうかのテスト
prop_ucat xs ys zs = (xs `ucat` ys) `ucat` zs == xs `ucat` (ys `ucat` zs)

return []
main = $forAllProperties (quickCheckWithResult stdArgs { maxSuccess = 2000 })

■動かし方/その出力例

$ stack runghc qc.hs
Run from outside a project, using implicit global project config
=== prop_cat from qc.hs:12 ===
+++ OK, passed 2000 tests.

=== prop_sub from qc.hs:20 ===
*** Failed! Falsifiable (after 9 tests and 7 shrinks):
[0]
[]
[0]

=== prop_ucat from qc.hs:29 ===
+++ OK, passed 2000 tests.

■コードの解説
cat, sub, ucat というリスト演算を定義し、それらが結合法則を満たすかどうかチェックしています。テストの結果、cat は合格、subは失格(つまり結合法則の反例が見つかった)、ucatは合格となりました。

■ポイント
1. TemplateHaskell を使う。
2. テストの名前は prop_ で始まる。 (TemplateHaskellを使っていることからの制約)
3. return[] とかいうキモいやつは我慢。 (TemplateHaskellを使っていることからの制約)
4. main は一番最後に来る。 (TemplateHaskellを使っていることからの制約)

QuickCheckで100回以上テストを回す(メモ)

HaskellにはQuickCheckという便利なライブラリがあります。これは、自分で作った関数が特定の性質を満たしているかどうか手早くテストするときに役に立ちます。

たとえば、あなたが(多分自分の勉強のために)2つのリストを結合する関数myconcatを次のように書いたとしましょう:

import Test.QuickCheck
-- $ stack install QuickCheck

myconcat :: (Eq a) => [a] -> [a] -> [a]
myconcat [] ys = ys
myconcat (x:xs) ys = x : (xs `myconcat` ys)

実際これは多くのHaskell教科書に(++)の参照実装として挙げられているものをそのまま真似ただけですから、当然

(xs `myconcat` ys) `myconcat` zs == xs `myconcat` (ys `myconcat` zs)

という性質は「常に」成り立つと期待したいところです。このような事を保証するためには、結局なんらかの証明を与える必要があります。
例えば Richard Bird 著/山下伸夫 訳『関数プログラミング入門 — Haskellで学ぶ原理と技法』では、そのような証明を「手で」つける例が随所で扱われています。あるいは、Coqのような言語を使って、成り立っていることが期待される性質が実際に成り立つことの形式的な証明を与えるという手段もあります。

いずれにせよ、何かのしっかりとした証明をつけるというのはなかなか面倒なことではあります。そこで、乱数で生成した例で手っ取り早くテストしたいという場合があります。特に、「期待される性質」が実際に成り立っていないかもしれないという疑念があるときにはこのような検査は有効です。間違った命題—その命題が本当に間違っているかどうかを事前に知ることができない場合が多いことが厄介なわけですが—を証明しようとあれこれ悩みたくないですからね。

今の場合ならソースコードの末尾にこんな関数を付け加えておけば良いです:

mytest xs ys zs = (xs `myconcat` ys) `myconcat` zs == xs `myconcat` (ys `myconcat` zs)

そしてghciから

*Main> quickCheck mytest
+++ OK, passed 100 tests.

と試せば良いわけです。

ところで、100回以上テストしたい場合はどうすればいいのでしょうか? ここ(stackoverflow)で答を見つけました。答から先に書くと、たとえば5000回テストしたい場合には

*Main>quickCheckWith stdArgs { maxSuccess = 5000 } mytest

とすればいいです。

引用した stackoverflow のあるコメントの後半に「どうやってこの答をみつけたか」の丁寧な解説があったので補足しつつ翻訳します。

1.API documentation を見に行く

API documentation のページはこんなふうなリンクから飛べる

2. quickCheck を見てその次に見たのは maxSuccess フィールドを持つ Args 型だった。

Args型

3. 全部のフィールドを書くのは嫌だったので、Args 型の値を探したら stdArgs が見つかった。(ブラウザの検索機能 Ctrl+F を使いましょう)。または、hoogle を使っても良かったかもしれない。

4. 自分の Args 型変数を使いたいので検索を続行した。次の行に quickCheckWith があった—これだ! または、hoogleを使うという手もあった。

img3

「使ったことがないライブラリをどう使うか」というのは非常に重要です。上に書いてあることはHoogleを使い慣れている人が当たり前にやっていることでしょうが、きちんと段階化し言語化してあるところが素晴らしいと思って訳してしまいました。

更に補足すると、stdArgs { maxSuccess = 5000 }の箇所は、stdArgsが返すArgs型の値の maxSuccessフィールドを 5000 に書き換えた値を生成しているのでした。

ココナツの問題をC++で解く

■前回の記事「Maybeの(>=>)を使って問題を解く」ではHaskellでココナツ問題を解いてみたが、もし使える言語がC++しかなかったらどうするか考えてみた。Haskellでは失敗する可能性のある関数を「合成」することができたが、C++にはそのような機能がないのでif文で分岐することになる。

#include <iostream>
#include <utility>

#define MAX 100000

using namespace std;

pair<bool,int>  g(int n, int r)
{
  pair<bool,int> retval = make_pair(false,0);
  if(0 == (n-r) % 5){
    const int x = 4*((n-r)/5);
    retval = make_pair(true,x);
  }
  return retval;
}

typedef pair<bool,int> mint;

bool check_num(int n)
{
  //1,1,1,1,1,0
  const mint n1 = g(n,1);
  if(n1.first){
    const mint n2 = g(n1.second,1);
    if(n2.first){
      const mint n3 = g(n2.second,1);
      if(n3.first){
        const mint n4 = g(n3.second,1);
        if(n4.first){
          const mint n5 = g(n4.second,1);
          if(n5.first){
            const mint nfin = g(n5.second,0);
            if(nfin.first){
              return true;
            }
          }
        }
      }
    }
  }
  return false;
}

int get_ans(){
  for(int n = 0; n < MAX; ++n){
    if(check_num(n)){
      return n;
    }
  }

  return -1;
}

int main()
{
  const int n = get_ans();
  cout << n << endl;
  return 0;
}

関数check_numをもう少し読みやすく出来ないかと考えてみたが、良い考えを思いつかなかった。

昔の自分なら、マクロを使って

bool check_num(int n)
{
  //1,1,1,1,1,0
  const mint n1 = g(n,1);

  #define MY_MACRO(X,Y,R)   g(X.second,R);if(! Y.first){return false;}

  const mint n2 = MY_MACRO(n1,n2,1);
  const mint n3 = MY_MACRO(n2,n3,1);
  const mint n4 = MY_MACRO(n3,n4,1);
  const mint n5 = MY_MACRO(n4,n5,1);
  const mint nfin = MY_MACRO(n5,nfin,0);

  return true;
}

のように書いたかもしれないが、疲れているときにこのようなコードを書くことの恐ろしさを何度か経験したのであまり乗り気にはなれない。

■結論は特にない。(HaskellがすごいとかC++がダメだと主張したいわけではない)。

Maybeの(>=>)を使って問題を解く

■マーティン・ガードナーのパズル本を見ていたらこんな問題が載っていた:

5人の男と一匹の猿が難破して無人島に漂着した。1日目、彼らは食糧としてたくさんのココナツを集めて回った。そしてその夜、すべてのココナツを積み上げて彼らは眠りについた。
 しかし全員が眠りについたあと、1人の男がふと目を覚ました。朝になってココナツを分けるとき、ひと悶着起きるかもしれないではないか。心配になった彼は自分の取り分を先取りしようと考えた。彼がココナツを5つの山に等分してみると、1つ余ったので、彼はそれを猿にあげてから、自分の取り分を隠して、残りを元通りに積んでおいた。
 しばらくして別の男が目を覚まして、同じことを考えた。やはりココナツは1つ余り、それは猿のものになった。こうして5人の男たちが順番に同じことをした。つまり1人ずつ目を覚ましては、ココナツの山を5つに分けて、残った1つを猿にあげて、自分の取り分を画した。朝になり、残ったココナツ全部を分けると、今度はきれいに5等分された。
(略) さて、最初にココナツはいくつあったのだろうか?

計算機で総当りしてももちろんこの問題は解ける。本には、これを少ない労力で解くためのトリックが紹介されていた。(「ガードナーの数学娯楽」/日本評論社)。そのトリックについてはこの記事では触れない。

この問題を見たとき、HaskellのMaybeモナドを使ったら素直に解けそうだと感じた。(そして実際に解けた)。ココナツの数をNとすると
N = 5A +1 ;  4A個の山を残す # 1人目の男
4A = 5B + 1 ; 4B個の山を残す # 2人目の男
4B = 5C + 1 ; 4C個の山を残す # 3人目の男
4C = 5D + 1 ; 4D個の山を残す # 4人目の男
4D = 5E +1 ; 4E個の山を残す # 5人目の男
4E = 5F ; きれいに5等分された
のようになる。「与えられた数から1を引いておけば5で割り切れる」という状況が続き、そうして得られた商の4倍だけ残すという操作が5回行われている。そこでこんな関数を考えてみよう:

g :: Int -> Int -> Maybe Int
g r n
    |  (n-r) `rem` 5 == 0  = Just( ((n-r) `quot` 5) * 4 )
    |  otherwise           = Nothing

こうすると、それぞれの男が行った操作は g 1 として表現できる:

g 1 :: Int -> Maybe Int

一般に、モナドMに対して X -> M Yの形の関数は、(>=>)で合成できるのだった。
(この記事では説明しないし、知っている必要もないが、この形の関数はこのモナドの与えるKleisli圏の射とみなす事ができ、(>=>)はこのタイプの射の「合成」とみなせるのだった)。

よって、5人の男がココナツに対して行った操作とその結果は

f :: Int -> Maybe Int
f = g 1 {- 1人目の男 -} >=> g 1{- 2人目の男 -} >=> g 1{- 3人目の男 -} >=> g 1{- 4人目の男 -} >=> g 1{- 5人目の男 -} >=> g 0

として表せる。もちろんこれはもっとコンパクトに

f = foldl1 (>=>) [g 1, g 1, g 1, g 1, g 1, g 0]

と書いてもいいし、さらにこれは

f = foldl1 (>=>) $ map g [1,1,1,1,1,0]

と書いてもいい。こうして得られたfInt -> Maybe Int という型シグネチャを持つ。元のクイズの答をNとするとき、 f N Just ...という形をしているはずである。そこで、こんな関数を用意してみよう:

--  f の答がNothing ではない場合の引数を得るように変形する
getJustArg :: (a -> Maybe b) -> (a -> Maybe a)
getJustArg f x
    | isJust (f x)  = Just x
    | otherwise     = Nothing

この関数を使えば、問題のNは map (getJustArg f) [1 ..] の最初の元から得られることがわかる。Data.List の

find :: (a -> Bool) -> [a] -> Maybe a

を使えば最初の元を取ってこられそうだ。findMaybeをかぶせて返してくるおかげで、
find isJust (map (getJustArg f) [1 ..])Maybe(Maybe Int) 値になる。そこで join してMaybe を一段に落としてやると、得られる答は Just n の形をしているので fromJustInt値を引っ張り出せる:

fromJust . join $ find isJust (map (getJustArg f) [1 ..])

以上をまとめると次のようなプログラムが得られる:

import Control.Monad
import Data.List
import Data.Maybe

g :: Int -> Int -> Maybe Int
g r n
    |  (n-r) `rem` 5 == 0  = Just( ((n-r) `quot` 5) * 4 )
    |  otherwise           = Nothing

f = foldl1 (>=>) $ map g [1,1,1,1,1,0]

getJustArg :: (a -> Maybe b) -> (a -> Maybe a)
getJustArg f x
    | isJust (f x)  = Just x
    | otherwise     = Nothing

main = do{
  print $ fromJust . join $ find isJust (map (getJustArg f) [1 ..])
  }

答は3121となる。

■まとめ
Maybeモナドに対するKleisli射の合成演算(>=>)を用いてクイズを解いてみた。

■おまけの問題

5人の男と一匹の猿が難破して無人島に漂着した。1日目、彼らは食糧としてたくさんのココナツを集めて回った。そしてその夜、すべてのココナツを積み上げて彼らは眠りについた。
 しかし全員が眠りについたあと、1人の男がふと目を覚ました。朝になってココナツを分けるとき、ひと悶着起きるかもしれないではないか。心配になった彼は自分の取り分を先取りしようと考えた。彼がココナツを5つの山に等分してみると、4つ余ったので、彼は余ったココナツを猿にあげてから、自分の取り分を隠して、残りを元通りに積んでおいた。
 しばらくして別の男が目を覚まして、同じことを考えた。今度は3つ余ったので、彼はやはり余ったココナツを猿に与え、自分の取り分を隠してから残りを積んでおいた。
三番目の男も同じことを考えたが、彼がココナツを5つの山に分けようとすると今度は2つ余った。やはり彼は余ったココナツを猿に与え、自分の取り分を隠してから残りを積んでおいた。
四番目の男も同じことを考えたが、彼がココナツを5つの山に分けようとすると今度は1つだけ余った。やはり彼は余ったココナツを猿に与え、自分の取り分を隠してから残りを積んでおいた。
五番目の男も同じことを考えたが、彼だけは仲間を裏切ることを恥ずかしく思い、結局何もしなかった。
朝になり、残ったココナツ全部を分けると、きれいに5等分された。
さて、最初にココナツはいくつあったのだろうか?

最小の答は3089個になるはずである。

Windowsからevinceを使う

■evinceとは
ubuntuなどをつかってるときのデフォルトのPDFビューワです.

■evinceをWindowsで使うメリット
アドビのPDFビューワと異なり,ファイルをロックしません.TeXWorksのような統合環境ではなくコマンドラインからlatexをコンパイルしているときに便利です.

■インストール方法
$ pacman -Ss evince
とやれば幾つか候補がでてくるはずです.

■使い方
$ evince hoge.pdf&
としてやり,hoge.texを色々編集してコンパイル.いちいちhoge.pdfを閉じる必要はありません.

C90: 「簡約!? λカ娘 9」 が出ます

C90の三日目(2016/08/14(日))に、サークル「参照透明な海を守る会」から『簡約!? λカ娘 9』が出ます。場所は「西地区f32a」です。

<簡約!? λカ娘 9> 内容紹介
第 1 章 λカ娘探索ファイナル (@ark_golgo)
第 2 章 変態する昆虫の観察 (@master_q)
第 3 章 IST(Internal Set Theory) 入門 (前編) (@dif_engine)

第 3 章の『 IST(Internal Set Theory) 入門 (前編) 』が私の記事です。

以下、いくつかの記事について簡単な紹介をします。自分が書いた記事以外はどれも「ちゃんと理解できていない」ので、自分の理解の程度に応じた紹介となります。ご了承ください。

第1章 λカ娘探索ファイナル
AlphaGo が凄いということはみなさんもご存知かと思いますが、では一体どこがどのように凄いのでしょうか?この記事ではコンピュータ囲碁の研究をしている荒木さんによって、コンピュータ囲碁の歴史とAlphaGoの強さの本質、そして将来のコンピュータ囲碁の展望が語られています。

第2章 変態する昆虫の観察
組み込み系のChibiOS/RT というOSは独自の(非POSIXの)スレッド機構を持ち、グローバルロック状態に応じて呼び出せるシステムAPIが変わるのだそうです。間違ったシステムAPIの呼び出しは未定義の挙動を引き起こすのですが、このたぐいのコーディングミスは実行時ではなく、コンパイル時にわかってほしいものです。そのための方法の一つはプログラムの静的なチェックを強化することです。岡部さんの方針は、この静的なチェックのためにATSを使うというものです。(この場合、ATSは最終的にC言語のソースコードを生成します。)

第3章 IST(Internal Set Theory) 入門 (前編)
Edward Nelson によって創始された超準集合論であるInternal Set Theory (以下、IST)という理論があります。
「ふつうの」超準解析、例えば齋藤正彦やM・デービスや中村徹の超準解析の本では、通常の集合論宇宙の超積を使って超準宇宙を作ります。
これに対し、NelsonによるISTにおいては、通常の集合論宇宙が超準宇宙に該当します。この宇宙の中に、一種のミニチュア宇宙が存在し、そこには空集合からスタートして集合論公理を有限回使って到達できるもの全てが含まれています。ISTでは、その意味で超準化という手続きは「すでに終わっている」ので超準宇宙の構成の議論は必要ありません。また、ISTはZFCの保存拡張になっているため、ZFC集合論での全ての定理はISTの定理でもあります。
(超積による超準宇宙の構成では正則性公理(基礎の公理)が省かれることがあります。したがって、ZFC集合論における議論を修正しないとZFC宇宙における定理を超準宇宙に輸入できないことがあります。)

このように言うとISTには良いことしかないようですが、NelsonのIST論文は若干読みにくいところがあります。それは、(1)読者に数理論理学の基礎的教養を要求している (2)ZFCにおける有限性のやや深い理解を要求している ところから来ているのではないかと思います。

(1)に関して言えば、ISTの公理図式は、量化子を「St付き」に変更するような操作を要求しており、論理式をオブジェクトとみなす視点が必要です。(2)に関して言えば、”直観的には”無限集合にしかなり得ない巨大な集合が有限集合であることがISTでは示されたりします。そして、そのようなことがISTにおける議論において有効に利用されたりする場面があります。このため、ISTを学ぶ人は「有限性とはなんだったのか」と悩むことになるでしょう。ISTにおける「有限性」の奇妙さに関連して、Nelson自身は次のような言葉を残しています:

—Perhaps it is fair to say that “finite” does not mean what we have always thought it to mean. What have we always thought it to mean?
I used to think that I knew what I had always thought it to mean, but I no longer think so. In any case, intuition changes with experience.

(1)も(2)もそれぞれ数理論理学と公理的集合論の基本的な教科書を読めば済む話なのですが、なかなか大変です(大変でした)。この章を読みこなせばNelsonによるISTの論文を読むための最低限の知識が得られる、そんな線を狙って執筆しました。なお、この(1)(2)を丁寧に説明しすぎて、肝心のISTの解説には入ることができなかったので「前編」とさせて頂きました。(後編は来年の予定です)。

表紙
久しぶりに表紙絵を描きました。「このすば」のめぐみんの衣装を着たイカ娘です。

簡約!? λカ娘 9 表紙

簡約!? λカ娘 9 表紙

(linux)最近のファイルをlsしたい

色々な論文を ~/Downloads に入れているうちにこのディレクトリに多数のファイルが置かれるようになってしまいました。もちろん ls -c すれば日付順に並べてくれますが沢山あるのでずらーっとファイルが列挙されてしまいます。そこで ls -c | head すれば最初の十個だけ示してくれます。もう少し多く見たい場合、たとえば最近の20個のファイルを見たい場合は ls -c | head -20 だとか、結局は同じことですが ls -c | head --lines=20 とすればよろしい。

TeXworks設定メモ

一発で見つけられなかったのでメモしておきます。

latexsetting

(追記: 「texworks 日本語」でググるのが正解だったらしい → TeX wiki — TeXworks/設定/日本語環境用の設定 )

(windows) TeXworks のテンプレートの場所

TeXworksで用意されているテンプレートはpLaTeXを通らないので、自作のテンプレートを用意している方も多いでしょう。
そうして苦労して作ったテンプレートは

C:\Users\USERNAME\.texlive2013\texmf-config\texworks\templates

に置くと、TeXworks からテンプレートに基づいて文書を作成する際に参照しやすくていいですよ。