kb84tkhrのブログ

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

Typed Racketのお勉強 (12)

7 Optimization in Typed Racket Typed Racketは型の情報を活かして最適化を行います 最適化を止めるには#lang typed/racket #:no-optimizeを使う RealよりもFloatといったように、型を具体的に指定すると効果的 リストがnullでないことがわかっている場合は…

Typed Racketのお勉強 (11)

6 Typed-Untyped Interaction Typedじゃない普通のRacketの関数からTyped Racketの関数は普通に呼べます Typed RacketからRacketの関数を呼ぶにはrequire/typedで型を指定してやります #lang racket (provide (struct-out pt) distance) (struct pt (x y)) (…

娘がもうすぐ小4で入塾テスト受けたりするわけですがこれで実際に授業が始まると夜の8時まで塾とかになるんですよね自分の小学生の頃を思い出すとこんなんでいいんだろうかという気がしなくもないです現代の忙しすぎる子供たち、的なそこまで詰め込んではい…

TiddlyWiki 5も使ってます

パーソナルではWorkflowy依存ですがお仕事のメモには今TiddlyWiki 5を使ってますクラウドにデータは置くなってことになってるんで じゃあOneNote使えよって話ではありますがどうも生理的に合わないところがありましてグラフィカルで自由度が高くなるとどうも…

Typed Racketのお勉強 (10)

5 Occurrence Typing Occurrence Typingとはあまり聞き慣れない言葉 さらっとぐぐってみましたがそれっぽい言葉は見つかりませんでした あまり普及してない概念なのかもしれません Typed Closureってやつでも出てくるようです 無理に訳そうとせず進みます な…

Typed Racketのお勉強 (9)

