Coqの新機能、Primitive Projectionについて
Coqリポジトリのtrunkを見ると、次の2つの機能が入っていることがわかります。
- Universe Polymorphism
- Primitive Projection
Universe Polymorphismは、グローバル定義をUniverseのレベルについて量化した形で定義することができる機能で、型に飾り付けをしたい場合(Homotopy n-typeやCategoryなどを定義したい場合)に宇宙ごとに異なる定義をする必要がなくなるという利点があります。
というのはさておき、この記事ではPrimitive Projectionを紹介します。
Primitive Projectionは、レコード型を定義したときにできる射影関数がプリミティブになるという機能です。Coqの内部で、普通の関数とは異なる特別な値として扱われるようです。
利点は次の2点のようです。
- 型検査の効率Up
- η変換ができる
ここでは後者の点についてサンプルコードを示します。
(* 従来のレコード型 *) Record Foo := Build_Foo { foo : unit }. Set Primitive Projections. (* Primitive Projectionを有効にしたレコード型 (Primitive Recordと呼ぶ) *) Record Bar := Build_Bar { bar : unit }. (* 従来のレコード型では、η変換はできない *) Goal forall f : Foo, f = Build_Foo (foo f). Proof. Fail reflexivity. Abort. (* Primitive Projectionを有効にしたレコード型では、η変換ができる *) Goal forall b : Bar, b = Build_Bar (bar b). Proof. reflexivity. Qed. (* どうやら、射影関数を自分で定義しても、同じ結果になるらしい? *) Definition foo2(f:Foo) : unit := let (foo2) := f in foo2. Goal forall f : Foo, f = Build_Foo (foo2 f). Proof. Fail reflexivity. Abort. Definition bar2(b:Bar) : unit := let (bar2) := b in bar2. Goal forall b : Bar, b = Build_Bar (bar2 b). Proof. reflexivity. Qed.
補足
そもそも、関数に関するη変換が入ったのが最近 (Coq 8.4以降) です。サンプルコードを示します。
Goal (fun (f:nat->nat) (n:nat) => f n) = (fun (f:nat->nat) => f). Proof. reflexivity. Qed.
面倒なので確かめていませんが、このような証明は以前は成立しなかったはずです。
よく使う Coq.Logic の公理
Coq.Logic にはCoqの集合論モデルにおいて正しい公理や、それらの間の関係が記述されている。
ここではその一部を取り上げて、意味を説明する。
前提知識
公理を仮定しない状態では、
- Coqの論理は直観主義論理である。
- ある2つが「等しい」という命題が証明できる場合は限定される。
- 証明の文脈(Prop)における「AまたはB」と、値の文脈(Set/Type)における「AまたはB」は区別される。前者から情報を取り出すことはできないようになっている(マッチングの型検査で弾かれる。)
以下、公理の説明
決定性の値の取り出し (description)
「条件を満たすものが唯一存在する」という命題から、具体的にその値を取り出す。
これによって証明できることは、例えば以下の内容がある。
- 二項関係であって関数としての条件を満たしているものから、関数を取り出す。
決定性の古典論理
場所: Coq.Logic.ClassicalDescription
名前どおり、Classical と Description を組み合わせたものである。
これによって証明できることは、例えば以下の内容がある。
- ある命題が正しいかどうかによる条件分岐を、関数中に書くことができる。
ジョン・メジャーの等式 (John Major's equality)
場所: Coq.Logic.JMeq
「型Aとその値の対」について、「型も等しいし、その値も等しい」という関係を考える。
「型Aと値x」と「型Aと値y」がこの意味で等しいとき、 x = y である。しかしこれはCoqでは公理なしでは導けない。これを仮定するのが JMeq である。
関数外延性 (functional extensionality)
場所: Coq.Logic.FunctionalExtensionality
二つの関数が等しいとは、どの値を入れても等しいことである。しかしこれはCoqでは公理なしでは導けない。これを仮定するのが FunctionalExtensionality である。
命題外延性 (propositional extensionality)
二つの命題が同値(A <-> B, 互いから互いを導ける)ならば、二つの命題は等しい(A = B)とみなしてよい。これにちょうど対応する公理はなぜか Coq の標準ライブラリにはない。次を参照のこと。
部分集合についての集合外延性 (extensionality of ensembles)
Aの部分集合を、所属関係を表す関数 A -> Prop で表すことにする。二つの部分集合が等しいとは、互いに包含していることとして定義される。
Ensembles に定義されている集合外延性 Extensionality_Ensembles は、関数外延性+命題外延性 よりは弱く、関数外延性よりは強い。
非決定性の値の取り出し (indefinite description)
場所: Coq.Logic.IndefiniteDescription
「条件Pを満たす値が存在する」という命題から、具体的に値を取り出す。(一意性は要求されない。)これは明らかにDescriptionより強い公理である。
IndefiniteDescriptionで言えることは、集合論における「選択公理」から導けることとほぼ同じだと思ってよい。
C++で多倍長整数ライブラリGMPを使う
目的
GCJなど一部のプログラミングコンテストでは既存のライブラリを使用することが認められている。
特にC++であれば多倍長整数ライブラリとしてGMPを使うのが妥当であると考えられる。GMPを直接叩くのもよいが、GMPのC++バインディングを使うのが簡単であると考えた。
GMPのインストール
Cygwinの場合は、インストーラーから libgmp-devel とその依存関係をインストールすればよい。
Ubuntuの場合は、aptでlibgmp-devをインストールすればよい。
他の場合は未調査。
コンパイル
例えば、次のようにしてコンパイルする。(他のオプションは適宜補う)
g++ main.cpp -lgmpxx -lgmp
このとき、引数の順番に注意すること。
例えば、ライブラリ指定をコンパイル対象より前に置いてしまうと、次のようなエラーメッセージが出る。(ライブラリ指定を忘れた場合も同様)
/tmp/cco0O7Yl.o: In function `__gmp_binary_plus::eval(__mpz_struct*, __mpz_struct const*, __mpz_struct const*)': main.cpp:(.text._ZN17__gmp_binary_plus4evalEP12__mpz_structPKS0_S3_[_ZN17__gmp_binary_plus4evalEP12__mpz_structPKS0_S3_]+0x27): undefined reference to `__gmpz_add' /tmp/cco0O7Yl.o: In function `__gmp_binary_multiplies::eval(__mpz_struct*, __mpz_struct const*, __mpz_struct const*)': main.cpp:(.text._ZN23__gmp_binary_multiplies4evalEP12__mpz_structPKS0_S3_[_ZN23__gmp_binary_multiplies4evalEP12__mpz_structPKS0_S3_]+0x27): undefined reference to `__gmpz_mul' /tmp/cco0O7Yl.o: In function `__gmp_binary_multiplies::eval(__mpz_struct*, __mpz_struct const*, long)': main.cpp:(.text._ZN23__gmp_binary_multiplies4evalEP12__mpz_structPKS0_l[_ZN23__gmp_binary_multiplies4evalEP12__mpz_structPKS0_l]+0x27): undefined reference to `__gmpz_mul_si' /tmp/cco0O7Yl.o: In function `__gmp_expr<__mpz_struct [1], __mpz_struct [1]>::__gmp_expr()': main.cpp:(.text._ZN10__gmp_exprIA1_12__mpz_structS1_EC2Ev[_ZN10__gmp_exprIA1_12__mpz_structS1_EC5Ev]+0x14): undefined reference to `__gmpz_init' /tmp/cco0O7Yl.o: In function `__gmp_expr<__mpz_struct [1], __mpz_struct [1]>::__gmp_expr(int)': main.cpp:(.text._ZN10__gmp_exprIA1_12__mpz_structS1_EC2Ei[_ZN10__gmp_exprIA1_12__mpz_structS1_EC5Ei]+0x20): undefined reference to `__gmpz_init_set_si' /tmp/cco0O7Yl.o: In function `__gmp_expr<__mpz_struct [1], __mpz_struct [1]>::~__gmp_expr()': main.cpp:(.text._ZN10__gmp_exprIA1_12__mpz_structS1_ED2Ev[_ZN10__gmp_exprIA1_12__mpz_structS1_ED5Ev]+0x14): undefined reference to `__gmpz_clear' /tmp/cco0O7Yl.o: In function `std::ostream& operator<< <__mpz_struct [1], __mpz_struct [1]>(std::ostream&, __gmp_expr<__mpz_struct [1], __mpz_struct [1]> const&)': main.cpp:(.text._ZlsIA1_12__mpz_structS1_ERSoS2_RK10__gmp_exprIT_T0_E[_ZlsIA1_12__mpz_structS1_ERSoS2_RK10__gmp_exprIT_T0_E]+0x32): undefined reference to `operator<<(std::ostream&, __mpz_struct const*)' /tmp/cco0O7Yl.o: In function `__gmp_expr<__mpz_struct [1], __mpz_struct [1]>::__gmp_expr<__gmp_binary_expr<__gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_plus> >(__gmp_expr<__mpz_struct [1], __gmp_binary_expr<__gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_plus> > const&)': main.cpp:(.text._ZN10__gmp_exprIA1_12__mpz_structS1_EC2I17__gmp_binary_exprIS2_S2_17__gmp_binary_plusEEERKS_IS1_T_E[_ZN10__gmp_exprIA1_12__mpz_structS1_EC5I17__gmp_binary_exprIS2_S2_17__gmp_binary_plusEEERKS_IS1_T_E]+0x18): undefined reference to `__gmpz_init' /tmp/cco0O7Yl.o: In function `__gmp_expr<__mpz_struct [1], __mpz_struct [1]>::__gmp_expr<__gmp_binary_expr<__gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_multiplies> >(__gmp_expr<__mpz_struct [1], __gmp_binary_expr<__gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_multiplies> > const&)': main.cpp:(.text._ZN10__gmp_exprIA1_12__mpz_structS1_EC2I17__gmp_binary_exprIS2_S2_23__gmp_binary_multipliesEEERKS_IS1_T_E[_ZN10__gmp_exprIA1_12__mpz_structS1_EC5I17__gmp_binary_exprIS2_S2_23__gmp_binary_multipliesEEERKS_IS1_T_E]+0x18): undefined reference to `__gmpz_init' /tmp/cco0O7Yl.o: In function `__gmp_expr<__mpz_struct [1], __mpz_struct [1]>::__gmp_expr<__gmp_binary_expr<__gmp_expr<__mpz_struct [1], __gmp_binary_expr<long, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_multiplies> >, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_plus> >(__gmp_expr<__mpz_struct [1], __gmp_binary_expr<__gmp_expr<__mpz_struct [1], __gmp_binary_expr<long, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_multiplies> >, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_plus> > const&)': main.cpp:(.text._ZN10__gmp_exprIA1_12__mpz_structS1_EC2I17__gmp_binary_exprIS_IS1_S4_IlS2_23__gmp_binary_multipliesEES2_17__gmp_binary_plusEEERKS_IS1_T_E[_ZN10__gmp_exprIA1_12__mpz_structS1_EC5I17__gmp_binary_exprIS_IS1_S4_IlS2_23__gmp_binary_multipliesEES2_17__gmp_binary_plusEEERKS_IS1_T_E]+0x18): undefined reference to `__gmpz_init' /tmp/cco0O7Yl.o: In function `__gmp_expr<__mpz_struct [1], __mpz_struct [1]>::__gmp_expr<__gmp_binary_expr<long, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_multiplies> >(__gmp_expr<__mpz_struct [1], __gmp_binary_expr<long, __gmp_expr<__mpz_struct [1], __mpz_struct [1]>, __gmp_binary_multiplies> > const&)': main.cpp:(.text._ZN10__gmp_exprIA1_12__mpz_structS1_EC2I17__gmp_binary_exprIlS2_23__gmp_binary_multipliesEEERKS_IS1_T_E[_ZN10__gmp_exprIA1_12__mpz_structS1_EC5I17__gmp_binary_exprIlS2_23__gmp_binary_multipliesEEERKS_IS1_T_E]+0x18): undefined reference to `__gmpz_init' collect2: error: ld returned 1 exit status
サンプル
整数nとmを入力すると、フィボナッチ数列のn番目を計算するプログラム。
- m = 1 のとき、再帰による計算を行う。(四則演算の回数は指数オーダー)
- m = 2 のとき、動的計画法による計算を行う。(四則演算の回数は線形)
- m = 3 のとき、行列累乗による計算を行う。(四則演算の回数は対数オーダー)
#include <iostream> #include <gmpxx.h> mpz_class fib1(int), fib2(int), fib3(int); int main() { int n, m; std::cin >> n >> m; if(m == 1) { std::cout << fib1(n) << std::endl; } else if(m == 2) { std::cout << fib2(n) << std::endl; } else if(m == 3) { std::cout << fib3(n) << std::endl; } return 0; } mpz_class fib1(int n) { if(n <= 1) return n; else return fib1(n - 1) + fib1(n - 2); } mpz_class fib2(int n) { mpz_class a = 1, b = 0; for(int i = 0; i < n; ++i) { swap(a, b); b += a; } return b; } mpz_class fib3(int n) { mpz_class a = 1, b = 0, c, d; for(int i = 30; i >= 0; --i) { c = a * a + b * b; d = b * (2 * a + b); if((n >> i) & 1) { b = c + d; swap(a, d); } else { swap(a, c); swap(b, d); } } return b; }
解説
mpz_classは、GMPの多倍長整数のC++によるラッパークラスである。これはintとほぼ同じように取り扱うことができる。
- 四則演算はほぼ通常通り使える。
- iostreamを用いる場合は、intと同様に読み書きできる。
- intからの自動キャストがある。
mpz_classは通常の整数型とは違い、生成コストやコピーコストに気を使ったほうがよい場面がある。vectorと同様、mpz_classには高速なswapが定義されているので、それを用いるのがよい(気がする)。
最近のGMPのC++バインディングにはムーブコンストラクタが定義されている。C++11を使うとコピーコストが低くなる場面があるかもしれない。(未検証)
PowerPC64アセンブリ開発環境の整備
目的
PowerPC64アセンブリの演習のための環境を手元で構築する.
最新情報へのリンク
2015/01/11 以下のように事情が変化している。
- PowerPC64 アセンブリ開発環境の設定メモに、以下の手順を現在行った場合に起きる問題への対処法がある。
- crosstool-ngのバージョンは1.20.0が最新。
- 実は、crosstool-ngを使わなくても、gcc-powerpc-linux-gnuやg++-powerpc-linux-gnuなどをインストールし、powerpc-linux-gnu-gcc等のコンパイラのコマンドに-m64オプションを付けて実行すればよいっぽいこともわかった。
crosstool-ngの導入
必要なパッケージの準備
$ sudo apt-get install build-essential gperf texinfo gawk libtool automake libncurses5-dev
ソースコードを入手してビルド
$ wget http://crosstool-ng.org/download/crosstool-ng/crosstool-ng-1.19.0.tar.bz2 $ tar jxvf crosstool-ng-1.19.0.tar.bz2 $ cd crosstool-ng-1.19.0 $ ./configure $ make $ sudo make install
PowerPC64用クロスコンパイラのビルド
必要なパッケージを入れる
これらはcross-gdbのビルドに必要(入れていないとビルドの最後のほうで失敗して泣く)
$ sudo apt-get install libexpat1-dev python2.7-dev
ソースを補完するディレクトリを掘る
デフォルトだとホームの下のsrcに設定されている.ディレクトリがないと保存されないので掘っておく
$ mkdir ~/src
作業ディレクトリを掘る
$ mkdir ppc64-toolchain $ cd ppc64-toolchain
設定をいじる
$ ct-ng menuconfig
設定画面の使い方
- 上下: 選択肢の移動
- スペース: 選択肢の選択
- 左右: <Select> / <Exit> / <Help> の間を移動
- Enter: <Select> / <Exit> / <Help> のうち選択されているものを実行
- 上下キーで C compiler ---> に移動,スペースで中に入る
- 上下キーで [*] Fortran に移動,スペースでチェックを消す
- 上下キーで [*] Java に移動,スペースでチェックを消す
- 左右キーで < Exit > を選択,Enterで実行→外に出る
- 左右キーで < Exit > を選択,Enterで実行→設定終了
終了時に設定を保存するか聞かれるのでYesと答える
ビルド実行
$ ct-ng build
あとはひたすら待つと勝手にビルドとインストールを実行してくれる
インストール先はデフォルトでは次のような構成
~/x-tools ~/x-tools/powerpc64-unknown-linux-gnu ~/x-tools/powerpc64-unknown-linux-gnu/bin ~/x-tools/powerpc64-unknown-linux-gnu/include ~/x-tools/powerpc64-unknown-linux-gnu/lib ~/x-tools/powerpc64-unknown-linux-gnu/libexec ~/x-tools/powerpc64-unknown-linux-gnu/powerpc64-unknown-linux-gnu ~/x-tools/powerpc64-unknown-linux-gnu/share
例えば,binの中身は次のようになっている
powerpc64-unknown-linux-gnu-addr2line powerpc64-unknown-linux-gnu-ar powerpc64-unknown-linux-gnu-as powerpc64-unknown-linux-gnu-c++ powerpc64-unknown-linux-gnu-cc powerpc64-unknown-linux-gnu-c++filt powerpc64-unknown-linux-gnu-cpp powerpc64-unknown-linux-gnu-ct-ng.config powerpc64-unknown-linux-gnu-embedspu powerpc64-unknown-linux-gnu-g++ powerpc64-unknown-linux-gnu-gcc powerpc64-unknown-linux-gnu-gcc-4.5.2 powerpc64-unknown-linux-gnu-gccbug powerpc64-unknown-linux-gnu-gcov powerpc64-unknown-linux-gnu-gdb powerpc64-unknown-linux-gnu-gdbtui powerpc64-unknown-linux-gnu-gprof powerpc64-unknown-linux-gnu-ld powerpc64-unknown-linux-gnu-ldd powerpc64-unknown-linux-gnu-nm powerpc64-unknown-linux-gnu-objcopy powerpc64-unknown-linux-gnu-objdump powerpc64-unknown-linux-gnu-populate powerpc64-unknown-linux-gnu-ranlib powerpc64-unknown-linux-gnu-readelf powerpc64-unknown-linux-gnu-size powerpc64-unknown-linux-gnu-strings powerpc64-unknown-linux-gnu-strip
コンパイルする
PATHの追加
環境変数PATHを追加する.
$ export PATH=$HOME/x-tools/powerpc64-unknown-linux-gnu/bin:$PATH
これを毎回実行するのは面倒なので,~/.bashrcに追記する.
$ echo 'export PATH=$HOME/x-tools/powerpc64-unknown-linux-gnu/bin:$PATH' >> ~/.bashrc
サンプルソースコード
次のようなCソースコードをhello.cという名前で作成する.
#include <stdio.h> int main() { puts("Hello, world!"); return 0; }
コンパイル
コンパイルする
$ powerpc64-unknown-linux-gnu-gcc hello.c $ file a.out a.out: ELF 64-bit MSB executable, 64-bit PowerPC or cisco 7500, version 1 (SYSV), dynamically linked (uses shared libs), for GNU/Linux 2.6.31, not stripped
確かにPowerPC64用のバイナリである.
アセンブリソースの出力
アセンブリのソースを出力してみる
$ powerpc64-unknown-linux-gnu-gcc -S hello.c $ cat hello.s .file "hello.c" .section ".toc","aw" .section ".text" .section .rodata .align 3 .LC0: .string "Hello, world!" .section ".toc","aw" .LC1: .tc .LC0[TC],.LC0 .section ".text" .align 2 .globl main .section ".opd","aw" .align 3 main: .quad .L.main,.TOC.@tocbase,0 .previous .type main, @function .L.main: mflr 0 std 0,16(1) std 31,-8(1) stdu 1,-128(1) mr 31,1 ld 3,.LC1@toc(2) bl puts nop li 0,0 mr 3,0 addi 1,31,128 ld 0,16(1) mtlr 0 ld 31,-8(1) blr .long 0 .byte 0,0,0,1,128,1,0,1 .size main,.-.L.main .ident "GCC: (crosstool-NG 1.19.0) 4.5.2"
確かにPowerPC64のアセンブリコードが出力されている.
実行
生成されたバイナリはPowerPC64用なのでそのままでは実行できない.
$ ./a.out bash: ./a.out: cannot execute binary file
そこで,エミュレーターQEMUのユーザーモードエミュレーション機能を用いる.
qemu-userのインストール
$ sudo apt-get install qemu-user
QEMU_LD_PREFIXの設定
このままでは先ほどのa.outを実行できない.というのも,依存しているライブラリがあり,QEMUがその場所を把握していないからである.
$ export QEMU_LD_PREFIX=$HOME/x-tools/powerpc64-unknown-linux-gnu/powerpc64-unknown-linux-gnu/
これも毎回実行するのは面倒なので,~/.bashrcに追記しておく.
$ echo 'export QEMU_LD_PREFIX=$HOME/x-tools/powerpc64-unknown-linux-gnu/powerpc64-unknown-linux-gnu/' >> ~/.bashrc
a.outを実行してみる
$ qemu-ppc64 ./a.out Hello, world!
無事実行できた!
デバッガの利用
powerpc64-unknwon-linux-gnu-gdb自体はPowerPC64コードを実行する機能をもたないようなので,qemu-ppc64で実行しているものを遠隔操作する方法を用いる.(リモートデバッグという)
プログラムを実行
12345のところはポート番号なので,他の数字でもよい.このポートにgdbから接続する.
$ qemu-ppc64 -g 12345 ./a.out
こうすると,qemu-ppc64は待機状態になる.
デバッガを起動
別の端末を開いて,gdbを起動する.
$ powerpc64-unknwon-linux-gnu-gdb a.out
実行中のqemu-ppc64に接続する.
(gdb) target remote localhost:12345
これでデバッグの準備が整った.
デバッガを使う
ブレークポイントを設定してみる
(gdb) b main Breakpoint 1 at 0x1000051c: file hello.c, line 4.
実行してみる
(gdb) c Continuing. Breakpoint 1, main () at hello.c:4 4 puts("Hello, world!");
r (run) ではなくc (continue) であることに注意!
もう一回continueするとputsが実行されて終了する.このとき,qemu-ppc64を実行している端末でHello, world!が出力されるので確認すること.
(gdb) c Continuing. [Inferior 1 (Remote target) exited normally]
gdbを終了する.
(gdb) q
ipc_botの紹介
この記事はTheorem Prover Advent Calendarの22日めの担当記事です.
今年の僕の持ちネタの一つですが,ipc_bot というTwitter botを作りました.
このbotは直観主義命題論理の命題を投げると解いてくれるbotです.
仕組み
証明を探すのは適当にやっても出来るのですが,証明が存在しないことを確認するのは結構大変です.
(古典論理の場合は与えられた命題の否定をSATソルバーにかければ正誤がわかりますが,直観主義論理命題論理だとそう簡単ではありません)
証明が存在するかどうかを有限時間内で判定するには,推論規則を色々いじる必要があります.しかしその説明をはてなブログで書くのが面倒になってしまったので過去に某所に寄稿したものを見て下さい. http://www.tsg.ne.jp/buho/305/buho305.pdf [PDF]
その他の応用例
Coqのtautoがこのような決定アルゴリズムを使っているようです.
試しにそこそこ複雑な命題を投げても,きちんと答えを返してくれます.
Goal forall P Q R S:Prop, ~~((P <-> (Q <-> (R <-> S))) <-> (((P <-> Q) <-> R) <-> S)). Proof. tauto. Qed. Goal forall P Q R S:Prop, (P <-> (Q <-> (R <-> S))) <-> (((P <-> Q) <-> R) <-> S). Proof. try tauto. (* fail *) Abort.
形式的証明
かつて形式的証明を書いたことがあります.
- スライド: http://www.slideshare.net/qnighy/proving-decidability-of-intuitionistic-propositional-calculus-on-coq
- ソースコード: https://github.com/qnighy/IPC-Coq
また,Coqのcontribにも検証済みの証明探索アルゴリズムがあります.こちらについては未確認ですが,OCamlへの抽出もできるようになっており,かなりよく出来ていることが推察されます.
まとめ
随分と雑な記事になってしまってすみません.来年は精進します.
お詫びに,おもちゃの定理証明器に線形型を加えたものへのリンクを貼っておきます.
まだ型検査器しか作ってないですが一応定理証明器と言えると思います.ですが,おもちゃの定理証明器についてはkikxさんが既に記事にしていたようなのであまり書くことがありませんでした.
以上です.
情報オリンピック予選 2014
情報オリンピックの予選に参加しました.(予選は誰でも参加できます)
次のような制約で解くことにしていました.
結局1と4を解きました.
1番
Wolf RPGエディターで解きました.たぶん合っていると思います.
https://drive.google.com/file/d/0B0wUgziNPuKGUlZmaG5ka0ZIYUk/edit?usp=sharing
2番
TeXでようやくできました.もしかしたら処理系依存のところなどがあるかもしれません.
手元の環境はTeX, Version 3.1415926 (TeX Live 2013)です.
%\catcode`\@=11 \immediate\write16{} \def\fstimpl#1 #2\relax{#1} \def\fst#1{\expandafter\fstimpl#1\relax} \def\sndimpl#1 #2\relax{#2} \def\snd#1{\expandafter\sndimpl#1\relax} \read-1to\NM \def\N{\fst{\NM}} \def\M{\snd{\NM}} \newcount\x \newcount\y \newcount\z \newcount\w \newcount\k \x0 { \loop\ifnum\x<\N \read-1to\tmp \global\expandafter\edef\csname costs\the\x \endcsname{\tmp} \global\expandafter\edef\csname prefs\the\x \endcsname{0} %\immediate\write16{costs[x] = \csname costs\the\x \endcsname} \advance\x1 \repeat } \y0 { \loop\ifnum\y<\M \read-1to\tmp \k\tmp { \x0 \loop\ifnum\x<\N \w\csname costs\the\x \endcsname %\immediate\write16{k = \the\k, x = \the\x, w = \the\w, costs[x]=\csname costs\the\x \endcsname} \ifnum\k<\w \else \z\csname prefs\the\x \endcsname \advance\z1 \global\expandafter\edef\csname prefs\the\x \endcsname{\the\z} %\immediate\write16{OK! x=\the\x, prefs=\the\z} \x\N \fi \advance\x1 \repeat } \advance\y1 \repeat } \x0 \w0 \loop\ifnum\x<\N \y\csname prefs\the\x \endcsname \z\csname prefs\the\w \endcsname \y\csname prefs\the\x \endcsname %\immediate\write16{prefs[\the\x] = \csname prefs\the\x \endcsname} \ifnum\y>\z \w\x \fi \advance\x1 \repeat \advance\w1 \immediate\write16{\the\w} \bye
3番
コンテストから1週間経ち,今更感がありますが,Scratchで書きました.ご確認ください.
http://scratch.mit.edu/projects/15970373/
入力を1列でしか受け取れないのが残念ですが仕方ないですね.
4番
Excelで解きました.一部間違ってるかもしれません.
https://drive.google.com/file/d/0B0wUgziNPuKGNVJWVWRBdXhxSG8/edit?usp=sharing
追記:間違いの理由がわかりました.n=1000のときだけ落ちるような間違いでした.