kb84tkhrのブログ

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

睡眠時間

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

ゲーデルの不完全性定理の証明のアレを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)))))))) 変数が束縛…

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

主語が大きいって言われそうですが日本人ってほんとに英語の勉強が好きですねグローバルだから英語だと まあそれを完全に否定するわけではないんですけど本当にかっこいいのは、世界中の人がこの人のいうことを聞きたい、直接会話したいけどあの人は日本語し…

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

前回の記事についてTwitterで泣きを入れてみたところ なんと結城先生直々にリプいただけました 2乗が出てくるからくりがつかめました いただいたリプ 「部分論理式の総数」で押さえているようです。添付画像は岩波文庫『不完全性定理』の当該部分(ゲーデル…

66日(以上)経過

行動が習慣になるまでにかかる日数は平均66日 小さな習慣 作者: スティーヴン・ガイズ,田口未和 出版社/メーカー: ダイヤモンド社 発売日: 2017/04/27 メディア: 単行本(ソフトカバー) この商品を含むブログ (1件) を見る 66日はいつのまにか過ぎてました…

ゲーデルの不完全性定理の証明のアレを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)))) 見…

ゲーデルの不完全性定理の証明のアレを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…

失敗してみせる

これな 有料記事だけど見えるところだけでだいたいわかります(ウチは読売取ってるので紙で読んだ) 要は、大人が苦労してなにかをやりとげてるところをみた赤ちゃんのほうが簡単にやってるところを見た赤ちゃんよりも粘り強く行動するって話いかにもありそ…

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