4 Types in Typed Racket (続き) もうちょっと調べないともやっとするな・・・ 前回よくわからなかったのがこれ B ... BのふたつめのBがどうして必要なのかわからない (: fold-left (All (C A B ...) (-> (-> C A B ... B C) C (Listof A) (Listof B) ... B …

NHK GJ

今日はNHKで精霊の守り人の特集みたいなのやってましたね 上橋菜穂子の本を読んだのはごく最近、しかも守り人シリーズじゃなくて獣の奏者の方だったりするんですけどこのひとの書いたものなら間違いないっていう感覚です(何様 精霊の守り人シリーズはとりあ…

Typed Racketのお勉強 (8)

4 Types in Typed Racket (続き) Rest argumentsの単純なケース (この前もちょっと出てきてましたが) *で0個以上の繰り返しであることを示してます (: sum (-> Number * Number)) (define (sum . xs) (if (null? xs) 0 (+ (car xs) (apply sum (cdr xs))))…

Typed Racketのお勉強 (7)

4 Types in Typed Racket (続き) Typed Racketはパラメータ多相にも対応しています Maybeモナドっぽいもの (struct None ()) (struct (a) Some ([v : a])) (define-type (Opt a) (U None (Some a))) (struct (a) ...)は型aを引数に取った型の定義 型だけ作っ…

Typed Racketのお勉強 (6)

4 Types in Typed Racket (続き) いくつかの型を取る可能性がある変数や関数はUnion型になります > (if (even? 37) 'yes 'no) - : Symbol [more precisely: (U 'yes 'no)] 'no 'yesや'noを返す、っていうところまで見てるんですねえ ってそういうの見ないと…

小さな目標と細切れになった時間

ここんとこしばらく、小さな目標が達成するだけに近い状態なんですよね10時半には眠くて目を開けていられなくなるんで なぜだろう午後カフェインを取らないようにしたから?10時以降にスマホやノートPCを使わないようにしたから? 数学の本を読んでいるから…

失敗した

ビジネス手帳1小型版を買ったばっかりではありますが 高橋 手帳 2018年 1月始まり ウィークリー ニューダイアリー ミニ 1 黒 No.133 出版社/メーカー: 高橋書店 発売日: 2017/08/29 メディア: オフィス用品 この商品を含むブログを見る ってのがあることにい…

Typed Racketのお勉強 (5)

4 Types in Typed Racket 主な基本型はInteger, Flonum, String, Char, Boolean, ->(関数)あたりですが なんか妙に細かい型があります 数値型にPositiveとNegativeがある、くらいは理解できますが こないだ出たZero型、One型の他にもTrue型とかある、という…

こどもの国(のアイスはおいしい&ディアボロ)

今日は娘とこどもの国へ行ってきました ここの楽しみはソフトクリーム自分評価では史上最高他では知らないなめらかさなんだろうこれは こどもの国で売ってる牛乳は特別牛乳って言ってまあざっくりいうととても優れた牛乳ってことなんですが実際おいしいし で…

手帳&工作

ここ何年かビジネス手帳1ばかり、と書いておきつつ来年は小型版を使ってみることに 高橋 手帳 2018年 1月始まり ウィークリー ビジネス手帳 小型版 1 黒 No.140 出版社/メーカー: 高橋書店 発売日: 2017/08/29 メディア: オフィス用品 この商品を含むブログ…

Typed Racketのお勉強 (4)

3 Specifying Types の続き (let ([x : Number 3]) (add1 x)) は、こういう風に書くこともできます (let ([#{x : Number} 3]) (add1 x)) こちらの書き方を使うと、前者の書き方に対応してない式でも 型を示すことができます (: assert-symbols! ((Listof Any…

喜ぶべきか

今日娘からLINEがありましてね 限定BOX勧誘で選択UR取ったって言うんですよしばらくかかって貯めた石50個使って一発で この強運娘が 帰ったらそれはもう嬉しそうな顔でお出迎え寝るまでテンション上がりっぱなし ちょっと複雑なところでもあるんですけどね将…

Typed Racketのお勉強 (3)

3 Specifying Types の続き 前回、型を指定しないで定義したidの型を見るのを忘れてました > (define (id z) z) > id - : (-> Any Any) #<procedure:id> Any型というのがあるんですね 次はlambdaの修飾 > (lambda ([x : Number]) : Number (+ x 5)) - : (-> Number Number)</procedure:id>…

Typed Racketのお勉強 (2)

3 Specifying Types :を使った修飾は値の定義やローカルの定義でも使えます (let () (: x Number) (define x 7) (add1 x)) たいていのバインド式は式の中でも型を書けるようになっています (define x : Number 7) (define (id [z : Number]) : Number z) ど…

Typed Racketのお勉強 (1)

Typed RacketはRacketに型を付けたものです The Typed Racket Guideを見ながら勉強していきます 詳細はThe Typed Racket Referenceに 1 Quick Start とりあえずこれをやれと ソース先頭の#lang racketを#lang typed/racketに変える (require mod)を(require …

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

いっぱい関数出てきたなと思いましてね 以前、Scheme手習いでインタプリタ作ったときに書いたような 関数の呼び出し関係の図を作ってみようと思ったんですけどね たいへんな目に会いました 思ってたのを遥かに超えて複雑でした うまく配置してみようという気…

13歳の娘に語るガロアの数学 再読中

結局購入してあらためてゆっくり読んでます雰囲気はわかってきたと思うんですがまだところどころピンときてないところがあって全体が見えてない感じ ほんとのところはラグランジュ分解式やガロア群を自分で求めてみるくらいまでしないとピンとこないのかもし…

手帳遍歴(というほどでもない)

私の手帳は1月始まりなのでそろそろ次の手帳を考える季節ですといってもここ数年は高橋書店のビジネス手帳1ばかり 高橋 手帳 2018年 1月始まり ウィークリー ビジネス手帳1 黒 No.47 出版社/メーカー: 高橋書店 発売日: 2017/08/29 メディア: オフィス用品 …

子供にしかけてみた

今のところ途切れることなく順調に続いている小さな習慣ですが これは子供にいい習慣を身につけさせるのにも応用できるでしょうか 子供の習慣づけにも使えるかなあ - kb84tkhrのブログ とにかくやってみることにしましたうまくいかなくても泣かない さてどれ…

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

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

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))))))) こういうの見るとつい 束縛が入れ子にな…