サウナトランス　その3

一年ぐらいサウナに通っている。いまだに「これ！」といったととのいは得られていない。

自分の好みは大体分かってきた。ドライサウナよりスチームサウナが好きとか、水風呂の温度はあと１℃高くても良いとか、外気浴は気持ちいいとか。

 

そんな中、面白い現象を発見したので報告する。危険な気もするので自己責任で。

 

サウナ5分→水風呂1分→外気浴5分が、定番の1セットだと思うのだが、外気浴に行ったところで、大きく息を吸い、息を止める。

すると、座っているのに立ちくらみのような感覚に襲われる。くら～っとする。

もっとキマると、意識がもうろうとして、手足がびくんびくん痙攣する。

 

非日常感覚を味わえて、気持ち良い。

この現象を、「裏ととのい」と呼ぶ事にしよう。

 

18/04/03追記

マジでやばい気がしてきたので、もうやめよう。

　

　

　

　

　

Agdaのインストール

19/10/13 追記

 

この動画が良い感じだ。
 

 
動画の後で標準モジュールを入れる。
 
・標準モジュールをhttp://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibraryから落としてきて
C:\Users\アカウント名\AppData\Roaming\agda
に置く。（agdaフォルダがなければ作る）
・librariesというファイルを作って中にC:\Users\アカウント名\AppData\Roaming\agda\agda-stdlib-0.17\standard-library.agda-libと書く。
・defaultsというファイルを作って中にstandard-libraryと書く。
コマンドプロンプトで
> agda -I -l standard-library
と打ってエラーが出ずにAgdaが起動すればOK。
 

 
Agdaは管理者権限で実行しないといけない。
 
Emacs for Agdaのショートカットのプロパティで、
「管理者権限としてこのプログラムを実行する」にチェックを入れれば、
.agdaファイルをダブルクリックで開く時も、常に管理者権限で起動する。

19/10/13 追記ここまで



Agda（アグダ）は定理証明器、すなわち数学的な証明を検証するコンピュータプログラムである。
Coqのライバルである。
AgdaをWin10にインストールしてみた。

Haskellのcabalで
> cabal install agda
としてみたけど、なんかエラーが出たのでウイルスセキュリティを止める。

それでやると今度は「mingwかCygwin使え」って言われたので、
mingwのmsysで
$ cabal install agda
とやるとインストールできた。

2時間かかった。w



-----
・標準モジュールをhttp://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.StandardLibraryから落としてきて
C:\Users\[user]\AppData\Roaming\agda
に置く。
・librariesというファイルを作って中にC:\Users\[user]\AppData\Roaming\agda\agda-stdlib-0.12\standard-library.agda-libと書く。
・defaultsというファイルを作って中にstandard-libraryと書く。
コマンドプロンプトで
> agda -I -l standard-library
と打ってエラーが出ずにAgdaが起動すればOK。

-----
http://cha.la.coocan.jp/doc/NTEmacs.html#sec7
emacs-25.1-simple_ime-no_symbol.zip
emacsを入れて、
環境変数HOMEを作って、同じ場所に.emacsを置いて、中に
(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))
と書く。

-----
hello.agdaを作ってemacsで以下を書く。
module hello where
open import IO
main = run (putStrLn "Hello, あぐだworld!")
C-c C-lで型チェックが通ればOK。
(C-c C-x C-c)コマンドでコンパイルすることもできる。

2日かかった。w





サウナトランス　その2

二日連続でサウナに行ってきた俺。
しかし、今日もととのわなかった。　手足のしびれとかはあったんだけどなー

原因を考えてみる。
①サウナに入っている時間が短い
12分計を見てた所（12分計は針が一周すると12分たつ）、8分ぐらいで出てた。
これが限界。10分とか入ってられない。　慣れればいけるようになるだろうか。

②サウナ→水風呂のセットが少ない
昨日今日と3セットやってみたんだが、5セットくらいやる必要があるだろうか。

③メンタル系の薬を飲んでいる
これが大きいんじゃないかと睨んでいる。脳に直接作用する薬だからね。
ととのいの妨げになっているかもしれない。　かといって薬を抜くのはリスクが高いし。

④そもそも自分はととのわない体質なのだ
これだったらあきらめるしかないな。

まあ、ととのわなくても、サウナと水風呂だけでも気持ちいいし、普通のサウナライフを楽しみましょう。
さあ、明日も行くかー（え
　
　　
　
　
　
　　
　


サウナトランス

phaさんのブログ でサウナについての記事があった。
僕もそろそろ37だし、「サウナトランス」というものを体験できるらしいので、
近場のスーパー銭湯に行ってみることにした。
あと、ここ の記事も良かった。

サウナに入ると、むっちゃ暑い。鼻で息をすると良いとあったが、熱気が鼻腔を刺激する。
体内時計で10分くらいたったかな～って頃にサウナ室を出る。
（12分計の見方が分からなかった）

水風呂つめた～い。我慢して肩までつかる。
おお、意外といけんじゃん。「温度の羽衣」をまとえてたのかな。
サウナより水風呂のほうが心地よい。　5分くらい浸かってたかな。

