/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を使うとコピーコストが低くなる場面があるかもしれない。(未検証)

2014-01-18

PowerPC64アセンブリ開発環境の整備

目的

PowerPC64アセンブリの演習のための環境を手元で構築する．

前提

Ubuntu 13.10 (x86_64) を利用していると仮定する．

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

bash用の補完プラグインを入れる

入れなくても良い

sudo cp ct-ng.comp /etc/bash_completion.d/

PowerPC64用クロスコンパイラのビルド

必要なパッケージを入れる

これらはcross-gdbのビルドに必要(入れていないとビルドの最後のほうで失敗して泣く)

$ sudo apt-get install libexpat1-dev python2.7-dev

ソースを補完するディレクトリを掘る

デフォルトだとホームの下のsrcに設定されている．ディレクトリがないと保存されないので掘っておく

$ mkdir ~/src

作業ディレクトリを掘る

$ mkdir ppc64-toolchain
$ cd ppc64-toolchain

powerpc64-unknown-linux-gnu用に設定する

$ ct-ng powerpc64-unknown-linux-gnu

設定をいじる

$ ct-ng menuconfig

設定画面の使い方

上下: 選択肢の移動
スペース: 選択肢の選択
左右: <Select> / <Exit> / <Help> の間を移動
Enter: <Select> / <Exit> / <Help> のうち選択されているものを実行

推奨の設定: FortranとJavaを外す

上下キーで 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がその場所を把握していないからである．

QEMU_LD_PREFIX環境変数を設定

$ 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で実行しているものを遠隔操作する方法を用いる．(リモートデバッグという)

デバッグオプションをつけてコンパイル

デバッガを使う上で-gをつけないと余りに不便．

$ powerpc64-unknown-linux-gnu-gcc -g hello.c

プログラムを実行

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

2013-12-22

ipc_botの紹介

この記事はTheorem Prover Advent Calendar の22日めの担当記事です．

今年の僕の持ちネタの一つですが，ipc_bot というTwitter botを作りました．

https://twitter.com/ipc_bot

このbotは直観主義命題論理の命題を投げると解いてくれるbotです．

仕組み

証明を探すのは適当にやっても出来るのですが，証明が存在しないことを確認するのは結構大変です．

(古典論理の場合は与えられた命題の否定をSATソルバーにかければ正誤がわかりますが，直観主義論理命題論理だとそう簡単ではありません)

証明が存在するかどうかを有限時間内で判定するには，推論規則を色々いじる必要があります．しかしその説明をはてなブログで書くのが面倒になってしまったので過去に某所に寄稿したものを見て下さい． http://www.tsg.ne.jp/buho/305/buho305.pdf [PDF]

ソースコード

ソースコードはここにあります．

https://github.com/qnighy/ipc_solver

その他の応用例

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.

形式的証明

かつて形式的証明を書いたことがあります．

また，Coqのcontribにも検証済みの証明探索アルゴリズムがあります．こちらについては未確認ですが，OCamlへの抽出もできるようになっており，かなりよく出来ていることが推察されます．

http://coq.inria.fr/pylons/pylons/contribs/view/IPC/v8.4

まとめ

随分と雑な記事になってしまってすみません．来年は精進します．

お詫びに，おもちゃの定理証明器に線形型を加えたものへのリンクを貼っておきます．

https://github.com/qnighy/proofline0

まだ型検査器しか作ってないですが一応定理証明器と言えると思います．ですが，おもちゃの定理証明器についてはkikxさんが既に記事にしていたようなのであまり書くことがありませんでした．

以上です．

2013-12-15

情報オリンピック予選 2014

情報オリンピックの予選に参加しました．(予選は誰でも参加できます)

次のような制約で解くことにしていました．

1番は Wolf RPGエディター
2番は TeX
3番は Scratch
4番は Excel
5番は APL
6番は Bash

結局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のときだけ落ちるような間違いでした．

2013-09-03

夏季セミナー参加記＆反省会

来年やる人が同じ失敗をしないために色々書いておきます

途中で「です・ます」調でなくなっているのは息切れです。めんどくさいので直していません

参加記

端的にまとめます

