kb84tkhrのブログ

何を書こうか考え中です あ、あと組織とは関係ないってやつです 個人的なやつ

睡眠時間

今日は仕事が遅くなってちょっと遅めの帰宅
といってもつい5〜6年くらい前まではこれくらいが普通だった気がする
よく働いてたなあ
ちゃんと働けてたんだっけ
いつも眠かった気がする

今でも睡眠時間は6時間半くらいでもっと寝たいくらいだもんなあ

最近は「あ、頭働いてない」というのがよくわかるように
なってきた気がします
もしかしたら昔は頭が働いてないのが常態で
気が付きようがなかったのかもしれません

8時間寝たらもっと頭が働くようになったりするのかなあ
5時半に起きてるので8時間寝るということはえーと9時半に寝るのか
子供より先に寝なきゃだな
それに定時帰りしても何かする時間がなくなっちゃう気がするけど・・・?

睡眠8時間、仕事8時間、あとウチの会社は昼休みが8時間の内に
入ってないから昼休みで1時間、通勤は往復で2時間半
朝ごはん・晩ごはん・お風呂・歯磨きでどれくらいかなあ
1時間半とすると残り3時間

けっこう残るもんだな
残らないのはまだ無駄な時間があるってことか

8時間睡眠・・・
1週間くらい試してみる?

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (21)

定義24 "変数"vはxのn番目の場所では"束縛"されている

(define (IsBoundAt v n x)
  (and (IsVar v)
       (IsForm x)
       (∃ a b c ≦ x (and (= x (** (** a (ForAll v b)) c))
                         (IsForm b)
                         (<= (+ (len a) 1) n)
                         (<= n (+ (len a) (len (ForAll v b))))))))

変数が束縛されるのは∀v(b)の形でbの中にvが含まれているとき、と

bの中にまた∀v(c)があっても大丈夫かな?
束縛されてることには変わりないからいいのか

定義25 "変数"vはxのn番目の場所では"束縛"されてない

(define (IsFreeAt v n x)
  (and (IsVar v)
       (IsForm x)
       (= v (elm x n))
       (<= n (len x))
       (not (IsBoundAt v n x))))

いろいろチェックがついてますが見たまま

定義26 vはxの"自由変数"である

(define (IsFree v x)
  (∃ n ≦ (len x) (IsFreeAt v n x)))

xのどこでもいいから1箇所でもvがFreeに現れていれば

さて、動かすのをあきらめてみるともうほとんど書き写してるだけっていう状態ですが
これでいいんでしょうか

英語を話すのがグローバルか

主語が大きいって言われそうですが日本人ってほんとに英語の勉強が好きですね
グローバルだから英語だと

まあそれを完全に否定するわけではないんですけど
本当にかっこいいのは、世界中の人が
この人のいうことを聞きたい、直接会話したいけど
あの人は日本語しか知らないから自分が日本語を覚えて日本に行こう、
って思ってもらえるような人ですよね

具体的にこの人がそう、ってのがあるわけじゃないんですけど
人じゃないですが日本のアニメってそんな感じですよね
それが人になった感じ 

まあそんなことをいいつつも子供にはチャレンジイングリッシュを
やらせてたりするんですけどね
いやほんとは古文とか漢文とかやった方が面白いんじゃないかと
思って誘導したりしてたんですけど失敗しました

で英語がそこそこできるようになるとグローバル人材の次のステップは
欧米風な仕事のやり方を覚えたりキリスト教や世界史を覚えて
あっちの人と格調高い会話しましょう、みたいな流れがあるみたいです
よくわかってませんが

自分も海外関連の仕事するようになっていろいろ興味が出たし
それはそれでいいと思うんですけど

自分たちがあっちの仕事のやり方を覚えたりキリスト教や西洋史を
勉強したりしても結局アッチの土俵で戦うみたいなことになっちゃって
そこで対等以上になるのってたいへんですよね

日本の仕事のやり方、おかしいところもあるけど
いまだに海外から研究されているようなところもあるし
日本の仕事のやり方を輸出するくらいの勢いでありたいと思います

歴史や宗教でも日本の方をよく知ってて
「へーキリスト教ではそうなんだ日本の神道ではこうだよ」とか
言えたほうがお互い楽しそうな気がします

