kb84tkhrのブログ

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

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

定理証明手習い (4) J-Bob初体験

J-Bobは、ある式を別の式に書き換えるのを手助けしてくれるプログラムです。 「A 放課後」でJ-Bobの使い方が紹介されています 章の内容に沿って書かれているのでとりあえず言われるまま入れてみます > (J-Bob/step (prelude) '(car (cons 'ham '(eggs))) '()…

定理証明手習い (A) というわけで

(どういうわけ)しおり紐3本はさんでみました!

DynalistとWorkflowy

たいしたアクセスもないこのブログですがアクセス解析を見ているとここ2ヶ月くらいはずっとこの記事がアクセス数1位をキープしてますはっきり数は出ませんがアクセス数も増えてるんじゃないかなちょっとずつDynalistがポピュラーになってきてるんでしょう…

定理証明手習い (3) 「1.いつものゲームに新しいルールを」

『Scheme手習い』を読んだことは? 'nil #tですよ! ある式に等しい式は無数にあるが、値はひとつしかない 変数の値が決まってなくても式の値が決まることがある 注目する部分を「フォーカス」、その外側を「文脈」と呼ぶ フォーカスを、それに等しい式で置…

定理証明手習い (2) J-Bobを動かす

「自分で動かしながら楽しみたい」という読者のために、J-Bobという簡素な定理証明支援系を用意してあります。 必須じゃないという書き方ですね でもせっかくですから動かしてみたい まずはThe Little Proverのページにアクセスしてみます J-BobはGitHubから…

あけましておめでとうございます