場所：今年は埼玉の準山奥でやりました。2009年に僕が生徒として参加したときと同じです。
チューター：今年はチューターが8人と多く、そのうち一人は初の女性チューターでした。
08/26
- 適切な電車が30分に一本程度しかないので、参加者の多くが同じ電車で来ていました。
- 自己紹介がgdgdだったので何とかしたい
- 無線LAN機器が不足していた
- 部屋割りも全然決めていなかった。事前に決めたほうがスムーズかも
08/27
- 普通にセミナーをした
- たまに理解が進まなそうなところとかについて軽く白板を使って説明したりした
08/28
- 普通にセミナーをした
- たまに実装が微妙にバグっている人の手助け？をしていた
- 交流と称していろいろなことをやった(後述)
08/29
- 普通に発表準備をした
- 定期的に発表を聞いてチェックしてた
08/30
- 発表があった(togetter参照)
- 案の定定刻に始められるわけがなかったので反省(後述)
- そのあと帰った

反省1: 自己紹介のgdgd感

gdgdなのが全面的に悪いわけではないけど時間は勿体無いよね。

今年は

名前
所属
学年
Twitterアカウント(任意)
その他(任意)

を言ってもらったけど、いずれにせよ何を話してもらうか最初に宣言しておいたほうが話しやすくなるから、来年はぜひ予め検討しておくべき。

その他

好きなプログラミング言語
普段使っているOS
好きなアニメ・漫画作品

など、最初の話題作りになりそう(？)なことを言ってもらうのもありかもしれない。

ちなみにこの日の全体の流れは次のような感じ。

夏季セミナーについての概略(by チューターリーダー)
- あらかじめ話す内容を考えておいたほうがいいかも
チューター自己紹介(年齢順)
- 紹介の順番とかもあらかじめ決めたほうがgdgdしなくて済むと思う
生徒自己紹介(名簿順)
本の紹介(担当チューターによる)
本選びフェーズ
- これについては後述
- ここまでで90分かかった
荷物を持って宿泊棟に行き、そのあと夕食
- 食堂と宿泊棟が近く、研修棟が遠かったのでこの順番にした。
戻ってセミナー#1

反省2: 必要な機材

今年は無線LANルーターが初日に1台しかなかったのが大変だった。

結局次の日に事務局の人が持ってきてくれたのでよかったが、あらかじめ必要な機材のリストをチューターの側でまとめておいて、事務局の人に伝えておいたほうが、混乱が避けられるかも。

なお、具体的には次のような機材があるとよい。

無線LANルーター: 部屋の数だけあると良い。
- また、セミナー終了後に使うためにもう1台あっても良いかもしれない。(これはチューターの私物でもよい。セミナーで使ったものを流用してもよいが、機材の移動はできるだけ避けたい)
- JOIではAirMac Extremeを使うので、AirMacの設定に詳しいマカーの人をあらかじめ見つけておくといいだろう。
電源タップ
- コンセントが壁からしか生えていない部屋のほうが多いので、距離が稼げるもののほうが良い
- 今年の感触としては、一人1コンセントあれば足りそう
LANケーブル・有線LANのハブ
- 無線LANルーターが存在しているのであればその数のLANケーブルだけあればとりあえず十分
- 念のためあっても良いかも

反省3: 部屋割り

今年は8班で3部屋にわかれてセミナーを行った。この部屋割りはその場で決めたが、事前に決めることも可能であったように思う。

ちなみに部屋は、できるだけ入れ替わるように(いろいろな班と相席するように)部屋割りをつくった。

反省4: 本決め

JOIではJMOと違って用意されている本の数=生徒の数であり、本が余ることはない。

本の決め方は

白板上に残り枠数を書いておいて、まだ確定していない生徒は希望する本の欄に名前を書いておく
- この時点では移動可
誰も移動しなくなったら、その時点で選抜を開始する
- 枠数より少ないところは確定
- 枠数より多いところはじゃんけんして、勝った人から確定
手順1に戻る

を繰り返すことによって行った。最小費用流を使うという意見もあったが、人間がやるのであればこれがわかりやすくて適切だと思う。

反省5: 交流

前の年に企画したものと同様に、今年も3日目に交流という名前のついた時間を2時間用意した。

今年は特に何も用意していなかったので、次のようなことをやった。

