一阶逻辑中的几个反直觉结论
最近的Research牵涉到一些时态逻辑的东西，但推式子的时候反而发现一些很简单的一阶逻辑结论之前都没注意到，感觉自己白学了。 首先是这个 $$(\exists x. P(x)) \to Q \iff \forall x.P(x) \to Q$$ 很奇怪，为什么“任意”放进括号里就变成“存在”了呢？其实这也很好…
1,214 2023-12-03 去围观
Cairo Compiler Learning Notes
Excerpts from How Cairo Works Introduction to Cairo Registers ap: allocation pointer fp: frame pointer pc: program counter Basic instructions [fp - 1] = [ap - 2] + [fp + 4] [ap - 1] = [fp + 10] * [ap]; ap++ [ap - 1] = [fp + 10] + 12345; ap++ #…
2,767 2022-06-02 去围观Rosette Learning Notes
Excerpts from The Rosette Guide. Rosette Essentials Symbolic Values (define-symbolic b boolean?) Specification (define (check-mid impl lo hi) ; Assuming that (assume (bvsle (int32 0) lo)) ; 0 ≤ lo and (assume (bvsle lo hi)) …
2,482 2022-06-02 去围观
Notes of "The Logic of Computer Programming"
Link: The Logic of Computer Programming Four aspect: correctness termination transformation development Program A: Partial Correctness totally correct: if we execute Program A on any input satisfying the input assertion, the program will ha…
3,783 2021-11-13 去围观
