ちょっと入出力の練習

連投です.
某H社のtex記法がアレなのでGoogle Chart APIを使っているのですが,
直に打つのは面倒なので,latexの$$←こいつで挟んだ記法からGoogle Chartのイメージを取ってくるhtmlに変換するスクリプヨを書いていたわけです.
まあgauche使います.
いい入出力の練習です.

#!/usr/bin/env gosh
;; google chart に変換

(define (convert-tex port) ;convert-tex :: <port> -> <string>(portから変換後の文字列を出します)
  (define (foo in-port ls mode) ;modeは$$で挟まれた中にstreamが居るのかを判定しています.一個一個steamからcharを取り出してloopさせます
    (let ([ch (read-char in-port)])
      (define (dispatch!)
	(cond ((and (eq? ch #\$) mode)
	       (begin (set! ls (cons "<img src=\"http://chart.apis.google.com/chart?cht=tx&chf=bg,s,ffffff&chco=0000ff&chl=" ls))
		      (set! mode (not mode))))
	      ((and (eq? ch #\$) (not mode)) 
	       (begin (set! ls (cons "\"/>" ls))
		      (set! mode (not mode))))
	      (else (set! ls (cons (make-string 1 ch) ls)))))
      (if (eof-object? ch) ls
	  (begin (dispatch!) (foo in-port ls mode)))))
  (string-join (reverse (foo port '() #t)) ""))

(define (open->convert->write filename) ;fileをopenしてconvertしたものを<filename>-convertedという名前のfileに書き出します
  (let ([converted-txt (call-with-input-file filename convert-tex)])
    (call-with-output-file (string-append filename "-converted") (lambda (oport) (display converted-txt oport) ))))

(define (main args) ; mainループ.第一引数はデフォルトで"この"filenameになっているので捨てるのを忘れない
  (if (null? (cdr args)) (format #t "Convert done!\n")
      (let ([filename (cadr args)]
	    [rest-args (cdr args)])
	(open->convert->write filename)
	(main rest-args))))

取り合えず,hatena.scmとか名前付けて,diary.txtにtexのソース入れて

./hatena.scm diary.txt

するとコンバートされたのがdiary.txt-convertedに入ります.
昨日の記事はこうやって書きました.
背景とか文字色とか変えたい場合は適宜なんかいじってくらさい.
byebye

安定のHamkins大先生

本日(昨日)のmathoverflow案件:
Increasing and Descending Chains of Inner Models for Measurable Cardinals

初見で(b)がわかったのでtwitterの鍵垢に書いたんだけど,一応ここにも書く.
ただ時間的にその直後にHamkins先生のよりgeneralな回答が載っていてあれだった.

Question (b)

"クラスmanyに可測基数が存在して,各順序数について番目に可測基数を表すこととして上の-加法的な2値測度の列で,となるものが存在する"
はZFC上でどの程度の無矛盾性を持つか?

これに対する回答はZFC上で矛盾するというものでありその証明は以下の通り:

(b)が嘘の証明

を最小の可測基数とすると

が成り立ちます.
もまた可測基数のとき,上の測度は全部の中に入っているので,となってしまって2に矛盾です.

となります.
ここで証明の中の1,2に立ち入りましょう:

(1)の証明

まず,が可測基数でがその上の測度のとき,がどのように作られるかを見る必要があります.
とは,俗に言うによる超べきというもので以下のように定めます:
,
.
ここでとはを代表元とする同値類で,使われている同値関係

というもの.
このようにして決めたものの推移的崩壊をとると求めるが決まります.

ではからは初等埋め込みが以下のようにして定まります:
.
ここでを値とする定数関数です.
すると,が成り立つことがわかります.
ですが,任意のに対してとなる代表元が取れます.
が成り立つので,定義から

となります.
ここで,未満個の集合の和に関して加法的であるので,

となるが定まります.
このことはまさにを示しているのでとなります.
は任意だったのでが示せたことになります.
はもっと簡単です.
が順序を保存する写像であることを利用すればすぐに証明できます.

以上の議論で上でidentityであることがわかりました.
このことから上でもidentityであることがわかります.
実際,は可測基数で強極限基数であるのでの要素は皆濃度未満になります.
このことと,上の-帰納法を用いれば先ほどの議論と同様に

が示せます.
であったのでに含まれることが示せました.

(2)の証明

こっちは以下の通り.
まず,は最小の可測基数です.
故に,上で最小の可測基数です(は初等埋め込みなので).
が成り立つと言いましたが,実はも成り立ちます.
特に,にあるの部分集合をすべて含んでいます.
したがって,もしが成り立つならば,上で-加法的な2値測度になっています.
このことは,上で可測基数であることになりますが,簡単にわかるようにです.
これはさきほど言った上で最小の可測基数であることに反します.

こんな感じ.
まあリンクはったHamkinsの解説の方が明らかにスマートなんだけど,参考になったらよいです.
bye

C85

コミケで薄い本"The dark side of Forcing II"のなかの一つの記事10pagesくらいを担当しました。
内容は、KunenのInconsistencyの定理についてです。
Reinhardt基数のことについて書いたのです。
ラインハルト基数。
でも書籍中ではリインちゃんと読んでいます。
これは、まあ敢えてネタバレすると、皆さんご存知のリリカルなのはA'sにおいて登場するリインちゃん(Reinforce)になぞらえてつけた名前です(まあ偶然にもforceもかかっているわけなんで)。
まあ、登場するとは言っても初代リインフォースは作中では登場とほぼ同時、その力を二代目Reinforce zwei託して死んでしまいます。
なんとまあ儚いことですが、これが記事の本編とも関係しているわけです、はい。
実際Reinhardt基数ってのは幻の基数でして、登場とほぼ同時期にその非存在が証明されてしまいました。
そっくりです。
でその証明ってのがKunenのInconsistencyというやつです。
暇があったら証明読んでやって下さい。
一応主張書くだけ書いて今日は終わりにします:

Emacs で Racket の Repl を使えるようにするための覚えがき。

いいかげん乳離れならぬGauche離れをしたいと思っていたので。

Geiserと呼ばれるパッケージを使うのが楽です。
Emacs で package-install して持ってきます。
(詳しくはこことかに載っています)
使うrepoはmelpaで、emacs上で

[M-x] package-refresh-contents [RETURN]
[M-x] package-install [RETURN] geiser [RETURN]

します。
Racketはapt-getで持ってきます。
早速

[M-x] run-geiser [RETURN]

するとimplementationはどれか聞かれるのでracketと答えます:

racket [RETURN]

するとgeiserは5.3のracketじゃないとだめだよ!と怒られました。
使ってるマシンはubuntuで普通にapt-getすると現時点ではversion 5.1.3が入ります。
Debianのsid/mainでも使っていればこんなことはなかったんでしょうが、改めてsidから最新のversion 5.3.6を取ってきます。
今度はちゃんと起動して

Welcome to Racket v5.3.6.
racket@> 

と表示されて成功です。やたー
終了するには[C-c C-q]で。
終わり(特に落ちは無いです)

2013年とは一体何だったのか

手帳見ると思い出して涙が出るかもしれないので思い出せる範囲で書きます。

1月

某活してました。味噌カツではないです。セミナーセミナーセミナー。なおお金はほぼでない。

2月

某活つらいです。主に高速バス。
おそらく予算的にもJRバス使うのがたぶんいい。
3日前までに券とれば早割が効いて東京名古屋間だと最安片道3000円くらいで行け、コンスタントに予約に空きがある。
各種旅行会社が運営しているバスだと、これより安くいける場合があるが予約いっぱいだったり日によって値段の変動が大きいなどあまり期待はしないほうがいい。
新幹線使えば楽できるんだけど、そうそうお金は(就職セミナー主催側からは)でない。

3月

この辺になると少し落ち着いてくる。
面接とか絞れてくるし、あっちからお金出るパターンもある。
あんま覚えてないけど初内々定きたのこの月だったか。
三月の最終週は東京(面接)→京都(数学会)→東京(面接)とかは宿やバス内でで講演スライド修正とかしてたし発狂しかけた。
数学会の講演は無事に終わったのでよかったです。

4月

この月の前半で活動打ちきりました。
てか志望してたとこ全部選考ハイスピードなんだよ。
結局ゲットしたのは内々定一個だけであと5こくらい最終で全部蹴られましたね。
そこに決めて終わり、ちゃんちゃん。
そういえばFE試験受けたのこの月だっけ。

5月〜7月

覚えてない、というか放心であった。
ゼミはやっていた。
ゼミのテキストおよび論文がクソであったことは印象に深い。
大御所某T氏の論文と戯れたのはいい思い出。

8月

某人の提案によりコミケで本を出すことに。
楽しかったです、いい経験をさせてもらいました。
数学基礎論サマースクールもありました。同じ週にコミケだったので色々楽でした。
千葉大学の自称幼女にも会いました。楽しかったです。
後半は論理学徒のつどいなるものに参加およびお手伝いしてきました。
(肩書き的には副主宰だったんですが、この世において「副主宰」なる言葉から溢れるディストピア感にはあまり触れたくはないのだ(こうして触れてしまった))

9月

ゼミがくる。そして修論が足音を立てて近づいてきた季節であった。
こわい。こわい。さっさと逃げねば
SGLセミナには新メンバーもやって参りました。

10月

学校的には後期スタートです。が平常運行。
なぜかディープげふんげふんラーニングなるものの勉強会に誘われて参加し始めました。
めっちゃおもしろいです。ただ炎上案件な気がしてなりません。
果たして実装はできるのでしょうか、乞うご期待です。

11月

世間では数学基礎論若手の会なるものが開催されたようですがぼくは参加しませんでした。
そして修論のプレッシャーが刻々と近づいております。
てか修論書いてます。
いや修論の80%くらいは3月の数学会の内容の書き写し見たいなもんですが。

12月

結構心的にあれだった。
修論の証明に所々欠陥があってもうだめかと思った。
でもなんとかなった。ありがとう指導教員、acknowledgementにもちゃんと書くよ。

あとはコミケ第2段でした。頑張って書きました。
空回りっぽい感じでしたが発起人がうまくまとめてくれました。ありがとうございます。


こんな感じだろうか。
まあ、また来年も生きていたらなんか書くかもしれません。

では良いお年を。

testes

This entry is made to learn how to use Google Chart API.
The following mathematical article is based on a sequence of facts in set theory, that is known to be proved with ZFC:

Let be the Cohen forcing which adds one Cohen real.

Then the following holds:

This proves that whenever if a universe is some generic extension of some definable inner model with the Cohen forcing, there must be a Souslin tree.

On the other hand, it is well-known that the set-theoretical principle implies the existence of Souslin trees.
In particular, Souslin trees exists in , the Godel's constructible universe.

This shows that the existence of Souslin trees is compatible with both of combinatorics and the universe having many generic objects.
This is an interesting phenomenon.

I am interested also in the properties which are compatible both with combinatorics and large cardinal combinatorics.
An important case is the Singular Cardinal Hypothesis(SCH).
SCH is the following statement that Generalize the generalized Continuum Hypothesis(GCH):

For every singlar cardinal ,

It is known that SCH follows from the GCH and hence is a consequence of combinatorics.
But Solovay showed that SCH holds for all cardinal "above" a supercompact cardinal, which is a very large cardinal.

I'm seeking the reason why such phenomena are observed and expecting that Souslin trees will play a crucial role in analysis.

とりあえずはてな記法よりまし。

flymakeすげえ

flymake名前は聞いたことあったけど使ってみたらヤバかった。

とりあえず、infoとして
にゃあさんの戯言日記:
http://d.hatena.ne.jp/nyaasan/20071216/p1
からとって来ました。

CC-modeだけでは寂しいので、gaucheと連携させたい、というところで、
Higepon's blog - Mona OS and Mosh -- 小黒さんのSchemeにおけるglint + Emacs + flymake を試してみた:
http://d.hatena.ne.jp/higepon/20080309/1205043148
を参照。

glintって何じゃぽんということで、gaucheで書かれたschemeのcodecheckerらしいです:
glint
インストールの手順はここからcodechek-0.1.2.tgzを落として、
Ubuntuだったらapt-getでgauche-devを入れた上で、

$ gauche-package install --install-as=root codecheck-0.1.2.tgz

あとは、前の記事のスクリプト.emacs.elに追加します。

あと気になるのは、LaTeXでして、参考にしたのは、
yamblog -- latex用flymake

最後に自分の.emacsを晒して終わりにします:
https://gist.github.com/srbmiy/5127520


うおぉ、時間ない。