与えられた条件を満たす漢字や英単語をできるだけ多く列挙するゲーム
Set(iPad用)
空気を読むゲーム(iPad用)

来年もやるなら、ぜひ準備万端で挑んでほしい。(gdgdにやったせいでかなり時間を浪費した気がする)

反省6: 発表時間

今年は発表時間が昼休みを挟んで3時間+2時間だったので、前半に5チーム・後半に3チームと分けることにした。

これを決めたのは交流の時間の冒頭。発表順はそのタイミングで決めるのが正解だと思うが、時間の分け方とかはあらかじめ考えておいたほうが良かった気もする。

計算上は1人あたり10分ということになったのでこれを採用したが、次の日にこれではまずいということに気づいた。
結局、1人あたり10分の計算で時間を組むが、発表にかけていい時間は1人あたり7分程度ということにした。

この時間設定は結果としては正解だった。午前の発表が始まったのは予定の30分後だった。(というか、さすがに予定時間ちょうどに始めるのは不可能)

この日は僕は食堂が開いて一番に食事を取り、8時にレアン君のスライドをチェックした後、8時半に発表会の会場に着いて配線等の作業をしていたが、たぶん生徒が9時ちょうどに着席していたとしてもその時点で発表をするのは不可能であったように思う。

以下の準備が必要なので注意すること。

無線LAN。去年や今年みたいに皆でTwitterで実況しながらやる流れでいくなら今後も必須。AirMac Extreme 1台では接続数的に足りなかったので2台稼働させた。
場合によっては電源タップ。
- 今年のように、床から供給できる部屋であるほうが望ましい。
プロジェクター類。
- これに関しては発表者側の環境との関係もあるので厄介(後述)
発表会についての説明をするスライド
- 「発表したらSlideshare等にぜひアップロードして」とか「ハッシュタグは#JOIss だよ」とか、そういう色々を予め連絡してから発表会を始めるとよい
スライドなどのデータを集めるためのUSBメモリ
- 複数あっても良いかもしれないけどめんどくさいからやっぱり1つでいいや
タイマー
- iPad/iPhoneでプレゼンタイマーというのがあって、去年と今年はこれを使った
- 予めインストールしておこう
- 今年は6,7,8分経過時に鳴らした
togetterにまとめる人の用意(やるのであれば)
- 便利なのでやってほしい

反省7: 生徒への連絡等

プロジェクターとの接続テストは予め実施しておきたい。
- 今年は接続テストは不可能だったけど、せめて接続可能なインターフェースの確認(たいていVGAだけだけど)とその周知をしておくべきだった
スライドやデータ(主にソースコード)は参加者への配布のため回収するということの周知
- スライドはオリジナル(pptxやkeyやodp)とpdfの両方が用意されているとなおよい
参加記はもはや義務化してもいいのでは？
- 「参加記を書くまでが夏季セミナーです」的な

まとめると、発表会前と発表会後に以下のことは伝えるといいと思う(今年の場合の例)

発表の予定時間
1人あたりの発表に許された時間
質疑応答のタイミング(個人の発表ごと？班ごと？)
- 今年は、個人の発表ごとに質問があるか聞いて、10秒経ったら次の発表に移った。
スライドやデータを集めるということ
- 発表中か発表前に集めたほうがいいです(終わったら解散なので)
スライドのアップロードのお願い
- Slideshare/Speakerdeck等へのスライドのアップロードを是非お願いしてください。
  - 色々オフィシャルに持っておきづらいスライドが多いので個人であげてもらうほうがよい
ハッシュタグ
- #JOIss
家に帰ったら参加記を書いてくださいとお願いしましょう
解散前に集合写真を撮るのを忘れないようにしましょう
- 今年は忘れかけた(odan君が指摘してくれたので助かった)

あと終わった後に、次のようなことをするのもチューターの仕事です

集めたスライドやデータをまとめて参加者に配布すること
- 配布しなければいけないので予め連絡をとれる状況にしておいたほうがいいです
- 連絡がつきそうになければ事務局の人経由でも大丈夫かもしれないけれど
参加記やスライドのアップロードを催促して、ブログにまとめること

反省8: チューター会議とリーダー

ここまで書いてて思ったのだが、チューター会議みたいなのをやったほうが話がスムーズに進むのではないか？

