kb84tkhrのブログ

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

2017-01-01から1年間の記事一覧

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

素因数分解の本体 素因数分解は(Listof (Pairof Natural Natural))という型で表しています 0の素因数分解とか、2の素因数分解の3番目の因数とか変なやつは'(0 .0)で表しました

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

さてPが定義できたので素因数分解と定義3の再定義を まずは補助関数から

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

定義4 nの階乗 型をつけただけ

「ちょっと残業」

っていうとき、実際どれくらい残業してるか、って業界とか会社とか人によってかなり違いますよね ウチの会社でも千差万別働き方改革とは言いますがまだまだ残業が長い人も多いです そういう私は以前はけっこう長かったんですが徐々に短くなってきたり意図的…

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

というわけでマクロなし作戦

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

関数を定義したりマクロを定義したりするややこしいマクロを直すよりも まずはできそうなところからやってみます

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

では #lang typed/racket 動くだけは動いたりするかな?

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

さてTyped Racketもざっと見たので型をつけていってみます 動かせないのでテストもできませんでしたが うまく型を付けられれば静的なチェックだけでもバグが見つかるのではと(実際ときどき間違えてたし) さてどんな型をつけましょうか 型っぽいものはゲー…

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歳の娘に語るガロアの数学 再読中

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