「10.8.4 変数・記号・論理式」の続き 定義22 "基本論理式"から組み上げた"論理式"の列である うーナントカ以下じゃなくてナントカ未満のパターンもあったか まあいいやとりあえず1引けばおんなじことだし (define (IsFormSeq x) (and (> (len x) 0) (∀ n ≦ …

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

「10.8.4 変数・記号・論理式」の続き 定義21 "¬(a)"または"(a)∨(b)"または"∀v(a)"である とりあえずそのまま (define (IsNotOp x a) (= x (Not a))) (define (IsOrOp x a b) (= x (Or a b))) (define (IsForallOp x a) (∃ v ≦ x (and (IsVar v) (= x (ForAl…

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

「10.8.4 変数・記号・論理式」の続き 定義20 xは"基本論理式"である (define (IsElementForm x) (∃ a b n ≦ x (and (IsNthType a (+ n 1)) (IsNthType b n) (= x (** a (paren b)))))) 遅いのでなんとかしましょう 全然ダメなのも含めて全部総当りでやるの…

考える力がないわけじゃないと思うんですが

ウチの子に考える力がないと思ってるわけじゃないんですけどね考える「習慣」がないかなーとは思ってます 自分はそもそも、「考える」ってなんだかわかってなかった気がしていて見て答えが思い浮かべば「わかる」そうでなければ「わからない」くらいしか考え…

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

「10.8.4 変数・記号・論理式」の続き 定義20 xは"基本論理式"である 変数が三つになった ぐぬぬ さすがに3つめのパターンを追加するというわけにもいくまい Fear of Macrosになんかあったな・・・いやないな じゃあSMPHにも・・・あれないな どっかで再帰…

DynalistのGoogle Calendar Integrationを(ちょっとだけ)試す

DynalistにはGoogle CalendarとSyncする機能がありますただしProの機能手帳派なのでスマホのカレンダーとか使ってないんですけどDynalist Proの試用期間が今日で終わりってことに気づいて急ぎでちょっとだけ試してみることにしました面白そうだし まずは準備…

アラン・ピーズ、バーバラ・ピーズ『自動的に夢がかなっていく ブレイン・プログラミング』

本屋でふと手に取ったこの本 自動的に夢がかなっていく ブレイン・プログラミング 作者: アラン・ピーズ,バーバラ・ピーズ,市中芳江 出版社/メーカー: サンマーク出版 発売日: 2017/08/10 メディア: 単行本(ソフトカバー) この商品を含むブログを見る 『話…

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

「10.8.4 変数・記号・論理式」の続き さて前回、勘違いに気づくまではもっと高速化しないとと思って 素因数分解する版を書き始めてました 乗った船なので続けてみます 素因数分解は12を((2 . 2) (3 . 1))と表現してみました ((0 . 0))というのは0とか1を因…

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

「10.8.4 変数・記号・論理式」の続き 定義18 "第n型の記号"である (define (IsNthType x n) (or (and (= n 1) (IsNumberType x)) (and (> n 1) (∃ v ≦ x (and (IsVarType v n) (= x (<> v))))))) さて高速化 もともと、#tが帰るようなときは遅くないんです…

プリンキピアからのニュートン

プリンキピアといってもこれですが プリンキピア:マスター・オブ・サイエンス Shin Hirota ゲーム ¥360 App Storeで見かけてピンと来て購入しましたニュートンが活躍してた時代のヨーロッパを舞台としてたくさんの科学者が競って研究するというシミュレーシ…

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

「10.8.4 変数・記号・論理式」の続き 時間がかかるのはいつものパターンで書き換え (define (IsNumberType x) (let loop ((k 1)) (let ((e (elm x k))) (cond ((not (= e cf)) (and (or (= e c0) (IsVarType e 1)) (= (elm x (+ k 1)) 0))) (else (loop (+ …

今のところWorkflowyな気持ち

Dynalist https://dynalist.io/ っていうアウトライナーのサービスがあります 後発だけあってWorkflowyの上位互換的なサービスになってます Dynalistいいかも - kb84tkhrのブログ ということでDynalistを試用してますが今のところの印象は、まだWorkflowyの…

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

「10.8.4 変数・記号・論理式」の続き 定義16 xの、n番目の後続数 定義17 nに対する"数項" (define (succ n x) (cond ((= n 0) x) (else (** (<> cf) (succ (- n 1) x))))) (define ( ̄ n) (succ n (<> c0))) 数項の" ̄"はちょっと無理がある気もしますが気…

とにかく達成

月末で半期末な金曜日ですが普通に定時退社して友人と飲み会へさて今日の小さな習慣を 書くネタはいくつかストックしてるんですけど、書こうと思うくらいの話は書き始めると5分で終わるとは行かなくなってしまいますブログ書いてもあと三つあるし そうか、飲…

微妙に時間が取れてないけど

今週はちょっと残業とかあって微妙に時間が取れてないんですがとりあえず小さな習慣分だけはクリアしてますていうかもうちょっとやってます 本来やろうと思ってる分に比べると少ないんですけどまあいいかなと でもこれが常態化しちゃったらダメなんでしょう…

後付けのルールを押し付けない

子供に後付けのルールを押し付けないように心がけています ウチは週末ほぼ必ず本屋に行くんですがそこでよく見かけるのが本を読んでる子供のところへ親が寄ってきて「ほらもう帰るわよ!いつまで読んでるの!」と言ってる風景 これの何が後付けかってことな…

Dynalistいいかも

Dynalist https://dynalist.io/ っていうアウトライナーのサービスがあります 後発だけあってWorkflowyの上位互換的なサービスになってます 無償で無制限のアイテムを作成可能なのがうれしい しかも申し込んでしばらくはProの機能が使えます 無償でも十分使…

(オッサンにとっての?)真理

食べ過ぎると体力を消費します背筋が苦しくなったり翌日疲れが出たり なんてことを思うようになったのは年を食ってからですかね学生の頃は焼肉食べに行けば当然食べ放題目の前に肉がある限り食べるっていう感じでしたいつの間にか食べ放題にするより量は少な…

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

「10.8.4 変数・記号・論理式」の続き ものは試しでprimeをこんな風にしてみました (define (prime n x) (let ((p (P n))) (if (CanDivide x p) p 0))) 素因数分解には必ず2から歯抜け無しで素数が出てくるという前提動かしてみると > (profile (paren (<> 7…

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

「10.8.4 変数・記号・論理式」 ここらへんから証明っぽくなってきます 定義11 xは"第n型"の"変数"である (define (IsVarBase p) (and (> p crp) (IsPrime p))) (define (IsVarType x n) (and (>= n 1) (∃ p ≦ x (and (IsVarBase p) (= x (expt p n)))))) こ…

2種類のキレイ好き

世界には2種類のキレイ好きがいるようですね ひとつめのキレイ好きは、そのまんまですがキレイだとうれしくて掃除するのも楽しいというタイプキレイ好きと言って思い浮かべるのはこっちでしょうか もうひとつのキレイ好きは、キレイなのが好きというより汚…

ハーディ『ある数学者の弁明』私家版翻訳、ですってよ

ハーディっていう数学者がいまして、自分には数学自体の功績よりもラマヌジャンを見つけて育てたっていう方が印象的な人なんですがなんかユニークな人でもあったみたいでこの人の書いた「ある数学者の弁明」って本が面白そうだな―読んでみたいなーと思ってい…