リアルじゃなくてSkype上とかでもいいけど。

あと今年は名目上のリーダーみたいなのが決まっていた程度で、鶴の一声みたいな人がいなかったからgdgdだったところがある気がするので、もうちょっとちゃんとリーダーを決めてやったほうがいいかもしれない。

反省9: 生徒の内輪ネタ

悪いということではないが、生徒の内輪ネタには毎回ヒヤヒヤさせられるので思ったことをここに書いておく。

自己紹介フェーズで内輪ネタがいっぱい出てきたので、JOIとか初めての人がドン引きしないかすごくヒヤヒヤしてた。少なくとも今年は大丈夫だったみたいだが。
発表で、同じ研修施設を使っていた中学校がネタにされているのもなんかヒヤヒヤしながら聞いていた。
あと、離席した人のPCがロックされていなかったらTwitterで勝手に発言するという習慣も、なんとなく皆了解している感じがあるけど、あれで本気で怒る人だっていてもおかしくないだろうなあとかちょっと思う。せめてこれ以上エスカレートしないような方向性で見守るのがいいのかなあ。

反省10: JMOとの比較

JMOのに参加したときを思い出しながら比較してみる(あんまり反省っぽくないけど)

まずいちばん大きいのが日数で、JOI夏季セミナーが4泊5日なのに対してJMO夏季セミナーは6泊7日ある。

これによってセミナー時間が増えているかどうかはさておき、僕の記憶では自由時間がかなり一杯あって、毎日人狼やら何やらで遊んでいた気がする。あとバーベキューしたりとか滝まで歩いて行ったりとか。

こういう時間がJOIにもあればなーと常々思っているが、一方で、そういう自由時間があっても半分くらいの人がTwitterしながらコード書いてるだけの会になりそうな気もして、なんか微妙…と思うこともある。

人数は、JOIが生徒25名前後でチューターは今年は多くて8名だったのに対して、JMOでは生徒が35人程度、チューターが15人程度。人数が多く、チューター比率も高いようだ。ちなみに女子の人数は同じくらい。

(チューターの気持ちだけで決められる問題ではないが)人数は多いほうがいい、と僕は思っている。ただ人数が増えたらその分運営をしっかりやっていかないとだめになりそう。

本は、JMOではJOIと違って本のほうが余分にあるので、生徒の選択によっては班が消滅したりする。(余った本がどうなるのかは知らない) これはこれでアリだけど別にそうする必然性も無いんじゃないかなと思う。

まとめ

次回僕が参加できるかどうかわからないけど、次回リーダー格の人には是非、こういった内容に注意しながら、よりよい夏季セミナーを作っていってほしい。

前提知識

古典論理 (classical logic)

決定性の値の取り出し (description)

決定性の古典論理

ジョン・メジャーの等式 (John Major's equality)

関数外延性 (functional extensionality)

命題外延性 (propositional extensionality)

部分集合についての集合外延性 (extensionality of ensembles)

非決定性の値の取り出し (indefinite description)

目的

GMPのインストール

サンプル

解説

目的

最新情報へのリンク

前提

crosstool-ngの導入

必要なパッケージの準備

ソースコードを入手してビルド

bash用の補完プラグインを入れる

PowerPC64用クロスコンパイラのビルド

必要なパッケージを入れる

ソースを補完するディレクトリを掘る

作業ディレクトリを掘る

powerpc64-unknown-linux-gnu用に設定する

設定をいじる

ビルド実行

コンパイルする

PATHの追加

サンプルソースコード

アセンブリソースの出力

実行

qemu-userのインストール

QEMU_LD_PREFIXの設定

a.outを実行してみる

デバッガの利用

デバッグオプションをつけてコンパイル

プログラムを実行

デバッガを起動

デバッガを使う

仕組み

その他の応用例

形式的証明

まとめ

1番

2番

3番

4番

参加記

反省1: 自己紹介のgdgd感

反省2: 必要な機材

反省3: 部屋割り

反省4: 本決め

反省5: 交流

反省6: 発表時間

反省7: 生徒への連絡等

反省8: チューター会議とリーダー

反省9: 生徒の内輪ネタ

反省10: JMOとの比較

まとめ