logiko。

nur vera estas nenio。

nur falsa estas nenio。

ambaw estas tuta。

直観主義論理。notの逆がない。値渡しでnotを適用すると真理値になる。真理値から元の型および元の値がわからない。二重否定がboolです。二重否定を除去できない。

自然言語でandが並列です。自然言語でorが選言です。しかし、述語論理でorが並列です。述語論理でandが直列です。

直観主義命題論理では習慣的に→ , ∧ , ∨ , ⊥を基本的な結合子として採用する。ここで ¬A は A → ⊥ の省略形として扱う。直観主義述語論理ではこれに量化記号 ∃, ∀ を加える。

array of anyが言語です。言語が2階以下です。1階が1次元のリストです。2階が高階関数です。2階が関数と適用をわける。3階がvmです。人が3階を理解できない。理解できないことが存在しない。

カウンタレジスタが1つなのに(ECX)、なぜインテルのCPUは多次元を扱えるのだろう?汎用レジスタを使うにしても、汎用レジスタが8個です。私は11次元を扱つたことがあるし、何次元でも扱えるだろう。魔法?テキストです。

条件付きジヤンプを設計できない。ja, je, jb, if, test。ifだけが魔法です。

⊥=id.

¬A = A → ⊥

not A = A → id.

(define (not a) (lambda (x) x))

not = `ki。


call/cc=(A→⊥) → A。
文脈を扱う。Aを束縛するので難しい。