これを3セット繰り返した。

サウナを出てコーヒー牛乳を飲みながらリラックスタイム。

だが……


ととのわねええええーーーーー
何も起こらねーぞ。

30分くらい甲子園の決勝を見ながらぼーっとしてたが変化なし。
仕方なく煙草を吸って家路についた。

あれかな、サウナに入っている時間が短かったのかな。
さあ、明日も行くか、どうするか。
　
　
　
　
　
　　
　
　
　
　

　

どうぶつしょうぎ

どうぶつしょうぎに最近はまっています。
3*4のマスで、駒は4種類しかないけど、結構奥が深いです。

どうぶつしょうぎ/幻冬舎エデュケーション
￥1,543
Amazon.co.jp

僕はAndroidのケータイを持っているので、アプリで遊んでいます。
おすすめのアプリを2つ紹介します。

さくさく将棋
普通にCOMと対戦ができます。僕はまだEasyLevel5までしかいってません。

どうぶつしょうぎ大全
こちらは対戦はできませんが、1手ごとに先手後手の優劣が分かります。

さくさく将棋で棋譜をつけながら対戦して、
その結果をどうぶつしょうぎ大全で解析するのが良いと思います。
　
あと、定跡はここのサイトに詳しいです。
xawa雑記帳: どうぶつしょうぎ
　
　
　
　
　

停止性問題から不完全性定理へ

ほとんどWikipediaの写しだけど……

「停止性問題の決定不能性定理」とは、停止性問題を常に正しく解くプログラムは存在しない、という定理である。
すなわち以下の性質を満たすプログラムHは存在しない、という定理である。

全てのプログラムAと全てのデータxに対し、
・A(x)の実行は停止する ⇒ H(A,x)はYESを出力する。
・A(x)の実行は停止しない ⇒ H(A,x)はNOを出力する。

証明

停止性問題を解くプログラムHが存在すると仮定して矛盾を導く。
M(A)を、H(A,A)=YESなら停止せず、H(A,A)=NOなら
0を出力して停止するプログラムとする。
(H(A,A)と無限ループを組み合わせる事でM(A)を作る事ができる。)

M(M)は停止するだろうか？
・M(M)が停止したとすると、Mの定義よりH(M,M)=NO。
Hの定義よりH(M,M)=NOとなるのはM(M)が停止しないときのみなので、矛盾。
・M(M)が停止しないとすると、Mの定義よりH(M,M)=YES。
Hの定義より、H(M,M)=YESとなるのはM(M)が停止するときのみなので、矛盾。

よって停止性問題を解くプログラムHは存在しない。


ここからが本題です。
停止性問題の決定不能性を利用して
ゲーデルの第一不完全性定理を示すことができる。のです。

halt(A,x)を、A(x)の実行は停止する、をあらわす述語とします。
もし、ある体系Tが、任意の文を証明または反証するならば、
(A,xを入力として)Tの定理を枚挙するプログラムを走らせて、
(いつかはhalt(A,x)もしくは￢halt(A,x)の定理があらわれるので)
　・halt(A,x)があらわれた ⇒ YESを出力する。
　・￢halt(A,x)があらわれた ⇒ NOを出力する。

という方法で停止性問題が肯定的に解けてしまう。
これは停止性問題の決定不能性に反するので、
Tでは証明も反証もできない文が存在しなければならない。

ということです。
本当はTのΣ1健全性とΠ1健全性を言わなきゃいけないとかあるらしいのですが、
(僕が分からないので)スキップします。





ゲーデルの不完全性定理

ゲーデルの不完全性定理を証明するには、数学の体系内で「対角化」とか「証明できない」
といった述語を構成しないといけないのですが、ここではスキップします。

次の文を考えます。
「xの対角化は証明できない」の対角化は証明できない　---Gとおく
「xの対角化は証明できない」の「対角化」は、
「xの対角化は証明できない」の対角化は証明できない　ですから
(「対角化」は述語を2回重ねる事に注目)、
文G　=　Gは証明できない
となります。これで自己言及文が作れました。

「Gは証明できない」を証明したいので、背理法で考えます。
Gは証明できる　と仮定します。(仮定1)
->「Gは証明できない」が証明できる　__________※Gを展開
->Gは証明できない　__________※Aが証明できる->Aである　を使っています
Gは証明できる、かつ、Gは証明できない、だから矛盾
よって(仮定1)が否定されて、「Gは証明できない」となります。

「￢Gは証明できない」を証明したいので、背理法で考えます。
￢Gは証明できる　と仮定します。(仮定2)
->「Gは証明できない」の否定が証明できる　__________※Gを展開
->「Gは証明できる」が証明できる
->Gは証明できる　__________※Aが証明できる->Aである　を使っています
->「Gは証明できない」が証明できる　__________※Gを展開
->Gは証明できない　__________※Aが証明できる->Aである　を使っています
Gは証明できる、かつ、Gは証明できない、だから矛盾
よって(仮定2)が否定されて、「￢Gは証明できない」となります。

「Gは証明できない」「￢Gは証明できない」という事が分かりました。
以上がゲーデルの不完全性定理のエッセンスです。