Reading: Little Prover


Law of Dethm: you can swap any part of the arguments to a function with a corresponding expression, and then rewrite the function body to include those swapped args to uncover a focus:

  1. the rewritten function body bodye must have a conclusion (equal p q) or (equal q p)

  2. the conclusion can’t be in an if condition: example:

# not allowed!

if apple == fruit:
    make_pie = true
    make_compost = true

apple == fruit # QED!?


a focus is only pertinent to an if-question if the focus is contained by the if-question’s answer or if-else

That makes sense – we can’t tell anything about a focus if it’s not related to the question: for example, the focus “the ocean is blue”, has nothing to do with the question “if the sky is blue”… in this form:

if the sky is blue:
    then birds will sing gaily
        birds remain quiet
if the ocean is filled with oxygen:
    then the ocean is blue
        the fish remain quiet

The focus “the ocean is blue”–even if it shares the same idea of “blueness” with the sky–is a total non-sequiter to the if-question “if the sky is blue”.


This book started to click for me at the end of ch3. I’m still settling on a workflow for working through the proofs; I started writing directly into the repl to get the quick feedback. I’d build a proof line at a time, enter it and use the output to guide me onto the next step. Once the proof was complete, I’d define and save it in Dr Rackets editor window.


Total A function is total if it evaluates to an expression that has a value, no matter what value is passed to it.

What is (size x)?

This is not intuitive yet:

(size '(a b c))
; 3

(size '(a (b c)))
; 4

This is even less intuitive, but informative!

(size '(a (cons 'b (c))))
; 8

(size '(a (cons 'b '(c))))
; 10

So creating a list using '() is different from a cons.

(cons '() (cons '() '()))
; (() ())

(size (cons '() (cons '() '())))
; 2


Frustrating: things are starting to get interesting, but at the same LESS practical. So I wrestle with justifying the time and effort of reading, understanding, typing out and even writing about the experience of reading the book, versus making something “practical” that will “help advance my career”.