失敗してみせる
これな
有料記事だけど見えるところだけでだいたいわかります
（ウチは読売取ってるので紙で読んだ）
要は、大人が苦労してなにかをやりとげてるところをみた赤ちゃんのほうが
簡単にやってるところを見た赤ちゃんよりも粘り強く行動するって話
いかにもありそうな話
っていうのはまず自分の話からすると
失敗するのを見られるのが嫌で、失敗するくらいなら始めからやらない、って
ところがあります
（失敗しても取り繕って失敗してないふりをするとかもある）
（たぶんバレバレだけど）
で、育て方だったのか遺伝なのか、ウチの娘もそっくり同じ
勉強にしろ遊びにしろ、ちょっと難しいかも、と思うと手を付けようとしません
あーここは自分に似たな、難しいことにも挑戦してほしいな、と思って
「失敗してもいいんだよ」くらいは言ってあげるんですが
それくらいでは決心がゆらぐことはありません
で、また違う話をすると
子供に何かさせようとするときは、○○しなさいって言うよりも
親が○○してるところを（繰り返し）見せるほうが効果があると思ってます
なのでことさら本とノートとペンを持って子供に見えるところで
勉強してたりとかします
つまり
失敗してもいいから難しいことにも挑戦してほしい、というなら
自分が難しそうなことに何度も挑戦して失敗してるところ（そして
最後に成功してるところ）を見せるべきなんじゃないかと
親が何でもスイスイできてるのに自分はなかなかできない、って
いうんだと確かに挑戦する気が起きなくなっても不思議はないよなあと
ということに気づいたのがわりと最近
しかしまあこれが難しい
上に書いたような人なんでどうやって失敗するかなんて考えたこともないし
（まあ普通ないと思いますけど）
演技で失敗するとか発想が浮かびません
勉強してるときはしょっちゅう行き詰まってるんですけど
そこまで理解してくれっていうのもまだちょっと難しい気がする
難しい難しいどうしたらいいんだこれもだめこれもだめとか
口に出して言ってみるとか？
パパわかんないんだけどいっしょに考えて、ってお願いしてみるとか？
実際できそうにない難しい目標を立てて挑戦してるところを見せる？
どうしたらいいかなあ？
ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (17)
「10.8.4 変数・記号・論理式」の続き
定義22 "基本論理式"から組み上げた"論理式"の列である
うーナントカ以下じゃなくてナントカ未満のパターンもあったか
まあいいやとりあえず1引けばおんなじことだし
(define (IsFormSeq x)
(and (> (len x) 0)
(∀ n ≦ (len x)
(⇒ (> n 0)
(or (IsElementForm (elm x n))
(∃ p q ≦ (- n 1)
(and (> p 0) (> q 0)
(IsOp (elm x n) (elm x p) (elm x q)))))))))今回は列の列を相手にするということでかなりつらいはず・・・
一番簡単な「"基本論理式"から組み上げた"論理式"の列」であるx2(0)で
> (IsFormSeq (gnum (gnum (var 1 2) clp c0 crp)))
Interactions disabledふむ
> (gnum (gnum (var 1 2) clp c0 crp))
out of memory ここのゲーデル数を求める時点でもうアウト
> (gnum (var 1 2) clp c0 crp)
85358558703482190127297085877476961847445387329503425822247990708594951927598812588177312402905487114240ということは2の85358558703482190127297085877476961847445387329503425822247990708594951927598812588177312402905487114240乗ってことだもんな
ループの回数を減らすことはできてもゲーデル数を小さくするわけにはいかないもんなあ
完全に詰み
いったん逃避して
(define (IsFormSeq x)
:
(∃ p q ＜ n
:と書けるようにしますかね
≦が全角なので＜も全角にしました ただの気分
(define ≦ #f)
(define ＜ #f)
(define-syntax (define-equipment stx)
(syntax-parse stx
((_ name term notfound found)
#:with fname (format-id stx "~a≦" #'name)
#'(begin
(define (fname max f)
(let loop ((x 0))
(cond ((> x max) (notfound x))
((term (f x)) (found x))
(else (loop (+ x 1))))))
(define-syntax (name stx)
(syntax-parse stx
#:literals (≦ ＜)
[(_ v:id ≦ max:expr body:expr)
#'(fname max (λ (v) body))]
[(_ v:id ...+ vn:id ≦ max:expr body:expr)
#'(name v (... ...) ≦ max (fname max (λ (vn) body)))]
[(_ v:id ＜ max:expr body:expr)
#'(fname (- max 1) (λ (v) body))]
[(_ v:id ...+ vn:id ＜ max:expr body:expr)
#'(name v (... ...) ＜ max (fname (- max 1) (λ (vn) body)))]))))))原始的にやりました
パターンが繰り返しになっているのは気になるところ
パターンがまだ増えるようならまた考えるかも
ゲーデルの不完全性定理の証明のアレを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 (ForAll v a)))))
(define (IsOp x a b)
(or (IsNotOp x a)
(IsOrOp x a b)
(IsForallOp x a)))案の定IsForallOpが（#fになるときに）遅いので書き直し
(define (IsForallOp x a)
(let ((v (elm x 2)))
(and (IsVar v)
(= x (ForAll v a)))))今日はこれだけ！
ゲーデルの不完全性定理の証明のアレを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))))))遅いのでなんとかしましょう
全然ダメなのも含めて全部総当りでやるのがなにしろ無理があるんだよな（n回目）
記号をひとつずつ見ていって正しい形かどうか確認すればいいかな
(define (IsElementForm x)
(and (IsVar (elm x 1))
(= (elm x 2) clp)
((IsNthType <xの3番目〜(- (len x) 1)番目の要素>
(- <(elm x 1)の型> 1))
(= (elm (len x)) crp)))てことだけどこれどう書くといいのかなあ
第2型以上は全部変数ですので「(elm x 1)の型」はこんな関数で取れます
(define (VarType x)
(factor-expt (car (factorization x))))「xの3番目〜(- (len x) 1)番目の要素」はどうしましょうねえ
とりあえずそのまま書いてみましょうか
あんまりうまくないやり方な気はしますけど、具体的に困ってから考えることにします
列のs番目からe番目までの記号を取り出した列を作ります
(define (ExtractSequence x s e)
(let ((f (factorization x)))
(apply gnum (map factor-expt (drop (take f e) (- s 1))))))リスト相手だとパーツがそろってて楽だなあ
全部リストでやりなおしてみる？
遅延リストになるかな？
でもここはそのまま突っ切る
(define (IsElementForm x)
(let ((l (len x)))
(and (>= l 4)
(let* ((a (elm x 1))
(b (ExtractSequence x 3 (- (len x) 1)))
(n (VarType a)))
(and (IsVar a)
(= (elm x 2) clp)
(IsNthType b (- n 1))
(= (elm x (len x)) crp))))))動いた
これくらいになってくると元の式と同じ仕様になっているかどうか不安
（ほかも不安ですが）
考える力がないわけじゃないと思うんですが
ウチの子に考える力がないと思ってるわけじゃないんですけどね
考える「習慣」がないかなーとは思ってます
自分はそもそも、「考える」ってなんだかわかってなかった気がしていて
見て答えが思い浮かべば「わかる」そうでなければ「わからない」くらいしか
考えてなかったような
思い浮かぶまで時間をかけたりすることはありましたけど
今は、とにかく思いついたことを書き付けていくってことが
「考える」には大事だな、と思ってます
「考える」がわかった、とはとても言えません
まだまだ初心者ですから
そんな自分の性質を強く受け継いだと思われる娘は
「どうしてそうなるのかな？」「どうするとうまくいきそう？」などと
聞くと即時に「わからない」と返してきます
ただし、気をつけなければならないことは、「質問をして、相手が答えられなくてもいい」ということを知っておくことです。
信じていいですか先生
質問されると自動的に頭は考え出しますから、アウトプットの質は問いません。答えなくても頭は動いているということなのです。
考えることを放棄してるような気もするんですが先生
「知らない」と「わからない」の区別がついてない気もするんですよね
「知らない」ことは「わからない」という感じ
あと、「教えてもらってない」＝「知らない」でもあるような気がします
自分がそうだったから
わからない→調べる、とかわからない→考えるの道筋をつけるには
どうしたらいいかなあ
（と思って数学ガールへとなんとか誘導しようとしている）
「わからない」と言われても泣かずに聞き続けようとも思います
ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (14)
「10.8.4 変数・記号・論理式」の続き
定義20 xは"基本論理式"である
変数が三つになった
ぐぬぬ
さすがに３つめのパターンを追加するというわけにもいくまい
Fear of Macrosになんかあったな・・・いやないな
じゃあSMPHにも・・・あれないな
どっかで再帰的にマクロ定義を呼んでる例があったと思うんだけど
こんな感じでいけるかな
(define-syntax (define-equipment stx)
(syntax-parse stx
((_ name term notfound found)
#:with fname (format-id stx "~a≦" #'name)
#'(begin
(define (fname max f)
(let loop ((x 0))
(cond ((> x max) (notfound x))
((term (f x)) (found x))
(else (loop (+ x 1))))))
(define-syntax (name stx)
(syntax-parse stx
#:literals (≦)
[(_ v:id ≦ max:expr body:expr)
#'(fname max (λ (v) body))]
;こうだった
;[(_ v1:id v2:id ≦ max:expr body:expr)
; #'(fname max (λ (v1) (fname max (λ (v2) body))))]))))))
;こうする
[(_ v:id ...+ vn:id ≦ max:expr body:expr)
#'(name v ... ≦ max (fname max (λ (vn) body)))]))))))やってみるとエラー
syntax: no pattern variables before ellipsis in template in: ...(name v ...の...がダメって言われてるっぽいです
やりたいことはこのとおりだと思うんだけど・・・
わからん
ちょっとマクロが二重になってて何がなんだかわからないので
いったんシンプルなマクロで確認します
(define-syntax (∀ stx)
(syntax-parse stx
#:literals (≦)
[(∀ v:id ≦ max:expr body:expr)
#'(_∀<= max (λ (v) body))]
[(∀ v:id ...+ vn:id ≦ max:expr body:expr)
#'(∀ v ... ≦ max (_∀<= max (λ (vn) body)))]))あれーこれだと動くなあ
いっしょじゃない？
・・・
・・・
そうか
マクロを定義するマクロで...を使うときにエスケープみたいなことするのがあった
(... ...)だ
単なる...だと、外側のsyntax-parseが展開しようとして
v?そんなパターン変数ないけど？て言ってるわけか
(... ...)なら外側のsyntax-parseがいったん...にしてくれるわけか
こうだな
[(_ v:id ...+ vn:id ≦ max:expr body:expr)
#'(name v (... ...) ≦ max (fname max (λ (vn) body)))]))))))大丈夫そうな雰囲気
やっと書けます
(define (IsElementForm x)
(∃ a b n ≦ x
(and (IsNthType a (+ n 1))
(IsNthType b n)
(= x (** a (paren b))))))まともに動きそうな気がしません
一番簡単な論理式はたぶんx2(x1)ですが
x2(x1)のゲーデル数
= 2^17^2・3^11・5^17・7^13
= 13024682419354582233779462566753686805335294697495029574927977097869102772155580534084672913040998400000000000000000ですから
DynalistのGoogle Calendar Integrationを（ちょっとだけ）試す
DynalistにはGoogle CalendarとSyncする機能があります
ただしProの機能
手帳派なのでスマホのカレンダーとか使ってないんですけど
Dynalist Proの試用期間が今日で終わりってことに気づいて
急ぎでちょっとだけ試してみることにしました
面白そうだし
まずは準備
- SettingsのDynalist ProタブでGoogle Calendar Integrationのところで
Turn on Google Calendar syncをクリック - Googleとの連携を許可
- Dynalinkに戻ってGoogle Calendar IntegrationのSync events toで
- 同期したいカレンダーを選択
どうもここでDynalistを再読込しないと現れないっぽいです
ちょっと悩みました - 同期するドキュメントを選択
Enable sync or disable sync for all documentsでEnable syncを選ぶと
全ドキュメントが同期されます
ドキュメントを右クリックして個別に同期設定することもできます
これで同期されるはず
Dynalistで !(2017-10-07 11:00 +09:00) Dynalistから というアイテムを作ると
Google Calendarの2017-10-07 11:00に「Dynalist から」というスケジュールが
入りました
詳細を見ると
作成元: Dynalist
説明: From Dynalist: #ACTIVE > #PROJECT > #Dynalist > Google Calender Integration ちょっとだけ試す > Dynalistから Link: https://dynalist.io/d/...
みたいになってます
なるほど
時間を指定しない形式 !(2017-10-07) +09:00) なら終日予定になります
+09:00はタイムゾーンの指定で９時の予定という意味ではありません
すこし時間がかかることもあるみたいです
SettingsにReflesh Calendarというのがあるので
急ぎならこれをクリックすると即反映されるということかな
Dynalist側を修正するとGoogle Calendarにも反映されます
一方、Google Calendarで入力した予定がDynalistに反映される、ってことはない模様
Dynalistで入力した予定をGoogle Calendarで修正してもDynalistには反映されないぽい
要するにDynalist→Google Calendarの一方向の同期ってことのようです
とすると、Google Calendar側で修正すると混乱しそうな気がします
Dynalist用のCalendarを作っておいて、そこはGoogle Calendar側では
見るだけ、ってことにしておいたほうが安全かな？
ほんとにちょっと試してみただけなので、もしかすると双方向に同期できるのかも
しれませんが・・・
