kb84tkhrのブログ

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

2017-10-01から1ヶ月間の記事一覧

辞書引き学習ってありますね

自分はあんまり辞書とか引かずに来た人なんですけどねだいたい想像で済ませちゃう感じ辞書こまめに引いてる博学な感じの人に憧れを感じたり で、辞書引き学習ってのがちょっと気になってたんですけど娘はやっぱり自分に似たのか、辞書にはあんまり興味を引か…

Workflowyに戻りました

微妙な違和感を感じつつ使っていたDynalistからWorkflowyに戻りました その前にほぼ1ドキュメントにまとめていたのでデータ移行はExport→コピー→Workflowyでペーストでおしまいです その後ちょっと整理し直しましたがDynalist風の記法はまあそのままでも読め…

髪の色の件ですが

生まれつき茶色い髪を黒く染めさせた学校が話題になってますね ところでウチの娘は規則にうるさい派自分から風紀委員になりたいというほど南みれいに憧れてとかいうわけでもなくもとからそんな感じ ちょっと気になったので、こういう話があるんだけどどう思…

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

定義43 xはaとbの"直接の帰結"である (define (IsConseq x a b) (or (= a (implies b x)) (∃ v ≦ x (and (IsVar v) (= x (ForAll v a)))))) ところで推論規則って、これだけで足りるんですか 論理学とか見ると、もっといろいろ書いてあるっぽいんですけど 推…

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

ElementForm周辺が盛大にバグってました ぐぬぬ 変数と、ひとつの変数だけからなる列が混乱しまくってる どっちも整数だけど、別の型として扱ってれば検出できたかな でもさらっと考えて見るとこのプログラムって型付けしにくそうだな もう少しでひととおり…

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

定義37 zは、yの中でvが"自由"な範囲に、"束縛"された"変数"を持たない (define (IsNotBoundIn z y v) (not (∃ n ≦ (len y) (∃ m ≦ (len z) (∃ w ≦ z (and (= w (elm z m)) (IsBoundAt w n y) (IsFreeAt v n y))))))) こういうの見るとつい 束縛が入れ子にな…

まだDynalist使ってますが

どうもドキュメントだとかフォルダとかに馴染めず結局ひとつのドキュメントに全部寄せてしまってますちがうドキュメントにあると目につかないんですよねー そこがいいという人もいると思いますが自分はときどき目につくほうがいいと思ってますDynalistでも全…

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

定義35 xは公理II-nから得られる"論理式"である 定義36 xは公理IIから得られる"論理式"である (define (IsSchemaII n x) (case n ((1) (∃ p ≦ x (and (IsForm p) (= x (Implies (Or p p) p))))) ((2) (∃ p q ≦ x (and (IsForm p) (IsForm q) (= x (Implies p…

1行書けばいいと言ってもね

小さな目標で1行でいいから書くといってもこれがまた簡単ではない気がしてきています 達成! というほどはなかなか開き直れず今日はちょっと時間ないから短めに・・・と思うと今度はネタがなかったり書こうと思ってるネタがないわけじゃないんですけど書こう…

今年の作品

月に2回、日曜日に書道教室に行ってましてね今年の作品です

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

もうほとんど「Racketで書いてみる」という部分には意味がなくなっている気がする 今日このごろですが続けます 10.8.5 公理・定理・形式的証明 やっと次の節に入りました 最近はただ式をコードに置き換えてるだけって感じになってましたが どうもそれ以前の…

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

定義32 "(a)→(b)"、"(a)∧(b)"、"(a)⇄(b)"、"∃x(a)"を得る関数 (define (Implies a b) (Or (Not a) b)) (define (And a b) (Not (Or (Not a) (Not b)))) (define (Equiv a b) (And (Implies a b) (Implies b a))) (define (Exists x a) (Not (ForAll x (Not a…

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

ちょっと蒸し返しますけど (define (M23 x) (expt (P (sqr (len x))) (* x (sqr (len x))))) ここって素数指数表現が歯抜けになってないことを前提にしてることになりませんか primeからここまで、歯抜けでもいい流れできてたと思うんですが まあでも、歯抜…

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

定義27 xのn番目の要素をcで置き換えたもの (define (substAtWith x n c) (Min z ≦ (M8 x c) (∃ a b ≦ x (and (= n (+ (len a) 1)) (= x (** (** a (<> (elm x n))) b)) (= z (** (** a c) b)))))) aという列があって aとxのn番目の要素とbをつないだものがx…

睡眠時間

今日は仕事が遅くなってちょっと遅めの帰宅といってもつい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を因…