Show newer

@SuricrasiaOnline Clearly it shifts stdout to the left 943 bits. Hope you've got those newfangled AVX modes.

C++ test! what's the output of:
std::cout << 1000 - 0100 + 0010 - 0001 << std::endl

me: i love type theory
me: *uses a proof assistant*
me, through pained breath: man

actually after he's dug out of the graves in the ground, he's not called "Frankenstein's Monster", he's called "lava"

Show thread

actually he's not called "Frankenstein's Monster", he's called "The Frankenstein"

thinking back to the guy travelling to mexico to avoid the dutch covid "hysteria". to mexico, where at each entrance there is someone to measure your temperature and force you to wash your hands and put on a mask. btw, this guy was wearing a mask incorrectly in the train while explaining this plan.

Show thread

dutch people: all foreigners are lazy, that's why the netherlands is so cool
also dutch people: i can't be bothered putting this mask over my nose

open poll what's your favorite weird cpu instruction

any architecture, any time period.

endogenous and exogenous hormones 

bleaugh hormones. can't live with em. can't live without em. amirite folxks

Show thread

anyway, the point of this story is that I want to arrange things in my Lisp so the equality-check operator, when applied to functions f g, returns the prop `∀ x, f x = g x'.

and then there can be a bit of automatic proof search that allows you to cast such props back to booleans.

Show thread

i guess the formula should look more like `∀ x, is-natural x → _' to make it true. and then we'd have to define `(is-natural x)' in a clever way so that it doesn't start by inspecting the type of `x' and see if it's an int, since `τ whatever' isn't (guaranteed to be) an int.

unless we do some evil type-level hackery? might be possible to arrange that in my Lisp.

Show thread

(τ is the dual to Hilbert's ε operator, i.e. τ P is the strongest counterexample to ∀ x, P x, so P(τ P) → ∀ x, P x. similarly, ε P is the weakest example of ∃ x, P x, so ∃ x, P x → P (ε x). and forall-elim / exists-intro turn this into a bi-implication.)

so you can just say like `∀ x, x = 0 ∨ ∃ y, x = y + 1' in this "logic" as (forall (λ (x) (or (= x 0) (exists (λ (y) (= x (+ y 1))))))), where `forall', `or' and `exists' are constructors and the rest just regular old Lisp values.

Show thread

in unrelated news, thinking about what would happen if I wrote a hol-style verifier in Lisp. and we'd use HOAS to represent propositions.

so you have a function `(verify prop proof) -> bool' that checks `proof' is a valid proof of `prop'. and `∀ x, P x' is encoded as `(forall P)', where `P' is an arbitrary one-parameter function.

and we'd just let P have side effects, since we're in Lisp.

and forall-intro would look like `(P (τ P)) → ∀ x, P x', where `τ' is just a one-field struct constructor

Show thread

this might very well become the cover image of my phd thesis at this rate :C

Show thread
Show older

Mastodon is a server for a federated social network: everyone can run a server if they want to, including me. So this is a Mastodon server for me (Vierkantor) and my friends.