そういうわけで子供には(マンガ版だけど)古事記とか日本の古典とか、
ちはやふるとかとめはねっ!とか読ませているわけです(なんか違ってきた

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (20)

前回の記事についてTwitterで泣きを入れてみたところ
なんと結城先生直々にリプいただけました
2乗が出てくるからくりがつかめました

いただいたリプ

ゲーデル 不完全性定理 (岩波文庫)

ゲーデル 不完全性定理 (岩波文庫)

 

ではゆっくり考えてみます

xにいたる論理式列の長さは、xの部分論理式の総数以下である

「部分論理式」というのが何なのかは書いてありませんが
論理式の中に含まれる、論理式の形をした部分ということでしょう
前回ちょっと作ってみた∀z1((¬(x2(0)))∨(y2(f0)))で言えば
(¬(x2(0)))∨(y2(f0))y2(f0)¬(x2(0))x2(0)がそれにあたると思われます、
あ、数学っぽく考えれば∀z1((¬(x2(0)))∨(y2(f0)))自身も含んでそうですね
そうすると5つ

この場合、論理式列の長さは以下の通り5ですから一致してますね

x2(0) | ¬(x2(0)) | y2(f0) | (¬(x2(0)))∨(y2(f0)) | ∀z1((¬(x2(0)))∨(y2(f0)))

論理式の生成ルールを1回適用すると論理式列がひとつ長くなると同時に
新しい論理式がひとつでき、
捨てない限りその論理式はxに現れるはずですから部分論理式となります
なので通常は論理式列の長さと部分論理式の数が一致しそうです

論理式列の長さが部分論理式の総数より少なくなるのは・・・
えーと?またわからない?

じゃあ部分論理式はどれくらい作れるのかと考えてみると

長さ1の部分論理式:(たかだか)(len x)

∀z1((¬(x2(0)))∨(y2(f0)))だと、z1(、・・・が
部分論理式になりうるとして
最大限に見積もってもxの長さまでしかないですよ、ってこと
実際には長さ1の論理式はありえませんが

いや、論理式の形をしてなくても数えるルールなのかな?
それなら論理式列の長さの方が短くなる
「たかだか」がついてるのは((のように一致するものは
ひとつと数える、とか?

同様にして

長さ2の部分論理式: (len x)-1個  (∀z1 z1( ((・・・)
長さ3の部分論理式: (len x)-2個  (∀z1( z1(( ((¬・・・)
:
:
長さ(len x)の部分論理式: 1個 (∀z1((¬(x2(0)))∨(y2(f0))))

合計で(len x)×((len x)+1)/2個 ≦ (len x)^2、となるので
論理式の列の長さは(len x)^2を超えることはない

というのが2乗のでてくるしくみでした
実際のところは2乗のオーダじゃないと思いますがそこは割り切ってるんでしょうね

66日(以上)経過

行動が習慣になるまでにかかる日数は平均66日 

小さな習慣

小さな習慣

 

66日はいつのまにか過ぎてました
続いてるのは続いてます

ほんとにいつのまにか、って感じで、がんばって達成したという感じではありません
小さな習慣なんだからそんなものでしょう
ダレてるような気もするし日常になった気もします
まだほっといてもついついやっちゃうレベルに達している感じはしません

これはあくまでも平均値で、実際には18日から254日と大きな幅がありました。 

完全な習慣化までのどのへんに位置しているのかなあ
といっても「本日完全な習慣化を達成しました!おめでとうございます!」みたいな
瞬間があるわけじゃないのはわかってるんですけど

習慣になる前の最初の兆しはやりたくないという抵抗が弱まることです。

いつもやりたくなくってやめてたのかというとちょっと違う気もするんですが
とりあえずやっておくか、という気分はあります
以前はちゃんとやる時間がないからやらない、からいつのまにかやらなくなった、
へのコンボがほとんど成功してましたからよくなっているとは言えそうです

あと、せっかく続いてるし、っていう気分は出てきてますね

ほんとうに重要なのは、行動が習慣になる兆しを見逃さないことです。

この気分は兆しなのか
それともちょっとダレ気味に日常化している気分が兆しなのか
はたまたまだ兆しは現れていないのか

その一方、無理するほど詰め込んでるわけではありませんが
微妙に時間が不足してとりあえず達成だけしておくっていうことが
ちょくちょくあることは気になっています
もうちょっとできそうだけど小さな目標を達成したからまあこれでいいや、みたいなの

新しくできた"赤ちゃん神経経路"は、同じ行動を繰り返すうちに成長を始め、やがて以前からの行動と競争するようになります。

何も変えずにやることだけ増やすっていうのはやっぱりありえないんですよね
競争して負けてほしい以前からの行動ってなんだろう
平均で見ると少し仕事から帰るのが早くなったかもしれません

次の振り返りはいつだろう?半年くらい?

 

 

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (19)

まだちょっとすっきりしない

M23をもういちど考え直す

(define (M23 x)
  (expt (P (sqr (len x))) (* x (sqr (len x)))))

(define (IsEndedWith n x)
  (= (elm n (len n)) x))

(define (IsForm x)
  (∃ n ≦ (M23 x) (and (IsFormSeq n)
                      (IsEndedWith n x))))

見間違えだったりしないよな・・・大丈夫なはず

(M23 x)
最後の要素がxと一致する、"基本論理式"から組み上げた"論理式"の列、
ゲーデル数の上限

この論理式の列をE1、E2、・・・、En(=x)と書くことにすると
そのゲーデル数は2^E1*3^E2* ... *Pk^Ek* ... *Pn^En

Pk(1≦k≦n)≦Pnは明らか

そしてNotOrForallはすべて与えられた論理式に記号を
追加するので組み立てられていく論理式は長くなっていく一方
作ったけど使わないといった無駄なことをしない限り
登場する論理式の中ではxが最大となるはず

したがって

2^E1* 3^E2* ... *Pk^Ek* ... *Pn^En

Pn^ x*Pn^ x* ... *Pn^ x* ... *Pn^En

を超えることはないと言える
ここまでは問題ない
あとはn(len x)^2を超えないことを言えればいいんだけどここが問題

どうにもイメージが湧かないのでいったん定義に戻って考え直す

Ekは

(A) 基本論理式 a(b) である
か、すでに組み立てられた論理式Ei、Ej(1≦i,j≦k)を使っった以下の式のいずれか
(B1) ¬(Ei)
(B2) (Ei)∨(Ej)
(B3) ∀v(Ei)

ちょっくら具体的に作ってみる

(1) x2(0) : (A)より
(2) ¬(x2(0)) : (1)と(B1)より
(3) y2(f0) : (A)より
(4) (¬(x2(0)))∨(y2(f0)) : (2)(3)と(B2)より
(5) ∀z1((¬(x2(0)))∨(y2(f0))) : (4)と(B3)より - Xとする

(len X)=24だから(len X)^2=576
5ステップで作った論理式のステップ数の上限が576っていうんだからかなり富豪
ていうか2乗してなくても富豪

(A)〜(B3)までを論理式の長さの点から見てみる

(A) 基本論理式は最低4記号からなる
(B1) 与えられた論理式に¬、(、)の3記号を追加
(B2) 与えられた論理式に(、)、∨、(、)の5記号を追加
(B3) 与えられた論理式に∀、v、(、)の4記号を追加

ゲーデルの証明の中では無駄な論理式を作って捨てるようなことはしないと
考えて問題なさそうなので
そうすると作った論理式が縮んだり消えたりすることはなく
(A)で導入した基本論理式や(B1)〜(B3)で追加した記号はすべて
xの中に現れる(はず・・・)

逆に、与えられた論理式を組み立てるための列もなんら悩むことなく構成できそう

そう考えると、列の要素がひとつ増えるたびに、最終的にできあがる論理式は
最低でも3記号分増えることになる
つまりnの上限は(len x)÷3ってことになってしまう
大雑把な上限の話をしてるんだから÷3は省くとしても
2乗がついてるのはさすがに意味があるはずだよなあ

ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (18)

「10.8.4 変数・記号・論理式」の続き

なにごともなかったかのように続けてみる

定義23 xは論理式である

(define (M23 x)
  (expt (P (sqr (len x))) (* x (sqr (len x)))))

(define (IsEndedWith n x)
  (= (elm n (len n)) x))

(define (IsForm x)
  (∃ n ≦ (M23 x) (and (IsFormSeq n)
                      (IsEndedWith n x))))

M23はいったいどういう意味だろう

まずIsFormから考えてみる
nが"基本論理式"から組み上げた"論理式"の列で、nの最後の要素がxと一致する、
ってことだな

これとM23の形を見比べてみる
(sqr (len x))番目の素数を使ってるところを見ると、
論理式の列の長さは長くても(sqr (len x))だと言いたいのでしょう

そしてそれぞれの論理式は基本論理式かまたはそれまでに出現した論理式をもとに
NotOrForallで作られ、最終的にできあがるのがxなので
無駄さえなければxが最大であるはず

つまりここで(P (sqr (len x)))Pとk書くことにすると
まじめに計算すれば2^?*3^?*5^?*...*P^?となるところを
上限が大きくて困ることないよね!と
P^x*P^x*P^x*...*P^xにしてしまってるということのように思われます

ということはあとはxを作るのに必要な論理式の数が多くても
(sqr (len x))だとわかればいいわけですがうーん
xに含まれる記号が(len x)個で、
ありえないけど仮にすべての記号が1文字からなる論理式であるとして、
その論理式を組み立てるのには最大でも(len x)個の論理式からなる列があればよい、
ってことかなあ
まだちょっとすっきりしない