プログラミング覚えて億万長者になろうとかScratchで勉強しても役に立たないからちゃんとした言語でやろうとかそういうの聞くとそういうものかなあなんか違うなあ、と感じます 自分が思い浮かぶのはこれこういう考え方でプログラミング教育をしてくれないか…

っていう話はここまで変形しないと言えないもの？ (if (atom x) 't (if (atom (car x)) 't (< (size (cons (car (car x)) (cons (cdr (car x)) (cdr x)))) (size (cons (cons (car (car x)) (cdr (car x))) (cdr x)))))) 反例なら上に上げた主張の時点でもう…

alignか それだ見覚えあったのは 確かそのときも全関数であることの証明だった

ついに10章 （といってもラスボスは付録Cにいると思われる） rotate なんかこの動きは見たことがある 全体的に言えばrotateしてる感じはあるけど ミクロに言うと何がどうなっているのかな コンスの数は4

先日マシュマロで紹介した『ちょっとしたことでうまくいく 発達障害の人が上手に働くための本 』が翔泳社さんですね。あと『実用Common Lisp』はすごく勉強になりました。#マシュマロを投げ合おう https://t.co/lFQLu8QvFo pic.twitter.com/Z5ZqWOGCKM — 読…

set?/t-nilも普通に証明できるかな できない理由は思いつかない set?/tとset?/nilをあわせた手間よりは楽にできるんじゃないかな やってみよう

A部はset?を展開して整理するだけ すぐ終わる E部はやっぱりまず前提をスルーしてその内側から set?を展開して (atom xs)を整理して (member? (car xs) (cdr xs))で持ち上げて (set? (cdr xs))で持ち上げて 整理してやるだけ

set?/tとかset?/nilを証明しないといけませんかね。 そうですよ！ 178ページです。 そんだけ 自力でやってみるかな できるとわかってるだけでも足しになる 新しい技も覚えたし（使うかどうかわからないけど

set?/atomの定理に戻りましょう。 え、そっち？ set?/tとかset?/nilは？ この定理の証明は、ちょっとだけ意外で、ちょっとだけ楽しく、ちょっとだけで終わります。 set?/add-atomsの特殊ケースにすぎないのでちょっとだけで終わりそうな予感はしますが 意外…

下記にオレンジ色で示したif式のQuestion部は、どちらも同じ(set? (add-atoms (cdr a) bs))という意味です。 知ってた しかし、if-nest-Aやif-nest-Eで単純な形にはできません。 先に言ってくれ！

テキストに沿って証明を進めます ここ、自分で考えたらやっぱりけっこう大変なんだろうなあ

Scrapboxが楽しいんですがWorkflowyも捨てがたいどうしたものですかね

Defun帰納法はかなり適用範囲が広そうなやり方です Defun帰納法は、自分たちで書くどんな関数でも使えるのでしょうか？ 帰納的な主張を構成する方法にしろ、全域性の主張を構成する方法にしろ、どんな関数に対しても構成はできます。 ifの位置にもよるけど持…

リスト型帰納法やスター型帰納法はDefun帰納法に含まれるそうです リスト型帰納法はlist-inductionから作ります

Defun式帰納法、とか言ってまた難しく書いてあります ていうか前よりわからないので今回も定義にしたがって追ってみます

ということでadd-atoms用の帰納法が作れるのならどんなものでしょうか list-inductionのときは主張を読んでみたら普通に帰納法だねって感じだったので まず自分で普通に考えてみます

今は所謂月間横ケイ、週間レフト式の手帳を使っているんですけれどもね せっかく月間ページが横ケイで、レフト式の左側と同じ並び方になっているんですから週間と同じように右ページをメモにしてほしいんですよ右ページがメモになっていれば、月の目標とかタ…

スター型でダメならどうすればいいのでしょうか ここではadd-atomsで使われている再帰について考えます add-atomsで使われている再帰は「自然な再帰」でしょうか carやcdrをたどっていく再帰に比べれば複雑ですが 不自然かというとそうでもない気もします

8章から続いて、atoms関連の関数・定理について考えていきます set?はmember?を呼び出しているのでだんだんこの世界も複雑になってきました set?、member?、add-atomsの全域性については8章で証明済みです

今日は少し時間取ってScrapboxに50ページほど書いてみました50ページと言ってもほとんどが数行のページなんで量としてはたいしたことはありません ちょっと書いてはキーワードをリンクにしてクリック、をとりとめもなく続けているとなんかいろいろ出てきて楽…

8章では関数の全域性の主張の作り方をやりました 9章では定理の帰納法の作り方をやります 具体的に言うと、list-inductionとかstar-inductionに当たるものを作るということです いやちょっと違うな

っていう話を 関数 (defun name (x1 ... xn) body) および尺度 m が与えられたら、 body の部分式に対して次のようにして主張を構成する。 とか言って難しく書いてあります 難しいのでadd-atomsを1字1句このとおりにやってみます

小さな習慣を始めて半年が経ちました 早いなあ初期の目標はいまもそのままでレベルアップさせたりはしていません

はじめました scrapbox.io 今のところちょっとお試しというレベル Scrapboxって何かって言うとひとことで言えばモダンなWiki？で合ってる？

8章では全域性の主張の作り方をやるんでした 題材はこれ

まずmember?とset?の定義が出てきますがこれは下準備 いままでどおりにやるだけです (if (natp (size ys)) ...)は定理にしておきますね

次のフォーカスでctx?/tを使えるでしょうか？ はい、オレンジ色で示したぜんていがあるので使えます。あとでctx?/tの証明はしないといけませんけどね。 あとでいいんだっけ？

これは以前行きづまった(if (equal x '()) 't 'nil)を(equal x '())に変形するにちょっと似てる？ 定理証明手習い (28) 補助定理 - kb84tkhrのブログ さて(if (equal a b) 't 'nil)はどうかな

前回の記事書いてみて思ったのは ((A A 1 1) (equal-if x '?))とかを並べて書いてあるコードを見るより 途中経過の式を並べたものを見るほうがわかりやすいなってこと

(ctx? x)という前提が真の場合、そのifのAnswer部にある(ctx? x)を'tに置き換えられるでしょうか？ む これは以前行きづまった (if (equal x '()) 't 'nil)を(equal x '())に変形する にちょっと似てる？ 置き換えてよいのではないでしょうか。真である前提…